diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-12-10 07:02:21 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-12-10 07:02:21 +0000 |
commit | 3fd65ea9f5b5cdb2fe4b511b76abcad89e1cd71d (patch) | |
tree | 02ed170f72d4b48fe158da051e86bf1567f46469 /src/theory | |
parent | 48b147577ba6a894f8f0498c39c7e77d466b0538 (diff) |
a bit more changes, when propagting equalities/dis-equalities don't assert them to theories that rewrite them to true. for example, 1 != 0 rewrites to true, so it shouldn't get propagated to arithmetic.
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/theory_engine.cpp | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index aa897b244..5ef7480e8 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -590,10 +590,14 @@ void TheoryEngine::propagate(TNode literal, theory::TheoryId theory) { if (Theory::setContains(currentTheory, lhsNotified) && Theory::setContains(currentTheory, rhsNotified)) { // Normalize the equality Node equality = Rewriter::rewriteEquality(currentTheory, atom); - // The assertion - Node assertion = negated ? equality.notNode() : equality; - // Remember it to assert later - d_propagatedEqualities.push_back(SharedEquality(assertion, literal, theory, currentTheory)); + if (equality.getKind() != kind::CONST_BOOLEAN) { + // The assertion + Node assertion = negated ? equality.notNode() : equality; + // Remember it to assert later + d_propagatedEqualities.push_back(SharedEquality(assertion, literal, theory, currentTheory)); + } else { + Assert(negated || equality.getConst<bool>()); + } } } } |