Explicitly pass current sygus solution to exclude (#3209)

diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index 97e5a53384a013e3a10216b83b68e0c42bc60ec6..89978e34bc8c6d251b9958aaee562e5baa1ad17b 100644 (file)
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -300,6 +300,10 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems)
   }
   Assert(d_master != nullptr);
 
+  // get the list of terms that the master strategy is interested in
+  std::vector<Node> terms;
+  d_master->getTermList(d_candidates, terms);
+
   // process the sygus streaming guard
   if (options::sygusStream())
   {
@@ -308,17 +312,16 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems)
     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();
+      printAndContinueStream(terms, vals);
       d_current_stream_guard = currGuard;
       return true;
     }
   }
 
-  // get the list of terms that the master strategy is interested in
-  std::vector<Node> terms;
-  d_master->getTermList(d_candidates, terms);
-
   Assert(!d_candidates.empty());
 
   Trace("cegqi-check") << "CegConjuncture : check, build candidates..."
@@ -329,7 +332,9 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems)
   // If a module is not trying to repair constants in solutions and the option
   // sygusRepairConst  is true, we use a default scheme for trying to repair
   // constants here.
-  if (options::sygusRepairConst() && !d_master->usingRepairConst())
+  bool doRepairConst =
+      options::sygusRepairConst() && !d_master->usingRepairConst();
+  if (doRepairConst)
   {
     // have we tried to repair the previous solution?
     // if not, call the repair constant utility
@@ -431,6 +436,17 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems)
 
   NodeManager* nm = NodeManager::currentNM();
 
+  // check the side condition
+  if (constructed_cand)
+  {
+    if (!checkSideCondition(candidate_values))
+    {
+      excludeCurrentSolution(terms, candidate_values);
+      Trace("cegqi-engine") << "...failed side condition" << std::endl;
+      return false;
+    }
+  }
+
   // must get a counterexample to the value of the current candidate
   Node inst;
   if (constructed_cand)
@@ -529,33 +545,6 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems)
   // this is used for remembering the solution
   recordInstantiation(candidate_values);
 
-  // check the side condition
-  Node sc;
-  if (!d_embedSideCondition.isNull() && constructed_cand)
-  {
-    sc = d_embedSideCondition.substitute(d_candidates.begin(),
-                                         d_candidates.end(),
-                                         candidate_values.begin(),
-                                         candidate_values.end());
-    sc = Rewriter::rewrite(sc);
-    Trace("cegqi-engine") << "Check side condition..." << std::endl;
-    Trace("cegqi-debug") << "Check side condition : " << sc << std::endl;
-    SmtEngine scSmt(nm->toExprManager());
-    scSmt.setIsInternalSubsolver();
-    scSmt.setLogic(smt::currentSmtEngine()->getLogicInfo());
-    scSmt.assertFormula(sc.toExpr());
-    Result r = scSmt.checkSat();
-    Trace("cegqi-debug") << "...got side condition : " << r << std::endl;
-    if (r == Result::UNSAT)
-    {
-      // exclude the current solution TODO
-      excludeCurrentSolution();
-      Trace("cegqi-engine") << "...failed side condition" << std::endl;
-      return false;
-    }
-    Trace("cegqi-engine") << "...passed side condition" << std::endl;
-  }
-
   Node query = lem;
   bool success = false;
   if (query.isConst() && !query.getConst<bool>())
@@ -623,7 +612,7 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems)
     {
       // if we were successful, we immediately print the current solution.
       // this saves us from introducing a verification lemma and a new guard.
-      printAndContinueStream();
+      printAndContinueStream(terms, candidate_values);
       return false;
     }
     d_hasSolution = true;
@@ -633,6 +622,31 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems)
   return true;
 }
 
+bool SynthConjecture::checkSideCondition(const std::vector<Node>& cvals) const
+{
+  if (!d_embedSideCondition.isNull())
+  {
+    Node sc = d_embedSideCondition.substitute(
+        d_candidates.begin(), d_candidates.end(), cvals.begin(), cvals.end());
+    sc = Rewriter::rewrite(sc);
+    Trace("cegqi-engine") << "Check side condition..." << std::endl;
+    Trace("cegqi-debug") << "Check side condition : " << sc << std::endl;
+    NodeManager* nm = NodeManager::currentNM();
+    SmtEngine scSmt(nm->toExprManager());
+    scSmt.setIsInternalSubsolver();
+    scSmt.setLogic(smt::currentSmtEngine()->getLogicInfo());
+    scSmt.assertFormula(sc.toExpr());
+    Result r = scSmt.checkSat();
+    Trace("cegqi-debug") << "...got side condition : " << r << std::endl;
+    if (r == Result::UNSAT)
+    {
+      return false;
+    }
+    Trace("cegqi-engine") << "...passed side condition" << std::endl;
+  }
+  return true;
+}
+
 void SynthConjecture::doRefine(std::vector<Node>& lems)
 {
   Assert(lems.empty());
@@ -955,7 +969,8 @@ Node SynthConjecture::SygusStreamDecisionStrategy::mkLiteral(unsigned i)
   return curr_stream_guard;
 }
 
-void SynthConjecture::printAndContinueStream()
+void SynthConjecture::printAndContinueStream(const std::vector<Node>& enums,
+                                             const std::vector<Node>& values)
 {
   Assert(d_master != nullptr);
   // we have generated a solution, print it
@@ -963,10 +978,11 @@ void SynthConjecture::printAndContinueStream()
   // this output stream should coincide with wherever --dump-synth is output on
   Options& nodeManagerOptions = NodeManager::currentNM()->getOptions();
   printSynthSolution(*nodeManagerOptions.getOut());
-  excludeCurrentSolution();
+  excludeCurrentSolution(enums, values);
 }
 
-void SynthConjecture::excludeCurrentSolution()
+void SynthConjecture::excludeCurrentSolution(const std::vector<Node>& enums,
+                                             const std::vector<Node>& values)
 {
   // We will not refine the current candidate solution since it is a solution
   // thus, we clear information regarding the current refinement
@@ -976,21 +992,16 @@ void SynthConjecture::excludeCurrentSolution()
   // However, we need to exclude the current solution using an explicit
   // blocking clause, so that we proceed to the next solution. We do this only
   // for passively-generated enumerators (TermDbSygus::isPassiveEnumerator).
-  std::vector<Node> terms;
-  d_master->getTermList(d_candidates, terms);
   std::vector<Node> exp;
-  for (const Node& cprog : terms)
+  for (unsigned i = 0, tsize = enums.size(); i < tsize; i++)
   {
+    Node cprog = enums[i];
     Assert(d_tds->isEnumerator(cprog));
     if (d_tds->isPassiveEnumerator(cprog))
     {
-      Node sol = cprog;
-      if (!d_cinfo[cprog].d_inst.empty())
-      {
-        sol = d_cinfo[cprog].d_inst.back();
-        // add to explanation of exclusion
-        d_tds->getExplain()->getExplanationForEquality(cprog, sol, exp);
-      }
+      Node cval = values[i];
+      // add to explanation of exclusion
+      d_tds->getExplain()->getExplanationForEquality(cprog, cval, exp);
     }
   }
   if (!exp.empty())

diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h
index 605592d0af65974dee7d36a3944549b297b73bf6..33fff68447799f49541f271947ec1e47756644ad 100644 (file)
--- a/src/theory/quantifiers/sygus/synth_conjecture.h
+++ b/src/theory/quantifiers/sygus/synth_conjecture.h
@@ -154,6 +154,13 @@ class SynthConjecture
       Node x, Node e, TypeNode tn, unsigned tindex, unsigned depth);
   /** print out debug information about this conjecture */
   void debugPrint(const char* c);
+  /** check side condition
+   *
+   * This returns false if the solution { d_candidates -> cvals } does not
+   * satisfy the side condition of the conjecture maintained by this class,
+   * if it exists, and true otherwise.
+   */
+  bool checkSideCondition(const std::vector<Node>& cvals) const;
 
  private:
   /** reference to quantifier engine */
@@ -367,10 +374,15 @@ class SynthConjecture
    * 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, which we refer to as a "stream exclusion lemma".
+   *
+   * The argument enums is the set of enumerators that comprise the current
+   * solution, and values is their current values.
    */
-  void printAndContinueStream();
-  /** exclude the current solution */
-  void excludeCurrentSolution();
+  void printAndContinueStream(const std::vector<Node>& enums,
+                              const std::vector<Node>& values);
+  /** exclude the current solution { enums -> values } */
+  void excludeCurrentSolution(const std::vector<Node>& enums,
+                              const std::vector<Node>& values);
   /**
    * Whether we have guarded a stream exclusion lemma when using sygusStream.
    * This is an optimization that allows us to guard only the first stream