Age | Commit message (Collapse) | Author | |
---|---|---|---|
2018-03-05 | Fix for sampler. (#1639) | Andrew Reynolds | |
2018-03-02 | Optimization for sygus streaming mode (#1636) | Andrew Reynolds | |
2018-03-02 | Simplify sygus wrt miniscoping (#1634) | Andrew Reynolds | |
2018-03-02 | Print candidate rewrites in terms of original grammar (#1635) | Andrew Reynolds | |
2018-03-01 | Create infrastructure for sygus modules (#1632) | Andrew Reynolds | |
2018-02-27 | Minor fixes for rec-fun (#1616) | Andrew Reynolds | |
2018-02-27 | Improvements to sygus sampling (#1621) | Andrew Reynolds | |
2018-02-14 | Quantifiers subdirectories (#1608) | Andrew Reynolds | |
2018-02-12 | Option to use extended rewriter as a preprocessing pass (#1600) | Andrew Reynolds | |
2018-02-12 | Minor improvements to sygus sampler (#1598) | Andrew Reynolds | |
2018-02-10 | More minor improvements to synth-rr (#1597) | Andrew Reynolds | |
2018-02-09 | Move BitVector specific funs from bv::utils to util/bitvector.h. (#1589) | Aina Niemetz | |
2018-02-09 | Class to reduce printing of redundant candidate rewrites (#1588) | Andrew Reynolds | |
2018-02-08 | Adding virtual destructors on classes with virtual functions. (#1583) | Tim King | |
2018-02-08 | Minor improvements to sygus sampling. (#1577) | Andrew Reynolds | |
2018-02-07 | Fixing more inconsistent usages of override. (#1575) | Tim King | |
2018-02-06 | Fixes two memory leaks coming from Transf. (#1564) | Tim King | |
First, it adds a virtual destructor so the subclasses will get cleaned up. Second, it wraps the returned pointer in a unique_ptr. Should fix ASAN failures in the nightly run. | |||
2018-02-06 | Updated copyright header for bv_inverter.(cpp|h). | Aina Niemetz | |
2018-02-06 | Resolving warnings from -Winconsistent-missing-override on clang. (#1563) | Tim King | |
2018-02-05 | Statically eliminate redundant sygus constructors (#1560) | Andrew Reynolds | |
2018-02-04 | Sample based on sygus grammar by default (#1558) | Andrew Reynolds | |
2018-02-02 | Option to use sampling for CEGIS (#1555) | Andrew Reynolds | |
2018-02-02 | Fix remaining synthesis solution regressions (#1557) | Andrew Reynolds | |
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-29 | Generalize explanations for PBE sygus strings based on negative contains ↵ | Andrew Reynolds | |
when multiple strategies are present (#1546) | |||
2018-01-28 | Sort children of all commutative operators for sygus. (#1544) | Andrew Reynolds | |
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 | |
Previously, we computed an inverse for s1 o x, x o s2, s1 o x o s2 while disregarding that invertibility depends on si. This adds this handling as an optional heuristic for concats over (dis)equality since it improves performance on a considerable number of benchmarks. | |||
2018-01-21 | Refactor and fix solveBvLit for CBQI BV. (#1526) | Aina Niemetz | |
This refactors and simplifies solveBvLit() and fixes the following: - generate side conditions for BITVECTOR_NEG, BITVECTOR_NOT, BITVECTOR_PLUS, BITVECTOR_XOR over inequalities and disequality - fix CONCAT handling (generate side conditions rather then computing an inverse which was incorrect) - fix SIGN_EXTEND handling (same as with CONCATs) | |||
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 | |
This removes division by constant handling in the BV inverter introduced in #1498. Division by constant was simplified to: x / s OP t ---> x = t / s^-1 if s odd and there exists a multiplicative modular inverse s^-1. This however, is incorrect since x / s * 1 / s^-1 != x / (s * s^-1) | |||
2018-01-10 | Removing throw specifiers for TypeRules. (#1501) | 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 | |
Removing more miscellaneous throw specifiers. | |||
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. ↵ | Tim King | |
(#1487) | |||
2018-01-05 | Add special {SGE,SGT,NE}_UDIV1 side conditions for BV of size 1. (#1483) | Mathias Preiner | |
This commit further fixes some other issues with bit-vectors of size 1. | |||
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 | |
Includes: - Basic rewriting for choice functions in the builtin rewriter, - Do not consider more than one equal term in ceg instantiator (helps cases where we have a repeated pattern of duplicate instantiations), - Do not introduce dummy extract equalities in the cbqi-bv-rm-extract pass (dummy concat equalities suffice). - Do not consider extracts in nested quantified formulas in the cbqi-bv-rm-extract pass. | |||
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 | |