diff --git a/src/org/sosy_lab/java_smt/api/FunctionDeclarationKind.java b/src/org/sosy_lab/java_smt/api/FunctionDeclarationKind.java index 02f1b7281f..8eef4d99ad 100644 --- a/src/org/sosy_lab/java_smt/api/FunctionDeclarationKind.java +++ b/src/org/sosy_lab/java_smt/api/FunctionDeclarationKind.java @@ -298,6 +298,8 @@ public enum FunctionDeclarationKind { STR_TO_CODE, STR_LT, STR_LE, + + RE_NONE, RE_PLUS, RE_STAR, RE_OPTIONAL, @@ -308,6 +310,13 @@ public enum FunctionDeclarationKind { RE_COMPLEMENT, RE_DIFFERENCE, + // Separation logic + SEP_EMP, + SEP_NIL, + SEP_PTO, + SEP_STAR, + SEP_WAND, + // default case /** diff --git a/src/org/sosy_lab/java_smt/api/SLFormulaManager.java b/src/org/sosy_lab/java_smt/api/SLFormulaManager.java index 46cfcf7e01..15575fa119 100644 --- a/src/org/sosy_lab/java_smt/api/SLFormulaManager.java +++ b/src/org/sosy_lab/java_smt/api/SLFormulaManager.java @@ -80,8 +80,8 @@ public interface SLFormulaManager { * * @param the type of the address formula. * @param the type of the address formula type. - * @param pAdressType the type of the address formula. + * @param pAddressType the type of the address formula. * @return a formula representing the "nil" element for the given address type. */ - > AF makeNilElement(AT pAdressType); + > AF makeNilElement(AT pAddressType); } diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractNumeralFormulaManager.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractNumeralFormulaManager.java index 72d3e65574..b3fc78f24f 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractNumeralFormulaManager.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractNumeralFormulaManager.java @@ -207,11 +207,15 @@ public ResultFormulaType sum(List operands) { } protected TFormulaInfo sumImpl(List operands) { - TFormulaInfo result = makeNumberImpl(0); - for (TFormulaInfo operand : operands) { - result = add(result, operand); + if (operands.isEmpty()) { + return makeNumberImpl(0); + } else { + TFormulaInfo result = operands.get(0); + for (TFormulaInfo operand : operands.subList(1, operands.size())) { + result = add(result, operand); + } + return result; } - return result; } @Override 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 6bb9882a89..0d93695191 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java @@ -336,7 +336,7 @@ public R visit(FormulaVisitor visitor, Formula formula, final Expr f) { } else if (type.isRoundingMode()) { return visitor.visitConstant(formula, getRoundingMode(f)); } else if (type.isString()) { - return visitor.visitConstant(formula, f.getConstString()); + return visitor.visitConstant(formula, f.getConstString().toString()); } else if (type.isArray()) { ArrayStoreAll storeAll = f.getConstArrayStoreAll(); Expr constant = storeAll.getExpr(); @@ -481,6 +481,7 @@ private Expr normalize(Expr operator) { .put(Kind.BITVECTOR_NEG, FunctionDeclarationKind.BV_NEG) .put(Kind.BITVECTOR_EXTRACT, FunctionDeclarationKind.BV_EXTRACT) .put(Kind.BITVECTOR_CONCAT, FunctionDeclarationKind.BV_CONCAT) + .put(Kind.BITVECTOR_TO_NAT, FunctionDeclarationKind.UBV_TO_INT) .put(Kind.BITVECTOR_SIGN_EXTEND, FunctionDeclarationKind.BV_SIGN_EXTENSION) .put(Kind.BITVECTOR_ZERO_EXTEND, FunctionDeclarationKind.BV_ZERO_EXTENSION) // Floating-point theory @@ -544,6 +545,12 @@ private Expr normalize(Expr operator) { .put(Kind.SELECT, FunctionDeclarationKind.SELECT) .put(Kind.STORE, FunctionDeclarationKind.STORE) .put(Kind.STORE_ALL, FunctionDeclarationKind.CONST) + // Separation logic + .put(Kind.SEP_EMP, FunctionDeclarationKind.SEP_EMP) + .put(Kind.SEP_NIL, FunctionDeclarationKind.SEP_NIL) + .put(Kind.SEP_PTO, FunctionDeclarationKind.SEP_PTO) + .put(Kind.SEP_STAR, FunctionDeclarationKind.SEP_STAR) + .put(Kind.SEP_WAND, FunctionDeclarationKind.SEP_WAND) .buildOrThrow(); private FunctionDeclarationKind getDeclarationKind(Expr f) { 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 4f0004b6cd..756c7939c5 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java @@ -648,6 +648,7 @@ private Term normalize(Term operator) { .put(Kind.STRING_FROM_CODE, FunctionDeclarationKind.STR_FROM_CODE) .put(Kind.STRING_LT, FunctionDeclarationKind.STR_LT) .put(Kind.STRING_LEQ, FunctionDeclarationKind.STR_LE) + .put(Kind.REGEXP_NONE, FunctionDeclarationKind.RE_NONE) .put(Kind.REGEXP_PLUS, FunctionDeclarationKind.RE_PLUS) .put(Kind.REGEXP_STAR, FunctionDeclarationKind.RE_STAR) .put(Kind.REGEXP_OPT, FunctionDeclarationKind.RE_OPTIONAL) @@ -660,6 +661,12 @@ private Term normalize(Term operator) { .put(Kind.SELECT, FunctionDeclarationKind.SELECT) .put(Kind.STORE, FunctionDeclarationKind.STORE) .put(Kind.CONST_ARRAY, FunctionDeclarationKind.CONST) + // Separation logic + .put(Kind.SEP_EMP, FunctionDeclarationKind.SEP_EMP) + .put(Kind.SEP_NIL, FunctionDeclarationKind.SEP_NIL) + .put(Kind.SEP_PTO, FunctionDeclarationKind.SEP_PTO) + .put(Kind.SEP_STAR, FunctionDeclarationKind.SEP_STAR) + .put(Kind.SEP_WAND, FunctionDeclarationKind.SEP_WAND) .build(); private FunctionDeclarationKind getDeclarationKind(Term f) { 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 379430a0b6..c16bd41fb7 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java @@ -158,6 +158,11 @@ StringBuilder getSMTLIB2DeclarationsFor(ImmutableMap varsAndUFs) { return declarations; } + @Override + protected Term simplify(Term f) throws InterruptedException { + return creator.getSolver().simplify(f); + } + @Override public T substitute( final T f, final Map fromToMapping) { 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 1f03712b1f..f79bcf0d41 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5InterpolatingProver.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5InterpolatingProver.java @@ -181,7 +181,8 @@ private Term getCVC5Interpolation(Collection formulasA, Collection f Term interpolant; try { itpSolver.assertFormula(phiPlus); - interpolant = itpSolver.getInterpolant(termManager.mkTerm(Kind.NOT, phiMinus)); + interpolant = + itpSolver.simplify(itpSolver.getInterpolant(termManager.mkTerm(Kind.NOT, phiMinus))); } finally { itpSolver.deletePointer(); } 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 6bb7c0f618..3f112c6296 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5StringFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5StringFormulaManager.java @@ -140,17 +140,7 @@ protected Term allCharImpl() { @Override 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 = termManager.mkInteger(1); - Term cond = - termManager.mkTerm( - Kind.AND, - 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()); + return termManager.mkTerm(Kind.REGEXP_RANGE, start, end); } @Override diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java index 5c053434a7..ffee210878 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java @@ -602,6 +602,8 @@ private FunctionDeclarationKind getDeclarationKind(IExpression input) { return FunctionDeclarationKind.OTHER; } else if (fun == ModuloArithmetic.int_cast()) { return FunctionDeclarationKind.OTHER; + } else if (fun == PrincessEnvironment.stringTheory.re_none()) { + return FunctionDeclarationKind.RE_NONE; } else { return FunctionDeclarationKind.UF; } diff --git a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolNumeralFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolNumeralFormulaManager.java index 7c7657d1d1..9a8b12c5bb 100644 --- a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolNumeralFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolNumeralFormulaManager.java @@ -16,6 +16,7 @@ import de.uni_freiburg.informatik.ultimate.logic.Script; import de.uni_freiburg.informatik.ultimate.logic.Sort; import de.uni_freiburg.informatik.ultimate.logic.Term; +import java.math.BigInteger; import java.util.ArrayDeque; import java.util.Arrays; import java.util.Deque; @@ -174,4 +175,16 @@ public Term lessThan(Term pNumber1, Term pNumber2) { public Term lessOrEquals(Term pNumber1, Term pNumber2) { return env.term("<=", pNumber1, pNumber2); } + + @Override + protected Term sumImpl(List operands) { + switch (operands.size()) { + case 0: + return env.numeral(BigInteger.ZERO); + case 1: + return operands.get(0); + default: + return env.term("+", operands.toArray(new Term[0])); + } + } } diff --git a/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java index 900aebec4e..3ee645ff4d 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java @@ -9,7 +9,6 @@ package org.sosy_lab.java_smt.solvers.z3; import static com.google.common.base.Preconditions.checkArgument; -import static com.microsoft.z3.enumerations.Z3_decl_kind.Z3_OP_DISTINCT; import com.google.common.base.Preconditions; import com.google.common.collect.HashBasedTable; @@ -659,7 +658,7 @@ private FunctionDeclarationKind getDeclarationKind(long f) { Z3_decl_kind decl = Z3_decl_kind.fromInt(Native.getDeclKind(environment, Native.getAppDecl(environment, f))); - assert (arity > 0) || (arity == 0 && decl == Z3_OP_DISTINCT) + assert arity >= 0 : String.format( "Unexpected arity '%s' for formula '%s' for handling a function application.", arity, Native.astToString(environment, f)); diff --git a/src/org/sosy_lab/java_smt/solvers/z3/Z3NumeralFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/z3/Z3NumeralFormulaManager.java index ea834fbdb1..2c380b8848 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3NumeralFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3NumeralFormulaManager.java @@ -60,9 +60,7 @@ protected Long makeVariableImpl(String varName) { @Override protected Long negate(Long pNumber) { - long sort = Native.getSort(z3context, pNumber); - long minusOne = Native.mkInt(z3context, -1, sort); - return Native.mkMul(z3context, 2, new long[] {minusOne, pNumber}); + return Native.mkUnaryMinus(z3context, pNumber); } @Override @@ -74,6 +72,8 @@ protected Long add(Long pNumber1, Long pNumber2) { protected Long sumImpl(List operands) { if (operands.isEmpty()) { return makeNumberImpl(0); + } else if (operands.size() == 1) { + return operands.get(0); } else { return Native.mkAdd(z3context, operands.size(), Longs.toArray(operands)); } diff --git a/src/org/sosy_lab/java_smt/solvers/z3/Z3QuantifiedFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/z3/Z3QuantifiedFormulaManager.java index 424f6bef9d..c11263ad43 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3QuantifiedFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3QuantifiedFormulaManager.java @@ -38,11 +38,11 @@ public Long mkQuantifier(Quantifier q, List pVariables, Long pBody) { return Native.mkQuantifierConst( z3context, q == Quantifier.FORALL, - 0, + 1, pVariables.size(), Longs.toArray(pVariables), 0, - new long[0], + null, pBody); } @@ -53,8 +53,8 @@ protected Long eliminateQuantifiers(Long pExtractInfo) // to run "qe-light" before "qe". // "qe" does not perform a "qe-light" as a preprocessing on its own! - // One might want to run the tactic "ctx-solver-simplify" on the result. - - return z3FormulaCreator.applyTactics(z3context, pExtractInfo, "qe-light", "qe"); + return Native.simplify( + getFormulaCreator().getEnv(), + z3FormulaCreator.applyTactics(z3context, pExtractInfo, "qe-light", "qe")); } } diff --git a/src/org/sosy_lab/java_smt/test/ArrayFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/ArrayFormulaManagerTest.java index 178d4b73e8..40564d9150 100644 --- a/src/org/sosy_lab/java_smt/test/ArrayFormulaManagerTest.java +++ b/src/org/sosy_lab/java_smt/test/ArrayFormulaManagerTest.java @@ -88,9 +88,9 @@ public void testIntIndexStringValue() throws SolverException, InterruptedExcepti StringFormula stringTwo = smgr.makeString("two"); IntegerFormula intFour = imgr.makeNumber(4); ArrayFormula arr1 = - amgr.makeArray("arr1", FormulaType.IntegerType, StringType); + amgr.makeArray("arr1", IntegerType, StringType); ArrayFormula arr2 = - amgr.makeArray("arr2", FormulaType.IntegerType, StringType); + amgr.makeArray("arr2", IntegerType, StringType); BooleanFormula query = bmgr.and( amgr.equivalence(arr2, amgr.store(arr1, intFour, stringTwo)), diff --git a/src/org/sosy_lab/java_smt/test/SLFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/SLFormulaManagerTest.java index 72c1494850..07e1652ae1 100644 --- a/src/org/sosy_lab/java_smt/test/SLFormulaManagerTest.java +++ b/src/org/sosy_lab/java_smt/test/SLFormulaManagerTest.java @@ -10,6 +10,9 @@ import static com.google.common.truth.Truth.assertThat; import static org.junit.Assert.assertThrows; +import static org.sosy_lab.java_smt.api.FunctionDeclarationKind.SEP_EMP; +import static org.sosy_lab.java_smt.api.FunctionDeclarationKind.SEP_PTO; +import static org.sosy_lab.java_smt.api.FunctionDeclarationKind.SEP_STAR; import com.google.common.collect.ImmutableList; import com.google.common.collect.ImmutableSet; @@ -21,12 +24,17 @@ import org.junit.Test; import org.sosy_lab.java_smt.SolverContextFactory.Solvers; import org.sosy_lab.java_smt.api.BooleanFormula; +import org.sosy_lab.java_smt.api.Formula; import org.sosy_lab.java_smt.api.FormulaType; +import org.sosy_lab.java_smt.api.FunctionDeclaration; +import org.sosy_lab.java_smt.api.FunctionDeclarationKind; import org.sosy_lab.java_smt.api.Model; import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula; import org.sosy_lab.java_smt.api.ProverEnvironment; import org.sosy_lab.java_smt.api.SolverContext.ProverOptions; import org.sosy_lab.java_smt.api.SolverException; +import org.sosy_lab.java_smt.api.visitors.DefaultFormulaVisitor; +import org.sosy_lab.java_smt.api.visitors.TraversalProcess; public class SLFormulaManagerTest extends SolverBasedTest0.ParameterizedSolverBasedTest0 { @@ -307,4 +315,41 @@ public void testListValidCycle() throws InterruptedException, SolverException { BooleanFormula sepTree = slmgr.makeStar(makeStarAll(ptos), ptoLastNil); assertThatFormula(sepTree).isSatisfiable(ProverOptions.ENABLE_SEPARATION_LOGIC); } + + @Test + public void testVisitSL() { + IntegerFormula num0 = imgr.makeNumber(0); + IntegerFormula num42 = imgr.makeNumber(42); + IntegerFormula p = imgr.makeVariable("p"); + BooleanFormula pointsTo = slmgr.makePointsTo(p, num42); + BooleanFormula emptyHeap = + slmgr.makeEmptyHeap(FormulaType.IntegerType, FormulaType.IntegerType); + BooleanFormula heap = slmgr.makeStar(pointsTo, emptyHeap); + + List visited = new ArrayList<>(); + List kinds = new ArrayList<>(); + mgr.visitRecursively( + heap, + new DefaultFormulaVisitor<>() { + @Override + protected TraversalProcess visitDefault(Formula f) { + visited.add(f); + return TraversalProcess.CONTINUE; + } + + @Override + public TraversalProcess visitFunction( + Formula f, List args, FunctionDeclaration functionDeclaration) { + kinds.add(functionDeclaration.getKind()); + return super.visitFunction(f, args, functionDeclaration); + } + }); + assertThat(kinds).containsExactly(SEP_STAR, SEP_EMP, SEP_PTO); + if (solverToUse() == Solvers.CVC4) { + // CVC4 uses a ground-term-based encoding for EMP, which introduces an additional term ZERO. + assertThat(visited).containsExactly(heap, pointsTo, emptyHeap, num0, num42, p); + } else { + assertThat(visited).containsExactly(heap, pointsTo, emptyHeap, num42, p); + } + } }