Added legacy solver

buildSrc/src/main/kotlin/Deps.kt

@@ -13,6 +13,7 @@
  *  See the License for the specific language governing permissions and
  *  limitations under the License.
  */
+
 object Deps {
 
     val guava = "com.google.guava:guava:${Versions.guava}"
@@ -24,7 +25,8 @@ object Deps {
         val runtime = "org.antlr:antlr4-runtime:${Versions.antlr}"
     }
 
-    val z3 = "lib/com.microsoft.z3.jar"
+    val z3 = "lib/current/com.microsoft.z3.jar"
+    val z3legacy = "lib/legacy/com.microsoft.z3.jar"
 
     val jcommander = "com.beust:jcommander:${Versions.jcommander}"
 

lib/legacy/README

@@ -0,0 +1 @@
+This is the old version of Z3, used for legacy / backwards-compatibility purposes. 

settings.gradle.kts

@@ -51,6 +51,7 @@ include(
 
     "solver/solver",
     "solver/solver-z3",
+    "solver/solver-z3-legacy",
     "solver/solver-smtlib",
     "solver/solver-smtlib-cli",
     "solver/graph-solver",

subprojects/cfa/cfa-analysis/build.gradle.kts

@@ -23,6 +23,6 @@ dependencies {
     implementation(project(":theta-common"))
     implementation(project(":theta-core"))
     implementation(project(":theta-solver"))
-    testImplementation(project(":theta-solver-z3"))
+    testImplementation(project(":theta-solver-z3-legacy"))
     testImplementation(project(":theta-solver-smtlib"))
 }

subprojects/cfa/cfa-analysis/src/test/java/hu/bme/mit/theta/cfa/analysis/impact/CfaPredImpactCheckerTest.java

@@ -36,7 +36,7 @@
 import hu.bme.mit.theta.cfa.dsl.CfaDslManager;
 import hu.bme.mit.theta.common.visualization.writer.GraphvizWriter;
 import hu.bme.mit.theta.solver.ItpSolver;
-import hu.bme.mit.theta.solver.z3.Z3SolverFactory;
+import hu.bme.mit.theta.solver.z3.Z3LegacySolverFactory;
 
 public final class CfaPredImpactCheckerTest {
 
@@ -46,8 +46,8 @@ public void test() throws FileNotFoundException, IOException {
         final CFA cfa = CfaDslManager.createCfa(
                 new FileInputStream("src/test/resources/counter5_true.cfa"));
 
-        final Solver abstractionSolver = Z3SolverFactory.getInstance().createSolver();
-        final ItpSolver refinementSolver = Z3SolverFactory.getInstance().createItpSolver();
+        final Solver abstractionSolver = Z3LegacySolverFactory.getInstance().createSolver();
+        final ItpSolver refinementSolver = Z3LegacySolverFactory.getInstance().createItpSolver();
 
         final PredImpactChecker checker = PredImpactChecker.create(
                 CfaLbeLts.of(cfa.getErrorLoc().get()), cfa.getInitLoc(),

subprojects/cfa/cfa-cli/build.gradle.kts

@@ -25,7 +25,7 @@ dependencies {
     implementation(project(":theta-common"))
     implementation(project(":theta-analysis"))
     implementation(project(":theta-cfa-analysis"))
-    implementation(project(":theta-solver-z3"))
+    implementation(project(":theta-solver-z3-legacy"))
     implementation(project(":theta-solver-smtlib"))
 }
 

subprojects/cfa/cfa-cli/src/main/java/hu/bme/mit/theta/cfa/cli/CfaCli.java

@@ -54,7 +54,7 @@
 import hu.bme.mit.theta.solver.SolverFactory;
 import hu.bme.mit.theta.solver.SolverManager;
 import hu.bme.mit.theta.solver.smtlib.SmtLibSolverManager;
-import hu.bme.mit.theta.solver.z3.Z3SolverFactory;
+import hu.bme.mit.theta.solver.z3.Z3LegacySolverFactory;
 import hu.bme.mit.theta.solver.z3.Z3SolverManager;
 
 import java.io.File;
@@ -336,7 +336,7 @@ private void printError(final Throwable ex) {
     private void writeCex(final Unsafe<?, ?> status) throws FileNotFoundException {
         @SuppressWarnings("unchecked") final Trace<CfaState<?>, CfaAction> trace = (Trace<CfaState<?>, CfaAction>) status.getTrace();
         final Trace<CfaState<ExplState>, CfaAction> concrTrace = CfaTraceConcretizer.concretize(
-                trace, Z3SolverFactory.getInstance());
+                trace, Z3LegacySolverFactory.getInstance());
         final File file = new File(cexfile);
         PrintWriter printWriter = null;
         try {

subprojects/common/analysis/build.gradle.kts

@@ -23,6 +23,6 @@ dependencies {
     implementation(project(":theta-core"))
     implementation(project(":theta-solver"))
     implementation(project(":theta-graph-solver"))
-    testImplementation(project(":theta-solver-z3"))
+    testImplementation(project(":theta-solver-z3-legacy"))
     implementation("com.corundumstudio.socketio:netty-socketio:2.0.6")
 }

subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/BoundedTest.kt

@@ -28,7 +28,7 @@ import hu.bme.mit.theta.core.type.inttype.IntExprs
 import hu.bme.mit.theta.core.type.inttype.IntExprs.Int
 import hu.bme.mit.theta.core.utils.StmtUtils
 import hu.bme.mit.theta.core.utils.indexings.VarIndexingFactory
-import hu.bme.mit.theta.solver.z3.Z3SolverFactory
+import hu.bme.mit.theta.solver.z3.Z3LegacySolverFactory
 import org.junit.Assert
 import org.junit.Test
 
@@ -66,9 +66,9 @@ class BoundedTest {
 
     @Test
     fun testBoundedUnsafe() {
-        val solver = Z3SolverFactory.getInstance().createSolver()
-        val itpSolver = Z3SolverFactory.getInstance().createItpSolver()
-        val indSolver = Z3SolverFactory.getInstance().createSolver()
+        val solver = Z3LegacySolverFactory.getInstance().createSolver()
+        val itpSolver = Z3LegacySolverFactory.getInstance().createItpSolver()
+        val indSolver = Z3LegacySolverFactory.getInstance().createSolver()
         val checker: BoundedChecker<*, *> = BoundedChecker(
             monolithicExpr = unsafeMonolithicExpr!!,
             bmcSolver = solver,
@@ -83,9 +83,9 @@ class BoundedTest {
 
     @Test
     fun testBoundedSafe() {
-        val solver = Z3SolverFactory.getInstance().createSolver()
-        val itpSolver = Z3SolverFactory.getInstance().createItpSolver()
-        val indSolver = Z3SolverFactory.getInstance().createSolver()
+        val solver = Z3LegacySolverFactory.getInstance().createSolver()
+        val itpSolver = Z3LegacySolverFactory.getInstance().createItpSolver()
+        val indSolver = Z3LegacySolverFactory.getInstance().createSolver()
         val checker: BoundedChecker<*, *> = BoundedChecker(
             monolithicExpr = safeMonolithicExpr!!,
             bmcSolver = solver,

subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/expl/ExplInitFuncTest.java

@@ -32,13 +32,13 @@
 import hu.bme.mit.theta.core.decl.VarDecl;
 import hu.bme.mit.theta.core.type.inttype.IntType;
 import hu.bme.mit.theta.solver.Solver;
-import hu.bme.mit.theta.solver.z3.Z3SolverFactory;
+import hu.bme.mit.theta.solver.z3.Z3LegacySolverFactory;
 
 public class ExplInitFuncTest {
 
     private final VarDecl<IntType> x = Var("x", Int());
     private final VarDecl<IntType> y = Var("y", Int());
-    private final Solver solver = Z3SolverFactory.getInstance().createSolver();
+    private final Solver solver = Z3LegacySolverFactory.getInstance().createSolver();
 
     @Test
     public void test1() {

subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/expl/ExplStatePredicateTest.java

@@ -38,13 +38,13 @@
 import hu.bme.mit.theta.core.type.booltype.BoolType;
 import hu.bme.mit.theta.core.type.inttype.IntType;
 import hu.bme.mit.theta.solver.Solver;
-import hu.bme.mit.theta.solver.z3.Z3SolverFactory;
+import hu.bme.mit.theta.solver.z3.Z3LegacySolverFactory;
 
 @RunWith(Parameterized.class)
 public class ExplStatePredicateTest {
 
     private static final VarDecl<IntType> x = Var("x", Int());
-    private final Solver solver = Z3SolverFactory.getInstance().createSolver();
+    private final Solver solver = Z3LegacySolverFactory.getInstance().createSolver();
 
     @Parameter(value = 0)
     public Expr<BoolType> expr;

subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/expl/ExplStmtTransFuncTest.java

@@ -48,11 +48,11 @@
 import hu.bme.mit.theta.core.type.booltype.BoolExprs;
 import hu.bme.mit.theta.core.type.inttype.IntType;
 import hu.bme.mit.theta.solver.Solver;
-import hu.bme.mit.theta.solver.z3.Z3SolverFactory;
+import hu.bme.mit.theta.solver.z3.Z3LegacySolverFactory;
 
 public class ExplStmtTransFuncTest {
 
-    private final Solver solver = Z3SolverFactory.getInstance().createSolver();
+    private final Solver solver = Z3LegacySolverFactory.getInstance().createSolver();
     private final VarDecl<IntType> x = Var("x", Int());
     private final VarDecl<IntType> y = Var("y", Int());
 

subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/expl/ExplTransFuncTest.java

@@ -22,7 +22,7 @@
 import hu.bme.mit.theta.core.model.ImmutableValuation;
 import hu.bme.mit.theta.core.type.inttype.IntType;
 import hu.bme.mit.theta.core.utils.indexings.VarIndexingFactory;
-import hu.bme.mit.theta.solver.z3.Z3SolverFactory;
+import hu.bme.mit.theta.solver.z3.Z3LegacySolverFactory;
 import org.junit.Assert;
 import org.junit.Test;
 
@@ -44,7 +44,7 @@ public class ExplTransFuncTest {
     private final ExplState state = ExplState.of(
             ImmutableValuation.builder().put(x, Int(1)).build());
 
-    ExplTransFunc transFunc = ExplTransFunc.create(Z3SolverFactory.getInstance().createSolver());
+    ExplTransFunc transFunc = ExplTransFunc.create(Z3LegacySolverFactory.getInstance().createSolver());
 
     @Test
     public void testNormal() {

subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/expr/ExprOrdLeqTest.java

@@ -37,7 +37,7 @@
 import hu.bme.mit.theta.core.type.Expr;
 import hu.bme.mit.theta.core.type.inttype.IntType;
 import hu.bme.mit.theta.solver.Solver;
-import hu.bme.mit.theta.solver.z3.Z3SolverFactory;
+import hu.bme.mit.theta.solver.z3.Z3LegacySolverFactory;
 
 @RunWith(Parameterized.class)
 public final class ExprOrdLeqTest {
@@ -72,7 +72,7 @@ public static Collection<Object[]> data() {
 
     @Test
     public void testIsTop() {
-        final Solver solver = Z3SolverFactory.getInstance().createSolver();
+        final Solver solver = Z3LegacySolverFactory.getInstance().createSolver();
         final PartialOrd<ExprState> ord = ExprOrd.create(solver);
         assertEquals(ord.isLeq(state1, state2), leq);
     }

subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/expr/ExprStatesTest.java

@@ -24,7 +24,7 @@
 import hu.bme.mit.theta.core.utils.indexings.VarIndexing;
 import hu.bme.mit.theta.core.utils.indexings.VarIndexingFactory;
 import hu.bme.mit.theta.solver.Solver;
-import hu.bme.mit.theta.solver.z3.Z3SolverFactory;
+import hu.bme.mit.theta.solver.z3.Z3LegacySolverFactory;
 import org.junit.Assert;
 import org.junit.Test;
 
@@ -38,7 +38,7 @@ public class ExprStatesTest {
 
     private final VarDecl<IntType> vx = Var("x", Int());
     private final ExplPrec prec = ExplPrec.of(Collections.singleton(vx));
-    private final Solver solver = Z3SolverFactory.getInstance().createSolver();
+    private final Solver solver = Z3LegacySolverFactory.getInstance().createSolver();
 
     @Test
     public void test1() {

subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/expr/ExprTraceCheckersTest.java

@@ -28,7 +28,7 @@
 import hu.bme.mit.theta.core.utils.indexings.VarIndexingFactory;
 import hu.bme.mit.theta.solver.ItpSolver;
 import hu.bme.mit.theta.solver.UCSolver;
-import hu.bme.mit.theta.solver.z3.Z3SolverFactory;
+import hu.bme.mit.theta.solver.z3.Z3LegacySolverFactory;
 import org.junit.Before;
 import org.junit.Test;
 
@@ -56,8 +56,8 @@ public final class ExprTraceCheckersTest {
 
     @Before
     public void before() {
-        final ItpSolver itpSolver = Z3SolverFactory.getInstance().createItpSolver();
-        final UCSolver ucSolver = Z3SolverFactory.getInstance().createUCSolver();
+        final ItpSolver itpSolver = Z3LegacySolverFactory.getInstance().createItpSolver();
+        final UCSolver ucSolver = Z3LegacySolverFactory.getInstance().createUCSolver();
         traceCheckers = new ArrayList<>();
         traceCheckers.add(ExprTraceSeqItpChecker.create(True(), True(), itpSolver));
         traceCheckers.add(ExprTraceFwBinItpChecker.create(True(), True(), itpSolver));

subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/pred/PredInitFuncTest.java

@@ -35,13 +35,13 @@
 import hu.bme.mit.theta.core.decl.VarDecl;
 import hu.bme.mit.theta.core.type.inttype.IntType;
 import hu.bme.mit.theta.solver.Solver;
-import hu.bme.mit.theta.solver.z3.Z3SolverFactory;
+import hu.bme.mit.theta.solver.z3.Z3LegacySolverFactory;
 
 public class PredInitFuncTest {
 
     private final VarDecl<IntType> x = Var("x", Int());
     private final VarDecl<IntType> y = Var("y", Int());
-    private final Solver solver = Z3SolverFactory.getInstance().createSolver();
+    private final Solver solver = Z3LegacySolverFactory.getInstance().createSolver();
     private final PredAbstractor predAbstractor = PredAbstractors.booleanSplitAbstractor(solver);
 
     @Test

subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/pred/PredOrdTest.java

@@ -26,13 +26,13 @@
 import hu.bme.mit.theta.core.decl.Decls;
 import hu.bme.mit.theta.core.decl.VarDecl;
 import hu.bme.mit.theta.core.type.inttype.IntType;
-import hu.bme.mit.theta.solver.z3.Z3SolverFactory;
+import hu.bme.mit.theta.solver.z3.Z3LegacySolverFactory;
 
 public class PredOrdTest {
 
     private final VarDecl<IntType> VX = Decls.Var("x", Int());
 
-    private final PredOrd ord = PredOrd.create(Z3SolverFactory.getInstance().createSolver());
+    private final PredOrd ord = PredOrd.create(Z3LegacySolverFactory.getInstance().createSolver());
 
     PredState sb = PredState.of(False());
     PredState s1 = PredState.of(Gt(VX.getRef(), Int(1)));

subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/pred/PredTransFuncTest.java

@@ -39,13 +39,13 @@
 import hu.bme.mit.theta.core.stmt.Stmts;
 import hu.bme.mit.theta.core.type.inttype.IntType;
 import hu.bme.mit.theta.solver.Solver;
-import hu.bme.mit.theta.solver.z3.Z3SolverFactory;
+import hu.bme.mit.theta.solver.z3.Z3LegacySolverFactory;
 
 public class PredTransFuncTest {
 
     private final VarDecl<IntType> x = Var("x", Int());
     private final VarDecl<IntType> y = Var("y", Int());
-    private final Solver solver = Z3SolverFactory.getInstance().createSolver();
+    private final Solver solver = Z3LegacySolverFactory.getInstance().createSolver();
     private final PredTransFunc transFunc = PredTransFunc.create(
             PredAbstractors.booleanSplitAbstractor(solver));
 

subprojects/solver/graph-solver/build.gradle.kts

@@ -22,5 +22,5 @@ dependencies {
     implementation(project(":theta-common"))
     implementation(project(":theta-core"))
     implementation(project(":theta-solver"))
-    testImplementation(project(":theta-solver-z3"))
+    testImplementation(project(":theta-solver-z3-legacy"))
 }