diff options
Diffstat (limited to 'src/theory/quantifiers/sygus/cegis.cpp')
| -rw-r--r-- | src/theory/quantifiers/sygus/cegis.cpp | 28 |
1 files changed, 20 insertions, 8 deletions
diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp index c8e14e4bd..fdc0b28e0 100644 --- a/src/theory/quantifiers/sygus/cegis.cpp +++ b/src/theory/quantifiers/sygus/cegis.cpp @@ -39,6 +39,7 @@ Cegis::Cegis(Env& env, SynthConjecture* p) : SygusModule(env, qs, qim, tds, p), d_eval_unfold(tds->getEvalUnfold()), + d_cexClosedEnum(false), d_cegis_sampler(env), d_usingSymCons(false) { @@ -47,11 +48,18 @@ Cegis::Cegis(Env& env, bool Cegis::initialize(Node conj, Node n, const std::vector<Node>& candidates) { d_base_body = n; + d_cexClosedEnum = true; if (d_base_body.getKind() == NOT && d_base_body[0].getKind() == FORALL) { for (const Node& v : d_base_body[0][0]) { d_base_vars.push_back(v); + if (!v.getType().isClosedEnumerable()) + { + // not closed enumerable, refinement lemmas cannot be sent to the + // quantifier-free datatype solver + d_cexClosedEnum = false; + } } d_base_body = d_base_body[0][1]; } @@ -467,14 +475,18 @@ void Cegis::addRefinementLemmaConjunct(unsigned wcounter, void Cegis::registerRefinementLemma(const std::vector<Node>& vars, Node lem) { addRefinementLemma(lem); - // Make the refinement lemma and add it to lems. - // This lemma is guarded by the parent's guard, which has the semantics - // "this conjecture has a solution", hence this lemma states: - // if the parent conjecture has a solution, it satisfies the specification - // for the given concrete point. - Node rlem = - NodeManager::currentNM()->mkNode(OR, d_parent->getGuard().negate(), lem); - d_qim.addPendingLemma(rlem, InferenceId::QUANTIFIERS_SYGUS_CEGIS_REFINE); + // must be closed enumerable + if (d_cexClosedEnum && options().quantifiers.sygusEvalUnfold) + { + // Make the refinement lemma and add it to lems. + // This lemma is guarded by the parent's guard, which has the semantics + // "this conjecture has a solution", hence this lemma states: + // if the parent conjecture has a solution, it satisfies the specification + // for the given concrete point. + Node rlem = NodeManager::currentNM()->mkNode( + OR, d_parent->getGuard().negate(), lem); + d_qim.addPendingLemma(rlem, InferenceId::QUANTIFIERS_SYGUS_CEGIS_REFINE); + } } bool Cegis::usingRepairConst() { return true; } |