From 42794501e81c44dce5c2f7687af288af030ef63e Mon Sep 17 00:00:00 2001 From: Clark Barrett Date: Mon, 11 Jun 2012 16:14:01 +0000 Subject: [PATCH] Fix for array bug with decision heuristic Also fixed one bv rewrite failure (more to come) --- src/theory/arrays/theory_arrays.cpp | 32 +++++++++++++++++----------- src/theory/arrays/theory_arrays.h | 3 ++- src/theory/bv/theory_bv_rewriter.cpp | 10 +++++---- src/theory/rewriter.cpp | 2 ++ 4 files changed, 29 insertions(+), 18 deletions(-) diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 91bbae2f4..81661acd1 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -71,6 +71,7 @@ TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputC d_RowQueue(c), d_RowAlreadyAdded(u), d_sharedArrays(c), + d_sharedOther(c), d_sharedTerms(c, false), d_reads(c), d_permRef(c) @@ -481,9 +482,12 @@ void TheoryArrays::addSharedTerm(TNode t) { Debug("arrays::sharing") << spaces(getSatContext()->getLevel()) << "TheoryArrays::addSharedTerm(" << t << ")" << std::endl; d_equalityEngine.addTriggerTerm(t, THEORY_ARRAY); if (t.getType().isArray()) { - d_sharedArrays.insert(t,true); + d_sharedArrays.insert(t); } else { +#ifdef CVC4_ASSERTIONS + d_sharedOther.insert(t); +#endif d_sharedTerms = true; } } @@ -507,18 +511,18 @@ EqualityStatus TheoryArrays::getEqualityStatus(TNode a, TNode b) { void TheoryArrays::computeCareGraph() { if (d_sharedArrays.size() > 0) { - context::CDHashMap::iterator it1 = d_sharedArrays.begin(), it2, iend = d_sharedArrays.end(); + context::CDHashSet::iterator it1 = d_sharedArrays.begin(), it2, iend = d_sharedArrays.end(); for (; it1 != iend; ++it1) { for (it2 = it1, ++it2; it2 != iend; ++it2) { - if ((*it1).first.getType() != (*it2).first.getType()) { + if ((*it1).getType() != (*it2).getType()) { continue; } - EqualityStatus eqStatusArr = getEqualityStatus((*it1).first, (*it2).first); + EqualityStatus eqStatusArr = getEqualityStatus((*it1), (*it2)); if (eqStatusArr != EQUALITY_UNKNOWN) { continue; } - Assert(d_valuation.getEqualityStatus((*it1).first, (*it2).first) == EQUALITY_UNKNOWN); - addCarePair((*it1).first, (*it2).first); + Assert(d_valuation.getEqualityStatus((*it1), (*it2)) == EQUALITY_UNKNOWN); + addCarePair((*it1), (*it2)); ++d_numSharedArrayVarSplits; return; } @@ -533,6 +537,11 @@ void TheoryArrays::computeCareGraph() for (unsigned i = 0; i < size; ++ i) { TNode r1 = d_reads[i]; + // Make sure shared terms were identified correctly + Assert(theoryOf(r1[0]) == THEORY_ARRAY || isShared(r1[0])); + Assert(theoryOf(r1[1]) == THEORY_ARRAY || + d_sharedOther.find(r1[1]) != d_sharedOther.end()); + for (unsigned j = i + 1; j < size; ++ j) { TNode r2 = d_reads[j]; @@ -707,13 +716,10 @@ void TheoryArrays::check(Effort e) { Node ak = nm->mkNode(kind::SELECT, fact[0][0], k); Node bk = nm->mkNode(kind::SELECT, fact[0][1], k); - if (!d_equalityEngine.hasTerm(ak)) { - preRegisterTerm(ak); - } - if (!d_equalityEngine.hasTerm(bk)) { - preRegisterTerm(bk); - } - d_equalityEngine.assertEquality(ak.eqNode(bk), false, fact); + Node eq = d_valuation.ensureLiteral(ak.eqNode(bk)); + Assert(eq.getKind() == kind::EQUAL); + d_equalityEngine.assertEquality(eq, false, fact); + propagate(eq.notNode()); Trace("arrays-lem")<<"Arrays::addExtLemma "<< ak << " /= " << bk <<"\n"; ++d_numExt; } diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index 54d20d478..80fe692c0 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -305,7 +305,8 @@ class TheoryArrays : public Theory { context::CDQueue d_RowQueue; context::CDHashSet d_RowAlreadyAdded; - context::CDHashMap d_sharedArrays; + context::CDHashSet d_sharedArrays; + context::CDHashSet d_sharedOther; context::CDO d_sharedTerms; context::CDList d_reads; std::hash_map d_diseqCache; diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp index 47725444d..85ccbc787 100644 --- a/src/theory/bv/theory_bv_rewriter.cpp +++ b/src/theory/bv/theory_bv_rewriter.cpp @@ -521,10 +521,6 @@ RewriteResponse TheoryBVRewriter::RewriteEqual(TNode node, bool preregister) { >::apply(node); return RewriteResponse(REWRITE_DONE, resultNode); } - else if(RewriteRule::applies(node)) { - Node resultNode = RewriteRule::run(node); - return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); - } else { Node resultNode = LinearRewriteStrategy < RewriteRule, @@ -532,6 +528,12 @@ RewriteResponse TheoryBVRewriter::RewriteEqual(TNode node, bool preregister) { RewriteRule, RewriteRule >::apply(node); + + if(RewriteRule::applies(resultNode)) { + resultNode = RewriteRule::run(resultNode); + return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); + } + return RewriteResponse(REWRITE_DONE, resultNode); } } diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp index 18274e060..7d5f541c0 100644 --- a/src/theory/rewriter.cpp +++ b/src/theory/rewriter.cpp @@ -173,6 +173,8 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) { rewriteStackTop.node = response.node; break; } + // Check for trivial rewrite loop of size 2 + Assert(Rewriter::callPostRewrite((TheoryId) rewriteStackTop.theoryId, response.node).node != rewriteStackTop.node); rewriteStackTop.node = response.node; } // We're done with the post rewrite, so we add to the cache -- 2.30.2