summaryrefslogtreecommitdiff
path: root/src/theory/bv/bv_subtheory_inequality.cpp
AgeCommit message (Expand)Author
2019-03-26Update copyright headers.Aina Niemetz
2018-08-02 Add timer for BV inequality solver. (#2265)Aina Niemetz
2018-06-25Updated copyright headers.Aina Niemetz
2018-02-09Remove mkNode from bv::utils (#1587)Aina Niemetz
2017-12-08Make collect model info return a Bool (#1421)Andrew Reynolds
2017-07-07Update copyright headers.Mathias Preiner
2016-10-13Merging bv parts of ajr/bvExt branch, minor additions to ExtTheory.ajreynol
2016-04-20update from the masterPaulMeng
2016-01-08Removing StatisticsRegistry's static functions current() and registerStat().Tim King
2015-12-14Refactoring Options Handler & Library Cycle BreakingTim King
2015-05-28added options for controlling resource step-count for various solving stagesLiana Hadarean
2014-11-17Resource-limiting work.Liana Hadarean
2014-11-12Fix BV inequality solver caching.Morgan Deters
2014-07-01Update copyrights.Morgan Deters
2014-06-14added bv inequality lemmasLiana Hadarean
2014-06-12fixing bv inequality solver explanation buglianah
2013-12-05Update copyrights, add missing file-level documentation; fix perms.Morgan Deters
2013-11-27General pre-release cleanup commitMorgan Deters
2013-07-22Bug fix for --fmf-fmc for non-uninterpreted sort quantifiers, added infrastru...Andrew Reynolds
2013-07-16fixed bug520Liana Hadarean
2013-04-10fixed getModelValue to only query the value of leaves and evaluate more compl...lianah
2013-04-02Regenerated copyrights: canonicalized names, no emailsMorgan Deters
2013-04-01update copyrightsMorgan Deters
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-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-23non-incremental inequality solver seems to be bug-free (i.e. passes fuzzing)lianah
2013-03-20generalized bv inequality reasoning to handle both strict and non-strict ineq...lianah
2013-03-19inequality reasoning works on small examples added to regressions (not increm...Liana Hadarean
2013-03-19implementing more inequality graph stuff; work in progress doesn't compileLiana Hadarean
2013-03-18more work on inequality reasoning for bvlianah
2013-03-16started work on the inequality bv subtheorylianah
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback