From d5879beb14d85117e4438f7acbff4da68b593274 Mon Sep 17 00:00:00 2001
From: Karlheinz Friedberger <kfriedberger@gmail.com>
Date: Sat, 30 Nov 2019 17:51:22 +0100
Subject: [PATCH] Update Princess to latest release '2019-11-20'.

---
 lib/ivy.xml                                   |  2 +-
 .../PrincessBitvectorFormulaManager.java      |  2 +-
 .../princess/PrincessFormulaCreator.java      | 46 +++++++++----------
 3 files changed, 24 insertions(+), 26 deletions(-)

diff --git a/lib/ivy.xml b/lib/ivy.xml
index a5d68bd4cf..3ccc4b905d 100644
--- 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
index 66f21aa101..961200f9c1 100644
--- 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
index 58e4cd5802..8008d0c664 100644
--- 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);
   }