SyGuS instantiation quantifiers module (#3910)

1 files changed, 11 insertions, 2 deletions

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 6e60780d6..e4caaa539 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -29,6 +29,7 @@
 #include "theory/quantifiers/quant_split.h"
 #include "theory/quantifiers/quantifiers_rewriter.h"
 #include "theory/quantifiers/sygus/synth_engine.h"
+#include "theory/quantifiers/sygus_inst.h"
 #include "theory/sep/theory_sep.h"
 #include "theory/theory_engine.h"
 #include "theory/uf/equality_engine.h"
@@ -54,7 +55,8 @@ class QuantifiersEnginePrivate
         d_fs(nullptr),
         d_i_cbqi(nullptr),
         d_qsplit(nullptr),
-        d_anti_skolem(nullptr)
+        d_anti_skolem(nullptr),
+        d_sygus_inst(nullptr)
   {
   }
   ~QuantifiersEnginePrivate() {}
@@ -85,6 +87,8 @@ class QuantifiersEnginePrivate
   std::unique_ptr<quantifiers::QuantDSplit> d_qsplit;
   /** quantifiers anti-skolemization */
   std::unique_ptr<quantifiers::QuantAntiSkolem> d_anti_skolem;
+  /** SyGuS instantiation engine */
+  std::unique_ptr<quantifiers::SygusInst> d_sygus_inst;
   //------------------------------ end quantifiers modules
   /** initialize
    *
@@ -159,6 +163,11 @@ class QuantifiersEnginePrivate
       d_fs.reset(new quantifiers::InstStrategyEnum(qe, d_rel_dom.get()));
       modules.push_back(d_fs.get());
     }
+    if (options::sygusInst())
+    {
+      d_sygus_inst.reset(new quantifiers::SygusInst(qe));
+      modules.push_back(d_sygus_inst.get());
+    }
   }
 };
 
@@ -203,7 +212,7 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c,
   d_util.push_back(d_term_util.get());
   d_util.push_back(d_term_db.get());
 
-  if (options::sygus())
+  if (options::sygus() || options::sygusInst())
   {
     d_sygus_tdb.reset(new quantifiers::TermDbSygus(c, this));
   }