new algorithm to generate interesting tasks ... first try

jayhorn · Feb 2, 2017 · ef0199c · ef0199c
1 parent 451d676
commit ef0199c
Show file tree

Hide file tree

Showing 3 changed files with 353 additions and 85 deletions.
diff --git a/src/lazabs/horn/bottomup/HornClauses.scala b/src/lazabs/horn/bottomup/HornClauses.scala
@@ -223,6 +223,26 @@ object HornClauses {
       quanConsts(Quantifier.ALL, constants.toSeq, matrix)
     }
 
+    def instantiatePredicates(mapping : Map[Predicate, IFormula]) : Clause = {
+      import IExpression._
+
+      val (headFor, newHead) = head.pred match {
+        case pred if (mapping contains pred) =>
+          (VariableSubstVisitor(mapping(pred), (head.args.toList, 0)),
+           FALSE())
+        case _ => (i(false), head)
+      }
+
+      val (substBodyLits, newBody) = body partition (mapping contains _.pred)
+      val substBody =
+        and(for (a <- substBodyLits)
+            yield VariableSubstVisitor(mapping(a.pred), (a.args.toList, 0)))
+
+      val newConstraint = (constraint &&& substBody) &&& ~headFor
+
+      Clause(newHead, newBody, newConstraint)
+    }
+
     def toSMTString : String = SMTLineariser asString this.toFormula
 
     def toPrettyString : String =