diff options
Diffstat (limited to 'src/theory/quantifiers/sygus/sygus_unif_strat.cpp')
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_unif_strat.cpp | 271 |
1 files changed, 166 insertions, 105 deletions
diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp index 86efffd1f..d3a5d6c23 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp @@ -80,8 +80,7 @@ std::ostream& operator<<(std::ostream& os, StrategyType st) void SygusUnifStrategy::initialize(QuantifiersEngine* qe, Node f, - std::vector<Node>& enums, - std::vector<Node>& lemmas) + std::vector<Node>& enums) { Assert(d_candidate.isNull()); d_candidate = f; @@ -92,8 +91,10 @@ void SygusUnifStrategy::initialize(QuantifiersEngine* qe, collectEnumeratorTypes(d_root, role_equal); // add the enumerators enums.insert(enums.end(), d_esym_list.begin(), d_esym_list.end()); - // learn redundant ops - staticLearnRedundantOps(lemmas); + // finish the initialization of the strategy + // this computes if each node is conditional + std::map<Node, std::map<NodeRole, bool> > visited; + finishInit(getRootEnumerator(), role_equal, visited, false); } void SygusUnifStrategy::initializeType(TypeNode tn) @@ -101,10 +102,13 @@ void SygusUnifStrategy::initializeType(TypeNode tn) d_tinfo[tn].d_this_type = tn; } -Node SygusUnifStrategy::getRootEnumerator() +Node SygusUnifStrategy::getRootEnumerator() const { - std::map<EnumRole, Node>::iterator it = d_tinfo[d_root].d_enum.find(enum_io); - Assert(it != d_tinfo[d_root].d_enum.end()); + std::map<TypeNode, EnumTypeInfo>::const_iterator itt = d_tinfo.find(d_root); + Assert(itt != d_tinfo.end()); + std::map<EnumRole, Node>::const_iterator it = + itt->second.d_enum.find(enum_io); + Assert(it != itt->second.d_enum.end()); return it->second; } @@ -702,10 +706,10 @@ void SygusUnifStrategy::staticLearnRedundantOps(std::vector<Node>& lemmas) Trace("sygus-unif") << std::endl; Trace("sygus-unif") << "Strategy for candidate " << d_candidate << " is : " << std::endl; + debugPrint("sygus-unif"); std::map<Node, std::map<NodeRole, bool> > visited; std::map<Node, std::map<unsigned, bool> > needs_cons; - staticLearnRedundantOps( - getRootEnumerator(), role_equal, visited, needs_cons, 0, false); + staticLearnRedundantOps(getRootEnumerator(), role_equal, visited, needs_cons); // now, check the needs_cons map for (std::pair<const Node, std::map<unsigned, bool> >& nce : needs_cons) { @@ -730,124 +734,181 @@ void SygusUnifStrategy::staticLearnRedundantOps(std::vector<Node>& lemmas) } } +void SygusUnifStrategy::debugPrint(const char* c) +{ + if (Trace.isOn(c)) + { + std::map<Node, std::map<NodeRole, bool> > visited; + debugPrint(c, getRootEnumerator(), role_equal, visited, 0); + } +} + void SygusUnifStrategy::staticLearnRedundantOps( Node e, NodeRole nrole, std::map<Node, std::map<NodeRole, bool> >& visited, - std::map<Node, std::map<unsigned, bool> >& needs_cons, - int ind, - bool isCond) + std::map<Node, std::map<unsigned, bool> >& needs_cons) { - std::map<Node, EnumInfo>::iterator itn = d_einfo.find(e); - Assert(itn != d_einfo.end()); - - if (visited[e].find(nrole) == visited[e].end() - || (isCond && !itn->second.isConditional())) + if (visited[e].find(nrole) != visited[e].end()) + { + return; + } + visited[e][nrole] = true; + EnumInfo& ei = getEnumInfo(e); + if (ei.isTemplated()) { - visited[e][nrole] = true; - // if conditional - if (isCond) + return; + } + TypeNode etn = e.getType(); + EnumTypeInfo& tinfo = getEnumTypeInfo(etn); + StrategyNode& snode = tinfo.getStrategyNode(nrole); + if (snode.d_strats.empty()) + { + return; + } + std::map<unsigned, bool> needs_cons_curr; + // various strategies + for (unsigned j = 0, size = snode.d_strats.size(); j < size; j++) + { + EnumTypeInfoStrat* etis = snode.d_strats[j]; + int cindex = Datatype::indexOf(etis->d_cons.toExpr()); + Assert(cindex != -1); + needs_cons_curr[static_cast<unsigned>(cindex)] = false; + for (std::pair<Node, NodeRole>& cec : etis->d_cenum) { - itn->second.setConditional(); + staticLearnRedundantOps(cec.first, cec.second, visited, needs_cons); } - indent("sygus-unif", ind); - Trace("sygus-unif") << e << " :: node role : " << nrole; - Trace("sygus-unif") - << ", type : " - << ((DatatypeType)e.getType().toType()).getDatatype().getName(); - if (isCond) + } + // get the master enumerator for the type of this enumerator + std::map<TypeNode, Node>::iterator itse = d_master_enum.find(etn); + if (itse == d_master_enum.end()) + { + return; + } + Node em = itse->second; + Assert(!em.isNull()); + // get the current datatype + const Datatype& dt = static_cast<DatatypeType>(etn.toType()).getDatatype(); + // all constructors that are not a part of a strategy are needed + for (unsigned j = 0, size = dt.getNumConstructors(); j < size; j++) + { + if (needs_cons_curr.find(j) == needs_cons_curr.end()) { - Trace("sygus-unif") << ", conditional"; + needs_cons_curr[j] = true; } - Trace("sygus-unif") << ", enum role : " << itn->second.getRole(); - - if (itn->second.isTemplated()) + } + // update the constructors that the master enumerator needs + if (needs_cons.find(em) == needs_cons.end()) + { + needs_cons[em] = needs_cons_curr; + } + else + { + for (unsigned j = 0, size = dt.getNumConstructors(); j < size; j++) { - Trace("sygus-unif") << ", templated : (lambda " - << itn->second.d_template_arg << " " - << itn->second.d_template << ")" << std::endl; + needs_cons[em][j] = needs_cons[em][j] || needs_cons_curr[j]; } - else + } +} + +void SygusUnifStrategy::finishInit( + Node e, + NodeRole nrole, + std::map<Node, std::map<NodeRole, bool> >& visited, + bool isCond) +{ + EnumInfo& ei = getEnumInfo(e); + if (visited[e].find(nrole) != visited[e].end() + && (!isCond || ei.isConditional())) + { + return; + } + visited[e][nrole] = true; + // set conditional + if (isCond) + { + ei.setConditional(); + } + if (ei.isTemplated()) + { + return; + } + TypeNode etn = e.getType(); + EnumTypeInfo& tinfo = getEnumTypeInfo(etn); + StrategyNode& snode = tinfo.getStrategyNode(nrole); + for (unsigned j = 0, size = snode.d_strats.size(); j < size; j++) + { + EnumTypeInfoStrat* etis = snode.d_strats[j]; + StrategyType strat = etis->d_this; + bool newIsCond = isCond || strat == strat_ITE; + for (std::pair<Node, NodeRole>& cec : etis->d_cenum) { - Trace("sygus-unif") << std::endl; - TypeNode etn = e.getType(); + finishInit(cec.first, cec.second, visited, newIsCond); + } + } +} - // enumerator type info - std::map<TypeNode, EnumTypeInfo>::iterator itt = d_tinfo.find(etn); - Assert(itt != d_tinfo.end()); - EnumTypeInfo& tinfo = itt->second; +void SygusUnifStrategy::debugPrint( + const char* c, + Node e, + NodeRole nrole, + std::map<Node, std::map<NodeRole, bool> >& visited, + int ind) +{ + if (visited[e].find(nrole) != visited[e].end()) + { + indent(c, ind); + Trace(c) << e << " :: node role : " << nrole << std::endl; + return; + } + visited[e][nrole] = true; + EnumInfo& ei = getEnumInfo(e); - // strategy info - std::map<NodeRole, StrategyNode>::iterator itsn = - tinfo.d_snodes.find(nrole); - Assert(itsn != tinfo.d_snodes.end()); - StrategyNode& snode = itsn->second; + TypeNode etn = e.getType(); - if (snode.d_strats.empty()) - { - return; - } - std::map<unsigned, bool> needs_cons_curr; - // various strategies - for (unsigned j = 0, size = snode.d_strats.size(); j < size; j++) - { - EnumTypeInfoStrat* etis = snode.d_strats[j]; - StrategyType strat = etis->d_this; - bool newIsCond = isCond || strat == strat_ITE; - indent("sygus-unif", ind + 1); - Trace("sygus-unif") << "Strategy : " << strat - << ", from cons : " << etis->d_cons << std::endl; - int cindex = Datatype::indexOf(etis->d_cons.toExpr()); - Assert(cindex != -1); - needs_cons_curr[static_cast<unsigned>(cindex)] = false; - for (std::pair<Node, NodeRole>& cec : etis->d_cenum) - { - // recurse - staticLearnRedundantOps( - cec.first, cec.second, visited, needs_cons, ind + 2, newIsCond); - } - } - // get the master enumerator for the type of this enumerator - std::map<TypeNode, Node>::iterator itse = d_master_enum.find(etn); - if (itse == d_master_enum.end()) - { - return; - } - Node em = itse->second; - Assert(!em.isNull()); - // get the current datatype - const Datatype& dt = - static_cast<DatatypeType>(etn.toType()).getDatatype(); - // all constructors that are not a part of a strategy are needed - for (unsigned j = 0, size = dt.getNumConstructors(); j < size; j++) - { - if (needs_cons_curr.find(j) == needs_cons_curr.end()) - { - needs_cons_curr[j] = true; - } - } - // update the constructors that the master enumerator needs - if (needs_cons.find(em) == needs_cons.end()) - { - needs_cons[em] = needs_cons_curr; - } - else - { - for (unsigned j = 0, size = dt.getNumConstructors(); j < size; j++) - { - needs_cons[em][j] = needs_cons[em][j] || needs_cons_curr[j]; - } - } - } + indent(c, ind); + Trace(c) << e << " :: node role : " << nrole; + Trace(c) << ", type : " + << static_cast<DatatypeType>(etn.toType()).getDatatype().getName(); + if (ei.isConditional()) + { + Trace(c) << ", conditional"; } - else + Trace(c) << ", enum role : " << ei.getRole(); + + if (ei.isTemplated()) + { + Trace(c) << ", templated : (lambda " << ei.d_template_arg << " " + << ei.d_template << ")"; + } + Trace(c) << std::endl; + + EnumTypeInfo& tinfo = getEnumTypeInfo(etn); + StrategyNode& snode = tinfo.getStrategyNode(nrole); + for (unsigned j = 0, size = snode.d_strats.size(); j < size; j++) { - indent("sygus-unif", ind); - Trace("sygus-unif") << e << " :: node role : " << nrole << std::endl; + EnumTypeInfoStrat* etis = snode.d_strats[j]; + StrategyType strat = etis->d_this; + indent(c, ind + 1); + Trace(c) << "Strategy : " << strat << ", from cons : " << etis->d_cons + << std::endl; + for (std::pair<Node, NodeRole>& cec : etis->d_cenum) + { + // recurse + debugPrint(c, cec.first, cec.second, visited, ind + 2); + } } } void EnumInfo::initialize(EnumRole role) { d_role = role; } + +StrategyNode& EnumTypeInfo::getStrategyNode(NodeRole nrole) +{ + std::map<NodeRole, StrategyNode>::iterator it = d_snodes.find(nrole); + Assert(it != d_snodes.end()); + return it->second; +} + bool EnumTypeInfoStrat::isValid(UnifContext& x) { if ((x.getCurrentRole() == role_string_prefix |