diff --git a/src/org/sosy_lab/java_smt/api/FunctionDeclarationKind.java b/src/org/sosy_lab/java_smt/api/FunctionDeclarationKind.java index a203fa1f2d..2421eca80c 100644 --- a/src/org/sosy_lab/java_smt/api/FunctionDeclarationKind.java +++ b/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. */ diff --git a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java index 23e7328956..3c4712fb3a 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java +++ b/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) diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java index 946b6be069..54761f9a1e 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java +++ b/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) diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaCreator.java index ff35694c4a..a96aa8f4ee 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaCreator.java @@ -37,6 +37,7 @@ import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.MSAT_TAG_BV_UREM; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.MSAT_TAG_BV_XOR; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.MSAT_TAG_BV_ZEXT; +import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.MSAT_TAG_DIVIDE; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.MSAT_TAG_EQ; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.MSAT_TAG_FLOOR; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.MSAT_TAG_FP_ABS; @@ -65,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; @@ -402,12 +406,16 @@ private FunctionDeclarationKind getDeclarationKind(long pF) { case MSAT_TAG_TIMES: return FunctionDeclarationKind.MUL; + case MSAT_TAG_DIVIDE: + return FunctionDeclarationKind.DIV; case MSAT_TAG_PLUS: return FunctionDeclarationKind.ADD; case MSAT_TAG_LEQ: 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 +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; diff --git a/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java index bde94b3e5f..e4882f176b 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java +++ b/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; diff --git a/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java b/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java index 56b0200874..390f8ab4cf 100644 --- a/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java @@ -310,6 +310,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();