summaryrefslogtreecommitdiff
path: root/test/regress/regress1/sygus
AgeCommit message (Collapse)Author
2020-03-20Fix variable shadowing issue in sygus-inference (#4121)Andrew Reynolds
This makes the sygus-inference preprocessing pass avoid variable shadowing, which technically could happen by forcing unexpected options. Fixes #4083.
2020-03-19Fix regression output related to sygus+bv-div-zero (#4122)Andrew Reynolds
2020-03-12Do not make models for quantified function variables (#4039)Andrew Reynolds
If we combine finite model finding and higher-order, then we could try to find a model find operators whose kind was BOUND_VARIABLE.
2020-03-11Guard against null relevancy condition in SyGuS (#4033)Andrew Reynolds
Fixes #4025. Also makes our sygus default grammar for strings (slightly) better by including a dummy character, which is required for solving the regression added by this PR. A more robust (but unintuitive to the user) solution would be to include str.from_code( Start_Int ).
2020-03-11Fix duplicate variable issue in sygus-qe-preproc (#4013)Andrew Reynolds
2020-03-09Rename sygus option name (#3977)Andrew Reynolds
This option enables the sygus solver (previous name was ceGuidedInst, deprecated from CAV 15 specific approach). It also improves when this option is set. In particular we ensure it is enabled when sygus is enabled for any reason.
2020-03-09Ensure standard miniscoping is applied before aggressive miniscoping (#3974)Andrew Reynolds
Fixes #3947.
2020-03-08Rewrite again full for DIV rewrite (#3945)Andrew Reynolds
Fixes #3944.
2020-03-06Support default sygus grammar construction for sets (#3842)Andrew Reynolds
Fixes #3645.
2020-02-28Replace conditional rewrite pass in quantifiers with the extended rewriter ↵Andrew Reynolds
(#3841) Fixes #3839. Previously, the quantifiers rewriter had a rewriting step that was an ad-hoc version of some of the rewrites that have been incorporated into the extended rewriter. Moreover, the code for that pass was buggy. This eliminates the previous conditional rewriting step from the "term process" rewrite pass in quantifiers. It additional adds an optional (disabled by default) rewriting pass that calls the extended rewriter on the body of quantified formulas. This subsumes the previous behavior and should not be buggy. Notice that the indentation in computeProcessTerms changed and subsequently has been updated to the new coding standards. This PR relies on #3840.
2020-02-26Fix regression (#3827)Andrew Reynolds
2020-02-26More fixes for printing sygus commands (#3812)Andrew Reynolds
Towards v1 -> v2 sygus conversion. This makes several fixes and improvements related to printing sygus commands: (1) The logic is extended with LIA, DT, UF internally during setDefaults instead of during parsing. This is the correct place for this extension of the logic since it should be applied regardless of the parser. 5 existing logic bugs were discovered as a result of this in regressions, which are fixed by this PR. (2) Ensures that terms in sygus grammars are printed without letification, since this is prohibited in sygus. Notice the formulas printed by constraints need to be letified (otherwise we can't convert large lustre benchmarks). Thus, the letification threshold should determine this but always be overridden for grammar terms. (3) Ensures final options are set for all sygus-specific commands, which follows the standards prescribed by sygus v2 (all set-* commands come before other commands).
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback