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/smt/smt_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/smt/smt_engine.cpp')
| -rw-r--r-- | src/smt/smt_engine.cpp | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index a80177429..86b0faaf6 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1029,7 +1029,10 @@ void SmtEngine::setDefaults() { // Set the options for the theoryOf if(!options::theoryOfMode.wasSetByUser()) { - if(d_logic.isSharingEnabled() && !d_logic.isTheoryEnabled(THEORY_BV) && !d_logic.isTheoryEnabled(THEORY_STRINGS)) { + if(d_logic.isSharingEnabled() && + !d_logic.isTheoryEnabled(THEORY_BV) && + !d_logic.isTheoryEnabled(THEORY_STRINGS) && + !d_logic.isTheoryEnabled(THEORY_SETS) ) { Trace("smt") << "setting theoryof-mode to term-based" << endl; options::theoryOfMode.set(THEORY_OF_TERM_BASED); } @@ -1057,7 +1060,10 @@ void SmtEngine::setDefaults() { } else { Theory::setUninterpretedSortOwner(THEORY_UF); } + // Turn on ite simplification for QF_LIA and QF_AUFBV + // WARNING: These checks match much more than just QF_AUFBV and + // QF_LIA logics. --K [2014/10/15] if(! options::doITESimp.wasSetByUser()) { bool qf_aufbv = !d_logic.isQuantified() && d_logic.isTheoryEnabled(THEORY_ARRAY) && |