Update Princess to latest release '2019-11-20'.

sosy-lab · Nov 30, 2019 · d5879be · d5879be
1 parent 98632b4
commit d5879be
Show file tree

Hide file tree

Showing 3 changed files with 24 additions and 26 deletions.
diff --git a/lib/ivy.xml b/lib/ivy.xml
@@ -125,7 +125,7 @@
         <dependency org="de.uni-freiburg.informatik.ultimate" name="smtinterpol" rev="2.5-533-ga4ba1513" conf="runtime-smtinterpol->master; contrib->sources"/>
 
         <!-- Princess -->
-        <dependency org="uuverifiers" name="princess_2.12" rev="2018-12-06-assertionless" conf="runtime-princess->default; contrib->sources">
+        <dependency org="uuverifiers" name="princess_2.12" rev="2019-11-20-assertionless" 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. -->

diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessBitvectorFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessBitvectorFormulaManager.java
@@ -22,7 +22,7 @@
 import ap.basetypes.IdealInt;
 import ap.parser.IExpression;
 import ap.parser.ITerm;
-import ap.theories.ModuloArithmetic$;
+import ap.theories.bitvectors.ModuloArithmetic$;
 import ap.types.Sort;
 import ap.types.Sort$;
 import com.google.common.base.Preconditions;

diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java
@@ -47,9 +47,8 @@
 import ap.parser.IVariable;
 import ap.terfor.conjunctions.Quantifier;
 import ap.terfor.preds.Predicate;
-import ap.theories.ModuloArithmetic;
-import ap.theories.ModuloArithmetic$;
 import ap.theories.SimpleArray;
+import ap.theories.bitvectors.ModuloArithmetic;
 import ap.theories.nia.GroebnerMultiplication$;
 import ap.types.Sort;
 import ap.types.Sort$;
@@ -84,34 +83,33 @@ class PrincessFormulaCreator
   private static final Map<Predicate, FunctionDeclarationKind> theoryPredKind = new HashMap<>();
 
   static {
-    final ModuloArithmetic$ modmod = ModuloArithmetic$.MODULE$;
-    theoryFunctionKind.put(modmod.bv_concat(), FunctionDeclarationKind.BV_CONCAT);
-    theoryFunctionKind.put(modmod.bv_extract(), FunctionDeclarationKind.BV_EXTRACT);
-    theoryFunctionKind.put(modmod.bv_not(), FunctionDeclarationKind.BV_NOT);
-    theoryFunctionKind.put(modmod.bv_neg(), FunctionDeclarationKind.BV_NEG);
-    theoryFunctionKind.put(modmod.bv_and(), FunctionDeclarationKind.BV_AND);
-    theoryFunctionKind.put(modmod.bv_or(), FunctionDeclarationKind.BV_OR);
-    theoryFunctionKind.put(modmod.bv_add(), FunctionDeclarationKind.BV_ADD);
-    theoryFunctionKind.put(modmod.bv_sub(), FunctionDeclarationKind.BV_SUB);
-    theoryFunctionKind.put(modmod.bv_mul(), FunctionDeclarationKind.BV_MUL);
-    theoryFunctionKind.put(modmod.bv_udiv(), FunctionDeclarationKind.BV_UDIV);
-    theoryFunctionKind.put(modmod.bv_sdiv(), FunctionDeclarationKind.BV_SDIV);
-    theoryFunctionKind.put(modmod.bv_urem(), FunctionDeclarationKind.BV_UREM);
-    theoryFunctionKind.put(modmod.bv_srem(), FunctionDeclarationKind.BV_SREM);
+    theoryFunctionKind.put(ModuloArithmetic.bv_concat(), FunctionDeclarationKind.BV_CONCAT);
+    theoryFunctionKind.put(ModuloArithmetic.bv_extract(), FunctionDeclarationKind.BV_EXTRACT);
+    theoryFunctionKind.put(ModuloArithmetic.bv_not(), FunctionDeclarationKind.BV_NOT);
+    theoryFunctionKind.put(ModuloArithmetic.bv_neg(), FunctionDeclarationKind.BV_NEG);
+    theoryFunctionKind.put(ModuloArithmetic.bv_and(), FunctionDeclarationKind.BV_AND);
+    theoryFunctionKind.put(ModuloArithmetic.bv_or(), FunctionDeclarationKind.BV_OR);
+    theoryFunctionKind.put(ModuloArithmetic.bv_add(), FunctionDeclarationKind.BV_ADD);
+    theoryFunctionKind.put(ModuloArithmetic.bv_sub(), FunctionDeclarationKind.BV_SUB);
+    theoryFunctionKind.put(ModuloArithmetic.bv_mul(), FunctionDeclarationKind.BV_MUL);
+    theoryFunctionKind.put(ModuloArithmetic.bv_udiv(), FunctionDeclarationKind.BV_UDIV);
+    theoryFunctionKind.put(ModuloArithmetic.bv_sdiv(), FunctionDeclarationKind.BV_SDIV);
+    theoryFunctionKind.put(ModuloArithmetic.bv_urem(), FunctionDeclarationKind.BV_UREM);
+    theoryFunctionKind.put(ModuloArithmetic.bv_srem(), FunctionDeclarationKind.BV_SREM);
     // modmod.bv_smod()?
-    theoryFunctionKind.put(modmod.bv_shl(), FunctionDeclarationKind.BV_SHL);
-    theoryFunctionKind.put(modmod.bv_lshr(), FunctionDeclarationKind.BV_LSHR);
-    theoryFunctionKind.put(modmod.bv_ashr(), FunctionDeclarationKind.BV_ASHR);
-    theoryFunctionKind.put(modmod.bv_xor(), FunctionDeclarationKind.BV_XOR);
+    theoryFunctionKind.put(ModuloArithmetic.bv_shl(), FunctionDeclarationKind.BV_SHL);
+    theoryFunctionKind.put(ModuloArithmetic.bv_lshr(), FunctionDeclarationKind.BV_LSHR);
+    theoryFunctionKind.put(ModuloArithmetic.bv_ashr(), FunctionDeclarationKind.BV_ASHR);
+    theoryFunctionKind.put(ModuloArithmetic.bv_xor(), FunctionDeclarationKind.BV_XOR);
     // modmod.bv_xnor()?
     // modmod.bv_comp()?
 
     // casts to integer, sign/zero-extension?
 
-    theoryPredKind.put(modmod.bv_ult(), FunctionDeclarationKind.BV_ULT);
-    theoryPredKind.put(modmod.bv_ule(), FunctionDeclarationKind.BV_ULE);
-    theoryPredKind.put(modmod.bv_slt(), FunctionDeclarationKind.BV_SLT);
-    theoryPredKind.put(modmod.bv_sle(), FunctionDeclarationKind.BV_SLE);
+    theoryPredKind.put(ModuloArithmetic.bv_ult(), FunctionDeclarationKind.BV_ULT);
+    theoryPredKind.put(ModuloArithmetic.bv_ule(), FunctionDeclarationKind.BV_ULE);
+    theoryPredKind.put(ModuloArithmetic.bv_slt(), FunctionDeclarationKind.BV_SLT);
+    theoryPredKind.put(ModuloArithmetic.bv_sle(), FunctionDeclarationKind.BV_SLE);
 
     theoryFunctionKind.put(GroebnerMultiplication$.MODULE$.mul(), FunctionDeclarationKind.MUL);
   }