Optimization for sygus streaming mode (#1636)

2 files changed, 72 insertions, 43 deletions

diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
index 3e71eedad..1dd4dcbeb 100644
--- a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
@@ -290,16 +290,14 @@ void CegConjecture::doCheck(std::vector<Node>& lems)
     }
   }
   
-  std::vector< Node > ic;
-  ic.push_back( d_quant.negate() );
-
   //immediately skolemize inner existentials
   Node instr = Rewriter::rewrite(inst);
+  Node lem;
   if (instr.getKind() == NOT && instr[0].getKind() == FORALL)
   {
     if (constructed_cand)
     {
-      ic.push_back(d_qe->getSkolemize()->getSkolemizedBody(instr[0]).negate());
+      lem = d_qe->getSkolemize()->getSkolemizedBody(instr[0]).negate();
     }
     if (sk_refine)
     {
@@ -312,7 +310,7 @@ void CegConjecture::doCheck(std::vector<Node>& lems)
     if (constructed_cand)
     {
       // use the instance itself
-      ic.push_back(instr);
+      lem = instr;
     }
     if (sk_refine)
     {
@@ -321,8 +319,8 @@ void CegConjecture::doCheck(std::vector<Node>& lems)
       d_ce_sk.push_back(Node::null());
     }
   }
-  if( constructed_cand ){
-    Node lem = nm->mkNode(OR, ic);
+  if (!lem.isNull())
+  {
     lem = Rewriter::rewrite( lem );
     //eagerly unfold applications of evaluation function
     if( options::sygusDirectEval() ){
@@ -330,9 +328,25 @@ void CegConjecture::doCheck(std::vector<Node>& lems)
       std::map< Node, Node > visited_n;
       lem = d_qe->getTermDatabaseSygus()->getEagerUnfold( lem, visited_n );
     }
-    lem = getStreamGuardedLemma(lem);
-    lems.push_back( lem );
+    // record the instantiation
+    // this is used for remembering the solution
     recordInstantiation(candidate_values);
+    if (lem.isConst() && !lem.getConst<bool>() && options::sygusStream())
+    {
+      // short circuit the check
+      // instead, we immediately print the current solution.
+      // this saves us from introducing a check lemma and a new guard.
+      printAndContinueStream();
+    }
+    else
+    {
+      // 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(), lem);
+      lem = getStreamGuardedLemma(lem);
+      lems.push_back(lem);
+    }
   }
 }
         
@@ -479,43 +493,13 @@ Node CegConjecture::getNextDecisionRequest( unsigned& priority ) {
             return curr_stream_guard;
           }else{
             if( !value ){
-              Assert(d_master != nullptr);
               Trace("cegqi-debug") << "getNextDecision : we have a new solution since stream guard was propagated false: " << curr_stream_guard << std::endl;
-              // we have generated a solution, print it
-              // get the current output stream
-              // this output stream should coincide with wherever --dump-synth is output on
-              Options& nodeManagerOptions = NodeManager::currentNM()->getOptions();
-              printSynthSolution( *nodeManagerOptions.getOut(), false );
               // need to make the next stream guard
               needs_new_stream_guard = true;
-              
-              // We will not refine the current candidate solution since it is a solution
-              // thus, we clear information regarding the current refinement
-              d_ce_sk.clear();
-              // However, we need to exclude the current solution using an
-              // explicit refinement
-              // so that we proceed to the next solution.
-              std::vector<Node> terms;
-              d_master->getTermList(d_candidates, terms);
-              Trace("cegqi-debug") << "getNextDecision : solution was : " << std::endl;
-              std::vector< Node > exp;
-              for (const Node& cprog : terms)
-              {
-                Node sol = cprog;
-                if( !d_cinfo[cprog].d_inst.empty() ){
-                  sol = d_cinfo[cprog].d_inst.back();
-                  // add to explanation of exclusion
-                  d_qe->getTermDatabaseSygus()
-                      ->getExplain()
-                      ->getExplanationForConstantEquality(cprog, sol, exp);
-                }
-                Trace("cegqi-debug") << "  " << cprog << " -> " << sol << std::endl;
-              }
-              Assert( !exp.empty() );
-              Node exc_lem = exp.size()==1 ? exp[0] : NodeManager::currentNM()->mkNode( kind::AND, exp );
-              exc_lem = exc_lem.negate();
-              Trace("cegqi-lemma") << "Cegqi::Lemma : stream exclude current solution : " << exc_lem << std::endl;
-              d_qe->getOutputChannel().lemma( exc_lem );
+              // the guard has propagated false, indicating that a verify
+              // lemma was unsatisfiable. Hence, the previous candidate is
+              // an actual solution. We print and continue the stream.
+              printAndContinueStream();
             }
           }
         }
@@ -539,6 +523,45 @@ Node CegConjecture::getNextDecisionRequest( unsigned& priority ) {
   return Node::null();
 }
 
+void CegConjecture::printAndContinueStream()
+{
+  Assert(d_master != nullptr);
+  // we have generated a solution, print it
+  // get the current output stream
+  // this output stream should coincide with wherever --dump-synth is output on
+  Options& nodeManagerOptions = NodeManager::currentNM()->getOptions();
+  printSynthSolution(*nodeManagerOptions.getOut(), false);
+
+  // We will not refine the current candidate solution since it is a solution
+  // thus, we clear information regarding the current refinement
+  d_ce_sk.clear();
+  // However, we need to exclude the current solution using an explicit
+  // blocking clause, so that we proceed to the next solution.
+  std::vector<Node> terms;
+  d_master->getTermList(d_candidates, terms);
+  std::vector<Node> exp;
+  for (const Node& cprog : terms)
+  {
+    Node sol = cprog;
+    if (!d_cinfo[cprog].d_inst.empty())
+    {
+      sol = d_cinfo[cprog].d_inst.back();
+      // add to explanation of exclusion
+      d_qe->getTermDatabaseSygus()
+          ->getExplain()
+          ->getExplanationForConstantEquality(cprog, sol, exp);
+    }
+  }
+  Assert(!exp.empty());
+  Node exc_lem = exp.size() == 1
+                     ? exp[0]
+                     : NodeManager::currentNM()->mkNode(kind::AND, exp);
+  exc_lem = exc_lem.negate();
+  Trace("cegqi-lemma") << "Cegqi::Lemma : stream exclude current solution : "
+                       << exc_lem << std::endl;
+  d_qe->getOutputChannel().lemma(exc_lem);
+}
+
 void CegConjecture::printSynthSolution( std::ostream& out, bool singleInvocation ) {
   Trace("cegqi-debug") << "Printing synth solution..." << std::endl;
   Assert( d_quant[0].getNumChildren()==d_embed_quant[0].getNumChildren() );
diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.h b/src/theory/quantifiers/sygus/ce_guided_conjecture.h
index 8ab871d08..215a4d161 100644
--- a/src/theory/quantifiers/sygus/ce_guided_conjecture.h
+++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.h
@@ -226,6 +226,12 @@ private:
    * returned by getCurrentStreamGuard, otherwise this returns n.
    */
   Node getStreamGuardedLemma(Node n) const;
+  /**
+   * Prints the current synthesis solution to the output stream indicated by
+   * the Options object, send a lemma blocking the current solution to the
+   * output channel.
+   */
+  void printAndContinueStream();
   //-------------------------------- end sygus stream
   //-------------------------------- non-syntax guided (deprecated)
   /** Whether we are syntax-guided (e.g. was the input in SyGuS format).