Merge pull request #391 from sosy-lab/257-more-theories-for-princess

Add support for Strings and Rationals to the Princess backend

Author: kfriedberger

.classpath

@@ -28,6 +28,10 @@ SPDX-License-Identifier: Apache-2.0
 	<classpathentry kind="lib" path="lib/java/runtime-princess/scala-library.jar"/>
 	<classpathentry kind="lib" path="lib/java/runtime-princess/princess-smt-parser_2.13.jar"/>
 	<classpathentry kind="lib" path="lib/java/runtime-princess/java-cup-runtime.jar"/>
+	<classpathentry kind="lib" path="lib/java/runtime-princess/automaton.jar"/>
+	<classpathentry kind="lib" path="lib/java/runtime-princess/org.sat4j.core.jar"/>
+	<classpathentry kind="lib" path="lib/java/runtime-princess/ostrich_2.13.jar"/>
+	<classpathentry kind="lib" path="lib/java/runtime-princess/ostrich-ecma2020-parser_2.13.jar"/>
 	<classpathentry kind="lib" path="lib/java/runtime-z3/com.microsoft.z3.jar" sourcepath="lib/java-contrib/com.microsoft.z3-sources.jar"/>
 	<classpathentry kind="lib" path="lib/java/runtime-cvc4/CVC4.jar"/>
 	<classpathentry kind="lib" path="lib/java/runtime-cvc5/cvc5.jar"/>

.idea/JavaSMT.iml

@@ -98,7 +98,8 @@ SPDX-License-Identifier: Apache-2.0
         <dependency org="org.apache.ivy" name="ivy" rev="${ivy.target_version}" conf="build->default"/>
 
         <!-- Google Auto-Value
-             Library for auto-generating value types. --><dependency org="com.google.auto.value" name="auto-value" rev="1.11.0" conf="build->default"/>
+             Library for auto-generating value types. -->
+        <dependency org="com.google.auto.value" name="auto-value" rev="1.11.0" conf="build->default"/>
         <dependency org="com.google.auto.value" name="auto-value-annotations" rev="1.11.0" conf="build->default; contrib->sources"/>
 
         <!-- Annotations we use for @Nullable etc. -->
@@ -149,13 +150,19 @@ SPDX-License-Identifier: Apache-2.0
         <dependency org="de.uni-freiburg.informatik.ultimate" name="smtinterpol" rev="2.5-1242-g5c50fb6d" conf="runtime-smtinterpol->master; contrib->sources"/>
 
         <!-- Princess for our Maven release -->
-        <dependency org="io.github.uuverifiers" name="princess_2.13" rev="2024-01-12" conf="runtime-princess-with-javacup->default; contrib->sources"/>
-        <!-- Princess for our Ivy release-->
-        <dependency org="io.github.uuverifiers" name="princess_2.13" rev="2024-01-12" conf="runtime-princess->default; contrib->sources">
-          <!-- Exclude dependency on java-cup and replace it with java-cup-runtime, which is enough.
+        <dependency org="io.github.uuverifiers" name="princess_2.13" rev="2024-11-08" conf="runtime-princess-with-javacup->default; contrib->sources"/>
+        <!-- Princess and Ostrich for our Ivy release -->
+        <dependency org="io.github.uuverifiers" name="princess_2.13" rev="2024-11-08" conf="runtime-princess->default; contrib->sources">
+            <!-- Exclude dependency on java-cup and replace it with java-cup-runtime, which is enough.
                We use the JAR that is published by us instead of the one from net.sf.squirrel-sql.thirdparty-non-maven
                because the latter does not provide a separate JAR for java-cup-runtime. -->
-          <exclude org="net.sf.squirrel-sql.thirdparty-non-maven" name="java-cup"/>
+            <exclude org="net.sf.squirrel-sql.thirdparty-non-maven" name="java-cup"/>
+        </dependency>
+        <dependency org="io.github.uuverifiers" name="ostrich_2.13" rev="1.4.1" conf="runtime-princess->default; contrib->sources">
+            <!-- Exclude dependency on java-cup and replace it with java-cup-runtime, which is enough.
+               We use the JAR that is published by us instead of the one from net.sf.squirrel-sql.thirdparty-non-maven
+               because the latter does not provide a separate JAR for java-cup-runtime. -->
+            <exclude org="net.sf.squirrel-sql.thirdparty-non-maven" name="java-cup"/>
         </dependency>
         <dependency org="edu.tum.cs" name="java-cup" rev="11b-20160615" conf="runtime-princess->runtime"/>
 

lib/ivy.xml

@@ -30,7 +30,7 @@ protected final FormulaCreator<TFormulaInfo, TType, TEnv, TFuncDecl> getFormulaC
     return formulaCreator;
   }
 
-  final TFormulaInfo extractInfo(Formula pBits) {
+  protected final TFormulaInfo extractInfo(Formula pBits) {
     return getFormulaCreator().extractInfo(pBits);
   }
 

src/org/sosy_lab/java_smt/basicimpl/AbstractBaseFormulaManager.java

@@ -11,6 +11,7 @@
 import static com.google.common.base.Preconditions.checkState;
 
 import com.google.common.base.Preconditions;
+import com.google.common.collect.ImmutableList;
 import com.google.common.collect.ImmutableSet;
 import com.google.common.collect.Iterables;
 import com.google.common.collect.LinkedHashMultimap;
@@ -149,7 +150,7 @@ protected void unregisterEvaluator(Evaluator pEvaluator) {
   }
 
   protected void closeAllEvaluators() {
-    evaluators.forEach(Evaluator::close);
+    ImmutableList.copyOf(evaluators).forEach(Evaluator::close);
     evaluators.clear();
   }
 

src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java

@@ -32,11 +32,11 @@ protected AbstractStringFormulaManager(
     super(pCreator);
   }
 
-  private StringFormula wrapString(TFormulaInfo formulaInfo) {
+  protected StringFormula wrapString(TFormulaInfo formulaInfo) {
     return getFormulaCreator().encapsulateString(formulaInfo);
   }
 
-  private RegexFormula wrapRegex(TFormulaInfo formulaInfo) {
+  protected RegexFormula wrapRegex(TFormulaInfo formulaInfo) {
     return getFormulaCreator().encapsulateRegex(formulaInfo);
   }
 

src/org/sosy_lab/java_smt/basicimpl/AbstractStringFormulaManager.java

@@ -137,43 +137,59 @@ public final TType getRegexType() {
   public abstract TFormulaInfo makeVariable(TType type, String varName);
 
   public BooleanFormula encapsulateBoolean(TFormulaInfo pTerm) {
-    assert getFormulaType(pTerm).isBooleanType();
+    checkArgument(
+        getFormulaType(pTerm).isBooleanType(),
+        "Boolean formula has unexpected type: %s",
+        getFormulaType(pTerm));
     return new BooleanFormulaImpl<>(pTerm);
   }
 
   protected BitvectorFormula encapsulateBitvector(TFormulaInfo pTerm) {
-    assert getFormulaType(pTerm).isBitvectorType();
+    checkArgument(
+        getFormulaType(pTerm).isBitvectorType(),
+        "Bitvector formula has unexpected type: %s",
+        getFormulaType(pTerm));
     return new BitvectorFormulaImpl<>(pTerm);
   }
 
   protected FloatingPointFormula encapsulateFloatingPoint(TFormulaInfo pTerm) {
-    assert getFormulaType(pTerm).isFloatingPointType();
+    checkArgument(
+        getFormulaType(pTerm).isFloatingPointType(),
+        "Floatingpoint formula has unexpected type: %s",
+        getFormulaType(pTerm));
     return new FloatingPointFormulaImpl<>(pTerm);
   }
 
   protected <TI extends Formula, TE extends Formula> ArrayFormula<TI, TE> encapsulateArray(
       TFormulaInfo pTerm, FormulaType<TI> pIndexType, FormulaType<TE> pElementType) {
-    assert getFormulaType(pTerm).equals(FormulaType.getArrayType(pIndexType, pElementType))
-        : "Expected: "
-            + getFormulaType(pTerm)
-            + " but found: "
-            + FormulaType.getArrayType(pIndexType, pElementType);
-
+    checkArgument(
+        getFormulaType(pTerm).equals(FormulaType.getArrayType(pIndexType, pElementType)),
+        "Array formula has unexpected type: %s",
+        getFormulaType(pTerm));
     return new ArrayFormulaImpl<>(pTerm, pIndexType, pElementType);
   }
 
   protected StringFormula encapsulateString(TFormulaInfo pTerm) {
-    assert getFormulaType(pTerm).isStringType();
+    checkArgument(
+        getFormulaType(pTerm).isStringType(),
+        "String formula has unexpected type: %s",
+        getFormulaType(pTerm));
     return new StringFormulaImpl<>(pTerm);
   }
 
   protected RegexFormula encapsulateRegex(TFormulaInfo pTerm) {
-    assert getFormulaType(pTerm).isRegexType();
+    checkArgument(
+        getFormulaType(pTerm).isRegexType(),
+        "Regex formula has unexpected type: %s",
+        getFormulaType(pTerm));
     return new RegexFormulaImpl<>(pTerm);
   }
 
   protected EnumerationFormula encapsulateEnumeration(TFormulaInfo pTerm) {
-    assert getFormulaType(pTerm).isEnumerationType();
+    checkArgument(
+        getFormulaType(pTerm).isEnumerationType(),
+        "Enumeration formula has unexpected type: %s",
+        getFormulaType(pTerm));
     return new EnumerationFormulaImpl<>(pTerm);
   }
 
@@ -183,10 +199,12 @@ public Formula encapsulateWithTypeOf(TFormulaInfo pTerm) {
 
   @SuppressWarnings("unchecked")
   public <T extends Formula> T encapsulate(FormulaType<T> pType, TFormulaInfo pTerm) {
-    assert pType.equals(getFormulaType(pTerm))
-        : String.format(
-            "Trying to encapsulate formula %s of type %s as %s",
-            pTerm, getFormulaType(pTerm), pType);
+    checkArgument(
+        pType.equals(getFormulaType(pTerm)),
+        "Trying to encapsulate formula %s of type %s as %s",
+        pTerm,
+        getFormulaType(pTerm),
+        pType);
     if (pType.isBooleanType()) {
       return (T) new BooleanFormulaImpl<>(pTerm);
     } else if (pType.isIntegerType()) {

src/org/sosy_lab/java_smt/basicimpl/FormulaCreator.java

@@ -23,7 +23,9 @@
 import java.util.ArrayDeque;
 import java.util.ArrayList;
 import java.util.Collection;
+import java.util.Collections;
 import java.util.Deque;
+import java.util.LinkedHashSet;
 import java.util.List;
 import java.util.Optional;
 import java.util.Set;
@@ -32,6 +34,7 @@
 import org.sosy_lab.common.collect.PathCopyingPersistentTreeMap;
 import org.sosy_lab.common.collect.PersistentMap;
 import org.sosy_lab.java_smt.api.BooleanFormula;
+import org.sosy_lab.java_smt.api.Formula;
 import org.sosy_lab.java_smt.api.Model;
 import org.sosy_lab.java_smt.api.SolverContext.ProverOptions;
 import org.sosy_lab.java_smt.api.SolverException;
@@ -46,6 +49,15 @@ abstract class PrincessAbstractProver<E> extends AbstractProverWithAllSat<E> {
   protected final PrincessFormulaManager mgr;
   protected final Deque<Level> trackingStack = new ArrayDeque<>(); // symbols on all levels
 
+  /**
+   * Values returned by {@link Model#evaluate(Formula)}.
+   *
+   * <p>We need to record these to make sure that the values returned by the evaluator are
+   * consistant. Calling {@link #isUnsat()} will reset this list as the underlying model has been
+   * updated.
+   */
+  protected final Set<IFormula> evaluatedTerms = new LinkedHashSet<>();
+
   // assign a unique partition number for eah added constraint, for unsat-core and interpolation.
   protected final UniqueIdGenerator idGenerator = new UniqueIdGenerator();
   protected final Deque<PersistentMap<Integer, BooleanFormula>> partitions = new ArrayDeque<>();
@@ -76,9 +88,11 @@ protected PrincessAbstractProver(
   public boolean isUnsat() throws SolverException {
     Preconditions.checkState(!closed);
     wasLastSatCheckSat = false;
+    evaluatedTerms.clear();
     final Value result = api.checkSat(true);
     if (result.equals(SimpleAPI.ProverStatus$.MODULE$.Sat())) {
       wasLastSatCheckSat = true;
+      evaluatedTerms.add(api.partialModelAsFormula());
       return false;
     } else if (result.equals(SimpleAPI.ProverStatus$.MODULE$.Unsat())) {
       return true;
@@ -121,14 +135,27 @@ protected void popImpl() {
     // we have to recreate symbols on lower levels, because JavaSMT assumes "global" symbols.
     Level level = trackingStack.pop();
     api.addBooleanVariables(asScala(level.booleanSymbols));
-    api.addConstants(asScala(level.intSymbols));
+    api.addConstants(asScala(level.theorySymbols));
     level.functionSymbols.forEach(api::addFunction);
     if (!trackingStack.isEmpty()) {
       trackingStack.peek().mergeWithHigher(level);
     }
     partitions.pop();
   }
 
+  /**
+   * Get all terms that have been evaluated in the current model. The formulas are assignments that
+   * extend the original model.
+   */
+  Collection<IFormula> getEvaluatedTerms() {
+    return Collections.unmodifiableCollection(evaluatedTerms);
+  }
+
+  /** Track an assignment `term == value` for an evaluated term and its value. */
+  void addEvaluatedTerm(IFormula pFormula) {
+    evaluatedTerms.add(pFormula);
+  }
+
   @SuppressWarnings("resource")
   @Override
   public Model getModel() throws SolverException {
@@ -138,6 +165,7 @@ public Model getModel() throws SolverException {
     return new CachingModel(getEvaluatorWithoutChecks());
   }
 
+  @SuppressWarnings("resource")
   @Override
   protected PrincessModel getEvaluatorWithoutChecks() throws SolverException {
     final PartialModel partialModel;
@@ -146,7 +174,7 @@ protected PrincessModel getEvaluatorWithoutChecks() throws SolverException {
     } catch (SimpleAPIException ex) {
       throw new SolverException(ex.getMessage(), ex);
     }
-    return new PrincessModel(this, partialModel, creator, api);
+    return registerEvaluator(new PrincessModel(this, partialModel, creator, api));
   }
 
   /**
@@ -213,12 +241,12 @@ void addSymbol(IFormula f) {
     }
   }
 
-  /** add external definition: integer variable. */
+  /** add external definition: theory variable (integer, rational, string, etc). */
   void addSymbol(ITerm f) {
     Preconditions.checkState(!closed);
     api.addConstant(f);
     if (!trackingStack.isEmpty()) {
-      trackingStack.peek().intSymbols.add(f);
+      trackingStack.peek().theorySymbols.add(f);
     }
   }
 
@@ -233,21 +261,21 @@ void addSymbol(IFunction f) {
 
   static class Level {
     final List<IFormula> booleanSymbols = new ArrayList<>();
-    final List<ITerm> intSymbols = new ArrayList<>();
+    final List<ITerm> theorySymbols = new ArrayList<>();
     final List<IFunction> functionSymbols = new ArrayList<>();
 
     Level() {}
 
     /** add higher level to current level, we keep the order of creating symbols. */
     void mergeWithHigher(Level other) {
       this.booleanSymbols.addAll(other.booleanSymbols);
-      this.intSymbols.addAll(other.intSymbols);
+      this.theorySymbols.addAll(other.theorySymbols);
       this.functionSymbols.addAll(other.functionSymbols);
     }
 
     @Override
     public String toString() {
-      return String.format("{%s, %s, %s}", booleanSymbols, intSymbols, functionSymbols);
+      return String.format("{%s, %s, %s}", booleanSymbols, theorySymbols, functionSymbols);
     }
   }
 }