Visitor: Add support for integer-bv conversion in 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/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

@@ -65,6 +65,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;
@@ -408,6 +411,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:
@@ -465,6 +470,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

@@ -655,6 +655,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;
@@ -760,6 +762,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;