summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/sygus/cegis_unif.cpp
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2021-02-22 17:19:20 -0600
committerGitHub <noreply@github.com>2021-02-22 17:19:20 -0600
commit13819c4ae33a103b1075e816772a305b16db9157 (patch)
treef8598d57ac30065091fd2115af2f25cef1673acd /src/theory/quantifiers/sygus/cegis_unif.cpp
parent4479383c2fd8a3b81ab63d66f843b09b5c9d0cd3 (diff)
Eliminate raw use of output channel and valuation in quantifiers (#5933)
This makes all lemmas in quantifiers sent through the inference manager. It begins adding InferenceId values for some of these calls. All uses of Valuation are replaced by calls to QuantifiersState.
Diffstat (limited to 'src/theory/quantifiers/sygus/cegis_unif.cpp')
-rw-r--r--src/theory/quantifiers/sygus/cegis_unif.cpp23
1 files changed, 14 insertions, 9 deletions
diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp
index 239fa3c94..c548f7f8f 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.cpp
+++ b/src/theory/quantifiers/sygus/cegis_unif.cpp
@@ -30,8 +30,9 @@ namespace quantifiers {
CegisUnif::CegisUnif(QuantifiersEngine* qe,
QuantifiersState& qs,
+ QuantifiersInferenceManager& qim,
SynthConjecture* p)
- : Cegis(qe, p), d_sygus_unif(p), d_u_enum_manager(qe, qs, p)
+ : Cegis(qe, qim, p), d_sygus_unif(p), d_u_enum_manager(qe, qs, qim, p)
{
}
@@ -216,7 +217,7 @@ bool CegisUnif::getEnumValues(const std::vector<Node>& enums,
<< "CegisUnif::lemma, inter-unif-enumerator "
"symmetry breaking lemma : "
<< slem << "\n";
- d_qe->getOutputChannel().lemma(slem);
+ d_qim.lemma(slem, InferenceId::UNKNOWN);
addedUnifEnumSymBreakLemma = true;
break;
}
@@ -364,7 +365,7 @@ bool CegisUnif::processConstructCandidates(const std::vector<Node>& enums,
{
Trace("cegis-unif-lemma")
<< "CegisUnif::lemma, separation lemma : " << lem << "\n";
- d_qe->getOutputChannel().lemma(lem);
+ d_qim.lemma(lem, InferenceId::UNKNOWN);
}
Trace("cegis-unif") << "..failed to separate heads\n---CegisUnif Engine---\n";
return false;
@@ -399,9 +400,13 @@ void CegisUnif::registerRefinementLemma(const std::vector<Node>& vars,
}
CegisUnifEnumDecisionStrategy::CegisUnifEnumDecisionStrategy(
- QuantifiersEngine* qe, QuantifiersState& qs, SynthConjecture* parent)
- : DecisionStrategyFmf(qs.getSatContext(), qe->getValuation()),
+ QuantifiersEngine* qe,
+ QuantifiersState& qs,
+ QuantifiersInferenceManager& qim,
+ SynthConjecture* parent)
+ : DecisionStrategyFmf(qs.getSatContext(), qs.getValuation()),
d_qe(qe),
+ d_qim(qim),
d_parent(parent)
{
d_initialized = false;
@@ -503,7 +508,7 @@ Node CegisUnifEnumDecisionStrategy::mkLiteral(unsigned n)
// G_uq_i => size(ve) >= log_2( i-1 )
// In other words, if we use i conditions, then we allow terms in our
// solution whose size is at most log_2(i-1).
- d_qe->getOutputChannel().lemma(fair_lemma);
+ d_qim.lemma(fair_lemma, InferenceId::UNKNOWN);
}
}
@@ -611,7 +616,7 @@ void CegisUnifEnumDecisionStrategy::setUpEnumerator(Node e,
Trace("cegis-unif-enum-lemma")
<< "CegisUnifEnum::lemma, remove redundant ops of " << e << " : "
<< sym_break_red_ops << "\n";
- d_qe->getOutputChannel().lemma(sym_break_red_ops);
+ d_qim.lemma(sym_break_red_ops, InferenceId::UNKNOWN);
}
// symmetry breaking between enumerators
if (!si.d_enums[index].empty() && index == 0)
@@ -622,7 +627,7 @@ void CegisUnifEnumDecisionStrategy::setUpEnumerator(Node e,
Node sym_break = nm->mkNode(GEQ, size_e, size_e_prev);
Trace("cegis-unif-enum-lemma")
<< "CegisUnifEnum::lemma, enum sym break:" << sym_break << "\n";
- d_qe->getOutputChannel().lemma(sym_break);
+ d_qim.lemma(sym_break, InferenceId::UNKNOWN);
}
// register the enumerator
si.d_enums[index].push_back(e);
@@ -678,7 +683,7 @@ void CegisUnifEnumDecisionStrategy::registerEvalPtAtSize(Node e,
Node lem = NodeManager::currentNM()->mkNode(OR, disj);
Trace("cegis-unif-enum-lemma")
<< "CegisUnifEnum::lemma, domain:" << lem << "\n";
- d_qe->getOutputChannel().lemma(lem);
+ d_qim.lemma(lem, InferenceId::UNKNOWN);
}
} // namespace quantifiers
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback