diff options
| author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2017-11-21 17:33:35 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-11-21 17:33:35 -0600 |
| commit | b2f4485e9d079806da4e95983dc849b1741c7823 (patch) | |
| tree | faa9ce48a4bfaae47d2385f0b0e9337eb204aa0e /src/options | |
| parent | 60f1dd27da89be80c172e15e01c49f58e0ceb6c0 (diff) | |
Adding infrastructure for normalizing SyGuS grammars (#1397)
* minor
Using string previously computed
* adding option
* starting module for simplifying grammars
* more
* more
* fix
* fix
* fix
* fix
* fix
* removing unused command
* removing unused command
* removing unnecessary quantifier engine
* adding lambda support
* transient
* reverting changes
* starting normalization of integers
* removing unnecessary objects
* using for_each
* rebuilding given datatypes
* recrating types as given
* bug fixing
* minor
* reverting space changes
* addressing review
* addressing review
Diffstat (limited to 'src/options')
| -rw-r--r-- | src/options/quantifiers_options | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index 8106c5e5d..1a4275d77 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -272,6 +272,8 @@ option sygusMinGrammarAgg --sygus-min-grammar-agg bool :default false aggressively minimize sygus grammars option sygusAddConstGrammar --sygus-add-const-grammar bool :default true statically add constants appearing in conjecture to grammars +option sygusNormalizeGrammar --sygus-norm-grammar bool :default false + statically normalize sygus grammars based on flattening option sygusTemplEmbedGrammar --sygus-templ-embed-grammar bool :default false embed sygus templates into grammars |