int-to-bv: correct model values (#6811)

the int-to-bv preprocessing pass produced wrong models.
This PR fixes this in a similar fashion to other preprocessing passes, by adding a substitution to the preprocessing pass context. This requires moving the main translation function to be a class method, rather than a helper method in an empty namespace.

Thanks to @alex-ozdemir for raising this issue and producing a triggering benchmark (added to regressions in this PR).

diff --git a/src/preprocessing/passes/int_to_bv.cpp b/src/preprocessing/passes/int_to_bv.cpp
index df9d44e39b334f2c8c03bfacf34a76e34b3c0b2e..8c18ccf541af1edf1560ed220a093fdd24673774 100644 (file)
--- a/src/preprocessing/passes/int_to_bv.cpp
+++ b/src/preprocessing/passes/int_to_bv.cpp
@@ -29,6 +29,7 @@
 #include "options/base_options.h"
 #include "options/smt_options.h"
 #include "preprocessing/assertion_pipeline.h"
+#include "preprocessing/preprocessing_pass_context.h"
 #include "theory/rewriter.h"
 #include "theory/theory.h"
 #include "util/bitvector.h"
@@ -41,7 +42,6 @@ namespace passes {
 using namespace std;
 using namespace cvc5::theory;
 
-using NodeMap = std::unordered_map<Node, Node>;
 
 namespace {
 
@@ -101,8 +101,9 @@ Node intToBVMakeBinary(TNode n, NodeMap& cache)
   }
   return cache[n];
 }
+}  // namespace
 
-Node intToBV(TNode n, NodeMap& cache)
+Node IntToBV::intToBV(TNode n, NodeMap& cache)
 {
   int size = options::solveIntAsBV();
   AlwaysAssert(size > 0);
@@ -216,6 +217,8 @@ Node intToBV(TNode n, NodeMap& cache)
           result = sm->mkDummySkolem("__intToBV_var",
                                      nm->mkBitVectorType(size),
                                      "Variable introduced in intToBV pass");
+          Node bv2nat = nm->mkNode(kind::BITVECTOR_TO_NAT, result);
+          d_preprocContext->addSubstitution(current, bv2nat);
         }
       }
       else if (current.isConst())
@@ -249,9 +252,11 @@ Node intToBV(TNode n, NodeMap& cache)
       cache[current] = result;
     }
   }
+  Trace("int-to-bv-debug") << "original: " << n << std::endl;
+  Trace("int-to-bv-debug") << "binary: " << n_binary << std::endl;
+  Trace("int-to-bv-debug") << "result: " << cache[n_binary] << std::endl;
   return cache[n_binary];
 }
-}  // namespace
 
 IntToBV::IntToBV(PreprocessingPassContext* preprocContext)
     : PreprocessingPass(preprocContext, "int-to-bv"){};

diff --git a/src/preprocessing/passes/int_to_bv.h b/src/preprocessing/passes/int_to_bv.h
index 5d6ac15e406f3892b825d4a17f6c7a5450fe6841..43830f03bd07a21d0c94a0a16fce13c4587161c0 100644 (file)
--- a/src/preprocessing/passes/int_to_bv.h
+++ b/src/preprocessing/passes/int_to_bv.h
@@ -22,16 +22,20 @@
 #ifndef CVC5__PREPROCESSING__PASSES__INT_TO_BV_H
 #define CVC5__PREPROCESSING__PASSES__INT_TO_BV_H
 
+#include "expr/node.h"
 #include "preprocessing/preprocessing_pass.h"
 
 namespace cvc5 {
 namespace preprocessing {
 namespace passes {
 
+using NodeMap = std::unordered_map<Node, Node>;
+
 class IntToBV : public PreprocessingPass
 {
  public:
   IntToBV(PreprocessingPassContext* preprocContext);
+  Node intToBV(TNode n, NodeMap& cache);
 
  protected:
   PreprocessingPassResult applyInternal(

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index abd21e2221f21e0351939b5adbfa5363574ed9cb..63d34ebe1d5092e17de1021e08f64e9db62cd280 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -418,6 +418,7 @@ set(regress_0_tests
   regress0/bv/inequality04.smt2
   regress0/bv/inequality05.smt2
   regress0/bv/int_to_bv_err_on_demand_1.smt2
+  regress0/bv/int_to_bv_model.smt2
   regress0/bv/issue-4075.smt2
   regress0/bv/issue-4076.smt2
   regress0/bv/issue-4130.smt2

diff --git a/test/regress/regress0/bv/int_to_bv_model.smt2 b/test/regress/regress0/bv/int_to_bv_model.smt2
new file mode 100644 (file)
index 0000000..ebe8ab1
--- /dev/null
+++ b/test/regress/regress0/bv/int_to_bv_model.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --solve-int-as-bv=9 --check-models
+; EXPECT: sat
+(set-logic QF_NIA)
+(declare-const a Int)
+(declare-const b Int)
+(assert (= (+ (* a 251) a) (+ b (* b 211))))
+(assert (not (= a 0)))
+(check-sat)