Princess: Update Princess to version 2025-06-25 and Ostrich to 2.0

Author: daniel-raffler

lib/ivy.xml

@@ -170,16 +170,16 @@ 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 and Ostrich for our Maven release -->
-        <dependency org="io.github.uuverifiers" name="princess_2.13" rev="2024-11-08" conf="runtime-princess-with-javacup->default; contrib->sources"/>
-        <dependency org="io.github.uuverifiers" name="ostrich_2.13" rev="1.4.1" conf="runtime-princess-with-javacup->default; contrib->sources"/>
+        <dependency org="io.github.uuverifiers" name="princess_2.13" rev="2025-06-25" conf="runtime-princess-with-javacup->default; contrib->sources"/>
+        <dependency org="io.github.uuverifiers" name="ostrich_2.13" rev="2.0" 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">
+        <dependency org="io.github.uuverifiers" name="princess_2.13" rev="2025-06-25" 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="io.github.uuverifiers" name="ostrich_2.13" rev="1.4.1" conf="runtime-princess->default; contrib->sources">
+        <dependency org="io.github.uuverifiers" name="ostrich_2.13" rev="2.0" 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/solvers/princess/PrincessFormulaCreator.java

@@ -42,16 +42,14 @@
 import ap.theories.arrays.ExtArray;
 import ap.theories.bitvectors.ModuloArithmetic;
 import ap.theories.nia.GroebnerMultiplication$;
-import ap.theories.rationals.Fractions;
-import ap.theories.rationals.Rationals$;
+import ap.theories.rationals.Rationals;
 import ap.types.Sort;
 import ap.types.Sort$;
 import com.google.common.base.Preconditions;
 import com.google.common.collect.HashBasedTable;
 import com.google.common.collect.ImmutableList;
 import com.google.common.collect.ImmutableSet;
 import com.google.common.collect.Table;
-import java.lang.reflect.InvocationTargetException;
 import java.util.HashMap;
 import java.util.LinkedHashMap;
 import java.util.List;
@@ -108,6 +106,13 @@ class PrincessFormulaCreator
     // modmod.bv_xnor()?
     // modmod.bv_comp()?
 
+    theoryFunctionKind.put(Rationals.addition(), FunctionDeclarationKind.ADD);
+    theoryFunctionKind.put(Rationals.multiplication(), FunctionDeclarationKind.MUL);
+    theoryFunctionKind.put(Rationals.multWithFraction(), FunctionDeclarationKind.MUL);
+    theoryFunctionKind.put(Rationals.multWithRing(), FunctionDeclarationKind.MUL);
+    theoryFunctionKind.put(Rationals.division(), FunctionDeclarationKind.DIV);
+    theoryFunctionKind.put(Rationals.RatDivZero(), FunctionDeclarationKind.OTHER);
+
     // casts to integer, sign/zero-extension?
 
     theoryPredKind.put(ModuloArithmetic.bv_ult(), FunctionDeclarationKind.BV_ULT);
@@ -207,30 +212,28 @@ public Object convertValue(IExpression value) {
       return ((IIntLit) value).value().bigIntValue();
     }
     if (value instanceof IFunApp) {
-      IFunApp fun = (IFunApp) value;
-      switch (fun.fun().name()) {
+      IFunApp app = (IFunApp) value;
+      switch (app.fun().name()) {
         case "true":
-          Preconditions.checkArgument(fun.fun().arity() == 0);
+          Preconditions.checkArgument(app.fun().arity() == 0);
           return true;
         case "false":
-          Preconditions.checkArgument(fun.fun().arity() == 0);
+          Preconditions.checkArgument(app.fun().arity() == 0);
           return false;
         case "mod_cast":
           // we found a bitvector BV(lower, upper, ctxt), lets extract the last parameter
-          return ((IIntLit) fun.apply(2)).value().bigIntValue();
-        case "_int":
-        case "Rat_int":
-          Preconditions.checkArgument(fun.fun().arity() == 1);
-          ITerm term = fun.apply(0);
+          return ((IIntLit) app.apply(2)).value().bigIntValue();
+        case "Rat_fromRing":
+          Preconditions.checkArgument(app.fun().arity() == 1);
+          ITerm term = app.apply(0);
           if (term instanceof IIntLit) {
             return ((IIntLit) term).value().bigIntValue();
           }
           break;
-        case "_frac":
         case "Rat_frac":
-          Preconditions.checkArgument(fun.fun().arity() == 2);
-          ITerm term1 = fun.apply(0);
-          ITerm term2 = fun.apply(1);
+          Preconditions.checkArgument(app.fun().arity() == 2);
+          ITerm term1 = app.apply(0);
+          ITerm term2 = app.apply(1);
           if (term1 instanceof IIntLit && term2 instanceof IIntLit) {
             Rational ratValue =
                 Rational.of(
@@ -241,7 +244,7 @@ public Object convertValue(IExpression value) {
           break;
         case "str_empty":
         case "str_cons":
-          return strToString(fun);
+          return strToString(app);
         default:
       }
     }
@@ -360,8 +363,11 @@ private String getName(IExpression input) {
     }
   }
 
-  /** Returns true if the expression is a constant number. */
-  private static boolean isConstant(IFunApp pExpr) {
+  /** Returns true if the expression is a constant value. */
+  private static boolean isValue(IFunApp pExpr) {
+    if (!pExpr.fun().equals(Rationals.frac()) && !pExpr.fun().equals(Rationals.fromRing())) {
+      return false;
+    }
     for (IExpression sub : asJava(pExpr.args())) {
       if (!(sub instanceof IIntLit)) {
         return false;
@@ -370,23 +376,6 @@ private static boolean isConstant(IFunApp pExpr) {
     return true;
   }
 
-  /** Returns true if the expression is an integer literal. */
-  private static boolean isRatInt(IFunApp pExpr) {
-    // We need to use reflection to get Rationals.int() as `int` can't be a method name in Java
-    final IFunction ratInt;
-    try {
-      ratInt = (IFunction) Fractions.class.getMethod("int").invoke(Rationals$.MODULE$);
-    } catch (IllegalAccessException | NoSuchMethodException | InvocationTargetException ex) {
-      throw new RuntimeException(ex);
-    }
-    return isConstant(pExpr) && pExpr.fun().equals(ratInt);
-  }
-
-  /** Returns true if the expression is a faction literal. */
-  private static boolean isRatFrac(IFunApp pExpr) {
-    return isConstant(pExpr) && pExpr.fun().equals(Rationals$.MODULE$.frac());
-  }
-
   @SuppressWarnings("deprecation")
   @Override
   public <R> R visit(FormulaVisitor<R> visitor, final Formula f, final IExpression input) {
@@ -398,8 +387,7 @@ public <R> R visit(FormulaVisitor<R> visitor, final Formula f, final IExpression
       IBoolLit literal = (IBoolLit) input;
       return visitor.visitConstant(f, literal.value());
 
-    } else if (input instanceof IFunApp
-        && (isRatInt((IFunApp) input) || isRatFrac((IFunApp) input))) {
+    } else if (input instanceof IFunApp && (isValue((IFunApp) input))) {
       return visitor.visitConstant(f, convertValue(input));
 
     } else if (input instanceof IQuantified) {

src/org/sosy_lab/java_smt/solvers/princess/PrincessRationalFormulaManager.java

@@ -40,15 +40,14 @@ public class PrincessRationalFormulaManager
   @Override
   protected boolean isNumeral(IExpression value) {
     if (value instanceof IFunApp) {
-      IFunApp fun = (IFunApp) value;
-      switch (fun.fun().name()) {
-        case "int":
-        case "Rat_int":
-          assert fun.fun().arity() == 1;
-          return ifmgr.isNumeral(fun.apply(0));
-        case "frac":
-          assert fun.fun().arity() == 2;
-          return ifmgr.isNumeral(fun.apply(0)) && ifmgr.isNumeral(fun.apply(1));
+      IFunApp app = (IFunApp) value;
+      switch (app.fun().name()) {
+        case "Rat_fromRing":
+          assert app.fun().arity() == 1;
+          return ifmgr.isNumeral(app.apply(0));
+        case "Rat_frac":
+          assert app.fun().arity() == 2;
+          return ifmgr.isNumeral(app.apply(0)) && ifmgr.isNumeral(app.apply(1));
       }
     }
     return false;
@@ -68,40 +67,34 @@ protected IExpression makeNumberImpl(BigInteger i) {
     return fromInteger(ifmgr.makeNumberImpl(i));
   }
 
-  @Override
-  protected IExpression makeNumberImpl(Rational pI) {
-    return divide(makeNumberImpl(pI.getNum()), makeNumberImpl(pI.getDen()));
-  }
-
-  @Override
-  protected IExpression makeNumberImpl(String i) {
-    return makeNumberImpl(new BigDecimal(i));
-  }
-
   @Override
   protected IExpression makeNumberImpl(double pNumber) {
     return makeNumberImpl(BigDecimal.valueOf(pNumber));
   }
 
   @Override
   protected IExpression makeNumberImpl(BigDecimal pNumber) {
-    if (pNumber.stripTrailingZeros().scale() <= 0) {
-      // We have an integer number
-      // Return the term for a/1
-      return PrincessEnvironment.rationalTheory.int2ring(
-          ifmgr.makeNumberImpl(pNumber.toBigInteger()));
+    return makeNumberImpl(Rational.ofBigDecimal(pNumber));
+  }
+
+  @Override
+  protected IExpression makeNumberImpl(Rational pI) {
+    if (pI.isIntegral()) {
+      return makeNumberImpl(pI.getNum());
     } else {
-      // We have a fraction a/b
-      // Convert the numerator and the divisor and then return the fraction
-      List<ITerm> args =
-          ImmutableList.of(
-              ifmgr.makeNumberImpl(pNumber.unscaledValue()),
-              ifmgr.makeNumberImpl(BigInteger.valueOf(10).pow(pNumber.scale())));
       return new IFunApp(
-          PrincessEnvironment.rationalTheory.frac(), PrincessEnvironment.toSeq(args));
+          PrincessEnvironment.rationalTheory.frac(),
+          PrincessEnvironment.toSeq(
+              ImmutableList.of(
+                  ifmgr.makeNumberImpl(pI.getNum()), ifmgr.makeNumberImpl(pI.getDen()))));
     }
   }
 
+  @Override
+  protected IExpression makeNumberImpl(String i) {
+    return makeNumberImpl(new BigDecimal(i));
+  }
+
   @Override
   protected IExpression makeVariableImpl(String varName) {
     return getFormulaCreator().makeVariable(PrincessEnvironment.FRACTION_SORT, varName);