Princess: Use Sort.sortOf() to get the type of a Princess formula

The old code was a workaround for a bug in Princess that has since been fixed: uuverifiers/princess#16
sosy-lab · Jan 14, 2025 · 58a4ad1 · 58a4ad1
1 parent fd322fa
commit 58a4ad1
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 57 deletions.
diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java
@@ -22,10 +22,7 @@
 import ap.parser.IFunApp;
 import ap.parser.IFunction;
 import ap.parser.IIntFormula;
-import ap.parser.IPlus;
 import ap.parser.ITerm;
-import ap.parser.ITermITE;
-import ap.parser.ITimes;
 import ap.parser.Parser2InputAbsy.TranslationException;
 import ap.parser.PartialEvaluator;
 import ap.parser.SMTLineariser;
@@ -569,20 +566,6 @@ static FormulaType<?> getFormulaType(IExpression pFormula) {
     //  term is rational. We should figure out why and then open a new issue for this.
     if (pFormula instanceof IFormula) {
       return FormulaType.BooleanType;
-    } else if (pFormula instanceof ITimes) {
-      // coeff is always INT, lets check the subterm.
-      ITimes times = (ITimes) pFormula;
-      return getFormulaType(times.subterm());
-    } else if (pFormula instanceof IPlus) {
-      IPlus plus = (IPlus) pFormula;
-      FormulaType<?> t1 = getFormulaType(plus.t1());
-      FormulaType<?> t2 = getFormulaType(plus.t2());
-      return mergeFormulaTypes(t1, t2);
-    } else if (pFormula instanceof ITermITE) {
-      ITermITE plus = (ITermITE) pFormula;
-      FormulaType<?> t1 = getFormulaType(plus.left());
-      FormulaType<?> t2 = getFormulaType(plus.right());
-      return mergeFormulaTypes(t1, t2);
     } else {
       final Sort sort = Sort$.MODULE$.sortOf((ITerm) pFormula);
       try {
@@ -598,25 +581,6 @@ static FormulaType<?> getFormulaType(IExpression 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;

diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessModel.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessModel.java
@@ -22,9 +22,7 @@
 import ap.parser.IFormula;
 import ap.parser.IFunApp;
 import ap.parser.IIntLit;
-import ap.parser.IPlus;
 import ap.parser.ITerm;
-import ap.parser.ITimes;
 import ap.terfor.preds.Predicate;
 import ap.theories.arrays.ExtArray;
 import ap.theories.arrays.ExtArray.ArraySort;
@@ -249,24 +247,6 @@ public String toString() {
     return model.toString();
   }
 
-  /** Tries to determine the Sort of a Term. */
-  private Sort getSort(IExpression pTerm) {
-    // Just using sortof() won't work as Princess may have simplified the original term
-    // FIXME: This may also affect other parts of the code that use sortof()
-    if (pTerm instanceof ITimes) {
-      ITimes times = (ITimes) pTerm;
-      return getSort(times.subterm());
-    } else if (pTerm instanceof IPlus) {
-      IPlus plus = (IPlus) pTerm;
-      return getSort(plus.apply(0));
-    } else if (pTerm instanceof IFormula) {
-      return creator.getBoolType();
-    } else {
-      // TODO: Do we need more cases?
-      return Sort$.MODULE$.sortOf((ITerm) pTerm);
-    }
-  }
-
   /**
    * Simplify rational values.
    *
@@ -301,7 +281,8 @@ private ITerm simplifyRational(ITerm pTerm) {
 
     if (expr instanceof ITerm) {
       ITerm term = (ITerm) expr;
-      ITerm var = api.createConstant(newVariable, getSort(term));
+      Sort sort = Sort$.MODULE$.sortOf(term);
+      ITerm var = api.createConstant(newVariable, sort);
       api.addAssertion(var.$eq$eq$eq(term));
       api.checkSat(true);
       ITerm value = simplifyRational(api.evalToTerm(var));