From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 12 Nov 2020 16:56:25 +0000 (-0600)
Subject: Fix redundant refinement lemma in sygus solver (#5399)
X-Git-Tag: cvc5-1.0.0~2607
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3b79066c39054efb95fdb71c3727482764e8a064;p=cvc5.git

Fix redundant refinement lemma in sygus solver (#5399)

This ensures we do manual exclusion of candidate solutions that have counterexamples that are repeated, in particular in the case where the synthesis conjecture has no free variables.

This PR removes special casing for ground synthesis conjectures and fixes the exclusion during the refinement stage of sygus.

This is a prerequisite for updating arithmetic to not eliminate extended operators at expand definitions, which forces this feature to be exercised in a number of regressions.
---

diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index 2b4eba3b7..8dd9a455a 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -519,31 +519,25 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems)
     inst = d_base_inst;
   }
 
-  // check whether we will run CEGIS on inner skolem variables
-  bool sk_refine = (!isGround() || d_refine_count == 0) && constructed_cand;
-  if (sk_refine)
+  if (!constructed_cand)
   {
-    if (options::cegisSample() == options::CegisSampleMode::TRUST)
-    {
-      // 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;
-      return true;
-    }
-    Assert(!d_set_ce_sk_vars);
+    return false;
   }
-  else
+
+  // if we trust the sampling we ran, we terminate now
+  if (options::cegisSample() == options::CegisSampleMode::TRUST)
   {
-    if (!constructed_cand)
-    {
-      return false;
-    }
+    // 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;
+    return true;
   }
+  Assert(!d_set_ce_sk_vars);
 
   // immediately skolemize inner existentials
   Node lem;
@@ -587,11 +581,8 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems)
       lem = inst;
     }
   }
-  if (sk_refine)
-  {
-    d_ce_sk_vars.insert(d_ce_sk_vars.end(), sks.begin(), sks.end());
-    d_set_ce_sk_vars = true;
-  }
+  d_ce_sk_vars.insert(d_ce_sk_vars.end(), sks.begin(), sks.end());
+  d_set_ce_sk_vars = true;
 
   if (lem.isNull())
   {
@@ -807,8 +798,13 @@ bool SynthConjecture::doRefine()
     Trace("sygus-engine-debug") << "  ...(warning) failed to refine candidate, "
                                    "manually exclude candidate."
                                 << std::endl;
+    std::vector<Node> cvals;
+    for (const Node& c : d_candidates)
+    {
+      cvals.push_back(d_cinfo[c].d_inst.back());
+    }
     // something went wrong, exclude the current candidate
-    excludeCurrentSolution(sk_vars, sk_subs);
+    excludeCurrentSolution(d_candidates, cvals);
     // Note this happens when evaluation is incapable of disproving a candidate
     // for counterexample point c, but satisfiability checking happened to find
     // the the same point c is indeed a true counterexample. It is sound
@@ -1087,6 +1083,8 @@ void SynthConjecture::printAndContinueStream(const std::vector<Node>& enums,
 void SynthConjecture::excludeCurrentSolution(const std::vector<Node>& enums,
                                              const std::vector<Node>& values)
 {
+  Trace("cegqi-debug") << "Exclude current solution: " << 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;