Simplify sygus solver and sygus stream (#5389)

This simplifies the sygus solver based on the fact that verification lemmas are always processed in a separate subsolver.

In particular, this means that the implementation of --sygus-stream can be simplified signficantly.

1 files changed, 39 insertions, 126 deletions

diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index 8dd9a455a..b8700f7f6 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -43,10 +43,8 @@ namespace theory {
 namespace quantifiers {
 
 SynthConjecture::SynthConjecture(QuantifiersEngine* qe,
-                                 SynthEngine* p,
                                  SygusStatistics& s)
     : d_qe(qe),
-      d_parent(p),
       d_stats(s),
       d_tds(qe->getTermDatabaseSygus()),
       d_hasSolution(false),
@@ -255,15 +253,6 @@ void SynthConjecture::assign(Node q)
     d_qe->getOutputChannel().lemma(lem);
   }
 
-  if (options::sygusStream())
-  {
-    d_stream_strategy.reset(new SygusStreamDecisionStrategy(
-        d_qe->getSatContext(), d_qe->getValuation()));
-    d_qe->getDecisionManager()->registerStrategy(
-        DecisionManager::STRAT_QUANT_SYGUS_STREAM_FEASIBLE,
-        d_stream_strategy.get());
-    d_current_stream_guard = d_stream_strategy->getLiteral(0);
-  }
   Trace("cegqi") << "...finished, single invocation = " << isSingleInvocation()
                  << std::endl;
 }
@@ -314,9 +303,7 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems)
     {
       d_hasSolution = true;
       // the conjecture has a solution, so its negation holds
-      Node lem = d_quant.negate();
-      lem = getStreamGuardedLemma(lem);
-      lems.push_back(lem);
+      lems.push_back(d_quant.negate());
     }
     return true;
   }
@@ -327,24 +314,6 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems)
   std::vector<Node> terms;
   d_master->getTermList(d_candidates, terms);
 
-  // process the sygus streaming guard
-  if (options::sygusStream())
-  {
-    Assert(!isSingleInvocation());
-    // it may be the case that we have a new solution now
-    Node currGuard = getCurrentStreamGuard();
-    if (currGuard != d_current_stream_guard)
-    {
-      std::vector<Node> vals;
-      std::vector<int> status;
-      getSynthSolutionsInternal(vals, status);
-      // we have a new guard, print and continue the stream
-      printAndContinueStream(terms, vals);
-      d_current_stream_guard = currGuard;
-      return true;
-    }
-  }
-
   Assert(!d_candidates.empty());
 
   Trace("cegqi-check") << "CegConjuncture : check, build candidates..."
@@ -530,17 +499,14 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems)
     // we have that the current candidate passed a sample test
     // since we trust sampling in this mode, we assert there is no
     // counterexample to the conjecture here.
-    Node lem = nm->mkNode(OR, d_quant.negate(), nm->mkConst(false));
-    lem = getStreamGuardedLemma(lem);
-    lems.push_back(lem);
-    recordInstantiation(candidate_values);
-    d_hasSolution = true;
+    lems.push_back(d_quant.negate());
+    recordSolution(candidate_values);
     return true;
   }
   Assert(!d_set_ce_sk_vars);
 
   // immediately skolemize inner existentials
-  Node lem;
+  Node query;
   // introduce the skolem variables
   std::vector<Node> sks;
   std::vector<Node> vars;
@@ -571,49 +537,36 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems)
         Trace("cegqi-check-debug")
             << "  introduce skolem " << sk << " for " << v << "\n";
       }
-      lem = inst[0][1].substitute(
+      query = inst[0][1].substitute(
           vars.begin(), vars.end(), sks.begin(), sks.end());
-      lem = lem.negate();
+      query = query.negate();
     }
     else
     {
       // use the instance itself
-      lem = inst;
+      query = inst;
     }
   }
   d_ce_sk_vars.insert(d_ce_sk_vars.end(), sks.begin(), sks.end());
   d_set_ce_sk_vars = true;
 
-  if (lem.isNull())
+  if (query.isNull())
   {
     // no lemma to check
     return false;
   }
 
   // simplify the lemma based on the term database sygus utility
-  lem = d_tds->rewriteNode(lem);
+  query = d_tds->rewriteNode(query);
   // eagerly unfold applications of evaluation function
-  Trace("cegqi-debug") << "pre-unfold counterexample : " << lem << std::endl;
-  // record the instantiation
-  // this is used for remembering the solution
-  recordInstantiation(candidate_values);
-
-  Node query = lem;
-  bool success = false;
-  if (query.isConst() && !query.getConst<bool>())
-  {
-    // short circuit the check
-    lem = d_quant.negate();
-    success = true;
-  }
-  else
+  Trace("cegqi-debug") << "pre-unfold counterexample : " << query << std::endl;
+  // Record the solution, which may be falsified below. We require recording
+  // here since the result of the satisfiability test may be unknown.
+  recordSolution(candidate_values);
+
+  if (!query.isConst() || query.getConst<bool>())
   {
-    // This is the "verification lemma", which states
-    // either this conjecture does not have a solution, or candidate_values
-    // is a solution for this conjecture.
-    lem = nm->mkNode(OR, d_quant.negate(), query);
     Trace("sygus-engine") << "  *** Verify with subcall..." << std::endl;
-
     Result r =
         checkWithSubsolver(query.toExpr(), d_ce_sk_vars, d_ce_sk_var_mvs);
     Trace("sygus-engine") << "  ...got " << r << std::endl;
@@ -644,15 +597,7 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems)
       }
       return false;
     }
-    else if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
-    {
-      // if the result in the subcall was unsatisfiable, we avoid
-      // rechecking, hence we drop "query" from the verification lemma
-      lem = d_quant.negate();
-      // we can short circuit adding the lemma (for sygus stream)
-      success = true;
-    }
-    else
+    else if (r.asSatisfiabilityResult().isSat() != Result::UNSAT)
     {
       // In the rare case that the subcall is unknown, we simply exclude the
       // solution, without adding a counterexample point. This should only
@@ -664,22 +609,21 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems)
       d_qe->getOutputChannel().setIncomplete();
       return false;
     }
+    // otherwise we are unsat, and we will process the solution below
   }
-  if (success)
+  // now mark that we have a solution
+  d_hasSolution = true;
+  if (options::sygusStream())
   {
-    d_hasSolution = true;
-    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(terms, candidate_values);
-      // streaming means now we immediately are looking for a new solution
-      d_hasSolution = false;
-      return false;
-    }
+    // immediately print the current solution
+    printAndContinueStream(terms, candidate_values);
+    // streaming means now we immediately are looking for a new solution
+    d_hasSolution = false;
+    return false;
   }
-  lem = getStreamGuardedLemma(lem);
-  lems.push_back(lem);
+  // Use lemma to terminate with "unsat", this is justified by the verification
+  // check above, which confirms the synthesis conjecture is solved.
+  lems.push_back(d_quant.negate());
   return true;
 }
 
@@ -1027,47 +971,6 @@ void SynthConjecture::debugPrint(const char* c)
   Trace(c) << "  * Counterexample skolems : " << d_ce_sk_vars << std::endl;
 }
 
-Node SynthConjecture::getCurrentStreamGuard() const
-{
-  if (d_stream_strategy != nullptr)
-  {
-    // the stream guard is the current asserted literal of the stream strategy
-    Node lit = d_stream_strategy->getAssertedLiteral();
-    if (lit.isNull())
-    {
-      // if none exist, get the first
-      lit = d_stream_strategy->getLiteral(0);
-    }
-    return lit;
-  }
-  return Node::null();
-}
-
-Node SynthConjecture::getStreamGuardedLemma(Node n) const
-{
-  if (options::sygusStream())
-  {
-    // if we are in streaming mode, we guard with the current stream guard
-    Node csg = getCurrentStreamGuard();
-    Assert(!csg.isNull());
-    return NodeManager::currentNM()->mkNode(kind::OR, csg.negate(), n);
-  }
-  return n;
-}
-
-SynthConjecture::SygusStreamDecisionStrategy::SygusStreamDecisionStrategy(
-    context::Context* satContext, Valuation valuation)
-    : DecisionStrategyFmf(satContext, valuation)
-{
-}
-
-Node SynthConjecture::SygusStreamDecisionStrategy::mkLiteral(unsigned i)
-{
-  NodeManager* nm = NodeManager::currentNM();
-  Node curr_stream_guard = nm->mkSkolem("G_Stream", nm->booleanType());
-  return curr_stream_guard;
-}
-
 void SynthConjecture::printAndContinueStream(const std::vector<Node>& enums,
                                              const std::vector<Node>& values)
 {
@@ -1299,6 +1202,16 @@ bool SynthConjecture::getSynthSolutions(
   return true;
 }
 
+void SynthConjecture::recordSolution(std::vector<Node>& vs)
+{
+  Assert(vs.size() == d_candidates.size());
+  d_cinfo.clear();
+  for (unsigned i = 0; i < vs.size(); i++)
+  {
+    d_cinfo[d_candidates[i]].d_inst.push_back(vs[i]);
+  }
+}
+
 bool SynthConjecture::getSynthSolutionsInternal(std::vector<Node>& sols,
                                                 std::vector<int>& statuses)
 {
@@ -1327,7 +1240,7 @@ bool SynthConjecture::getSynthSolutionsInternal(std::vector<Node>& sols,
     }
     else
     {
-      Node cprog = getCandidate(i);
+      Node cprog = d_candidates[i];
       if (!d_cinfo[cprog].d_inst.empty())
       {
         // the solution is just the last instantiated term