summaryrefslogtreecommitdiff
path: root/test/regress/regress1/sygus
AgeCommit message (Collapse)Author
2019-11-06Support for SyGuS PBE + recursive functions (#3433)Andrew Reynolds
2019-11-04Make getSynthSolution return a Bool (#3306)Andrew Reynolds
2019-10-23Fixes 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-14Remove benchmark (#3389)Andrew Reynolds
2019-10-14Support UF in default sygus grammars (#3319)Andrew Reynolds
2019-10-14Apply sygus repair constant techniques restricted to refinement lemmas (#3386)Andrew Reynolds
2019-10-14Ensure lemmas from sygus repair const are guarded (#3385)Andrew Reynolds
2019-09-29Avoid cases of empty sygus grammars (#3301)Andrew Reynolds
2019-09-29Fail single invocation techniques when utility inference fails. (#3322)Andrew Reynolds
2019-09-27Fix case of disjunctive conclusion in strings (#3254)Andrew Reynolds
2019-09-25Add isParameterized function to Expr (#3303)Andrew Reynolds
2019-09-13Disallow 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-23Exclude redundant lemmas when tracking inst lemmas. (#3210)Andrew Reynolds
2019-08-20Fixes for sygus inference on quantifier free problems (#3202)Andrew Reynolds
2019-08-02Support default sygus grammar for strings (#3148)Andrew Reynolds
2019-07-19Fixes for sygus with datatypes (#3103)Andrew Reynolds
2019-06-11Do not require sygus constructors to be flattened (#3049)Andrew Reynolds
2019-04-05Fix another corner case of datatypes+PBE (#2938)Andrew Reynolds
2019-04-03Fix combination of datatypes + strings in PBE (#2930)Andrew Reynolds
2019-03-22More fixes for PBE with datatypes (#2882)Andrew Reynolds
2019-03-21Rewrite selectors correctly applied to constructors (#2875)Andrew Reynolds
2019-03-19Fix fairness issue with fast sygus enumerator (#2873)Andrew Reynolds
2018-12-19Fix issues with REWRITE_DONE in floating point rewriter (#2762)Andrew Reynolds
2018-11-21Quickly 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-05Allow 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-05Update default options for sygus (#2586)Andrew Reynolds
2018-09-22cmake: Added regression tests and target make regress.Aina Niemetz
2018-09-22cmake: Added initial build infrastructure.Aina Niemetz
2018-09-13Uses information gain heuristic for building better solutions from DTs (#2451)Haniel Barbosa
2018-08-24Add 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-21Use cbqi-full for sygus (#2346)Andrew Reynolds
2018-08-20Add 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-08Disable argument relevance for sygus by default (#2288)Andrew Reynolds
2018-08-06Add RegLan to smt2/sygus parsers. (#2276)Andrew Reynolds
2018-08-06Remove support for Enum sygus syntax. (#2264)Andrew Reynolds
2018-08-06 Fixes and improvements for single invocation inference (#2261)Andrew Reynolds
2018-08-06Fix degenerate case of sygus grammar construction for 0-argument Bools (#2260)Andrew Reynolds
2018-07-26Fix 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-21Optimizations and fixes for computing whether a type is finite (#2179)Andrew Reynolds
2018-06-15Disable solving non-linear BV literals by default (#2070)Andrew Reynolds
2018-05-21Infrastructure to mark unused sygus strategies (#1950)Andrew Reynolds
2018-05-18Unified fairness scheme for cegis unif (#1941)Andrew Reynolds
2018-05-17Fix debugPrint and add regress. (#1934)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback