summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
2018-01-23Fix MULT handling for CBQI BV. (#1531)Aina Niemetz
2018-01-23Commenting out throw specifiers for DeltaRationExceptions. These functions ca...Tim King
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-21Only push/pop around check-sat if it is associated with an assertion (#1525)Andrew Reynolds
2018-01-17Removes yet more throw specifiers. Updating the documentation as needed. (#1518)Tim King
2018-01-15Removing more miscellaneous throw specifiers. (#1509)Tim King
2018-01-14Removing throw specifiers from Type. (#1511)Tim King
2018-01-14Removing throw specifiers from OptionsHandler. (#1510)Tim King
2018-01-13Remove BITVECTOR_SUB from isInvertible(). (#1513)Aina Niemetz
2018-01-12Improvements for CBQI BV (#1504)Andrew Reynolds
2018-01-10Removed division by constant handling for CBQI BV (unsound). (#1508)Aina Niemetz
2018-01-10Removing throw specifiers for TypeRules. (#1501)Tim King
2018-01-10Removing throw specifiers from type enumerators. (#1502)Tim King
2018-01-09Cleaning up throw specifiers on Exception and subclasses. (#1475)Tim King
2018-01-09Fix linearization for terms where the solve variable does not occur. (#1506)Mathias Preiner
2018-01-09Reorganized bitvector.h. (#1505)Aina Niemetz
2018-01-09Fix output of --trace=help. (#1500)Aina Niemetz
2018-01-09Removing throw specifiers from miscellaneous src/expr/ classes. (#1503)Tim King
2018-01-08Removing more miscellaneous throw specifiers. (#1488)Tim King
2018-01-08Add bv util mkConst(unsigned, Integer&). (#1499)Aina Niemetz
2018-01-08Remove throw specifiers from symbol table. (#1490)Tim King
2018-01-08Added division by constant handling for CBQI BV. (#1498)Aina Niemetz
2018-01-08Removes throw specifiers from command.{h,cpp}. (#1485)Tim King
2018-01-08Improvements to quant+BV/Bool variable elimination (#1495)Andrew Reynolds
2018-01-08Remove throw specifiers from datatype. (#1489)Tim King
2018-01-07Re-ordering field initialization in QuantInfo to remove compiler warning. (#1...Tim King
2018-01-07Removes RationalFromDoubleException. Replaces this with an explicit M… (#1476)Tim King
2018-01-06Removing throw specifiers from src/parser/. (#1486)Tim King
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-04Improvements for CBQI (#1478)Andrew Reynolds
2018-01-04Removing miscellaneous throw specifiers. (#1474)Tim King
2018-01-03Removing throw specifiers from context/. (#1473)Tim King
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-03Global negate (#1466)Andrew Reynolds
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-02Rewrites for BitVector multiplication (#1465)Andrew Reynolds
2018-01-02Add side conditions for inequalities of LSHR. (#1462)Mathias Preiner
2018-01-02Improve rewriter for string equality (#1427)Andrew Reynolds
2017-12-29Add side conditions for inequalities over BITVECTOR_UREM for CBQI BV. (#1460)Aina Niemetz
2017-12-29Fix RNG for seed = 0. (#1459)Aina Niemetz
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback