summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/sygus/sygus_unif_rl.cpp')
-rw-r--r--src/theory/quantifiers/sygus/sygus_unif_rl.cpp150
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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback