diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-06-14 01:08:11 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-06-14 01:08:11 +0000 |
commit | dd713fdbc16b07adc8011dea09b53fb3bc168662 (patch) | |
tree | cc58788ed58fd86c5aaa58c0fafa2bbb0f8b6567 /src | |
parent | 1267706e0c508ada17d75c07c4606eb108ae5309 (diff) |
* removing rewriteEquality from the rewriter
* theories now get either an assertion from the SAT solver (normalized) or an (dis-)equality between two shared terms that is non-normalized
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/arith/arith_rewriter.h | 4 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays.h | 6 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays_rewriter.h | 4 | ||||
-rw-r--r-- | src/theory/booleans/theory_bool_rewriter.h | 5 | ||||
-rw-r--r-- | src/theory/builtin/theory_builtin_rewriter.h | 5 | ||||
-rw-r--r-- | src/theory/bv/bitblaster.cpp | 8 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewriter.h | 5 | ||||
-rw-r--r-- | src/theory/datatypes/datatypes_rewriter.h | 4 | ||||
-rwxr-xr-x | src/theory/mkrewriter | 6 | ||||
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.h | 3 | ||||
-rw-r--r-- | src/theory/rewriter.cpp | 9 | ||||
-rw-r--r-- | src/theory/rewriter.h | 8 | ||||
-rw-r--r-- | src/theory/rewriter_tables_template.h | 8 | ||||
-rw-r--r-- | src/theory/rewriterules/theory_rewriterules_rewriter.h | 8 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 47 | ||||
-rw-r--r-- | src/theory/uf/theory_uf_rewriter.h | 4 |
16 files changed, 35 insertions, 99 deletions
diff --git a/src/theory/arith/arith_rewriter.h b/src/theory/arith/arith_rewriter.h index 748ed8686..c32cc0e56 100644 --- a/src/theory/arith/arith_rewriter.h +++ b/src/theory/arith/arith_rewriter.h @@ -34,10 +34,6 @@ public: static RewriteResponse preRewrite(TNode n); static RewriteResponse postRewrite(TNode n); - static Node rewriteEquality(TNode equality) { - // Arithmetic owns the domain, so this is totally ok - return Rewriter::rewrite(equality); - } static void init() { } diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index 1bf42a105..25797dda3 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -271,16 +271,14 @@ class TheoryArrays : public Theory { } } // Propagate equality between shared terms - Node equality = Rewriter::rewriteEquality(theory::THEORY_UF, t1.eqNode(t2)); - return d_arrays.propagate(equality); + return d_arrays.propagate(t1.eqNode(t2)); } else { if (t1.getType().isArray()) { if (!d_arrays.isShared(t1) || !d_arrays.isShared(t2)) { return true; } } - Node equality = Rewriter::rewriteEquality(theory::THEORY_UF, t1.eqNode(t2)); - return d_arrays.propagate(equality.notNode()); + return d_arrays.propagate(t1.eqNode(t2).notNode()); } return true; } diff --git a/src/theory/arrays/theory_arrays_rewriter.h b/src/theory/arrays/theory_arrays_rewriter.h index 627f34a30..c6ef5cd25 100644 --- a/src/theory/arrays/theory_arrays_rewriter.h +++ b/src/theory/arrays/theory_arrays_rewriter.h @@ -109,10 +109,6 @@ public: return RewriteResponse(REWRITE_DONE, node); } - static Node rewriteEquality(TNode node) { - return postRewrite(node).node; - } - static inline void init() {} static inline void shutdown() {} diff --git a/src/theory/booleans/theory_bool_rewriter.h b/src/theory/booleans/theory_bool_rewriter.h index d26a4d478..6771f775c 100644 --- a/src/theory/booleans/theory_bool_rewriter.h +++ b/src/theory/booleans/theory_bool_rewriter.h @@ -37,11 +37,6 @@ public: return preRewrite(node); } - static Node rewriteEquality(TNode node) { - Unreachable(); - return node; - } - static void init() {} static void shutdown() {} diff --git a/src/theory/builtin/theory_builtin_rewriter.h b/src/theory/builtin/theory_builtin_rewriter.h index e299f84e7..acf535388 100644 --- a/src/theory/builtin/theory_builtin_rewriter.h +++ b/src/theory/builtin/theory_builtin_rewriter.h @@ -48,11 +48,6 @@ public: } } - static inline Node rewriteEquality(TNode equality) { - Unreachable(); - return equality; - } - static inline void init() {} static inline void shutdown() {} diff --git a/src/theory/bv/bitblaster.cpp b/src/theory/bv/bitblaster.cpp index 5bb906841..a9c6d2676 100644 --- a/src/theory/bv/bitblaster.cpp +++ b/src/theory/bv/bitblaster.cpp @@ -94,17 +94,15 @@ void Bitblaster::bbAtom(TNode node) { BVDebug("bitvector-bitblast") << "Bitblasting node " << node <<"\n"; ++d_statistics.d_numAtoms; // the bitblasted definition of the atom - Node atom_bb = d_atomBBStrategies[node.getKind()](node, this); + Node atom_bb = Rewriter::rewrite(d_atomBBStrategies[node.getKind()](node, this)); // asserting that the atom is true iff the definition holds Node atom_definition = mkNode(kind::IFF, node, atom_bb); - // do boolean simplifications if possible - Node rewritten = Rewriter::rewrite(atom_definition); if (!Options::current()->bitvectorEagerBitblast) { - d_cnfStream->convertAndAssert(rewritten, true, false); + d_cnfStream->convertAndAssert(atom_definition, true, false); d_bitblastedAtoms.insert(node); } else { - d_bvOutput->lemma(rewritten, false); + d_bvOutput->lemma(atom_definition, false); } } diff --git a/src/theory/bv/theory_bv_rewriter.h b/src/theory/bv/theory_bv_rewriter.h index bfd8a2897..6b885f1ed 100644 --- a/src/theory/bv/theory_bv_rewriter.h +++ b/src/theory/bv/theory_bv_rewriter.h @@ -84,11 +84,6 @@ public: static RewriteResponse preRewrite(TNode node); - static Node rewriteEquality(TNode node) { - Debug("bitvector") << "TheoryBV::rewriteEquality(" << node << ")" << std::endl; - return postRewrite(node).node; - } - static void init(); static void shutdown(); diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h index 124e6870d..ea1409108 100644 --- a/src/theory/datatypes/datatypes_rewriter.h +++ b/src/theory/datatypes/datatypes_rewriter.h @@ -108,10 +108,6 @@ public: return RewriteResponse(REWRITE_DONE, in); } - static Node rewriteEquality(TNode equality) { - return postRewrite(equality).node; - } - static inline void init() {} static inline void shutdown() {} diff --git a/src/theory/mkrewriter b/src/theory/mkrewriter index 780409d52..71a8ea097 100755 --- a/src/theory/mkrewriter +++ b/src/theory/mkrewriter @@ -47,8 +47,6 @@ post_rewrite_calls= post_rewrite_get_cache= post_rewrite_set_cache= -rewrite_equality_calls= - seen_theory=false seen_theory_builtin=false @@ -140,9 +138,6 @@ function rewriter { post_rewrite_set_cache="${post_rewrite_set_cache} case ${theory_id}: return RewriteAttibute<${theory_id}>::setPostRewriteCache(node, cache); " - rewrite_equality_calls="${rewrite_equality_calls} case ${theory_id}: return ${class}::rewriteEquality(node); -" - lineno=${BASH_LINENO[0]} check_theory_seen } @@ -235,7 +230,6 @@ for var in \ rewriter_includes \ pre_rewrite_calls \ post_rewrite_calls \ - rewrite_equality_calls \ pre_rewrite_get_cache \ post_rewrite_get_cache \ pre_rewrite_set_cache \ diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index 8c037d30b..4f51edab8 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -65,9 +65,6 @@ private: public: static RewriteResponse preRewrite(TNode in); static RewriteResponse postRewrite(TNode in); - static Node rewriteEquality(TNode equality) { - return postRewrite(equality).node; - } static inline void init() {} static inline void shutdown() {} private: diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp index e0b1458fb..8c20c84c1 100644 --- a/src/theory/rewriter.cpp +++ b/src/theory/rewriter.cpp @@ -64,15 +64,6 @@ Node Rewriter::rewrite(TNode node) { return rewriteTo(theory::Theory::theoryOf(node), node); } -Node Rewriter::rewriteEquality(theory::TheoryId theoryId, TNode node) { - Assert(node.getKind() == kind::EQUAL); - Trace("rewriter") << "Rewriter::rewriteEquality(" << theoryId << "," << node << ")"<< std::endl; - Node result = Rewriter::callRewriteEquality(theoryId, node); - Trace("rewriter") << "Rewriter::rewriteEquality(" << theoryId << "," << node << ") => " << result << std::endl; - Assert(result.getKind() == kind::EQUAL || result.isConst()); - return result; -} - Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) { #ifdef CVC4_ASSERTIONS diff --git a/src/theory/rewriter.h b/src/theory/rewriter.h index e80606c95..4169cb9fe 100644 --- a/src/theory/rewriter.h +++ b/src/theory/rewriter.h @@ -99,12 +99,6 @@ public: static Node rewrite(TNode node); /** - * Rewrite an equality between two terms that are already in normal form, so - * that the equality is in theory-normal form. - */ - static Node rewriteEquality(theory::TheoryId theoryId, TNode node); - - /** * Should be called before the rewriter gets used for the first time. */ static void init(); @@ -113,6 +107,8 @@ public: * Should be called to clean up any state. */ static void shutdown(); + + };/* class Rewriter */ }/* CVC4::theory namespace */ diff --git a/src/theory/rewriter_tables_template.h b/src/theory/rewriter_tables_template.h index cd79dcd9f..9ab98168e 100644 --- a/src/theory/rewriter_tables_template.h +++ b/src/theory/rewriter_tables_template.h @@ -45,14 +45,6 @@ ${post_rewrite_calls} } } -Node Rewriter::callRewriteEquality(theory::TheoryId theoryId, TNode node) { - switch(theoryId) { -${rewrite_equality_calls} - default: - Unreachable(); - } -} - Node Rewriter::getPreRewriteCache(theory::TheoryId theoryId, TNode node) { switch(theoryId) { ${pre_rewrite_get_cache} diff --git a/src/theory/rewriterules/theory_rewriterules_rewriter.h b/src/theory/rewriterules/theory_rewriterules_rewriter.h index d9da095f7..3d01dc2a5 100644 --- a/src/theory/rewriterules/theory_rewriterules_rewriter.h +++ b/src/theory/rewriterules/theory_rewriterules_rewriter.h @@ -57,14 +57,6 @@ public: } /** - * Rewrite an equality, in case special handling is required. - */ - static Node rewriteEquality(TNode equality) { - // often this will suffice - return postRewrite(equality).node; - } - - /** * Initialize the rewriter. */ static inline void init() { diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 8abc7a0e3..060d48230 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -394,7 +394,9 @@ void TheoryEngine::combineTheories() { Assert(!d_sharedTerms.areDisequal(carePair.a, carePair.b), "Please don't care about stuff you were notified about"); // The equality in question - Node equality = Rewriter::rewriteEquality(carePair.theory, carePair.a.eqNode(carePair.b)); + Node equality = carePair.a < carePair.b ? + carePair.a.eqNode(carePair.b) : + carePair.b.eqNode(carePair.a); // Normalize the equality Node normalizedEquality = Rewriter::rewrite(equality); @@ -862,33 +864,41 @@ void TheoryEngine::assertToTheory(TNode assertion, theory::TheoryId toTheoryId, } return; } - - // We are left with internal distribution of shared literals - Assert(atom.getKind() == kind::EQUAL); - Node normalizedAtom = Rewriter::rewriteEquality(toTheoryId, atom); - Node normalizedAssertion = polarity ? normalizedAtom : normalizedAtom.notNode(); - - // If we normalize to true or false, it's a special case - if (normalizedAtom.isConst()) { - if (polarity == normalizedAtom.getConst<bool>()) { - // Trivially true, just ignore - return; + + // See if it rewrites to true or false directly + Node normalizedLiteral = Rewriter::rewrite(assertion); + if (normalizedLiteral.isConst()) { + if (normalizedLiteral.getConst<bool>()) { + // trivially true, but theories need to share even trivially true facts + // unless of course it is the theory that normalized it + if (Theory::theoryOf(atom) == toTheoryId) { + return; + } } else { // Mark the propagation for explanations - if (markPropagation(normalizedAssertion, assertion, toTheoryId, fromTheoryId)) { + if (markPropagation(normalizedLiteral, assertion, toTheoryId, fromTheoryId)) { // Get the explanation (conflict will figure out where it came from) - conflict(normalizedAssertion, toTheoryId); + conflict(normalizedLiteral, toTheoryId); } else { Unreachable(); } return; } } - - // Try and assert + + // Normalize to lhs < rhs + Assert(atom.getKind() == kind::EQUAL); + Assert(atom[0] != atom[1]); + Node normalizedAtom = atom; + if (atom[0] > atom[1]) { + normalizedAtom = atom[1].eqNode(atom[0]); + } + Node normalizedAssertion = polarity ? normalizedAtom : normalizedAtom.notNode(); + + // Try and assert (note that we assert the non-normalized one) if (markPropagation(normalizedAssertion, assertion, toTheoryId, fromTheoryId)) { // Check if has been pre-registered with the theory - bool preregistered = d_propEngine->isSatLiteral(normalizedAssertion) && Theory::theoryOf(normalizedAtom) == toTheoryId; + bool preregistered = d_propEngine->isSatLiteral(normalizedAssertion) && Theory::theoryOf(normalizedAssertion) == toTheoryId; // Assert away theoryOf(toTheoryId)->assertFact(normalizedAssertion, preregistered); d_factsAsserted = true; @@ -1139,9 +1149,8 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) { Assert(properConflict(fullConflict)); lemma(fullConflict, true, true); } else { - Debug("theory::conflict") << "TheoryEngine::conflict(" << conflict << ", " << theoryId << "):" << std::endl; - // When only one theory, the conflict should need no processing + Debug("theory::conflict") << "TheoryEngine::conflict(" << conflict << ", " << theoryId << ")" << std::endl; Assert(properConflict(conflict)); lemma(conflict, true, true); } diff --git a/src/theory/uf/theory_uf_rewriter.h b/src/theory/uf/theory_uf_rewriter.h index be4906ab6..8ba39f372 100644 --- a/src/theory/uf/theory_uf_rewriter.h +++ b/src/theory/uf/theory_uf_rewriter.h @@ -54,10 +54,6 @@ public: return RewriteResponse(REWRITE_DONE, node); } - static Node rewriteEquality(TNode equality) { - return postRewrite(equality).node; - } - static inline void init() {} static inline void shutdown() {} |