Smaller improvements on several solvers

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
 
   /**

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);
 }

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

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) {

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) {

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) {

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();
     }

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

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;
       }

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]));
+    }
+  }
 }

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));

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));
     }

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"));
   }
 }

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)),

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);
+    }
+  }
 }