add prenex

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

@@ -152,7 +152,7 @@ object Main extends App with LazyLogging {
   }
 
   //  clear()
-  //  generateExample("omitting/conference")
+    generateExample("omitting/conference")
   //    generateExample("tests/declasstest")
-  generateAllExamples()
+//  generateAllExamples()
 }
\ No newline at end of file

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

@@ -16,6 +16,8 @@ object FOLTL {
     def collect[T](coll: PartialFunction[Formula, List[T]]) = FormulaFunctions.collect(coll, this)
     def opsize() = FormulaFunctions.opsize(this)
     
+    def toPrenex() = FormulaFunctions.toPrenex(this)
+    
     def removeOTQuantifiers() = FormulaFunctions.removeOTQuantifiers(this)
     def parallelRename(vars:List[Var], newvars:List[Var]) = FormulaFunctions.parallelRename(this, vars, newvars)
 

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

@@ -10,16 +10,16 @@ object FormulaFunctions extends LazyLogging {
       t match {
         // Extractors
         // Exists, Forall
-        case Quantifier(_, ps, t)  => free(t, bound ++ ps)
-        case UnOp(make, t)         => free(t, bound)
+        case Quantifier(_, ps, t) => free(t, bound ++ ps)
+        case UnOp(make, t)        => free(t, bound)
         // And, Or, Eq, Implies
-        case BinOp(_, t1, t2)      => free(t1, bound) ++ free(t2, bound)
+        case BinOp(_, t1, t2)     => free(t1, bound) ++ free(t2, bound)
 
-//      TODO: path is not a free variable anymore
-//        case Fun(_, Some(ind), ps) => (ps.toSet -- bound) + Var(ind)
-        case Fun(_, _, ps)         => (ps.toSet -- bound)
-        case v: Var if !bound(v)   => Set(v)
-        case x                     => Set()
+        //      TODO: path is not a free variable anymore
+        //        case Fun(_, Some(ind), ps) => (ps.toSet -- bound) + Var(ind)
+        case Fun(_, _, ps)        => (ps.toSet -- bound)
+        case v: Var if !bound(v)  => Set(v)
+        case x                    => Set()
       }
     }
     free(t, Set())
@@ -61,7 +61,9 @@ object FormulaFunctions extends LazyLogging {
       case Quantifier(_, xs, t) if xs.isEmpty => t
       case Quantifier(_, _, True)             => True
       case Quantifier(_, _, False)            => False
-
+      
+      // TODO: Double quantifiers
+      
       // Remove variables from quantifiers if not used in the body
       //      case Quantifier(qmake, xs, t) if !(xs.toSet -- t.freeVars()).isEmpty =>
       //        qmake((xs.toSet.intersect(t.freeVars())).toList, t)
@@ -76,6 +78,12 @@ object FormulaFunctions extends LazyLogging {
     val t1 = everywhere(simp, t)
     if (t == t1) t1 else simplify(t1)
   }
+  
+  def eliminateImplication(f:Formula) = {
+    f everywhere {
+      case Implies(f1, f2) => Or(Neg(f1), f2)
+    }
+  }
 
   def everywhere(trans: PartialFunction[Formula, Formula], t: Formula): Formula = {
     if (trans.isDefinedAt(t))
@@ -167,20 +175,119 @@ object FormulaFunctions extends LazyLogging {
   }
 
   // f[newvars/vars]
-  def parallelRename(f: Formula, vars: List[Var], newvars: List[Var]):Formula = {
+  def parallelRename(f: Formula, vars: List[Var], newvars: List[Var]): Formula = {
     val repls = vars zip newvars toMap
-    
+
     parallelRename(f, repls)
   }
-  
-  def parallelRename(f: Formula, repls:Map[Var, Var]):Formula = {
-     f everywhere {
+
+  def parallelRename(f: Formula, repls: Map[Var, Var]): Formula = {
+    f everywhere {
       case v: Var if repls.contains(v) => repls(v)
-      case Fun(f, ind, params) => Fun(f, ind, params map (p => repls.getOrElse(p, p)))
+      case Fun(f, ind, params)         => Fun(f, ind, params map (p => repls.getOrElse(p, p)))
       case Quantifier(make, xs, f) => {
         val rep = repls -- (xs)
         make(xs, parallelRename(f, rep))
       }
     }
   }
+
+  /**
+   * Check if there exist quantifiers binding the same variable more than once
+   */
+  def hasDuplicateBindings(f: Formula) = {
+    def boundNames(f: Formula): List[Var] = {
+      f collect {
+        case Quantifier(make, xs, sub) => xs ++: boundNames(sub)
+      }
+    }
+    boundNames(f).groupBy(n => n).exists(_._2.length > 1)
+  }
+
+  def toPrenex(f: Formula) = {
+    def stripQuantifiers(f:Formula):Formula = {
+      f everywhere {
+        case Quantifier(_, _, fsub) => stripQuantifiers(fsub)
+      }
+    }
+    
+    def collectQuantifiers(f:Formula) = {    
+      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)
+          case BinOp(make, f1, f2) => {
+            val q1 = collectQuantifiersSub(f1)
+            val q2 = collectQuantifiersSub(f2)
+            
+            // Merge while trying to stay in BS, if possible 
+            // TODO: could be improved to minimize quantifier alternations)
+            // TODO: merge universals with same type by renaming 
+            val ex1 = q1.takeWhile(_._1)
+            val rest1 = q1.drop(ex1.size)
+            
+            val ex2 = q2.takeWhile(_._1)
+            val rest2 = q2.drop(ex2.size)
+            
+            ex1 ++ ex2 ++ rest1 ++ rest2
+          }
+        }
+      }
+      collectQuantifiersSub(f).map(_._2)
+    }
+    
+    def generateName(base:Var, bound:Set[Var]) = {
+
+      val chars = base.name.toCharArray()
+      val (basename, start) = if (chars.last.isDigit) {
+        (base.name.dropRight(1), chars.last.toInt + 1) 
+      } else {
+        (base.name, 1)
+      }
+      val stream = Stream.from(start)
+      
+      val droppedstream = stream.dropWhile(i => bound.contains(Var(basename + i, base.typ)))
+      
+      Var(basename + droppedstream.head, base.typ)
+    }
+    
+    def fixBinding(f:Formula, bound:Set[Var]):(Formula, Set[Var]) = {
+      f match {
+        case UnOp(make, f1) => {
+          val (newf, newbounds) = fixBinding(f1, bound)
+          (make(newf), newbounds)
+        }
+        case BinOp(make, f1, f2) => {
+          val (newf1, newbound) = fixBinding(f1, bound) 
+          val (newf2, newbound2) = fixBinding(f2, newbound)
+          (make(newf1, newf2), 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) = fixBinding(renamed, bound ++ binding)
+          val newf = make(binding.toList, fixedrename)
+          (newf, newbound)
+        }
+        // Functions, Variables
+        case f => (f, bound)
+      }
+    }
+    
+    if (hasDuplicateBindings(f)) {
+      logger.info(s"Formula $f binds variables more than once - renaming bindings")
+    }
+    
+    val negnf = eliminateImplication(f).simplify()
+    val (simp, boundVars) = fixBinding(negnf, Set())
+    
+    // Simplify first to push negation inward
+    val quants = collectQuantifiers(simp)
+    val stripped = stripQuantifiers(simp)
+    
+    quants.foldRight(stripped)((quant, inner) => quant(inner))
+  }
 }
\ No newline at end of file

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

@@ -63,6 +63,9 @@ object InvariantChecker extends LazyLogging {
           case Fun(f, i, p) if b.may && f == b.pred.get => Fun(f, p)
         }
       } else precond
+      
+      val test1 = inv.toPrenex()
+      val test2 = stubprecond.toPrenex()
 
       val f = Implies(inv, stubprecond)
 

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

@@ -45,4 +45,33 @@ class FOLTLTest extends FlatSpec {
     res should be (And("c", Exists("a", Fun("f", List("a","a")))))
   }
   
+  it should "compute prenex form" in {
+    val f = Forall("x", Exists("y", And("x", Forall("z", Or(Neg(Forall("a", "a")), "z")))))
+    
+    f.toPrenex() should be (Forall("x", Exists("y", Forall("z", Exists("a", And("x", Or(Neg("a"), "z")))))))
+  }
+  
+  it should "rebind variable names for prenex" in {
+    val f = Forall("x", And(Exists("z", "z"), Forall("z", Or(Neg(Forall("a", "a")), "z"))))
+    
+    f.toPrenex() should be (Forall("x", Exists("z", Forall("z1", Exists("a", And("z", Or(Neg("a"), "z1"))))))) 
+  }
+  
+  it should "rebind several things" in {
+    val f = And.make(Forall("x", "x"), Forall("x", "x"), Forall("x","x"))
+    println(f.toPrenex())
+  }
+  
+  it should "work on implication" in {
+    val f = Implies(Forall("a", "a"), Exists("x", "x"))
+    
+    f.toPrenex() should be (Exists("a", Exists("x", Or(Neg("a"), "x"))))
+  }
+  
+  it should "preserve BS" in {
+    val f = And(Forall("a", "a"), Exists("z", "z"))
+    
+    f.toPrenex() should be (Exists("z", Forall("a", And("a", "z"))))
+  }
+  
 }
\ No newline at end of file