| Age | Commit message (Expand) | Author |
|---|
| 2020-06-16 | Update copyright headers. | Aina Niemetz |
| 2020-02-26 | Fix node arity issue in reduction of int2bv (#3777) | Andrew Reynolds |
| 2020-01-28 | Avoid PLUS with one child for bv2nat elimination (#3639) | Andrew Reynolds |
| 2019-10-30 | Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. (#3366) | Mathias Preiner |
| 2019-03-26 | Update copyright headers. | Aina Niemetz |
| 2018-09-11 | Support model cores via option --produce-model-cores. (#2407) | Andrew Reynolds |
| 2018-08-03 | Add rewrite for BITVECTOR_ITE with const children. (#2271) | Aina Niemetz |
| 2018-02-20 | Improve documentation of bv::utils::isCoreTerm (#1617) | Aina Niemetz |
| 2018-02-20 | Unrecursified and merged bv::utils::is(Core|Equality)Term. (#1605) | Aina Niemetz |
| 2018-02-16 | bv::utils::mk(And|Or) Do not return true if size of vector is 0. (#1613) | Aina Niemetz |
| 2018-02-15 | Removed bv::utils::mkConjunction (redundant). (#1610) | Aina Niemetz |
| 2018-02-13 | Moved (unrecursified) bv::utils::collectVars. (#1602) | Aina Niemetz |
| 2018-02-11 | Move (unrecursified) bv::utils::numNodes to lazy_bitblaster.cpp. (#1594) | Aina Niemetz |
| 2018-02-09 | Move BitVector specific funs from bv::utils to util/bitvector.h. (#1589) | Aina Niemetz |
| 2018-02-09 | Remove mkNode from bv::utils (#1587) | Aina Niemetz |
| 2018-02-08 | Clean up bv utils (part one). (#1580) | Aina Niemetz |
| 2018-02-08 | Simplify and cleanup bv::utils::mkConjunction. (#1571) | Aina Niemetz |
| 2018-02-07 | Use template for bv::utils::mkOr. (#1570) | Aina Niemetz |
| 2018-02-07 | Use template for bv::utils::mkAnd. (#1569) | Aina Niemetz |
| 2018-02-06 | Renamed bv::utils::isBVGroundTerm to isBvConstTerm. (#1568) | Aina Niemetz |
| 2018-02-06 | Split and document theory_bv_utils. (#1566) | Aina Niemetz |
| 2018-01-15 | Removing more miscellaneous throw specifiers. (#1509) | Tim King |
| 2018-01-08 | Add bv util mkConst(unsigned, Integer&). (#1499) | Aina Niemetz |
| 2018-01-05 | Add special {SGE,SGT,NE}_UDIV1 side conditions for BV of size 1. (#1483) | Mathias Preiner |
| 2018-01-02 | Rewrites for BitVector multiplication (#1465) | Andrew Reynolds |
| 2017-12-20 | Add rewriting rule for ranking benchmarks. (#1448) | Mathias Preiner |
| 2017-12-08 | Add CEGQI BV linearization of additions and equalities over additions. (#1417) | Mathias Preiner |
| 2017-12-08 | Fixed side conditions for CBQI BV, added unit tests. (#1434) | Aina Niemetz |
| 2017-10-04 | Add mkZero, mkOne and mkUmulo to bv utils. (#1200) | Aina Niemetz |
| 2017-07-20 | Moving from the gnu extensions for hash maps to the c++11 hash maps | Tim King |
| 2017-07-07 | Update copyright headers. | Mathias Preiner |
| 2016-10-13 | Merging bv parts of ajr/bvExt branch, minor additions to ExtTheory. | ajreynol |
| 2016-04-20 | update from the master | PaulMeng |
| 2016-01-26 | Merged bit-vector and uf proof branch. | Liana Hadarean |
| 2015-08-20 | fix to bug659 due to algebraic solver model building | Liana Hadarean |
| 2015-07-20 | Squashed merge of SygusComp 2015 branch. | ajreynol |
| 2014-07-01 | Update copyrights. | Morgan Deters |
| 2014-06-19 | Fix compile errors with some versions of GCC. | Morgan Deters |
| 2014-06-14 | bv static learning and rewrites for power of 2 terms | lianah |
| 2014-06-10 | Merging CAV14 paper bit-vector work. | lianah |
| 2014-04-17 | simplify mkSkolem naming system: don't use $$ | Kshitij Bansal |
| 2013-12-24 | Minor code cleanup. | Morgan Deters |
| 2013-12-05 | Update copyrights, add missing file-level documentation; fix perms. | Morgan Deters |
| 2013-09-13 | Documentation fixes, some code typo fixes, file perms, other minor things. | Morgan Deters |
| 2013-04-30 | added several rewrite rules (BitwiseSlicing, Ule/SleEliminate, ExtractSignExt... | lianah |
| 2013-04-26 | Merge experimental decisionweight branch | Kshitij Bansal |
| 2013-04-02 | Regenerated copyrights: canonicalized names, no emails | Morgan Deters |
| 2013-04-01 | update copyrights | Morgan Deters |
| 2013-03-26 | added model generation for bv subtheories and bv-inequality solver option | lianah |
| 2013-03-23 | fixed some explanation problems for the core theory; still slow | lianah |
