summaryrefslogtreecommitdiff
path: root/test/unit/theory
AgeCommit message (Expand)Author
2017-10-25Removing throw specifiers from OutputChannel and subclasses. (#1209)Tim King
2017-10-04Add mkZero, mkOne and mkUmulo to bv utils. (#1200)Aina Niemetz
2017-08-17Remove unused SubrangeBound(s) classes (#221)Andres Noetzli
2017-07-20Moving from the gnu extensions for hash maps to the c++11 hash mapsTim King
2017-07-12Fix unit tests for subranges. Fix destructors for context objs in unit tests.ajreynol
2017-07-07Update copyright headers.Mathias Preiner
2017-07-05Update unit test, news.ajreynol
2016-12-08Fix (inactive) `MultSlice` rewriteAndres Notzli
2016-11-30Add unit test for `MultDistrib` ruleAndres Notzli
2016-11-18Fix for unit test after changing default "all supported" logic name.Clark Barrett
2016-06-18Fix unit test.ajreynol
2016-04-03Updating the copyright headers and scripts.Tim King
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback