Age | Commit message (Collapse) | Author | |
---|---|---|---|
2018-04-08 | Allow predetermined first-order variables when constructing deep embedding. ↵ | Andrew Reynolds | |
(#1757) | |||
2018-04-08 | Check free variables in assertions (#1737) | Andrew Reynolds | |
2018-04-08 | Add quantifier name attribute. (#1756) | Andrew Reynolds | |
2018-04-05 | Add more general SignExtendUltConst rewriting. (#1385) | Mathias Preiner | |
This also adds an additional check in processAssertions to ensure that all assertions are guaranteed to be rewritten (there was only a comment stating this). | |||
2018-04-04 | Proper initialization and destruction of sygus unif (#1750) | Andrew Reynolds | |
2018-04-04 | Fix for corner case of higher-order matching (#1708) | Andrew Reynolds | |
2018-04-04 | Do not debug check models when unknown (#1748) | Andrew Reynolds | |
2018-04-04 | Fix sygus infer (#1747) | Andrew Reynolds | |
2018-04-03 | Option to turn arbitrary input into sygus (#1704) | Andrew Reynolds | |
Preprocessing pass that turns an arbitrary (e.g. smt2) input into a sygus conjecture, which is helpful for Horn clause solving. This includes improvements to the robustness of the sygus solver. | |||
2018-04-03 | Make sygus unif I/O an subclass of sygus unif (#1741) | Andrew Reynolds | |
2018-04-03 | Use choice when expanding definitions for inverse transcendental functions ↵ | Andrew Reynolds | |
(#1742) | |||
2018-04-03 | Internal sygus type checking (#1734) | Andrew Reynolds | |
2018-04-02 | Improvements to extended rewriter for Booleans and ITE (#1705) | Andrew Reynolds | |
2018-04-02 | Make sygus unif utility use sygus unif strategies (#1732) | Andrew Reynolds | |
2018-04-02 | Reorganize bitblaster code. (#1695) | Mathias Preiner | |
This splits bitblaster_template.h into the separate header files {aig,eager,lazy}_bitblaster.h and bitblaster.h (the template class TBitblaster). All the bitblaster related code is moved into the sub-directory bitblast/. | |||
2018-03-30 | Split strategy representation from SygusUnif (#1730) | Andrew Reynolds | |
2018-03-30 | Do not use factoring inference for transcendental functions (#1707) | Andrew Reynolds | |
2018-03-29 | Simplify sygus unif so that it is one-to-one with functions to synthesize ↵ | Andrew Reynolds | |
(#1726) | |||
2018-03-27 | Make sygus pbe use sygus unif utility (#1724) | Andrew Reynolds | |
2018-03-27 | Fix for --sygus-rr-synth (#1723) | Andrew Reynolds | |
2018-03-27 | Make sygus unif utility (#1720) | Andrew Reynolds | |
2018-03-27 | Filter candidate rewrites based on matching (#1682) | Andrew Reynolds | |
2018-03-26 | Better normalization of string concatenation (#1719) | Andres Noetzli | |
2018-03-26 | Documentation and simplifications for PBE (#1677) | Andrew Reynolds | |
2018-03-26 | Add reasoning for inequalities in str rewriter (#1713) | Andres Noetzli | |
2018-03-26 | Synth-check and accelerate options for sygus-rr (#1691) | Andrew Reynolds | |
2018-03-26 | Abort when sygus-verify finds unsoundness. (#1717) | Andrew Reynolds | |
2018-03-26 | Rewrites for substr of strings of length one (#1712) | Andres Noetzli | |
This commit adds a rewrite for substrings of strings of length one to the empty string if it can be shown that it is not possible that the start position and the length are both greater than zero: ``` (str.substr "A" x y) --> "" if x = 0 |= 0 >= y ``` The commit introduces a set of functions to check such entailments with assumptions. | |||
2018-03-25 | Cleanup various exit calls (#1692) | Andrew Reynolds | |
2018-03-23 | Remove abstract regular expression constant (#1698) | Andrew Reynolds | |
2018-03-23 | Remove unused code (#1700) | Andrew Reynolds | |
2018-03-23 | Minor reorganization for ematching (#1701) | Andrew Reynolds | |
2018-03-23 | Enable post-condition strenghtening by default for non-syntax restricted ↵ | Andrew Reynolds | |
invariant synthesis (#1703) | |||
2018-03-21 | More rewrites for indexof (#1648) | Andrew Reynolds | |
2018-03-21 | Fix for string disequality processing (#1679) | Andrew Reynolds | |
2018-03-20 | Add support for CaDiCaL as eager BV SAT solver. (#1675) | Mathias Preiner | |
2018-03-20 | Minor refactor datatypes sygus (#1673) | Andrew Reynolds | |
2018-03-20 | Internally remove redundant assertions and infer equalities in ↵ | Andrew Reynolds | |
NonLinearExtension (#1633) | |||
2018-03-20 | Minor fix and addition to sygus sampler (#1678) | Andrew Reynolds | |
2018-03-19 | Enable CEGQI for non-linear (#1674) | Andrew Reynolds | |
2018-03-19 | Document inferences for strings (#1642) | Andrew Reynolds | |
2018-03-09 | Some minor cleanup in bv::utils. (#1663) | Aina Niemetz | |
2018-03-08 | Fix Travis for unit test compilation errors. (#1651) | Mathias Preiner | |
make units does not fail if we have compile error for a unit test, however, make check does. -Wsuggest-override is now explicitly disabled for unit tests since CxxTest does not add override keywords to the generated source code and thus get a lot of compiler warnings. Further, this fixes some issues introduced with #1647 due to make units not failing on Travis and fixes the nightly builds. | |||
2018-03-06 | Make statistics output consistent. (#1647) | Mathias Preiner | |
* Fixes --hide-zero-stats (and really skips the 0 values) * Removes the additional newline after each statistic * Introduces theory::getStatsPrefix(TheoryId) to generate consistent prefixes for statistics based on the theory id (e.g., THEORY_BV -> "theory::bv"). | |||
2018-03-06 | Simplify initialization of quantifiers engine (#1641) | Andrew Reynolds | |
2018-03-06 | Refactor symmetry breaking in datatypes sygus (#1640) | Andrew Reynolds | |
2018-03-05 | Update semantics for string indexof and replace (#1630) | Andrew Reynolds | |
2018-03-05 | Enable -Wsuggest-override by default. (#1643) | Mathias Preiner | |
Adds missing override keywords. | |||
2018-03-05 | Fix for sampler. (#1639) | Andrew Reynolds | |
2018-03-02 | Optimization for sygus streaming mode (#1636) | Andrew Reynolds | |