diff options
| author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-05-16 17:53:41 +0000 |
|---|---|---|
| committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-05-16 17:53:41 +0000 |
| commit | 5ec347a55a3b32e9d92d8a6a5d683cb9f3f3fee5 (patch) | |
| tree | 871a53d147d218f926d53421b48db872c9d6747d /src/theory/term_registration_visitor.cpp | |
| parent | 9154e647013e4575f60807d5b73582bccfd052e2 (diff) | |
Changes to SAT solver:
* allowing propagation of false literals (handles conflict)
* allowing lemmas during BCP (bug 337)
* UF does direct propagation, without checking for literal value anymore
Diffstat (limited to 'src/theory/term_registration_visitor.cpp')
| -rw-r--r-- | src/theory/term_registration_visitor.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp index 4a2a5f135..e1ef51d09 100644 --- a/src/theory/term_registration_visitor.cpp +++ b/src/theory/term_registration_visitor.cpp @@ -30,7 +30,7 @@ std::string PreRegisterVisitor::toString() const { bool PreRegisterVisitor::alreadyVisited(TNode current, TNode parent) { - Debug("register::internal") << "PreRegisterVisitor::alreadyVisited(" << current << "," << parent << ") => "; + Debug("register::internal") << "PreRegisterVisitor::alreadyVisited(" << current << "," << parent << ")" << std::endl; TheoryId currentTheoryId = Theory::theoryOf(current); @@ -134,7 +134,7 @@ std::string SharedTermsVisitor::toString() const { bool SharedTermsVisitor::alreadyVisited(TNode current, TNode parent) const { - Debug("register::internal") << "SharedTermsVisitor::alreadyVisited(" << current << "," << parent << ") => "; + Debug("register::internal") << "SharedTermsVisitor::alreadyVisited(" << current << "," << parent << ")" << std::endl; TNodeVisitedMap::const_iterator find = d_visited.find(current); |