From: lianah Date: Wed, 17 Apr 2013 19:34:16 +0000 (-0400) Subject: innd examples are solved fast, but destruction assertion fail X-Git-Tag: cvc5-1.0.0~7293^2~5 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=eaa9f9af40941ef1aeb93367884e692301b60280;p=cvc5.git innd examples are solved fast, but destruction assertion fail --- diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index f8ec22943..35db0975e 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1928,11 +1928,11 @@ bool SmtEnginePrivate::nonClausalSimplify() { void SmtEnginePrivate::bvToBool() { - Trace("simplify") << "SmtEnginePrivate::bvToBool()" << endl; + Trace("bv-to-bool") << "SmtEnginePrivate::bvToBool()" << endl; std::vector 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]); + d_assertionsToCheck[i] = Rewriter::rewrite(new_assertions[i]); } } diff --git a/src/theory/bv/bv_to_bool.cpp b/src/theory/bv/bv_to_bool.cpp index 44c4bd021..8084a7282 100644 --- a/src/theory/bv/bv_to_bool.cpp +++ b/src/theory/bv/bv_to_bool.cpp @@ -30,7 +30,7 @@ void BvToBoolVisitor::addToCache(TNode term, Node new_term) { } Node BvToBoolVisitor::getCache(TNode term) const { - if (!hasCache(term)) { + if (!hasCache(term) || term.getKind() == kind::CONST_BITVECTOR) { return term; } return d_cache.find(term)->second; @@ -62,9 +62,11 @@ 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) && - node[0].getType().isBitVector() && - node[0].getType().getBitVectorSize() == 1; + isConvertibleBvTerm(node[0]) && + isConvertibleBvTerm(node[1]); } bool BvToBoolVisitor::isConvertibleBvTerm(TNode node) { @@ -81,6 +83,10 @@ bool BvToBoolVisitor::isConvertibleBvTerm(TNode node) { 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) { @@ -98,32 +104,51 @@ Node BvToBoolVisitor::convertBvAtom(TNode node) { Node result; switch(kind) { case kind::BITVECTOR_ULT: { - TNode a = getBoolForBvTerm(node[0]); - TNode b = getBoolForBvTerm(node[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 = 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: { - TNode a = getBoolForBvTerm(node[0]); - TNode b = getBoolForBvTerm(node[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 = 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::EQUAL, a, b); + 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: { - TNode a = getBoolForBvTerm(node[0]); - TNode b = getBoolForBvTerm(node[1]); + 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; } @@ -138,16 +163,19 @@ Node BvToBoolVisitor::convertBvTerm(TNode node) { return getBoolForBvTerm(node); } if (node.getKind() == kind::CONST_BITVECTOR) { - return (node == d_one ? utils::mkTrue() : utils::mkFalse()); + Node result = node == d_one ? utils::mkTrue() : utils::mkFalse(); + storeBvToBool(node, result); + return result; } } if (kind == kind::ITE) { - TNode cond = getCache(node[0]); - TNode true_branch = getBoolForBvTerm(node[1]); - TNode false_branch = getBoolForBvTerm(node[2]); + 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; } @@ -175,6 +203,7 @@ Node BvToBoolVisitor::convertBvTerm(TNode node) { } Node result = builder; storeBvToBool(node, result); + Debug("bv-to-bool") << "BvToBoolVisitor::convertBvTerm " << node <<" => " << result << "\n"; return result; } @@ -191,9 +220,8 @@ void BvToBoolVisitor::visit(TNode current, TNode parent) { Debug("bv-to-bool") << "BvToBoolVisitor visit (" << current << ", " << parent << ")\n"; Assert (!alreadyVisited(current, parent) && !hasCache(current)); - - Node result; + Node result; // make sure that the bv terms we are replacing to not occur in other contexts check(current, parent); @@ -217,14 +245,20 @@ void BvToBoolVisitor::visit(TNode current, TNode parent) { result = builder; } } - Assert (result != Node()); + Assert (result != Node()); + Debug("bv-to-bool") << " =>" << result <<"\n"; addToCache(current, result); } BvToBoolVisitor::return_type BvToBoolVisitor::done(TNode node) { Assert (hasCache(node)); - return getCache(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) { @@ -242,7 +276,8 @@ bool BvToBoolPreprocessor::matchesBooleanPatern(TNode current) { void BvToBoolPreprocessor::liftBoolToBV(const std::vector& assertions, std::vector& new_assertions) { - TNodeNodeMap candidates; + BvToBoolVisitor bvToBoolVisitor; + for (unsigned i = 0; i < assertions.size(); ++i) { if (matchesBooleanPatern(assertions[i])) { TNode assertion = assertions[i]; @@ -250,21 +285,21 @@ void BvToBoolPreprocessor::liftBoolToBV(const std::vector& assertions, std Assert (bv_var.getKind() == kind::VARIABLE && bv_var.getType().isBitVector() && bv_var.getType().getBitVectorSize() == 1); - TNode bool_cond = assertion[1]; + Node bool_cond = NodeVisitor::run(bvToBoolVisitor, assertion[1]); Assert (bool_cond.getType().isBoolean()); - if (candidates.find(bv_var) == candidates.end()) { + if (!bvToBoolVisitor.hasBoolTerm(bv_var)) { Debug("bv-to-bool") << "BBvToBoolPreprocessor::liftBvToBoolBV candidate: " << bv_var <<"\n"; - candidates[bv_var] = bool_cond; + bvToBoolVisitor.storeBvToBool(bv_var, bool_cond); } else { Debug("bv-to-bool") << "BvToBoolPreprocessor::liftBvToBoolBV multiple def " << bv_var <<"\n"; } } } - BvToBoolVisitor bvToBoolVisitor(candidates); for (unsigned i = 0; i < assertions.size(); ++i) { Node new_assertion = NodeVisitor::run(bvToBoolVisitor, assertions[i]); - new_assertions.push_back(new_assertion); + 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 index 39c6b4251..186f2b317 100644 --- a/src/theory/bv/bv_to_bool.h +++ b/src/theory/bv/bv_to_bool.h @@ -25,11 +25,11 @@ namespace theory { namespace bv { typedef __gnu_cxx::hash_set TNodeSet; -typedef __gnu_cxx::hash_map TNodeNodeMap; +typedef __gnu_cxx::hash_map NodeNodeMap; class BvToBoolVisitor { - TNodeNodeMap d_bvToBoolMap; - TNodeNodeMap d_cache; + NodeNodeMap d_bvToBoolMap; + NodeNodeMap d_cache; Node d_one; Node d_zero; @@ -40,14 +40,13 @@ class BvToBoolVisitor { bool isConvertibleBvTerm(TNode node); bool isConvertibleBvAtom(TNode node); Node getBoolForBvTerm(TNode node); - void storeBvToBool(TNode bv_term, TNode bool_term); Node convertBvAtom(TNode node); Node convertBvTerm(TNode node); void check(TNode current, TNode parent); public: typedef Node return_type; - BvToBoolVisitor(TNodeNodeMap& bvToBool) - : d_bvToBoolMap(bvToBool), + BvToBoolVisitor() + : d_bvToBoolMap(), d_cache(), d_one(utils::mkConst(BitVector(1, 1u))), d_zero(utils::mkConst(BitVector(1, 0u))) @@ -56,6 +55,8 @@ public: 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); }; 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 22a0b00ed..6c8341345 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1277,7 +1277,7 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) { } } -void TheoryEngine::ppBvToBool(const std::vector& assertions, std::vector new_assertions) { +void TheoryEngine::ppBvToBool(const std::vector& assertions, std::vector& new_assertions) { d_bvToBoolPreprocessor.liftBoolToBV(assertions, new_assertions); } diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 6d355ccce..c21819ea1 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -753,7 +753,7 @@ private: theory::bv::BvToBoolPreprocessor d_bvToBoolPreprocessor; public: - void ppBvToBool(const std::vector& assertions, std::vector new_assertions); + void ppBvToBool(const std::vector& assertions, std::vector& new_assertions); Node ppSimpITE(TNode assertion); void ppUnconstrainedSimp(std::vector& assertions);