diff options
Diffstat (limited to 'src/theory/quantifiers/sygus/sygus_unif_rl.cpp')
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_unif_rl.cpp | 150 |
1 files changed, 131 insertions, 19 deletions
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 */ |