Normalize grammars - 2 (#1420)
authorHaniel Barbosa <hanielbbarbosa@gmail.com>
Sun, 3 Dec 2017 19:18:42 +0000 (13:18 -0600)
committerGitHub <noreply@github.com>
Sun, 3 Dec 2017 19:18:42 +0000 (13:18 -0600)
commit612e4e2a58e3bd47708b7e6f8771b539ee1383bf
tree54f58134f004a212600c14b6970ddc0b95d181d6
parent3179bfe0fff1372b4080196dd28f0079d859830f
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.
src/options/quantifiers_options
src/printer/sygus_print_callback.cpp
src/printer/sygus_print_callback.h
src/theory/quantifiers/sygus_grammar_cons.cpp
src/theory/quantifiers/sygus_grammar_norm.cpp
src/theory/quantifiers/sygus_grammar_norm.h
src/theory/quantifiers/term_database_sygus.cpp