From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 2 Dec 2020 01:12:01 +0000 (-0600)
Subject: Remove assertion related to CEGQI dependency lemmas (#5559)
X-Git-Tag: cvc5-1.0.0~2529
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=fc92c8a035b43733ba50b7672ae40e97dcd9e518;p=cvc5.git

Remove assertion related to CEGQI dependency lemmas (#5559)

This assertion does not hold when we mix --sygus-inst with normal CEGQI.

Should fix the nightlies.
---

diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
index 1a67a2b16..1d917b8f4 100644
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
@@ -156,7 +156,11 @@ bool InstStrategyCegqi::registerCbqiLemma(Node q)
         {
           d_parent_quant[q].push_back(qi);
           d_children_quant[qi].push_back(q);
-          Assert(hasAddedCbqiLemma(qi));
+          // may not have added the CEX lemma, but the literal is created by
+          // the following call regardless. One rare case where this can happen
+          // is if both sygus-inst and CEGQI are being run in parallel, and
+          // a parent quantified formula is not handled by CEGQI, but a child
+          // is.
           Node qicel = getCounterexampleLiteral(qi);
           dep.push_back(qi);
           dep.push_back(qicel);
@@ -164,6 +168,9 @@ bool InstStrategyCegqi::registerCbqiLemma(Node q)
       }
       if (!dep.empty())
       {
+        // This lemma states that if the child is active, then the parent must
+        // be asserted, in particular G => Q where G is the CEX literal for the
+        // child and Q is the parent.
         Node dep_lemma = nm->mkNode(IMPLIES, ceLit, nm->mkNode(AND, dep));
         Trace("cegqi-lemma")
             << "Counterexample dependency lemma : " << dep_lemma << std::endl;