diff --git a/build/build-publish-solvers/solver-cvc4.xml b/build/build-publish-solvers/solver-cvc4.xml index 29a671396c..749a7397a4 100644 --- a/build/build-publish-solvers/solver-cvc4.xml +++ b/build/build-publish-solvers/solver-cvc4.xml @@ -12,15 +12,15 @@ SPDX-License-Identifier: Apache-2.0 - - - + + + Please specify the path to CVC4 with the flag -Dcvc4.path=/path/to/cvc4. The path has to point to the root CVC4 folder, i.e., - a checkout of the official git repository from 'https://github.com/CVC4/CVC4.git'. + a checkout of the official git repository from 'https://github.com/CVC4/CVC4-archived.git'. Note that shell substitutions do not work and a full absolute path has to be specified. @@ -36,56 +36,94 @@ SPDX-License-Identifier: Apache-2.0 - + + - + + + - + + - + - - - - - - - - - - - + - - + + + - - - - + + + + + + + + + + + + + + + - - - + + + + + + + cvc4]]> + + + + + + + + + + + + + + + + + + diff --git a/doc/Developers-How-to-Release-into-Ivy.md b/doc/Developers-How-to-Release-into-Ivy.md index 634dbc7886..0c735c7fdf 100644 --- a/doc/Developers-How-to-Release-into-Ivy.md +++ b/doc/Developers-How-to-Release-into-Ivy.md @@ -129,6 +129,21 @@ Example: ant publish-z3-legacy -Dz3.path=../solvers/z3/z3 -Dz3.customRev=4.5.0 ``` +### Publishing CVC4 + +We use the Docker image with Ubuntu 18.04 for publishing CVC4. +Please manually add two additional dependencies before running the build script: + +```bash +pip3 install toml +apt-get install antlr3 libantlr3c-dev +``` + +Then run the build script to publish the bindings: + +```bash +ant publish-cvc4 -Dcvc4.path=/workspace/CVC4-archived -Dcvc4.customRev=1.8.1 +``` ### Publishing CVC5 diff --git a/lib/ivy.xml b/lib/ivy.xml index ad599f7fd6..7444de2cd9 100644 --- a/lib/ivy.xml +++ b/lib/ivy.xml @@ -190,7 +190,7 @@ SPDX-License-Identifier: Apache-2.0 - + diff --git a/lib/native/x86_64-linux/libcvc4.so b/lib/native/x86_64-linux/libcvc4.so index 43896ee4ca..bbb04644ed 120000 --- a/lib/native/x86_64-linux/libcvc4.so +++ b/lib/native/x86_64-linux/libcvc4.so @@ -1 +1 @@ -../../java/runtime-cvc4/libcvc4.so \ No newline at end of file +../../java/runtime-cvc4/x64/libcvc4.so \ No newline at end of file diff --git a/lib/native/x86_64-linux/libcvc4jni.so b/lib/native/x86_64-linux/libcvc4jni.so index c1984b81e6..15778e28ff 120000 --- a/lib/native/x86_64-linux/libcvc4jni.so +++ b/lib/native/x86_64-linux/libcvc4jni.so @@ -1 +1 @@ -../../java/runtime-cvc4/libcvc4jni.so \ No newline at end of file +../../java/runtime-cvc4/x64/libcvc4jni.so \ No newline at end of file diff --git a/lib/native/x86_64-linux/libcvc4parser.so b/lib/native/x86_64-linux/libcvc4parser.so deleted file mode 120000 index 59e9dc8e4a..0000000000 --- a/lib/native/x86_64-linux/libcvc4parser.so +++ /dev/null @@ -1 +0,0 @@ -../../java/runtime-cvc4/libcvc4parser.so \ No newline at end of file diff --git a/solvers_ivy_conf/ivy_cvc4.xml b/solvers_ivy_conf/ivy_cvc4.xml index e415e3f427..52d53aee69 100644 --- a/solvers_ivy_conf/ivy_cvc4.xml +++ b/solvers_ivy_conf/ivy_cvc4.xml @@ -23,14 +23,27 @@ SPDX-License-Identifier: Apache-2.0 - + + + + + + + + + + + + - - - - + + + + + + diff --git a/src/org/sosy_lab/java_smt/api/FormulaType.java b/src/org/sosy_lab/java_smt/api/FormulaType.java index 8835ad7ebe..60dcb75177 100644 --- a/src/org/sosy_lab/java_smt/api/FormulaType.java +++ b/src/org/sosy_lab/java_smt/api/FormulaType.java @@ -21,8 +21,10 @@ import com.google.errorprone.annotations.Immutable; import java.util.List; import java.util.Set; +import java.util.regex.Pattern; import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula; import org.sosy_lab.java_smt.api.NumeralFormula.RationalFormula; +import org.sosy_lab.java_smt.basicimpl.Tokenizer; /** * Type of a formula. @@ -418,8 +420,7 @@ public String toString() { @Override public String toSMTLIBString() { - throw new UnsupportedOperationException( - "rounding mode is not expected in symbol declarations"); + return "RoundingMode"; } } @@ -613,4 +614,37 @@ public static FormulaType fromString(String t) { throw new AssertionError("unknown type:" + t); } } + + public static FormulaType fromSMTLIBString(String t) { + if (t.equals("Bool")) { + return BooleanType; + } else if (t.equals("Int")) { + return IntegerType; + } else if (t.equals("Real")) { + return RationalType; + } else if (t.equals("String")) { + return StringType; + } else if (t.equals("RegLan")) { + return RegexType; + } else if (t.equals("RoundingMode")) { + return FloatingPointRoundingModeType; + } else if (t.startsWith("(_ FloatingPoint")) { + var m = Pattern.compile("\\(\\s*_\\s+FloatingPoint\\s+(\\d+)\\s+(\\d+)\\s*\\)").matcher(t); + checkArgument(m.find()); + return FormulaType.getFloatingPointTypeFromSizesWithHiddenBit( + Integer.parseInt(m.group(1)), Integer.parseInt(m.group(2))); + } else if (t.startsWith("(_ BitVec")) { + var m = Pattern.compile("\\(\\s*_\\s+BitVec\\s+(\\d+)\\s*\\)").matcher(t); + checkArgument(m.find()); + return FormulaType.getBitvectorTypeWithSize(Integer.parseInt(m.group(1))); + } else if (t.startsWith("(Array")) { + var tokens = Tokenizer.tokenize(t.substring(1, t.length() - 1)); + checkArgument(tokens.size() == 3); + var domain = fromSMTLIBString(tokens.get(1)); + var range = fromSMTLIBString(tokens.get(2)); + return FormulaType.getArrayType(domain, range); + } else { + throw new AssertionError("unknown type:" + t); + } + } } diff --git a/src/org/sosy_lab/java_smt/basicimpl/Tokenizer.java b/src/org/sosy_lab/java_smt/basicimpl/Tokenizer.java index 0d7c3912ff..fa65f861c8 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/Tokenizer.java +++ b/src/org/sosy_lab/java_smt/basicimpl/Tokenizer.java @@ -121,9 +121,16 @@ public static List tokenize(String input) { // Handle opening brackets token.append("("); level++; + } else if (c == ')') { + throw new IllegalArgumentException( + "parentheses do not match, unexpected closing parenthesis"); } else { - // Should be unreachable: all top-level expressions need parentheses around them - throw new IllegalArgumentException(); + token.append(c); + } + } else { + if (!token.isEmpty()) { + builder.add(token.toString()); + token = new StringBuilder(); } } } else { @@ -146,7 +153,10 @@ public static List tokenize(String input) { } if (level != 0) { // Throw an exception if the brackets don't match - throw new IllegalArgumentException("brackets do not match, too many open brackets"); + throw new IllegalArgumentException("parentheses do not match, too many open parentheses"); + } + if (!token.isEmpty()) { + builder.add(token.toString()); } return builder.build(); } diff --git a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4ArrayFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4ArrayFormulaManager.java index 79c121a400..89d5b645a8 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4ArrayFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4ArrayFormulaManager.java @@ -50,7 +50,8 @@ protected Expr internalMakeArray( protected Expr internalMakeArray( FormulaType pIndexType, FormulaType pElementType, Expr defaultElement) { final Type cvc4ArrayType = toSolverType(FormulaType.getArrayType(pIndexType, pElementType)); - return exprManager.mkConst(new ArrayStoreAll((ArrayType) cvc4ArrayType, defaultElement)); + return exprManager.mkConst( + new ArrayStoreAll(exprManager, (ArrayType) cvc4ArrayType, defaultElement)); } @Override diff --git a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4BitvectorFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4BitvectorFormulaManager.java index 11083dad09..73242a0757 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4BitvectorFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4BitvectorFormulaManager.java @@ -13,7 +13,6 @@ import edu.stanford.CVC4.BitVectorRotateLeft; import edu.stanford.CVC4.BitVectorRotateRight; import edu.stanford.CVC4.BitVectorSignExtend; -import edu.stanford.CVC4.BitVectorType; import edu.stanford.CVC4.BitVectorZeroExtend; import edu.stanford.CVC4.Expr; import edu.stanford.CVC4.ExprManager; @@ -235,7 +234,7 @@ protected Expr toIntegerFormulaImpl(Expr pBv, boolean pSigned) { // TODO check what is cheaper for the solver: // checking the first BV-bit or computing max-int-value for the given size - final int size = Math.toIntExact(new BitVectorType(pBv.getType()).getSize()); + final int size = ((BitvectorType) formulaCreator.getFormulaType(pBv)).getSize(); final BigInteger modulo = BigInteger.ONE.shiftLeft(size); final BigInteger maxInt = BigInteger.ONE.shiftLeft(size - 1).subtract(BigInteger.ONE); final Expr moduloExpr = exprManager.mkConst(new Rational(modulo.toString())); @@ -254,8 +253,6 @@ protected Expr toIntegerFormulaImpl(Expr pBv, boolean pSigned) { @Override protected Expr distinctImpl(List pParam) { - vectorExpr param = new vectorExpr(); - pParam.forEach(param::add); - return exprManager.mkExpr(Kind.DISTINCT, param); + return exprManager.mkExpr(Kind.DISTINCT, new vectorExpr(exprManager, pParam)); } } diff --git a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4BooleanFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4BooleanFormulaManager.java index 4acf4d5deb..03989581f9 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4BooleanFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4BooleanFormulaManager.java @@ -87,11 +87,7 @@ protected Expr andImpl(Collection pParams) { return switch (operands.size()) { case 0 -> cvc4True; case 1 -> Iterables.getOnlyElement(operands); - default -> { - vectorExpr vExpr = new vectorExpr(); - operands.forEach(vExpr::add); - yield exprManager.mkExpr(Kind.AND, vExpr); - } + default -> exprManager.mkExpr(Kind.AND, new vectorExpr(exprManager, operands)); }; } @@ -127,13 +123,7 @@ protected Expr orImpl(Collection pParams) { return switch (operands.size()) { case 0 -> cvc4False; case 1 -> Iterables.getOnlyElement(operands); - default -> { - vectorExpr vExpr = new vectorExpr(); - for (Expr e : operands) { - vExpr.add(e); - } - yield exprManager.mkExpr(Kind.OR, vExpr); - } + default -> exprManager.mkExpr(Kind.OR, new vectorExpr(exprManager, operands)); }; } diff --git a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java index 8050503f4d..7a2c9e940e 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java @@ -19,8 +19,6 @@ import com.google.common.collect.Iterables; import com.google.common.primitives.Ints; import edu.stanford.CVC4.ArrayStoreAll; -import edu.stanford.CVC4.ArrayType; -import edu.stanford.CVC4.BitVectorType; import edu.stanford.CVC4.Expr; import edu.stanford.CVC4.ExprManager; import edu.stanford.CVC4.FunctionType; @@ -149,25 +147,13 @@ protected FormulaType getArrayFormu @SuppressWarnings("unchecked") @Override public FormulaType getFormulaType(T pFormula) { - Type t = extractInfo(pFormula).getType(); - if (pFormula instanceof BitvectorFormula) { - checkArgument(t.isBitVector(), "BitvectorFormula with actual type %s: %s", t, pFormula); + if (pFormula instanceof BitvectorFormula + || pFormula instanceof FloatingPointFormula + || pFormula instanceof ArrayFormula) { return (FormulaType) getFormulaType(extractInfo(pFormula)); - - } else if (pFormula instanceof FloatingPointFormula) { - checkArgument( - t.isFloatingPoint(), "FloatingPointFormula with actual type %s: %s", t, pFormula); - edu.stanford.CVC4.FloatingPointType fpType = new edu.stanford.CVC4.FloatingPointType(t); - return (FormulaType) - FormulaType.getFloatingPointTypeFromSizesWithHiddenBit( - (int) fpType.getExponentSize(), (int) fpType.getSignificandSize()); // with hidden bit - - } else if (pFormula instanceof ArrayFormula) { - FormulaType arrayIndexType = getArrayFormulaIndexType((ArrayFormula) pFormula); - FormulaType arrayElementType = getArrayFormulaElementType((ArrayFormula) pFormula); - return (FormulaType) FormulaType.getArrayType(arrayIndexType, arrayElementType); + } else { + return super.getFormulaType(pFormula); } - return super.getFormulaType(pFormula); } @Override @@ -180,32 +166,16 @@ private FormulaType getFormulaTypeFromTermType(Type t) { return FormulaType.BooleanType; } else if (t.isInteger()) { return FormulaType.IntegerType; - } else if (t.isBitVector()) { - // apparently, we can get a t instanceof Type here for that t instanceof BitVectorType does - // not hold, hence we use the new BitVectorType(t) here as a workaround: - return FormulaType.getBitvectorTypeWithSize((int) new BitVectorType(t).getSize()); - } else if (t.isFloatingPoint()) { - edu.stanford.CVC4.FloatingPointType fpType = new edu.stanford.CVC4.FloatingPointType(t); - return FormulaType.getFloatingPointTypeFromSizesWithHiddenBit( - (int) fpType.getExponentSize(), (int) fpType.getSignificandSize()); // with hidden bit - } else if (t.isRoundingMode()) { - return FormulaType.FloatingPointRoundingModeType; } else if (t.isReal()) { // The theory REAL in CVC4 is the theory of (infinite precision!) real numbers. // As such, the theory RATIONAL is contained in REAL. TODO: find a better solution. return FormulaType.RationalType; - } else if (t.isArray()) { - ArrayType arrayType = new ArrayType(t); // instead of casting, create a new type. - FormulaType indexType = getFormulaTypeFromTermType(arrayType.getIndexType()); - FormulaType elementType = getFormulaTypeFromTermType(arrayType.getConstituentType()); - return FormulaType.getArrayType(indexType, elementType); } else if (t.isString()) { return FormulaType.StringType; } else if (t.isRegExp()) { return FormulaType.RegexType; } else { - throw new AssertionError( - "Unhandled type '%s' with base type '%s'.".formatted(t, t.getBaseType())); + return FormulaType.fromSMTLIBString(t.toString()); } } @@ -384,8 +354,9 @@ public R visit(FormulaVisitor visitor, Formula formula, final Expr f) { List args = ImmutableList.copyOf(Iterables.transform(f, this::encapsulate)); List> argsTypes = new ArrayList<>(); Expr operator = normalize(f.getOperator()); - if (operator.getType().isFunction()) { - vectorType argTypes = new FunctionType(operator.getType()).getArgTypes(); + if (operator.getType().isFunction() + && operator.getType() instanceof FunctionType functionType) { + vectorType argTypes = functionType.getArgTypes(); for (int i = 0; i < argTypes.size(); i++) { argsTypes.add(getFormulaTypeFromTermType(argTypes.get(i))); } @@ -582,11 +553,7 @@ public Expr callFunctionImpl(Expr pDeclaration, List pArgs) { return pDeclaration; } } else { - vectorExpr args = new vectorExpr(); - for (Expr expr : pArgs) { - args.add(expr); - } - return exprManager.mkExpr(pDeclaration, args); + return exprManager.mkExpr(pDeclaration, new vectorExpr(exprManager, pArgs)); } } @@ -597,21 +564,17 @@ public Expr declareUFImpl(String pName, Type pReturnType, List pArgTypes) } Expr exp = functionsCache.get(pName); if (exp == null) { - vectorType args = new vectorType(); - for (Type t : pArgTypes) { - args.add(t); - } - exp = exprManager.mkVar(pName, exprManager.mkFunctionType(args, pReturnType)); + exp = + exprManager.mkVar( + pName, + exprManager.mkFunctionType(new vectorType(exprManager, pArgTypes), pReturnType)); functionsCache.put(pName, exp); } else { // We can't cast the cached type to FormulaType, even though it is a function type, due to a // bug in the CVC4 Java bindings. As a workaround we create another function type for the // current arguments and then compare it to the type from the cache - vectorType args = new vectorType(); - for (Type t : pArgTypes) { - args.add(t); - } - var argumentType = exprManager.mkFunctionType(args, pReturnType); + var argumentType = + exprManager.mkFunctionType(new vectorType(exprManager, pArgTypes), pReturnType); var cachedType = exp.getType(); Preconditions.checkArgument( cachedType.equals(argumentType), diff --git a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaManager.java b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaManager.java index 330547eeca..5d306844cb 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaManager.java @@ -73,10 +73,7 @@ public Expr equalImpl(Expr pArg1, Expr pArgs) { @Override public Expr distinctImpl(Iterable pArgs) { - vectorExpr vec = new vectorExpr(); - for (Expr e : pArgs) { - vec.add(e); - } + vectorExpr vec = new vectorExpr(getEnvironment(), pArgs); if (vec.size() < 2) { return getEnvironment().mkConst(true); } else { diff --git a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4Model.java b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4Model.java index 44e9853843..cdfd0c4955 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4Model.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4Model.java @@ -15,7 +15,6 @@ import com.google.common.collect.Collections2; import com.google.common.collect.ImmutableList; import com.google.common.collect.ImmutableSet; -import edu.stanford.CVC4.ArrayType; import edu.stanford.CVC4.Expr; import edu.stanford.CVC4.ExprManager; import edu.stanford.CVC4.Kind; @@ -162,7 +161,7 @@ private List buildArrayAssignments(Expr expr, Expr value) { Expr select = creator.getEnv().mkExpr(Kind.SELECT, expr, index); // CASE 1: nested array dimension, let's recurse deeper - if (new ArrayType(expr.getType()).getConstituentType().isArray()) { + if (element.getType().isArray()) { result.addAll(buildArrayAssignments(select, element)); } else { diff --git a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4NativeAPITest.java b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4NativeAPITest.java index ee96f54adf..0477a0c5f0 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4NativeAPITest.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4NativeAPITest.java @@ -29,8 +29,6 @@ import edu.stanford.CVC4.Type; import edu.stanford.CVC4.UnsatCore; import edu.stanford.CVC4.vectorExpr; -import java.io.FileNotFoundException; -import java.io.UnsupportedEncodingException; import org.junit.After; import org.junit.AssumptionViolatedException; import org.junit.Before; @@ -532,9 +530,8 @@ public void checkQuantifierExistsIncomplete() { Expr zero = exprMgr.mkConst(new Rational(0)); Expr xBound = exprMgr.mkBoundVar("x", exprMgr.integerType()); - vectorExpr vec = new vectorExpr(); - vec.add(xBound); - Expr quantifiedVars = exprMgr.mkExpr(Kind.BOUND_VAR_LIST, vec); + Expr quantifiedVars = + exprMgr.mkExpr(Kind.BOUND_VAR_LIST, new vectorExpr(exprMgr, new Expr[] {xBound})); Expr aAtxEq0s = aAtxEq0.substitute(x, xBound); Expr exists = exprMgr.mkExpr(Kind.EXISTS, quantifiedVars, exprMgr.mkExpr(Kind.NOT, aAtxEq0s)); Expr notExists = exprMgr.mkExpr(Kind.NOT, exists); @@ -568,9 +565,8 @@ public void checkQuantifierEliminationLIA() { Expr body = exprMgr.mkExpr(Kind.OR, first, second); Expr xBound = exprMgr.mkBoundVar("x", exprMgr.integerType()); - vectorExpr vec = new vectorExpr(); - vec.add(xBound); - Expr quantifiedVars = exprMgr.mkExpr(Kind.BOUND_VAR_LIST, vec); + Expr quantifiedVars = + exprMgr.mkExpr(Kind.BOUND_VAR_LIST, new vectorExpr(exprMgr, new Expr[] {xBound})); Expr bodySubst = body.substitute(x, xBound); Expr assertion = exprMgr.mkExpr(Kind.FORALL, quantifiedVars, bodySubst); @@ -582,7 +578,7 @@ public void checkQuantifierEliminationLIA() { @SuppressWarnings("unused") @Test - public void checkQuantifierWithUf() throws FileNotFoundException, UnsupportedEncodingException { + public void checkQuantifierWithUf() { Expr var = exprMgr.mkVar("var", exprMgr.integerType()); // start with a normal, free variable! Expr boundVar = exprMgr.mkVar("boundVar", exprMgr.integerType()); @@ -603,9 +599,8 @@ public void checkQuantifierWithUf() throws FileNotFoundException, UnsupportedEnc // This is the bound variable used for boundVar Expr boundVarBound = exprMgr.mkBoundVar("boundVar", exprMgr.integerType()); - vectorExpr vec = new vectorExpr(); - vec.add(boundVarBound); - Expr quantifiedVars = exprMgr.mkExpr(Kind.BOUND_VAR_LIST, vec); + Expr quantifiedVars = + exprMgr.mkExpr(Kind.BOUND_VAR_LIST, new vectorExpr(exprMgr, new Expr[] {boundVarBound})); // Subst all boundVar variables with the bound version Expr bodySubst = body.substitute(boundVar, boundVarBound); Expr quantFormula = exprMgr.mkExpr(Kind.EXISTS, quantifiedVars, bodySubst); @@ -641,9 +636,8 @@ public void checkInterruptBehaviour() { Expr body = exprMgr.mkExpr(Kind.OR, aAtxEq0, aAtxEq1); Expr xBound = exprMgr.mkBoundVar("x_b", exprMgr.integerType()); - vectorExpr vec = new vectorExpr(); - vec.add(xBound); - Expr quantifiedVars = exprMgr.mkExpr(Kind.BOUND_VAR_LIST, vec); + Expr quantifiedVars = + exprMgr.mkExpr(Kind.BOUND_VAR_LIST, new vectorExpr(exprMgr, new Expr[] {xBound})); Expr bodySubst = body.substitute(x, xBound); Expr assertion = exprMgr.mkExpr(Kind.FORALL, quantifiedVars, bodySubst); @@ -685,9 +679,8 @@ public void checkQuantifierEliminationBV() { Kind.EQUAL, exprMgr.mkExpr(Kind.MULT, xBv, yBv), exprMgr.mkConst(new BitVector(1))); Expr xBound = exprMgr.mkBoundVar("y_bv", exprMgr.mkBitVectorType(width)); - vectorExpr vec = new vectorExpr(); - vec.add(xBound); - Expr quantifiedVars = exprMgr.mkExpr(Kind.BOUND_VAR_LIST, vec); + Expr quantifiedVars = + exprMgr.mkExpr(Kind.BOUND_VAR_LIST, new vectorExpr(exprMgr, new Expr[] {xBound})); Expr bodySubst = body.substitute(yBv, xBound); Expr assertion = exprMgr.mkExpr(Kind.EXISTS, quantifiedVars, bodySubst); diff --git a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4NumeralFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4NumeralFormulaManager.java index aacd719cab..8f7e4bda3d 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4NumeralFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4NumeralFormulaManager.java @@ -181,9 +181,7 @@ protected Expr distinctImpl(List pParam) { if (pParam.size() < 2) { return exprManager.mkConst(true); } else { - vectorExpr param = new vectorExpr(); - pParam.forEach(param::add); - return exprManager.mkExpr(Kind.DISTINCT, param); + return exprManager.mkExpr(Kind.DISTINCT, new vectorExpr(exprManager, pParam)); } } } diff --git a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4QuantifiedFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4QuantifiedFormulaManager.java index b6ec93c9c5..8f5bf116f0 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4QuantifiedFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4QuantifiedFormulaManager.java @@ -78,7 +78,7 @@ public Expr mkQuantifier(Quantifier pQ, List pVars, Expr pBody) { !pVars.isEmpty(), "Missing variables for quantifier '%s' and body '%s'.", pQ, pBody); // CVC4 uses its own lists for quantifier that may only have bound vars - vectorExpr vec = new vectorExpr(); + vectorExpr vec = new vectorExpr(exprManager); Expr substBody = pBody; // every free needs a bound copy. As the internal Id is different for every variable, even // with the same name, this is fine. diff --git a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4SolverContext.java b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4SolverContext.java index b5bd086812..318313ff43 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4SolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4SolverContext.java @@ -13,6 +13,8 @@ import edu.stanford.CVC4.ExprManager; import edu.stanford.CVC4.SExpr; import edu.stanford.CVC4.SmtEngine; +import java.util.ArrayList; +import java.util.List; import java.util.Set; import java.util.function.Consumer; import java.util.logging.Level; @@ -29,6 +31,10 @@ public final class CVC4SolverContext extends AbstractSolverContext { + // Keep a global list of all contexts to prevent the garbge collector from doing its job + // See https://github.com/sosy-lab/java-smt/issues/169 + private static List contexts = new ArrayList<>(); + // creator is final, except after closing, then null. private CVC4FormulaCreator creator; private final ShutdownNotifier shutdownNotifier; @@ -43,6 +49,10 @@ private CVC4SolverContext( this.creator = creator; shutdownNotifier = pShutdownNotifier; randomSeed = pRandomSeed; + + synchronized (CVC4SolverContext.class) { + contexts.add(this); + } } public static SolverContext create( @@ -117,8 +127,7 @@ public String getVersion() { @Override public void close() { if (creator != null) { - creator.getEnv().delete(); - creator = null; + // Never close the context } } diff --git a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4StringFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4StringFormulaManager.java index 29de4feb14..1b611e1b2d 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4StringFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4StringFormulaManager.java @@ -71,9 +71,7 @@ protected Expr length(Expr pParam) { @Override protected Expr concatImpl(List parts) { Preconditions.checkArgument(parts.size() > 1); - vectorExpr vector = new vectorExpr(); - parts.forEach(vector::add); - return exprManager.mkExpr(Kind.STRING_CONCAT, vector); + return exprManager.mkExpr(Kind.STRING_CONCAT, new vectorExpr(exprManager, parts)); } @Override @@ -129,7 +127,7 @@ protected Expr makeRegexImpl(String value) { @Override protected Expr noneImpl() { - return exprManager.mkExpr(Kind.REGEXP_EMPTY, new vectorExpr()); + return exprManager.mkExpr(Kind.REGEXP_EMPTY, new vectorExpr(exprManager)); } @Override @@ -139,7 +137,7 @@ protected Expr allImpl() { @Override protected Expr allCharImpl() { - return exprManager.mkExpr(Kind.REGEXP_SIGMA, new vectorExpr()); + return exprManager.mkExpr(Kind.REGEXP_SIGMA, new vectorExpr(exprManager)); } /** @@ -174,9 +172,7 @@ protected Expr range(Expr start, Expr end) { @Override protected Expr concatRegexImpl(List parts) { Preconditions.checkArgument(parts.size() > 1); - vectorExpr vector = new vectorExpr(); - parts.forEach(vector::add); - return exprManager.mkExpr(Kind.REGEXP_CONCAT, vector); + return exprManager.mkExpr(Kind.REGEXP_CONCAT, new vectorExpr(exprManager, parts)); } @Override diff --git a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4TheoremProver.java b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4TheoremProver.java index 57cb1dfd2f..6cac04b915 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4TheoremProver.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4TheoremProver.java @@ -37,6 +37,10 @@ class CVC4TheoremProver extends AbstractProverWithAllSat implements ProverEnvironment, BasicProverEnvironment { + // Keep a global list of all provers to prevent the garbge collector from doing its job + // See https://github.com/sosy-lab/java-smt/issues/169 + private static List provers = new ArrayList<>(); + private final CVC4FormulaCreator creator; private final int randomSeed; SmtEngine smtEngine; // final except for SL theory @@ -64,6 +68,10 @@ class CVC4TheoremProver extends AbstractProverWithAllSat BooleanFormulaManager pBmgr) { super(pOptions, pBmgr, pShutdownNotifier); + synchronized (CVC4TheoremProver.class) { + provers.add(this); + } + creator = pFormulaCreator; randomSeed = pRandomSeed; incremental = !enableSL; @@ -237,9 +245,7 @@ public Optional> unsatCoreOverAssumptions( @Override public void close() { if (!closed) { - exportMapping.delete(); - // smtEngine.delete(); - exprManager.delete(); + // Never release a prover } super.close(); } diff --git a/src/org/sosy_lab/java_smt/test/SolverContextTest.java b/src/org/sosy_lab/java_smt/test/SolverContextTest.java index 4ae681fa02..20b6568221 100644 --- a/src/org/sosy_lab/java_smt/test/SolverContextTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverContextTest.java @@ -109,7 +109,7 @@ public void testFormulaAccessAfterClose() { assertThat(term.hashCode()).isEqualTo(hash); assertThat(term).isEqualTo(term2); - // For CVC4 and Bitwuzla, we close the solver, however do not finalize and cleanup the terms, + // For CVC4, we close the solver, however, we do not finalize and cleanup the terms, // thus direct access is possible, operations are forbidden. // See https://github.com/sosy-lab/java-smt/issues/169 assume() @@ -117,7 +117,7 @@ public void testFormulaAccessAfterClose() { "Solver %s does not support to access formulae after closing the context", solverToUse()) .that(solverToUse()) - .isNoneOf(Solvers.CVC4, Solvers.BITWUZLA); + .isNotEqualTo(Solvers.CVC4); // Java-based solvers allow more, i.e. they wait for GC, which is nice.