diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-11-10 13:11:20 -0500 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-11-18 20:29:45 -0500 |
commit | 07a2c86207758b504ed744840990ff143ffc7af7 (patch) | |
tree | af4b7db21c71fee5ef4a2e79b50e670fb125d0d5 /src/theory/theory_engine.cpp | |
parent | fb6326517ce661d4d9bb1c593cce2a8b91eb51b3 (diff) |
Set Constant's normal form and other short fixes
Other short fixes:
* use debug tag "theory::assertions::fulleffort" to dump assertions only at FULL_EFFORT
* theoryof-mode fix in smt_engine.cpp
* hack in TheoryModel::getModelValue [TODO: notify Clark/Andy]
* Lemma generation when it rewrites to true/false fix
* TermInfoManager::addTerm(..) fix
* Move SUBSET rewrite to preRewrite
* On preRegister, queue up propagation to be done upfront
** Hospital4 fails when all other fixes have been applied but not this one. Good to have an actual benchmark which relies on this code.
* TheorySetsProperties::getCardinality(..) fix
Thanks to Alvise Rabitti and Stefano Calzavara for reporting some of these; and to Morgan and Clark for help in fixing!
Diffstat (limited to 'src/theory/theory_engine.cpp')
-rw-r--r-- | src/theory/theory_engine.cpp | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index d83626a6b..9d91c096a 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -379,6 +379,13 @@ void TheoryEngine::check(Theory::Effort effort) { printAssertions("theory::assertions"); } + if(Theory::fullEffort(effort)) { + Trace("theory::assertions::fulleffort") << endl; + if (Trace.isOn("theory::assertions::fulleffort")) { + printAssertions("theory::assertions::fulleffort"); + } + } + // Note that we've discharged all the facts d_factsAsserted = false; @@ -1194,6 +1201,7 @@ theory::EqualityStatus TheoryEngine::getEqualityStatus(TNode a, TNode b) { } Node TheoryEngine::getModelValue(TNode var) { + if(var.isConst()) return var; // FIXME: HACK!!! Assert(d_sharedTerms.isShared(var)); return theoryOf(Theory::theoryOf(var.getType()))->getModelValue(var); } |