diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-05-03 21:11:18 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-05-03 21:11:18 -0500 |
commit | 3fe18c9d3b15e1c4a7bf23d54bf92e2ae27c6a80 (patch) | |
tree | f74e2f7091c4b91dced5edfc410582568095c2f8 /src/theory | |
parent | 09f164674497e70044cc7759b00c6477db90b7be (diff) |
Initialize cegis unif strategy (#1861)
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/quantifiers/sygus/cegis_unif.cpp | 20 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_unif.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_unif_io.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_unif_rl.cpp | 150 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_unif_rl.h | 46 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_unif_strat.cpp | 271 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_unif_strat.h | 70 |
7 files changed, 407 insertions, 154 deletions
diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp index ee8fb6f12..cc477fa62 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.cpp +++ b/src/theory/quantifiers/sygus/cegis_unif.cpp @@ -14,7 +14,9 @@ #include "theory/quantifiers/sygus/cegis_unif.h" +#include "options/base_options.h" #include "options/quantifiers_options.h" +#include "printer/printer.h" #include "theory/quantifiers/sygus/ce_guided_conjecture.h" #include "theory/quantifiers/sygus/sygus_unif_rl.h" #include "theory/quantifiers/sygus/term_database_sygus.h" @@ -55,6 +57,12 @@ bool CegisUnif::initialize(Node n, unif_candidates.push_back(c); } } + for (const Node& e : d_cond_enums) + { + Node g = d_tds->getActiveGuardForEnumerator(e); + Assert(!g.isNull()); + d_enum_to_active_guard[e] = g; + } // initialize the enumeration manager d_u_enum_manager.initialize(unif_candidates); return true; @@ -73,6 +81,8 @@ void CegisUnif::getTermList(const std::vector<Node>& candidates, Valuation& valuation = d_qe->getValuation(); for (const Node& e : d_cond_enums) { + 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 @@ -109,8 +119,14 @@ bool CegisUnif::constructCandidates(const std::vector<Node>& enums, { continue; } - Trace("cegis-unif-enum") << " " << enums[i] << " -> " << enum_values[i] - << std::endl; + if (Trace.isOn("cegis-unif-enum")) + { + Trace("cegis-unif-enum") << " " << enums[i] << " -> "; + std::stringstream ss; + Printer::getPrinter(options::outputLanguage()) + ->toStreamSygus(ss, enum_values[i]); + Trace("cegis-unif-enum") << ss.str() << std::endl; + } unsigned sz = d_tds->getSygusTermSize(enum_values[i]); if (i == 0 || sz < min_term_size) { diff --git a/src/theory/quantifiers/sygus/sygus_unif.cpp b/src/theory/quantifiers/sygus/sygus_unif.cpp index dc927388e..23b04aa4d 100644 --- a/src/theory/quantifiers/sygus/sygus_unif.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif.cpp @@ -41,7 +41,7 @@ void SygusUnif::initialize(QuantifiersEngine* qe, { d_candidates.push_back(f); // initialize the strategy - d_strategy[f].initialize(qe, f, enums, lemmas); + d_strategy[f].initialize(qe, f, enums); } } diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.cpp b/src/theory/quantifiers/sygus/sygus_unif_io.cpp index eb607d2c3..8f2038d31 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_io.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_io.cpp @@ -477,6 +477,8 @@ void SygusUnifIo::initialize(QuantifiersEngine* qe, d_ecache.clear(); d_candidate = funs[0]; SygusUnif::initialize(qe, funs, enums, lemmas); + // learn redundant operators based on the strategy + d_strategy[d_candidate].staticLearnRedundantOps(lemmas); } void SygusUnifIo::addExample(const std::vector<Node>& input, Node output) diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp index 3b7cef4b9..2cf751927 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp @@ -31,11 +31,17 @@ void SygusUnifRl::initialize(QuantifiersEngine* qe, std::vector<Node>& lemmas) { d_ecache.clear(); - d_cand_to_cond_enum.clear(); d_cand_to_pt_enum.clear(); - /* TODO populate d_unif_candidates and remove lemmas cleaning */ - SygusUnif::initialize(qe, funs, enums, lemmas); - lemmas.clear(); + // initialize + std::vector<Node> all_enums; + SygusUnif::initialize(qe, funs, all_enums, lemmas); + // based on the strategy inferred for each function, determine if we are + // using a unification strategy that is compatible our approach. + for (const Node& f : funs) + { + registerStrategy(f); + } + enums.insert(enums.end(), d_cond_enums.begin(), d_cond_enums.end()); /* Copy candidates and check whether CegisUnif for any of them */ for (const Node& c : d_unif_candidates) { @@ -73,23 +79,28 @@ Node SygusUnifRl::purifyLemma(Node n, /* Recurse */ unsigned size = n.getNumChildren(); Kind k = n.getKind(); - /* Whether application of a function-to-synthesize */ - bool fapp = k == APPLY_UF && size > 0; - Assert(std::find(d_candidates.begin(), d_candidates.end(), n[0]) - == d_candidates.end()); - /* Whether application of a (non-)unification function-to-synthesize */ - bool u_fapp = fapp && usingUnif(n[0]); - bool nu_fapp = fapp && !usingUnif(n[0]); /* We retrive model value now because purified node may not have a value */ Node nv = n; - /* get model value of non-top level applications of functions-to-synthesize - occurring under a unification function-to-synthesize */ - if (ensureConst && fapp) + /* Whether application of a function-to-synthesize */ + bool fapp = k == APPLY_UF && size > 0; + bool u_fapp = false; + bool nu_fapp = false; + if (fapp) { - nv = d_parent->getModelValue(n); - Assert(n != nv); - Trace("sygus-unif-rl-purify") << "PurifyLemma : model value for " << n - << " is " << nv << "\n"; + Assert(std::find(d_candidates.begin(), d_candidates.end(), n[0]) + != d_candidates.end()); + /* 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 */ + if (ensureConst) + { + nv = d_parent->getModelValue(n); + Assert(n != nv); + Trace("sygus-unif-rl-purify") + << "PurifyLemma : model value for " << n << " is " << nv << "\n"; + } } /* Travese to purify */ bool childChanged = false; @@ -210,6 +221,7 @@ void SygusUnifRl::initializeConstructSol() {} void SygusUnifRl::initializeConstructSolFor(Node f) {} bool SygusUnifRl::constructSolution(std::vector<Node>& sols) { + initializeConstructSol(); for (const Node& c : d_candidates) { if (!usingUnif(c)) @@ -221,7 +233,16 @@ bool SygusUnifRl::constructSolution(std::vector<Node>& sols) } else { - return false; + 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 true; @@ -229,6 +250,20 @@ bool SygusUnifRl::constructSolution(std::vector<Node>& sols) Node SygusUnifRl::constructSol(Node f, Node e, NodeRole nrole, int ind) { + indent("sygus-unif-sol", ind); + Trace("sygus-unif-sol") << "ConstructSol: SygusRL : " << e << std::endl; + // is there a decision tree strategy? + if (nrole == role_equal) + { + std::map<Node, DecisionTreeInfo>::iterator itd = d_enum_to_dt.find(e); + if (itd != d_enum_to_dt.end()) + { + indent("sygus-unif-sol", ind); + Trace("sygus-unif-sol") + << "...it has a decision tree strategy." << std::endl; + } + } + return Node::null(); } @@ -237,6 +272,83 @@ bool SygusUnifRl::usingUnif(Node f) return d_unif_candidates.find(f) != d_unif_candidates.end(); } +void SygusUnifRl::registerStrategy(Node f) +{ + if (Trace.isOn("sygus-unif-rl-strat")) + { + 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<Node, std::map<NodeRole, bool> > visited; + registerStrategyNode(f, e, role_equal, visited); +} + +void SygusUnifRl::registerStrategyNode( + Node f, + Node e, + NodeRole nrole, + std::map<Node, std::map<NodeRole, bool> >& visited) +{ + Trace("sygus-unif-rl-strat") << " register node " << e << std::endl; + if (visited[e].find(nrole) != visited[e].end()) + { + return; + } + visited[e][nrole] = true; + TypeNode etn = e.getType(); + EnumTypeInfo& tinfo = d_strategy[f].getEnumTypeInfo(etn); + StrategyNode& snode = tinfo.getStrategyNode(nrole); + for (unsigned j = 0, size = snode.d_strats.size(); j < size; j++) + { + EnumTypeInfoStrat* etis = snode.d_strats[j]; + StrategyType strat = etis->d_this; + // is this a simple recursive ITE strategy? + if (strat == strat_ITE && nrole == role_equal) + { + bool success = true; + for (unsigned c = 1; c <= 2; c++) + { + std::pair<Node, NodeRole> child = etis->d_cenum[c]; + if (child.first != e || child.second != nrole) + { + success = false; + break; + } + } + if (success) + { + Node cond = etis->d_cenum[0].first; + Assert(etis->d_cenum[0].second == role_ite_condition); + Trace("sygus-unif-rl-strat") + << " ...detected recursive ITE strategy, condition enumerator : " + << cond << std::endl; + // indicate that we will be enumerating values for cond + registerConditionalEnumerator(f, e, cond); + } + } + // TODO: recurse? for (std::pair<Node, NodeRole>& cec : etis->d_cenum) + } +} + +void SygusUnifRl::registerConditionalEnumerator(Node f, Node e, Node cond) +{ + // we will do unification for this candidate + d_unif_candidates.insert(f); + // add to the list of all conditional enumerators + if (std::find(d_cond_enums.begin(), d_cond_enums.end(), cond) + == d_cond_enums.end()) + { + d_cond_enums.push_back(cond); + // register the conditional enumerator + d_tds->registerEnumerator(cond, f, d_parent, true); + } + // register that this enumerator has a decision tree construction + d_enum_to_dt[e].d_cond_enum = cond; +} + } /* CVC4::theory::quantifiers namespace */ } /* CVC4::theory namespace */ } /* CVC4 namespace */ diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.h b/src/theory/quantifiers/sygus/sygus_unif_rl.h index dc1b14641..b8ead4986 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_rl.h +++ b/src/theory/quantifiers/sygus/sygus_unif_rl.h @@ -73,8 +73,6 @@ class SygusUnifRl : public SygusUnif CegConjecture* d_parent; /* Functions-to-synthesize (a.k.a. candidates) with unification strategies */ std::unordered_set<Node, NodeHashFunction> d_unif_candidates; - /* Maps unif candidates to their conditonal enumerators */ - std::map<Node, Node> d_cand_to_cond_enum; /** * This class stores information regarding an enumerator, including: a * database @@ -151,6 +149,50 @@ class SygusUnifRl : public SygusUnif bool ensureConst, std::vector<Node>& model_guards, BoolNodePairMap& cache); + /* + -------------------------------------------------------------- + Strategy information + -------------------------------------------------------------- + */ + /** + * This class stores the necessary information for building a decision tree + * for a particular node in the strategy tree of a candidate variable f. + */ + class DecisionTreeInfo + { + public: + /** + * The enumerator in the strategy tree that stores conditions of the + * decision tree. + */ + Node d_cond_enum; + }; + /** map from enumerators in the strategy trees to the above data */ + std::map<Node, DecisionTreeInfo> d_enum_to_dt; + /** all conditional enumerators */ + std::vector<Node> d_cond_enums; + /** register strategy + * + * Initialize the above data for the relevant enumerators in the strategy tree + * of candidate variable f. + */ + void registerStrategy(Node f); + /** register strategy node + * + * Called while traversing the strategy tree of f. The arguments e and nrole + * indicate the current node in the tree we are traversing, and visited + * indicates the nodes we have already visited. + */ + void registerStrategyNode(Node f, + Node e, + NodeRole nrole, + std::map<Node, std::map<NodeRole, bool>>& visited); + /** register conditional enumerator + * + * Registers that cond is a conditional enumerator for building a (recursive) + * decision tree at strategy node e within the strategy tree of f. + */ + void registerConditionalEnumerator(Node f, Node e, Node cond); }; } /* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp index 86efffd1f..d3a5d6c23 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp @@ -80,8 +80,7 @@ std::ostream& operator<<(std::ostream& os, StrategyType st) void SygusUnifStrategy::initialize(QuantifiersEngine* qe, Node f, - std::vector<Node>& enums, - std::vector<Node>& lemmas) + std::vector<Node>& enums) { Assert(d_candidate.isNull()); d_candidate = f; @@ -92,8 +91,10 @@ void SygusUnifStrategy::initialize(QuantifiersEngine* qe, collectEnumeratorTypes(d_root, role_equal); // add the enumerators enums.insert(enums.end(), d_esym_list.begin(), d_esym_list.end()); - // learn redundant ops - staticLearnRedundantOps(lemmas); + // finish the initialization of the strategy + // this computes if each node is conditional + std::map<Node, std::map<NodeRole, bool> > visited; + finishInit(getRootEnumerator(), role_equal, visited, false); } void SygusUnifStrategy::initializeType(TypeNode tn) @@ -101,10 +102,13 @@ void SygusUnifStrategy::initializeType(TypeNode tn) d_tinfo[tn].d_this_type = tn; } -Node SygusUnifStrategy::getRootEnumerator() +Node SygusUnifStrategy::getRootEnumerator() const { - std::map<EnumRole, Node>::iterator it = d_tinfo[d_root].d_enum.find(enum_io); - Assert(it != d_tinfo[d_root].d_enum.end()); + std::map<TypeNode, EnumTypeInfo>::const_iterator itt = d_tinfo.find(d_root); + Assert(itt != d_tinfo.end()); + std::map<EnumRole, Node>::const_iterator it = + itt->second.d_enum.find(enum_io); + Assert(it != itt->second.d_enum.end()); return it->second; } @@ -702,10 +706,10 @@ void SygusUnifStrategy::staticLearnRedundantOps(std::vector<Node>& lemmas) Trace("sygus-unif") << std::endl; Trace("sygus-unif") << "Strategy for candidate " << d_candidate << " is : " << std::endl; + debugPrint("sygus-unif"); std::map<Node, std::map<NodeRole, bool> > visited; std::map<Node, std::map<unsigned, bool> > needs_cons; - staticLearnRedundantOps( - getRootEnumerator(), role_equal, visited, needs_cons, 0, false); + staticLearnRedundantOps(getRootEnumerator(), role_equal, visited, needs_cons); // now, check the needs_cons map for (std::pair<const Node, std::map<unsigned, bool> >& nce : needs_cons) { @@ -730,124 +734,181 @@ void SygusUnifStrategy::staticLearnRedundantOps(std::vector<Node>& lemmas) } } +void SygusUnifStrategy::debugPrint(const char* c) +{ + if (Trace.isOn(c)) + { + std::map<Node, std::map<NodeRole, bool> > visited; + debugPrint(c, getRootEnumerator(), role_equal, visited, 0); + } +} + void SygusUnifStrategy::staticLearnRedundantOps( Node e, NodeRole nrole, std::map<Node, std::map<NodeRole, bool> >& visited, - std::map<Node, std::map<unsigned, bool> >& needs_cons, - int ind, - bool isCond) + std::map<Node, std::map<unsigned, bool> >& needs_cons) { - std::map<Node, EnumInfo>::iterator itn = d_einfo.find(e); - Assert(itn != d_einfo.end()); - - if (visited[e].find(nrole) == visited[e].end() - || (isCond && !itn->second.isConditional())) + if (visited[e].find(nrole) != visited[e].end()) + { + return; + } + visited[e][nrole] = true; + EnumInfo& ei = getEnumInfo(e); + if (ei.isTemplated()) { - visited[e][nrole] = true; - // if conditional - if (isCond) + return; + } + TypeNode etn = e.getType(); + EnumTypeInfo& tinfo = getEnumTypeInfo(etn); + StrategyNode& snode = tinfo.getStrategyNode(nrole); + if (snode.d_strats.empty()) + { + return; + } + std::map<unsigned, bool> needs_cons_curr; + // various strategies + for (unsigned j = 0, size = snode.d_strats.size(); j < size; j++) + { + EnumTypeInfoStrat* etis = snode.d_strats[j]; + int cindex = Datatype::indexOf(etis->d_cons.toExpr()); + Assert(cindex != -1); + needs_cons_curr[static_cast<unsigned>(cindex)] = false; + for (std::pair<Node, NodeRole>& cec : etis->d_cenum) { - itn->second.setConditional(); + staticLearnRedundantOps(cec.first, cec.second, visited, needs_cons); } - indent("sygus-unif", ind); - Trace("sygus-unif") << e << " :: node role : " << nrole; - Trace("sygus-unif") - << ", type : " - << ((DatatypeType)e.getType().toType()).getDatatype().getName(); - if (isCond) + } + // get the master enumerator for the type of this enumerator + std::map<TypeNode, Node>::iterator itse = d_master_enum.find(etn); + if (itse == d_master_enum.end()) + { + return; + } + Node em = itse->second; + Assert(!em.isNull()); + // get the current datatype + const Datatype& dt = static_cast<DatatypeType>(etn.toType()).getDatatype(); + // all constructors that are not a part of a strategy are needed + for (unsigned j = 0, size = dt.getNumConstructors(); j < size; j++) + { + if (needs_cons_curr.find(j) == needs_cons_curr.end()) { - Trace("sygus-unif") << ", conditional"; + needs_cons_curr[j] = true; } - Trace("sygus-unif") << ", enum role : " << itn->second.getRole(); - - if (itn->second.isTemplated()) + } + // update the constructors that the master enumerator needs + if (needs_cons.find(em) == needs_cons.end()) + { + needs_cons[em] = needs_cons_curr; + } + else + { + for (unsigned j = 0, size = dt.getNumConstructors(); j < size; j++) { - Trace("sygus-unif") << ", templated : (lambda " - << itn->second.d_template_arg << " " - << itn->second.d_template << ")" << std::endl; + needs_cons[em][j] = needs_cons[em][j] || needs_cons_curr[j]; } - else + } +} + +void SygusUnifStrategy::finishInit( + Node e, + NodeRole nrole, + std::map<Node, std::map<NodeRole, bool> >& visited, + bool isCond) +{ + EnumInfo& ei = getEnumInfo(e); + if (visited[e].find(nrole) != visited[e].end() + && (!isCond || ei.isConditional())) + { + return; + } + visited[e][nrole] = true; + // set conditional + if (isCond) + { + ei.setConditional(); + } + if (ei.isTemplated()) + { + return; + } + TypeNode etn = e.getType(); + EnumTypeInfo& tinfo = getEnumTypeInfo(etn); + StrategyNode& snode = tinfo.getStrategyNode(nrole); + for (unsigned j = 0, size = snode.d_strats.size(); j < size; j++) + { + EnumTypeInfoStrat* etis = snode.d_strats[j]; + StrategyType strat = etis->d_this; + bool newIsCond = isCond || strat == strat_ITE; + for (std::pair<Node, NodeRole>& cec : etis->d_cenum) { - Trace("sygus-unif") << std::endl; - TypeNode etn = e.getType(); + finishInit(cec.first, cec.second, visited, newIsCond); + } + } +} - // enumerator type info - std::map<TypeNode, EnumTypeInfo>::iterator itt = d_tinfo.find(etn); - Assert(itt != d_tinfo.end()); - EnumTypeInfo& tinfo = itt->second; +void SygusUnifStrategy::debugPrint( + const char* c, + Node e, + NodeRole nrole, + std::map<Node, std::map<NodeRole, bool> >& visited, + int ind) +{ + if (visited[e].find(nrole) != visited[e].end()) + { + indent(c, ind); + Trace(c) << e << " :: node role : " << nrole << std::endl; + return; + } + visited[e][nrole] = true; + EnumInfo& ei = getEnumInfo(e); - // strategy info - std::map<NodeRole, StrategyNode>::iterator itsn = - tinfo.d_snodes.find(nrole); - Assert(itsn != tinfo.d_snodes.end()); - StrategyNode& snode = itsn->second; + TypeNode etn = e.getType(); - if (snode.d_strats.empty()) - { - return; - } - std::map<unsigned, bool> needs_cons_curr; - // various strategies - for (unsigned j = 0, size = snode.d_strats.size(); j < size; j++) - { - EnumTypeInfoStrat* etis = snode.d_strats[j]; - StrategyType strat = etis->d_this; - bool newIsCond = isCond || strat == strat_ITE; - indent("sygus-unif", ind + 1); - Trace("sygus-unif") << "Strategy : " << strat - << ", from cons : " << etis->d_cons << std::endl; - int cindex = Datatype::indexOf(etis->d_cons.toExpr()); - Assert(cindex != -1); - needs_cons_curr[static_cast<unsigned>(cindex)] = false; - for (std::pair<Node, NodeRole>& cec : etis->d_cenum) - { - // recurse - staticLearnRedundantOps( - cec.first, cec.second, visited, needs_cons, ind + 2, newIsCond); - } - } - // get the master enumerator for the type of this enumerator - std::map<TypeNode, Node>::iterator itse = d_master_enum.find(etn); - if (itse == d_master_enum.end()) - { - return; - } - Node em = itse->second; - Assert(!em.isNull()); - // get the current datatype - const Datatype& dt = - static_cast<DatatypeType>(etn.toType()).getDatatype(); - // all constructors that are not a part of a strategy are needed - for (unsigned j = 0, size = dt.getNumConstructors(); j < size; j++) - { - if (needs_cons_curr.find(j) == needs_cons_curr.end()) - { - needs_cons_curr[j] = true; - } - } - // update the constructors that the master enumerator needs - if (needs_cons.find(em) == needs_cons.end()) - { - needs_cons[em] = needs_cons_curr; - } - else - { - for (unsigned j = 0, size = dt.getNumConstructors(); j < size; j++) - { - needs_cons[em][j] = needs_cons[em][j] || needs_cons_curr[j]; - } - } - } + indent(c, ind); + Trace(c) << e << " :: node role : " << nrole; + Trace(c) << ", type : " + << static_cast<DatatypeType>(etn.toType()).getDatatype().getName(); + if (ei.isConditional()) + { + Trace(c) << ", conditional"; } - else + Trace(c) << ", enum role : " << ei.getRole(); + + if (ei.isTemplated()) + { + Trace(c) << ", templated : (lambda " << ei.d_template_arg << " " + << ei.d_template << ")"; + } + Trace(c) << std::endl; + + EnumTypeInfo& tinfo = getEnumTypeInfo(etn); + StrategyNode& snode = tinfo.getStrategyNode(nrole); + for (unsigned j = 0, size = snode.d_strats.size(); j < size; j++) { - indent("sygus-unif", ind); - Trace("sygus-unif") << e << " :: node role : " << nrole << std::endl; + EnumTypeInfoStrat* etis = snode.d_strats[j]; + StrategyType strat = etis->d_this; + indent(c, ind + 1); + Trace(c) << "Strategy : " << strat << ", from cons : " << etis->d_cons + << std::endl; + for (std::pair<Node, NodeRole>& cec : etis->d_cenum) + { + // recurse + debugPrint(c, cec.first, cec.second, visited, ind + 2); + } } } void EnumInfo::initialize(EnumRole role) { d_role = role; } + +StrategyNode& EnumTypeInfo::getStrategyNode(NodeRole nrole) +{ + std::map<NodeRole, StrategyNode>::iterator it = d_snodes.find(nrole); + Assert(it != d_snodes.end()); + return it->second; +} + bool EnumTypeInfoStrat::isValid(UnifContext& x) { if ((x.getCurrentRole() == role_string_prefix diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.h b/src/theory/quantifiers/sygus/sygus_unif_strat.h index 0ab7ea1d6..8f9adefb9 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_strat.h +++ b/src/theory/quantifiers/sygus/sygus_unif_strat.h @@ -198,6 +198,8 @@ class EnumTypeInfo std::map<EnumRole, Node> d_enum; /** map from node roles to strategy nodes */ std::map<NodeRole, StrategyNode> d_snodes; + /** get strategy node for node role */ + StrategyNode& getStrategyNode(NodeRole nrole); }; /** represents a strategy for a SyGuS datatype type @@ -253,18 +255,10 @@ class SygusUnifStrategy * * This call constructs a set of enumerators for the relevant subfields of * the grammar of f and adds them to enums. - * - * This also may result in lemmas being added to lemmas, - * which correspond to static symmetry breaking predicates (for example, - * those that exclude ITE from enumerators whose role is enum_io when the - * strategy is ITE_strat). */ - void initialize(QuantifiersEngine* qe, - Node f, - std::vector<Node>& enums, - std::vector<Node>& lemmas); + void initialize(QuantifiersEngine* qe, Node f, std::vector<Node>& enums); /** Get the root enumerator for this class */ - Node getRootEnumerator(); + Node getRootEnumerator() const; /** * Get the enumerator info for enumerator e, where e must be an enumerator * initialized by this class (in enums after a call to initialize). @@ -276,6 +270,20 @@ class SygusUnifStrategy */ EnumTypeInfo& getEnumTypeInfo(TypeNode tn); + /** static learn redundant operators + * + * This learns static lemmas for pruning enumerative space based on the + * strategy for the function-to-synthesize of this class, and stores these + * into lemmas. + * + * These may correspond to static symmetry breaking predicates (for example, + * those that exclude ITE from enumerators whose role is enum_io when the + * strategy is ITE_strat). + */ + void staticLearnRedundantOps(std::vector<Node>& lemmas); + /** debug print this strategy on Trace c */ + void debugPrint(const char* c); + private: /** reference to quantifier engine */ QuantifiersEngine* d_qe; @@ -332,13 +340,6 @@ class SygusUnifStrategy Node n, std::map<Node, unsigned>& templ_var_index, std::map<unsigned, unsigned>& templ_injection); - /** static learn redundant operators - * - * This learns static lemmas for pruning enumerative space based on the - * strategy for the function-to-synthesize of this class, and stores these - * into lemmas. - */ - void staticLearnRedundantOps(std::vector<Node>& lemmas); /** helper for static learn redundant operators * * (e, nrole) specify the strategy node in the graph we are currently @@ -346,19 +347,38 @@ class SygusUnifStrategy * * This method builds the mapping needs_cons, which maps (master) enumerators * to a map from the constructors that it needs. - * - * ind is the depth in the strategy graph we are at (for debugging). - * - * isCond is whether the current enumerator is conditional (beneath a - * conditional of an strat_ITE strategy). */ void staticLearnRedundantOps( Node e, NodeRole nrole, std::map<Node, std::map<NodeRole, bool> >& visited, - std::map<Node, std::map<unsigned, bool> >& needs_cons, - int ind, - bool isCond); + std::map<Node, std::map<unsigned, bool> >& needs_cons); + /** finish initialization of the strategy tree + * + * (e, nrole) specify the strategy node in the graph we are currently + * analyzing, visited stores the nodes we have already visited. + * + * isCond is whether the current enumerator is conditional (beneath a + * conditional of an strat_ITE strategy). + */ + void finishInit(Node e, + NodeRole nrole, + std::map<Node, std::map<NodeRole, bool> >& visited, + bool isCond); + /** helper for debug print + * + * Prints the node e with role nrole on Trace(c). + * + * (e, nrole) specify the strategy node in the graph we are currently + * analyzing, visited stores the nodes we have already visited. + * + * ind is the current level of indentation (for debugging) + */ + void debugPrint(const char* c, + Node e, + NodeRole nrole, + std::map<Node, std::map<NodeRole, bool> >& visited, + int ind); //------------------------------ end strategy registration }; |