Add support for Strings and Rationals to the Princess backend

.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"/>

build/ivysettings.xml

@@ -16,14 +16,20 @@ SPDX-License-Identifier: Apache-2.0
          Keep this file synchronized with
          https://gitlab.com/sosy-lab/software/java-project-template
     -->
-    <settings defaultResolver="Sosy-Lab"/>
+    <settings defaultResolver="Repos"/>
     <property name="repo.dir" value="${basedir}/repository"/>
     <resolvers>
         <!-- Resolver for downloading dependencies -->
-        <url name="Sosy-Lab" descriptor="required">
-            <ivy pattern="${ivy.repo.url}/[organisation]/[module]/ivy-[revision].xml" />
-            <artifact pattern="${ivy.repo.url}/[organisation]/[module]/[artifact]-[revision](-[classifier]).[ext]" />
-        </url>
+        <chain name="Repos">
+            <url name="Sosy-Lab">
+                <ivy pattern="${ivy.repo.url}/[organisation]/[module]/ivy-[revision].xml"/>
+                <artifact pattern="${ivy.repo.url}/[organisation]/[module]/[artifact]-[revision](-[classifier]).[ext]"/>
+            </url>
+            <url name="Maven-Repo" m2compatible="true">
+                <ivy pattern="https://repo1.maven.org/maven2/[organisation]/[module]/ivy-[revision].xml"/>
+                <artifact pattern="https://repo1.maven.org/maven2/[organisation]/[module]/[revision]/[artifact]-[revision].[ext]"/>
+            </url>
+        </chain>
 
         <!-- Resolver for publishing this project -->
         <filesystem name="Sosy-Lab-Publish">

lib/ivy.xml

@@ -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,9 +150,18 @@ 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">
+        <dependency org="io.github.uuverifiers" name="princess_2.13" rev="2024-03-22" conf="runtime-princess-with-javacup->default" />
+
+        <!-- Princess and Ostrich for our Ivy release -->
+        <dependency org="org.scala-lang" name="scala-library" rev="2.13.8" conf="runtime-princess->default"/>
+        <dependency org="io.github.uuverifiers" name="princess-parser_2.13" rev="2024-03-22" conf="runtime-princess->default"/>
+        <dependency org="io.github.uuverifiers" name="princess-smt-parser_2.13" rev="2024-03-22"/>
+        <dependency org="io.github.uuverifiers" name="princess_2.13" rev="2024-03-22" conf="runtime-princess->default"/>
+        <dependency org="org.sat4j" name="org.sat4j.core" rev="2.3.1" conf="runtime-princess->default"/>
+        <dependency org="org.scalacheck" name="scalacheck_2.13" rev="1.14.0" conf="runtime-princess->default"/>
+        <dependency org="dk.brics.automaton" name="automaton" rev="1.11-8" conf="runtime-princess->default"/>
+        <dependency org="io.github.uuverifiers" name="ostrich-ecma2020-parser_2.13" rev="1.3" conf="runtime-princess->default"/>
+        <dependency org="io.github.uuverifiers" name="ostrich_2.13" rev="1.3.5" conf="runtime-princess->default">
           <!-- 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. -->

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

@@ -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/AbstractStringFormulaManager.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/FormulaCreator.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/solvers/princess/PrincessAbstractProver.java

@@ -121,7 +121,7 @@ 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);
@@ -213,12 +213,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 +233,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);
     }
   }
 }