diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-05-10 11:38:03 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-05-10 11:38:03 -0500 |
| commit | aef0e5ed90b1b8913b5c8c743cbcd012d5916ba7 (patch) | |
| tree | 220b9c9758d342e0a6f95ba46a96730d31d6f417 | |
| parent | a7393ad4724476d7544483996f65877876698348 (diff) | |
Fix priority of decisions for cegis unif (#1897)
| -rw-r--r-- | src/theory/quantifiers/sygus/cegis_unif.cpp | 20 |
1 files 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); } |