From fc92c8a035b43733ba50b7672ae40e97dcd9e518 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 1 Dec 2020 19:12:01 -0600 Subject: [PATCH] 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. --- src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) 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; -- 2.30.2