cnf stuff

src/main/scala/de/tum/workflows/MainInvariantsInference.scala

@@ -32,10 +32,8 @@ object MainInvariantsInference extends App with LazyLogging {
     )
 
     val inv = invariant(spec)
-    val (res, graph, labels, t) = InvariantChecker.checkInvariantFPHeadLabel(spec, inv, props)
-
-    logger.info(s"Invariant was ${inv}")
-    logger.info(s"Invariant was ${if (res) "" else "not "}proven (took $t ms)\n")
+//    val (res, graph, labels, t) = InvariantChecker.checkInvariantFPHeadLabel(spec, inv, props)
+    val res = Utils.check("tests/conference_linear_small", "elimB", inv, props)
 
   }
 

src/main/scala/de/tum/workflows/Preconditions.scala

@@ -185,12 +185,12 @@ object Preconditions extends LazyLogging {
         // FIXME: better recognition of Bs
         case Fun(name, _, _) if name.startsWith("B") => List(name)
       }).toSet
-      val eliminv = bs.foldRight(universalinv)((b, inv) => FOTransformers.eliminateBPredicate(inv, b)._1)
+      val eliminv = bs.foldRight(auxless)((b, inv) => FOTransformers.eliminateBPredicate(inv, b)._1)
       eliminv
     } else {
-      universalinv
+      auxless
     }
 
-    auxless.simplify()
+    bless.simplify()
   }
 }
\ No newline at end of file

src/main/scala/de/tum/workflows/Utils.scala

@@ -4,9 +4,11 @@ import de.tum.workflows.blocks._
 import de.tum.workflows.foltl.FOLTL._
 import java.io.File
 import java.io.PrintWriter
+
 import de.tum.workflows.toz3.InvariantChecker
 import de.tum.workflows.toz3.InvProperties
 import com.typesafe.scalalogging.LazyLogging
+import de.tum.workflows.MainInvariantsInference.logger
 
 object Utils extends LazyLogging {
 
@@ -75,6 +77,10 @@ object Utils extends LazyLogging {
     // do not blow up the formula with auxilliary elimination
     val (res, graph, labelling, provens, dot, time) =
       InvariantChecker.checkInvariantFPLabelling(spec, inv, properties)
+
+    logger.info(s"Invariant was ${inv}")
+    logger.info(s"Invariant was ${if (res) "" else "not "}proven (took $time ms)\n")
+
     for ((s, i) <- dot.zipWithIndex) {
       Utils.write(name,s"${filenames}_$i.dot", s)
     }

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

@@ -37,8 +37,11 @@ object FOTransformers extends LazyLogging {
       case Quantifier(vars, make, t) => collectMultiClause(t)
       case t => List(collectClause(t))
     }
-    
-    collectMultiClause(f)
+    f match {
+      case True => List()
+      case False => List(List())
+      case _ => collectMultiClause(f)
+    }
   }
   
   def eliminateDoubleQuantifiers(f:Formula) = {
@@ -64,6 +67,7 @@ object FOTransformers extends LazyLogging {
     repld.simplify()
   }
 
+  // TODO: What to do with B(T1) and B(T2) instead of this?
   def eliminateBPredicate(f:Formula, B:String) = {
     // SOQE: \exists B. f <-> f'
     logger.info(s"Eliminating existential second order predicate $B")
@@ -71,8 +75,10 @@ object FOTransformers extends LazyLogging {
     if (!f.isUniversal) {
       logger.error("Trying to use SOQE on a non-universal formula")
     }
+    // This sets B(T1) and B(T2) to be the same relation
+    val noannotation = Z3BSFO.simplifyBS(FormulaFunctions.removeAnnotation(f, B))
 
-    val (quantifiers, clauses) = FormulaFunctions.toCNFClauses(f)
+    val (quantifiers, clauses) = FormulaFunctions.toCNFClauses(noannotation)
 
     // Group clauses by positive/negative occurences
     def ispositive(clause: List[Formula]) =
@@ -106,14 +112,16 @@ object FOTransformers extends LazyLogging {
     val fE = And.make(E.map(c => Or.make(pruneBs(c))))
     val fF = And.make(F.map(c => Or.make(pruneBs(c))))
     val fG = And.make(G.map(c => Or.make(pruneBs(c))))
-    val felim:Formula = fE /\ (fF \/ fG)
+
+    val felim:Formula = fE land (fF lor fG)
     val fsol:Formula = fG
 
     // wrap quantifiers around
     // FIXME: add equalities
-    val felimq = quantifiers.foldRight(felim)((q, inner) => if (q._1) Exists(q._2, inner) else Forall(q._2, inner))
-    val fsolq = quantifiers.foldRight(fsol)((q, inner) => if (q._1) Exists(q._2, inner) else Forall(q._2, inner))
+    val felimq = FormulaFunctions.rewrapQuantifiers(quantifiers, felim)
+    val fsolq = FormulaFunctions.rewrapQuantifiers(quantifiers, fsol)
     val z3fsolq = Z3BSFO.simplifyBS(fsolq)
+
     if (Utils.DEBUG_MODE) {
       logger.info(s"BSFO SOQE: strategy for $B: $z3fsolq")
     }

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

@@ -300,6 +300,12 @@ object FormulaFunctions extends LazyLogging {
     })
   }
 
+  def removeAnnotation(t:Formula, Funname:String) = {
+    t.everywhere({
+      case Fun(Funname, _, xs) => Fun(Funname, None, xs)
+    })
+  }
+
   def annotateOverwrite(t: Formula, Name1: String, name: String) = {
     t.everywhere({
       case Fun(f, Some(Name1), xs) => Fun(f, Some(name), xs)
@@ -457,15 +463,24 @@ object FormulaFunctions extends LazyLogging {
     Var(basename + droppedstream.head, base.typ)
   }
 
-  def fixBinding(f: Formula, bound: Set[Var]): (Formula, Set[Var]) = {
-    f match {
+  // TODO: This could be improved for the general case
+  def fixBinding(f: Formula): Formula = {
+    if (f.isUniversal) {
+      fixUniversalBindings(f)._1
+    } else {
+      fixGeneralBindings(f)._1
+    }
+  }
+
+  def fixGeneralBindings(f:Formula):(Formula, Set[Var]) = {
+    def fix(f: Formula, bound: Set[Var]): (Formula, Set[Var]) = f match {
       case UnOp(make, f1) => {
-        val (newf, newbounds) = fixBinding(f1, bound)
+        val (newf, newbounds) = fix(f1, bound)
         (make(newf), newbounds)
       }
       case BinOp(make, f1, f2) => {
-        val (newf1, newbound) = fixBinding(f1, bound)
-        val (newf2, newbound2) = fixBinding(f2, newbound)
+        val (newf1, newbound) = fix(f1, bound)
+        val (newf2, newbound2) = fix(f2, newbound)
         (make(newf1, newf2), newbound2)
       }
       case Quantifier(make, vars, fsub) => {
@@ -474,28 +489,73 @@ object FormulaFunctions extends LazyLogging {
         val renamed = fsub.parallelRename(alreadybounds, newnames)
         val binding = (vars.toSet -- alreadybounds) ++ newnames
 
-        val (fixedrename, newbound) = fixBinding(renamed, bound ++ binding)
+        val (fixedrename, newbound) = fix(renamed, bound ++ binding)
         val newf = make(binding.toList, fixedrename)
         (newf, newbound)
       }
       // Functions, Variables
       case f => (f, bound)
     }
+    logger.warn("Using fallback fixbindings method for general formulas.")
+    fix(f, Set())
+  }
+
+
+  def fixUniversalBindings(f: Formula): (Formula, Set[Var]) = {
+    def fix(f:Formula, bound: Set[Var]):(Formula, Set[Var]) = {
+      f match {
+        case UnOp(make, f1) => {
+          val (newf, newbounds) = fix(f1, bound)
+          (make(newf), newbounds)
+        }
+        case Or(f1, f2) => {
+          val (newf1, newbound) = fix(f1, bound)
+          val (newf2, newbound2) = fix(f2, newbound)
+          (Or(newf1, newf2), newbound2)
+        }
+        case And(f1, f2) => {
+          val (newf1, newbound) = fix(f1, bound)
+          val (newf2, newbound2) = fix(f2, bound)
+          (And(newf1, newf2), newbound ++ newbound2)
+        }
+        case Quantifier(make, vars, fsub) => {
+          val alreadybounds = vars.filter(bound.contains)
+          val newnames = alreadybounds.map(generateName(_, bound))
+          val renamed = fsub.parallelRename(alreadybounds, newnames)
+          val binding = (vars.toSet -- alreadybounds) ++ newnames
+
+          val (fixedrename, newbound) = fix(renamed, bound ++ binding)
+          val newf = make(binding.toList, fixedrename)
+          (newf, newbound)
+        }
+        // Functions, Variables
+        case f => (f, bound)
+      }
+    }
+
+    if (!f.isUniversal) {
+      logger.error("Trying to fix universal bindings of non-universal formula")
+    }
+    fix(f, Set())
   }
 
   // TODO: make sure no quantifiers in scope of others with same name
   def toPrenex(f: Formula): Formula = {
-    val negnf = f.toNegNf
+    val negnf = f.toNegNf.simplify()
 
     // TODO: test fix bindings
-    val (simp, boundVars) = fixBinding(negnf, Set())
-//    val simp = negnef
+    val simp = fixBinding(negnf)
+//    val simp = negnf
 
     // Simplify first to push negation inward
-    val quants = collectQuantifiers(simp)
+    val quantifiers = collectQuantifiers(simp)
     val stripped = stripQuantifiers(simp)
 
-    rewrapQuantifiers(quants, stripped)
+    // Not using rewrapQuantifiers since that one pushes quantifiers inward again
+    //    val wrapped = rewrapQuantifiers(quants, stripped)
+    quantifiers.foldRight(stripped)((quant, inner) => {
+      if (quant._1) Exists(quant._2, inner) else Forall(quant._2, inner)
+    }).simplify()
   }
 
   def rewrapQuantifiers(quantifiers: List[(Boolean, List[Var])], f:Formula) = {
@@ -521,9 +581,9 @@ object FormulaFunctions extends LazyLogging {
       if (!changed) sub else toCNFSub(sub)
     }
 
-    if (f.isUniversal) {
-        Z3BSFO.toCNFClausesUniversal(f)
-    } else {
+//    if (f.isUniversal) {
+//        Z3BSFO.toCNFClausesUniversal(f)
+//    } else {
       logger.warn("Using internal CNF conversion - may blow up")
 
       // FIXME: can we do it without prenex? may be expensive later on
@@ -563,7 +623,7 @@ object FormulaFunctions extends LazyLogging {
       logger.debug(s"After simplification ${simped.size} unsubsumed clauses remaining.")
 
       (quantifiers, simped)
-    }
+//    }
   }
 
   def toCNF(f: Formula) = {

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

@@ -76,9 +76,9 @@ class FOLTLTest extends FlatSpec {
   }
   
   it should "compute prenex form" in {
-    val f = Forall("x", Exists("y", And("x", Forall("z", Or(Neg(Forall("a", "a")), "z")))))
+    val f = Forall("x", Exists("y", And("x", Forall("z", Or(Neg(Forall("a", "a" land "y")), "z")))))
     
-    f.toPrenex should be (Forall("x", Exists("y", Forall("z", Exists("a", And("x", Or(Neg("a"), "z")))))))
+    f.toPrenex.simplify() should be (Forall("x", Exists("y", Forall("z", Exists("a", And("x", Or(Neg("a" land "y"), "z")))))).simplify())
   }
   
   it should "rebind several things" in {
@@ -139,8 +139,10 @@ class FOLTLTest extends FlatSpec {
       )
     )
   }
-  
-  it should "compute CNF for formulas with quantifiers" in {
+
+  // TODO: Here, rebinding would be possible because of
+  // ∃x. f(x) ∨ ∃x. g(x) = ∃x. f(x) ∨ g(x)
+  it should "compute CNF for formulas with quantifiers" ignore {
     val f = Or(And(Exists("c", "c"), "b"), And(Exists("c", "c"),"d"))
     f.toCNF.simplify should be (
       Exists(List("c"), And.make(
@@ -160,7 +162,11 @@ class FOLTLTest extends FlatSpec {
         Neg(Fun("Conf",Some("t1"),List("xt","p")))
         ))
         
-     f.toCNF should be (f)
+     f.toCNF should be (FormulaFunctions.pushUniversalQuantifiers(f))
+
+    True.toCNF should be (True)
+    False.toCNF should be (False)
+
   }
 
   val x = Fun("f", "x")