Age | Commit message (Collapse) | Author | |
---|---|---|---|
2019-11-06 | Support for SyGuS PBE + recursive functions (#3433) | Andrew Reynolds | |
2019-11-04 | Make getSynthSolution return a Bool (#3306) | Andrew Reynolds | |
2019-10-23 | Fixes for SyGuS + regular expressions (#3313) | Andrew Reynolds | |
This commit fixes numerous issues involving the combination of SyGuS and regular expressions. Combining SyGuS and regular expressions may involve constructing regular expressions that are neither variables nor builtin regular expression operators. The code was not robust for this case, either throwing spurious assertion failures or having incorrect behavior. | |||
2019-10-14 | Remove benchmark (#3389) | Andrew Reynolds | |
2019-10-14 | Support UF in default sygus grammars (#3319) | Andrew Reynolds | |
2019-10-14 | Apply sygus repair constant techniques restricted to refinement lemmas (#3386) | Andrew Reynolds | |
2019-10-14 | Ensure lemmas from sygus repair const are guarded (#3385) | Andrew Reynolds | |
2019-09-29 | Avoid cases of empty sygus grammars (#3301) | Andrew Reynolds | |
2019-09-29 | Fail single invocation techniques when utility inference fails. (#3322) | Andrew Reynolds | |
2019-09-27 | Fix case of disjunctive conclusion in strings (#3254) | Andrew Reynolds | |
2019-09-25 | Add isParameterized function to Expr (#3303) | Andrew Reynolds | |
2019-09-13 | Disallow let in sygus grammars, check for free variables in sygus ↵ | Andrew Reynolds | |
constructors (#3259) | |||
2019-09-12 | Fix default grammar construction for arrays when no free variables are ↵ | Andrew Reynolds | |
present (#3225) | |||
2019-08-23 | Exclude redundant lemmas when tracking inst lemmas. (#3210) | Andrew Reynolds | |
2019-08-20 | Fixes for sygus inference on quantifier free problems (#3202) | Andrew Reynolds | |
2019-08-02 | Support default sygus grammar for strings (#3148) | Andrew Reynolds | |
2019-07-19 | Fixes for sygus with datatypes (#3103) | Andrew Reynolds | |
2019-06-11 | Do not require sygus constructors to be flattened (#3049) | Andrew Reynolds | |
2019-04-05 | Fix another corner case of datatypes+PBE (#2938) | Andrew Reynolds | |
2019-04-03 | Fix combination of datatypes + strings in PBE (#2930) | Andrew Reynolds | |
2019-03-22 | More fixes for PBE with datatypes (#2882) | Andrew Reynolds | |
2019-03-21 | Rewrite selectors correctly applied to constructors (#2875) | Andrew Reynolds | |
2019-03-19 | Fix fairness issue with fast sygus enumerator (#2873) | Andrew Reynolds | |
2018-12-19 | Fix issues with REWRITE_DONE in floating point rewriter (#2762) | Andrew Reynolds | |
2018-11-21 | Quickly recognize when PBE conjectures are infeasible (#2718) | Andrew Reynolds | |
Recognizes when the conjecture has conflicting I/O pairs. Also includes a minor change to the default behavior of PBE. This change broke a delicate regression array_search_2, which I fixed by adding some additional options to make it more robust. After this PR, we immediately find 4/7 unsolved in PBE strings of sygusComp 2018 to be infeasible. | |||
2018-11-05 | Allow partial models with optimized sygus enumeration (#2682) | Andrew Reynolds | |
2018-10-09 | Support for basic actively-generated enumerators (#2606) | Andrew Reynolds | |
2018-10-05 | Fix cache for sygus post-condition inference (#2592) | Andrew Reynolds | |
2018-10-05 | Update default options for sygus (#2586) | Andrew Reynolds | |
2018-09-22 | cmake: Added regression tests and target make regress. | Aina Niemetz | |
2018-09-22 | cmake: Added initial build infrastructure. | Aina Niemetz | |
2018-09-13 | Uses information gain heuristic for building better solutions from DTs (#2451) | Haniel Barbosa | |
2018-08-24 | Add tests that enumerate and verify rewrite rules (#2344) | Andres Noetzli | |
2018-08-21 | Fix processing of nested Variable construct in sygus let bodies (#2351) | Andrew Reynolds | |
2018-08-21 | Use cbqi-full for sygus (#2346) | Andrew Reynolds | |
2018-08-20 | Add regressions that increase coverage (#2337) | Andrew Reynolds | |
2018-08-17 | Add sygus stream regressions (#2330) | Andrew Reynolds | |
2018-08-17 | Eliminate partial operators in sygus grammar normalization (#2323) | Andrew Reynolds | |
This corrects a bug that was introduced in #2266 (the hack removed there was necessary). This ensures that we handle operators like bvudiv, bvsdiv, bvurem, div, rem, / properly in sygus. This also enables total semantics for BV div-by-zero for sygus. | |||
2018-08-08 | Disable argument relevance for sygus by default (#2288) | Andrew Reynolds | |
2018-08-06 | Add RegLan to smt2/sygus parsers. (#2276) | Andrew Reynolds | |
2018-08-06 | Remove support for Enum sygus syntax. (#2264) | Andrew Reynolds | |
2018-08-06 | Fixes and improvements for single invocation inference (#2261) | Andrew Reynolds | |
2018-08-06 | Fix degenerate case of sygus grammar construction for 0-argument Bools (#2260) | Andrew Reynolds | |
2018-07-26 | Fix rewriter for lambda (#2211) | Andrew Reynolds | |
The rewriter for lambda is currently too aggressive, there are cases like: lambda xy. x = y that are converted into an array representation that when indexing based on x gives (store y true false), which is subsequently converted to: lambda fv_1 fv_2. fv_1 = y where fv_1 and fv_2 are canonical free variables. Here, y is used as index but was not substituted hence is incorrectly made free. To make things simpler, this PR disables any rewriting for lambda unless the array representation of the lambda is a constant, which hardcodes/simplifies a previous argument (reqConst=true). This fixes a sygus issue I ran into yesterday (regression added in this PR). Some parts of the code were formatted as a result. | |||
2018-07-23 | sygusComp2018: add regressions (#2191) | Andrew Reynolds | |
2018-07-21 | Optimizations and fixes for computing whether a type is finite (#2179) | Andrew Reynolds | |
2018-06-15 | Disable solving non-linear BV literals by default (#2070) | Andrew Reynolds | |
2018-05-21 | Infrastructure to mark unused sygus strategies (#1950) | Andrew Reynolds | |
2018-05-18 | Unified fairness scheme for cegis unif (#1941) | Andrew Reynolds | |
2018-05-17 | Fix debugPrint and add regress. (#1934) | Andrew Reynolds | |