ineq

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

@@ -198,14 +198,19 @@ object Preconditions extends LazyLogging {
 
     // Win game
     val bless = if (properties.eliminateB) {
-      val bs = oless.collect {
-        case f:Fun if f.isB() => List(f.name)
-      }.toSet
-      if (bs.nonEmpty && !untouched.contains(Properties.INFNAME)) {
+      val bs = spec.w.sig.bs
+
+      val occuringBs = bs.filter(b =>
+        oless.hasSubFormula {
+          case Fun(b.name, _, _) => true
+        }
+      )
+
+      if (occuringBs.nonEmpty && !untouched.contains(Properties.INFNAME)) {
         logger.error("Trying to compute strategies for B with B,B' not necessarily equal")
       }
 
-      bs.foldRight(oless)((b, inv) => FOTransformers.eliminateBPredicate(inv, b)._1)
+      occuringBs.foldRight(oless)((b, inv) => FOTransformers.eliminateBPredicate(inv, b)._1)
     } else {
       oless
     }

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

@@ -80,7 +80,7 @@ object WorkflowParser extends RegexParsers with PackratParsers with LazyLogging
     val oracles = filtered.filter(_.isOracle())
     val bs = filtered.filter(_.isB())
     val rels = filtered -- oracles -- bs
-    Signature(oracles, rels)
+    Signature(oracles, bs, rels)
   }
   
   def typeMap(typedvars: List[Var]) = {

src/main/scala/de/tum/workflows/blocks/Workflow.scala

@@ -5,9 +5,9 @@ import com.typesafe.scalalogging.LazyLogging
 import de.tum.workflows.Utils
 import de.tum.workflows.foltl.Properties
 
-case class Signature(oracles: Set[Fun], preds: Set[Fun])
+case class Signature(oracles: Set[Fun], bs: Set[Fun], preds: Set[Fun])
 object Signature {
-  val EMPTY = Signature(Set(), Set())
+  val EMPTY = Signature(Set(), Set(), Set())
 }
 
 case class Workflow(sig: Signature, steps: List[Block]) {

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

@@ -13,6 +13,7 @@ object FOLTL {
     lazy val simplify: Formula = FormulaFunctions.simplify(this)
 
     lazy val freeVars: Set[Var] = FormulaFunctions.freeVars(this)
+    lazy val boundVars: Set[Var] = FormulaFunctions.boundVars(this)
     lazy val opsize: Int = FormulaFunctions.opsize(this)
 
     def everywhere(trans: PartialFunction[Formula, Formula]): Formula = FormulaFunctions.everywhere(trans, this)

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

@@ -67,17 +67,18 @@ 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) = {
+  def eliminateBPredicate(f:Formula, b:Fun) = {
+    val NAME = b.name
+
     // SOQE: \exists B. f <-> f'
-    logger.debug(s"Eliminating existential second order predicate $B")
+    logger.debug(s"Eliminating existential second order predicate $b")
 
     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
     // Use the best available simplification
-    val noannotation = Z3BSFO.simplifyBS(FormulaFunctions.removeAnnotation(f, B))
+    val noannotation = Z3BSFO.simplifyBS(FormulaFunctions.removeAnnotation(f, NAME))
 
     val (quantifiers, clauses) = FormulaFunctions.toCNFClauses(noannotation)
 
@@ -90,20 +91,20 @@ object FOTransformers extends LazyLogging {
 
     def pruneBs(clause: List[Formula]) = {
       clause filterNot {
-        case Neg(Fun(B, _, _)) => true
-        case Fun(B, _, _) => true
+        case Neg(Fun(NAME, _, _)) => true
+        case Fun(NAME, _, _) => true
         case _ => false
       }
     }
     def getPositiveBArguments(clause: List[Formula]):Set[List[Var]] = {
       clause flatMap {
-        case Fun(B, _, vars) => List(vars)
+        case Fun(NAME, _, vars) => List(vars)
         case _ => List()
       } toSet
     }
     def getNegativeBArguments(clause: List[Formula]):Set[List[Var]] = {
       clause flatMap {
-        case Neg(Fun(B, _, vars))=> List(vars)
+        case Neg(Fun(NAME, _, vars))=> List(vars)
         case _ => List()
       } toSet
     }
@@ -155,19 +156,26 @@ object FOTransformers extends LazyLogging {
     val fGHineq = And.make(FGineq)
     val simpfGHineq = Z3BSFO.simplifyBS(fGHineq)
 
-
     val felim:Formula = fE land fFGineq land fGHineq
-    // TODO: Add ineq with ys
-    val fsol:Formula = And.make(gks)
-
-    // wrap quantifiers around
     val felimq = FormulaFunctions.rewrapQuantifiers(quantifiers, felim)
+
+    // Compute solution
+    val bounds = gks.flatMap(_.freeVars) ++ gks.flatMap(_.boundVars)
+
+    val freeparams = b.params.map(p => FormulaFunctions.generateName(p, bounds.toSet))
+    val gkineq = for ((gk, gargs) <- gks.zip(Gargs); garg <- gargs) yield {
+      Or.make(gk
+        ,
+        ineq(garg, freeparams)
+      )
+    }
+    val fsol:Formula = And.make(gkineq)
     val fsolq = FormulaFunctions.rewrapQuantifiers(quantifiers, fsol)
 
     val z3fsolq = Z3BSFO.simplifyBS(fsolq)
 
     if (Utils.DEBUG_MODE) {
-      logger.info(s"BSFO SOQE: strategy for $B: $z3fsolq")
+      logger.info(s"BSFO SOQE: strategy for ${b.updatedParams(freeparams)}: $z3fsolq")
     }
 
     (felimq, z3fsolq)

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

@@ -29,6 +29,17 @@ object FormulaFunctions extends LazyLogging {
     free(t, Set())
   }
 
+  // @tailrec version?
+  def boundVars(f:Formula): Set[Var] = {
+    def boundInner(f: Formula): List[Var] = {
+      f collect {
+        case Quantifier(_, xs, sub) => xs ++ boundInner(sub)
+      }
+    }
+    boundInner(f).toSet
+  }
+
+
   def simplify(t: Formula): Formula = {
     val simp: PartialFunction[Formula, Formula] = {
       // Push negation inward
@@ -363,12 +374,7 @@ object FormulaFunctions extends LazyLogging {
    * 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)
+    boundVars(f).groupBy(n => n.name).exists(_._2.size > 1)
   }
 
   def stripQuantifiers(f: Formula): Formula = {
@@ -502,7 +508,7 @@ object FormulaFunctions extends LazyLogging {
       case f => (f, bound)
     }
     logger.warn("Using fallback fixbindings method for general formulas.")
-    fix(f, Set())
+    fix(f, f.freeVars)
   }
 
 
@@ -541,7 +547,7 @@ object FormulaFunctions extends LazyLogging {
     if (!f.isUniversal) {
       logger.error("Trying to fix universal bindings of non-universal formula")
     }
-    fix(f, Set())
+    fix(f, f.freeVars)
   }
 
   // TODO: make sure no quantifiers in scope of others with same name

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

@@ -154,7 +154,7 @@ class FOTransformSpec extends FlatSpec {
 
   "SOQE" should "work" in {
     val f = Fun("f","x") land Fun("g", "x") land Fun("B", "x")
-    val (a,b) = FOTransformers.eliminateBPredicate(f, "B")
+    val (a,b) = FOTransformers.eliminateBPredicate(f, Fun("B", "x"))
 
     println(a,b)
   }

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

@@ -13,7 +13,7 @@ import com.typesafe.scalalogging.LazyLogging
 
 class ParserTest extends FlatSpec {
 
-  val oxrxssig = Signature(Set(Fun("O", List("x","s"))), Set(Fun("R", List("x", "s"))))
+  val oxrxssig = Signature(Set(Fun("O", List("x","s"))), Set(), Set(Fun("R", List("x", "s"))))
 
   def testResult(s: String, sig: Signature) {
     testResult(s, Workflow(sig, List()))
@@ -93,6 +93,7 @@ class ParserTest extends FlatSpec {
     val w = Workflow(
       Signature(
         Set(Fun("O", List("s"))),
+        Set(),
         Set(
           Fun("S", List("x", "y", "s")),
           Fun("R", List("y", "s")),
@@ -155,7 +156,7 @@ class ParserTest extends FlatSpec {
     val x = Var("x", "Agent")
     val s = Var("s", "Paper")
 
-    val typedsig = Signature(Set(Fun("O", List(x))), Set(Fun("R", List(x, s))))
+    val typedsig = Signature(Set(Fun("O", List(x))), Set(), Set(Fun("R", List(x, s))))
 
     val w = Workflow(
       typedsig,
@@ -180,6 +181,7 @@ class ParserTest extends FlatSpec {
     val w = Workflow(
       Signature(
         Set(Fun("O", List("s"))),
+        Set(),
         Set(Fun("R", List("x", "s")))),
       List(
         ForallMayBlock(List("x", "s"), "choice0",