diff options
author | Tim King <taking@cs.nyu.edu> | 2010-03-08 21:29:50 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2010-03-08 21:29:50 +0000 |
commit | 1596c6b8205ca706f56c0e544bd49ba7cfab6e51 (patch) | |
tree | 0b600d02c68269df4db16a0028f547577f565129 /src/theory/uf/theory_uf.cpp | |
parent | b1d9707979074abb8fed7ad4e8a2b15648c69324 (diff) |
Improved output for theory uf
Diffstat (limited to 'src/theory/uf/theory_uf.cpp')
-rw-r--r-- | src/theory/uf/theory_uf.cpp | 39 |
1 files changed, 35 insertions, 4 deletions
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index b4597c7c7..111f06fe9 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -38,14 +38,20 @@ TheoryUF::TheoryUF(Context* c, OutputChannel& out) : TheoryUF::~TheoryUF(){} void TheoryUF::preRegisterTerm(TNode n){ + Debug("uf") << "uf: begin preRegisterTerm(" << n << ")" << std::endl; + Debug("uf") << "uf: end preRegisterTerm(" << n << ")" << std::endl; } void TheoryUF::registerTerm(TNode n){ + Debug("uf") << "uf: begin registerTerm(" << n << ")" << std::endl; + n.printAst(Debug("uf")); + + d_registered.push_back(n); -#ifdef CVC4_DEBUG - n.printAst(Warning()); -#endif /* CVC4_DEBUG */ + + + ECData* ecN; @@ -132,6 +138,7 @@ void TheoryUF::registerTerm(TNode n){ ecChild->addPredecessor(n, d_context); } } + Debug("uf") << "uf: end registerTerm(" << n << ")" << std::endl; } @@ -238,20 +245,41 @@ void TheoryUF::merge(){ if(ecX == ecY) continue; + Debug("uf") << "merging equivalence classes for " << std::endl; + Debug("uf") << "left equivalence class :"; + (ecX->getRep()).printAst(Debug("uf")); + Debug("uf") << "right equivalence class :"; + (ecY->getRep()).printAst(Debug("uf")); + + ccUnion(ecX, ecY); } } Node TheoryUF::constructConflict(TNode diseq){ + Debug("uf") << "uf: begin constructConflict()" << std::endl; + NodeBuilder<> nb(kind::AND); nb << diseq; for(unsigned i=0; i<d_assertions.size(); ++i) nb << d_assertions[i]; - return nb; + Node conflict = nb; + + + Debug("uf") << "conflict constructed : "; + conflict.printAst(Debug("uf")); + Debug("uf") << std::endl; + + Debug("uf") << "uf: ending constructConflict()" << std::endl; + + return conflict; } void TheoryUF::check(Effort level){ + + Debug("uf") << "uf: begin check(" << level << ")" << std::endl; + while(!done()){ Node assertion = get(); @@ -288,4 +316,7 @@ void TheoryUF::check(Effort level){ } } } + + Debug("uf") << "uf: end check(" << level << ")" << std::endl; + } |