Fixed interpolation, and tests

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

Hide file tree

Showing 7 changed files with 45 additions and 29 deletions.
diff --git a/...solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTItpMarker.java b/...solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTItpMarker.java
@@ -15,8 +15,6 @@
  */
 package hu.bme.mit.theta.solver.javasmt;
 
-import hu.bme.mit.theta.core.type.Expr;
-import hu.bme.mit.theta.core.type.booltype.BoolType;
 import hu.bme.mit.theta.solver.ItpMarker;
 import hu.bme.mit.theta.solver.Stack;
 import hu.bme.mit.theta.solver.impl.StackImpl;
@@ -25,15 +23,15 @@
 
 import static com.google.common.base.Preconditions.checkNotNull;
 
-final class JavaSMTItpMarker implements ItpMarker {
+final class JavaSMTItpMarker<T> implements ItpMarker {
 
-    private final Stack<Expr<BoolType>> terms;
+    private final Stack<T> terms;
 
     public JavaSMTItpMarker() {
         terms = new StackImpl<>();
     }
 
-    public void add(final Expr<BoolType> term) {
+    public void add(final T term) {
         terms.add(checkNotNull(term));
     }
 
@@ -45,7 +43,7 @@ public void pop(final int n) {
         terms.pop(n);
     }
 
-    public Collection<Expr<BoolType>> getTerms() {
+    public Collection<T> getTerms() {
         return terms.toCollection();
     }
 

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
@@ -87,8 +87,8 @@ public void add(final ItpMarker marker, final Expr<BoolType> assertion) {
         checkArgument(markers.toCollection().contains(marker), "Marker not found in solver");
         final JavaSMTItpMarker z3Marker = (JavaSMTItpMarker) marker;
         BooleanFormula term = (BooleanFormula) transformationManager.toTerm(assertion);
-        solver.add(assertion, term);
-        z3Marker.add(assertion);
+        Object c = solver.add(assertion, term);
+        z3Marker.add(c);
     }
 
     @Override
@@ -100,17 +100,9 @@ public Interpolant getInterpolant(final ItpPattern pattern) {
 
 
         try {
-            final List<BooleanFormula> interpolants = interpolatingProverEnvironment.getSeqInterpolants(z3ItpPattern.stream().
-                    map(javaSMTItpMarker -> javaSMTItpMarker.getTerms().stream().
-                            map(expr1 -> {
-                                var term = transformationManager.toTerm(expr1);
-                                try {
-                                    return interpolatingProverEnvironment.addConstraint((BooleanFormula) term);
-                                } catch (InterruptedException e) {
-                                    throw new JavaSMTSolverException(e);
-                                }
-                            }).toList()).
-                    toList());
+            final List<BooleanFormula> interpolants =
+                    interpolatingProverEnvironment.getSeqInterpolants(
+                            z3ItpPattern.stream().map(JavaSMTItpMarker::getTerms).toList());
             Map<ItpMarker, Expr<BoolType>> itpMap = Containers.createMap();
             for (int i = 0; i < interpolants.size(); i++) {
                 BooleanFormula term = interpolants.get(i);

diff --git a/...ts/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTSolver.java b/...ts/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTSolver.java
@@ -94,14 +94,16 @@ public void add(final Expr<BoolType> assertion) {
         add(assertion, term);
     }
 
-    void add(final Expr<BoolType> assertion, final BooleanFormula term) {
+    Object add(final Expr<BoolType> assertion, final BooleanFormula term) {
         assertions.add(assertion);
+        Object ret;
         try {
-            solver.addConstraint(term);
+            ret = solver.addConstraint(term);
         } catch (InterruptedException e) {
             throw new JavaSMTSolverException(e);
         }
         clearState();
+        return ret;
     }
 
 

diff --git a/.../solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTTermTransformer.java b/.../solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTTermTransformer.java
@@ -23,6 +23,7 @@
 import hu.bme.mit.theta.core.decl.Decl;
 import hu.bme.mit.theta.core.type.Expr;
 import hu.bme.mit.theta.core.type.Type;
+import hu.bme.mit.theta.core.type.abstracttype.AbstractExprs;
 import hu.bme.mit.theta.core.type.bvtype.BvExtractExpr;
 import hu.bme.mit.theta.core.type.bvtype.BvLitExpr;
 import hu.bme.mit.theta.core.type.bvtype.BvSExtExpr;
@@ -36,6 +37,7 @@
 import hu.bme.mit.theta.core.type.functype.FuncType;
 import hu.bme.mit.theta.core.type.inttype.IntLitExpr;
 import hu.bme.mit.theta.core.utils.BvUtils;
+import hu.bme.mit.theta.core.utils.TypeUtils;
 import org.sosy_lab.common.rationals.Rational;
 import org.sosy_lab.java_smt.api.ArrayFormula;
 import org.sosy_lab.java_smt.api.BitvectorFormula;
@@ -220,6 +222,10 @@ public JavaSMTTermTransformer(final JavaSMTSymbolTable symbolTable, SolverContex
             final Expr<BvType> op = (Expr<BvType>) transform(args.get(0), model, vars);
             return BvSExtExpr.of(op, BvType.of(type.getSize()));
         });
+        environment.put(Tuple2.of("EqZero", 1), (term, args, model, vars) -> {
+            final Expr<?> op = transform(args.get(0), model, vars);
+            return AbstractExprs.Eq(op, TypeUtils.getDefaultValue(op.getType()));
+        });
     }
 
     private void addFunc(String name, Tuple2<Integer, QuadFunction<Formula, List<Formula>, Model, List<Decl<?>>, Expr<?>>> func) {

diff --git a/...er/solver-javasmt/src/test/java/hu/bme/mit/theta/solver/javasmt/JavaSMTItpSolverTest.java b/...er/solver-javasmt/src/test/java/hu/bme/mit/theta/solver/javasmt/JavaSMTItpSolverTest.java
@@ -64,7 +64,7 @@ public final class JavaSMTItpSolverTest {
 
     @Before
     public void initialize() {
-        solver = JavaSMTSolverFactory.create(Solvers.CVC5, new String[]{}).createItpSolver();
+        solver = JavaSMTSolverFactory.create(Solvers.SMTINTERPOL, new String[]{}).createItpSolver();
 
         final ConstDecl<IntType> ad = Const("a", Int());
         final ConstDecl<IntType> bd = Const("b", Int());
@@ -158,7 +158,7 @@ public void testTreeInterpolation() {
         System.out.println("----------");
     }
 
-    //    @Test
+    @Test
     public void testLIA() {
         final ItpMarker A = solver.createMarker();
         final ItpMarker B = solver.createMarker();

diff --git a/...olver/solver-javasmt/src/test/java/hu/bme/mit/theta/solver/javasmt/JavaSMTSolverTest.java b/...olver/solver-javasmt/src/test/java/hu/bme/mit/theta/solver/javasmt/JavaSMTSolverTest.java
@@ -15,6 +15,8 @@
  */
 package hu.bme.mit.theta.solver.javasmt;
 
+import hu.bme.mit.theta.common.OsHelper;
+import hu.bme.mit.theta.common.OsHelper.OperatingSystem;
 import hu.bme.mit.theta.common.Tuple2;
 import hu.bme.mit.theta.core.decl.ConstDecl;
 import hu.bme.mit.theta.core.decl.ParamDecl;
@@ -79,11 +81,18 @@ public final class JavaSMTSolverTest {
 
     @Parameters(name = "solver: {0}")
     public static Collection<?> operations() {
-        return Arrays.asList(new Object[][]{
-                {Solvers.Z3, JavaSMTSolverFactory.create(Solvers.Z3, new String[]{}).createSolver()},
-                {Solvers.CVC5, JavaSMTSolverFactory.create(Solvers.CVC5, new String[]{}).createSolver()},
-                {Solvers.PRINCESS, JavaSMTSolverFactory.create(Solvers.PRINCESS, new String[]{}).createSolver()},
-        });
+        if (OsHelper.getOs().equals(OperatingSystem.LINUX)) {
+            return Arrays.asList(new Object[][]{
+                    {Solvers.Z3, JavaSMTSolverFactory.create(Solvers.Z3, new String[]{}).createSolver()},
+                    {Solvers.CVC5, JavaSMTSolverFactory.create(Solvers.CVC5, new String[]{}).createSolver()},
+                    {Solvers.PRINCESS, JavaSMTSolverFactory.create(Solvers.PRINCESS, new String[]{}).createSolver()},
+            });
+        } else {
+            return Arrays.asList(new Object[][]{
+                    {Solvers.Z3, JavaSMTSolverFactory.create(Solvers.Z3, new String[]{}).createSolver()},
+                    {Solvers.PRINCESS, JavaSMTSolverFactory.create(Solvers.PRINCESS, new String[]{}).createSolver()},
+            });
+        }
     }
 
     @Test

diff --git a/.../solver-javasmt/src/test/java/hu/bme/mit/theta/solver/javasmt/JavaSMTTransformerTest.java b/.../solver-javasmt/src/test/java/hu/bme/mit/theta/solver/javasmt/JavaSMTTransformerTest.java
@@ -16,6 +16,8 @@
 package hu.bme.mit.theta.solver.javasmt;
 
 import com.google.common.collect.Sets;
+import hu.bme.mit.theta.common.OsHelper;
+import hu.bme.mit.theta.common.OsHelper.OperatingSystem;
 import hu.bme.mit.theta.core.type.Expr;
 import hu.bme.mit.theta.core.type.bvtype.BvRotateLeftExpr;
 import hu.bme.mit.theta.core.type.bvtype.BvRotateRightExpr;
@@ -57,6 +59,13 @@ public class JavaSMTTransformerTest {
 
     @Parameters(name = "expr: {0}, solver: {1}")
     public static Collection<?> operations() {
+        final Set<Solvers> solvers;
+        if (OsHelper.getOs().equals(OperatingSystem.LINUX)) {
+            solvers = Set.of(Solvers.Z3, Solvers.CVC5, Solvers.PRINCESS);
+        } else {
+            solvers = Set.of(Solvers.Z3, Solvers.PRINCESS);
+        }
+
         return Sets.cartesianProduct(Stream.of(
                 BvTestUtils.BasicOperations().stream().map(o -> ((Object[])o)[2]),
                 BvTestUtils.BitvectorOperations().stream().map(o -> ((Object[])o)[2]),
@@ -71,7 +80,7 @@ public static Collection<?> operations() {
                 IntTestUtils.BasicOperations().stream().map(o -> ((Object[])o)[1])
         ).reduce(Stream::concat).get()
                 .filter(JavaSMTTransformerTest::supported)
-                        .collect(Collectors.toSet()), Set.of(Solvers.Z3, Solvers.CVC5, Solvers.PRINCESS)).stream()
+                        .collect(Collectors.toSet()), Set.of()).stream()
                 .map(objects -> new Object[]{objects.get(0), objects.get(1)}).toList();
     }