diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/prop/minisat/core/Solver.h | 3 | ||||
-rw-r--r-- | src/prop/minisat/simp/SimpSolver.cc | 4 | ||||
-rw-r--r-- | src/prop/options | 3 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 24 | ||||
-rw-r--r-- | src/theory/bv/Makefile.am | 4 | ||||
-rw-r--r-- | src/theory/bv/bv_to_bool.cpp | 305 | ||||
-rw-r--r-- | src/theory/bv/bv_to_bool.h | 79 | ||||
-rw-r--r-- | src/theory/bv/options | 3 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.cpp | 9 | ||||
-rw-r--r-- | src/theory/term_registration_visitor.h | 6 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 7 | ||||
-rw-r--r-- | src/theory/theory_engine.h | 4 |
12 files changed, 443 insertions, 8 deletions
diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h index 9338f9b55..55780479a 100644 --- a/src/prop/minisat/core/Solver.h +++ b/src/prop/minisat/core/Solver.h @@ -173,6 +173,7 @@ public: bool solve (Lit p, Lit q, Lit r); // Search for a model that respects three assumptions. bool okay () const; // FALSE means solver is in a conflicting state + void toDimacs (); void toDimacs (FILE* f, const vec<Lit>& assumps); // Write CNF to file in DIMACS-format. void toDimacs (const char *file, const vec<Lit>& assumps); void toDimacs (FILE* f, Clause& c, vec<Var>& map, Var& max); @@ -539,12 +540,14 @@ inline bool Solver::solve (const vec<Lit>& assumps){ budgetOff(); as inline lbool Solver::solveLimited (const vec<Lit>& assumps){ assumps.copyTo(assumptions); return solve_(); } inline bool Solver::okay () const { return ok; } +inline void Solver::toDimacs () { vec<Lit> as; toDimacs(stdout, as); } inline void Solver::toDimacs (const char* file){ vec<Lit> as; toDimacs(file, as); } inline void Solver::toDimacs (const char* file, Lit p){ vec<Lit> as; as.push(p); toDimacs(file, as); } inline void Solver::toDimacs (const char* file, Lit p, Lit q){ vec<Lit> as; as.push(p); as.push(q); toDimacs(file, as); } inline void Solver::toDimacs (const char* file, Lit p, Lit q, Lit r){ vec<Lit> as; as.push(p); as.push(q); as.push(r); toDimacs(file, as); } + //================================================================================================= // Debug etc: diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc index 9c3e59954..0e0e5d3ae 100644 --- a/src/prop/minisat/simp/SimpSolver.cc +++ b/src/prop/minisat/simp/SimpSolver.cc @@ -113,6 +113,10 @@ Var SimpSolver::newVar(bool sign, bool dvar, bool isTheoryAtom, bool preRegister lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp) { + if (options::minisatDumpDimacs()) { + toDimacs(); + return l_Undef; + } popTrail(); vec<Var> extra_frozen; diff --git a/src/prop/options b/src/prop/options index cda99538c..e3a0f814a 100644 --- a/src/prop/options +++ b/src/prop/options @@ -28,4 +28,7 @@ option sat_refine_conflicts --refine-conflicts bool option minisatUseElim --minisat-elimination bool :default true :read-write use Minisat elimination +option minisatDumpDimacs --minisat-dump-dimacs bool :default false + instead of solving minisat dumps the asserted clauses in Dimacs format + endmodule diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 864b444df..0d9d63d91 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -349,7 +349,9 @@ private: */ bool checkForBadSkolems(TNode n, TNode skolem, hash_map<Node, bool, NodeHashFunction>& cache); - + // Lift bit-vectors of size 1 to booleans + void bvToBool(); + // Simplify ITE structure void simpITE(); @@ -1925,6 +1927,15 @@ bool SmtEnginePrivate::nonClausalSimplify() { } +void SmtEnginePrivate::bvToBool() { + Trace("bv-to-bool") << "SmtEnginePrivate::bvToBool()" << endl; + std::vector<Node> new_assertions; + d_smt.d_theoryEngine->ppBvToBool(d_assertionsToCheck, new_assertions); + for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) { + d_assertionsToCheck[i] = Rewriter::rewrite(new_assertions[i]); + } +} + void SmtEnginePrivate::simpITE() { TimerStat::CodeTimer simpITETimer(d_smt.d_stats->d_simpITETime); @@ -2772,6 +2783,17 @@ void SmtEnginePrivate::processAssertions() { } dumpAssertions("post-static-learning", d_assertionsToCheck); + // Lift bit-vectors of size 1 to bool + if(options::bvToBool()) { + Chat() << "...doing bvToBool..." << endl; + bvToBool(); + } + + Trace("smt") << "POST bvToBool" << endl; + Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl; + Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl; + + dumpAssertions("pre-ite-removal", d_assertionsToCheck); { Chat() << "removing term ITEs..." << endl; diff --git a/src/theory/bv/Makefile.am b/src/theory/bv/Makefile.am index a70521791..8651f280b 100644 --- a/src/theory/bv/Makefile.am +++ b/src/theory/bv/Makefile.am @@ -12,6 +12,8 @@ libbv_la_SOURCES = \ type_enumerator.h \ bitblaster.h \ bitblaster.cpp \ + bv_to_bool.h \ + bv_to_bool.cpp \ bv_subtheory.h \ bv_subtheory_core.h \ bv_subtheory_core.cpp \ @@ -36,7 +38,7 @@ libbv_la_SOURCES = \ theory_bv_type_rules.h \ theory_bv_rewriter.h \ theory_bv_rewriter.cpp \ - cd_set_collection.h + cd_set_collection.h EXTRA_DIST = \ kinds diff --git a/src/theory/bv/bv_to_bool.cpp b/src/theory/bv/bv_to_bool.cpp new file mode 100644 index 000000000..8084a7282 --- /dev/null +++ b/src/theory/bv/bv_to_bool.cpp @@ -0,0 +1,305 @@ +/********************* */ +/*! \file bv_to_bool.h + ** \verbatim + ** Original author: Liana Hadarean + ** Major contributors: None. + ** Minor contributors (to current version): None. + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** 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 "util/node_visitor.h" +#include "theory/bv/bv_to_bool.h" + +using namespace std; +using namespace CVC4; +using namespace CVC4::theory; +using namespace CVC4::theory::bv; + +void BvToBoolVisitor::addToCache(TNode term, Node new_term) { + Assert (new_term != Node()); + Assert (!hasCache(term)); + d_cache[term] = new_term; +} + +Node BvToBoolVisitor::getCache(TNode term) const { + if (!hasCache(term) || term.getKind() == kind::CONST_BITVECTOR) { + return term; + } + return d_cache.find(term)->second; +} + +bool BvToBoolVisitor::hasCache(TNode term) const { + return d_cache.find(term) != d_cache.end(); +} + +void BvToBoolVisitor::start(TNode node) {} + +void BvToBoolVisitor::storeBvToBool(TNode bv_term, TNode bool_term) { + Assert (bv_term.getType().isBitVector() && + bv_term.getType().getBitVectorSize() == 1); + Assert (bool_term.getType().isBoolean() && d_bvToBoolMap.find(bv_term) == d_bvToBoolMap.end()); + d_bvToBoolMap[bv_term] = bool_term; +} + +Node BvToBoolVisitor::getBoolForBvTerm(TNode node) { + Assert (d_bvToBoolMap.find(node) != d_bvToBoolMap.end()); + return d_bvToBoolMap[node]; +} + +bool BvToBoolVisitor::alreadyVisited(TNode current, TNode parent) { + return d_cache.find(current) != d_cache.end(); +} + +bool BvToBoolVisitor::isConvertibleBvAtom(TNode node) { + Kind kind = node.getKind(); + return (kind == kind::BITVECTOR_ULT || + kind == kind::BITVECTOR_ULE || + kind == kind::BITVECTOR_SLT || + kind == kind::BITVECTOR_SLE || + kind == kind::EQUAL) && + isConvertibleBvTerm(node[0]) && + isConvertibleBvTerm(node[1]); +} + +bool BvToBoolVisitor::isConvertibleBvTerm(TNode node) { + // we have already converted it and the result is cached + if (d_bvToBoolMap.find(node) != d_bvToBoolMap.end()) { + return true; + } + + Kind kind = node.getKind(); + if (!node.getType().isBitVector() || node.getType().getBitVectorSize() != 1) + return false; + + if (kind == kind::CONST_BITVECTOR) { + return true; + } + + if (kind == kind::ITE) { + return isConvertibleBvTerm(node[1]) && isConvertibleBvTerm(node[2]); + } + + if (kind == kind::BITVECTOR_AND || kind == kind::BITVECTOR_OR || + kind == kind::BITVECTOR_NOT || kind == kind::BITVECTOR_XOR) { + for (unsigned i = 0; i < node.getNumChildren(); ++i) { + if (!isConvertibleBvTerm(node[i])) + return false; + } + return true; + } + return false; +} + +Node BvToBoolVisitor::convertBvAtom(TNode node) { + Assert (node.getType().isBoolean()); + Kind kind = node.getKind(); + Node result; + switch(kind) { + case kind::BITVECTOR_ULT: { + Node a = getBoolForBvTerm(node[0]); + Node b = getBoolForBvTerm(node[1]); + Node a_eq_0 = utils::mkNode(kind::IFF, a, utils::mkFalse()); + Node b_eq_1 = utils::mkNode(kind::IFF, b, utils::mkTrue()); + result = utils::mkNode(kind::AND, a_eq_0, b_eq_1); + break; + } + case kind::BITVECTOR_ULE: { + Node a = getBoolForBvTerm(node[0]); + Node b = getBoolForBvTerm(node[1]); + Node a_eq_0 = utils::mkNode(kind::IFF, a, utils::mkFalse()); + Node b_eq_1 = utils::mkNode(kind::IFF, b, utils::mkTrue()); + Node a_lt_b = utils::mkNode(kind::AND, a_eq_0, b_eq_1); + Node a_eq_b = utils::mkNode(kind::IFF, a, b); + result = utils::mkNode(kind::OR, a_lt_b, a_eq_b); + break; + } + case kind::BITVECTOR_SLT: { + Node a = getBoolForBvTerm(node[0]); + Node b = getBoolForBvTerm(node[1]); + Node a_eq_1 = utils::mkNode(kind::IFF, a, utils::mkTrue()); + Node b_eq_0 = utils::mkNode(kind::IFF, b, utils::mkFalse()); + result = utils::mkNode(kind::AND, a_eq_1, b_eq_0); + break; + } + case kind::BITVECTOR_SLE: { + Node a = getBoolForBvTerm(node[0]); + Node b = getBoolForBvTerm(node[1]); + Node a_eq_1 = utils::mkNode(kind::IFF, a, utils::mkTrue()); + Node b_eq_0 = utils::mkNode(kind::IFF, b, utils::mkFalse()); + Node a_slt_b = utils::mkNode(kind::AND, a_eq_1, b_eq_0); + Node a_eq_b = utils::mkNode(kind::IFF, a, b); + result = utils::mkNode(kind::OR, a_slt_b, a_eq_b); + break; + } + case kind::EQUAL: { + Node a = getBoolForBvTerm(node[0]); + Node b = getBoolForBvTerm(node[1]); + result = utils::mkNode(kind::IFF, a, b); + break; + } + default: + Unhandled(); + } + Debug("bv-to-bool") << "BvToBoolVisitor::convertBvAtom " << node <<" => " << result << "\n"; + Assert (result != Node()); + return result; +} + +Node BvToBoolVisitor::convertBvTerm(TNode node) { + Assert (node.getType().isBitVector() && + node.getType().getBitVectorSize() == 1); + Kind kind = node.getKind(); + + if (node.getNumChildren() == 0) { + if (node.getKind() == kind::VARIABLE) { + return getBoolForBvTerm(node); + } + if (node.getKind() == kind::CONST_BITVECTOR) { + Node result = node == d_one ? utils::mkTrue() : utils::mkFalse(); + storeBvToBool(node, result); + return result; + } + } + + if (kind == kind::ITE) { + Node cond = getCache(node[0]); + Node true_branch = getBoolForBvTerm(node[1]); + Node false_branch = getBoolForBvTerm(node[2]); + Node result = utils::mkNode(kind::ITE, cond, true_branch, false_branch); + storeBvToBool(node, result); + Debug("bv-to-bool") << "BvToBoolVisitor::convertBvTerm " << node <<" => " << result << "\n"; + return result; + } + + Kind new_kind; + 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 << getBoolForBvTerm(node[i]); + } + Node result = builder; + storeBvToBool(node, result); + Debug("bv-to-bool") << "BvToBoolVisitor::convertBvTerm " << node <<" => " << result << "\n"; + return result; +} + +void BvToBoolVisitor::check(TNode current, TNode parent) { + if (d_bvToBoolMap.find(current) != d_bvToBoolMap.end()) { + if (!isConvertibleBvTerm(parent) && !isConvertibleBvAtom(parent)) { + Debug("bv-to-bool") << "BvToBoolVisitor::check " << current << " in non boolean context: \n" + << " " << parent << "\n"; + } + } +} + +void BvToBoolVisitor::visit(TNode current, TNode parent) { + Debug("bv-to-bool") << "BvToBoolVisitor visit (" << current << ", " << parent << ")\n"; + Assert (!alreadyVisited(current, parent) && + !hasCache(current)); + + Node result; + // make sure that the bv terms we are replacing to not occur in other contexts + check(current, parent); + + if (isConvertibleBvAtom(current)) { + result = convertBvAtom(current); + } else if (isConvertibleBvTerm(current)) { + result = convertBvTerm(current); + } 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 = getCache(current[i]); + Assert (converted.getType() == current[i].getType()); + builder << converted; + } + result = builder; + } + } + Assert (result != Node()); + Debug("bv-to-bool") << " =>" << result <<"\n"; + addToCache(current, result); +} + + +BvToBoolVisitor::return_type BvToBoolVisitor::done(TNode node) { + Assert (hasCache(node)); + Node result = getCache(node); + return result; +} + +bool BvToBoolVisitor::hasBoolTerm(TNode node) { + return d_bvToBoolMap.find(node) != d_bvToBoolMap.end(); +} + +bool BvToBoolPreprocessor::matchesBooleanPatern(TNode current) { + // we are looking for something of the type (= (bvvar 1) (some predicate)) + if (current.getKind() == kind::IFF && + current[0].getKind() == kind::EQUAL && + current[0][0].getType().isBitVector() && + current[0][0].getType().getBitVectorSize() == 1 && + current[0][0].getKind() == kind::VARIABLE && + current[0][1].getKind() == kind::CONST_BITVECTOR) { + return true; + } + return false; +} + + +void BvToBoolPreprocessor::liftBoolToBV(const std::vector<Node>& assertions, std::vector<Node>& new_assertions) { + BvToBoolVisitor bvToBoolVisitor; + + for (unsigned i = 0; i < assertions.size(); ++i) { + if (matchesBooleanPatern(assertions[i])) { + TNode assertion = assertions[i]; + TNode bv_var = assertion[0][0]; + Assert (bv_var.getKind() == kind::VARIABLE && + bv_var.getType().isBitVector() && + bv_var.getType().getBitVectorSize() == 1); + Node bool_cond = NodeVisitor<BvToBoolVisitor>::run(bvToBoolVisitor, assertion[1]); + Assert (bool_cond.getType().isBoolean()); + if (!bvToBoolVisitor.hasBoolTerm(bv_var)) { + Debug("bv-to-bool") << "BBvToBoolPreprocessor::liftBvToBoolBV candidate: " << bv_var <<"\n"; + bvToBoolVisitor.storeBvToBool(bv_var, bool_cond); + } else { + Debug("bv-to-bool") << "BvToBoolPreprocessor::liftBvToBoolBV multiple def " << bv_var <<"\n"; + } + } + } + + for (unsigned i = 0; i < assertions.size(); ++i) { + Node new_assertion = NodeVisitor<BvToBoolVisitor>::run(bvToBoolVisitor, + assertions[i]); + new_assertions.push_back(new_assertion); + Trace("bv-to-bool") << " " << assertions[i] <<" => " << new_assertions[i] <<"\n"; + } +} diff --git a/src/theory/bv/bv_to_bool.h b/src/theory/bv/bv_to_bool.h new file mode 100644 index 000000000..186f2b317 --- /dev/null +++ b/src/theory/bv/bv_to_bool.h @@ -0,0 +1,79 @@ +/********************* */ +/*! \file bv_to_bool.h + ** \verbatim + ** Original author: Liana Hadarean + ** Major contributors: None. + ** Minor contributors (to current version): None. + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** 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 "cvc4_private.h" +#include "theory/bv/theory_bv_utils.h" + +#ifndef __CVC4__THEORY__BV__BV_TO_BOOL_H +#define __CVC4__THEORY__BV__BV_TO_BOOL_H + +namespace CVC4 { +namespace theory { +namespace bv { + +typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet; +typedef __gnu_cxx::hash_map<Node, Node, TNodeHashFunction> NodeNodeMap; + +class BvToBoolVisitor { + NodeNodeMap d_bvToBoolMap; + NodeNodeMap d_cache; + Node d_one; + Node d_zero; + + void addToCache(TNode term, Node new_term); + Node getCache(TNode term) const; + bool hasCache(TNode term) const; + + bool isConvertibleBvTerm(TNode node); + bool isConvertibleBvAtom(TNode node); + Node getBoolForBvTerm(TNode node); + Node convertBvAtom(TNode node); + Node convertBvTerm(TNode node); + void check(TNode current, TNode parent); +public: + typedef Node return_type; + BvToBoolVisitor() + : d_bvToBoolMap(), + d_cache(), + d_one(utils::mkConst(BitVector(1, 1u))), + d_zero(utils::mkConst(BitVector(1, 0u))) + {} + void start(TNode node); + bool alreadyVisited(TNode current, TNode parent); + void visit(TNode current, TNode parent); + return_type done(TNode node); + void storeBvToBool(TNode bv_term, TNode bool_term); + bool hasBoolTerm(TNode node); +}; + + +class BvToBoolPreprocessor { + bool matchesBooleanPatern(TNode node); +public: + BvToBoolPreprocessor() + {} + ~BvToBoolPreprocessor() {} + void liftBoolToBV(const std::vector<Node>& assertions, std::vector<Node>& new_assertions); +}; + + +}/* CVC4::theory::bv namespace */ +}/* CVC4::theory namespace */ + +}/* CVC4 namespace */ + + +#endif /* __CVC4__THEORY__BV__BV_TO_BOOL_H */ diff --git a/src/theory/bv/options b/src/theory/bv/options index 2e53b029c..7b87baa21 100644 --- a/src/theory/bv/options +++ b/src/theory/bv/options @@ -19,5 +19,8 @@ option bitvectorInequalitySolver --bv-inequality-solver bool :default true option bitvectorCoreSolver --bv-core-solver bool turn on the core solver for the bit-vector theory + +option bvToBool --bv-to-bool bool + lift bit-vectors of size 1 to booleans when possible endmodule diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 433223308..fd2946d24 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -124,6 +124,7 @@ void TheoryBV::sendConflict() { void TheoryBV::check(Effort e) { + Trace("bitvector") <<"TheoryBV::check (" << e << ")\n"; Debug("bitvector") << "TheoryBV::check(" << e << ")" << std::endl; if (options::bitvectorEagerBitblast()) { return; @@ -244,10 +245,10 @@ Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, SubstitutionMap& outSubstitu Node TheoryBV::ppRewrite(TNode t) { - if (RewriteRule<BitwiseEq>::applies(t)) { - Node result = RewriteRule<BitwiseEq>::run<false>(t); - return Rewriter::rewrite(result); - } + // if (RewriteRule<BitwiseEq>::applies(t)) { + // Node result = RewriteRule<BitwiseEq>::run<false>(t); + // return Rewriter::rewrite(result); + // } if (options::bitvectorCoreSolver() && t.getKind() == kind::EQUAL) { std::vector<Node> equalities; diff --git a/src/theory/term_registration_visitor.h b/src/theory/term_registration_visitor.h index 768508d2c..5f89af9c6 100644 --- a/src/theory/term_registration_visitor.h +++ b/src/theory/term_registration_visitor.h @@ -95,7 +95,11 @@ public: * Notifies the engine of all the theories used. */ bool done(TNode node); - + ~PreRegisterVisitor() { + for (TNodeToTheorySetMap::const_iterator it = d_visited.begin(); it != d_visited.end(); ++it) { + std::cout << it->first <<"\n"; + } + } }; diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 442b1ef1c..6c8341345 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -119,7 +119,8 @@ TheoryEngine::TheoryEngine(context::Context* context, d_factsAsserted(context, false), d_preRegistrationVisitor(this, context), d_sharedTermsVisitor(d_sharedTerms), - d_unconstrainedSimp(context, logicInfo) + d_unconstrainedSimp(context, logicInfo), + d_bvToBoolPreprocessor() { for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; ++ theoryId) { d_theoryTable[theoryId] = NULL; @@ -1276,6 +1277,10 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) { } } +void TheoryEngine::ppBvToBool(const std::vector<Node>& assertions, std::vector<Node>& new_assertions) { + d_bvToBoolPreprocessor.liftBoolToBV(assertions, new_assertions); +} + Node TheoryEngine::ppSimpITE(TNode assertion) { Node result = d_iteSimplifier.simpITE(assertion); diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 9abdaa034..c21819ea1 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -45,6 +45,7 @@ #include "theory/ite_simplifier.h" #include "theory/unconstrained_simplifier.h" #include "theory/uf/equality_engine.h" +#include "theory/bv/bv_to_bool.h" namespace CVC4 { @@ -748,8 +749,11 @@ private: /** For preprocessing pass simplifying unconstrained expressions */ UnconstrainedSimplifier d_unconstrainedSimp; + /** For preprocessing pass lifting bit-vectors of size 1 to booleans */ + theory::bv::BvToBoolPreprocessor d_bvToBoolPreprocessor; public: + void ppBvToBool(const std::vector<Node>& assertions, std::vector<Node>& new_assertions); Node ppSimpITE(TNode assertion); void ppUnconstrainedSimp(std::vector<Node>& assertions); |