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

8 files changed, 210 insertions, 373 deletions

diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index 717ee9dae..00059bba6 100644
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -941,24 +941,6 @@ header = "options/quantifiers_options.h"
   help       = "include constants when reconstruct solutions for single invocation conjectures in original grammar"
 
 [[option]]
-  name       = "cegqiSolMinCore"
-  category   = "regular"
-  long       = "cegqi-si-sol-min-core"
-  type       = "bool"
-  default    = "false"
-  read_only  = true
-  help       = "minimize solutions for single invocation conjectures based on unsat core"
-
-[[option]]
-  name       = "cegqiSolMinInst"
-  category   = "regular"
-  long       = "cegqi-si-sol-min-inst"
-  type       = "bool"
-  default    = "true"
-  read_only  = true
-  help       = "minimize individual instantiations for single invocation conjectures based on unsat core"
-
-[[option]]
   name       = "cegqiSingleInvAbort"
   category   = "regular"
   long       = "cegqi-si-abort"
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);
 
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
index 24a594351..59c463b96 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
@@ -16,7 +16,11 @@
 
 #include "expr/node_algorithm.h"
 #include "options/quantifiers_options.h"
+#include "smt/smt_engine.h"
+#include "smt/smt_engine_scope.h"
+#include "smt/smt_statistics_registry.h"
 #include "theory/arith/arith_msum.h"
+#include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/sygus/sygus_grammar_cons.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_enumeration.h"
@@ -31,89 +35,22 @@ using namespace std;
 
 namespace CVC4 {
 
-bool CegqiOutputSingleInv::doAddInstantiation( std::vector< Node >& subs ) {
-  return d_out->doAddInstantiation( subs );
-}
-
-bool CegqiOutputSingleInv::isEligibleForInstantiation( Node n ) {
-  return d_out->isEligibleForInstantiation( n );
-}
-
-bool CegqiOutputSingleInv::addLemma( Node n ) {
-  return d_out->addLemma( n );
-}
-
 CegSingleInv::CegSingleInv(QuantifiersEngine* qe, SynthConjecture* p)
     : d_qe(qe),
       d_parent(p),
       d_sip(new SingleInvocationPartition),
       d_sol(new CegSingleInvSol(qe)),
-      d_cosi(new CegqiOutputSingleInv(this)),
-      d_cinst(new CegInstantiator(d_qe, d_cosi, false, false)),
-      d_c_inst_match_trie(NULL),
       d_single_invocation(false)
 {
-  // The third and fourth arguments of d_cosi set to (false,false) until we have
-  // solution reconstruction for delta and infinity.
 
-  if (options::incrementalSolving()) {
-    d_c_inst_match_trie = new inst::CDInstMatchTrie(qe->getUserContext());
-  }
 }
 
 CegSingleInv::~CegSingleInv()
 {
-  if (d_c_inst_match_trie) {
-    delete d_c_inst_match_trie;
-  }
-  delete d_cosi;
   delete d_sol;  // (new CegSingleInvSol(qe)),
   delete d_sip;  // d_sip(new SingleInvocationPartition),
 }
 
-void CegSingleInv::getInitialSingleInvLemma(Node g, std::vector<Node>& lems)
-{
-  Assert(!g.isNull());
-  Assert(!d_single_inv.isNull());
-  // make for new var/sk
-  d_single_inv_var.clear();
-  d_single_inv_sk.clear();
-  Node inst;
-  NodeManager* nm = NodeManager::currentNM();
-  if (d_single_inv.getKind() == FORALL)
-  {
-    for (unsigned i = 0, size = d_single_inv[0].getNumChildren(); i < size; i++)
-    {
-      std::stringstream ss;
-      ss << "k_" << d_single_inv[0][i];
-      Node k = nm->mkSkolem(ss.str(),
-                            d_single_inv[0][i].getType(),
-                            "single invocation function skolem");
-      d_single_inv_var.push_back(d_single_inv[0][i]);
-      d_single_inv_sk.push_back(k);
-      d_single_inv_sk_index[k] = i;
-    }
-    inst = d_single_inv[1].substitute(d_single_inv_var.begin(),
-                                      d_single_inv_var.end(),
-                                      d_single_inv_sk.begin(),
-                                      d_single_inv_sk.end());
-  }
-  else
-  {
-    inst = d_single_inv;
-  }
-  inst = TermUtil::simpleNegate(inst);
-  Trace("cegqi-si") << "Single invocation initial lemma : " << inst
-                    << std::endl;
-
-  // register with the instantiator
-  Node ginst = nm->mkNode(OR, g.negate(), inst);
-  lems.push_back(ginst);
-  // make and register the instantiator
-  d_cinst.reset(new CegInstantiator(d_qe, d_cosi, false, false));
-  d_cinst->registerCounterexampleLemma(lems, d_single_inv_sk);
-}
-
 void CegSingleInv::initialize(Node q)
 {
   // can only register one quantified formula with this
@@ -340,44 +277,7 @@ void CegSingleInv::finishInit(bool syntaxRestricted)
   }
 
   // we now have determined whether we will do single invocation techniques
-  if( d_single_invocation ){
-    d_single_inv = d_sip->getSingleInvocation();
-    d_single_inv = TermUtil::simpleNegate( d_single_inv );
-    std::vector<Node> func_vars;
-    d_sip->getFunctionVariables(func_vars);
-    if (!func_vars.empty())
-    {
-      Node pbvl = NodeManager::currentNM()->mkNode(BOUND_VAR_LIST, func_vars);
-      d_single_inv = NodeManager::currentNM()->mkNode( FORALL, pbvl, d_single_inv );
-    }
-    //now, introduce the skolems
-    std::vector<Node> sivars;
-    d_sip->getSingleInvocationVariables(sivars);
-    for (unsigned i = 0, size = sivars.size(); i < size; i++)
-    {
-      Node v = NodeManager::currentNM()->mkSkolem(
-          "a", sivars[i].getType(), "single invocation arg");
-      d_single_inv_arg_sk.push_back( v );
-    }
-    d_single_inv = d_single_inv.substitute(sivars.begin(),
-                                           sivars.end(),
-                                           d_single_inv_arg_sk.begin(),
-                                           d_single_inv_arg_sk.end());
-    Trace("cegqi-si") << "Single invocation formula is : " << d_single_inv << std::endl;
-    // check whether we can handle this quantified formula
-    CegHandledStatus status = CegInstantiator::isCbqiQuant(d_single_inv);
-    if( status<CEG_HANDLED )
-    {
-      Trace("cegqi-si") << "...do not invoke single invocation techniques since the quantified formula does not have a handled counterexample-guided instantiation strategy!" << std::endl;
-      d_single_invocation = false;
-      d_single_inv = Node::null();
-    }
-    else if( options::cbqiPreRegInst() && d_single_inv.getKind()==FORALL ){
-      //just invoke the presolve now
-      d_cinst->presolve( d_single_inv );
-    }
-  }
-  if( !d_single_invocation )
+  if (!d_single_invocation)
   {
     d_single_inv = Node::null();
     Trace("cegqi-si") << "Formula is not single invocation." << std::endl;
@@ -387,120 +287,117 @@ void CegSingleInv::finishInit(bool syntaxRestricted)
       ss << "Property is not handled by single invocation." << std::endl;
       throw LogicException(ss.str());
     }
+    return;
   }
-}
-
-bool CegSingleInv::doAddInstantiation(std::vector<Node>& subs)
-{
-  Assert( d_single_inv_sk.size()==subs.size() );
-  Trace("cegqi-si-inst-debug") << "CegSingleInv::doAddInstantiation, #vars = ";
-  Trace("cegqi-si-inst-debug") << d_single_inv_sk.size() << "..." << std::endl;
-  std::stringstream siss;
-  if( Trace.isOn("cegqi-si-inst-debug") || Trace.isOn("cegqi-engine") ){
-    siss << "  * single invocation: " << std::endl;
-    for( unsigned j=0; j<d_single_inv_sk.size(); j++ ){
-      Node op = d_sip->getFunctionForFirstOrderVariable(d_single_inv[0][j]);
-      Assert(!op.isNull());
-      siss << "    * " << op;
-      siss << " (" << d_single_inv_sk[j] << ")";
-      siss << " -> " << subs[j] << std::endl;
-    }
+  NodeManager* nm = NodeManager::currentNM();
+  d_single_inv = d_sip->getSingleInvocation();
+  d_single_inv = TermUtil::simpleNegate(d_single_inv);
+  std::vector<Node> func_vars;
+  d_sip->getFunctionVariables(func_vars);
+  if (!func_vars.empty())
+  {
+    Node pbvl = nm->mkNode(BOUND_VAR_LIST, func_vars);
+    // mark as quantifier elimination to ensure its structure is preserved
+    Node n_attr =
+        nm->mkSkolem("qe_si",
+                     nm->booleanType(),
+                     "Auxiliary variable for qe attr for single invocation.");
+    QuantElimAttribute qea;
+    n_attr.setAttribute(qea, true);
+    n_attr = nm->mkNode(INST_ATTRIBUTE, n_attr);
+    n_attr = nm->mkNode(INST_PATTERN_LIST, n_attr);
+    // make the single invocation conjecture
+    d_single_inv = nm->mkNode(FORALL, pbvl, d_single_inv, n_attr);
   }
-  Trace("cegqi-si-inst-debug") << siss.str();
-
-  bool alreadyExists;
-  Node lem;
-  if( subs.empty() ){
-    Assert( d_single_inv.getKind()!=FORALL );
-    alreadyExists = false;
-    lem = d_single_inv;
-  }else{
-    Assert( d_single_inv.getKind()==FORALL );
-    if( options::incrementalSolving() ){
-      alreadyExists = !d_c_inst_match_trie->addInstMatch( d_qe, d_single_inv, subs, d_qe->getUserContext() );
-    }else{
-      alreadyExists = !d_inst_match_trie.addInstMatch( d_qe, d_single_inv, subs );
-    }
-    Trace("cegqi-si-inst-debug") << "  * success = " << !alreadyExists << std::endl;
-    //Trace("cegqi-si-inst-debug") << siss.str();
-    //Trace("cegqi-si-inst-debug") << "  * success = " << !alreadyExists << std::endl;
-    if( alreadyExists ){
-      return false;
-    }else{
-      Trace("cegqi-engine") << siss.str() << std::endl;
-      Assert( d_single_inv_var.size()==subs.size() );
-      lem = d_single_inv[1].substitute( d_single_inv_var.begin(), d_single_inv_var.end(), subs.begin(), subs.end() );
-      if( d_qe->getTermUtil()->containsVtsTerm( lem ) ){
-        Trace("cegqi-engine-debug") << "Rewrite based on vts symbols..." << std::endl;
-        lem = d_qe->getTermUtil()->rewriteVtsSymbols( lem );
-      }
-    }
+  // now, introduce the skolems
+  std::vector<Node> sivars;
+  d_sip->getSingleInvocationVariables(sivars);
+  for (unsigned i = 0, size = sivars.size(); i < size; i++)
+  {
+    Node v = NodeManager::currentNM()->mkSkolem(
+        "a", sivars[i].getType(), "single invocation arg");
+    d_single_inv_arg_sk.push_back(v);
   }
-  Trace("cegqi-engine-debug") << "Rewrite..." << std::endl;
-  lem = Rewriter::rewrite( lem );
-  Trace("cegqi-si") << "Single invocation lemma : " << lem << std::endl;
-  if( std::find( d_lemmas_produced.begin(), d_lemmas_produced.end(), lem )==d_lemmas_produced.end() ){
-    d_curr_lemmas.push_back( lem );
-    d_lemmas_produced.push_back( lem );
-    d_inst.push_back( std::vector< Node >() );
-    d_inst.back().insert( d_inst.back().end(), subs.begin(), subs.end() );
+  d_single_inv = d_single_inv.substitute(sivars.begin(),
+                                         sivars.end(),
+                                         d_single_inv_arg_sk.begin(),
+                                         d_single_inv_arg_sk.end());
+  Trace("cegqi-si") << "Single invocation formula is : " << d_single_inv
+                    << std::endl;
+  // check whether we can handle this quantified formula
+  CegHandledStatus status = CegInstantiator::isCbqiQuant(d_single_inv);
+  if (status < CEG_HANDLED)
+  {
+    Trace("cegqi-si") << "...do not invoke single invocation techniques since "
+                         "the quantified formula does not have a handled "
+                         "counterexample-guided instantiation strategy!"
+                      << std::endl;
+    d_single_invocation = false;
+    d_single_inv = Node::null();
   }
-  return true;
 }
-
-bool CegSingleInv::isEligibleForInstantiation(Node n)
+bool CegSingleInv::solve()
 {
-  return n.getKind()!=SKOLEM || std::find( d_single_inv_arg_sk.begin(), d_single_inv_arg_sk.end(), n )!=d_single_inv_arg_sk.end();
-}
-
-bool CegSingleInv::addLemma(Node n)
-{
-  d_curr_lemmas.push_back( n );
-  return true;
-}
-
-bool CegSingleInv::check(std::vector<Node>& lems)
-{
-  if( !d_single_inv.isNull() ) {
-    Trace("cegqi-si-debug") << "CegSingleInv::check..." << std::endl;
-    Trace("cegqi-si-debug")
-        << "CegSingleInv::check consulting ceg instantiation..." << std::endl;
-    d_curr_lemmas.clear();
-    Assert( d_cinst!=NULL );
-    //call check for instantiator
-    d_cinst->check();
-    Trace("cegqi-si-debug") << "...returned " << d_curr_lemmas.size() << " lemmas " <<  std::endl;
-    //add lemmas
-    lems.insert( lems.end(), d_curr_lemmas.begin(), d_curr_lemmas.end() );
-    return !lems.empty();
-  }else{
-    // not single invocation
+  if (d_single_inv.isNull())
+  {
+    // not using single invocation techniques
     return false;
   }
-}
-
-Node CegSingleInv::constructSolution(std::vector<unsigned>& indices,
-                                     unsigned i,
-                                     unsigned index,
-                                     std::map<Node, Node>& weak_imp)
-{
-  Assert( index<d_inst.size() );
-  Assert( i<d_inst[index].size() );
-  unsigned uindex = indices[index];
-  if( index==indices.size()-1 ){
-    return d_inst[uindex][i];
-  }else{
-    Node cond = d_lemmas_produced[uindex];
-    //weaken based on unsat core
-    std::map< Node, Node >::iterator itw = weak_imp.find( cond );
-    if( itw!=weak_imp.end() ){
-      cond = itw->second;
+  Trace("cegqi-si") << "Solve using single invocation..." << std::endl;
+  NodeManager* nm = NodeManager::currentNM();
+  // solve the single invocation conjecture using a fresh copy of SMT engine
+  SmtEngine siSmt(nm->toExprManager());
+  siSmt.setLogic(smt::currentSmtEngine()->getLogicInfo());
+  siSmt.assertFormula(d_single_inv.toExpr());
+  Result r = siSmt.checkSat();
+  Trace("cegqi-si") << "Result: " << r << std::endl;
+  if (r.asSatisfiabilityResult().isSat() != Result::UNSAT)
+  {
+    // conjecture is infeasible or unknown
+    return false;
+  }
+  // now, get the instantiations
+  std::vector<Expr> qs;
+  siSmt.getInstantiatedQuantifiedFormulas(qs);
+  Assert(qs.size() <= 1);
+  // track the instantiations, as solution construction is based on this
+  Trace("cegqi-si") << "#instantiated quantified formulas=" << qs.size()
+                    << std::endl;
+  d_inst.clear();
+  d_instConds.clear();
+  for (const Expr& q : qs)
+  {
+    TNode qn = Node::fromExpr(q);
+    Assert(qn.getKind() == FORALL);
+    std::vector<std::vector<Expr> > tvecs;
+    siSmt.getInstantiationTermVectors(q, tvecs);
+    Trace("cegqi-si") << "#instantiations of " << q << "=" << tvecs.size()
+                      << std::endl;
+    std::vector<Node> vars;
+    for (const Node& v : qn[0])
+    {
+      vars.push_back(v);
+    }
+    Node body = qn[1];
+    for (unsigned i = 0, ninsts = tvecs.size(); i < ninsts; i++)
+    {
+      std::vector<Expr>& tvi = tvecs[i];
+      std::vector<Node> inst;
+      for (const Expr& t : tvi)
+      {
+        inst.push_back(Node::fromExpr(t));
+      }
+      Trace("cegqi-si") << "  Instantiation: " << inst << std::endl;
+      d_inst.push_back(inst);
+      Assert(inst.size() == vars.size());
+      Node ilem =
+          body.substitute(vars.begin(), vars.end(), inst.begin(), inst.end());
+      ilem = Rewriter::rewrite(ilem);
+      d_instConds.push_back(ilem);
+      Trace("cegqi-si") << "  Instantiation Lemma: " << ilem << std::endl;
     }
-    cond = TermUtil::simpleNegate( cond );
-    Node ite1 = d_inst[uindex][i];
-    Node ite2 = constructSolution( indices, i, index+1, weak_imp );
-    return NodeManager::currentNM()->mkNode( ITE, cond, ite1, ite2 );
   }
+  return true;
 }
 
 //TODO: use term size?
@@ -549,7 +446,7 @@ Node CegSingleInv::getSolution(unsigned sol_index,
                                bool rconsSygus)
 {
   Assert( d_sol!=NULL );
-  Assert( !d_lemmas_produced.empty() );
+  Assert(!d_inst.empty());
   const Datatype& dt = ((DatatypeType)(stn).toType()).getDatatype();
   Node varList = Node::fromExpr( dt.getSygusVarList() );
   Node prog = d_quant[0][sol_index];
@@ -573,34 +470,11 @@ Node CegSingleInv::getSolution(unsigned sol_index,
 
     //construct the solution
     Trace("csi-sol") << "Sort solution return values " << sol_index << std::endl;
-    bool useUnsatCore = false;
-    std::vector< Node > active_lemmas;
-    //minimize based on unsat core, if possible
-    std::map< Node, Node > weak_imp;
-    if( options::cegqiSolMinCore() ){
-      if( options::cegqiSolMinInst() ){
-        if( d_qe->getUnsatCoreLemmas( active_lemmas, weak_imp ) ){
-          useUnsatCore = true;
-        }
-      }else{
-        if( d_qe->getUnsatCoreLemmas( active_lemmas ) ){
-          useUnsatCore = true;
-        }
-      }
-    } 
-    Assert( d_lemmas_produced.size()==d_inst.size() );
     std::vector< unsigned > indices;
-    for( unsigned i=0; i<d_lemmas_produced.size(); i++ ){
-      bool incl = true;
-      if( useUnsatCore ){
-        incl = std::find( active_lemmas.begin(), active_lemmas.end(), d_lemmas_produced[i] )!=active_lemmas.end();
-      }
-      if( incl ){
-        Assert( sol_index<d_inst[i].size() );
-        indices.push_back( i );
-      }
+    for (unsigned i = 0, ninst = d_inst.size(); i < ninst; i++)
+    {
+      indices.push_back(i);
     }
-    Trace("csi-sol") << "...included " << indices.size() << " / " << d_lemmas_produced.size() << " instantiations." << std::endl;
     Assert( !indices.empty() );
     //sort indices based on heuristic : currently, do all constant returns first (leads to simpler conditions)
     // TODO : to minimize solution size, put the largest term last
@@ -609,7 +483,17 @@ Node CegSingleInv::getSolution(unsigned sol_index,
     ssii.d_i = sol_index;
     std::sort( indices.begin(), indices.end(), ssii );
     Trace("csi-sol") << "Construct solution" << std::endl;
-    s = constructSolution( indices, sol_index, 0, weak_imp );
+    std::reverse(indices.begin(), indices.end());
+    s = d_inst[indices[0]][sol_index];
+    // it is an ITE chain whose conditions are the instantiations
+    NodeManager* nm = NodeManager::currentNM();
+    for (unsigned j = 1, nindices = indices.size(); j < nindices; j++)
+    {
+      unsigned uindex = indices[j];
+      Node cond = d_instConds[uindex];
+      cond = TermUtil::simpleNegate(cond);
+      s = nm->mkNode(ITE, cond, d_inst[uindex][sol_index], s);
+    }
     Assert( vars.size()==d_sol->d_varList.size() );
     s = s.substitute( vars.begin(), vars.end(), d_sol->d_varList.begin(), d_sol->d_varList.end() );
   }
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.h b/src/theory/quantifiers/sygus/ce_guided_single_inv.h
index b6f282c65..fb216ce0b 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.h
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.h
@@ -28,17 +28,6 @@ namespace theory {
 namespace quantifiers {
 
 class SynthConjecture;
-class CegSingleInv;
-
-class CegqiOutputSingleInv : public CegqiOutput {
- public:
- CegqiOutputSingleInv(CegSingleInv* out) : d_out(out) {}
- virtual ~CegqiOutputSingleInv() {}
- CegSingleInv* d_out;
- bool doAddInstantiation(std::vector<Node>& subs) override;
- bool isEligibleForInstantiation(Node n) override;
- bool addLemma(Node lem) override;
-};
 
 class DetTrace {
 private:
@@ -174,9 +163,6 @@ class CegSingleInv
                                std::vector< Node >& terms,
                                std::map< Node, std::vector< Node > >& teq,
                                Node n, std::vector< Node >& conj );
-  // constructing solution
-  Node constructSolution(std::vector<unsigned>& indices, unsigned i,
-                         unsigned index, std::map<Node, Node>& weak_imp);
   Node postProcessSolution(Node n);
  private:
   /** pointer to the quantifiers engine */
@@ -189,10 +175,6 @@ class CegSingleInv
   std::map< Node, TransitionInference > d_ti;
   // solution reconstruction
   CegSingleInvSol* d_sol;
-  // the instantiator's output channel
-  CegqiOutputSingleInv* d_cosi;
-  // the instantiator
-  std::unique_ptr<CegInstantiator> d_cinst;
 
   // list of skolems for each argument of programs
   std::vector<Node> d_single_inv_arg_sk;
@@ -202,9 +184,6 @@ class CegSingleInv
   std::map<Node, int> d_single_inv_sk_index;
   // program to solution index
   std::map<Node, unsigned> d_prog_to_sol_index;
-  // lemmas produced
-  inst::InstMatchTrie d_inst_match_trie;
-  inst::CDInstMatchTrie* d_c_inst_match_trie;
   // original conjecture
   Node d_orig_conjecture;
   // solution
@@ -212,18 +191,18 @@ class CegSingleInv
   Node d_solution;
   Node d_sygus_solution;
  public:
-  // lemmas produced
-  std::vector<Node> d_lemmas_produced;
+  /**
+   * The list of instantiations that suffice to show the first-order equivalent
+   * of the negated synthesis conjecture is unsatisfiable.
+   */
   std::vector<std::vector<Node> > d_inst;
+  /**
+   * The list of instantiation lemmas, corresponding to instantiations of the
+   * first order conjecture for the term vectors above.
+   */
+  std::vector<Node> d_instConds;
 
  private:
-  std::vector<Node> d_curr_lemmas;
-  // add instantiation
-  bool doAddInstantiation( std::vector< Node >& subs );
-  //is eligible for instantiation
-  bool isEligibleForInstantiation( Node n );
-  // add lemma
-  bool addLemma( Node lem );
   // conjecture
   Node d_quant;
   Node d_simp_quant;
@@ -246,27 +225,25 @@ class CegSingleInv
   // get simplified conjecture
   Node getSimplifiedConjecture() { return d_simp_quant; }
  public:
-  /** get the single invocation lemma(s)
-   *
-   * This adds lemmas to lem that initializes this class for doing
-   * counterexample-guided instantiation for the synthesis conjecture. These
-   * lemmas correspond to the negation of the body of the (anti-skolemized)
-   * form of the conjecture for fresh skolems.
-   *
-   * Argument g is guard, for which all the above lemmas are guarded.
-   */
-  void getInitialSingleInvLemma(Node g, std::vector<Node>& lems);
   // initialize this class for synthesis conjecture q
   void initialize( Node q );
   /** finish initialize
    *
    * This method sets up final decisions about whether to use single invocation
-   * techniques. The argument syntaxRestricted is whether the syntax for
-   * solutions for the initialized conjecture is restricted.
+   * techniques.
+   *
+   * The argument syntaxRestricted is whether the syntax for solutions for the
+   * initialized conjecture is restricted.
    */
   void finishInit(bool syntaxRestricted);
-  //check
-  bool check( std::vector< Node >& lems );
+  /** solve
+   *
+   * If single invocation techniques are being used, it solves
+   * the first order form of the negated synthesis conjecture using a fresh
+   * copy of the SMT engine. This method returns true if it has successfully
+   * found a solution to the synthesis conjecture using this method.
+   */
+  bool solve();
   //get solution
   Node getSolution( unsigned sol_index, TypeNode stn, int& reconstructed, bool rconsSygus = true );
   //reconstruct to syntax
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index b302c4657..6fdbfd0bc 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -46,6 +46,7 @@ namespace quantifiers {
 SynthConjecture::SynthConjecture(QuantifiersEngine* qe)
     : d_qe(qe),
       d_tds(qe->getTermDatabaseSygus()),
+      d_hasSolution(false, qe->getUserContext()),
       d_ceg_si(new CegSingleInv(qe, this)),
       d_ceg_proc(new SynthConjectureProcess(qe)),
       d_ceg_gc(new CegGrammarConstructor(qe, this)),
@@ -72,6 +73,12 @@ SynthConjecture::SynthConjecture(QuantifiersEngine* qe)
 
 SynthConjecture::~SynthConjecture() {}
 
+void SynthConjecture::presolve()
+{
+  // we don't have a solution yet
+  d_hasSolution = false;
+}
+
 void SynthConjecture::assign(Node q)
 {
   Assert(d_embed_quant.isNull());
@@ -216,22 +223,6 @@ void SynthConjecture::assign(Node q)
   // has been used on this call to check.
   d_qe->getOutputChannel().requirePhase(d_feasible_guard, true);
 
-  if (isSingleInvocation())
-  {
-    std::vector<Node> lems;
-    d_ceg_si->getInitialSingleInvLemma(d_feasible_guard, lems);
-    for (unsigned i = 0; i < lems.size(); i++)
-    {
-      Trace("cegqi-lemma") << "Cegqi::Lemma : single invocation " << i << " : "
-                           << lems[i] << std::endl;
-      d_qe->getOutputChannel().lemma(lems[i]);
-      if (Trace.isOn("cegqi-debug"))
-      {
-        Node rlem = Rewriter::rewrite(lems[i]);
-        Trace("cegqi-debug") << "...rewritten : " << rlem << std::endl;
-      }
-    }
-  }
   Node gneg = d_feasible_guard.negate();
   for (unsigned i = 0; i < guarded_lemmas.size(); i++)
   {
@@ -288,17 +279,24 @@ bool SynthConjecture::needsCheck()
   return true;
 }
 
-void SynthConjecture::doSingleInvCheck(std::vector<Node>& lems)
-{
-  if (d_ceg_si != NULL)
-  {
-    d_ceg_si->check(lems);
-  }
-}
-
 bool SynthConjecture::needsRefinement() const { return d_set_ce_sk_vars; }
 bool SynthConjecture::doCheck(std::vector<Node>& lems)
 {
+  if (isSingleInvocation())
+  {
+    // We now try to solve with the single invocation solver, which may or may
+    // not succeed in solving the conjecture. In either case,  we are done and
+    // return true.
+    if (d_ceg_si->solve())
+    {
+      d_hasSolution = true;
+      // the conjecture has a solution, so its negation holds
+      Node lem = d_quant.negate();
+      lem = getStreamGuardedLemma(lem);
+      lems.push_back(lem);
+    }
+    return true;
+  }
   Assert(d_master != nullptr);
 
   // process the sygus streaming guard
@@ -618,12 +616,16 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems)
       // free logic is undecidable.
     }
   }
-  if (success && options::sygusStream())
+  if (success)
   {
-    // if we were successful, we immediately print the current solution.
-    // this saves us from introducing a verification lemma and a new guard.
-    printAndContinueStream();
-    return false;
+    if (options::sygusStream())
+    {
+      // if we were successful, we immediately print the current solution.
+      // this saves us from introducing a verification lemma and a new guard.
+      printAndContinueStream();
+      return false;
+    }
+    d_hasSolution = true;
   }
   lem = getStreamGuardedLemma(lem);
   lems.push_back(lem);
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h
index 1cc3702b6..605592d0a 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.h
+++ b/src/theory/quantifiers/sygus/synth_conjecture.h
@@ -70,6 +70,8 @@ class SynthConjecture
  public:
   SynthConjecture(QuantifiersEngine* qe);
   ~SynthConjecture();
+  /** presolve */
+  void presolve();
   /** get original version of conjecture */
   Node getConjecture() { return d_quant; }
   /** get deep embedding version of conjecture */
@@ -82,11 +84,6 @@ class SynthConjecture
   bool needsCheck();
   /** whether the conjecture is waiting for a call to doRefine below */
   bool needsRefinement() const;
-  /** do single invocation check
-   * This updates Gamma for an iteration of step 2 of Figure 1 of Reynolds et al
-   * CAV 2015.
-   */
-  void doSingleInvCheck(std::vector<Node>& lems);
   /** do syntax-guided enumerative check
    *
    * This is step 2(a) of Figure 3 of Reynolds et al CAV 2015.
@@ -165,6 +162,11 @@ class SynthConjecture
   TermDbSygus* d_tds;
   /** The feasible guard. */
   Node d_feasible_guard;
+  /**
+   * Do we have a solution in this user context? This is user-context dependent
+   * to enable use cases of sygus in incremental mode.
+   */
+  context::CDO<bool> d_hasSolution;
   /** the decision strategy for the feasible guard */
   std::unique_ptr<DecisionStrategy> d_feasible_strategy;
   /** single invocation utility */
diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp
index afa40bdd8..f78886249 100644
--- a/src/theory/quantifiers/sygus/synth_engine.cpp
+++ b/src/theory/quantifiers/sygus/synth_engine.cpp
@@ -295,34 +295,6 @@ bool SynthEngine::checkConjecture(SynthConjecture* conj)
   if (!conj->needsRefinement())
   {
     Trace("cegqi-engine-debug") << "Do conjecture check..." << std::endl;
-    if (conj->isSingleInvocation())
-    {
-      std::vector<Node> clems;
-      conj->doSingleInvCheck(clems);
-      if (!clems.empty())
-      {
-        for (const Node& lem : clems)
-        {
-          Trace("cegqi-lemma")
-              << "Cegqi::Lemma : single invocation instantiation : " << lem
-              << std::endl;
-          d_quantEngine->addLemma(lem);
-        }
-        d_statistics.d_cegqi_si_lemmas += clems.size();
-        Trace("cegqi-engine") << "  ...try single invocation." << std::endl;
-      }
-      else
-      {
-        // This can happen for non-monotonic instantiation strategies. We
-        // set --cbqi-full to ensure that for most strategies (e.g. BV), we
-        // are using a monotonic strategy.
-        Trace("cegqi-warn")
-            << "  ...FAILED to add cbqi instantiation for single invocation!"
-            << std::endl;
-      }
-      return true;
-    }
-
     Trace("cegqi-engine-debug")
         << "  *** Check candidate phase..." << std::endl;
     std::vector<Node> cclems;