Merge pull request #629 from sosy-lab/feat/smaller-improvements-on-several-solvers

kfriedberger · web-flow · commit 8b4e62547595 · 2026-03-27T00:30:43.000+01:00
Smaller improvements on several solvers
diff --git 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
@@ -80,8 +80,8 @@ public interface SLFormulaManager {
    *
    * @param <AF> the type of the address formula.
    * @param <AT> 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 extends Formula, AT extends FormulaType<AF>> AF makeNilElement(AT pAdressType);
+  <AF extends Formula, AT extends FormulaType<AF>> 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
@@ -207,11 +207,15 @@ public ResultFormulaType sum(List<ParamFormulaType> operands) {
   }
 
   protected TFormulaInfo sumImpl(List<TFormulaInfo> 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
@@ -336,7 +336,7 @@ public <R> R visit(FormulaVisitor<R> 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
@@ -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
@@ -158,6 +158,11 @@ StringBuilder getSMTLIB2DeclarationsFor(ImmutableMap<String, Term> varsAndUFs) {
     return declarations;
   }
 
+  @Override
+  protected Term simplify(Term f) throws InterruptedException {
+    return creator.getSolver().simplify(f);
+  }
+
   @Override
   public <T extends Formula> T substitute(
       final T f, final Map<? extends Formula, ? extends Formula> 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
@@ -181,7 +181,8 @@ private Term getCVC5Interpolation(Collection<Term> formulasA, Collection<Term> 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
@@ -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
@@ -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
@@ -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<Term> 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
@@ -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
@@ -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<Long> 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
@@ -38,11 +38,11 @@ public Long mkQuantifier(Quantifier q, List<Long> 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
@@ -88,9 +88,9 @@ public void testIntIndexStringValue() throws SolverException, InterruptedExcepti
     StringFormula stringTwo = smgr.makeString("two");
     IntegerFormula intFour = imgr.makeNumber(4);
     ArrayFormula<IntegerFormula, StringFormula> arr1 =
-        amgr.makeArray("arr1", FormulaType.IntegerType, StringType);
+        amgr.makeArray("arr1", IntegerType, StringType);
     ArrayFormula<IntegerFormula, StringFormula> 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
@@ -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<Formula> visited = new ArrayList<>();
+    List<FunctionDeclarationKind> 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<Formula> 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);
+    }
+  }
 }

Original file line number	Diff line number	Diff line change
`@@ -80,8 +80,8 @@ public interface SLFormulaManager {`
`80`	`80`	`*`
`81`	`81`	`* @param <AF> the type of the address formula.`
`82`	`82`	`* @param <AT> the type of the address formula type.`
`83`		`- * @param pAdressType the type of the address formula.`
	`83`	`+ * @param pAddressType the type of the address formula.`
`84`	`84`	`* @return a formula representing the "nil" element for the given address type.`
`85`	`85`	`*/`
`86`		`- <AF extends Formula, AT extends FormulaType<AF>> AF makeNilElement(AT pAdressType);`
	`86`	`+ <AF extends Formula, AT extends FormulaType<AF>> AF makeNilElement(AT pAddressType);`
`87`	`87`	`}`
Original file line number	Diff line number	Diff line change
`@@ -207,11 +207,15 @@ public ResultFormulaType sum(List<ParamFormulaType> operands) {`
`207`	`207`	`}`
`208`	`208`
`209`	`209`	`protected TFormulaInfo sumImpl(List<TFormulaInfo> operands) {`
`210`		`- TFormulaInfo result = makeNumberImpl(0);`
`211`		`- for (TFormulaInfo operand : operands) {`
`212`		`- result = add(result, operand);`
	`210`	`+ if (operands.isEmpty()) {`
	`211`	`+ return makeNumberImpl(0);`
	`212`	`+ } else {`
	`213`	`+ TFormulaInfo result = operands.get(0);`
	`214`	`+ for (TFormulaInfo operand : operands.subList(1, operands.size())) {`
	`215`	`+ result = add(result, operand);`
	`216`	`+ }`
	`217`	`+ return result;`
`213`	`218`	`}`
`214`		`- return result;`
`215`	`219`	`}`
`216`	`220`
`217`	`221`	`@Override`
Original file line number	Diff line number	Diff line change
`@@ -602,6 +602,8 @@ private FunctionDeclarationKind getDeclarationKind(IExpression input) {`
`602`	`602`	`return FunctionDeclarationKind.OTHER;`
`603`	`603`	`} else if (fun == ModuloArithmetic.int_cast()) {`
`604`	`604`	`return FunctionDeclarationKind.OTHER;`
	`605`	`+ } else if (fun == PrincessEnvironment.stringTheory.re_none()) {`
	`606`	`+ return FunctionDeclarationKind.RE_NONE;`
`605`	`607`	`} else {`
`606`	`608`	`return FunctionDeclarationKind.UF;`
`607`	`609`	`}`