| Age | Commit message (Expand) | Author |
|---|
| 2018-02-02 | Option to use sampling for CEGIS (#1555) | Andrew Reynolds |
| 2018-02-02 | Restoring ostream format. Resolves a few CIDs 1362780. (#1543) | Tim King |
| 2018-02-02 | Fix remaining synthesis solution regressions (#1557) | Andrew Reynolds |
| 2018-02-02 | Option to check solutions produced by SyGuS solver (#1553) | Haniel Barbosa |
| 2018-02-01 | Add interface in sygus to get synthesis solution Nodes (#1552) | Andrew Reynolds |
| 2018-02-01 | Use sygus to synthesize/verify rewrite rules (#1547) | Andrew Reynolds |
| 2018-01-30 | Further clean and document datatypes rewriter (#1548) | Andrew Reynolds |
| 2018-01-29 | Generalize explanations for PBE sygus strings based on negative contains when... | Andrew Reynolds |
| 2018-01-28 | Sort children of all commutative operators for sygus. (#1544) | Andrew Reynolds |
| 2018-01-26 | Removing structurally dead code. (#1540) | Tim King |
| 2018-01-23 | Fix MULT handling for CBQI BV. (#1531) | Aina Niemetz |
| 2018-01-23 | Commenting out throw specifiers for DeltaRationExceptions. These functions ca... | Tim King |
| 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-17 | Removes yet more throw specifiers. Updating the documentation as needed. (#1518) | Tim King |
| 2018-01-15 | Removing more miscellaneous throw specifiers. (#1509) | Tim King |
| 2018-01-13 | Remove BITVECTOR_SUB from isInvertible(). (#1513) | Aina Niemetz |
| 2018-01-12 | Improvements for CBQI BV (#1504) | Andrew Reynolds |
| 2018-01-10 | Removed division by constant handling for CBQI BV (unsound). (#1508) | Aina Niemetz |
| 2018-01-10 | Removing throw specifiers for TypeRules. (#1501) | Tim King |
| 2018-01-10 | Removing throw specifiers from type enumerators. (#1502) | Tim King |
| 2018-01-09 | Cleaning up throw specifiers on Exception and subclasses. (#1475) | Tim King |
| 2018-01-09 | Fix linearization for terms where the solve variable does not occur. (#1506) | Mathias Preiner |
| 2018-01-08 | Removing more miscellaneous throw specifiers. (#1488) | Tim King |
| 2018-01-08 | Add bv util mkConst(unsigned, Integer&). (#1499) | 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-07 | Re-ordering field initialization in QuantInfo to remove compiler warning. (#1... | Tim King |
| 2018-01-07 | Removes RationalFromDoubleException. Replaces this with an explicit M… (#1476) | Tim King |
| 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-04 | Improvements for CBQI (#1478) | Andrew Reynolds |
| 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-03 | Global negate (#1466) | Andrew Reynolds |
| 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 | Rewrites for BitVector multiplication (#1465) | Andrew Reynolds |
| 2018-01-02 | Add side conditions for inequalities of LSHR. (#1462) | Mathias Preiner |
| 2018-01-02 | Improve rewriter for string equality (#1427) | Andrew Reynolds |
| 2017-12-29 | Add side conditions for inequalities over BITVECTOR_UREM for CBQI BV. (#1460) | Aina Niemetz |
| 2017-12-29 | Cbqi repeat solve literal (#1458) | Andrew Reynolds |
| 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 |
