Set Constant's normal form and other short fixes
authorKshitij Bansal <kshitij@cs.nyu.edu>
Mon, 10 Nov 2014 18:11:20 +0000 (13:11 -0500)
committerKshitij Bansal <kshitij@cs.nyu.edu>
Wed, 19 Nov 2014 01:29:45 +0000 (20:29 -0500)
commit07a2c86207758b504ed744840990ff143ffc7af7
treeaf4b7db21c71fee5ef4a2e79b50e670fb125d0d5
parentfb6326517ce661d4d9bb1c593cce2a8b91eb51b3
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!
src/smt/smt_engine.cpp
src/theory/sets/normal_form.h
src/theory/sets/theory_sets_private.cpp
src/theory/sets/theory_sets_private.h
src/theory/sets/theory_sets_rewriter.cpp
src/theory/sets/theory_sets_type_enumerator.h
src/theory/sets/theory_sets_type_rules.h
src/theory/theory_engine.cpp