Replaced sat check with tautology check in test

csanadtelbisz · Mar 24, 2024 · 6884d45 · 6884d45
1 parent 078aaf5
commit 6884d45
Show file tree

Hide file tree

Showing 3 changed files with 16 additions and 2 deletions.
diff --git a/subprojects/common/core/src/testFixtures/java/hu/bme/mit/theta/core/utils/BoolTestUtils.java b/subprojects/common/core/src/testFixtures/java/hu/bme/mit/theta/core/utils/BoolTestUtils.java
@@ -26,7 +26,9 @@
 import java.util.Collection;
 import java.util.List;
 
+import static hu.bme.mit.theta.core.decl.Decls.Const;
 import static hu.bme.mit.theta.core.decl.Decls.Param;
+import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Geq;
 import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Ite;
 import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Lt;
 import static hu.bme.mit.theta.core.type.booltype.BoolExprs.And;
@@ -49,10 +51,12 @@ public static Collection<?> BasicOperations() {
         final var p1 = Param("x", Int());
         final var p2 = Param("y", Int());
         final var p3 = Param("z", Int());
+        final var c1 = Const("c", Int());
 
         return Arrays.asList(new Object[][]{
 
-                {IteExpr.class, Int(1), Ite(False(), Int(2), Int(1))},
+                {IteExpr.class, Ite(Geq(c1.getRef(), Int(0)), Int(1), Int(2)), Ite(Lt(c1.getRef(), Int(0)), Int(2), Int(1))},
+                {ImplyExpr.class, False(), Imply(True(), False())},
                 {ImplyExpr.class, False(), Imply(True(), False())},
                 {XorExpr.class, False(), Xor(True(), True())},
                 {OrExpr.class, True(), Or(True(), True())},

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
@@ -112,6 +112,7 @@ public JavaSMTTermTransformer(final JavaSMTSymbolTable symbolTable, SolverContex
         addFunc("xor", exprBinaryOperator(hu.bme.mit.theta.core.type.booltype.XorExpr::create));
         addFunc("or", exprMultiaryOperator(hu.bme.mit.theta.core.type.booltype.OrExpr::create));
         addFunc("ite", exprTernaryOperator(hu.bme.mit.theta.core.type.anytype.IteExpr::create));
+        addFunc("if", exprTernaryOperator(hu.bme.mit.theta.core.type.anytype.IteExpr::create));
         addFunc("prime", exprUnaryOperator(hu.bme.mit.theta.core.type.anytype.PrimeExpr::of));
         addFunc("=", exprBinaryOperator(hu.bme.mit.theta.core.type.abstracttype.AbstractExprs::Eq));
         addFunc(">=", exprBinaryOperator(hu.bme.mit.theta.core.type.abstracttype.AbstractExprs::Geq));
@@ -172,7 +173,9 @@ public JavaSMTTermTransformer(final JavaSMTSymbolTable symbolTable, SolverContex
         addFunc("bvashr", exprBinaryOperator(hu.bme.mit.theta.core.type.bvtype.BvArithShiftRightExpr::create));
         addFunc("bvlshr", exprBinaryOperator(hu.bme.mit.theta.core.type.bvtype.BvLogicShiftRightExpr::create));
         addFunc("bvrol", exprBinaryOperator(hu.bme.mit.theta.core.type.bvtype.BvRotateLeftExpr::create));
+        addFunc("ext_rotate_left", exprBinaryOperator(hu.bme.mit.theta.core.type.bvtype.BvRotateLeftExpr::create));
         addFunc("bvror", exprBinaryOperator(hu.bme.mit.theta.core.type.bvtype.BvRotateRightExpr::create));
+        addFunc("ext_rotate_right", exprBinaryOperator(hu.bme.mit.theta.core.type.bvtype.BvRotateRightExpr::create));
         addFunc("bvult", exprBinaryOperator(hu.bme.mit.theta.core.type.bvtype.BvULtExpr::create));
         addFunc("bvule", exprBinaryOperator(hu.bme.mit.theta.core.type.bvtype.BvULeqExpr::create));
         addFunc("bvugt", exprBinaryOperator(hu.bme.mit.theta.core.type.bvtype.BvUGtExpr::create));

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
@@ -46,6 +46,7 @@
 import java.util.stream.Collectors;
 
 import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Eq;
+import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Not;
 import static org.junit.Assert.assertNotNull;
 import static org.junit.Assume.assumeFalse;
 import static org.junit.runners.Parameterized.Parameters;
@@ -114,8 +115,14 @@ public void testRoundtripTransformer() throws Exception {
                     throw e; // for functions, we don't want the solver to step in
                 }
                 try (final var solver = JavaSMTSolverFactory.create(this.solver, new String[]{}).createSolver()) {
+                    solver.push();
                     solver.add(Eq(expr, expExpr));
-                    Assert.assertTrue(solver.check().isSat());
+                    Assert.assertTrue("(= %s %s) is unsat\n".formatted(expr, expExpr), solver.check().isSat());
+                    solver.pop();
+                    solver.push();
+                    solver.add(Not(Eq(expr, expExpr)));
+                    Assert.assertTrue("(not (= %s %s)) is sat with model %s\n".formatted(expr, expExpr, solver.check().isSat() ? solver.getModel() : ""), solver.check().isUnsat());
+                    solver.pop();
                 }
             }
         }