More theories for Princess

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

lib/ivy.xml

@@ -96,7 +96,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.10.3" conf="build->default"/>
+             Library for auto-generating value types. -->
+        <dependency org="com.google.auto.value" name="auto-value" rev="1.10.3" conf="build->default"/>
         <dependency org="com.google.auto.value" name="auto-value-annotations" rev="1.10.3" conf="build->default; contrib->sources"/>
 
         <!-- Annotations we use for @Nullable etc. -->
@@ -146,10 +147,17 @@ SPDX-License-Identifier: Apache-2.0
         <!-- SmtInterpol -->
         <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="2023-06-19" conf="runtime-princess-with-javacup->default; contrib->sources"/>
-        <!-- Princess for our Ivy release-->
-        <dependency org="io.github.uuverifiers" name="princess_2.13" rev="2023-06-19" conf="runtime-princess->default; contrib->sources">
+        <!-- Princess and Ostrich for our Maven release -->
+        <!-- Princess is already included in Ostrich, so we do not need an explicit dependency to Princess.
+        <dependency org="io.github.uuverifiers" name="princess_2.12" rev="2021-11-15" conf="runtime-princess-with-javacup->default; contrib->sources"/>
+        -->
+        <dependency org="io.github.uuverifiers" name="ostrich_2.12" rev="1.1" conf="runtime-princess-with-javacup->default; contrib->sources"/>
+
+        <!-- Princess and Ostrich for our Ivy release-->
+        <!-- Princess is already included in Ostrich, so we do not need an explicit dependency to Princess.
+        <dependency org="io.github.uuverifiers" name="princess_2.12" rev="2021-11-15" conf="runtime-princess->default; contrib->sources">
+        -->
+        <dependency org="io.github.uuverifiers" name="ostrich_2.13" rev="1.3" 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. -->

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/PrincessEnvironment.java

@@ -21,7 +21,9 @@
 import ap.parser.IFunApp;
 import ap.parser.IFunction;
 import ap.parser.IIntFormula;
+import ap.parser.IPlus;
 import ap.parser.ITerm;
+import ap.parser.ITimes;
 import ap.parser.Parser2InputAbsy.TranslationException;
 import ap.parser.PartialEvaluator;
 import ap.parser.SMTLineariser;
@@ -30,8 +32,10 @@
 import ap.terfor.ConstantTerm;
 import ap.terfor.preds.Predicate;
 import ap.theories.ExtArray;
+import ap.theories.ExtArray.ArraySort;
 import ap.theories.bitvectors.ModuloArithmetic;
-import ap.theories.rationals.Fractions.FractionSort$;
+import ap.theories.rationals.Rationals$;
+import ap.theories.strings.StringTheory;
 import ap.types.Sort;
 import ap.types.Sort$;
 import ap.types.Sort.MultipleValueBool$;
@@ -50,6 +54,7 @@
 import java.nio.file.Path;
 import java.util.ArrayDeque;
 import java.util.ArrayList;
+import java.util.Arrays;
 import java.util.Deque;
 import java.util.HashMap;
 import java.util.HashSet;
@@ -60,6 +65,7 @@
 import java.util.Optional;
 import java.util.Set;
 import java.util.TreeMap;
+import java.util.stream.Collectors;
 import org.checkerframework.checker.nullness.qual.Nullable;
 import org.sosy_lab.common.Appender;
 import org.sosy_lab.common.Appenders;
@@ -72,6 +78,8 @@
 import org.sosy_lab.common.io.PathCounterTemplate;
 import org.sosy_lab.java_smt.api.FormulaType;
 import org.sosy_lab.java_smt.api.SolverContext.ProverOptions;
+import ostrich.OFlags;
+import ostrich.OstrichStringTheory;
 import scala.Tuple2;
 import scala.Tuple4;
 import scala.collection.immutable.Seq;
@@ -101,6 +109,29 @@ class PrincessEnvironment {
 
   public static final Sort BOOL_SORT = Sort$.MODULE$.Bool();
   public static final Sort INTEGER_SORT = Sort.Integer$.MODULE$;
+  public static final Sort NAT_SORT = Sort.Nat$.MODULE$;
+
+  static final StringTheory stringTheory =
+      new OstrichStringTheory(
+          toSeq(new ArrayList<>()),
+          new OFlags(
+              OFlags.$lessinit$greater$default$1(),
+              OFlags.$lessinit$greater$default$2(),
+              OFlags.$lessinit$greater$default$3(),
+              OFlags.$lessinit$greater$default$4(),
+              OFlags.$lessinit$greater$default$5(),
+              OFlags.$lessinit$greater$default$6(),
+              OFlags.$lessinit$greater$default$7(),
+              OFlags.$lessinit$greater$default$8(),
+              OFlags.$lessinit$greater$default$9(),
+              OFlags.$lessinit$greater$default$10(),
+              OFlags.$lessinit$greater$default$11(),
+              OFlags.$lessinit$greater$default$12()));
+  public static final Sort STRING_SORT = stringTheory.StringSort();
+  public static final Sort REGEX_SORT = stringTheory.RegexSort();
+
+  static Rationals$ rationalTheory = Rationals$.MODULE$;
+  public static final Sort FRACTION_SORT = rationalTheory.dom();
 
   @Option(secure = true, description = "log all queries as Princess-specific Scala code")
   private boolean logAllQueriesAsScala = false;
@@ -509,14 +540,23 @@ static FormulaType<?> getFormulaType(IExpression pFormula) {
     if (pFormula instanceof IFormula) {
       return FormulaType.BooleanType;
     } else if (pFormula instanceof ITerm) {
-      final Sort sort = Sort$.MODULE$.sortOf((ITerm) pFormula);
+      ITerm formula = (ITerm) pFormula;
+      if (pFormula instanceof ITimes) {
+        // coeff is always INT, lets check the subterm.
+        formula = ((ITimes) formula).subterm();
+      } else if (pFormula instanceof IPlus) {
+        return mergeFormulaTypes(
+            getFormulaType(((IPlus) pFormula).t1()), getFormulaType(((IPlus) pFormula).t2()));
+      }
+      final Sort sort = Sort$.MODULE$.sortOf(formula);
       try {
         return getFormulaTypeFromSort(sort);
       } catch (IllegalArgumentException e) {
         // add more info about the formula, then rethrow
         throw new IllegalArgumentException(
             String.format(
-                "Unknown formula type '%s' for formula '%s'.", pFormula.getClass(), pFormula),
+                "Unknown formula type '%s' of sort '%s' for formula '%s'.",
+                pFormula.getClass(), sort.toString(), pFormula),
             e);
       }
     }
@@ -525,15 +565,38 @@ static FormulaType<?> getFormulaType(IExpression pFormula) {
             "Unknown formula type '%s' for formula '%s'.", pFormula.getClass(), pFormula));
   }
 
+  /**
+   * Merge INTEGER and RATIONAL type or INTEGER and BITVECTOR and return the more general type. The
+   * ordering is: RATIONAL > INTEGER > BITVECTOR.
+   *
+   * @throws IllegalArgumentException for any other type.
+   */
+  private static FormulaType<?> mergeFormulaTypes(FormulaType<?> type1, FormulaType<?> type2) {
+    if ((type1.isIntegerType() || type1.isRationalType())
+        && (type2.isIntegerType() || type2.isRationalType())) {
+      return type1.isRationalType() ? type1 : type2;
+    }
+    if ((type1.isIntegerType() || type1.isBitvectorType())
+        && (type2.isIntegerType() || type2.isBitvectorType())) {
+      return type1.isIntegerType() ? type1 : type2;
+    }
+    throw new IllegalArgumentException(
+        String.format("Types %s and %s can not be merged.", type1, type2));
+  }
+
   private static FormulaType<?> getFormulaTypeFromSort(final Sort sort) {
     if (sort == PrincessEnvironment.BOOL_SORT) {
       return FormulaType.BooleanType;
-    } else if (sort == PrincessEnvironment.INTEGER_SORT) {
+    } else if (sort == PrincessEnvironment.INTEGER_SORT || sort == PrincessEnvironment.NAT_SORT) {
       return FormulaType.IntegerType;
-    } else if (sort instanceof FractionSort$) {
+    } else if (sort == PrincessEnvironment.FRACTION_SORT) {
       return FormulaType.RationalType;
+    } else if (sort == PrincessEnvironment.STRING_SORT) {
+      return FormulaType.StringType;
+    } else if (sort == PrincessEnvironment.REGEX_SORT) {
+      return FormulaType.RegexType;
     } else if (sort instanceof ExtArray.ArraySort) {
-      Seq<Sort> indexSorts = ((ExtArray.ArraySort) sort).theory().indexSorts();
+      Seq<Sort> indexSorts = ((ArraySort) sort).theory().indexSorts();
       Sort elementSort = ((ExtArray.ArraySort) sort).theory().objSort();
       assert indexSorts.iterator().size() == 1 : "unexpected index type in Array type:" + sort;
       // assert indexSorts.size() == 1; // TODO Eclipse does not like simpler code.
@@ -643,6 +706,15 @@ static <T> Seq<T> toSeq(List<T> list) {
     return collectionAsScalaIterableConverter(list).asScala().toSeq();
   }
 
+  static Seq<ITerm> toITermSeq(List<IExpression> exprs) {
+    return PrincessEnvironment.toSeq(
+        exprs.stream().map(e -> (ITerm) e).collect(Collectors.toList()));
+  }
+
+  static Seq<ITerm> toITermSeq(IExpression... exprs) {
+    return toITermSeq(Arrays.asList(exprs));
+  }
+
   IExpression simplify(IExpression f) {
     // TODO this method is not tested, check it!
     if (f instanceof IFormula) {