diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-05-03 20:18:18 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-05-03 20:18:18 +0000 |
commit | 1433806056059339dd16ae8e431feaae23553150 (patch) | |
tree | cf678baa687b1a19e479c28a1c01470bb2f120c7 /src/theory/bv | |
parent | 8ef2015de66fc409a2a2958b9452c0c9b1456ee3 (diff) |
Some cleanup starting off from trying to understand the sharing code. Changes include
* fixed term visitor from the bvprop branch
* removed all the warnings from builds -- warnings are there to be noted *NOT* to be used as scribbles
* moved the LogicInfo into the theory constructor
Diffstat (limited to 'src/theory/bv')
-rw-r--r-- | src/theory/bv/theory_bv.cpp | 24 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.h | 7 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_normalization.h | 9 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_simplification.h | 17 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewriter.h | 3 |
5 files changed, 26 insertions, 34 deletions
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index a3f4364ba..b6f12793d 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -36,13 +36,13 @@ const bool d_useEqualityEngine = true; const bool d_useSatPropagation = true; -TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation) - : Theory(THEORY_BV, c, u, out, valuation), +TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) + : Theory(THEORY_BV, c, u, out, valuation, logicInfo), d_context(c), d_assertions(c), d_bitblaster(new Bitblaster(c) ), - d_statistics(), d_alreadyPropagatedSet(c), + d_statistics(), d_notify(*this), d_equalityEngine(d_notify, c, "theory::bv::TheoryBV"), d_conflict(c, false), @@ -204,7 +204,7 @@ void TheoryBV::check(Effort e) // If in conflict, output the conflict if (d_conflict) { - Debug("bitvector") << spaces(getContext()->getLevel()) << "TheoryBV::check(): conflict " << d_conflictNode << std::endl; + Debug("bitvector") << spaces(getSatContext()->getLevel()) << "TheoryBV::check(): conflict " << d_conflictNode << std::endl; d_out->conflict(d_conflictNode); return; } @@ -247,7 +247,7 @@ Node TheoryBV::getValue(TNode n) { void TheoryBV::propagate(Effort e) { - BVDebug("bitvector") << spaces(getContext()->getLevel()) << "TheoryBV::propagate()" << std::endl; + BVDebug("bitvector") << spaces(getSatContext()->getLevel()) << "TheoryBV::propagate()" << std::endl; if (d_conflict) { return; @@ -256,13 +256,13 @@ void TheoryBV::propagate(Effort e) { // get new propagations from the equality engine for (; d_literalsToPropagateIndex < d_literalsToPropagate.size(); d_literalsToPropagateIndex = d_literalsToPropagateIndex + 1) { TNode literal = d_literalsToPropagate[d_literalsToPropagateIndex]; - BVDebug("bitvector") << spaces(getContext()->getLevel()) << "TheoryBV::propagate(): propagating from equality engine: " << literal << std::endl; + BVDebug("bitvector") << spaces(getSatContext()->getLevel()) << "TheoryBV::propagate(): propagating from equality engine: " << literal << std::endl; bool satValue; Node normalized = Rewriter::rewrite(literal); if (!d_valuation.hasSatValue(normalized, satValue) || satValue) { d_out->propagate(literal); } else { - Debug("bitvector") << spaces(getContext()->getLevel()) << "TheoryBV::propagate(): in conflict, normalized = " << normalized << std::endl; + Debug("bitvector") << spaces(getSatContext()->getLevel()) << "TheoryBV::propagate(): in conflict, normalized = " << normalized << std::endl; Node negatedLiteral; std::vector<TNode> assumptions; if (normalized != d_false) { @@ -353,11 +353,11 @@ Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, SubstitutionMap& outSubstitu bool TheoryBV::propagate(TNode literal) { - Debug("bitvector") << spaces(getContext()->getLevel()) << "TheoryBV::propagate(" << literal << ")" << std::endl; + Debug("bitvector") << spaces(getSatContext()->getLevel()) << "TheoryBV::propagate(" << literal << ")" << std::endl; // If already in conflict, no more propagation if (d_conflict) { - Debug("bitvector") << spaces(getContext()->getLevel()) << "TheoryBV::propagate(" << literal << "): already in conflict" << std::endl; + Debug("bitvector") << spaces(getSatContext()->getLevel()) << "TheoryBV::propagate(" << literal << "): already in conflict" << std::endl; return false; } @@ -369,7 +369,7 @@ bool TheoryBV::propagate(TNode literal) // If asserted, we might be in conflict if (isAsserted) { if (!satValue) { - Debug("bitvector") << spaces(getContext()->getLevel()) << "TheoryBV::propagate(" << literal << ", normalized = " << normalized << ") => conflict" << std::endl; + Debug("bitvector") << spaces(getSatContext()->getLevel()) << "TheoryBV::propagate(" << literal << ", normalized = " << normalized << ") => conflict" << std::endl; std::vector<TNode> assumptions; Node negatedLiteral; if (normalized != d_false) { @@ -386,7 +386,7 @@ bool TheoryBV::propagate(TNode literal) } // Nothing, just enqueue it for propagation and mark it as asserted already - Debug("bitvector") << spaces(getContext()->getLevel()) << "TheoryBV::propagate(" << literal << ") => enqueuing for propagation" << std::endl; + Debug("bitvector") << spaces(getSatContext()->getLevel()) << "TheoryBV::propagate(" << literal << ") => enqueuing for propagation" << std::endl; d_literalsToPropagate.push_back(literal); return true; @@ -432,7 +432,7 @@ Node TheoryBV::explain(TNode node) { void TheoryBV::addSharedTerm(TNode t) { - Debug("bitvector::sharing") << spaces(getContext()->getLevel()) << "TheoryBV::addSharedTerm(" << t << ")" << std::endl; + Debug("bitvector::sharing") << spaces(getSatContext()->getLevel()) << "TheoryBV::addSharedTerm(" << t << ")" << std::endl; if (d_useEqualityEngine) { d_equalityEngine.addTriggerTerm(t); } diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index 940eaef56..c4953213d 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -69,7 +69,7 @@ private: public: - TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation); + TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo); ~TheoryBV(); void preRegisterTerm(TNode n); @@ -86,6 +86,7 @@ public: //Node preprocessTerm(TNode term); PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions); + private: class Statistics { @@ -107,13 +108,13 @@ private: NotifyClass(TheoryBV& uf): d_bv(uf) {} bool notify(TNode propagation) { - Debug("bitvector") << spaces(d_bv.getContext()->getLevel()) << "NotifyClass::notify(" << propagation << ")" << std::endl; + Debug("bitvector") << spaces(d_bv.getSatContext()->getLevel()) << "NotifyClass::notify(" << propagation << ")" << std::endl; // Just forward to bv return d_bv.propagate(propagation); } void notify(TNode t1, TNode t2) { - Debug("arrays") << spaces(d_bv.getContext()->getLevel()) << "NotifyClass::notify(" << t1 << ", " << t2 << ")" << std::endl; + Debug("arrays") << spaces(d_bv.getSatContext()->getLevel()) << "NotifyClass::notify(" << t1 << ", " << t2 << ")" << std::endl; // Propagate equality between shared terms Node equality = Rewriter::rewriteEquality(theory::THEORY_UF, t1.eqNode(t2)); d_bv.propagate(t1.eqNode(t2)); diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h index 5587e25eb..da3fb6554 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h +++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h @@ -384,18 +384,15 @@ Node RewriteRule<NegMult>::apply(Node node) { BVDebug("bv-rewrite") << "RewriteRule<NegMult>(" << node << ")" << std::endl; TNode mult = node[0]; std::vector<Node> children; - bool has_const = false; + BitVector bv(utils::getSize(node), (unsigned)1); for(unsigned i = 0; i < mult.getNumChildren(); ++i) { if(mult[i].getKind() == kind::CONST_BITVECTOR) { - Assert(has_const == false); - has_const = true; - BitVector bv = mult[i].getConst<BitVector>(); - children.push_back(utils::mkConst(-bv)); + bv = bv * mult[i].getConst<BitVector>(); } else { children.push_back(mult[i]); } } - Assert (has_const); + children.push_back(utils::mkConst(-bv)); return utils::mkSortedNode(kind::BITVECTOR_MULT, children); } diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h index 530949de2..490b413db 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h +++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h @@ -308,15 +308,17 @@ Node RewriteRule<XorOne>::apply(Node node) { for(unsigned i = 0; i < node.getNumChildren(); ++i) { if (node[i] == ones) { // make sure only ones occurs only once - Assert(!found_ones); - found_ones = true; + found_ones = !found_ones; } else { children.push_back(node[i]); } } - children[0] = utils::mkNode(kind::BITVECTOR_NOT, children[0]); - return utils::mkSortedNode(kind::BITVECTOR_XOR, children); + Node result = utils::mkNode(kind::BITVECTOR_XOR, children); + if (found_ones) { + result = utils::mkNode(kind::BITVECTOR_NOT, result); + } + return result; } @@ -344,16 +346,11 @@ template<> inline Node RewriteRule<XorZero>::apply(Node node) { BVDebug("bv-rewrite") << "RewriteRule<XorZero>(" << node << ")" << std::endl; std::vector<Node> children; - bool found_zero = false; Node zero = utils::mkConst(utils::getSize(node), 0); // XorSimplify should have been called before for(unsigned i = 0; i < node.getNumChildren(); ++i) { - if (node[i] == zero) { - // make sure zero occurs only once - Assert(!found_zero); - found_zero = true; - } else { + if (node[i] != zero) { children.push_back(node[i]); } } diff --git a/src/theory/bv/theory_bv_rewriter.h b/src/theory/bv/theory_bv_rewriter.h index 0ce3fa303..60715ee60 100644 --- a/src/theory/bv/theory_bv_rewriter.h +++ b/src/theory/bv/theory_bv_rewriter.h @@ -33,10 +33,7 @@ struct AllRewriteRules; typedef RewriteResponse (*RewriteFunction) (TNode, bool); class TheoryBVRewriter { - // static CVC4_THREADLOCAL(AllRewriteRules*) s_allRules; - // static CVC4_THREADLOCAL(TimerStat*) d_rewriteTimer; -#warning "TODO: Double check thread safety and make sure the fix compiles on mac." static RewriteFunction d_rewriteTable[kind::LAST_KIND]; static RewriteResponse IdentityRewrite(TNode node, bool prerewrite = false); |