diff options
| author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-03-08 23:03:48 +0000 |
|---|---|---|
| committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-03-08 23:03:48 +0000 |
| commit | de0160112edbed8ce9b62bf87172ae2f0e99a013 (patch) | |
| tree | c9fc1e4b7f365dbd34a79b8360f3ac8a006aad68 /src/theory/theory.h | |
| parent | fc810750142ee15917c6d77d21d987c369ce774b (diff) | |
adding simple-uf to the regressions, and the code that apparently solves it
Diffstat (limited to 'src/theory/theory.h')
| -rw-r--r-- | src/theory/theory.h | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/theory/theory.h b/src/theory/theory.h index 86badb9bd..83082ff5d 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -169,6 +169,7 @@ public: * Assert a fact in the current context. */ void assertFact(TNode n) { + Debug("theory") << "Theory::assertFact(" << n << ")" << std::endl; d_facts.push(n); } @@ -293,10 +294,14 @@ Node TheoryImpl<T>::get() { Node fact = d_facts.front(); d_facts.pop(); + Debug("theory") << "Theory::get() => " << fact << "(" << d_facts.size() << " left)" << std::endl; + if(! fact.getAttribute(RegisteredAttr())) { std::list<TNode> toReg; toReg.push_back(fact); + Debug("theory") << "Theory::get(): registering new atom" << std::endl; + /* Essentially this is doing a breadth-first numbering of * non-registered subterms with children. Any non-registered * leaves are immediately registered. */ |