summaryrefslogtreecommitdiff
path: root/src/smt
AgeCommit message (Collapse)Author
2013-04-02Regenerated copyrights: canonicalized names, no emailsMorgan Deters
2013-04-01update copyrightsMorgan Deters
2013-04-01Fix regression error by turning off model-based solver when models are onClark Barrett
(ironic, yes, but model-based solver doesn't yet produce models)
2013-04-01Turning on model based array solver for QF_AXClark Barrett
2013-04-01Made eager lemmas an option, enabled for QF_AXClark Barrett
2013-04-01Disabling eager array index splitting for QF_AXClark Barrett
2013-04-01Fixes 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-01Merging 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-01Fix bug 491 and related issues with checkModel() and quantifiers. Enabling ↵Morgan Deters
previously-failing testcase.
2013-03-30Disabling eager array index splitting for QF_AUFLIAClark Barrett
Minor changes to model-based array solver
2013-03-29make Boolean term conversion partially non-recursive (resolves bug 501)Morgan Deters
2013-03-26Fixes for warnings from clang++, from -std=gnu++0x, from swig, and from javacMorgan Deters
2013-03-22Support for Boolean term conversion in datatypes.Morgan Deters
2013-03-21Some model and printing fixes for defined functions in input.Morgan Deters
2013-03-21Fix for SmtEngine::expandDefinitions()---improper TypeCheckingExceptionMorgan Deters
2013-03-20Some statistics for narrowing down incrementality issues (push/pop vs solve ↵Morgan Deters
timing)
2013-03-19Fixes for miplib-trick application (and a new testcase)Morgan Deters
2013-03-15Boolean terms rewriting for quantified variables of type Bool, when ↵Morgan Deters
quantifier body uses them in term context
2013-03-14Merge branch '1.0.x'Morgan Deters
2013-03-14fix to build system: #include the proper file when they are in both builds ↵Morgan Deters
and src
2013-03-11ite removal option for quantifiers --ite-remove-quant, e-matching for ↵Andrew Reynolds
boolean terms, improvement for pre skolemization
2013-03-05Merge branch '1.0.x'Morgan Deters
Conflicts: src/smt/smt_engine.cpp
2013-03-05Bugfix for SmtEngine: proper unsubscribing for NodeManager eventsMorgan Deters
2013-03-01Merge branch '1.0.x'Morgan Deters
2013-02-26Fix for quantifiers containing Boolean terms.Morgan Deters
2013-02-24added 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-20Some exception specification fixes in SmtEngine/Command infrastructureMorgan Deters
2013-02-16Some cleanup and copyright updatingMorgan Deters
* update some copyrights for 2013 * cleaned up some comments/ifdefs, indentation * some spelling corrections * add some missing makefiles
2013-02-12Fix a preprocessing performance issue.Morgan Deters
2013-02-07Merge branch '1.0.x'Morgan Deters
Conflicts: src/theory/quantifiers/theory_quantifiers.cpp
2013-02-07Significant work on bug #491 (not yet closed).Morgan Deters
2013-02-05Fix to miplib trick to make it less "cautious" and apply in more casesMorgan Deters
2013-02-04Some 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-04Model 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-03Some cleanup of miplib regressions and optionsMorgan Deters
2013-02-03new option for doing top-level miplib substitutions (or not)Morgan Deters
2013-02-03extended miplib trick to 6 vars, should work on pp miplib examples nowMorgan Deters
2013-02-03new miplib pass, works for 1 or 2 varsMorgan Deters
2013-01-27some 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-27some fixes for Intel benchmarks regarding quantifiers and datatypes, ↵Andrew Reynolds
datatypes theory still crashes for datatypes with boolean subfields
2013-01-25fix --check-model --finite-model-find when used together (related to bug 486)Morgan Deters
2013-01-25Fix errors and reduce warnings on clang (merge from mdeters/clang)Morgan Deters
2013-01-25fix --check-model --finite-model-find when used together (related to bug 486)Morgan Deters
2013-01-24Add win32 support (merge from mdeters/win32, with some cleanup).Morgan Deters
2012-12-11SMT-LIB compliance fix to get-assignment; resolves bug 480Morgan Deters
2012-12-01Fix 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-01remove an obsolete (and incorrect) assertion in boolean-terms; also add ↵Morgan Deters
failing regression for bug 472
2012-12-01Some fixes for boolean arraysMorgan Deters
also a regression for bug 411 (this commit was certified error- and warning-free by the test-and-commit script.)
2012-12-01definition-expansion fixed for get-model, resolves bug 411Morgan Deters
2012-12-01Adding SmtEngine::setLogic(const char* logic) so that ↵Tim King
smt.setLogic("QF_LRA"); works.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback