From: makaimann Date: Mon, 10 Dec 2018 16:37:11 +0000 (-0800) Subject: BoolToBV modes (off, ite, all) (#2530) X-Git-Tag: cvc5-1.0.0~4330 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e1dc39321cd4ab29b436025badfb05714f5649b3;p=cvc5.git BoolToBV modes (off, ite, all) (#2530) --- diff --git a/src/options/CMakeLists.txt b/src/options/CMakeLists.txt index c711567ab..b86db8d00 100644 --- a/src/options/CMakeLists.txt +++ b/src/options/CMakeLists.txt @@ -9,6 +9,8 @@ libcvc4_add_sources( arith_unate_lemma_mode.cpp arith_unate_lemma_mode.h base_handlers.h + bool_to_bv_mode.cpp + bool_to_bv_mode.h bv_bitblast_mode.cpp bv_bitblast_mode.h datatypes_modes.h diff --git a/src/options/bool_to_bv_mode.cpp b/src/options/bool_to_bv_mode.cpp new file mode 100644 index 000000000..670e15419 --- /dev/null +++ b/src/options/bool_to_bv_mode.cpp @@ -0,0 +1,42 @@ +/********************* */ +/*! \file bool_to_bv_mode.cpp +** \verbatim +** Top contributors (to current version): +** Makai Mann +** 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 Modes for bool-to-bv preprocessing pass +** +** Modes for bool-to-bv preprocessing pass which tries to lower booleans +** to bit-vectors of width 1 at various levels of aggressiveness. +**/ + +#include "options/bool_to_bv_mode.h" + +#include + + +namespace CVC4 +{ + std::ostream& operator<<(std::ostream& out, preprocessing::passes::BoolToBVMode mode) { + switch(mode) { + case preprocessing::passes::BOOL_TO_BV_OFF: + out << "BOOL_TO_BV_OFF"; + break; + case preprocessing::passes::BOOL_TO_BV_ITE: + out << "BOOL_TO_BV_ITE"; + break; + case preprocessing::passes::BOOL_TO_BV_ALL: + out << "BOOL_TO_BV_ALL"; + break; + default: + out << "BoolToBVMode:UNKNOWN![" << unsigned(mode) << "]"; + } + + return out; + } +} // namespace CVC4 diff --git a/src/options/bool_to_bv_mode.h b/src/options/bool_to_bv_mode.h new file mode 100644 index 000000000..f2911c339 --- /dev/null +++ b/src/options/bool_to_bv_mode.h @@ -0,0 +1,57 @@ +/********************* */ +/*! \file bool_to_bv_mode.h +** \verbatim +** Top contributors (to current version): +** Makai Mann +** 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 Modes for bool-to-bv preprocessing pass +** +** Modes for bool-to-bv preprocessing pass which tries to lower booleans +** to bit-vectors of width 1 at various levels of aggressiveness. +**/ + +#include "cvc4_private.h" + +#ifndef __CVC4__PREPROCESSING__PASSES__BOOL_TO_BV_MODE_H +#define __CVC4__PREPROCESSING__PASSES__BOOL_TO_BV_MODE_H + +#include + +namespace CVC4 { +namespace preprocessing { +namespace passes { + +/** Enumeration of bool-to-bv modes */ +enum BoolToBVMode +{ + /** + * No bool-to-bv pass + */ + BOOL_TO_BV_OFF, + + /** + * Only lower bools in condition of ITEs + * Tries to give more info to bit-vector solver + * by using bit-vector-ITEs when possible + */ + BOOL_TO_BV_ITE, + + /** + * Lower every bool beneath the top layer to be a + * bit-vector + */ + BOOL_TO_BV_ALL +}; +} +} + +std::ostream& operator<<(std::ostream& out, preprocessing::passes::BoolToBVMode mode); + +} + +#endif /* __CVC4__PREPROCESSING__PASSES__BOOL_TO_BV_MODE_H */ diff --git a/src/options/bv_options.toml b/src/options/bv_options.toml index 15a9047c7..00290da7d 100644 --- a/src/options/bv_options.toml +++ b/src/options/bv_options.toml @@ -105,11 +105,22 @@ header = "options/bv_options.h" [[option]] name = "boolToBitvector" + smt_name = "bool-to-bv" category = "regular" - long = "bool-to-bv" + long = "bool-to-bv=MODE" + type = "CVC4::preprocessing::passes::BoolToBVMode" + default = "CVC4::preprocessing::passes::BOOL_TO_BV_OFF" + handler = "stringToBoolToBVMode" + includes = ["options/bool_to_bv_mode.h"] + help = "convert booleans to bit-vectors of size 1 at various levels of aggressiveness, see --bool-to-bv=help" + +[[option]] + name = "bitwiseEq" + category = "regular" + long = "bitwise-eq" type = "bool" - default = "false" - help = "convert booleans to bit-vectors of size 1 when possible" + default = "true" + help = "lift equivalence with one-bit bit-vectors to be boolean operations" [[option]] name = "bitvectorDivByZeroConst" diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index a808ecd3c..420396452 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -1301,6 +1301,50 @@ theory::bv::BvSlicerMode OptionsHandler::stringToBvSlicerMode( } } +const std::string OptionsHandler::s_boolToBVModeHelp = + "\ +BoolToBV pass modes supported by the --bool-to-bv option:\n\ +\n\ +off (default)\n\ ++ Don't push any booleans to width one bit-vectors\n\ +\n\ +ite\n\ ++ Try to turn ITEs into BITVECTOR_ITE when possible. It can fail per-formula \n\ + if not all sub-formulas can be turned to bit-vectors\n\ +\n\ +all\n\ ++ Force all booleans to be bit-vectors of width one except at the top level.\n\ + Most aggressive mode\n\ +"; + +preprocessing::passes::BoolToBVMode OptionsHandler::stringToBoolToBVMode( + std::string option, std::string optarg) +{ + if (optarg == "off") + { + return preprocessing::passes::BOOL_TO_BV_OFF; + } + else if (optarg == "ite") + { + return preprocessing::passes::BOOL_TO_BV_ITE; + } + else if (optarg == "all") + { + return preprocessing::passes::BOOL_TO_BV_ALL; + } + else if (optarg == "help") + { + puts(s_boolToBVModeHelp.c_str()); + exit(1); + } + else + { + throw OptionException(std::string("unknown option for --bool-to-bv: `") + + optarg + + "'. Try --bool-to-bv=help"); + } +} + void OptionsHandler::setBitblastAig(std::string option, bool arg) { if(arg) { diff --git a/src/options/options_handler.h b/src/options/options_handler.h index 53e317895..f96632696 100644 --- a/src/options/options_handler.h +++ b/src/options/options_handler.h @@ -27,6 +27,7 @@ #include "options/arith_propagation_mode.h" #include "options/arith_unate_lemma_mode.h" #include "options/base_handlers.h" +#include "options/bool_to_bv_mode.h" #include "options/bv_bitblast_mode.h" #include "options/datatypes_modes.h" #include "options/decision_mode.h" @@ -137,6 +138,8 @@ public: std::string optarg); theory::bv::BvSlicerMode stringToBvSlicerMode(std::string option, std::string optarg); + preprocessing::passes::BoolToBVMode stringToBoolToBVMode(std::string option, + std::string optarg); void setBitblastAig(std::string option, bool arg); theory::bv::SatSolverMode stringToSatSolver(std::string option, @@ -229,6 +232,7 @@ public: static const std::string s_bvSatSolverHelp; static const std::string s_booleanTermConversionModeHelp; static const std::string s_bvSlicerModeHelp; + static const std::string s_boolToBVModeHelp; static const std::string s_cegqiFairModeHelp; static const std::string s_decisionModeHelp; static const std::string s_instFormatHelp ; diff --git a/src/preprocessing/passes/bool_to_bv.cpp b/src/preprocessing/passes/bool_to_bv.cpp index c8a59bdc4..252ab941c 100644 --- a/src/preprocessing/passes/bool_to_bv.cpp +++ b/src/preprocessing/passes/bool_to_bv.cpp @@ -9,17 +9,17 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief The BoolToBv preprocessing pass + ** \brief The BoolToBV preprocessing pass ** **/ #include "preprocessing/passes/bool_to_bv.h" #include -#include -#include +#include "base/map_util.h" #include "expr/node.h" +#include "options/bv_options.h" #include "smt/smt_statistics_registry.h" #include "theory/rewriter.h" #include "theory/theory.h" @@ -30,183 +30,253 @@ 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(){}; + : PreprocessingPass(preprocContext, "bool-to-bv"), 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) + + unsigned size = assertionsToPreprocess->size(); + for (unsigned i = 0; i < size; ++i) { - assertionsToPreprocess->replace(i, Rewriter::rewrite(new_assertions[i])); + assertionsToPreprocess->replace( + i, Rewriter::rewrite(lowerAssertion((*assertionsToPreprocess)[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; + return PreprocessingPassResult::NO_CONFLICT; } -Node BoolToBV::getLowerCache(TNode term) const +Node BoolToBV::fromCache(TNode n) const { - Assert(hasLowerCache(term)); - return d_lowerCache.find(term)->second; + if (d_lowerCache.find(n) != d_lowerCache.end()) + { + return d_lowerCache.find(n)->second; + } + return n; } -bool BoolToBV::hasLowerCache(TNode term) const +bool BoolToBV::needToRebuild(TNode n) const { - return d_lowerCache.find(term) != d_lowerCache.end(); + // check if any children were rebuilt + for (const Node& nn : n) + { + if (ContainsKey(d_lowerCache, nn)) + { + return true; + } + } + return false; } -Node BoolToBV::lowerNode(TNode current, bool topLevel) +Node BoolToBV::lowerAssertion(const TNode& a) { - Node result; + bool optionITE = options::boolToBitvector() == BOOL_TO_BV_ITE; NodeManager* nm = NodeManager::currentNM(); - if (hasLowerCache(current)) - { - result = getLowerCache(current); - } - else + std::vector visit; + visit.push_back(a); + std::unordered_set visited; + // for ite mode, keeps track of whether you're in an ite condition + // for all mode, unused + std::unordered_set ite_cond; + + while (!visit.empty()) { - if (current.getNumChildren() == 0) + TNode n = visit.back(); + visit.pop_back(); + + int numChildren = n.getNumChildren(); + Kind k = n.getKind(); + Debug("bool-to-bv") << "BoolToBV::lowerAssertion Post-traversal with " << n + << " and visited = " << ContainsKey(visited, n) + << std::endl; + + // Mark as visited + /* Optimization: if it's a leaf, don't need to wait to do the work */ + if (!ContainsKey(visited, n) && (numChildren > 0)) { - if (current.getKind() == kind::CONST_BOOLEAN) + visited.insert(n); + visit.push_back(n); + + // insert children in reverse order so that they're processed in order + // important for rewriting which sorts by node id + for (int i = numChildren - 1; i >= 0; --i) { - result = (current == bv::utils::mkTrue()) ? d_one : d_zero; + visit.push_back(n[i]); } - else + + if (optionITE) { - result = current; + // check for ite-conditions + if (k == kind::ITE) + { + ite_cond.insert(n[0]); + } + else if (ContainsKey(ite_cond, n)) + { + // being part of an ite condition is inherited from the parent + ite_cond.insert(n.begin(), n.end()); + } } } + /* Optimization for ite mode */ + else if (optionITE && !ContainsKey(ite_cond, n) && !needToRebuild(n)) + { + Debug("bool-to-bv") + << "BoolToBV::lowerAssertion Skipping because don't need to rebuild: " + << n << std::endl; + // in ite mode, if you've already visited the node but it's not + // in an ite condition and doesn't need to be rebuilt, then + // don't need to do anything + continue; + } else { - Kind kind = current.getKind(); - Kind new_kind = kind; - switch (kind) - { - case kind::EQUAL: - if (current[0].getType().isBitVector() - || current[0].getType().isBoolean()) - { - 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::IMPLIES: new_kind = kind::BITVECTOR_OR; 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) + lowerNode(n); + } + } + + if (fromCache(a).getType().isBitVector()) + { + return nm->mkNode(kind::EQUAL, fromCache(a), bv::utils::mkOne(1)); + } + else + { + Assert(a == fromCache(a)); + return a; + } +} + +void BoolToBV::lowerNode(const TNode& n) +{ + NodeManager* nm = NodeManager::currentNM(); + Kind k = n.getKind(); + + bool all_bv = true; + // check if it was able to convert all children to bitvectors + for (const Node& nn : n) + { + all_bv = all_bv && fromCache(nn).getType().isBitVector(); + if (!all_bv) + { + break; + } + } + + if (!all_bv || (n.getNumChildren() == 0)) + { + if ((options::boolToBitvector() == BOOL_TO_BV_ALL) + && n.getType().isBoolean()) + { + if (k == kind::CONST_BOOLEAN) { - // 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 if (kind == kind::IMPLIES) { - // Special-case IMPLIES because needs to be rewritten. - converted = lowerNode(current[0]); - builder << nm->mkNode(kind::BITVECTOR_NOT, converted); - converted = lowerNode(current[1]); - builder << converted; + d_lowerCache[n] = (n == bv::utils::mkTrue()) ? bv::utils::mkOne(1) + : bv::utils::mkZero(1); } else { - for (unsigned i = 0; i < current.getNumChildren(); ++i) - { - converted = lowerNode(current[i]); - builder << converted; - } + d_lowerCache[n] = + nm->mkNode(kind::ITE, n, bv::utils::mkOne(1), bv::utils::mkZero(1)); } - result = builder; + + Debug("bool-to-bv") << "BoolToBV::lowerNode " << n << " =>\n" + << fromCache(n) << std::endl; + ++(d_statistics.d_numTermsForcedLowered); + return; } - if (result.getType().isBoolean()) + else { - ++(d_statistics.d_numTermsForcedLowered); - result = nm->mkNode(kind::ITE, result, d_one, d_zero); + // invariant + // either one of the children is not a bit-vector or bool + // i.e. something that can't be 'forced' to a bitvector + // or it's in 'ite' mode which will give up on bools that + // can't be converted easily + + Debug("bool-to-bv") << "BoolToBV::lowerNode skipping: " << n << std::endl; + return; } - addToLowerCache(current, result); } - if (topLevel) + + Kind new_kind = k; + switch (k) { - result = nm->mkNode(kind::EQUAL, result, d_one); + 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::IMPLIES: new_kind = kind::BITVECTOR_OR; break; + case kind::ITE: 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; } - 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) + NodeBuilder<> builder(new_kind); + if ((options::boolToBitvector() == BOOL_TO_BV_ALL) && (new_kind != k)) + { + ++(d_statistics.d_numTermsLowered); + } + + if (n.getMetaKind() == kind::metakind::PARAMETERIZED) + { + builder << n.getOperator(); + } + + // special case IMPLIES because needs to be rewritten + if (k == kind::IMPLIES) + { + builder << nm->mkNode(kind::BITVECTOR_NOT, fromCache(n[0])); + builder << fromCache(n[1]); + } + else { - Node new_assertion = lowerNode(assertions[i], true); - new_assertions.push_back(new_assertion); - Trace("bool-to-bv") << " " << assertions[i] << " => " << new_assertions[i] - << "\n"; + for (const Node& nn : n) + { + builder << fromCache(nn); + } } + + Debug("bool-to-bv") << "BoolToBV::lowerNode " << n << " =>\n" + << builder << std::endl; + + d_lowerCache[n] = builder.constructNode(); } BoolToBV::Statistics::Statistics() - : d_numTermsLowered("preprocessing::passes::BoolToBV::NumTermsLowered", 0), - d_numAtomsLowered("preprocessing::passes::BoolToBV::NumAtomsLowered", 0), + : d_numIteToBvite("preprocessing::passes::BoolToBV::NumIteToBvite", 0), + d_numTermsLowered("preprocessing::passes:BoolToBV::NumTermsLowered", 0), d_numTermsForcedLowered( "preprocessing::passes::BoolToBV::NumTermsForcedLowered", 0) { - smtStatisticsRegistry()->registerStat(&d_numTermsLowered); - smtStatisticsRegistry()->registerStat(&d_numAtomsLowered); - smtStatisticsRegistry()->registerStat(&d_numTermsForcedLowered); + smtStatisticsRegistry()->registerStat(&d_numIteToBvite); + if (options::boolToBitvector() == BOOL_TO_BV_ALL) + { + // these statistics wouldn't be correct in the ITE mode, + // because it might discard rebuilt nodes if it fails to + // convert a bool to width-one bit-vector (never forces) + smtStatisticsRegistry()->registerStat(&d_numTermsLowered); + smtStatisticsRegistry()->registerStat(&d_numTermsForcedLowered); + } } BoolToBV::Statistics::~Statistics() { - smtStatisticsRegistry()->unregisterStat(&d_numTermsLowered); - smtStatisticsRegistry()->unregisterStat(&d_numAtomsLowered); - smtStatisticsRegistry()->unregisterStat(&d_numTermsForcedLowered); + smtStatisticsRegistry()->unregisterStat(&d_numIteToBvite); + if (options::boolToBitvector() == BOOL_TO_BV_ALL) + { + smtStatisticsRegistry()->unregisterStat(&d_numTermsLowered); + smtStatisticsRegistry()->unregisterStat(&d_numTermsForcedLowered); + } } diff --git a/src/preprocessing/passes/bool_to_bv.h b/src/preprocessing/passes/bool_to_bv.h index 49c9dc944..da99d3c84 100644 --- a/src/preprocessing/passes/bool_to_bv.h +++ b/src/preprocessing/passes/bool_to_bv.h @@ -2,14 +2,14 @@ /*! \file bool_to_bv.h ** \verbatim ** Top contributors (to current version): - ** Yoni Zohar + ** Makai Mann, Yoni Zohar ** 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 + ** \brief The BoolToBV preprocessing pass ** **/ @@ -18,9 +18,9 @@ #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 "theory/bv/theory_bv_utils.h" #include "util/statistics_registry.h" namespace CVC4 { @@ -39,24 +39,33 @@ class BoolToBV : public PreprocessingPass private: struct Statistics { + IntStat d_numIteToBvite; 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); - NodeNodeMap d_lowerCache; - Node d_one; - Node d_zero; + /* Takes an assertion and tries to create more bit-vector structure */ + Node lowerAssertion(const TNode& a); + + /* Tries to lower one node to a width-one bit-vector */ + void lowerNode(const TNode& n); + + /* Returns cached node if it exists, otherwise returns the node */ + Node fromCache(TNode n) const; + + /** Checks if any of the nodes children were rebuilt, + * in which case n needs to be rebuilt as well + */ + bool needToRebuild(TNode n) const; + Statistics d_statistics; -}; // class + + /* Keeps track of lowered nodes */ + std::unordered_map d_lowerCache; +}; // class BoolToBV + } // namespace passes } // namespace preprocessing } // namespace CVC4 diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 6814ad531..7abfd8273 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1379,17 +1379,17 @@ void SmtEngine::setDefaults() { options::bitvectorToBool.set(false); } - if (options::boolToBitvector()) + if (options::boolToBitvector() != preprocessing::passes::BOOL_TO_BV_OFF) { if (options::boolToBitvector.wasSetByUser()) { throw OptionException( - "bool-to-bv not supported with unsat cores/proofs"); + "bool-to-bv != off not supported with unsat cores/proofs"); } - Notice() << "SmtEngine: turning off bool-to-bitvector to support unsat " + Notice() << "SmtEngine: turning off bool-to-bv to support unsat " "cores/proofs" << endl; - options::boolToBitvector.set(false); + setOption("boolToBitvector", SExpr("off")); } if (options::bvIntroducePow2()) @@ -1449,13 +1449,18 @@ void SmtEngine::setDefaults() { if (options::cbqiBv() && d_logic.isQuantified()) { - if(options::boolToBitvector.wasSetByUser()) { - throw OptionException( - "bool-to-bv not supported with CBQI BV for quantified logics"); + if (options::boolToBitvector() != preprocessing::passes::BOOL_TO_BV_OFF) + { + if (options::boolToBitvector.wasSetByUser()) + { + throw OptionException( + "bool-to-bv != off not supported with CBQI BV for quantified " + "logics"); + } + Notice() << "SmtEngine: turning off bool-to-bitvector to support CBQI BV" + << endl; + setOption("boolToBitvector", SExpr("off")); } - Notice() << "SmtEngine: turning off bool-to-bitvector to support CBQI BV" - << endl; - options::boolToBitvector.set(false); } // cases where we need produce models @@ -1617,6 +1622,19 @@ void SmtEngine::setDefaults() { } } + if (options::boolToBitvector() == preprocessing::passes::BOOL_TO_BV_ALL + && !d_logic.isTheoryEnabled(THEORY_BV)) + { + if (options::boolToBitvector.wasSetByUser()) + { + throw OptionException( + "bool-to-bv=all not supported for non-bitvector logics."); + } + Notice() << "SmtEngine: turning off bool-to-bv for non-bv logic: " + << d_logic.getLogicString() << std::endl; + setOption("boolToBitvector", SExpr("off")); + } + if (! options::bvEagerExplanations.wasSetByUser() && d_logic.isTheoryEnabled(THEORY_ARRAYS) && d_logic.isTheoryEnabled(THEORY_BV)) { diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index e60d60456..949a3d738 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -740,7 +740,7 @@ Node TheoryBV::ppRewrite(TNode t) { Debug("bv-pp-rewrite") << "TheoryBV::ppRewrite " << t << "\n"; Node res = t; - if (RewriteRule::applies(t)) { + if (options::bitwiseEq() && RewriteRule::applies(t)) { Node result = RewriteRule::run(t); res = Rewriter::rewrite(result); } else if (d_isCoreTheory && t.getKind() == kind::EQUAL) { diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index f22796929..9e942aae1 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -159,7 +159,8 @@ set(regress_0_tests regress0/bv/ackermann2.smt2 regress0/bv/ackermann3.smt2 regress0/bv/ackermann4.smt2 - regress0/bv/bool-to-bv.smt2 + regress0/bv/bool-to-bv-all.smt2 + regress0/bv/bool-to-bv-ite.smt2 regress0/bv/bug260a.smt regress0/bv/bug260b.smt regress0/bv/bug440.smt diff --git a/test/regress/regress0/bv/bool-to-bv-all.smt2 b/test/regress/regress0/bv/bool-to-bv-all.smt2 new file mode 100644 index 000000000..5947699d9 --- /dev/null +++ b/test/regress/regress0/bv/bool-to-bv-all.smt2 @@ -0,0 +1,19 @@ +; COMMAND-LINE: --bool-to-bv=all +; EXPECT: sat +(set-logic QF_BV) +(declare-fun x2 () (_ BitVec 3)) +(declare-fun x1 () (_ BitVec 3)) +(declare-fun x0 () (_ BitVec 3)) +(declare-fun b1 () Bool) +(declare-fun b2 () Bool) +(declare-fun b3 () Bool) +(assert (not (bvult (bvudiv (bvudiv (bvudiv x0 x0) x1) x2) x1))) +(assert (not (bvslt (bvudiv (bvudiv (bvudiv x0 x0) x1) x2) x1))) +(assert (= #b000 x2)) +(assert (=> b1 b2)) +(assert (and b1 b2)) +(assert (or b1 b2)) +(assert (xor b1 b3)) +(assert (not (xor b2 b2))) +(assert (ite b2 b2 b1)) +(check-sat) diff --git a/test/regress/regress0/bv/bool-to-bv-ite.smt2 b/test/regress/regress0/bv/bool-to-bv-ite.smt2 new file mode 100644 index 000000000..e1be3ea10 --- /dev/null +++ b/test/regress/regress0/bv/bool-to-bv-ite.smt2 @@ -0,0 +1,13 @@ +; COMMAND-LINE: --bool-to-bv=ite +; EXPECT: sat +(set-logic QF_BV) +(declare-fun x2 () (_ BitVec 3)) +(declare-fun x1 () (_ BitVec 3)) +(declare-fun x0 () (_ BitVec 3)) +(declare-fun b1 () Bool) +(declare-fun b2 () Bool) +(assert (not (bvult (bvudiv (bvudiv (bvudiv x0 x0) x1) x2) x1))) +(assert (= #b000 x2)) +(assert (=> b1 b2)) +(assert (= x2 (ite (bvugt x0 x1) (bvadd x0 (_ bv1 3)) (bvadd x1 (_ bv1 3))))) +(check-sat) diff --git a/test/regress/regress0/bv/bool-to-bv.smt2 b/test/regress/regress0/bv/bool-to-bv.smt2 deleted file mode 100644 index 8706c51a8..000000000 --- a/test/regress/regress0/bv/bool-to-bv.smt2 +++ /dev/null @@ -1,19 +0,0 @@ -; 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)) -(declare-fun b1 () Bool) -(declare-fun b2 () Bool) -(declare-fun b3 () Bool) -(assert (not (bvult (bvudiv (bvudiv (bvudiv x0 x0) x1) x2) x1))) -(assert (not (bvslt (bvudiv (bvudiv (bvudiv x0 x0) x1) x2) x1))) -(assert (= #b000 x2)) -(assert (=> b1 b2)) -(assert (and b1 b2)) -(assert (or b1 b2)) -(assert (xor b1 b3)) -(assert (not (xor b2 b2))) -(assert (ite b2 b2 b1)) -(check-sat)