diff --git a/.classpath b/.classpath index 52a207f1a7..54849d8b59 100644 --- a/.classpath +++ b/.classpath @@ -28,6 +28,8 @@ SPDX-License-Identifier: Apache-2.0 + + diff --git a/.idea/JavaSMT.iml b/.idea/JavaSMT.iml index c9ee959dbd..7078551355 100644 --- a/.idea/JavaSMT.iml +++ b/.idea/JavaSMT.iml @@ -190,6 +190,24 @@ SPDX-License-Identifier: Apache-2.0 + + + + + + + + + + + + + + + + + + diff --git a/build.xml b/build.xml index 2cb4a302ae..ceba6e1ba9 100644 --- a/build.xml +++ b/build.xml @@ -31,7 +31,8 @@ SPDX-License-Identifier: Apache-2.0 runtime-princess, runtime-smtinterpol, runtime-yices2, - runtime-z3 + runtime-z3, + runtime-apron "/> diff --git a/build/build-publish-solvers.xml b/build/build-publish-solvers.xml index b88aea311f..e503c59537 100644 --- a/build/build-publish-solvers.xml +++ b/build/build-publish-solvers.xml @@ -11,7 +11,7 @@ SPDX-License-Identifier: Apache-2.0 --> - + @@ -20,5 +20,6 @@ SPDX-License-Identifier: Apache-2.0 + diff --git a/build/build-publish-solvers/solver-apron.xml b/build/build-publish-solvers/solver-apron.xml new file mode 100644 index 0000000000..1bca8a3577 --- /dev/null +++ b/build/build-publish-solvers/solver-apron.xml @@ -0,0 +1,108 @@ + + + + + + + + + + + + + Please specify the path to Apron with the flag -Dapron.path=/path/to/apron. + The path has to point to the root Apron folder, i.e., + a checkout of the official git repositoy from 'https://github.com/antoinemine/apron'. + Note that shell substitutions do not work and a full absolute path has to be specified. + + + Please specify a custom revision with the flag -Dapron.customRev=XXX. + The custom revision has to be unique amongst the already known version + numbers from the ivy repository. The script will append the git revision. + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/lib/ivy.xml b/lib/ivy.xml index d24ed0975a..4d512978c1 100644 --- a/lib/ivy.xml +++ b/lib/ivy.xml @@ -18,7 +18,8 @@ SPDX-License-Identifier: Apache-2.0 - Java wrapper for SMT solvers like Z3, MathSAT5, SMTInterpol, Princess, CVC4, CVC5, Boolector, and Yices2. + Java wrapper for SMT solvers like Z3, MathSAT5, SMTInterpol, Princess, CVC4, CVC5, + Boolector, Yices2, OpenSMT and Apron. @@ -41,6 +42,7 @@ SPDX-License-Identifier: Apache-2.0 + @@ -165,6 +167,7 @@ SPDX-License-Identifier: Apache-2.0 + diff --git a/lib/native/x86_64-linux/libapron.so b/lib/native/x86_64-linux/libapron.so new file mode 120000 index 0000000000..2060d3f718 --- /dev/null +++ b/lib/native/x86_64-linux/libapron.so @@ -0,0 +1 @@ +lib/java/runtime-apron/libapron.so \ No newline at end of file diff --git a/lib/native/x86_64-linux/libboxD.so b/lib/native/x86_64-linux/libboxD.so new file mode 120000 index 0000000000..adf9f30bef --- /dev/null +++ b/lib/native/x86_64-linux/libboxD.so @@ -0,0 +1 @@ +lib/java/runtime-apron/libboxD.so \ No newline at end of file diff --git a/lib/native/x86_64-linux/libjapron.so b/lib/native/x86_64-linux/libjapron.so new file mode 120000 index 0000000000..7b15aac3cc --- /dev/null +++ b/lib/native/x86_64-linux/libjapron.so @@ -0,0 +1 @@ +lib/java/runtime-apron/libjapron.so \ No newline at end of file diff --git a/lib/native/x86_64-linux/libjgmp.so b/lib/native/x86_64-linux/libjgmp.so new file mode 120000 index 0000000000..c7a7f443fd --- /dev/null +++ b/lib/native/x86_64-linux/libjgmp.so @@ -0,0 +1 @@ +lib/java/runtime-apron/libjgmp.so \ No newline at end of file diff --git a/lib/native/x86_64-linux/liboctD.so b/lib/native/x86_64-linux/liboctD.so new file mode 120000 index 0000000000..f36a41b056 --- /dev/null +++ b/lib/native/x86_64-linux/liboctD.so @@ -0,0 +1 @@ +lib/java/runtime-apron/liboctD.so \ No newline at end of file diff --git a/lib/native/x86_64-linux/libpolkaMPQ.so b/lib/native/x86_64-linux/libpolkaMPQ.so new file mode 120000 index 0000000000..2e09ce7d43 --- /dev/null +++ b/lib/native/x86_64-linux/libpolkaMPQ.so @@ -0,0 +1 @@ +lib/java/runtime-apron/libpolkaMPQ.so \ No newline at end of file diff --git a/solvers_ivy_conf/ivy_apron.xml b/solvers_ivy_conf/ivy_apron.xml new file mode 100644 index 0000000000..9cda8a9d14 --- /dev/null +++ b/solvers_ivy_conf/ivy_apron.xml @@ -0,0 +1,41 @@ + + + + + + + + + Apron Numerical Abstract Domain library. + Apron provided with GNU Lesser General Public License. + + + + + + + + + + + + + + + + + + + + + \ No newline at end of file diff --git a/src/org/sosy_lab/java_smt/SolverContextFactory.java b/src/org/sosy_lab/java_smt/SolverContextFactory.java index f5754b32ad..aca2aaeb09 100644 --- a/src/org/sosy_lab/java_smt/SolverContextFactory.java +++ b/src/org/sosy_lab/java_smt/SolverContextFactory.java @@ -29,6 +29,7 @@ import org.sosy_lab.java_smt.delegate.logging.LoggingSolverContext; import org.sosy_lab.java_smt.delegate.statistics.StatisticsSolverContext; import org.sosy_lab.java_smt.delegate.synchronize.SynchronizedSolverContext; +import org.sosy_lab.java_smt.solvers.apron.ApronSolverContext; import org.sosy_lab.java_smt.solvers.boolector.BoolectorSolverContext; import org.sosy_lab.java_smt.solvers.cvc4.CVC4SolverContext; import org.sosy_lab.java_smt.solvers.cvc5.CVC5SolverContext; @@ -57,7 +58,8 @@ public enum Solvers { BOOLECTOR, CVC4, CVC5, - YICES2 + YICES2, + APRON } @Option(secure = true, description = "Export solver queries in SmtLib format into a file.") @@ -290,6 +292,9 @@ private SolverContext generateContext0(Solvers solverToCreate) case BOOLECTOR: return BoolectorSolverContext.create(config, shutdownNotifier, logfile, randomSeed, loader); + case APRON: + return ApronSolverContext.create(nonLinearArithmetic, shutdownNotifier, logger); + default: throw new AssertionError("no solver selected"); } diff --git a/src/org/sosy_lab/java_smt/solvers/apron/ApronApiTest.java b/src/org/sosy_lab/java_smt/solvers/apron/ApronApiTest.java new file mode 100644 index 0000000000..7f4adb86de --- /dev/null +++ b/src/org/sosy_lab/java_smt/solvers/apron/ApronApiTest.java @@ -0,0 +1,239 @@ +// This file is part of JavaSMT, +// an API wrapper for a collection of SMT solvers: +// https://github.com/sosy-lab/java-smt +// +// SPDX-FileCopyrightText: 2024 Dirk Beyer +// +// SPDX-License-Identifier: Apache-2.0 + +package org.sosy_lab.java_smt.solvers.apron; + +import static com.google.common.truth.Truth.assertThat; +import static com.google.common.truth.Truth.assertWithMessage; + +import apron.Abstract1; +import apron.ApronException; +import apron.Environment; +import apron.Lincons1; +import apron.Manager; +import apron.MpqScalar; +import apron.Polka; +import apron.PolkaEq; +import apron.Tcons1; +import apron.Texpr0Node; +import apron.Texpr1BinNode; +import apron.Texpr1CstNode; +import apron.Texpr1Node; +import apron.Texpr1VarNode; +import com.google.common.base.Preconditions; +import org.junit.AssumptionViolatedException; +import org.junit.BeforeClass; +import org.junit.Test; +import org.sosy_lab.common.NativeLibraries; + +public class ApronApiTest { + + public static Manager manager = new PolkaEq(); + + @BeforeClass + public static void loadApron() { + try { + NativeLibraries.loadLibrary("japron"); + NativeLibraries.loadLibrary("jgmp"); + } catch (UnsatisfiedLinkError e) { + throw new AssumptionViolatedException("Apron is not available", e); + } + } + + @Test + public void solverBackendTest() {} + + /** + * Simple Example that shows how to build constraints in Apron. + * + * @throws ApronException throws Exception + */ + @Test + public void example() throws ApronException { + Manager pManager = new Polka(false); + String[] intVars = {"x"}; + String[] realVars = {"y"}; + + Environment environment = new Environment(intVars, realVars); + // x <= 2 and x >= -3 + // x <= 2 --> -x+2 >= 0 + Lincons1 cons1 = new Lincons1(environment); + cons1.setCoeff("x", new MpqScalar(-1)); + cons1.setCst(new MpqScalar(+2)); + cons1.setKind(Lincons1.SUPEQ); + // x >= - 3 --> x+3 >= 0 + Lincons1 cons2 = new Lincons1(environment); + cons2.setCoeff("x", new MpqScalar(1)); + cons2.setCst(new MpqScalar(+3)); + cons2.setKind(Lincons1.SUPEQ); + Abstract1 abstract1 = new Abstract1(pManager, new Lincons1[] {cons1, cons2}); + assertWithMessage("The domain is not UNSAT for sure.") + .that(abstract1.isBottom(pManager)) + .isFalse(); + } + + /** + * This test shows an example where Apron fails to give a correct solution for a set of + * constraints that should be unsat; This behavior is not unintended, because some domains can not + * represent exact disjunctions like != (https://github.com/antoinemine/apron/issues/92). + * + * @throws ApronException throws exception + */ + @Test + public void distinctTest() throws ApronException { + // x,y = 1 and x!=y + Texpr1VarNode x = new Texpr1VarNode("x"); + Texpr1VarNode y = new Texpr1VarNode("y"); + Texpr1BinNode leftArg = new Texpr1BinNode(Texpr1BinNode.OP_SUB, x, y); + Environment environment = new Environment(new String[] {"x", "y"}, new String[] {}); + Tcons1 xIsZero = new Tcons1(environment, Tcons1.EQ, x); + Tcons1 yIsZero = new Tcons1(environment, Tcons1.EQ, y); + Tcons1 constraint = new Tcons1(environment, Tcons1.DISEQ, leftArg); + Abstract1 abstract1 = new Abstract1(manager, new Tcons1[] {xIsZero, yIsZero, constraint}); + Preconditions.checkArgument(!abstract1.isBottom(manager)); // should return isBottom == true, + // but doesn't!!! + } + + /** + * Test that gives an example of how a domain simplifies constraints. + * + * @throws ApronException throws exception + */ + @Test + public void addConstraintsTest() throws ApronException { + // x+x = 0 and x = 0 is added as only one constraints + Texpr1VarNode x = new Texpr1VarNode("x"); + Texpr1BinNode add = new Texpr1BinNode(Texpr1BinNode.OP_ADD, x, x); + Environment environment = new Environment(new String[] {"x"}, new String[] {}); + Tcons1 isZero = new Tcons1(environment, Tcons1.EQ, add); + Tcons1 xisZero = new Tcons1(environment, Tcons1.EQ, x); + Abstract1 abstract1 = new Abstract1(manager, new Tcons1[] {isZero, xisZero}); + assertThat(abstract1.toTcons(manager).length).isEqualTo(1); + } + + /** Somehow the hasVar() method does only work for nodes of level 0. */ + @Test + public void hasVarTest() { + // code form github + Texpr1VarNode x = new Texpr1VarNode("x"); + Environment environment = new Environment(new String[] {"x"}, new String[] {}); + System.out.println(x.hasVar("x")); + Texpr0Node xZero = x.toTexpr0Node(environment); + System.out.println(xZero.hasDim(environment.dimOfVar("x"))); + + // has Texpr1VarNode "x"? + Texpr1VarNode x1 = new Texpr1VarNode("x"); + Environment environment1 = new Environment(new String[] {"x"}, new String[] {"y"}); + assertThat(x1.hasVar("x")).isFalse(); // should be true + assertThat(x1.hasVar("y")).isFalse(); + Texpr0Node xZero1 = x.toTexpr0Node(environment1); + assertThat(xZero1.hasDim(environment1.dimOfVar("x"))).isTrue(); + assertThat(xZero1.hasDim(environment1.dimOfVar("y"))).isFalse(); + + // has x+x "x"? + Texpr1BinNode xPlusx = new Texpr1BinNode(Texpr1BinNode.OP_ADD, x, x); + assertThat(xPlusx.hasVar("x")).isFalse(); // should be true + Texpr0Node zeroxPlusx = xPlusx.toTexpr0Node(environment); + assertThat(zeroxPlusx.hasDim(environment.dimOfVar("x"))).isTrue(); + } + + /** + * For having the correct behaviour for Integer nodes one has to specify the rounding type + * (Integer) and rounding direction; otherwise the nodes will be handled as rational-type nodes. + * + * @throws ApronException throws exception + */ + @Test + public void integerRoundingTest() throws ApronException { + // 4 = 4 * 4/3 + Environment environment = new Environment(new String[] {"x"}, new String[] {}); + Texpr1CstNode four = new Texpr1CstNode(new MpqScalar(4)); + Texpr1CstNode three = new Texpr1CstNode(new MpqScalar(3)); + Texpr1BinNode div = + new Texpr1BinNode( + Texpr1BinNode.OP_DIV, Texpr1Node.RTYPE_INT, Texpr1Node.RDIR_DOWN, four, three); + Texpr1BinNode mul = new Texpr1BinNode(Texpr1BinNode.OP_MUL, four, div); + Texpr1BinNode sub = + new Texpr1BinNode( + Texpr1BinNode.OP_SUB, Texpr1Node.RTYPE_INT, Texpr1Node.RDIR_DOWN, four, mul); + Tcons1 eq = new Tcons1(environment, Tcons1.EQ, sub); + Abstract1 abstract1 = new Abstract1(manager, new Tcons1[] {eq}); + assertThat(abstract1.isBottom(manager)).isFalse(); + + // 1 = 2*(1/2) + Texpr1CstNode one = new Texpr1CstNode(new MpqScalar(1)); + Texpr1CstNode two = new Texpr1CstNode(new MpqScalar(2)); + Texpr1BinNode half = + new Texpr1BinNode( + Texpr1BinNode.OP_DIV, Texpr1Node.RTYPE_INT, Texpr1Node.RDIR_DOWN, one, two); + Texpr1BinNode mul2 = new Texpr1BinNode(Texpr1BinNode.OP_MUL, two, half); + Texpr1BinNode sub2 = + new Texpr1BinNode( + Texpr1BinNode.OP_SUB, Texpr1Node.RTYPE_INT, Texpr1Node.RDIR_DOWN, one, mul2); + Tcons1 eq2 = new Tcons1(environment, Tcons1.EQ, sub2); + Abstract1 abstract2 = new Abstract1(manager, new Tcons1[] {eq2}); + assertThat(abstract2.isBottom(manager)).isTrue(); + + // x = 2*(x/2) and x = 1 + Texpr1VarNode x = new Texpr1VarNode("x"); + Texpr1BinNode xMinusOne = + new Texpr1BinNode(Texpr1BinNode.OP_SUB, Texpr1Node.RTYPE_INT, Texpr1Node.RDIR_DOWN, x, one); + // x=1 + Tcons1 eqXisOne = new Tcons1(environment, Tcons1.EQ, xMinusOne); + // x/2 + Texpr1BinNode xDivTwo = + new Texpr1BinNode(Texpr1BinNode.OP_DIV, Texpr1Node.RTYPE_INT, Texpr1Node.RDIR_DOWN, x, two); + // 2*(x/2) + Texpr1BinNode twoMul = new Texpr1BinNode(Texpr1BinNode.OP_MUL, two, xDivTwo); + // x - 2*(x/2) + Texpr1BinNode xSub = + new Texpr1BinNode( + Texpr1BinNode.OP_SUB, Texpr1Node.RTYPE_INT, Texpr1Node.RDIR_DOWN, x, twoMul); + // x-2*(x/2) = 0 + Tcons1 eq3 = new Tcons1(environment, Tcons1.EQ, xSub); + Abstract1 abstract3 = new Abstract1(manager, new Tcons1[] {eq3, eqXisOne}); + assertThat(abstract3.isBottom(manager)).isFalse(); // isBottom() should be true! + + // a = 10 and b = 5 and a-b = 7*((a-b)/7) + Environment environment1 = new Environment(new String[] {"a", "b"}, new String[] {}); + Texpr1VarNode a = new Texpr1VarNode("a"); + Texpr1VarNode b = new Texpr1VarNode("b"); + Texpr1CstNode ten = new Texpr1CstNode(new MpqScalar(10)); + Texpr1CstNode five = new Texpr1CstNode(new MpqScalar(5)); + Texpr1CstNode seven = new Texpr1CstNode(new MpqScalar(7)); + // a=10 + Texpr1BinNode aMin10 = + new Texpr1BinNode(Texpr1BinNode.OP_SUB, Texpr1Node.RTYPE_INT, Texpr1Node.RDIR_DOWN, a, ten); + Tcons1 aIsTen = new Tcons1(environment1, Tcons1.EQ, aMin10); + // b=5 + Texpr1BinNode bMin5 = + new Texpr1BinNode( + Texpr1BinNode.OP_SUB, Texpr1Node.RTYPE_INT, Texpr1Node.RDIR_DOWN, b, five); + Tcons1 bIsFive = new Tcons1(environment1, Tcons1.EQ, bMin5); + // a-b + Texpr1BinNode aMinb = + new Texpr1BinNode(Texpr1BinNode.OP_SUB, Texpr1Node.RTYPE_INT, Texpr1Node.RDIR_DOWN, a, b); + // (a-b)/7 + Texpr1BinNode div7 = + new Texpr1BinNode( + Texpr1BinNode.OP_DIV, Texpr1Node.RTYPE_INT, Texpr1Node.RDIR_DOWN, aMinb, seven); + // 7*((a-b)/7) + Texpr1BinNode mul7 = + new Texpr1BinNode( + Texpr1BinNode.OP_MUL, Texpr1Node.RTYPE_INT, Texpr1Node.RDIR_DOWN, seven, div7); + // (a-b)-(7*((a-b)/7))) + Texpr1BinNode all = + new Texpr1BinNode( + Texpr1BinNode.OP_SUB, Texpr1Node.RTYPE_INT, Texpr1Node.RDIR_DOWN, aMinb, mul7); + // (a-b)-(7*((a-b)/7))) = 0 + Tcons1 eq1 = new Tcons1(environment1, Tcons1.EQ, all); + Abstract1 abstract11 = new Abstract1(manager, new Tcons1[] {eq1, aIsTen, bIsFive}); + // isBottom() returns true because eq1 is not added + assertThat(abstract11.isBottom(manager)).isFalse(); + } +} diff --git a/src/org/sosy_lab/java_smt/solvers/apron/ApronBooleanFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/apron/ApronBooleanFormulaManager.java new file mode 100644 index 0000000000..9c548b9170 --- /dev/null +++ b/src/org/sosy_lab/java_smt/solvers/apron/ApronBooleanFormulaManager.java @@ -0,0 +1,164 @@ +// This file is part of JavaSMT, +// an API wrapper for a collection of SMT solvers: +// https://github.com/sosy-lab/java-smt +// +// SPDX-FileCopyrightText: 2024 Dirk Beyer +// +// SPDX-License-Identifier: Apache-2.0 + +package org.sosy_lab.java_smt.solvers.apron; + +import apron.Abstract1; +import apron.ApronException; +import apron.Environment; +import apron.Tcons1; +import apron.Texpr1Node; +import java.math.BigInteger; +import java.util.ArrayList; +import java.util.HashMap; +import java.util.List; +import java.util.Map; +import java.util.logging.Level; +import java.util.logging.Logger; +import org.sosy_lab.java_smt.basicimpl.AbstractBooleanFormulaManager; +import org.sosy_lab.java_smt.solvers.apron.types.ApronFormulaType; +import org.sosy_lab.java_smt.solvers.apron.types.ApronNode; +import org.sosy_lab.java_smt.solvers.apron.types.ApronNode.ApronConstraint; +import org.sosy_lab.java_smt.solvers.apron.types.ApronNode.ApronNumeralNode.ApronIntCstNode; + +/** + * Apron only supports and-operations by stacking constraints. Boolean type variables do not exist. + */ +public class ApronBooleanFormulaManager + extends AbstractBooleanFormulaManager { + + private final ApronFormulaCreator apronFormulaCreator; + private final Logger logger = Logger.getLogger("BooleanFormula logger"); + + protected ApronBooleanFormulaManager(ApronFormulaCreator pCreator) { + super(pCreator); + this.apronFormulaCreator = pCreator; + } + + @Override + protected ApronNode makeVariableImpl(String pVar) { + throw new UnsupportedOperationException("Apron supports only numeral variables."); + } + + /** + * True is symbolized by 1=1, false by 1!=1. + * + * @param value boolean value to implement + * @return ApronConstraint of the form 1=1 (true) or 1!=1 (false) + */ + @Override + protected ApronNode makeBooleanImpl(boolean value) { + ApronIntCstNode one = new ApronIntCstNode(BigInteger.ONE); + Map map = new HashMap<>(); + if (value) { + // 1 != 0 + map.put(one, Tcons1.DISEQ); + } else { + // 1 = 0 + map.put(one, Tcons1.EQ); + } + return new ApronConstraint(apronFormulaCreator.getFormulaEnvironment(), map); + } + + @Override + protected ApronNode not(ApronNode pParam1) { + throw new UnsupportedOperationException("Apron does not support not() operations."); + } + + /** + * the and() method is implemented by stacking two constraints. + * + * @param pParam1 ApronConstraint 1 + * @param pParam2 ApronConstraint 2 + * @return new ApronConstraint which combines the two input constraints + */ + @Override + protected ApronNode and(ApronNode pParam1, ApronNode pParam2) { + ApronConstraint cons1 = (ApronConstraint) pParam1; + ApronConstraint cons2 = (ApronConstraint) pParam2; + List constraints = new ArrayList<>(); + constraints.add(cons1); + constraints.add(cons2); + return new ApronConstraint(constraints, apronFormulaCreator.getFormulaEnvironment()); + } + + @Override + protected ApronNode or(ApronNode pParam1, ApronNode pParam2) { + throw new UnsupportedOperationException("Apron does not support or() operations."); + } + + @Override + protected ApronNode xor(ApronNode pParam1, ApronNode pParam2) { + throw new UnsupportedOperationException("Apron does not support xor() operations."); + } + + @Override + protected ApronNode equivalence(ApronNode bits1, ApronNode bits2) { + throw new UnsupportedOperationException("Apron does not support equivalence() operations."); + } + + /** + * For checking whether a BooleanFormula is true, Apron needs an Abstract1 object with the formula + * as input. Then one can check, if the Abstract1 object is bottom (for false). + * + * @param bits ApronConstraint to check + * @return !isBottom() + */ + @Override + protected boolean isTrue(ApronNode bits) { + try { + ApronConstraint constraint = (ApronConstraint) bits; + Map map = constraint.getConstraintNodes(); + Tcons1[] tcons1s = map.keySet().toArray(new Tcons1[map.size()]); + Abstract1 helper = new Abstract1(this.apronFormulaCreator.getManager(), tcons1s); + boolean isBottom = helper.isBottom(this.apronFormulaCreator.getManager()); + if (isBottom) { + return false; + } else { + logger.setLevel(Level.WARNING); + logger.warning( + "Apron can only guarantee for clear results for UNSAT! SAT can " + + "also mean UNKNOWN!"); + return true; + } + } catch (ApronException pException) { + throw new RuntimeException(pException); + } + } + + /** + * For checking whether a BooleanFormula is false, Apron needs an Abstract1 object with the + * formula as input. Then one can check, if the Abstract1 object is bottom (for false). + * + * @param bits ApronConstraint to check + * @return isBottom() + */ + @Override + protected boolean isFalse(ApronNode bits) { + try { + ApronConstraint constraint = (ApronConstraint) bits; + Map map = constraint.getConstraintNodes(); + Tcons1[] tcons1s = map.keySet().toArray(new Tcons1[map.size()]); + Abstract1 helper = new Abstract1(this.apronFormulaCreator.getManager(), tcons1s); + Boolean isBottom = helper.isBottom(this.apronFormulaCreator.getManager()); + if (!isBottom) { + logger.setLevel(Level.WARNING); + logger.warning( + "Apron can only guarantee for clear results for UNSAT! SAT can also mean UNKNOWN!"); + } + return isBottom; + } catch (ApronException pException) { + throw new RuntimeException(pException); + } + } + + @Override + protected ApronNode ifThenElse(ApronNode cond, ApronNode f1, ApronNode f2) { + throw new UnsupportedOperationException("Apron does not support ifThenElse() operations."); + } +} diff --git a/src/org/sosy_lab/java_smt/solvers/apron/ApronEvaluator.java b/src/org/sosy_lab/java_smt/solvers/apron/ApronEvaluator.java new file mode 100644 index 0000000000..bd7d1fe61b --- /dev/null +++ b/src/org/sosy_lab/java_smt/solvers/apron/ApronEvaluator.java @@ -0,0 +1,48 @@ +// This file is part of JavaSMT, +// an API wrapper for a collection of SMT solvers: +// https://github.com/sosy-lab/java-smt +// +// SPDX-FileCopyrightText: 2024 Dirk Beyer +// +// SPDX-License-Identifier: Apache-2.0 + +package org.sosy_lab.java_smt.solvers.apron; + +import org.checkerframework.checker.nullness.qual.Nullable; +import org.sosy_lab.java_smt.api.SolverException; +import org.sosy_lab.java_smt.basicimpl.AbstractEvaluator; +import org.sosy_lab.java_smt.basicimpl.AbstractProver; +import org.sosy_lab.java_smt.basicimpl.FormulaCreator; +import org.sosy_lab.java_smt.solvers.apron.types.ApronFormulaType; +import org.sosy_lab.java_smt.solvers.apron.types.ApronNode; + +public class ApronEvaluator extends AbstractEvaluator { + + private final ApronTheoremProver theoremProver; + private ApronModel apronModel; + + protected ApronEvaluator( + AbstractProver pProver, + FormulaCreator creator) + throws SolverException { + super(pProver, creator); + this.theoremProver = (ApronTheoremProver) pProver; + this.apronModel = (ApronModel) theoremProver.getModel(); + } + + @Override + protected @Nullable ApronNode evalImpl(ApronNode formula) { + try { + this.apronModel = (ApronModel) theoremProver.getModel(); + return apronModel.getValue(formula); + } catch (SolverException e) { + throw new RuntimeException(e); + } + } + + @Override + public void close() { + this.theoremProver.close(); + this.apronModel.close(); + } +} diff --git a/src/org/sosy_lab/java_smt/solvers/apron/ApronFormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/apron/ApronFormulaCreator.java new file mode 100644 index 0000000000..0c3544a090 --- /dev/null +++ b/src/org/sosy_lab/java_smt/solvers/apron/ApronFormulaCreator.java @@ -0,0 +1,267 @@ +// This file is part of JavaSMT, +// an API wrapper for a collection of SMT solvers: +// https://github.com/sosy-lab/java-smt +// +// SPDX-FileCopyrightText: 2024 Dirk Beyer +// +// SPDX-License-Identifier: Apache-2.0 + +package org.sosy_lab.java_smt.solvers.apron; + +import apron.Abstract1; +import apron.ApronException; +import apron.Environment; +import apron.Manager; +import apron.Tcons1; +import apron.Texpr1Node; +import com.google.common.base.Preconditions; +import java.math.BigInteger; +import java.util.HashMap; +import java.util.List; +import java.util.Map; +import org.sosy_lab.common.rationals.Rational; +import org.sosy_lab.java_smt.api.BooleanFormula; +import org.sosy_lab.java_smt.api.Formula; +import org.sosy_lab.java_smt.api.FormulaType.FloatingPointType; +import org.sosy_lab.java_smt.api.visitors.FormulaVisitor; +import org.sosy_lab.java_smt.basicimpl.FormulaCreator; +import org.sosy_lab.java_smt.solvers.apron.types.ApronFormulaType; +import org.sosy_lab.java_smt.solvers.apron.types.ApronFormulaType.ApronBooleanType; +import org.sosy_lab.java_smt.solvers.apron.types.ApronFormulaType.ApronIntegerType; +import org.sosy_lab.java_smt.solvers.apron.types.ApronFormulaType.ApronRationalType; +import org.sosy_lab.java_smt.solvers.apron.types.ApronFormulaType.FormulaType; +import org.sosy_lab.java_smt.solvers.apron.types.ApronNode; +import org.sosy_lab.java_smt.solvers.apron.types.ApronNode.ApronConstraint; +import org.sosy_lab.java_smt.solvers.apron.types.ApronNode.ApronNumeralNode.ApronIntBinaryNode; +import org.sosy_lab.java_smt.solvers.apron.types.ApronNode.ApronNumeralNode.ApronIntCstNode; +import org.sosy_lab.java_smt.solvers.apron.types.ApronNode.ApronNumeralNode.ApronIntUnaryNode; +import org.sosy_lab.java_smt.solvers.apron.types.ApronNode.ApronNumeralNode.ApronIntVarNode; +import org.sosy_lab.java_smt.solvers.apron.types.ApronNode.ApronNumeralNode.ApronRatBinaryNode; +import org.sosy_lab.java_smt.solvers.apron.types.ApronNode.ApronNumeralNode.ApronRatCstNode; +import org.sosy_lab.java_smt.solvers.apron.types.ApronNode.ApronNumeralNode.ApronRatUnaryNode; +import org.sosy_lab.java_smt.solvers.apron.types.ApronNode.ApronNumeralNode.ApronRatVarNode; + +public class ApronFormulaCreator + extends FormulaCreator { + + /** variables is a map that stores all variable-objects with their name as key. */ + private final Map variableNamesToNodes; + + private final Manager manager; + private Environment formulaEnvironment; + + protected ApronFormulaCreator( + Manager pManager, + Environment pO, + ApronBooleanType boolType, + ApronIntegerType pIntegerType, + ApronRationalType pRationalType) { + super(pO, boolType, pIntegerType, pRationalType, null, null); + this.formulaEnvironment = pO; + this.variableNamesToNodes = new HashMap<>(); + this.manager = pManager; + } + + /** + * Method for extracting the value of a formula. + * + * @param exprNode an additional formula where the type can be received from. + * @param value the formula to be converted. + * @return for constants (actual value), variables (String names) and constraints (Boolean value) + */ + @Override + public Object convertValue(ApronNode exprNode, ApronNode value) { + FormulaType valueType = value.getType(); + + // constants + if (valueType == FormulaType.INTEGER && value instanceof ApronIntCstNode) { + return ((ApronIntCstNode) value).getValue(); + } else if (valueType == FormulaType.RATIONAL && value instanceof ApronRatCstNode) { + BigInteger num = ((ApronRatCstNode) value).getNumerator(); + BigInteger den = ((ApronRatCstNode) value).getDenominator(); + Rational div = Rational.of(num, den); + // for integer values + if (den.equals(BigInteger.ONE)) { + return num; + } + return div; + } else if (value instanceof ApronIntVarNode) { + // integer variables + return ((ApronIntVarNode) value).getVarName(); + } else if (value instanceof ApronRatVarNode) { + // rational variables + return ((ApronRatVarNode) value).getVarName(); + } else if (value instanceof ApronConstraint) { + // constraints + try { + ApronConstraint constraint = (ApronConstraint) value; + Map map = constraint.getConstraintNodes(); + Tcons1[] tcons1s = map.keySet().toArray(new Tcons1[map.size()]); + Abstract1 helper = new Abstract1(this.manager, tcons1s); + return !helper.isBottom(this.manager); + } catch (ApronException pException) { + throw new RuntimeException(pException); + } + } + return null; + } + + public Manager getManager() { + return manager; + } + + public Environment getFormulaEnvironment() { + return this.formulaEnvironment; + } + + public void setFormulaEnvironment(Environment pFormulaEnvironment) { + formulaEnvironment = pFormulaEnvironment; + } + + @Override + public ApronFormulaType getBitvectorType(int bitwidth) { + throw new UnsupportedOperationException("Apron does not support bitvector operations."); + } + + @Override + public ApronFormulaType getFloatingPointType(FloatingPointType type) { + throw new UnsupportedOperationException("Apron does not support floating point operations."); + } + + @Override + public ApronFormulaType getArrayType(ApronFormulaType indexType, ApronFormulaType elementType) { + throw new UnsupportedOperationException("Apron does not support array operations."); + } + + /** + * For making a Formula (Type ApronNode) for a variable it is important to also update the + * environment! + * + * @param pApronFormulaType Integer or Rational? + * @param varName name of the variable + * @return object of either ApronIntVarNode (Type Integer) or ApronRatVarNode (Type Rational) + */ + @Override + public ApronNode makeVariable(ApronFormulaType pApronFormulaType, String varName) { + Preconditions.checkArgument( + (pApronFormulaType.getType().equals(FormulaType.INTEGER) + || pApronFormulaType.getType().equals(FormulaType.RATIONAL)), + "Only Integer or rational variables allowed!"); + if (formulaEnvironment.hasVar(varName)) { + return variableNamesToNodes.get(varName); + } + if (pApronFormulaType.getType().equals(FormulaType.INTEGER)) { + ApronIntVarNode varNode = new ApronIntVarNode(varName, this); + variableNamesToNodes.put(varName, varNode); + return varNode; + } else { + ApronRatVarNode varNode = new ApronRatVarNode(varName, this); + variableNamesToNodes.put(varName, varNode); + return varNode; + } + } + + Map getVariables() { + return variableNamesToNodes; + } + + @Override + public org.sosy_lab.java_smt.api.FormulaType getFormulaType(ApronNode formula) { + FormulaType type = formula.getType(); + if (type.equals(FormulaType.BOOLEAN)) { + return org.sosy_lab.java_smt.api.FormulaType.BooleanType; + } else if (type.equals(FormulaType.RATIONAL)) { + return org.sosy_lab.java_smt.api.FormulaType.RationalType; + } else if (type.equals(FormulaType.INTEGER)) { + return org.sosy_lab.java_smt.api.FormulaType.IntegerType; + } + throw new IllegalArgumentException("Type" + type + "not available!"); + } + + @Override + public R visit(FormulaVisitor visitor, Formula formula, ApronNode f) { + throw new UnsupportedOperationException("Visit function is not supported by Apron."); + } + + @Override + public ApronNode callFunctionImpl(Long declaration, List args) { + throw new UnsupportedOperationException("Apron does not support callFunctionImpl()."); + } + + @Override + public Long declareUFImpl( + String pName, ApronFormulaType pReturnType, List pArgTypes) { + return null; + } + + @Override + protected Long getBooleanVarDeclarationImpl(ApronNode pApronFormula) { + return null; + } + + /** + * SuppressWarning of unchecked is used here because the unchecked warning was because of + * unchecked class cast, but as all formulas are instances of ApronNode and ApronNode inherits + * from Formula, the Class Cast is correct here. + * + * @param pType type of the formula + * @param pTerm term to encapsulate + * @param all subclasses of ApronNode, all extend Formula + * @return more specified ApronNode + */ + @Override + @SuppressWarnings("unchecked") + public T encapsulate( + org.sosy_lab.java_smt.api.FormulaType pType, ApronNode pTerm) { + if (pType.isBooleanType()) { + ApronConstraint constraint = (ApronConstraint) pTerm; + return (T) new ApronNode.ApronConstraint(constraint); + } else if (pType.isIntegerType()) { + if (pTerm instanceof ApronIntCstNode) { + ApronIntCstNode node = (ApronIntCstNode) pTerm; + return (T) new ApronNode.ApronNumeralNode.ApronIntCstNode(node); + } else if (pTerm instanceof ApronIntVarNode) { + ApronIntVarNode node = (ApronIntVarNode) pTerm; + return (T) new ApronNode.ApronNumeralNode.ApronIntVarNode(node); + } else if (pTerm instanceof ApronIntUnaryNode) { + ApronIntUnaryNode node = (ApronIntUnaryNode) pTerm; + return (T) new ApronNode.ApronNumeralNode.ApronIntUnaryNode(node); + } else if (pTerm instanceof ApronIntBinaryNode) { + ApronIntBinaryNode node = (ApronIntBinaryNode) pTerm; + return (T) new ApronNode.ApronNumeralNode.ApronIntBinaryNode(node); + } else { + throw new IllegalArgumentException("Term " + pTerm + " not supported in Apron."); + } + } else if (pType.isRationalType()) { + if (pTerm instanceof ApronRatCstNode) { + ApronRatCstNode node = (ApronRatCstNode) pTerm; + return (T) new ApronNode.ApronNumeralNode.ApronRatCstNode(node); + } else if (pTerm instanceof ApronRatVarNode) { + ApronRatVarNode node = (ApronRatVarNode) pTerm; + return (T) new ApronNode.ApronNumeralNode.ApronRatVarNode(node); + } else if (pTerm instanceof ApronRatUnaryNode) { + ApronRatUnaryNode node = (ApronRatUnaryNode) pTerm; + return (T) new ApronNode.ApronNumeralNode.ApronRatUnaryNode(node); + } else if (pTerm instanceof ApronRatBinaryNode) { + ApronRatBinaryNode node = (ApronRatBinaryNode) pTerm; + return (T) new ApronNode.ApronNumeralNode.ApronRatBinaryNode(node); + } else { + throw new IllegalArgumentException("Term " + pTerm + " not supported in Apron."); + } + + } else { + throw new IllegalArgumentException("Type " + pType + " not supported in Apron."); + } + } + + @Override + public ApronNode extractInfo(Formula pT) { + return ApronFormulaManager.getTerm(pT); + } + + @Override + public BooleanFormula encapsulateBoolean(ApronNode pTerm) { + ApronConstraint constraint = (ApronConstraint) pTerm; + return new ApronConstraint(constraint); + } +} diff --git a/src/org/sosy_lab/java_smt/solvers/apron/ApronFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/apron/ApronFormulaManager.java new file mode 100644 index 0000000000..3206b82195 --- /dev/null +++ b/src/org/sosy_lab/java_smt/solvers/apron/ApronFormulaManager.java @@ -0,0 +1,63 @@ +// This file is part of JavaSMT, +// an API wrapper for a collection of SMT solvers: +// https://github.com/sosy-lab/java-smt +// +// SPDX-FileCopyrightText: 2024 Dirk Beyer +// +// SPDX-License-Identifier: Apache-2.0 + +package org.sosy_lab.java_smt.solvers.apron; + +import apron.Environment; +import java.util.Map; +import org.sosy_lab.common.Appender; +import org.sosy_lab.java_smt.api.BooleanFormula; +import org.sosy_lab.java_smt.api.Formula; +import org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager; +import org.sosy_lab.java_smt.solvers.apron.types.ApronFormulaType; +import org.sosy_lab.java_smt.solvers.apron.types.ApronNode; + +public class ApronFormulaManager + extends AbstractFormulaManager { + + protected ApronFormulaManager( + ApronFormulaCreator pFormulaCreator, + ApronUFManager functionManager, + ApronBooleanFormulaManager booleanManager, + ApronIntegerFormulaManager pIntegerFormulaManager, + ApronRationalFormulaManager pRationalFormulaManager) { + super( + pFormulaCreator, + functionManager, + booleanManager, + pIntegerFormulaManager, + pRationalFormulaManager, + null, + null, + null, + null, + null, + null, + null); + } + + public static ApronNode getTerm(Formula pFormula) { + return ((ApronNode) pFormula).getInstance(); + } + + @Override + public BooleanFormula parse(String s) throws IllegalArgumentException { + throw new UnsupportedOperationException("Apron does not support parse()."); + } + + @Override + public Appender dumpFormula(ApronNode t) { + throw new UnsupportedOperationException("Apron does not support dumpFormula()."); + } + + @Override + public T substitute( + T f, Map fromToMapping) { + throw new UnsupportedOperationException("Apron does not support substitute()."); + } +} diff --git a/src/org/sosy_lab/java_smt/solvers/apron/ApronIntegerFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/apron/ApronIntegerFormulaManager.java new file mode 100644 index 0000000000..f60d26af0c --- /dev/null +++ b/src/org/sosy_lab/java_smt/solvers/apron/ApronIntegerFormulaManager.java @@ -0,0 +1,220 @@ +// This file is part of JavaSMT, +// an API wrapper for a collection of SMT solvers: +// https://github.com/sosy-lab/java-smt +// +// SPDX-FileCopyrightText: 2024 Dirk Beyer +// +// SPDX-License-Identifier: Apache-2.0 + +package org.sosy_lab.java_smt.solvers.apron; + +import apron.Tcons1; +import apron.Texpr0Node; +import apron.Texpr1BinNode; +import apron.Texpr1UnNode; +import java.math.BigDecimal; +import java.math.BigInteger; +import java.util.ArrayList; +import java.util.HashMap; +import java.util.List; +import java.util.Map; +import java.util.Set; +import org.sosy_lab.java_smt.api.BooleanFormula; +import org.sosy_lab.java_smt.api.IntegerFormulaManager; +import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula; +import org.sosy_lab.java_smt.solvers.apron.types.ApronFormulaType; +import org.sosy_lab.java_smt.solvers.apron.types.ApronFormulaType.ApronIntegerType; +import org.sosy_lab.java_smt.solvers.apron.types.ApronFormulaType.FormulaType; +import org.sosy_lab.java_smt.solvers.apron.types.ApronNode; +import org.sosy_lab.java_smt.solvers.apron.types.ApronNode.ApronConstraint; +import org.sosy_lab.java_smt.solvers.apron.types.ApronNode.ApronNumeralNode.ApronIntBinaryNode; +import org.sosy_lab.java_smt.solvers.apron.types.ApronNode.ApronNumeralNode.ApronIntCstNode; +import org.sosy_lab.java_smt.solvers.apron.types.ApronNode.ApronNumeralNode.ApronIntUnaryNode; + +public class ApronIntegerFormulaManager + extends ApronNumeralFormulaManager + implements IntegerFormulaManager { + + private final ApronFormulaType integerType = new ApronIntegerType(); + private final ApronFormulaCreator apronFormulaCreator; + + protected ApronIntegerFormulaManager( + ApronFormulaCreator pCreator, NonLinearArithmetic pNonLinearArithmetic) { + super(pCreator, pNonLinearArithmetic); + this.apronFormulaCreator = pCreator; + } + + @Override + protected FormulaType getNumeralType() { + return FormulaType.INTEGER; + } + + @Override + protected ApronNode makeVariableImpl(String i) { + return this.apronFormulaCreator.makeVariable(integerType, i); + } + + @Override + protected ApronNode makeNumberImpl(double pNumber) { + return new ApronIntCstNode(BigDecimal.valueOf(pNumber).toBigInteger()); + } + + @Override + protected ApronNode makeNumberImpl(BigDecimal pNumber) { + return new ApronIntCstNode(pNumber.toBigInteger()); + } + + @Override + protected ApronNode makeNumberImpl(long i) { + return new ApronIntCstNode(BigInteger.valueOf(i)); + } + + @Override + protected ApronNode makeNumberImpl(BigInteger i) { + return new ApronIntCstNode(i); + } + + @Override + protected ApronNode makeNumberImpl(String i) { + return new ApronIntCstNode(new BigInteger(i)); + } + + @Override + public BooleanFormula modularCongruence( + IntegerFormula number1, IntegerFormula number2, BigInteger n) { + return modularCongruence(number1, number2, n.longValue()); + } + + @Override + public BooleanFormula modularCongruence(IntegerFormula number1, IntegerFormula number2, long n) { + // (= x (* n (div x n))); div = x/n; x = number1 - number2 Frage ist, ob num1 mod num2 = n ist + // Test mit 8 und 3 : 8-3 = 2 * (8-3)/2 --> hier entsteht ein fehler + if (n > 0) { + ApronIntCstNode nN = new ApronIntCstNode(BigInteger.valueOf(n)); + ApronIntBinaryNode x = + new ApronIntBinaryNode( + ApronFormulaManager.getTerm(number1), + ApronFormulaManager.getTerm(number2), + Texpr1BinNode.OP_SUB); + ApronIntBinaryNode div = new ApronIntBinaryNode(x, nN, Texpr1BinNode.OP_DIV); + ApronIntBinaryNode mul = new ApronIntBinaryNode(nN, div, Texpr1BinNode.OP_MUL); + ApronIntBinaryNode left = new ApronIntBinaryNode(x, mul, Texpr1BinNode.OP_SUB); + Map map = new HashMap<>(); + map.put(left, Tcons1.EQ); + return new ApronNode.ApronConstraint(apronFormulaCreator.getFormulaEnvironment(), map); + } + ApronIntCstNode zero = new ApronIntCstNode(BigInteger.ZERO); + Map map = new HashMap<>(); + map.put(zero, Tcons1.EQ); // 0=0 for true + return new ApronConstraint(apronFormulaCreator.getFormulaEnvironment(), map); + } + + @Override + public IntegerFormula modulo(IntegerFormula numerator, IntegerFormula denominator) { + ApronNode node1 = (ApronNode) numerator; + ApronNode node2 = (ApronNode) denominator; + Set vars = apronFormulaCreator.getVariables().keySet(); + // Somehow hasVar() only works for level0 of Apron (example in ApronNativeApiTest) + Texpr0Node zeroNode = node2.getNode().toTexpr0Node(apronFormulaCreator.getFormulaEnvironment()); + for (String var : vars) { + if (zeroNode.hasDim(apronFormulaCreator.getFormulaEnvironment().dimOfVar(var))) { + throw new UnsupportedOperationException("Denominator must not contain variables!"); + } + } + return new ApronIntBinaryNode(node1, node2, Texpr1BinNode.OP_MOD); + } + + @Override + protected ApronNode negate(ApronNode pParam1) { + return new ApronIntUnaryNode(pParam1, Texpr1UnNode.OP_NEG); + } + + @Override + protected ApronNode add(ApronNode pParam1, ApronNode pParam2) { + return new ApronIntBinaryNode(pParam1, pParam2, Texpr1BinNode.OP_ADD); + } + + @Override + protected ApronNode sumImpl(List operands) { + if (!operands.isEmpty()) { + ApronNode first = operands.remove(0); + for (ApronNode operand : operands) { + first = new ApronIntBinaryNode(first, operand, Texpr1BinNode.OP_ADD); + } + return first; + } + return makeNumberImpl(0); + } + + @Override + protected ApronNode subtract(ApronNode pParam1, ApronNode pParam2) { + return new ApronIntBinaryNode(pParam1, pParam2, Texpr1BinNode.OP_SUB); + } + + @Override + protected ApronNode divide(ApronNode pParam1, ApronNode pParam2) { + return new ApronIntBinaryNode(pParam1, pParam2, Texpr1BinNode.OP_DIV); + } + + @Override + protected ApronNode multiply(ApronNode pParam1, ApronNode pParam2) { + return new ApronIntBinaryNode(pParam1, pParam2, Texpr1BinNode.OP_MUL); + } + + @Override + protected ApronNode equal(ApronNode pParam1, ApronNode pParam2) { + ApronIntBinaryNode binaryNode = new ApronIntBinaryNode(pParam1, pParam2, Texpr1BinNode.OP_SUB); + Map map = new HashMap<>(); + map.put(binaryNode, Tcons1.EQ); + return new ApronConstraint(apronFormulaCreator.getFormulaEnvironment(), map); + } + + @Override + protected ApronNode distinctImpl(List pNumbers) { + List constraints = new ArrayList<>(); + for (int i = 0; i < pNumbers.size(); i++) { + for (int j = 0; j < i; j++) { + ApronNode apronNode = + new ApronIntBinaryNode(pNumbers.get(i), pNumbers.get(j), Texpr1BinNode.OP_SUB); + Map map = new HashMap<>(); + map.put(apronNode, Tcons1.DISEQ); + ApronConstraint constraint = + new ApronConstraint(apronFormulaCreator.getFormulaEnvironment(), map); + constraints.add(constraint); + } + } + return new ApronConstraint(constraints, apronFormulaCreator.getFormulaEnvironment()); + } + + @Override + protected ApronNode greaterThan(ApronNode pParam1, ApronNode pParam2) { + ApronIntBinaryNode binaryNode = new ApronIntBinaryNode(pParam1, pParam2, Texpr1BinNode.OP_SUB); + Map map = new HashMap<>(); + map.put(binaryNode, Tcons1.SUP); + return new ApronConstraint(apronFormulaCreator.getFormulaEnvironment(), map); + } + + @Override + protected ApronNode greaterOrEquals(ApronNode pParam1, ApronNode pParam2) { + ApronIntBinaryNode binaryNode = new ApronIntBinaryNode(pParam1, pParam2, Texpr1BinNode.OP_SUB); + Map map = new HashMap<>(); + map.put(binaryNode, Tcons1.SUPEQ); + return new ApronConstraint(apronFormulaCreator.getFormulaEnvironment(), map); + } + + @Override + protected ApronNode lessThan(ApronNode pParam1, ApronNode pParam2) { + ApronIntBinaryNode binaryNode = new ApronIntBinaryNode(pParam2, pParam1, Texpr1BinNode.OP_SUB); + Map map = new HashMap<>(); + map.put(binaryNode, Tcons1.SUP); + return new ApronConstraint(apronFormulaCreator.getFormulaEnvironment(), map); + } + + @Override + protected ApronNode lessOrEquals(ApronNode pParam1, ApronNode pParam2) { + ApronIntBinaryNode binaryNode = new ApronIntBinaryNode(pParam2, pParam1, Texpr1BinNode.OP_SUB); + Map map = new HashMap<>(); + map.put(binaryNode, Tcons1.SUPEQ); + return new ApronConstraint(apronFormulaCreator.getFormulaEnvironment(), map); + } +} diff --git a/src/org/sosy_lab/java_smt/solvers/apron/ApronModel.java b/src/org/sosy_lab/java_smt/solvers/apron/ApronModel.java new file mode 100644 index 0000000000..f5d5891ce6 --- /dev/null +++ b/src/org/sosy_lab/java_smt/solvers/apron/ApronModel.java @@ -0,0 +1,300 @@ +// This file is part of JavaSMT, +// an API wrapper for a collection of SMT solvers: +// https://github.com/sosy-lab/java-smt +// +// SPDX-FileCopyrightText: 2024 Dirk Beyer +// +// SPDX-License-Identifier: Apache-2.0 + +package org.sosy_lab.java_smt.solvers.apron; + +import apron.Abstract1; +import apron.ApronException; +import apron.Environment; +import apron.Interval; +import apron.Manager; +import apron.MpqScalar; +import apron.Tcons1; +import apron.Texpr0Node; +import apron.Texpr1BinNode; +import apron.Texpr1Node; +import apron.Texpr1UnNode; +import apron.Texpr1VarNode; +import com.google.common.base.Preconditions; +import com.google.common.base.Splitter; +import com.google.common.collect.ImmutableList; +import com.google.common.collect.ImmutableSet; +import java.math.BigInteger; +import java.util.Collection; +import java.util.HashMap; +import java.util.List; +import java.util.Map; +import org.checkerframework.checker.nullness.qual.Nullable; +import org.sosy_lab.java_smt.api.BooleanFormula; +import org.sosy_lab.java_smt.basicimpl.AbstractModel; +import org.sosy_lab.java_smt.solvers.apron.types.ApronFormulaType; +import org.sosy_lab.java_smt.solvers.apron.types.ApronNode; +import org.sosy_lab.java_smt.solvers.apron.types.ApronNode.ApronConstraint; +import org.sosy_lab.java_smt.solvers.apron.types.ApronNode.ApronNumeralNode.ApronIntBinaryNode; +import org.sosy_lab.java_smt.solvers.apron.types.ApronNode.ApronNumeralNode.ApronIntCstNode; +import org.sosy_lab.java_smt.solvers.apron.types.ApronNode.ApronNumeralNode.ApronIntVarNode; +import org.sosy_lab.java_smt.solvers.apron.types.ApronNode.ApronNumeralNode.ApronRatBinaryNode; +import org.sosy_lab.java_smt.solvers.apron.types.ApronNode.ApronNumeralNode.ApronRatCstNode; +import org.sosy_lab.java_smt.solvers.apron.types.ApronNode.ApronNumeralNode.ApronRatUnaryNode; +import org.sosy_lab.java_smt.solvers.apron.types.ApronNode.ApronNumeralNode.ApronRatVarNode; + +public class ApronModel extends AbstractModel { + + private final ApronFormulaCreator formulaCreator; + private final ApronTheoremProver prover; + private final ImmutableList assertedExpressions; + private final ImmutableList model; + private final ApronBooleanFormulaManager booleanFormulaManager; + + protected ApronModel( + ApronTheoremProver pProver, + ApronFormulaCreator creator, + Collection pAssertedExpressions) { + super(pProver, creator); + this.formulaCreator = creator; + this.prover = pProver; + this.assertedExpressions = ImmutableList.copyOf(pAssertedExpressions); + this.booleanFormulaManager = new ApronBooleanFormulaManager(creator); + this.model = generateModel(); + } + + @Override + public ImmutableList asList() { + Preconditions.checkState(!isClosed()); + return generateModel(); + } + + private ImmutableList generateModel() { + ImmutableSet.Builder builder = ImmutableSet.builder(); + for (ApronConstraint constraint : assertedExpressions) { + for (String var : constraint.getVarNames()) { + builder.add(getAssignment(var)); + } + } + return builder.build().asList(); + } + + private ValueAssignment getAssignment(String pVar) { + try { + // check if the variable is of type integer + if (formulaCreator.getFormulaEnvironment().isInt(pVar)) { + return getIntAssignment(pVar); + } else { + return getRatAssignment(pVar); + } + } catch (ApronException pApronException) { + throw new RuntimeException(pApronException); + } + } + + private ValueAssignment getIntAssignment(String pVar) throws ApronException { + ApronNode keyFormula = formulaCreator.getVariables().get(pVar); + Manager man = this.prover.getAbstract1().getCreationManager(); + // shows the interval for all values the variable can take + Interval interval = this.prover.getAbstract1().getBound(man, pVar); + // gives the lower bound of the interval + BigInteger big; + MpqScalar upperBound = (MpqScalar) interval.sup; + MpqScalar lowerBound = (MpqScalar) interval.inf; + // Test if abstract1-object is Bottom + if (interval.isBottom()) { + throw new RuntimeException("There is no model because the assertion stack is UNSAT."); + } + // is the upper bound +infinity? + if (upperBound.isInfty() == 1) { + // is the lower bound -infinity? + if (lowerBound.isInfty() == -1) { + big = BigInteger.ZERO; + } else { + big = new BigInteger(interval.inf.toString()); + } + } else { + big = new BigInteger(interval.sup.toString()); + } + // valueFormula refers to the lower bound + ApronIntCstNode valueFormula = new ApronIntCstNode(big); + // creates a formula of the form: key - lower bound + ApronIntBinaryNode binaryNode = + new ApronIntBinaryNode(keyFormula, valueFormula, Texpr1BinNode.OP_SUB); + // creates a constraint of the form key - lower bound = 0 (Apron format of key = lower bound) + Map map = new HashMap<>(); + map.put(binaryNode, Tcons1.EQ); + BooleanFormula formula = new ApronConstraint(formulaCreator.getFormulaEnvironment(), map); + return new ValueAssignment( + keyFormula, + valueFormula, + formula, + pVar, + formulaCreator.convertValue(keyFormula, valueFormula), + ImmutableList.of()); + } + + private ValueAssignment getRatAssignment(String pVar) throws ApronException { + ApronNode keyFormula = formulaCreator.getVariables().get(pVar); + Manager man = this.prover.getAbstract1().getCreationManager(); + // shows the interval for all values the variable can take + Interval interval = this.prover.getAbstract1().getBound(man, pVar); + // gives the upper bound of the interval + String strValue; + MpqScalar upperBound = (MpqScalar) interval.sup; + MpqScalar lowerBound = (MpqScalar) interval.inf; + // is the upper bound +infinity? + if (upperBound.isInfty() == 1) { + // is the lower bound -infinity? + if (lowerBound.isInfty() == -1) { + strValue = "0"; + } else { + strValue = lowerBound.toString(); + } + } else { + strValue = upperBound.toString(); + } + // translates the value into nominator and denominator + List numbers = Splitter.on('/').splitToList(strValue); + BigInteger nominator = new BigInteger(numbers.get(0)); + ApronRatCstNode valueFormula; + if (numbers.size() > 1) { + BigInteger denominator = new BigInteger(numbers.get(1)); + valueFormula = new ApronRatCstNode(nominator, denominator); + } else { // if the value is an integer + valueFormula = new ApronRatCstNode(nominator, BigInteger.ONE); + } + // creates a formula of the form: key - lower bound + ApronRatBinaryNode binaryNode = + new ApronRatBinaryNode(keyFormula, valueFormula, Texpr1BinNode.OP_SUB); + // creates a constraint of the form key - lower bound = 0 (Apron format of key = lower bound) + Map map = new HashMap<>(); + map.put(binaryNode, Tcons1.EQ); + BooleanFormula formula = new ApronConstraint(formulaCreator.getFormulaEnvironment(), map); + Object node = formulaCreator.convertValue(keyFormula, valueFormula); + return new ValueAssignment(keyFormula, valueFormula, formula, pVar, node, ImmutableList.of()); + } + + @Override + protected @Nullable ApronNode evalImpl(ApronNode formula) { + Preconditions.checkState(!isClosed()); + return getValue(formula); + } + + /** + * method for extracting the model value for a variable or more complex formula. + * + * @param pNode formula to get a model for + * @return model value + */ + public ApronNode getValue(ApronNode pNode) { + if (pNode instanceof ApronConstraint) { + // evaluation of equations + return booleanFormulaManager.makeBooleanImpl(booleanFormulaManager.isTrue(pNode)); + } else { + Texpr1Node texpr1Node = pNode.getNode(); + Texpr0Node texpr0Node = texpr1Node.toTexpr0Node(formulaCreator.getFormulaEnvironment()); + if (texpr0Node.getDims().length == 0) { + // if a node has noc variables, return node + return pNode; + } else if (pNode instanceof ApronIntVarNode) { + return getIntVarValue((ApronIntVarNode) pNode); + } else if (pNode instanceof ApronRatVarNode) { + return getRatVarValue((ApronRatVarNode) pNode); + } else { + return getComplexValue(pNode); + } + } + } + + private ApronNode getComplexValue(ApronNode pNode) { + Preconditions.checkState( + !((pNode instanceof ApronIntCstNode) + || (pNode instanceof ApronIntVarNode) + || (pNode instanceof ApronRatCstNode) + || (pNode instanceof ApronRatVarNode) + || (pNode instanceof ApronConstraint))); + + Texpr1Node nodeToEvaluate = pNode.getNode(); + String resultName = "result"; + // node for storing the result + Texpr1VarNode resultVar = new Texpr1VarNode(resultName); + for (ValueAssignment assignment : model) { + String modelVar = assignment.getName(); + ApronNode toSub = (ApronNode) assignment.getValueAsFormula(); + Texpr1Node toSubT = toSub.getNode(); + // hasVar() only works for Texpr0Node + Texpr0Node zeroNode = nodeToEvaluate.toTexpr0Node(formulaCreator.getFormulaEnvironment()); + boolean hasVarZero = + zeroNode.hasDim(formulaCreator.getFormulaEnvironment().dimOfVar(modelVar)); + // if the node to evaluate has the variable of the current assignment, substitute the + // variable with the assigned value + if (hasVarZero) { + // substitutes every occurence of the variable with the value stored in model + Texpr1Node param1 = nodeToEvaluate.substitute(modelVar, toSubT); + nodeToEvaluate = param1; + } + } + // if the node to substitute has no variables anymore, build an equation of the form + // resultVar = nodeToEvaluate; This is the passed to a helper Abstract1 object; The result + // of the evaluation is a bound of the interval of possible values for resultVar + if (nodeToEvaluate.getVars().length == 0) { + // nodeToEvaluate - resultVar + Texpr1Node result = new Texpr1BinNode(Texpr1BinNode.OP_SUB, nodeToEvaluate, resultVar); + // nodeToEvaluate - resultVar = 0 --> resultVar = nodeToEvaluate + Environment environment = new Environment(new String[] {}, new String[] {resultName}); + Tcons1 equation = new Tcons1(environment, Tcons1.EQ, result); + Tcons1[] c = new Tcons1[] {equation}; + try { + Abstract1 abstract1 = new Abstract1(prover.getAbstract1().getCreationManager(), c); + // getting the lower bound of the interval which refers to all values the variable can + // take + Object bound = + abstract1.getBound(prover.getAbstract1().getCreationManager(), resultName).sup; + String strValue = bound.toString(); + List numbers = Splitter.on('/').splitToList(strValue); + BigInteger nominator = new BigInteger(numbers.get(0)); + ApronRatCstNode valueFormula; + if (numbers.size() > 1) { // for rational lower bounds + BigInteger denominator = new BigInteger(numbers.get(1)); + valueFormula = new ApronRatCstNode(nominator, denominator); + } else { // if the value is an integer + valueFormula = new ApronRatCstNode(nominator, BigInteger.ONE); + } + return valueFormula; + } catch (ApronException e) { + throw new RuntimeException(e); + } + } else { + // if the nodeToEvaluate has still variables, that can not be substituted, the node is + // returned + if (nodeToEvaluate instanceof Texpr1VarNode) { + return new ApronRatVarNode((Texpr1VarNode) nodeToEvaluate, this.formulaCreator); + } else if (nodeToEvaluate instanceof Texpr1UnNode) { + return new ApronRatUnaryNode((Texpr1UnNode) nodeToEvaluate); + } else { + return new ApronRatBinaryNode((Texpr1BinNode) nodeToEvaluate); + } + } + } + + private ApronNode getIntVarValue(ApronIntVarNode varNode) { + String varName = varNode.getVarName(); + for (ValueAssignment assignment : model) { + if (varName.equals(assignment.getName())) { + return (ApronNode) assignment.getValueAsFormula(); + } + } + return new ApronIntCstNode(BigInteger.ZERO); // Use 0 as default value + } + + private ApronNode getRatVarValue(ApronRatVarNode varNode) { + String varName = varNode.getVarName(); + for (ValueAssignment assignment : model) { + if (varName.equals(assignment.getName())) { + return (ApronNode) assignment.getValueAsFormula(); + } + } + return new ApronIntCstNode(BigInteger.ZERO); // Use 0 as default value + } +} diff --git a/src/org/sosy_lab/java_smt/solvers/apron/ApronNumeralFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/apron/ApronNumeralFormulaManager.java new file mode 100644 index 0000000000..3edaddb9f2 --- /dev/null +++ b/src/org/sosy_lab/java_smt/solvers/apron/ApronNumeralFormulaManager.java @@ -0,0 +1,38 @@ +// This file is part of JavaSMT, +// an API wrapper for a collection of SMT solvers: +// https://github.com/sosy-lab/java-smt +// +// SPDX-FileCopyrightText: 2024 Dirk Beyer +// +// SPDX-License-Identifier: Apache-2.0 + +package org.sosy_lab.java_smt.solvers.apron; + +import apron.Environment; +import org.sosy_lab.java_smt.api.NumeralFormula; +import org.sosy_lab.java_smt.basicimpl.AbstractNumeralFormulaManager; +import org.sosy_lab.java_smt.basicimpl.FormulaCreator; +import org.sosy_lab.java_smt.solvers.apron.types.ApronFormulaType; +import org.sosy_lab.java_smt.solvers.apron.types.ApronFormulaType.FormulaType; +import org.sosy_lab.java_smt.solvers.apron.types.ApronNode; + +@SuppressWarnings("ClassTypeParameterName") +abstract class ApronNumeralFormulaManager< + ParamFormulaType extends NumeralFormula, ResultFormulaType extends NumeralFormula> + extends AbstractNumeralFormulaManager< + ApronNode, ApronFormulaType, Environment, ParamFormulaType, ResultFormulaType, Long> { + + protected ApronNumeralFormulaManager( + FormulaCreator pCreator, + NonLinearArithmetic pNonLinearArithmetic) { + super(pCreator, pNonLinearArithmetic); + } + + @Override + protected boolean isNumeral(ApronNode val) { + FormulaType type = val.getType(); + return !type.equals(FormulaType.BOOLEAN); + } + + protected abstract FormulaType getNumeralType(); +} diff --git a/src/org/sosy_lab/java_smt/solvers/apron/ApronRationalFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/apron/ApronRationalFormulaManager.java new file mode 100644 index 0000000000..e1e85ee278 --- /dev/null +++ b/src/org/sosy_lab/java_smt/solvers/apron/ApronRationalFormulaManager.java @@ -0,0 +1,221 @@ +// This file is part of JavaSMT, +// an API wrapper for a collection of SMT solvers: +// https://github.com/sosy-lab/java-smt +// +// SPDX-FileCopyrightText: 2024 Dirk Beyer +// +// SPDX-License-Identifier: Apache-2.0 + +package org.sosy_lab.java_smt.solvers.apron; + +import apron.Tcons1; +import apron.Texpr1BinNode; +import apron.Texpr1UnNode; +import com.google.common.base.Preconditions; +import com.google.common.base.Splitter; +import java.math.BigDecimal; +import java.math.BigInteger; +import java.util.ArrayList; +import java.util.HashMap; +import java.util.List; +import java.util.Map; +import org.sosy_lab.common.rationals.Rational; +import org.sosy_lab.java_smt.api.NumeralFormula; +import org.sosy_lab.java_smt.api.NumeralFormula.RationalFormula; +import org.sosy_lab.java_smt.api.RationalFormulaManager; +import org.sosy_lab.java_smt.solvers.apron.types.ApronFormulaType; +import org.sosy_lab.java_smt.solvers.apron.types.ApronFormulaType.ApronRationalType; +import org.sosy_lab.java_smt.solvers.apron.types.ApronFormulaType.FormulaType; +import org.sosy_lab.java_smt.solvers.apron.types.ApronNode; +import org.sosy_lab.java_smt.solvers.apron.types.ApronNode.ApronConstraint; +import org.sosy_lab.java_smt.solvers.apron.types.ApronNode.ApronNumeralNode.ApronRatBinaryNode; +import org.sosy_lab.java_smt.solvers.apron.types.ApronNode.ApronNumeralNode.ApronRatCstNode; +import org.sosy_lab.java_smt.solvers.apron.types.ApronNode.ApronNumeralNode.ApronRatUnaryNode; +import org.sosy_lab.java_smt.solvers.apron.types.ApronNode.ApronNumeralNode.ApronRatVarNode; + +public class ApronRationalFormulaManager + extends ApronNumeralFormulaManager + implements RationalFormulaManager { + + private final ApronFormulaCreator apronFormulaCreator; + private final ApronFormulaType rationalType = new ApronRationalType(); + + protected ApronRationalFormulaManager( + ApronFormulaCreator pFormulaCreator, NonLinearArithmetic pNonLinearArithmetic) { + super(pFormulaCreator, pNonLinearArithmetic); + this.apronFormulaCreator = pFormulaCreator; + } + + @Override + protected FormulaType getNumeralType() { + return FormulaType.RATIONAL; + } + + @Override + protected ApronNode makeVariableImpl(String i) { + return apronFormulaCreator.makeVariable(rationalType, i); + } + + @Override + protected ApronNode makeNumberImpl(double pNumber) { + BigDecimal dec = BigDecimal.valueOf(pNumber); + Rational rat = Rational.ofBigDecimal(dec); + return new ApronRatCstNode(rat.getNum(), rat.getDen()); + } + + @Override + protected ApronNode makeNumberImpl(BigDecimal pNumber) { + Rational rat = Rational.ofBigDecimal(pNumber); + return new ApronRatCstNode(rat.getNum(), rat.getDen()); + } + + @Override + protected ApronNode makeNumberImpl(long i) { + return new ApronRatCstNode(BigInteger.valueOf(i), BigInteger.ONE); + } + + @Override + protected ApronNode makeNumberImpl(BigInteger i) { + return new ApronRatCstNode(i, BigInteger.ONE); + } + + @Override + protected ApronNode makeNumberImpl(String i) { + Preconditions.checkArgument( + !(i.contains(".") || i.contains(",")), "Rational number has to be written like 2/5."); + List numbers = Splitter.on('/').splitToList(i); + BigInteger num = new BigInteger(numbers.get(0)); + if (numbers.size() > 1) { + BigInteger den = new BigInteger(numbers.get(1)); + return new ApronRatCstNode(num, den); + } + return new ApronRatCstNode(num, BigInteger.ONE); + } + + @Override + protected ApronNode negate(ApronNode pParam1) { + return new ApronRatUnaryNode(pParam1, Texpr1UnNode.OP_NEG); + } + + @Override + protected ApronNode add(ApronNode pParam1, ApronNode pParam2) { + return new ApronRatBinaryNode(pParam1, pParam2, Texpr1BinNode.OP_ADD); + } + + @Override + protected ApronNode sumImpl(List operands) { + if (!operands.isEmpty()) { + ApronNode first = operands.remove(0); + for (ApronNode operand : operands) { + first = new ApronRatBinaryNode(first, operand, Texpr1BinNode.OP_ADD); + } + return first; + } + return makeNumberImpl(0); + } + + @Override + protected ApronNode subtract(ApronNode pParam1, ApronNode pParam2) { + return new ApronRatBinaryNode(pParam1, pParam2, Texpr1BinNode.OP_SUB); + } + + @Override + protected ApronNode divide(ApronNode pParam1, ApronNode pParam2) { + return new ApronRatBinaryNode(pParam1, pParam2, Texpr1BinNode.OP_DIV); + } + + @Override + protected ApronNode multiply(ApronNode pParam1, ApronNode pParam2) { + return new ApronRatBinaryNode(pParam1, pParam2, Texpr1BinNode.OP_MUL); + } + + @Override + protected ApronNode equal(ApronNode pParam1, ApronNode pParam2) { + ApronRatBinaryNode binaryNode = new ApronRatBinaryNode(pParam1, pParam2, Texpr1BinNode.OP_SUB); + Map map = new HashMap<>(); + map.put(binaryNode, Tcons1.EQ); + ApronConstraint constraint = + new ApronConstraint(apronFormulaCreator.getFormulaEnvironment(), map); + return constraint; + } + + @Override + protected ApronNode distinctImpl(List pNumbers) { + List constraints = new ArrayList<>(); + for (int i = 0; i < pNumbers.size(); i++) { + for (int j = 0; j < i; j++) { + ApronNode apronNode = + new ApronRatBinaryNode(pNumbers.get(i), pNumbers.get(j), Texpr1BinNode.OP_SUB); + Map map = new HashMap<>(); + map.put(apronNode, Tcons1.DISEQ); + ApronConstraint constraint = + new ApronConstraint(apronFormulaCreator.getFormulaEnvironment(), map); + constraints.add(constraint); + } + } + return new ApronConstraint(constraints, apronFormulaCreator.getFormulaEnvironment()); + } + + @Override + protected ApronNode greaterThan(ApronNode pParam1, ApronNode pParam2) { + ApronRatBinaryNode binaryNode = new ApronRatBinaryNode(pParam1, pParam2, Texpr1BinNode.OP_SUB); + Map map = new HashMap<>(); + map.put(binaryNode, Tcons1.SUP); + return new ApronConstraint(apronFormulaCreator.getFormulaEnvironment(), map); + } + + @Override + protected ApronNode greaterOrEquals(ApronNode pParam1, ApronNode pParam2) { + ApronRatBinaryNode binaryNode = new ApronRatBinaryNode(pParam1, pParam2, Texpr1BinNode.OP_SUB); + Map map = new HashMap<>(); + map.put(binaryNode, Tcons1.SUPEQ); + return new ApronConstraint(apronFormulaCreator.getFormulaEnvironment(), map); + } + + @Override + protected ApronNode lessThan(ApronNode pParam1, ApronNode pParam2) { + ApronRatBinaryNode binaryNode = new ApronRatBinaryNode(pParam2, pParam1, Texpr1BinNode.OP_SUB); + Map map = new HashMap<>(); + map.put(binaryNode, Tcons1.SUP); + return new ApronConstraint(apronFormulaCreator.getFormulaEnvironment(), map); + } + + @Override + protected ApronNode lessOrEquals(ApronNode pParam1, ApronNode pParam2) { + ApronRatBinaryNode binaryNode = new ApronRatBinaryNode(pParam2, pParam1, Texpr1BinNode.OP_SUB); + Map map = new HashMap<>(); + map.put(binaryNode, Tcons1.SUPEQ); + return new ApronConstraint(apronFormulaCreator.getFormulaEnvironment(), map); + } + + @Override + protected ApronNode floor(ApronNode pTerm) { + return toInteger(pTerm); + } + + /** + * uses especially for this case designed constructors of all Integer Type ApronNode. + * + * @param pNumeralNode rational Node + * @return integer Node + */ + private ApronNode toInteger(ApronNode pNumeralNode) { + FormulaType pType = pNumeralNode.getType(); + if (pType.equals(FormulaType.RATIONAL)) { + if (pNumeralNode instanceof ApronRatCstNode) { + ApronRatCstNode node = (ApronRatCstNode) pNumeralNode; + return new ApronNode.ApronNumeralNode.ApronIntCstNode(node); + } else if (pNumeralNode instanceof ApronRatVarNode) { + ApronRatVarNode node = (ApronRatVarNode) pNumeralNode; + return new ApronNode.ApronNumeralNode.ApronIntVarNode(node); + } else if (pNumeralNode instanceof ApronRatUnaryNode) { + ApronRatUnaryNode node = (ApronRatUnaryNode) pNumeralNode; + return new ApronNode.ApronNumeralNode.ApronRatUnaryNode(node); + } else if (pNumeralNode instanceof ApronRatBinaryNode) { + ApronRatBinaryNode node = (ApronRatBinaryNode) pNumeralNode; + return new ApronNode.ApronNumeralNode.ApronRatBinaryNode(node); + } + } + throw new IllegalArgumentException("Parameter must be rational ApronNode."); + } +} diff --git a/src/org/sosy_lab/java_smt/solvers/apron/ApronSolverContext.java b/src/org/sosy_lab/java_smt/solvers/apron/ApronSolverContext.java new file mode 100644 index 0000000000..cc59feea3a --- /dev/null +++ b/src/org/sosy_lab/java_smt/solvers/apron/ApronSolverContext.java @@ -0,0 +1,136 @@ +// This file is part of JavaSMT, +// an API wrapper for a collection of SMT solvers: +// https://github.com/sosy-lab/java-smt +// +// SPDX-FileCopyrightText: 2024 Dirk Beyer +// +// SPDX-License-Identifier: Apache-2.0 + +package org.sosy_lab.java_smt.solvers.apron; + +import apron.ApronException; +import apron.Environment; +import apron.Manager; +import apron.Polka; +import java.util.Set; +import java.util.logging.Level; +import org.sosy_lab.common.ShutdownNotifier; +import org.sosy_lab.common.log.LogManager; +import org.sosy_lab.java_smt.SolverContextFactory.Solvers; +import org.sosy_lab.java_smt.api.InterpolatingProverEnvironment; +import org.sosy_lab.java_smt.api.OptimizationProverEnvironment; +import org.sosy_lab.java_smt.api.ProverEnvironment; +import org.sosy_lab.java_smt.basicimpl.AbstractNumeralFormulaManager.NonLinearArithmetic; +import org.sosy_lab.java_smt.basicimpl.AbstractSolverContext; +import org.sosy_lab.java_smt.solvers.apron.types.ApronFormulaType.ApronBooleanType; +import org.sosy_lab.java_smt.solvers.apron.types.ApronFormulaType.ApronIntegerType; +import org.sosy_lab.java_smt.solvers.apron.types.ApronFormulaType.ApronRationalType; + +public class ApronSolverContext extends AbstractSolverContext { + + private final ApronFormulaCreator formulaCreator; + private final Manager manager; + private final LogManager logger; + private final ShutdownNotifier shutdownNotifier; + private boolean closed = false; + + protected ApronSolverContext( + ApronFormulaManager fmgr, + Manager pManager, + ApronFormulaCreator pFormulaCreator, + ShutdownNotifier pShutdownNotifier, + LogManager pLogger) { + super(fmgr); + this.manager = pManager; + this.formulaCreator = pFormulaCreator; + this.logger = pLogger; + this.shutdownNotifier = pShutdownNotifier; + } + + public static synchronized ApronSolverContext create( + NonLinearArithmetic pNonLinearArithmetic, + ShutdownNotifier pShutdownNotifier, + LogManager pLogger) { + Environment env = new Environment(); + Manager manager = new Polka(true); + ApronBooleanType booleanType = new ApronBooleanType(); + ApronIntegerType integerType = new ApronIntegerType(); + ApronRationalType rationalType = new ApronRationalType(); + ApronFormulaCreator formulaCreator = + new ApronFormulaCreator(manager, env, booleanType, integerType, rationalType); + ApronUFManager ufManager = new ApronUFManager(formulaCreator); + ApronBooleanFormulaManager booleanFormulaManager = + new ApronBooleanFormulaManager(formulaCreator); + ApronIntegerFormulaManager integerFormulaManager = + new ApronIntegerFormulaManager(formulaCreator, pNonLinearArithmetic); + ApronRationalFormulaManager rationalFormulaManager = + new ApronRationalFormulaManager(formulaCreator, pNonLinearArithmetic); + ApronFormulaManager fmgr = + new ApronFormulaManager( + formulaCreator, + ufManager, + booleanFormulaManager, + integerFormulaManager, + rationalFormulaManager); + return new ApronSolverContext(fmgr, manager, formulaCreator, pShutdownNotifier, pLogger); + } + + public Manager getManager() { + return this.manager; + } + + public ApronFormulaCreator getFormulaCreator() { + return this.formulaCreator; + } + + @Override + public String getVersion() { + return this.manager.getVersion(); + } + + @Override + public Solvers getSolverName() { + return Solvers.APRON; + } + + @Override + public void close() { + if (!closed) { + closed = true; + logger.log(Level.FINER, "Freeing Apron Environment"); + } + } + + @Override + protected ProverEnvironment newProverEnvironment0(Set options) { + return newApronProverEnvironment(options); + } + + private ProverEnvironment newApronProverEnvironment(Set pProverOptions) { + try { + ApronBooleanFormulaManager booleanFormulaManager = + new ApronBooleanFormulaManager(this.formulaCreator); + return new ApronTheoremProver( + pProverOptions, booleanFormulaManager, this.shutdownNotifier, this); + } catch (ApronException pApronException) { + throw new RuntimeException(pApronException); + } + } + + @Override + protected InterpolatingProverEnvironment newProverEnvironmentWithInterpolation0( + Set pSet) { + throw new UnsupportedOperationException(); + } + + @Override + protected OptimizationProverEnvironment newOptimizationProverEnvironment0( + Set pSet) { + throw new UnsupportedOperationException("Optimization prover not supported by Apron."); + } + + @Override + protected boolean supportsAssumptionSolving() { + return true; + } +} diff --git a/src/org/sosy_lab/java_smt/solvers/apron/ApronTheoremProver.java b/src/org/sosy_lab/java_smt/solvers/apron/ApronTheoremProver.java new file mode 100644 index 0000000000..e6457c780f --- /dev/null +++ b/src/org/sosy_lab/java_smt/solvers/apron/ApronTheoremProver.java @@ -0,0 +1,195 @@ +// This file is part of JavaSMT, +// an API wrapper for a collection of SMT solvers: +// https://github.com/sosy-lab/java-smt +// +// SPDX-FileCopyrightText: 2024 Dirk Beyer +// +// SPDX-License-Identifier: Apache-2.0 + +package org.sosy_lab.java_smt.solvers.apron; + +import apron.Abstract1; +import apron.ApronException; +import apron.Tcons1; +import apron.Texpr1Node; +import com.google.common.base.Preconditions; +import com.google.common.collect.ImmutableList; +import java.util.ArrayList; +import java.util.Collection; +import java.util.List; +import java.util.Map; +import java.util.Optional; +import java.util.Set; +import java.util.logging.Level; +import java.util.logging.Logger; +import org.checkerframework.checker.nullness.qual.Nullable; +import org.sosy_lab.common.ShutdownNotifier; +import org.sosy_lab.java_smt.api.BooleanFormula; +import org.sosy_lab.java_smt.api.BooleanFormulaManager; +import org.sosy_lab.java_smt.api.Evaluator; +import org.sosy_lab.java_smt.api.Model; +import org.sosy_lab.java_smt.api.Model.ValueAssignment; +import org.sosy_lab.java_smt.api.ProverEnvironment; +import org.sosy_lab.java_smt.api.SolverContext.ProverOptions; +import org.sosy_lab.java_smt.api.SolverException; +import org.sosy_lab.java_smt.basicimpl.AbstractProverWithAllSat; +import org.sosy_lab.java_smt.solvers.apron.types.ApronNode.ApronConstraint; + +public class ApronTheoremProver extends AbstractProverWithAllSat + implements ProverEnvironment { + + private final ApronSolverContext solverContext; + private final Logger logger = Logger.getLogger("TheoremProver logger"); + private Abstract1 abstract1; + + protected ApronTheoremProver( + Set pSet, + BooleanFormulaManager pBmgr, + ShutdownNotifier pShutdownNotifier, + ApronSolverContext pApronSolverContext) + throws ApronException { + super(pSet, pBmgr, pShutdownNotifier); + this.solverContext = pApronSolverContext; + this.abstract1 = + new Abstract1( + pApronSolverContext.getManager(), + pApronSolverContext.getFormulaCreator().getFormulaEnvironment()); + } + + public ApronSolverContext getSolverContext() { + return solverContext; + } + + @Override + public ImmutableList getModelAssignments() throws SolverException { + Preconditions.checkState(!closed); + return super.getModelAssignments(); + } + + public boolean getClosed() { + return closed; + } + + @Override + protected void popImpl() { + // Do nothing + } + + @Override + protected @Nullable Void addConstraintImpl(BooleanFormula constraint) + throws InterruptedException { + ApronConstraint node = (ApronConstraint) ApronFormulaManager.getTerm(constraint); + try { + for (Map.Entry cons : node.getConstraintNodes().entrySet()) { + Tcons1[] consOld = abstract1.toTcons(solverContext.getManager()); + Tcons1[] newCons = new Tcons1[consOld.length + 1]; + int i = 0; + for (Tcons1 c : consOld) { + c.extendEnvironment(solverContext.getFormulaCreator().getFormulaEnvironment()); + newCons[i] = c; + i++; + } + newCons[consOld.length] = cons.getKey(); + this.abstract1.changeEnvironment( + solverContext.getManager(), + solverContext.getFormulaCreator().getFormulaEnvironment(), + false); + this.abstract1 = new Abstract1(solverContext.getManager(), newCons); + } + } catch (ApronException e) { + throw new RuntimeException(e); + } + return null; + } + + @Override + protected void pushImpl() throws InterruptedException { + // Do nothing + } + + @Override + public boolean isUnsat() throws SolverException, InterruptedException { + Preconditions.checkState(!closed); + try { + if (abstract1.isBottom(solverContext.getManager())) { + return true; + } else { + logger.setLevel(Level.WARNING); + logger.warning( + "Apron can only guarantee for clear results for UNSAT! SAT can " + + "also mean UNKNOWN!"); + return false; + } + } catch (ApronException pApronException) { + throw new RuntimeException(pApronException); + } + } + + @Override + public Model getModel() throws SolverException { + Preconditions.checkState(!closed); + ImmutableList.Builder constraints = ImmutableList.builder(); + for (var f : getAssertedFormulas()) { + constraints.add((ApronConstraint) ApronFormulaManager.getTerm(f)); + } + return new ApronModel(this, solverContext.getFormulaCreator(), constraints.build()); + } + + @Override + public List getUnsatCore() { + throw new UnsupportedOperationException("Unsatcore not supported."); + } + + @Override + public Optional> unsatCoreOverAssumptions( + Collection assumptions) throws SolverException, InterruptedException { + throw new NullPointerException(); + } + + /** + * with the help of the join() method form the Apron-library one can build a new abstract1 object + * with additional constraints. + * + * @param assumptions A list of literals. + * @return if the prover is satisfiable with some additional assumptions + * @throws SolverException throws exception + * @throws InterruptedException throws exception + */ + @Override + public boolean isUnsatWithAssumptions(Collection assumptions) + throws SolverException, InterruptedException { + Preconditions.checkState(!closed); + List constraints = new ArrayList<>(); + for (BooleanFormula assumption : assumptions) { + ApronConstraint cons = (ApronConstraint) ApronFormulaManager.getTerm(assumption); + for (Map.Entry entry : cons.getConstraintNodes().entrySet()) { + constraints.add(entry.getKey()); + } + } + Tcons1[] tcons1s = constraints.toArray(new Tcons1[constraints.size()]); + try { + Abstract1 absNew = new Abstract1(solverContext.getManager(), tcons1s); + Abstract1 result = this.abstract1.joinCopy(solverContext.getManager(), absNew); + return result.isBottom(solverContext.getManager()); + } catch (ApronException e) { + throw new RuntimeException(e.toString()); + } + } + + public Abstract1 getAbstract1() { + return abstract1; + } + + @Override + protected Evaluator getEvaluatorWithoutChecks() throws SolverException { + throw new UnsupportedOperationException("Apron does not support Evaluator without checks."); + } + + @Override + public void close() { + if (!closed) { + closed = true; + } + super.close(); + } +} diff --git a/src/org/sosy_lab/java_smt/solvers/apron/ApronUFManager.java b/src/org/sosy_lab/java_smt/solvers/apron/ApronUFManager.java new file mode 100644 index 0000000000..300ab6b58a --- /dev/null +++ b/src/org/sosy_lab/java_smt/solvers/apron/ApronUFManager.java @@ -0,0 +1,21 @@ +// This file is part of JavaSMT, +// an API wrapper for a collection of SMT solvers: +// https://github.com/sosy-lab/java-smt +// +// SPDX-FileCopyrightText: 2024 Dirk Beyer +// +// SPDX-License-Identifier: Apache-2.0 + +package org.sosy_lab.java_smt.solvers.apron; + +import apron.Environment; +import org.sosy_lab.java_smt.basicimpl.AbstractUFManager; +import org.sosy_lab.java_smt.solvers.apron.types.ApronFormulaType; +import org.sosy_lab.java_smt.solvers.apron.types.ApronNode; + +public class ApronUFManager + extends AbstractUFManager { + protected ApronUFManager(ApronFormulaCreator pCreator) { + super(pCreator); + } +} diff --git a/src/org/sosy_lab/java_smt/solvers/apron/package-info.java b/src/org/sosy_lab/java_smt/solvers/apron/package-info.java new file mode 100644 index 0000000000..ab0c0fbe7f --- /dev/null +++ b/src/org/sosy_lab/java_smt/solvers/apron/package-info.java @@ -0,0 +1,14 @@ +// This file is part of JavaSMT, +// an API wrapper for a collection of SMT solvers: +// https://github.com/sosy-lab/java-smt +// +// SPDX-FileCopyrightText: 2024 Dirk Beyer +// +// SPDX-License-Identifier: Apache-2.0 + +/** Interface the Apron Numerical Abstract Domain Library. */ +@com.google.errorprone.annotations.CheckReturnValue +@javax.annotation.ParametersAreNonnullByDefault +@org.sosy_lab.common.annotations.FieldsAreNonnullByDefault +@org.sosy_lab.common.annotations.ReturnValuesAreNonnullByDefault +package org.sosy_lab.java_smt.solvers.apron; diff --git a/src/org/sosy_lab/java_smt/solvers/apron/types/ApronFormulaType.java b/src/org/sosy_lab/java_smt/solvers/apron/types/ApronFormulaType.java new file mode 100644 index 0000000000..bde0419c0b --- /dev/null +++ b/src/org/sosy_lab/java_smt/solvers/apron/types/ApronFormulaType.java @@ -0,0 +1,54 @@ +// This file is part of JavaSMT, +// an API wrapper for a collection of SMT solvers: +// https://github.com/sosy-lab/java-smt +// +// SPDX-FileCopyrightText: 2024 Dirk Beyer +// +// SPDX-License-Identifier: Apache-2.0 + +package org.sosy_lab.java_smt.solvers.apron.types; + +/** + * This is a helper-class for defining the integer, rational and boolean type for the Generics of + * ApronFormulaCreator. + */ +public interface ApronFormulaType { + + FormulaType getType(); + + enum FormulaType { + BOOLEAN, + INTEGER, + RATIONAL + } + + class ApronIntegerType implements ApronFormulaType { + + public ApronIntegerType() {} + + @Override + public FormulaType getType() { + return FormulaType.INTEGER; + } + } + + class ApronRationalType implements ApronFormulaType { + + public ApronRationalType() {} + + @Override + public FormulaType getType() { + return FormulaType.RATIONAL; + } + } + + class ApronBooleanType implements ApronFormulaType { + + public ApronBooleanType() {} + + @Override + public FormulaType getType() { + return FormulaType.BOOLEAN; + } + } +} diff --git a/src/org/sosy_lab/java_smt/solvers/apron/types/ApronNode.java b/src/org/sosy_lab/java_smt/solvers/apron/types/ApronNode.java new file mode 100644 index 0000000000..7ed12a1215 --- /dev/null +++ b/src/org/sosy_lab/java_smt/solvers/apron/types/ApronNode.java @@ -0,0 +1,882 @@ +// This file is part of JavaSMT, +// an API wrapper for a collection of SMT solvers: +// https://github.com/sosy-lab/java-smt +// +// SPDX-FileCopyrightText: 2024 Dirk Beyer +// +// SPDX-License-Identifier: Apache-2.0 + +package org.sosy_lab.java_smt.solvers.apron.types; + +import apron.Coeff; +import apron.Environment; +import apron.MpqScalar; +import apron.Scalar; +import apron.StringVar; +import apron.Tcons1; +import apron.Texpr1BinNode; +import apron.Texpr1CstNode; +import apron.Texpr1Node; +import apron.Texpr1UnNode; +import apron.Texpr1VarNode; +import apron.Var; +import com.google.common.base.Preconditions; +import com.google.common.base.Splitter; +import com.google.errorprone.annotations.Immutable; +import java.math.BigInteger; +import java.util.ArrayList; +import java.util.Arrays; +import java.util.HashMap; +import java.util.HashSet; +import java.util.List; +import java.util.Map; +import java.util.Set; +import org.sosy_lab.common.rationals.Rational; +import org.sosy_lab.java_smt.api.BooleanFormula; +import org.sosy_lab.java_smt.api.Formula; +import org.sosy_lab.java_smt.api.NumeralFormula; +import org.sosy_lab.java_smt.solvers.apron.ApronFormulaCreator; +import org.sosy_lab.java_smt.solvers.apron.types.ApronFormulaType.FormulaType; + +/** + * This is a wrapper for formulas from the Apron-library. All numeral formulas refer to + * Apron-library instances of Texpr1Node; All BooleanFormulas refer to Tcons1; The wrapper is needed + * to implement methods that are needed for the JavaSMT-binding but are not provided by the + * Apron-library. SupressWarnig has to be used, because the internal Texpr1Node form the Apron + * library is not immutble. But all instances are final. + */ +@SuppressWarnings("Immutable") +public interface ApronNode extends Formula { + + FormulaType getType(); + + Texpr1Node getNode(); + + /** + * this array is needed for getting all variable names; it is not possible to directly extract the + * name of a variable used in an Texpr1Node; that is the reason why the names are tracked + * additionally. + * + * @return String-array with all variables that are used in the created formulas + */ + Set getVarNames(); + + ApronNode getInstance(); + + @Immutable + interface ApronNumeralNode extends ApronNode, NumeralFormula { + /** This class wraps all rational constants, defined by numerator and denominator. */ + @Immutable + class ApronRatCstNode implements RationalFormula, ApronNumeralNode { + + private final FormulaType type = FormulaType.RATIONAL; + private final Texpr1CstNode cstNode; + private final BigInteger numerator; + private final BigInteger denominator; + + private final Rational rational; + + public ApronRatCstNode(BigInteger pNumerator, BigInteger pDenominator) { + this.cstNode = new Texpr1CstNode(new MpqScalar(pNumerator, pDenominator)); + this.numerator = pNumerator; + this.denominator = pDenominator; + this.rational = Rational.of(numerator, denominator); + } + + public ApronRatCstNode(ApronRatCstNode pNode) { + this.cstNode = pNode.getNode(); + this.numerator = pNode.getNumerator(); + this.denominator = pNode.getDenominator(); + this.rational = Rational.of(numerator, denominator); + } + + public ApronRatCstNode(Texpr1CstNode pNode) { + this.cstNode = pNode; + Coeff coeff = pNode.getConstant(); + Scalar scalar = coeff.inf(); + String string = scalar.toString(); + final List strings = Splitter.on('/').splitToList(string); + if (strings.size() == 1) { + this.numerator = BigInteger.valueOf(Long.parseLong(strings.get(0))); + this.denominator = BigInteger.ONE; + } else { + this.numerator = BigInteger.valueOf(Long.parseLong(strings.get(0))); + this.denominator = BigInteger.valueOf(Long.parseLong(strings.get(0))); + } + this.rational = Rational.of(numerator, denominator); + } + + public Rational getRational() { + return rational; + } + + @Override + public FormulaType getType() { + return this.type; + } + + @Override + public Texpr1CstNode getNode() { + return cstNode; + } + + @Override + public Set getVarNames() { + return new HashSet<>(); + } + + public BigInteger getDenominator() { + return denominator; + } + + public BigInteger getNumerator() { + return numerator; + } + + @Override + public ApronNode getInstance() { + return this; + } + + @Override + public String toString() { + return cstNode.toString(); + } + + @Override + public boolean equals(Object other) { + if (other == this) { + return true; + } + if (!(other instanceof ApronRatCstNode)) { + return false; + } + return this == ((ApronRatCstNode) other).getInstance(); + } + + @Override + public int hashCode() { + return this.cstNode.hashCode(); + } + } + + /** This class wraps variables for rational values. */ + class ApronRatVarNode implements RationalFormula, ApronNumeralNode { + + private final FormulaType type = FormulaType.RATIONAL; + private final Texpr1VarNode varNode; + private final String varName; + + private final ApronFormulaCreator formulaCreator; + + public ApronRatVarNode(String pVarName, ApronFormulaCreator pFormulaCreator) { + this.varNode = new Texpr1VarNode(pVarName); + this.formulaCreator = pFormulaCreator; + this.varName = pVarName; + addVarToEnv(); + } + + public ApronRatVarNode(ApronRatVarNode pNode) { + this.varNode = pNode.getNode(); + this.varName = pNode.getVarName(); + this.formulaCreator = pNode.getFormulaCreator(); + } + + public ApronRatVarNode(Texpr1VarNode pNode, ApronFormulaCreator pFormulaCreator) { + Preconditions.checkState(pFormulaCreator.getFormulaEnvironment().hasVar(pNode.toString())); + this.varNode = pNode; + this.formulaCreator = pFormulaCreator; + this.varName = pNode.toString(); + } + + public String getVarName() { + return varName; + } + + public ApronFormulaCreator getFormulaCreator() { + return formulaCreator; + } + + @Override + public String toString() { + return varNode.toString(); + } + + @Override + public boolean equals(Object other) { + + if (other == this) { + return true; + } + if (!(other instanceof ApronRatVarNode)) { + return false; + } + return this == ((ApronRatVarNode) other).getInstance(); + } + + @Override + public int hashCode() { + return this.varNode.hashCode(); + } + + @Override + public FormulaType getType() { + return this.type; + } + + /** + * this method is needed to add the variable to the Environment; the Environment from the + * Apron library holds all variables in two separated arrays, one for Integers and one for + * Rationals; it is a necessary component of an Abstract1 object. + */ + private void addVarToEnv() { + Var[] intVars = formulaCreator.getFormulaEnvironment().getIntVars(); + Var[] realVars = formulaCreator.getFormulaEnvironment().getRealVars(); + Var[] newRealVars = new Var[realVars.length + 1]; + int i = 0; + for (Var var : realVars) { + newRealVars[i] = var; + i++; + } + newRealVars[realVars.length] = new StringVar(this.varName); + formulaCreator.setFormulaEnvironment(new Environment(intVars, newRealVars)); + } + + @Override + public Texpr1VarNode getNode() { + return varNode; + } + + @Override + public Set getVarNames() { + Set vars = new HashSet<>(); + vars.add(this.varName); + return vars; + } + + @Override + public ApronNode getInstance() { + return this; + } + } + + /** + * This class wraps terms with unary arithmetic operators for rational values (ex. -x); it is + * build by an unary operator and a Node; + */ + class ApronRatUnaryNode implements RationalFormula, ApronNumeralNode { + private final Texpr1UnNode unaryNode; + private final Set varNames; + + public ApronRatUnaryNode(ApronNode param, int op) { + this.unaryNode = new Texpr1UnNode(op, param.getNode()); + this.varNames = param.getVarNames(); + } + + public ApronRatUnaryNode(ApronRatUnaryNode pNode) { + this.unaryNode = pNode.getNode(); + this.varNames = pNode.getVarNames(); + } + + public ApronRatUnaryNode(Texpr1UnNode pNode) { + this.unaryNode = pNode; + Var[] stringVars = pNode.getVars(); + Set variableNames = new HashSet<>(); + for (Var var : stringVars) { + variableNames.add(var.toString()); + } + this.varNames = variableNames; + } + + @Override + public String toString() { + return unaryNode.toString(); + } + + @Override + public boolean equals(Object other) { + if (other == this) { + return true; + } + if (!(other instanceof ApronRatUnaryNode)) { + return false; + } + return this == ((ApronRatUnaryNode) other).getInstance(); + } + + @Override + public int hashCode() { + return this.unaryNode.hashCode(); + } + + @Override + public FormulaType getType() { + return null; + } + + @Override + public Texpr1UnNode getNode() { + return this.unaryNode; + } + + @Override + public Set getVarNames() { + return varNames; + } + + @Override + public ApronNode getInstance() { + return this; + } + } + + /** + * This class wraps terms with binary arithmetic operators for rational values (ex. a+4.5); a + * binary node is defined by a binary operator and two nodes; + */ + class ApronRatBinaryNode implements RationalFormula, ApronNumeralNode { + + private final FormulaType type = FormulaType.RATIONAL; + private final Texpr1BinNode binaryNode; + private final Set varNames; + + public ApronRatBinaryNode(ApronNode param1, ApronNode param2, int op) { + this.binaryNode = new Texpr1BinNode(op, param1.getNode(), param2.getNode()); + this.varNames = new HashSet<>(); + // adding the variable names of both parameters to @varNames + this.varNames.addAll(param1.getVarNames()); + this.varNames.addAll(param2.getVarNames()); + } + + public ApronRatBinaryNode(ApronRatBinaryNode pNode) { + this.binaryNode = pNode.getNode(); + this.varNames = pNode.getVarNames(); + } + + public ApronRatBinaryNode(Texpr1BinNode pNode) { + this.binaryNode = pNode; + Var[] stringVars = pNode.getVars(); + Set variableNames = new HashSet<>(); + for (Var var : stringVars) { + variableNames.add(var.toString()); + } + this.varNames = variableNames; + } + + @Override + public String toString() { + return binaryNode.toString(); + } + + @Override + public boolean equals(Object other) { + if (other == this) { + return true; + } + if (!(other instanceof ApronRatBinaryNode)) { + return false; + } + return this == ((ApronRatBinaryNode) other).getInstance(); + } + + @Override + public int hashCode() { + return this.binaryNode.hashCode(); + } + + @Override + public FormulaType getType() { + return this.type; + } + + @Override + public Texpr1BinNode getNode() { + return this.binaryNode; + } + + @Override + public Set getVarNames() { + return varNames; + } + + @Override + public ApronNode getInstance() { + return this; + } + } + + /** This class wraps integer constants, defined by their BigInteger value. */ + class ApronIntCstNode implements IntegerFormula, ApronNumeralNode { + + private final FormulaType type = FormulaType.INTEGER; + private final Texpr1CstNode cstNode; + private final BigInteger value; + + public ApronIntCstNode(BigInteger pNumerator) { + this.cstNode = new Texpr1CstNode(new MpqScalar(pNumerator)); + this.value = pNumerator; + } + + public ApronIntCstNode(ApronIntCstNode pNode) { + this.cstNode = pNode.getNode(); + this.value = pNode.getValue(); + } + + /** + * constructor for transforming a rational constant to an integer constant. + * + * @param ratNode constant formula to transform + */ + public ApronIntCstNode(ApronRatCstNode ratNode) { + this.cstNode = + new Texpr1CstNode( + new MpqScalar( + BigInteger.valueOf( + Double.valueOf(Math.floor(ratNode.getRational().doubleValue())) + .longValue()))); + this.value = + BigInteger.valueOf( + Double.valueOf(Math.floor(ratNode.getRational().doubleValue())).longValue()); + } + + @Override + public String toString() { + return cstNode.toString(); + } + + @Override + public boolean equals(Object other) { + + if (other == this) { + return true; + } + if (!(other instanceof ApronIntCstNode)) { + return false; + } + return this == ((ApronIntCstNode) other).getInstance(); + } + + @Override + public int hashCode() { + return this.cstNode.hashCode(); + } + + @Override + public FormulaType getType() { + return this.type; + } + + @Override + public Texpr1CstNode getNode() { + return cstNode; + } + + @Override + public Set getVarNames() { + return new HashSet<>(); + } + + public BigInteger getValue() { + return value; + } + + @Override + public ApronNode getInstance() { + return this; + } + } + + /** This class wraps variables for integer values. */ + class ApronIntVarNode implements IntegerFormula, ApronNumeralNode { + + private final FormulaType type = FormulaType.INTEGER; + private final Texpr1VarNode varNode; + private final String varName; + private final ApronFormulaCreator formulaCreator; + + public ApronIntVarNode(String pVarName, ApronFormulaCreator pFormulaCreator) { + this.varNode = new Texpr1VarNode(pVarName); + this.varName = pVarName; + this.formulaCreator = pFormulaCreator; + addVarToEnv(); + } + + public ApronIntVarNode(ApronIntVarNode pNode) { + this.varNode = pNode.getNode(); + this.formulaCreator = pNode.getFormulaCreator(); + this.varName = pNode.getVarName(); + } + + /** + * constructor for converting a rational variable to an integer variable. + * + * @param rationalNode variable formula that should be transformed + */ + public ApronIntVarNode(ApronRatVarNode rationalNode) { + this.varNode = new Texpr1VarNode(rationalNode.varName); + this.varName = rationalNode.varName; + this.formulaCreator = rationalNode.getFormulaCreator(); + // deleting real variable from environment + Var[] intVars = formulaCreator.getFormulaEnvironment().getIntVars(); + Var[] realVars = formulaCreator.getFormulaEnvironment().getRealVars(); + List list = new ArrayList<>(Arrays.asList(realVars)); + Var v = new StringVar(varName); + list.remove(v); + Var[] newRealVars = new Var[list.size()]; + newRealVars = list.toArray(newRealVars); + formulaCreator.setFormulaEnvironment(new Environment(intVars, newRealVars)); + // adding int var to Environment + addVarToEnv(); + } + + public String getVarName() { + return varName; + } + + public ApronFormulaCreator getFormulaCreator() { + return formulaCreator; + } + + @Override + public String toString() { + return varNode.toString(); + } + + @Override + public boolean equals(Object other) { + + if (other == this) { + return true; + } + if (!(other instanceof ApronIntVarNode)) { + return false; + } + return this == ((ApronIntVarNode) other).getInstance(); + } + + @Override + public int hashCode() { + return this.varNode.hashCode(); + } + + @Override + public FormulaType getType() { + return this.type; + } + + @Override + public Texpr1VarNode getNode() { + return varNode; + } + + /** + * this method is needed to add the variable to the Environment; the Environment from the + * Apron library holds all variables in two separated arrays, one for Integers and one for + * Rationals; it is a necessary component of each Abstract1 object. + */ + private void addVarToEnv() { + Var[] intVars = formulaCreator.getFormulaEnvironment().getIntVars(); + Var[] realVars = formulaCreator.getFormulaEnvironment().getRealVars(); + Var[] newIntVars = new Var[intVars.length + 1]; + int i = 0; + for (Var var : intVars) { + newIntVars[i] = var; + i++; + } + newIntVars[intVars.length] = new StringVar(this.varName); + formulaCreator.setFormulaEnvironment(new Environment(newIntVars, realVars)); + } + + @Override + public Set getVarNames() { + Set vars = new HashSet<>(); + vars.add(this.varName); + return vars; + } + + @Override + public ApronNode getInstance() { + return this; + } + } + + /** + * This class wraps terms with unary arithmetic operators for integer values (ex. -x); it is + * build by an unary operator and a node + */ + class ApronIntUnaryNode implements IntegerFormula, ApronNumeralNode { + private final Texpr1UnNode unaryNode; + private final Set varNames; + + public ApronIntUnaryNode(ApronNode param, int op) { + this.unaryNode = + new Texpr1UnNode(op, Texpr1Node.RTYPE_INT, Texpr1Node.RDIR_DOWN, param.getNode()); + this.varNames = param.getVarNames(); + } + + public ApronIntUnaryNode(ApronIntUnaryNode pNode) { + this.unaryNode = pNode.getNode(); + this.unaryNode.setRoundingType(Texpr1Node.RTYPE_INT); + this.unaryNode.setRoundingDirection(Texpr1Node.RDIR_DOWN); + this.varNames = pNode.getVarNames(); + } + + /** + * constructor for transforming a rational formula to an integer formula. + * + * @param rationalNode formula to transform + */ + public ApronIntUnaryNode(ApronRatUnaryNode rationalNode) { + this.unaryNode = rationalNode.getNode(); + this.unaryNode.setRoundingType(Texpr1Node.RTYPE_INT); + this.unaryNode.setRoundingDirection(Texpr1Node.RDIR_DOWN); + this.varNames = rationalNode.getVarNames(); + } + + @Override + public String toString() { + return unaryNode.toString(); + } + + @Override + public boolean equals(Object other) { + + if (other == this) { + return true; + } + if (!(other instanceof ApronIntUnaryNode)) { + return false; + } + return this == ((ApronIntUnaryNode) other).getInstance(); + } + + @Override + public int hashCode() { + return this.unaryNode.hashCode(); + } + + @Override + public FormulaType getType() { + return null; + } + + @Override + public Texpr1UnNode getNode() { + return this.unaryNode; + } + + @Override + public Set getVarNames() { + return varNames; + } + + @Override + public ApronNode getInstance() { + return this; + } + } + + /** + * This class wraps terms with binary arithmetic operators for integer values (ex. x+3); it is + * build with an binary operator and two nodes + */ + class ApronIntBinaryNode implements IntegerFormula, ApronNumeralNode { + + private final FormulaType type = FormulaType.INTEGER; + private final Texpr1BinNode binaryNode; + private final Set varNames; + + public ApronIntBinaryNode(ApronNode param1, ApronNode param2, int op) { + this.binaryNode = + new Texpr1BinNode( + op, Texpr1Node.RTYPE_INT, Texpr1Node.RDIR_DOWN, param1.getNode(), param2.getNode()); + // adding the variablenames of both parameters to @varNames + this.varNames = new HashSet<>(); + varNames.addAll(param1.getVarNames()); + varNames.addAll(param2.getVarNames()); + } + + public ApronIntBinaryNode(ApronIntBinaryNode pNode) { + this.binaryNode = pNode.getNode(); + this.binaryNode.setRoundingType(Texpr1Node.RTYPE_INT); + this.binaryNode.setRoundingDirection(Texpr1Node.RDIR_DOWN); + this.varNames = pNode.getVarNames(); + } + + /** + * constructor for transforming a rational binary formula to an integer one. + * + * @param rationalNode formula to transform + */ + public ApronIntBinaryNode(ApronRatBinaryNode rationalNode) { + this.binaryNode = rationalNode.getNode(); + this.binaryNode.setRoundingType(Texpr1Node.RTYPE_INT); + this.binaryNode.setRoundingDirection(Texpr1Node.RDIR_DOWN); + this.varNames = rationalNode.getVarNames(); + } + + @Override + public String toString() { + return binaryNode.toString(); + } + + @Override + public boolean equals(Object other) { + + if (other == this) { + return true; + } + if (!(other instanceof ApronIntBinaryNode)) { + return false; + } + return this == ((ApronIntBinaryNode) other).getInstance(); + } + + @Override + public int hashCode() { + return this.binaryNode.hashCode(); + } + + @Override + public FormulaType getType() { + return this.type; + } + + @Override + public Texpr1BinNode getNode() { + return this.binaryNode; + } + + @Override + public Set getVarNames() { + return varNames; + } + + @Override + public ApronNode getInstance() { + return this; + } + } + } + + /** + * This class wraps boolean formulas defined by a node and a boolean operator =,!=, >, >=. All + * boolean formulas in Apron are syntactically like "Texpr1Node operation 0"; a constraint is + * defined by a map of Texpr1Nodes and an operation. The reason for the map is, that Apron does + * not have an extra and-operation. Stacking constraints ia a way to implement this for JavaSMT. + */ + class ApronConstraint implements BooleanFormula, ApronNode { + + private final Map constraintNodes; + private final List apronNodes; + private final Set varNames; + + /** + * Constructor for building a constraint form a map of nodes and Tcons1-operations (ex.: [ + * (a+1), Tcons1.EQ] -> (a+1) = 0). + * + * @param pEnvironment environment of all existing variables + * @param pConstraints map of nodes and boolean operators + */ + public ApronConstraint(Environment pEnvironment, Map pConstraints) { + this.constraintNodes = new HashMap<>(); + this.varNames = new HashSet<>(); + this.apronNodes = new ArrayList<>(); + for (Map.Entry entry : pConstraints.entrySet()) { + ApronNode key = entry.getKey(); + Integer kind = entry.getValue(); + Tcons1 tcons1 = new Tcons1(pEnvironment, kind, key.getNode()); + this.constraintNodes.put(tcons1, key.getNode()); + this.varNames.addAll(key.getVarNames()); + this.apronNodes.add(key); + } + } + + public ApronConstraint(ApronConstraint pConstraint) { + this.constraintNodes = pConstraint.getConstraintNodes(); + this.apronNodes = pConstraint.getApronNodes(); + this.varNames = pConstraint.getVarNames(); + } + + /** + * Constructor for building a new constraint out of a list of constraints. + * + * @param pConstraints list of constraints to build a new constraint + * @param pEnvironment environment of all existing variables + */ + public ApronConstraint(List pConstraints, Environment pEnvironment) { + this.constraintNodes = new HashMap<>(); + this.varNames = new HashSet<>(); + this.apronNodes = new ArrayList<>(); + for (ApronConstraint c : pConstraints) { + for (Map.Entry entry : c.getConstraintNodes().entrySet()) { + Tcons1 tcons1 = entry.getKey().extendEnvironmentCopy(pEnvironment); + constraintNodes.put(tcons1, entry.getValue()); + } + varNames.addAll(c.getVarNames()); + apronNodes.addAll(c.getApronNodes()); + } + } + + public List getApronNodes() { + return apronNodes; + } + + @Override + public String toString() { + StringBuilder builder = new StringBuilder(); + for (Map.Entry node : this.constraintNodes.entrySet()) { + builder.append(node.getKey().toString()).append("\n"); + } + return builder.toString(); + } + + @Override + public boolean equals(Object other) { + + if (other == this) { + return true; + } + if (!(other instanceof ApronConstraint)) { + return false; + } + return this == ((ApronConstraint) other).getInstance(); + } + + @Override + public int hashCode() { + return this.constraintNodes.hashCode(); + } + + @Override + public FormulaType getType() { + return FormulaType.BOOLEAN; + } + + /** + * As constraints can consist of multiple constraints, it is not logical to return just one + * constraint. + * + * @return the left side of the equation; ex.: 2x + 3 < 0 --> 2x + 3 + */ + @Override + public Texpr1Node getNode() { + throw new RuntimeException( + "For ApronConstraints, pleas use getConstraintNodes() or " + "getApronNodes()" + "."); + } + + public Map getConstraintNodes() { + return this.constraintNodes; + } + + @Override + public Set getVarNames() { + return varNames; + } + + @Override + public ApronNode getInstance() { + return this; + } + } +} diff --git a/src/org/sosy_lab/java_smt/solvers/apron/types/package-info.java b/src/org/sosy_lab/java_smt/solvers/apron/types/package-info.java new file mode 100644 index 0000000000..8577ca89de --- /dev/null +++ b/src/org/sosy_lab/java_smt/solvers/apron/types/package-info.java @@ -0,0 +1,14 @@ +// This file is part of JavaSMT, +// an API wrapper for a collection of SMT solvers: +// https://github.com/sosy-lab/java-smt +// +// SPDX-FileCopyrightText: 2024 Dirk Beyer +// +// SPDX-License-Identifier: Apache-2.0 + +/** Type interfaces for Apron. */ +@com.google.errorprone.annotations.CheckReturnValue +@javax.annotation.ParametersAreNonnullByDefault +@org.sosy_lab.common.annotations.FieldsAreNonnullByDefault +@org.sosy_lab.common.annotations.ReturnValuesAreNonnullByDefault +package org.sosy_lab.java_smt.solvers.apron.types; diff --git a/src/org/sosy_lab/java_smt/test/BooleanFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/BooleanFormulaManagerTest.java index 2e0b29fec1..2d0cff59e6 100644 --- a/src/org/sosy_lab/java_smt/test/BooleanFormulaManagerTest.java +++ b/src/org/sosy_lab/java_smt/test/BooleanFormulaManagerTest.java @@ -52,6 +52,7 @@ public void testVariableNamedFalse() throws SolverException, InterruptedExceptio @Test public void testConjunctionCollector() { + requireNonNumeralVariables(); List terms = ImmutableList.of( bmgr.makeVariable("a"), @@ -66,6 +67,7 @@ public void testConjunctionCollector() { @Test public void testDisjunctionCollector() { + requireNonNumeralVariables(); List terms = ImmutableList.of( bmgr.makeVariable("a"), @@ -88,6 +90,7 @@ public void testConjunctionArgsExtractionEmpty() throws SolverException, Interru @Test public void testConjunctionArgsExtraction() throws SolverException, InterruptedException { + requireNonNumeralVariables(); requireIntegers(); BooleanFormula input = bmgr.and(bmgr.makeVariable("a"), imgr.equal(imgr.makeNumber(1), imgr.makeVariable("x"))); @@ -101,6 +104,7 @@ public void testConjunctionArgsExtraction() throws SolverException, InterruptedE @Test public void testConjunctionArgsExtractionRecursive() throws SolverException, InterruptedException { + requireNonNumeralVariables(); BooleanFormula input; ImmutableSet comparisonSet; if (imgr != null) { @@ -166,6 +170,7 @@ public void testDisjunctionArgsExtractionEmpty() throws SolverException, Interru @Test public void testDisjunctionArgsExtraction() throws SolverException, InterruptedException { + requireNonNumeralVariables(); BooleanFormula input; ImmutableSet comparisonSet; if (imgr != null) { @@ -194,6 +199,7 @@ public void testDisjunctionArgsExtraction() throws SolverException, InterruptedE @Test public void testDisjunctionArgsExtractionRecursive() throws SolverException, InterruptedException { + requireNonNumeralVariables(); BooleanFormula input; ImmutableSet comparisonSet; if (imgr != null) { @@ -251,6 +257,7 @@ public void testDisjunctionArgsExtractionRecursive() @Test public void simplificationTest() { + requireNonNumeralVariables(); // Boolector and CVC5 fail this as it either simplifies to much, or nothing // TODO: maybe this is just a matter of options, check! assume() @@ -305,6 +312,7 @@ public void simplificationTest() { @Test public void simpleImplicationTest() throws InterruptedException, SolverException { + requireNonNumeralVariables(); BooleanFormula x = bmgr.makeVariable("x"); BooleanFormula y = bmgr.makeVariable("y"); BooleanFormula z = bmgr.makeVariable("z"); @@ -315,6 +323,7 @@ public void simpleImplicationTest() throws InterruptedException, SolverException @Test public void simplifiedNot() { + requireNonNumeralVariables(); BooleanFormula fTrue = bmgr.makeTrue(); BooleanFormula fFalse = bmgr.makeFalse(); BooleanFormula var1 = bmgr.makeVariable("var1"); @@ -336,6 +345,7 @@ public void simplifiedNot() { @Test public void simplifiedAnd() { + requireNonNumeralVariables(); BooleanFormula fTrue = bmgr.makeTrue(); BooleanFormula fFalse = bmgr.makeFalse(); BooleanFormula var1 = bmgr.makeVariable("var1"); @@ -359,6 +369,7 @@ public void simplifiedAnd() { @Test public void simplifiedOr() { + requireNonNumeralVariables(); BooleanFormula fTrue = bmgr.makeTrue(); BooleanFormula fFalse = bmgr.makeFalse(); BooleanFormula var1 = bmgr.makeVariable("var1"); @@ -382,6 +393,7 @@ public void simplifiedOr() { @Test public void simplifiedIfThenElse() { + requireNonNumeralVariables(); BooleanFormula fTrue = bmgr.makeTrue(); BooleanFormula fFalse = bmgr.makeFalse(); BooleanFormula var1 = bmgr.makeVariable("var1"); diff --git a/src/org/sosy_lab/java_smt/test/BooleanFormulaSubjectTest.java b/src/org/sosy_lab/java_smt/test/BooleanFormulaSubjectTest.java index 2f85cca4b8..5ed9198abe 100644 --- a/src/org/sosy_lab/java_smt/test/BooleanFormulaSubjectTest.java +++ b/src/org/sosy_lab/java_smt/test/BooleanFormulaSubjectTest.java @@ -34,6 +34,7 @@ public class BooleanFormulaSubjectTest extends SolverBasedTest0.ParameterizedSol @Before public void setupFormulas() { + requireNot(); if (imgr != null) { simpleFormula = imgr.equal(imgr.makeVariable("a"), imgr.makeNumber(1)); contradiction = @@ -66,7 +67,7 @@ public void testIsSatisfiableYes() throws SolverException, InterruptedException @Test public void testIsSatisfiableNo() { - // INFO: OpenSMT does not support unsat core + requireUnsatCore(); assume() .withMessage("Solver does not support unsat core generation in a usable way") .that(solverToUse()) @@ -167,9 +168,9 @@ public void testIsEquisatisfiableToYes() throws SolverException, InterruptedExce public void testIsEquisatisfiableToNo() { BooleanFormula simpleFormula2; if (imgr != null) { - simpleFormula2 = imgr.equal(imgr.makeVariable("a"), imgr.makeNumber("2")); + simpleFormula2 = imgr.equal(imgr.makeVariable("a"), imgr.makeNumber(2)); } else { - simpleFormula2 = bvmgr.equal(bvmgr.makeVariable(2, "a"), bvmgr.makeVariable(2, "2")); + simpleFormula2 = bvmgr.equal(bvmgr.makeVariable(2, "a"), bvmgr.makeBitvector(2, 2)); } AssertionError failure = expectFailure( diff --git a/src/org/sosy_lab/java_smt/test/FormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/FormulaManagerTest.java index fffdcb36e7..430a556ca8 100644 --- a/src/org/sosy_lab/java_smt/test/FormulaManagerTest.java +++ b/src/org/sosy_lab/java_smt/test/FormulaManagerTest.java @@ -33,7 +33,10 @@ public class FormulaManagerTest extends SolverBasedTest0.ParameterizedSolverBase @Test public void testEmptySubstitution() throws SolverException, InterruptedException { + requireUninterpretedFunctions(); requireSubstitution(); + // Boolector does not support substitution + assume().that(solverToUse()).isNotEqualTo(Solvers.BOOLECTOR); assume().withMessage("Princess fails").that(solver).isNotEqualTo(Solvers.PRINCESS); IntegerFormula variable1 = imgr.makeVariable("variable1"); @@ -54,6 +57,9 @@ public void testEmptySubstitution() throws SolverException, InterruptedException @Test public void testNoSubstitution() throws SolverException, InterruptedException { requireSubstitution(); + requireUninterpretedFunctions(); + // Boolector does not support substitution + assume().that(solverToUse()).isNotEqualTo(Solvers.BOOLECTOR); assume().withMessage("Princess fails").that(solver).isNotEqualTo(Solvers.PRINCESS); IntegerFormula variable1 = imgr.makeVariable("variable1"); @@ -79,8 +85,10 @@ public void testNoSubstitution() throws SolverException, InterruptedException { @Test public void testSubstitution() throws SolverException, InterruptedException { + requireNonNumeralVariables(); requireSubstitution(); - + // Boolector does not support substitution + assume().that(solverToUse()).isNotEqualTo(Solvers.BOOLECTOR); BooleanFormula input = bmgr.or( bmgr.and(bmgr.makeVariable("a"), bmgr.makeVariable("b")), @@ -101,8 +109,10 @@ public void testSubstitution() throws SolverException, InterruptedException { @Test public void testSubstitutionTwice() throws SolverException, InterruptedException { + requireNonNumeralVariables(); requireSubstitution(); - + // Boolector does not support substitution + assume().that(solverToUse()).isNotEqualTo(Solvers.BOOLECTOR); BooleanFormula input = bmgr.or( bmgr.and(bmgr.makeVariable("a"), bmgr.makeVariable("b")), @@ -171,6 +181,7 @@ public void testSubstitutionSelfReference() throws SolverException, InterruptedE @Test public void formulaEqualsAndHashCode() { + requireUninterpretedFunctions(); // Solvers without integers (Boolector) get their own test below assume().that(solverToUse()).isNotEqualTo(Solvers.BOOLECTOR); FunctionDeclaration fb = fmgr.declareUF("f_b", IntegerType, IntegerType); @@ -270,6 +281,7 @@ public void bitvectorFormulaEqualsAndHashCode() { @Test public void variableNameExtractorTest() { + requireOr(); // Since Boolector does not support integers we use bitvectors if (imgr != null) { BooleanFormula constr = @@ -302,6 +314,7 @@ public void variableNameExtractorTest() { @Test public void ufNameExtractorTest() { + requireUninterpretedFunctions(); // Since Boolector does not support integers we use bitvectors for constraints if (imgr != null) { BooleanFormula constraint = @@ -336,6 +349,7 @@ public void ufNameExtractorTest() { @Test public void simplifyIntTest() throws SolverException, InterruptedException { requireIntegers(); + requireNot(); // x=1 && y=x+2 && z=y+3 --> simplified: x=1 && y=3 && z=6 IntegerFormula num1 = imgr.makeNumber(1); IntegerFormula num2 = imgr.makeNumber(2); diff --git a/src/org/sosy_lab/java_smt/test/ModelEvaluationTest.java b/src/org/sosy_lab/java_smt/test/ModelEvaluationTest.java index ec82b870b7..a16d7822cb 100644 --- a/src/org/sosy_lab/java_smt/test/ModelEvaluationTest.java +++ b/src/org/sosy_lab/java_smt/test/ModelEvaluationTest.java @@ -133,6 +133,7 @@ public void testGetRationalsEvaluation() throws SolverException, InterruptedExce @Test public void testGetBooleansEvaluation() throws SolverException, InterruptedException { + requireNonNumeralVariables(); final boolean defaultValue; if (solverToUse() == Solvers.OPENSMT) { defaultValue = true; // Default value for boolean in OpenSMT is 'true'. @@ -159,6 +160,7 @@ public void testGetStringsEvaluation() throws SolverException, InterruptedExcept @Test public void testModelGeneration() throws SolverException, InterruptedException { + requireNonNumeralVariables(); try (ProverEnvironment prover = context.newProverEnvironment(ProverOptions.GENERATE_MODELS)) { prover.push(bmgr.and(getConstraints())); for (int i = 0; i < problemSize; i++) { @@ -172,6 +174,7 @@ public void testModelGeneration() throws SolverException, InterruptedException { @Test public void testEvaluatorGeneration() throws SolverException, InterruptedException { + requireNonNumeralVariables(); try (ProverEnvironment prover = context.newProverEnvironment(ProverOptions.GENERATE_MODELS)) { prover.push(bmgr.and(getConstraints())); for (int i = 0; i < problemSize; i++) { diff --git a/src/org/sosy_lab/java_smt/test/ModelTest.java b/src/org/sosy_lab/java_smt/test/ModelTest.java index f1622b109b..331b5cfed0 100644 --- a/src/org/sosy_lab/java_smt/test/ModelTest.java +++ b/src/org/sosy_lab/java_smt/test/ModelTest.java @@ -102,6 +102,7 @@ public void testEmpty() throws SolverException, InterruptedException { @Test public void testOnlyTrue() throws SolverException, InterruptedException { + requireUnsatCore(); try (ProverEnvironment prover = context.newProverEnvironment(ProverOptions.GENERATE_MODELS)) { prover.push(bmgr.makeTrue()); assertThat(prover).isSatisfiable(); @@ -117,6 +118,7 @@ public void testOnlyTrue() throws SolverException, InterruptedException { @Test public void testGetSmallIntegers() throws SolverException, InterruptedException { requireIntegers(); + requireNot(); testModelGetters( imgr.equal(imgr.makeVariable("x"), imgr.makeNumber(10)), imgr.makeVariable("x"), @@ -127,6 +129,7 @@ public void testGetSmallIntegers() throws SolverException, InterruptedException @Test public void testGetNegativeIntegers() throws SolverException, InterruptedException { requireIntegers(); + requireNot(); testModelGetters( imgr.equal(imgr.makeVariable("x"), imgr.makeNumber(-10)), imgr.makeVariable("x"), @@ -137,6 +140,7 @@ public void testGetNegativeIntegers() throws SolverException, InterruptedExcepti @Test public void testGetLargeIntegers() throws SolverException, InterruptedException { requireIntegers(); + requireNot(); BigInteger large = new BigInteger("1000000000000000000000000000000000000000"); testModelGetters( imgr.equal(imgr.makeVariable("x"), imgr.makeNumber(large)), @@ -149,6 +153,7 @@ public void testGetLargeIntegers() throws SolverException, InterruptedException public void testGetSmallIntegralRationals() throws SolverException, InterruptedException { requireIntegers(); requireRationals(); + requireNot(); testModelGetters( rmgr.equal(rmgr.makeVariable("x"), rmgr.makeNumber(1)), rmgr.makeVariable("x"), @@ -160,6 +165,7 @@ public void testGetSmallIntegralRationals() throws SolverException, InterruptedE public void testGetLargeIntegralRationals() throws SolverException, InterruptedException { requireIntegers(); requireRationals(); + requireNot(); BigInteger large = new BigInteger("1000000000000000000000000000000000000000"); testModelGetters( rmgr.equal(rmgr.makeVariable("x"), rmgr.makeNumber(large)), @@ -172,6 +178,7 @@ public void testGetLargeIntegralRationals() throws SolverException, InterruptedE public void testGetRationals() throws SolverException, InterruptedException { requireIntegers(); requireRationals(); + requireNot(); for (String name : VARIABLE_NAMES) { testModelGetters( rmgr.equal(rmgr.makeVariable(name), rmgr.makeNumber(Rational.ofString("1/3"))), @@ -184,6 +191,7 @@ public void testGetRationals() throws SolverException, InterruptedException { /** Test that different names are no problem for Bools in the model. */ @Test public void testGetBooleans() throws SolverException, InterruptedException { + requireNonNumeralVariables(); // Some names are specificly chosen to test the Boolector model for (String name : VARIABLE_NAMES) { testModelGetters(bmgr.makeVariable(name), bmgr.makeBoolean(true), true, name); @@ -209,6 +217,7 @@ public void testGetBvs() throws SolverException, InterruptedException { @Test public void testGetInts() throws SolverException, InterruptedException { requireIntegers(); + requireNot(); for (String name : VARIABLE_NAMES) { testModelGetters( imgr.equal(imgr.makeVariable(name), imgr.makeNumber(1)), @@ -244,6 +253,7 @@ public void testGetBvUfs() throws SolverException, InterruptedException { @Test public void testGetIntUfs() throws SolverException, InterruptedException { requireIntegers(); + requireUninterpretedFunctions(); // Some names are specificly chosen to test the Boolector model // Use 1 instead of 0 or max bv value, as solvers tend to use 0, min or max as default for (String ufName : VARIABLE_NAMES) { @@ -266,6 +276,7 @@ public void testGetIntUfs() throws SolverException, InterruptedException { @Test public void testGetUFs() throws SolverException, InterruptedException { + requireUninterpretedFunctions(); // Boolector does not support integers if (imgr != null) { IntegerFormula x = @@ -300,6 +311,7 @@ public void testGetUFs() throws SolverException, InterruptedException { @Test public void testGetUFsWithMultipleAssignments() throws SolverException, InterruptedException { requireIntegers(); + requireUninterpretedFunctions(); List constraints = new ArrayList<>(); int num = 4; @@ -335,6 +347,7 @@ public void testGetUFsWithMultipleAssignments() throws SolverException, Interrup @Test public void testGetUFwithMoreParams() throws Exception { + requireUninterpretedFunctions(); // Boolector does not support integers if (imgr != null) { IntegerFormula x = @@ -357,6 +370,7 @@ public void testGetUFwithMoreParams() throws Exception { @Test public void testGetMultipleUFsWithInts() throws Exception { requireIntegers(); + requireUninterpretedFunctions(); IntegerFormula arg1 = imgr.makeVariable("arg1"); IntegerFormula arg2 = imgr.makeVariable("arg2"); FunctionDeclaration declaration = @@ -763,6 +777,7 @@ public void testEmptyStackModel() throws SolverException, InterruptedException { @Test public void testNonExistantSymbol() throws SolverException, InterruptedException { + requireUnsatCore(); if (imgr != null) { try (ProverEnvironment prover = context.newProverEnvironment(ProverOptions.GENERATE_MODELS)) { prover.push(bmgr.makeBoolean(true)); @@ -863,6 +878,7 @@ public void testPartialModelsUF() throws SolverException, InterruptedException { @Test public void testEvaluatingConstants() throws SolverException, InterruptedException { + requireNonNumeralVariables(); try (ProverEnvironment prover = context.newProverEnvironment(ProverOptions.GENERATE_MODELS)) { prover.push(bmgr.makeVariable("b")); assertThat(prover.isUnsat()).isFalse(); @@ -893,6 +909,7 @@ public void testEvaluatingConstants() throws SolverException, InterruptedExcepti @Test public void testEvaluatingConstantsWithOperation() throws SolverException, InterruptedException { + requireNonNumeralVariables(); try (ProverEnvironment prover = context.newProverEnvironment(ProverOptions.GENERATE_MODELS)) { prover.push(bmgr.makeVariable("b")); assertThat(prover.isUnsat()).isFalse(); @@ -2296,6 +2313,10 @@ public void modelAfterSolverCloseTest() throws SolverException, InterruptedExcep @SuppressWarnings("resource") @Test(expected = IllegalStateException.class) public void testGenerateModelsOption() throws SolverException, InterruptedException { + assume() + .withMessage("The Apron solver can not execute this test.") + .that(solver) + .isNotSameInstanceAs(Solvers.APRON); try (ProverEnvironment prover = context.newProverEnvironment()) { // no option assertThat(prover).isSatisfiable(); prover.getModel(); @@ -2305,6 +2326,10 @@ public void testGenerateModelsOption() throws SolverException, InterruptedExcept @Test(expected = IllegalStateException.class) public void testGenerateModelsOption2() throws SolverException, InterruptedException { + assume() + .withMessage("The Apron solver can not execute this test.") + .that(solver) + .isNotSameInstanceAs(Solvers.APRON); try (ProverEnvironment prover = context.newProverEnvironment()) { // no option assertThat(prover).isSatisfiable(); prover.getModelAssignments(); @@ -2359,6 +2384,7 @@ public void testGetRationals1() throws SolverException, InterruptedException { @Test public void testGetBooleans1() throws SolverException, InterruptedException { + requireNonNumeralVariables(); evaluateInModel(bmgr.makeVariable("x"), bmgr.makeBoolean(true), true); evaluateInModel(bmgr.makeVariable("x"), bmgr.makeBoolean(false), false); evaluateInModel( @@ -2375,6 +2401,7 @@ public void testGetBooleans1() throws SolverException, InterruptedException { // TODO CVC5 crashes on making the first boolean symbol when using timeout ???. public void testDeeplyNestedFormulaLIA() throws SolverException, InterruptedException { requireIntegers(); + requireNonNumeralVariables(); testDeeplyNestedFormula( depth -> imgr.makeVariable("i_" + depth), diff --git a/src/org/sosy_lab/java_smt/test/NonLinearArithmeticTest.java b/src/org/sosy_lab/java_smt/test/NonLinearArithmeticTest.java index 786ae61578..eccade9fcf 100644 --- a/src/org/sosy_lab/java_smt/test/NonLinearArithmeticTest.java +++ b/src/org/sosy_lab/java_smt/test/NonLinearArithmeticTest.java @@ -135,6 +135,7 @@ public void testLinearMultiplication() throws SolverException, InterruptedExcept @Test public void testLinearMultiplicationUnsatisfiable() throws SolverException, InterruptedException { + requireXOr(); T a = nmgr.makeVariable("a"); BooleanFormula f = @@ -164,6 +165,7 @@ public void testMultiplicationOfVariables() throws SolverException, InterruptedE @Test public void testMultiplicationOfVariablesUnsatisfiable() throws SolverException, InterruptedException { + requireNot(); T a = nmgr.makeVariable("a"); T b = nmgr.makeVariable("b"); T c = nmgr.makeVariable("c"); @@ -187,6 +189,7 @@ public void testMultiplicationOfVariablesUnsatisfiable() @Test public void testDivisionByConstant() throws SolverException, InterruptedException { + requireCallFunctionImpl(); T a = nmgr.makeVariable("a"); BooleanFormula f = @@ -200,6 +203,7 @@ public void testDivisionByConstant() throws SolverException, InterruptedExceptio @Test public void testDivisionByZero() throws SolverException, InterruptedException { + requireCallFunctionImpl(); // INFO: OpenSmt does not allow division by zero assume() .withMessage("Solver %s does not support division by zero", solverToUse()) @@ -220,6 +224,8 @@ public void testDivisionByZero() throws SolverException, InterruptedException { @Test public void testDivisionByConstantUnsatisfiable() throws SolverException, InterruptedException { + requireXOr(); + requireCallFunctionImpl(); T a = nmgr.makeVariable("a"); BooleanFormula f = @@ -241,6 +247,7 @@ public void testDivisionByConstantUnsatisfiable() throws SolverException, Interr @Test public void testDivision() throws SolverException, InterruptedException { + requireCallFunctionImpl(); T a = nmgr.makeVariable("a"); // (a == 2) && (3 == 6 / a) @@ -256,6 +263,7 @@ public void testDivision() throws SolverException, InterruptedException { @Test public void testDivisionUnsatisfiable() throws SolverException, InterruptedException { + requireNot(); T a = nmgr.makeVariable("a"); BooleanFormula f = diff --git a/src/org/sosy_lab/java_smt/test/NonLinearArithmeticWithModuloTest.java b/src/org/sosy_lab/java_smt/test/NonLinearArithmeticWithModuloTest.java index 16b811f764..7a8ae339f2 100644 --- a/src/org/sosy_lab/java_smt/test/NonLinearArithmeticWithModuloTest.java +++ b/src/org/sosy_lab/java_smt/test/NonLinearArithmeticWithModuloTest.java @@ -99,6 +99,7 @@ public void testModuloConstant() throws SolverException, InterruptedException { @Test public void testModuloConstantUnsatisfiable() throws SolverException, InterruptedException { requireIntegers(); + requirePrecision(); IntegerFormula a = imgr.makeVariable("a"); BooleanFormula f = @@ -123,6 +124,7 @@ public void testModuloConstantUnsatisfiable() throws SolverException, Interrupte @Test public void testModulo() throws SolverException, InterruptedException { requireIntegers(); + requireNonLinearModulo(); IntegerFormula a = imgr.makeVariable("a"); BooleanFormula f = @@ -138,6 +140,7 @@ public void testModulo() throws SolverException, InterruptedException { @Test public void testModuloUnsatisfiable() throws SolverException, InterruptedException { requireIntegers(); + requireNonLinearModulo(); IntegerFormula a = imgr.makeVariable("a"); BooleanFormula f = diff --git a/src/org/sosy_lab/java_smt/test/NumeralFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/NumeralFormulaManagerTest.java index 4461a7495a..8118a82732 100644 --- a/src/org/sosy_lab/java_smt/test/NumeralFormulaManagerTest.java +++ b/src/org/sosy_lab/java_smt/test/NumeralFormulaManagerTest.java @@ -56,6 +56,7 @@ public void distinctTest2() throws SolverException, InterruptedException { @Test public void distinctTest3() throws SolverException, InterruptedException { requireIntegers(); + requirePrecision(); IntegerFormula zero = imgr.makeNumber(0); IntegerFormula four = imgr.makeNumber(4); List symbols = new ArrayList<>(); @@ -88,6 +89,7 @@ public void failOnInvalidStringRational() { public void testSubTypes() { requireIntegers(); requireRationals(); + requireUninterpretedFunctions(); IntegerFormula a = imgr.makeVariable("a"); RationalFormula r = rmgr.makeVariable("r"); List> argTypes = diff --git a/src/org/sosy_lab/java_smt/test/ProverEnvironmentTest.java b/src/org/sosy_lab/java_smt/test/ProverEnvironmentTest.java index 5380e5d4b3..19027f9c09 100644 --- a/src/org/sosy_lab/java_smt/test/ProverEnvironmentTest.java +++ b/src/org/sosy_lab/java_smt/test/ProverEnvironmentTest.java @@ -12,6 +12,7 @@ import static com.google.common.truth.Truth8.assertThat; import static com.google.common.truth.TruthJUnit.assume; import static org.junit.Assert.assertThrows; +import static org.sosy_lab.java_smt.SolverContextFactory.Solvers.APRON; import static org.sosy_lab.java_smt.SolverContextFactory.Solvers.CVC4; import static org.sosy_lab.java_smt.SolverContextFactory.Solvers.CVC5; import static org.sosy_lab.java_smt.SolverContextFactory.Solvers.MATHSAT5; @@ -35,6 +36,7 @@ public class ProverEnvironmentTest extends SolverBasedTest0.ParameterizedSolverB @Test public void assumptionsTest() throws SolverException, InterruptedException { + requireNonNumeralVariables(); BooleanFormula b = bmgr.makeVariable("b"); BooleanFormula c = bmgr.makeVariable("c"); @@ -50,6 +52,7 @@ public void assumptionsTest() throws SolverException, InterruptedException { @Test public void assumptionsWithModelTest() throws SolverException, InterruptedException { + requireNonNumeralVariables(); assume() .withMessage("MathSAT can't construct models for SAT check with assumptions") .that(solver) @@ -72,6 +75,7 @@ public void assumptionsWithModelTest() throws SolverException, InterruptedExcept @Test public void unsatCoreTest() throws SolverException, InterruptedException { + // Boolector and Apron do not support unsat core requireUnsatCore(); try (BasicProverEnvironment pe = context.newProverEnvironment(GENERATE_UNSAT_CORE)) { unsatCoreTest0(pe); @@ -130,11 +134,12 @@ public void unsatCoreWithAssumptionsNullTest() { @Test public void unsatCoreWithAssumptionsTest() throws SolverException, InterruptedException { requireUnsatCore(); + requireNonNumeralVariables(); assume() .withMessage( "Solver %s does not support unsat core generation over assumptions", solverToUse()) .that(solverToUse()) - .isNoneOf(PRINCESS, CVC4, CVC5); + .isNoneOf(PRINCESS, CVC4, CVC5, APRON); try (ProverEnvironment pe = context.newProverEnvironment(GENERATE_UNSAT_CORE_OVER_ASSUMPTIONS)) { pe.push(); diff --git a/src/org/sosy_lab/java_smt/test/RationalFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/RationalFormulaManagerTest.java index 1515133f88..9bf84fa030 100644 --- a/src/org/sosy_lab/java_smt/test/RationalFormulaManagerTest.java +++ b/src/org/sosy_lab/java_smt/test/RationalFormulaManagerTest.java @@ -54,6 +54,7 @@ public void rationalToIntTest() throws SolverException, InterruptedException { @Test public void intToIntTest() throws SolverException, InterruptedException { requireIntegers(); + requireNot(); for (double v : SOME_DOUBLES) { IntegerFormula i = imgr.makeNumber((int) Math.floor(v)); assertThat(mgr.getFormulaType(i)).isEqualTo(FormulaType.IntegerType); @@ -65,6 +66,7 @@ public void intToIntTest() throws SolverException, InterruptedException { @Test public void intToIntWithRmgrTest() throws SolverException, InterruptedException { requireRationals(); + requireNot(); for (double v : SOME_DOUBLES) { IntegerFormula i = imgr.makeNumber((int) Math.floor(v)); assertThat(mgr.getFormulaType(i)).isEqualTo(FormulaType.IntegerType); @@ -109,6 +111,7 @@ public void forallFloorIsLessThanValueTest() throws SolverException, Interrupted @Test public void visitFloorTest() { requireRationals(); + requireVisit(); assume() .withMessage("Solver %s does not support floor operation", solverToUse()) .that(solverToUse()) diff --git a/src/org/sosy_lab/java_smt/test/SolverAllSatTest.java b/src/org/sosy_lab/java_smt/test/SolverAllSatTest.java index 0ef9a46b14..c6c0f2e018 100644 --- a/src/org/sosy_lab/java_smt/test/SolverAllSatTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverAllSatTest.java @@ -119,7 +119,7 @@ public String getResult() { @Test public void allSatTest_unsat() throws SolverException, InterruptedException { requireIntegers(); - + requireNonNumeralVariables(); IntegerFormula a = imgr.makeVariable("i"); IntegerFormula n1 = imgr.makeNumber(1); IntegerFormula n2 = imgr.makeNumber(2); @@ -152,7 +152,7 @@ public void apply(List pModel) { @Test public void allSatTest_xor() throws SolverException, InterruptedException { requireIntegers(); - + requireNonNumeralVariables(); IntegerFormula a = imgr.makeVariable("i"); IntegerFormula n1 = imgr.makeNumber(1); IntegerFormula n2 = imgr.makeNumber(2); @@ -181,6 +181,7 @@ public void allSatTest_xor() throws SolverException, InterruptedException { @Test public void allSatTest_nondetValue() throws SolverException, InterruptedException { + requireNonNumeralVariables(); BooleanFormula v1 = bmgr.makeVariable("b1"); BooleanFormula v2 = bmgr.makeVariable("b2"); diff --git a/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java b/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java index d57494e017..9230fbc43a 100644 --- a/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java +++ b/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java @@ -208,6 +208,14 @@ protected final void requireIntegers() { .isNotNull(); } + protected final void requirePrecision() { + assume() + .withMessage( + "Solver %s gives non-precise solutions due to over-approximation", solverToUse()) + .that(solverToUse()) + .isNotEqualTo(Solvers.APRON); + } + /** Skip test if the solver does not support rationals. */ protected final void requireRationals() { assume() @@ -303,7 +311,7 @@ protected void requireParser() { assume() .withMessage("Solver %s does not support parsing formulae", solverToUse()) .that(solverToUse()) - .isNoneOf(Solvers.CVC4, Solvers.BOOLECTOR, Solvers.YICES2, Solvers.CVC5); + .isNoneOf(Solvers.CVC4, Solvers.BOOLECTOR, Solvers.YICES2, Solvers.CVC5, Solvers.APRON); } protected void requireArrayModel() { @@ -325,14 +333,14 @@ protected void requireVisitor() { assume() .withMessage("Solver %s does not support formula visitor", solverToUse()) .that(solverToUse()) - .isNotEqualTo(Solvers.BOOLECTOR); + .isNoneOf(Solvers.BOOLECTOR, Solvers.APRON); } protected void requireUnsatCore() { assume() .withMessage("Solver %s does not support unsat core generation", solverToUse()) .that(solverToUse()) - .isNoneOf(Solvers.BOOLECTOR, Solvers.OPENSMT); + .isNoneOf(Solvers.BOOLECTOR, Solvers.OPENSMT, Solvers.APRON); } protected void requireUnsatCoreOverAssumptions() { @@ -346,7 +354,72 @@ protected void requireSubstitution() { assume() .withMessage("Solver %s does not support formula substitution", solverToUse()) .that(solverToUse()) - .isNotEqualTo(Solvers.BOOLECTOR); + .isNoneOf(Solvers.BOOLECTOR, Solvers.APRON); + } + + protected void requireNonNumeralVariables() { + assume() + .withMessage("Solver %s does not support non-numeral variables", solverToUse()) + .that(solverToUse()) + .isNotEqualTo(Solvers.APRON); + } + + protected void requireDumpFormula() { + assume() + .withMessage("Solver %s does not support dumpFormula() method", solverToUse()) + .that(solverToUse()) + .isNotEqualTo(Solvers.APRON); + } + + protected void requireNot() { + assume() + .withMessage("Solver %s does not support not()-operations", solverToUse()) + .that(solverToUse()) + .isNotEqualTo(Solvers.APRON); + } + + protected void requireOr() { + assume() + .withMessage("Solver %s does not support or()-operations", solverToUse()) + .that(solverToUse()) + .isNotEqualTo(Solvers.APRON); + } + + protected void requireXOr() { + assume() + .withMessage("Solver %s does not support xor()-operations", solverToUse()) + .that(solverToUse()) + .isNotEqualTo(Solvers.APRON); + } + + protected void requireNonLinearModulo() { + assume() + .withMessage( + "Solver %s does not support variables as denumerator in modulo operations", + solverToUse()) + .that(solverToUse()) + .isNotEqualTo(Solvers.APRON); + } + + protected void requireCallFunctionImpl() { + assume() + .withMessage("Solver %s does not support callFunctionImpl()", solverToUse()) + .that(solverToUse()) + .isNotEqualTo(Solvers.APRON); + } + + protected void requireUninterpretedFunctions() { + assume() + .withMessage("Solver %s does not support uninterpreted functions", solverToUse()) + .that(solverToUse()) + .isNotEqualTo(Solvers.APRON); + } + + protected void requireVisit() { + assume() + .withMessage("Solver %s does not support visit()-method", solverToUse()) + .that(solverToUse()) + .isNotEqualTo(Solvers.APRON); } protected void requireUserPropagators() { @@ -414,6 +487,9 @@ protected void evaluateInModel( case BOOLECTOR: // ignore, Boolector provides no useful values break; + case APRON: + // ignore, Apron does not provide useful values + break; default: Truth.assertThat(eval).isIn(possibleExpectedFormulas); } diff --git a/src/org/sosy_lab/java_smt/test/SolverConcurrencyTest.java b/src/org/sosy_lab/java_smt/test/SolverConcurrencyTest.java index ea3bae1d36..d5a4050c46 100644 --- a/src/org/sosy_lab/java_smt/test/SolverConcurrencyTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverConcurrencyTest.java @@ -148,7 +148,7 @@ private void requireBitvectors() { assume() .withMessage("Solver does not support bitvectors") .that(solver) - .isNoneOf(Solvers.SMTINTERPOL, Solvers.YICES2, Solvers.OPENSMT); + .isNoneOf(Solvers.SMTINTERPOL, Solvers.YICES2, Solvers.OPENSMT, Solvers.APRON); } private void requireOptimization() { @@ -162,7 +162,15 @@ private void requireOptimization() { Solvers.CVC4, Solvers.CVC5, Solvers.YICES2, - Solvers.OPENSMT); + Solvers.OPENSMT, + Solvers.APRON); + } + + protected void requireNonNumeralVariables() { + assume() + .withMessage("Solver %s does not support non-numeral variables", solverToUse()) + .that(solverToUse()) + .isNotEqualTo(Solvers.APRON); } /** @@ -172,6 +180,7 @@ private void requireOptimization() { @Test public void testIntConcurrencyWithConcurrentContext() { requireIntegers(); + requireNonNumeralVariables(); assertConcurrency( "testIntConcurrencyWithConcurrentContext", () -> { @@ -225,6 +234,7 @@ BooleanFormula getFormula() { public void testFormulaTranslationWithConcurrentContexts() throws InvalidConfigurationException, InterruptedException, SolverException { requireIntegers(); + requireNonNumeralVariables(); // CVC4 does not support parsing and therefore no translation. // Princess has a wierd bug // TODO: Look into the Princess problem @@ -280,7 +290,7 @@ public void testFormulaTranslationWithConcurrentContexts() @Test public void testIntConcurrencyWithoutConcurrentContext() throws InvalidConfigurationException { requireIntegers(); - + requireNonNumeralVariables(); assume() .withMessage("Solver does not support concurrency without concurrent context.") .that(solver) @@ -350,6 +360,7 @@ public void testConcurrentOptimization() { @Test public void testConcurrentStack() throws InvalidConfigurationException, InterruptedException { requireConcurrentMultipleStackSupport(); + requireNonNumeralVariables(); SolverContext context = initSolver(); FormulaManager mgr = context.getFormulaManager(); IntegerFormulaManager imgr = mgr.getIntegerFormulaManager(); @@ -437,6 +448,7 @@ private void intConcurrencyTest(SolverContext context) @Test public void continuousRunningThreadFormulaTransferTranslateTest() { requireIntegers(); + requireNonNumeralVariables(); // CVC4 does not support parsing and therefore no translation. // Princess has a wierd bug // TODO: Look into the Princess problem diff --git a/src/org/sosy_lab/java_smt/test/SolverContextFactoryTest.java b/src/org/sosy_lab/java_smt/test/SolverContextFactoryTest.java index c145b1b181..c42d758cd8 100644 --- a/src/org/sosy_lab/java_smt/test/SolverContextFactoryTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverContextFactoryTest.java @@ -71,7 +71,7 @@ private void requireNativeLibrary() { assume() .withMessage("Solver %s requires to load a native library", solverToUse()) .that(solverToUse()) - .isNoneOf(Solvers.SMTINTERPOL, Solvers.PRINCESS); + .isNoneOf(Solvers.SMTINTERPOL, Solvers.PRINCESS, Solvers.APRON); } /** @@ -86,6 +86,7 @@ private void requireSupportedOperatingSystem() { .withMessage( "Solver %s is not yet supported in the operating system %s", solverToUse(), OS); switch (solverToUse()) { + case APRON: case SMTINTERPOL: case PRINCESS: // any operating system is allowed, Java is already available. diff --git a/src/org/sosy_lab/java_smt/test/SolverContextTest.java b/src/org/sosy_lab/java_smt/test/SolverContextTest.java index e1a5708096..646982a5f5 100644 --- a/src/org/sosy_lab/java_smt/test/SolverContextTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverContextTest.java @@ -27,6 +27,7 @@ public void testMultipleContextClose() { @Test public void testFormulaAccessAfterClose() { + requireNonNumeralVariables(); BooleanFormula term = bmgr.makeVariable("variable"); BooleanFormula term2 = bmgr.makeVariable("variable"); BooleanFormula term3 = bmgr.makeVariable("test"); diff --git a/src/org/sosy_lab/java_smt/test/SolverFormulaIOTest.java b/src/org/sosy_lab/java_smt/test/SolverFormulaIOTest.java index 125a3a568e..71d0099482 100644 --- a/src/org/sosy_lab/java_smt/test/SolverFormulaIOTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverFormulaIOTest.java @@ -99,6 +99,7 @@ public class SolverFormulaIOTest extends SolverBasedTest0.ParameterizedSolverBas @Test public void varDumpTest() { + requireNonNumeralVariables(); // Boolector will fail this anyway since bools are bitvecs for btor TruthJUnit.assume().that(solver).isNotEqualTo(Solvers.BOOLECTOR); BooleanFormula a = bmgr.makeVariable("main::a"); @@ -116,6 +117,7 @@ public void varDumpTest() { @Test public void varDumpTest2() { + requireNonNumeralVariables(); // Boolector will fail this anyway since bools are bitvecs for btor TruthJUnit.assume().that(solver).isNotEqualTo(Solvers.BOOLECTOR); @@ -147,6 +149,7 @@ public void varDumpTest2() { @Test public void valDumpTest() { + requireOr(); // Boolector will fail this anyway since bools are bitvecs for btor TruthJUnit.assume().that(solver).isNotEqualTo(Solvers.BOOLECTOR); BooleanFormula tr1 = bmgr.makeBoolean(true); @@ -167,6 +170,7 @@ public void valDumpTest() { @Test public void intsDumpTest() { requireIntegers(); + requireDumpFormula(); IntegerFormula f1 = imgr.makeVariable("a"); IntegerFormula val = imgr.makeNumber(1); BooleanFormula formula = imgr.equal(f1, val); @@ -198,6 +202,7 @@ public void bvDumpTest() { @Test public void funcsDumpTest() { requireIntegers(); + requireUninterpretedFunctions(); IntegerFormula int1 = imgr.makeNumber(1); IntegerFormula var = imgr.makeVariable("var_a"); FunctionDeclaration funA = @@ -299,6 +304,7 @@ public void parseMathSatTestParseFirst3() throws SolverException, InterruptedExc @Test public void redundancyTest() { + requireNonNumeralVariables(); assume() .withMessage( "Solver %s does not remove redundant sub formulae from formula dump.", solverToUse()) @@ -325,6 +331,7 @@ public void redundancyTest() { @Test public void funDeclareTest() { requireIntegers(); + requireUninterpretedFunctions(); IntegerFormula int1 = imgr.makeNumber(1); IntegerFormula int2 = imgr.makeNumber(2); @@ -347,6 +354,7 @@ public void funDeclareTest() { @Test public void funDeclareTest2() { requireIntegers(); + requireUninterpretedFunctions(); IntegerFormula int1 = imgr.makeNumber(1); IntegerFormula int2 = imgr.makeNumber(2); diff --git a/src/org/sosy_lab/java_smt/test/SolverFormulaWithAssumptionsTest.java b/src/org/sosy_lab/java_smt/test/SolverFormulaWithAssumptionsTest.java index 2bef74b3ef..5f4f8b7c76 100644 --- a/src/org/sosy_lab/java_smt/test/SolverFormulaWithAssumptionsTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverFormulaWithAssumptionsTest.java @@ -176,6 +176,7 @@ public void assumptionsTest() @Test @SuppressWarnings("CheckReturnValue") public void assumptionsTest1() throws SolverException, InterruptedException { + requireNonNumeralVariables(); /* (declare-fun A () Bool) (push 1) diff --git a/src/org/sosy_lab/java_smt/test/SolverStackTest0.java b/src/org/sosy_lab/java_smt/test/SolverStackTest0.java index 94617e98c2..ef910416ce 100644 --- a/src/org/sosy_lab/java_smt/test/SolverStackTest0.java +++ b/src/org/sosy_lab/java_smt/test/SolverStackTest0.java @@ -61,6 +61,7 @@ protected final void requireUfValuesInModel() { @Test public void simpleStackTestBool() throws SolverException, InterruptedException { + requireNonNumeralVariables(); BasicProverEnvironment stack = newEnvironmentForTest(context); int i = index.getFreshId(); @@ -117,6 +118,8 @@ public void simpleStackTestBool() throws SolverException, InterruptedException { @Test public void singleStackTestInteger() throws SolverException, InterruptedException { + // FIXME: Apron can only guarantee for clear results for UNSAT + assume().that(solverToUse()).isNotEqualTo(Solvers.APRON); requireIntegers(); BasicProverEnvironment env = newEnvironmentForTest(context); @@ -125,6 +128,8 @@ public void singleStackTestInteger() throws SolverException, InterruptedExceptio @Test public void singleStackTestRational() throws SolverException, InterruptedException { + // FIXME: Apron can only guarantee for clear results for UNSAT + assume().that(solverToUse()).isNotEqualTo(Solvers.APRON); requireRationals(); requireTheoryCombination(); @@ -228,6 +233,8 @@ public void stackTest4() throws InterruptedException { @Test public void largeStackUsageTest() throws InterruptedException, SolverException { + requireNonNumeralVariables(); + BasicProverEnvironment stack = newEnvironmentForTest(context); for (int i = 0; i < 20; i++) { assertThat(stack.size()).isEqualTo(i); @@ -243,6 +250,8 @@ public void largeStackUsageTest() throws InterruptedException, SolverException { @Test public void largerStackUsageTest() throws InterruptedException, SolverException { + requireNonNumeralVariables(); + int n = 1000; if (ImmutableList.of(Solvers.PRINCESS, Solvers.OPENSMT).contains(solverToUse())) { n = 50; // some solvers are slower, so we use a smaller number @@ -272,6 +281,9 @@ public void stackTest5() throws InterruptedException { @Test public void stackTestUnsat() throws InterruptedException, SolverException { + // FIXME: Apron can only guarantee for clear results for UNSAT + assume().that(solverToUse()).isNotEqualTo(Solvers.APRON); + BasicProverEnvironment stack = newEnvironmentForTest(context, ProverOptions.GENERATE_MODELS); assertThat(stack).isSatisfiable(); stack.push(); @@ -290,6 +302,9 @@ public void stackTestUnsat() throws InterruptedException, SolverException { @Test public void stackTestUnsat2() throws InterruptedException, SolverException { + // FIXME: Apron can only guarantee for clear results for UNSAT + assume().that(solverToUse()).isNotEqualTo(Solvers.APRON); + BasicProverEnvironment stack = newEnvironmentForTest(context, ProverOptions.GENERATE_MODELS); assertThat(stack).isSatisfiable(); stack.push(); @@ -316,6 +331,7 @@ public void stackTestUnsat2() throws InterruptedException, SolverException { @Test public void symbolsOnStackTest() throws InterruptedException, SolverException { requireModel(); + requireNonNumeralVariables(); BasicProverEnvironment stack = newEnvironmentForTest(context, ProverOptions.GENERATE_MODELS); @@ -344,6 +360,7 @@ public void symbolsOnStackTest() throws InterruptedException, SolverException { @Test public void constraintTestBool1() throws SolverException, InterruptedException { + requireNonNumeralVariables(); BooleanFormula a = bmgr.makeVariable("bool_a"); try (BasicProverEnvironment stack = newEnvironmentForTest(context)) { @@ -361,6 +378,7 @@ public void constraintTestBool1() throws SolverException, InterruptedException { @Test public void constraintTestBool2() throws SolverException, InterruptedException { + requireNonNumeralVariables(); BooleanFormula a = bmgr.makeVariable("bool_a"); try (BasicProverEnvironment stack = newEnvironmentForTest(context)) { @@ -378,6 +396,7 @@ public void constraintTestBool2() throws SolverException, InterruptedException { @Test public void constraintTestBool3() throws SolverException, InterruptedException { + requireNonNumeralVariables(); BooleanFormula a = bmgr.makeVariable("bool_a"); try (BasicProverEnvironment stack = newEnvironmentForTest(context)) { @@ -395,6 +414,7 @@ public void constraintTestBool3() throws SolverException, InterruptedException { @Test public void constraintTestBool4() throws SolverException, InterruptedException { + requireNonNumeralVariables(); BasicProverEnvironment stack = newEnvironmentForTest(context); stack.addConstraint(bmgr.makeVariable("bool_a")); assertThat(stack).isSatisfiable(); @@ -412,6 +432,7 @@ public void satTestBool5() throws SolverException, InterruptedException { @Test public void dualStackTest() throws SolverException, InterruptedException { requireMultipleStackSupport(); + requireNonNumeralVariables(); BooleanFormula a = bmgr.makeVariable("bool_a"); BooleanFormula not = bmgr.not(a); @@ -442,6 +463,7 @@ public void dualStackTest() throws SolverException, InterruptedException { @Test public void dualStackTest2() throws SolverException, InterruptedException { requireMultipleStackSupport(); + requireNonNumeralVariables(); BooleanFormula a = bmgr.makeVariable("bool_a"); BooleanFormula not = bmgr.not(a); @@ -469,6 +491,8 @@ public void dualStackTest2() throws SolverException, InterruptedException { @Test public void multiStackTest() throws SolverException, InterruptedException { requireMultipleStackSupport(); + requireNonNumeralVariables(); + int limit = 10; BooleanFormula a = bmgr.makeVariable("bool_a"); @@ -530,6 +554,8 @@ public void avoidDualStacksIfNotSupported() throws InterruptedException { */ @Test public void dualStackGlobalDeclarations() throws SolverException, InterruptedException { + requireNonNumeralVariables(); + // Create non-empty stack BasicProverEnvironment stack1 = newEnvironmentForTest(context); stack1.push(bmgr.makeVariable("bool_a")); @@ -612,6 +638,7 @@ public void modelForSatFormulaWithLargeValue() throws SolverException, Interrupt @Test public void modelForSatFormulaWithUF() throws SolverException, InterruptedException { requireIntegers(); + requireUninterpretedFunctions(); requireTheoryCombination(); try (BasicProverEnvironment stack = @@ -642,6 +669,7 @@ public void modelForSatFormulaWithUF() throws SolverException, InterruptedExcept @Test @SuppressWarnings("resource") public void multiCloseTest() throws SolverException, InterruptedException { + requireNonNumeralVariables(); BasicProverEnvironment stack = newEnvironmentForTest(context, ProverOptions.GENERATE_MODELS); try { // do something on the stack diff --git a/src/org/sosy_lab/java_smt/test/SolverTacticsTest.java b/src/org/sosy_lab/java_smt/test/SolverTacticsTest.java index db5b9841ae..37225313bd 100644 --- a/src/org/sosy_lab/java_smt/test/SolverTacticsTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverTacticsTest.java @@ -134,6 +134,7 @@ public void cnfTacticDefaultTest3() throws SolverException, InterruptedException @Test public void ufEliminationSimpleTest() throws SolverException, InterruptedException { requireIntegers(); + requireUninterpretedFunctions(); // f := uf(v1, v3) XOR uf(v2, v4) IntegerFormula variable1 = imgr.makeVariable("variable1"); IntegerFormula variable2 = imgr.makeVariable("variable2"); @@ -165,6 +166,7 @@ public void ufEliminationSimpleTest() throws SolverException, InterruptedExcepti @Test public void ufEliminationNestedUfsTest() throws SolverException, InterruptedException { requireIntegers(); + requireUninterpretedFunctions(); // f :=uf2(uf1(v1, v2), v3) XOR uf2(uf1(v2, v1), v4) IntegerFormula variable1 = imgr.makeVariable("variable1"); IntegerFormula variable2 = imgr.makeVariable("variable2"); diff --git a/src/org/sosy_lab/java_smt/test/SolverTheoriesTest.java b/src/org/sosy_lab/java_smt/test/SolverTheoriesTest.java index c9dda2adf0..fe020ec693 100644 --- a/src/org/sosy_lab/java_smt/test/SolverTheoriesTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverTheoriesTest.java @@ -40,6 +40,7 @@ public class SolverTheoriesTest extends SolverBasedTest0.ParameterizedSolverBase @Test public void basicBoolTest() throws SolverException, InterruptedException { + requireNonNumeralVariables(); BooleanFormula a = bmgr.makeVariable("a"); BooleanFormula b = bmgr.makeBoolean(false); BooleanFormula c = bmgr.xor(a, b); @@ -222,6 +223,7 @@ private void assertOperation( @Test public void intTest3_DivModLinear() throws SolverException, InterruptedException { requireIntegers(); + requireNot(); IntegerFormula a = imgr.makeVariable("int_a"); IntegerFormula b = imgr.makeVariable("int_b"); @@ -279,6 +281,7 @@ public void intTest3_DivModLinear() throws SolverException, InterruptedException @Test public void intTest3_DivModLinear_zeroDenumerator() throws SolverException, InterruptedException { requireIntegers(); + requireNot(); IntegerFormula a = imgr.makeVariable("int_a"); IntegerFormula num10 = imgr.makeNumber(10); @@ -342,6 +345,7 @@ public void intTest3_DivModNonLinear() throws SolverException, InterruptedExcept // not all solvers support division-by-variable, // we guarantee soundness by allowing any value that yields SAT. requireIntegers(); + requireNot(); IntegerFormula a = imgr.makeVariable("int_a"); IntegerFormula b = imgr.makeVariable("int_b"); @@ -471,6 +475,7 @@ public void intTestBV_DivMod() throws SolverException, InterruptedException { @Test public void intTest4_ModularCongruence_Simple() throws SolverException, InterruptedException { requireIntegers(); + requirePrecision(); final IntegerFormula x = imgr.makeVariable("x"); final BooleanFormula f1 = imgr.modularCongruence(x, imgr.makeNumber(0), 2); final BooleanFormula f2 = imgr.equal(x, imgr.makeNumber(1)); @@ -481,6 +486,7 @@ public void intTest4_ModularCongruence_Simple() throws SolverException, Interrup @Test public void intTest4_ModularCongruence() throws SolverException, InterruptedException { requireIntegers(); + requireNot(); IntegerFormula a = imgr.makeVariable("int_a"); IntegerFormula b = imgr.makeVariable("int_b"); IntegerFormula c = imgr.makeVariable("int_c"); @@ -526,6 +532,7 @@ public void intTest4_ModularCongruence() throws SolverException, InterruptedExce public void intTest4_ModularCongruence_NegativeNumbers() throws SolverException, InterruptedException { requireIntegers(); + requireNot(); IntegerFormula a = imgr.makeVariable("int_a"); IntegerFormula b = imgr.makeVariable("int_b"); IntegerFormula c = imgr.makeVariable("int_c"); @@ -549,6 +556,7 @@ public void intTest4_ModularCongruence_NegativeNumbers() @Test public void testHardCongruence() throws SolverException, InterruptedException { requireIntegers(); + requirePrecision(); IntegerFormula a = imgr.makeVariable("a"); IntegerFormula b = imgr.makeVariable("b"); IntegerFormula c = imgr.makeVariable("c"); @@ -597,6 +605,7 @@ public void realTest() throws SolverException, InterruptedException { @Test public void testUfWithBoolType() throws SolverException, InterruptedException { requireIntegers(); + requireUninterpretedFunctions(); FunctionDeclaration uf = fmgr.declareUF("fun_ib", FormulaType.BooleanType, FormulaType.IntegerType); BooleanFormula uf0 = fmgr.callUF(uf, imgr.makeNumber(0)); @@ -616,6 +625,7 @@ public void testUfWithBoolType() throws SolverException, InterruptedException { @Test public void testUfWithBoolArg() throws SolverException, InterruptedException { + requireUninterpretedFunctions(); assume() .withMessage("Solver %s does not support boolean arguments", solverToUse()) .that(solver) @@ -689,6 +699,7 @@ public void quantifierEliminationTest2() throws SolverException, InterruptedExce @Test public void testGetFormulaType() { requireIntegers(); + requireNonNumeralVariables(); BooleanFormula _boolVar = bmgr.makeVariable("boolVar"); assertThat(mgr.getFormulaType(_boolVar)).isEqualTo(FormulaType.BooleanType); @@ -826,6 +837,7 @@ public void testNestedBitVectorArray() { @Test public void nonLinearMultiplication() throws SolverException, InterruptedException { requireIntegers(); + requirePrecision(); IntegerFormula i2 = imgr.makeNumber(2); IntegerFormula i3 = imgr.makeNumber(3); IntegerFormula i4 = imgr.makeNumber(4); @@ -950,6 +962,7 @@ public void multiplicationSquares() throws SolverException, InterruptedException @Test public void multiplicationFactors() throws SolverException, InterruptedException { requireIntegers(); + requirePrecision(); IntegerFormula i37 = imgr.makeNumber(37); IntegerFormula i1 = imgr.makeNumber(1); IntegerFormula x = imgr.makeVariable("x"); @@ -976,6 +989,7 @@ public void multiplicationFactors() throws SolverException, InterruptedException @Test public void multiplicationCubic() throws SolverException, InterruptedException { requireIntegers(); + requirePrecision(); IntegerFormula i125 = imgr.makeNumber(125); IntegerFormula i27 = imgr.makeNumber(27); IntegerFormula i5 = imgr.makeNumber(5); @@ -1015,6 +1029,7 @@ public void multiplicationCubic() throws SolverException, InterruptedException { @Test public void nonLinearDivision() throws SolverException, InterruptedException { requireIntegers(); + requirePrecision(); IntegerFormula i2 = imgr.makeNumber(2); IntegerFormula i3 = imgr.makeNumber(3); IntegerFormula i4 = imgr.makeNumber(4); @@ -1048,6 +1063,7 @@ public void nonLinearDivision() throws SolverException, InterruptedException { @Test public void integerDivisionRounding() throws SolverException, InterruptedException { requireIntegers(); + requirePrecision(); IntegerFormula varSeven = imgr.makeVariable("a"); IntegerFormula varEight = imgr.makeVariable("b"); @@ -1093,6 +1109,7 @@ public void integerDivisionRounding() throws SolverException, InterruptedExcepti @Test @SuppressWarnings("CheckReturnValue") public void testVariableWithDifferentSort() { + requireNonNumeralVariables(); assume().that(solverToUse()).isNotIn(VAR_TRACKING_SOLVERS); bmgr.makeVariable("x"); if (imgr != null) { @@ -1117,6 +1134,7 @@ public void testFailOnVariableWithDifferentSort() { @Test @SuppressWarnings("CheckReturnValue") public void testVariableAndUFWithDifferentSort() { + requireNonNumeralVariables(); assume().that(solverToUse()).isNotIn(VAR_AND_UF_TRACKING_SOLVERS); bmgr.makeVariable("y"); fmgr.declareUF("y", FormulaType.BooleanType, FormulaType.BooleanType); @@ -1140,6 +1158,8 @@ public void testFailOnUFAndVariableWithDifferentSort() { @Test public void testVariableAndUFWithEqualSort() { + requireNonNumeralVariables(); + requireUninterpretedFunctions(); assume() .withMessage("Solver %s does not support UFs without arguments", solverToUse()) .that(solverToUse()) diff --git a/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java b/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java index 0b8df31836..f92b3ba29d 100644 --- a/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java @@ -65,6 +65,7 @@ public void releaseThreads() { @Test public void allLocalTest() throws InterruptedException, SolverException { requireIntegers(); + requireNonNumeralVariables(); BooleanFormula formula = hardProblem.generate(DEFAULT_PROBLEM_SIZE); @@ -78,6 +79,7 @@ public void allLocalTest() throws InterruptedException, SolverException { public void nonLocalContextTest() throws ExecutionException, InterruptedException, SolverException { requireIntegers(); + requireNonNumeralVariables(); assume().that(solverToUse()).isNotEqualTo(Solvers.CVC5); // generate a new context in another thread, i.e., non-locally @@ -113,6 +115,7 @@ public void nonLocalContextTest() public void nonLocalFormulaTest() throws InterruptedException, SolverException, ExecutionException { requireIntegers(); + requireNonNumeralVariables(); assume().that(solverToUse()).isNotEqualTo(Solvers.CVC5); // generate a new formula in another thread, i.e., non-locally @@ -142,6 +145,7 @@ public void nonLocalFormulaTest() @Test public void nonLocalProverTest() throws InterruptedException, ExecutionException { requireIntegers(); + requireNonNumeralVariables(); assume().that(solverToUse()).isNotEqualTo(Solvers.CVC5); BooleanFormula formula = hardProblem.generate(DEFAULT_PROBLEM_SIZE); @@ -177,6 +181,7 @@ public void nonLocalProverTest() throws InterruptedException, ExecutionException public void nonLocalFormulaTranslationTest() throws Throwable { // Test that even when using translation, the thread local problem persists for CVC5 requireIntegers(); + requireNonNumeralVariables(); BooleanFormula formula = hardProblem.generate(DEFAULT_PROBLEM_SIZE); @@ -339,6 +344,7 @@ public void nonLocalInterpolationTest() throws InterruptedException, Executi @Test public void wrongContextTest() throws InterruptedException, SolverException, InvalidConfigurationException { + requireNonNumeralVariables(); assume() .that(solverToUse()) .isNoneOf( diff --git a/src/org/sosy_lab/java_smt/test/TimeoutTest.java b/src/org/sosy_lab/java_smt/test/TimeoutTest.java index 80af046e9a..d1496a4095 100644 --- a/src/org/sosy_lab/java_smt/test/TimeoutTest.java +++ b/src/org/sosy_lab/java_smt/test/TimeoutTest.java @@ -79,6 +79,7 @@ public void testTacticTimeout() { @Test(timeout = TIMOUT_MILLISECONDS) public void testProverTimeoutInt() throws InterruptedException { requireIntegers(); + requireNonNumeralVariables(); TruthJUnit.assume() .withMessage(solverToUse() + " does not support interruption") .that(solverToUse()) diff --git a/src/org/sosy_lab/java_smt/test/TranslateFormulaTest.java b/src/org/sosy_lab/java_smt/test/TranslateFormulaTest.java index 28d3851267..910b85ac25 100644 --- a/src/org/sosy_lab/java_smt/test/TranslateFormulaTest.java +++ b/src/org/sosy_lab/java_smt/test/TranslateFormulaTest.java @@ -93,14 +93,14 @@ private void requireParserTo() { assume() .withMessage("Solver %s does not support parsing formulae", translateTo) .that(translateTo) - .isNoneOf(Solvers.CVC4, Solvers.BOOLECTOR, Solvers.YICES2, Solvers.CVC5); + .isNoneOf(Solvers.CVC4, Solvers.BOOLECTOR, Solvers.YICES2, Solvers.CVC5, Solvers.APRON); } private void requireParserFrom() { assume() .withMessage("Solver %s does not support parsing formulae", translateFrom) .that(translateFrom) - .isNoneOf(Solvers.CVC4, Solvers.BOOLECTOR, Solvers.YICES2, Solvers.CVC5); + .isNoneOf(Solvers.CVC4, Solvers.BOOLECTOR, Solvers.YICES2, Solvers.CVC5, Solvers.APRON); } private void requireIntegers() { @@ -110,10 +110,17 @@ private void requireIntegers() { .isNotEqualTo(Solvers.BOOLECTOR); } + private void requireOr() { + assume() + .withMessage("Solver %s does not support or()", translateFrom) + .that(translateFrom) + .isNotEqualTo(Solvers.APRON); + } + @Test public void testDumpingAndParsing() throws SolverException, InterruptedException { requireParserTo(); - + requireOr(); BooleanFormula input = createTestFormula(managerFrom); String out = managerFrom.dumpFormula(input).toString(); BooleanFormula parsed = managerTo.parse(out); @@ -124,6 +131,7 @@ public void testDumpingAndParsing() throws SolverException, InterruptedException @Test public void testTranslating() throws SolverException, InterruptedException { requireParserTo(); + requireOr(); BooleanFormula inputFrom = createTestFormula(managerFrom); BooleanFormula inputTo = createTestFormula(managerTo); @@ -134,6 +142,7 @@ public void testTranslating() throws SolverException, InterruptedException { @Test public void testTranslatingForIContextIdentity() throws SolverException, InterruptedException { + requireOr(); assume().that(translateTo).isEqualTo(translateFrom); FormulaManager manager = managerFrom; @@ -146,6 +155,7 @@ public void testTranslatingForIContextIdentity() throws SolverException, Interru @Test public void testTranslatingForContextSibling() throws SolverException, InterruptedException { + requireOr(); assume().that(translateTo).isEqualTo(translateFrom); assume() diff --git a/src/org/sosy_lab/java_smt/test/UFManagerTest.java b/src/org/sosy_lab/java_smt/test/UFManagerTest.java index a14e90d21f..4d92c70563 100644 --- a/src/org/sosy_lab/java_smt/test/UFManagerTest.java +++ b/src/org/sosy_lab/java_smt/test/UFManagerTest.java @@ -32,6 +32,7 @@ public class UFManagerTest extends SolverBasedTest0.ParameterizedSolverBasedTest @Test public void testDeclareAndCallUFWithInt() throws SolverException, InterruptedException { requireIntegers(); + requireUninterpretedFunctions(); IntegerFormula x = imgr.makeVariable("x"); IntegerFormula value = imgr.makeNumber(1234); @@ -57,6 +58,7 @@ public void testDeclareAndCallUFWithInt() throws SolverException, InterruptedExc @Test public void testDeclareAndCallUFWithRational() throws SolverException, InterruptedException { requireRationals(); + requireUninterpretedFunctions(); RationalFormula x = rmgr.makeVariable("x"); RationalFormula value = rmgr.makeNumber(0.5); @@ -91,6 +93,7 @@ public void testDeclareAndCallUFWithIntAndRational() requireIntegers(); requireRationals(); + requireUninterpretedFunctions(); IntegerFormula x = imgr.makeVariable("x"); IntegerFormula value = imgr.makeNumber(1234); @@ -134,6 +137,7 @@ public void testDeclareAndCallUFWithIntAndRational() public void testDeclareAndCallUFWithIncompatibleTypesIntVsRational() { requireIntegers(); requireRationals(); + requireUninterpretedFunctions(); for (String name : VALID_NAMES) { FunctionDeclaration declaration = @@ -154,6 +158,7 @@ public void testDeclareAndCallUFWithIncompatibleTypesIntVsRational() { @Test public void testDeclareAndCallUFWithIncompatibleTypesIntVsBool() { requireIntegers(); + requireUninterpretedFunctions(); for (String name : VALID_NAMES) { FunctionDeclaration declaration = @@ -167,6 +172,7 @@ public void testDeclareAndCallUFWithIncompatibleTypesIntVsBool() { public void testDeclareAndCallUFWithIncompatibleTypesBoolVsInt() { requireIntegers(); requireBooleanArgument(); + requireUninterpretedFunctions(); for (String name : VALID_NAMES) { FunctionDeclaration declaration = @@ -299,6 +305,7 @@ public void testDeclareAndCallUFWithBvWithUnsupportedName() { @Test public void testDeclareAndCallUFWithTypedArgs() { requireBooleanArgument(); + requireUninterpretedFunctions(); createAndCallUF("fooBool1", FormulaType.BooleanType, bmgr.makeTrue()); createAndCallUF("fooBool2", FormulaType.BooleanType, bmgr.makeTrue(), bmgr.makeTrue()); createAndCallUF( @@ -323,6 +330,7 @@ public void testDeclareAndCallUFWithTypedArgs() { @Test public void testDeclareAndCallUFWithRationalArgs() { requireRationals(); + requireUninterpretedFunctions(); createAndCallUF("fooRat1", FormulaType.RationalType, rmgr.makeNumber(2.5)); createAndCallUF("fooRat2", FormulaType.IntegerType, rmgr.makeNumber(1.5), rmgr.makeNumber(2.5)); requireBooleanArgument(); diff --git a/src/org/sosy_lab/java_smt/test/UfEliminationTest.java b/src/org/sosy_lab/java_smt/test/UfEliminationTest.java index c2e40f1d13..c53ab399d9 100644 --- a/src/org/sosy_lab/java_smt/test/UfEliminationTest.java +++ b/src/org/sosy_lab/java_smt/test/UfEliminationTest.java @@ -42,6 +42,7 @@ public void setUp() { @Test public void simpleTest() throws SolverException, InterruptedException { requireIntegers(); + requireUninterpretedFunctions(); // f := uf(v1, v3) XOR uf(v2, v4) IntegerFormula variable1 = imgr.makeVariable("variable1"); @@ -74,6 +75,7 @@ public void simpleTest() throws SolverException, InterruptedException { @Test public void nestedUfs() throws SolverException, InterruptedException { requireIntegers(); + requireUninterpretedFunctions(); // f := uf2(uf1(v1, v2), v3) XOR uf2(uf1(v2, v1), v4) IntegerFormula variable1 = imgr.makeVariable("variable1"); @@ -111,6 +113,7 @@ public void nestedUfs() throws SolverException, InterruptedException { @Test public void nestedUfs2() throws SolverException, InterruptedException { requireIntegers(); + requireUninterpretedFunctions(); // f := uf2(uf1(v1, uf2(v3, v6)), v3) < uf2(uf1(v2, uf2(v4, v5)), v4) IntegerFormula variable1 = imgr.makeVariable("variable1"); @@ -155,6 +158,7 @@ public void nestedUfs2() throws SolverException, InterruptedException { @Test public void nestedUfs3() throws SolverException, InterruptedException { requireIntegers(); + requireUninterpretedFunctions(); // f := uf(v1) < uf(v2) IntegerFormula variable1 = imgr.makeVariable("variable1"); @@ -184,6 +188,7 @@ public void nestedUfs3() throws SolverException, InterruptedException { public void twoFormulasTest() throws SolverException, InterruptedException { // See FormulaManagerTest.testEmptySubstitution(), FormulaManagerTest.testNoSubstitution() requireIntegers(); + requireUninterpretedFunctions(); assume().withMessage("Princess fails").that(solver).isNotEqualTo(Solvers.PRINCESS); // f := uf(v1, v3) XOR uf(v2, v4) @@ -248,6 +253,7 @@ public void quantifierTest() { @Test public void substitutionTest() throws SolverException, InterruptedException { requireIntegers(); + requireUninterpretedFunctions(); // f := uf(v1, v3) \/ NOT(uf(v2, v4))) IntegerFormula variable1 = imgr.makeVariable("variable1"); diff --git a/src/org/sosy_lab/java_smt/test/VariableNamesTest.java b/src/org/sosy_lab/java_smt/test/VariableNamesTest.java index b743f74fcf..2bbc50b468 100644 --- a/src/org/sosy_lab/java_smt/test/VariableNamesTest.java +++ b/src/org/sosy_lab/java_smt/test/VariableNamesTest.java @@ -253,6 +253,7 @@ private void testName0( @Test public void testBoolVariable() { + requireNonNumeralVariables(); for (String name : getAllNames()) { createVariableWith(bmgr::makeVariable, name); } @@ -555,6 +556,7 @@ public Void visitAtom(BooleanFormula pAtom, FunctionDeclaration @Test public void testBoolVariableDump() { + requireNonNumeralVariables(); for (String name : getAllNames()) { BooleanFormula var = createVariableWith(bmgr::makeVariable, name); if (var != null) { @@ -566,6 +568,7 @@ public void testBoolVariableDump() { @Test public void testEqBoolVariableDump() { + requireNonNumeralVariables(); for (String name : getAllNames()) { BooleanFormula var = createVariableWith(bmgr::makeVariable, name); if (var != null) {