diff options
author | Tim King <taking@cs.nyu.edu> | 2011-12-15 20:39:20 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2011-12-15 20:39:20 +0000 |
commit | 9bcda83d2d322a97b5896ce160c298f6a159a2d2 (patch) | |
tree | 0004a4ad7f84c996230ad168a9ca73c20018a374 /src | |
parent | e85f690a704a4182a8ffc8b96cff71737f5c0904 (diff) |
Partial fix in arithmetic for propagating shared terms. This partially resolves bug 289. Adds failing tests to regress1.
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/arith/theory_arith.cpp | 38 |
1 files changed, 36 insertions, 2 deletions
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 53559d949..dfd82b960 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -889,6 +889,24 @@ Node TheoryArith::explain(TNode n) { } } +void flattenAnd(Node n, std::vector<TNode>& out){ + Assert(n.getKind() == kind::AND); + for(Node::iterator i=n.begin(), i_end=n.end(); i != i_end; ++i){ + Node curr = *i; + if(curr.getKind() == kind::AND){ + flattenAnd(curr, out); + }else{ + out.push_back(curr); + } + } +} + +Node flattenAnd(Node n){ + std::vector<TNode> out; + flattenAnd(n, out); + return NodeManager::currentNM()->mkNode(kind::AND, out); +} + void TheoryArith::propagate(Effort e) { if(quickCheckOrMore(e)){ bool propagated = false; @@ -910,8 +928,24 @@ void TheoryArith::propagate(Effort e) { if(flag) { //Currently if the flag is set this came from an equality detected by the //equality engine in the the difference manager. - d_out->propagate(toProp); - propagated = true; + if(toProp.getKind() == kind::EQUAL){ + Node normalized = Rewriter::rewrite(toProp); + Node notNormalized = normalized.notNode(); + + if(d_diseq.find(notNormalized) == d_diseq.end()){ + d_out->propagate(toProp); + propagated = true; + }else{ + Node exp = d_differenceManager.explain(toProp); + Node lp = flattenAnd(exp.andNode(exp)); + d_out->conflict(exp); + propagated = true; + break; + } + }else{ + d_out->propagate(toProp); + propagated = true; + } }else if(inContextAtom(atom)){ Node satValue = d_valuation.getSatValue(toProp); AlwaysAssert(satValue.isNull()); |