summaryrefslogtreecommitdiff
path: root/src/util/ite_removal.h
AgeCommit message (Collapse)Author
2013-04-01update copyrightsMorgan Deters
2013-03-11ite removal option for quantifiers --ite-remove-quant, e-matching for ↵Andrew Reynolds
boolean terms, improvement for pre skolemization
2012-10-11Standardizing copyright notice. Touches **ALL** sources, guys, sorry.. it'sMorgan Deters
just the header comments at the top, though. Don't update to this rev if you don't have time for a complete rebuild, and exclude this rev if you want to see what's new across a range of commits. (this commit was certified error- and warning-free by the test-and-commit script.)
2012-10-05Bug-related:Morgan Deters
* ITE removal fixed to be context-dependent (on UserContext). Resolves incrementality bugs 376 and 396 (which had given wrong answers). * some bugfixes for incrementality that Dejan found (fixes bug 394) * fix for bug in SmtEngine::getValue() where definitions weren't respected (partially resolves bug 411, but get-model is still broken). * change status of microwave21.ec.minimized.smt2 (it's actually unsat, but was labeled sat); re-enable it for "make regress" Also: * --check-model doesn't fail if quantified assertions don't simplify away. * fix some examples, and the Java system test, for the disappearance of the BoolExpr class * add copy constructor to array type enumerator (the type enumerator framework requires copy ctors, and the automatically-generated copy ctor was copying pointers that were then deleted, leaving dangling pointers in the copy and causing segfaults) * --dump=assertions now implies --dump=skolems * --dump=assertions:pre-<PASS> and --dump=assertions:post-<PASS> now allow you to dump before/after a particular preprocessing pass. E.g., --dump=assertions:pre-ite-removal or --dump=assertions:post-static-learning. "--dump=assertions" by itself is after all preprocessing, just before CNF conversion. * minor fixes to dumping output * include Model in language bindings Minor refactoring/misc: * fix compiler warning in src/theory/model.cpp * remove unnecessary SmtEngine::printModel(). * mkoptions script doesn't give progress output if stdout isn't a terminal (e.g., if it's written to a log, or piped through less(1), or whatever). * add some type enumerator unit tests * de-emphasize --parse-only and --preprocess-only (they aren't really "common" options) * fix some exception throw() specifications in SmtEngine * minor documentation clarifications
2012-05-09Merge from decision branch (ITE support)Kshitij Bansal
Major changes from last merge * ITEs supported * Don't share theory lemmas to DE, only assertions Should probably be noted that 'make regress' doesn't quite pass with --decision=justification. Throws off search in couple of arith benchmarks. No serious performance changes expected. Keep an eye.
2012-04-30Added map from skolem variables to new ite formulas in ite removal.Clark Barrett
d_sharedTermsExist is now set based on logicInfo instead of dynamically when shared terms are found.
2012-03-09Some work on the dump infrastructure to support portfolio work.Morgan Deters
Dump("foo") << FooCommand(...); now "dumps" the textual representation of the command (in the current output language) to a file, IF dumping is on at configure-time, AND the "muzzle" feature is off, AND the "foo" flag is turned on for the dump stream during this run. If it's a portfolio build, the above will also store the command in a CommandSequence, IF the "foo" flag is turned on for the dump stream during this run. This is done even if the muzzle is on. This commit also cleans up some code that used the dump feature (in arrays, particularly).
2011-09-28variety of visibility fixes (should clean up some of the many warnings on ↵Morgan Deters
MacOS-production-dynamic builds)
2011-09-02Merge from my post-smtcomp branch. Includes:Morgan Deters
Dumping infrastructure. Can dump preprocessed queries and clauses. Can also dump queries (for testing with another solver) to see if any conflicts are missed, T-propagations are missed, all lemmas are T-valid, etc. For a full list of options see --dump=help. CUDD building much cleaner. Documentation and assertion fixes. Printer improvements, printing of commands in language-defined way, etc. Typechecker stuff in expr package now autogenerated, no need to manually edit the expr package when adding a new theory. CVC3 compatibility layer (builds as libcompat). SWIG detection and language binding support (infrastructure). Support for some Z3 extended commands (like datatypes) in SMT-LIBv2 mode (when not in compliance mode). Copyright and file headers regenerated.
2011-07-05updated preprocessing and rewriting input equalities into inequalities for LRADejan Jovanović
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback