CVC5: support more function for visitation.
Found by JUnit test 'FormulaToCExpressionConverterTest' in CPAchecker.
@@ -474,6 +474,8 @@ public class CVC5FormulaCreator extends FormulaCreator<Term, Sort, Solver, Term>
.put(Kind.ADD, FunctionDeclarationKind.ADD)
.put(Kind.MULT, FunctionDeclarationKind.MUL)
.put(Kind.SUB, FunctionDeclarationKind.SUB)
+ .put(Kind.INTS_MODULUS, FunctionDeclarationKind.MODULO)
+ .put(Kind.INTS_DIVISION, FunctionDeclarationKind.DIV)
.put(Kind.DIVISION, FunctionDeclarationKind.DIV)
.put(Kind.LT, FunctionDeclarationKind.LT)
.put(Kind.LEQ, FunctionDeclarationKind.LTE)
@@ -505,6 +507,9 @@ public class CVC5FormulaCreator extends FormulaCreator<Term, Sort, Solver, Term>
.put(Kind.BITVECTOR_CONCAT, FunctionDeclarationKind.BV_CONCAT)
.put(Kind.BITVECTOR_SIGN_EXTEND, FunctionDeclarationKind.BV_SIGN_EXTENSION)
.put(Kind.BITVECTOR_ZERO_EXTEND, FunctionDeclarationKind.BV_ZERO_EXTENSION)
+ .put(Kind.BITVECTOR_SHL, FunctionDeclarationKind.BV_SHL)
+ .put(Kind.BITVECTOR_ASHR, FunctionDeclarationKind.BV_ASHR)
+ .put(Kind.BITVECTOR_LSHR, FunctionDeclarationKind.BV_LSHR)
// Floating-point theory
.put(Kind.TO_INTEGER, FunctionDeclarationKind.FLOOR)
.put(Kind.TO_REAL, FunctionDeclarationKind.TO_REAL)
@@ -528,6 +533,7 @@ public class CVC5FormulaCreator extends FormulaCreator<Term, Sort, Solver, Term>
.put(Kind.FLOATINGPOINT_SUB, FunctionDeclarationKind.FP_SUB)
.put(Kind.FLOATINGPOINT_MULT, FunctionDeclarationKind.FP_MUL)
.put(Kind.FLOATINGPOINT_DIV, FunctionDeclarationKind.FP_DIV)
+ .put(Kind.FLOATINGPOINT_NEG, FunctionDeclarationKind.FP_NEG)
.put(Kind.FLOATINGPOINT_LT, FunctionDeclarationKind.FP_LT)
.put(Kind.FLOATINGPOINT_LEQ, FunctionDeclarationKind.FP_LE)
.put(Kind.FLOATINGPOINT_GT, FunctionDeclarationKind.FP_GT)
