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.

2 files changed, 15 insertions, 0 deletions

diff --git a/src/printer/sygus_print_callback.cpp b/src/printer/sygus_print_callback.cpp
index c5287e469..77f68e097 100644
--- a/src/printer/sygus_print_callback.cpp
+++ b/src/printer/sygus_print_callback.cpp
@@ -208,5 +208,7 @@ void SygusEmptyPrintCallback::toStreamSygus(const Printer* p,
   }
 }
 
+std::shared_ptr<SygusEmptyPrintCallback> SygusEmptyPrintCallback::d_empty_pc = nullptr;
+
 } /* CVC4::printer namespace */
 } /* CVC4 namespace */
diff --git a/src/printer/sygus_print_callback.h b/src/printer/sygus_print_callback.h
index 84da0f86c..e0c220e00 100644
--- a/src/printer/sygus_print_callback.h
+++ b/src/printer/sygus_print_callback.h
@@ -154,6 +154,19 @@ class CVC4_PUBLIC SygusEmptyPrintCallback : public SygusPrintCallback
   virtual void toStreamSygus(const Printer* p,
                              std::ostream& out,
                              Expr e) const override;
+  /* Retrieves empty callback pointer */
+  static inline std::shared_ptr<SygusEmptyPrintCallback> getEmptyPC()
+  {
+    if (!d_empty_pc)
+    {
+      d_empty_pc = std::make_shared<SygusEmptyPrintCallback>();
+    }
+    return d_empty_pc;
+  }
+
+ private:
+  /* empty callback object */
+  static std::shared_ptr<SygusEmptyPrintCallback> d_empty_pc;
 };
 
 } /* CVC4::printer namespace */