summaryrefslogtreecommitdiff
path: root/src/smt
AgeCommit message (Expand)Author
2013-04-01update copyrightsMorgan Deters
2013-04-01Fix regression error by turning off model-based solver when models are onClark Barrett
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
2013-04-01Merging some cleanup work:Morgan Deters
2013-04-01Fix bug 491 and related issues with checkModel() and quantifiers. Enabling p...Morgan Deters
2013-03-30Disabling eager array index splitting for QF_AUFLIAClark Barrett
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 t...Morgan Deters
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 quantifie...Morgan Deters
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 an...Morgan Deters
2013-03-11ite removal option for quantifiers --ite-remove-quant, e-matching for boolean...Andrew Reynolds
2013-03-05Merge branch '1.0.x'Morgan Deters
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 datatype...Andrew Reynolds
2013-02-20Some exception specification fixes in SmtEngine/Command infrastructureMorgan Deters
2013-02-16Some cleanup and copyright updatingMorgan Deters
2013-02-12Fix a preprocessing performance issue.Morgan Deters
2013-02-07Merge branch '1.0.x'Morgan Deters
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
2013-02-04Model no longer adds subterms of quantifiers to equality engine, this fixed b...Andrew Reynolds
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, datatype...Andrew Reynolds
2013-01-27some fixes for Intel benchmarks regarding quantifiers and datatypes, datatype...Andrew Reynolds
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
2012-12-01remove an obsolete (and incorrect) assertion in boolean-terms; also add faili...Morgan Deters
2012-12-01Some fixes for boolean arraysMorgan Deters
2012-12-01definition-expansion fixed for get-model, resolves bug 411Morgan Deters
2012-12-01Adding SmtEngine::setLogic(const char* logic) so that smt.setLogic("QF_LRA");...Tim King
2012-11-30Fix assertion in smt_engine's getValueClark Barrett
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback