Modular bv2int part 1 (#6212)

This PR introduces the header file for a more modular bv-to-int module, that will be called from the preprocessing pass bv-to-int, and possibly from the bit-vector solver after preprocessing.

The header file is basically a copy of the bv_to_int.h header file from preprocessing, with some adjustments to increase modularity.

In addition to the header file we also introduce an empty unit test that #includes the header, in order to identify compilation errors. The unit test will be populated in subsequent PRs, that will also include implementations.

2 files changed, 48 insertions, 0 deletions

diff --git a/test/unit/theory/CMakeLists.txt b/test/unit/theory/CMakeLists.txt
index dd312498f..723369200 100644
--- a/test/unit/theory/CMakeLists.txt
+++ b/test/unit/theory/CMakeLists.txt
@@ -20,6 +20,7 @@ cvc4_add_unit_test_white(theory_bags_rewriter_white theory)
 cvc4_add_unit_test_white(theory_bags_type_rules_white theory)
 cvc4_add_unit_test_white(theory_bv_rewriter_white theory)
 cvc4_add_unit_test_white(theory_bv_white theory)
+cvc4_add_unit_test_white(theory_bv_int_blaster_white theory)
 cvc4_add_unit_test_white(theory_engine_white theory)
 cvc4_add_unit_test_white(theory_int_opt_white theory)
 cvc4_add_unit_test_white(theory_quantifiers_bv_instantiator_white theory)
diff --git a/test/unit/theory/theory_bv_int_blaster_white.cpp b/test/unit/theory/theory_bv_int_blaster_white.cpp
new file mode 100644
index 000000000..7888ba52b
--- /dev/null
+++ b/test/unit/theory/theory_bv_int_blaster_white.cpp
@@ -0,0 +1,47 @@
+/*********************                                                        */
+/*! \file theory_bv_rewriter_white.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Yoni Zohar
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Unit tests for bit-vector solving via integers
+ **
+ ** Unit tests for bit-vector solving via integers.
+ **/
+
+#include <iostream>
+#include <memory>
+#include <vector>
+
+#include "test_smt.h"
+#include "theory/bv/int_blaster.h"
+#include "util/bitvector.h"
+
+namespace CVC4 {
+
+using namespace kind;
+using namespace theory;
+
+namespace test {
+
+class TestTheoryWhiteBvIntblaster : public TestSmtNoFinishInit
+{
+ protected:
+  void SetUp() override
+  {
+    TestSmtNoFinishInit::SetUp();
+    d_smtEngine->setOption("produce-models", "true");
+    d_smtEngine->finishInit();
+    d_true = d_nodeManager->mkConst<bool>(true);
+    d_one = d_nodeManager->mkConst<Rational>(Rational(1));
+  }
+  Node d_true;
+  Node d_one;
+};
+}  // namespace test
+}  // namespace CVC4