Simplify skolemization in sygus solver (#7331)

The core sygus solver predates the use of subsolvers. When doing verification checks in the CEGIS loop, we previously added unique lemmas to the main solver with fresh skolem variables. We now call subsolvers only, meaning that the set of skolem variables used in verification calls can be fixed.

2 files changed, 67 insertions, 135 deletions

diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index 4fa8ba78e..fdbb0750b 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -57,7 +57,7 @@ SynthConjecture::SynthConjecture(Env& env,
       d_treg(tr),
       d_stats(s),
       d_tds(tr.getTermDatabaseSygus()),
-      d_verify(options(), qs.getLogicInfo(), d_tds),
+      d_verify(options(), logicInfo(), d_tds),
       d_hasSolution(false),
       d_ceg_si(new CegSingleInv(env, tr, s)),
       d_templInfer(new SygusTemplateInfer),
@@ -70,7 +70,7 @@ SynthConjecture::SynthConjecture(Env& env,
       d_ceg_cegisUnif(new CegisUnif(env, qs, qim, d_tds, this)),
       d_sygus_ccore(new CegisCoreConnective(env, qs, qim, d_tds, this)),
       d_master(nullptr),
-      d_set_ce_sk_vars(false),
+      d_setInnerSksModel(false),
       d_repair_index(0),
       d_guarded_stream_exc(false)
 {
@@ -108,7 +108,7 @@ void SynthConjecture::assign(Node q)
 
   // initialize the guard
   d_feasible_guard = sm->mkDummySkolem("G", nm->booleanType());
-  d_feasible_guard = Rewriter::rewrite(d_feasible_guard);
+  d_feasible_guard = rewrite(d_feasible_guard);
   d_feasible_guard = d_qstate.getValuation().ensureLiteral(d_feasible_guard);
   AlwaysAssert(!d_feasible_guard.isNull());
 
@@ -179,8 +179,22 @@ void SynthConjecture::assign(Node q)
   Trace("cegqi") << "Base quantified formula is : " << d_embed_quant
                  << std::endl;
   // construct base instantiation
-  d_base_inst = Rewriter::rewrite(d_qim.getInstantiate()->getInstantiation(
-      d_embed_quant, vars, d_candidates));
+  Subs bsubs;
+  bsubs.add(vars, d_candidates);
+  d_base_inst = rewrite(bsubs.apply(d_embed_quant[1]));
+  d_checkBody = d_embed_quant[1];
+  if (d_checkBody.getKind() == NOT && d_checkBody[0].getKind() == FORALL)
+  {
+    for (const Node& v : d_checkBody[0][0])
+    {
+      Node sk = sm->mkDummySkolem("rsk", v.getType());
+      bsubs.add(v, sk);
+      d_innerVars.push_back(v);
+      d_innerSks.push_back(sk);
+    }
+    d_checkBody = d_checkBody[0][1].negate();
+  }
+  d_checkBody = rewrite(bsubs.apply(d_checkBody));
   if (!d_embedSideCondition.isNull() && !vars.empty())
   {
     d_embedSideCondition = d_embedSideCondition.substitute(
@@ -239,14 +253,6 @@ void SynthConjecture::assign(Node q)
   }
 
   Assert(d_qreg.getQuantAttributes().isSygus(q));
-  // if the base instantiation is an existential, store its variables
-  if (d_base_inst.getKind() == NOT && d_base_inst[0].getKind() == FORALL)
-  {
-    for (const Node& v : d_base_inst[0][0])
-    {
-      d_inner_vars.push_back(v);
-    }
-  }
 
   // register the strategy
   d_feasible_strategy.reset(new DecisionStrategySingleton(
@@ -298,7 +304,7 @@ bool SynthConjecture::needsCheck()
   return true;
 }
 
-bool SynthConjecture::needsRefinement() const { return d_set_ce_sk_vars; }
+bool SynthConjecture::needsRefinement() const { return d_setInnerSksModel; }
 bool SynthConjecture::doCheck()
 {
   if (isSingleInvocation())
@@ -426,7 +432,7 @@ bool SynthConjecture::doCheck()
             if (Trace.isOn("sygus-engine-rr"))
             {
               Node bv = d_tds->sygusToBuiltin(nv, tn);
-              bv = Rewriter::rewrite(bv);
+              bv = rewrite(bv);
               Trace("sygus-engine-rr") << " -> " << bv << std::endl;
             }
           }
@@ -456,9 +462,6 @@ bool SynthConjecture::doCheck()
     }
   }
 
-  NodeManager* nm = NodeManager::currentNM();
-  SkolemManager* sm = nm->getSkolemManager();
-
   // check the side condition if we constructed a candidate
   if (constructed_cand)
   {
@@ -471,7 +474,7 @@ bool SynthConjecture::doCheck()
   }
 
   // must get a counterexample to the value of the current candidate
-  Node inst;
+  Node query;
   if (constructed_cand)
   {
     if (Trace.isOn("cegqi-check"))
@@ -485,14 +488,14 @@ bool SynthConjecture::doCheck()
       }
     }
     Assert(candidate_values.size() == d_candidates.size());
-    inst = d_base_inst.substitute(d_candidates.begin(),
-                                  d_candidates.end(),
-                                  candidate_values.begin(),
-                                  candidate_values.end());
+    query = d_checkBody.substitute(d_candidates.begin(),
+                                   d_candidates.end(),
+                                   candidate_values.begin(),
+                                   candidate_values.end());
   }
   else
   {
-    inst = d_base_inst;
+    query = d_checkBody;
   }
 
   if (!constructed_cand)
@@ -512,52 +515,26 @@ bool SynthConjecture::doCheck()
     recordSolution(candidate_values);
     return true;
   }
-  Assert(!d_set_ce_sk_vars);
+  Assert(!d_setInnerSksModel);
 
-  // immediately skolemize inner existentials
-  Node query;
-  // introduce the skolem variables
-  std::vector<Node> sks;
-  std::vector<Node> vars;
-  if (constructed_cand)
+  // print the candidate solution for debugging
+  if (constructed_cand && printDebug)
   {
-    if (printDebug)
-    {
-      const Options& sopts = options();
-      std::ostream& out = *sopts.base.out;
-      out << "(sygus-candidate ";
-      Assert(d_quant[0].getNumChildren() == candidate_values.size());
-      for (unsigned i = 0, ncands = candidate_values.size(); i < ncands; i++)
-      {
-        Node v = candidate_values[i];
-        std::stringstream ss;
-        TermDbSygus::toStreamSygus(ss, v);
-        out << "(" << d_quant[0][i] << " " << ss.str() << ")";
-      }
-      out << ")" << std::endl;
-    }
-    if (inst.getKind() == NOT && inst[0].getKind() == FORALL)
+    const Options& sopts = options();
+    std::ostream& out = *sopts.base.out;
+    out << "(sygus-candidate ";
+    Assert(d_quant[0].getNumChildren() == candidate_values.size());
+    for (size_t i = 0, ncands = candidate_values.size(); i < ncands; i++)
     {
-      for (const Node& v : inst[0][0])
-      {
-        Node sk = sm->mkDummySkolem("rsk", v.getType());
-        sks.push_back(sk);
-        vars.push_back(v);
-        Trace("cegqi-check-debug")
-            << "  introduce skolem " << sk << " for " << v << "\n";
-      }
-      query = inst[0][1].substitute(
-          vars.begin(), vars.end(), sks.begin(), sks.end());
-      query = query.negate();
-    }
-    else
-    {
-      // use the instance itself
-      query = inst;
+      Node v = candidate_values[i];
+      std::stringstream ss;
+      TermDbSygus::toStreamSygus(ss, v);
+      out << "(" << d_quant[0][i] << " " << ss.str() << ")";
     }
+    out << ")" << std::endl;
   }
-  d_ce_sk_vars.insert(d_ce_sk_vars.end(), sks.begin(), sks.end());
-  d_set_ce_sk_vars = true;
+
+  d_setInnerSksModel = true;
 
   if (query.isNull())
   {
@@ -569,7 +546,7 @@ bool SynthConjecture::doCheck()
   // here since the result of the satisfiability test may be unknown.
   recordSolution(candidate_values);
 
-  Result r = d_verify.verify(query, d_ce_sk_vars, d_ce_sk_var_mvs);
+  Result r = d_verify.verify(query, d_innerSks, d_innerSksModel);
 
   if (r.asSatisfiabilityResult().isSat() == Result::SAT)
   {
@@ -632,71 +609,29 @@ bool SynthConjecture::checkSideCondition(const std::vector<Node>& cvals) const
 
 bool SynthConjecture::doRefine()
 {
-  Assert(d_set_ce_sk_vars);
-
-  // first, make skolem substitution
-  Trace("cegqi-refine") << "doRefine : construct skolem substitution..."
-                        << std::endl;
-  std::vector<Node> sk_vars;
-  std::vector<Node> sk_subs;
-  // collect the substitution over all disjuncts
-  if (!d_ce_sk_vars.empty())
-  {
-    Trace("cegqi-refine") << "Get model values for skolems..." << std::endl;
-    Assert(d_inner_vars.size() == d_ce_sk_vars.size());
-    if (d_ce_sk_var_mvs.empty())
-    {
-      std::vector<Node> model_values;
-      for (const Node& v : d_ce_sk_vars)
-      {
-        Node mv = getModelValue(v);
-        Trace("cegqi-refine") << "  " << v << " -> " << mv << std::endl;
-        model_values.push_back(mv);
-      }
-      sk_subs.insert(sk_subs.end(), model_values.begin(), model_values.end());
-    }
-    else
-    {
-      Assert(d_ce_sk_var_mvs.size() == d_ce_sk_vars.size());
-      sk_subs.insert(
-          sk_subs.end(), d_ce_sk_var_mvs.begin(), d_ce_sk_var_mvs.end());
-    }
-    sk_vars.insert(sk_vars.end(), d_inner_vars.begin(), d_inner_vars.end());
-  }
-  else
-  {
-    Assert(d_inner_vars.empty());
-  }
-
+  Assert(d_setInnerSksModel);
   Trace("cegqi-refine") << "doRefine : Construct refinement lemma..."
                         << std::endl;
   Trace("cegqi-refine-debug")
-      << "  For counterexample skolems : " << d_ce_sk_vars << std::endl;
-  Node base_lem;
-  if (d_base_inst.getKind() == NOT && d_base_inst[0].getKind() == FORALL)
-  {
-    base_lem = d_base_inst[0][1];
-  }
-  else
-  {
-    base_lem = d_base_inst.negate();
-  }
+      << "  For counterexample skolems : " << d_innerSks << std::endl;
+  Node base_lem = d_checkBody.negate();
 
-  Assert(sk_vars.size() == sk_subs.size());
+  Assert(d_innerSks.size() == d_innerSksModel.size());
 
   Trace("cegqi-refine") << "doRefine : substitute..." << std::endl;
-  base_lem = base_lem.substitute(
-      sk_vars.begin(), sk_vars.end(), sk_subs.begin(), sk_subs.end());
+  base_lem = base_lem.substitute(d_innerSks.begin(),
+                                 d_innerSks.end(),
+                                 d_innerSksModel.begin(),
+                                 d_innerSksModel.end());
   Trace("cegqi-refine") << "doRefine : rewrite..." << std::endl;
   base_lem = d_tds->rewriteNode(base_lem);
   Trace("cegqi-refine") << "doRefine : register refinement lemma " << base_lem
                         << "..." << std::endl;
   size_t prevPending = d_qim.numPendingLemmas();
-  d_master->registerRefinementLemma(sk_vars, base_lem);
+  d_master->registerRefinementLemma(d_innerSks, base_lem);
   Trace("cegqi-refine") << "doRefine : finished" << std::endl;
-  d_set_ce_sk_vars = false;
-  d_ce_sk_vars.clear();
-  d_ce_sk_var_mvs.clear();
+  d_setInnerSksModel = false;
+  d_innerSksModel.clear();
 
   // check if we added a lemma
   bool addedLemma = d_qim.numPendingLemmas() > prevPending;
@@ -800,7 +735,7 @@ void SynthConjecture::debugPrint(const char* c)
 {
   Trace(c) << "Synthesis conjecture : " << d_embed_quant << std::endl;
   Trace(c) << "  * Candidate programs : " << d_candidates << std::endl;
-  Trace(c) << "  * Counterexample skolems : " << d_ce_sk_vars << std::endl;
+  Trace(c) << "  * Counterexample skolems : " << d_innerSks << std::endl;
 }
 
 void SynthConjecture::printAndContinueStream(const std::vector<Node>& enums,
@@ -820,9 +755,8 @@ void SynthConjecture::excludeCurrentSolution(const std::vector<Node>& enums,
                        << values << std::endl;
   // We will not refine the current candidate solution since it is a solution
   // thus, we clear information regarding the current refinement
-  d_set_ce_sk_vars = false;
-  d_ce_sk_vars.clear();
-  d_ce_sk_var_mvs.clear();
+  d_setInnerSksModel = false;
+  d_innerSksModel.clear();
   // 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).
@@ -1097,7 +1031,7 @@ bool SynthConjecture::getSynthSolutionsInternal(std::vector<Node>& sols,
             TNode tsol = sol;
             sol = templ.substitute(templa, tsol);
             Trace("cegqi-inv-debug") << "With template : " << sol << std::endl;
-            sol = Rewriter::rewrite(sol);
+            sol = rewrite(sol);
             Trace("cegqi-inv-debug") << "Simplified : " << sol << std::endl;
             // now, reconstruct to the syntax
             sol = d_ceg_si->reconstructToSyntax(sol, tn, status, true);
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h
index d7635c816..a146c3b15 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.h
+++ b/src/theory/quantifiers/sygus/synth_conjecture.h
@@ -132,7 +132,7 @@ class SynthConjecture : protected EnvObj
    */
   Node getGuard() const;
   /** is ground */
-  bool isGround() { return d_inner_vars.empty(); }
+  bool isGround() const { return d_innerVars.empty(); }
   /** are we using single invocation techniques */
   bool isSingleInvocation() const;
   /** preregister conjecture
@@ -268,25 +268,23 @@ class SynthConjecture : protected EnvObj
    * (exists y. F) is shorthand above for ~( forall y. ~F ).
    */
   Node d_base_inst;
+  /** The skolemized form of the above formula. */
+  Node d_checkBody;
   /** list of variables on inner quantification */
-  std::vector<Node> d_inner_vars;
-  /**
-   * The set of skolems for the current "verification" lemma, if one exists.
-   * This may be added to during calls to doCheck(). The model values for these
-   * skolems are analyzed during doRefine().
-   */
-  std::vector<Node> d_ce_sk_vars;
+  std::vector<Node> d_innerVars;
+  /** list of skolems on inner quantification */
+  std::vector<Node> d_innerSks;
   /**
    * If we have already tested the satisfiability of the current verification
-   * lemma, this stores the model values of d_ce_sk_vars in the current
+   * lemma, this stores the model values of d_innerSks in the current
    * (satisfiable, failed) verification lemma.
    */
-  std::vector<Node> d_ce_sk_var_mvs;
+  std::vector<Node> d_innerSksModel;
   /**
    * Whether the above vector has been set. We have this flag since the above
    * vector may be set to empty (e.g. for ground synthesis conjectures).
    */
-  bool d_set_ce_sk_vars;
+  bool d_setInnerSksModel;
 
   /** the asserted (negated) conjecture */
   Node d_quant;