summaryrefslogtreecommitdiff
path: root/src/theory
AgeCommit message (Expand)Author
2013-04-01update copyrightsMorgan Deters
2013-04-01Made eager lemmas an option, enabled 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-28fix memory corruption in arrays destructorMorgan 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
2013-03-27reverted the core solver to do static slicing, added option --bv-core-solverlianah
2013-03-27fixed inequality checkDisequalities inefficiencylianah
2013-03-27fixed some model stufflianah
2013-03-27fixed model generation bug; commented out attempt at inequality propagationlianah
2013-03-26inequality solver now only splits on disequalities when completelianah
2013-03-26added model generation for bv subtheories and bv-inequality solver optionlianah
2013-03-26core theory currently disabledlianah
2013-03-26getModelValue implementation in bitvectorsDejan Jovanović
2013-03-26addingDejan Jovanović
2013-03-26moving bv before arraysDejan Jovanović
2013-03-26fixed inequality bugs due to improper explanationlianah
2013-03-25cleaned up the bv subtheory interface; added check for inequality theory comp...lianah
2013-03-25getEqualityStatus now also queries the inequality solverlianah
2013-03-24added support for disequalities in the inequality solverLiana Hadarean
2013-03-24incremental inequality solver implementedlianah
2013-03-23non-incremental inequality solver seems to be bug-free (i.e. passes fuzzing)lianah
2013-03-23fixed some explanation problems for the core theory; still slowlianah
2013-03-22Support for Boolean term conversion in datatypes.Morgan Deters
2013-03-21Merge branch 'master' into bv-corelianah
2013-03-21another typo/bugfix for equality constant evaluationDejan Jovanović
2013-03-21Merge branch 'master' into bv-corelianah
2013-03-21fixed more equality stufflianah
2013-03-21Better error in case of nonlinear assertions while in linear logicMorgan Deters
2013-03-21fixing markings of internal nodes in equality engineDejan Jovanović
2013-03-21fixed compilation problemlianah
2013-03-21incorporated dejan's constant evaluation; now getting destruction seg faultlianah
2013-03-21Merge branch 'master' into bv-corelianah
2013-03-21disabled ineqlianah
2013-03-21more equality constant evaluationDejan Jovanović
2013-03-21added regression test for constant evallianah
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback