Age | Commit message (Expand) | Author |
2021-05-26 | More precise includes of `Node` constants (#6617) | Andres Noetzli |
2021-05-21 | BV: Rename BITVECTOR_PLUS to BITVECTOR_ADD. (#6589) | Aina Niemetz |
2021-05-13 | Add std::hash overloads for Node, TNode and TypeNode. (#6534) | Mathias Preiner |
2021-04-12 | Refactor and update copyright headers. (#6316) | Aina Niemetz |
2021-04-07 | Replace calls to NodeManager::mkSkolem with SkolemManager::mkDummySkolem (#6291) | Andrew Reynolds |
2021-04-06 | Remove template argument from `NodeBuilder` (#6290) | Andres Noetzli |
2021-04-01 | Rename namespace CVC5 to cvc5. (#6258) | Aina Niemetz |
2021-03-31 | Rename namespace CVC4 to CVC5. (#6249) | Aina Niemetz |
2021-03-09 | Update copyright headers to 2021. (#6081) | Aina Niemetz |
2021-03-05 | Remove partial UDIV/UREM operators. (#6069) | Mathias Preiner |
2020-09-22 | Update copyright header script to support CMake and Python files (#5067) | Mathias Preiner |
2020-06-16 | Update copyright headers. | Aina Niemetz |
2020-05-19 | Renamed operator CHOICE to WITNESS (#4207) | mudathirmahgoub |
2020-04-20 | Make option names related to CEGQI consistent (#4316) | Andrew Reynolds |
2020-03-05 | Enable -Wshadow and fix warnings. (#3909) | Mathias Preiner |
2019-03-26 | Update copyright headers. | Aina Niemetz |
2018-10-08 | BV inverter: Factor out util functions. (#2603) | Aina Niemetz |
2018-06-15 | Disable solving non-linear BV literals by default (#2070) | Andrew Reynolds |
2018-04-13 | allowing --bool-to-bv without quantifiers (#1771) | yoni206 |
2018-02-09 | Move BitVector specific funs from bv::utils to util/bitvector.h. (#1589) | Aina Niemetz |
2018-02-06 | Updated copyright header for bv_inverter.(cpp|h). | Aina Niemetz |
2018-01-23 | Fix MULT handling for CBQI BV. (#1531) | Aina Niemetz |
2018-01-22 | Add previous concat handling for CBQI BV as heuristic for EQ. (#1528) | Aina Niemetz |
2018-01-21 | Refactor and fix solveBvLit for CBQI BV. (#1526) | Aina Niemetz |
2018-01-13 | Remove BITVECTOR_SUB from isInvertible(). (#1513) | Aina Niemetz |
2018-01-10 | Removed division by constant handling for CBQI BV (unsound). (#1508) | Aina Niemetz |
2018-01-08 | Added division by constant handling for CBQI BV. (#1498) | Aina Niemetz |
2018-01-08 | Improvements to quant+BV/Bool variable elimination (#1495) | Andrew Reynolds |
2018-01-05 | Add special {SGE,SGT,NE}_UDIV1 side conditions for BV of size 1. (#1483) | Mathias Preiner |
2018-01-05 | Use simpler EQUAL SCs for LSHR0, LSHR1, ASHR0, AHSR1, SHL0, SHL1. (#1482) | Mathias Preiner |
2018-01-05 | Add UGT/SGT side conditions for AND/OR + other fixes. (#1481) | Mathias Preiner |
2018-01-04 | Fix side condition handling for PLUS, XOR, SIGN_EXTEND for CBQI BV. (#1480) | Aina Niemetz |
2018-01-04 | Add side conditions for inequalities of SHL. (#1472) | Mathias Preiner |
2018-01-03 | Add side conditions for UGT/SGT over BITVECTOR_UREM for CBQI BV. (#1470) | Aina Niemetz |
2018-01-03 | Add UGT/SGT side conditions for LSHR. (#1469) | Mathias Preiner |
2018-01-03 | Add side conditions for inequalities over BITVECTOR_MULT for CBQI BV. (#1468) | Aina Niemetz |
2018-01-02 | Add side conditions for inequalities of ASHR. (#1461) | Mathias Preiner |
2018-01-02 | Add side conditions for inequalities over BITVECTOR_UDIV for CBQI BV. (#1464) | Aina Niemetz |
2018-01-02 | Simplify side condition for SGE over UREM (index = 1) for CBQI BV. (#1463) | Aina Niemetz |
2018-01-02 | Fix handling for UGT/SGT. (#1467) | Mathias Preiner |
2018-01-02 | Add side conditions for inequalities of LSHR. (#1462) | Mathias Preiner |
2017-12-29 | Add side conditions for inequalities over BITVECTOR_UREM for CBQI BV. (#1460) | Aina Niemetz |
2017-12-29 | Add side conditions for inequalities of AND/OR. (#1457) | Mathias Preiner |
2017-12-28 | Add unit tests for side conditions for inequality for CBQI BV. (#1455) | Aina Niemetz |
2017-12-27 | Minor refactor for inequality handling for CBQI BV. (#1452) | Aina Niemetz |
2017-12-20 | Add explicit disequality handling when generating side condition for CBQI BV.... | Aina Niemetz |
2017-12-15 | Enable side condition handling for shifts introduced in #1441. (#1444) | Aina Niemetz |
2017-12-13 | Add missing side conditions for SHL, LSHR, ASHR for CBQI BV. (#1441) | Aina Niemetz |
2017-12-08 | Fixed side conditions for CBQI BV, added unit tests. (#1434) | Aina Niemetz |
2017-12-04 | Fix side condition for BITVECTOR_MULT. (#1422) | Mathias Preiner |