cnf, predicate resolution

src/main/scala/de/tum/workflows/foltl/FOLTL.scala

@@ -15,10 +15,12 @@ object FOLTL {
     def in(name: String) = FormulaFunctions.annotate(this, name)
     def in(name: String, ignore: Set[String]) = FormulaFunctions.annotate(this, name, ignore)
     def collect[T](coll: PartialFunction[Formula, List[T]]) = FormulaFunctions.collect(coll, this)
+    def hasSubFormula(coll: PartialFunction[Formula, Boolean]) = FormulaFunctions.hasSubFormula(coll, this)
     def opsize() = FormulaFunctions.opsize(this)
     
     def toPrenex() = FormulaFunctions.toPrenex(this)
     def toNegNf() = FormulaFunctions.toNegNf(this)
+    def toCNF() = FormulaFunctions.toCNF(this)
     def isBS() = FormulaFunctions.isBS(this)
     
     def removeOTQuantifiers() = FormulaFunctions.removeOTQuantifiers(this)

src/main/scala/de/tum/workflows/foltl/FOLTLTermFunctions.scala

@@ -50,6 +50,8 @@ object FormulaFunctions extends LazyLogging {
       case And(t, False)                      => False
       case And(True, t)                       => t
       case And(t, True)                       => t
+      
+//      case Or(t1, Neg(t2)) if t1 == t2        => True
 
       // Equivalence
       case Eq(t1, t2) if t1 == t2             => True
@@ -63,9 +65,11 @@ object FormulaFunctions extends LazyLogging {
       case Quantifier(_, _, True)             => True
       case Quantifier(_, _, False)            => False
 
-      // TODO: Double quantifiers
+      // Gobble up equal quantifiers
+      case Forall(vars1, Forall(vars2, f))    => Forall(vars1 ++ vars2, f)
+      case Exists(vars1, Exists(vars2, f))    => Exists(vars1 ++ vars2, f)
 
-      // Remove variables from quantifiers if not used in the body
+      // Remove variables from quantifiers if not used in the body: Caution - expensive
       //      case Quantifier(qmake, xs, t) if !(xs.toSet -- t.freeVars()).isEmpty =>
       //        qmake((xs.toSet.intersect(t.freeVars())).toList, t)
       //
@@ -109,16 +113,16 @@ object FormulaFunctions extends LazyLogging {
     }
   }
 
-  def collect[T](combine: (T*) => T, empty: T)(coll: PartialFunction[Formula, T], t: Formula): T = {
+  def collect[T](combine: (T*) => T)(coll: PartialFunction[Formula, T], t: Formula): T = {
     if (coll.isDefinedAt(t))
       coll(t)
     else
       t match {
         // Extractors
-        case Quantifier(make, ps, t) => collect(combine, empty)(coll, t)
-        case UnOp(make, t)           => collect(combine, empty)(coll, t)
-        case BinOp(make, t1, t2)     => combine(collect(combine, empty)(coll, t1), collect(combine, empty)(coll, t2))
-        case x                       => empty
+        case Quantifier(make, ps, t) => combine(collect(combine)(coll, t))
+        case UnOp(make, t)           => combine(collect(combine)(coll, t))
+        case BinOp(make, t1, t2)     => combine(collect(combine)(coll, t1), collect(combine)(coll, t2))
+        case x                       => combine()
       }
   }
 
@@ -134,16 +138,35 @@ object FormulaFunctions extends LazyLogging {
         case x                       => List.empty
       }
   }
+  
+  def hasSubFormula(coll: PartialFunction[Formula, Boolean], t: Formula) = {
+    def or(bs:Boolean*) = { bs.exists(identity) }
+    collect(or)(coll, t)
+  }
+  
+//  def hasSubFormula(check: (Formula => Boolean), t: Formula): Boolean = {
+//    if (check(t)) {
+//      true
+//    } else {
+//      t match {
+//        // Extractors
+//        case Quantifier(make, ps, t) => hasSubFormula(check, t)
+//        case UnOp(make, t)           => hasSubFormula(check, t)
+//        case BinOp(make, t1, t2)     => hasSubFormula(check, t1) || hasSubFormula(check, t2)
+//        case x                       => false
+//      }
+//    }
+//  }
 
   def assumeEmpty(t: Formula, name: String) = {
     t.everywhere({
       case Fun(f, _, _) if f == name => False
     })
   }
-  
-  def assumeAllEmpty(f:Formula, names:List[String]) = {
+
+  def assumeAllEmpty(f: Formula, names: List[String]) = {
     // Assume all workflow relations empty
-    val assumers = names.map(p => (f: Formula) => assumeEmpty(f,p))
+    val assumers = names.map(p => (f: Formula) => assumeEmpty(f, p))
     val allempty = assumers.reduce(_ andThen _)(f)
     allempty.simplify()
   }
@@ -217,8 +240,8 @@ object FormulaFunctions extends LazyLogging {
       case Quantifier(_, _, fsub) => stripQuantifiers(fsub)
     }
   }
-  
-    def collectQuantifiersSub(f: Formula): List[(Boolean, Formula => Quantifier)] = {
+
+  def collectQuantifiersSub(f: Formula): List[(Boolean, Formula => Quantifier)] = {
     f collect {
       case Exists(xs, fsub) => List((true, (t: Formula) => (Exists(xs, t)))) ++ collectQuantifiersSub(fsub)
       case Forall(xs, fsub) => List((false, (t: Formula) => (Forall(xs, t)))) ++ collectQuantifiersSub(fsub)
@@ -243,16 +266,16 @@ object FormulaFunctions extends LazyLogging {
   def collectQuantifiers(f: Formula) = {
     collectQuantifiersSub(f).map(_._2)
   }
-  
-  def isBS(f:Formula) = {
+
+  def isBS(f: Formula) = {
     val quantprefix = collectQuantifiersSub(f.toNegNf())
     // has no forall exists in quantifier prefix
     !quantprefix.sliding(2).exists(list => !list(0)._1 && list(1)._1)
   }
-  
-  def toNegNf(f:Formula) = {
+
+  def toNegNf(f: Formula) = {
     val bound = if (hasDuplicateBindings(f)) {
-//      logger.info(s"Formula binds variables more than once - renaming bindings: ${f.pretty}")
+      //      logger.info(s"Formula binds variables more than once - renaming bindings: ${f.pretty}")
       FormulaFunctions.fixBinding(f, Set())._1
     } else f
     eliminateImplication(bound).simplify()
@@ -309,4 +332,62 @@ object FormulaFunctions extends LazyLogging {
 
     quants.foldRight(stripped)((quant, inner) => quant(inner))
   }
+
+  def toCNF(f: Formula) = {
+    def toCNFSub(f: Formula): Formula = {
+      f.everywhere({
+        case Or(And(f1, f2), f3) => And(toCNFSub(Or(f1, f3)), toCNFSub(Or(f2, f3)))
+        case Or(f1, And(f2, f3)) => And(toCNFSub(Or(f1, f2)), toCNFSub(Or(f1, f3)))
+      })
+    }
+
+    // FIXME: can we do it without prenex? may be expensive later on
+    val normalized = f.toNegNf().toPrenex()
+
+    // normalized is now Quantifiers, then only And/Or with Negation inside
+    toCNFSub(normalized)
+  }
+  
+  /**
+   * Resolves a universally quantified predicate
+   * Blows up the formula linearly due to CNF
+   */
+  def eliminatePredicate(f:Formula, name: String) = {
+    def listFunsWithName(f:Formula, name:String) = {
+      f.collect({
+        case Fun(n, ind, vars) if n == name => List((Some(Fun(n, ind, vars)), None))
+        case Neg(Fun(n, ind, vars)) if n == name => List((None, Some(Neg(Fun(n, ind, vars)))))
+      })
+    }
+  
+    val norm = f.toCNF()
+    
+    val removed = norm.everywhere({
+      // find top-level ORs in CNF
+      case inner:Or => {
+        val list = listFunsWithName(inner, name)
+        
+        val positives = list.map(_._1).flatten
+        val negatives = list.map(_._2).flatten
+        
+        val isSuperFluous = positives.exists { f1 => 
+          negatives.exists { f2 => Neg(f1) == f2 }
+        }
+        
+        if (isSuperFluous) {
+          // Remove clause
+          True
+        } else {
+          // Remove predicate both in positive and negative
+          inner.everywhere ({
+            case Neg(Fun(n, ind, vars)) if n == name => False
+            case Fun(n, ind, vars) if n == name => False
+          })
+        }
+      }
+    })
+    
+    removed.simplify()
+    
+  }
 }
\ No newline at end of file

src/main/scala/de/tum/workflows/ltl/LTL.scala

@@ -26,6 +26,10 @@ object LTL extends LazyLogging {
     }
   }
   
+  /**
+   * Gobble up all outermost existential quantifiers
+   * Needs to have non-conflicting bindings
+   */
   def eliminateExistentials(t:Formula) = {
     
     def coll:PartialFunction[Formula, List[Var]] = {
@@ -91,6 +95,9 @@ object LTL extends LazyLogging {
     })
   }
   
+  /**
+   * Replace function calls Fun("f", List("x")) by Var("f_x")
+   */
   def eliminatePredicates(t: Formula) = {
     t.everywhere({
       case Fun(f, ind, tup) => {
@@ -100,4 +107,32 @@ object LTL extends LazyLogging {
     })
   }
   
+  /**
+   * Instantiates universals in EA formulae.
+   * Does not change quantifier structure, but returns formula in NegNF
+   */
+  def instantiateUniversals(f:Formula) = {
+    // Check fragment
+    if (!f.isBS()) {
+      logger.error("Trying to instantiate Universals for wrong fragment")
+      logger.error(s"Formula was $f")
+    }
+    
+    val nf = f.toNegNf()
+    val (agents, inner) = LTL.eliminateExistentials(nf)
+    val existbound = Exists(agents, inner)
+    LTL.eliminateUniversals(existbound, agents)    
+  }
+  
+  /**
+   * Instantiates inner Existentials in AE formulae.
+   * Does not change quantifier structure, but returns formula in NegNF
+   */
+  def instantiateInnerExistentials(f:Formula) = {
+    val neg = Neg(f).toNegNf()
+    
+    val res = instantiateUniversals(neg)
+    Neg(res).toNegNf()
+  }
+  
 }
\ No newline at end of file

src/main/scala/de/tum/workflows/toz3/InvariantChecker.scala

@@ -58,7 +58,7 @@ object InvariantChecker extends LazyLogging {
       }
     } else precond
     
-    // TODO: do not do this here
+    // TODO: do we do this here?
     val firstprecond = if (isfirst) {
       stubprecond.assumeEmpty(sig.preds.map(_.name).toList)
     } else { stubprecond }
@@ -78,11 +78,7 @@ object InvariantChecker extends LazyLogging {
       logger.error(s"Not in BS: Invariant implication ${tocheck.pretty}")
     }
 
-    val negnf = tocheck.toNegNf()
-
-    val (agents, inner) = LTL.eliminateExistentials(negnf)
-    val existbound = Exists(agents, inner)
-    val univfree = LTL.eliminateUniversals(existbound, agents)
+    val univfree = LTL.instantiateUniversals(tocheck)
 
     //      val test3 = univfree.pretty()
     //      println(test3)

src/test/scala/Test.scala

@@ -11,31 +11,36 @@ import com.microsoft.z3.Model
 
 object Test extends App {
   
-  val TIMEOUT = 30000 // in milliseconds
-
-  val easyForm = Exists(List("x"), And(Fun("p", List("x")), Next(Neg(Fun("p", List("x"))))))
-
-  val cfg = new HashMap[String, String]()
-  cfg.put("timeout", TIMEOUT.toString())
-
-  val ctx = new Context(cfg)
-
-  val qe = ctx.mkTactic("qe")
-  val default = ctx.mkTactic("smt")
-  val t = ctx.andThen(qe, default)
-
-  val s = ctx.mkSolver(t)
-
-  s.add(toZ3.translate(easyForm, ctx))
-  val c = s.check()
-  val model = s.getModel()
-  
-  println(s"Z3 model:\n${model}")
-  
-  val consts = model.getConstDecls()
-  println(consts(0).getName)
+    println(List(true, false, false).reduceLeft(_ && _))
+    println(List(true).reduceLeft(_ && _))
+    println(List(false).reduceLeft(_ && _))
+    println(List().foldLeft(true)((_:Boolean) && (_:Boolean)))
   
-  println("MODEL:")
-  toZ3.printModel(model)
+//  val TIMEOUT = 30000 // in milliseconds
+//
+//  val easyForm = Exists(List("x"), And(Fun("p", List("x")), Next(Neg(Fun("p", List("x"))))))
+//
+//  val cfg = new HashMap[String, String]()
+//  cfg.put("timeout", TIMEOUT.toString())
+//
+//  val ctx = new Context(cfg)
+//
+//  val qe = ctx.mkTactic("qe")
+//  val default = ctx.mkTactic("smt")
+//  val t = ctx.andThen(qe, default)
+//
+//  val s = ctx.mkSolver(t)
+//
+//  s.add(toZ3.translate(easyForm, ctx))
+//  val c = s.check()
+//  val model = s.getModel()
+//  
+//  println(s"Z3 model:\n${model}")
+//  
+//  val consts = model.getConstDecls()
+//  println(consts(0).getName)
+//  
+//  println("MODEL:")
+//  toZ3.printModel(model)
   
 }
\ No newline at end of file

src/test/scala/de/tum/workflows/ltl/tests/FOLTLTest.scala

@@ -74,4 +74,24 @@ class FOLTLTest extends FlatSpec {
     f.toPrenex() should be (Exists("z", Forall("a", And("a", "z"))))
   }
   
+  it should "compute CNF" in {
+    val f = Or(And("a", "b"), And("c","d"))
+    
+    f.toCNF() should be (
+      And(
+          And(Or("a", "c"), Or("a","d")), 
+          And(Or("b","c"), Or("b","d"))
+      )    
+    )
+  }
+  
+  it should "compute CNF for formulas with quantifiers" in {
+    val f = Or(And(Exists("c", "c"), "b"), And(Exists("c", "c"),"d"))
+    f.toCNF().simplify() should be (
+      Exists(List("c", "c1"), And(
+          And(Or("c", "c1"), Or("c","d")), 
+          And(Or("b","c1"), Or("b","d"))
+      ))    
+    )
+  }
 }
\ No newline at end of file

src/test/scala/de/tum/workflows/ltl/tests/LTLTests.scala

@@ -8,6 +8,7 @@ import de.tum.workflows.foltl.FOLTL._
 import de.tum.workflows.ltl.LTL
 import de.tum.workflows.Implicits._
 import de.tum.workflows.WorkflowParser
+import de.tum.workflows.foltl.FormulaFunctions
 
 class LTLSpec extends FlatSpec {
 
@@ -65,5 +66,59 @@ class LTLSpec extends FlatSpec {
     )
   }
   
+  "Existential Elimination" should "work in AE formulae" in {
+    val f = Forall(List("x","y"), Exists("z", Fun("f", List("x","z"))))
+    
+    LTL.instantiateInnerExistentials(f) should be (
+      Forall(List("x","y"), Or(Fun("f", List("x","x")), Fun("f", List("x","y")))) 
+    )
+   }
+  
+  "hasSubFormula" should "find subformulas" in {
+    val f = Forall(List("x","y"), Exists("z", Fun("f", List("x","z"))))
+    val f2 = And("b", Or("c", f))
+    
+    f2.hasSubFormula({
+      case inner if f == inner => true
+    }) should be (true)
+    
+        
+    f2.hasSubFormula({
+      case inner if f == inner => false
+    }) should be (false)
+    
+    f2.hasSubFormula({
+      case something => false
+    }) should be (false)
+    
+    f2.hasSubFormula({
+      case And(f1, f2) => true
+      case Forall(vars, f) => false
+    }) should be (true)
+    
+    f2.hasSubFormula({
+      case Forall(vars, f) => true
+    }) should be (true)
+  }
+  
+  "removePredicate" should "remove correct things" in {
+    val f = And(Or(Fun("f", "x"), Neg(Fun("f","x"))), "y")
+    
+    FormulaFunctions.eliminatePredicate(f, "f") should be (
+      Var("y")    
+    )
+    
+    val f2 = And(Or(Fun("f", "x"), Neg(Fun("f","y"))), "z")
+    
+    FormulaFunctions.eliminatePredicate(f2, "f") should be (
+      False
+    )   
+    
+    val f3 = Forall("x", And(Or(Fun("f", "x"), Neg(Fun("f","y"))), "z"))
+    
+    FormulaFunctions.eliminatePredicate(f3, "f") should be (
+      False
+    )  
+  }
   
 }
\ No newline at end of file