Call separate SMT engine for single invocation sygus (#3151)

2 files changed, 30 insertions, 12 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 27ee446fe..78f47993f 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1321,14 +1321,6 @@ void SmtEngine::setDefaults() {
       options::unconstrainedSimp.set(uncSimp);
     }
   }
-  if (!options::proof())
-  {
-    // minimizing solutions from single invocation requires proofs
-    if (options::cegqiSolMinCore() && options::cegqiSolMinCore.wasSetByUser())
-    {
-      throw OptionException("cegqi-si-sol-min-core requires --proof");
-    }
-  }
 
   // Disable options incompatible with unsat cores and proofs or output an
   // error if enabled explicitly
@@ -1804,8 +1796,12 @@ void SmtEngine::setDefaults() {
     Notice() << "SmtEngine: turning off cbqi to support instMaxLevel" << endl;
     options::cbqi.set(false);
   }
-  //track instantiations?
-  if( options::cbqiNestedQE() || ( options::proof() && !options::trackInstLemmas.wasSetByUser() ) ){
+  // Do we need to track instantiations?
+  // Needed for sygus due to single invocation techniques.
+  if (options::cbqiNestedQE()
+      || (options::proof() && !options::trackInstLemmas.wasSetByUser())
+      || is_sygus)
+  {
     options::trackInstLemmas.set( true );
   }
 
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index eba73c380..4ac21d392 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -587,11 +587,33 @@ class CVC4_PUBLIC SmtEngine
   /** Same as above, but without user-provided grammar restrictions */
   bool getAbduct(const Expr& conj, Expr& abd);
 
-  /** Get list of quantified formulas that were instantiated. */
+  /**
+   * Get list of quantified formulas that were instantiated on the last call
+   * to check-sat.
+   */
   void getInstantiatedQuantifiedFormulas(std::vector<Expr>& qs);
 
-  /** Get instantiations. */
+  /**
+   * Get instantiations for quantified formula q.
+   *
+   * If q was a quantified formula that was instantiated on the last call to
+   * check-sat (i.e. q is returned as part of the vector in the method
+   * getInstantiatedQuantifiedFormulas above), then the list of instantiations
+   * of that formula that were generated are added to insts.
+   *
+   * In particular, if q is of the form forall x. P(x), then insts is a list
+   * of formulas of the form P(t1), ..., P(tn).
+   */
   void getInstantiations(Expr q, std::vector<Expr>& insts);
+  /**
+   * Get instantiation term vectors for quantified formula q.
+   *
+   * This method is similar to above, but in the example above, we return the
+   * (vectors of) terms t1, ..., tn instead.
+   *
+   * Notice that these are not guaranteed to come in the same order as the
+   * instantiation lemmas above.
+   */
   void getInstantiationTermVectors(Expr q,
                                    std::vector<std::vector<Expr> >& tvecs);