summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/Makefile.am6
-rw-r--r--src/preprocessing/passes/bool_to_bv.cpp200
-rw-r--r--src/preprocessing/passes/bool_to_bv.h64
-rw-r--r--src/preprocessing/passes/bv_to_bool.cpp310
-rw-r--r--src/preprocessing/passes/bv_to_bool.h (renamed from src/theory/bv/bv_to_bool.h)75
-rw-r--r--src/preprocessing/preprocessing_pass_registry.cpp5
-rw-r--r--src/preprocessing/preprocessing_pass_registry.h5
-rw-r--r--src/smt/smt_engine.cpp45
-rw-r--r--src/theory/bv/bv_to_bool.cpp387
-rw-r--r--src/theory/quantifiers/term_util.cpp1
-rw-r--r--src/theory/theory_engine.cpp9
-rw-r--r--src/theory/theory_engine.h4
-rw-r--r--test/regress/Makefile.tests2
-rw-r--r--test/regress/regress0/bv/bool-to-bv.smt29
-rw-r--r--test/regress/regress0/bv/bv-to-bool.smt185
15 files changed, 837 insertions, 470 deletions
diff --git a/src/Makefile.am b/src/Makefile.am
index 7b364129f..289ed11d4 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -68,6 +68,10 @@ libcvc4_la_SOURCES = \
preprocessing/passes/int_to_bv.h \
preprocessing/passes/pseudo_boolean_processor.cpp \
preprocessing/passes/pseudo_boolean_processor.h \
+ preprocessing/passes/bool_to_bv.cpp \
+ preprocessing/passes/bool_to_bv.h \
+ preprocessing/passes/bv_to_bool.cpp \
+ preprocessing/passes/bv_to_bool.h \
preprocessing/passes/symmetry_detect.cpp \
preprocessing/passes/symmetry_detect.h \
preprocessing/preprocessing_pass.cpp \
@@ -322,8 +326,6 @@ libcvc4_la_SOURCES = \
theory/bv/bv_subtheory_core.h \
theory/bv/bv_subtheory_inequality.cpp \
theory/bv/bv_subtheory_inequality.h \
- theory/bv/bv_to_bool.cpp \
- theory/bv/bv_to_bool.h \
theory/bv/bvintropow2.cpp \
theory/bv/bvintropow2.h \
theory/bv/slicer.cpp \
diff --git a/src/preprocessing/passes/bool_to_bv.cpp b/src/preprocessing/passes/bool_to_bv.cpp
new file mode 100644
index 000000000..511f09a71
--- /dev/null
+++ b/src/preprocessing/passes/bool_to_bv.cpp
@@ -0,0 +1,200 @@
+/********************* */
+/*! \file bool_to_bv.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Liana Hadarean, Aina Niemetz, Clark Barrett
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 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 The BoolToBv preprocessing pass
+ **
+ **/
+
+#include "preprocessing/passes/bool_to_bv.h"
+
+#include <string>
+#include <unordered_map>
+#include <vector>
+
+#include "expr/node.h"
+#include "smt/smt_statistics_registry.h"
+#include "theory/rewriter.h"
+#include "theory/theory.h"
+
+namespace CVC4 {
+namespace preprocessing {
+namespace passes {
+using namespace CVC4::theory;
+
+BoolToBV::BoolToBV(PreprocessingPassContext* preprocContext)
+ : PreprocessingPass(preprocContext, "bool-to-bv"),
+ d_lowerCache(),
+ d_one(bv::utils::mkOne(1)),
+ d_zero(bv::utils::mkZero(1)),
+ d_statistics(){};
+
+PreprocessingPassResult BoolToBV::applyInternal(
+ AssertionPipeline* assertionsToPreprocess)
+{
+ NodeManager::currentResourceManager()->spendResource(
+ options::preprocessStep());
+ std::vector<Node> new_assertions;
+ lowerBoolToBv(assertionsToPreprocess->ref(), new_assertions);
+ for (unsigned i = 0; i < assertionsToPreprocess->size(); ++i)
+ {
+ assertionsToPreprocess->replace(i, Rewriter::rewrite(new_assertions[i]));
+ }
+ return PreprocessingPassResult::NO_CONFLICT;
+}
+
+void BoolToBV::addToLowerCache(TNode term, Node new_term)
+{
+ Assert(new_term != Node());
+ Assert(!hasLowerCache(term));
+ d_lowerCache[term] = new_term;
+}
+
+Node BoolToBV::getLowerCache(TNode term) const
+{
+ Assert(hasLowerCache(term));
+ return d_lowerCache.find(term)->second;
+}
+
+bool BoolToBV::hasLowerCache(TNode term) const
+{
+ return d_lowerCache.find(term) != d_lowerCache.end();
+}
+
+Node BoolToBV::lowerNode(TNode current, bool topLevel)
+{
+ Node result;
+ NodeManager* nm = NodeManager::currentNM();
+ if (hasLowerCache(current))
+ {
+ result = getLowerCache(current);
+ }
+ else
+ {
+ if (current.getNumChildren() == 0)
+ {
+ if (current.getKind() == kind::CONST_BOOLEAN)
+ {
+ result = (current == bv::utils::mkTrue()) ? d_one : d_zero;
+ }
+ else
+ {
+ result = current;
+ }
+ }
+ else
+ {
+ Kind kind = current.getKind();
+ Kind new_kind = kind;
+ switch (kind)
+ {
+ case kind::EQUAL: new_kind = kind::BITVECTOR_COMP; break;
+ case kind::AND: new_kind = kind::BITVECTOR_AND; break;
+ case kind::OR: new_kind = kind::BITVECTOR_OR; break;
+ case kind::NOT: new_kind = kind::BITVECTOR_NOT; break;
+ case kind::XOR: new_kind = kind::BITVECTOR_XOR; break;
+ case kind::ITE:
+ if (current.getType().isBitVector() || current.getType().isBoolean())
+ {
+ new_kind = kind::BITVECTOR_ITE;
+ }
+ break;
+ case kind::BITVECTOR_ULT: new_kind = kind::BITVECTOR_ULTBV; break;
+ case kind::BITVECTOR_SLT: new_kind = kind::BITVECTOR_SLTBV; break;
+ case kind::BITVECTOR_ULE:
+ case kind::BITVECTOR_UGT:
+ case kind::BITVECTOR_UGE:
+ case kind::BITVECTOR_SLE:
+ case kind::BITVECTOR_SGT:
+ case kind::BITVECTOR_SGE:
+ // Should have been removed by rewriting.
+ Unreachable();
+ default: break;
+ }
+ NodeBuilder<> builder(new_kind);
+ if (kind != new_kind)
+ {
+ ++(d_statistics.d_numTermsLowered);
+ }
+ if (current.getMetaKind() == kind::metakind::PARAMETERIZED)
+ {
+ builder << current.getOperator();
+ }
+ Node converted;
+ if (new_kind == kind::ITE)
+ {
+ // Special-case ITE because need condition to be Boolean.
+ converted = lowerNode(current[0], true);
+ builder << converted;
+ converted = lowerNode(current[1]);
+ builder << converted;
+ converted = lowerNode(current[2]);
+ builder << converted;
+ }
+ else
+ {
+ for (unsigned i = 0; i < current.getNumChildren(); ++i)
+ {
+ converted = lowerNode(current[i]);
+ builder << converted;
+ }
+ }
+ result = builder;
+ }
+ if (result.getType().isBoolean())
+ {
+ ++(d_statistics.d_numTermsForcedLowered);
+ result = nm->mkNode(kind::ITE, result, d_one, d_zero);
+ }
+ addToLowerCache(current, result);
+ }
+ if (topLevel)
+ {
+ result = nm->mkNode(kind::EQUAL, result, d_one);
+ }
+ Assert(result != Node());
+ Debug("bool-to-bv") << "BoolToBV::lowerNode " << current << " => \n"
+ << result << "\n";
+ return result;
+}
+
+void BoolToBV::lowerBoolToBv(const std::vector<Node>& assertions,
+ std::vector<Node>& new_assertions)
+{
+ for (unsigned i = 0; i < assertions.size(); ++i)
+ {
+ Node new_assertion = lowerNode(assertions[i], true);
+ new_assertions.push_back(new_assertion);
+ Trace("bool-to-bv") << " " << assertions[i] << " => " << new_assertions[i]
+ << "\n";
+ }
+}
+
+BoolToBV::Statistics::Statistics()
+ : d_numTermsLowered("preprocessing::passes::BoolToBV::NumTermsLowered", 0),
+ d_numAtomsLowered("preprocessing::passes::BoolToBV::NumAtomsLowered", 0),
+ d_numTermsForcedLowered(
+ "preprocessing::passes::BoolToBV::NumTermsForcedLowered", 0)
+{
+ smtStatisticsRegistry()->registerStat(&d_numTermsLowered);
+ smtStatisticsRegistry()->registerStat(&d_numAtomsLowered);
+ smtStatisticsRegistry()->registerStat(&d_numTermsForcedLowered);
+}
+
+BoolToBV::Statistics::~Statistics()
+{
+ smtStatisticsRegistry()->unregisterStat(&d_numTermsLowered);
+ smtStatisticsRegistry()->unregisterStat(&d_numAtomsLowered);
+ smtStatisticsRegistry()->unregisterStat(&d_numTermsForcedLowered);
+}
+
+} // namespace passes
+} // namespace preprocessing
+} // namespace CVC4
diff --git a/src/preprocessing/passes/bool_to_bv.h b/src/preprocessing/passes/bool_to_bv.h
new file mode 100644
index 000000000..e85693d1c
--- /dev/null
+++ b/src/preprocessing/passes/bool_to_bv.h
@@ -0,0 +1,64 @@
+/********************* */
+/*! \file bool_to_bv.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Liana Hadarean, Clark Barrett, Paul Meng
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 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 The BoolToBv preprocessing pass
+ **
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__PREPROCESSING__PASSES__BOOL_TO_BV_H
+#define __CVC4__PREPROCESSING__PASSES__BOOL_TO_BV_H
+
+#include "preprocessing/passes/bv_to_bool.h"
+#include "preprocessing/preprocessing_pass.h"
+#include "preprocessing/preprocessing_pass_context.h"
+#include "util/statistics_registry.h"
+
+namespace CVC4 {
+namespace preprocessing {
+namespace passes {
+
+class BoolToBV : public PreprocessingPass
+{
+ public:
+ BoolToBV(PreprocessingPassContext* preprocContext);
+
+ protected:
+ PreprocessingPassResult applyInternal(
+ AssertionPipeline* assertionsToPreprocess) override;
+
+ private:
+ struct Statistics
+ {
+ IntStat d_numTermsLowered;
+ IntStat d_numAtomsLowered;
+ IntStat d_numTermsForcedLowered;
+ Statistics();
+ ~Statistics();
+ };
+
+ void lowerBoolToBv(const std::vector<Node>& assertions,
+ std::vector<Node>& new_assertions);
+ void addToLowerCache(TNode term, Node new_term);
+ Node getLowerCache(TNode term) const;
+ bool hasLowerCache(TNode term) const;
+ Node lowerNode(TNode current, bool topLevel = false);
+ Statistics d_statistics;
+ NodeNodeMap d_lowerCache;
+ Node d_one;
+ Node d_zero;
+}; // class
+} // namespace passes
+} // namespace preprocessing
+} // namespace CVC4
+
+#endif /* __CVC4__PREPROCESSING__PASSES__BOOL_TO_BV_H */
diff --git a/src/preprocessing/passes/bv_to_bool.cpp b/src/preprocessing/passes/bv_to_bool.cpp
new file mode 100644
index 000000000..b01a60031
--- /dev/null
+++ b/src/preprocessing/passes/bv_to_bool.cpp
@@ -0,0 +1,310 @@
+/********************* */
+/*! \file bv_to_bool.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Liana Hadarean, Aina Niemetz, Clark Barrett
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 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 Preprocessing pass that lifts bit-vectors of size 1 to booleans.
+ **
+ ** Preprocessing pass that lifts bit-vectors of size 1 to booleans.
+ **/
+
+#include "preprocessing/passes/bv_to_bool.h"
+
+#include <string>
+#include <unordered_map>
+#include <vector>
+
+#include "expr/node.h"
+#include "theory/rewriter.h"
+#include "theory/theory.h"
+
+#include "smt/smt_statistics_registry.h"
+#include "smt_util/node_visitor.h"
+
+namespace CVC4 {
+namespace preprocessing {
+namespace passes {
+
+using namespace std;
+using namespace CVC4::theory;
+
+BVToBool::BVToBool(PreprocessingPassContext* preprocContext)
+ : PreprocessingPass(preprocContext, "bv-to-bool"),
+ d_liftCache(),
+ d_boolCache(),
+ d_one(bv::utils::mkOne(1)),
+ d_zero(bv::utils::mkZero(1)),
+ d_statistics(){};
+
+PreprocessingPassResult BVToBool::applyInternal(
+ AssertionPipeline* assertionsToPreprocess)
+{
+ NodeManager::currentResourceManager()->spendResource(
+ options::preprocessStep());
+ std::vector<Node> new_assertions;
+ liftBvToBool(assertionsToPreprocess->ref(), new_assertions);
+ for (unsigned i = 0; i < assertionsToPreprocess->size(); ++i)
+ {
+ assertionsToPreprocess->replace(i, Rewriter::rewrite(new_assertions[i]));
+ }
+ return PreprocessingPassResult::NO_CONFLICT;
+}
+
+void BVToBool::addToLiftCache(TNode term, Node new_term)
+{
+ Assert(new_term != Node());
+ Assert(!hasLiftCache(term));
+ Assert(term.getType() == new_term.getType());
+ d_liftCache[term] = new_term;
+}
+
+Node BVToBool::getLiftCache(TNode term) const
+{
+ Assert(hasLiftCache(term));
+ return d_liftCache.find(term)->second;
+}
+
+bool BVToBool::hasLiftCache(TNode term) const
+{
+ return d_liftCache.find(term) != d_liftCache.end();
+}
+
+void BVToBool::addToBoolCache(TNode term, Node new_term)
+{
+ Assert(new_term != Node());
+ Assert(!hasBoolCache(term));
+ Assert(bv::utils::getSize(term) == 1);
+ Assert(new_term.getType().isBoolean());
+ d_boolCache[term] = new_term;
+}
+
+Node BVToBool::getBoolCache(TNode term) const
+{
+ Assert(hasBoolCache(term));
+ return d_boolCache.find(term)->second;
+}
+
+bool BVToBool::hasBoolCache(TNode term) const
+{
+ return d_boolCache.find(term) != d_boolCache.end();
+}
+bool BVToBool::isConvertibleBvAtom(TNode node)
+{
+ Kind kind = node.getKind();
+ return (kind == kind::EQUAL && node[0].getType().isBitVector()
+ && node[0].getType().getBitVectorSize() == 1
+ && node[1].getType().isBitVector()
+ && node[1].getType().getBitVectorSize() == 1
+ && node[0].getKind() != kind::BITVECTOR_EXTRACT
+ && node[1].getKind() != kind::BITVECTOR_EXTRACT);
+}
+
+bool BVToBool::isConvertibleBvTerm(TNode node)
+{
+ if (!node.getType().isBitVector() || node.getType().getBitVectorSize() != 1)
+ return false;
+
+ Kind kind = node.getKind();
+
+ if (kind == kind::CONST_BITVECTOR || kind == kind::ITE
+ || kind == kind::BITVECTOR_AND
+ || kind == kind::BITVECTOR_OR
+ || kind == kind::BITVECTOR_NOT
+ || kind == kind::BITVECTOR_XOR
+ || kind == kind::BITVECTOR_COMP)
+ {
+ return true;
+ }
+
+ return false;
+}
+
+Node BVToBool::convertBvAtom(TNode node)
+{
+ Assert(node.getType().isBoolean() && node.getKind() == kind::EQUAL);
+ Assert(bv::utils::getSize(node[0]) == 1);
+ Assert(bv::utils::getSize(node[1]) == 1);
+ Node a = convertBvTerm(node[0]);
+ Node b = convertBvTerm(node[1]);
+ Node result = NodeManager::currentNM()->mkNode(kind::EQUAL, a, b);
+ Debug("bv-to-bool") << "BVToBool::convertBvAtom " << node << " => " << result
+ << "\n";
+
+ ++(d_statistics.d_numAtomsLifted);
+ return result;
+}
+
+Node BVToBool::convertBvTerm(TNode node)
+{
+ Assert(node.getType().isBitVector()
+ && node.getType().getBitVectorSize() == 1);
+
+ if (hasBoolCache(node)) return getBoolCache(node);
+
+ NodeManager* nm = NodeManager::currentNM();
+
+ if (!isConvertibleBvTerm(node))
+ {
+ ++(d_statistics.d_numTermsForcedLifted);
+ Node result = nm->mkNode(kind::EQUAL, node, d_one);
+ addToBoolCache(node, result);
+ Debug("bv-to-bool") << "BVToBool::convertBvTerm " << node << " => "
+ << result << "\n";
+ return result;
+ }
+
+ if (node.getNumChildren() == 0)
+ {
+ Assert(node.getKind() == kind::CONST_BITVECTOR);
+ Node result = node == d_one ? bv::utils::mkTrue() : bv::utils::mkFalse();
+ // addToCache(node, result);
+ Debug("bv-to-bool") << "BVToBool::convertBvTerm " << node << " => "
+ << result << "\n";
+ return result;
+ }
+
+ ++(d_statistics.d_numTermsLifted);
+
+ Kind kind = node.getKind();
+ if (kind == kind::ITE)
+ {
+ Node cond = liftNode(node[0]);
+ Node true_branch = convertBvTerm(node[1]);
+ Node false_branch = convertBvTerm(node[2]);
+ Node result = nm->mkNode(kind::ITE, cond, true_branch, false_branch);
+ addToBoolCache(node, result);
+ Debug("bv-to-bool") << "BVToBool::convertBvTerm " << node << " => "
+ << result << "\n";
+ return result;
+ }
+
+ Kind new_kind;
+ // special case for XOR as it has to be binary
+ // while BITVECTOR_XOR can be n-ary
+ if (kind == kind::BITVECTOR_XOR)
+ {
+ new_kind = kind::XOR;
+ Node result = convertBvTerm(node[0]);
+ for (unsigned i = 1; i < node.getNumChildren(); ++i)
+ {
+ Node converted = convertBvTerm(node[i]);
+ result = nm->mkNode(kind::XOR, result, converted);
+ }
+ Debug("bv-to-bool") << "BVToBool::convertBvTerm " << node << " => "
+ << result << "\n";
+ return result;
+ }
+
+ if (kind == kind::BITVECTOR_COMP)
+ {
+ Node result = nm->mkNode(kind::EQUAL, node[0], node[1]);
+ addToBoolCache(node, result);
+ Debug("bv-to-bool") << "BVToBool::convertBvTerm " << node << " => "
+ << result << "\n";
+ return result;
+ }
+
+ switch (kind)
+ {
+ case kind::BITVECTOR_OR: new_kind = kind::OR; break;
+ case kind::BITVECTOR_AND: new_kind = kind::AND; break;
+ case kind::BITVECTOR_XOR: new_kind = kind::XOR; break;
+ case kind::BITVECTOR_NOT: new_kind = kind::NOT; break;
+ default: Unhandled();
+ }
+
+ NodeBuilder<> builder(new_kind);
+ for (unsigned i = 0; i < node.getNumChildren(); ++i)
+ {
+ builder << convertBvTerm(node[i]);
+ }
+
+ Node result = builder;
+ addToBoolCache(node, result);
+ Debug("bv-to-bool") << "BVToBool::convertBvTerm " << node << " => " << result
+ << "\n";
+ return result;
+}
+
+Node BVToBool::liftNode(TNode current)
+{
+ Node result;
+
+ if (hasLiftCache(current))
+ {
+ result = getLiftCache(current);
+ }
+ else if (isConvertibleBvAtom(current))
+ {
+ result = convertBvAtom(current);
+ addToLiftCache(current, result);
+ }
+ else
+ {
+ if (current.getNumChildren() == 0)
+ {
+ result = current;
+ }
+ else
+ {
+ NodeBuilder<> builder(current.getKind());
+ if (current.getMetaKind() == kind::metakind::PARAMETERIZED)
+ {
+ builder << current.getOperator();
+ }
+ for (unsigned i = 0; i < current.getNumChildren(); ++i)
+ {
+ Node converted = liftNode(current[i]);
+ Assert(converted.getType() == current[i].getType());
+ builder << converted;
+ }
+ result = builder;
+ addToLiftCache(current, result);
+ }
+ }
+ Assert(result != Node());
+ Assert(result.getType() == current.getType());
+ Debug("bv-to-bool") << "BVToBool::liftNode " << current << " => \n"
+ << result << "\n";
+ return result;
+}
+
+void BVToBool::liftBvToBool(const std::vector<Node>& assertions,
+ std::vector<Node>& new_assertions)
+{
+ for (unsigned i = 0; i < assertions.size(); ++i)
+ {
+ Node new_assertion = liftNode(assertions[i]);
+ new_assertions.push_back(Rewriter::rewrite(new_assertion));
+ Trace("bv-to-bool") << " " << assertions[i] << " => " << new_assertions[i]
+ << "\n";
+ }
+}
+
+BVToBool::Statistics::Statistics()
+ : d_numTermsLifted("preprocessing::passes::BVToBool::NumTermsLifted", 0),
+ d_numAtomsLifted("preprocessing::passes::BVToBool::NumAtomsLifted", 0),
+ d_numTermsForcedLifted(
+ "preprocessing::passes::BVToBool::NumTermsForcedLifted", 0)
+{
+ smtStatisticsRegistry()->registerStat(&d_numTermsLifted);
+ smtStatisticsRegistry()->registerStat(&d_numAtomsLifted);
+ smtStatisticsRegistry()->registerStat(&d_numTermsForcedLifted);
+}
+
+BVToBool::Statistics::~Statistics()
+{
+ smtStatisticsRegistry()->unregisterStat(&d_numTermsLifted);
+ smtStatisticsRegistry()->unregisterStat(&d_numAtomsLifted);
+ smtStatisticsRegistry()->unregisterStat(&d_numTermsForcedLifted);
+}
+
+} // passes
+} // Preprocessing
+} // CVC4
diff --git a/src/theory/bv/bv_to_bool.h b/src/preprocessing/passes/bv_to_bool.h
index 93a83626e..f772087e8 100644
--- a/src/theory/bv/bv_to_bool.h
+++ b/src/preprocessing/passes/bv_to_bool.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Liana Hadarean, Clark Barrett, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 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
@@ -16,71 +16,64 @@
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__BV__BV_TO_BOOL_H
-#define __CVC4__THEORY__BV__BV_TO_BOOL_H
-
-#include <unordered_map>
+#ifndef __CVC4__PREPROCESSING__PASSES__BV_TO_BOOL_H
+#define __CVC4__PREPROCESSING__PASSES__BV_TO_BOOL_H
+#include "preprocessing/preprocessing_pass.h"
+#include "preprocessing/preprocessing_pass_context.h"
#include "theory/bv/theory_bv_utils.h"
#include "util/statistics_registry.h"
namespace CVC4 {
-namespace theory {
-namespace bv {
+namespace preprocessing {
+namespace passes {
typedef std::unordered_map<Node, Node, NodeHashFunction> NodeNodeMap;
-class BvToBoolPreprocessor {
+class BVToBool : public PreprocessingPass
+{
+
+ public:
+ BVToBool(PreprocessingPassContext* preprocContext);
+
+ protected:
+ PreprocessingPassResult applyInternal(
+ AssertionPipeline* assertionsToPreprocess) override;
- struct Statistics {
+ private:
+ struct Statistics
+ {
IntStat d_numTermsLifted;
IntStat d_numAtomsLifted;
IntStat d_numTermsForcedLifted;
- IntStat d_numTermsLowered;
- IntStat d_numAtomsLowered;
- IntStat d_numTermsForcedLowered;
Statistics();
~Statistics();
};
-
- NodeNodeMap d_liftCache;
- NodeNodeMap d_boolCache;
- Node d_one;
- Node d_zero;
-
void addToBoolCache(TNode term, Node new_term);
Node getBoolCache(TNode term) const;
- bool hasBoolCache(TNode term) const;
+ bool hasBoolCache(TNode term) const;
void addToLiftCache(TNode term, Node new_term);
Node getLiftCache(TNode term) const;
- bool hasLiftCache(TNode term) const;
-
+ bool hasLiftCache(TNode term) const;
+
bool isConvertibleBvTerm(TNode node);
bool isConvertibleBvAtom(TNode node);
Node convertBvAtom(TNode node);
Node convertBvTerm(TNode node);
Node liftNode(TNode current);
- Statistics d_statistics;
+ void liftBvToBool(const std::vector<Node>& assertions,
+ std::vector<Node>& new_assertions);
- NodeNodeMap d_lowerCache;
- void addToLowerCache(TNode term, Node new_term);
- Node getLowerCache(TNode term) const;
- bool hasLowerCache(TNode term) const;
- Node lowerNode(TNode current, bool topLevel = false);
-
-public:
- BvToBoolPreprocessor();
- void liftBvToBool(const std::vector<Node>& assertions, std::vector<Node>& new_assertions);
- void lowerBoolToBv(const std::vector<Node>& assertions, std::vector<Node>& new_assertions);
-};
-
-
-
-}/* CVC4::theory::bv namespace */
-}/* CVC4::theory namespace */
-
-}/* CVC4 namespace */
+ Statistics d_statistics;
+ NodeNodeMap d_liftCache;
+ NodeNodeMap d_boolCache;
+ Node d_one;
+ Node d_zero;
+};
+} // namespace passes
+} // namespace preprocessing
+} // namespace CVC4
-#endif /* __CVC4__THEORY__BV__BV_TO_BOOL_H */
+#endif /* __CVC4__PREPROCESSING__PASSES__BV_TO_BOOL_H */
diff --git a/src/preprocessing/preprocessing_pass_registry.cpp b/src/preprocessing/preprocessing_pass_registry.cpp
index 4f0693a25..71a91309b 100644
--- a/src/preprocessing/preprocessing_pass_registry.cpp
+++ b/src/preprocessing/preprocessing_pass_registry.cpp
@@ -45,5 +45,10 @@ PreprocessingPass* PreprocessingPassRegistry::getPass(
return d_stringToPreprocessingPass[ppName].get();
}
+void PreprocessingPassRegistry::unregisterPasses()
+{
+ d_stringToPreprocessingPass.clear();
+}
+
} // namespace preprocessing
} // namespace CVC4
diff --git a/src/preprocessing/preprocessing_pass_registry.h b/src/preprocessing/preprocessing_pass_registry.h
index 37cff676b..e374a6bdb 100644
--- a/src/preprocessing/preprocessing_pass_registry.h
+++ b/src/preprocessing/preprocessing_pass_registry.h
@@ -42,6 +42,11 @@ class PreprocessingPassRegistry {
*/
PreprocessingPass* getPass(const std::string& ppName);
+ /**
+ Clears all passes from the registry.
+ */
+ void unregisterPasses();
+
private:
bool hasPass(const std::string& ppName);
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 9453adefd..97fbe82b8 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -68,7 +68,9 @@
#include "options/strings_options.h"
#include "options/theory_options.h"
#include "options/uf_options.h"
+#include "preprocessing/passes/bool_to_bv.h"
#include "preprocessing/passes/bv_gauss.h"
+#include "preprocessing/passes/bv_to_bool.h"
#include "preprocessing/passes/int_to_bv.h"
#include "preprocessing/passes/pseudo_boolean_processor.h"
#include "preprocessing/passes/symmetry_detect.h"
@@ -611,12 +613,6 @@ public:
*/
bool checkForBadSkolems(TNode n, TNode skolem, NodeToBoolHashMap& cache);
- // Lift bit-vectors of size 1 to booleans
- void bvToBool();
-
- // Convert booleans to bit-vectors of size 1
- void boolToBv();
-
// Abstract common structure over small domains to UF
// return true if changes were made.
void bvAbstraction();
@@ -751,6 +747,11 @@ public:
d_smt.d_nodeManager->unsubscribeEvents(this);
}
+ void unregisterPreprocessingPasses()
+ {
+ d_preprocessingPassRegistry.unregisterPasses();
+ }
+
ResourceManager* getResourceManager() { return d_resourceManager; }
void spendResource(unsigned amount)
{
@@ -1225,6 +1226,9 @@ SmtEngine::~SmtEngine()
d_definedFunctions->deleteSelf();
d_fmfRecFunctionsDefined->deleteSelf();
+ //destroy all passes before destroying things that they refer to
+ d_private->unregisterPreprocessingPasses();
+
delete d_theoryEngine;
d_theoryEngine = NULL;
delete d_propEngine;
@@ -2590,6 +2594,12 @@ void SmtEnginePrivate::finishInit() {
d_preprocessingPassRegistry.registerPass("int-to-bv", std::move(intToBV));
d_preprocessingPassRegistry.registerPass("pseudo-boolean-processor",
std::move(pbProc));
+ std::unique_ptr<BVToBool> bvToBool(
+ new BVToBool(d_preprocessingPassContext.get()));
+ d_preprocessingPassRegistry.registerPass("bv-to-bool", std::move(bvToBool));
+ std::unique_ptr<BoolToBV> boolToBv(
+ new BoolToBV(d_preprocessingPassContext.get()));
+ d_preprocessingPassRegistry.registerPass("bool-to-bv", std::move(boolToBv));
}
Node SmtEnginePrivate::expandDefinitions(TNode n, unordered_map<Node, Node, NodeHashFunction>& cache, bool expandOnly)
@@ -3273,25 +3283,6 @@ void SmtEnginePrivate::bvAbstraction() {
}
-void SmtEnginePrivate::bvToBool() {
- Trace("bv-to-bool") << "SmtEnginePrivate::bvToBool()" << endl;
- spendResource(options::preprocessStep());
- std::vector<Node> new_assertions;
- d_smt.d_theoryEngine->ppBvToBool(d_assertions.ref(), new_assertions);
- for (unsigned i = 0; i < d_assertions.size(); ++ i) {
- d_assertions.replace(i, Rewriter::rewrite(new_assertions[i]));
- }
-}
-
-void SmtEnginePrivate::boolToBv() {
- Trace("bool-to-bv") << "SmtEnginePrivate::boolToBv()" << endl;
- spendResource(options::preprocessStep());
- std::vector<Node> new_assertions;
- d_smt.d_theoryEngine->ppBoolToBv(d_assertions.ref(), new_assertions);
- for (unsigned i = 0; i < d_assertions.size(); ++ i) {
- d_assertions.replace(i, Rewriter::rewrite(new_assertions[i]));
- }
-}
bool SmtEnginePrivate::simpITE() {
TimerStat::CodeTimer simpITETimer(d_smt.d_stats->d_simpITETime);
@@ -4209,7 +4200,7 @@ void SmtEnginePrivate::processAssertions() {
if(options::bitvectorToBool()) {
dumpAssertions("pre-bv-to-bool", d_assertions);
Chat() << "...doing bvToBool..." << endl;
- bvToBool();
+ d_preprocessingPassRegistry.getPass("bv-to-bool")->apply(&d_assertions);
dumpAssertions("post-bv-to-bool", d_assertions);
Trace("smt") << "POST bvToBool" << endl;
}
@@ -4217,7 +4208,7 @@ void SmtEnginePrivate::processAssertions() {
if(options::boolToBitvector()) {
dumpAssertions("pre-bool-to-bv", d_assertions);
Chat() << "...doing boolToBv..." << endl;
- boolToBv();
+ d_preprocessingPassRegistry.getPass("bool-to-bv")->apply(&d_assertions);
dumpAssertions("post-bool-to-bv", d_assertions);
Trace("smt") << "POST boolToBv" << endl;
}
diff --git a/src/theory/bv/bv_to_bool.cpp b/src/theory/bv/bv_to_bool.cpp
deleted file mode 100644
index 54c9cb08a..000000000
--- a/src/theory/bv/bv_to_bool.cpp
+++ /dev/null
@@ -1,387 +0,0 @@
-/********************* */
-/*! \file bv_to_bool.cpp
- ** \verbatim
- ** Top contributors (to current version):
- ** Liana Hadarean, Aina Niemetz, Clark Barrett
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 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 Preprocessing pass that lifts bit-vectors of size 1 to booleans.
- **
- ** Preprocessing pass that lifts bit-vectors of size 1 to booleans.
- **/
-#include "theory/bv/bv_to_bool.h"
-
-#include "smt_util/node_visitor.h"
-#include "smt/smt_statistics_registry.h"
-
-using namespace std;
-using namespace CVC4;
-using namespace CVC4::theory;
-using namespace CVC4::theory::bv;
-
-BvToBoolPreprocessor::BvToBoolPreprocessor()
- : d_liftCache()
- , d_boolCache()
- , d_one(utils::mkOne(1))
- , d_zero(utils::mkZero(1))
- , d_statistics()
-{}
-
-void BvToBoolPreprocessor::addToLiftCache(TNode term, Node new_term) {
- Assert (new_term != Node());
- Assert (!hasLiftCache(term));
- Assert (term.getType() == new_term.getType());
- d_liftCache[term] = new_term;
-}
-
-Node BvToBoolPreprocessor::getLiftCache(TNode term) const {
- Assert(hasLiftCache(term));
- return d_liftCache.find(term)->second;
-}
-
-bool BvToBoolPreprocessor::hasLiftCache(TNode term) const {
- return d_liftCache.find(term) != d_liftCache.end();
-}
-
-void BvToBoolPreprocessor::addToBoolCache(TNode term, Node new_term) {
- Assert (new_term != Node());
- Assert (!hasBoolCache(term));
- Assert (utils::getSize(term) == 1);
- Assert (new_term.getType().isBoolean());
- d_boolCache[term] = new_term;
-}
-
-Node BvToBoolPreprocessor::getBoolCache(TNode term) const {
- Assert(hasBoolCache(term));
- return d_boolCache.find(term)->second;
-}
-
-bool BvToBoolPreprocessor::hasBoolCache(TNode term) const {
- return d_boolCache.find(term) != d_boolCache.end();
-}
-bool BvToBoolPreprocessor::isConvertibleBvAtom(TNode node) {
- Kind kind = node.getKind();
- return (kind == kind::EQUAL &&
- node[0].getType().isBitVector() &&
- node[0].getType().getBitVectorSize() == 1 &&
- node[1].getType().isBitVector() &&
- node[1].getType().getBitVectorSize() == 1 &&
- node[0].getKind() != kind::BITVECTOR_EXTRACT &&
- node[1].getKind() != kind::BITVECTOR_EXTRACT);
-}
-
-bool BvToBoolPreprocessor::isConvertibleBvTerm(TNode node) {
- if (!node.getType().isBitVector() ||
- node.getType().getBitVectorSize() != 1)
- return false;
-
- Kind kind = node.getKind();
-
- if (kind == kind::CONST_BITVECTOR ||
- kind == kind::ITE ||
- kind == kind::BITVECTOR_AND ||
- kind == kind::BITVECTOR_OR ||
- kind == kind::BITVECTOR_NOT ||
- kind == kind::BITVECTOR_XOR ||
- kind == kind::BITVECTOR_COMP) {
- return true;
- }
-
- return false;
-}
-
-Node BvToBoolPreprocessor::convertBvAtom(TNode node)
-{
- Assert(node.getType().isBoolean() && node.getKind() == kind::EQUAL);
- Assert(utils::getSize(node[0]) == 1);
- Assert(utils::getSize(node[1]) == 1);
- Node a = convertBvTerm(node[0]);
- Node b = convertBvTerm(node[1]);
- Node result = NodeManager::currentNM()->mkNode(kind::EQUAL, a, b);
- Debug("bv-to-bool") << "BvToBoolPreprocessor::convertBvAtom " << node
- << " => " << result << "\n";
-
- ++(d_statistics.d_numAtomsLifted);
- return result;
-}
-
-Node BvToBoolPreprocessor::convertBvTerm(TNode node)
-{
- Assert(node.getType().isBitVector()
- && node.getType().getBitVectorSize() == 1);
-
- if (hasBoolCache(node)) return getBoolCache(node);
-
- NodeManager* nm = NodeManager::currentNM();
-
- if (!isConvertibleBvTerm(node))
- {
- ++(d_statistics.d_numTermsForcedLifted);
- Node result = nm->mkNode(kind::EQUAL, node, d_one);
- addToBoolCache(node, result);
- Debug("bv-to-bool") << "BvToBoolPreprocessor::convertBvTerm " << node
- << " => " << result << "\n";
- return result;
- }
-
- if (node.getNumChildren() == 0)
- {
- Assert(node.getKind() == kind::CONST_BITVECTOR);
- Node result = node == d_one ? utils::mkTrue() : utils::mkFalse();
- // addToCache(node, result);
- Debug("bv-to-bool") << "BvToBoolPreprocessor::convertBvTerm " << node
- << " => " << result << "\n";
- return result;
- }
-
- ++(d_statistics.d_numTermsLifted);
-
- Kind kind = node.getKind();
- if (kind == kind::ITE)
- {
- Node cond = liftNode(node[0]);
- Node true_branch = convertBvTerm(node[1]);
- Node false_branch = convertBvTerm(node[2]);
- Node result = nm->mkNode(kind::ITE, cond, true_branch, false_branch);
- addToBoolCache(node, result);
- Debug("bv-to-bool") << "BvToBoolPreprocessor::convertBvTerm " << node
- << " => " << result << "\n";
- return result;
- }
-
- Kind new_kind;
- // special case for XOR as it has to be binary
- // while BITVECTOR_XOR can be n-ary
- if (kind == kind::BITVECTOR_XOR)
- {
- new_kind = kind::XOR;
- Node result = convertBvTerm(node[0]);
- for (unsigned i = 1; i < node.getNumChildren(); ++i)
- {
- Node converted = convertBvTerm(node[i]);
- result = nm->mkNode(kind::XOR, result, converted);
- }
- Debug("bv-to-bool") << "BvToBoolPreprocessor::convertBvTerm " << node
- << " => " << result << "\n";
- return result;
- }
-
- if (kind == kind::BITVECTOR_COMP)
- {
- Node result = nm->mkNode(kind::EQUAL, node[0], node[1]);
- addToBoolCache(node, result);
- Debug("bv-to-bool") << "BvToBoolPreprocessor::convertBvTerm " << node
- << " => " << result << "\n";
- return result;
- }
-
- switch (kind)
- {
- case kind::BITVECTOR_OR: new_kind = kind::OR; break;
- case kind::BITVECTOR_AND: new_kind = kind::AND; break;
- case kind::BITVECTOR_XOR: new_kind = kind::XOR; break;
- case kind::BITVECTOR_NOT: new_kind = kind::NOT; break;
- default: Unhandled();
- }
-
- NodeBuilder<> builder(new_kind);
- for (unsigned i = 0; i < node.getNumChildren(); ++i)
- {
- builder << convertBvTerm(node[i]);
- }
-
- Node result = builder;
- addToBoolCache(node, result);
- Debug("bv-to-bool") << "BvToBoolPreprocessor::convertBvTerm " << node
- << " => " << result << "\n";
- return result;
-}
-
-Node BvToBoolPreprocessor::liftNode(TNode current) {
- Node result;
-
- if (hasLiftCache(current)) {
- result = getLiftCache(current);
- }else if (isConvertibleBvAtom(current)) {
- result = convertBvAtom(current);
- addToLiftCache(current, result);
- } else {
- if (current.getNumChildren() == 0) {
- result = current;
- } else {
- NodeBuilder<> builder(current.getKind());
- if (current.getMetaKind() == kind::metakind::PARAMETERIZED) {
- builder << current.getOperator();
- }
- for (unsigned i = 0; i < current.getNumChildren(); ++i) {
- Node converted = liftNode(current[i]);
- Assert (converted.getType() == current[i].getType());
- builder << converted;
- }
- result = builder;
- addToLiftCache(current, result);
- }
- }
- Assert (result != Node());
- Assert(result.getType() == current.getType());
- Debug("bv-to-bool") << "BvToBoolPreprocessor::liftNode " << current << " => \n" << result << "\n";
- return result;
-}
-
-void BvToBoolPreprocessor::liftBvToBool(const std::vector<Node>& assertions, std::vector<Node>& new_assertions) {
- for (unsigned i = 0; i < assertions.size(); ++i) {
- Node new_assertion = liftNode(assertions[i]);
- new_assertions.push_back(new_assertion);
- Trace("bv-to-bool") << " " << assertions[i] <<" => " << new_assertions[i] <<"\n";
- }
-}
-
-BvToBoolPreprocessor::Statistics::Statistics()
- : d_numTermsLifted("theory::bv::BvToBool::NumTermsLifted", 0)
- , d_numAtomsLifted("theory::bv::BvToBool::NumAtomsLifted", 0)
- , d_numTermsForcedLifted("theory::bv::BvToBool::NumTermsForcedLifted", 0)
- , d_numTermsLowered("theory::bv::BvToBool::NumTermsLowered", 0)
- , d_numAtomsLowered("theory::bv::BvToBool::NumAtomsLowered", 0)
- , d_numTermsForcedLowered("theory::bv::BvToBool::NumTermsForcedLowered", 0)
-{
- smtStatisticsRegistry()->registerStat(&d_numTermsLifted);
- smtStatisticsRegistry()->registerStat(&d_numAtomsLifted);
- smtStatisticsRegistry()->registerStat(&d_numTermsForcedLifted);
- smtStatisticsRegistry()->registerStat(&d_numTermsLowered);
- smtStatisticsRegistry()->registerStat(&d_numAtomsLowered);
- smtStatisticsRegistry()->registerStat(&d_numTermsForcedLowered);
-}
-
-BvToBoolPreprocessor::Statistics::~Statistics() {
- smtStatisticsRegistry()->unregisterStat(&d_numTermsLifted);
- smtStatisticsRegistry()->unregisterStat(&d_numAtomsLifted);
- smtStatisticsRegistry()->unregisterStat(&d_numTermsForcedLifted);
- smtStatisticsRegistry()->unregisterStat(&d_numTermsLowered);
- smtStatisticsRegistry()->unregisterStat(&d_numAtomsLowered);
- smtStatisticsRegistry()->unregisterStat(&d_numTermsForcedLowered);
-}
-
-void BvToBoolPreprocessor::addToLowerCache(TNode term, Node new_term) {
- Assert (new_term != Node());
- Assert (!hasLowerCache(term));
- d_lowerCache[term] = new_term;
-}
-
-Node BvToBoolPreprocessor::getLowerCache(TNode term) const {
- Assert(hasLowerCache(term));
- return d_lowerCache.find(term)->second;
-}
-
-bool BvToBoolPreprocessor::hasLowerCache(TNode term) const {
- return d_lowerCache.find(term) != d_lowerCache.end();
-}
-
-Node BvToBoolPreprocessor::lowerNode(TNode current, bool topLevel)
-{
- Node result;
- NodeManager* nm = NodeManager::currentNM();
- if (hasLowerCache(current))
- {
- result = getLowerCache(current);
- }
- else
- {
- if (current.getNumChildren() == 0)
- {
- if (current.getKind() == kind::CONST_BOOLEAN)
- {
- result = (current == utils::mkTrue()) ? d_one : d_zero;
- }
- else
- {
- result = current;
- }
- }
- else
- {
- Kind kind = current.getKind();
- Kind new_kind = kind;
- switch (kind)
- {
- case kind::EQUAL: new_kind = kind::BITVECTOR_COMP; break;
- case kind::AND: new_kind = kind::BITVECTOR_AND; break;
- case kind::OR: new_kind = kind::BITVECTOR_OR; break;
- case kind::NOT: new_kind = kind::BITVECTOR_NOT; break;
- case kind::XOR: new_kind = kind::BITVECTOR_XOR; break;
- case kind::ITE:
- if (current.getType().isBitVector() || current.getType().isBoolean())
- {
- new_kind = kind::BITVECTOR_ITE;
- }
- break;
- case kind::BITVECTOR_ULT: new_kind = kind::BITVECTOR_ULTBV; break;
- case kind::BITVECTOR_SLT: new_kind = kind::BITVECTOR_SLTBV; break;
- case kind::BITVECTOR_ULE:
- case kind::BITVECTOR_UGT:
- case kind::BITVECTOR_UGE:
- case kind::BITVECTOR_SLE:
- case kind::BITVECTOR_SGT:
- case kind::BITVECTOR_SGE:
- // Should have been removed by rewriting.
- Unreachable();
- default: break;
- }
- NodeBuilder<> builder(new_kind);
- if (kind != new_kind)
- {
- ++(d_statistics.d_numTermsLowered);
- }
- if (current.getMetaKind() == kind::metakind::PARAMETERIZED)
- {
- builder << current.getOperator();
- }
- Node converted;
- if (new_kind == kind::ITE)
- {
- // Special-case ITE because need condition to be Boolean.
- converted = lowerNode(current[0], true);
- builder << converted;
- converted = lowerNode(current[1]);
- builder << converted;
- converted = lowerNode(current[2]);
- builder << converted;
- }
- else
- {
- for (unsigned i = 0; i < current.getNumChildren(); ++i)
- {
- converted = lowerNode(current[i]);
- builder << converted;
- }
- }
- result = builder;
- }
- if (result.getType().isBoolean())
- {
- ++(d_statistics.d_numTermsForcedLowered);
- result = nm->mkNode(kind::ITE, result, d_one, d_zero);
- }
- addToLowerCache(current, result);
- }
- if (topLevel)
- {
- result = nm->mkNode(kind::EQUAL, result, d_one);
- }
- Assert(result != Node());
- Debug("bool-to-bv") << "BvToBoolPreprocessor::lowerNode " << current
- << " => \n"
- << result << "\n";
- return result;
-}
-
-void BvToBoolPreprocessor::lowerBoolToBv(const std::vector<Node>& assertions, std::vector<Node>& new_assertions) {
- for (unsigned i = 0; i < assertions.size(); ++i) {
- Node new_assertion = lowerNode(assertions[i], true);
- new_assertions.push_back(new_assertion);
- Trace("bool-to-bv") << " " << assertions[i] <<" => " << new_assertions[i] <<"\n";
- }
-}
diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp
index 76d95bf5e..a80737fe2 100644
--- a/src/theory/quantifiers/term_util.cpp
+++ b/src/theory/quantifiers/term_util.cpp
@@ -20,6 +20,7 @@
#include "options/quantifiers_options.h"
#include "options/uf_options.h"
#include "theory/arith/arith_msum.h"
+#include "theory/bv/theory_bv_utils.h"
#include "theory/quantifiers/term_database.h"
#include "theory/quantifiers/term_enumeration.h"
#include "theory/quantifiers_engine.h"
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 850c7ed97..885c36bb5 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -314,7 +314,6 @@ TheoryEngine::TheoryEngine(context::Context* context,
d_preRegistrationVisitor(this, context),
d_sharedTermsVisitor(d_sharedTerms),
d_unconstrainedSimp(new UnconstrainedSimplifier(context, logicInfo)),
- d_bvToBoolPreprocessor(),
d_theoryAlternatives(),
d_attr_handle(),
d_arithSubstitutionsAdded("theory::arith::zzz::arith::substitutions", 0)
@@ -1990,14 +1989,6 @@ void TheoryEngine::staticInitializeBVOptions(
}
}
-void TheoryEngine::ppBvToBool(const std::vector<Node>& assertions, std::vector<Node>& new_assertions) {
- d_bvToBoolPreprocessor.liftBvToBool(assertions, new_assertions);
-}
-
-void TheoryEngine::ppBoolToBv(const std::vector<Node>& assertions, std::vector<Node>& new_assertions) {
- d_bvToBoolPreprocessor.lowerBoolToBv(assertions, new_assertions);
-}
-
bool TheoryEngine::ppBvAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions) {
bv::TheoryBV* bv_theory = (bv::TheoryBV*)d_theoryTable[THEORY_BV];
return bv_theory->applyAbstraction(assertions, new_assertions);
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 04e3c5697..80853bb6f 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -35,7 +35,6 @@
#include "smt/command.h"
#include "smt_util/lemma_channels.h"
#include "theory/atom_requests.h"
-#include "theory/bv/bv_to_bool.h"
#include "theory/interrupted.h"
#include "theory/rewriter.h"
#include "theory/shared_terms_database.h"
@@ -851,11 +850,8 @@ private:
UnconstrainedSimplifier* d_unconstrainedSimp;
/** For preprocessing pass lifting bit-vectors of size 1 to booleans */
- theory::bv::BvToBoolPreprocessor d_bvToBoolPreprocessor;
public:
void staticInitializeBVOptions(const std::vector<Node>& assertions);
- void ppBvToBool(const std::vector<Node>& assertions, std::vector<Node>& new_assertions);
- void ppBoolToBv(const std::vector<Node>& assertions, std::vector<Node>& new_assertions);
bool ppBvAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions);
void mkAckermanizationAssertions(std::vector<Node>& assertions);
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index af242b408..5b12c005c 100644
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -154,6 +154,7 @@ REG0_TESTS = \
regress0/bug605.cvc \
regress0/bug639.smt2 \
regress0/buggy-ite.smt2 \
+ regress0/bv/bool-to-bv.smt2 \
regress0/bv/bug260a.smt \
regress0/bv/bug260b.smt \
regress0/bv/bug440.smt \
@@ -161,6 +162,7 @@ REG0_TESTS = \
regress0/bv/bug734.smt2 \
regress0/bv/bv-int-collapse1.smt2 \
regress0/bv/bv-int-collapse2.smt2 \
+ regress0/bv/bv-to-bool.smt \
regress0/bv/bv-options1.smt2 \
regress0/bv/bv-options2.smt2 \
regress0/bv/bv-options3.smt2 \
diff --git a/test/regress/regress0/bv/bool-to-bv.smt2 b/test/regress/regress0/bv/bool-to-bv.smt2
new file mode 100644
index 000000000..9d336af96
--- /dev/null
+++ b/test/regress/regress0/bv/bool-to-bv.smt2
@@ -0,0 +1,9 @@
+; COMMAND-LINE: --bool-to-bv
+; EXPECT: sat
+(set-logic QF_BV)
+(declare-fun x2 () (_ BitVec 3))
+(declare-fun x1 () (_ BitVec 3))
+(declare-fun x0 () (_ BitVec 3))
+(assert (not (bvult (bvudiv (bvudiv (bvudiv x0 x0) x1) x2) x1)))
+(assert (= #b000 x2))
+(check-sat)
diff --git a/test/regress/regress0/bv/bv-to-bool.smt b/test/regress/regress0/bv/bv-to-bool.smt
new file mode 100644
index 000000000..ef4cec257
--- /dev/null
+++ b/test/regress/regress0/bv/bv-to-bool.smt
@@ -0,0 +1,185 @@
+; COMMAND-LINE: --bv-to-bool
+; EXPECT: sat
+(benchmark fuzzsmt
+:logic QF_BV
+:status sat
+:extrafuns ((v0 BitVec[16]))
+:extrafuns ((v1 BitVec[2]))
+:extrafuns ((v2 BitVec[11]))
+:extrafuns ((v3 BitVec[5]))
+:extrafuns ((v4 BitVec[15]))
+:formula
+(let (?e5 bv0[1])
+(let (?e6 (ite (bvult v4 (sign_extend[13] v1)) bv1[1] bv0[1]))
+(let (?e7 (bvadd (sign_extend[9] v1) v2))
+(let (?e8 (bvcomp v4 v4))
+(let (?e9 (bvadd ?e7 (zero_extend[10] ?e6)))
+(let (?e10 (bvand v0 (sign_extend[11] v3)))
+(let (?e11 (ite (bvsge (zero_extend[11] v3) v0) bv1[1] bv0[1]))
+(let (?e12 (ite (bvsge (zero_extend[9] v1) ?e9) bv1[1] bv0[1]))
+(let (?e13 (repeat[1] v0))
+(let (?e14 (bvshl ?e6 ?e12))
+(let (?e15 (ite (= bv1[1] (extract[0:0] v0)) ?e9 (zero_extend[10] ?e6)))
+(let (?e16 (ite (bvsle (sign_extend[9] v1) v2) bv1[1] bv0[1]))
+(let (?e17 (ite (bvsge v4 (zero_extend[14] ?e6)) bv1[1] bv0[1]))
+(let (?e18 (bvcomp (sign_extend[10] ?e6) ?e9))
+(let (?e19 (ite (bvsle ?e15 ?e15) bv1[1] bv0[1]))
+(let (?e20 (ite (bvule ?e10 (zero_extend[15] ?e5)) bv1[1] bv0[1]))
+(flet ($e21 (= (zero_extend[10] ?e18) ?e9))
+(flet ($e22 (= ?e7 ?e7))
+(flet ($e23 (= ?e17 ?e6))
+(flet ($e24 (= (zero_extend[15] ?e17) ?e10))
+(flet ($e25 (= (zero_extend[10] ?e16) ?e7))
+(flet ($e26 (= (sign_extend[13] v1) v4))
+(flet ($e27 (= (sign_extend[15] ?e16) v0))
+(flet ($e28 (= (sign_extend[15] ?e18) ?e10))
+(flet ($e29 (= ?e7 (sign_extend[10] ?e18)))
+(flet ($e30 (= ?e9 (sign_extend[9] v1)))
+(flet ($e31 (= ?e11 ?e18))
+(flet ($e32 (= (sign_extend[15] ?e20) ?e10))
+(flet ($e33 (= ?e18 ?e8))
+(flet ($e34 (= ?e14 ?e6))
+(flet ($e35 (= (zero_extend[15] ?e20) v0))
+(flet ($e36 (= v4 (sign_extend[14] ?e11)))
+(flet ($e37 (= (sign_extend[1] v4) ?e13))
+(flet ($e38 (= ?e20 ?e16))
+(flet ($e39 (= v1 (sign_extend[1] ?e14)))
+(flet ($e40 (= ?e5 ?e19))
+(flet ($e41 (= ?e7 (sign_extend[10] ?e14)))
+(flet ($e42 (= ?e15 (sign_extend[6] v3)))
+(flet ($e43 (= ?e18 ?e18))
+(flet ($e44 (= ?e16 ?e8))
+(flet ($e45 (= (sign_extend[15] ?e8) v0))
+(flet ($e46 (= (zero_extend[4] ?e15) v4))
+(flet ($e47 (= (sign_extend[14] ?e20) v4))
+(flet ($e48 (= v3 (sign_extend[4] ?e17)))
+(flet ($e49 (= ?e17 ?e6))
+(flet ($e50 (= ?e10 (sign_extend[15] ?e16)))
+(flet ($e51 (= ?e16 ?e18))
+(flet ($e52 (= (sign_extend[10] ?e12) ?e9))
+(flet ($e53 (= ?e8 ?e19))
+(flet ($e54 (= (zero_extend[1] ?e14) v1))
+(flet ($e55 (= v1 (sign_extend[1] ?e6)))
+(flet ($e56 (= v4 (zero_extend[14] ?e14)))
+(flet ($e57 (= ?e17 ?e20))
+(flet ($e58 (= ?e20 ?e11))
+(flet ($e59 (= (zero_extend[4] ?e6) v3))
+(flet ($e60 (= v0 (zero_extend[5] ?e9)))
+(flet ($e61 (= v0 (sign_extend[15] ?e17)))
+(flet ($e62 (= ?e15 ?e9))
+(flet ($e63 (= (sign_extend[4] ?e15) v4))
+(flet ($e64 (= (zero_extend[10] ?e16) ?e15))
+(flet ($e65 (= v4 (zero_extend[14] ?e18)))
+(flet ($e66 (= (sign_extend[10] ?e14) ?e9))
+(flet ($e67 (= ?e20 ?e17))
+(flet ($e68 (= ?e14 ?e18))
+(flet ($e69 (= ?e10 (sign_extend[5] ?e9)))
+(flet ($e70 (= ?e5 ?e16))
+(flet ($e71 (= (zero_extend[10] ?e19) ?e15))
+(flet ($e72 (= ?e15 ?e9))
+(flet ($e73 (= ?e12 ?e11))
+(flet ($e74 (= (sign_extend[10] ?e14) ?e7))
+(flet ($e75 (= ?e20 ?e20))
+(flet ($e76 (= ?e12 ?e18))
+(flet ($e77 (= ?e20 ?e16))
+(flet ($e78 (= ?e17 ?e16))
+(flet ($e79 (= (zero_extend[14] ?e17) v4))
+(flet ($e80 (= ?e7 (sign_extend[10] ?e8)))
+(flet ($e81 (= ?e11 ?e20))
+(flet ($e82 (= ?e9 (sign_extend[10] ?e8)))
+(flet ($e83 (= v0 (zero_extend[15] ?e18)))
+(flet ($e84 (= ?e17 ?e12))
+(flet ($e85 (= (zero_extend[4] ?e18) v3))
+(flet ($e86 (= v1 (sign_extend[1] ?e5)))
+(flet ($e87 (= ?e14 ?e5))
+(flet ($e88 (= ?e13 (zero_extend[15] ?e14)))
+(flet ($e89 (= ?e19 ?e16))
+(flet ($e90 (= ?e20 ?e17))
+(flet ($e91 (= ?e15 v2))
+(flet ($e92 (or $e72 $e38))
+(flet ($e93 (if_then_else $e58 $e65 $e60))
+(flet ($e94 (not $e71))
+(flet ($e95 (and $e75 $e63))
+(flet ($e96 (and $e82 $e53))
+(flet ($e97 (iff $e22 $e59))
+(flet ($e98 (if_then_else $e96 $e41 $e29))
+(flet ($e99 (not $e46))
+(flet ($e100 (not $e39))
+(flet ($e101 (not $e62))
+(flet ($e102 (iff $e91 $e83))
+(flet ($e103 (implies $e51 $e61))
+(flet ($e104 (not $e33))
+(flet ($e105 (xor $e84 $e45))
+(flet ($e106 (implies $e54 $e50))
+(flet ($e107 (iff $e40 $e57))
+(flet ($e108 (xor $e30 $e89))
+(flet ($e109 (implies $e68 $e103))
+(flet ($e110 (if_then_else $e101 $e52 $e99))
+(flet ($e111 (or $e80 $e110))
+(flet ($e112 (iff $e108 $e88))
+(flet ($e113 (xor $e86 $e78))
+(flet ($e114 (not $e48))
+(flet ($e115 (if_then_else $e67 $e92 $e49))
+(flet ($e116 (implies $e77 $e93))
+(flet ($e117 (and $e26 $e25))
+(flet ($e118 (or $e47 $e117))
+(flet ($e119 (or $e87 $e21))
+(flet ($e120 (not $e64))
+(flet ($e121 (not $e119))
+(flet ($e122 (and $e106 $e118))
+(flet ($e123 (or $e114 $e43))
+(flet ($e124 (implies $e100 $e74))
+(flet ($e125 (iff $e123 $e109))
+(flet ($e126 (iff $e23 $e37))
+(flet ($e127 (not $e121))
+(flet ($e128 (and $e70 $e98))
+(flet ($e129 (if_then_else $e76 $e90 $e122))
+(flet ($e130 (iff $e81 $e111))
+(flet ($e131 (implies $e24 $e24))
+(flet ($e132 (iff $e130 $e42))
+(flet ($e133 (if_then_else $e79 $e34 $e94))
+(flet ($e134 (implies $e102 $e56))
+(flet ($e135 (or $e66 $e27))
+(flet ($e136 (and $e131 $e55))
+(flet ($e137 (iff $e105 $e120))
+(flet ($e138 (if_then_else $e129 $e85 $e32))
+(flet ($e139 (xor $e44 $e132))
+(flet ($e140 (xor $e133 $e139))
+(flet ($e141 (and $e134 $e128))
+(flet ($e142 (or $e127 $e113))
+(flet ($e143 (implies $e136 $e136))
+(flet ($e144 (iff $e143 $e36))
+(flet ($e145 (not $e144))
+(flet ($e146 (if_then_else $e35 $e137 $e142))
+(flet ($e147 (if_then_else $e116 $e126 $e112))
+(flet ($e148 (and $e141 $e97))
+(flet ($e149 (implies $e146 $e115))
+(flet ($e150 (not $e140))
+(flet ($e151 (and $e150 $e95))
+(flet ($e152 (if_then_else $e147 $e138 $e147))
+(flet ($e153 (or $e135 $e31))
+(flet ($e154 (iff $e148 $e73))
+(flet ($e155 (or $e152 $e69))
+(flet ($e156 (not $e107))
+(flet ($e157 (if_then_else $e149 $e28 $e104))
+(flet ($e158 (iff $e157 $e124))
+(flet ($e159 (iff $e125 $e151))
+(flet ($e160 (if_then_else $e154 $e159 $e145))
+(flet ($e161 (iff $e155 $e155))
+(flet ($e162 (iff $e160 $e160))
+(flet ($e163 (iff $e158 $e156))
+(flet ($e164 (iff $e162 $e162))
+(flet ($e165 (and $e163 $e161))
+(flet ($e166 (xor $e164 $e165))
+(flet ($e167 (or $e166 $e166))
+(flet ($e168 (or $e167 $e167))
+(flet ($e169 (iff $e153 $e153))
+(flet ($e170 (or $e168 $e168))
+(flet ($e171 (or $e169 $e169))
+(flet ($e172 (not $e171))
+(flet ($e173 (implies $e170 $e170))
+(flet ($e174 (not $e172))
+(flet ($e175 (iff $e173 $e174))
+$e175
+))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback