fork(4) download
copy 
  1. import scala.util.parsing.combinator._
  2.  
  3. abstract class Expr
  4. case class Const(value: Boolean) extends Expr
  5. case class Atom(name: String) extends Expr
  6. case class Not(expr: Expr) extends Expr
  7. case class And(left: Expr, right: Expr) extends Expr
  8. case class  Or(left: Expr, right: Expr) extends Expr
  9. case class Iff(left: Expr, right: Expr) extends Expr
  10. case class Imp(left: Expr, right: Expr) extends Expr
  11.  
  12. class MyParser extends JavaTokenParsers {
  13.  
  14.     def expr = chainl1(term, parseIffImp) ; def parseIffImp = "<=>" ^^^ {Iff} | "=>" ^^^ {Imp}
  15.     def term = chainl1(factor, parseAndOr) ; def parseAndOr = "/\\" ^^^ {And} | "\\/" ^^^ {Or}
  16.     def factor: Parser[Expr] = "~" ~> factor ^^ {Not} | primary 
  17.     def primary = "#T" ^^^ {Const(true)} | "#F" ^^^ {Const(false)} | ident ^^ {Atom} | "(" ~> expr <~ ")"
  18. }
  19.  
  20. object Main extends MyParser {
  21.  
  22.     def toStr(expr: Expr, p: Int, r: Int): String = {
  23.  
  24.         def par(p0: Int, s: String) = if (p > p0 || (p == p0 && r == 1)) s else ""
  25.  
  26.         expr match {
  27.             case Const(true) => "#true" case Const(false) => "#false"
  28.             case Atom(name) => name case Not(e) => "~" + toStr(e,3,r)
  29.             case And(e1, e2) => par(2,"(") + toStr(e1,2,0) + "/\\" + toStr(e2,2,1) + par(2,")")
  30.             case  Or(e1, e2) => par(2,"(") + toStr(e1,2,0) + "\\/" + toStr(e2,2,1) + par(2,")")
  31.             case Imp(e1, e2) => par(1,"(") + toStr(e1,1,0) + "=>"  + toStr(e2,1,1) + par(1,")")
  32.             case Iff(e1, e2) => par(1,"(") + toStr(e1,1,0) + "<=>" + toStr(e2,1,1) + par(1,")") }
  33.     }
  34.  
  35.     def simplify(expr: Expr): Expr = {
  36.  
  37.         def simplifyH(expr: Expr) = expr match {
  38.             case Not(   Const(true))  => Const(false) case Not(Const(false))    => Const(true)
  39.             case And(p, Const(false)) => Const(false) case And(Const(false), p) => Const(false)
  40.             case And(p, Const(true))  => p            case And(Const(true),  p) => p
  41.             case  Or(p, Const(false)) => p            case  Or(Const(false), p) => p
  42.             case  Or(p, Const(true))  => Const(true)  case  Or(Const(true),  p) => Const(true)
  43.             case Imp(p, Const(true))  => Const(true)  case Imp(Const(true),  p) => p
  44.             case Imp(p, Const(false)) => Not(p)       case Imp(Const(false), p) => Const(true)
  45.             case Iff(p, Const(true))  => p            case Iff(Const(true),  p) => p
  46.             case Iff(p, Const(false)) => Not(p)       case Iff(Const(false), p) => Not(p)                
  47.             case Not(Not(p)) => p                     case e => e }
  48.  
  49.         expr match {
  50.             case Not(p)    => simplifyH(Not(simplify(p)))
  51.             case And(p, q) => simplifyH(And(simplify(p), simplify(q)))
  52.             case  Or(p, q) => simplifyH( Or(simplify(p), simplify(q)))
  53.             case Iff(p, q) => simplifyH(Iff(simplify(p), simplify(q)))
  54.             case Imp(p, q) => simplifyH(Imp(simplify(p), simplify(q))) case e => e }
  55.     }
  56.  
  57.     def nnf(expr: Expr): Expr = expr match {
  58.         case And(p, q) => And(nnf(p), nnf(q)) case  Or(p, q) =>  Or(nnf(p), nnf(q))
  59.         case Imp(p, q) =>  Or(nnf(Not(p)), nnf(q))
  60.         case Iff(p, q) =>  Or(And(nnf(p), nnf(q)), And(nnf(Not(p)), nnf(Not(q))))
  61.         case Not(Not(p)) => nnf(p)
  62.         case Not(And(p, q)) =>  Or(nnf(Not(p)), nnf(Not(q)))
  63.         case Not( Or(p, q)) => And(nnf(Not(p)), nnf(Not(q)))
  64.         case Not(Imp(p, q)) => And(nnf(p), nnf(Not(q)))
  65.         case Not(Iff(p, q)) =>  Or(And(nnf(p), nnf(Not(q))), And(nnf(Not(p)), nnf(q))) case e => e }
  66.  
  67.     def cnf(expr: Expr): Expr = {
  68.  
  69.         def distr(expr: Expr): Expr = expr match {
  70.             case Or(And(p, q), And(r, s)) => And(And(distr(Or(p, r)), distr(Or(p, s))), 
  71.                                                  And(distr(Or(q, r)), distr(Or(q, s))))
  72.             case Or(p, And(q, r)) => And(distr(Or(p, q)), distr(Or(p, r)))
  73.             case Or(And(p, q), r) => And(distr(Or(p, r)), distr(Or(q, r))) case e => e }
  74.  
  75.         expr match {
  76.             case  Or(p, q) => distr(Or(cnf(p), cnf(q))) case And(p, q) => And(cnf(p), cnf(q)) case e => e }
  77.     }
  78.  
  79.     def lcnf(expr: Expr): List[List[Expr]] = {
  80.  
  81.         def lcnfH1(list: List[Expr], expr: Expr): List[Expr] = expr match {
  82.             case And(p, q) => list ::: lcnfH1(List(), p) ::: lcnfH1(List(), q) case e => e :: list }
  83.         def lcnfH2(list: List[Expr])(expr: Expr): List[Expr] = expr match {
  84.             case Or(p, q) => list ::: lcnfH2(List())(p) ::: lcnfH2(List())(q) case e => e :: list }
  85.  
  86.         lcnfH1(List(), expr) map lcnfH2(List())_
  87.     }
  88.  
  89.     def resolution(clist: List[List[Expr]]): Boolean = {
  90.  
  91.         def isAtom(expr: Expr) = expr match { case Atom(_) => true case _ => false }
  92.         def removeNot(expr: Expr) = expr match { case Not(p) => p 
  93.             case Const(false) => Const(true) case Const(true) => Const(false) }
  94.         def splitClause(clause: List[Expr]) = {
  95.             val (pos, neg) = clause partition (isAtom _) ; List(pos, neg map (removeNot _)) }
  96.         def isTrueClause(clause: List[Expr]) = { val List(lits, nlits) = splitClause(clause)
  97.             ((lits map ((e: Expr) => nlits exists ( _ == e))) :\ false)(_||_) }
  98.         def isLitTrueClause(clause: List[Expr]) = clause match {
  99.             case List(Const(true)) => true case List(Not(Const(false))) => true case _ => false }
  100.         def simplifyClause(clause: List[Expr]) = if (isTrueClause(clause)) List(Const(true)) else clause
  101.         def simplifyLcnf(clist: List[List[Expr]]) = {
  102.             (clist map (simplifyClause _)) remove (isLitTrueClause _) }
  103.         def negateLit(e: Expr) = e match { case Not(p) => p case p => Not(p) }
  104.  
  105.         def s2l[T](set: Set[T]) = set.toList ; def l2s[T](list: List[T]) = list.toSet
  106.  
  107.         def resolutionH2(tp4: (List[Expr], List[List[Expr]], List[List[Expr]], Boolean), lit: Expr) = {
  108.             val (c, cs, d, b) = tp4 ; if (d == List()) (c, cs, d, b) else {
  109.                 val nlit = negateLit(lit) ; val c1 = c diff List(lit)
  110.                 val cs1 = (cs filter ((c: List[Expr]) => c exists (_ == nlit))) map (_ diff List(nlit))
  111.                 var d1 = cs1 map (_ ::: c1) ; val cs2h = ((cs map l2s) union (d1 map l2s)).distinct
  112.                 val cs2 = (cs2h map s2l) remove (isTrueClause _) ; d1 = cs2 diff cs
  113.                 val b1 = if (d1.isEmpty) false else (d1 exists (_ == List()) ) ; (c, cs2, d1, b1) 
  114.             }
  115.         }
  116.  
  117.         def resolutionH1(c: List[Expr], cs: List[List[Expr]], d: List[List[Expr]], b: Boolean): Boolean =
  118.             (c, cs, d, b) match {
  119.                 case (_, List(), _, _) => false case (_, _, _, true) => true
  120.                 case (List(), c::cs, d, b) => resolutionH1(c, cs, d, b)
  121.                 case (c, cs, d, b) => { 
  122.                     val (c1, cs1, d1, b1) = ((c, cs, d ++ List(List(Atom(""))), b) /: c)(resolutionH2)
  123.                     resolutionH1(List(), cs1, d1, b1) } }
  124.  
  125.         clist match {
  126.             case List(Const(false)::rest) => true 
  127.             case _ => resolutionH1(List(), simplifyLcnf(clist) map 
  128.                 ((c: List[Expr]) => s2l(l2s(c))), List(), false) }        
  129.     }
  130.  
  131.     def main(args: Array[String]) {
  132.  
  133.         var input = ""
  134.  
  135.         do  { input = readLine() ; if (input != null && input != "") {
  136.  
  137.             val output = parseAll(expr, input) match {
  138.                 case Failure(msg, _) => "failure: " + msg case Error(msg, _) => "error: " + msg
  139.                 case Success(parsed, _) => {
  140.                     val nResRet = resolution(lcnf(cnf(simplify(nnf(simplify(Not(parsed)))))))
  141.                     val pResRet = resolution(lcnf(cnf(simplify(nnf(simplify(parsed))))))
  142.                     toStr(parsed, 0, 0) + "\n" + 
  143.                         (if (nResRet) "true" else if (pResRet) "false" else "it depends")
  144.                 }
  145.             }
  146.  
  147.             println(output) }
  148.         } while (input != null && input != "")
  149.     }
  150. }
Success #stdin #stdout 0.52s 248448KB
comments (?)
stdin
copy 
(a\/b)/\(a=>c)/\(b=>c)=>c
~((a\/b)/\(a=>c)/\(b=>c)=>c)
a/\b/\c=>a\/b\/c
a\/b=>a/\b
a\/~a<=>#T
b/\~b<=>#F
((a/\b)=>c)<=>(a=>(b=>c))
a/\b\/~a\/~b
((a\/b)=>c)<=>(a=>(b=>c))
a/\b/\c<=>~(a\/b\/c)
stdout
copy 
a\/b/\(a=>c)/\(b=>c)=>c
true
~(a\/b/\(a=>c)/\(b=>c)=>c)
false
a/\b/\c=>a\/b\/c
true
a\/b=>a/\b
it depends
a\/~a<=>#true
true
b/\~b<=>#false
true
a/\b=>c<=>(a=>(b=>c))
true
a/\b\/~a\/~b
true
a\/b=>c<=>(a=>(b=>c))
it depends
a/\b/\c<=>~(a\/b\/c)
it depends
https://ideone.com/P2deE
language:
Scala (scala 2.12.8)
created:
11 years ago
visibility:
secret

Share or Embed source code

Discover > Sphere Engine API

The brand new service which powers Ideone!

Discover > IDE Widget

Widget for compiling and running the source code in a web browser!