Age | Commit message (Collapse) | Author | |
---|---|---|---|
2020-03-20 | Fix 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-19 | Fix regression output related to sygus+bv-div-zero (#4122) | Andrew Reynolds | |
2020-03-12 | Do 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-11 | Guard 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-11 | Fix duplicate variable issue in sygus-qe-preproc (#4013) | Andrew Reynolds | |
2020-03-09 | Rename 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-09 | Ensure standard miniscoping is applied before aggressive miniscoping (#3974) | Andrew Reynolds | |
Fixes #3947. | |||
2020-03-08 | Rewrite again full for DIV rewrite (#3945) | Andrew Reynolds | |
Fixes #3944. | |||
2020-03-06 | Support default sygus grammar construction for sets (#3842) | Andrew Reynolds | |
Fixes #3645. | |||
2020-02-28 | Replace 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-26 | Fix regression (#3827) | Andrew Reynolds | |
2020-02-26 | More 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-26 | Use 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-12 | Ensure ext rewrites for associative ops dont throw assertions for kind ↵ | Andrew Reynolds | |
arities (#3681) | |||
2020-01-30 | Eliminate spurious postprocessing step for single invocation (#3674) | Andrew Reynolds | |
2020-01-28 | Do not insist on bound values being constant in arithmetic instantiation (#3643) | Andrew Reynolds | |
2020-01-23 | Fix trivial solve method for single invocation (#3650) | Andrew Reynolds | |
2020-01-22 | Fix single invocation partition for non-function non-atomic types (#3642) | Andrew Reynolds | |
2020-01-22 | Fix check for subtypes in sygus PBE (#3640) | Andrew Reynolds | |
2020-01-14 | Generalize example-based sym breaking to conjectures with constant function ↵ | Andrew Reynolds | |
apps (#3605) | |||
2020-01-10 | Fix side condition check in sygus core connective (#3600) | Andrew Reynolds | |
2020-01-10 | Track trivial cases in transition inference (#3598) | Andrew Reynolds | |
2020-01-08 | Fix backtracking issue in sygus fast enumerator (#3593) | Andrew Reynolds | |
2020-01-07 | Update any-constant and normalization policies for sygus grammars (#3583) | Andrew Reynolds | |
2019-12-13 | Disable check-synth-sol in regression with recursive functions (#3560) | Andrew Reynolds | |
2019-12-12 | Fix Unif+PI algorithm with symbolic unfolding (#3558) | Haniel Barbosa | |
2019-12-12 | Fixes for regressions (#3557) | Andrew Reynolds | |
2019-12-11 | Fix CEGIS refinement for recursive functions evaluation (#3555) | Andrew Reynolds | |
2019-12-08 | [Regressions] Require proof support for abduction (#3546) | Andres Noetzli | |
2019-12-06 | New algorithm for interpolation and abduction based on unsat cores (#3255) | Andrew Reynolds | |
2019-12-05 | Refactor mode options for Unif+PI (#3531) | Andrew Reynolds | |
2019-12-04 | New grammar construction modes for SyGuS (#3486) | Andrew Reynolds | |
2019-12-04 | Fix (#3530) | Andrew Reynolds | |
2019-12-04 | Fix single invocation solution construction for multiple function case (#3516) | Andrew Reynolds | |
2019-12-02 | Fix case of higher-order + sygus inference (#3509) | Andrew Reynolds | |
2019-11-29 | Fix fast SyGuS enumeration for interpreted constants (#3501) | Andrew Reynolds | |
2019-11-27 | Fix sygus inference for choice functions introduced at preprocess (#3500) | Andrew Reynolds | |
2019-11-27 | Enable sygusRecFun by default and fixes SyGuS+RecFun+HO issues (#3502) | Haniel Barbosa | |
2019-11-22 | fixing stupid typo (#3488) | Haniel Barbosa | |
2019-11-21 | hard limit for rec-fun eval (#3485) | Haniel Barbosa | |
2019-11-20 | Lazy evaluation via rec-funs of ITE expressions (#3482) | Haniel Barbosa | |
2019-11-15 | Fix wrong kind in sygus version 1 parser (#3463) | Andrew Reynolds | |
2019-11-10 | Fix bugs related to sygus higher-order + recursive functions (#3448) | Andrew Reynolds | |
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 | |