Refactor sygus_util to TermDb. Initial work on solution reconstruction into syntax for single inv properties.

1 files changed, 3 insertions, 0 deletions

diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 78609914f..bdb2795b4 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -39,6 +39,7 @@ class QuantifiersEngine;
 
 namespace quantifiers {
   class TermDb;
+  class TermDbSygus;
 }
 
 class QuantifiersModule {
@@ -290,6 +291,8 @@ public:
   quantifiers::FirstOrderModel* getModel() { return d_model; }
   /** get term database */
   quantifiers::TermDb* getTermDatabase() { return d_term_db; }
+  /** get term database sygus */
+  quantifiers::TermDbSygus* getTermDatabaseSygus();
   /** get trigger database */
   inst::TriggerTrie* getTriggerDatabase() { return d_tr_trie; }
   /** add term to database */