From 14944f1115fa2ad20afa3873626c2804731aff71 Mon Sep 17 00:00:00 2001
From: yoni206 <yoni206@users.noreply.github.com>
Date: Wed, 30 Jun 2021 05:11:56 -0700
Subject: 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).
---
 src/preprocessing/passes/int_to_bv.cpp | 11 ++++++++---
 src/preprocessing/passes/int_to_bv.h   |  4 ++++
 2 files changed, 12 insertions(+), 3 deletions(-)

(limited to 'src/preprocessing/passes')

diff --git a/src/preprocessing/passes/int_to_bv.cpp b/src/preprocessing/passes/int_to_bv.cpp
index df9d44e39..8c18ccf54 100644
--- 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 5d6ac15e4..43830f03b 100644
--- 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(
-- 
cgit v1.2.3