Cegis-specific infrastructure (#1933)

6 files changed, 165 insertions, 113 deletions

diff --git a/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp b/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp
index 0aebbe11a..031507c11 100644
--- a/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp
@@ -138,11 +138,8 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) {
           addedLemma = true;
         }else{
           //this may happen if we eagerly unfold, simplify to true
-          if( !options::sygusDirectEval() ){
-            Trace("cegqi-warn") << "  ...FAILED to add candidate!" << std::endl;
-          }else{
-            Trace("cegqi-engine-debug") << "  ...FAILED to add candidate!" << std::endl;
-          }
+          Trace("cegqi-engine-debug")
+              << "  ...FAILED to add candidate!" << std::endl;
         }
       }
       if( addedLemma ){
diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp
index 47053080a..ec17294f9 100644
--- a/src/theory/quantifiers/sygus/cegis.cpp
+++ b/src/theory/quantifiers/sygus/cegis.cpp
@@ -13,7 +13,9 @@
  **/
 
 #include "theory/quantifiers/sygus/cegis.h"
+#include "options/base_options.h"
 #include "options/quantifiers_options.h"
+#include "printer/printer.h"
 #include "theory/quantifiers/sygus/ce_guided_conjecture.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/theory_engine.h"
@@ -27,6 +29,7 @@ namespace theory {
 namespace quantifiers {
 
 Cegis::Cegis(QuantifiersEngine* qe, CegConjecture* p) : SygusModule(qe, p) {}
+
 bool Cegis::initialize(Node n,
                        const std::vector<Node>& candidates,
                        std::vector<Node>& lemmas)
@@ -49,7 +52,13 @@ bool Cegis::initialize(Node n,
     TypeNode bt = d_base_body.getType();
     d_cegis_sampler.initialize(bt, d_base_vars, options::sygusSamples());
   }
+  return processInitialize(n, candidates, lemmas);
+}
 
+bool Cegis::processInitialize(Node n,
+                              const std::vector<Node>& candidates,
+                              std::vector<Node>& lemmas)
+{
   // initialize an enumerator for each candidate
   for (unsigned i = 0; i < candidates.size(); i++)
   {
@@ -69,9 +78,9 @@ bool Cegis::addEvalLemmas(const std::vector<Node>& candidates,
 {
   NodeManager* nm = NodeManager::currentNM();
   bool addedEvalLemmas = false;
-  if (options::sygusCRefEval())
+  if (options::sygusRefEval())
   {
-    Trace("cegqi-engine") << "  *** Do conjecture refinement evaluation..."
+    Trace("cegqi-engine") << "  *** Do refinement lemma evaluation..."
                           << std::endl;
     // see if any refinement lemma is refuted by evaluation
     std::vector<Node> cre_lems;
@@ -82,8 +91,8 @@ bool Cegis::addEvalLemmas(const std::vector<Node>& candidates,
       {
         if (d_qe->addLemma(lem))
         {
-          Trace("cegqi-lemma") << "Cegqi::Lemma : cref evaluation : " << lem
-                               << std::endl;
+          Trace("cegqi-lemma")
+              << "Cegqi::Lemma : ref evaluation : " << lem << std::endl;
           addedEvalLemmas = true;
         }
       }
@@ -91,61 +100,107 @@ bool Cegis::addEvalLemmas(const std::vector<Node>& candidates,
          add the lemmas below as well, in parallel. */
     }
   }
-  if (!options::sygusDirectEval())
-  {
-    return addedEvalLemmas;
-  }
-  Trace("cegqi-engine") << "  *** Do direct evaluation..." << std::endl;
-  std::vector<Node> eager_terms, eager_vals, eager_exps;
-  for (unsigned i = 0, size = candidates.size(); i < size; ++i)
+  if (options::sygusEvalUnfold())
   {
-    Trace("cegqi-debug") << "  register " << candidates[i] << " -> "
-                         << candidate_values[i] << std::endl;
-    d_tds->registerModelValue(candidates[i],
-                              candidate_values[i],
-                              eager_terms,
-                              eager_vals,
-                              eager_exps);
-  }
-  Trace("cegqi-debug") << "...produced " << eager_terms.size()
-                       << " eager evaluation lemmas.\n";
-  for (unsigned i = 0, size = eager_terms.size(); i < size; ++i)
-  {
-    Node lem = nm->mkNode(
-        OR, eager_exps[i].negate(), eager_terms[i].eqNode(eager_vals[i]));
-    if (d_qe->addLemma(lem))
+    Trace("cegqi-engine") << "  *** Do evaluation unfolding..." << std::endl;
+    std::vector<Node> eager_terms, eager_vals, eager_exps;
+    for (unsigned i = 0, size = candidates.size(); i < size; ++i)
     {
-      Trace("cegqi-lemma") << "Cegqi::Lemma : evaluation : " << lem
-                           << std::endl;
-      addedEvalLemmas = true;
+      Trace("cegqi-debug") << "  register " << candidates[i] << " -> "
+                           << candidate_values[i] << std::endl;
+      d_tds->registerModelValue(candidates[i],
+                                candidate_values[i],
+                                eager_terms,
+                                eager_vals,
+                                eager_exps);
+    }
+    Trace("cegqi-debug") << "...produced " << eager_terms.size()
+                         << " evaluation unfold lemmas.\n";
+    for (unsigned i = 0, size = eager_terms.size(); i < size; ++i)
+    {
+      Node lem = nm->mkNode(
+          OR, eager_exps[i].negate(), eager_terms[i].eqNode(eager_vals[i]));
+      if (d_qe->addLemma(lem))
+      {
+        Trace("cegqi-lemma")
+            << "Cegqi::Lemma : evaluation unfold : " << lem << std::endl;
+        addedEvalLemmas = true;
+      }
     }
   }
   return addedEvalLemmas;
 }
 
-/** construct candidate */
 bool Cegis::constructCandidates(const std::vector<Node>& enums,
                                 const std::vector<Node>& enum_values,
                                 const std::vector<Node>& candidates,
                                 std::vector<Node>& candidate_values,
                                 std::vector<Node>& lems)
 {
-  if (addEvalLemmas(enums, enum_values))
+  if (Trace.isOn("cegis"))
   {
-    // it may be repairable
-    SygusRepairConst* src = d_parent->getRepairConst();
-    std::vector<Node> fail_cvs = enum_values;
-    if (src->repairSolution(candidates, fail_cvs, candidate_values))
+    Trace("cegis") << "  Enumerators :\n";
+    for (unsigned i = 0, size = enums.size(); i < size; ++i)
     {
-      return true;
+      Trace("cegis") << "    " << enums[i] << " -> ";
+      std::stringstream ss;
+      Printer::getPrinter(options::outputLanguage())
+          ->toStreamSygus(ss, enum_values[i]);
+      Trace("cegis") << ss.str() << std::endl;
     }
+  }
+  // evaluate on refinement lemmas
+  bool addedEvalLemmas = addEvalLemmas(enums, enum_values);
+
+  // try to construct candidates
+  if (!processConstructCandidates(enums,
+                                  enum_values,
+                                  candidates,
+                                  candidate_values,
+                                  !addedEvalLemmas,
+                                  lems))
+  {
     return false;
   }
-  candidate_values.insert(
-      candidate_values.end(), enum_values.begin(), enum_values.end());
+
+  if (options::cegisSample() != CEGIS_SAMPLE_NONE && lems.empty())
+  {
+    // if we didn't add a lemma, trying sampling to add a refinement lemma
+    // that immediately refutes the candidate we just constructed
+    if (sampleAddRefinementLemma(enums, enum_values, lems))
+    {
+      // restart (should be guaranteed to add evaluation lemmas on this call)
+      return constructCandidates(
+          enums, enum_values, candidates, candidate_values, lems);
+    }
+  }
   return true;
 }
 
+bool Cegis::processConstructCandidates(const std::vector<Node>& enums,
+                                       const std::vector<Node>& enum_values,
+                                       const std::vector<Node>& candidates,
+                                       std::vector<Node>& candidate_values,
+                                       bool satisfiedRl,
+                                       std::vector<Node>& lems)
+{
+  if (satisfiedRl)
+  {
+    candidate_values.insert(
+        candidate_values.end(), enum_values.begin(), enum_values.end());
+    return true;
+  }
+  SygusRepairConst* src = d_parent->getRepairConst();
+  if (src != nullptr)
+  {
+    // it may be repairable
+    std::vector<Node> fail_cvs = enum_values;
+    Assert(candidates.size() == fail_cvs.size());
+    return src->repairSolution(candidates, fail_cvs, candidate_values);
+  }
+  return false;
+}
+
 void Cegis::addRefinementLemma(Node lem)
 {
   d_refinement_lemmas.push_back(lem);
@@ -371,21 +426,13 @@ void Cegis::getRefinementEvalLemmas(const std::vector<Node>& vs,
       break;
     }
   }
-  // if we didn't add a lemma, trying sampling to add one
-  if (options::cegisSample() != CEGIS_SAMPLE_NONE && lems.empty())
-  {
-    if (sampleAddRefinementLemma(vs, ms, lems))
-    {
-      // restart (should be guaranteed to add evaluation lemmas
-      getRefinementEvalLemmas(vs, ms, lems);
-    }
-  }
 }
 
 bool Cegis::sampleAddRefinementLemma(const std::vector<Node>& candidates,
                                      const std::vector<Node>& vals,
                                      std::vector<Node>& lems)
 {
+  Trace("cegqi-engine") << "  *** Do sample add refinement..." << std::endl;
   if (Trace.isOn("cegis-sample"))
   {
     Trace("cegis-sample") << "Check sampling for candidate solution"
diff --git a/src/theory/quantifiers/sygus/cegis.h b/src/theory/quantifiers/sygus/cegis.h
index cbd563e07..e5ee6bc56 100644
--- a/src/theory/quantifiers/sygus/cegis.h
+++ b/src/theory/quantifiers/sygus/cegis.h
@@ -72,6 +72,23 @@ class Cegis : public SygusModule
    * formula P( CegConjecture::d_candidates, y ).
    */
   Node d_base_body;
+  //----------------------------------cegis-implementation-specific
+  /** do cegis-implementation-specific intialization for this class */
+  virtual bool processInitialize(Node n,
+                                 const std::vector<Node>& candidates,
+                                 std::vector<Node>& lemmas);
+  /** do cegis-implementation-specific construct candidate
+   *
+   * satisfiedRl is whether all refinement lemmas are satisfied under the
+   * substitution { enums -> enum_values }.
+   */
+  virtual bool processConstructCandidates(const std::vector<Node>& enums,
+                                          const std::vector<Node>& enum_values,
+                                          const std::vector<Node>& candidates,
+                                          std::vector<Node>& candidate_values,
+                                          bool satisfiedRl,
+                                          std::vector<Node>& lems);
+  //----------------------------------end cegis-implementation-specific
 
   //-----------------------------------refinement lemmas
   /** refinement lemmas */
diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp
index 20f062722..9ae598f83 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.cpp
+++ b/src/theory/quantifiers/sygus/cegis_unif.cpp
@@ -33,9 +33,9 @@ CegisUnif::CegisUnif(QuantifiersEngine* qe, CegConjecture* p)
 }
 
 CegisUnif::~CegisUnif() {}
-bool CegisUnif::initialize(Node n,
-                           const std::vector<Node>& candidates,
-                           std::vector<Node>& lemmas)
+bool CegisUnif::processInitialize(Node n,
+                                  const std::vector<Node>& candidates,
+                                  std::vector<Node>& lemmas)
 {
   Trace("cegis-unif") << "Initialize CegisUnif : " << n << std::endl;
   // list of strategy points for unification candidates
@@ -99,27 +99,16 @@ void CegisUnif::getTermList(const std::vector<Node>& candidates,
   }
 }
 
-bool CegisUnif::constructCandidates(const std::vector<Node>& enums,
-                                    const std::vector<Node>& enum_values,
-                                    const std::vector<Node>& candidates,
-                                    std::vector<Node>& candidate_values,
-                                    std::vector<Node>& lems)
+bool CegisUnif::processConstructCandidates(const std::vector<Node>& enums,
+                                           const std::vector<Node>& enum_values,
+                                           const std::vector<Node>& candidates,
+                                           std::vector<Node>& candidate_values,
+                                           bool satisfiedRl,
+                                           std::vector<Node>& lems)
 {
-  if (Trace.isOn("cegis-unif-enum"))
-  {
-    Trace("cegis-unif-enum") << "  Evaluation heads :\n";
-    for (unsigned i = 0, size = enums.size(); i < size; ++i)
-    {
-      Trace("cegis-unif-enum") << "    " << enums[i] << " -> ";
-      std::stringstream ss;
-      Printer::getPrinter(options::outputLanguage())
-          ->toStreamSygus(ss, enum_values[i]);
-      Trace("cegis-unif-enum") << ss.str() << std::endl;
-    }
-  }
-  // evaluate on refinement lemmas
-  if (addEvalLemmas(enums, enum_values))
+  if (!satisfiedRl)
   {
+    // if we didn't satisfy the specification, there is no way to repair
     return false;
   }
   // the unification enumerators (return values, conditions) and their model
@@ -137,9 +126,8 @@ bool CegisUnif::constructCandidates(const std::vector<Node>& enums,
     {
       for (unsigned index = 0; index < 2; index++)
       {
-        Trace("cegis-unif-enum")
-            << "  " << (index == 0 ? "Return values" : "Conditions") << " for "
-            << e << ":\n";
+        Trace("cegis") << "  " << (index == 0 ? "Return values" : "Conditions")
+                       << " for " << e << ":\n";
         // get the current unification enumerators
         d_u_enum_manager.getEnumeratorsForStrategyPt(
             e, unif_enums[index][e], index);
@@ -147,13 +135,13 @@ bool CegisUnif::constructCandidates(const std::vector<Node>& enums,
         for (const Node& eu : unif_enums[index][e])
         {
           Node m_eu = d_parent->getModelValue(eu);
-          if (Trace.isOn("cegis-unif-enum"))
+          if (Trace.isOn("cegis"))
           {
-            Trace("cegis-unif-enum") << "    " << eu << " -> ";
+            Trace("cegis") << "    " << eu << " -> ";
             std::stringstream ss;
             Printer::getPrinter(options::outputLanguage())
                 ->toStreamSygus(ss, m_eu);
-            Trace("cegis-unif-enum") << ss.str() << std::endl;
+            Trace("cegis") << ss.str() << std::endl;
           }
           unif_values[index][e].push_back(m_eu);
         }
diff --git a/src/theory/quantifiers/sygus/cegis_unif.h b/src/theory/quantifiers/sygus/cegis_unif.h
index ecaec4129..5c2c11e4d 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.h
+++ b/src/theory/quantifiers/sygus/cegis_unif.h
@@ -183,10 +183,6 @@ class CegisUnif : public Cegis
  public:
   CegisUnif(QuantifiersEngine* qe, CegConjecture* p);
   ~CegisUnif();
-  /** initialize this class */
-  bool initialize(Node n,
-                  const std::vector<Node>& candidates,
-                  std::vector<Node>& lemmas) override;
   /** Retrieves enumerators for constructing solutions
    *
    * Non-unification candidates have themselves as enumerators, while for
@@ -195,33 +191,6 @@ class CegisUnif : public Cegis
    */
   void getTermList(const std::vector<Node>& candidates,
                    std::vector<Node>& enums) override;
-  /** Tries to build new candidate solutions with new enumerated expressions
-   *
-   * This function relies on a data-driven unification-based approach for
-   * constructing solutions for the functions-to-synthesize. See SygusUnifRl for
-   * more details.
-   *
-   * Calls to this function are such that terms is the list of active
-   * enumerators (returned by getTermList), and term_values are their current
-   * model values. This function registers { terms -> terms_values } in
-   * the database of values that have been enumerated, which are in turn used
-   * for constructing candidate solutions when possible.
-   *
-   * This function also excludes models where (terms = terms_values) by adding
-   * blocking clauses to lems. For example, for grammar:
-   *   A -> A+A | x | 1 | 0
-   * and a call where terms = { d } and term_values = { +( x, 1 ) }, it adds:
-   *   ~G V ~is_+( d ) V ~is_x( d.1 ) V ~is_1( d.2 )
-   * to lems, where G is active guard of the enumerator d (see
-   * TermDatabaseSygus::getActiveGuardForEnumerator). This blocking clause
-   * indicates that d should not be given the model value +( x, 1 ) anymore,
-   * since { d -> +( x, 1 ) } has now been added to the database of this class.
-   */
-  bool constructCandidates(const std::vector<Node>& enums,
-                           const std::vector<Node>& enum_values,
-                           const std::vector<Node>& candidates,
-                           std::vector<Node>& candidate_values,
-                           std::vector<Node>& lems) override;
 
   /** Communicates refinement lemma to unification utility and external modules
    *
@@ -249,6 +218,38 @@ class CegisUnif : public Cegis
   Node getNextDecisionRequest(unsigned& priority) override;
 
  private:
+  /** do cegis-implementation-specific intialization for this class */
+  bool processInitialize(Node n,
+                         const std::vector<Node>& candidates,
+                         std::vector<Node>& lemmas) override;
+  /** Tries to build new candidate solutions with new enumerated expressions
+   *
+   * This function relies on a data-driven unification-based approach for
+   * constructing solutions for the functions-to-synthesize. See SygusUnifRl for
+   * more details.
+   *
+   * Calls to this function are such that terms is the list of active
+   * enumerators (returned by getTermList), and term_values are their current
+   * model values. This function registers { terms -> terms_values } in
+   * the database of values that have been enumerated, which are in turn used
+   * for constructing candidate solutions when possible.
+   *
+   * This function also excludes models where (terms = terms_values) by adding
+   * blocking clauses to lems. For example, for grammar:
+   *   A -> A+A | x | 1 | 0
+   * and a call where terms = { d } and term_values = { +( x, 1 ) }, it adds:
+   *   ~G V ~is_+( d ) V ~is_x( d.1 ) V ~is_1( d.2 )
+   * to lems, where G is active guard of the enumerator d (see
+   * TermDatabaseSygus::getActiveGuardForEnumerator). This blocking clause
+   * indicates that d should not be given the model value +( x, 1 ) anymore,
+   * since { d -> +( x, 1 ) } has now been added to the database of this class.
+   */
+  bool processConstructCandidates(const std::vector<Node>& enums,
+                                  const std::vector<Node>& enum_values,
+                                  const std::vector<Node>& candidates,
+                                  std::vector<Node>& candidate_values,
+                                  bool satisfiedRl,
+                                  std::vector<Node>& lems) override;
   /**
    * Sygus unif utility. This class implements the core algorithm (e.g. decision
    * tree learning) that this module relies upon.
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp
index 0b7841170..b530edeaa 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.cpp
+++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp
@@ -1261,7 +1261,8 @@ unsigned TermDbSygus::getAnchorDepth( Node n ) {
 
 
 void TermDbSygus::registerEvalTerm( Node n ) {
-  if( options::sygusDirectEval() ){
+  if (options::sygusEvalUnfold())
+  {
     if( n.getKind()==APPLY_UF && !n.getType().isBoolean() ){
       TypeNode tn = n[0].getType();
       if( tn.isDatatype() ){
@@ -1344,7 +1345,8 @@ void TermDbSygus::registerModelValue( Node a, Node v, std::vector< Node >& terms
           Node expn;
           // unfold?
           bool do_unfold = false;
-          if( options::sygusUnfoldBool() ){
+          if (options::sygusEvalUnfoldBool())
+          {
             if( bTerm.getKind()==ITE || bTerm.getType().isBoolean() ){
               do_unfold = true;
             }