Adding infrastructure for normalizing SyGuS grammars (#1397)
authorHaniel Barbosa <hanielbbarbosa@gmail.com>
Tue, 21 Nov 2017 23:33:35 +0000 (17:33 -0600)
committerGitHub <noreply@github.com>
Tue, 21 Nov 2017 23:33:35 +0000 (17:33 -0600)
commitb2f4485e9d079806da4e95983dc849b1741c7823
treefaa9ce48a4bfaae47d2385f0b0e9337eb204aa0e
parent60f1dd27da89be80c172e15e01c49f58e0ceb6c0
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
src/Makefile.am
src/options/quantifiers_options
src/theory/quantifiers/sygus_grammar_cons.cpp
src/theory/quantifiers/sygus_grammar_norm.cpp [new file with mode: 0644]
src/theory/quantifiers/sygus_grammar_norm.h [new file with mode: 0644]