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/Makefile.am | |
| 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/Makefile.am')
| -rw-r--r-- | src/Makefile.am | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/Makefile.am b/src/Makefile.am index f5694dc71..dc0a2b62a 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -445,6 +445,8 @@ libcvc4_la_SOURCES = \ theory/quantifiers/sygus_invariance.h \ theory/quantifiers/sygus_grammar_cons.cpp \ theory/quantifiers/sygus_grammar_cons.h \ + theory/quantifiers/sygus_grammar_norm.cpp \ + theory/quantifiers/sygus_grammar_norm.h \ theory/quantifiers/sygus_process_conj.cpp \ theory/quantifiers/sygus_process_conj.h \ theory/quantifiers/symmetry_breaking.cpp \ |