diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-12-01 19:12:01 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-12-01 17:12:01 -0800 |
commit | fc92c8a035b43733ba50b7672ae40e97dcd9e518 (patch) | |
tree | 7c56f83f96c83b70c50a44984363b70db720bfc6 /src | |
parent | a87df2bb60a8739d4eb24b60efca79f8d2b7d806 (diff) |
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.
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp | 9 |
1 files changed, 8 insertions, 1 deletions
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; |