theory/quantifiers/sygus/sygus_process_conj.h \
theory/quantifiers/sygus/sygus_unif.cpp \
theory/quantifiers/sygus/sygus_unif.h \
+ theory/quantifiers/sygus/sygus_unif_io.cpp \
+ theory/quantifiers/sygus/sygus_unif_io.h \
theory/quantifiers/sygus/sygus_unif_strat.cpp \
theory/quantifiers/sygus/sygus_unif_strat.h \
theory/quantifiers/sygus/term_database_sygus.cpp \
#include "context/cdhashmap.h"
#include "theory/quantifiers/sygus/sygus_module.h"
-#include "theory/quantifiers/sygus/sygus_unif.h"
+#include "theory/quantifiers/sygus/sygus_unif_io.h"
namespace CVC4 {
namespace theory {
* the core algorithm (e.g. decision tree learning) that this module relies
* upon.
*/
- std::map<Node, SygusUnif> d_sygus_unif;
+ std::map<Node, SygusUnifIo> d_sygus_unif;
/**
* map from candidates to the list of enumerators that are being used to
* build solutions for that candidate by the above utility.
namespace theory {
namespace quantifiers {
-UnifContext::UnifContext() : d_has_string_pos(role_invalid)
-{
- d_true = NodeManager::currentNM()->mkConst(true);
- d_false = NodeManager::currentNM()->mkConst(false);
-}
-
-bool UnifContext::updateContext(SygusUnif* pbe,
- std::vector<Node>& vals,
- bool pol)
-{
- Assert(d_vals.size() == vals.size());
- bool changed = false;
- Node poln = pol ? d_true : d_false;
- for (unsigned i = 0; i < vals.size(); i++)
- {
- if (vals[i] != poln)
- {
- if (d_vals[i] == d_true)
- {
- d_vals[i] = d_false;
- changed = true;
- }
- }
- }
- if (changed)
- {
- d_visit_role.clear();
- }
- return changed;
-}
-
-bool UnifContext::updateStringPosition(SygusUnif* pbe,
- std::vector<unsigned>& pos)
-{
- Assert(pos.size() == d_str_pos.size());
- bool changed = false;
- for (unsigned i = 0; i < pos.size(); i++)
- {
- if (pos[i] > 0)
- {
- d_str_pos[i] += pos[i];
- changed = true;
- }
- }
- if (changed)
- {
- d_visit_role.clear();
- }
- return changed;
-}
-
-bool UnifContext::isReturnValueModified()
-{
- if (d_has_string_pos != role_invalid)
- {
- return true;
- }
- return false;
-}
-
-void UnifContext::initialize(SygusUnif* pbe)
-{
- Assert(d_vals.empty());
- Assert(d_str_pos.empty());
-
- // initialize with #examples
- unsigned sz = pbe->d_examples.size();
- for (unsigned i = 0; i < sz; i++)
- {
- d_vals.push_back(d_true);
- }
-
- if (!pbe->d_examples_out.empty())
- {
- // output type of the examples
- TypeNode exotn = pbe->d_examples_out[0].getType();
-
- if (exotn.isString())
- {
- for (unsigned i = 0; i < sz; i++)
- {
- d_str_pos.push_back(0);
- }
- }
- }
- d_visit_role.clear();
-}
-
-void UnifContext::getCurrentStrings(SygusUnif* pbe,
- const std::vector<Node>& vals,
- std::vector<String>& ex_vals)
-{
- bool isPrefix = d_has_string_pos == role_string_prefix;
- String dummy;
- for (unsigned i = 0; i < vals.size(); i++)
- {
- if (d_vals[i] == pbe->d_true)
- {
- Assert(vals[i].isConst());
- unsigned pos_value = d_str_pos[i];
- if (pos_value > 0)
- {
- Assert(d_has_string_pos != role_invalid);
- String s = vals[i].getConst<String>();
- Assert(pos_value <= s.size());
- ex_vals.push_back(isPrefix ? s.suffix(s.size() - pos_value)
- : s.prefix(s.size() - pos_value));
- }
- else
- {
- ex_vals.push_back(vals[i].getConst<String>());
- }
- }
- else
- {
- // irrelevant, add dummy
- ex_vals.push_back(dummy);
- }
- }
-}
-
-bool UnifContext::getStringIncrement(SygusUnif* pbe,
- bool isPrefix,
- const std::vector<String>& ex_vals,
- const std::vector<Node>& vals,
- std::vector<unsigned>& inc,
- unsigned& tot)
-{
- for (unsigned j = 0; j < vals.size(); j++)
- {
- unsigned ival = 0;
- if (d_vals[j] == pbe->d_true)
- {
- // example is active in this context
- Assert(vals[j].isConst());
- String mystr = vals[j].getConst<String>();
- ival = mystr.size();
- if (mystr.size() <= ex_vals[j].size())
- {
- if (!(isPrefix ? ex_vals[j].strncmp(mystr, ival)
- : ex_vals[j].rstrncmp(mystr, ival)))
- {
- Trace("sygus-pbe-dt-debug") << "X";
- return false;
- }
- }
- else
- {
- Trace("sygus-pbe-dt-debug") << "X";
- return false;
- }
- }
- Trace("sygus-pbe-dt-debug") << ival;
- tot += ival;
- inc.push_back(ival);
- }
- return true;
-}
-bool UnifContext::isStringSolved(SygusUnif* pbe,
- const std::vector<String>& ex_vals,
- const std::vector<Node>& vals)
-{
- for (unsigned j = 0; j < vals.size(); j++)
- {
- if (d_vals[j] == pbe->d_true)
- {
- // example is active in this context
- Assert(vals[j].isConst());
- String mystr = vals[j].getConst<String>();
- if (ex_vals[j] != mystr)
- {
- return false;
- }
- }
- }
- return true;
-}
-
-// status : 0 : exact, -1 : vals is subset, 1 : vals is superset
-Node SubsumeTrie::addTermInternal(Node t,
- const std::vector<Node>& vals,
- bool pol,
- std::vector<Node>& subsumed,
- bool spol,
- unsigned index,
- int status,
- bool checkExistsOnly,
- bool checkSubsume)
-{
- if (index == vals.size())
- {
- if (status == 0)
- {
- // set the term if checkExistsOnly = false
- if (d_term.isNull() && !checkExistsOnly)
- {
- d_term = t;
- }
- }
- else if (status == 1)
- {
- Assert(checkSubsume);
- // found a subsumed term
- if (!d_term.isNull())
- {
- subsumed.push_back(d_term);
- if (!checkExistsOnly)
- {
- // remove it if checkExistsOnly = false
- d_term = Node::null();
- }
- }
- }
- else
- {
- Assert(!checkExistsOnly && checkSubsume);
- }
- return d_term;
- }
- NodeManager* nm = NodeManager::currentNM();
- // the current value
- Assert(pol || (vals[index].isConst() && vals[index].getType().isBoolean()));
- Node cv = pol ? vals[index] : nm->mkConst(!vals[index].getConst<bool>());
- // if checkExistsOnly = false, check if the current value is subsumed if
- // checkSubsume = true, if so, don't add
- if (!checkExistsOnly && checkSubsume)
- {
- Assert(cv.isConst() && cv.getType().isBoolean());
- std::vector<bool> check_subsumed_by;
- if (status == 0)
- {
- if (!cv.getConst<bool>())
- {
- check_subsumed_by.push_back(spol);
- }
- }
- else if (status == -1)
- {
- check_subsumed_by.push_back(spol);
- if (!cv.getConst<bool>())
- {
- check_subsumed_by.push_back(!spol);
- }
- }
- // check for subsumed nodes
- for (unsigned i = 0, size = check_subsumed_by.size(); i < size; i++)
- {
- bool csbi = check_subsumed_by[i];
- Node csval = nm->mkConst(csbi);
- // check if subsumed
- std::map<Node, SubsumeTrie>::iterator itc = d_children.find(csval);
- if (itc != d_children.end())
- {
- Node ret = itc->second.addTermInternal(t,
- vals,
- pol,
- subsumed,
- spol,
- index + 1,
- -1,
- checkExistsOnly,
- checkSubsume);
- // ret subsumes t
- if (!ret.isNull())
- {
- return ret;
- }
- }
- }
- }
- Node ret;
- std::vector<bool> check_subsume;
- if (status == 0)
- {
- if (checkExistsOnly)
- {
- std::map<Node, SubsumeTrie>::iterator itc = d_children.find(cv);
- if (itc != d_children.end())
- {
- ret = itc->second.addTermInternal(t,
- vals,
- pol,
- subsumed,
- spol,
- index + 1,
- 0,
- checkExistsOnly,
- checkSubsume);
- }
- }
- else
- {
- Assert(spol);
- ret = d_children[cv].addTermInternal(t,
- vals,
- pol,
- subsumed,
- spol,
- index + 1,
- 0,
- checkExistsOnly,
- checkSubsume);
- if (ret != t)
- {
- // we were subsumed by ret, return
- return ret;
- }
- }
- if (checkSubsume)
- {
- Assert(cv.isConst() && cv.getType().isBoolean());
- // check for subsuming
- if (cv.getConst<bool>())
- {
- check_subsume.push_back(!spol);
- }
- }
- }
- else if (status == 1)
- {
- Assert(checkSubsume);
- Assert(cv.isConst() && cv.getType().isBoolean());
- check_subsume.push_back(!spol);
- if (cv.getConst<bool>())
- {
- check_subsume.push_back(spol);
- }
- }
- if (checkSubsume)
- {
- // check for subsumed terms
- for (unsigned i = 0, size = check_subsume.size(); i < size; i++)
- {
- Node csval = nm->mkConst<bool>(check_subsume[i]);
- std::map<Node, SubsumeTrie>::iterator itc = d_children.find(csval);
- if (itc != d_children.end())
- {
- itc->second.addTermInternal(t,
- vals,
- pol,
- subsumed,
- spol,
- index + 1,
- 1,
- checkExistsOnly,
- checkSubsume);
- // clean up
- if (itc->second.isEmpty())
- {
- Assert(!checkExistsOnly);
- d_children.erase(csval);
- }
- }
- }
- }
- return ret;
-}
-
-Node SubsumeTrie::addTerm(Node t,
- const std::vector<Node>& vals,
- bool pol,
- std::vector<Node>& subsumed)
-{
- return addTermInternal(t, vals, pol, subsumed, true, 0, 0, false, true);
-}
-
-Node SubsumeTrie::addCond(Node c, const std::vector<Node>& vals, bool pol)
-{
- std::vector<Node> subsumed;
- return addTermInternal(c, vals, pol, subsumed, true, 0, 0, false, false);
-}
-
-void SubsumeTrie::getSubsumed(const std::vector<Node>& vals,
- bool pol,
- std::vector<Node>& subsumed)
-{
- addTermInternal(Node::null(), vals, pol, subsumed, true, 0, 1, true, true);
-}
-
-void SubsumeTrie::getSubsumedBy(const std::vector<Node>& vals,
- bool pol,
- std::vector<Node>& subsumed_by)
-{
- // flip polarities
- addTermInternal(
- Node::null(), vals, !pol, subsumed_by, false, 0, 1, true, true);
-}
-
-void SubsumeTrie::getLeavesInternal(const std::vector<Node>& vals,
- bool pol,
- std::map<int, std::vector<Node> >& v,
- unsigned index,
- int status)
-{
- if (index == vals.size())
- {
- Assert(!d_term.isNull());
- Assert(std::find(v[status].begin(), v[status].end(), d_term)
- == v[status].end());
- v[status].push_back(d_term);
- }
- else
- {
- Assert(vals[index].isConst() && vals[index].getType().isBoolean());
- bool curr_val_true = vals[index].getConst<bool>() == pol;
- for (std::map<Node, SubsumeTrie>::iterator it = d_children.begin();
- it != d_children.end();
- ++it)
- {
- int new_status = status;
- // if the current value is true
- if (curr_val_true)
- {
- if (status != 0)
- {
- Assert(it->first.isConst() && it->first.getType().isBoolean());
- new_status = (it->first.getConst<bool>() ? 1 : -1);
- if (status != -2 && new_status != status)
- {
- new_status = 0;
- }
- }
- }
- it->second.getLeavesInternal(vals, pol, v, index + 1, new_status);
- }
- }
-}
-
-void SubsumeTrie::getLeaves(const std::vector<Node>& vals,
- bool pol,
- std::map<int, std::vector<Node> >& v)
-{
- getLeavesInternal(vals, pol, v, 0, -2);
-}
-
SygusUnif::SygusUnif()
{
- d_true = NodeManager::currentNM()->mkConst(true);
- d_false = NodeManager::currentNM()->mkConst(false);
}
SygusUnif::~SygusUnif() {}
d_candidate = f;
d_qe = qe;
d_tds = qe->getTermDatabaseSygus();
-
+ // initialize the strategy
d_strategy.initialize(qe, f, enums, lemmas);
}
-void SygusUnif::resetExamples()
-{
- d_examples.clear();
- d_examples_out.clear();
- // also clear information in strategy tree
- // TODO
-}
-
-void SygusUnif::addExample(const std::vector<Node>& input, Node output)
-{
- d_examples.push_back(input);
- d_examples_out.push_back(output);
-}
-
-void SygusUnif::notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas)
-{
- Node c = d_candidate;
- Assert(!d_examples.empty());
- Assert(d_examples.size() == d_examples_out.size());
-
- EnumInfo& ei = d_strategy.getEnumInfo(e);
- // The explanation for why the current value should be excluded in future
- // iterations.
- Node exp_exc;
-
- TypeNode xtn = e.getType();
- Node bv = d_tds->sygusToBuiltin(v, xtn);
- std::vector<Node> base_results;
- // compte the results
- for (unsigned j = 0, size = d_examples.size(); j < size; j++)
- {
- Node res = d_tds->evaluateBuiltin(xtn, bv, d_examples[j]);
- Trace("sygus-pbe-enum-debug")
- << "...got res = " << res << " from " << bv << std::endl;
- base_results.push_back(res);
- }
- // is it excluded for domain-specific reason?
- std::vector<Node> exp_exc_vec;
- if (getExplanationForEnumeratorExclude(e, v, base_results, exp_exc_vec))
- {
- Assert(!exp_exc_vec.empty());
- exp_exc = exp_exc_vec.size() == 1
- ? exp_exc_vec[0]
- : NodeManager::currentNM()->mkNode(AND, exp_exc_vec);
- Trace("sygus-pbe-enum")
- << " ...fail : term is excluded (domain-specific)" << std::endl;
- }
- else
- {
- // notify all slaves
- Assert(!ei.d_enum_slave.empty());
- // explanation for why this value should be excluded
- for (unsigned s = 0; s < ei.d_enum_slave.size(); s++)
- {
- Node xs = ei.d_enum_slave[s];
-
- EnumInfo& eiv = d_strategy.getEnumInfo(xs);
-
- EnumCache& ecv = d_ecache[xs];
-
- Trace("sygus-pbe-enum") << "Process " << xs << " from " << s << std::endl;
- // bool prevIsCover = false;
- if (eiv.getRole() == enum_io)
- {
- Trace("sygus-pbe-enum") << " IO-Eval of ";
- // prevIsCover = eiv.isFeasible();
- }
- else
- {
- Trace("sygus-pbe-enum") << "Evaluation of ";
- }
- Trace("sygus-pbe-enum") << xs << " : ";
- // evaluate all input/output examples
- std::vector<Node> results;
- Node templ = eiv.d_template;
- TNode templ_var = eiv.d_template_arg;
- std::map<Node, bool> cond_vals;
- for (unsigned j = 0, size = base_results.size(); j < size; j++)
- {
- Node res = base_results[j];
- Assert(res.isConst());
- if (!templ.isNull())
- {
- TNode tres = res;
- res = templ.substitute(templ_var, res);
- res = Rewriter::rewrite(res);
- Assert(res.isConst());
- }
- Node resb;
- if (eiv.getRole() == enum_io)
- {
- Node out = d_examples_out[j];
- Assert(out.isConst());
- resb = res == out ? d_true : d_false;
- }
- else
- {
- resb = res;
- }
- cond_vals[resb] = true;
- results.push_back(resb);
- if (Trace.isOn("sygus-pbe-enum"))
- {
- if (resb.getType().isBoolean())
- {
- Trace("sygus-pbe-enum") << (resb == d_true ? "1" : "0");
- }
- else
- {
- Trace("sygus-pbe-enum") << "?";
- }
- }
- }
- bool keep = false;
- if (eiv.getRole() == enum_io)
- {
- // latter is the degenerate case of no examples
- if (cond_vals.find(d_true) != cond_vals.end() || cond_vals.empty())
- {
- // check subsumbed/subsuming
- std::vector<Node> subsume;
- if (cond_vals.find(d_false) == cond_vals.end())
- {
- // it is the entire solution, we are done
- Trace("sygus-pbe-enum")
- << " ...success, full solution added to PBE pool : "
- << d_tds->sygusToBuiltin(v) << std::endl;
- if (!ecv.isSolved())
- {
- ecv.setSolved(v);
- // it subsumes everything
- ecv.d_term_trie.clear();
- ecv.d_term_trie.addTerm(v, results, true, subsume);
- }
- keep = true;
- }
- else
- {
- Node val = ecv.d_term_trie.addTerm(v, results, true, subsume);
- if (val == v)
- {
- Trace("sygus-pbe-enum") << " ...success";
- if (!subsume.empty())
- {
- ecv.d_enum_subsume.insert(
- ecv.d_enum_subsume.end(), subsume.begin(), subsume.end());
- Trace("sygus-pbe-enum")
- << " and subsumed " << subsume.size() << " terms";
- }
- Trace("sygus-pbe-enum")
- << "! add to PBE pool : " << d_tds->sygusToBuiltin(v)
- << std::endl;
- keep = true;
- }
- else
- {
- Assert(subsume.empty());
- Trace("sygus-pbe-enum") << " ...fail : subsumed" << std::endl;
- }
- }
- }
- else
- {
- Trace("sygus-pbe-enum")
- << " ...fail : it does not satisfy examples." << std::endl;
- }
- }
- else
- {
- // must be unique up to examples
- Node val = ecv.d_term_trie.addCond(v, results, true);
- if (val == v)
- {
- Trace("sygus-pbe-enum") << " ...success! add to PBE pool : "
- << d_tds->sygusToBuiltin(v) << std::endl;
- keep = true;
- }
- else
- {
- Trace("sygus-pbe-enum")
- << " ...fail : term is not unique" << std::endl;
- }
- d_cond_count++;
- }
- if (keep)
- {
- // notify to retry the build of solution
- d_check_sol = true;
- ecv.addEnumValue(v, results);
- }
- }
- }
-
- // exclude this value on subsequent iterations
- if (exp_exc.isNull())
- {
- // if we did not already explain why this should be excluded, use default
- exp_exc = d_tds->getExplain()->getExplanationForEquality(e, v);
- }
- exp_exc = exp_exc.negate();
- Trace("sygus-pbe-enum-lemma")
- << "SygusUnif : enumeration exclude lemma : " << exp_exc << std::endl;
- lemmas.push_back(exp_exc);
-}
-
Node SygusUnif::constructSolution()
{
Node c = d_candidate;
// already has a solution
return d_solution;
}
- else
- {
- // only check if an enumerator updated
- if (d_check_sol)
- {
- Trace("sygus-pbe") << "Construct solution, #iterations = " << d_cond_count
- << std::endl;
- d_check_sol = false;
- // try multiple times if we have done multiple conditions, due to
- // non-determinism
- Node vc;
- for (unsigned i = 0; i <= d_cond_count; i++)
- {
- Trace("sygus-pbe-dt")
- << "ConstructPBE for candidate: " << c << std::endl;
- Node e = d_strategy.getRootEnumerator();
- UnifContext x;
- x.initialize(this);
- Node vcc = constructSolution(e, role_equal, x, 1);
- if (!vcc.isNull())
- {
- if (vc.isNull() || (!vc.isNull()
+ // only check if an enumerator updated
+ if (d_check_sol)
+ {
+ Trace("sygus-pbe") << "Construct solution, #iterations = " << d_cond_count
+ << std::endl;
+ d_check_sol = false;
+ // try multiple times if we have done multiple conditions, due to
+ // non-determinism
+ Node vc;
+ for (unsigned i = 0; i <= d_cond_count; i++)
+ {
+ Trace("sygus-pbe-dt") << "ConstructPBE for candidate: " << c << std::endl;
+ Node e = d_strategy.getRootEnumerator();
+ // initialize a call to construct solution
+ initializeConstructSol();
+ // call the virtual construct solution method
+ Node vcc = constructSol(e, role_equal, 1);
+ // if we constructed the solution, and we either did not previously have
+ // a solution, or the new solution is better (smaller).
+ if (!vcc.isNull()
+ && (vc.isNull() || (!vc.isNull()
&& d_tds->getSygusTermSize(vcc)
- < d_tds->getSygusTermSize(vc)))
- {
- Trace("sygus-pbe")
- << "**** PBE SOLVED : " << c << " = " << vcc << std::endl;
- Trace("sygus-pbe") << "...solved at iteration " << i << std::endl;
- vc = vcc;
- }
- }
- }
- if (!vc.isNull())
+ < d_tds->getSygusTermSize(vc))))
{
- d_solution = vc;
- return vc;
+ Trace("sygus-pbe") << "**** SygusUnif SOLVED : " << c << " = " << vcc
+ << std::endl;
+ Trace("sygus-pbe") << "...solved at iteration " << i << std::endl;
+ vc = vcc;
}
- Trace("sygus-pbe") << "...failed to solve." << std::endl;
}
- return Node::null();
- }
-}
-
-// ------------------------------------ solution construction from enumeration
-
-bool SygusUnif::useStrContainsEnumeratorExclude(Node e)
-{
- TypeNode xbt = d_tds->sygusToBuiltinType(e.getType());
- if (xbt.isString())
- {
- std::map<Node, bool>::iterator itx = d_use_str_contains_eexc.find(e);
- if (itx != d_use_str_contains_eexc.end())
+ if (!vc.isNull())
{
- return itx->second;
- }
- Trace("sygus-pbe-enum-debug") << "Is " << e << " is str.contains exclusion?"
- << std::endl;
- d_use_str_contains_eexc[e] = true;
- EnumInfo& ei = d_strategy.getEnumInfo(e);
- for (const Node& sn : ei.d_enum_slave)
- {
- EnumInfo& eis = d_strategy.getEnumInfo(sn);
- EnumRole er = eis.getRole();
- if (er != enum_io && er != enum_concat_term)
- {
- Trace("sygus-pbe-enum-debug") << " incompatible slave : " << sn
- << ", role = " << er << std::endl;
- d_use_str_contains_eexc[e] = false;
- return false;
- }
- if (eis.isConditional())
- {
- Trace("sygus-pbe-enum-debug")
- << " conditional slave : " << sn << std::endl;
- d_use_str_contains_eexc[e] = false;
- return false;
- }
- }
- Trace("sygus-pbe-enum-debug")
- << "...can use str.contains exclusion." << std::endl;
- return d_use_str_contains_eexc[e];
- }
- return false;
-}
-
-bool SygusUnif::getExplanationForEnumeratorExclude(Node e,
- Node v,
- std::vector<Node>& results,
- std::vector<Node>& exp)
-{
- if (useStrContainsEnumeratorExclude(e))
- {
- NodeManager* nm = NodeManager::currentNM();
- // This check whether the example evaluates to something that is larger than
- // the output for some input/output pair. If so, then this term is never
- // useful. We generalize its explanation below.
-
- if (Trace.isOn("sygus-pbe-cterm-debug"))
- {
- Trace("sygus-pbe-enum") << std::endl;
- }
- // check if all examples had longer length that the output
- Assert(d_examples_out.size() == results.size());
- Trace("sygus-pbe-cterm-debug") << "Check enumerator exclusion for " << e
- << " -> " << d_tds->sygusToBuiltin(v)
- << " based on str.contains." << std::endl;
- std::vector<unsigned> cmp_indices;
- for (unsigned i = 0, size = results.size(); i < size; i++)
- {
- Assert(results[i].isConst());
- Assert(d_examples_out[i].isConst());
- Trace("sygus-pbe-cterm-debug") << " " << results[i] << " <> "
- << d_examples_out[i];
- Node cont = nm->mkNode(STRING_STRCTN, d_examples_out[i], results[i]);
- Node contr = Rewriter::rewrite(cont);
- if (contr == d_false)
- {
- cmp_indices.push_back(i);
- Trace("sygus-pbe-cterm-debug") << "...not contained." << std::endl;
- }
- else
- {
- Trace("sygus-pbe-cterm-debug") << "...contained." << std::endl;
- }
- }
- if (!cmp_indices.empty())
- {
- // we check invariance with respect to a negative contains test
- NegContainsSygusInvarianceTest ncset;
- ncset.init(e, d_examples, d_examples_out, cmp_indices);
- // construct the generalized explanation
- d_tds->getExplain()->getExplanationFor(e, v, exp, ncset);
- Trace("sygus-pbe-cterm")
- << "PBE-cterm : enumerator exclude " << d_tds->sygusToBuiltin(v)
- << " due to negative containment." << std::endl;
- return true;
+ d_solution = vc;
+ return vc;
}
+ Trace("sygus-pbe") << "...failed to solve." << std::endl;
}
- return false;
+ return Node::null();
}
-void SygusUnif::EnumCache::addEnumValue(Node v, std::vector<Node>& results)
-{
- // should not have been enumerated before
- Assert(d_enum_val_to_index.find(v) == d_enum_val_to_index.end());
- d_enum_val_to_index[v] = d_enum_vals.size();
- d_enum_vals.push_back(v);
- d_enum_vals_res.push_back(results);
-}
-
-Node SygusUnif::constructBestSolvedTerm(std::vector<Node>& solved,
- UnifContext& x)
+Node SygusUnif::constructBestSolvedTerm(const std::vector<Node>& solved)
{
Assert(!solved.empty());
return solved[0];
}
-Node SygusUnif::constructBestStringSolvedTerm(std::vector<Node>& solved,
- UnifContext& x)
+Node SygusUnif::constructBestStringSolvedTerm(const std::vector<Node>& solved)
{
Assert(!solved.empty());
return solved[0];
}
-Node SygusUnif::constructBestSolvedConditional(std::vector<Node>& solved,
- UnifContext& x)
+Node SygusUnif::constructBestSolvedConditional(const std::vector<Node>& solved)
{
Assert(!solved.empty());
return solved[0];
}
-Node SygusUnif::constructBestConditional(std::vector<Node>& conds,
- UnifContext& x)
+Node SygusUnif::constructBestConditional(const std::vector<Node>& conds)
{
Assert(!conds.empty());
double r = Random::getRandom().pickDouble(0.0, 1.0);
}
Node SygusUnif::constructBestStringToConcat(
- std::vector<Node> strs,
- std::map<Node, unsigned> total_inc,
- std::map<Node, std::vector<unsigned> > incr,
- UnifContext& x)
+ const std::vector<Node>& strs,
+ const std::map<Node, unsigned>& total_inc,
+ const std::map<Node, std::vector<unsigned> >& incr)
{
Assert(!strs.empty());
- std::random_shuffle(strs.begin(), strs.end());
+ std::vector<Node> strs_tmp = strs;
+ std::random_shuffle(strs_tmp.begin(), strs_tmp.end());
// prefer one that has incremented by more than 0
- for (const Node& ns : strs)
+ for (const Node& ns : strs_tmp)
{
- if (total_inc[ns] > 0)
+ const std::map<Node, unsigned>::const_iterator iti = total_inc.find(ns);
+ if (iti != total_inc.end() && iti->second > 0)
{
return ns;
}
}
- return strs[0];
-}
-
-Node SygusUnif::constructSolution(Node e,
- NodeRole nrole,
- UnifContext& x,
- int ind)
-{
- TypeNode etn = e.getType();
- if (Trace.isOn("sygus-pbe-dt-debug"))
- {
- indent("sygus-pbe-dt-debug", ind);
- Trace("sygus-pbe-dt-debug") << "ConstructPBE: (" << e << ", " << nrole
- << ") for type " << etn << " in context ";
- print_val("sygus-pbe-dt-debug", x.d_vals);
- if (x.d_has_string_pos != role_invalid)
- {
- Trace("sygus-pbe-dt-debug") << ", string context [" << x.d_has_string_pos;
- for (unsigned i = 0, size = x.d_str_pos.size(); i < size; i++)
- {
- Trace("sygus-pbe-dt-debug") << " " << x.d_str_pos[i];
- }
- Trace("sygus-pbe-dt-debug") << "]";
- }
- Trace("sygus-pbe-dt-debug") << std::endl;
- }
- // enumerator type info
- EnumTypeInfo& tinfo = d_strategy.getEnumTypeInfo(etn);
-
- // get the enumerator information
- EnumInfo& einfo = d_strategy.getEnumInfo(e);
-
- EnumCache& ecache = d_ecache[e];
-
- Node ret_dt;
- if (nrole == role_equal)
- {
- if (!x.isReturnValueModified())
- {
- if (ecache.isSolved())
- {
- // this type has a complete solution
- ret_dt = ecache.getSolved();
- indent("sygus-pbe-dt", ind);
- Trace("sygus-pbe-dt") << "return PBE: success : solved "
- << d_tds->sygusToBuiltin(ret_dt) << std::endl;
- Assert(!ret_dt.isNull());
- }
- else
- {
- // could be conditionally solved
- std::vector<Node> subsumed_by;
- ecache.d_term_trie.getSubsumedBy(x.d_vals, true, subsumed_by);
- if (!subsumed_by.empty())
- {
- ret_dt = constructBestSolvedTerm(subsumed_by, x);
- indent("sygus-pbe-dt", ind);
- Trace("sygus-pbe-dt") << "return PBE: success : conditionally solved"
- << d_tds->sygusToBuiltin(ret_dt) << std::endl;
- }
- else
- {
- indent("sygus-pbe-dt-debug", ind);
- Trace("sygus-pbe-dt-debug")
- << " ...not currently conditionally solved." << std::endl;
- }
- }
- }
- if (ret_dt.isNull())
- {
- if (d_tds->sygusToBuiltinType(e.getType()).isString())
- {
- // check if a current value that closes all examples
- // get the term enumerator for this type
- std::map<EnumRole, Node>::iterator itnt =
- tinfo.d_enum.find(enum_concat_term);
- if (itnt != tinfo.d_enum.end())
- {
- Node et = itnt->second;
-
- EnumCache& ecachet = d_ecache[et];
- // get the current examples
- std::vector<String> ex_vals;
- x.getCurrentStrings(this, d_examples_out, ex_vals);
- Assert(ecache.d_enum_vals.size() == ecache.d_enum_vals_res.size());
-
- // test each example in the term enumerator for the type
- std::vector<Node> str_solved;
- for (unsigned i = 0, size = ecachet.d_enum_vals.size(); i < size; i++)
- {
- if (x.isStringSolved(this, ex_vals, ecachet.d_enum_vals_res[i]))
- {
- str_solved.push_back(ecachet.d_enum_vals[i]);
- }
- }
- if (!str_solved.empty())
- {
- ret_dt = constructBestStringSolvedTerm(str_solved, x);
- indent("sygus-pbe-dt", ind);
- Trace("sygus-pbe-dt") << "return PBE: success : string solved "
- << d_tds->sygusToBuiltin(ret_dt) << std::endl;
- }
- else
- {
- indent("sygus-pbe-dt-debug", ind);
- Trace("sygus-pbe-dt-debug")
- << " ...not currently string solved." << std::endl;
- }
- }
- }
- }
- }
- else if (nrole == role_string_prefix || nrole == role_string_suffix)
- {
- // check if each return value is a prefix/suffix of all open examples
- if (!x.isReturnValueModified() || x.d_has_string_pos == nrole)
- {
- std::map<Node, std::vector<unsigned> > incr;
- bool isPrefix = nrole == role_string_prefix;
- std::map<Node, unsigned> total_inc;
- std::vector<Node> inc_strs;
- // make the value of the examples
- std::vector<String> ex_vals;
- x.getCurrentStrings(this, d_examples_out, ex_vals);
- if (Trace.isOn("sygus-pbe-dt-debug"))
- {
- indent("sygus-pbe-dt-debug", ind);
- Trace("sygus-pbe-dt-debug") << "current strings : " << std::endl;
- for (unsigned i = 0, size = ex_vals.size(); i < size; i++)
- {
- indent("sygus-pbe-dt-debug", ind + 1);
- Trace("sygus-pbe-dt-debug") << ex_vals[i] << std::endl;
- }
- }
-
- // check if there is a value for which is a prefix/suffix of all active
- // examples
- Assert(ecache.d_enum_vals.size() == ecache.d_enum_vals_res.size());
-
- for (unsigned i = 0, size = ecache.d_enum_vals.size(); i < size; i++)
- {
- Node val_t = ecache.d_enum_vals[i];
- Assert(incr.find(val_t) == incr.end());
- indent("sygus-pbe-dt-debug", ind);
- Trace("sygus-pbe-dt-debug")
- << "increment string values : " << val_t << " : ";
- Assert(ecache.d_enum_vals_res[i].size() == d_examples_out.size());
- unsigned tot = 0;
- bool exsuccess = x.getStringIncrement(this,
- isPrefix,
- ex_vals,
- ecache.d_enum_vals_res[i],
- incr[val_t],
- tot);
- if (!exsuccess)
- {
- incr.erase(val_t);
- Trace("sygus-pbe-dt-debug") << "...fail" << std::endl;
- }
- else
- {
- total_inc[val_t] = tot;
- inc_strs.push_back(val_t);
- Trace("sygus-pbe-dt-debug")
- << "...success, total increment = " << tot << std::endl;
- }
- }
-
- if (!incr.empty())
- {
- ret_dt = constructBestStringToConcat(inc_strs, total_inc, incr, x);
- Assert(!ret_dt.isNull());
- indent("sygus-pbe-dt", ind);
- Trace("sygus-pbe-dt")
- << "PBE: CONCAT strategy : choose " << (isPrefix ? "pre" : "suf")
- << "fix value " << d_tds->sygusToBuiltin(ret_dt) << std::endl;
- // update the context
- bool ret = x.updateStringPosition(this, incr[ret_dt]);
- AlwaysAssert(ret == (total_inc[ret_dt] > 0));
- x.d_has_string_pos = nrole;
- }
- else
- {
- indent("sygus-pbe-dt", ind);
- Trace("sygus-pbe-dt") << "PBE: failed CONCAT strategy, no values are "
- << (isPrefix ? "pre" : "suf")
- << "fix of all examples." << std::endl;
- }
- }
- else
- {
- indent("sygus-pbe-dt", ind);
- Trace("sygus-pbe-dt")
- << "PBE: failed CONCAT strategy, prefix/suffix mismatch."
- << std::endl;
- }
- }
- if (ret_dt.isNull() && !einfo.isTemplated())
- {
- // we will try a single strategy
- EnumTypeInfoStrat* etis = nullptr;
- std::map<NodeRole, StrategyNode>::iterator itsn =
- tinfo.d_snodes.find(nrole);
- if (itsn != tinfo.d_snodes.end())
- {
- // strategy info
- StrategyNode& snode = itsn->second;
- if (x.d_visit_role[e].find(nrole) == x.d_visit_role[e].end())
- {
- x.d_visit_role[e][nrole] = true;
- // try a random strategy
- if (snode.d_strats.size() > 1)
- {
- std::random_shuffle(snode.d_strats.begin(), snode.d_strats.end());
- }
- // get an eligible strategy index
- unsigned sindex = 0;
- while (sindex < snode.d_strats.size()
- && !snode.d_strats[sindex]->isValid(&x))
- {
- sindex++;
- }
- // if we found a eligible strategy
- if (sindex < snode.d_strats.size())
- {
- etis = snode.d_strats[sindex];
- }
- }
- }
- if (etis != nullptr)
- {
- StrategyType strat = etis->d_this;
- indent("sygus-pbe-dt", ind + 1);
- Trace("sygus-pbe-dt")
- << "...try STRATEGY " << strat << "..." << std::endl;
-
- std::map<unsigned, Node> look_ahead_solved_children;
- std::vector<Node> dt_children_cons;
- bool success = true;
-
- // for ITE
- Node split_cond_enum;
- int split_cond_res_index = -1;
-
- for (unsigned sc = 0, size = etis->d_cenum.size(); sc < size; sc++)
- {
- indent("sygus-pbe-dt", ind + 1);
- Trace("sygus-pbe-dt")
- << "construct PBE child #" << sc << "..." << std::endl;
- Node rec_c;
- std::map<unsigned, Node>::iterator itla =
- look_ahead_solved_children.find(sc);
- if (itla != look_ahead_solved_children.end())
- {
- rec_c = itla->second;
- indent("sygus-pbe-dt-debug", ind + 1);
- Trace("sygus-pbe-dt-debug")
- << "ConstructPBE: look ahead solved : "
- << d_tds->sygusToBuiltin(rec_c) << std::endl;
- }
- else
- {
- std::pair<Node, NodeRole>& cenum = etis->d_cenum[sc];
-
- // update the context
- std::vector<Node> prev;
- if (strat == strat_ITE && sc > 0)
- {
- EnumCache& ecache_cond = d_ecache[split_cond_enum];
- Assert(split_cond_res_index >= 0);
- Assert(split_cond_res_index
- < (int)ecache_cond.d_enum_vals_res.size());
- prev = x.d_vals;
- bool ret = x.updateContext(
- this,
- ecache_cond.d_enum_vals_res[split_cond_res_index],
- sc == 1);
- AlwaysAssert(ret);
- }
-
- // recurse
- if (strat == strat_ITE && sc == 0)
- {
- Node ce = cenum.first;
-
- EnumCache& ecache_child = d_ecache[ce];
-
- // only used if the return value is not modified
- if (!x.isReturnValueModified())
- {
- if (x.d_uinfo.find(ce) == x.d_uinfo.end())
- {
- Trace("sygus-pbe-dt-debug2")
- << " reg : PBE: Look for direct solutions for conditional "
- "enumerator "
- << ce << " ... " << std::endl;
- Assert(ecache_child.d_enum_vals.size()
- == ecache_child.d_enum_vals_res.size());
- for (unsigned i = 1; i <= 2; i++)
- {
- std::pair<Node, NodeRole>& te_pair = etis->d_cenum[i];
- Node te = te_pair.first;
- EnumCache& ecache_te = d_ecache[te];
- bool branch_pol = (i == 1);
- // for each condition, get terms that satisfy it in this
- // branch
- for (unsigned k = 0, size = ecache_child.d_enum_vals.size();
- k < size;
- k++)
- {
- Node cond = ecache_child.d_enum_vals[k];
- std::vector<Node> solved;
- ecache_te.d_term_trie.getSubsumedBy(
- ecache_child.d_enum_vals_res[k], branch_pol, solved);
- Trace("sygus-pbe-dt-debug2")
- << " reg : PBE: " << d_tds->sygusToBuiltin(cond)
- << " has " << solved.size() << " solutions in branch "
- << i << std::endl;
- if (!solved.empty())
- {
- Node slv = constructBestSolvedTerm(solved, x);
- Trace("sygus-pbe-dt-debug2")
- << " reg : PBE: ..." << d_tds->sygusToBuiltin(slv)
- << " is a solution under branch " << i;
- Trace("sygus-pbe-dt-debug2")
- << " of condition " << d_tds->sygusToBuiltin(cond)
- << std::endl;
- x.d_uinfo[ce].d_look_ahead_sols[cond][i] = slv;
- }
- }
- }
- }
- }
-
- // get the conditionals in the current context : they must be
- // distinguishable
- std::map<int, std::vector<Node> > possible_cond;
- std::map<Node, int> solved_cond; // stores branch
- ecache_child.d_term_trie.getLeaves(x.d_vals, true, possible_cond);
-
- std::map<int, std::vector<Node> >::iterator itpc =
- possible_cond.find(0);
- if (itpc != possible_cond.end())
- {
- if (Trace.isOn("sygus-pbe-dt-debug"))
- {
- indent("sygus-pbe-dt-debug", ind + 1);
- Trace("sygus-pbe-dt-debug")
- << "PBE : We have " << itpc->second.size()
- << " distinguishable conditionals:" << std::endl;
- for (Node& cond : itpc->second)
- {
- indent("sygus-pbe-dt-debug", ind + 2);
- Trace("sygus-pbe-dt-debug")
- << d_tds->sygusToBuiltin(cond) << std::endl;
- }
- }
-
- // static look ahead conditional : choose conditionals that have
- // solved terms in at least one branch
- // only applicable if we have not modified the return value
- std::map<int, std::vector<Node> > solved_cond;
- if (!x.isReturnValueModified())
- {
- Assert(x.d_uinfo.find(ce) != x.d_uinfo.end());
- int solve_max = 0;
- for (Node& cond : itpc->second)
- {
- std::map<Node, std::map<unsigned, Node> >::iterator itla =
- x.d_uinfo[ce].d_look_ahead_sols.find(cond);
- if (itla != x.d_uinfo[ce].d_look_ahead_sols.end())
- {
- int nsolved = itla->second.size();
- solve_max = nsolved > solve_max ? nsolved : solve_max;
- solved_cond[nsolved].push_back(cond);
- }
- }
- int n = solve_max;
- while (n > 0)
- {
- if (!solved_cond[n].empty())
- {
- rec_c = constructBestSolvedConditional(solved_cond[n], x);
- indent("sygus-pbe-dt", ind + 1);
- Trace("sygus-pbe-dt")
- << "PBE: ITE strategy : choose solved conditional "
- << d_tds->sygusToBuiltin(rec_c) << " with " << n
- << " solved children..." << std::endl;
- std::map<Node, std::map<unsigned, Node> >::iterator itla =
- x.d_uinfo[ce].d_look_ahead_sols.find(rec_c);
- Assert(itla != x.d_uinfo[ce].d_look_ahead_sols.end());
- for (std::pair<const unsigned, Node>& las : itla->second)
- {
- look_ahead_solved_children[las.first] = las.second;
- }
- break;
- }
- n--;
- }
- }
-
- // otherwise, guess a conditional
- if (rec_c.isNull())
- {
- rec_c = constructBestConditional(itpc->second, x);
- Assert(!rec_c.isNull());
- indent("sygus-pbe-dt", ind);
- Trace("sygus-pbe-dt")
- << "PBE: ITE strategy : choose random conditional "
- << d_tds->sygusToBuiltin(rec_c) << std::endl;
- }
- }
- else
- {
- // TODO (#1250) : degenerate case where children have different
- // types?
- indent("sygus-pbe-dt", ind);
- Trace("sygus-pbe-dt") << "return PBE: failed ITE strategy, "
- "cannot find a distinguishable condition"
- << std::endl;
- }
- if (!rec_c.isNull())
- {
- Assert(ecache_child.d_enum_val_to_index.find(rec_c)
- != ecache_child.d_enum_val_to_index.end());
- split_cond_res_index = ecache_child.d_enum_val_to_index[rec_c];
- split_cond_enum = ce;
- Assert(split_cond_res_index >= 0);
- Assert(split_cond_res_index
- < (int)ecache_child.d_enum_vals_res.size());
- }
- }
- else
- {
- rec_c = constructSolution(cenum.first, cenum.second, x, ind + 2);
- }
-
- // undo update the context
- if (strat == strat_ITE && sc > 0)
- {
- x.d_vals = prev;
- }
- }
- if (!rec_c.isNull())
- {
- dt_children_cons.push_back(rec_c);
- }
- else
- {
- success = false;
- break;
- }
- }
- if (success)
- {
- Assert(dt_children_cons.size() == etis->d_sol_templ_args.size());
- // ret_dt = NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR,
- // dt_children );
- ret_dt = etis->d_sol_templ;
- ret_dt = ret_dt.substitute(etis->d_sol_templ_args.begin(),
- etis->d_sol_templ_args.end(),
- dt_children_cons.begin(),
- dt_children_cons.end());
- indent("sygus-pbe-dt-debug", ind);
- Trace("sygus-pbe-dt-debug")
- << "PBE: success : constructed for strategy " << strat << std::endl;
- }
- else
- {
- indent("sygus-pbe-dt-debug", ind);
- Trace("sygus-pbe-dt-debug")
- << "PBE: failed for strategy " << strat << std::endl;
- }
- }
- }
-
- if (!ret_dt.isNull())
- {
- Assert(ret_dt.getType() == e.getType());
- }
- indent("sygus-pbe-dt", ind);
- Trace("sygus-pbe-dt") << "ConstructPBE: returned " << ret_dt << std::endl;
- return ret_dt;
+ return strs_tmp[0];
}
void SygusUnif::indent(const char* c, int ind)
namespace theory {
namespace quantifiers {
-class SygusUnif;
-
-/** Unification context
- *
- * This class maintains state information during calls to
- * SygusUnif::constructSolution, which implements unification-based
- * approaches for construction solutions to synthesis conjectures.
- */
-class UnifContext
-{
- public:
- UnifContext();
- /**
- * This intiializes this context based on information in pbe regarding the
- * kinds of examples it contains.
- */
- void initialize(SygusUnif* pbe);
-
- //----------for ITE strategy
- /** the value of the context conditional
- *
- * This stores a list of Boolean constants that is the same length of the
- * number of input/output example pairs we are considering. For each i,
- * if d_vals[i] = true, i/o pair #i is active according to this context
- * if d_vals[i] = false, i/o pair #i is inactive according to this context
- */
- std::vector<Node> d_vals;
- /** update the examples
- *
- * if pol=true, this method updates d_vals to d_vals & vals
- * if pol=false, this method updates d_vals to d_vals & ( ~vals )
- */
- bool updateContext(SygusUnif* pbe, std::vector<Node>& vals, bool pol);
- //----------end for ITE strategy
-
- //----------for CONCAT strategies
- /** the position in the strings
- *
- * For each i/o example pair, this stores the length of the current solution
- * for the input of the pair, where the solution for that input is a prefix
- * or
- * suffix of the output of the pair. For example, if our i/o pairs are:
- * f( "abcd" ) = "abcdcd"
- * f( "aa" ) = "aacd"
- * If the solution we have currently constructed is str.++( x1, "c", ... ),
- * then d_str_pos = ( 5, 3 ), where notice that
- * str.++( "abc", "c" ) is a prefix of "abcdcd" and
- * str.++( "aa", "c" ) is a prefix of "aacd".
- */
- std::vector<unsigned> d_str_pos;
- /** has string position
- *
- * Whether the solution positions indicate a prefix or suffix of the output
- * examples. If this is role_invalid, then we have not updated the string
- * position.
- */
- NodeRole d_has_string_pos;
- /** update the string examples
- *
- * This method updates d_str_pos to d_str_pos + pos.
- */
- bool updateStringPosition(SygusUnif* pbe, std::vector<unsigned>& pos);
- /** get current strings
- *
- * This returns the prefix/suffix of the string constants stored in vals
- * of size d_str_pos, and stores the result in ex_vals. For example, if vals
- * is (abcdcd", "aacde") and d_str_pos = ( 5, 3 ), then we add
- * "d" and "de" to ex_vals.
- */
- void getCurrentStrings(SygusUnif* pbe,
- const std::vector<Node>& vals,
- std::vector<String>& ex_vals);
- /** get string increment
- *
- * If this method returns true, then inc and tot are updated such that
- * for all active indices i,
- * vals[i] is a prefix (or suffix if isPrefix=false) of ex_vals[i], and
- * inc[i] = str.len(vals[i])
- * for all inactive indices i, inc[i] = 0
- * We set tot to the sum of inc[i] for i=1,...,n. This indicates the total
- * number of characters incremented across all examples.
- */
- bool getStringIncrement(SygusUnif* pbe,
- bool isPrefix,
- const std::vector<String>& ex_vals,
- const std::vector<Node>& vals,
- std::vector<unsigned>& inc,
- unsigned& tot);
- /** returns true if ex_vals[i] = vals[i] for all active indices i. */
- bool isStringSolved(SygusUnif* pbe,
- const std::vector<String>& ex_vals,
- const std::vector<Node>& vals);
- //----------end for CONCAT strategies
-
- /** is return value modified?
- *
- * This returns true if we are currently in a state where the return value
- * of the solution has been modified, e.g. by a previous node that solved
- * for a prefix.
- */
- bool isReturnValueModified();
- /** visited role
- *
- * This is the current set of enumerator/node role pairs we are currently
- * visiting. This set is cleared when the context is updated.
- */
- std::map<Node, std::map<NodeRole, bool> > d_visit_role;
-
- /** unif context enumerator information */
- class UEnumInfo
- {
- public:
- UEnumInfo() {}
- /** map from conditions and branch positions to a solved node
- *
- * For example, if we have:
- * f( 1 ) = 2 ^ f( 3 ) = 4 ^ f( -1 ) = 1
- * Then, valid entries in this map is:
- * d_look_ahead_sols[x>0][1] = x+1
- * d_look_ahead_sols[x>0][2] = 1
- * For the first entry, notice that for all input examples such that x>0
- * evaluates to true, which are (1) and (3), we have that their output
- * values for x+1 under the substitution that maps x to the input value,
- * resulting in 2 and 4, are equal to the output value for the respective
- * pairs.
- */
- std::map<Node, std::map<unsigned, Node> > d_look_ahead_sols;
- };
- /** map from enumerators to the above info class */
- std::map<Node, UEnumInfo> d_uinfo;
-
- private:
- /** true and false nodes */
- Node d_true;
- Node d_false;
-};
-
-/** Subsumption trie
-*
-* This class manages a set of terms for a PBE sygus enumerator.
-*
-* In PBE sygus, we are interested in, for each term t, the set of I/O examples
-* that it satisfies, which can be represented by a vector of Booleans.
-* For example, given conjecture:
-* f( 1 ) = 2 ^ f( 3 ) = 4 ^ f( -1 ) = 1 ^ f( 5 ) = 5
-* If solutions for f are of the form (lambda x. [term]), then:
-* Term x satisfies 0001,
-* Term x+1 satisfies 1100,
-* Term 2 satisfies 0100.
-* Above, term 2 is subsumed by term x+1, since the set of I/O examples that
-* x+1 satisfies are a superset of those satisfied by 2.
-*/
-class SubsumeTrie
-{
- public:
- SubsumeTrie() {}
- /**
- * Adds term t to the trie, removes all terms that are subsumed by t from the
- * trie and adds them to subsumed. The set of I/O examples that t satisfies
- * is given by (pol ? vals : !vals).
- */
- Node addTerm(Node t,
- const std::vector<Node>& vals,
- bool pol,
- std::vector<Node>& subsumed);
- /**
- * Adds term c to the trie, without calculating/updating based on
- * subsumption. This is useful for using this class to store conditionals
- * in ITE strategies, where any conditional whose set of vals is unique
- * (as opposed to not subsumed) is useful.
- */
- Node addCond(Node c, const std::vector<Node>& vals, bool pol);
- /**
- * Returns the set of terms that are subsumed by (pol ? vals : !vals).
- */
- void getSubsumed(const std::vector<Node>& vals,
- bool pol,
- std::vector<Node>& subsumed);
- /**
- * Returns the set of terms that subsume (pol ? vals : !vals). This
- * is for instance useful when determining whether there exists a term
- * that satisfies all active examples in the decision tree learning
- * algorithm.
- */
- void getSubsumedBy(const std::vector<Node>& vals,
- bool pol,
- std::vector<Node>& subsumed_by);
- /**
- * Get the leaves of the trie, which we store in the map v.
- * v[-1] stores the children that always evaluate to !pol,
- * v[1] stores the children that always evaluate to pol,
- * v[0] stores the children that both evaluate to true and false for at least
- * one example.
- */
- void getLeaves(const std::vector<Node>& vals,
- bool pol,
- std::map<int, std::vector<Node> >& v);
- /** is this trie empty? */
- bool isEmpty() { return d_term.isNull() && d_children.empty(); }
- /** clear this trie */
- void clear()
- {
- d_term = Node::null();
- d_children.clear();
- }
-
- private:
- /** the term at this node */
- Node d_term;
- /** the children nodes of this trie */
- std::map<Node, SubsumeTrie> d_children;
- /** helper function for above functions */
- Node addTermInternal(Node t,
- const std::vector<Node>& vals,
- bool pol,
- std::vector<Node>& subsumed,
- bool spol,
- unsigned index,
- int status,
- bool checkExistsOnly,
- bool checkSubsume);
- /** helper function for above functions */
- void getLeavesInternal(const std::vector<Node>& vals,
- bool pol,
- std::map<int, std::vector<Node> >& v,
- unsigned index,
- int status);
-};
-
/** Sygus unification utility
*
* This utility implements synthesis-by-unification style approaches for a
*/
class SygusUnif
{
- friend class UnifContext;
-
public:
SygusUnif();
~SygusUnif();
* 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);
- /** reset examples
- *
- * Reset the specification for f.
- *
- * Notice that this does not reset the
- */
- void resetExamples();
- /** add example
- *
- * This adds input -> output to the specification for f. The arity of
- * input should be equal to the number of arguments in the sygus variable
- * list of the grammar of f. That is, if we are searching for solutions for f
- * of the form (lambda v1...vn. t), then the arity of input should be n.
- */
- void addExample(const std::vector<Node>& input, Node output);
+ virtual void initialize(QuantifiersEngine* qe,
+ Node f,
+ std::vector<Node>& enums,
+ std::vector<Node>& lemmas);
/**
* Notify that the value v has been enumerated for enumerator e. This call
* will add lemmas L to lemmas such that L entails e^M != v for all future
* models M.
*/
- void notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas);
+ virtual void notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas) = 0;
/** construct solution
*
* This attempts to construct a solution based on the current set of
* set of enumerated values is insufficient, or if a non-deterministic
* strategy aborts).
*/
- Node constructSolution();
+ virtual Node constructSolution();
- private:
+ protected:
/** reference to quantifier engine */
QuantifiersEngine* d_qe;
/** sygus term database of d_qe */
quantifiers::TermDbSygus* d_tds;
- /** true and false nodes */
- Node d_true;
- Node d_false;
- /** input of I/O examples */
- std::vector<std::vector<Node> > d_examples;
- /** output of I/O examples */
- std::vector<Node> d_examples_out;
//-----------------------debug printing
/** print ind indentations on trace c */
bool pol = true);
//-----------------------end debug printing
- /**
- * This class stores information regarding an enumerator, including:
- * a database of values that have been enumerated for this enumerator.
- */
- class EnumCache
- {
- public:
- EnumCache() {}
- /**
- * Notify this class that the term v has been enumerated for this enumerator.
- * Its evaluation under the set of examples in pbe are stored in results.
- */
- void addEnumValue(Node v, std::vector<Node>& results);
- /**
- * Notify this class that slv is the complete solution to the synthesis
- * conjecture. This occurs rarely, for instance, when during an ITE strategy
- * we find that a single enumerated term covers all examples.
- */
- void setSolved(Node slv) { d_enum_solved = slv; }
- /** Have we been notified that a complete solution exists? */
- bool isSolved() { return !d_enum_solved.isNull(); }
- /** Get the complete solution to the synthesis conjecture. */
- Node getSolved() { return d_enum_solved; }
- /** Values that have been enumerated for this enumerator */
- std::vector<Node> d_enum_vals;
- /**
- * This either stores the values of f( I ) for inputs
- * or the value of f( I ) = O if d_role==enum_io
- */
- std::vector<std::vector<Node> > d_enum_vals_res;
- /**
- * The set of values in d_enum_vals that have been "subsumed" by others
- * (see SubsumeTrie for explanation of subsumed).
- */
- std::vector<Node> d_enum_subsume;
- /** Map from values to their index in d_enum_vals. */
- std::map<Node, unsigned> d_enum_val_to_index;
- /**
- * A subsumption trie containing the values in d_enum_vals. Depending on the
- * role of this enumerator, values may either be added to d_term_trie with
- * subsumption (if role=enum_io), or without (if role=enum_ite_condition or
- * enum_concat_term).
- */
- SubsumeTrie d_term_trie;
- private:
- /**
- * Whether an enumerated value for this conjecture has solved the entire
- * conjecture.
- */
- Node d_enum_solved;
- };
- /** maps enumerators to the information above */
- std::map<Node, EnumCache> d_ecache;
/**
* Whether we will try to construct solution on the next call to
std::map<Node, bool> d_use_str_contains_eexc;
//------------------------------ constructing solutions
- /** helper function for construct solution.
+ /** implementation-dependent initialize construct solution
+ *
+ * Called once before each attempt to construct solutions.
+ */
+ virtual void initializeConstructSol() = 0;
+ /** implementation-dependent function for construct solution.
*
* Construct a solution based on enumerator e for function-to-synthesize of
* this class with node role nrole in context x.
*
* ind is the term depth of the context (for debugging).
*/
- Node constructSolution(Node e, NodeRole nrole, UnifContext& x, int ind);
+ virtual Node constructSol(Node e, NodeRole nrole, int ind) = 0;
/** Heuristically choose the best solved term from solved in context x,
* currently return the first. */
- Node constructBestSolvedTerm(std::vector<Node>& solved, UnifContext& x);
+ virtual Node constructBestSolvedTerm(const std::vector<Node>& solved);
/** Heuristically choose the best solved string term from solved in context
* x, currently return the first. */
- Node constructBestStringSolvedTerm(std::vector<Node>& solved, UnifContext& x);
+ virtual Node constructBestStringSolvedTerm(const std::vector<Node>& solved);
/** Heuristically choose the best solved conditional term from solved in
* context x, currently random */
- Node constructBestSolvedConditional(std::vector<Node>& solved,
- UnifContext& x);
+ virtual Node constructBestSolvedConditional(const std::vector<Node>& solved);
/** Heuristically choose the best conditional term from conds in context x,
* currently random */
- Node constructBestConditional(std::vector<Node>& conds, UnifContext& x);
+ virtual Node constructBestConditional(const std::vector<Node>& conds);
/** Heuristically choose the best string to concatenate from strs to the
* solution in context x, currently random
* incr stores the vector of indices that are incremented by this solution in
* example outputs.
* total_inc[x] is the sum of incr[x] for each x in strs.
*/
- Node constructBestStringToConcat(std::vector<Node> strs,
- std::map<Node, unsigned> total_inc,
- std::map<Node, std::vector<unsigned> > incr,
- UnifContext& x);
+ virtual Node constructBestStringToConcat(
+ const std::vector<Node>& strs,
+ const std::map<Node, unsigned>& total_inc,
+ const std::map<Node, std::vector<unsigned> >& incr);
//------------------------------ end constructing solutions
};
--- /dev/null
+/********************* */
+/*! \file sygus_unif_io.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of sygus_unif_io
+ **/
+
+#include "theory/quantifiers/sygus/sygus_unif_io.h"
+
+#include "theory/datatypes/datatypes_rewriter.h"
+#include "theory/quantifiers/sygus/term_database_sygus.h"
+#include "theory/quantifiers/term_util.h"
+#include "util/random.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+UnifContextIo::UnifContextIo() : d_curr_role(role_invalid)
+{
+ d_true = NodeManager::currentNM()->mkConst(true);
+ d_false = NodeManager::currentNM()->mkConst(false);
+}
+
+NodeRole UnifContextIo::getCurrentRole() { return d_curr_role; }
+
+bool UnifContextIo::updateContext(SygusUnifIo* sui,
+ std::vector<Node>& vals,
+ bool pol)
+{
+ Assert(d_vals.size() == vals.size());
+ bool changed = false;
+ Node poln = pol ? d_true : d_false;
+ for (unsigned i = 0; i < vals.size(); i++)
+ {
+ if (vals[i] != poln)
+ {
+ if (d_vals[i] == d_true)
+ {
+ d_vals[i] = d_false;
+ changed = true;
+ }
+ }
+ }
+ if (changed)
+ {
+ d_visit_role.clear();
+ }
+ return changed;
+}
+
+bool UnifContextIo::updateStringPosition(SygusUnifIo* sui,
+ std::vector<unsigned>& pos,
+ NodeRole nrole)
+{
+ Assert(pos.size() == d_str_pos.size());
+ bool changed = false;
+ for (unsigned i = 0; i < pos.size(); i++)
+ {
+ if (pos[i] > 0)
+ {
+ d_str_pos[i] += pos[i];
+ changed = true;
+ }
+ }
+ if (changed)
+ {
+ d_visit_role.clear();
+ }
+ d_curr_role = nrole;
+ return changed;
+}
+
+void UnifContextIo::initialize(SygusUnifIo* sui)
+{
+ // clear previous data
+ d_vals.clear();
+ d_str_pos.clear();
+ d_curr_role = role_equal;
+ d_visit_role.clear();
+ d_uinfo.clear();
+
+ // initialize with #examples
+ unsigned sz = sui->d_examples.size();
+ for (unsigned i = 0; i < sz; i++)
+ {
+ d_vals.push_back(d_true);
+ }
+
+ if (!sui->d_examples_out.empty())
+ {
+ // output type of the examples
+ TypeNode exotn = sui->d_examples_out[0].getType();
+
+ if (exotn.isString())
+ {
+ for (unsigned i = 0; i < sz; i++)
+ {
+ d_str_pos.push_back(0);
+ }
+ }
+ }
+ d_visit_role.clear();
+}
+
+void UnifContextIo::getCurrentStrings(SygusUnifIo* sui,
+ const std::vector<Node>& vals,
+ std::vector<String>& ex_vals)
+{
+ bool isPrefix = d_curr_role == role_string_prefix;
+ String dummy;
+ for (unsigned i = 0; i < vals.size(); i++)
+ {
+ if (d_vals[i] == sui->d_true)
+ {
+ Assert(vals[i].isConst());
+ unsigned pos_value = d_str_pos[i];
+ if (pos_value > 0)
+ {
+ Assert(d_curr_role != role_invalid);
+ String s = vals[i].getConst<String>();
+ Assert(pos_value <= s.size());
+ ex_vals.push_back(isPrefix ? s.suffix(s.size() - pos_value)
+ : s.prefix(s.size() - pos_value));
+ }
+ else
+ {
+ ex_vals.push_back(vals[i].getConst<String>());
+ }
+ }
+ else
+ {
+ // irrelevant, add dummy
+ ex_vals.push_back(dummy);
+ }
+ }
+}
+
+bool UnifContextIo::getStringIncrement(SygusUnifIo* sui,
+ bool isPrefix,
+ const std::vector<String>& ex_vals,
+ const std::vector<Node>& vals,
+ std::vector<unsigned>& inc,
+ unsigned& tot)
+{
+ for (unsigned j = 0; j < vals.size(); j++)
+ {
+ unsigned ival = 0;
+ if (d_vals[j] == sui->d_true)
+ {
+ // example is active in this context
+ Assert(vals[j].isConst());
+ String mystr = vals[j].getConst<String>();
+ ival = mystr.size();
+ if (mystr.size() <= ex_vals[j].size())
+ {
+ if (!(isPrefix ? ex_vals[j].strncmp(mystr, ival)
+ : ex_vals[j].rstrncmp(mystr, ival)))
+ {
+ Trace("sygus-sui-dt-debug") << "X";
+ return false;
+ }
+ }
+ else
+ {
+ Trace("sygus-sui-dt-debug") << "X";
+ return false;
+ }
+ }
+ Trace("sygus-sui-dt-debug") << ival;
+ tot += ival;
+ inc.push_back(ival);
+ }
+ return true;
+}
+bool UnifContextIo::isStringSolved(SygusUnifIo* sui,
+ const std::vector<String>& ex_vals,
+ const std::vector<Node>& vals)
+{
+ for (unsigned j = 0; j < vals.size(); j++)
+ {
+ if (d_vals[j] == sui->d_true)
+ {
+ // example is active in this context
+ Assert(vals[j].isConst());
+ String mystr = vals[j].getConst<String>();
+ if (ex_vals[j] != mystr)
+ {
+ return false;
+ }
+ }
+ }
+ return true;
+}
+
+// status : 0 : exact, -1 : vals is subset, 1 : vals is superset
+Node SubsumeTrie::addTermInternal(Node t,
+ const std::vector<Node>& vals,
+ bool pol,
+ std::vector<Node>& subsumed,
+ bool spol,
+ unsigned index,
+ int status,
+ bool checkExistsOnly,
+ bool checkSubsume)
+{
+ if (index == vals.size())
+ {
+ if (status == 0)
+ {
+ // set the term if checkExistsOnly = false
+ if (d_term.isNull() && !checkExistsOnly)
+ {
+ d_term = t;
+ }
+ }
+ else if (status == 1)
+ {
+ Assert(checkSubsume);
+ // found a subsumed term
+ if (!d_term.isNull())
+ {
+ subsumed.push_back(d_term);
+ if (!checkExistsOnly)
+ {
+ // remove it if checkExistsOnly = false
+ d_term = Node::null();
+ }
+ }
+ }
+ else
+ {
+ Assert(!checkExistsOnly && checkSubsume);
+ }
+ return d_term;
+ }
+ NodeManager* nm = NodeManager::currentNM();
+ // the current value
+ Assert(pol || (vals[index].isConst() && vals[index].getType().isBoolean()));
+ Node cv = pol ? vals[index] : nm->mkConst(!vals[index].getConst<bool>());
+ // if checkExistsOnly = false, check if the current value is subsumed if
+ // checkSubsume = true, if so, don't add
+ if (!checkExistsOnly && checkSubsume)
+ {
+ Assert(cv.isConst() && cv.getType().isBoolean());
+ std::vector<bool> check_subsumed_by;
+ if (status == 0)
+ {
+ if (!cv.getConst<bool>())
+ {
+ check_subsumed_by.push_back(spol);
+ }
+ }
+ else if (status == -1)
+ {
+ check_subsumed_by.push_back(spol);
+ if (!cv.getConst<bool>())
+ {
+ check_subsumed_by.push_back(!spol);
+ }
+ }
+ // check for subsumed nodes
+ for (unsigned i = 0, size = check_subsumed_by.size(); i < size; i++)
+ {
+ bool csbi = check_subsumed_by[i];
+ Node csval = nm->mkConst(csbi);
+ // check if subsumed
+ std::map<Node, SubsumeTrie>::iterator itc = d_children.find(csval);
+ if (itc != d_children.end())
+ {
+ Node ret = itc->second.addTermInternal(t,
+ vals,
+ pol,
+ subsumed,
+ spol,
+ index + 1,
+ -1,
+ checkExistsOnly,
+ checkSubsume);
+ // ret subsumes t
+ if (!ret.isNull())
+ {
+ return ret;
+ }
+ }
+ }
+ }
+ Node ret;
+ std::vector<bool> check_subsume;
+ if (status == 0)
+ {
+ if (checkExistsOnly)
+ {
+ std::map<Node, SubsumeTrie>::iterator itc = d_children.find(cv);
+ if (itc != d_children.end())
+ {
+ ret = itc->second.addTermInternal(t,
+ vals,
+ pol,
+ subsumed,
+ spol,
+ index + 1,
+ 0,
+ checkExistsOnly,
+ checkSubsume);
+ }
+ }
+ else
+ {
+ Assert(spol);
+ ret = d_children[cv].addTermInternal(t,
+ vals,
+ pol,
+ subsumed,
+ spol,
+ index + 1,
+ 0,
+ checkExistsOnly,
+ checkSubsume);
+ if (ret != t)
+ {
+ // we were subsumed by ret, return
+ return ret;
+ }
+ }
+ if (checkSubsume)
+ {
+ Assert(cv.isConst() && cv.getType().isBoolean());
+ // check for subsuming
+ if (cv.getConst<bool>())
+ {
+ check_subsume.push_back(!spol);
+ }
+ }
+ }
+ else if (status == 1)
+ {
+ Assert(checkSubsume);
+ Assert(cv.isConst() && cv.getType().isBoolean());
+ check_subsume.push_back(!spol);
+ if (cv.getConst<bool>())
+ {
+ check_subsume.push_back(spol);
+ }
+ }
+ if (checkSubsume)
+ {
+ // check for subsumed terms
+ for (unsigned i = 0, size = check_subsume.size(); i < size; i++)
+ {
+ Node csval = nm->mkConst<bool>(check_subsume[i]);
+ std::map<Node, SubsumeTrie>::iterator itc = d_children.find(csval);
+ if (itc != d_children.end())
+ {
+ itc->second.addTermInternal(t,
+ vals,
+ pol,
+ subsumed,
+ spol,
+ index + 1,
+ 1,
+ checkExistsOnly,
+ checkSubsume);
+ // clean up
+ if (itc->second.isEmpty())
+ {
+ Assert(!checkExistsOnly);
+ d_children.erase(csval);
+ }
+ }
+ }
+ }
+ return ret;
+}
+
+Node SubsumeTrie::addTerm(Node t,
+ const std::vector<Node>& vals,
+ bool pol,
+ std::vector<Node>& subsumed)
+{
+ return addTermInternal(t, vals, pol, subsumed, true, 0, 0, false, true);
+}
+
+Node SubsumeTrie::addCond(Node c, const std::vector<Node>& vals, bool pol)
+{
+ std::vector<Node> subsumed;
+ return addTermInternal(c, vals, pol, subsumed, true, 0, 0, false, false);
+}
+
+void SubsumeTrie::getSubsumed(const std::vector<Node>& vals,
+ bool pol,
+ std::vector<Node>& subsumed)
+{
+ addTermInternal(Node::null(), vals, pol, subsumed, true, 0, 1, true, true);
+}
+
+void SubsumeTrie::getSubsumedBy(const std::vector<Node>& vals,
+ bool pol,
+ std::vector<Node>& subsumed_by)
+{
+ // flip polarities
+ addTermInternal(
+ Node::null(), vals, !pol, subsumed_by, false, 0, 1, true, true);
+}
+
+void SubsumeTrie::getLeavesInternal(const std::vector<Node>& vals,
+ bool pol,
+ std::map<int, std::vector<Node> >& v,
+ unsigned index,
+ int status)
+{
+ if (index == vals.size())
+ {
+ Assert(!d_term.isNull());
+ Assert(std::find(v[status].begin(), v[status].end(), d_term)
+ == v[status].end());
+ v[status].push_back(d_term);
+ }
+ else
+ {
+ Assert(vals[index].isConst() && vals[index].getType().isBoolean());
+ bool curr_val_true = vals[index].getConst<bool>() == pol;
+ for (std::map<Node, SubsumeTrie>::iterator it = d_children.begin();
+ it != d_children.end();
+ ++it)
+ {
+ int new_status = status;
+ // if the current value is true
+ if (curr_val_true)
+ {
+ if (status != 0)
+ {
+ Assert(it->first.isConst() && it->first.getType().isBoolean());
+ new_status = (it->first.getConst<bool>() ? 1 : -1);
+ if (status != -2 && new_status != status)
+ {
+ new_status = 0;
+ }
+ }
+ }
+ it->second.getLeavesInternal(vals, pol, v, index + 1, new_status);
+ }
+ }
+}
+
+void SubsumeTrie::getLeaves(const std::vector<Node>& vals,
+ bool pol,
+ std::map<int, std::vector<Node> >& v)
+{
+ getLeavesInternal(vals, pol, v, 0, -2);
+}
+
+SygusUnifIo::SygusUnifIo()
+{
+ d_true = NodeManager::currentNM()->mkConst(true);
+ d_false = NodeManager::currentNM()->mkConst(false);
+}
+
+SygusUnifIo::~SygusUnifIo() {}
+
+void SygusUnifIo::initialize(QuantifiersEngine* qe,
+ Node f,
+ std::vector<Node>& enums,
+ std::vector<Node>& lemmas)
+{
+ d_examples.clear();
+ d_examples_out.clear();
+ d_ecache.clear();
+ SygusUnif::initialize(qe, f, enums, lemmas);
+}
+
+void SygusUnifIo::addExample(const std::vector<Node>& input, Node output)
+{
+ d_examples.push_back(input);
+ d_examples_out.push_back(output);
+}
+
+void SygusUnifIo::notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas)
+{
+ Trace("sygus-sui-enum") << "Notify enumeration for " << e << " : " << v
+ << std::endl;
+ Node c = d_candidate;
+ Assert(!d_examples.empty());
+ Assert(d_examples.size() == d_examples_out.size());
+
+ EnumInfo& ei = d_strategy.getEnumInfo(e);
+ // The explanation for why the current value should be excluded in future
+ // iterations.
+ Node exp_exc;
+
+ TypeNode xtn = e.getType();
+ Node bv = d_tds->sygusToBuiltin(v, xtn);
+ std::vector<Node> base_results;
+ // compte the results
+ for (unsigned j = 0, size = d_examples.size(); j < size; j++)
+ {
+ Node res = d_tds->evaluateBuiltin(xtn, bv, d_examples[j]);
+ Trace("sygus-sui-enum-debug")
+ << "...got res = " << res << " from " << bv << std::endl;
+ base_results.push_back(res);
+ }
+ // is it excluded for domain-specific reason?
+ std::vector<Node> exp_exc_vec;
+ if (getExplanationForEnumeratorExclude(e, v, base_results, exp_exc_vec))
+ {
+ Assert(!exp_exc_vec.empty());
+ exp_exc = exp_exc_vec.size() == 1
+ ? exp_exc_vec[0]
+ : NodeManager::currentNM()->mkNode(AND, exp_exc_vec);
+ Trace("sygus-sui-enum")
+ << " ...fail : term is excluded (domain-specific)" << std::endl;
+ }
+ else
+ {
+ // notify all slaves
+ Assert(!ei.d_enum_slave.empty());
+ // explanation for why this value should be excluded
+ for (unsigned s = 0; s < ei.d_enum_slave.size(); s++)
+ {
+ Node xs = ei.d_enum_slave[s];
+
+ EnumInfo& eiv = d_strategy.getEnumInfo(xs);
+
+ EnumCache& ecv = d_ecache[xs];
+
+ Trace("sygus-sui-enum") << "Process " << xs << " from " << s << std::endl;
+ // bool prevIsCover = false;
+ if (eiv.getRole() == enum_io)
+ {
+ Trace("sygus-sui-enum") << " IO-Eval of ";
+ // prevIsCover = eiv.isFeasible();
+ }
+ else
+ {
+ Trace("sygus-sui-enum") << "Evaluation of ";
+ }
+ Trace("sygus-sui-enum") << xs << " : ";
+ // evaluate all input/output examples
+ std::vector<Node> results;
+ Node templ = eiv.d_template;
+ TNode templ_var = eiv.d_template_arg;
+ std::map<Node, bool> cond_vals;
+ for (unsigned j = 0, size = base_results.size(); j < size; j++)
+ {
+ Node res = base_results[j];
+ Assert(res.isConst());
+ if (!templ.isNull())
+ {
+ TNode tres = res;
+ res = templ.substitute(templ_var, res);
+ res = Rewriter::rewrite(res);
+ Assert(res.isConst());
+ }
+ Node resb;
+ if (eiv.getRole() == enum_io)
+ {
+ Node out = d_examples_out[j];
+ Assert(out.isConst());
+ resb = res == out ? d_true : d_false;
+ }
+ else
+ {
+ resb = res;
+ }
+ cond_vals[resb] = true;
+ results.push_back(resb);
+ if (Trace.isOn("sygus-sui-enum"))
+ {
+ if (resb.getType().isBoolean())
+ {
+ Trace("sygus-sui-enum") << (resb == d_true ? "1" : "0");
+ }
+ else
+ {
+ Trace("sygus-sui-enum") << "?";
+ }
+ }
+ }
+ bool keep = false;
+ if (eiv.getRole() == enum_io)
+ {
+ // latter is the degenerate case of no examples
+ if (cond_vals.find(d_true) != cond_vals.end() || cond_vals.empty())
+ {
+ // check subsumbed/subsuming
+ std::vector<Node> subsume;
+ if (cond_vals.find(d_false) == cond_vals.end())
+ {
+ // it is the entire solution, we are done
+ Trace("sygus-sui-enum")
+ << " ...success, full solution added to PBE pool : "
+ << d_tds->sygusToBuiltin(v) << std::endl;
+ if (!ecv.isSolved())
+ {
+ ecv.setSolved(v);
+ // it subsumes everything
+ ecv.d_term_trie.clear();
+ ecv.d_term_trie.addTerm(v, results, true, subsume);
+ }
+ keep = true;
+ }
+ else
+ {
+ Node val = ecv.d_term_trie.addTerm(v, results, true, subsume);
+ if (val == v)
+ {
+ Trace("sygus-sui-enum") << " ...success";
+ if (!subsume.empty())
+ {
+ ecv.d_enum_subsume.insert(
+ ecv.d_enum_subsume.end(), subsume.begin(), subsume.end());
+ Trace("sygus-sui-enum")
+ << " and subsumed " << subsume.size() << " terms";
+ }
+ Trace("sygus-sui-enum")
+ << "! add to PBE pool : " << d_tds->sygusToBuiltin(v)
+ << std::endl;
+ keep = true;
+ }
+ else
+ {
+ Assert(subsume.empty());
+ Trace("sygus-sui-enum") << " ...fail : subsumed" << std::endl;
+ }
+ }
+ }
+ else
+ {
+ Trace("sygus-sui-enum")
+ << " ...fail : it does not satisfy examples." << std::endl;
+ }
+ }
+ else
+ {
+ // must be unique up to examples
+ Node val = ecv.d_term_trie.addCond(v, results, true);
+ if (val == v)
+ {
+ Trace("sygus-sui-enum") << " ...success! add to PBE pool : "
+ << d_tds->sygusToBuiltin(v) << std::endl;
+ keep = true;
+ }
+ else
+ {
+ Trace("sygus-sui-enum")
+ << " ...fail : term is not unique" << std::endl;
+ }
+ d_cond_count++;
+ }
+ if (keep)
+ {
+ // notify to retry the build of solution
+ d_check_sol = true;
+ ecv.addEnumValue(v, results);
+ }
+ }
+ }
+
+ // exclude this value on subsequent iterations
+ if (exp_exc.isNull())
+ {
+ // if we did not already explain why this should be excluded, use default
+ exp_exc = d_tds->getExplain()->getExplanationForEquality(e, v);
+ }
+ exp_exc = exp_exc.negate();
+ Trace("sygus-sui-enum-lemma")
+ << "SygusUnifIo : enumeration exclude lemma : " << exp_exc << std::endl;
+ lemmas.push_back(exp_exc);
+}
+
+// ------------------------------------ solution construction from enumeration
+
+bool SygusUnifIo::useStrContainsEnumeratorExclude(Node e)
+{
+ TypeNode xbt = d_tds->sygusToBuiltinType(e.getType());
+ if (xbt.isString())
+ {
+ std::map<Node, bool>::iterator itx = d_use_str_contains_eexc.find(e);
+ if (itx != d_use_str_contains_eexc.end())
+ {
+ return itx->second;
+ }
+ Trace("sygus-sui-enum-debug")
+ << "Is " << e << " is str.contains exclusion?" << std::endl;
+ d_use_str_contains_eexc[e] = true;
+ EnumInfo& ei = d_strategy.getEnumInfo(e);
+ for (const Node& sn : ei.d_enum_slave)
+ {
+ EnumInfo& eis = d_strategy.getEnumInfo(sn);
+ EnumRole er = eis.getRole();
+ if (er != enum_io && er != enum_concat_term)
+ {
+ Trace("sygus-sui-enum-debug") << " incompatible slave : " << sn
+ << ", role = " << er << std::endl;
+ d_use_str_contains_eexc[e] = false;
+ return false;
+ }
+ if (eis.isConditional())
+ {
+ Trace("sygus-sui-enum-debug")
+ << " conditional slave : " << sn << std::endl;
+ d_use_str_contains_eexc[e] = false;
+ return false;
+ }
+ }
+ Trace("sygus-sui-enum-debug")
+ << "...can use str.contains exclusion." << std::endl;
+ return d_use_str_contains_eexc[e];
+ }
+ return false;
+}
+
+bool SygusUnifIo::getExplanationForEnumeratorExclude(Node e,
+ Node v,
+ std::vector<Node>& results,
+ std::vector<Node>& exp)
+{
+ if (useStrContainsEnumeratorExclude(e))
+ {
+ NodeManager* nm = NodeManager::currentNM();
+ // This check whether the example evaluates to something that is larger than
+ // the output for some input/output pair. If so, then this term is never
+ // useful. We generalize its explanation below.
+
+ if (Trace.isOn("sygus-sui-cterm-debug"))
+ {
+ Trace("sygus-sui-enum") << std::endl;
+ }
+ // check if all examples had longer length that the output
+ Assert(d_examples_out.size() == results.size());
+ Trace("sygus-sui-cterm-debug")
+ << "Check enumerator exclusion for " << e << " -> "
+ << d_tds->sygusToBuiltin(v) << " based on str.contains." << std::endl;
+ std::vector<unsigned> cmp_indices;
+ for (unsigned i = 0, size = results.size(); i < size; i++)
+ {
+ Assert(results[i].isConst());
+ Assert(d_examples_out[i].isConst());
+ Trace("sygus-sui-cterm-debug")
+ << " " << results[i] << " <> " << d_examples_out[i];
+ Node cont = nm->mkNode(STRING_STRCTN, d_examples_out[i], results[i]);
+ Node contr = Rewriter::rewrite(cont);
+ if (contr == d_false)
+ {
+ cmp_indices.push_back(i);
+ Trace("sygus-sui-cterm-debug") << "...not contained." << std::endl;
+ }
+ else
+ {
+ Trace("sygus-sui-cterm-debug") << "...contained." << std::endl;
+ }
+ }
+ if (!cmp_indices.empty())
+ {
+ // we check invariance with respect to a negative contains test
+ NegContainsSygusInvarianceTest ncset;
+ ncset.init(e, d_examples, d_examples_out, cmp_indices);
+ // construct the generalized explanation
+ d_tds->getExplain()->getExplanationFor(e, v, exp, ncset);
+ Trace("sygus-sui-cterm")
+ << "PBE-cterm : enumerator exclude " << d_tds->sygusToBuiltin(v)
+ << " due to negative containment." << std::endl;
+ return true;
+ }
+ }
+ return false;
+}
+
+void SygusUnifIo::EnumCache::addEnumValue(Node v, std::vector<Node>& results)
+{
+ // should not have been enumerated before
+ Assert(d_enum_val_to_index.find(v) == d_enum_val_to_index.end());
+ d_enum_val_to_index[v] = d_enum_vals.size();
+ d_enum_vals.push_back(v);
+ d_enum_vals_res.push_back(results);
+}
+
+void SygusUnifIo::initializeConstructSol() { d_context.initialize(this); }
+
+Node SygusUnifIo::constructSol(Node e, NodeRole nrole, int ind)
+{
+ UnifContextIo& x = d_context;
+ TypeNode etn = e.getType();
+ if (Trace.isOn("sygus-sui-dt-debug"))
+ {
+ indent("sygus-sui-dt-debug", ind);
+ Trace("sygus-sui-dt-debug") << "ConstructPBE: (" << e << ", " << nrole
+ << ") for type " << etn << " in context ";
+ print_val("sygus-sui-dt-debug", x.d_vals);
+ NodeRole ctx_role = x.getCurrentRole();
+ Trace("sygus-sui-dt-debug") << ", context role [" << ctx_role;
+ if (ctx_role == role_string_prefix || ctx_role == role_string_suffix)
+ {
+ Trace("sygus-sui-dt-debug") << ", string pos : ";
+ for (unsigned i = 0, size = x.d_str_pos.size(); i < size; i++)
+ {
+ Trace("sygus-sui-dt-debug") << " " << x.d_str_pos[i];
+ }
+ }
+ Trace("sygus-sui-dt-debug") << "]";
+ Trace("sygus-sui-dt-debug") << std::endl;
+ }
+ // enumerator type info
+ EnumTypeInfo& tinfo = d_strategy.getEnumTypeInfo(etn);
+
+ // get the enumerator information
+ EnumInfo& einfo = d_strategy.getEnumInfo(e);
+
+ EnumCache& ecache = d_ecache[e];
+
+ Node ret_dt;
+ if (nrole == role_equal)
+ {
+ if (!x.isReturnValueModified())
+ {
+ if (ecache.isSolved())
+ {
+ // this type has a complete solution
+ ret_dt = ecache.getSolved();
+ indent("sygus-sui-dt", ind);
+ Trace("sygus-sui-dt") << "return PBE: success : solved "
+ << d_tds->sygusToBuiltin(ret_dt) << std::endl;
+ Assert(!ret_dt.isNull());
+ }
+ else
+ {
+ // could be conditionally solved
+ std::vector<Node> subsumed_by;
+ ecache.d_term_trie.getSubsumedBy(x.d_vals, true, subsumed_by);
+ if (!subsumed_by.empty())
+ {
+ ret_dt = constructBestSolvedTerm(subsumed_by);
+ indent("sygus-sui-dt", ind);
+ Trace("sygus-sui-dt") << "return PBE: success : conditionally solved"
+ << d_tds->sygusToBuiltin(ret_dt) << std::endl;
+ }
+ else
+ {
+ indent("sygus-sui-dt-debug", ind);
+ Trace("sygus-sui-dt-debug")
+ << " ...not currently conditionally solved." << std::endl;
+ }
+ }
+ }
+ if (ret_dt.isNull())
+ {
+ if (d_tds->sygusToBuiltinType(e.getType()).isString())
+ {
+ // check if a current value that closes all examples
+ // get the term enumerator for this type
+ std::map<EnumRole, Node>::iterator itnt =
+ tinfo.d_enum.find(enum_concat_term);
+ if (itnt != tinfo.d_enum.end())
+ {
+ Node et = itnt->second;
+
+ EnumCache& ecachet = d_ecache[et];
+ // get the current examples
+ std::vector<String> ex_vals;
+ x.getCurrentStrings(this, d_examples_out, ex_vals);
+ Assert(ecache.d_enum_vals.size() == ecache.d_enum_vals_res.size());
+
+ // test each example in the term enumerator for the type
+ std::vector<Node> str_solved;
+ for (unsigned i = 0, size = ecachet.d_enum_vals.size(); i < size; i++)
+ {
+ if (x.isStringSolved(this, ex_vals, ecachet.d_enum_vals_res[i]))
+ {
+ str_solved.push_back(ecachet.d_enum_vals[i]);
+ }
+ }
+ if (!str_solved.empty())
+ {
+ ret_dt = constructBestStringSolvedTerm(str_solved);
+ indent("sygus-sui-dt", ind);
+ Trace("sygus-sui-dt") << "return PBE: success : string solved "
+ << d_tds->sygusToBuiltin(ret_dt) << std::endl;
+ }
+ else
+ {
+ indent("sygus-sui-dt-debug", ind);
+ Trace("sygus-sui-dt-debug")
+ << " ...not currently string solved." << std::endl;
+ }
+ }
+ }
+ }
+ }
+ else if (nrole == role_string_prefix || nrole == role_string_suffix)
+ {
+ // check if each return value is a prefix/suffix of all open examples
+ if (!x.isReturnValueModified() || x.getCurrentRole() == nrole)
+ {
+ std::map<Node, std::vector<unsigned> > incr;
+ bool isPrefix = nrole == role_string_prefix;
+ std::map<Node, unsigned> total_inc;
+ std::vector<Node> inc_strs;
+ // make the value of the examples
+ std::vector<String> ex_vals;
+ x.getCurrentStrings(this, d_examples_out, ex_vals);
+ if (Trace.isOn("sygus-sui-dt-debug"))
+ {
+ indent("sygus-sui-dt-debug", ind);
+ Trace("sygus-sui-dt-debug") << "current strings : " << std::endl;
+ for (unsigned i = 0, size = ex_vals.size(); i < size; i++)
+ {
+ indent("sygus-sui-dt-debug", ind + 1);
+ Trace("sygus-sui-dt-debug") << ex_vals[i] << std::endl;
+ }
+ }
+
+ // check if there is a value for which is a prefix/suffix of all active
+ // examples
+ Assert(ecache.d_enum_vals.size() == ecache.d_enum_vals_res.size());
+
+ for (unsigned i = 0, size = ecache.d_enum_vals.size(); i < size; i++)
+ {
+ Node val_t = ecache.d_enum_vals[i];
+ Assert(incr.find(val_t) == incr.end());
+ indent("sygus-sui-dt-debug", ind);
+ Trace("sygus-sui-dt-debug")
+ << "increment string values : " << val_t << " : ";
+ Assert(ecache.d_enum_vals_res[i].size() == d_examples_out.size());
+ unsigned tot = 0;
+ bool exsuccess = x.getStringIncrement(this,
+ isPrefix,
+ ex_vals,
+ ecache.d_enum_vals_res[i],
+ incr[val_t],
+ tot);
+ if (!exsuccess)
+ {
+ incr.erase(val_t);
+ Trace("sygus-sui-dt-debug") << "...fail" << std::endl;
+ }
+ else
+ {
+ total_inc[val_t] = tot;
+ inc_strs.push_back(val_t);
+ Trace("sygus-sui-dt-debug")
+ << "...success, total increment = " << tot << std::endl;
+ }
+ }
+
+ if (!incr.empty())
+ {
+ ret_dt = constructBestStringToConcat(inc_strs, total_inc, incr);
+ Assert(!ret_dt.isNull());
+ indent("sygus-sui-dt", ind);
+ Trace("sygus-sui-dt")
+ << "PBE: CONCAT strategy : choose " << (isPrefix ? "pre" : "suf")
+ << "fix value " << d_tds->sygusToBuiltin(ret_dt) << std::endl;
+ // update the context
+ bool ret = x.updateStringPosition(this, incr[ret_dt], nrole);
+ AlwaysAssert(ret == (total_inc[ret_dt] > 0));
+ }
+ else
+ {
+ indent("sygus-sui-dt", ind);
+ Trace("sygus-sui-dt") << "PBE: failed CONCAT strategy, no values are "
+ << (isPrefix ? "pre" : "suf")
+ << "fix of all examples." << std::endl;
+ }
+ }
+ else
+ {
+ indent("sygus-sui-dt", ind);
+ Trace("sygus-sui-dt")
+ << "PBE: failed CONCAT strategy, prefix/suffix mismatch."
+ << std::endl;
+ }
+ }
+ if (ret_dt.isNull() && !einfo.isTemplated())
+ {
+ // we will try a single strategy
+ EnumTypeInfoStrat* etis = nullptr;
+ std::map<NodeRole, StrategyNode>::iterator itsn =
+ tinfo.d_snodes.find(nrole);
+ if (itsn != tinfo.d_snodes.end())
+ {
+ // strategy info
+ StrategyNode& snode = itsn->second;
+ if (x.d_visit_role[e].find(nrole) == x.d_visit_role[e].end())
+ {
+ x.d_visit_role[e][nrole] = true;
+ // try a random strategy
+ if (snode.d_strats.size() > 1)
+ {
+ std::random_shuffle(snode.d_strats.begin(), snode.d_strats.end());
+ }
+ // get an eligible strategy index
+ unsigned sindex = 0;
+ while (sindex < snode.d_strats.size()
+ && !snode.d_strats[sindex]->isValid(x))
+ {
+ sindex++;
+ }
+ // if we found a eligible strategy
+ if (sindex < snode.d_strats.size())
+ {
+ etis = snode.d_strats[sindex];
+ }
+ }
+ }
+ if (etis != nullptr)
+ {
+ StrategyType strat = etis->d_this;
+ indent("sygus-sui-dt", ind + 1);
+ Trace("sygus-sui-dt")
+ << "...try STRATEGY " << strat << "..." << std::endl;
+
+ std::map<unsigned, Node> look_ahead_solved_children;
+ std::vector<Node> dt_children_cons;
+ bool success = true;
+
+ // for ITE
+ Node split_cond_enum;
+ int split_cond_res_index = -1;
+
+ for (unsigned sc = 0, size = etis->d_cenum.size(); sc < size; sc++)
+ {
+ indent("sygus-sui-dt", ind + 1);
+ Trace("sygus-sui-dt")
+ << "construct PBE child #" << sc << "..." << std::endl;
+ Node rec_c;
+ std::map<unsigned, Node>::iterator itla =
+ look_ahead_solved_children.find(sc);
+ if (itla != look_ahead_solved_children.end())
+ {
+ rec_c = itla->second;
+ indent("sygus-sui-dt-debug", ind + 1);
+ Trace("sygus-sui-dt-debug")
+ << "ConstructPBE: look ahead solved : "
+ << d_tds->sygusToBuiltin(rec_c) << std::endl;
+ }
+ else
+ {
+ std::pair<Node, NodeRole>& cenum = etis->d_cenum[sc];
+
+ // update the context
+ std::vector<Node> prev;
+ if (strat == strat_ITE && sc > 0)
+ {
+ EnumCache& ecache_cond = d_ecache[split_cond_enum];
+ Assert(split_cond_res_index >= 0);
+ Assert(split_cond_res_index
+ < (int)ecache_cond.d_enum_vals_res.size());
+ prev = x.d_vals;
+ bool ret = x.updateContext(
+ this,
+ ecache_cond.d_enum_vals_res[split_cond_res_index],
+ sc == 1);
+ AlwaysAssert(ret);
+ }
+
+ // recurse
+ if (strat == strat_ITE && sc == 0)
+ {
+ Node ce = cenum.first;
+
+ EnumCache& ecache_child = d_ecache[ce];
+
+ // only used if the return value is not modified
+ if (!x.isReturnValueModified())
+ {
+ if (x.d_uinfo.find(ce) == x.d_uinfo.end())
+ {
+ Trace("sygus-sui-dt-debug2")
+ << " reg : PBE: Look for direct solutions for conditional "
+ "enumerator "
+ << ce << " ... " << std::endl;
+ Assert(ecache_child.d_enum_vals.size()
+ == ecache_child.d_enum_vals_res.size());
+ for (unsigned i = 1; i <= 2; i++)
+ {
+ std::pair<Node, NodeRole>& te_pair = etis->d_cenum[i];
+ Node te = te_pair.first;
+ EnumCache& ecache_te = d_ecache[te];
+ bool branch_pol = (i == 1);
+ // for each condition, get terms that satisfy it in this
+ // branch
+ for (unsigned k = 0, size = ecache_child.d_enum_vals.size();
+ k < size;
+ k++)
+ {
+ Node cond = ecache_child.d_enum_vals[k];
+ std::vector<Node> solved;
+ ecache_te.d_term_trie.getSubsumedBy(
+ ecache_child.d_enum_vals_res[k], branch_pol, solved);
+ Trace("sygus-sui-dt-debug2")
+ << " reg : PBE: " << d_tds->sygusToBuiltin(cond)
+ << " has " << solved.size() << " solutions in branch "
+ << i << std::endl;
+ if (!solved.empty())
+ {
+ Node slv = constructBestSolvedTerm(solved);
+ Trace("sygus-sui-dt-debug2")
+ << " reg : PBE: ..." << d_tds->sygusToBuiltin(slv)
+ << " is a solution under branch " << i;
+ Trace("sygus-sui-dt-debug2")
+ << " of condition " << d_tds->sygusToBuiltin(cond)
+ << std::endl;
+ x.d_uinfo[ce].d_look_ahead_sols[cond][i] = slv;
+ }
+ }
+ }
+ }
+ }
+
+ // get the conditionals in the current context : they must be
+ // distinguishable
+ std::map<int, std::vector<Node> > possible_cond;
+ std::map<Node, int> solved_cond; // stores branch
+ ecache_child.d_term_trie.getLeaves(x.d_vals, true, possible_cond);
+
+ std::map<int, std::vector<Node> >::iterator itpc =
+ possible_cond.find(0);
+ if (itpc != possible_cond.end())
+ {
+ if (Trace.isOn("sygus-sui-dt-debug"))
+ {
+ indent("sygus-sui-dt-debug", ind + 1);
+ Trace("sygus-sui-dt-debug")
+ << "PBE : We have " << itpc->second.size()
+ << " distinguishable conditionals:" << std::endl;
+ for (Node& cond : itpc->second)
+ {
+ indent("sygus-sui-dt-debug", ind + 2);
+ Trace("sygus-sui-dt-debug")
+ << d_tds->sygusToBuiltin(cond) << std::endl;
+ }
+ }
+
+ // static look ahead conditional : choose conditionals that have
+ // solved terms in at least one branch
+ // only applicable if we have not modified the return value
+ std::map<int, std::vector<Node> > solved_cond;
+ if (!x.isReturnValueModified())
+ {
+ Assert(x.d_uinfo.find(ce) != x.d_uinfo.end());
+ int solve_max = 0;
+ for (Node& cond : itpc->second)
+ {
+ std::map<Node, std::map<unsigned, Node> >::iterator itla =
+ x.d_uinfo[ce].d_look_ahead_sols.find(cond);
+ if (itla != x.d_uinfo[ce].d_look_ahead_sols.end())
+ {
+ int nsolved = itla->second.size();
+ solve_max = nsolved > solve_max ? nsolved : solve_max;
+ solved_cond[nsolved].push_back(cond);
+ }
+ }
+ int n = solve_max;
+ while (n > 0)
+ {
+ if (!solved_cond[n].empty())
+ {
+ rec_c = constructBestSolvedConditional(solved_cond[n]);
+ indent("sygus-sui-dt", ind + 1);
+ Trace("sygus-sui-dt")
+ << "PBE: ITE strategy : choose solved conditional "
+ << d_tds->sygusToBuiltin(rec_c) << " with " << n
+ << " solved children..." << std::endl;
+ std::map<Node, std::map<unsigned, Node> >::iterator itla =
+ x.d_uinfo[ce].d_look_ahead_sols.find(rec_c);
+ Assert(itla != x.d_uinfo[ce].d_look_ahead_sols.end());
+ for (std::pair<const unsigned, Node>& las : itla->second)
+ {
+ look_ahead_solved_children[las.first] = las.second;
+ }
+ break;
+ }
+ n--;
+ }
+ }
+
+ // otherwise, guess a conditional
+ if (rec_c.isNull())
+ {
+ rec_c = constructBestConditional(itpc->second);
+ Assert(!rec_c.isNull());
+ indent("sygus-sui-dt", ind);
+ Trace("sygus-sui-dt")
+ << "PBE: ITE strategy : choose random conditional "
+ << d_tds->sygusToBuiltin(rec_c) << std::endl;
+ }
+ }
+ else
+ {
+ // TODO (#1250) : degenerate case where children have different
+ // types?
+ indent("sygus-sui-dt", ind);
+ Trace("sygus-sui-dt") << "return PBE: failed ITE strategy, "
+ "cannot find a distinguishable condition"
+ << std::endl;
+ }
+ if (!rec_c.isNull())
+ {
+ Assert(ecache_child.d_enum_val_to_index.find(rec_c)
+ != ecache_child.d_enum_val_to_index.end());
+ split_cond_res_index = ecache_child.d_enum_val_to_index[rec_c];
+ split_cond_enum = ce;
+ Assert(split_cond_res_index >= 0);
+ Assert(split_cond_res_index
+ < (int)ecache_child.d_enum_vals_res.size());
+ }
+ }
+ else
+ {
+ rec_c = constructSol(cenum.first, cenum.second, ind + 2);
+ }
+
+ // undo update the context
+ if (strat == strat_ITE && sc > 0)
+ {
+ x.d_vals = prev;
+ }
+ }
+ if (!rec_c.isNull())
+ {
+ dt_children_cons.push_back(rec_c);
+ }
+ else
+ {
+ success = false;
+ break;
+ }
+ }
+ if (success)
+ {
+ Assert(dt_children_cons.size() == etis->d_sol_templ_args.size());
+ // ret_dt = NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR,
+ // dt_children );
+ ret_dt = etis->d_sol_templ;
+ ret_dt = ret_dt.substitute(etis->d_sol_templ_args.begin(),
+ etis->d_sol_templ_args.end(),
+ dt_children_cons.begin(),
+ dt_children_cons.end());
+ indent("sygus-sui-dt-debug", ind);
+ Trace("sygus-sui-dt-debug")
+ << "PBE: success : constructed for strategy " << strat << std::endl;
+ }
+ else
+ {
+ indent("sygus-sui-dt-debug", ind);
+ Trace("sygus-sui-dt-debug")
+ << "PBE: failed for strategy " << strat << std::endl;
+ }
+ }
+ }
+
+ if (!ret_dt.isNull())
+ {
+ Assert(ret_dt.getType() == e.getType());
+ }
+ indent("sygus-sui-dt", ind);
+ Trace("sygus-sui-dt") << "ConstructPBE: returned " << ret_dt << std::endl;
+ return ret_dt;
+}
+
+} /* CVC4::theory::quantifiers namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
--- /dev/null
+/********************* */
+/*! \file sygus_unif_io.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief sygus_unif_io
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_IO_H
+#define __CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_IO_H
+
+#include <map>
+#include "theory/quantifiers/sygus/sygus_unif.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+class SygusUnifIo;
+
+/** Unification context
+ *
+ * This class maintains state information during calls to
+ * SygusUnifIo::constructSolution, which implements unification-based
+ * approaches for constructing solutions to synthesis conjectures.
+ */
+class UnifContextIo : public UnifContext
+{
+ public:
+ UnifContextIo();
+ /** get current role */
+ virtual NodeRole getCurrentRole() override;
+
+ /**
+ * This intiializes this context based on information in sui regarding the
+ * kinds of examples it contains.
+ */
+ void initialize(SygusUnifIo* sui);
+
+ //----------for ITE strategy
+ /** the value of the context conditional
+ *
+ * This stores a list of Boolean constants that is the same length of the
+ * number of input/output example pairs we are considering. For each i,
+ * if d_vals[i] = true, i/o pair #i is active according to this context
+ * if d_vals[i] = false, i/o pair #i is inactive according to this context
+ */
+ std::vector<Node> d_vals;
+ /** update the examples
+ *
+ * if pol=true, this method updates d_vals to d_vals & vals
+ * if pol=false, this method updates d_vals to d_vals & ( ~vals )
+ */
+ bool updateContext(SygusUnifIo* sui, std::vector<Node>& vals, bool pol);
+ //----------end for ITE strategy
+
+ //----------for CONCAT strategies
+ /** the position in the strings
+ *
+ * For each i/o example pair, this stores the length of the current solution
+ * for the input of the pair, where the solution for that input is a prefix
+ * or
+ * suffix of the output of the pair. For example, if our i/o pairs are:
+ * f( "abcd" ) = "abcdcd"
+ * f( "aa" ) = "aacd"
+ * If the solution we have currently constructed is str.++( x1, "c", ... ),
+ * then d_str_pos = ( 5, 3 ), where notice that
+ * str.++( "abc", "c" ) is a prefix of "abcdcd" and
+ * str.++( "aa", "c" ) is a prefix of "aacd".
+ */
+ std::vector<unsigned> d_str_pos;
+ /** update the string examples
+ *
+ * This method updates d_str_pos to d_str_pos + pos, and updates the current
+ * role to nrole.
+ */
+ bool updateStringPosition(SygusUnifIo* sui,
+ std::vector<unsigned>& pos,
+ NodeRole nrole);
+ /** get current strings
+ *
+ * This returns the prefix/suffix of the string constants stored in vals
+ * of size d_str_pos, and stores the result in ex_vals. For example, if vals
+ * is (abcdcd", "aacde") and d_str_pos = ( 5, 3 ), then we add
+ * "d" and "de" to ex_vals.
+ */
+ void getCurrentStrings(SygusUnifIo* sui,
+ const std::vector<Node>& vals,
+ std::vector<String>& ex_vals);
+ /** get string increment
+ *
+ * If this method returns true, then inc and tot are updated such that
+ * for all active indices i,
+ * vals[i] is a prefix (or suffix if isPrefix=false) of ex_vals[i], and
+ * inc[i] = str.len(vals[i])
+ * for all inactive indices i, inc[i] = 0
+ * We set tot to the sum of inc[i] for i=1,...,n. This indicates the total
+ * number of characters incremented across all examples.
+ */
+ bool getStringIncrement(SygusUnifIo* sui,
+ bool isPrefix,
+ const std::vector<String>& ex_vals,
+ const std::vector<Node>& vals,
+ std::vector<unsigned>& inc,
+ unsigned& tot);
+ /** returns true if ex_vals[i] = vals[i] for all active indices i. */
+ bool isStringSolved(SygusUnifIo* sui,
+ const std::vector<String>& ex_vals,
+ const std::vector<Node>& vals);
+ //----------end for CONCAT strategies
+
+ /** visited role
+ *
+ * This is the current set of enumerator/node role pairs we are currently
+ * visiting. This set is cleared when the context is updated.
+ */
+ std::map<Node, std::map<NodeRole, bool> > d_visit_role;
+
+ /** unif context enumerator information */
+ class UEnumInfo
+ {
+ public:
+ UEnumInfo() {}
+ /** map from conditions and branch positions to a solved node
+ *
+ * For example, if we have:
+ * f( 1 ) = 2 ^ f( 3 ) = 4 ^ f( -1 ) = 1
+ * Then, valid entries in this map is:
+ * d_look_ahead_sols[x>0][1] = x+1
+ * d_look_ahead_sols[x>0][2] = 1
+ * For the first entry, notice that for all input examples such that x>0
+ * evaluates to true, which are (1) and (3), we have that their output
+ * values for x+1 under the substitution that maps x to the input value,
+ * resulting in 2 and 4, are equal to the output value for the respective
+ * pairs.
+ */
+ std::map<Node, std::map<unsigned, Node> > d_look_ahead_sols;
+ };
+ /** map from enumerators to the above info class */
+ std::map<Node, UEnumInfo> d_uinfo;
+
+ private:
+ /** true and false nodes */
+ Node d_true;
+ Node d_false;
+ /** current role (see getCurrentRole). */
+ NodeRole d_curr_role;
+};
+
+/** Subsumption trie
+*
+* This class manages a set of terms for a PBE sygus enumerator.
+*
+* In PBE sygus, we are interested in, for each term t, the set of I/O examples
+* that it satisfies, which can be represented by a vector of Booleans.
+* For example, given conjecture:
+* f( 1 ) = 2 ^ f( 3 ) = 4 ^ f( -1 ) = 1 ^ f( 5 ) = 5
+* If solutions for f are of the form (lambda x. [term]), then:
+* Term x satisfies 0001,
+* Term x+1 satisfies 1100,
+* Term 2 satisfies 0100.
+* Above, term 2 is subsumed by term x+1, since the set of I/O examples that
+* x+1 satisfies are a superset of those satisfied by 2.
+*/
+class SubsumeTrie
+{
+ public:
+ SubsumeTrie() {}
+ /**
+ * Adds term t to the trie, removes all terms that are subsumed by t from the
+ * trie and adds them to subsumed. The set of I/O examples that t satisfies
+ * is given by (pol ? vals : !vals).
+ */
+ Node addTerm(Node t,
+ const std::vector<Node>& vals,
+ bool pol,
+ std::vector<Node>& subsumed);
+ /**
+ * Adds term c to the trie, without calculating/updating based on
+ * subsumption. This is useful for using this class to store conditionals
+ * in ITE strategies, where any conditional whose set of vals is unique
+ * (as opposed to not subsumed) is useful.
+ */
+ Node addCond(Node c, const std::vector<Node>& vals, bool pol);
+ /**
+ * Returns the set of terms that are subsumed by (pol ? vals : !vals).
+ */
+ void getSubsumed(const std::vector<Node>& vals,
+ bool pol,
+ std::vector<Node>& subsumed);
+ /**
+ * Returns the set of terms that subsume (pol ? vals : !vals). This
+ * is for instance useful when determining whether there exists a term
+ * that satisfies all active examples in the decision tree learning
+ * algorithm.
+ */
+ void getSubsumedBy(const std::vector<Node>& vals,
+ bool pol,
+ std::vector<Node>& subsumed_by);
+ /**
+ * Get the leaves of the trie, which we store in the map v.
+ * v[-1] stores the children that always evaluate to !pol,
+ * v[1] stores the children that always evaluate to pol,
+ * v[0] stores the children that both evaluate to true and false for at least
+ * one example.
+ */
+ void getLeaves(const std::vector<Node>& vals,
+ bool pol,
+ std::map<int, std::vector<Node> >& v);
+ /** is this trie empty? */
+ bool isEmpty() { return d_term.isNull() && d_children.empty(); }
+ /** clear this trie */
+ void clear()
+ {
+ d_term = Node::null();
+ d_children.clear();
+ }
+
+ private:
+ /** the term at this node */
+ Node d_term;
+ /** the children nodes of this trie */
+ std::map<Node, SubsumeTrie> d_children;
+ /** helper function for above functions */
+ Node addTermInternal(Node t,
+ const std::vector<Node>& vals,
+ bool pol,
+ std::vector<Node>& subsumed,
+ bool spol,
+ unsigned index,
+ int status,
+ bool checkExistsOnly,
+ bool checkSubsume);
+ /** helper function for above functions */
+ void getLeavesInternal(const std::vector<Node>& vals,
+ bool pol,
+ std::map<int, std::vector<Node> >& v,
+ unsigned index,
+ int status);
+};
+
+/** Sygus unification I/O utility
+ *
+ * This class implement synthesis-by-unification, where the specification is
+ * I/O examples. With respect to SygusUnif, it's main interface function is
+ * addExample, which adds an I/O example to the specification.
+ */
+class SygusUnifIo : public SygusUnif
+{
+ friend class UnifContextIo;
+
+ public:
+ SygusUnifIo();
+ ~SygusUnifIo();
+
+ /** initialize */
+ virtual void initialize(QuantifiersEngine* qe,
+ Node f,
+ std::vector<Node>& enums,
+ std::vector<Node>& lemmas) override;
+ /** Notify enumeration */
+ virtual void notifyEnumeration(Node e,
+ Node v,
+ std::vector<Node>& lemmas) override;
+
+ /** add example
+ *
+ * This adds input -> output to the specification for f. The arity of
+ * input should be equal to the number of arguments in the sygus variable
+ * list of the grammar of f. That is, if we are searching for solutions for f
+ * of the form (lambda v1...vn. t), then the arity of input should be n.
+ */
+ void addExample(const std::vector<Node>& input, Node output);
+
+ protected:
+ /** true and false nodes */
+ Node d_true;
+ Node d_false;
+ /** input of I/O examples */
+ std::vector<std::vector<Node> > d_examples;
+ /** output of I/O examples */
+ std::vector<Node> d_examples_out;
+
+ /**
+ * This class stores information regarding an enumerator, including:
+ * a database of values that have been enumerated for this enumerator.
+ */
+ class EnumCache
+ {
+ public:
+ EnumCache() {}
+ /**
+ * Notify this class that the term v has been enumerated for this enumerator.
+ * Its evaluation under the set of examples in sui are stored in results.
+ */
+ void addEnumValue(Node v, std::vector<Node>& results);
+ /**
+ * Notify this class that slv is the complete solution to the synthesis
+ * conjecture. This occurs rarely, for instance, when during an ITE strategy
+ * we find that a single enumerated term covers all examples.
+ */
+ void setSolved(Node slv) { d_enum_solved = slv; }
+ /** Have we been notified that a complete solution exists? */
+ bool isSolved() { return !d_enum_solved.isNull(); }
+ /** Get the complete solution to the synthesis conjecture. */
+ Node getSolved() { return d_enum_solved; }
+ /** Values that have been enumerated for this enumerator */
+ std::vector<Node> d_enum_vals;
+ /**
+ * This either stores the values of f( I ) for inputs
+ * or the value of f( I ) = O if d_role==enum_io
+ */
+ std::vector<std::vector<Node> > d_enum_vals_res;
+ /**
+ * The set of values in d_enum_vals that have been "subsumed" by others
+ * (see SubsumeTrie for explanation of subsumed).
+ */
+ std::vector<Node> d_enum_subsume;
+ /** Map from values to their index in d_enum_vals. */
+ std::map<Node, unsigned> d_enum_val_to_index;
+ /**
+ * A subsumption trie containing the values in d_enum_vals. Depending on the
+ * role of this enumerator, values may either be added to d_term_trie with
+ * subsumption (if role=enum_io), or without (if role=enum_ite_condition or
+ * enum_concat_term).
+ */
+ SubsumeTrie d_term_trie;
+
+ private:
+ /**
+ * Whether an enumerated value for this conjecture has solved the entire
+ * conjecture.
+ */
+ Node d_enum_solved;
+ };
+ /** maps enumerators to the information above */
+ std::map<Node, EnumCache> d_ecache;
+
+ /** domain-specific enumerator exclusion techniques
+ *
+ * Returns true if the value v for e can be excluded based on a
+ * domain-specific exclusion technique like the ones below.
+ *
+ * results : the values of v under the input examples,
+ * exp : if this function returns true, then exp contains a (possibly
+ * generalize) explanation for why v can be excluded.
+ */
+ bool getExplanationForEnumeratorExclude(Node e,
+ Node v,
+ std::vector<Node>& results,
+ std::vector<Node>& exp);
+ /** returns true if we can exlude values of e based on negative str.contains
+ *
+ * Values v for e may be excluded if we realize that the value of v under the
+ * substitution for some input example will never be contained in some output
+ * example. For details on this technique, see NegContainsSygusInvarianceTest
+ * in sygus_invariance.h.
+ *
+ * This function depends on whether e is being used to enumerate values
+ * for any node that is conditional in the strategy graph. For example,
+ * nodes that are children of ITE strategy nodes are conditional. If any node
+ * is conditional, then this function returns false.
+ */
+ bool useStrContainsEnumeratorExclude(Node e);
+ /** cache for the above function */
+ std::map<Node, bool> d_use_str_contains_eexc;
+
+ /** the unification context used within constructSolution */
+ UnifContextIo d_context;
+ /** initialize construct solution */
+ void initializeConstructSol() override;
+ /** construct solution */
+ Node constructSol(Node e, NodeRole nrole, int ind) override;
+};
+
+} /* CVC4::theory::quantifiers namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_IO_H */
}
void EnumInfo::initialize(EnumRole role) { d_role = role; }
-bool EnumTypeInfoStrat::isValid(UnifContext* x)
+bool EnumTypeInfoStrat::isValid(UnifContext& x)
{
- if ((x->d_has_string_pos == role_string_prefix
+ if ((x.getCurrentRole() == role_string_prefix
&& d_this == strat_CONCAT_SUFFIX)
- || (x->d_has_string_pos == role_string_suffix
+ || (x.getCurrentRole() == role_string_suffix
&& d_this == strat_CONCAT_PREFIX))
{
return false;
};
std::ostream& operator<<(std::ostream& os, StrategyType st);
-class UnifContext;
+/** virtual base class for context in synthesis-by-unification approaches */
+class UnifContext
+{
+ public:
+ /** Get the current role
+ *
+ * In a particular context when constructing solutions in synthesis by
+ * unification, we may be solving based on a modified role. For example,
+ * if we are currently synthesizing x in a solution ("a" ++ x), we are
+ * synthesizing the string suffix of the overall solution. In this case, this
+ * function returns role_string_suffix.
+ */
+ virtual NodeRole getCurrentRole() = 0;
+ /** is return value modified?
+ *
+ * This returns true if we are currently in a state where the return value
+ * of the solution has been modified, e.g. by a previous node that solved
+ * for a string prefix.
+ */
+ bool isReturnValueModified() { return getCurrentRole() != role_equal; }
+};
/**
* This class stores information regarding an enumerator, including
/** the template for the solution */
Node d_sol_templ;
/** Returns true if argument is valid strategy in unification context x */
- bool isValid(UnifContext* x);
+ bool isValid(UnifContext& x);
};
/**
projects / cvc5.git / commitdiff