Merge pull request #509 from sosy-lab/supportMoreTermKinds

Add more FunctionDeclarationKinds for the visitor

Author: daniel-raffler

src/org/sosy_lab/java_smt/api/FunctionDeclarationKind.java

@@ -92,6 +92,9 @@ public enum FunctionDeclarationKind {
   /** Identity operation, converts from integers to rationals, also known as {@code to_real}. */
   TO_REAL,
 
+  /** Convert from integer to bitvector. */
+  INT_TO_BV,
+
   // Simple bitvector operations
 
   /** Extraction over bitvectors. */
@@ -205,6 +208,12 @@ public enum FunctionDeclarationKind {
   /** Cast a signed bitvector to a floating-point number. */
   BV_SCASTTO_FP,
 
+  /** Cast an unsigned bitvector to an integer number. */
+  UBV_TO_INT,
+
+  /** Cast a signed bitvector to an integer number. */
+  SBV_TO_INT,
+
   // Simple floating point operations
 
   /** Negation of a floating point. */

src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java

@@ -438,6 +438,7 @@ private Expr normalize(Expr operator) {
           .put(Kind.LEQ, FunctionDeclarationKind.LTE)
           .put(Kind.GT, FunctionDeclarationKind.GT)
           .put(Kind.GEQ, FunctionDeclarationKind.GTE)
+          .put(Kind.INT_TO_BITVECTOR, FunctionDeclarationKind.INT_TO_BV)
           // Bitvector theory
           .put(Kind.BITVECTOR_PLUS, FunctionDeclarationKind.BV_ADD)
           .put(Kind.BITVECTOR_SUB, FunctionDeclarationKind.BV_SUB)

src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java

@@ -543,6 +543,7 @@ private Term normalize(Term operator) {
           .put(Kind.LEQ, FunctionDeclarationKind.LTE)
           .put(Kind.GT, FunctionDeclarationKind.GT)
           .put(Kind.GEQ, FunctionDeclarationKind.GTE)
+          .put(Kind.INT_TO_BITVECTOR, FunctionDeclarationKind.INT_TO_BV)
           // Bitvector theory
           .put(Kind.BITVECTOR_ADD, FunctionDeclarationKind.BV_ADD)
           .put(Kind.BITVECTOR_SUB, FunctionDeclarationKind.BV_SUB)
@@ -574,9 +575,11 @@ private Term normalize(Term operator) {
           .put(Kind.BITVECTOR_LSHR, FunctionDeclarationKind.BV_LSHR)
           .put(Kind.BITVECTOR_ROTATE_LEFT, FunctionDeclarationKind.BV_ROTATE_LEFT_BY_INT)
           .put(Kind.BITVECTOR_ROTATE_RIGHT, FunctionDeclarationKind.BV_ROTATE_RIGHT_BY_INT)
-          // Floating-point theory
           .put(Kind.TO_INTEGER, FunctionDeclarationKind.FLOOR)
           .put(Kind.TO_REAL, FunctionDeclarationKind.TO_REAL)
+          .put(Kind.BITVECTOR_SBV_TO_INT, FunctionDeclarationKind.SBV_TO_INT)
+          .put(Kind.BITVECTOR_UBV_TO_INT, FunctionDeclarationKind.UBV_TO_INT)
+          // Floating-point theory
           .put(Kind.FLOATINGPOINT_TO_SBV, FunctionDeclarationKind.FP_CASTTO_SBV)
           .put(Kind.FLOATINGPOINT_TO_UBV, FunctionDeclarationKind.FP_CASTTO_UBV)
           .put(Kind.FLOATINGPOINT_TO_FP_FROM_FP, FunctionDeclarationKind.FP_CASTTO_FP)

src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaCreator.java

@@ -66,6 +66,9 @@
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.MSAT_TAG_FP_TO_SBV;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.MSAT_TAG_FP_TO_UBV;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.MSAT_TAG_IFF;
+import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.MSAT_TAG_INT_FROM_SBV;
+import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.MSAT_TAG_INT_FROM_UBV;
+import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.MSAT_TAG_INT_TO_BV;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.MSAT_TAG_ITE;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.MSAT_TAG_LEQ;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.MSAT_TAG_NOT;
@@ -411,6 +414,8 @@ private FunctionDeclarationKind getDeclarationKind(long pF) {
         return FunctionDeclarationKind.LTE;
       case MSAT_TAG_EQ:
         return FunctionDeclarationKind.EQ;
+      case MSAT_TAG_INT_TO_BV:
+        return FunctionDeclarationKind.INT_TO_BV;
       case MSAT_TAG_ARRAY_READ:
         return FunctionDeclarationKind.SELECT;
       case MSAT_TAG_ARRAY_WRITE:
@@ -468,6 +473,10 @@ private FunctionDeclarationKind getDeclarationKind(long pF) {
         return FunctionDeclarationKind.BV_ROTATE_LEFT_BY_INT;
       case MSAT_TAG_BV_ROR:
         return FunctionDeclarationKind.BV_ROTATE_RIGHT_BY_INT;
+      case MSAT_TAG_INT_FROM_UBV:
+        return FunctionDeclarationKind.UBV_TO_INT;
+      case MSAT_TAG_INT_FROM_SBV:
+        return FunctionDeclarationKind.SBV_TO_INT;
 
       case MSAT_TAG_FP_NEG:
         return FunctionDeclarationKind.FP_NEG;

src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java

@@ -658,6 +658,8 @@ private FunctionDeclarationKind getDeclarationKind(long f) {
         return FunctionDeclarationKind.FLOOR;
       case Z3_OP_TO_REAL:
         return FunctionDeclarationKind.TO_REAL;
+      case Z3_OP_INT2BV:
+        return FunctionDeclarationKind.INT_TO_BV;
 
       case Z3_OP_UNINTERPRETED:
         return FunctionDeclarationKind.UF;
@@ -763,6 +765,10 @@ private FunctionDeclarationKind getDeclarationKind(long f) {
         return FunctionDeclarationKind.BV_ROTATE_LEFT;
       case Z3_OP_EXT_ROTATE_RIGHT:
         return FunctionDeclarationKind.BV_ROTATE_RIGHT;
+      case Z3_OP_BV2INT:
+        return FunctionDeclarationKind.UBV_TO_INT;
+      case Z3_OP_SBV2INT:
+        return FunctionDeclarationKind.SBV_TO_INT;
 
       case Z3_OP_FPA_NEG:
         return FunctionDeclarationKind.FP_NEG;

src/org/sosy_lab/java_smt/test/SolverVisitorTest.java

@@ -298,6 +298,57 @@ public void rationalConstantVisit() {
     }
   }
 
+  @Test
+  public void integerDivisionVisit() {
+    requireIntegers();
+    assume().that(solver).isNotEqualTo(Solvers.PRINCESS); // Princess will rewrite the term
+
+    IntegerFormula x = imgr.makeVariable("x");
+    IntegerFormula y = imgr.makeVariable("y");
+    IntegerFormula c = imgr.makeNumber(7);
+
+    if (solver.equals(Solvers.MATHSAT5)) {
+      // MathSAT will rewrite if we don't use a variable in the denominator
+      checkKind(imgr.divide(x, y), FunctionDeclarationKind.DIV);
+    } else {
+      // Otherwise, just use a constant to support solvers that don't have non-linear arithmetics
+      checkKind(imgr.divide(x, c), FunctionDeclarationKind.DIV);
+    }
+  }
+
+  @Test
+  public void integerToBitvectorConversionVisit() {
+    requireIntegers();
+    requireBitvectors();
+
+    // Yices does not support integer to bitvector conversions
+    assume().that(solver).isNotEqualTo(Solvers.YICES2);
+    // Princess uses mod_casts internally, which makes it hard to figure out when conversion happen
+    // TODO Find out if mod_cast/int_cast could be mapped to (S)BV_TO_INT and INT_TO_BV
+    assume().that(solver).isNotEqualTo(Solvers.PRINCESS);
+
+    IntegerFormula x = imgr.makeVariable("x");
+    checkKind(bvmgr.makeBitvector(8, x), FunctionDeclarationKind.INT_TO_BV);
+  }
+
+  @Test
+  public void bitvectorToIntegerConversionVisit() {
+    requireIntegers();
+    requireBitvectors();
+
+    // Yices does not support integer to bitvector conversions
+    assume().that(solver).isNotEqualTo(Solvers.YICES2);
+    // CVC4, CVC5 and Z3 will rewrite SBV_TO_INT to a term that only uses unsigned integers
+    assume().that(solver).isNoneOf(Solvers.Z3, Solvers.CVC4, Solvers.CVC5);
+    // Princess uses mod_casts internally, which makes it hard to figure out when conversion happen
+    assume().that(solver).isNotEqualTo(Solvers.PRINCESS);
+
+    BitvectorFormula y = bvmgr.makeVariable(8, "y");
+
+    checkKind(bvmgr.toIntegerFormula(y, true), FunctionDeclarationKind.SBV_TO_INT);
+    checkKind(bvmgr.toIntegerFormula(y, false), FunctionDeclarationKind.UBV_TO_INT);
+  }
+
   @Test
   public void arrayVisit() {
     requireArrays();