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.

1 files changed, 1 insertions, 4 deletions

diff --git a/src/theory/quantifiers/term_database_sygus.cpp b/src/theory/quantifiers/term_database_sygus.cpp
index 8625d9089..295d7fb52 100644
--- a/src/theory/quantifiers/term_database_sygus.cpp
+++ b/src/theory/quantifiers/term_database_sygus.cpp
@@ -237,8 +237,6 @@ Node TermDbSygus::getGenericBase( TypeNode tn, const Datatype& dt, int c ) {
     Trace("sygus-db-debug") << "Sygus DB : Generic is " << g << std::endl;
     Node gr = Rewriter::rewrite( g );
     Trace("sygus-db-debug") << "Sygus DB : Generic rewritten is " << gr << std::endl;
-    gr = Node::fromExpr( smt::currentSmtEngine()->expandDefinitions( gr.toExpr() ) );
-    Trace("sygus-db-debug") << "Sygus DB : Generic base " << dt[c].getName() << " : " << gr << std::endl;
     d_generic_base[tn][c] = gr;
     return gr;
   }else{
@@ -411,8 +409,7 @@ Node TermDbSygus::getNormalized(TypeNode t, Node prog)
 {
   std::map< Node, Node >::iterator itn = d_normalized[t].find( prog );
   if( itn==d_normalized[t].end() ){
-    Node progr = Node::fromExpr( smt::currentSmtEngine()->expandDefinitions( prog.toExpr() ) );
-    progr = Rewriter::rewrite( progr );
+    Node progr = Rewriter::rewrite( prog );
     Trace("sygus-sym-break2") << "...rewrites to " << progr << std::endl;
     d_normalized[t][prog] = progr;
     return progr;