diff options
| author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-05-27 05:44:13 +0000 |
|---|---|---|
| committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-05-27 05:44:13 +0000 |
| commit | b390cfa8f095048472cb3dd0b9ccc22fbd51f411 (patch) | |
| tree | de6d485b9b164806f408d714cd50e7da7db5da6c /src/theory/shared_terms_database.cpp | |
| parent | 28096861af9b01e4bad6059346446d97b9708cb7 (diff) | |
Committing the work on equality engine, I need to see how it does on the regressions. New additions:
* areDisequal(x, y) -> areDisequal(x, y, needProof): when asking for a disequality you must say needProof if you will ask for an explanation later.
* propagation of shared dis-equalities (not yet complete, once case missing)
* changes to the theories that use it, authors should check up on the changes
Diffstat (limited to 'src/theory/shared_terms_database.cpp')
| -rw-r--r-- | src/theory/shared_terms_database.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/shared_terms_database.cpp b/src/theory/shared_terms_database.cpp index 90037b90b..0c893482a 100644 --- a/src/theory/shared_terms_database.cpp +++ b/src/theory/shared_terms_database.cpp @@ -297,7 +297,7 @@ bool SharedTermsDatabase::areEqual(TNode a, TNode b) { bool SharedTermsDatabase::areDisequal(TNode a, TNode b) { - return d_equalityEngine.areDisequal(a,b); + return d_equalityEngine.areDisequal(a,b,false); } void SharedTermsDatabase::processSharedLiteral(TNode literal, TNode reason) @@ -305,7 +305,7 @@ void SharedTermsDatabase::processSharedLiteral(TNode literal, TNode reason) bool negated = literal.getKind() == kind::NOT; TNode atom = negated ? literal[0] : literal; if (negated) { - Assert(!d_equalityEngine.areDisequal(atom[0], atom[1])); + Assert(!d_equalityEngine.areDisequal(atom[0], atom[1],false)); d_equalityEngine.assertEquality(atom, false, reason); // !!! need to send this out } |