summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/bv_inverter.cpp
AgeCommit message (Expand)Author
2018-10-08 BV inverter: Factor out util functions. (#2603)Aina Niemetz
2018-06-15Disable solving non-linear BV literals by default (#2070)Andrew Reynolds
2018-04-13allowing --bool-to-bv without quantifiers (#1771)yoni206
2018-02-09Move BitVector specific funs from bv::utils to util/bitvector.h. (#1589)Aina Niemetz
2018-02-06Updated copyright header for bv_inverter.(cpp|h).Aina Niemetz
2018-01-23Fix MULT handling for CBQI BV. (#1531)Aina Niemetz
2018-01-22Add previous concat handling for CBQI BV as heuristic for EQ. (#1528)Aina Niemetz
2018-01-21Refactor and fix solveBvLit for CBQI BV. (#1526)Aina Niemetz
2018-01-13Remove BITVECTOR_SUB from isInvertible(). (#1513)Aina Niemetz
2018-01-10Removed division by constant handling for CBQI BV (unsound). (#1508)Aina Niemetz
2018-01-08Added division by constant handling for CBQI BV. (#1498)Aina Niemetz
2018-01-08Improvements to quant+BV/Bool variable elimination (#1495)Andrew Reynolds
2018-01-05Add special {SGE,SGT,NE}_UDIV1 side conditions for BV of size 1. (#1483)Mathias Preiner
2018-01-05Use simpler EQUAL SCs for LSHR0, LSHR1, ASHR0, AHSR1, SHL0, SHL1. (#1482)Mathias Preiner
2018-01-05Add UGT/SGT side conditions for AND/OR + other fixes. (#1481)Mathias Preiner
2018-01-04Fix side condition handling for PLUS, XOR, SIGN_EXTEND for CBQI BV. (#1480)Aina Niemetz
2018-01-04Add side conditions for inequalities of SHL. (#1472)Mathias Preiner
2018-01-03Add side conditions for UGT/SGT over BITVECTOR_UREM for CBQI BV. (#1470)Aina Niemetz
2018-01-03Add 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-02Add side conditions for inequalities over BITVECTOR_UDIV for CBQI BV. (#1464)Aina Niemetz
2018-01-02Simplify side condition for SGE over UREM (index = 1) for CBQI BV. (#1463)Aina Niemetz
2018-01-02Fix handling for UGT/SGT. (#1467)Mathias Preiner
2018-01-02Add side conditions for inequalities of LSHR. (#1462)Mathias Preiner
2017-12-29Add side conditions for inequalities over BITVECTOR_UREM for CBQI BV. (#1460)Aina Niemetz
2017-12-29Add side conditions for inequalities of AND/OR. (#1457)Mathias Preiner
2017-12-28Add unit tests for side conditions for inequality for CBQI BV. (#1455)Aina Niemetz
2017-12-27Minor refactor for inequality handling for CBQI BV. (#1452)Aina Niemetz
2017-12-20Add explicit disequality handling when generating side condition for CBQI BV....Aina Niemetz
2017-12-15Enable side condition handling for shifts introduced in #1441. (#1444)Aina Niemetz
2017-12-13Add missing side conditions for SHL, LSHR, ASHR for CBQI BV. (#1441)Aina Niemetz
2017-12-08Fixed side conditions for CBQI BV, added unit tests. (#1434)Aina Niemetz
2017-12-04Fix side condition for BITVECTOR_MULT. (#1422)Mathias Preiner
2017-11-01CBQI BV choice expressions (#1296)Andrew Reynolds
2017-10-25CBQI BV: Add handling for missing operators. (#1274)Aina Niemetz
2017-10-23CBQI BV: Add ULT/SLT inverse handling. (#1268)Aina Niemetz
2017-10-19CBQI BV: Refactor solve_bv_constraint. (#1265)Aina Niemetz
2017-10-13CBQI BV: Added EXTRACT handling. (#1240)Aina Niemetz
2017-10-11Enable regressions for CBQI BV and fix inverse for LSHR. (#1234)Aina Niemetz
2017-10-11Add side conditions for UDIV_TOTAL, SHL, CONCAT. (#1224)Mathias Preiner
2017-10-09Split term database (#1206)Andrew Reynolds
2017-10-09CBQI BV: Add inverse for more operators. (#1213)Aina Niemetz
2017-10-02Address comments from PR #1164. (#1174)Mathias Preiner
2017-09-29Move BvInverter class into separate file. (#1173)Mathias Preiner
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback