summaryrefslogtreecommitdiff
path: root/test/unit/theory
AgeCommit message (Expand)Author
2016-04-20update from the masterPaulMeng
2016-01-28Adding listeners to Options.Tim King
2016-01-26Merged bit-vector and uf proof branch.Liana Hadarean
2016-01-08Adding a new Listener utility class. Changing the ResourceManager to use List...Tim King
2016-01-05Removing dead code. StackingMap only appeared in unit tests.Tim King
2016-01-05Add SmtGlobals ClassTim King
2015-12-26Merged my changes from experimental branch (new array decision procedure,Clark Barrett
2015-12-14Refactoring Options Handler & Library Cycle BreakingTim King
2014-12-03Floating point infrastructure.Martin Brain
2014-11-17Resource-limiting work.Liana Hadarean
2014-09-25fix unit test for new fair datatype enumerationMorgan Deters
2014-07-01Update copyrights.Morgan Deters
2014-06-21fixed build failurelianah
2014-06-19added model generation to eager bit-blasting and turned abc off by defaultlianah
2014-06-19disable unate lemmas when using incremental modeKshitij Bansal
2014-06-11fixed unit tests failureslianah
2014-03-12Fix LogicInfo unit test.Morgan Deters
2014-03-04Don't theory-preprocess under quantifiers; but DO theory-preprocess lemmas (r...Morgan Deters
2014-02-21add new theory (sets)Kshitij Bansal
2014-01-22Delay QuantifiersEngine and UF strong solver initialization until after final...Morgan Deters
2013-12-05Update copyrights, add missing file-level documentation; fix perms.Morgan Deters
2013-09-11Theory of strings.Tianyi Liang
2013-05-29Merge branch '1.2.x'Morgan Deters
2013-05-28Standardize SMT-LIBv2 set of logics to use LogicInfo.Morgan Deters
2013-05-09Changing the integer normal form to increase matching.Tim King
2013-05-03Fixing compilation of unit tests. These problems were due to splitLemma() bei...Tim King
2013-04-02Regenerated copyrights: canonicalized names, no emailsMorgan Deters
2013-04-01update copyrightsMorgan Deters
2012-11-17* Fix for bug 445 agreed to in meeting 11/13/2012: always dump in ALL_SUPPORT...Morgan Deters
2012-11-10Updates to Clark's commit r4540:Morgan Deters
2012-10-26Fix to subrange type enumerator, and its unit test. Resolves bug 436.Morgan Deters
2012-10-11Standardizing copyright notice. Touches **ALL** sources, guys, sorry.. it'sMorgan Deters
2012-10-06* Fix some regressions' expected outputs.Morgan Deters
2012-10-05Bug-related:Morgan Deters
2012-09-28rename Assert.h/Assert.cpp to cvc4_assert.h/cvc4_assert.cpp -- we need to mak...Morgan Deters
2012-09-28Public interface review items:Morgan Deters
2012-08-31merge from fmf-devel branch. more updates to models: now with collectModelIn...Andrew Reynolds
2012-08-26Array constants finished and working. Unit tests for array constants.Clark Barrett
2012-08-16The SmtEngine now ensures that setLogicInternal() is called even if there is ...Morgan Deters
2012-08-03Comparisons for LogicInfos, and associated testsMorgan Deters
2012-07-31Options merge. This commit:Morgan Deters
2012-07-27removing unecessary filesAndrew Reynolds
2012-07-26Datatype enumerator work. This version is not a "fair" enumerator, but I got...Morgan Deters
2012-07-16Support for having two SmtEngines with the same ExprManager.Morgan Deters
2012-07-14Type enumerator infrastructure and uninterpreted constant support. No suppor...Morgan Deters
2012-06-11Merge from quantifiers2-trunkmerge branch.Morgan Deters
2012-06-07LogicInfo locking implemented, and some initialization-order issues in SmtEng...Morgan Deters
2012-06-06Changes to the combination mechanism, lots of details. Not done yet, there ar...Dejan Jovanović
2012-05-22This commit merges in the branch arithmetic/cprop.Tim King
2012-05-17Fixing an issue with LogicInfo::isPure() that turned off simplification in QF...Morgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback