From: lianah Date: Fri, 12 Apr 2013 20:15:30 +0000 (-0400) Subject: finished implementing bv to bool lifting and added --bv-to-bool option X-Git-Tag: cvc5-1.0.0~7293^2~8 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c5c8a6497f8ac52c4f2c57fcd5ed23790f26c735;p=cvc5.git finished implementing bv to bool lifting and added --bv-to-bool option --- diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 55000c94d..9ee2c5722 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& cache); - + // Lift bit-vectors of size 1 to booleans + void bvToBool(); + // Simplify ITE structure void simpITE(); @@ -1925,6 +1927,14 @@ bool SmtEnginePrivate::nonClausalSimplify() { } +void SmtEnginePrivate::bvToBool() { + Trace("simplify") << "SmtEnginePrivate::bvToBool()" << endl; + + for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) { + d_assertionsToCheck[i] = d_smt.d_theoryEngine->ppBvToBool(d_assertionsToCheck[i]); + } +} + void SmtEnginePrivate::simpITE() { TimerStat::CodeTimer simpITETimer(d_smt.d_stats->d_simpITETime); @@ -2474,6 +2484,16 @@ bool SmtEnginePrivate::simplifyAssertions() Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl; Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl; + // 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; + if(options::repeatSimp() && options::simplificationMode() != SIMPLIFICATION_MODE_NONE) { Chat() << "...doing another round of nonclausal simplification..." << endl; Trace("simplify") << "SmtEnginePrivate::simplify(): " diff --git a/src/theory/bv/bv_to_bool.cpp b/src/theory/bv/bv_to_bool.cpp index f39d12a39..5ab7cf144 100644 --- a/src/theory/bv/bv_to_bool.cpp +++ b/src/theory/bv/bv_to_bool.cpp @@ -23,22 +23,40 @@ using namespace CVC4; using namespace CVC4::theory; using namespace CVC4::theory::bv; -void BvToBoolVisitor::addToCache(TNode bv_term, Node bool_term) { - Assert (!hasCache(bv_term)); +void BvToBoolVisitor::storeBvToBool(TNode bv_term, Node bool_term) { + Assert (!hasBoolTerm(bv_term)); Assert (bool_term.getType().isBoolean()); - d_cache[bv_term] = bool_term; + d_bvToBoolTerm[bv_term] = bool_term; } -Node BvToBoolVisitor::getCache(TNode bv_term) const { - Assert (hasCache(bv_term)); - return d_cache.find(bv_term)->second; +Node BvToBoolVisitor::getBoolTerm(TNode bv_term) const { + Assert(hasBoolTerm(bv_term)); + return d_bvToBoolTerm.find(bv_term)->second; } -bool BvToBoolVisitor::hasCache(TNode bv_term) const { +bool BvToBoolVisitor::hasBoolTerm(TNode bv_term) const { Assert (bv_term.getType().isBitVector()); - return d_cache.find(bv_term) != d_cache.end(); + return d_bvToBoolTerm.find(bv_term) != d_bvToBoolTerm.end(); } +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)) { + 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) {} bool BvToBoolVisitor::alreadyVisited(TNode current, TNode parent) { @@ -60,95 +78,126 @@ bool BvToBoolVisitor::isConvertibleToBool(TNode current) { kind == kind::BITVECTOR_AND || kind == kind::BITVECTOR_XOR || kind == kind::BITVECTOR_NOT || - // kind == kind::BITVECTOR_PLUS || - // kind == kind::BITVECTOR_SUB || - // kind == kind::BITVECTOR_NEG || kind == kind::BITVECTOR_ULT || kind == kind::BITVECTOR_ULE || kind == kind::EQUAL) { - return current[0].getType().getBitVectorSize() == 1; + // we can convert it to bool if all of the children can also be converted + // to bool + if (! current[0].getType().getBitVectorSize() == 1) + return false; + for (unsigned i = 0; i < current.getNumChildren(); ++i) { + // we assume that the children have been visited + if (!hasBoolTerm(current[i])) + return false; + } + return true; } if (kind == kind::ITE && type.isBitVector()) { - return type.getBitVectorSize() == 1; + return type.getBitVectorSize() == 1 && hasBoolTerm(current[1]) && hasBoolTerm(current[2]); } return false; } + Node BvToBoolVisitor::convertToBool(TNode current) { + Debug("bv-to-bool") << "BvToBoolVisitor::convertToBool (" << current << ") "; Kind kind = current.getKind(); - if (kind == kind::BITVECTOR_ULT) { - TNode a = getCache(current[0]); - TNode b = getCache(current[1]); + + Node new_current; + if (current.getNumChildren() == 0) { + if (current.getKind() == kind::CONST_BITVECTOR) { + new_current = current == d_one? utils::mkTrue() : utils::mkFalse(); + } else { + new_current = utils::mkNode(kind::EQUAL, current, d_one); + } + Debug("bv-to-bool") << "=> " << new_current << "\n"; + } else if (kind == kind::BITVECTOR_ULT) { + TNode a = getBoolTerm(current[0]); + TNode b = getBoolTerm(current[1]); Node a_eq_0 = utils::mkNode(kind::EQUAL, a, d_zero); Node b_eq_1 = utils::mkNode(kind::EQUAL, b, d_one); - Node new_current = utils::mkNode(kind::AND, a_eq_0, b_eq_1); - return new_current; - } - if (kind == kind::BITVECTOR_ULE) { - TNode a = getCache(current[0]); - TNode b = getCache(current[1]); + new_current = utils::mkNode(kind::AND, a_eq_0, b_eq_1); + } else if (kind == kind::BITVECTOR_ULE) { + TNode a = getBoolTerm(current[0]); + TNode b = getBoolTerm(current[1]); Node a_eq_0 = utils::mkNode(kind::EQUAL, a, d_zero); Node b_eq_1 = utils::mkNode(kind::EQUAL, b, d_one); Node a_lt_b = utils::mkNode(kind::AND, a_eq_0, b_eq_1); Node a_eq_b = utils::mkNode(kind::EQUAL, a, b); - Node new_current = utils::mkNode(kind::OR, a_lt_b, a_eq_b); - return new_current; + new_current = utils::mkNode(kind::OR, a_lt_b, a_eq_b); + } else if (kind == kind::ITE) { + TNode cond = current[0]; + TNode a = getBoolTerm(current[1]); + TNode b = getBoolTerm(current[2]); + new_current = utils::mkNode(kind::ITE, cond, a, b); + } else { + 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; + case kind::EQUAL: + new_kind = kind::IFF; + break; + default: + Unreachable("Unknown kind ", kind); + } + NodeBuilder<> builder(new_kind); + if (current.getMetaKind() == kind::metakind::PARAMETERIZED) { + builder << current.getOperator(); + } + for (unsigned i = 0; i < current.getNumChildren(); ++i) { + builder << getBoolTerm(current[i]); + } + new_current = builder; } - - Kind new_kind; - switch (kind) { - case kind::BITVECTOR_OR : - new_kind = kind::OR; - case kind::BITVECTOR_AND: - new_kind = kind::AND; - case kind::BITVECTOR_XOR: - new_kind = kind::XOR; - case kind::BITVECTOR_NOT: - new_kind = kind::NOT; - case kind::BITVECTOR_ULT: - default: - Unreachable(); - } - NodeBuilder<> builder(new_kind); - for (unsigned i = 0; i < current.getNumChildren(); ++i) { - builder << getCache(current[i]); + Debug("bv-to-bool") << "=> " << new_current << "\n"; + if (current.getType().isBitVector()) { + storeBvToBool(current, new_current); + } else { + addToCache(current, new_current); } - return builder; + return new_current; } void BvToBoolVisitor::visit(TNode current, TNode parent) { + Debug("bv-to-bool") << "BvToBoolVisitor visit (" << current << ", " << parent << ")\n"; Assert (!alreadyVisited(current, parent)); d_visited.insert(current); - - if (current.getNumChildren() == 0 && - isConvertibleToBool(current)) { - Node bool_current; - if (current.getKind() == kind::CONST_BITVECTOR) { - bool_current = current == d_one? utils::mkTrue() : utils::mkFalse(); - } else { - bool_current = utils::mkNode(kind::EQUAL, current, d_one); - } - addToCache(current, bool_current); - return; - } + Node result; // if it has more than one child if (isConvertibleToBool(current)) { - Node bool_current = convertToBool(current); - addToCache(current, bool_current); + result = convertToBool(current); } else { - NodeBuilder<> builder(current.getKind()); - for (unsigned i = 0; i < current.getNumChildren(); ++i) { - Node converted = getCache(current[i]); - if (converted.getType() == current[i].getType()) { - builder << converted; - } else { - builder << current[i]; + 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]); + if (converted.getType() == current[i].getType()) { + builder << converted; + } else { + builder << current[i]; + } } + result = builder; } - Node result = builder; addToCache(current, result); } } diff --git a/src/theory/bv/bv_to_bool.h b/src/theory/bv/bv_to_bool.h index ef80930b4..d5673a295 100644 --- a/src/theory/bv/bv_to_bool.h +++ b/src/theory/bv/bv_to_bool.h @@ -29,20 +29,27 @@ class BvToBoolVisitor { typedef __gnu_cxx::hash_set TNodeSet; typedef __gnu_cxx::hash_map TNodeNodeMap; TNodeNodeMap d_cache; + TNodeNodeMap d_bvToBoolTerm; TNodeSet d_visited; Node d_one; Node d_zero; - void addToCache(TNode bv_term, Node bool_term); - Node getCache(TNode bv_term) const; - bool hasCache(TNode bv_term) const; + void storeBvToBool(TNode bv_term, Node bool_term); + Node getBoolTerm(TNode bv_term) const; + bool hasBoolTerm(TNode bv_term) const; + void addToCache(TNode term, Node new_term); + Node getCache(TNode term) const; + bool hasCache(TNode term) const; + + bool isConvertibleToBool(TNode current); Node convertToBool(TNode current); public: typedef Node return_type; BvToBoolVisitor() : d_cache(), + d_bvToBoolTerm(), d_visited(), d_one(utils::mkConst(BitVector(1, 1u))), d_zero(utils::mkConst(BitVector(1, 0u))) 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::applies(t)) { - Node result = RewriteRule::run(t); - return Rewriter::rewrite(result); - } + // if (RewriteRule::applies(t)) { + // Node result = RewriteRule::run(t); + // return Rewriter::rewrite(result); + // } if (options::bitvectorCoreSolver() && t.getKind() == kind::EQUAL) { std::vector equalities; diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 442b1ef1c..6f965879d 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,12 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) { } } +Node TheoryEngine::ppBvToBool(TNode assertion) { + Node result = d_bvToBoolPreprocessor.liftBoolToBV(assertion); + result = Rewriter::rewrite(result); + return result; +} + 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..324b952b0 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: + Node ppBvToBool(TNode assertion); Node ppSimpITE(TNode assertion); void ppUnconstrainedSimp(std::vector& assertions);