diff options
| author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2017-12-03 13:18:42 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-12-03 13:18:42 -0600 |
| commit | 612e4e2a58e3bd47708b7e6f8771b539ee1383bf (patch) | |
| tree | 54f58134f004a212600c14b6970ddc0b95d181d6 /src/options | |
| parent | 3179bfe0fff1372b4080196dd28f0079d859830f (diff) | |
Normalize grammars - 2 (#1420)
This is another step towards addressing #1304 and #1344. This pull request:
- Refactors SygusGrammarNorm
- Makes SyGusGrammarNorm a default component in the construction of grammar. The linearization of grammars however only occurs if the option --sygus-grammar-norm is used.
- Performs a "chain transformation" in the application of the PLUS operator in integer grammars
- Removes redundant expansions of definitions from TermDbSygus
- Adds a default empty print callback to SygusEmptyPrintCallback
This lays the basis for more general linearizations.
Diffstat (limited to 'src/options')
| -rw-r--r-- | src/options/quantifiers_options | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index 4a7a9e8a7..f997a8923 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -272,8 +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 sygusGrammarNorm --sygus-grammar-norm bool :default false + statically normalize sygus grammars based on flattening (linearization) option sygusTemplEmbedGrammar --sygus-templ-embed-grammar bool :default false embed sygus templates into grammars |