diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/Makefile.am | 6 | ||||
| -rw-r--r-- | src/preprocessing/passes/bool_to_bv.cpp | 200 | ||||
| -rw-r--r-- | src/preprocessing/passes/bool_to_bv.h | 64 | ||||
| -rw-r--r-- | src/preprocessing/passes/bv_to_bool.cpp | 310 | ||||
| -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.cpp | 5 | ||||
| -rw-r--r-- | src/preprocessing/preprocessing_pass_registry.h | 5 | ||||
| -rw-r--r-- | src/smt/smt_engine.cpp | 45 | ||||
| -rw-r--r-- | src/theory/bv/bv_to_bool.cpp | 387 | ||||
| -rw-r--r-- | src/theory/quantifiers/term_util.cpp | 1 | ||||
| -rw-r--r-- | src/theory/theory_engine.cpp | 9 | ||||
| -rw-r--r-- | src/theory/theory_engine.h | 4 |
12 files changed, 641 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); |