Added CVC5 libraries, fixed some bugs

ftsrg · Mar 18, 2024 · 4337a71 · 4337a71
1 parent d0eba27
commit 4337a71
Show file tree

Hide file tree

Showing 18 changed files with 184 additions and 91 deletions.
diff --git a/buildSrc/src/main/kotlin/Deps.kt b/buildSrc/src/main/kotlin/Deps.kt
@@ -28,6 +28,8 @@ object Deps {
     val z3 = "lib/com.microsoft.z3.jar"
     val z3legacy = "lib/com.microsoft.z3legacy.jar"
 
+    val cvc5 = "lib/cvc5.jar"
+
     val javasmt = "org.sosy-lab:java-smt:${Versions.javasmt}"
 
     val jcommander = "com.beust:jcommander:${Versions.jcommander}"

diff --git a/lib/cvc5.jar b/lib/cvc5.jar
diff --git a/lib/libcvc5.so.1 b/lib/libcvc5.so.1
diff --git a/lib/libcvc5jni.so b/lib/libcvc5jni.so
diff --git a/lib/libcvc5parser.so b/lib/libcvc5parser.so
diff --git a/lib/libcvc5parser.so.1 b/lib/libcvc5parser.so.1
diff --git a/lib/libpoly.so.0 b/lib/libpoly.so.0
diff --git a/lib/libpolyxx.so.0 b/lib/libpolyxx.so.0
diff --git a/subprojects/solver/solver-javasmt/build.gradle.kts b/subprojects/solver/solver-javasmt/build.gradle.kts
@@ -22,5 +22,6 @@ dependencies {
     implementation(project(":theta-core"))
     implementation(project(":theta-solver"))
     implementation(Deps.javasmt)
+    implementation(files(rootDir.resolve(Deps.cvc5)))
     testImplementation(testFixtures(project(":theta-core")))
 }
diff --git a/.../solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTExprTransformer.java b/.../solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTExprTransformer.java
@@ -161,6 +161,7 @@
 import java.util.ArrayList;
 import java.util.List;
 import java.util.concurrent.ExecutionException;
+import java.util.function.Supplier;
 import java.util.stream.Stream;
 
 final class JavaSMTExprTransformer {
@@ -186,13 +187,13 @@ public JavaSMTExprTransformer(final JavaSMTTransformationManager transformer, fi
         this.transformer = transformer;
         this.env = new Env();
 
-        booleanFormulaManager = context.getFormulaManager().getBooleanFormulaManager();
-        integerFormulaManager = context.getFormulaManager().getIntegerFormulaManager();
-        rationalFormulaManager = context.getFormulaManager().getRationalFormulaManager();
-        bitvectorFormulaManager = context.getFormulaManager().getBitvectorFormulaManager();
-        floatingPointFormulaManager = context.getFormulaManager().getFloatingPointFormulaManager();
-        quantifiedFormulaManager = context.getFormulaManager().getQuantifiedFormulaManager();
-        arrayFormulaManager= context.getFormulaManager().getArrayFormulaManager();
+        booleanFormulaManager = orElseNull(() -> context.getFormulaManager().getBooleanFormulaManager());
+        integerFormulaManager = orElseNull(() -> context.getFormulaManager().getIntegerFormulaManager());
+        rationalFormulaManager = orElseNull(() -> context.getFormulaManager().getRationalFormulaManager());
+        bitvectorFormulaManager = orElseNull(() -> context.getFormulaManager().getBitvectorFormulaManager());
+        floatingPointFormulaManager = orElseNull(() -> context.getFormulaManager().getFloatingPointFormulaManager());
+        quantifiedFormulaManager = orElseNull(() -> context.getFormulaManager().getQuantifiedFormulaManager());
+        arrayFormulaManager = orElseNull(() -> context.getFormulaManager().getArrayFormulaManager());
 
         exprToTerm = CacheBuilder.newBuilder().maximumSize(CACHE_SIZE).build();
 
@@ -435,6 +436,13 @@ public JavaSMTExprTransformer(final JavaSMTTransformationManager transformer, fi
                 .build();
     }
 
+    private static <T> T orElseNull(Supplier<T> supplier) {
+        try {
+            return supplier.get();
+        } catch (UnsupportedOperationException uoe) {
+            return null;
+        }
+    }
     private static Tuple2<Expr<?>, List<Expr<?>>> extractFuncAndArgs(final FuncAppExpr<?, ?> expr) {
         final Expr<?> func = expr.getFunc();
         final Expr<?> arg = expr.getParam();
@@ -887,7 +895,7 @@ private Formula transformBvSMod(final BvSModExpr expr) {
         final BitvectorFormula leftOpTerm = (BitvectorFormula) toTerm(expr.getLeftOp());
         final BitvectorFormula rightOpTerm = (BitvectorFormula) toTerm(expr.getRightOp());
 
-        return bitvectorFormulaManager.modulo(leftOpTerm, rightOpTerm, true);
+        return bitvectorFormulaManager.modulo(leftOpTerm, rightOpTerm, true); // TODO: this will create an SREM instruction, which is faulty.
     }
 
     private Formula transformBvURem(final BvURemExpr expr) {
@@ -1208,7 +1216,7 @@ private Formula transformFpFromBv(final FpFromBvExpr expr) {
     private Formula transformFpToBv(final FpToBvExpr expr) {
         final FloatingPointFormula op = (FloatingPointFormula) toTerm(expr.getOp());
 
-        return floatingPointFormulaManager.toIeeeBitvector(op);
+        return floatingPointFormulaManager.castTo(op, expr.getSgn(), FormulaType.getBitvectorTypeWithSize(expr.getSize()));
     }
     /*
      * Arrays
@@ -1220,7 +1228,7 @@ private Formula transformFpToFp(final FpToFpExpr expr) {
         return floatingPointFormulaManager.castTo(
                 op,
                 true, // ignored
-                FloatingPointType.getFloatingPointType(expr.getExpBits(), expr.getSignBits()),
+                FloatingPointType.getFloatingPointType(expr.getExpBits(), expr.getSignBits() - 1),
                 transformFpRoundingMode(expr.getRoundingMode()));
     }
 

diff --git a/...solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTItpSolver.java b/...solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTItpSolver.java
@@ -40,6 +40,7 @@
 import static com.google.common.base.Preconditions.checkArgument;
 import static com.google.common.base.Preconditions.checkNotNull;
 import static com.google.common.base.Preconditions.checkState;
+import static hu.bme.mit.theta.core.type.booltype.BoolExprs.False;
 
 final class JavaSMTItpSolver implements ItpSolver, Solver {
 
@@ -97,17 +98,26 @@ public Interpolant getInterpolant(final ItpPattern pattern) {
         checkArgument(pattern instanceof JavaSMTItpPattern);
         final List<JavaSMTItpMarker> z3ItpPattern = ((JavaSMTItpPattern) pattern).getSequence();
 
+
         try {
             final List<BooleanFormula> interpolants = interpolatingProverEnvironment.getSeqInterpolants(z3ItpPattern.stream().
                     map(javaSMTItpMarker -> javaSMTItpMarker.getTerms().stream().
-                            map(transformationManager::toTerm).toList()).
+                            map(expr1 -> {
+                                var term = transformationManager.toTerm(expr1);
+                                try {
+                                    return interpolatingProverEnvironment.addConstraint((BooleanFormula) term);
+                                } catch (InterruptedException e) {
+                                    throw new JavaSMTSolverException(e);
+                                }
+                            }).toList()).
                     toList());
             Map<ItpMarker, Expr<BoolType>> itpMap = Containers.createMap();
             for (int i = 0; i < interpolants.size(); i++) {
                 BooleanFormula term = interpolants.get(i);
                 Expr<BoolType> expr = (Expr<BoolType>) termTransformer.toExpr(term);
                 itpMap.put(z3ItpPattern.get(i), expr);
             }
+            itpMap.put(z3ItpPattern.get(interpolants.size()), False());
             return new JavaSMTInterpolant(itpMap);
         } catch (SolverException | InterruptedException e) {
             throw new JavaSMTSolverException(e);