From: Haniel Barbosa Date: Tue, 8 May 2018 18:41:37 +0000 (-0500) Subject: Classifying data in SygusUnifRL (#1886) X-Git-Tag: cvc5-1.0.0~5079 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=919c30e541668ad1ada6a294be55112594a942bd;p=cvc5.git Classifying data in SygusUnifRL (#1886) --- diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp index 8fa4af99c..06b552276 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.cpp +++ b/src/theory/quantifiers/sygus/cegis_unif.cpp @@ -2,7 +2,7 @@ /*! \file cegis_unif.cpp ** \verbatim ** Top contributors (to current version): - ** Haniel Barbosa + ** Haniel Barbosa, Andrew Reynolds ** This file is part of the CVC4 project. ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. @@ -39,11 +39,11 @@ bool CegisUnif::initialize(Node n, std::vector& lemmas) { Trace("cegis-unif") << "Initialize CegisUnif : " << n << std::endl; - /* Init UNIF util */ + // Init UNIF util d_sygus_unif.initialize(d_qe, candidates, d_cond_enums, lemmas); Trace("cegis-unif") << "Initializing enums for pure Cegis case\n"; std::vector unif_candidates; - /* Initialize enumerators for non-unif functions-to-synhesize */ + // Initialize enumerators for non-unif functions-to-synhesize for (const Node& c : candidates) { if (!d_sygus_unif.usingUnif(c)) @@ -81,12 +81,12 @@ void CegisUnif::getTermList(const std::vector& candidates, Valuation& valuation = d_qe->getValuation(); for (const Node& e : d_cond_enums) { - Trace("cegis-unif-debug") - << "Check conditional enumerator : " << e << std::endl; + Trace("cegis-unif-debug") << "Check conditional enumerator : " << e + << std::endl; Assert(d_enum_to_active_guard.find(e) != d_enum_to_active_guard.end()); Node g = d_enum_to_active_guard[e]; - /* Get whether the active guard for this enumerator is set. If so, then - there may exist more values for it, and hence we add it to enums. */ + // Get whether the active guard for this enumerator is set. If so, then + // there may exist more values for it, and hence we add it to enums. Node gstatus = valuation.getSatValue(g); if (!gstatus.isNull() && gstatus.getConst()) { @@ -113,7 +113,7 @@ bool CegisUnif::constructCandidates(const std::vector& enums, Trace("cegis-unif-enum") << "Register new enumerated values :\n"; for (unsigned i = 0, size = enums.size(); i < size; ++i) { - /* Only conditional enumerators will be notified to unif utility */ + // Only conditional enumerators will be notified to unif utility if (std::find(d_cond_enums.begin(), d_cond_enums.end(), enums[i]) == d_cond_enums.end()) { @@ -139,7 +139,7 @@ bool CegisUnif::constructCandidates(const std::vector& enums, enum_consider.push_back(i); } } - /* only consider the enumerators that are at minimum size (for fairness) */ + // only consider the enumerators that are at minimum size (for fairness) Trace("cegis-unif-enum") << "...register " << enum_consider.size() << " / " << enums.size() << std::endl; for (unsigned i = 0, ecsize = enum_consider.size(); i < ecsize; ++i) @@ -148,7 +148,7 @@ bool CegisUnif::constructCandidates(const std::vector& enums, Node e = enums[j], v = enum_values[j]; std::vector enum_lems; d_sygus_unif.notifyEnumeration(e, v, enum_lems); - /* the lemmas must be guarded by the active guard of the enumerator */ + // the lemmas must be guarded by the active guard of the enumerator Assert(d_enum_to_active_guard.find(e) != d_enum_to_active_guard.end()); Node g = d_enum_to_active_guard[e]; for (unsigned j = 0, size = enum_lems.size(); j < size; ++j) @@ -157,7 +157,7 @@ bool CegisUnif::constructCandidates(const std::vector& enums, } lems.insert(lems.end(), enum_lems.begin(), enum_lems.end()); } - /* divide-and-conquer solution bulding for candidates using unif util */ + // divide-and-conquer solution bulding for candidates using unif util std::vector sols; if (d_sygus_unif.constructSolution(sols)) { @@ -180,10 +180,10 @@ void CegisUnif::registerRefinementLemma(const std::vector& vars, { d_u_enum_manager.registerEvalPts(ep.second, ep.first); } - /* 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. */ + // 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. lems.push_back(NodeManager::currentNM()->mkNode( OR, d_parent->getGuard().negate(), plem)); } diff --git a/src/theory/quantifiers/sygus/cegis_unif.h b/src/theory/quantifiers/sygus/cegis_unif.h index 93ab69668..4ea6a887a 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.h +++ b/src/theory/quantifiers/sygus/cegis_unif.h @@ -2,7 +2,7 @@ /*! \file cegis_unif.h ** \verbatim ** Top contributors (to current version): - ** Haniel Barbosa + ** Haniel Barbosa, Andrew Reynolds ** This file is part of the CVC4 project. ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp index 2f0460c64..1260c62af 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp @@ -2,7 +2,7 @@ /*! \file sygus_unif_rl.cpp ** \verbatim ** Top contributors (to current version): - ** Haniel Barbosa + ** Haniel Barbosa, Andrew Reynolds ** This file is part of the CVC4 project. ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. @@ -30,8 +30,6 @@ void SygusUnifRl::initialize(QuantifiersEngine* qe, std::vector& enums, std::vector& lemmas) { - d_ecache.clear(); - d_cand_to_eval_hds.clear(); // initialize std::vector all_enums; SygusUnif::initialize(qe, funs, all_enums, lemmas); @@ -42,12 +40,12 @@ void SygusUnifRl::initialize(QuantifiersEngine* qe, registerStrategy(f); } enums.insert(enums.end(), d_cond_enums.begin(), d_cond_enums.end()); - /* Copy candidates and check whether CegisUnif for any of them */ + // Copy candidates and check whether CegisUnif for any of them for (const Node& c : d_unif_candidates) { - d_app_to_pt[c].clear(); + d_hd_to_pt[c].clear(); d_cand_to_eval_hds[c].clear(); - d_purified_count[c] = 0; + d_cand_to_hd_count[c] = 0; } } @@ -55,13 +53,29 @@ void SygusUnifRl::notifyEnumeration(Node e, Node v, std::vector& lemmas) { Trace("sygus-unif-rl-notify") << "SyGuSUnifRl: Adding to enum " << e << " value " << v << "\n"; - d_ecache[e].d_enum_vals.push_back(v); - /* Exclude v from next enumerations for e */ + // Exclude v from next enumerations for e Node exc_lemma = d_tds->getExplain()->getExplanationForEquality(e, v).negate(); - Trace("sygus-unif-rl-notify") + Trace("sygus-unif-rl-notify-debug") << "SygusUnifRl : enumeration exclude lemma : " << exc_lemma << std::endl; lemmas.push_back(exc_lemma); + // Update all desicion trees in which this enumerator is a conditional + // enumerator, if any + std::map>::iterator it = d_cenum_to_stratpt.find(e); + if (it == d_cenum_to_stratpt.end()) + { + return; + } + for (const Node& stratpt : it->second) + { + Trace("sygus-unif-rl-dt") + << "...adding value " << v + << " to decision tree of strategy point : " << stratpt << std::endl; + Assert(d_stratpt_to_dt.find(stratpt) != d_stratpt_to_dt.end()); + // Register new condition value + d_stratpt_to_dt[stratpt].addCondValue(v); + Trace("sygus-unif-rl-dt") << "...added\n"; + } } Node SygusUnifRl::purifyLemma(Node n, @@ -76,12 +90,12 @@ Node SygusUnifRl::purifyLemma(Node n, Trace("sygus-unif-rl-purify-debug") << "... already visited " << n << "\n"; return it->second; } - /* Recurse */ + // Recurse unsigned size = n.getNumChildren(); Kind k = n.getKind(); - /* We retrive model value now because purified node may not have a value */ + // We retrive model value now because purified node may not have a value Node nv = n; - /* Whether application of a function-to-synthesize */ + // Whether application of a function-to-synthesize bool fapp = k == APPLY_UF && size > 0; bool u_fapp = false; bool nu_fapp = false; @@ -89,20 +103,20 @@ Node SygusUnifRl::purifyLemma(Node n, { Assert(std::find(d_candidates.begin(), d_candidates.end(), n[0]) != d_candidates.end()); - /* Whether application of a (non-)unification function-to-synthesize */ + // Whether application of a (non-)unification function-to-synthesize u_fapp = usingUnif(n[0]); nu_fapp = !usingUnif(n[0]); - /* get model value of non-top level applications of functions-to-synthesize - occurring under a unification function-to-synthesize */ + // get model value of non-top level applications of functions-to-synthesize + // occurring under a unification function-to-synthesize if (ensureConst) { nv = d_parent->getModelValue(n); Assert(n != nv); - Trace("sygus-unif-rl-purify") - << "PurifyLemma : model value for " << n << " is " << nv << "\n"; + Trace("sygus-unif-rl-purify") << "PurifyLemma : model value for " << n + << " is " << nv << "\n"; } } - /* Travese to purify */ + // Travese to purify bool childChanged = false; std::vector children; NodeManager* nm = NodeManager::currentNM(); @@ -113,7 +127,7 @@ Node SygusUnifRl::purifyLemma(Node n, children.push_back(n[i]); continue; } - /* Arguments of non-unif functions do not need to be constant */ + // Arguments of non-unif functions do not need to be constant Node child = purifyLemma( n[i], !nu_fapp && (ensureConst || u_fapp), model_guards, cache); children.push_back(child); @@ -122,10 +136,21 @@ Node SygusUnifRl::purifyLemma(Node n, Node nb; if (childChanged) { - if (n.hasOperator()) + if (fapp && n.hasOperator()) { + Trace("sygus-unif-rl-purify-debug") << "Node " << n + << " has operator and fapp is true\n"; children.insert(children.begin(), n.getOperator()); } + if (Trace.isOn("sygus-unif-rl-purify-debug")) + { + Trace("sygus-unif-rl-purify-debug") + << "...rebuilding " << n << " with kind " << k << " and children:\n"; + for (const Node& child : children) + { + Trace("sygus-unif-rl-purify-debug") << "...... " << child << "\n"; + } + } nb = NodeManager::currentNM()->mkNode(k, children); Trace("sygus-unif-rl-purify") << "PurifyLemma : transformed " << n << " into " << nb << "\n"; @@ -134,7 +159,7 @@ Node SygusUnifRl::purifyLemma(Node n, { nb = n; } - /* Map to point enumerator every unification function-to-synthesize */ + // Map to point enumerator every unification function-to-synthesize if (u_fapp) { Node np; @@ -146,28 +171,29 @@ Node SygusUnifRl::purifyLemma(Node n, Assert(nb.hasOperator()); children.insert(children.begin(), n.getOperator()); } - /* Build purified head with fresh skolem and recreate node */ + // Build purified head with fresh skolem and recreate node std::stringstream ss; - ss << nb[0] << "_" << d_purified_count[nb[0]]++; + ss << nb[0] << "_" << d_cand_to_hd_count[nb[0]]++; Node new_f = nm->mkSkolem(ss.str(), nb[0].getType()); - /* Adds new enumerator to map from candidate */ + // Adds new enumerator to map from candidate Trace("sygus-unif-rl-purify") << "...new enum " << new_f - << " for candidate " << nb[0] << "\n"; + << " for candidate " << nb[0] << "\n"; d_cand_to_eval_hds[nb[0]].push_back(new_f); - /* Maps new enumerator to its respective tuple of arguments */ - d_app_to_pt[new_f] = + // Maps new enumerator to its respective tuple of arguments + d_hd_to_pt[new_f] = std::vector(children.begin() + 2, children.end()); - if (Trace.isOn("sygus-unif-rl-purify")) + if (Trace.isOn("sygus-unif-rl-purify-debug")) { - Trace("sygus-unif-rl-purify") << "...[" << new_f << "] --> ("; - for (const Node& pt_i : d_app_to_pt[new_f]) + Trace("sygus-unif-rl-purify-debug") << "...[" << new_f << "] --> ("; + for (const Node& pt_i : d_hd_to_pt[new_f]) { - Trace("sygus-unif-rl-purify") << pt_i << " "; + Trace("sygus-unif-rl-purify-debug") << pt_i << " "; } - Trace("sygus-unif-rl-purify") << ")\n"; + Trace("sygus-unif-rl-purify-debug") << ")\n"; } - /* replace first child and rebulid node */ + // replace first child and rebulid node children[1] = new_f; + Assert(children.size() > 1); np = NodeManager::currentNM()->mkNode(k, children); d_app_to_purified[nb] = np; } @@ -180,7 +206,7 @@ Node SygusUnifRl::purifyLemma(Node n, << np << "\n"; nb = np; } - /* Add equality between purified fapp and model value */ + // Add equality between purified fapp and model value if (ensureConst && fapp) { model_guards.push_back( @@ -190,8 +216,8 @@ Node SygusUnifRl::purifyLemma(Node n, << model_guards.back() << "\n"; } nb = Rewriter::rewrite(nb); - /* every non-top level application of function-to-synthesize must be reduced - to a concrete constant */ + // every non-top level application of function-to-synthesize must be reduced + // to a concrete constant Assert(!ensureConst || nb.isConst()); Trace("sygus-unif-rl-purify-debug") << "... caching [" << n << "] = " << nb << "\n"; @@ -203,7 +229,7 @@ Node SygusUnifRl::addRefLemma(Node lemma, std::map>& eval_hds) { Trace("sygus-unif-rl-purify") << "Registering lemma at SygusUnif : " << lemma - << "\n"; + << "\n"; std::vector model_guards; BoolNodePairMap cache; // cache previous sizes @@ -213,7 +239,7 @@ Node SygusUnifRl::addRefLemma(Node lemma, prev_n_eval_hds[cp.first] = cp.second.size(); } - /* Make the purified lemma which will guide the unification utility. */ + // Make the purified lemma which will guide the unification utility. Node plem = purifyLemma(lemma, false, model_guards, cache); if (!model_guards.empty()) { @@ -236,6 +262,20 @@ Node SygusUnifRl::addRefLemma(Node lemma, for (unsigned j = prevn, size = cp.second.size(); j < size; j++) { eval_hds[c].push_back(cp.second[j]); + // Add new point to respective decision trees + Assert(d_cand_cenums.find(c) != d_cand_cenums.end()); + for (const Node& cenum : d_cand_cenums[c]) + { + Assert(d_cenum_to_stratpt.find(cenum) != d_cenum_to_stratpt.end()); + for (const Node& stratpt : d_cenum_to_stratpt[cenum]) + { + Assert(d_stratpt_to_dt.find(stratpt) != d_stratpt_to_dt.end()); + Trace("sygus-unif-rl-dt") << "Add point with head " << cp.second[j] + << " to strategy point " << stratpt << "\n"; + // Register new point from new head + d_stratpt_to_dt[stratpt].addPoint(cp.second[j]); + } + } } } @@ -265,8 +305,8 @@ bool SygusUnifRl::constructSolution(std::vector& sols) { return false; } - Trace("sygus-unif-rl-sol") - << "Adding solution " << v << " to unif candidate " << c << "\n"; + Trace("sygus-unif-rl-sol") << "Adding solution " << v + << " to unif candidate " << c << "\n"; sols.push_back(v); } } @@ -280,12 +320,18 @@ Node SygusUnifRl::constructSol(Node f, Node e, NodeRole nrole, int ind) // is there a decision tree strategy? if (nrole == role_equal) { - std::map::iterator itd = d_enum_to_dt.find(e); - if (itd != d_enum_to_dt.end()) + std::map::iterator itd = d_stratpt_to_dt.find(e); + if (itd != d_stratpt_to_dt.end()) { indent("sygus-unif-sol", ind); - Trace("sygus-unif-sol") - << "...it has a decision tree strategy." << std::endl; + Trace("sygus-unif-sol") << "...it has a decision tree strategy.\n"; + if (itd->second.isSeparated()) + { + Trace("sygus-unif-sol") + << "...... points are separated and I have for root enum the value " + << d_parent->getModelValue(e) << "\n"; + return d_parent->getModelValue(e); + } } } @@ -301,13 +347,13 @@ void SygusUnifRl::registerStrategy(Node f) { if (Trace.isOn("sygus-unif-rl-strat")) { - Trace("sygus-unif-rl-strat") - << "Strategy for " << f << " is : " << std::endl; + Trace("sygus-unif-rl-strat") << "Strategy for " << f + << " is : " << std::endl; d_strategy[f].debugPrint("sygus-unif-rl-strat"); } Trace("sygus-unif-rl-strat") << "Register..." << std::endl; Node e = d_strategy[f].getRootEnumerator(); - std::map > visited; + std::map> visited; registerStrategyNode(f, e, role_equal, visited); } @@ -315,7 +361,7 @@ void SygusUnifRl::registerStrategyNode( Node f, Node e, NodeRole nrole, - std::map >& visited) + std::map>& visited) { Trace("sygus-unif-rl-strat") << " register node " << e << std::endl; if (visited[e].find(nrole) != visited[e].end()) @@ -367,11 +413,111 @@ void SygusUnifRl::registerConditionalEnumerator(Node f, Node e, Node cond) == d_cond_enums.end()) { d_cond_enums.push_back(cond); + d_cand_cenums[f].push_back(cond); // register the conditional enumerator d_tds->registerEnumerator(cond, f, d_parent, true); + d_cenum_to_stratpt[cond].clear(); + } + // register that this strategy node has a decision tree construction + d_stratpt_to_dt[e].initialize(cond, this, &d_strategy[f]); + // associate conditional enumerator with strategy node + d_cenum_to_stratpt[cond].push_back(e); +} + +void SygusUnifRl::DecisionTreeInfo::initialize(Node cond_enum, + SygusUnifRl* unif, + SygusUnifStrategy* strategy) +{ + d_cond_enum = cond_enum; + d_unif = unif; + d_strategy = strategy; + // Retrieve template + EnumInfo& eiv = d_strategy->getEnumInfo(d_cond_enum); + d_template = NodePair(eiv.d_template, eiv.d_template_arg); + // Initialize classifier + d_pt_sep.initialize(this); +} + +void SygusUnifRl::DecisionTreeInfo::addPoint(Node f) +{ + d_pt_sep.d_trie.add(f, &d_pt_sep, d_conds.size()); +} + +void SygusUnifRl::DecisionTreeInfo::addCondValue(Node condv) +{ + d_conds.push_back(condv); + d_pt_sep.d_trie.addClassifier(&d_pt_sep, d_conds.size() - 1); +} + +bool SygusUnifRl::DecisionTreeInfo::isSeparated() +{ + for (const std::pair>& rep_to_class : + d_pt_sep.d_trie.d_rep_to_class) + { + Assert(!rep_to_class.second.empty()); + Node v = rep_to_class.second[0]; + unsigned i, size = rep_to_class.second.size(); + for (i = 1; i < size; ++i) + { + Node vi = d_unif->d_parent->getModelValue(rep_to_class.second[i]); + if (v != vi) + { + Trace("sygus-unif-rl-dt") << "...in sep class heads with diff values: " + << rep_to_class.second[0] << " and " + << rep_to_class.second[i] << "\n"; + break; + } + } + // Heads with different model values + if (i != size) + { + return false; + } + } + return true; +} + +void SygusUnifRl::DecisionTreeInfo::PointSeparator::initialize( + DecisionTreeInfo* dt) +{ + d_dt = dt; +} + +Node SygusUnifRl::DecisionTreeInfo::PointSeparator::evaluate(Node n, + unsigned index) +{ + Assert(index < d_dt->d_conds.size()); + // Retrieve respective built_in condition + Node cond = d_dt->d_conds[index]; + TypeNode tn = cond.getType(); + Node builtin_cond = d_dt->d_unif->d_tds->sygusToBuiltin(cond, tn); + // Retrieve evaluation point + Assert(d_dt->d_unif->d_hd_to_pt.find(n) != d_dt->d_unif->d_hd_to_pt.end()); + std::vector pt = d_dt->d_unif->d_hd_to_pt[n]; + // compute the result + Node res = d_dt->d_unif->d_tds->evaluateBuiltin(tn, builtin_cond, pt); + if (Trace.isOn("sygus-unif-rl-sep")) + { + Trace("sygus-unif-rl-sep") << "...got res = " << res << " from cond " + << builtin_cond << " on pt " << n << " ( "; + for (const Node& pti : pt) + { + Trace("sygus-unif-rl-sep") << pti << " "; + } + Trace("sygus-unif-rl-sep") << ")\n"; + } + // If condition is templated, recompute result accordingly + Node templ = d_dt->d_template.first; + TNode templ_var = d_dt->d_template.second; + if (!templ.isNull()) + { + res = templ.substitute(templ_var, res); + res = Rewriter::rewrite(res); + Trace("sygus-unif-rl-sep") << "...after template res = " << res + << std::endl; } - // register that this enumerator has a decision tree construction - d_enum_to_dt[e].d_cond_enum = cond; + Assert(res.isConst()); + return res; } } /* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.h b/src/theory/quantifiers/sygus/sygus_unif_rl.h index 29c67aa81..d618876da 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_rl.h +++ b/src/theory/quantifiers/sygus/sygus_unif_rl.h @@ -2,7 +2,7 @@ /*! \file sygus_unif_rl.h ** \verbatim ** Top contributors (to current version): - ** Haniel Barbosa + ** Haniel Barbosa, Andrew Reynolds ** This file is part of the CVC4 project. ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. @@ -20,6 +20,7 @@ #include #include "theory/quantifiers/sygus/sygus_unif.h" +#include "theory/quantifiers/lazy_trie.h" #include "theory/quantifiers_engine.h" namespace CVC4 { @@ -31,6 +32,7 @@ using BoolNodePairHashFunction = PairHashFunction; using BoolNodePairMap = std::unordered_map; +using NodePair = std::pair; class CegConjecture; @@ -82,20 +84,6 @@ class SygusUnifRl : public SygusUnif CegConjecture* d_parent; /* Functions-to-synthesize (a.k.a. candidates) with unification strategies */ std::unordered_set d_unif_candidates; - /** - * This class stores information regarding an enumerator, including: a - * database of values that have been enumerated for this enumerator. - */ - class EnumCache - { - public: - EnumCache() {} - ~EnumCache() {} - /** Values that have been enumerated for this enumerator */ - std::vector d_enum_vals; - }; - /** maps enumerators to the information above */ - std::map d_ecache; /** construct sol */ Node constructSol(Node f, Node e, NodeRole nrole, int ind) override; /** collects data from refinement lemmas to drive solution construction @@ -111,16 +99,20 @@ class SygusUnifRl : public SygusUnif Purification -------------------------------------------------------------- */ - /* Maps unif candidates to heads of their evaluation points */ + /** + * maps heads of applications of a unif function-to-synthesize to their tuple + * of arguments (which constitute a "data point" aka an "evaluation point") + */ + std::map> d_hd_to_pt; + /** maps unif candidates to heads of their evaluation points */ std::map> d_cand_to_eval_hds; /** - * maps applications of the function-to-synthesize to their tuple of arguments - * (which constitute a "data point") */ - std::map> d_app_to_pt; - /** Maps applications of unif functions-to-synthesize to purified symbols*/ + * maps applications of unif functions-to-synthesize to the result of their + * purification */ std::map d_app_to_purified; - /** Maps unif functions-to-synthesize to counters of purified symbols */ - std::map d_purified_count; + /** maps unif functions-to-synthesize to counters of heads of evaluation + * points */ + std::map d_cand_to_hd_count; /** * This is called on the refinement lemma and will rewrite applications of * functions-to-synthesize to their respective purified form, i.e. such that @@ -136,10 +128,10 @@ class SygusUnifRl : public SygusUnif * * When the traversal encounters an application of a unification * function-to-synthesize it will proceed to ensure that the arguments of that - * function application are constants (the ensureConst becomes "true"). If an + * function application are constants (ensureConst becomes "true"). If an * applicatin of a non-unif function-to-synthesize is reached, the requirement - * is lifted (the ensureConst becomes "false"). This avoides introducing - * spurious equalities in model_guards. + * is lifted (ensureConst becomes "false"). This avoides introducing spurious + * equalities in model_guards. * * For example if "f" is being synthesized with a unification strategy and "g" * is not then the application @@ -152,7 +144,8 @@ class SygusUnifRl : public SygusUnif * would be purified into * g(0) = c1 ^ f1(c1) = c2 => f2(+(0,c2)) * - * This function also populates the maps for point enumerators + * This function also populates the maps between candidates, heads and + * evaluation points */ Node purifyLemma(Node n, bool ensureConst, @@ -170,14 +163,71 @@ class SygusUnifRl : public SygusUnif class DecisionTreeInfo { public: + DecisionTreeInfo() {} + ~DecisionTreeInfo() {} + /** initializes this class */ + void initialize(Node cond_enum, + SygusUnifRl* unif, + SygusUnifStrategy* strategy); + /** adds the respective evaluation point of the head f */ + void addPoint(Node f); + /** adds a condition value to the pool of condition values */ + void addCondValue(Node condv); + /** whether all points that must be separated are separated **/ + bool isSeparated(); + /** reference to parent unif util */ + SygusUnifRl* d_unif; + /** enumerator template (if no templates, nodes in pair are Node::null()) */ + NodePair d_template; + /** enumerated condition values */ + std::vector d_conds; + + private: + /** + * reference to infered strategy for the function-to-synthesize this DT is + * associated with + */ + SygusUnifStrategy* d_strategy; /** * The enumerator in the strategy tree that stores conditions of the * decision tree. */ Node d_cond_enum; + /** Classifies evaluation points according to enumerated condition values + * + * Maintains the invariant that points evaluated in the same way in the + * current condition values are kept in the same "separation class." + */ + class PointSeparator : public LazyTrieEvaluator + { + public: + /** initializes this class */ + void initialize(DecisionTreeInfo* dt); + /** + * evaluates the respective evaluation point of the head n on the index-th + * condition + */ + Node evaluate(Node n, unsigned index) override; + + /** the lazy trie for building the separation classes */ + LazyTrieMulti d_trie; + + private: + /** reference to parent unif util */ + DecisionTreeInfo* d_dt; + }; + /** + * Utility for determining how evaluation points are separated by currently + * enumerated condiotion values + */ + PointSeparator d_pt_sep; }; - /** map from enumerators in the strategy trees to the above data */ - std::map d_enum_to_dt; + /** maps strategy points in the strategy tree to the above data */ + std::map d_stratpt_to_dt; + /** maps conditional enumerators to strategy points in which they occur */ + std::map> d_cenum_to_stratpt; + /** maps unif candidates to their conditional enumerators */ + std::map> d_cand_cenums; /** all conditional enumerators */ std::vector d_cond_enums; /** register strategy