summaryrefslogtreecommitdiff
path: root/test/unit/theory
AgeCommit message (Expand)Author
2018-02-08Updated copyrightAina Niemetz
2018-01-24Added unit tests for PLUS, NEG, NOT ICs for CBQI BV. (#1534)Aina Niemetz
2018-01-21Refactor and fix solveBvLit for CBQI BV. (#1526)Aina Niemetz
2018-01-09Fix linearization for terms where the solve variable does not occur. (#1506)Mathias Preiner
2018-01-05Add UGT/SGT side conditions for AND/OR + other fixes. (#1481)Mathias Preiner
2018-01-02Add side conditions for inequalities over BITVECTOR_UDIV for CBQI BV. (#1464)Aina Niemetz
2018-01-02Fix handling for UGT/SGT. (#1467)Mathias Preiner
2017-12-29Add side conditions for inequalities over BITVECTOR_UREM for CBQI BV. (#1460)Aina Niemetz
2017-12-28Fix unit tests for ineq for CBQI BV. (#1456)Aina Niemetz
2017-12-28Add unit tests for side conditions for inequality for CBQI BV. (#1455)Aina Niemetz
2017-12-20Add explicit disequality handling when generating side condition for CBQI BV....Aina Niemetz
2017-12-13Add missing side conditions for SHL, LSHR, ASHR for CBQI BV. (#1441)Aina Niemetz
2017-12-08Add CEGQI BV linearization of additions and equalities over additions. (#1417)Mathias Preiner
2017-12-08Fixed side conditions for CBQI BV, added unit tests. (#1434)Aina Niemetz
2017-11-30Add Gaussian Elimination as a preprocessing pass for BV. (#1342)Aina Niemetz
2017-11-15Adding garbage collection for Proof objects. (#1294)Tim King
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback