improve visitation of some operations for SMTInterpol and CVC4.

The missing operations were found through testing around in CPAchecker.
sosy-lab · Sep 25, 2022 · c6bd3d7 · c6bd3d7
1 parent 72de08a
commit c6bd3d7
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 0 deletions.
diff --git a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java
@@ -418,6 +418,8 @@ private Expr normalize(Expr operator) {
           .put(Kind.PLUS, FunctionDeclarationKind.ADD)
           .put(Kind.MULT, FunctionDeclarationKind.MUL)
           .put(Kind.MINUS, FunctionDeclarationKind.SUB)
+          .put(Kind.INTS_DIVISION, FunctionDeclarationKind.DIV)
+          .put(Kind.INTS_MODULUS, FunctionDeclarationKind.MODULO)
           .put(Kind.DIVISION, FunctionDeclarationKind.DIV)
           .put(Kind.LT, FunctionDeclarationKind.LT)
           .put(Kind.LEQ, FunctionDeclarationKind.LTE)
@@ -441,6 +443,9 @@ private Expr normalize(Expr operator) {
           .put(Kind.BITVECTOR_SDIV, FunctionDeclarationKind.BV_SDIV)
           .put(Kind.BITVECTOR_UDIV, FunctionDeclarationKind.BV_UDIV)
           .put(Kind.BITVECTOR_SREM, FunctionDeclarationKind.BV_SREM)
+          .put(Kind.BITVECTOR_SHL, FunctionDeclarationKind.BV_SHL)
+          .put(Kind.BITVECTOR_ASHR, FunctionDeclarationKind.BV_ASHR)
+          .put(Kind.BITVECTOR_LSHR, FunctionDeclarationKind.BV_LSHR)
           // TODO: find out where Kind.BITVECTOR_SMOD fits in here
           .put(Kind.BITVECTOR_UREM, FunctionDeclarationKind.BV_UREM)
           .put(Kind.BITVECTOR_NOT, FunctionDeclarationKind.BV_NOT)
@@ -467,6 +472,7 @@ private Expr normalize(Expr operator) {
           .put(Kind.FLOATINGPOINT_MAX, FunctionDeclarationKind.FP_MAX)
           .put(Kind.FLOATINGPOINT_MIN, FunctionDeclarationKind.FP_MIN)
           .put(Kind.FLOATINGPOINT_SQRT, FunctionDeclarationKind.FP_SQRT)
+          .put(Kind.FLOATINGPOINT_NEG, FunctionDeclarationKind.FP_NEG)
           .put(Kind.FLOATINGPOINT_PLUS, FunctionDeclarationKind.FP_ADD)
           .put(Kind.FLOATINGPOINT_SUB, FunctionDeclarationKind.FP_SUB)
           .put(Kind.FLOATINGPOINT_MULT, FunctionDeclarationKind.FP_MUL)

diff --git a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolFormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolFormulaCreator.java
@@ -322,8 +322,10 @@ private FunctionDeclarationKind getDeclarationKind(ApplicationTerm input) {
       case "-":
         return FunctionDeclarationKind.SUB;
       case "/":
+      case "div":
         return FunctionDeclarationKind.DIV;
       case "%":
+      case "mod":
         return FunctionDeclarationKind.MODULO;
       case "<":
         return FunctionDeclarationKind.LT;