Skip to content

Commit

Permalink
CVC5: Updated the JavaSMT backend for CVC5 to use the new TermManager…
Browse files Browse the repository at this point in the history 
…. See cvc5/cvc5#10426 for the interface. This will solve issue #310.
  • Loading branch information
@daniel-raffler
daniel-raffler committed Apr 4, 2024
1 parent 8bd80fb commit 7d7b00c
Show file tree
Hide file tree
Showing 20 changed files with 662 additions and 586 deletions.
4 changes: 3 additions & 1 deletion src/org/sosy_lab/java_smt/solvers/cvc5/CVC5AbstractProver.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,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.ArrayList;
import java.util.Collection;
Expand Down Expand Up @@ -52,8 +53,9 @@ protected CVC5AbstractProver(
mgr = pMgr;
creator = pFormulaCreator;
incremental = !enableSL;
solver = new Solver();

TermManager termManager = creator.getEnv();
solver = new Solver(termManager);
setSolverOptions(randomSeed, pOptions, solver);
}

Expand Down
15 changes: 8 additions & 7 deletions src/org/sosy_lab/java_smt/solvers/cvc5/CVC5ArrayFormulaManager.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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.api.FormulaType.ArrayFormulaType;
import org.sosy_lab.java_smt.basicimpl.AbstractArrayFormulaManager;

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
Expand All @@ -48,6 +49,6 @@ protected <TI extends Formula, TE extends Formula> Term internalMakeArray(

@Override
protected Term equivalence(Term pArray1, Term pArray2) {
return solver.mkTerm(Kind.EQUAL, pArray1, pArray2);
return termManager.mkTerm(Kind.EQUAL, pArray1, pArray2);
}
}
102 changes: 51 additions & 51 deletions src/org/sosy_lab/java_smt/solvers/cvc5/CVC5BitvectorFormulaManager.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 "
Expand All @@ -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 "
Expand All @@ -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 "
Expand All @@ -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(
Expand All @@ -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);
Expand All @@ -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);
Expand All @@ -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 "
Expand All @@ -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()) {
Expand All @@ -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);
}

Expand All @@ -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]));
}
}
Loading

0 comments on commit 7d7b00c

Please sign in to comment.