Age | Commit message (Collapse) | Author | |
---|---|---|---|
2013-04-02 | Regenerated copyrights: canonicalized names, no emails | Morgan Deters | |
2013-04-01 | update copyrights | Morgan Deters | |
2013-04-01 | Fix regression error by turning off model-based solver when models are on | Clark Barrett | |
(ironic, yes, but model-based solver doesn't yet produce models) | |||
2013-04-01 | Turning on model based array solver for QF_AX | Clark Barrett | |
2013-04-01 | Made eager lemmas an option, enabled for QF_AX | Clark Barrett | |
2013-04-01 | Disabling eager array index splitting for QF_AX | Clark Barrett | |
2013-04-01 | Fixes for two bugs: | Morgan Deters | |
* one that Tim found in model generation for records containing Booleans * another that the fuzzer found in quantifiers + check-models Test cases enabled/added for both. | |||
2013-04-01 | Merging some cleanup work: | Morgan Deters | |
* Comment cleanup * Spelling fixes * Fix warnings * Documentation updates * References in docs to cryptominisat removed * Unneeded scope resolutions removed * Old, unused regression removed | |||
2013-04-01 | Fix bug 491 and related issues with checkModel() and quantifiers. Enabling ↵ | Morgan Deters | |
previously-failing testcase. | |||
2013-03-30 | Disabling eager array index splitting for QF_AUFLIA | Clark Barrett | |
Minor changes to model-based array solver | |||
2013-03-29 | make Boolean term conversion partially non-recursive (resolves bug 501) | Morgan Deters | |
2013-03-26 | Fixes for warnings from clang++, from -std=gnu++0x, from swig, and from javac | Morgan Deters | |
2013-03-22 | Support for Boolean term conversion in datatypes. | Morgan Deters | |
2013-03-21 | Some model and printing fixes for defined functions in input. | Morgan Deters | |
2013-03-21 | Fix for SmtEngine::expandDefinitions()---improper TypeCheckingException | Morgan Deters | |
2013-03-20 | Some statistics for narrowing down incrementality issues (push/pop vs solve ↵ | Morgan Deters | |
timing) | |||
2013-03-19 | Fixes for miplib-trick application (and a new testcase) | Morgan Deters | |
2013-03-15 | Boolean terms rewriting for quantified variables of type Bool, when ↵ | Morgan Deters | |
quantifier body uses them in term context | |||
2013-03-14 | Merge branch '1.0.x' | Morgan Deters | |
2013-03-14 | fix to build system: #include the proper file when they are in both builds ↵ | Morgan Deters | |
and src | |||
2013-03-11 | ite removal option for quantifiers --ite-remove-quant, e-matching for ↵ | Andrew Reynolds | |
boolean terms, improvement for pre skolemization | |||
2013-03-05 | Merge branch '1.0.x' | Morgan Deters | |
Conflicts: src/smt/smt_engine.cpp | |||
2013-03-05 | Bugfix for SmtEngine: proper unsubscribing for NodeManager events | Morgan Deters | |
2013-03-01 | Merge branch '1.0.x' | Morgan Deters | |
2013-02-26 | Fix for quantifiers containing Boolean terms. | Morgan Deters | |
2013-02-24 | added option --model-u-dt-enum for outputting uninterpreted sorts as ↵ | Andrew Reynolds | |
datatype enumerations + minor update to array rewriter to improve output for this option, minor refactoring of representative selection for quantifier instantiation, initial draft of disequality propagation option --uf-ss-deq-prop, other refactoring of uf strong solver, fixed bug 496, improvement for fmf enumeration of finite built-in sorts | |||
2013-02-20 | Some exception specification fixes in SmtEngine/Command infrastructure | Morgan Deters | |
2013-02-16 | Some cleanup and copyright updating | Morgan Deters | |
* update some copyrights for 2013 * cleaned up some comments/ifdefs, indentation * some spelling corrections * add some missing makefiles | |||
2013-02-12 | Fix a preprocessing performance issue. | Morgan Deters | |
2013-02-07 | Merge branch '1.0.x' | Morgan Deters | |
Conflicts: src/theory/quantifiers/theory_quantifiers.cpp | |||
2013-02-07 | Significant work on bug #491 (not yet closed). | Morgan Deters | |
2013-02-05 | Fix to miplib trick to make it less "cautious" and apply in more cases | Morgan Deters | |
2013-02-04 | Some fixes for the miplib preprocessing pass. | Morgan Deters | |
* TNode violation bug fix (thanks to Tim King for discovery & fix) * change Boolean miplib-trick substitution option into a threshold * ppAssert() the generated miplib constraints to arithmetic | |||
2013-02-04 | Model no longer adds subterms of quantifiers to equality engine, this fixed ↵ | Andrew Reynolds | |
bug 492 and resolves previous issue for bug 486.\n Multiple improvements for E-matching: do not choose multi-triggers if single triggers exist, only create multi-triggers that contain all variables, consider multiple terms per equivalence class but only add one instantiation per round per (trigger,term) pair.\nImprovements for strong solver: make use of sort inference information when choosing splits, check for cliques eagerly when disequalities are asserted. | |||
2013-02-03 | Some cleanup of miplib regressions and options | Morgan Deters | |
2013-02-03 | new option for doing top-level miplib substitutions (or not) | Morgan Deters | |
2013-02-03 | extended miplib trick to 6 vars, should work on pp miplib examples now | Morgan Deters | |
2013-02-03 | new miplib pass, works for 1 or 2 vars | Morgan Deters | |
2013-01-27 | some fixes for Intel benchmarks regarding quantifiers and datatypes, ↵ | Andrew Reynolds | |
datatypes theory still crashes for datatypes with boolean subfields (cherry picked from master bcbf52ffbe0416ecf70bdb644017c338c0540793) | |||
2013-01-27 | some fixes for Intel benchmarks regarding quantifiers and datatypes, ↵ | Andrew Reynolds | |
datatypes theory still crashes for datatypes with boolean subfields | |||
2013-01-25 | fix --check-model --finite-model-find when used together (related to bug 486) | Morgan Deters | |
2013-01-25 | Fix errors and reduce warnings on clang (merge from mdeters/clang) | Morgan Deters | |
2013-01-25 | fix --check-model --finite-model-find when used together (related to bug 486) | Morgan Deters | |
2013-01-24 | Add win32 support (merge from mdeters/win32, with some cleanup). | Morgan Deters | |
2012-12-11 | SMT-LIB compliance fix to get-assignment; resolves bug 480 | Morgan Deters | |
2012-12-01 | Fix the way abstract values are typed; fixes some compliance issues. | Morgan Deters | |
Also support array-store-all for Boolean terms (related to abstract values, since that's the only way for the user to include an array-store-all in an assertion). (this commit was certified error- and warning-free by the test-and-commit script.) | |||
2012-12-01 | remove an obsolete (and incorrect) assertion in boolean-terms; also add ↵ | Morgan Deters | |
failing regression for bug 472 | |||
2012-12-01 | Some fixes for boolean arrays | Morgan Deters | |
also a regression for bug 411 (this commit was certified error- and warning-free by the test-and-commit script.) | |||
2012-12-01 | definition-expansion fixed for get-model, resolves bug 411 | Morgan Deters | |
2012-12-01 | Adding SmtEngine::setLogic(const char* logic) so that ↵ | Tim King | |
smt.setLogic("QF_LRA"); works. |