Extended quantifiers support

build.sbt

@@ -2,7 +2,7 @@
 lazy val commonSettings = Seq(
     name := "Eldarica",
     organization := "uuverifiers",
-    version := "2.1",
+    version := "2.1-ext",
     homepage := Some(url("https://github.com/uuverifiers/eldarica")),
     licenses := Seq("BSD License 2.0" -> url("https://github.com/uuverifiers/eldarica/blob/master/LICENSE")),
     scmInfo              := Some(ScmInfo(

eldEnv

@@ -23,19 +23,31 @@ LAZABS_HOME=`dirname "${SOURCE}"`;
 
 export JAVA_OPTS="-Xmx8096m -Xss20000k";
 
-if [ -f ${LAZABS_HOME}/dist/lazabs.jar ]; then
-
-   	# binary distribution
-	export LAZABS_CMD="java ${JAVA_OPTS} -cp ${LAZABS_HOME}/dist/lazabs.jar"
-
-else if [ -f ${LAZABS_HOME}/target/scala-2.*/Eldarica-assembly*.jar ]; then
-
-        # binary distribution from sbt
-	export LAZABS_CMD="java ${JAVA_OPTS} -cp ${LAZABS_HOME}/target/scala-2.*/Eldarica-assembly*.jar"
+if [ -f "${LAZABS_HOME}/dist/lazabs.jar" ]; then
 
+    # binary distribution
+    export LAZABS_CMD="java ${JAVA_OPTS} -cp ${LAZABS_HOME}/dist/lazabs.jar"
 else
-
+    ASSEMBLY_FILES=$(ls -1 ${LAZABS_HOME}/target/scala-2.*/Eldarica-assembly*.jar 2>/dev/null)
+    ASSEMBLY_COUNT=$(echo "$ASSEMBLY_FILES" | grep -c '^')
+
+    if [ "$ASSEMBLY_COUNT" -gt 0 ]; then
+        if [ "$ASSEMBLY_COUNT" -eq 1 ]; then
+            # binary distribution from sbt
+            export LAZABS_CMD="java ${JAVA_OPTS} -cp $ASSEMBLY_FILES"
+        else
+            # find latest assembly
+            latest=''
+            for file in $ASSEMBLY_FILES; do
+                if [ -z "$latest" ] || [ "$file" -nt "$latest" ]; then
+                    latest=$file
+                fi
+            done
+            echo "Warning: multiple assembly files found in target directory, using $latest"
+            export LAZABS_CMD="java ${JAVA_OPTS} -cp $latest"
+        fi
+    else
         echo "Could not find Eldarica jar" >&2
         exit 1
-
-fi; fi
+    fi
+fi

regression-tests/horn-arrays/Answers

@@ -323,8 +323,8 @@ splitting.smt2
 unsat
 
 0: FALSE -> 1
-1: inv(store(const(4), 0, 1), store(const(3), 0, 2), 1, 2) -> 2
-2: inv(store(const(4), 0, 1), store(const(3), 0, 2), 0, 0)
+1: inv(store(const(3), 0, 1), store(const(4), 0, 2), 1, 2) -> 2
+2: inv(store(const(3), 0, 1), store(const(4), 0, 2), 0, 0)
 
 splitting2.smt2
 sat

src/main/scala/lazabs/ast/ASTree.scala

@@ -30,7 +30,8 @@
 package lazabs.ast
 
 import lazabs.types._
-import ap.theories.{ADT, Heap, Theory, TheoryCollector, TheoryRegistry}
+import ap.theories.{ADT, Heap}
+import lazabs.horn.extendedquantifiers.theories.AbstractExtendedQuantifier
 
 
 object ASTree {
@@ -109,6 +110,11 @@ object ASTree {
                      exprList: Seq[Expression]) extends Expression
   case class HeapPred(heap: Heap, name: String,
                      exprList: Seq[Expression]) extends Expression
+
+  // Extended quantifiers
+  case class ExtQuantifierFun(extQuantifier: AbstractExtendedQuantifier,
+                              exprList: Seq[Expression]) extends Expression
+
   // Bit-vectors
 
   case class BVconst(bits: Int, num : BigInt) extends Expression
@@ -157,10 +163,11 @@ object ASTree {
   // ternary expressions
   sealed abstract class TernaryOperator(val st: String)
   case class IfThenElseOp() extends TernaryOperator ("if")
-  case class ArrayUpdateOp() extends TernaryOperator ("update")  
+  case class ArrayUpdateOp() extends TernaryOperator ("update")
+  case class ExtendedQuantifierOp() extends TernaryOperator ("extquans")
   case class TernaryExpression(op: TernaryOperator, e1: Expression, e2: Expression, e3: Expression) extends Expression  
 
-  // binray expressions
+  // binary expressions
   sealed abstract class BinaryOperator(val st: String)
   case class IfThenOp() extends BinaryOperator ("if")
   case class AssignmentOp() extends BinaryOperator ("=")

src/main/scala/lazabs/horn/abstractions/AbstractionBuilder.scala

@@ -35,6 +35,7 @@ import lazabs.horn.concurrency.ReaderMain
 import lazabs.horn.bottomup.HornPredAbs.predArgumentSorts
 
 import ap.basetypes.IdealInt
+import ap.parser.IExpression.Predicate
 import ap.theories.nia.GroebnerMultiplication
 import ap.theories.rationals.Rationals
 import ap.theories.bitvectors.ModuloArithmetic.ModSort
@@ -56,13 +57,14 @@ object StaticAbstractionBuilder {
  */
 class StaticAbstractionBuilder(
          clauses : Seq[HornClauses.Clause],
-         abstractionType : StaticAbstractionBuilder.AbstractionType.Value) {
+         abstractionType : StaticAbstractionBuilder.AbstractionType.Value,
+         substitutablePredicates : Set[Predicate] = Set()) {
 
   import IExpression._
   import HornClauses.Clause
   import VerificationHints._
 
-  val loopDetector = new LoopDetector(clauses)
+  val loopDetector = new LoopDetector(clauses, substitutablePredicates)
 
   Console.err.println("Loop heads:")
 

src/main/scala/lazabs/horn/abstractions/LoopDetector.scala

@@ -42,6 +42,7 @@ import ap.terfor.equations.ReduceWithEqs
 import ap.types.Sort
 import ap.theories.ModuloArithmetic
 import ap.parser._
+import ap.parser.IExpression.Predicate
 import ap.util.{LRUCache, Seqs}
 
 import scala.collection.mutable.{LinkedHashSet, ArrayBuffer,
@@ -51,7 +52,8 @@ import scala.collection.mutable.{LinkedHashSet, ArrayBuffer,
  * Compute loops and loop heads of the given set of clauses,
  * using a generalised version of the dominator relation.
  */
-class LoopDetector(clauses : Seq[HornClauses.Clause]) {
+class LoopDetector(clauses            : Seq[HornClauses.Clause],
+                   substitutablePreds : Set[Predicate] = Set()) {
 
   import IExpression._
   import HornClauses.Clause
@@ -66,14 +68,16 @@ class LoopDetector(clauses : Seq[HornClauses.Clause]) {
     while (oldSize != allPredicates.size) {
       oldSize = allPredicates.size
       for (Clause(IAtom(headP, _), body, _) <- clauses)
-        if (body forall { case IAtom(p, _) => allPredicates contains p })
+        if (body forall { case IAtom(p, _) =>
+          (allPredicates contains p) || (substitutablePreds contains p)})
           allPredicates += headP
     }
   }
 
   val reachableClauses =
     for (clause@Clause(_, body, _) <- clauses;
-         if (body forall { case IAtom(p, _) => allPredicates contains p }))
+         if (body.filter(b => !(substitutablePreds contains b.pred)) forall {
+           case IAtom(p, _) => allPredicates contains p}))
     yield clause
 
   val clausesWithHead =
@@ -87,7 +91,8 @@ class LoopDetector(clauses : Seq[HornClauses.Clause]) {
 
     val body2head =
       ((for (Clause(IAtom(head, _), body, _) <- reachableClauses;
-                    IAtom(b, _) <- body)
+                    IAtom(b, _) <- body.filter(b =>
+                      !(substitutablePreds contains b.pred)))
         yield (b, head)) groupBy (_._1)) mapValues (_ map (_._2))
 
     val workqueue = new LinkedHashSet[Predicate]
@@ -105,7 +110,8 @@ class LoopDetector(clauses : Seq[HornClauses.Clause]) {
       val oldSet = domCandidates(p)
       val newSet =
         (for (Clause(_, body, _) <- pClauses.iterator) yield {
-           (Set(p) /: (for (IAtom(q, _) <- body.iterator)
+           (Set(p) /: (for (IAtom(q, _) <- body.filter(b =>
+             !(substitutablePreds contains b.pred)).iterator)
                        yield domCandidates(q))) (_ ++ _)
          }) reduce (_ & _)
 
@@ -122,7 +128,8 @@ class LoopDetector(clauses : Seq[HornClauses.Clause]) {
 
   val loopHeads =
     (for (clause@Clause(IAtom(p, _), body, _) <- reachableClauses.iterator;
-          if (body exists { case IAtom(q, _) => dominates(p, q) }))
+          if (body.filter(b => !(substitutablePreds contains b.pred)) exists {
+            case IAtom(q, _) => dominates(p, q) }))
      yield p).toSet
 
   val loopBodies =
@@ -135,15 +142,17 @@ class LoopDetector(clauses : Seq[HornClauses.Clause]) {
          oldSize = bodyPreds.size
          for (Clause(IAtom(p, _), body, _) <- reachableClauses.iterator;
               if (bodyPreds contains p);
-              IAtom(q, _) <- body.iterator;
+              IAtom(q, _) <- body.filter(b =>
+                !(substitutablePreds contains b.pred)).iterator;
               if (dominates(head, q)))
            bodyPreds += q
        }
 
        (head,
         for (clause@Clause(IAtom(p, _), body, _) <- reachableClauses;
              if ((bodyPreds contains p) &&
-                 (body exists { case IAtom(q, _) => bodyPreds contains q })))
+                 (body.filter(b => !(substitutablePreds contains b.pred)) exists {
+                   case IAtom(q, _) => bodyPreds contains q })))
         yield clause)
      }).toMap