From aef0e5ed90b1b8913b5c8c743cbcd012d5916ba7 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 10 May 2018 11:38:03 -0500 Subject: [PATCH] Fix priority of decisions for cegis unif (#1897) --- src/theory/quantifiers/sygus/cegis_unif.cpp | 20 ++++++++++++++++++-- 1 file changed, 18 insertions(+), 2 deletions(-) diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp index a99e726b6..a5ab27bf3 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.cpp +++ b/src/theory/quantifiers/sygus/cegis_unif.cpp @@ -266,7 +266,7 @@ Node CegisUnifEnumManager::getNextDecisionRequest(unsigned& priority) bool value; if (!d_qe->getValuation().hasSatValue(lit, value)) { - priority = 0; + priority = 1; return lit; } else if (!value) @@ -306,7 +306,22 @@ void CegisUnifEnumManager::incrementNumEnumerators() Node size_eu = nm->mkNode(DT_SIZE, eu); Node size_eu_prev = nm->mkNode(DT_SIZE, eu_prev); Node sym_break = nm->mkNode(GEQ, size_eu, size_eu_prev); + Trace("cegis-unif-enum-lemma") + << "CegisUnifEnum::lemma, enum sym break:" << sym_break << "\n"; d_qe->getOutputChannel().lemma(sym_break); + // if the sygus datatype is interpreted as an infinite type + // (this should be the case for almost all examples) + if (!ct.isInterpretedFinite()) + { + // it is disequal from all previous ones + for (const Node eui : ci.second.d_enums) + { + Node deq = eu.eqNode(eui).negate(); + Trace("cegis-unif-enum-lemma") + << "CegisUnifEnum::lemma, enum deq:" << deq << "\n"; + d_qe->getOutputChannel().lemma(deq); + } + } } ci.second.d_enums.push_back(eu); d_tds->registerEnumerator(eu, d_null, d_parent); @@ -353,7 +368,8 @@ void CegisUnifEnumManager::registerEvalPtAtSize(TypeNode ct, disj.push_back(ei.eqNode(itc->second.d_enums[i])); } Node lem = NodeManager::currentNM()->mkNode(OR, disj); - Trace("cegis-unif-enum") << "Adding lemma " << lem << "\n"; + Trace("cegis-unif-enum-lemma") + << "CegisUnifEnum::lemma, domain:" << lem << "\n"; d_qe->getOutputChannel().lemma(lem); } -- 2.30.2