bv2int: support models in tests (#5068)

Previous changes in this preprocessing pass have already enabled model generation when using it.
However, the satisfiable tests still had --no-check-models.

The changes in this PR:

All --no-check-models from current tests for the preprocessing pass are removed.
Refactoring of the relevant part of the code.
Solves CVC4/cvc4-projects#128.

Remark: disabling white-spaces when reviewing this PR is recommended.

17 files changed, 66 insertions, 60 deletions

diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp
index e40b828b5..13ad086e8 100644
--- a/src/preprocessing/passes/bv_to_int.cpp
+++ b/src/preprocessing/passes/bv_to_int.cpp
@@ -687,11 +687,7 @@ Node BVToInt::translateNoChildren(Node original)
         uint64_t bvsize = original.getType().getBitVectorSize();
         translation = newVar;
         d_rangeAssertions.insert(mkRangeConstraint(newVar, bvsize));
-        std::vector<Expr> args;
-        Node intToBVOp = d_nm->mkConst<IntToBitVector>(IntToBitVector(bvsize));
-        Node newNode = d_nm->mkNode(intToBVOp, newVar);
-        smt::currentSmtEngine()->defineFunction(
-            original.toExpr(), args, newNode.toExpr(), true);
+        defineBVUFAsIntUF(original, newVar);
     }
     else if (original.getType().isFunction())
     {
@@ -756,41 +752,49 @@ Node BVToInt::translateFunctionSymbol(Node bvUF)
 
 void BVToInt::defineBVUFAsIntUF(Node bvUF, Node intUF)
 {
-  // This function should only be called after translating
-  // the function symbol to a new function symbol
-  // with the right domain and range.
-
-  // get domain and range of the original function
-  TypeNode tn = bvUF.getType();
-  vector<TypeNode> bvDomain = tn.getArgTypes();
-  TypeNode bvRange = tn.getRangeType();
-
+  // The resulting term
+  Node result;
+  // The type of the resulting term
+  TypeNode resultType;
   // symbolic arguments of original function
   vector<Expr> args;
-  // children of the new symbolic application
-  vector<Node> achildren;
-  achildren.push_back(intUF);
-  int i = 0;
-  for (TypeNode d : bvDomain)
-  {
-    // Each bit-vector argument is casted to a natural number
-    // Other arguments are left intact.
-    Node fresh_bound_var = d_nm->mkBoundVar(d);
-    args.push_back(fresh_bound_var.toExpr());
-    Node castedArg = args[i];
-    if (d.isBitVector())
+  if (!bvUF.getType().isFunction()) {
+    // bvUF is a variable.
+    // in this case, the result is just the original term
+    // (it will be casted later if needed)
+    result = intUF;
+    resultType = bvUF.getType();
+  } else {
+    // bvUF is a function with arguments
+    // The arguments need to be casted as well.
+    TypeNode tn = bvUF.getType();
+    resultType = tn.getRangeType();
+    vector<TypeNode> bvDomain = tn.getArgTypes();
+    // children of the new symbolic application
+    vector<Node> achildren;
+    achildren.push_back(intUF);
+    int i = 0;
+    for (const TypeNode& d : bvDomain)
     {
-      castedArg = castToType(castedArg, d_nm->integerType());
+      // Each bit-vector argument is casted to a natural number
+      // Other arguments are left intact.
+      Node fresh_bound_var = d_nm->mkBoundVar(d);
+      args.push_back(fresh_bound_var.toExpr());
+      Node castedArg = args[i];
+      if (d.isBitVector())
+      {
+        castedArg = castToType(castedArg, d_nm->integerType());
+      }
+      achildren.push_back(castedArg);
+      i++;
     }
-    achildren.push_back(castedArg);
-    i++;
+    result = d_nm->mkNode(kind::APPLY_UF, achildren);
   }
-  Node intApplication = d_nm->mkNode(kind::APPLY_UF, achildren);
-  // If the range is BV, the application needs to be casted back.
-  intApplication = castToType(intApplication, bvRange);
+  // If the result is BV, it needs to be casted back.
+  result = castToType(result, resultType);
   // add the function definition to the smt engine.
   smt::currentSmtEngine()->defineFunction(
-      bvUF.toExpr(), args, intApplication.toExpr(), true);
+      bvUF.toExpr(), args, result.toExpr(), true);
 }
 
 bool BVToInt::childrenTypesChanged(Node n)
diff --git a/src/preprocessing/passes/bv_to_int.h b/src/preprocessing/passes/bv_to_int.h
index db2d08b7d..b84726878 100644
--- a/src/preprocessing/passes/bv_to_int.h
+++ b/src/preprocessing/passes/bv_to_int.h
@@ -289,11 +289,12 @@ class BVToInt : public PreprocessingPass
    * When a UF f is translated to a UF g,
    * we add a define-fun command to the smt-engine
    * to relate between f and g.
+   * We do the same when f and g are just variables.
    * This is useful, for example, when asking
    * for a model-value of a term that includes the
    * original UF f.
-   * @param bvUF the original function
-   * @param intUF the translated function
+   * @param bvUF the original function or variable
+   * @param intUF the translated function or variable
    */
   void defineBVUFAsIntUF(Node bvUF, Node intUF);
 
diff --git a/test/regress/regress0/bv/bv_to_int1.smt2 b/test/regress/regress0/bv/bv_to_int1.smt2
index f812ccbc8..970a9fd75 100644
--- a/test/regress/regress0/bv/bv_to_int1.smt2
+++ b/test/regress/regress0/bv/bv_to_int1.smt2
@@ -1,7 +1,7 @@
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models  --no-check-unsat-cores
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=2 --no-check-models  --no-check-unsat-cores
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=3 --no-check-models  --no-check-unsat-cores
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=4 --no-check-models  --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1   --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=2   --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=3   --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=4   --no-check-unsat-cores
 ; EXPECT: unsat
 (set-logic QF_BV)
 (declare-fun x () (_ BitVec 4))
diff --git a/test/regress/regress0/bv/bv_to_int2.smt2 b/test/regress/regress0/bv/bv_to_int2.smt2
index 00fd51baf..d60f4903b 100644
--- a/test/regress/regress0/bv/bv_to_int2.smt2
+++ b/test/regress/regress0/bv/bv_to_int2.smt2
@@ -1,6 +1,6 @@
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models  --no-check-unsat-cores
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=5 --no-check-models  --no-check-unsat-cores
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=8 --no-check-models  --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1   --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=5   --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=8   --no-check-unsat-cores
 ; EXPECT: sat
 (set-logic QF_BV)
 (declare-fun a () (_ BitVec 8))
diff --git a/test/regress/regress0/bv/bv_to_int_bitwise.smt2 b/test/regress/regress0/bv/bv_to_int_bitwise.smt2
index 6f08c2e8d..444551776 100644
--- a/test/regress/regress0/bv/bv_to_int_bitwise.smt2
+++ b/test/regress/regress0/bv/bv_to_int_bitwise.smt2
@@ -1,5 +1,5 @@
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models  --no-check-unsat-cores
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=5 --no-check-models  --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1   --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=5   --no-check-unsat-cores
 ; EXPECT: unsat
 (set-logic QF_BV)
 (declare-fun s () (_ BitVec 4))
diff --git a/test/regress/regress0/bv/bv_to_int_bvmul1.smt2 b/test/regress/regress0/bv/bv_to_int_bvmul1.smt2
index ec4206812..e21415244 100644
--- a/test/regress/regress0/bv/bv_to_int_bvmul1.smt2
+++ b/test/regress/regress0/bv/bv_to_int_bvmul1.smt2
@@ -1,10 +1,11 @@
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models  --no-check-unsat-cores
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=4 --no-check-models  --no-check-unsat-cores
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=8 --no-check-models  --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1   --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=4   --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=8   --no-check-unsat-cores
 ; EXPECT: sat
 (set-logic QF_BV)
 (declare-fun a () (_ BitVec 8))
 (declare-fun b () (_ BitVec 8))
 (assert (bvult (bvmul a b) (bvudiv a b)))
+(assert (bvugt a (_ bv0 8)))
 
 (check-sat)
diff --git a/test/regress/regress0/bv/bv_to_int_bvmul2.smt2 b/test/regress/regress0/bv/bv_to_int_bvmul2.smt2
index 4e940b5df..4bbe5685e 100644
--- a/test/regress/regress0/bv/bv_to_int_bvmul2.smt2
+++ b/test/regress/regress0/bv/bv_to_int_bvmul2.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models  --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1   --no-check-unsat-cores
 ; EXPECT: unsat
 (set-logic QF_BV)
 (declare-fun T4_180 () (_ BitVec 32))
diff --git a/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf.smt2 b/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf.smt2
index c621aa112..5879542eb 100644
--- a/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf.smt2
+++ b/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models  --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1   --no-check-unsat-cores
 ; EXPECT: sat
 (set-logic QF_UFBV)
 (declare-fun a () (_ BitVec 4))
diff --git a/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf_sorts.smt2 b/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf_sorts.smt2
index 8fbe96eab..f43c8c860 100644
--- a/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf_sorts.smt2
+++ b/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf_sorts.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models  --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1   --no-check-unsat-cores
 ; EXPECT: sat
 (set-logic QF_UFBV)
 (declare-sort S 0)
diff --git a/test/regress/regress0/bv/bv_to_int_elim_err.smt2 b/test/regress/regress0/bv/bv_to_int_elim_err.smt2
index b17aeeacf..01ee5dad8 100644
--- a/test/regress/regress0/bv/bv_to_int_elim_err.smt2
+++ b/test/regress/regress0/bv/bv_to_int_elim_err.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models 
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1  
 ; EXPECT: sat
 (set-logic QF_BV)
 (declare-fun _substvar_183_ () (_ BitVec 32))
diff --git a/test/regress/regress0/bv/bv_to_int_zext.smt2 b/test/regress/regress0/bv/bv_to_int_zext.smt2
index ab09d7341..42e06a940 100644
--- a/test/regress/regress0/bv/bv_to_int_zext.smt2
+++ b/test/regress/regress0/bv/bv_to_int_zext.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models  --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1   --no-check-unsat-cores
 ; EXPECT: unsat
 (set-logic QF_BV)
 (declare-fun T1_31078 () (_ BitVec 8))
diff --git a/test/regress/regress2/bv_to_int_ashr.smt2 b/test/regress/regress2/bv_to_int_ashr.smt2
index 3f2d90a00..11952839f 100644
--- a/test/regress/regress2/bv_to_int_ashr.smt2
+++ b/test/regress/regress2/bv_to_int_ashr.smt2
@@ -1,5 +1,5 @@
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models  --no-check-unsat-cores
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=8 --no-check-models  --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1   --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=8   --no-check-unsat-cores
 ; EXPECT: unsat
 (set-logic QF_BV)
 (declare-fun a () (_ BitVec 8))
diff --git a/test/regress/regress2/bv_to_int_mask_array_1.smt2 b/test/regress/regress2/bv_to_int_mask_array_1.smt2
index 394a1d876..970f27fb9 100644
--- a/test/regress/regress2/bv_to_int_mask_array_1.smt2
+++ b/test/regress/regress2/bv_to_int_mask_array_1.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models  --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1   --no-check-unsat-cores
 ; EXPECT: unsat
 (set-logic ALL)
 (declare-fun A () (Array Int Int))
diff --git a/test/regress/regress2/bv_to_int_mask_array_2.smt2 b/test/regress/regress2/bv_to_int_mask_array_2.smt2
index 36eabdb28..0960b9359 100644
--- a/test/regress/regress2/bv_to_int_mask_array_2.smt2
+++ b/test/regress/regress2/bv_to_int_mask_array_2.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models  --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1   --no-check-unsat-cores
 ; EXPECT: sat
 (set-logic ALL)
 (declare-fun A () (Array Int Int))
diff --git a/test/regress/regress2/bv_to_int_mask_array_3.smt2 b/test/regress/regress2/bv_to_int_mask_array_3.smt2
index 7eef1ad4e..329ee715a 100644
--- a/test/regress/regress2/bv_to_int_mask_array_3.smt2
+++ b/test/regress/regress2/bv_to_int_mask_array_3.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models  --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1   --no-check-unsat-cores
 ; EXPECT: sat
 (set-logic ALL)
 (declare-fun A () (Array (_ BitVec 4) (_ BitVec 4)))
diff --git a/test/regress/regress2/bv_to_int_shifts.smt2 b/test/regress/regress2/bv_to_int_shifts.smt2
index d213b0c3d..7971b2bfe 100644
--- a/test/regress/regress2/bv_to_int_shifts.smt2
+++ b/test/regress/regress2/bv_to_int_shifts.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models  --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1   --no-check-unsat-cores
 ; EXPECT: sat
 (set-logic QF_BV)
 (declare-fun s () (_ BitVec 4))
diff --git a/test/regress/regress3/bv_to_int_and_or.smt2 b/test/regress/regress3/bv_to_int_and_or.smt2
index 3dc179aea..2524e8772 100644
--- a/test/regress/regress3/bv_to_int_and_or.smt2
+++ b/test/regress/regress3/bv_to_int_and_or.smt2
@@ -1,5 +1,5 @@
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models  --no-check-unsat-cores
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=2 --no-check-models  --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1   --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=2   --no-check-unsat-cores
 ; EXPECT: unsat
 (set-logic QF_BV)
 (declare-fun a () (_ BitVec 4))