diff --git a/.appveyor.yml b/.appveyor.yml index 61f66ffb8b..797eb36576 100644 --- a/.appveyor.yml +++ b/.appveyor.yml @@ -44,6 +44,7 @@ build_script: Copy-Item -Path "lib\java\runtime-z3\x64\*.dll" -Destination "lib\native\x86_64-windows\" -Force Copy-Item -Path "lib\java\runtime-mathsat\x64\*.dll" -Destination "lib\native\x86_64-windows\" -Force Copy-Item -Path "lib\java\runtime-bitwuzla\x64\*.dll" -Destination "lib\native\x86_64-windows\" -Force + Copy-Item -Path "lib\java\runtime-cvc5\x64\*.dll" -Destination "lib\native\x86_64-windows\" -Force test_script: - ant unit-tests diff --git a/README.md b/README.md index a59a31dcf6..15727b8379 100644 --- a/README.md +++ b/README.md @@ -65,7 +65,7 @@ JavaSMT supports several SMT solvers (see [Getting Started](doc/Getting-started. | [Bitwuzla](https://bitwuzla.github.io/) | :heavy_check_mark:² | :heavy_check_mark:² | :heavy_check_mark: | | | | a fast solver for bitvector logic | | [Boolector](https://boolector.github.io/) | :heavy_check_mark: | | | | | | a fast solver for bitvector logic, misses formula introspection, deprecated | | [CVC4](https://cvc4.github.io/) | :heavy_check_mark: | | | | | | | -| [CVC5](https://cvc5.github.io/) | :heavy_check_mark: | | | | | | | +| [CVC5](https://cvc5.github.io/) | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | | | | | | [MathSAT5](http://mathsat.fbk.eu/) | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | | [maybe](https://github.com/sosy-lab/java-smt/pull/430)³ | | | | [OpenSMT](https://verify.inf.usi.ch/opensmt) | :heavy_check_mark:² | :heavy_check_mark:² | | | | | | | [OptiMathSAT](http://optimathsat.disi.unitn.it/) | :heavy_check_mark: | | | | | | based on MathSAT5, with support for optimization queries | diff --git a/build/build-maven-publish.xml b/build/build-maven-publish.xml index 73204abef6..a7ea814d3b 100644 --- a/build/build-maven-publish.xml +++ b/build/build-maven-publish.xml @@ -229,15 +229,15 @@ SPDX-License-Identifier: Apache-2.0 + + - - - - - + + + - + + - - - - - Please specify the path to CVC5 with the flag -Dcvc5.path=/path/to/cvc5. - The path has to point to the root CVC5 folder, i.e., - a checkout of the official git repository from 'https://github.com/cvc5/cvc5'. - Note that shell substitutions do not work and a full absolute path has to be specified. - + + Please specify a custom revision with the flag -Dcvc5.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. + + @@ -51,96 +44,105 @@ SPDX-License-Identifier: Apache-2.0 - - - - - - + + + + + + + - + + + - + + - - - + - - + + + - - - - - + + + - - - - - - - - - - - - - - - - - - - + + + + + + + + + + + - - + + + - - + + + - - - - - - - - - - - - - - - - - + + + + + + + + + + + - - - - - + + + - - - + + - - - + + + + + + + + + + + + + + - - + description="Publish CVC5 binaries to Ivy repository."> + + + + + + + + + diff --git a/doc/Developers-How-to-Release-into-Ivy.md b/doc/Developers-How-to-Release-into-Ivy.md index 216bc1406f..e10ec75c24 100644 --- a/doc/Developers-How-to-Release-into-Ivy.md +++ b/doc/Developers-How-to-Release-into-Ivy.md @@ -114,23 +114,36 @@ ant publish-z3 -Dz3.path=$Z3_DIR/build ``` Finally follow the instructions shown in the message at the end. - -### Publishing CVC5 (previously CVC4) +### Publishing CVC5 We prefer to compile our own CVC5 binaries and Java bindings. For simple usage, we provide a Docker definition/environment under `/docker`, in which the following command can be run. -To publish CVC5, checkout the [CVC5 repository](https://github.com/cvc5/cvc5). -Then execute the following command in the JavaSMT directory, -where `$CVC5_DIR` is the path to the CVC5 directory and `$CVC5_VERSION` is the version number: +To publish CVC5, checkout the [CVC5 repository](https://github.com/cvc5/cvc5) and download the +JDK for windows and arm64 from Oracle. We will build bindings for several platforms and +the JDKs are needed to cross-compile. To start building, execute the following command +in the JavaSMT directory, where `$CVC5_DIR` is the path to the CVC5 directory and +`$CVC5_VERSION` is the version number: + ``` -ant publish-cvc5 -Dcvc5.path=$CVC5_DIR -Dcvc5.customRev=$CVC5_VERSION +ant publish-cvc5 \ + -Dcvc5.path=$CVC5_DIR\ + -Dcvc5.customRev=$CVC5_VERSION \ + -Djdk-windows.path=$JDK_DIR_WINDOWS \ + -Djdk-linux-arm64.path=$JDK_DIR_LINUX_ARM64 ``` + Example: + ``` -ant publish-cvc5 -Dcvc5.path=../CVC5 -Dcvc5.customRev=1.0.1 +ant publish-cvc5 \ + -Dcvc5.path=../CVC5 \ + -Dcvc5.customRev=1.2.1 \ + -Djdk-windows-x64.path=/workspace/solvers/jdk/openjdk-17.0.2_windows-x64_bin/jdk-17.0.2/ \ + -Djdk-linux-arm64.path=/workspace/solvers/jdk/openjdk-17.0.2_linux-aarch64_bin/jdk-17.0.2/ ``` + During the build process, our script automatically appends the git-revision after the version. Finally, follow the instructions shown in the message at the end. diff --git a/docker/ubuntu1804.Dockerfile b/docker/ubuntu1804.Dockerfile index 4d34173420..af3a8999a8 100644 --- a/docker/ubuntu1804.Dockerfile +++ b/docker/ubuntu1804.Dockerfile @@ -28,7 +28,7 @@ RUN apt-get update \ && apt-get clean # Yices2 requires some dependencies -RUN apt-get update \ +RUN apt-get update \ && apt-get install -y \ autoconf gperf \ && apt-get clean @@ -36,7 +36,7 @@ RUN apt-get update \ # CVC5 requires some dependencies RUN apt-get update \ && apt-get install -y \ - python3 python3-toml python3-pyparsing flex libssl-dev \ + python3 python3-venv python3-toml python3-pyparsing flex libssl-dev cmake \ && apt-get clean \ && wget https://github.com/Kitware/CMake/releases/download/v3.26.3/cmake-3.26.3.tar.gz \ && tar -zxvf cmake-3.26.3.tar.gz \ diff --git a/docker/ubuntu2204.Dockerfile b/docker/ubuntu2204.Dockerfile index 5f9f003e91..39e3c84e91 100644 --- a/docker/ubuntu2204.Dockerfile +++ b/docker/ubuntu2204.Dockerfile @@ -37,7 +37,7 @@ RUN apt-get update \ # CVC5 requires some dependencies RUN apt-get update \ && apt-get install -y \ - python3 python3-toml python3-pyparsing flex libssl-dev cmake \ + python3 python3-venv python3-toml python3-pyparsing flex libssl-dev cmake \ && apt-get clean # Bitwuzla requires Ninja and Meson (updated version from pip), and uses SWIG >4.0 from dependencies. diff --git a/lib/ivy.xml b/lib/ivy.xml index 9bc2230cb6..53a5b2b9e5 100644 --- a/lib/ivy.xml +++ b/lib/ivy.xml @@ -45,7 +45,9 @@ SPDX-License-Identifier: Apache-2.0 - + + + @@ -66,10 +68,10 @@ SPDX-License-Identifier: Apache-2.0 @@ -191,7 +193,7 @@ SPDX-License-Identifier: Apache-2.0 - + diff --git a/lib/native/arm64-linux/libcvc5jni.so b/lib/native/arm64-linux/libcvc5jni.so new file mode 120000 index 0000000000..d79d2b02a3 --- /dev/null +++ b/lib/native/arm64-linux/libcvc5jni.so @@ -0,0 +1 @@ +../../java/runtime-cvc5/arm64/libcvc5jni.so \ No newline at end of file diff --git a/lib/native/x86_64-linux/libcvc5.so b/lib/native/x86_64-linux/libcvc5.so deleted file mode 120000 index d6d1b10eb4..0000000000 --- a/lib/native/x86_64-linux/libcvc5.so +++ /dev/null @@ -1 +0,0 @@ -../../java/runtime-cvc5/libcvc5.so \ No newline at end of file diff --git a/lib/native/x86_64-linux/libcvc5jni.so b/lib/native/x86_64-linux/libcvc5jni.so index cb3baddc07..619731b58a 120000 --- a/lib/native/x86_64-linux/libcvc5jni.so +++ b/lib/native/x86_64-linux/libcvc5jni.so @@ -1 +1 @@ -../../java/runtime-cvc5/libcvc5jni.so \ No newline at end of file +../../java/runtime-cvc5/x64/libcvc5jni.so \ No newline at end of file diff --git a/lib/native/x86_64-linux/libcvc5parser.so b/lib/native/x86_64-linux/libcvc5parser.so deleted file mode 120000 index 5fd14c4069..0000000000 --- a/lib/native/x86_64-linux/libcvc5parser.so +++ /dev/null @@ -1 +0,0 @@ -../../java/runtime-cvc5/libcvc5parser.so \ No newline at end of file diff --git a/lib/native/x86_64-linux/libpoly.so b/lib/native/x86_64-linux/libpoly.so deleted file mode 120000 index 4e31a33a6f..0000000000 --- a/lib/native/x86_64-linux/libpoly.so +++ /dev/null @@ -1 +0,0 @@ -../../java/runtime-cvc5/libpoly.so \ No newline at end of file diff --git a/lib/native/x86_64-linux/libpolyxx.so b/lib/native/x86_64-linux/libpolyxx.so deleted file mode 120000 index a88ab9fe61..0000000000 --- a/lib/native/x86_64-linux/libpolyxx.so +++ /dev/null @@ -1 +0,0 @@ -../../java/runtime-cvc5/libpolyxx.so \ No newline at end of file diff --git a/lib/native/x86_64-windows/README.md b/lib/native/x86_64-windows/README.md index 036078c8a0..7b582a1bea 100644 --- a/lib/native/x86_64-windows/README.md +++ b/lib/native/x86_64-windows/README.md @@ -39,6 +39,10 @@ For MathSAT5: For Bitwuzla: - `mklink libbitwuzlaj.dll ..\..\java\runtime-bitwuzla\x64\libbitwuzlaj.dll` +For CVC5: + +- `mlink libcvc5jni.dll ..\..\java\runtime-cvc5\x64\libcvcjni.so` + ### With a direct copy of the library: An alternative simple solution (without the need of administrator rights) is to copy over @@ -57,6 +61,10 @@ For MathSAT5: For Bitwuzla: - `copy ..\..\java\runtime-bitwuzla\x64\libbitwuzlaj.dll libbitwuzlaj.dll` +For CVC5: + +- `copy ..\..\java\runtime-cvc5\x64\libcvc5jni.dll libcvc5jni.dll` + Or simply use a wildcard: - `copy ..\..\java\runtime-*\*dll .\` - `copy ..\..\java\runtime-*\x64\*dll .\` diff --git a/solvers_ivy_conf/ivy_cvc5.xml b/solvers_ivy_conf/ivy_cvc5.xml index 5d2c0ff45e..4fd3be303d 100644 --- a/solvers_ivy_conf/ivy_cvc5.xml +++ b/solvers_ivy_conf/ivy_cvc5.xml @@ -11,9 +11,9 @@ SPDX-License-Identifier: Apache-2.0 --> + xmlns:e="http://ant.apache.org/ivy/extra" + xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" + xsi:noNamespaceSchemaLocation="http://ant.apache.org/ivy/schemas/ivy.xsd"> @@ -23,16 +23,27 @@ SPDX-License-Identifier: Apache-2.0 - + + + + + + + + + + + + + - - - - - - + + + + + diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5AbstractProver.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5AbstractProver.java index d2292667c1..85cfb0a23c 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5AbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5AbstractProver.java @@ -14,16 +14,17 @@ import com.google.common.collect.ImmutableMap; import com.google.errorprone.annotations.CanIgnoreReturnValue; import io.github.cvc5.CVC5ApiException; +import io.github.cvc5.CVC5ApiRecoverableException; import io.github.cvc5.Result; import io.github.cvc5.Solver; import io.github.cvc5.Term; +import io.github.cvc5.TermManager; import io.github.cvc5.UnknownExplanation; import java.util.ArrayDeque; import java.util.ArrayList; import java.util.Collection; import java.util.Deque; import java.util.List; -import java.util.Map.Entry; import java.util.Optional; import java.util.Set; import org.sosy_lab.common.ShutdownNotifier; @@ -63,9 +64,11 @@ protected CVC5AbstractProver( mgr = pMgr; creator = pFormulaCreator; incremental = !enableSL; - solver = new Solver(); assertedTerms.add(PathCopyingPersistentTreeMap.of()); + TermManager termManager = creator.getEnv(); + solver = new Solver(termManager); + setSolverOptions(randomSeed, pOptions, pFurtherOptionsMap, solver); } @@ -74,6 +77,13 @@ protected void setSolverOptions( Set pOptions, ImmutableMap pFurtherOptionsMap, Solver pSolver) { + try { + CVC5SolverContext.setSolverOptions(pSolver, randomSeed, pFurtherOptionsMap); + } catch (CVC5ApiRecoverableException e) { + // We've already used these options in CVC5SolverContext, so there should be no exception + throw new AssertionError("Unexpected exception", e); + } + if (incremental) { pSolver.setOption("incremental", "true"); } @@ -85,18 +95,16 @@ protected void setSolverOptions( } pSolver.setOption("produce-assertions", "true"); pSolver.setOption("dump-models", "true"); - pSolver.setOption("output-language", "smt2"); - pSolver.setOption("seed", String.valueOf(randomSeed)); // Set Strings option to enable all String features (such as lessOrEquals) pSolver.setOption("strings-exp", "true"); + // Enable experimental array features + // Needed when array constants (= with default element) are used + pSolver.setOption("arrays-exp", "true"); + // Enable more complete quantifier solving (for more info see CVC5QuantifiedFormulaManager) pSolver.setOption("full-saturate-quant", "true"); - - for (Entry option : pFurtherOptionsMap.entrySet()) { - pSolver.setOption(option.getKey(), option.getValue()); - } } @Override diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5ArrayFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5ArrayFormulaManager.java index 7363f46c90..03fdc21a45 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5ArrayFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5ArrayFormulaManager.java @@ -9,31 +9,32 @@ package org.sosy_lab.java_smt.solvers.cvc5; import io.github.cvc5.Kind; -import io.github.cvc5.Solver; import io.github.cvc5.Sort; import io.github.cvc5.Term; +import io.github.cvc5.TermManager; import org.sosy_lab.java_smt.api.Formula; import org.sosy_lab.java_smt.api.FormulaType; import org.sosy_lab.java_smt.basicimpl.AbstractArrayFormulaManager; @SuppressWarnings("MethodTypeParameterName") -public class CVC5ArrayFormulaManager extends AbstractArrayFormulaManager { +public class CVC5ArrayFormulaManager + extends AbstractArrayFormulaManager { - private final Solver solver; + private final TermManager termManager; public CVC5ArrayFormulaManager(CVC5FormulaCreator pFormulaCreator) { super(pFormulaCreator); - solver = pFormulaCreator.getEnv(); + termManager = pFormulaCreator.getEnv(); } @Override protected Term select(Term pArray, Term pIndex) { - return solver.mkTerm(Kind.SELECT, pArray, pIndex); + return termManager.mkTerm(Kind.SELECT, pArray, pIndex); } @Override protected Term store(Term pArray, Term pIndex, Term pValue) { - return solver.mkTerm(Kind.STORE, pArray, pIndex, pValue); + return termManager.mkTerm(Kind.STORE, pArray, pIndex, pValue); } @Override @@ -48,11 +49,11 @@ protected Term internalMakeArray( protected Term internalMakeArray( FormulaType pIndexType, FormulaType pElementType, Term defaultElement) { final Sort cvc5ArrayType = toSolverType(FormulaType.getArrayType(pIndexType, pElementType)); - return solver.mkConstArray(cvc5ArrayType, defaultElement); + return termManager.mkConstArray(cvc5ArrayType, defaultElement); } @Override protected Term equivalence(Term pArray1, Term pArray2) { - return solver.mkTerm(Kind.EQUAL, pArray1, pArray2); + return termManager.mkTerm(Kind.EQUAL, pArray1, pArray2); } } diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5BitvectorFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5BitvectorFormulaManager.java index 16976695a1..83a9fae343 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5BitvectorFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5BitvectorFormulaManager.java @@ -11,27 +11,27 @@ import io.github.cvc5.CVC5ApiException; import io.github.cvc5.Kind; import io.github.cvc5.Op; -import io.github.cvc5.Solver; import io.github.cvc5.Sort; import io.github.cvc5.Term; +import io.github.cvc5.TermManager; import java.math.BigInteger; import java.util.List; import org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager; public class CVC5BitvectorFormulaManager - extends AbstractBitvectorFormulaManager { + extends AbstractBitvectorFormulaManager { - private final Solver solver; + private final TermManager termManager; protected CVC5BitvectorFormulaManager( CVC5FormulaCreator pCreator, CVC5BooleanFormulaManager pBmgr) { super(pCreator, pBmgr); - solver = pCreator.getEnv(); + termManager = pCreator.getEnv(); } @Override protected Term concat(Term pParam1, Term pParam2) { - return solver.mkTerm(Kind.BITVECTOR_CONCAT, pParam1, pParam2); + return termManager.mkTerm(Kind.BITVECTOR_CONCAT, pParam1, pParam2); } @Override @@ -39,11 +39,11 @@ protected Term extract(Term pParam1, int pMsb, int pLsb) { Op ext; try { if (pMsb < pLsb || pMsb >= pParam1.getSort().getBitVectorSize() || pLsb < 0 || pMsb < 0) { - ext = solver.mkOp(Kind.BITVECTOR_EXTRACT, 0, 0); + ext = termManager.mkOp(Kind.BITVECTOR_EXTRACT, 0, 0); } else { - ext = solver.mkOp(Kind.BITVECTOR_EXTRACT, pMsb, pLsb); + ext = termManager.mkOp(Kind.BITVECTOR_EXTRACT, pMsb, pLsb); } - return solver.mkTerm(ext, pParam1); + return termManager.mkTerm(ext, pParam1); } catch (CVC5ApiException e) { throw new IllegalArgumentException( "You tried creating a invalid bitvector extract from bit " @@ -62,11 +62,11 @@ protected Term extend(Term pParam1, int pExtensionBits, boolean signed) { final Op op; try { if (signed) { - op = solver.mkOp(Kind.BITVECTOR_SIGN_EXTEND, pExtensionBits); + op = termManager.mkOp(Kind.BITVECTOR_SIGN_EXTEND, pExtensionBits); } else { - op = solver.mkOp(Kind.BITVECTOR_ZERO_EXTEND, pExtensionBits); + op = termManager.mkOp(Kind.BITVECTOR_ZERO_EXTEND, pExtensionBits); } - return solver.mkTerm(op, pParam1); + return termManager.mkTerm(op, pParam1); } catch (CVC5ApiException e) { throw new IllegalArgumentException( "You tried creating a invalid bitvector extend with term " @@ -83,7 +83,7 @@ protected Term makeBitvectorImpl(int pLength, BigInteger pI) { pI = transformValueToRange(pLength, pI); try { // Use String conversion as it can hold more values - return solver.mkBitVector(pLength, pI.toString(), 10); + return termManager.mkBitVector(pLength, pI.toString(), 10); } catch (CVC5ApiException e) { throw new IllegalArgumentException( "You tried creating a invalid bitvector with length " @@ -98,7 +98,7 @@ protected Term makeBitvectorImpl(int pLength, BigInteger pI) { @Override protected Term makeVariableImpl(int length, String varName) { try { - Sort type = solver.mkBitVectorSort(length); + Sort type = termManager.mkBitVectorSort(length); return getFormulaCreator().makeVariable(type, varName); } catch (CVC5ApiException e) { throw new IllegalArgumentException( @@ -114,22 +114,22 @@ protected Term makeVariableImpl(int length, String varName) { @Override protected Term shiftRight(Term pParam1, Term pParam2, boolean signed) { if (signed) { - return solver.mkTerm(Kind.BITVECTOR_ASHR, pParam1, pParam2); + return termManager.mkTerm(Kind.BITVECTOR_ASHR, pParam1, pParam2); } else { - return solver.mkTerm(Kind.BITVECTOR_LSHR, pParam1, pParam2); + return termManager.mkTerm(Kind.BITVECTOR_LSHR, pParam1, pParam2); } } @Override protected Term shiftLeft(Term pParam1, Term pParam2) { - return solver.mkTerm(Kind.BITVECTOR_SHL, pParam1, pParam2); + return termManager.mkTerm(Kind.BITVECTOR_SHL, pParam1, pParam2); } @Override protected Term rotateLeftByConstant(Term pNumber, int pToRotate) { try { - Op op = solver.mkOp(Kind.BITVECTOR_ROTATE_LEFT, pToRotate); - return solver.mkTerm(op, pNumber); + Op op = termManager.mkOp(Kind.BITVECTOR_ROTATE_LEFT, pToRotate); + return termManager.mkTerm(op, pNumber); } catch (CVC5ApiException e) { throw new IllegalArgumentException( String.format("You tried rotation a bitvector %s with shift %d", pNumber, pToRotate), e); @@ -139,8 +139,8 @@ protected Term rotateLeftByConstant(Term pNumber, int pToRotate) { @Override protected Term rotateRightByConstant(Term pNumber, int pToRotate) { try { - Op op = solver.mkOp(Kind.BITVECTOR_ROTATE_RIGHT, pToRotate); - return solver.mkTerm(op, pNumber); + Op op = termManager.mkOp(Kind.BITVECTOR_ROTATE_RIGHT, pToRotate); + return termManager.mkTerm(op, pNumber); } catch (CVC5ApiException e) { throw new IllegalArgumentException( String.format("You tried rotation a bitvector %s with shift %d", pNumber, pToRotate), e); @@ -149,113 +149,113 @@ protected Term rotateRightByConstant(Term pNumber, int pToRotate) { @Override protected Term not(Term pParam1) { - return solver.mkTerm(Kind.BITVECTOR_NOT, pParam1); + return termManager.mkTerm(Kind.BITVECTOR_NOT, pParam1); } @Override protected Term and(Term pParam1, Term pParam2) { - return solver.mkTerm(Kind.BITVECTOR_AND, pParam1, pParam2); + return termManager.mkTerm(Kind.BITVECTOR_AND, pParam1, pParam2); } @Override protected Term or(Term pParam1, Term pParam2) { - return solver.mkTerm(Kind.BITVECTOR_OR, pParam1, pParam2); + return termManager.mkTerm(Kind.BITVECTOR_OR, pParam1, pParam2); } @Override protected Term xor(Term pParam1, Term pParam2) { - return solver.mkTerm(Kind.BITVECTOR_XOR, pParam1, pParam2); + return termManager.mkTerm(Kind.BITVECTOR_XOR, pParam1, pParam2); } @Override protected Term negate(Term pParam1) { - return solver.mkTerm(Kind.BITVECTOR_NEG, pParam1); + return termManager.mkTerm(Kind.BITVECTOR_NEG, pParam1); } @Override protected Term add(Term pParam1, Term pParam2) { - return solver.mkTerm(Kind.BITVECTOR_ADD, pParam1, pParam2); + return termManager.mkTerm(Kind.BITVECTOR_ADD, pParam1, pParam2); } @Override protected Term subtract(Term pParam1, Term pParam2) { - return solver.mkTerm(Kind.BITVECTOR_SUB, pParam1, pParam2); + return termManager.mkTerm(Kind.BITVECTOR_SUB, pParam1, pParam2); } @Override protected Term divide(Term pParam1, Term pParam2, boolean signed) { if (signed) { - return solver.mkTerm(Kind.BITVECTOR_SDIV, pParam1, pParam2); + return termManager.mkTerm(Kind.BITVECTOR_SDIV, pParam1, pParam2); } else { - return solver.mkTerm(Kind.BITVECTOR_UDIV, pParam1, pParam2); + return termManager.mkTerm(Kind.BITVECTOR_UDIV, pParam1, pParam2); } } @Override protected Term remainder(Term pParam1, Term pParam2, boolean signed) { if (signed) { - return solver.mkTerm(Kind.BITVECTOR_SREM, pParam1, pParam2); + return termManager.mkTerm(Kind.BITVECTOR_SREM, pParam1, pParam2); } else { - return solver.mkTerm(Kind.BITVECTOR_UREM, pParam1, pParam2); + return termManager.mkTerm(Kind.BITVECTOR_UREM, pParam1, pParam2); } } @Override protected Term smodulo(Term pParam1, Term pParam2) { - return solver.mkTerm(Kind.BITVECTOR_SMOD, pParam1, pParam2); + return termManager.mkTerm(Kind.BITVECTOR_SMOD, pParam1, pParam2); } @Override protected Term multiply(Term pParam1, Term pParam2) { - return solver.mkTerm(Kind.BITVECTOR_MULT, pParam1, pParam2); + return termManager.mkTerm(Kind.BITVECTOR_MULT, pParam1, pParam2); } @Override protected Term equal(Term pParam1, Term pParam2) { - return solver.mkTerm(Kind.EQUAL, pParam1, pParam2); + return termManager.mkTerm(Kind.EQUAL, pParam1, pParam2); } @Override protected Term lessThan(Term pParam1, Term pParam2, boolean signed) { if (signed) { - return solver.mkTerm(Kind.BITVECTOR_SLT, pParam1, pParam2); + return termManager.mkTerm(Kind.BITVECTOR_SLT, pParam1, pParam2); } else { - return solver.mkTerm(Kind.BITVECTOR_ULT, pParam1, pParam2); + return termManager.mkTerm(Kind.BITVECTOR_ULT, pParam1, pParam2); } } @Override protected Term lessOrEquals(Term pParam1, Term pParam2, boolean signed) { if (signed) { - return solver.mkTerm(Kind.BITVECTOR_SLE, pParam1, pParam2); + return termManager.mkTerm(Kind.BITVECTOR_SLE, pParam1, pParam2); } else { - return solver.mkTerm(Kind.BITVECTOR_ULE, pParam1, pParam2); + return termManager.mkTerm(Kind.BITVECTOR_ULE, pParam1, pParam2); } } @Override protected Term greaterThan(Term pParam1, Term pParam2, boolean signed) { if (signed) { - return solver.mkTerm(Kind.BITVECTOR_SGT, pParam1, pParam2); + return termManager.mkTerm(Kind.BITVECTOR_SGT, pParam1, pParam2); } else { - return solver.mkTerm(Kind.BITVECTOR_UGT, pParam1, pParam2); + return termManager.mkTerm(Kind.BITVECTOR_UGT, pParam1, pParam2); } } @Override protected Term greaterOrEquals(Term pParam1, Term pParam2, boolean signed) { if (signed) { - return solver.mkTerm(Kind.BITVECTOR_SGE, pParam1, pParam2); + return termManager.mkTerm(Kind.BITVECTOR_SGE, pParam1, pParam2); } else { - return solver.mkTerm(Kind.BITVECTOR_UGE, pParam1, pParam2); + return termManager.mkTerm(Kind.BITVECTOR_UGE, pParam1, pParam2); } } @Override protected Term makeBitvectorImpl(int pLength, Term pParam1) { try { - Op length = solver.mkOp(Kind.INT_TO_BITVECTOR, pLength); - return solver.mkTerm(length, pParam1); + Op length = termManager.mkOp(Kind.INT_TO_BITVECTOR, pLength); + return termManager.mkTerm(length, pParam1); } catch (CVC5ApiException e) { throw new IllegalArgumentException( "You tried creating a invalid bitvector out of a integer term " @@ -269,7 +269,7 @@ protected Term makeBitvectorImpl(int pLength, Term pParam1) { @Override protected Term toIntegerFormulaImpl(Term pBv, boolean pSigned) { - Term intExpr = solver.mkTerm(Kind.BITVECTOR_TO_NAT, pBv); + Term intExpr = termManager.mkTerm(Kind.BITVECTOR_TO_NAT, pBv); // CVC5 returns unsigned int by default if (pSigned && pBv.getSort().isBitVector()) { @@ -280,14 +280,14 @@ protected Term toIntegerFormulaImpl(Term pBv, boolean pSigned) { final int size = Math.toIntExact(pBv.getSort().getBitVectorSize()); final BigInteger modulo = BigInteger.ONE.shiftLeft(size); final BigInteger maxInt = BigInteger.ONE.shiftLeft(size - 1).subtract(BigInteger.ONE); - final Term moduloExpr = solver.mkInteger(modulo.longValue()); - final Term maxIntExpr = solver.mkInteger(maxInt.longValue()); + final Term moduloExpr = termManager.mkInteger(modulo.longValue()); + final Term maxIntExpr = termManager.mkInteger(maxInt.longValue()); intExpr = - solver.mkTerm( + termManager.mkTerm( Kind.ITE, - solver.mkTerm(Kind.GT, intExpr, maxIntExpr), - solver.mkTerm(Kind.SUB, intExpr, moduloExpr), + termManager.mkTerm(Kind.GT, intExpr, maxIntExpr), + termManager.mkTerm(Kind.SUB, intExpr, moduloExpr), intExpr); } @@ -296,6 +296,6 @@ protected Term toIntegerFormulaImpl(Term pBv, boolean pSigned) { @Override protected Term distinctImpl(List pParam) { - return solver.mkTerm(Kind.DISTINCT, pParam.toArray(new Term[0])); + return termManager.mkTerm(Kind.DISTINCT, pParam.toArray(new Term[0])); } } diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5BooleanFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5BooleanFormulaManager.java index 25cc18a660..5afd964c27 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5BooleanFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5BooleanFormulaManager.java @@ -12,26 +12,26 @@ import com.google.common.collect.Iterables; import io.github.cvc5.CVC5ApiException; import io.github.cvc5.Kind; -import io.github.cvc5.Solver; import io.github.cvc5.Sort; import io.github.cvc5.Term; +import io.github.cvc5.TermManager; import java.util.Collection; import java.util.LinkedHashSet; import java.util.Set; import org.sosy_lab.java_smt.basicimpl.AbstractBooleanFormulaManager; public class CVC5BooleanFormulaManager - extends AbstractBooleanFormulaManager { + extends AbstractBooleanFormulaManager { - private final Solver solver; + private final TermManager termManager; private final Term pTrue; private final Term pFalse; protected CVC5BooleanFormulaManager(CVC5FormulaCreator pCreator) { super(pCreator); - solver = pCreator.getEnv(); - pTrue = solver.mkBoolean(true); - pFalse = solver.mkBoolean(false); + termManager = pCreator.getEnv(); + pTrue = termManager.mkBoolean(true); + pFalse = termManager.mkBoolean(false); } @Override @@ -58,7 +58,7 @@ protected Term not(Term pParam1) { } catch (CVC5ApiException e) { throw new IllegalArgumentException("Failure when negating the term '" + pParam1 + "'.", e); } - return solver.mkTerm(Kind.NOT, pParam1); + return termManager.mkTerm(Kind.NOT, pParam1); } @Override @@ -74,7 +74,7 @@ protected Term and(Term pParam1, Term pParam2) { } else if (pParam1.equals(pParam2)) { return pParam1; } - return solver.mkTerm(Kind.AND, pParam1, pParam2); + return termManager.mkTerm(Kind.AND, pParam1, pParam2); } @Override @@ -96,7 +96,7 @@ protected Term andImpl(Collection pParams) { case 1: return Iterables.getOnlyElement(operands); default: - return solver.mkTerm(Kind.AND, operands.toArray(new Term[0])); + return termManager.mkTerm(Kind.AND, operands.toArray(new Term[0])); } } @@ -113,7 +113,7 @@ protected Term or(Term pParam1, Term pParam2) { } else if (pParam1.equals(pParam2)) { return pParam1; } - return solver.mkTerm(Kind.OR, pParam1, pParam2); + return termManager.mkTerm(Kind.OR, pParam1, pParam2); } @Override @@ -135,23 +135,23 @@ protected Term orImpl(Collection pParams) { case 1: return Iterables.getOnlyElement(operands); default: - return solver.mkTerm(Kind.OR, operands.toArray(new Term[0])); + return termManager.mkTerm(Kind.OR, operands.toArray(new Term[0])); } } @Override protected Term xor(Term pParam1, Term pParam2) { - return solver.mkTerm(Kind.XOR, pParam1, pParam2); + return termManager.mkTerm(Kind.XOR, pParam1, pParam2); } @Override protected Term equivalence(Term pBits1, Term pBits2) { - return solver.mkTerm(Kind.EQUAL, pBits1, pBits2); + return termManager.mkTerm(Kind.EQUAL, pBits1, pBits2); } @Override protected Term implication(Term bits1, Term bits2) { - return solver.mkTerm(Kind.IMPLIES, bits1, bits2); + return termManager.mkTerm(Kind.IMPLIES, bits1, bits2); } @Override @@ -177,6 +177,6 @@ protected Term ifThenElse(Term pCond, Term pF1, Term pF2) { } else if (isFalse(pF1) && isTrue(pF2)) { return not(pCond); } - return solver.mkTerm(Kind.ITE, pCond, pF1, pF2); + return termManager.mkTerm(Kind.ITE, pCond, pF1, pF2); } } diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5EnumerationFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5EnumerationFormulaManager.java index 4844b3bc5f..20463ce307 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5EnumerationFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5EnumerationFormulaManager.java @@ -14,25 +14,27 @@ import io.github.cvc5.Solver; import io.github.cvc5.Sort; import io.github.cvc5.Term; +import io.github.cvc5.TermManager; import org.sosy_lab.java_smt.api.FormulaType.EnumerationFormulaType; import org.sosy_lab.java_smt.basicimpl.AbstractEnumerationFormulaManager; -import org.sosy_lab.java_smt.basicimpl.FormulaCreator; public class CVC5EnumerationFormulaManager - extends AbstractEnumerationFormulaManager { + extends AbstractEnumerationFormulaManager { + private final TermManager termManager; private final Solver solver; - protected CVC5EnumerationFormulaManager(FormulaCreator pCreator) { + protected CVC5EnumerationFormulaManager(CVC5FormulaCreator pCreator) { super(pCreator); - solver = pCreator.getEnv(); + termManager = pCreator.getEnv(); + solver = pCreator.getSolver(); } @Override protected EnumType declareEnumeration0(EnumerationFormulaType pType) { DatatypeConstructorDecl[] constructors = pType.getElements().stream() - .map(solver::mkDatatypeConstructorDecl) + .map(termManager::mkDatatypeConstructorDecl) .toArray(DatatypeConstructorDecl[]::new); Sort enumType = solver.declareDatatype(pType.getName(), constructors); @@ -40,13 +42,13 @@ protected EnumType declareEnumeration0(EnumerationFormulaType pType) { ImmutableMap.Builder constantsMapping = ImmutableMap.builder(); for (String element : pType.getElements()) { Term decl = enumType.getDatatype().getConstructor(element).getTerm(); - constantsMapping.put(element, solver.mkTerm(Kind.APPLY_CONSTRUCTOR, decl)); + constantsMapping.put(element, termManager.mkTerm(Kind.APPLY_CONSTRUCTOR, decl)); } return new EnumType(pType, enumType, constantsMapping.buildOrThrow()); } @Override protected Term equivalenceImpl(Term pF1, Term pF2) { - return solver.mkTerm(Kind.EQUAL, pF1, pF2); + return termManager.mkTerm(Kind.EQUAL, pF1, pF2); } } diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5Evaluator.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5Evaluator.java index cde787182d..60b3b78dcc 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5Evaluator.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5Evaluator.java @@ -12,9 +12,10 @@ import io.github.cvc5.Solver; import io.github.cvc5.Sort; import io.github.cvc5.Term; +import io.github.cvc5.TermManager; import org.sosy_lab.java_smt.basicimpl.AbstractEvaluator; -public class CVC5Evaluator extends AbstractEvaluator { +public class CVC5Evaluator extends AbstractEvaluator { private final Solver solver; diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FloatingPointFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FloatingPointFormulaManager.java index 2197a05ed7..883a8a1f8a 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FloatingPointFormulaManager.java @@ -16,6 +16,7 @@ import io.github.cvc5.Solver; import io.github.cvc5.Sort; import io.github.cvc5.Term; +import io.github.cvc5.TermManager; import java.math.BigDecimal; import java.math.BigInteger; import org.sosy_lab.common.rationals.Rational; @@ -27,15 +28,17 @@ import org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager; public class CVC5FloatingPointFormulaManager - extends AbstractFloatingPointFormulaManager { + extends AbstractFloatingPointFormulaManager { + private final TermManager termManager; private final Solver solver; private final Term roundingMode; protected CVC5FloatingPointFormulaManager( CVC5FormulaCreator pCreator, FloatingPointRoundingMode pFloatingPointRoundingMode) { super(pCreator); - solver = pCreator.getEnv(); + termManager = pCreator.getEnv(); + solver = pCreator.getSolver(); roundingMode = getRoundingModeImpl(pFloatingPointRoundingMode); } @@ -48,15 +51,15 @@ protected Term getDefaultRoundingMode() { protected Term getRoundingModeImpl(FloatingPointRoundingMode pFloatingPointRoundingMode) { switch (pFloatingPointRoundingMode) { case NEAREST_TIES_TO_EVEN: - return solver.mkRoundingMode(RoundingMode.ROUND_NEAREST_TIES_TO_EVEN); + return termManager.mkRoundingMode(RoundingMode.ROUND_NEAREST_TIES_TO_EVEN); case NEAREST_TIES_AWAY: - return solver.mkRoundingMode(RoundingMode.ROUND_NEAREST_TIES_TO_AWAY); + return termManager.mkRoundingMode(RoundingMode.ROUND_NEAREST_TIES_TO_AWAY); case TOWARD_POSITIVE: - return solver.mkRoundingMode(RoundingMode.ROUND_TOWARD_POSITIVE); + return termManager.mkRoundingMode(RoundingMode.ROUND_TOWARD_POSITIVE); case TOWARD_NEGATIVE: - return solver.mkRoundingMode(RoundingMode.ROUND_TOWARD_NEGATIVE); + return termManager.mkRoundingMode(RoundingMode.ROUND_TOWARD_NEGATIVE); case TOWARD_ZERO: - return solver.mkRoundingMode(RoundingMode.ROUND_TOWARD_ZERO); + return termManager.mkRoundingMode(RoundingMode.ROUND_TOWARD_ZERO); default: throw new AssertionError( "Unexpected rounding mode encountered: " + pFloatingPointRoundingMode); @@ -72,14 +75,11 @@ protected Term makeNumberImpl(double pN, FloatingPointType pType, Term pRounding protected Term makeNumberImpl( BigInteger exponent, BigInteger mantissa, Sign sign, FloatingPointType type) { try { - final String signStr = sign.isNegative() ? "1" : "0"; - final String exponentStr = getBvRepresentation(exponent, type.getExponentSize()); - final String mantissaStr = getBvRepresentation(mantissa, type.getMantissaSize()); - final String bitvecForm = signStr + exponentStr + mantissaStr; - - final Term bv = - solver.mkBitVector(type.getExponentSize() + type.getMantissaSize() + 1, bitvecForm, 2); - return solver.mkFloatingPoint(type.getExponentSize(), type.getMantissaSize() + 1, bv); + return termManager.mkFloatingPoint( + termManager.mkBitVector(1, sign == Sign.NEGATIVE ? 1 : 0), + termManager.mkBitVector(type.getExponentSize(), exponent.toString(16), 16), + termManager.mkBitVector(type.getMantissaSize(), mantissa.toString(16), 16)); + } catch (CVC5ApiException e) { throw new IllegalArgumentException("You tried creating a invalid bitvector", e); } @@ -89,7 +89,8 @@ protected Term makeNumberImpl( protected Term makeNumberAndRound(String pN, FloatingPointType pType, Term pRoundingMode) { try { if (isNegativeZero(Double.valueOf(pN))) { - return solver.mkFloatingPointNegZero(pType.getExponentSize(), pType.getMantissaSize() + 1); + return termManager.mkFloatingPointNegZero( + pType.getExponentSize(), pType.getMantissaSize() + 1); } } catch (CVC5ApiException | NumberFormatException e) { // ignore and fallback to floating point from rational numbers @@ -98,11 +99,12 @@ protected Term makeNumberAndRound(String pN, FloatingPointType pType, Term pRoun try { Rational rationalValue = toRational(pN); Op realToFp = - solver.mkOp( + termManager.mkOp( Kind.FLOATINGPOINT_TO_FP_FROM_REAL, pType.getExponentSize(), pType.getMantissaSize() + 1); - Term term = solver.mkTerm(realToFp, pRoundingMode, solver.mkReal(rationalValue.toString())); + Term term = + termManager.mkTerm(realToFp, pRoundingMode, termManager.mkReal(rationalValue.toString())); // simplification removes the cast from real to fp and return a bit-precise fp-number. return solver.simplify(term); } catch (CVC5ApiException e) { @@ -149,7 +151,8 @@ protected Term makeVariableImpl(String varName, FloatingPointType pType) { @Override protected Term makePlusInfinityImpl(FloatingPointType pType) { try { - return solver.mkFloatingPointPosInf(pType.getExponentSize(), pType.getMantissaSize() + 1); + return termManager.mkFloatingPointPosInf( + pType.getExponentSize(), pType.getMantissaSize() + 1); } catch (CVC5ApiException e) { throw new IllegalArgumentException( "You tried creating a invalid positive floating point +infinity with exponent size " @@ -164,7 +167,8 @@ protected Term makePlusInfinityImpl(FloatingPointType pType) { @Override protected Term makeMinusInfinityImpl(FloatingPointType pType) { try { - return solver.mkFloatingPointNegInf(pType.getExponentSize(), pType.getMantissaSize() + 1); + return termManager.mkFloatingPointNegInf( + pType.getExponentSize(), pType.getMantissaSize() + 1); } catch (CVC5ApiException e) { throw new IllegalArgumentException( "You tried creating a invalid negative floating point -infinity with exponent size " @@ -179,7 +183,7 @@ protected Term makeMinusInfinityImpl(FloatingPointType pType) { @Override protected Term makeNaNImpl(FloatingPointType pType) { try { - return solver.mkFloatingPointNaN(pType.getExponentSize(), pType.getMantissaSize() + 1); + return termManager.mkFloatingPointNaN(pType.getExponentSize(), pType.getMantissaSize() + 1); } catch (CVC5ApiException e) { throw new IllegalArgumentException( "You tried creating a invalid NaN with exponent size " @@ -198,20 +202,20 @@ protected Term castToImpl( try { if (pTargetType.isFloatingPointType()) { Op fpToFp = - solver.mkOp( + termManager.mkOp( Kind.FLOATINGPOINT_TO_FP_FROM_FP, ((FloatingPointType) pTargetType).getExponentSize(), ((FloatingPointType) pTargetType).getMantissaSize() + 1); - return solver.mkTerm(fpToFp, pRoundingMode, pNumber); + return termManager.mkTerm(fpToFp, pRoundingMode, pNumber); } else if (pTargetType.isBitvectorType()) { BitvectorType targetType = (BitvectorType) pTargetType; Kind kind = pSigned ? Kind.FLOATINGPOINT_TO_SBV : Kind.FLOATINGPOINT_TO_UBV; - Op operation = solver.mkOp(kind, targetType.getSize()); - return solver.mkTerm(operation, pRoundingMode, pNumber); + Op operation = termManager.mkOp(kind, targetType.getSize()); + return termManager.mkTerm(operation, pRoundingMode, pNumber); } else if (pTargetType.isRationalType()) { - return solver.mkTerm(Kind.FLOATINGPOINT_TO_REAL, pNumber); + return termManager.mkTerm(Kind.FLOATINGPOINT_TO_REAL, pNumber); } else { return genericCast(pNumber, pTargetType); @@ -239,28 +243,28 @@ protected Term castFromImpl( } else if (formulaType.isRationalType()) { Op realToFp = - solver.mkOp( + termManager.mkOp( Kind.FLOATINGPOINT_TO_FP_FROM_REAL, pTargetType.getExponentSize(), pTargetType.getMantissaSize() + 1); - return solver.mkTerm(realToFp, pRoundingMode, pNumber); + return termManager.mkTerm(realToFp, pRoundingMode, pNumber); } else if (formulaType.isBitvectorType()) { if (pSigned) { Op realToSBv = - solver.mkOp( + termManager.mkOp( Kind.FLOATINGPOINT_TO_FP_FROM_SBV, pTargetType.getExponentSize(), pTargetType.getMantissaSize() + 1); - return solver.mkTerm(realToSBv, pRoundingMode, pNumber); + return termManager.mkTerm(realToSBv, pRoundingMode, pNumber); } else { Op realToUBv = - solver.mkOp( + termManager.mkOp( Kind.FLOATINGPOINT_TO_FP_FROM_UBV, pTargetType.getExponentSize(), pTargetType.getMantissaSize() + 1); - return solver.mkTerm(realToUBv, pRoundingMode, pNumber); + return termManager.mkTerm(realToUBv, pRoundingMode, pNumber); } } else { @@ -290,117 +294,117 @@ private Term genericCast(Term pNumber, FormulaType pTargetType) { "__cast_" + argType + "_to_" + pTargetType, toSolverType(pTargetType), ImmutableList.of(type)); - return solver.mkTerm(Kind.APPLY_UF, castFuncDecl, pNumber); + return termManager.mkTerm(Kind.APPLY_UF, castFuncDecl, pNumber); } @Override protected Term negate(Term pParam1) { - return solver.mkTerm(Kind.FLOATINGPOINT_NEG, pParam1); + return termManager.mkTerm(Kind.FLOATINGPOINT_NEG, pParam1); } @Override protected Term abs(Term pParam1) { - return solver.mkTerm(Kind.FLOATINGPOINT_ABS, pParam1); + return termManager.mkTerm(Kind.FLOATINGPOINT_ABS, pParam1); } @Override protected Term max(Term pParam1, Term pParam2) { - return solver.mkTerm(Kind.FLOATINGPOINT_MAX, pParam1, pParam2); + return termManager.mkTerm(Kind.FLOATINGPOINT_MAX, pParam1, pParam2); } @Override protected Term min(Term pParam1, Term pParam2) { - return solver.mkTerm(Kind.FLOATINGPOINT_MIN, pParam1, pParam2); + return termManager.mkTerm(Kind.FLOATINGPOINT_MIN, pParam1, pParam2); } @Override protected Term sqrt(Term pParam1, Term pRoundingMode) { - return solver.mkTerm(Kind.FLOATINGPOINT_SQRT, pRoundingMode, pParam1); + return termManager.mkTerm(Kind.FLOATINGPOINT_SQRT, pRoundingMode, pParam1); } @Override protected Term add(Term pParam1, Term pParam2, Term pRoundingMode) { - return solver.mkTerm(Kind.FLOATINGPOINT_ADD, pRoundingMode, pParam1, pParam2); + return termManager.mkTerm(Kind.FLOATINGPOINT_ADD, pRoundingMode, pParam1, pParam2); } @Override protected Term subtract(Term pParam1, Term pParam2, Term pRoundingMode) { - return solver.mkTerm(Kind.FLOATINGPOINT_SUB, pRoundingMode, pParam1, pParam2); + return termManager.mkTerm(Kind.FLOATINGPOINT_SUB, pRoundingMode, pParam1, pParam2); } @Override protected Term divide(Term pParam1, Term pParam2, Term pRoundingMode) { - return solver.mkTerm(Kind.FLOATINGPOINT_DIV, pRoundingMode, pParam1, pParam2); + return termManager.mkTerm(Kind.FLOATINGPOINT_DIV, pRoundingMode, pParam1, pParam2); } @Override protected Term multiply(Term pParam1, Term pParam2, Term pRoundingMode) { - return solver.mkTerm(Kind.FLOATINGPOINT_MULT, pRoundingMode, pParam1, pParam2); + return termManager.mkTerm(Kind.FLOATINGPOINT_MULT, pRoundingMode, pParam1, pParam2); } @Override protected Term remainder(Term pParam1, Term pParam2) { - return solver.mkTerm(Kind.FLOATINGPOINT_REM, pParam1, pParam2); + return termManager.mkTerm(Kind.FLOATINGPOINT_REM, pParam1, pParam2); } @Override protected Term assignment(Term pParam1, Term pParam2) { - return solver.mkTerm(Kind.EQUAL, pParam1, pParam2); + return termManager.mkTerm(Kind.EQUAL, pParam1, pParam2); } @Override protected Term equalWithFPSemantics(Term pParam1, Term pParam2) { - return solver.mkTerm(Kind.FLOATINGPOINT_EQ, pParam1, pParam2); + return termManager.mkTerm(Kind.FLOATINGPOINT_EQ, pParam1, pParam2); } @Override protected Term greaterThan(Term pParam1, Term pParam2) { - return solver.mkTerm(Kind.FLOATINGPOINT_GT, pParam1, pParam2); + return termManager.mkTerm(Kind.FLOATINGPOINT_GT, pParam1, pParam2); } @Override protected Term greaterOrEquals(Term pParam1, Term pParam2) { - return solver.mkTerm(Kind.FLOATINGPOINT_GEQ, pParam1, pParam2); + return termManager.mkTerm(Kind.FLOATINGPOINT_GEQ, pParam1, pParam2); } @Override protected Term lessThan(Term pParam1, Term pParam2) { - return solver.mkTerm(Kind.FLOATINGPOINT_LT, pParam1, pParam2); + return termManager.mkTerm(Kind.FLOATINGPOINT_LT, pParam1, pParam2); } @Override protected Term lessOrEquals(Term pParam1, Term pParam2) { - return solver.mkTerm(Kind.FLOATINGPOINT_LEQ, pParam1, pParam2); + return termManager.mkTerm(Kind.FLOATINGPOINT_LEQ, pParam1, pParam2); } @Override protected Term isNaN(Term pParam1) { - return solver.mkTerm(Kind.FLOATINGPOINT_IS_NAN, pParam1); + return termManager.mkTerm(Kind.FLOATINGPOINT_IS_NAN, pParam1); } @Override protected Term isInfinity(Term pParam1) { - return solver.mkTerm(Kind.FLOATINGPOINT_IS_INF, pParam1); + return termManager.mkTerm(Kind.FLOATINGPOINT_IS_INF, pParam1); } @Override protected Term isZero(Term pParam1) { - return solver.mkTerm(Kind.FLOATINGPOINT_IS_ZERO, pParam1); + return termManager.mkTerm(Kind.FLOATINGPOINT_IS_ZERO, pParam1); } @Override protected Term isSubnormal(Term pParam1) { - return solver.mkTerm(Kind.FLOATINGPOINT_IS_SUBNORMAL, pParam1); + return termManager.mkTerm(Kind.FLOATINGPOINT_IS_SUBNORMAL, pParam1); } @Override protected Term isNormal(Term pParam) { - return solver.mkTerm(Kind.FLOATINGPOINT_IS_NORMAL, pParam); + return termManager.mkTerm(Kind.FLOATINGPOINT_IS_NORMAL, pParam); } @Override protected Term isNegative(Term pParam) { - return solver.mkTerm(Kind.FLOATINGPOINT_IS_NEG, pParam); + return termManager.mkTerm(Kind.FLOATINGPOINT_IS_NEG, pParam); } @Override @@ -414,19 +418,19 @@ protected Term fromIeeeBitvectorImpl(Term bitvector, FloatingPointType pTargetTy Op exponentExtract; Op mantissaExtract; try { - signExtract = solver.mkOp(Kind.BITVECTOR_EXTRACT, size - 1, size - 1); - exponentExtract = solver.mkOp(Kind.BITVECTOR_EXTRACT, size - 2, mantissaSize); - mantissaExtract = solver.mkOp(Kind.BITVECTOR_EXTRACT, mantissaSize - 1, 0); + signExtract = termManager.mkOp(Kind.BITVECTOR_EXTRACT, size - 1, size - 1); + exponentExtract = termManager.mkOp(Kind.BITVECTOR_EXTRACT, size - 2, mantissaSize); + mantissaExtract = termManager.mkOp(Kind.BITVECTOR_EXTRACT, mantissaSize - 1, 0); } catch (CVC5ApiException e) { throw new IllegalArgumentException( "You tried creating a invalid bitvector extract in term " + bitvector + ".", e); } - Term sign = solver.mkTerm(signExtract, bitvector); - Term exponent = solver.mkTerm(exponentExtract, bitvector); - Term mantissa = solver.mkTerm(mantissaExtract, bitvector); + Term sign = termManager.mkTerm(signExtract, bitvector); + Term exponent = termManager.mkTerm(exponentExtract, bitvector); + Term mantissa = termManager.mkTerm(mantissaExtract, bitvector); - return solver.mkTerm(Kind.FLOATINGPOINT_FP, sign, exponent, mantissa); + return termManager.mkTerm(Kind.FLOATINGPOINT_FP, sign, exponent, mantissa); } @Override @@ -439,6 +443,6 @@ protected Term toIeeeBitvectorImpl(Term pNumber) { @Override protected Term round(Term pFormula, FloatingPointRoundingMode pRoundingMode) { - return solver.mkTerm(Kind.FLOATINGPOINT_RTI, getRoundingModeImpl(pRoundingMode), pFormula); + return termManager.mkTerm(Kind.FLOATINGPOINT_RTI, getRoundingModeImpl(pRoundingMode), pFormula); } } diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java index 44a75476de..ebde92e4e4 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java @@ -30,6 +30,7 @@ import io.github.cvc5.Solver; import io.github.cvc5.Sort; import io.github.cvc5.Term; +import io.github.cvc5.TermManager; import java.lang.reflect.Array; import java.math.BigInteger; import java.util.ArrayList; @@ -66,7 +67,7 @@ import org.sosy_lab.java_smt.solvers.cvc5.CVC5Formula.CVC5RegexFormula; import org.sosy_lab.java_smt.solvers.cvc5.CVC5Formula.CVC5StringFormula; -public class CVC5FormulaCreator extends FormulaCreator { +public class CVC5FormulaCreator extends FormulaCreator { /** CVC5 does not allow using some key-functions from SMTLIB2 as identifiers. */ private static final ImmutableSet UNSUPPORTED_IDENTIFIERS = ImmutableSet.of("let"); @@ -78,19 +79,25 @@ public class CVC5FormulaCreator extends FormulaCreator // String representation is equal (and they are equal) private final Table variablesCache = HashBasedTable.create(); private final Map functionsCache = new HashMap<>(); + private final TermManager termManager; private final Solver solver; - protected CVC5FormulaCreator(Solver pSolver) { + protected CVC5FormulaCreator(TermManager pTermManager, Solver pSolver) { super( - pSolver, - pSolver.getBooleanSort(), - pSolver.getIntegerSort(), - pSolver.getRealSort(), - pSolver.getStringSort(), - pSolver.getRegExpSort()); + pTermManager, + pTermManager.getBooleanSort(), + pTermManager.getIntegerSort(), + pTermManager.getRealSort(), + pTermManager.getStringSort(), + pTermManager.getRegExpSort()); + termManager = pTermManager; solver = pSolver; } + public Solver getSolver() { + return solver; + } + @Override public Term makeVariable(Sort sort, String name) { Term existingVar = variablesCache.get(name, sort.toString()); @@ -116,7 +123,7 @@ public Term makeVariable(Sort sort, String name) { 0] .getKey()); } - Term newVar = solver.mkConst(sort, name); + Term newVar = termManager.mkConst(sort, name); variablesCache.put(name, sort.toString(), newVar); return newVar; } @@ -131,14 +138,14 @@ public Term makeVariable(Sort sort, String name) { public Term makeBoundCopy(Term var) { Sort sort = var.getSort(); String name = getName(var); - Term boundCopy = solver.mkVar(sort, name); + Term boundCopy = termManager.mkVar(sort, name); return boundCopy; } @Override public Sort getBitvectorType(int pBitwidth) { try { - return solver.mkBitVectorSort(pBitwidth); + return termManager.mkBitVectorSort(pBitwidth); } catch (CVC5ApiException e) { throw new IllegalArgumentException( "Cannot create bitvector sort with size " + pBitwidth + ".", e); @@ -149,7 +156,7 @@ public Sort getBitvectorType(int pBitwidth) { public Sort getFloatingPointType(FloatingPointType pType) { try { // plus sign bit - return solver.mkFloatingPointSort(pType.getExponentSize(), pType.getMantissaSize() + 1); + return termManager.mkFloatingPointSort(pType.getExponentSize(), pType.getMantissaSize() + 1); } catch (CVC5ApiException e) { throw new IllegalArgumentException( "Cannot create floatingpoint sort with exponent size " @@ -163,7 +170,7 @@ public Sort getFloatingPointType(FloatingPointType pType) { @Override public Sort getArrayType(Sort pIndexType, Sort pElementType) { - return solver.mkArraySort(pIndexType, pElementType); + return termManager.mkArraySort(pIndexType, pElementType); } @Override @@ -692,7 +699,7 @@ public Term callFunctionImpl(final Term pDeclaration, final List pArgs) { if (pDeclaration.hasOp()) { Op op = pDeclaration.getOp(); - return solver.mkTerm(op, pArgs.toArray(new Term[] {})); + return termManager.mkTerm(op, pArgs.toArray(new Term[] {})); } else { try { Sort[] paramSorts = pDeclaration.getSort().getFunctionDomainSorts(); @@ -703,7 +710,7 @@ public Term callFunctionImpl(final Term pDeclaration, final List pArgs) { kind = Kind.APPLY_UF; args.add(0, pDeclaration); } - return solver.mkTerm(kind, args.toArray(new Term[] {})); + return termManager.mkTerm(kind, args.toArray(new Term[] {})); } catch (CVC5ApiException e) { throw new IllegalArgumentException( "Failure when building the UF '" @@ -737,7 +744,7 @@ private List castToParamTypeIfRequired(List pArgs, Sort[] pParamSort private Term castToParamTypeIfRequired(Term input, @Nullable Sort targetSort) { if (input.getSort().isInteger() && targetSort.isReal()) { - return solver.mkTerm(Kind.TO_REAL, input); + return termManager.mkTerm(Kind.TO_REAL, input); } return input; } @@ -766,8 +773,8 @@ public Term declareUFImpl(String pName, Sort pReturnType, List pArgTypes) Sort sort = pArgTypes.isEmpty() ? pReturnType - : solver.mkFunctionSort(pArgTypes.toArray(new Sort[0]), pReturnType); - exp = solver.mkConst(sort, pName); + : termManager.mkFunctionSort(pArgTypes.toArray(new Sort[0]), pReturnType); + exp = termManager.mkConst(sort, pName); functionsCache.put(pName, exp); } else { diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java index b98dd06385..d7fb51e845 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java @@ -13,16 +13,16 @@ import de.uni_freiburg.informatik.ultimate.logic.PrintTerm; import io.github.cvc5.CVC5ApiException; import io.github.cvc5.Kind; -import io.github.cvc5.Solver; import io.github.cvc5.Sort; import io.github.cvc5.Term; +import io.github.cvc5.TermManager; import java.util.LinkedHashMap; import java.util.Map; import org.sosy_lab.java_smt.api.Formula; import org.sosy_lab.java_smt.api.FormulaType; import org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager; -class CVC5FormulaManager extends AbstractFormulaManager { +class CVC5FormulaManager extends AbstractFormulaManager { private final CVC5FormulaCreator creator; diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5IntegerFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5IntegerFormulaManager.java index d1c120d978..da62fe3ef5 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5IntegerFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5IntegerFormulaManager.java @@ -42,7 +42,7 @@ protected Term makeNumberImpl(BigDecimal pNumber) { @Override public Term divide(Term pParam1, Term pParam2) { - return solver.mkTerm(Kind.INTS_DIVISION, pParam1, pParam2); + return termManager.mkTerm(Kind.INTS_DIVISION, pParam1, pParam2); } @Override @@ -56,10 +56,12 @@ protected Term modularCongruence(Term pNumber1, Term pNumber2, BigInteger pModul if (BigInteger.ZERO.compareTo(pModulo) < 0) { Term n = makeNumberImpl(pModulo); Term x = subtract(pNumber1, pNumber2); - return solver.mkTerm( - Kind.EQUAL, x, solver.mkTerm(Kind.MULT, n, solver.mkTerm(Kind.INTS_DIVISION, x, n))); + return termManager.mkTerm( + Kind.EQUAL, + x, + termManager.mkTerm(Kind.MULT, n, termManager.mkTerm(Kind.INTS_DIVISION, x, n))); } - return solver.mkBoolean(true); + return termManager.mkBoolean(true); } @Override @@ -73,7 +75,7 @@ protected Term makeNumberImpl(String pI) { throw new NumberFormatException("Number is not an integer value: " + pI); } try { - return solver.mkInteger(pI); + return termManager.mkInteger(pI); } catch (CVC5ApiException e) { throw new NumberFormatException("Number is not an integer value: " + pI); } diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5InterpolatingProver.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5InterpolatingProver.java index af2b569fe8..2f99bca077 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5InterpolatingProver.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5InterpolatingProver.java @@ -20,6 +20,7 @@ import io.github.cvc5.Kind; import io.github.cvc5.Solver; import io.github.cvc5.Term; +import io.github.cvc5.TermManager; import java.util.ArrayList; import java.util.Collection; import java.util.List; @@ -34,6 +35,8 @@ public class CVC5InterpolatingProver extends CVC5AbstractProver implements InterpolatingProverEnvironment { + private final TermManager termManager = creator.getEnv(); + private final FormulaManager mgr; private final Set solverOptions; private final ImmutableMap furtherOptionsMap; @@ -106,7 +109,7 @@ public List getSeqInterpolants(List final int n = partitions.size(); final List itps = new ArrayList<>(); - Term previousItp = solver.mkTrue(); + Term previousItp = termManager.mkTrue(); for (int i = 1; i < n; i++) { Collection formulasA = FluentIterable.from(partitions.get(i - 1)) @@ -181,13 +184,13 @@ private Term getCVC5Interpolation(Collection formulasA, Collection f Term phiMinus = bmgr.andImpl(formulasB); // Uses a separate Solver instance to leave the original solver-context unmodified - Solver itpSolver = new Solver(); + Solver itpSolver = new Solver(termManager); setSolverOptions(seed, solverOptions, furtherOptionsMap, itpSolver); Term interpolant; try { itpSolver.assertFormula(phiPlus); - interpolant = itpSolver.getInterpolant(itpSolver.mkTerm(Kind.NOT, phiMinus)); + interpolant = itpSolver.getInterpolant(termManager.mkTerm(Kind.NOT, phiMinus)); } finally { itpSolver.deletePointer(); } @@ -222,19 +225,19 @@ private void checkInterpolationCriteria(Term interpolant, Term phiPlus, Term phi Sets.difference(interpolantSymbols, intersection)); // build and check both Craig interpolation formulas with the generated interpolant. - Solver validationSolver = new Solver(); + Solver validationSolver = new Solver(termManager); // interpolation option is not required for validation super.setSolverOptions(seed, solverOptions, furtherOptionsMap, validationSolver); try { validationSolver.push(); - validationSolver.assertFormula(validationSolver.mkTerm(Kind.IMPLIES, phiPlus, interpolant)); + validationSolver.assertFormula(termManager.mkTerm(Kind.IMPLIES, phiPlus, interpolant)); checkState( validationSolver.checkSat().isSat(), "Invalid Craig interpolation: phi+ does not imply the interpolant."); validationSolver.pop(); validationSolver.push(); - validationSolver.assertFormula(validationSolver.mkTerm(Kind.AND, interpolant, phiMinus)); + validationSolver.assertFormula(termManager.mkTerm(Kind.AND, interpolant, phiMinus)); checkState( validationSolver.checkSat().isUnsat(), "Invalid Craig interpolation: interpolant does not contradict phi-."); diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5Model.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5Model.java index 793fa9b36b..cba98c1d85 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5Model.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5Model.java @@ -16,15 +16,17 @@ import io.github.cvc5.Solver; import io.github.cvc5.Sort; import io.github.cvc5.Term; +import io.github.cvc5.TermManager; import java.util.Collection; import org.sosy_lab.java_smt.api.BooleanFormula; import org.sosy_lab.java_smt.api.Formula; import org.sosy_lab.java_smt.api.FormulaManager; import org.sosy_lab.java_smt.basicimpl.AbstractModel; -public class CVC5Model extends AbstractModel { +public class CVC5Model extends AbstractModel { private final ImmutableList model; + private final TermManager termManager; private final Solver solver; private final ImmutableList assertedExpressions; @@ -37,6 +39,7 @@ public class CVC5Model extends AbstractModel { CVC5FormulaCreator pCreator, Collection pAssertedExpressions) { super(pProver, pCreator); + termManager = pCreator.getEnv(); solver = pProver.solver; mgr = pMgr; assertedExpressions = ImmutableList.copyOf(pAssertedExpressions); @@ -159,7 +162,7 @@ private ValueAssignment getAssignmentForUf(Term pKeyTerm) { Formula keyFormula = creator.encapsulateWithTypeOf(pKeyTerm); Formula valueFormula = creator.encapsulateWithTypeOf(valueTerm); BooleanFormula equation = - creator.encapsulateBoolean(solver.mkTerm(Kind.EQUAL, pKeyTerm, valueTerm)); + creator.encapsulateBoolean(termManager.mkTerm(Kind.EQUAL, pKeyTerm, valueTerm)); Object value = creator.convertValue(pKeyTerm, valueTerm); return new ValueAssignment( @@ -193,7 +196,7 @@ private ValueAssignment getAssignment(Term pKeyTerm) { Formula keyFormula = creator.encapsulateWithTypeOf(pKeyTerm); Formula valueFormula = creator.encapsulateWithTypeOf(valueTerm); BooleanFormula equation = - creator.encapsulateBoolean(solver.mkTerm(Kind.EQUAL, pKeyTerm, valueTerm)); + creator.encapsulateBoolean(termManager.mkTerm(Kind.EQUAL, pKeyTerm, valueTerm)); Object value = creator.convertValue(pKeyTerm, valueTerm); return new ValueAssignment( keyFormula, valueFormula, equation, nameStr, value, argumentInterpretationBuilder.build()); diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5NativeAPITest.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5NativeAPITest.java index a0c953b88b..e15fdec270 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5NativeAPITest.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5NativeAPITest.java @@ -15,16 +15,20 @@ import io.github.cvc5.CVC5ApiException; import io.github.cvc5.Kind; import io.github.cvc5.Op; +import io.github.cvc5.Proof; +import io.github.cvc5.ProofRule; import io.github.cvc5.Result; import io.github.cvc5.RoundingMode; import io.github.cvc5.Solver; import io.github.cvc5.Sort; import io.github.cvc5.Term; +import io.github.cvc5.TermManager; import java.util.ArrayList; import java.util.Arrays; import java.util.HashMap; import java.util.List; import java.util.Map; +import java.util.Optional; import org.junit.After; import org.junit.AssumptionViolatedException; import org.junit.Before; @@ -45,13 +49,12 @@ public class CVC5NativeAPITest { private static final String INVALID_GETVALUE_STRING_SAT = - "Cannot get value unless after a SAT or UNKNOWN response."; + "cannot get value unless after a SAT or UNKNOWN response."; - private static final String INVALID_TERM_BOUND_VAR = - "Cannot process term .* with free variables: .*"; + private static final String INVALID_TERM_BOUND_VAR = "cannot process term .* with free variables"; private static final String INVALID_MODEL_STRING = - "Cannot get model unless after a SAT or UNKNOWN response."; + "cannot get model unless after a SAT or UNKNOWN response."; @BeforeClass public static void loadCVC5() { @@ -67,22 +70,23 @@ public static void loadCVC5() { private Term aAtxEq0; private Term aAtxEq1; + private TermManager termManager; private Solver solver; @Before public void init() throws CVC5ApiException { + termManager = new TermManager(); solver = createEnvironment(); } - private static Solver createEnvironment() throws CVC5ApiException { - Solver newSolver = new Solver(); + private Solver createEnvironment() throws CVC5ApiException { + Solver newSolver = new Solver(termManager); newSolver.setLogic("ALL"); // options newSolver.setOption("incremental", "true"); newSolver.setOption("produce-models", "true"); newSolver.setOption("finite-model-find", "true"); - newSolver.setOption("sets-ext", "true"); newSolver.setOption("output-language", "smtlib2"); newSolver.setOption("strings-exp", "true"); @@ -92,6 +96,7 @@ private static Solver createEnvironment() throws CVC5ApiException { @After public void freeEnvironment() { solver.deletePointer(); + termManager.deletePointer(); } /* @@ -105,35 +110,35 @@ public void freeEnvironment() { @Test public void checkGetValueAndType() throws CVC5ApiException { // Constant values (NOT Kind,CONSTANT!) - assertThat(solver.mkBoolean(false).isBooleanValue()).isTrue(); - assertThat(solver.mkInteger(0).isIntegerValue()).isTrue(); - assertThat(solver.mkInteger(999).isIntegerValue()).isTrue(); - assertThat(solver.mkInteger(-1).isIntegerValue()).isTrue(); - assertThat(solver.mkInteger("0").isIntegerValue()).isTrue(); - assertThat(solver.mkString("").isStringValue()).isTrue(); + assertThat(termManager.mkBoolean(false).isBooleanValue()).isTrue(); + assertThat(termManager.mkInteger(0).isIntegerValue()).isTrue(); + assertThat(termManager.mkInteger(999).isIntegerValue()).isTrue(); + assertThat(termManager.mkInteger(-1).isIntegerValue()).isTrue(); + assertThat(termManager.mkInteger("0").isIntegerValue()).isTrue(); + assertThat(termManager.mkString("").isStringValue()).isTrue(); // Note: toString on String values does not equal the value!! - assertThat(solver.mkString("").toString()).isNotEqualTo(""); - assertThat(solver.mkString("").getStringValue()).isEqualTo(""); + assertThat(termManager.mkString("").toString()).isNotEqualTo(""); + assertThat(termManager.mkString("").getStringValue()).isEqualTo(""); // Variables (named const, because thats not confusing....) // Variables (Consts) return false if checked for value! - assertThat(solver.mkConst(solver.getBooleanSort()).isBooleanValue()).isFalse(); - assertThat(solver.mkConst(solver.getIntegerSort()).isIntegerValue()).isFalse(); + assertThat(termManager.mkConst(termManager.getBooleanSort()).isBooleanValue()).isFalse(); + assertThat(termManager.mkConst(termManager.getIntegerSort()).isIntegerValue()).isFalse(); // To check for variables we have to check for value and type - assertThat(solver.mkConst(solver.getBooleanSort()).getSort().isBoolean()).isTrue(); + assertThat(termManager.mkConst(termManager.getBooleanSort()).getSort().isBoolean()).isTrue(); // Test consts (variables). Consts are always false when checked for isTypedValue(), if you try // getTypedValue() on it anyway an exception is raised. This persists after sat. The only way of // checking and geting the values is via Kind.CONSTANT, type = sort and getValue() - Term intVar = solver.mkConst(solver.getIntegerSort(), "int_const"); + Term intVar = termManager.mkConst(termManager.getIntegerSort(), "int_const"); assertThat(intVar.isIntegerValue()).isFalse(); assertThat(intVar.getSort().isInteger()).isTrue(); Exception e = assertThrows(io.github.cvc5.CVC5ApiException.class, intVar::getIntegerValue); assertThat(e.toString()) .contains( - "Invalid argument 'int_const' for '*d_node', expected Term to be an integer value when" + "invalid argument 'int_const' for '*d_node', expected Term to be an integer value when" + " calling getIntegerValue()"); // Build a formula such that is has a value, assert and check sat and then check again - Term equality = solver.mkTerm(Kind.EQUAL, intVar, solver.mkInteger(1)); + Term equality = termManager.mkTerm(Kind.EQUAL, intVar, termManager.mkInteger(1)); solver.assertFormula(equality); // Is sat, no need to check solver.checkSat(); @@ -145,17 +150,19 @@ public void checkGetValueAndType() throws CVC5ApiException { // Op test assertThat(equality.getOp().toString()).isEqualTo("EQUAL"); assertThat( - solver.mkTerm(equality.getOp(), intVar, solver.mkInteger(1)).getId() + termManager.mkTerm(equality.getOp(), intVar, termManager.mkInteger(1)).getId() == equality.getId()) .isTrue(); // Note that variables (Kind.VARIABLES) are bound variables! - assertThat(solver.mkVar(solver.getIntegerSort()).getKind()).isEqualTo(Kind.VARIABLE); - assertThat(solver.mkVar(solver.getIntegerSort()).getKind()).isNotEqualTo(Kind.CONSTANT); + assertThat(termManager.mkVar(termManager.getIntegerSort()).getKind()).isEqualTo(Kind.VARIABLE); + assertThat(termManager.mkVar(termManager.getIntegerSort()).getKind()) + .isNotEqualTo(Kind.CONSTANT); // Uf return sort is codomain // Uf unapplied are CONSTANT - Sort intToBoolSort = solver.mkFunctionSort(solver.getIntegerSort(), solver.getBooleanSort()); + Sort intToBoolSort = + termManager.mkFunctionSort(termManager.getIntegerSort(), termManager.getBooleanSort()); assertThat(intToBoolSort.getFunctionCodomainSort().isBoolean()).isTrue(); - Term uf1 = solver.mkConst(intToBoolSort); + Term uf1 = termManager.mkConst(intToBoolSort); assertThat(uf1.getKind()).isNotEqualTo(Kind.VARIABLE); assertThat(uf1.getKind()).isEqualTo(Kind.CONSTANT); assertThat(uf1.getKind()).isNotEqualTo(Kind.APPLY_UF); @@ -164,18 +171,18 @@ public void checkGetValueAndType() throws CVC5ApiException { // arity 1 assertThat(uf1.getSort().getFunctionArity()).isEqualTo(1); // apply the uf, the kind is now APPLY_UF - Term appliedUf1 = solver.mkTerm(Kind.APPLY_UF, new Term[] {uf1, intVar}); + Term appliedUf1 = termManager.mkTerm(Kind.APPLY_UF, new Term[] {uf1, intVar}); assertThat(appliedUf1.getKind()).isNotEqualTo(Kind.VARIABLE); assertThat(appliedUf1.getKind()).isNotEqualTo(Kind.CONSTANT); assertThat(appliedUf1.getKind()).isEqualTo(Kind.APPLY_UF); assertThat(appliedUf1.getSort().isFunction()).isFalse(); // The ufs sort is always the returntype - assertThat(appliedUf1.getSort()).isEqualTo(solver.getBooleanSort()); + assertThat(appliedUf1.getSort()).isEqualTo(termManager.getBooleanSort()); assertThat(appliedUf1.getNumChildren()).isEqualTo(2); // The first child is the UF assertThat(appliedUf1.getChild(0).getSort()).isEqualTo(intToBoolSort); // The second child onwards are the arguments - assertThat(appliedUf1.getChild(1).getSort()).isEqualTo(solver.getIntegerSort()); + assertThat(appliedUf1.getChild(1).getSort()).isEqualTo(termManager.getIntegerSort()); } /* @@ -184,38 +191,39 @@ public void checkGetValueAndType() throws CVC5ApiException { */ @Test public void checkFPConversion() throws CVC5ApiException { - Term oneFourth = solver.mkReal("1/4"); - Term intOneFourth = solver.mkTerm(Kind.TO_INTEGER, oneFourth); - Term bvOneFourth = solver.mkTerm(solver.mkOp(Kind.INT_TO_BITVECTOR, 32), intOneFourth); + Term oneFourth = termManager.mkReal("1/4"); + Term intOneFourth = termManager.mkTerm(Kind.TO_INTEGER, oneFourth); + Term bvOneFourth = + termManager.mkTerm(termManager.mkOp(Kind.INT_TO_BITVECTOR, 32), intOneFourth); Exception e = assertThrows( io.github.cvc5.CVC5ApiException.class, - () -> solver.mkFloatingPoint(8, 24, bvOneFourth)); + () -> termManager.mkFloatingPoint(8, 24, bvOneFourth)); assertThat(e.toString()) .contains( - "Invalid argument '((_ int2bv 32) (to_int (/ 1 4)))' for 'val', expected bit-vector" - + " constant"); + "invalid argument '((_ int2bv 32) (to_int (/ 1 4)))' for 'val', expected bit-vector" + + " value"); } @Test public void checkSimpleUnsat() { - solver.assertFormula(solver.mkBoolean(false)); + solver.assertFormula(termManager.mkBoolean(false)); Result satCheck = solver.checkSat(); assertThat(satCheck.isUnsat()).isTrue(); } @Test public void checkSimpleSat() { - solver.assertFormula(solver.mkBoolean(true)); + solver.assertFormula(termManager.mkBoolean(true)); Result satCheck = solver.checkSat(); assertThat(satCheck.isSat()).isTrue(); } @Test public void checkSimpleEqualitySat() { - Term one = solver.mkInteger(1); - Term assertion = solver.mkTerm(Kind.EQUAL, one, one); + Term one = termManager.mkInteger(1); + Term assertion = termManager.mkTerm(Kind.EQUAL, one, one); solver.assertFormula(assertion); Result satCheck = solver.checkSat(); assertThat(satCheck.isSat()).isTrue(); @@ -223,9 +231,9 @@ public void checkSimpleEqualitySat() { @Test public void checkSimpleEqualityUnsat() { - Term zero = solver.mkInteger(0); - Term one = solver.mkInteger(1); - Term assertion = solver.mkTerm(Kind.EQUAL, zero, one); + Term zero = termManager.mkInteger(0); + Term one = termManager.mkInteger(1); + Term assertion = termManager.mkTerm(Kind.EQUAL, zero, one); solver.assertFormula(assertion); Result satCheck = solver.checkSat(); assertThat(satCheck.isSat()).isFalse(); @@ -233,8 +241,8 @@ public void checkSimpleEqualityUnsat() { @Test public void checkSimpleInequalityUnsat() { - Term one = solver.mkInteger(1); - Term assertion = solver.mkTerm(Kind.NOT, solver.mkTerm(Kind.EQUAL, one, one)); + Term one = termManager.mkInteger(1); + Term assertion = termManager.mkTerm(Kind.NOT, termManager.mkTerm(Kind.EQUAL, one, one)); solver.assertFormula(assertion); Result satCheck = solver.checkSat(); assertThat(satCheck.isSat()).isFalse(); @@ -242,9 +250,9 @@ public void checkSimpleInequalityUnsat() { @Test public void checkSimpleInequalitySat() { - Term zero = solver.mkInteger(0); - Term one = solver.mkInteger(1); - Term assertion = solver.mkTerm(Kind.NOT, solver.mkTerm(Kind.EQUAL, zero, one)); + Term zero = termManager.mkInteger(0); + Term one = termManager.mkInteger(1); + Term assertion = termManager.mkTerm(Kind.NOT, termManager.mkTerm(Kind.EQUAL, zero, one)); solver.assertFormula(assertion); Result satCheck = solver.checkSat(); assertThat(satCheck.isSat()).isTrue(); @@ -252,9 +260,9 @@ public void checkSimpleInequalitySat() { @Test public void checkSimpleLIAEqualitySat() { - Term one = solver.mkInteger(1); - Term two = solver.mkInteger(2); - Term assertion = solver.mkTerm(Kind.EQUAL, solver.mkTerm(Kind.ADD, one, one), two); + Term one = termManager.mkInteger(1); + Term two = termManager.mkInteger(2); + Term assertion = termManager.mkTerm(Kind.EQUAL, termManager.mkTerm(Kind.ADD, one, one), two); solver.assertFormula(assertion); Result satCheck = solver.checkSat(); assertThat(satCheck.isSat()).isTrue(); @@ -262,8 +270,8 @@ public void checkSimpleLIAEqualitySat() { @Test public void checkSimpleLIAEqualityUnsat() { - Term one = solver.mkInteger(1); - Term assertion = solver.mkTerm(Kind.EQUAL, solver.mkTerm(Kind.ADD, one, one), one); + Term one = termManager.mkInteger(1); + Term assertion = termManager.mkTerm(Kind.EQUAL, termManager.mkTerm(Kind.ADD, one, one), one); solver.assertFormula(assertion); Result satCheck = solver.checkSat(); assertThat(satCheck.isSat()).isFalse(); @@ -272,11 +280,13 @@ public void checkSimpleLIAEqualityUnsat() { @Test public void checkSimpleLIASat() { // x + y = 4 AND x * y = 4 - Term four = solver.mkInteger(4); - Term varX = solver.mkConst(solver.getIntegerSort(), "x"); - Term varY = solver.mkConst(solver.getIntegerSort(), "y"); - Term assertion1 = solver.mkTerm(Kind.EQUAL, solver.mkTerm(Kind.MULT, varX, varY), four); - Term assertion2 = solver.mkTerm(Kind.EQUAL, solver.mkTerm(Kind.ADD, varX, varY), four); + Term four = termManager.mkInteger(4); + Term varX = termManager.mkConst(termManager.getIntegerSort(), "x"); + Term varY = termManager.mkConst(termManager.getIntegerSort(), "y"); + Term assertion1 = + termManager.mkTerm(Kind.EQUAL, termManager.mkTerm(Kind.MULT, varX, varY), four); + Term assertion2 = + termManager.mkTerm(Kind.EQUAL, termManager.mkTerm(Kind.ADD, varX, varY), four); solver.assertFormula(assertion1); solver.assertFormula(assertion2); Result satCheck = solver.checkSat(); @@ -294,11 +304,12 @@ private int getInt(Term cvc5Term) { @Test public void checkSimpleLIAUnsat() { // x + y = 1 AND x * y = 1 - Term one = solver.mkInteger(1); - Term varX = solver.mkConst(solver.getIntegerSort(), "x"); - Term varY = solver.mkConst(solver.getIntegerSort(), "y"); - Term assertion1 = solver.mkTerm(Kind.EQUAL, solver.mkTerm(Kind.MULT, varX, varY), one); - Term assertion2 = solver.mkTerm(Kind.EQUAL, solver.mkTerm(Kind.ADD, varX, varY), one); + Term one = termManager.mkInteger(1); + Term varX = termManager.mkConst(termManager.getIntegerSort(), "x"); + Term varY = termManager.mkConst(termManager.getIntegerSort(), "y"); + Term assertion1 = + termManager.mkTerm(Kind.EQUAL, termManager.mkTerm(Kind.MULT, varX, varY), one); + Term assertion2 = termManager.mkTerm(Kind.EQUAL, termManager.mkTerm(Kind.ADD, varX, varY), one); solver.assertFormula(assertion1); solver.assertFormula(assertion2); Result satCheck = solver.checkSat(); @@ -309,10 +320,10 @@ public void checkSimpleLIAUnsat() { public void checkLIAModel() { // 1 + 2 = var // it follows that var = 3 - Term one = solver.mkInteger(1); - Term two = solver.mkInteger(2); - Term var = solver.mkConst(solver.getIntegerSort()); - Term assertion = solver.mkTerm(Kind.EQUAL, solver.mkTerm(Kind.ADD, one, two), var); + Term one = termManager.mkInteger(1); + Term two = termManager.mkInteger(2); + Term var = termManager.mkConst(termManager.getIntegerSort()); + Term assertion = termManager.mkTerm(Kind.EQUAL, termManager.mkTerm(Kind.ADD, one, two), var); solver.assertFormula(assertion); Result result = solver.checkSat(); assertThat(result.isSat()).isTrue(); @@ -324,11 +335,13 @@ public void checkLIAModel() { @Test public void checkSimpleLIRAUnsat2() { // x + y = 4 AND x * y = 4 - Term threeHalf = solver.mkReal(3, 2); - Term varX = solver.mkConst(solver.getRealSort(), "x"); - Term varY = solver.mkConst(solver.getRealSort(), "y"); - Term assertion1 = solver.mkTerm(Kind.EQUAL, solver.mkTerm(Kind.MULT, varX, varY), threeHalf); - Term assertion2 = solver.mkTerm(Kind.EQUAL, solver.mkTerm(Kind.ADD, varX, varY), threeHalf); + Term threeHalf = termManager.mkReal(3, 2); + Term varX = termManager.mkConst(termManager.getRealSort(), "x"); + Term varY = termManager.mkConst(termManager.getRealSort(), "y"); + Term assertion1 = + termManager.mkTerm(Kind.EQUAL, termManager.mkTerm(Kind.MULT, varX, varY), threeHalf); + Term assertion2 = + termManager.mkTerm(Kind.EQUAL, termManager.mkTerm(Kind.ADD, varX, varY), threeHalf); solver.assertFormula(assertion1); solver.assertFormula(assertion2); Result satCheck = solver.checkSat(); @@ -338,15 +351,16 @@ public void checkSimpleLIRAUnsat2() { @Test public void checkSimpleLIRASat() { // x + y = 8/5 AND x > 0 AND y > 0 AND x < 8/5 AND y < 8/5 - Term zero = solver.mkReal(0); - Term eightFifth = solver.mkReal(8, 5); - Term varX = solver.mkConst(solver.getRealSort(), "x"); - Term varY = solver.mkConst(solver.getRealSort(), "y"); - Term assertion1 = solver.mkTerm(Kind.GT, varX, zero); - Term assertion2 = solver.mkTerm(Kind.GT, varY, zero); - Term assertion3 = solver.mkTerm(Kind.LT, varX, eightFifth); - Term assertion4 = solver.mkTerm(Kind.LT, varY, eightFifth); - Term assertion5 = solver.mkTerm(Kind.EQUAL, solver.mkTerm(Kind.ADD, varX, varY), eightFifth); + Term zero = termManager.mkReal(0); + Term eightFifth = termManager.mkReal(8, 5); + Term varX = termManager.mkConst(termManager.getRealSort(), "x"); + Term varY = termManager.mkConst(termManager.getRealSort(), "y"); + Term assertion1 = termManager.mkTerm(Kind.GT, varX, zero); + Term assertion2 = termManager.mkTerm(Kind.GT, varY, zero); + Term assertion3 = termManager.mkTerm(Kind.LT, varX, eightFifth); + Term assertion4 = termManager.mkTerm(Kind.LT, varY, eightFifth); + Term assertion5 = + termManager.mkTerm(Kind.EQUAL, termManager.mkTerm(Kind.ADD, varX, varY), eightFifth); solver.assertFormula(assertion1); solver.assertFormula(assertion2); solver.assertFormula(assertion3); @@ -360,13 +374,14 @@ public void checkSimpleLIRASat() { @Test public void checkSimpleLRASat() { // x * y = 8/5 AND x < 4/5 - Term fourFifth = solver.mkReal(4, 5); - Term eightFifth = solver.mkReal(8, 5); - Term varX = solver.mkConst(solver.getRealSort(), "x"); - Term varY = solver.mkConst(solver.getRealSort(), "y"); + Term fourFifth = termManager.mkReal(4, 5); + Term eightFifth = termManager.mkReal(8, 5); + Term varX = termManager.mkConst(termManager.getRealSort(), "x"); + Term varY = termManager.mkConst(termManager.getRealSort(), "y"); - Term assertion1 = solver.mkTerm(Kind.EQUAL, solver.mkTerm(Kind.MULT, varX, varY), eightFifth); - Term assertion2 = solver.mkTerm(Kind.LT, varX, fourFifth); + Term assertion1 = + termManager.mkTerm(Kind.EQUAL, termManager.mkTerm(Kind.MULT, varX, varY), eightFifth); + Term assertion2 = termManager.mkTerm(Kind.LT, varX, fourFifth); solver.assertFormula(assertion1); solver.assertFormula(assertion2); @@ -378,13 +393,14 @@ public void checkSimpleLRASat() { @Test public void checkSimplePow() { // x ^ 2 = 4 AND x ^ 3 = 8 - Term two = solver.mkReal(2); - Term three = solver.mkReal(3); - Term four = solver.mkReal(4); - Term eight = solver.mkReal(8); - Term varX = solver.mkConst(solver.getRealSort(), "x"); - Term assertion1 = solver.mkTerm(Kind.EQUAL, solver.mkTerm(Kind.POW, varX, two), four); - Term assertion2 = solver.mkTerm(Kind.EQUAL, solver.mkTerm(Kind.POW, varX, three), eight); + Term two = termManager.mkReal(2); + Term three = termManager.mkReal(3); + Term four = termManager.mkReal(4); + Term eight = termManager.mkReal(8); + Term varX = termManager.mkConst(termManager.getRealSort(), "x"); + Term assertion1 = termManager.mkTerm(Kind.EQUAL, termManager.mkTerm(Kind.POW, varX, two), four); + Term assertion2 = + termManager.mkTerm(Kind.EQUAL, termManager.mkTerm(Kind.POW, varX, three), eight); solver.assertFormula(assertion1); solver.assertFormula(assertion2); Result satCheck = solver.checkSat(); @@ -396,16 +412,16 @@ public void checkSimplePow() { @Test public void checkSimpleFPSat() throws CVC5ApiException { // x * y = 1/4 - Term rmTerm = solver.mkRoundingMode(RoundingMode.ROUND_NEAREST_TIES_TO_AWAY); - Op mkRealOp = solver.mkOp(Kind.FLOATINGPOINT_TO_FP_FROM_REAL, 8, 24); - Term oneFourth = solver.mkTerm(mkRealOp, rmTerm, solver.mkReal(1, 4)); + Term rmTerm = termManager.mkRoundingMode(RoundingMode.ROUND_NEAREST_TIES_TO_AWAY); + Op mkRealOp = termManager.mkOp(Kind.FLOATINGPOINT_TO_FP_FROM_REAL, 8, 24); + Term oneFourth = termManager.mkTerm(mkRealOp, rmTerm, termManager.mkReal(1, 4)); - Term varX = solver.mkConst(solver.mkFloatingPointSort(8, 24), "x"); - Term varY = solver.mkConst(solver.mkFloatingPointSort(8, 24), "y"); + Term varX = termManager.mkConst(termManager.mkFloatingPointSort(8, 24), "x"); + Term varY = termManager.mkConst(termManager.mkFloatingPointSort(8, 24), "y"); Term assertion1 = - solver.mkTerm( + termManager.mkTerm( Kind.FLOATINGPOINT_EQ, - solver.mkTerm(Kind.FLOATINGPOINT_MULT, rmTerm, varX, varY), + termManager.mkTerm(Kind.FLOATINGPOINT_MULT, rmTerm, varX, varY), oneFourth); solver.assertFormula(assertion1); @@ -416,20 +432,20 @@ public void checkSimpleFPSat() throws CVC5ApiException { @Test public void checkSimpleFPUnsat() throws CVC5ApiException { // x * y = 1/4 AND x > 0 AND y < 0 - Term rmTerm = solver.mkRoundingMode(RoundingMode.ROUND_NEAREST_TIES_TO_AWAY); - Op mkRealOp = solver.mkOp(Kind.FLOATINGPOINT_TO_FP_FROM_REAL, 8, 24); - Term oneFourth = solver.mkTerm(mkRealOp, rmTerm, solver.mkReal(1, 4)); - Term zero = solver.mkTerm(mkRealOp, rmTerm, solver.mkReal(0)); + Term rmTerm = termManager.mkRoundingMode(RoundingMode.ROUND_NEAREST_TIES_TO_AWAY); + Op mkRealOp = termManager.mkOp(Kind.FLOATINGPOINT_TO_FP_FROM_REAL, 8, 24); + Term oneFourth = termManager.mkTerm(mkRealOp, rmTerm, termManager.mkReal(1, 4)); + Term zero = termManager.mkTerm(mkRealOp, rmTerm, termManager.mkReal(0)); - Term varX = solver.mkConst(solver.mkFloatingPointSort(8, 24), "x"); - Term varY = solver.mkConst(solver.mkFloatingPointSort(8, 24), "y"); + Term varX = termManager.mkConst(termManager.mkFloatingPointSort(8, 24), "x"); + Term varY = termManager.mkConst(termManager.mkFloatingPointSort(8, 24), "y"); Term assertion1 = - solver.mkTerm( + termManager.mkTerm( Kind.FLOATINGPOINT_EQ, - solver.mkTerm(Kind.FLOATINGPOINT_MULT, rmTerm, varX, varY), + termManager.mkTerm(Kind.FLOATINGPOINT_MULT, rmTerm, varX, varY), oneFourth); - Term assertion2 = solver.mkTerm(Kind.FLOATINGPOINT_GT, varX, zero); - Term assertion3 = solver.mkTerm(Kind.FLOATINGPOINT_LT, varY, zero); + Term assertion2 = termManager.mkTerm(Kind.FLOATINGPOINT_GT, varX, zero); + Term assertion3 = termManager.mkTerm(Kind.FLOATINGPOINT_LT, varY, zero); solver.assertFormula(assertion1); solver.assertFormula(assertion2); solver.assertFormula(assertion3); @@ -440,18 +456,20 @@ public void checkSimpleFPUnsat() throws CVC5ApiException { @Test public void checkSimpleLRAUnsat() { // x + y = x * y AND x - 1 = 0 - Term zero = solver.mkInteger(0); - Term one = solver.mkInteger(1); - Term varX = solver.mkConst(solver.getRealSort(), "x"); - Term varY = solver.mkConst(solver.getRealSort(), "y"); + Term zero = termManager.mkInteger(0); + Term one = termManager.mkInteger(1); + Term varX = termManager.mkConst(termManager.getRealSort(), "x"); + Term varY = termManager.mkConst(termManager.getRealSort(), "y"); Term assertion1 = - solver.mkTerm( - Kind.EQUAL, solver.mkTerm(Kind.MULT, varX, varY), solver.mkTerm(Kind.ADD, varX, varY)); + termManager.mkTerm( + Kind.EQUAL, + termManager.mkTerm(Kind.MULT, varX, varY), + termManager.mkTerm(Kind.ADD, varX, varY)); Term assertion2 = - solver.mkTerm( + termManager.mkTerm( Kind.EQUAL, - solver.mkTerm(Kind.SUB, varX, solver.mkTerm(Kind.TO_REAL, one)), - solver.mkTerm(Kind.TO_REAL, zero)); + termManager.mkTerm(Kind.SUB, varX, termManager.mkTerm(Kind.TO_REAL, one)), + termManager.mkTerm(Kind.TO_REAL, zero)); solver.assertFormula(assertion1); solver.assertFormula(assertion2); Result satCheck = solver.checkSat(); @@ -461,11 +479,13 @@ public void checkSimpleLRAUnsat() { @Test public void checkSimpleLRAUnsat2() { // x + y = 3/2 AND x * y = 3/2 - Term threeHalf = solver.mkReal(3, 2); - Term varX = solver.mkConst(solver.getRealSort(), "x"); - Term varY = solver.mkConst(solver.getRealSort(), "y"); - Term assertion1 = solver.mkTerm(Kind.EQUAL, solver.mkTerm(Kind.MULT, varX, varY), threeHalf); - Term assertion2 = solver.mkTerm(Kind.EQUAL, solver.mkTerm(Kind.ADD, varX, varY), threeHalf); + Term threeHalf = termManager.mkReal(3, 2); + Term varX = termManager.mkConst(termManager.getRealSort(), "x"); + Term varY = termManager.mkConst(termManager.getRealSort(), "y"); + Term assertion1 = + termManager.mkTerm(Kind.EQUAL, termManager.mkTerm(Kind.MULT, varX, varY), threeHalf); + Term assertion2 = + termManager.mkTerm(Kind.EQUAL, termManager.mkTerm(Kind.ADD, varX, varY), threeHalf); solver.assertFormula(assertion1); solver.assertFormula(assertion2); Result satCheck = solver.checkSat(); @@ -475,22 +495,25 @@ public void checkSimpleLRAUnsat2() { @Test public void checkSimpleIncrementalSolving() throws CVC5ApiException { // x + y = 3/2 AND x * y = 3/2 (AND x - 1 = 0) - Term zero = solver.mkInteger(0); - Term one = solver.mkInteger(1); - Term threeHalf = solver.mkReal(3, 2); - Term varX = solver.mkConst(solver.getRealSort(), "x"); - Term varY = solver.mkConst(solver.getRealSort(), "y"); + Term zero = termManager.mkInteger(0); + Term one = termManager.mkInteger(1); + Term threeHalf = termManager.mkReal(3, 2); + Term varX = termManager.mkConst(termManager.getRealSort(), "x"); + Term varY = termManager.mkConst(termManager.getRealSort(), "y"); // this alone is SAT Term assertion1 = - solver.mkTerm( - Kind.EQUAL, solver.mkTerm(Kind.MULT, varX, varY), solver.mkTerm(Kind.ADD, varX, varY)); + termManager.mkTerm( + Kind.EQUAL, + termManager.mkTerm(Kind.MULT, varX, varY), + termManager.mkTerm(Kind.ADD, varX, varY)); // both 2 and 3 make it UNSAT (either one) - Term assertion2 = solver.mkTerm(Kind.EQUAL, solver.mkTerm(Kind.ADD, varX, varY), threeHalf); + Term assertion2 = + termManager.mkTerm(Kind.EQUAL, termManager.mkTerm(Kind.ADD, varX, varY), threeHalf); Term assertion3 = - solver.mkTerm( + termManager.mkTerm( Kind.EQUAL, - solver.mkTerm(Kind.SUB, varX, solver.mkTerm(Kind.TO_REAL, one)), - solver.mkTerm(Kind.TO_REAL, zero)); + termManager.mkTerm(Kind.SUB, varX, termManager.mkTerm(Kind.TO_REAL, one)), + termManager.mkTerm(Kind.TO_REAL, zero)); solver.push(); solver.assertFormula(assertion1); Result satCheck = solver.checkSat(); @@ -514,7 +537,7 @@ public void checkSimpleIncrementalSolving() throws CVC5ApiException { /** Note that model and getValue are seperate! */ @Test public void checkInvalidModelGetValue() { - Term assertion = solver.mkBoolean(false); + Term assertion = termManager.mkBoolean(false); solver.assertFormula(assertion); Result result = solver.checkSat(); assertThat(result.isSat()).isFalse(); @@ -527,9 +550,9 @@ public void checkInvalidModelGetValue() { /** The getModel() call needs an array of sorts and terms. */ @Test public void checkGetModelUnsat() { - Term assertion = solver.mkBoolean(false); + Term assertion = termManager.mkBoolean(false); solver.assertFormula(assertion); - Sort[] sorts = new Sort[] {solver.getBooleanSort()}; + Sort[] sorts = new Sort[] {termManager.getBooleanSort()}; Term[] terms = new Term[] {assertion}; Result result = solver.checkSat(); assertThat(result.isSat()).isFalse(); @@ -548,22 +571,22 @@ public void checkGetModelUnsat() { */ @Test public void checkGetModelSatInvalidSort() { - Term assertion = solver.mkBoolean(true); + Term assertion = termManager.mkBoolean(true); solver.assertFormula(assertion); - Sort[] sorts = new Sort[] {solver.getBooleanSort()}; + Sort[] sorts = new Sort[] {termManager.getBooleanSort()}; Term[] terms = new Term[] {assertion}; Result result = solver.checkSat(); assertThat(result.isSat()).isTrue(); Exception e = assertThrows( io.github.cvc5.CVC5ApiRecoverableException.class, () -> solver.getModel(sorts, terms)); - assertThat(e.toString()).contains("Expecting an uninterpreted sort as argument to getModel."); + assertThat(e.toString()).contains("expected an uninterpreted sort as argument to getModel."); } /** Same as checkGetModelSatInvalidSort but with invalid term. */ @Test public void checkGetModelSatInvalidTerm() { - Term assertion = solver.mkBoolean(true); + Term assertion = termManager.mkBoolean(true); solver.assertFormula(assertion); Sort[] sorts = new Sort[] {}; Term[] terms = new Term[] {assertion}; @@ -572,12 +595,12 @@ public void checkGetModelSatInvalidTerm() { Exception e = assertThrows( io.github.cvc5.CVC5ApiRecoverableException.class, () -> solver.getModel(sorts, terms)); - assertThat(e.toString()).contains("Expecting a free constant as argument to getModel."); + assertThat(e.toString()).contains("expected a free constant as argument to getModel."); } @Test public void checkGetModelSat() { - Term assertion = solver.mkConst(solver.getBooleanSort()); + Term assertion = termManager.mkConst(termManager.getBooleanSort()); solver.assertFormula(assertion); Sort[] sorts = new Sort[] {}; Term[] terms = new Term[] {assertion}; @@ -594,7 +617,7 @@ public void checkGetModelSat() { */ @Test public void checkInvalidGetModel() { - Term assertion = solver.mkBoolean(false); + Term assertion = termManager.mkBoolean(false); solver.assertFormula(assertion); Result result = solver.checkSat(); assertThat(result.isSat()).isFalse(); @@ -606,9 +629,9 @@ public void checkInvalidGetModel() { /** It does not matter if you take an int or array or bv here, all result in the same error. */ @Test public void checkInvalidTypeOperationsAssert() throws CVC5ApiException { - Sort bvSort = solver.mkBitVectorSort(16); - Term bvVar = solver.mkConst(bvSort, "bla"); - Term assertion = solver.mkTerm(Kind.BITVECTOR_AND, bvVar, bvVar); + Sort bvSort = termManager.mkBitVectorSort(16); + Term bvVar = termManager.mkConst(bvSort, "bla"); + Term assertion = termManager.mkTerm(Kind.BITVECTOR_AND, bvVar, bvVar); Exception e = assertThrows(io.github.cvc5.CVC5ApiException.class, () -> solver.assertFormula(assertion)); @@ -618,50 +641,54 @@ public void checkInvalidTypeOperationsAssert() throws CVC5ApiException { /** It does not matter if you take an int or array or bv here, all result in the same error. */ @Test public void checkInvalidTypeOperationsCheckSat() throws CVC5ApiException { - Sort bvSort = solver.mkBitVectorSort(16); - Term bvVar = solver.mkConst(bvSort); - Term intVar = solver.mkConst(solver.getIntegerSort()); + Sort bvSort = termManager.mkBitVectorSort(16); + Term bvVar = termManager.mkConst(bvSort); + Term intVar = termManager.mkConst(termManager.getIntegerSort()); Term arrayVar = - solver.mkConst(solver.mkArraySort(solver.getIntegerSort(), solver.getIntegerSort())); + termManager.mkConst( + termManager.mkArraySort(termManager.getIntegerSort(), termManager.getIntegerSort())); Exception e = assertThrows( - io.github.cvc5.CVC5ApiException.class, () -> solver.mkTerm(Kind.AND, bvVar, bvVar)); + io.github.cvc5.CVC5ApiException.class, + () -> termManager.mkTerm(Kind.AND, bvVar, bvVar)); assertThat(e.toString()).contains("expecting a Boolean subexpression"); e = assertThrows( - io.github.cvc5.CVC5ApiException.class, () -> solver.mkTerm(Kind.AND, intVar, intVar)); + io.github.cvc5.CVC5ApiException.class, + () -> termManager.mkTerm(Kind.AND, intVar, intVar)); assertThat(e.toString()).contains("expecting a Boolean subexpression"); e = assertThrows( io.github.cvc5.CVC5ApiException.class, - () -> solver.mkTerm(Kind.AND, arrayVar, arrayVar)); + () -> termManager.mkTerm(Kind.AND, arrayVar, arrayVar)); assertThat(e.toString()).contains("expecting a Boolean subexpression"); } @Test public void checkBvInvalidZeroWidthAssertion() { Exception e = - assertThrows(io.github.cvc5.CVC5ApiException.class, () -> solver.mkBitVector(0, 1)); - assertThat(e.toString()).contains("Invalid argument '0' for 'size', expected a bit-width > 0"); + assertThrows(io.github.cvc5.CVC5ApiException.class, () -> termManager.mkBitVector(0, 1)); + assertThat(e.toString()).contains("invalid argument '0' for 'size', expected a bit-width > 0"); } @Test public void checkBvInvalidNegativeWidthCheckAssertion() { Exception e = - assertThrows(io.github.cvc5.CVC5ApiException.class, () -> solver.mkBitVector(-1, 1)); + assertThrows(io.github.cvc5.CVC5ApiException.class, () -> termManager.mkBitVector(-1, 1)); assertThat(e.toString()).contains("Expected size '-1' to be non negative."); } @Test public void checkSimpleBvEqualitySat() throws CVC5ApiException { // 1 + 0 = 1 with bitvectors - Term bvOne = solver.mkBitVector(16, 1); - Term bvZero = solver.mkBitVector(16, 0); + Term bvOne = termManager.mkBitVector(16, 1); + Term bvZero = termManager.mkBitVector(16, 0); Term assertion = - solver.mkTerm(Kind.EQUAL, solver.mkTerm(Kind.BITVECTOR_ADD, bvZero, bvOne), bvOne); + termManager.mkTerm( + Kind.EQUAL, termManager.mkTerm(Kind.BITVECTOR_ADD, bvZero, bvOne), bvOne); solver.assertFormula(assertion); Result satCheck = solver.checkSat(); assertThat(satCheck.isSat()).isTrue(); @@ -670,11 +697,12 @@ public void checkSimpleBvEqualitySat() throws CVC5ApiException { @Test public void checkSimpleBvEqualityUnsat() throws CVC5ApiException { // 0 + 1 = 2 UNSAT with bitvectors - Term bvZero = solver.mkBitVector(16, 0); - Term bvOne = solver.mkBitVector(16, 1); - Term bvTwo = solver.mkBitVector(16, 2); + Term bvZero = termManager.mkBitVector(16, 0); + Term bvOne = termManager.mkBitVector(16, 1); + Term bvTwo = termManager.mkBitVector(16, 2); Term assertion = - solver.mkTerm(Kind.EQUAL, solver.mkTerm(Kind.BITVECTOR_ADD, bvZero, bvOne), bvTwo); + termManager.mkTerm( + Kind.EQUAL, termManager.mkTerm(Kind.BITVECTOR_ADD, bvZero, bvOne), bvTwo); solver.assertFormula(assertion); Result satCheck = solver.checkSat(); assertThat(satCheck.isSat()).isFalse(); @@ -685,14 +713,15 @@ public void checkSimpleBvUnsat() throws CVC5ApiException { // var + 1 = 0 & var < max bitvector & var > 0; both < and > signed // Because of bitvector nature its UNSAT now - Term bvVar = solver.mkConst(solver.mkBitVectorSort(16), "bvVar"); - Term bvOne = solver.mkBitVector(16, 1); - Term bvZero = solver.mkBitVector(16, 0); + Term bvVar = termManager.mkConst(termManager.mkBitVectorSort(16), "bvVar"); + Term bvOne = termManager.mkBitVector(16, 1); + Term bvZero = termManager.mkBitVector(16, 0); Term assertion1 = - solver.mkTerm(Kind.EQUAL, solver.mkTerm(Kind.BITVECTOR_ADD, bvVar, bvOne), bvZero); + termManager.mkTerm( + Kind.EQUAL, termManager.mkTerm(Kind.BITVECTOR_ADD, bvVar, bvOne), bvZero); // mkMaxSigned(16); - Term assertion2 = solver.mkTerm(Kind.BITVECTOR_SLT, bvVar, makeMaxCVC5Bitvector(16, true)); - Term assertion3 = solver.mkTerm(Kind.BITVECTOR_SGT, bvVar, bvZero); + Term assertion2 = termManager.mkTerm(Kind.BITVECTOR_SLT, bvVar, makeMaxCVC5Bitvector(16, true)); + Term assertion3 = termManager.mkTerm(Kind.BITVECTOR_SGT, bvVar, bvZero); solver.assertFormula(assertion1); solver.assertFormula(assertion2); solver.assertFormula(assertion3); @@ -702,15 +731,15 @@ public void checkSimpleBvUnsat() throws CVC5ApiException { @Ignore public void checkBvDistinct() throws CVC5ApiException { - Sort bvSort = solver.mkBitVectorSort(6); + Sort bvSort = termManager.mkBitVectorSort(6); List bvs = new ArrayList<>(); for (int i = 0; i < 64; i++) { - bvs.add(solver.mkConst(bvSort, "a" + i + "_")); + bvs.add(termManager.mkConst(bvSort, "a" + i + "_")); } // TODO: this got worse in the 1.0.0 release and now this runs endlessly as well, check in later // version again. - Term distinct2 = solver.mkTerm(Kind.DISTINCT, bvs.toArray(new Term[0])); + Term distinct2 = termManager.mkTerm(Kind.DISTINCT, bvs.toArray(new Term[0])); solver.assertFormula(distinct2); assertThat(solver.checkSat().isSat()).isTrue(); solver.resetAssertions(); @@ -732,17 +761,18 @@ public void checkQuantifierExistsIncomplete() { // (not exists x . not b[x] = 0) AND (b[123] = 0) is SAT setupArrayQuant(); - Term zero = solver.mkInteger(0); + Term zero = termManager.mkInteger(0); - Term xBound = solver.mkVar(solver.getIntegerSort(), "x"); - Term quantifiedVars = solver.mkTerm(Kind.VARIABLE_LIST, xBound); + Term xBound = termManager.mkVar(termManager.getIntegerSort(), "x"); + Term quantifiedVars = termManager.mkTerm(Kind.VARIABLE_LIST, xBound); Term aAtxEq0s = aAtxEq0.substitute(x, xBound); - Term exists = solver.mkTerm(Kind.EXISTS, quantifiedVars, solver.mkTerm(Kind.NOT, aAtxEq0s)); - Term notExists = solver.mkTerm(Kind.NOT, exists); + Term exists = + termManager.mkTerm(Kind.EXISTS, quantifiedVars, termManager.mkTerm(Kind.NOT, aAtxEq0s)); + Term notExists = termManager.mkTerm(Kind.NOT, exists); - Term select123 = solver.mkTerm(Kind.SELECT, array, solver.mkInteger(123)); - Term selectEq0 = solver.mkTerm(Kind.EQUAL, select123, zero); - Term assertion = solver.mkTerm(Kind.AND, notExists, selectEq0); + Term select123 = termManager.mkTerm(Kind.SELECT, array, termManager.mkInteger(123)); + Term selectEq0 = termManager.mkTerm(Kind.EQUAL, select123, zero); + Term assertion = termManager.mkTerm(Kind.AND, notExists, selectEq0); // CVC5 does not allow non quantifier formulas as the top most formula Exception e = @@ -756,57 +786,58 @@ public void checkQuantifierEliminationLIA() { // quantifier-free equivalent: (2 < y) or (>= y 3) setupArrayQuant(); - Term three = solver.mkInteger(3); - Term five = solver.mkInteger(5); - Term seven = solver.mkInteger(7); + Term three = termManager.mkInteger(3); + Term five = termManager.mkInteger(5); + Term seven = termManager.mkInteger(7); - Term y = solver.mkConst(solver.getIntegerSort(), "y"); + Term y = termManager.mkConst(termManager.getIntegerSort(), "y"); - Term first = solver.mkTerm(Kind.LT, x, five); - Term second = solver.mkTerm(Kind.LT, seven, solver.mkTerm(Kind.ADD, x, y)); - Term body = solver.mkTerm(Kind.OR, first, second); + Term first = termManager.mkTerm(Kind.LT, x, five); + Term second = termManager.mkTerm(Kind.LT, seven, termManager.mkTerm(Kind.ADD, x, y)); + Term body = termManager.mkTerm(Kind.OR, first, second); - Term xBound = solver.mkVar(solver.getIntegerSort(), "xBound"); - Term quantifiedVars = solver.mkTerm(Kind.VARIABLE_LIST, xBound); + Term xBound = termManager.mkVar(termManager.getIntegerSort(), "xBound"); + Term quantifiedVars = termManager.mkTerm(Kind.VARIABLE_LIST, xBound); Term bodySubst = body.substitute(x, xBound); - Term assertion = solver.mkTerm(Kind.FORALL, quantifiedVars, bodySubst); + Term assertion = termManager.mkTerm(Kind.FORALL, quantifiedVars, bodySubst); Term result = solver.getQuantifierElimination(assertion); - Term resultCheck = solver.mkTerm(Kind.GEQ, y, three); + Term resultCheck = termManager.mkTerm(Kind.GEQ, y, three); assertThat(result.toString()).isEqualTo(resultCheck.toString()); } @Test public void checkQuantifierAndModelWithUf() throws CVC5ApiException { - Term var = solver.mkConst(solver.getIntegerSort(), "var"); + Term var = termManager.mkConst(termManager.getIntegerSort(), "var"); // start with a normal, free variable! - Term boundVar = solver.mkConst(solver.getIntegerSort(), "boundVar"); - Term varIsOne = solver.mkTerm(Kind.EQUAL, var, solver.mkInteger(4)); + Term boundVar = termManager.mkConst(termManager.getIntegerSort(), "boundVar"); + Term varIsOne = termManager.mkTerm(Kind.EQUAL, var, termManager.mkInteger(4)); // try not to use 0 as this is the default value for CVC5 models - Term boundVarIsTwo = solver.mkTerm(Kind.EQUAL, boundVar, solver.mkInteger(2)); - Term boundVarIsThree = solver.mkTerm(Kind.EQUAL, boundVar, solver.mkInteger(3)); + Term boundVarIsTwo = termManager.mkTerm(Kind.EQUAL, boundVar, termManager.mkInteger(2)); + Term boundVarIsThree = termManager.mkTerm(Kind.EQUAL, boundVar, termManager.mkInteger(3)); String func = "func"; - Sort intSort = solver.getIntegerSort(); + Sort intSort = termManager.getIntegerSort(); - Sort ufSort = solver.mkFunctionSort(intSort, intSort); - Term uf = solver.mkConst(ufSort, func); - Term funcAtBoundVar = solver.mkTerm(Kind.APPLY_UF, uf, boundVar); + Sort ufSort = termManager.mkFunctionSort(intSort, intSort); + Term uf = termManager.mkConst(ufSort, func); + Term funcAtBoundVar = termManager.mkTerm(Kind.APPLY_UF, uf, boundVar); Term body = - solver.mkTerm(Kind.AND, boundVarIsTwo, solver.mkTerm(Kind.EQUAL, var, funcAtBoundVar)); + termManager.mkTerm( + Kind.AND, boundVarIsTwo, termManager.mkTerm(Kind.EQUAL, var, funcAtBoundVar)); // This is the bound variable used for boundVar - Term boundVarBound = solver.mkVar(solver.getIntegerSort(), "boundVar"); - Term quantifiedVars = solver.mkTerm(Kind.VARIABLE_LIST, boundVarBound); + Term boundVarBound = termManager.mkVar(termManager.getIntegerSort(), "boundVar"); + Term quantifiedVars = termManager.mkTerm(Kind.VARIABLE_LIST, boundVarBound); // Subst all boundVar variables with the bound version Term bodySubst = body.substitute(boundVar, boundVarBound); - Term quantFormula = solver.mkTerm(Kind.EXISTS, quantifiedVars, bodySubst); + Term quantFormula = termManager.mkTerm(Kind.EXISTS, quantifiedVars, bodySubst); // var = 4 & boundVar = 3 & exists boundVar . ( boundVar = 2 & f(boundVar) = var ) - Term overallFormula = solver.mkTerm(Kind.AND, varIsOne, boundVarIsThree, quantFormula); + Term overallFormula = termManager.mkTerm(Kind.AND, varIsOne, boundVarIsThree, quantFormula); solver.assertFormula(overallFormula); @@ -826,7 +857,7 @@ public void checkQuantifierAndModelWithUf() throws CVC5ApiException { assertThat(solver.getValue(body).toString()).isEqualTo("false"); // The function is a applied uf assertThat(funcAtBoundVar.getKind()).isEqualTo(Kind.APPLY_UF); - assertThat(funcAtBoundVar.getSort()).isEqualTo(solver.getIntegerSort()); + assertThat(funcAtBoundVar.getSort()).isEqualTo(termManager.getIntegerSort()); assertThat(funcAtBoundVar.hasSymbol()).isFalse(); assertThat(solver.getValue(funcAtBoundVar).toString()).isEqualTo("4"); // The function has 2 children, 1st is the function, 2nd is the argument @@ -882,12 +913,12 @@ public void checkQuantifierAndModelWithUf() throws CVC5ApiException { @Test public void checkArrayQuantElim() { setupArrayQuant(); - Term body = solver.mkTerm(Kind.OR, aAtxEq0, aAtxEq1); + Term body = termManager.mkTerm(Kind.OR, aAtxEq0, aAtxEq1); - Term xBound = solver.mkVar(solver.getIntegerSort(), "x_b"); - Term quantifiedVars = solver.mkTerm(Kind.VARIABLE_LIST, xBound); + Term xBound = termManager.mkVar(termManager.getIntegerSort(), "x_b"); + Term quantifiedVars = termManager.mkTerm(Kind.VARIABLE_LIST, xBound); Term bodySubst = body.substitute(x, xBound); - Term assertion = solver.mkTerm(Kind.FORALL, quantifiedVars, bodySubst); + Term assertion = termManager.mkTerm(Kind.FORALL, quantifiedVars, bodySubst); Term result = solver.getQuantifierElimination(assertion); String resultString = @@ -907,46 +938,42 @@ public void checkQuantifierEliminationBV() throws CVC5ApiException { int width = 2; - Term xBv = solver.mkConst(solver.mkBitVectorSort(width), "x_bv"); - Term yBv = solver.mkConst(solver.mkBitVectorSort(width), "y_bv"); - Term mult = solver.mkTerm(Kind.BITVECTOR_MULT, xBv, yBv); - Term body = solver.mkTerm(Kind.EQUAL, mult, solver.mkBitVector(2, 1)); + Term xBv = termManager.mkConst(termManager.mkBitVectorSort(width), "x_bv"); + Term yBv = termManager.mkConst(termManager.mkBitVectorSort(width), "y_bv"); + Term mult = termManager.mkTerm(Kind.BITVECTOR_MULT, xBv, yBv); + Term body = termManager.mkTerm(Kind.EQUAL, mult, termManager.mkBitVector(2, 1)); - Term xBound = solver.mkVar(solver.mkBitVectorSort(width), "y_bv"); - Term quantifiedVars = solver.mkTerm(Kind.VARIABLE_LIST, xBound); + Term xBound = termManager.mkVar(termManager.mkBitVectorSort(width), "y_bv"); + Term quantifiedVars = termManager.mkTerm(Kind.VARIABLE_LIST, xBound); Term bodySubst = body.substitute(yBv, xBound); - Term assertion = solver.mkTerm(Kind.EXISTS, quantifiedVars, bodySubst); + Term assertion = termManager.mkTerm(Kind.EXISTS, quantifiedVars, bodySubst); Term quantElim = solver.getQuantifierElimination(assertion); - assertThat(quantElim.toString()) - .isEqualTo( - "(= (bvmul x_bv (witness ((x0 (_ BitVec 2))) (or (= (bvmul x_bv x0) #b01) (not (=" - + " (concat #b0 ((_ extract 0 0) (bvor x_bv (bvneg x_bv)))) #b01))))) #b01)"); - - // TODO: formely you could get a better result Term by using getValue(). But now getValue() only - // works after SAT since 1.0.0 and then getValue() prints trivial statements like false. + assertThat(quantElim.toString()).isEqualTo("(or (= #b01 (bvneg x_bv)) (= #b01 x_bv))"); } @Test public void checkArraySat() { // ((x = 123) & (select(arr, 5) = 123)) => ((select(arr, 5) = x) & (x = 123)) - Term five = solver.mkInteger(5); - Term oneTwoThree = solver.mkInteger(123); + Term five = termManager.mkInteger(5); + Term oneTwoThree = termManager.mkInteger(123); - Term xInt = solver.mkConst(solver.getIntegerSort(), "x_int"); + Term xInt = termManager.mkConst(termManager.getIntegerSort(), "x_int"); - Sort arraySort = solver.mkArraySort(solver.getIntegerSort(), solver.getIntegerSort()); - Term arr = solver.mkConst(arraySort, "arr"); + Sort arraySort = + termManager.mkArraySort(termManager.getIntegerSort(), termManager.getIntegerSort()); + Term arr = termManager.mkConst(arraySort, "arr"); - Term xEq123 = solver.mkTerm(Kind.EQUAL, xInt, oneTwoThree); + Term xEq123 = termManager.mkTerm(Kind.EQUAL, xInt, oneTwoThree); Term selAat5Eq123 = - solver.mkTerm(Kind.EQUAL, solver.mkTerm(Kind.SELECT, arr, five), oneTwoThree); - Term selAat5EqX = solver.mkTerm(Kind.EQUAL, solver.mkTerm(Kind.SELECT, arr, five), xInt); + termManager.mkTerm(Kind.EQUAL, termManager.mkTerm(Kind.SELECT, arr, five), oneTwoThree); + Term selAat5EqX = + termManager.mkTerm(Kind.EQUAL, termManager.mkTerm(Kind.SELECT, arr, five), xInt); - Term leftAnd = solver.mkTerm(Kind.AND, xEq123, selAat5Eq123); - Term rightAnd = solver.mkTerm(Kind.AND, xEq123, selAat5EqX); - Term impl = solver.mkTerm(Kind.IMPLIES, leftAnd, rightAnd); + Term leftAnd = termManager.mkTerm(Kind.AND, xEq123, selAat5Eq123); + Term rightAnd = termManager.mkTerm(Kind.AND, xEq123, selAat5EqX); + Term impl = termManager.mkTerm(Kind.IMPLIES, leftAnd, rightAnd); solver.assertFormula(impl); Result satCheck = solver.checkSat(); @@ -956,22 +983,24 @@ public void checkArraySat() { @Test public void checkArrayUnsat() { // (x = 123) & (select(arr, 5) = 123) & (select(arr, 5) != x) - Term five = solver.mkInteger(5); - Term oneTwoThree = solver.mkInteger(123); + Term five = termManager.mkInteger(5); + Term oneTwoThree = termManager.mkInteger(123); - Term xInt = solver.mkConst(solver.getIntegerSort(), "x_int"); + Term xInt = termManager.mkConst(termManager.getIntegerSort(), "x_int"); - Sort arraySort = solver.mkArraySort(solver.getIntegerSort(), solver.getIntegerSort()); - Term arr = solver.mkConst(arraySort, "arr"); + Sort arraySort = + termManager.mkArraySort(termManager.getIntegerSort(), termManager.getIntegerSort()); + Term arr = termManager.mkConst(arraySort, "arr"); - Term xEq123 = solver.mkTerm(Kind.EQUAL, xInt, oneTwoThree); + Term xEq123 = termManager.mkTerm(Kind.EQUAL, xInt, oneTwoThree); Term selAat5Eq123 = - solver.mkTerm(Kind.EQUAL, solver.mkTerm(Kind.SELECT, arr, five), oneTwoThree); + termManager.mkTerm(Kind.EQUAL, termManager.mkTerm(Kind.SELECT, arr, five), oneTwoThree); Term selAat5NotEqX = - solver.mkTerm( - Kind.NOT, solver.mkTerm(Kind.EQUAL, solver.mkTerm(Kind.SELECT, arr, five), xInt)); + termManager.mkTerm( + Kind.NOT, + termManager.mkTerm(Kind.EQUAL, termManager.mkTerm(Kind.SELECT, arr, five), xInt)); - Term assertion = solver.mkTerm(Kind.AND, xEq123, selAat5Eq123, selAat5NotEqX); + Term assertion = termManager.mkTerm(Kind.AND, xEq123, selAat5Eq123, selAat5NotEqX); solver.assertFormula(assertion); Result satCheck = solver.checkSat(); @@ -986,12 +1015,12 @@ public void checkUnsatCore() { // Enable UNSAT Core first! solver.setOption("produce-unsat-cores", "true"); - Sort boolSort = solver.getBooleanSort(); - Term a = solver.mkConst(boolSort, "a"); - Term b = solver.mkConst(boolSort, "b"); + Sort boolSort = termManager.getBooleanSort(); + Term a = termManager.mkConst(boolSort, "a"); + Term b = termManager.mkConst(boolSort, "b"); - Term aAndb = solver.mkTerm(Kind.AND, a, b); - Term notaOrb = solver.mkTerm(Kind.NOT, solver.mkTerm(Kind.OR, a, b)); + Term aAndb = termManager.mkTerm(Kind.AND, a, b); + Term notaOrb = termManager.mkTerm(Kind.NOT, termManager.mkTerm(Kind.OR, a, b)); solver.assertFormula(aAndb); solver.assertFormula(notaOrb); @@ -1013,41 +1042,41 @@ public void checkCustomTypesAndUFs() { // f(x) + f(y) <= 1 // not p(0) // p(f(y)) - Term zero = solver.mkInteger(0); - Term one = solver.mkInteger(1); + Term zero = termManager.mkInteger(0); + Term one = termManager.mkInteger(1); - Sort boolSort = solver.getBooleanSort(); - Sort intSort = solver.getIntegerSort(); + Sort boolSort = termManager.getBooleanSort(); + Sort intSort = termManager.getIntegerSort(); // You may use custom sorts just like bool or int - Sort mySort = solver.mkParamSort("f"); + Sort mySort = termManager.mkParamSort("f"); // Sort for UFs later - Sort mySortToInt = solver.mkFunctionSort(mySort, intSort); - Sort intToBool = solver.mkFunctionSort(intSort, boolSort); + Sort mySortToInt = termManager.mkFunctionSort(mySort, intSort); + Sort intToBool = termManager.mkFunctionSort(intSort, boolSort); - Term xTyped = solver.mkConst(mySort, "x"); - Term yTyped = solver.mkConst(mySort, "y"); + Term xTyped = termManager.mkConst(mySort, "x"); + Term yTyped = termManager.mkConst(mySort, "y"); // declare UFs - Term f = solver.mkConst(mySortToInt, "f"); - Term p = solver.mkConst(intToBool, "p"); + Term f = termManager.mkConst(mySortToInt, "f"); + Term p = termManager.mkConst(intToBool, "p"); // Apply UFs - Term fx = solver.mkTerm(Kind.APPLY_UF, f, xTyped); - Term fy = solver.mkTerm(Kind.APPLY_UF, f, yTyped); - Term sum = solver.mkTerm(Kind.ADD, fx, fy); - Term p0 = solver.mkTerm(Kind.APPLY_UF, p, zero); - Term pfy = solver.mkTerm(Kind.APPLY_UF, p, fy); + Term fx = termManager.mkTerm(Kind.APPLY_UF, f, xTyped); + Term fy = termManager.mkTerm(Kind.APPLY_UF, f, yTyped); + Term sum = termManager.mkTerm(Kind.ADD, fx, fy); + Term p0 = termManager.mkTerm(Kind.APPLY_UF, p, zero); + Term pfy = termManager.mkTerm(Kind.APPLY_UF, p, fy); // Make some assumptions Term assumptions1 = - solver.mkTerm( + termManager.mkTerm( Kind.AND, - solver.mkTerm(Kind.LEQ, zero, fx), - solver.mkTerm(Kind.LEQ, zero, fy), - solver.mkTerm(Kind.LEQ, sum, one)); + termManager.mkTerm(Kind.LEQ, zero, fx), + termManager.mkTerm(Kind.LEQ, zero, fy), + termManager.mkTerm(Kind.LEQ, sum, one)); - Term assumptions2 = solver.mkTerm(Kind.AND, p0.notTerm(), pfy); + Term assumptions2 = termManager.mkTerm(Kind.AND, p0.notTerm(), pfy); solver.assertFormula(assumptions1); solver.assertFormula(assumptions2); @@ -1057,16 +1086,17 @@ public void checkCustomTypesAndUFs() { @Test public void checkBooleanUFDeclaration() { - Sort boolSort = solver.getBooleanSort(); - Sort intSort = solver.getIntegerSort(); + Sort boolSort = termManager.getBooleanSort(); + Sort intSort = termManager.getIntegerSort(); // arg is bool, return is int - Sort ufSort = solver.mkFunctionSort(boolSort, intSort); - Term uf = solver.mkConst(ufSort, "fun_bi"); - Term ufTrue = solver.mkTerm(Kind.APPLY_UF, uf, solver.mkTrue()); - Term ufFalse = solver.mkTerm(Kind.APPLY_UF, uf, solver.mkFalse()); + Sort ufSort = termManager.mkFunctionSort(boolSort, intSort); + Term uf = termManager.mkConst(ufSort, "fun_bi"); + Term ufTrue = termManager.mkTerm(Kind.APPLY_UF, uf, termManager.mkTrue()); + Term ufFalse = termManager.mkTerm(Kind.APPLY_UF, uf, termManager.mkFalse()); - Term assumptions = solver.mkTerm(Kind.NOT, solver.mkTerm(Kind.EQUAL, ufTrue, ufFalse)); + Term assumptions = + termManager.mkTerm(Kind.NOT, termManager.mkTerm(Kind.EQUAL, ufTrue, ufFalse)); solver.assertFormula(assumptions); Result satCheck = solver.checkSat(); @@ -1081,39 +1111,39 @@ public void checkLIAUfsUnsat() { // f(x) + f(y) = y // f(x) = x + 1 // f(y) = y - 1 - Term zero = solver.mkInteger(0); - Term one = solver.mkInteger(1); + Term zero = termManager.mkInteger(0); + Term one = termManager.mkInteger(1); - Sort intSort = solver.getIntegerSort(); + Sort intSort = termManager.getIntegerSort(); // Sort for UFs later - Sort intToInt = solver.mkFunctionSort(intSort, intSort); + Sort intToInt = termManager.mkFunctionSort(intSort, intSort); - Term xInt = solver.mkConst(intSort, "x"); - Term yInt = solver.mkConst(intSort, "y"); + Term xInt = termManager.mkConst(intSort, "x"); + Term yInt = termManager.mkConst(intSort, "y"); // declare UFs - Term f = solver.mkConst(intToInt, "f"); + Term f = termManager.mkConst(intToInt, "f"); // Apply UFs - Term fx = solver.mkTerm(Kind.APPLY_UF, f, xInt); - Term fy = solver.mkTerm(Kind.APPLY_UF, f, yInt); - Term plus = solver.mkTerm(Kind.ADD, fx, fy); + Term fx = termManager.mkTerm(Kind.APPLY_UF, f, xInt); + Term fy = termManager.mkTerm(Kind.APPLY_UF, f, yInt); + Term plus = termManager.mkTerm(Kind.ADD, fx, fy); // Make some assumptions Term assumptions1 = - solver.mkTerm( + termManager.mkTerm( Kind.AND, - solver.mkTerm(Kind.LEQ, zero, fx), - solver.mkTerm(Kind.EQUAL, plus, xInt), - solver.mkTerm(Kind.LEQ, zero, fy)); + termManager.mkTerm(Kind.LEQ, zero, fx), + termManager.mkTerm(Kind.EQUAL, plus, xInt), + termManager.mkTerm(Kind.LEQ, zero, fy)); Term assumptions2 = - solver.mkTerm( + termManager.mkTerm( Kind.AND, - solver.mkTerm(Kind.EQUAL, fx, solver.mkTerm(Kind.ADD, xInt, one)), - solver.mkTerm(Kind.EQUAL, fy, solver.mkTerm(Kind.SUB, yInt, one)), - solver.mkTerm(Kind.EQUAL, plus, yInt)); + termManager.mkTerm(Kind.EQUAL, fx, termManager.mkTerm(Kind.ADD, xInt, one)), + termManager.mkTerm(Kind.EQUAL, fy, termManager.mkTerm(Kind.SUB, yInt, one)), + termManager.mkTerm(Kind.EQUAL, plus, yInt)); solver.assertFormula(assumptions1); solver.assertFormula(assumptions2); @@ -1126,35 +1156,35 @@ public void checkLIAUfsSat() { // f(x) = x + 1 // f(y) = y - 1 // x = y -> f(x) + f(y) = x AND f(x) + f(y) = y - Term one = solver.mkInteger(1); + Term one = termManager.mkInteger(1); - Sort intSort = solver.getIntegerSort(); + Sort intSort = termManager.getIntegerSort(); // Sort for UFs later - Sort intToInt = solver.mkFunctionSort(intSort, intSort); + Sort intToInt = termManager.mkFunctionSort(intSort, intSort); - Term xInt = solver.mkConst(intSort, "x"); - Term yInt = solver.mkConst(intSort, "y"); + Term xInt = termManager.mkConst(intSort, "x"); + Term yInt = termManager.mkConst(intSort, "y"); // declare UFs - Term f = solver.mkConst(intToInt, "f"); + Term f = termManager.mkConst(intToInt, "f"); // Apply UFs - Term fx = solver.mkTerm(Kind.APPLY_UF, f, xInt); - Term fy = solver.mkTerm(Kind.APPLY_UF, f, yInt); - Term plus = solver.mkTerm(Kind.ADD, fx, fy); + Term fx = termManager.mkTerm(Kind.APPLY_UF, f, xInt); + Term fy = termManager.mkTerm(Kind.APPLY_UF, f, yInt); + Term plus = termManager.mkTerm(Kind.ADD, fx, fy); - Term plusEqx = solver.mkTerm(Kind.EQUAL, plus, xInt); - Term plusEqy = solver.mkTerm(Kind.EQUAL, plus, yInt); - Term xEqy = solver.mkTerm(Kind.EQUAL, yInt, xInt); + Term plusEqx = termManager.mkTerm(Kind.EQUAL, plus, xInt); + Term plusEqy = termManager.mkTerm(Kind.EQUAL, plus, yInt); + Term xEqy = termManager.mkTerm(Kind.EQUAL, yInt, xInt); Term xEqyImplplusEqxAndy = - solver.mkTerm(Kind.IMPLIES, xEqy, solver.mkTerm(Kind.AND, plusEqx, plusEqy)); + termManager.mkTerm(Kind.IMPLIES, xEqy, termManager.mkTerm(Kind.AND, plusEqx, plusEqy)); Term assumptions = - solver.mkTerm( + termManager.mkTerm( Kind.AND, - solver.mkTerm(Kind.EQUAL, fx, solver.mkTerm(Kind.ADD, xInt, one)), - solver.mkTerm(Kind.EQUAL, fy, solver.mkTerm(Kind.SUB, yInt, one)), + termManager.mkTerm(Kind.EQUAL, fx, termManager.mkTerm(Kind.ADD, xInt, one)), + termManager.mkTerm(Kind.EQUAL, fy, termManager.mkTerm(Kind.SUB, yInt, one)), xEqyImplplusEqxAndy); solver.assertFormula(assumptions); @@ -1165,13 +1195,13 @@ public void checkLIAUfsSat() { @Test public void checkStringCompare() { - Term var1 = solver.mkConst(solver.getStringSort(), "0"); - Term var2 = solver.mkConst(solver.getStringSort(), "1"); + Term var1 = termManager.mkConst(termManager.getStringSort(), "0"); + Term var2 = termManager.mkConst(termManager.getStringSort(), "1"); Term f = - solver + termManager .mkTerm(Kind.STRING_LEQ, var1, var2) - .andTerm(solver.mkTerm(Kind.STRING_LEQ, var2, var1)); + .andTerm(termManager.mkTerm(Kind.STRING_LEQ, var2, var1)); // Thats no problem solver.assertFormula(f); @@ -1187,16 +1217,17 @@ public void checkStringCompare() { /** Sets up array and quantifier based formulas for tests. */ private void setupArrayQuant() { - Term zero = solver.mkInteger(0); - Term one = solver.mkInteger(1); + Term zero = termManager.mkInteger(0); + Term one = termManager.mkInteger(1); - x = solver.mkVar(solver.getIntegerSort(), "x"); + x = termManager.mkVar(termManager.getIntegerSort(), "x"); - Sort arraySort = solver.mkArraySort(solver.getIntegerSort(), solver.getIntegerSort()); - array = solver.mkVar(arraySort, "a"); + Sort arraySort = + termManager.mkArraySort(termManager.getIntegerSort(), termManager.getIntegerSort()); + array = termManager.mkVar(arraySort, "a"); - aAtxEq0 = solver.mkTerm(Kind.EQUAL, solver.mkTerm(Kind.SELECT, array, x), zero); - aAtxEq1 = solver.mkTerm(Kind.EQUAL, solver.mkTerm(Kind.SELECT, array, x), one); + aAtxEq0 = termManager.mkTerm(Kind.EQUAL, termManager.mkTerm(Kind.SELECT, array, x), zero); + aAtxEq1 = termManager.mkTerm(Kind.EQUAL, termManager.mkTerm(Kind.SELECT, array, x), one); } /** @@ -1215,15 +1246,15 @@ private Term makeMaxCVC5Bitvector(int width, boolean signed) throws CVC5ApiExcep } else { bitvecString = String.valueOf(new char[width]).replace("\0", "1"); } - return solver.mkBitVector(width, bitvecString, 2); + return termManager.mkBitVector(width, bitvecString, 2); } @Test public void termAccessAfterModelClosed() throws CVC5ApiException { Solver secondSolver = createEnvironment(); - Term v = solver.mkConst(solver.getIntegerSort(), "v"); - Term one = solver.mkInteger(1); - Term eq = solver.mkTerm(Kind.EQUAL, v, one); // v==1 + Term v = termManager.mkConst(termManager.getIntegerSort(), "v"); + Term one = termManager.mkInteger(1); + Term eq = termManager.mkTerm(Kind.EQUAL, v, one); // v==1 secondSolver.assertFormula(eq); Result result = secondSolver.checkSat(); @@ -1238,15 +1269,15 @@ public void termAccessAfterModelClosed() throws CVC5ApiException { @Test public void checkCVC5InterpolationMethod() { solver.setOption("produce-interpolants", "true"); - Term xp = solver.mkConst(solver.getIntegerSort(), "xp"); - Term y = solver.mkConst(solver.getIntegerSort(), "y"); + Term xp = termManager.mkConst(termManager.getIntegerSort(), "xp"); + Term y = termManager.mkConst(termManager.getIntegerSort(), "y"); - Term ip0 = solver.mkTerm(Kind.GT, xp, y); - Term ip1 = solver.mkTerm(Kind.EQUAL, xp, solver.mkInteger(0)); - Term ip2 = solver.mkTerm(Kind.GT, y, solver.mkInteger(0)); + Term ip0 = termManager.mkTerm(Kind.GT, xp, y); + Term ip1 = termManager.mkTerm(Kind.EQUAL, xp, termManager.mkInteger(0)); + Term ip2 = termManager.mkTerm(Kind.GT, y, termManager.mkInteger(0)); Term a = ip0; - Term b = solver.mkTerm(Kind.AND, ip1, ip2); + Term b = termManager.mkTerm(Kind.AND, ip1, ip2); assertThat(!interpolateAndCheck(solver, a, b).isNull()).isTrue(); } @@ -1261,13 +1292,13 @@ private Term interpolateAndCheck(Solver solverP, Term interpolantA, Term interpo // solver.setOption("produce-interpolants", "true"); solverP.assertFormula(interpolantA); System.out.println( - "Interpolation Pair:\n" + interpolantA + "\n" + solverP.mkTerm(Kind.NOT, interpolantB)); - Term interpolation = solverP.getInterpolant(solverP.mkTerm(Kind.NOT, interpolantB)); + "Interpolation Pair:\n" + interpolantA + "\n" + termManager.mkTerm(Kind.NOT, interpolantB)); + Term interpolation = solverP.getInterpolant(termManager.mkTerm(Kind.NOT, interpolantB)); System.out.println("Interpolation: " + interpolation); solverP.resetAssertions(); - Term cvc51 = solverP.mkTerm(Kind.IMPLIES, interpolantA, interpolation); + Term cvc51 = termManager.mkTerm(Kind.IMPLIES, interpolantA, interpolation); Term cvc52 = - solverP.mkTerm(Kind.IMPLIES, interpolation, solverP.mkTerm(Kind.NOT, interpolantB)); + termManager.mkTerm(Kind.IMPLIES, interpolation, termManager.mkTerm(Kind.NOT, interpolantB)); solverP.assertFormula(cvc51); solverP.assertFormula(cvc52); @@ -1277,19 +1308,19 @@ private Term interpolateAndCheck(Solver solverP, Term interpolantA, Term interpo } solverP.resetAssertions(); - solverP.assertFormula(solverP.mkTerm(Kind.NOT, solverP.mkTerm(Kind.AND, cvc51, cvc52))); + solverP.assertFormula(termManager.mkTerm(Kind.NOT, termManager.mkTerm(Kind.AND, cvc51, cvc52))); if (solverP.checkSat().isSat()) { System.out.println("Does not satisfy generally CVC5 Interpolation Definition"); return null; } solverP.resetAssertions(); - Term craig1 = solverP.mkTerm(Kind.IMPLIES, interpolantA, interpolation); + Term craig1 = termManager.mkTerm(Kind.IMPLIES, interpolantA, interpolation); Term craig2 = - solverP.mkTerm( + termManager.mkTerm( Kind.EQUAL, - solverP.mkTerm(Kind.AND, interpolation, interpolantB), - solverP.mkBoolean(false)); + termManager.mkTerm(Kind.AND, interpolation, interpolantB), + termManager.mkBoolean(false)); solverP.assertFormula(craig1); solverP.assertFormula(craig2); if (solverP.checkSat().isUnsat()) { @@ -1297,7 +1328,8 @@ private Term interpolateAndCheck(Solver solverP, Term interpolantA, Term interpo return null; } solverP.resetAssertions(); - solverP.assertFormula(solverP.mkTerm(Kind.NOT, solverP.mkTerm(Kind.AND, craig1, craig2))); + solverP.assertFormula( + termManager.mkTerm(Kind.NOT, termManager.mkTerm(Kind.AND, craig1, craig2))); if (solverP.checkSat().isSat()) { System.out.println("Does not satisfy generally Craig Interpolation Definition"); return null; @@ -1312,16 +1344,20 @@ public void testSimpleInterpolation() { // Out of InterpolatingProverTest.java // Line: 65 solver.setOption("produce-interpolants", "true"); - Term xprime = solver.mkConst(solver.getIntegerSort(), "x"); - Term y = solver.mkConst(solver.getIntegerSort(), "y"); - Term z = solver.mkConst(solver.getIntegerSort(), "z"); - Term f1 = solver.mkTerm(Kind.EQUAL, y, solver.mkTerm(Kind.MULT, solver.mkInteger(2), xprime)); + Term xprime = termManager.mkConst(termManager.getIntegerSort(), "x"); + Term y = termManager.mkConst(termManager.getIntegerSort(), "y"); + Term z = termManager.mkConst(termManager.getIntegerSort(), "z"); + Term f1 = + termManager.mkTerm( + Kind.EQUAL, y, termManager.mkTerm(Kind.MULT, termManager.mkInteger(2), xprime)); Term f2 = - solver.mkTerm( + termManager.mkTerm( Kind.EQUAL, y, - solver.mkTerm( - Kind.ADD, solver.mkInteger(1), solver.mkTerm(Kind.MULT, z, solver.mkInteger(2)))); + termManager.mkTerm( + Kind.ADD, + termManager.mkInteger(1), + termManager.mkTerm(Kind.MULT, z, termManager.mkInteger(2)))); interpolateAndCheck(solver, f1, f2); } @@ -1329,10 +1365,10 @@ public void testSimpleInterpolation() { public void testBitvectorSortinVariableCache() throws CVC5ApiException { Map variablesCache = new HashMap<>(); String name = "__ADDRESS_OF_main::i@"; - Sort sort = solver.mkBitVectorSort(32); + Sort sort = termManager.mkBitVectorSort(32); System.out.println(sort); System.out.println("--------"); - Term exp = variablesCache.computeIfAbsent(name, n -> solver.mkConst(sort, name)); + Term exp = variablesCache.computeIfAbsent(name, n -> termManager.mkConst(sort, name)); Preconditions.checkArgument( sort.equals(exp.getSort()), "symbol name %s with sort %s already in use for different sort %s with value %s as String", @@ -1341,4 +1377,63 @@ public void testBitvectorSortinVariableCache() throws CVC5ApiException { exp.getSort(), exp); } + + @Test + public void testProofMethods() throws CVC5ApiException { + solver.setOption("produce-proofs", "true"); + Sort boolSort = termManager.getBooleanSort(); + + // (declare-fun q1 () Bool) + // (declare-fun q2 () Bool) + // (assert (or (not q1) q2)) + // (assert q1) + // (assert (not q2)) + // (check-sat) + // (get-proof) + Term q1 = solver.declareFun("q1", new Sort[] {}, boolSort); + Term q2 = solver.declareFun("q2", new Sort[] {}, boolSort); + + solver.assertFormula(termManager.mkTerm(Kind.OR, termManager.mkTerm(Kind.NOT, q1), q2)); + solver.assertFormula(q1); + solver.assertFormula(termManager.mkTerm(Kind.NOT, q2)); + + Result satCheck = solver.checkSat(); + assertThat(satCheck.isUnsat()).isTrue(); + + Proof[] proofs = solver.getProof(); + + assertThat(proofs).isNotNull(); + + Proof proof = proofs[0]; + + // Test getRule + assertThat(proof.getRule()).isNotNull(); + + assertThat(proof.getRule()).isEqualTo(ProofRule.SCOPE); + + // Test getChildren + assertThat(proof.getChildren()).isNotNull(); + + assertThat(proof.getChildren()[0]).isNotNull(); + + // The way the proof DAG is structured, the root has one child, which has also one child and + // the child of the latter has more than one child. + Proof[] childOfSecondProof = proof.getChildren()[0].getChildren(); + + Proof[] childrenOfThirdProof = childOfSecondProof[0].getChildren(); + + assertThat(childrenOfThirdProof.length).isEqualTo(2); + + // Test equals + assertThat(childrenOfThirdProof[0].equals(childrenOfThirdProof[1])).isFalse(); + + assertThat(childrenOfThirdProof[0].equals(childrenOfThirdProof[0])).isTrue(); + + // Test getResult + assertThat(Optional.ofNullable(proof.getResult())).isNotNull(); + + // Test getArguments + assertThat(childrenOfThirdProof[0].getArguments()).isNotNull(); + assertThat(Optional.ofNullable(childrenOfThirdProof[0].getArguments()[0])).isNotNull(); + } } diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5NumeralFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5NumeralFormulaManager.java index 7ae237e3c0..aa4132b4cb 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5NumeralFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5NumeralFormulaManager.java @@ -18,9 +18,9 @@ import com.google.common.collect.ImmutableSet; import io.github.cvc5.CVC5ApiException; import io.github.cvc5.Kind; -import io.github.cvc5.Solver; import io.github.cvc5.Sort; import io.github.cvc5.Term; +import io.github.cvc5.TermManager; import java.math.BigInteger; import java.util.List; import java.util.regex.Pattern; @@ -31,7 +31,7 @@ abstract class CVC5NumeralFormulaManager< ParamFormulaType extends NumeralFormula, ResultFormulaType extends NumeralFormula> extends AbstractNumeralFormulaManager< - Term, Sort, Solver, ParamFormulaType, ResultFormulaType, Term> { + Term, Sort, TermManager, ParamFormulaType, ResultFormulaType, Term> { /** * CVC4 fails hard when creating Integers/Rationals instead of throwing an exception for invalid @@ -49,11 +49,11 @@ abstract class CVC5NumeralFormulaManager< private static final ImmutableSet NUMERIC_FUNCTIONS = ImmutableSet.of(ADD, SUB, MULT, DIVISION, INTS_DIVISION, INTS_MODULUS); - protected final Solver solver; + protected final TermManager termManager; CVC5NumeralFormulaManager(CVC5FormulaCreator pCreator, NonLinearArithmetic pNonLinearArithmetic) { super(pCreator, pNonLinearArithmetic); - solver = pCreator.getEnv(); + termManager = pCreator.getEnv(); } protected abstract Sort getNumeralType(); @@ -114,7 +114,7 @@ protected Term makeNumberImpl(String pI) { throw new NumberFormatException("number is not an rational value: " + pI); } try { - return solver.mkReal(pI); + return termManager.mkReal(pI); } catch (CVC5ApiException e) { throw new IllegalArgumentException( "You tried creating a invalid rational number with input Sring: " + pI + ".", e); @@ -129,7 +129,7 @@ protected Term makeVariableImpl(String varName) { @Override protected Term multiply(Term pParam1, Term pParam2) { - return solver.mkTerm(Kind.MULT, pParam1, pParam2); + return termManager.mkTerm(Kind.MULT, pParam1, pParam2); /* * In CVC4 we had to check if the terms consist of only numerals, if this * fails we have to do it again! @@ -143,55 +143,55 @@ protected Term multiply(Term pParam1, Term pParam2) { @Override protected Term modulo(Term pParam1, Term pParam2) { - return solver.mkTerm(Kind.INTS_MODULUS, pParam1, pParam2); + return termManager.mkTerm(Kind.INTS_MODULUS, pParam1, pParam2); } @Override protected Term negate(Term pParam1) { - return solver.mkTerm(Kind.NEG, pParam1); + return termManager.mkTerm(Kind.NEG, pParam1); } @Override protected Term add(Term pParam1, Term pParam2) { - return solver.mkTerm(Kind.ADD, pParam1, pParam2); + return termManager.mkTerm(Kind.ADD, pParam1, pParam2); } @Override protected Term subtract(Term pParam1, Term pParam2) { - return solver.mkTerm(Kind.SUB, pParam1, pParam2); + return termManager.mkTerm(Kind.SUB, pParam1, pParam2); } @Override protected Term equal(Term pParam1, Term pParam2) { - return solver.mkTerm(Kind.EQUAL, pParam1, pParam2); + return termManager.mkTerm(Kind.EQUAL, pParam1, pParam2); } @Override protected Term greaterThan(Term pParam1, Term pParam2) { - return solver.mkTerm(Kind.GT, pParam1, pParam2); + return termManager.mkTerm(Kind.GT, pParam1, pParam2); } @Override protected Term greaterOrEquals(Term pParam1, Term pParam2) { - return solver.mkTerm(Kind.GEQ, pParam1, pParam2); + return termManager.mkTerm(Kind.GEQ, pParam1, pParam2); } @Override protected Term lessThan(Term pParam1, Term pParam2) { - return solver.mkTerm(Kind.LT, pParam1, pParam2); + return termManager.mkTerm(Kind.LT, pParam1, pParam2); } @Override protected Term lessOrEquals(Term pParam1, Term pParam2) { - return solver.mkTerm(Kind.LEQ, pParam1, pParam2); + return termManager.mkTerm(Kind.LEQ, pParam1, pParam2); } @Override protected Term distinctImpl(List pParam) { if (pParam.size() < 2) { - return solver.mkTrue(); + return termManager.mkTrue(); } else { - return solver.mkTerm(Kind.DISTINCT, pParam.toArray(new Term[0])); + return termManager.mkTerm(Kind.DISTINCT, pParam.toArray(new Term[0])); } } } diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5QuantifiedFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5QuantifiedFormulaManager.java index 8230abf702..f8c1b8e184 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5QuantifiedFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5QuantifiedFormulaManager.java @@ -12,21 +12,22 @@ import io.github.cvc5.Solver; import io.github.cvc5.Sort; import io.github.cvc5.Term; +import io.github.cvc5.TermManager; import java.util.ArrayList; import java.util.List; import org.sosy_lab.java_smt.api.SolverException; import org.sosy_lab.java_smt.basicimpl.AbstractQuantifiedFormulaManager; -import org.sosy_lab.java_smt.basicimpl.FormulaCreator; public class CVC5QuantifiedFormulaManager - extends AbstractQuantifiedFormulaManager { + extends AbstractQuantifiedFormulaManager { + private final TermManager termManager; private final Solver solver; - protected CVC5QuantifiedFormulaManager(FormulaCreator pFormulaCreator) { + protected CVC5QuantifiedFormulaManager(CVC5FormulaCreator pFormulaCreator) { super(pFormulaCreator); - - solver = pFormulaCreator.getEnv(); + termManager = pFormulaCreator.getEnv(); + solver = new Solver(termManager); } /* @@ -76,8 +77,8 @@ public Term mkQuantifier(Quantifier pQ, List pVars, Term pBody) { } Kind quant = pQ == Quantifier.EXISTS ? Kind.EXISTS : Kind.FORALL; - Term boundVarsList = solver.mkTerm(Kind.VARIABLE_LIST, boundVars.toArray(new Term[0])); - return solver.mkTerm(quant, boundVarsList, substBody); + Term boundVarsList = termManager.mkTerm(Kind.VARIABLE_LIST, boundVars.toArray(new Term[0])); + return termManager.mkTerm(quant, boundVarsList, substBody); } } } diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5RationalFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5RationalFormulaManager.java index 57d7d0ca25..a3017ccb85 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5RationalFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5RationalFormulaManager.java @@ -42,11 +42,11 @@ protected Term makeNumberImpl(BigDecimal pNumber) { @Override public Term divide(Term pParam1, Term pParam2) { - return solver.mkTerm(Kind.DIVISION, pParam1, pParam2); + return termManager.mkTerm(Kind.DIVISION, pParam1, pParam2); } @Override protected Term floor(Term pNumber) { - return solver.mkTerm(Kind.TO_INTEGER, pNumber); + return termManager.mkTerm(Kind.TO_INTEGER, pNumber); } } diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5SLFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5SLFormulaManager.java index 511ff13229..0dc0b00b56 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5SLFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5SLFormulaManager.java @@ -9,43 +9,43 @@ package org.sosy_lab.java_smt.solvers.cvc5; import io.github.cvc5.Kind; -import io.github.cvc5.Solver; import io.github.cvc5.Sort; import io.github.cvc5.Term; +import io.github.cvc5.TermManager; import org.sosy_lab.java_smt.basicimpl.AbstractSLFormulaManager; -public class CVC5SLFormulaManager extends AbstractSLFormulaManager { +public class CVC5SLFormulaManager extends AbstractSLFormulaManager { - private final Solver solver; + private final TermManager termManager; protected CVC5SLFormulaManager(CVC5FormulaCreator pCreator) { super(pCreator); - solver = pCreator.getEnv(); + termManager = pCreator.getEnv(); } @Override protected Term makeStar(Term e1, Term e2) { - return solver.mkTerm(Kind.SEP_STAR, e1, e2); + return termManager.mkTerm(Kind.SEP_STAR, e1, e2); } @Override protected Term makePointsTo(Term pPtr, Term pTo) { - return solver.mkTerm(Kind.SEP_PTO, pPtr, pTo); + return termManager.mkTerm(Kind.SEP_PTO, pPtr, pTo); } @Override protected Term makeMagicWand(Term pE1, Term pE2) { - return solver.mkTerm(Kind.SEP_WAND, pE1, pE2); + return termManager.mkTerm(Kind.SEP_WAND, pE1, pE2); } @Override protected Term makeEmptyHeap(Sort pT1, Sort pT2) { // According to the documentation this is sortless - return solver.mkTerm(Kind.SEP_EMP); + return termManager.mkTerm(Kind.SEP_EMP); } @Override protected Term makeNilElement(Sort pSort) { - return solver.mkSepNil(pSort); + return termManager.mkSepNil(pSort); } } diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5SolverContext.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5SolverContext.java index 7e31515969..3d070b61b5 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5SolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5SolverContext.java @@ -12,9 +12,11 @@ import com.google.common.base.Preconditions; import com.google.common.base.Splitter; import com.google.common.base.Splitter.MapSplitter; +import com.google.common.collect.ImmutableList; import com.google.common.collect.ImmutableMap; import io.github.cvc5.CVC5ApiRecoverableException; import io.github.cvc5.Solver; +import io.github.cvc5.TermManager; import java.util.Map.Entry; import java.util.Set; import java.util.function.Consumer; @@ -72,6 +74,7 @@ private CVC5Settings(Configuration config) throws InvalidConfigurationException // creator is final, except after closing, then null. private CVC5FormulaCreator creator; + private final TermManager termManager; private final Solver solver; private final ShutdownNotifier shutdownNotifier; private final int randomSeed; @@ -82,6 +85,7 @@ private CVC5SolverContext( CVC5FormulaCreator pCreator, CVC5FormulaManager pManager, ShutdownNotifier pShutdownNotifier, + TermManager pTermManager, Solver pSolver, int pRandomSeed, CVC5Settings pSettings) { @@ -89,13 +93,14 @@ private CVC5SolverContext( creator = pCreator; shutdownNotifier = pShutdownNotifier; randomSeed = pRandomSeed; + termManager = pTermManager; solver = pSolver; settings = pSettings; } @VisibleForTesting static void loadLibrary(Consumer pLoader) { - pLoader.accept("cvc5jni"); + loadLibrariesWithFallback(pLoader, ImmutableList.of("cvc5jni"), ImmutableList.of("libcvc5jni")); // disable CVC5's own loading mechanism, // see io.github.cvc5.Util#loadLibraries and https://github.com/cvc5/cvc5/pull/9047 @@ -117,9 +122,15 @@ public static SolverContext create( loadLibrary(pLoader); - // This Solver is the central class for creating expressions/terms/formulae. + // The TermManager is the central class for creating expressions/terms/formulae. // We keep this instance available until the whole context is closed. - Solver newSolver = new Solver(); + TermManager termManager = new TermManager(); + + // Create a new solver instance + // We'll use this instance in some of the formula managers for simplifying terms and declaring + // datatypes. The actual solving is done on a different instance that is created by + // newProverEnvironment() + Solver newSolver = new Solver(termManager); try { setSolverOptions(newSolver, randomSeed, settings.furtherOptionsMap); @@ -127,7 +138,7 @@ public static SolverContext create( throw new InvalidConfigurationException(e.getMessage(), e); } - CVC5FormulaCreator pCreator = new CVC5FormulaCreator(newSolver); + CVC5FormulaCreator pCreator = new CVC5FormulaCreator(termManager, newSolver); // Create managers CVC5UFManager functionTheory = new CVC5UFManager(pCreator); @@ -161,7 +172,7 @@ public static SolverContext create( enumTheory); return new CVC5SolverContext( - pCreator, manager, pShutdownNotifier, newSolver, randomSeed, settings); + pCreator, manager, pShutdownNotifier, termManager, newSolver, randomSeed, settings); } /** @@ -169,29 +180,18 @@ public static SolverContext create( * * @throws CVC5ApiRecoverableException from native code. */ - private static void setSolverOptions( + static void setSolverOptions( Solver pSolver, int randomSeed, ImmutableMap furtherOptions) throws CVC5ApiRecoverableException { pSolver.setOption("seed", String.valueOf(randomSeed)); pSolver.setOption("output-language", "smtlib2"); + // Enable support for arbitrary size floating-point formats + pSolver.setOption("fp-exp", "true"); + for (Entry option : furtherOptions.entrySet()) { pSolver.setOption(option.getKey(), option.getValue()); } - - // Set Strings option to enable all String features (such as lessOrEquals). - // This should not have any effect for non-string theories. - // pSolver.setOption("strings-exp", "true"); - - // pSolver.setOption("finite-model-find", "true"); - // pSolver.setOption("sets-ext", "true"); - - // pSolver.setOption("produce-models", "true"); - // pSolver.setOption("produce-unsat-cores", "true"); - - // Neither simplification, arith-rewrite-equalities, pb-rewrites provide rewrites of trivial - // formulas only. - // Note: with solver.getOptionNames() you can get all options } @Override @@ -207,9 +207,8 @@ public String getVersion() { public void close() { if (creator != null) { closed = true; + termManager.deletePointer(); solver.deletePointer(); - // Don't use Context.deletePointers(); as it deletes statically information from all - // existing contexts, not only this one! creator = null; } } diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5StringFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5StringFormulaManager.java index db123b0a57..6bb7c0f618 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5StringFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5StringFormulaManager.java @@ -10,24 +10,24 @@ import com.google.common.base.Preconditions; import io.github.cvc5.Kind; -import io.github.cvc5.Solver; import io.github.cvc5.Sort; import io.github.cvc5.Term; +import io.github.cvc5.TermManager; import java.util.List; import org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager; -class CVC5StringFormulaManager extends AbstractStringFormulaManager { +class CVC5StringFormulaManager extends AbstractStringFormulaManager { - private final Solver solver; + private final TermManager termManager; CVC5StringFormulaManager(CVC5FormulaCreator pCreator) { super(pCreator); - solver = pCreator.getEnv(); + termManager = pCreator.getEnv(); } @Override protected Term makeStringImpl(String pValue) { - return solver.mkString(escapeUnicodeForSmtlib(pValue), true); + return termManager.mkString(escapeUnicodeForSmtlib(pValue), true); } @Override @@ -38,104 +38,104 @@ protected Term makeVariableImpl(String varName) { @Override protected Term equal(Term pParam1, Term pParam2) { - return solver.mkTerm(Kind.EQUAL, pParam1, pParam2); + return termManager.mkTerm(Kind.EQUAL, pParam1, pParam2); } @Override protected Term greaterThan(Term pParam1, Term pParam2) { - return solver.mkTerm(Kind.STRING_LT, pParam2, pParam1); + return termManager.mkTerm(Kind.STRING_LT, pParam2, pParam1); } @Override protected Term greaterOrEquals(Term pParam1, Term pParam2) { - return solver.mkTerm(Kind.STRING_LEQ, pParam2, pParam1); + return termManager.mkTerm(Kind.STRING_LEQ, pParam2, pParam1); } @Override protected Term lessThan(Term pParam1, Term pParam2) { - return solver.mkTerm(Kind.STRING_LT, pParam1, pParam2); + return termManager.mkTerm(Kind.STRING_LT, pParam1, pParam2); } @Override protected Term lessOrEquals(Term pParam1, Term pParam2) { - return solver.mkTerm(Kind.STRING_LEQ, pParam1, pParam2); + return termManager.mkTerm(Kind.STRING_LEQ, pParam1, pParam2); } @Override protected Term length(Term pParam) { - return solver.mkTerm(Kind.STRING_LENGTH, pParam); + return termManager.mkTerm(Kind.STRING_LENGTH, pParam); } @Override protected Term concatImpl(List parts) { Preconditions.checkArgument(parts.size() > 1); - return solver.mkTerm(Kind.STRING_CONCAT, parts.toArray(new Term[0])); + return termManager.mkTerm(Kind.STRING_CONCAT, parts.toArray(new Term[0])); } @Override protected Term prefix(Term prefix, Term str) { - return solver.mkTerm(Kind.STRING_PREFIX, prefix, str); + return termManager.mkTerm(Kind.STRING_PREFIX, prefix, str); } @Override protected Term suffix(Term suffix, Term str) { - return solver.mkTerm(Kind.STRING_SUFFIX, suffix, str); + return termManager.mkTerm(Kind.STRING_SUFFIX, suffix, str); } @Override protected Term in(Term str, Term regex) { - return solver.mkTerm(Kind.STRING_IN_REGEXP, str, regex); + return termManager.mkTerm(Kind.STRING_IN_REGEXP, str, regex); } @Override protected Term contains(Term str, Term part) { - return solver.mkTerm(Kind.STRING_CONTAINS, str, part); + return termManager.mkTerm(Kind.STRING_CONTAINS, str, part); } @Override protected Term indexOf(Term str, Term part, Term startIndex) { - return solver.mkTerm(Kind.STRING_INDEXOF, str, part, startIndex); + return termManager.mkTerm(Kind.STRING_INDEXOF, str, part, startIndex); } @Override protected Term charAt(Term str, Term index) { - return solver.mkTerm(Kind.STRING_CHARAT, str, index); + return termManager.mkTerm(Kind.STRING_CHARAT, str, index); } @Override protected Term substring(Term str, Term index, Term length) { - return solver.mkTerm(Kind.STRING_SUBSTR, str, index, length); + return termManager.mkTerm(Kind.STRING_SUBSTR, str, index, length); } @Override protected Term replace(Term fullStr, Term target, Term replacement) { - return solver.mkTerm(Kind.STRING_REPLACE, fullStr, target, replacement); + return termManager.mkTerm(Kind.STRING_REPLACE, fullStr, target, replacement); } @Override protected Term replaceAll(Term fullStr, Term target, Term replacement) { - return solver.mkTerm(Kind.STRING_REPLACE_ALL, fullStr, target, replacement); + return termManager.mkTerm(Kind.STRING_REPLACE_ALL, fullStr, target, replacement); } @Override protected Term makeRegexImpl(String value) { Term str = makeStringImpl(value); - return solver.mkTerm(Kind.STRING_TO_REGEXP, str); + return termManager.mkTerm(Kind.STRING_TO_REGEXP, str); } @Override protected Term noneImpl() { - return solver.mkTerm(Kind.REGEXP_NONE); + return termManager.mkTerm(Kind.REGEXP_NONE); } @Override protected Term allImpl() { - return solver.mkTerm(Kind.REGEXP_COMPLEMENT, noneImpl()); + return termManager.mkTerm(Kind.REGEXP_COMPLEMENT, noneImpl()); } @Override protected Term allCharImpl() { - return solver.mkTerm(Kind.REGEXP_ALLCHAR); + return termManager.mkTerm(Kind.REGEXP_ALLCHAR); } @Override @@ -143,66 +143,67 @@ protected Term range(Term start, Term end) { // Precondition: Both bounds must be single character Strings // CVC5 already checks that the lower bound is smaller than the upper bound and returns the // empty language otherwise. - Term one = solver.mkInteger(1); + Term one = termManager.mkInteger(1); Term cond = - solver.mkTerm( + termManager.mkTerm( Kind.AND, - solver.mkTerm(Kind.EQUAL, length(start), one), - solver.mkTerm(Kind.EQUAL, length(end), one)); - return solver.mkTerm(Kind.ITE, cond, solver.mkTerm(Kind.REGEXP_RANGE, start, end), noneImpl()); + termManager.mkTerm(Kind.EQUAL, length(start), one), + termManager.mkTerm(Kind.EQUAL, length(end), one)); + return termManager.mkTerm( + Kind.ITE, cond, termManager.mkTerm(Kind.REGEXP_RANGE, start, end), noneImpl()); } @Override protected Term concatRegexImpl(List parts) { Preconditions.checkArgument(parts.size() > 1); - return solver.mkTerm(Kind.REGEXP_CONCAT, parts.toArray(new Term[0])); + return termManager.mkTerm(Kind.REGEXP_CONCAT, parts.toArray(new Term[0])); } @Override protected Term union(Term pParam1, Term pParam2) { - return solver.mkTerm(Kind.REGEXP_UNION, pParam1, pParam2); + return termManager.mkTerm(Kind.REGEXP_UNION, pParam1, pParam2); } @Override protected Term intersection(Term pParam1, Term pParam2) { - return solver.mkTerm(Kind.REGEXP_INTER, pParam1, pParam2); + return termManager.mkTerm(Kind.REGEXP_INTER, pParam1, pParam2); } @Override protected Term closure(Term pParam) { - return solver.mkTerm(Kind.REGEXP_STAR, pParam); + return termManager.mkTerm(Kind.REGEXP_STAR, pParam); } @Override protected Term complement(Term pParam) { - return solver.mkTerm(Kind.REGEXP_COMPLEMENT, pParam); + return termManager.mkTerm(Kind.REGEXP_COMPLEMENT, pParam); } @Override protected Term difference(Term pParam1, Term pParam2) { - return solver.mkTerm(Kind.REGEXP_DIFF, pParam1, pParam2); + return termManager.mkTerm(Kind.REGEXP_DIFF, pParam1, pParam2); } @Override protected Term toIntegerFormula(Term pParam) { - return solver.mkTerm(Kind.STRING_TO_INT, pParam); + return termManager.mkTerm(Kind.STRING_TO_INT, pParam); } @Override protected Term toStringFormula(Term pParam) { Preconditions.checkArgument( - pParam.getSort().equals(solver.getIntegerSort()) || pParam.isIntegerValue(), + pParam.getSort().equals(termManager.getIntegerSort()) || pParam.isIntegerValue(), "CVC5 only supports INT to STRING conversion."); - return solver.mkTerm(Kind.STRING_FROM_INT, pParam); + return termManager.mkTerm(Kind.STRING_FROM_INT, pParam); } @Override protected Term toCodePoint(Term pParam) { - return solver.mkTerm(Kind.STRING_TO_CODE, pParam); + return termManager.mkTerm(Kind.STRING_TO_CODE, pParam); } @Override protected Term fromCodePoint(Term pParam) { - return solver.mkTerm(Kind.STRING_FROM_CODE, pParam); + return termManager.mkTerm(Kind.STRING_FROM_CODE, pParam); } } diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5UFManager.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5UFManager.java index 1b8a8032a5..a77bb3a610 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5UFManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5UFManager.java @@ -8,12 +8,12 @@ package org.sosy_lab.java_smt.solvers.cvc5; -import io.github.cvc5.Solver; import io.github.cvc5.Sort; import io.github.cvc5.Term; +import io.github.cvc5.TermManager; import org.sosy_lab.java_smt.basicimpl.AbstractUFManager; -class CVC5UFManager extends AbstractUFManager { +class CVC5UFManager extends AbstractUFManager { CVC5UFManager(CVC5FormulaCreator pCreator) { super(pCreator); diff --git a/src/org/sosy_lab/java_smt/test/InterpolatingProverTest.java b/src/org/sosy_lab/java_smt/test/InterpolatingProverTest.java index 150e792f5c..21f8a8f6f6 100644 --- a/src/org/sosy_lab/java_smt/test/InterpolatingProverTest.java +++ b/src/org/sosy_lab/java_smt/test/InterpolatingProverTest.java @@ -344,21 +344,7 @@ public void sequentialInterpolationIsNotRepeatedIndividualInterpolation() // sequential interpolation should always work as expected checkItpSequence(ImmutableList.of(A, B, C), itpSeq); - - if (solverToUse() == Solvers.CVC5) { - assertThatFormula(A).implies(itp1); - assertThatFormula(bmgr.and(A, B)).implies(itp2); - assertThatFormula(bmgr.and(itp1, B, C)).isUnsatisfiable(); - assertThatFormula(bmgr.and(itp2, C)).isUnsatisfiable(); - - // this is a counterexample for sequential interpolation via individual interpolants: - assertThatFormula(bmgr.not(bmgr.implication(bmgr.and(itp1, B), itp2))).isSatisfiable(); - - } else { - // other solvers satisfy this condition, - // because they internally use the same proof for all interpolation queries - checkItpSequence(ImmutableList.of(A, B, C), List.of(itp1, itp2)); - } + checkItpSequence(ImmutableList.of(A, B, C), List.of(itp1, itp2)); } @Test diff --git a/src/org/sosy_lab/java_smt/test/SolverContextFactoryTest.java b/src/org/sosy_lab/java_smt/test/SolverContextFactoryTest.java index f28b830d0d..c858e366e9 100644 --- a/src/org/sosy_lab/java_smt/test/SolverContextFactoryTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverContextFactoryTest.java @@ -93,10 +93,15 @@ private void requireSupportedOperatingSystem() { return; case BOOLECTOR: case CVC4: - case CVC5: case YICES2: assume.that(IS_LINUX).isTrue(); return; + case CVC5: + assume.that(IS_LINUX || IS_WINDOWS).isTrue(); + if (IS_LINUX) { + assume.that(isSufficientVersionOfLibcxx("cvc5jni")).isTrue(); + } + return; case OPENSMT: assume.that(IS_LINUX).isTrue(); assume.that(isSufficientVersionOfLibcxx("opensmtj")).isTrue(); @@ -149,6 +154,8 @@ private String[] getRequiredLibcxx(String library) { return new String[] {"GLIBC_2.33", "GLIBCXX_3.4.26", "GLIBCXX_3.4.29"}; case "mathsat5j": return new String[] {"GLIBC_2.33"}; + case "cvc5jni": + return new String[] {"GLIBC_2.32"}; default: return new String[] {}; } diff --git a/src/org/sosy_lab/java_smt/test/SolverContextTest.java b/src/org/sosy_lab/java_smt/test/SolverContextTest.java index f8146ee380..ae43a00463 100644 --- a/src/org/sosy_lab/java_smt/test/SolverContextTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverContextTest.java @@ -11,6 +11,7 @@ import static com.google.common.truth.Truth.assertThat; import static com.google.common.truth.TruthJUnit.assume; import static org.junit.Assert.assertThrows; +import static org.sosy_lab.java_smt.test.SolverContextFactoryTest.IS_WINDOWS; import org.junit.Test; import org.sosy_lab.common.configuration.InvalidConfigurationException; @@ -148,6 +149,10 @@ public void testCVC5WithValidOptions() throws InvalidConfigurationException { public void testCVC5WithValidOptionsTimeLimit() throws InvalidConfigurationException, InterruptedException { assume().that(solverToUse()).isEqualTo(Solvers.CVC5); + assume() + .withMessage("CVC5 has an issue with creating and closing a second context on Windows.") + .that(IS_WINDOWS) + .isFalse(); // tlimit-per is time limit in ms of wall clock time per query var configValid = diff --git a/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java b/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java index 654788f28c..7619b7b1fe 100644 --- a/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java @@ -178,6 +178,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(); + assume().that(solverToUse()).isNotEqualTo(Solvers.CVC5); BooleanFormula formula = hardProblem.generate(DEFAULT_PROBLEM_SIZE);