Merge pull request #518 from sosy-lab/princess-2025-06-25

Princess/Ostrich update

Author: kfriedberger

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/basicimpl/AbstractProver.java

@@ -30,7 +30,7 @@
 public abstract class AbstractProver<T> implements BasicProverEnvironment<T> {
 
   protected final boolean generateModels;
-  private final boolean generateAllSat;
+  protected final boolean generateAllSat;
   protected final boolean generateUnsatCores;
   private final boolean generateUnsatCoresOverAssumptions;
   protected final boolean enableSL;

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

@@ -29,6 +29,7 @@
 import java.util.List;
 import java.util.Optional;
 import java.util.Set;
+import java.util.concurrent.Callable;
 import org.sosy_lab.common.ShutdownNotifier;
 import org.sosy_lab.common.UniqueIdGenerator;
 import org.sosy_lab.common.collect.PathCopyingPersistentTreeMap;
@@ -53,7 +54,7 @@ abstract class PrincessAbstractProver<E> extends AbstractProverWithAllSat<E> {
    * 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
+   * consistent. Calling {@link #isUnsat()} will reset this list as the underlying model has been
    * updated.
    */
   protected final Set<IFormula> evaluatedTerms = new LinkedHashSet<>();
@@ -92,7 +93,10 @@ public boolean isUnsat() throws SolverException {
     final Value result = api.checkSat(true);
     if (result.equals(SimpleAPI.ProverStatus$.MODULE$.Sat())) {
       wasLastSatCheckSat = true;
-      evaluatedTerms.add(api.partialModelAsFormula());
+      if (this.generateModels || this.generateAllSat) {
+        // we only build the model if we have set the correct options
+        evaluatedTerms.add(callOrThrow(api::partialModelAsFormula));
+      }
       return false;
     } else if (result.equals(SimpleAPI.ProverStatus$.MODULE$.Unsat())) {
       return true;
@@ -148,6 +152,9 @@ protected void popImpl() {
    * extend the original model.
    */
   Collection<IFormula> getEvaluatedTerms() {
+    Preconditions.checkState(
+        this.generateModels || this.generateAllSat,
+        "Model generation was not enabled, no evaluated terms available.");
     return Collections.unmodifiableSet(evaluatedTerms);
   }
 
@@ -168,22 +175,22 @@ public Model getModel() throws SolverException {
   @SuppressWarnings("resource")
   @Override
   protected PrincessModel getEvaluatorWithoutChecks() throws SolverException {
-    final PartialModel partialModel;
-    try {
-      partialModel = partialModel();
-    } catch (SimpleAPIException ex) {
-      throw new SolverException(ex.getMessage(), ex);
-    }
+    final PartialModel partialModel = callOrThrow(api::partialModel);
     return registerEvaluator(new PrincessModel(this, partialModel, creator, api));
   }
 
   /**
-   * This method only exists to allow catching the exception from Scala in Java.
+   * This method only exists to allow catching some exceptions from Scala in Java.
    *
-   * @throws SimpleAPIException if model can not be constructed.
+   * @throws SolverException if the callable throws an Exception (including {@link
+   *     SimpleAPIException})
    */
-  private PartialModel partialModel() throws SimpleAPIException {
-    return api.partialModel();
+  private <T> T callOrThrow(Callable<T> callable) throws SolverException {
+    try {
+      return callable.call();
+    } catch (Exception ex) { // mainly for catching SimpleAPIException
+      throw new SolverException(ex.getMessage(), ex);
+    }
   }
 
   @Override

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

@@ -15,7 +15,6 @@
 import static scala.collection.JavaConverters.asJava;
 import static scala.collection.JavaConverters.asJavaCollection;
 
-import ap.basetypes.IdealInt;
 import ap.parser.IAtom;
 import ap.parser.IBinFormula;
 import ap.parser.IBinJunctor;
@@ -42,16 +41,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 +105,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 +211,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 +243,7 @@ public Object convertValue(IExpression value) {
           break;
         case "str_empty":
         case "str_cons":
-          return strToString(fun);
+          return strToString(app);
         default:
       }
     }
@@ -360,46 +362,39 @@ private String getName(IExpression input) {
     }
   }
 
-  /** Returns true if the expression is a constant number. */
-  private static boolean isConstant(IFunApp pExpr) {
-    for (IExpression sub : asJava(pExpr.args())) {
-      if (!(sub instanceof IIntLit)) {
-        return false;
+  /** Returns true if the expression is a constant value. */
+  private static boolean isValue(IExpression input) {
+    if (input instanceof IBoolLit || input instanceof IIntLit) {
+      // Boolean or integer literal
+      return true;
+    } else if (input instanceof IFunApp) {
+      IFunApp app = (IFunApp) input;
+      IFunction fun = app.fun();
+      if (fun.equals(Rationals.fromRing()) || fun.equals(Rationals.frac())) {
+        // Rational number literal
+        for (IExpression sub : asJava(app.args())) {
+          if (!(sub instanceof IIntLit)) {
+            return false;
+          }
+        }
+        return true;
+      }
+      if (fun.equals(ModuloArithmetic.mod_cast()) && input.apply(2) instanceof IIntLit) {
+        // Bitvector literal
+        return true;
+      }
+      if (CONSTANT_UFS.contains(fun.name())) {
+        // Nil, Cons from String theory
+        return true;
       }
     }
-    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());
+    return false;
   }
 
   @SuppressWarnings("deprecation")
   @Override
   public <R> R visit(FormulaVisitor<R> visitor, final Formula f, final IExpression input) {
-    if (input instanceof IIntLit) {
-      IdealInt value = ((IIntLit) input).value();
-      return visitor.visitConstant(f, value.bigIntValue());
-
-    } else if (input instanceof IBoolLit) {
-      IBoolLit literal = (IBoolLit) input;
-      return visitor.visitConstant(f, literal.value());
-
-    } else if (input instanceof IFunApp
-        && (isRatInt((IFunApp) input) || isRatFrac((IFunApp) input))) {
+    if (isValue(input)) {
       return visitor.visitConstant(f, convertValue(input));
 
     } else if (input instanceof IQuantified) {
@@ -474,20 +469,6 @@ public <R> R visit(FormulaVisitor<R> visitor, final Formula f, final IExpression
       return visit(visitor, f, ((IIntFormula) input).t());
     }
 
-    if (kind == FunctionDeclarationKind.OTHER && input instanceof IFunApp) {
-      if (ModuloArithmetic.mod_cast().equals(((IFunApp) input).fun())
-          && ((IFunApp) input).apply(2) instanceof IIntLit) {
-        // mod_cast(0, 256, 7) -> BV=7 with bitsize=8
-        return visitor.visitConstant(f, convertValue(input));
-      }
-    }
-
-    if (kind == FunctionDeclarationKind.UF && input instanceof IFunApp) {
-      if (CONSTANT_UFS.contains(((IFunApp) input).fun().name())) {
-        return visitor.visitConstant(f, convertValue(input));
-      }
-    }
-
     ImmutableList.Builder<Formula> args = ImmutableList.builder();
     ImmutableList.Builder<FormulaType<?>> argTypes = ImmutableList.builder();
     int arity = input.length();

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);
@@ -117,7 +110,7 @@ protected ITerm toType(IExpression param) {
 
   @Override
   protected IExpression floor(IExpression number) {
-    throw new UnsupportedOperationException("floor is not supported in Princess");
+    return Rationals.ring2int((ITerm) number);
   }
 
   @Override
@@ -142,7 +135,10 @@ protected IExpression multiply(IExpression number1, IExpression number2) {
 
   @Override
   protected IExpression divide(IExpression number1, IExpression number2) {
-    return Rationals.div(toType(number1), toType(number2));
+    // SMT-LIB allows division by zero, so we use divWithSpecialZero here.
+    // If the divisor is zero, divWithSpecialZero will evaluate to a unary UF `ratDivZero`,
+    // otherwise it is the normal division
+    return Rationals.divWithSpecialZero(toType(number1), toType(number2));
   }
 
   @Override