diff options
Diffstat (limited to 'src/theory/quantifiers/sygus')
| -rw-r--r-- | src/theory/quantifiers/sygus/cegis.cpp | 28 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/cegis.h | 7 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/cegis_core_connective.cpp | 74 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/cegis_core_connective.h | 42 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_grammar_cons.cpp | 3 |
5 files changed, 35 insertions, 119 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; } diff --git a/src/theory/quantifiers/sygus/cegis.h b/src/theory/quantifiers/sygus/cegis.h index 8e0fffdd1..8d1f0a1b2 100644 --- a/src/theory/quantifiers/sygus/cegis.h +++ b/src/theory/quantifiers/sygus/cegis.h @@ -119,6 +119,13 @@ class Cegis : public SygusModule std::vector<Node> d_rl_vals; /** all variables appearing in refinement lemmas */ std::unordered_set<Node> d_refinement_lemma_vars; + /** + * Are the counterexamples we are handling in this class of only closed + * enumerable types (see TypeNode::isClosedEnumerable). If this is false, + * then CEGIS refinement lemmas can contain terms that are unhandled by + * theory solvers, e.g. uninterpreted constants. + */ + bool d_cexClosedEnum; /** adds lem as a refinement lemma */ void addRefinementLemma(Node lem); diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.cpp b/src/theory/quantifiers/sygus/cegis_core_connective.cpp index 936310e4e..5a0cf8724 100644 --- a/src/theory/quantifiers/sygus/cegis_core_connective.cpp +++ b/src/theory/quantifiers/sygus/cegis_core_connective.cpp @@ -33,41 +33,6 @@ namespace cvc5 { namespace theory { namespace quantifiers { -bool VariadicTrie::add(Node n, const std::vector<Node>& i) -{ - VariadicTrie* curr = this; - for (const Node& ic : i) - { - curr = &(curr->d_children[ic]); - } - if (curr->d_data.isNull()) - { - curr->d_data = n; - return true; - } - return false; -} - -bool VariadicTrie::hasSubset(const std::vector<Node>& is) const -{ - if (!d_data.isNull()) - { - return true; - } - for (const std::pair<const Node, VariadicTrie>& p : d_children) - { - Node n = p.first; - if (std::find(is.begin(), is.end(), n) != is.end()) - { - if (p.second.hasSubset(is)) - { - return true; - } - } - } - return false; -} - CegisCoreConnective::CegisCoreConnective(Env& env, QuantifiersState& qs, QuantifiersInferenceManager& qim, @@ -595,38 +560,6 @@ bool CegisCoreConnective::Component::addToAsserts(CegisCoreConnective* p, return true; } -void CegisCoreConnective::getModel(SolverEngine& smt, - std::vector<Node>& vals) const -{ - for (const Node& v : d_vars) - { - Node mv = smt.getValue(v); - Trace("sygus-ccore-model") << v << " -> " << mv << " "; - vals.push_back(mv); - } -} - -bool CegisCoreConnective::getUnsatCore( - SolverEngine& smt, - const std::unordered_set<Node>& queryAsserts, - std::vector<Node>& uasserts) const -{ - UnsatCore uc = smt.getUnsatCore(); - bool hasQuery = false; - for (UnsatCore::const_iterator i = uc.begin(); i != uc.end(); ++i) - { - Node uassert = *i; - Trace("sygus-ccore-debug") << " uc " << uassert << std::endl; - if (queryAsserts.find(uassert) != queryAsserts.end()) - { - hasQuery = true; - continue; - } - uasserts.push_back(uassert); - } - return hasQuery; -} - Result CegisCoreConnective::checkSat(Node n, std::vector<Node>& mvs) const { Trace("sygus-ccore-debug") << "...check-sat " << n << "..." << std::endl; @@ -758,7 +691,8 @@ Node CegisCoreConnective::constructSolutionFromPool(Component& ccheck, std::unordered_set<Node> queryAsserts; queryAsserts.insert(ccheck.getFormula()); queryAsserts.insert(d_sc); - bool hasQuery = getUnsatCore(*checkSol, queryAsserts, uasserts); + bool hasQuery = + getUnsatCoreFromSubsolver(*checkSol, queryAsserts, uasserts); // now, check the side condition bool falseCore = false; if (!d_sc.isNull()) @@ -794,7 +728,7 @@ Node CegisCoreConnective::constructSolutionFromPool(Component& ccheck, uasserts.clear(); std::unordered_set<Node> queryAsserts2; queryAsserts2.insert(d_sc); - getUnsatCore(*checkSc, queryAsserts2, uasserts); + getUnsatCoreFromSubsolver(*checkSc, queryAsserts2, uasserts); falseCore = true; } } @@ -838,7 +772,7 @@ Node CegisCoreConnective::constructSolutionFromPool(Component& ccheck, // it does not entail the postcondition, add an assertion that blocks // the current point mvs.clear(); - getModel(*checkSol, mvs); + getModelFromSubsolver(*checkSol, d_vars, mvs); // should evaluate to true Node ean = evaluatePt(an, Node::null(), mvs); Assert(ean.isConst() && ean.getConst<bool>()); diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.h b/src/theory/quantifiers/sygus/cegis_core_connective.h index 3ee631dea..26784f939 100644 --- a/src/theory/quantifiers/sygus/cegis_core_connective.h +++ b/src/theory/quantifiers/sygus/cegis_core_connective.h @@ -22,6 +22,7 @@ #include "expr/node.h" #include "expr/node_trie.h" +#include "expr/variadic_trie.h" #include "smt/env_obj.h" #include "theory/quantifiers/sygus/cegis.h" #include "util/result.h" @@ -33,30 +34,6 @@ class SolverEngine; namespace theory { namespace quantifiers { -/** - * A trie that stores data at undetermined depth. Storing data at - * undetermined depth is in contrast to the NodeTrie (expr/node_trie.h), which - * assumes all data is stored at a fixed depth. - * - * Since data can be stored at any depth, we require both a d_children field - * and a d_data field. - */ -class VariadicTrie -{ - public: - /** the children of this node */ - std::map<Node, VariadicTrie> d_children; - /** the data at this node */ - Node d_data; - /** - * Add data with identifier n indexed by i, return true if data is not already - * stored at the node indexed by i. - */ - bool add(Node n, const std::vector<Node>& i); - /** Is there any data in this trie that is indexed by any subset of is? */ - bool hasSubset(const std::vector<Node>& is) const; -}; - /** CegisCoreConnective * * A sygus module that is specialized in handling conjectures of the form: @@ -336,23 +313,6 @@ class CegisCoreConnective : public Cegis Node d_sc; //-----------------------------------for SMT engine calls /** - * Assuming smt has just been called to check-sat and returned "SAT", this - * method adds the model for d_vars to mvs. - */ - void getModel(SolverEngine& smt, std::vector<Node>& mvs) const; - /** - * Assuming smt has just been called to check-sat and returned "UNSAT", this - * method get the unsat core and adds it to uasserts. - * - * The assertions in the argument queryAsserts (which we are not interested - * in tracking in the unsat core) are excluded from uasserts. - * If one of the formulas in queryAsserts was in the unsat core, then this - * method returns true. Otherwise, this method returns false. - */ - bool getUnsatCore(SolverEngine& smt, - const std::unordered_set<Node>& queryAsserts, - std::vector<Node>& uasserts) const; - /** * Return the result of checking satisfiability of formula n. * If n was satisfiable, then we store the model for d_vars in mvs. */ diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index 43c958ff9..9b4cfb9e1 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -20,6 +20,7 @@ #include "expr/ascription_type.h" #include "expr/dtype_cons.h" +#include "expr/node_algorithm.h" #include "options/quantifiers_options.h" #include "theory/bv/theory_bv_utils.h" #include "theory/datatypes/sygus_datatype_utils.h" @@ -420,6 +421,8 @@ void CegGrammarConstructor::mkSygusConstantsForType(TypeNode type, { // generate constant array over the first element of the constituent type Node c = type.mkGroundTerm(); + // note that c should never contain an uninterpreted constant + Assert(!expr::hasSubtermKind(UNINTERPRETED_CONSTANT, c)); ops.push_back(c); } else if (type.isRoundingMode()) |