diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-02-21 19:43:46 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-02-21 19:43:46 +0000 |
commit | f52bee51e20b0670f9a2bd13ae2fdefd5eba1546 (patch) | |
tree | e77af4a3fd4bd726d1f9ed1215fccf5aad1c50f2 /src/theory/theory_engine.cpp | |
parent | 9dcfc2fdc58bf46a434f9c228a828be8d580f529 (diff) |
Fix for bug303. The problem was with function applications that get normalized when added to the term database. For example, if x=y exists, and the term f(x) is added, f(y) was stored. So, when getExplanation(f(x), f(y)) was called, trouble ensued. I now keep the original version so that explanations can be properly produced.
Also added theory::assertions debug flag that will printout assertions of each theory for ease and uniformity of debugging in the future.
Diffstat (limited to 'src/theory/theory_engine.cpp')
-rw-r--r-- | src/theory/theory_engine.cpp | 27 |
1 files changed, 27 insertions, 0 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index e21e83671..75c64654d 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -133,6 +133,33 @@ void TheoryEngine::check(Theory::Effort effort) { Debug("theory") << "TheoryEngine::check(" << effort << "): running check" << std::endl; + if (Debug.isOn("theory::assertions")) { + for (unsigned theoryId = 0; theoryId < THEORY_LAST; ++ theoryId) { + Theory* theory = d_theoryTable[theoryId]; + if (theory && Theory::setContains((TheoryId)theoryId, d_activeTheories)) { + Debug("theory::assertions") << "--------------------------------------------" << std::endl; + Debug("theory::assertions") << "Assertions of " << theory->getId() << ": " << std::endl; + context::CDList<Assertion>::const_iterator it = theory->facts_begin(), it_end = theory->facts_end(); + for (unsigned i = 0; it != it_end; ++ it, ++i) { + if ((*it).isPreregistered) { + Debug("theory::assertions") << "[" << i << "]: "; + } else { + Debug("theory::assertions") << "(" << i << "): "; + } + Debug("theory::assertions") << (*it).assertion << endl; + } + + if (d_sharedTermsExist) { + Debug("theory::assertions") << "Shared terms of " << theory->getId() << ": " << std::endl; + context::CDList<TNode>::const_iterator it = theory->shared_terms_begin(), it_end = theory->shared_terms_end(); + for (unsigned i = 0; it != it_end; ++ it, ++i) { + Debug("theory::assertions") << "[" << i << "]: " << (*it) << endl; + } + } + } + } + } + // Do the checking CVC4_FOR_EACH_THEORY; |