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 /src/theory/quantifiers/sygus/cegis_unif.cpp | |
| parent | c308c094548bcd9bee59e33334d147a9afe97018 (diff) | |
Fix purification in SygusUnifRL (#1912)
Diffstat (limited to 'src/theory/quantifiers/sygus/cegis_unif.cpp')
| -rw-r--r-- | src/theory/quantifiers/sygus/cegis_unif.cpp | 7 |
1 files changed, 2 insertions, 5 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 |