diff options
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/quantifiers/sygus/cegis.cpp | 35 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/cegis.h | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_repair_const.cpp | 28 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_repair_const.h | 29 |
4 files changed, 80 insertions, 14 deletions
diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp index 96f347890..3a1ddc73c 100644 --- a/src/theory/quantifiers/sygus/cegis.cpp +++ b/src/theory/quantifiers/sygus/cegis.cpp @@ -198,6 +198,30 @@ bool Cegis::addEvalLemmas(const std::vector<Node>& candidates, return addedEvalLemmas; } +Node Cegis::getRefinementLemmaFormula() +{ + std::vector<Node> conj; + conj.insert( + conj.end(), d_refinement_lemmas.begin(), d_refinement_lemmas.end()); + // get the propagated values + for (unsigned i = 0, nprops = d_rl_eval_hds.size(); i < nprops; i++) + { + conj.push_back(d_rl_eval_hds[i].eqNode(d_rl_vals[i])); + } + // make the formula + NodeManager* nm = NodeManager::currentNM(); + Node ret; + if (conj.empty()) + { + ret = nm->mkConst(true); + } + else + { + ret = conj.size() == 1 ? conj[0] : nm->mkNode(AND, conj); + } + return ret; +} + bool Cegis::constructCandidates(const std::vector<Node>& enums, const std::vector<Node>& enum_values, const std::vector<Node>& candidates, @@ -235,11 +259,18 @@ bool Cegis::constructCandidates(const std::vector<Node>& enums, { std::vector<Node> fail_cvs = enum_values; Assert(candidates.size() == fail_cvs.size()); + // try to solve entire problem? if (src->repairSolution(candidates, fail_cvs, candidate_values)) { return true; } - // repair solution didn't work, exclude this solution + Node rl = getRefinementLemmaFormula(); + // try to solve for the refinement lemmas only + bool ret = + src->repairSolution(rl, candidates, fail_cvs, candidate_values); + // Even if ret is true, we will exclude the skeleton as well; this means + // that we have one chance to repair each skeleton. It is possible however + // that we might want to repair the same skeleton multiple times. std::vector<Node> exp; for (unsigned i = 0, size = enums.size(); i < size; i++) { @@ -252,7 +283,7 @@ bool Cegis::constructCandidates(const std::vector<Node>& enums, // must guard it expn = nm->mkNode(OR, d_parent->getGuard().negate(), expn.negate()); lems.push_back(expn); - return false; + return ret; } } diff --git a/src/theory/quantifiers/sygus/cegis.h b/src/theory/quantifiers/sygus/cegis.h index 891379992..08cf98c99 100644 --- a/src/theory/quantifiers/sygus/cegis.h +++ b/src/theory/quantifiers/sygus/cegis.h @@ -168,6 +168,8 @@ class Cegis : public SygusModule bool addEvalLemmas(const std::vector<Node>& candidates, const std::vector<Node>& candidate_values, std::vector<Node>& lems); + /** Get the node corresponding to the conjunction of all refinement lemmas. */ + Node getRefinementLemmaFormula(); //-----------------------------------end refinement lemmas /** Get refinement evaluation lemmas diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp index 4c5baa4bb..39506b593 100644 --- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp +++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp @@ -149,6 +149,19 @@ bool SygusRepairConst::repairSolution(const std::vector<Node>& candidates, std::vector<Node>& repair_cv, bool useConstantsAsHoles) { + return repairSolution(d_base_inst, + candidates, + candidate_values, + repair_cv, + useConstantsAsHoles); +} + +bool SygusRepairConst::repairSolution(Node sygusBody, + const std::vector<Node>& candidates, + const std::vector<Node>& candidate_values, + std::vector<Node>& repair_cv, + bool useConstantsAsHoles) +{ Assert(candidates.size() == candidate_values.size()); // if no grammar type allows constants, no repair is possible @@ -209,7 +222,8 @@ bool SygusRepairConst::repairSolution(const std::vector<Node>& candidates, NodeManager* nm = NodeManager::currentNM(); Trace("sygus-repair-const") << "Get first-order query..." << std::endl; - Node fo_body = getFoQuery(candidates, candidate_skeletons, sk_vars); + Node fo_body = + getFoQuery(sygusBody, candidates, candidate_skeletons, sk_vars); Trace("sygus-repair-const-debug") << "...got : " << fo_body << std::endl; @@ -225,7 +239,8 @@ bool SygusRepairConst::repairSolution(const std::vector<Node>& candidates, LogicInfo logic = smt::currentSmtEngine()->getLogicInfo(); if (logic.isTheoryEnabled(THEORY_ARITH) && logic.isLinear()) { - fo_body = fitToLogic(logic, + fo_body = fitToLogic(sygusBody, + logic, fo_body, candidates, candidate_skeletons, @@ -460,12 +475,12 @@ Node SygusRepairConst::getSkeleton(Node n, return visited[n]; } -Node SygusRepairConst::getFoQuery(const std::vector<Node>& candidates, +Node SygusRepairConst::getFoQuery(Node body, + const std::vector<Node>& candidates, const std::vector<Node>& candidate_skeletons, const std::vector<Node>& sk_vars) { NodeManager* nm = NodeManager::currentNM(); - Node body = d_base_inst; Trace("sygus-repair-const") << " Substitute skeletons..." << std::endl; body = body.substitute(candidates.begin(), candidates.end(), @@ -558,7 +573,8 @@ Node SygusRepairConst::getFoQuery(const std::vector<Node>& candidates, return fo_body; } -Node SygusRepairConst::fitToLogic(LogicInfo& logic, +Node SygusRepairConst::fitToLogic(Node body, + LogicInfo& logic, Node n, const std::vector<Node>& candidates, std::vector<Node>& candidate_skeletons, @@ -590,7 +606,7 @@ Node SygusRepairConst::fitToLogic(LogicInfo& logic, Assert(it != sk_vars.end()); sk_vars.erase(it); // reconstruct the query - n = getFoQuery(candidates, candidate_skeletons, sk_vars); + n = getFoQuery(body, candidates, candidate_skeletons, sk_vars); // reset the exclusion variable exc_var = Node::null(); } diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.h b/src/theory/quantifiers/sygus/sygus_repair_const.h index 26b7234a9..6be5ce5e6 100644 --- a/src/theory/quantifiers/sygus/sygus_repair_const.h +++ b/src/theory/quantifiers/sygus/sygus_repair_const.h @@ -53,9 +53,9 @@ class SygusRepairConst ~SygusRepairConst() {} /** initialize * - * Initialize this class with the base instantiation of the sygus conjecture - * (see CegConjecture::d_base_inst) and its candidate variables (see - * CegConjecture::d_candidates). + * Initialize this class with the base instantiation (body) of the sygus + * conjecture (see SynthConjecture::d_base_inst) and its candidate variables + * (see SynthConjecture::d_candidates). */ void initialize(Node base_inst, const std::vector<Node>& candidates); /** repair solution @@ -75,6 +75,17 @@ class SygusRepairConst * candidate_values to be repairable. In addition, if the flag * useConstantsAsHoles is true, we consider all constants whose (sygus) type * admit alls constants to be repairable. + * The repaired solution has the property that it satisfies the synthesis + * conjecture whose body is given by sygusBody. + */ + bool repairSolution(Node sygusBody, + const std::vector<Node>& candidates, + const std::vector<Node>& candidate_values, + std::vector<Node>& repair_cv, + bool useConstantsAsHoles = false); + /** + * Same as above, but where sygusBody is the body (base_inst) provided to the + * call to initialize of this class. */ bool repairSolution(const std::vector<Node>& candidates, const std::vector<Node>& candidate_values, @@ -148,12 +159,14 @@ class SygusRepairConst /** get first-order query * * This function returns a formula that is equivalent to the negation of the - * synthesis conjecture, where candidates are replaced by candidate_skeletons, + * synthesis conjecture whose body is given in the first argument, where + * candidates are replaced by candidate_skeletons, * whose free variables are in the set sk_vars. The returned formula * is a first-order (quantified) formula in the background logic, without UF, * of the form [***] above. */ - Node getFoQuery(const std::vector<Node>& candidates, + Node getFoQuery(Node body, + const std::vector<Node>& candidates, const std::vector<Node>& candidate_skeletons, const std::vector<Node>& sk_vars); /** fit to logic @@ -164,6 +177,9 @@ class SygusRepairConst * not enabled, we must undo some of the variables we introduced when * inferring candidate skeletons. * + * body is the (sygus) form of the original synthesis conjecture we are + * considering in this call. + * * This function may remove variables from sk_vars and the map * sk_vars_to_subs. The skeletons candidate_skeletons are obtained by * getSkeleton(...) on the resulting vectors. If this function returns a @@ -174,7 +190,8 @@ class SygusRepairConst * It uses the function below to choose which variables to remove from * sk_vars. */ - Node fitToLogic(LogicInfo& logic, + Node fitToLogic(Node body, + LogicInfo& logic, Node n, const std::vector<Node>& candidates, std::vector<Node>& candidate_skeletons, |