Encapsulate synth engine (#3271)

7 files changed, 42 insertions, 49 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 3d469f2b5..1cec8e123 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -3213,15 +3213,6 @@ void SmtEnginePrivate::processAssertions() {
     d_passes["nl-ext-purify"]->apply(&d_assertions);
   }
 
-  if( options::ceGuidedInst() ){
-    //register sygus conjecture pre-rewrite (motivated by solution reconstruction)
-    for (unsigned i = 0; i < d_assertions.size(); ++ i) {
-      d_smt.d_theoryEngine->getQuantifiersEngine()
-          ->getSynthEngine()
-          ->preregisterAssertion(d_assertions[i]);
-    }
-  }
-
   if (options::solveRealAsInt()) {
     d_passes["real-to-int"]->apply(&d_assertions);
   }
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index fcfef1541..e2a8540d4 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -43,8 +43,9 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-SynthConjecture::SynthConjecture(QuantifiersEngine* qe)
+SynthConjecture::SynthConjecture(QuantifiersEngine* qe, SynthEngine* p)
     : d_qe(qe),
+      d_parent(p),
       d_tds(qe->getTermDatabaseSygus()),
       d_hasSolution(false, qe->getUserContext()),
       d_ceg_si(new CegSingleInv(qe, this)),
@@ -1045,8 +1046,7 @@ void SynthConjecture::printSynthSolution(std::ostream& out)
       ss << prog;
       std::string f(ss.str());
       f.erase(f.begin());
-      SynthEngine* cei = d_qe->getSynthEngine();
-      ++(cei->d_statistics.d_solutions);
+      ++(d_parent->d_statistics.d_solutions);
 
       bool is_unique_term = true;
 
@@ -1086,11 +1086,11 @@ void SynthConjecture::printSynthSolution(std::ostream& out)
         is_unique_term = d_exprm[prog].addTerm(sol, out, rew_print);
         if (rew_print)
         {
-          ++(cei->d_statistics.d_candidate_rewrites_print);
+          ++(d_parent->d_statistics.d_candidate_rewrites_print);
         }
         if (!is_unique_term)
         {
-          ++(cei->d_statistics.d_filtered_solutions);
+          ++(d_parent->d_statistics.d_filtered_solutions);
         }
       }
       if (is_unique_term)
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h
index 33fff6844..8ae30f636 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.h
+++ b/src/theory/quantifiers/sygus/synth_conjecture.h
@@ -34,6 +34,8 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
+class SynthEngine;
+
 /**
  * A base class for generating values for actively-generated enumerators.
  * At a high level, the job of this class is to accept a stream of "abstract
@@ -68,7 +70,7 @@ class EnumValGenerator
 class SynthConjecture
 {
  public:
-  SynthConjecture(QuantifiersEngine* qe);
+  SynthConjecture(QuantifiersEngine* qe, SynthEngine* p);
   ~SynthConjecture();
   /** presolve */
   void presolve();
@@ -165,6 +167,8 @@ class SynthConjecture
  private:
   /** reference to quantifier engine */
   QuantifiersEngine* d_qe;
+  /** pointer to the synth engine that owns this */
+  SynthEngine* d_parent;
   /** term database sygus of d_qe */
   TermDbSygus* d_tds;
   /** The feasible guard. */
diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp
index f78886249..d13bd2dcf 100644
--- a/src/theory/quantifiers/sygus/synth_engine.cpp
+++ b/src/theory/quantifiers/sygus/synth_engine.cpp
@@ -35,8 +35,8 @@ namespace quantifiers {
 SynthEngine::SynthEngine(QuantifiersEngine* qe, context::Context* c)
     : QuantifiersModule(qe)
 {
-  d_conjs.push_back(
-      std::unique_ptr<SynthConjecture>(new SynthConjecture(d_quantEngine)));
+  d_conjs.push_back(std::unique_ptr<SynthConjecture>(
+      new SynthConjecture(d_quantEngine, this)));
   d_conj = d_conjs.back().get();
 }
 
@@ -255,8 +255,8 @@ void SynthEngine::assignConjecture(Node q)
   // allocate a new synthesis conjecture if not assigned
   if (d_conjs.back()->isAssigned())
   {
-    d_conjs.push_back(
-        std::unique_ptr<SynthConjecture>(new SynthConjecture(d_quantEngine)));
+    d_conjs.push_back(std::unique_ptr<SynthConjecture>(
+        new SynthConjecture(d_quantEngine, this)));
   }
   d_conjs.back()->assign(q);
 }
diff --git a/src/theory/quantifiers/sygus/synth_engine.h b/src/theory/quantifiers/sygus/synth_engine.h
index c4c09e7e6..e099657ad 100644
--- a/src/theory/quantifiers/sygus/synth_engine.h
+++ b/src/theory/quantifiers/sygus/synth_engine.h
@@ -86,9 +86,9 @@ class SynthEngine : public QuantifiersModule
    *
    * The purpose of this method is to inform the solution reconstruction
    * techniques within the single invocation module that n is an original
-   * assertion, prior to rewriting. This is used as a heuristic to remember
-   * terms that are likely to help when trying to reconstruct a solution
-   * that fits a given input syntax.
+   * assertion. This is used as a heuristic to remember terms that are likely
+   * to help when trying to reconstruct a solution that fits a given input
+   * syntax.
    */
   void preregisterAssertion(Node n);
 
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index a03596060..a6ec1c077 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -385,11 +385,6 @@ inst::TriggerTrie* QuantifiersEngine::getTriggerDatabase() const
   return d_tr_trie.get();
 }
 
-quantifiers::SynthEngine* QuantifiersEngine::getSynthEngine() const
-{
-  return d_private->d_synth_e.get();
-}
-
 QuantifiersModule * QuantifiersEngine::getOwner( Node q ) {
   std::map< Node, QuantifiersModule * >::iterator it = d_owner.find( q );
   if( it==d_owner.end() ){
@@ -527,24 +522,32 @@ void QuantifiersEngine::ppNotifyAssertions(
   Trace("quant-engine-proc")
       << "ppNotifyAssertions in QE, #assertions = " << assertions.size()
       << " check epr = " << (d_qepr != NULL) << std::endl;
-  if ((options::instLevelInputOnly() && options::instMaxLevel() != -1) ||
-      d_qepr != NULL) {
-    for (unsigned i = 0; i < assertions.size(); i++) {
-      if (options::instLevelInputOnly() && options::instMaxLevel() != -1) {
-        quantifiers::QuantAttributes::setInstantiationLevelAttr(assertions[i],
-                                                                0);
-      }
-      if (d_qepr != NULL) {
-        d_qepr->registerAssertion(assertions[i]);
-      }
+  if (options::instLevelInputOnly() && options::instMaxLevel() != -1)
+  {
+    for (const Node& a : assertions)
+    {
+      quantifiers::QuantAttributes::setInstantiationLevelAttr(a, 0);
     }
-    if (d_qepr != NULL) {
-      // must handle sources of other new constants e.g. separation logic
-      // FIXME: cleanup
-      sep::TheorySep* theory_sep =
-          static_cast<sep::TheorySep*>(getTheoryEngine()->theoryOf(THEORY_SEP));
-      theory_sep->initializeBounds();
-      d_qepr->finishInit();
+  }
+  if (d_qepr != NULL)
+  {
+    for (const Node& a : assertions)
+    {
+      d_qepr->registerAssertion(a);
+    }
+    // must handle sources of other new constants e.g. separation logic
+    // FIXME (as part of project 3) : cleanup
+    sep::TheorySep* theory_sep =
+        static_cast<sep::TheorySep*>(getTheoryEngine()->theoryOf(THEORY_SEP));
+    theory_sep->initializeBounds();
+    d_qepr->finishInit();
+  }
+  if (options::ceGuidedInst())
+  {
+    quantifiers::SynthEngine* sye = d_private->d_synth_e.get();
+    for (const Node& a : assertions)
+    {
+      sye->preregisterAssertion(a);
     }
   }
 }
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 36b58fd60..0a534d090 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -35,7 +35,6 @@
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/relevant_domain.h"
 #include "theory/quantifiers/skolemize.h"
-#include "theory/quantifiers/sygus/synth_engine.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_enumeration.h"
@@ -112,10 +111,6 @@ public:
   /** get relevant domain */
   quantifiers::RelevantDomain* getRelevantDomain() const;
   //---------------------- end utilities
-  //---------------------- modules (TODO remove these #1163)
-  /** ceg instantiation */
-  quantifiers::SynthEngine* getSynthEngine() const;
-  //---------------------- end modules
  private:
   /**
    * Maps quantified formulas to the module that owns them, if any module has