diff options
-rw-r--r-- | src/prop/bvminisat/bvminisat.cpp | 26 | ||||
-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 | 31 | ||||
-rw-r--r-- | src/theory/bv/Makefile.am | 4 | ||||
-rw-r--r-- | src/theory/bv/bv_to_bool.cpp | 314 | ||||
-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 | 33 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.h | 8 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules.h | 19 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_normalization.h | 137 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h | 29 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_simplification.h | 55 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewriter.cpp | 48 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_utils.h | 7 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 7 | ||||
-rw-r--r-- | src/theory/theory_engine.h | 4 |
19 files changed, 751 insertions, 63 deletions
diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp index 6bbe4bb3e..fa5f53113 100644 --- a/src/prop/bvminisat/bvminisat.cpp +++ b/src/prop/bvminisat/bvminisat.cpp @@ -101,11 +101,13 @@ void BVMinisatSatSolver::interrupt(){ } SatValue BVMinisatSatSolver::solve(){ + ++d_statistics.d_statCallsToSolve; return toSatLiteralValue(d_minisat->solve()); } SatValue BVMinisatSatSolver::solve(long unsigned int& resource){ Trace("limit") << "MinisatSatSolver::solve(): have limit of " << resource << " conflicts" << std::endl; + ++d_statistics.d_statCallsToSolve; if(resource == 0) { d_minisat->budgetOff(); } else { @@ -120,30 +122,6 @@ SatValue BVMinisatSatSolver::solve(long unsigned int& resource){ return result; } -// SatValue BVMinisatSatSolver::solve(const context::CDList<SatLiteral> & assumptions, bool only_bcp){ -// ++d_solveCount; -// ++d_statistics.d_statCallsToSolve; - -// Debug("sat::minisat") << "Solve with assumptions "; -// context::CDList<SatLiteral>::const_iterator it = assumptions.begin(); -// BVMinisat::vec<BVMinisat::Lit> assump; -// for(; it!= assumptions.end(); ++it) { -// SatLiteral lit = *it; -// Debug("sat::minisat") << lit <<" "; -// assump.push(toMinisatLit(lit)); -// } -// Debug("sat::minisat") <<"\n"; - -// clock_t begin, end; -// begin = clock(); -// d_minisat->setOnlyBCP(only_bcp); -// SatLiteralValue result = toSatLiteralValue(d_minisat->solve(assump)); -// end = clock(); -// d_statistics.d_statSolveTime = d_statistics.d_statSolveTime.getData() + (end - begin)/(double)CLOCKS_PER_SEC; -// return result; -// } - - void BVMinisatSatSolver::getUnsatCore(SatClause& unsatCore) { // TODO add assertion to check the call was after an unsat call for (int i = 0; i < d_minisat->conflict.size(); ++i) { 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 52bc0c4d3..0d473a1a1 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(); @@ -1825,11 +1827,15 @@ bool SmtEnginePrivate::nonClausalSimplify() { } hash_set<TNode, TNodeHashFunction> s; + Trace("debugging") << "NonClausal simplify pre-preprocess\n"; for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) { Node assertion = d_assertionsToPreprocess[i]; Node assertionNew = d_topLevelSubstitutions.apply(assertion); + Trace("debugging") << "assertion = " << assertion << endl; + Trace("debugging") << "assertionNew = " << assertionNew << endl; if (assertion != assertionNew) { assertion = Rewriter::rewrite(assertionNew); + Trace("debugging") << "rewrite(assertion) = " << assertion << endl; } Assert(Rewriter::rewrite(assertion) == assertion); for (;;) { @@ -1838,8 +1844,11 @@ bool SmtEnginePrivate::nonClausalSimplify() { break; } ++d_smt.d_stats->d_numConstantProps; + Trace("debugging") << "assertionNew = " << assertionNew << endl; assertion = Rewriter::rewrite(assertionNew); + Trace("debugging") << "assertionNew = " << assertionNew << endl; } + Trace("debugging") << "\n"; s.insert(assertion); d_assertionsToCheck.push_back(assertion); Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): " @@ -1927,6 +1936,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); @@ -2780,6 +2798,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..7bec805ef --- /dev/null +++ b/src/theory/bv/bv_to_bool.cpp @@ -0,0 +1,314 @@ +/********************* */ +/*! \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 && + bool_term.getType().isBoolean() && bv_term != Node() && bool_term != Node()); + if (d_bvToBoolMap.find(bv_term) != d_bvToBoolMap.end()) { + Assert (d_bvToBoolMap[bv_term] == bool_term); + } + 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; + } + + if (!node.getType().isBitVector() || node.getType().getBitVectorSize() != 1) + return false; + + Kind kind = node.getKind(); + + 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; + } + if (kind == kind::VARIABLE) { + storeBvToBool(node, utils::mkNode(kind::EQUAL, node, utils::mkConst(BitVector(1, 1u)))); + 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); + addToCache(current, result); + } 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; + } + addToCache(current, result); + } + Assert (result != Node()); + Debug("bv-to-bool") << " =>" << result <<"\n"; +} + + +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 c597cb083..4c31f3f44 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -43,6 +43,7 @@ TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& d_subtheories(), d_subtheoryMap(), d_statistics(), + d_lemmasAdded(c, false), d_conflict(c, false), d_literalsToPropagate(c), d_literalsToPropagateIndex(c, 0), @@ -125,8 +126,37 @@ void TheoryBV::sendConflict() { } } +void TheoryBV::checkForLemma(TNode fact) { + if (fact.getKind() == kind::EQUAL) { + if (fact[0].getKind() == kind::BITVECTOR_UREM_TOTAL) { + TNode urem = fact[0]; + TNode result = fact[1]; + TNode divisor = urem[1]; + Node result_ult_div = mkNode(kind::BITVECTOR_ULT, result, divisor); + Node divisor_eq_0 = mkNode(kind::EQUAL, + divisor, + mkConst(BitVector(getSize(divisor), 0u))); + Node split = utils::mkNode(kind::OR, divisor_eq_0, mkNode(kind::NOT, fact), result_ult_div); + lemma(split); + } + if (fact[1].getKind() == kind::BITVECTOR_UREM_TOTAL) { + TNode urem = fact[1]; + TNode result = fact[0]; + TNode divisor = urem[1]; + Node result_ult_div = mkNode(kind::BITVECTOR_ULT, result, divisor); + Node divisor_eq_0 = mkNode(kind::EQUAL, + divisor, + mkConst(BitVector(getSize(divisor), 0u))); + Node split = utils::mkNode(kind::OR, divisor_eq_0, mkNode(kind::NOT, fact), result_ult_div); + lemma(split); + } + } +} + + void TheoryBV::check(Effort e) { + Trace("bitvector") <<"TheoryBV::check (" << e << ")\n"; Debug("bitvector") << "TheoryBV::check(" << e << ")" << std::endl; if (options::bitvectorEagerBitblast()) { return; @@ -145,6 +175,7 @@ void TheoryBV::check(Effort e) while (!done()) { TNode fact = get().assertion; + // checkForLemma(fact); for (unsigned i = 0; i < d_subtheories.size(); ++i) { d_subtheories[i]->assertFact(fact); } @@ -249,7 +280,7 @@ 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); + Node result = RewriteRule<BitwiseEq>::run<false>(t); return Rewriter::rewrite(result); } diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index 481493e13..22e3d0507 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -85,6 +85,8 @@ private: Statistics d_statistics; + context::CDO<bool> d_lemmasAdded; + // Are we in conflict? context::CDO<bool> d_conflict; @@ -97,6 +99,8 @@ private: /** Index of the next literal to propagate */ context::CDO<unsigned> d_literalsToPropagateIndex; + + /** * Keeps a map from nodes to the subtheory that propagated it so that we can explain it * properly. @@ -147,7 +151,9 @@ private: void sendConflict(); - void lemma(TNode node) { d_out->lemma(node); } + void lemma(TNode node) { d_out->lemma(node); d_lemmasAdded = true; } + + void checkForLemma(TNode node); friend class Bitblaster; friend class BitblastSolver; diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h index e9a3494f0..baaf7e133 100644 --- a/src/theory/bv/theory_bv_rewrite_rules.h +++ b/src/theory/bv/theory_bv_rewrite_rules.h @@ -52,6 +52,7 @@ enum RewriteRuleId { SubEliminate, SltEliminate, SleEliminate, + UleEliminate, CompEliminate, RepeatEliminate, RotateLeftEliminate, @@ -125,12 +126,17 @@ enum RewriteRuleId { UremOne, UremSelf, ShiftZero, + + UltOne, + SltZero, + ZeroUlt, /// normalization rules ExtractBitwise, ExtractNot, ExtractArith, ExtractArith2, + ExtractSignExtend, DoubleNeg, NegMult, NegSub, @@ -148,7 +154,7 @@ enum RewriteRuleId { AndSimplify, OrSimplify, XorSimplify, - + BitwiseSlicing, // rules to simplify bitblasting BBPlusNeg }; @@ -262,7 +268,13 @@ inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) { case OrSimplify : out << "OrSimplify"; return out; case XorSimplify : out << "XorSimplify"; return out; case NegPlus : out << "NegPlus"; return out; - case BBPlusNeg : out << "BBPlusNeg"; return out; + case BBPlusNeg : out << "BBPlusNeg"; return out; + case UltOne : out << "UltOne"; return out; + case SltZero : out << "SltZero"; return out; + case ZeroUlt : out << "ZeroUlt"; return out; + case UleEliminate : out << "UleEliminate"; return out; + case BitwiseSlicing : out << "BitwiseSlicing"; return out; + case ExtractSignExtend : out << "ExtractSignExtend"; return out; default: Unreachable(); } @@ -477,6 +489,9 @@ struct AllRewriteRules { RewriteRule<BBPlusNeg> rule111; RewriteRule<SolveEq> rule112; RewriteRule<BitwiseEq> rule113; + RewriteRule<UltOne> rule114; + RewriteRule<SltZero> rule115; + }; template<> inline diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h index 4ba09ef67..2da4dfa6a 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h +++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h @@ -72,6 +72,58 @@ Node RewriteRule<ExtractNot>::apply(TNode node) { return utils::mkNode(kind::BITVECTOR_NOT, a); } +/** + * ExtractSignExtend + * + * (sign_extend k x) [i:j] => pushes extract in + * + * @return + */ + +template<> inline +bool RewriteRule<ExtractSignExtend>::applies(TNode node) { + if (node.getKind() == kind::BITVECTOR_EXTRACT && + node[0].getKind() == kind::BITVECTOR_SIGN_EXTEND) { + return true; + } + return false; +} + +template<> inline +Node RewriteRule<ExtractSignExtend>::apply(TNode node) { + Debug("bv-rewrite") << "RewriteRule<ExtractSignExtend>(" << node << ")" << std::endl; + TNode extendee = node[0][0]; + unsigned extendee_size = utils::getSize(extendee); + + unsigned high = utils::getExtractHigh(node); + unsigned low = utils::getExtractLow(node); + + Node resultNode; + // extract falls on extendee + if (high < extendee_size) { + resultNode = utils::mkExtract(extendee, high, low); + } else if (low < extendee_size && high >= extendee_size) { + // if extract overlaps sign extend and extendee + Node low_extract = utils::mkExtract(extendee, extendee_size - 1, low); + unsigned new_ammount = high - extendee_size + 1; + resultNode = utils::mkSignExtend(low_extract, new_ammount); + } else { + // extract only over sign extend + Assert (low >= extendee_size); + unsigned top = utils::getSize(extendee) - 1; + Node most_significant_bit = utils::mkExtract(extendee, top, top); + std::vector<Node> bits; + for (unsigned i = 0; i < high - low + 1; ++i) { + bits.push_back(most_significant_bit); + } + resultNode = utils::mkNode(kind::BITVECTOR_CONCAT, bits); + } + Debug("bv-rewrite") << " =>" << resultNode << std::endl; + return resultNode; +} + + + /** * ExtractArith * @@ -1032,19 +1084,84 @@ Node RewriteRule<XorSimplify>::apply(TNode node) { } +/** + * BitwiseSlicing + * + * (a bvand c) ==> (concat (bvand a[i0:j0] c0) ... (bvand a[in:jn] cn)) + * where c0,..., cn are maximally continuous substrings of 0 or 1 in the constant c + * + * Note: this rule assumes AndSimplify has already been called on the node + */ +template<> inline +bool RewriteRule<BitwiseSlicing>::applies(TNode node) { + if ((node.getKind() != kind::BITVECTOR_AND && + node.getKind() != kind::BITVECTOR_OR && + node.getKind() != kind::BITVECTOR_XOR) || + utils::getSize(node) == 1) + return false; + + for (unsigned i = 0; i < node.getNumChildren(); ++i) { + if (node[i].getKind() == kind::CONST_BITVECTOR) { + BitVector constant = node[i].getConst<BitVector>(); + // we do not apply the rule if the constant is all 0s or all 1s + if (constant == BitVector(utils::getSize(node), 0u)) + return false; + + for (unsigned i = 0; i < constant.getSize(); ++i) { + if (!constant.isBitSet(i)) + return true; + } + } + } + return false; +} +template<> inline +Node RewriteRule<BitwiseSlicing>::apply(TNode node) { + Debug("bv-rewrite") << "RewriteRule<BitwiseSlicing>(" << node << ")" << std::endl; + // get the constant + bool found_constant CVC4_UNUSED = false ; + TNode constant; + std::vector<Node> other_children; + for (unsigned i = 0; i < node.getNumChildren(); ++i) { + if (node[i].getKind() == kind::CONST_BITVECTOR) { + constant = node[i]; + Assert (!found_constant); + found_constant = true; + } else { + other_children.push_back(node[i]); + } + } + Assert (found_constant && other_children.size() == node.getNumChildren() - 1); -// template<> inline -// bool RewriteRule<AndSimplify>::applies(TNode node) { -// return (node.getKind() == kind::BITVECTOR_AND); -// } - -// template<> inline -// Node RewriteRule<AndSimplify>::apply(TNode node) { -// Debug("bv-rewrite") << "RewriteRule<AndSimplify>(" << node << ")" << std::endl; -// return resultNode; -// } + Node other = utils::mkNode(node.getKind(), other_children); + + BitVector bv_constant = constant.getConst<BitVector>(); + std::vector<Node> concat_children; + int start = bv_constant.getSize() - 1; + int end = start; + for (int i = end - 1; i >= 0; --i) { + if (bv_constant.isBitSet(i + 1) != bv_constant.isBitSet(i)) { + Node other_extract = utils::mkExtract(other, end, start); + Node const_extract = utils::mkExtract(constant, end, start); + Node bitwise_op = utils::mkNode(node.getKind(), const_extract, other_extract); + concat_children.push_back(bitwise_op); + start = end = i; + } else { + start--; + } + if (i == 0) { + Node other_extract = utils::mkExtract(other, end, 0); + Node const_extract = utils::mkExtract(constant, end, 0); + Node bitwise_op = utils::mkNode(node.getKind(), const_extract, other_extract); + concat_children.push_back(bitwise_op); + } + } + Node result = utils::mkNode(kind::BITVECTOR_CONCAT, concat_children); + Debug("bv-rewrite") << " =>" << result << std::endl; + return result; +} // template<> inline // bool RewriteRule<>::applies(TNode node) { diff --git a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h index 06ddc215d..cf36633fa 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h +++ b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h @@ -111,17 +111,30 @@ bool RewriteRule<SleEliminate>::applies(TNode node) { template <> Node RewriteRule<SleEliminate>::apply(TNode node) { Debug("bv-rewrite") << "RewriteRule<SleEliminate>(" << node << ")" << std::endl; - - unsigned size = utils::getSize(node[0]); - Node pow_two = utils::mkConst(BitVector(size, Integer(1).multiplyByPow2(size - 1))); - Node a = utils::mkNode(kind::BITVECTOR_PLUS, node[0], pow_two); - Node b = utils::mkNode(kind::BITVECTOR_PLUS, node[1], pow_two); - - return utils::mkNode(kind::BITVECTOR_ULE, a, b); - + + TNode a = node[0]; + TNode b = node[1]; + Node b_slt_a = utils::mkNode(kind::BITVECTOR_SLT, b, a); + return utils::mkNode(kind::NOT, b_slt_a); } template <> +bool RewriteRule<UleEliminate>::applies(TNode node) { + return (node.getKind() == kind::BITVECTOR_ULE); +} + +template <> +Node RewriteRule<UleEliminate>::apply(TNode node) { + Debug("bv-rewrite") << "RewriteRule<UleEliminate>(" << node << ")" << std::endl; + + TNode a = node[0]; + TNode b = node[1]; + Node b_ult_a = utils::mkNode(kind::BITVECTOR_ULT, b, a); + return utils::mkNode(kind::NOT, b_ult_a); +} + + +template <> bool RewriteRule<CompEliminate>::applies(TNode node) { return (node.getKind() == kind::BITVECTOR_COMP); } diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h index bcfb189af..d660dde29 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h +++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h @@ -524,6 +524,25 @@ Node RewriteRule<LteSelf>::apply(TNode node) { } /** + * ZeroUlt + * + * 0 < a ==> a != 0 + */ + +template<> inline +bool RewriteRule<ZeroUlt>::applies(TNode node) { + return (node.getKind() == kind::BITVECTOR_ULT && + node[0] == utils::mkConst(BitVector(utils::getSize(node[0]), Integer(0)))); +} + +template<> inline +Node RewriteRule<ZeroUlt>::apply(TNode node) { + Debug("bv-rewrite") << "RewriteRule<ZeroUlt>(" << node << ")" << std::endl; + return utils::mkNode(kind::NOT, utils::mkNode(kind::EQUAL, node[0], node[1])); +} + + +/** * UltZero * * a < 0 ==> false @@ -541,6 +560,42 @@ Node RewriteRule<UltZero>::apply(TNode node) { return utils::mkFalse(); } + +/** + * + */ +template<> inline +bool RewriteRule<UltOne>::applies(TNode node) { + return (node.getKind() == kind::BITVECTOR_ULT && + node[1] == utils::mkConst(BitVector(utils::getSize(node[0]), Integer(1)))); +} + +template<> inline +Node RewriteRule<UltOne>::apply(TNode node) { + Debug("bv-rewrite") << "RewriteRule<UltOne>(" << node << ")" << std::endl; + return utils::mkNode(kind::EQUAL, node[0], utils::mkConst(BitVector(utils::getSize(node[0]), 0u))); +} + +/** + * + */ +template<> inline +bool RewriteRule<SltZero>::applies(TNode node) { + return (node.getKind() == kind::BITVECTOR_SLT && + node[1] == utils::mkConst(BitVector(utils::getSize(node[0]), Integer(0)))); +} + +template<> inline +Node RewriteRule<SltZero>::apply(TNode node) { + Debug("bv-rewrite") << "RewriteRule<UltZero>(" << node << ")" << std::endl; + unsigned size = utils::getSize(node[0]); + Node most_significant_bit = utils::mkExtract(node[0], size - 1, size - 1); + Node one = utils::mkConst(BitVector(1, 1u)); + + return utils::mkNode(kind::EQUAL, most_significant_bit, one); +} + + /** * UltSelf * diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp index a712a8391..5a43e2c57 100644 --- a/src/theory/bv/theory_bv_rewriter.cpp +++ b/src/theory/bv/theory_bv_rewriter.cpp @@ -77,6 +77,8 @@ RewriteResponse TheoryBVRewriter::RewriteUlt(TNode node, bool preregister) { // if both arguments are constants evaluates RewriteRule<UltZero> // a < 0 rewrites to false + // RewriteRule<UltOne>, + // RewriteRule<ZeroUlt> >::apply(node); return RewriteResponse(REWRITE_DONE, resultNode); @@ -85,6 +87,7 @@ RewriteResponse TheoryBVRewriter::RewriteUlt(TNode node, bool preregister) { RewriteResponse TheoryBVRewriter::RewriteSlt(TNode node, bool preregister){ Node resultNode = LinearRewriteStrategy < RewriteRule < EvalSlt > + // RewriteRule < SltZero > >::apply(node); return RewriteResponse(REWRITE_DONE, resultNode); @@ -103,17 +106,18 @@ RewriteResponse TheoryBVRewriter::RewriteUle(TNode node, bool preregister){ RewriteRule<UleMax>, RewriteRule<ZeroUle>, RewriteRule<UleZero>, - RewriteRule<UleSelf> + RewriteRule<UleSelf>//, + // RewriteRule<UleEliminate> >::apply(node); return RewriteResponse(resultNode == node ? REWRITE_DONE : REWRITE_AGAIN, resultNode); } RewriteResponse TheoryBVRewriter::RewriteSle(TNode node, bool preregister){ Node resultNode = LinearRewriteStrategy - < RewriteRule < EvalSle > + < RewriteRule <EvalSle>//, + // RewriteRule <SleEliminate> >::apply(node); - - return RewriteResponse(REWRITE_DONE, resultNode); + return RewriteResponse(resultNode == node? REWRITE_DONE : REWRITE_AGAIN, resultNode); } RewriteResponse TheoryBVRewriter::RewriteUgt(TNode node, bool preregister){ @@ -173,6 +177,11 @@ RewriteResponse TheoryBVRewriter::RewriteExtract(TNode node, bool preregister) { return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); } + if (RewriteRule<ExtractSignExtend>::applies(node)) { + resultNode = RewriteRule<ExtractSignExtend>::run<false>(node); + return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); + } + if (RewriteRule<ExtractBitwise>::applies(node)) { resultNode = RewriteRule<ExtractBitwise>::run<false>(node); return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); @@ -219,14 +228,14 @@ RewriteResponse TheoryBVRewriter::RewriteAnd(TNode node, bool preregister){ resultNode = LinearRewriteStrategy < RewriteRule<FlattenAssocCommut>, - RewriteRule<AndSimplify> - // RewriteRule<EvalAnd>, - // RewriteRule<BitwiseIdemp>, - // //RewriteRule<BitwiseSlice>, -> might need rw again - // RewriteRule<AndZero>, - // RewriteRule<AndOne> + RewriteRule<AndSimplify>, + RewriteRule<BitwiseSlicing> >::apply(node); + if (resultNode.getKind() != node.getKind()) { + return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); + } + return RewriteResponse(REWRITE_DONE, resultNode); } @@ -235,8 +244,13 @@ RewriteResponse TheoryBVRewriter::RewriteOr(TNode node, bool preregister){ resultNode = LinearRewriteStrategy < RewriteRule<FlattenAssocCommut>, - RewriteRule<OrSimplify> + RewriteRule<OrSimplify>, + RewriteRule<BitwiseSlicing> >::apply(node); + + if (resultNode.getKind() != node.getKind()) { + return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); + } return RewriteResponse(REWRITE_DONE, resultNode); } @@ -247,7 +261,8 @@ RewriteResponse TheoryBVRewriter::RewriteXor(TNode node, bool preregister) { resultNode = LinearRewriteStrategy < RewriteRule<FlattenAssocCommut>, // flatten the expression RewriteRule<XorSimplify>, // simplify duplicates and constants - RewriteRule<XorZero> // checks if the constant part is zero and eliminates it + RewriteRule<XorZero>, // checks if the constant part is zero and eliminates it + RewriteRule<BitwiseSlicing> >::apply(node); // this simplification introduces new terms and might require further @@ -257,6 +272,10 @@ RewriteResponse TheoryBVRewriter::RewriteXor(TNode node, bool preregister) { return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); } + if (resultNode.getKind() != node.getKind()) { + return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); + } + return RewriteResponse(REWRITE_DONE, resultNode); } @@ -297,7 +316,8 @@ RewriteResponse TheoryBVRewriter::RewriteMult(TNode node, bool preregister) { resultNode = LinearRewriteStrategy < RewriteRule<FlattenAssocCommut>, // flattens and sorts - RewriteRule<MultSimplify> // multiplies constant part and checks for 0 + RewriteRule<MultSimplify>, // multiplies constant part and checks for 0 + RewriteRule<MultPow2> // replaces multiplication by a power of 2 by a shift >::apply(node); // only apply if every subterm was already rewritten @@ -313,7 +333,7 @@ RewriteResponse TheoryBVRewriter::RewriteMult(TNode node, bool preregister) { if(resultNode == node) { return RewriteResponse(REWRITE_DONE, resultNode); } - return RewriteResponse(REWRITE_DONE, resultNode); + return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); } RewriteResponse TheoryBVRewriter::RewritePlus(TNode node, bool preregister) { diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h index 174df03ab..5847bac3e 100644 --- a/src/theory/bv/theory_bv_utils.h +++ b/src/theory/bv/theory_bv_utils.h @@ -84,6 +84,7 @@ inline Node mkSortedNode(Kind kind, std::vector<Node>& children) { inline Node mkNode(Kind kind, std::vector<Node>& children) { + Assert (children.size() > 0); if (children.size() == 1) { return children[0]; } @@ -133,6 +134,12 @@ inline Node mkXor(TNode node1, TNode node2) { } +inline Node mkSignExtend(TNode node, unsigned ammount) { + NodeManager* nm = NodeManager::currentNM(); + Node signExtendOp = nm->mkConst<BitVectorSignExtend>(BitVectorSignExtend(ammount)); + return nm->mkNode(signExtendOp, node); +} + inline Node mkExtract(TNode node, unsigned high, unsigned low) { Node extractOp = NodeManager::currentNM()->mkConst<BitVectorExtract>(BitVectorExtract(high, low)); std::vector<Node> children; 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); |