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/term_registration_visitor.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/term_registration_visitor.cpp')
| -rw-r--r-- | src/theory/term_registration_visitor.cpp | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/src/theory/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp index 099871ceb..22b87c32f 100644 --- a/src/theory/term_registration_visitor.cpp +++ b/src/theory/term_registration_visitor.cpp @@ -32,7 +32,6 @@ bool PreRegisterVisitor::alreadyVisited(TNode current, TNode parent) { Debug("register::internal") << "PreRegisterVisitor::alreadyVisited(" << current << "," << parent << ")" << std::endl; - TheoryId currentTheoryId = Theory::theoryOf(current); TheoryId parentTheoryId = Theory::theoryOf(parent); |