summaryrefslogtreecommitdiff
path: root/src/smt
AgeCommit message (Expand)Author
2013-05-20Merge branch '1.2.x'Morgan Deters
2013-05-20Fix error reporting on use of (nonlinear) div,mod,/ symbolsMorgan Deters
2013-05-20Don't allow get-model & co after a user push/popMorgan Deters
2013-05-20Fix for equality-chaining of Booleans in SMT-LIBv2.Morgan Deters
2013-05-20Better error on invalid logic strings.Morgan Deters
2013-05-20Fix to empty response to (get-assignment).Morgan Deters
2013-05-17Add support for --dump-models option, in preparation for casc.Andrew Reynolds
2013-05-17Fix for equality-chaining of Booleans in SMT-LIBv2.Morgan Deters
2013-05-17Better error on invalid logic strings.Morgan Deters
2013-05-17Fix to empty response to (get-assignment).Morgan Deters
2013-05-09Add simplification option --fo-prop-quant. Add model support for new model-c...Andrew Reynolds
2013-05-08Add new method for checking candidate models, --fmf-fmc. Add infrastructure ...Andrew Reynolds
2013-05-08final updates for smt-eval scriptMorgan Deters
2013-05-06Disables justification stop only for LRA if the problem contains no ites. Thi...Tim King
2013-05-02Merge branch 'master' of https://github.com/CVC4/CVC4lianah
2013-05-01Fix to dumping re: boolean terms, datatypesMorgan Deters
2013-05-01Fix to boolean-terms; resolves bug #507Morgan Deters
2013-05-01added back BitwiseEq rulelianah
2013-04-30innd examples are solved fast, but destruction assertion faillianah
2013-04-30uncompiling new bv to bool liftinglianah
2013-04-30finished implementing bv to bool lifting and added --bv-to-bool optionlianah
2013-04-23Theory "alternates" supportMorgan Deters
2013-04-18making sure sat context is zero when user context is popped to 0 in SmtEngine...lianah
2013-04-18fixing destruction order in SmtEnginelianah
2013-04-03* changing the bitblast-eager to bitblast on pre-registerDejan Jovanović
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
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback