From a2df47ad560843301ba98c79f1f0fe5d6091c0ae Mon Sep 17 00:00:00 2001 From: yoni206 Date: Wed, 25 Apr 2018 11:54:23 -0700 Subject: [PATCH] Refactor bv-to-bool and bool-to-bv preprocessing passes (#1788) --- src/Makefile.am | 6 +- src/preprocessing/passes/bool_to_bv.cpp | 200 +++++++++ src/preprocessing/passes/bool_to_bv.h | 64 +++ src/preprocessing/passes/bv_to_bool.cpp | 310 ++++++++++++++ .../bv => preprocessing/passes}/bv_to_bool.h | 75 ++-- .../preprocessing_pass_registry.cpp | 5 + .../preprocessing_pass_registry.h | 5 + src/smt/smt_engine.cpp | 45 +- src/theory/bv/bv_to_bool.cpp | 387 ------------------ src/theory/quantifiers/term_util.cpp | 1 + src/theory/theory_engine.cpp | 9 - src/theory/theory_engine.h | 4 - test/regress/Makefile.tests | 2 + test/regress/regress0/bv/bool-to-bv.smt2 | 9 + test/regress/regress0/bv/bv-to-bool.smt | 185 +++++++++ 15 files changed, 837 insertions(+), 470 deletions(-) create mode 100644 src/preprocessing/passes/bool_to_bv.cpp create mode 100644 src/preprocessing/passes/bool_to_bv.h create mode 100644 src/preprocessing/passes/bv_to_bool.cpp rename src/{theory/bv => preprocessing/passes}/bv_to_bool.h (58%) delete mode 100644 src/theory/bv/bv_to_bool.cpp create mode 100644 test/regress/regress0/bv/bool-to-bv.smt2 create mode 100644 test/regress/regress0/bv/bv-to-bool.smt 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 +#include +#include + +#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 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& assertions, + std::vector& 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& assertions, + std::vector& 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 +#include +#include + +#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 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& assertions, + std::vector& 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 similarity index 58% rename from src/theory/bv/bv_to_bool.h rename to 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 +#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 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& assertions, + std::vector& 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& assertions, std::vector& new_assertions); - void lowerBoolToBv(const std::vector& assertions, std::vector& 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( + new BVToBool(d_preprocessingPassContext.get())); + d_preprocessingPassRegistry.registerPass("bv-to-bool", std::move(bvToBool)); + std::unique_ptr boolToBv( + new BoolToBV(d_preprocessingPassContext.get())); + d_preprocessingPassRegistry.registerPass("bool-to-bv", std::move(boolToBv)); } Node SmtEnginePrivate::expandDefinitions(TNode n, unordered_map& 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 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 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& assertions, std::vector& 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& assertions, std::vector& 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& assertions, std::vector& new_assertions) { - d_bvToBoolPreprocessor.liftBvToBool(assertions, new_assertions); -} - -void TheoryEngine::ppBoolToBv(const std::vector& assertions, std::vector& new_assertions) { - d_bvToBoolPreprocessor.lowerBoolToBv(assertions, new_assertions); -} - bool TheoryEngine::ppBvAbstraction(const std::vector& assertions, std::vector& 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& assertions); - void ppBvToBool(const std::vector& assertions, std::vector& new_assertions); - void ppBoolToBv(const std::vector& assertions, std::vector& new_assertions); bool ppBvAbstraction(const std::vector& assertions, std::vector& new_assertions); void mkAckermanizationAssertions(std::vector& 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 +)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) + -- 2.30.2