Princess: Handle all constant values for the visitor in isValue()

Author: daniel-raffler

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;
@@ -364,30 +363,38 @@ private String getName(IExpression input) {
   }
 
   /** 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;
+  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;
+    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 && isValue((IFunApp) input)) {
+    if (isValue(input)) {
       return visitor.visitConstant(f, convertValue(input));
 
     } else if (input instanceof IQuantified) {
@@ -462,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();