diff options
author | yoni206 <yoni206@users.noreply.github.com> | 2021-03-29 06:38:19 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-03-29 13:38:19 +0000 |
commit | ba91b0ea10021ad299f30d23de4864940bb78100 (patch) | |
tree | c7ac2601072c94de6ffc9e6f69c2b9ca92e248d5 /test/unit | |
parent | 38f797f5aa577a643e00ebc42e933a2552de575f (diff) |
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.
Diffstat (limited to 'test/unit')
-rw-r--r-- | test/unit/theory/CMakeLists.txt | 1 | ||||
-rw-r--r-- | test/unit/theory/theory_bv_int_blaster_white.cpp | 47 |
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 |