CVC5: Updated the JavaSMT backend for CVC5 to use the new TermManager. See cvc5/cvc5#10426 for the interface. This will solve issue #310.

Author: daniel-raffler

Diff for: src/org/sosy_lab/java_smt/solvers/cvc5/CVC5AbstractProver.java

@@ -17,6 +17,7 @@
 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;
@@ -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);
   }
 

Diff for: 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<Term, Sort, Solver, Term> {
+public class CVC5ArrayFormulaManager extends AbstractArrayFormulaManager<Term, Sort, TermManager,
+    Term> {
 
-  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 <TI extends Formula, TE extends Formula> Term internalMakeArray(
   protected <TI extends Formula, TE extends Formula> Term internalMakeArray(
       FormulaType<TI> pIndexType, FormulaType<TE> 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 for: src/org/sosy_lab/java_smt/solvers/cvc5/CVC5BitvectorFormulaManager.java

@@ -11,39 +11,39 @@
 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<Term, Sort, Solver, Term> {
+    extends AbstractBitvectorFormulaManager<Term, Sort, TermManager, Term> {
 
-  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
   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<Term> pParam) {
-    return solver.mkTerm(Kind.DISTINCT, pParam.toArray(new Term[0]));
+    return termManager.mkTerm(Kind.DISTINCT, pParam.toArray(new Term[0]));
   }
 }