diff options
author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2018-05-14 15:09:31 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-05-14 15:09:31 -0500 |
commit | b5264346e85bc7ca0235048f686cc252c60b0014 (patch) | |
tree | 0cdccbae0a91ffea9e187a02d13a9eddbe40c693 | |
parent | c308c094548bcd9bee59e33334d147a9afe97018 (diff) |
Fix purification in SygusUnifRL (#1912)
-rw-r--r-- | src/theory/quantifiers/sygus/cegis_unif.cpp | 7 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_unif_rl.cpp | 39 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_unif_rl.h | 2 |
3 files changed, 30 insertions, 18 deletions
diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp index 2456839e7..def21e6cc 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.cpp +++ b/src/theory/quantifiers/sygus/cegis_unif.cpp @@ -38,11 +38,10 @@ bool CegisUnif::initialize(Node n, const std::vector<Node>& candidates, std::vector<Node>& lemmas) { - Trace("cegis-unif") << "Initialize CegisUnif : " << n << std::endl; + Trace("cegis-unif-debug") << "Initialize CegisUnif : " << n << std::endl; // Init UNIF util std::map<Node, std::vector<Node>> strategy_lemmas; d_sygus_unif.initialize(d_qe, candidates, d_cond_enums, strategy_lemmas); - Trace("cegis-unif") << "Initializing enums for pure Cegis case\n"; std::vector<Node> unif_candidates; // Initialize enumerators for non-unif functions-to-synhesize for (const Node& c : candidates) @@ -148,7 +147,6 @@ bool CegisUnif::constructCandidates(const std::vector<Node>& enums, // evaluate on refinement lemmas if (addEvalLemmas(enums, enum_values)) { - Trace("cegis-unif-lemma") << "Added eval lemmas\n"; return false; } // build solutions (for unif candidates a divide-and-conquer approach is used) @@ -179,11 +177,10 @@ void CegisUnif::registerRefinementLemma(const std::vector<Node>& vars, std::map<Node, std::vector<Node>> eval_pts; Node plem = d_sygus_unif.addRefLemma(lem, eval_pts); d_refinement_lemmas.push_back(plem); - Trace("cegis-unif") << "* Refinement lemma:\n" << plem << "\n"; + Trace("cegis-unif-lemma") << "* Refinement lemma:\n" << plem << "\n"; // Notify the enumeration manager if there are new evaluation points for (const std::pair<const Node, std::vector<Node>>& ep : eval_pts) { - Trace("cegis-unif") << "** Registering new point:\n" << plem << "\n"; d_u_enum_manager.registerEvalPts(ep.second, ep.first); } // Make the refinement lemma and add it to lems. This lemma is guarded by the diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp index 427d413c8..6f68a9871 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp @@ -111,10 +111,25 @@ Node SygusUnifRl::purifyLemma(Node n, // occurring under a unification function-to-synthesize if (ensureConst) { - nv = d_parent->getModelValue(n); - Assert(n != nv); + std::map<Node, Node>::iterator it = d_cand_to_sol.find(n[0]); + // if function-to-synthesize, retrieve its built solution to replace in + // the application before computing the model value + AlwaysAssert(!u_fapp || it != d_cand_to_sol.end()); + if (it != d_cand_to_sol.end()) + { + TNode cand = n[0]; + Node tmp = n.substitute(cand, it->second); + nv = d_tds->evaluateWithUnfolding(tmp); + Trace("sygus-unif-rl-purify") << "PurifyLemma : model value for " << tmp + << " is " << nv << "\n"; + } + else + { + nv = d_parent->getModelValue(n); Trace("sygus-unif-rl-purify") << "PurifyLemma : model value for " << n << " is " << nv << "\n"; + } + Assert(n != nv); } } // Travese to purify @@ -299,20 +314,18 @@ bool SygusUnifRl::constructSolution(std::vector<Node>& sols) Trace("sygus-unif-rl-sol") << "Adding solution " << v << " to non-unif candidate " << c << "\n"; sols.push_back(v); + continue; } - else + initializeConstructSolFor(c); + Node v = constructSol(c, d_strategy[c].getRootEnumerator(), role_equal, 0); + if (v.isNull()) { - initializeConstructSolFor(c); - Node v = - constructSol(c, d_strategy[c].getRootEnumerator(), role_equal, 0); - if (v.isNull()) - { - return false; - } - Trace("sygus-unif-rl-sol") << "Adding solution " << v - << " to unif candidate " << c << "\n"; - sols.push_back(v); + return false; } + Trace("sygus-unif-rl-sol") << "Adding solution " << v + << " to unif candidate " << c << "\n"; + sols.push_back(v); + d_cand_to_sol[c] = v; } return true; } diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.h b/src/theory/quantifiers/sygus/sygus_unif_rl.h index 941bb5763..09a226ae7 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_rl.h +++ b/src/theory/quantifiers/sygus/sygus_unif_rl.h @@ -98,6 +98,8 @@ class SygusUnifRl : public SygusUnif void initializeConstructSol() override; /** initialize construction solution for function-to-synthesize f */ void initializeConstructSolFor(Node f) override; + /** maps unif functions-to~synhesize to their last built solutions */ + std::map<Node, Node> d_cand_to_sol; /* -------------------------------------------------------------- Purification |