summaryrefslogtreecommitdiff
path: root/test/regress/regress1/sygus
AgeCommit message (Collapse)Author
2020-02-26Use default consts when not using any const during grammar normalization (#3807)Andrew Reynolds
Fixes #3802. If we decide not to add the any constant constructor due to insufficient cegqi algorithms (or if the sort is Boolean), then we should add the default constants for a sort.
2020-02-12Ensure ext rewrites for associative ops dont throw assertions for kind ↵Andrew Reynolds
arities (#3681)
2020-01-30Eliminate spurious postprocessing step for single invocation (#3674)Andrew Reynolds
2020-01-28Do not insist on bound values being constant in arithmetic instantiation (#3643)Andrew Reynolds
2020-01-23Fix trivial solve method for single invocation (#3650)Andrew Reynolds
2020-01-22Fix single invocation partition for non-function non-atomic types (#3642)Andrew Reynolds
2020-01-22Fix check for subtypes in sygus PBE (#3640)Andrew Reynolds
2020-01-14Generalize example-based sym breaking to conjectures with constant function ↵Andrew Reynolds
apps (#3605)
2020-01-10Fix side condition check in sygus core connective (#3600)Andrew Reynolds
2020-01-10Track trivial cases in transition inference (#3598)Andrew Reynolds
2020-01-08Fix backtracking issue in sygus fast enumerator (#3593)Andrew Reynolds
2020-01-07Update any-constant and normalization policies for sygus grammars (#3583)Andrew Reynolds
2019-12-13Disable check-synth-sol in regression with recursive functions (#3560)Andrew Reynolds
2019-12-12Fix Unif+PI algorithm with symbolic unfolding (#3558)Haniel Barbosa
2019-12-12Fixes for regressions (#3557)Andrew Reynolds
2019-12-11Fix CEGIS refinement for recursive functions evaluation (#3555)Andrew Reynolds
2019-12-08[Regressions] Require proof support for abduction (#3546)Andres Noetzli
2019-12-06New algorithm for interpolation and abduction based on unsat cores (#3255)Andrew Reynolds
2019-12-05Refactor mode options for Unif+PI (#3531)Andrew Reynolds
2019-12-04New grammar construction modes for SyGuS (#3486)Andrew Reynolds
2019-12-04Fix (#3530)Andrew Reynolds
2019-12-04Fix single invocation solution construction for multiple function case (#3516)Andrew Reynolds
2019-12-02Fix case of higher-order + sygus inference (#3509)Andrew Reynolds
2019-11-29Fix fast SyGuS enumeration for interpreted constants (#3501)Andrew Reynolds
2019-11-27Fix sygus inference for choice functions introduced at preprocess (#3500)Andrew Reynolds
2019-11-27Enable sygusRecFun by default and fixes SyGuS+RecFun+HO issues (#3502)Haniel Barbosa
2019-11-22fixing stupid typo (#3488)Haniel Barbosa
2019-11-21hard limit for rec-fun eval (#3485)Haniel Barbosa
2019-11-20Lazy evaluation via rec-funs of ITE expressions (#3482)Haniel Barbosa
2019-11-15Fix wrong kind in sygus version 1 parser (#3463)Andrew Reynolds
2019-11-10Fix bugs related to sygus higher-order + recursive functions (#3448)Andrew Reynolds
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback