summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
2013-04-30Draft of the new propagation code.Tim King
2013-04-30Adding has bound counts and tracking for rows.Tim King
2013-04-26FCSimplex branch mergeTim King
2013-04-23Theory "alternates" supportMorgan Deters
2013-04-22add bit0 and bit1 constants to smt-lib v1 parserMorgan 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-17bool flatten: node num_children workaroundKshitij Bansal
2013-04-17boolean flatten: bug fix in dfs searchKshitij Bansal
2013-04-16boolean flatten rewrite: dont re-rewriteKshitij Bansal
2013-04-16generalize to handle andKshitij Bansal
2013-04-16flatten or nodesKshitij Bansal
2013-04-11Improved speed of no redundant lemma assertion by using hash setClark Barrett
2013-04-11Fixes for getModelVal in bv theoryClark Barrett
2013-04-11Added check for infinite lemma loopClark Barrett
2013-04-10fixed getModelValue to only query the value of leaves and evaluate more compl...lianah
2013-04-09Change TPTP parser to not use the STRING type; this necessary to repurpose st...Morgan Deters
2013-04-03* changing the bitblast-eager to bitblast on pre-registerDejan Jovanović
2013-04-03Some final minor changes before cutting 1.1.Morgan Deters
2013-04-03abort quantifiers check if master equality engine is inconsistent.Andrew Reynolds
2013-04-02Making arithmetic model reversion on unsat checks an option.Tim King
2013-04-02Regenerated copyrights: canonicalized names, no emailsMorgan Deters
2013-04-02Remove old README file from rewrite-rules left over from new-theory script lo...Morgan 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-01Cleaning up the demand restart code.Tim King
2013-04-01Adding a restart test strategy to integers.Tim King
2013-04-01Adding demand restart.Tim King
2013-04-01Merging some cleanup work:Morgan Deters
2013-04-01Fix for iff terms over equalities between the same term and differing constants.Tim King
2013-04-01Fix bug 491 and related issues with checkModel() and quantifiers. Enabling p...Morgan Deters
2013-04-01fixed TheoryBool rewriter buglianah
2013-04-01fixed bug 502; now the core bv solver only gives the model for variables and ...lianah
2013-03-30changed option to run inequality solver by defaultLiana Hadarean
2013-03-30Disabling eager array index splitting for QF_AUFLIAClark Barrett
2013-03-30do simple ite rewriting within quantifiersAndrew Reynolds
2013-03-29make Boolean term conversion partially non-recursive (resolves bug 501)Morgan Deters
2013-03-29Merge branch 'master' of github.com:CVC4/CVC4Dejan Jovanović
2013-03-29removing cryptominisat since we're not using itDejan Jovanović
2013-03-28fix memory corruption in arrays destructorMorgan Deters
2013-03-27some Java bindings fixes (fixes Debian build problems)Morgan Deters
2013-03-27Fixed a warning, made eager-index default to true (better for QF_AUFBV)Clark Barrett
2013-03-27Fixed bug in arraysClark Barrett
2013-03-27Added assertionClark Barrett
2013-03-27Updates to model-based array solverClark Barrett
2013-03-27New model-based array procedureClark Barrett
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback