2020-09-22 |
Mathias Preiner | Add simple BV solver (#5065) |
blob | commitdiff | raw |
2020-09-22 |
Mathias Preiner | Update copyright header script to support CMake and... |
blob | commitdiff | raw | diff to current |
2020-09-16 |
Abdalrhman Mohamed | Dump commands in internal code using command printing... |
blob | commitdiff | raw | diff to current |
2020-09-03 |
Gereon Kremer | Added a new rule to simplify (bvugt (bvurem T x) x... |
blob | commitdiff | raw | diff to current |
2020-08-03 |
yoni206 | New BV rewrite rules aimed at bv_to_int preprocessing... |
blob | commitdiff | raw | diff to current |
2020-06-16 |
Aina Niemetz | Update copyright headers. |
blob | commitdiff | raw | diff to current |
2019-10-30 |
Mathias Preiner | Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. ... |
blob | commitdiff | raw | diff to current |
2019-03-26 |
Aina Niemetz | Update copyright headers. |
blob | commitdiff | raw | diff to current |
2018-10-20 |
Aina Niemetz | BV rewrites (mined): Rule 35: ConcatPullUp (BITVECTOR_X... |
blob | commitdiff | raw | diff to current |
2018-10-17 |
Aina Niemetz | BV rewrites (mined): Rule 35: ConcatPullUp (BITVECTOR_O... |
blob | commitdiff | raw | diff to current |
2018-10-16 |
Aina Niemetz | BV rewrites (mined): Rule 35: ConcatPullUp (BITVECTOR_A... |
blob | commitdiff | raw | diff to current |
2018-08-07 |
Aina Niemetz | Add rewrite for nested BITVECTOR_ITE that can be merged... |
blob | commitdiff | raw | diff to current |
2018-08-04 |
Aina Niemetz | Add rewrite for nested BITVECTOR_ITE with cond_outer... |
blob | commitdiff | raw | diff to current |
2018-08-04 |
Aina Niemetz | Add rewrite for BITVECTOR_ITE with const children.... |
blob | commitdiff | raw | diff to current |
2018-08-03 |
Aina Niemetz | Add rewrite for BITVECTOR_ITE with term_then == term_el... |
blob | commitdiff | raw | diff to current |
2018-08-02 |
Aina Niemetz | Add rewrites for BITVECTOR_ITE and BITVECTOR_COMP with... |
blob | commitdiff | raw | diff to current |
2018-06-25 |
Aina Niemetz | Updated copyright headers. |
blob | commitdiff | raw | diff to current |
2018-05-30 |
Mathias Preiner | Normalize negated bit-vector terms over equalities... |
blob | commitdiff | raw | diff to current |
2017-12-21 |
Mathias Preiner | Add rewriting rule for ranking benchmarks. (#1448) |
blob | commitdiff | raw | diff to current |
2017-10-21 |
Mathias Preiner | Add rewriting rules for Eq/Ult with sign_extend and... |
blob | commitdiff | raw | diff to current |
2017-07-07 |
Mathias Preiner | Update copyright headers. |
blob | commitdiff | raw | diff to current |
2017-06-21 |
Andrew Reynolds | Merge pull request #175 from CVC4/fix_uninit |
blob | commitdiff | raw | diff to current |
2017-06-15 |
Clark Barrett | Merge pull request #167 from CVC4/fix_div |
blob | commitdiff | raw | diff to current |
2017-06-14 |
Andres Noetzli | Remove UdivSelf rewrite, add UdivZero rewrite |
blob | commitdiff | raw | diff to current |
2017-03-06 |
Clark Barrett | Adding support for bool-to-bv |
blob | commitdiff | raw | diff to current |
2017-03-02 |
ajreynol | Eliminate Boolean term conversion. Generalizes removeIT... |
blob | commitdiff | raw | diff to current |
2016-04-20 |
PaulMeng | update from the master |
blob | commitdiff | raw | diff to current |
2016-04-09 |
Guy | Merge branch 'master' of https://github.com/CVC4/CVC4 |
blob | commitdiff | raw | diff to current |
2016-04-04 |
Tim King | Updating the copyright headers and scripts. |
blob | commitdiff | raw | diff to current |
2016-02-02 |
Tim King | Moving dump.*, command.*, model.*, and ite_removal... |
blob | commitdiff | raw | diff to current |
2016-01-09 |
Tim King | Removing StatisticsRegistry's static functions current... |
blob | commitdiff | raw | diff to current |
2015-12-15 |
Tim King | Refactoring Options Handler & Library Cycle Breaking |
blob | commitdiff | raw | diff to current |
2015-07-28 |
Tianyi Liang | Merge branch 'master' of https://github.com/CVC4/CVC4 |
blob | commitdiff | raw | diff to current |
2015-07-20 |
ajreynol | Squashed merge of SygusComp 2015 branch. |
blob | commitdiff | raw | diff to current |
2014-11-10 |
Morgan Deters | Merge branch '1.4.x' |
blob | commitdiff | raw | diff to current |
2014-11-07 |
Morgan Deters | Merge branch '1.4.x' |
blob | commitdiff | raw | diff to current |
2014-11-07 |
Morgan Deters | Merge branch '1.4.x' |
blob | commitdiff | raw | diff to current |
2014-11-07 |
Morgan Deters | Merge branch '1.4.x' |
blob | commitdiff | raw | diff to current |
2014-11-05 |
Morgan Deters | Merge branch '1.4.x' |
blob | commitdiff | raw | diff to current |
2014-10-23 |
lianah | Fixed inefficiency in bit-vector rewrite rule. |
blob | commitdiff | raw | diff to current |
2014-07-10 |
Kshitij Bansal | Merge remote-tracking branch 'origin/master' into segfa... |
blob | commitdiff | raw | diff to current |
2014-07-01 |
Morgan Deters | Update copyrights. |
blob | commitdiff | raw | diff to current |
2014-06-15 |
lianah | bv static learning and rewrites for power of 2 terms |
blob | commitdiff | raw | diff to current |
2014-06-14 |
lianah | more bv rewrites |
blob | commitdiff | raw | diff to current |
2014-06-14 |
lianah | fixed merge |
blob | commitdiff | raw | diff to current |
2014-06-14 |
lianah | added bv inequality rewrite |
blob | commitdiff | raw | diff to current |
2014-06-10 |
lianah | Merging CAV14 paper bit-vector work. |
blob | commitdiff | raw | diff to current |
2013-11-06 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
blob | commitdiff | raw | diff to current |
2013-11-04 |
lianah | Merge branch 'master' of https://github.com/CVC4/CVC4 |
blob | commitdiff | raw | diff to current |
2013-10-09 |
lianah | fixed options::proof() segfault |
blob | commitdiff | raw | diff to current |
2013-09-30 |
Liana Hadarean | merged golden |
blob | commitdiff | raw | diff to current |
2013-09-18 |
Morgan Deters | Support for bv2nat/int2bv in parser and BV rewriter. |
blob | commitdiff | raw | diff to current |
2013-05-03 |
Tim King | Merging branch 'soiquickexplain'. |
blob | commitdiff | raw | diff to current |
2013-05-03 |
Tim King | Merge branch 'fcexplanations' |
blob | commitdiff | raw | diff to current |
2013-05-02 |
lianah | Merge branch 'master' of https://github.com/CVC4/CVC4 |
blob | commitdiff | raw | diff to current |
2013-04-30 |
lianah | added several rewrite rules (BitwiseSlicing, Ule/SleEli... |
blob | commitdiff | raw | diff to current |
2013-04-30 |
lianah | added bvule, bvsle operator elimination rulesl; added... |
blob | commitdiff | raw | diff to current |
2013-04-30 |
lianah | added some bv rewrite rules |
blob | commitdiff | raw | diff to current |
2013-04-30 |
lianah | added several rewrite rules (BitwiseSlicing, Ule/SleEli... |
blob | commitdiff | raw | diff to current |
2013-04-25 |
lianah | added bvule, bvsle operator elimination rulesl; added... |
blob | commitdiff | raw | diff to current |
2013-04-21 |
lianah | added some bv rewrite rules |
blob | commitdiff | raw | diff to current |
2013-04-02 |
Morgan Deters | Regenerated copyrights: canonicalized names, no emails |
blob | commitdiff | raw | diff to current |
2013-04-02 |
Morgan Deters | update copyrights |
blob | commitdiff | raw | diff to current |
2013-03-13 |
lianah | post failed attempts at getting the incremental solver... |
blob | commitdiff | raw | diff to current |
2013-02-26 |
lianah | Merge branch '1.0.x' of https://github.com/CVC4/CVC4... |
blob | commitdiff | raw | diff to current |
2013-02-15 |
Tim King | Merge branch '1.0.x' |
blob | commitdiff | raw | diff to current |
2013-02-14 |
Tim King | Removing BVDebug and replacing with Debug. |
blob | commitdiff | raw | diff to current |
2012-10-11 |
Morgan Deters | Standardizing copyright notice. Touches **ALL** source... |
blob | commitdiff | raw | diff to current |
2012-09-22 |
Morgan Deters | Separate public-facing and internal-facing interfaces... |
blob | commitdiff | raw | diff to current |
2012-06-13 |
Clark Barrett | Fixes lots of problems in bv rewrite rules and adds... |
blob | commitdiff | raw | diff to current |
2012-05-28 |
Clark Barrett | Added some BV rewrites, fixed bugs in array theory... |
blob | commitdiff | raw | diff to current |
2012-05-17 |
Liana Hadarean | Fixed bug 338: |
blob | commitdiff | raw | diff to current |
2012-04-04 |
Liana Hadarean | * added propagation as lemmas to TheoryBV: |
blob | commitdiff | raw | diff to current |
2012-03-22 |
Liana Hadarean | Merged updated version of the bitvector theory: |
blob | commitdiff | raw | diff to current |
2012-02-25 |
Liana Hadarean | Refactored CnfStream to work with the bv theory Bitblaster: |
blob | commitdiff | raw | diff to current |
2011-12-08 |
Morgan Deters | Disable a BV rewriter statistic (after checking with... |
blob | commitdiff | raw | diff to current |
2011-09-02 |
Morgan Deters | Merge from my post-smtcomp branch. Includes: |
blob | commitdiff | raw | diff to current |
2011-03-22 |
Dejan Jovanović | updating debug output usage to eliviate impact of bug 252 |
blob | commitdiff | raw | diff to current |
2011-02-25 |
Dejan Jovanović | slicing manager is not breaking the old regressions... |
blob | commitdiff | raw | diff to current |
2011-02-16 |
Dejan Jovanović | updates for the rewriter, added some statistics |
blob | commitdiff | raw | diff to current |
2010-10-03 |
Morgan Deters | file header documentation regenerated with contributors... |
blob | commitdiff | raw | diff to current |
2010-09-24 |
Dejan Jovanović | basic union find for bitvectors |
blob | commitdiff | raw | diff to current |
2010-09-20 |
Dejan Jovanović | bitvector rewriting for the core theory and testcases |
blob | commitdiff | raw | diff to current |
|