add trace to equalities

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

@@ -15,6 +15,7 @@ object Utils extends LazyLogging {
   val RESULTSFOLDER = "results"
   val DEBUG_MODE = true
   val Z3CONTEXTELIM = false
+  val APPROXELIM_MINSIZE = 50
 
   def mkString[T](string: Iterable[T], start: String, mid: String, end: String): String = {
     if (string.isEmpty) "" else string.mkString(start, mid, end)

src/main/scala/de/tum/niwo/blocks/Saturator.scala

 package de.tum.niwo.blocks
 
 import com.typesafe.scalalogging.LazyLogging
-import de.tum.niwo.Utils
 import de.tum.niwo.foltl.FOLTL._
-import de.tum.niwo.foltl.FormulaFunctions
+import de.tum.niwo.foltl.{FormulaFunctions, Properties}
 import de.tum.niwo.toz3.Z3BSFO
 
 object Saturator extends LazyLogging {
@@ -20,8 +19,9 @@ object Saturator extends LazyLogging {
       // FIXME: this may add too many eqs, since annotations T1, T2 are ignored
       val witheqs = for (c <- clauses) yield {
         val ineqs = for (pred <- allpredicates;
-                         pos <- FormulaFunctions.getPositiveArguments(c, pred.name);
-                         neg <- FormulaFunctions.getNegativeArguments(c, pred.name)
+                         trace <- List(None, Some(Properties.T1), Some(Properties.T2));
+                         pos <- FormulaFunctions.getPositiveArguments(c, pred.name, trace);
+                         neg <- FormulaFunctions.getNegativeArguments(c, pred.name, trace)
         ) yield {
           FormulaFunctions.eq(pos, neg)
         }

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

@@ -57,11 +57,34 @@ object FOTransformers extends LazyLogging {
   }
   
   def eliminateAuxiliaryPredicate(f:Formula, AUX:String, props:InvProperties): Formula = {
-    logger.debug(s"Eliminating universal second order predicate $AUX")
 
-    val cnf = if (!props.approxElim) f.toCNF else f.toNegNf
+    val result = if (!props.approxElim || f.opsize < Utils.APPROXELIM_MINSIZE) {
+      logger.debug(s"Eliminating universal second order predicate $AUX")
+      val (quants, clauses) = FormulaFunctions.toCNFClauses(f)
 
-    val repld = cnf everywhere {
+      val updatedclauses = for (clause <- clauses) yield {
+        val eqs = for (
+          trace <- List(None, Some(Properties.T1), Some(Properties.T2));
+          pos <- FormulaFunctions.getPositiveArguments(clause, AUX, trace);
+          neg <- FormulaFunctions.getNegativeArguments(clause, AUX, trace)) yield {
+          FormulaFunctions.eq(pos, neg)
+        }
+        if (eqs.nonEmpty) {
+          logger.trace(s"Introducing equalities while eliminating $AUX")
+        }
+        clause ++ eqs
+      }
+
+      val updatedcnf = And.make(updatedclauses.map(Or.make))
+      FormulaFunctions.rewrapQuantifiers(quants, updatedcnf)
+
+    } else {
+      logger.debug(s"Approximating elimination of universal second order predicate $AUX")
+      // Saturated formula, no equalities anywhere
+      f
+    }
+
+    val repld = result everywhere {
       case Neg(Fun(AUX, _, _)) => False
       case Fun(AUX, _, _) => False
     }
@@ -84,14 +107,14 @@ object FOTransformers extends LazyLogging {
     val (quantifiers, clauses) = FormulaFunctions.toCNFClauses(noannotation)
 
     // Group clauses by positive/negative occurences
-    val getPositiveBArguments = FormulaFunctions.getPositiveArguments(_, NAME)
-    val getNegativeBArguments = FormulaFunctions.getNegativeArguments(_, NAME)
+    val positiveBArguments = FormulaFunctions.getPositiveArguments(_, NAME, None)
+    val negativeBArguments = FormulaFunctions.getNegativeArguments(_, NAME, None)
 
     def ispositive(clause: List[Formula]) =
-      getPositiveBArguments(clause).nonEmpty
+      positiveBArguments(clause).nonEmpty
 
     def isnegative(clause: List[Formula]) =
-      getNegativeBArguments(clause).nonEmpty
+      negativeBArguments(clause).nonEmpty
 
     def pruneBs(clause: List[Formula]) = {
       clause filterNot {
@@ -104,17 +127,17 @@ object FOTransformers extends LazyLogging {
     val E = clauses.filter(c => !ispositive(c) && !isnegative(c))
     val F = clauses.filter(c => ispositive(c) && !isnegative(c))
     //  F \/ B z_1 ... B z_r
-    val Fargs = F.map(getPositiveBArguments)
+    val Fargs = F.map(positiveBArguments)
 
     val G = clauses.filter(c => isnegative(c) && !ispositive(c))
     // G \/ !B z'_1 ... !B z'_j
-    val Gargs = G.map(getNegativeBArguments)
+    val Gargs = G.map(negativeBArguments)
 
     val H = clauses.filter(c => ispositive(c) && isnegative(c))
 
     // H \/ B u_1 .. B u_l \/ !B v_1 ... ! B v_n
-    val HPositiveargs = H.map(getPositiveBArguments)
-    val HNegativeargs = H.map(getNegativeBArguments)
+    val HPositiveargs = H.map(positiveBArguments)
+    val HNegativeargs = H.map(negativeBArguments)
 
     if (H.nonEmpty) {
       logger.debug("BSFO SOQE: H is not empty, Ackermann not applicable")

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

@@ -592,7 +592,6 @@ object FormulaFunctions extends LazyLogging {
 //    } else {
 //      logger.warn("Using internal CNF conversion - may blow up")
 
-    // FIXME: can we do it without prenex? may be expensive later on
     val normalized = f.toPrenex.simplify
     logger.debug(s"Computing CNF of prenex formula of opsize ${normalized.opsize}")
 
@@ -695,15 +694,16 @@ object FormulaFunctions extends LazyLogging {
 
   }
 
-  def getPositiveArguments(clause: List[Formula], NAME:String):Set[List[Var]] = {
+  // matches positive arguments of the function with the correct annotation
+  def getPositiveArguments(clause: List[Formula], NAME:String, ANNOTATION:Option[String] = None):Set[List[Var]] = {
     clause flatMap {
-      case Fun(NAME, _, vars) => List(vars)
+      case Fun(NAME, ANNOTATION, vars) => List(vars)
       case _ => List()
     } toSet
   }
-  def getNegativeArguments(clause: List[Formula], NAME:String):Set[List[Var]] = {
+  def getNegativeArguments(clause: List[Formula], NAME:String, ANNOTATION:Option[String] = None):Set[List[Var]] = {
     clause flatMap {
-      case Neg(Fun(NAME, _, vars))=> List(vars)
+      case Neg(Fun(NAME, ANNOTATION, vars))=> List(vars)
       case _ => List()
     } toSet
   }

src/test/scala/de/tum/niwo/tests/ParserTest.scala

@@ -12,7 +12,7 @@ import de.tum.niwo.parser.WorkflowParser
 
 class ParserTest extends FlatSpec {
 
-  val oxrxssig = Signature(Set(Fun("O", List("x","s"))), Set(), Set(), Set(Fun("R", List("x", "s"))), Set())
+  val oxrxssig = Signature(Set(Fun("O", List("x","s")), Fun("choice0", List("x","s"))), Set(), Set(), Set(Fun("R", List("x", "s"))), Set())
 
   def testResult(s: String, sig: Signature) {
     testResult(s, Workflow(sig, List()))
@@ -91,7 +91,7 @@ class ParserTest extends FlatSpec {
       """
     val w = Workflow(
       Signature(
-        Set(Fun("O", List("s"))),
+        Set(Fun("O", List("s")), Fun("choice0", List("x","s"))),
         Set(),
         Set(),
         Set(
@@ -157,7 +157,7 @@ class ParserTest extends FlatSpec {
     val x = Var("x", "Agent")
     val s = Var("s", "Paper")
 
-    val typedsig = Signature(Set(Fun("O", List(x))), Set(), Set(), Set(Fun("R", List(x, s))), Set())
+    val typedsig = Signature(Set(Fun("O", List(x)), Fun("choice0", List(x))), Set(), Set(), Set(Fun("R", List(x, s))), Set())
 
     val w = Workflow(
       typedsig,

src/test/scala/de/tum/niwo/tests/papertests/InvariantEasychairTest.scala

@@ -115,7 +115,7 @@ class InvariantEasychairTest extends FlatSpec {
   }
 
   // Brittle against approx elim
-  it should "prove omitting/conference_fixed with auxelim approximation" ignore {
+  it should "prove omitting/conference_fixed with auxelim approximation" in {
     val name = "omitting/conference_fixed_stubborn"
     val inv = InvariantGenerator.invariantNoninterSingleBS _
     assert(checkSafe(name, "", inv, InvProperties(