From 2ac2c2a0c6ab1318736c026dfeb7533b5ffc7f29 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 10 May 2018 17:43:48 -0500 Subject: [PATCH] Exclude Boolean connectives from ITE conditions in SygusUnifStrat (#1900) --- src/expr/datatype.cpp | 6 ++ src/expr/datatype.h | 5 ++ src/theory/quantifiers/sygus/sygus_pbe.cpp | 46 ++++++++++++-- .../quantifiers/sygus/sygus_unif_strat.cpp | 63 ++++++++++++++----- .../quantifiers/sygus/term_database_sygus.cpp | 5 +- .../quantifiers/sygus/term_database_sygus.h | 2 +- 6 files changed, 102 insertions(+), 25 deletions(-) diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp index bcd3a0784..d697a6aaf 100644 --- a/src/expr/datatype.cpp +++ b/src/expr/datatype.cpp @@ -1141,6 +1141,12 @@ Expr DatatypeConstructor::getSelector(std::string name) const { return (*this)[name].getSelector(); } +Type DatatypeConstructor::getArgType(unsigned index) const +{ + PrettyCheckArgument(index < getNumArgs(), index, "index out of bounds"); + return static_cast((*this)[index].getType()).getRangeType(); +} + bool DatatypeConstructor::involvesExternalType() const{ for(const_iterator i = begin(); i != end(); ++i) { if(! SelectorType((*i).getSelector().getType()).getRangeType().isDatatype()) { diff --git a/src/expr/datatype.h b/src/expr/datatype.h index fffabac77..826711897 100644 --- a/src/expr/datatype.h +++ b/src/expr/datatype.h @@ -390,6 +390,11 @@ class CVC4_PUBLIC DatatypeConstructor { * is returned. */ Expr getSelector(std::string name) const; + /** + * Get argument type. Returns the return type of the i^th selector of this + * constructor. + */ + Type getArgType(unsigned i) const; /** get selector internal * diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp index 7faeb0252..401ab03ee 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.cpp +++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp @@ -179,21 +179,57 @@ bool CegConjecturePbe::initialize(Node n, std::map> strategy_lemmas; d_sygus_unif[c].initialize( d_qe, singleton_c, d_candidate_to_enum[c], strategy_lemmas); - // collect lemmas from all strategies - for (const std::pair>& p : strategy_lemmas) - { - lemmas.insert(lemmas.end(), p.second.begin(), p.second.end()); - } Assert(!d_candidate_to_enum[c].empty()); Trace("sygus-pbe") << "Initialize " << d_candidate_to_enum[c].size() << " enumerators for " << c << "..." << std::endl; + // collect list per type of strategy points with strategy lemmas + std::map> tn_to_strategy_pt; + for (const std::pair>& p : strategy_lemmas) + { + TypeNode tnsp = p.first.getType(); + tn_to_strategy_pt[tnsp].push_back(p.first); + } // initialize the enumerators + NodeManager* nm = NodeManager::currentNM(); for (const Node& e : d_candidate_to_enum[c]) { + TypeNode etn = e.getType(); d_tds->registerEnumerator(e, c, d_parent, true); Node g = d_tds->getActiveGuardForEnumerator(e); d_enum_to_active_guard[e] = g; d_enum_to_candidate[e] = c; + TNode te = e; + // initialize static symmetry breaking lemmas for it + // we register only one "master" enumerator per type + // thus, the strategy lemmas (which are for individual strategy points) + // are applicable (disjunctively) to the master enumerator + std::map>::iterator itt = + tn_to_strategy_pt.find(etn); + if (itt != tn_to_strategy_pt.end()) + { + std::vector disj; + for (const Node& sp : itt->second) + { + std::map>::iterator itsl = + strategy_lemmas.find(sp); + Assert(itsl != strategy_lemmas.end()); + if (!itsl->second.empty()) + { + TNode tsp = sp; + Node lem = itsl->second.size() == 1 ? itsl->second[0] + : nm->mkNode(AND, itsl->second); + if (tsp != te) + { + lem = lem.substitute(tsp, te); + } + disj.push_back(lem); + } + } + Node lem = disj.size() == 1 ? disj[0] : nm->mkNode(OR, disj); + Trace("sygus-pbe") << " static redundant op lemma : " << lem + << std::endl; + lemmas.push_back(lem); + } } Trace("sygus-pbe") << "Initialize " << d_examples[c].size() << " example points for " << c << "..." << std::endl; diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp index a3158fbe8..32af47c81 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp @@ -760,6 +760,8 @@ void SygusUnifStrategy::staticLearnRedundantOps( { return; } + Trace("sygus-strat-slearn") << "Learn redundant operators " << e << " " + << nrole << "..." << std::endl; visited[e][nrole] = true; EnumInfo& ei = getEnumInfo(e); if (ei.isTemplated()) @@ -769,34 +771,61 @@ void SygusUnifStrategy::staticLearnRedundantOps( TypeNode etn = e.getType(); EnumTypeInfo& tinfo = getEnumTypeInfo(etn); StrategyNode& snode = tinfo.getStrategyNode(nrole); - if (snode.d_strats.empty()) - { - return; - } std::map needs_cons_curr; - // various strategies + // constructors that correspond to strategies are not needed + // the intuition is that the strategy itself is responsible for constructing + // all terms that use the given constructor 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); + Trace("sygus-strat-slearn") + << "...by strategy, can exclude operator " << etis->d_cons << std::endl; needs_cons_curr[static_cast(cindex)] = false; for (std::pair& cec : etis->d_cenum) { staticLearnRedundantOps(cec.first, cec.second, visited, needs_cons); } } - // get the master enumerator for the type of this enumerator - std::map::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(etn.toType()).getDatatype(); - // all constructors that are not a part of a strategy are needed + // do not use recursive Boolean connectives for conditions of ITEs + if (nrole == role_ite_condition) + { + for (unsigned j = 0, size = dt.getNumConstructors(); j < size; j++) + { + Node op = Node::fromExpr(dt[j].getSygusOp()); + Trace("sygus-strat-slearn") + << "...for ite condition, look at operator : " << op << std::endl; + if (op.getKind() == kind::BUILTIN) + { + Kind k = NodeManager::operatorToKind(op); + if (k == NOT || k == OR || k == AND) + { + // can eliminate if their argument types are simple loops to this type + bool type_ok = true; + for (unsigned k = 0, nargs = dt[j].getNumArgs(); k < nargs; k++) + { + TypeNode tn = TypeNode::fromType(dt[j].getArgType(k)); + if (tn != etn) + { + type_ok = false; + break; + } + } + if (type_ok) + { + Trace("sygus-strat-slearn") + << "...for ite condition, can exclude Boolean connective : " + << op << std::endl; + needs_cons_curr[j] = false; + } + } + } + } + } + // all other constructors are needed for (unsigned j = 0, size = dt.getNumConstructors(); j < size; j++) { if (needs_cons_curr.find(j) == needs_cons_curr.end()) @@ -805,15 +834,15 @@ void SygusUnifStrategy::staticLearnRedundantOps( } } // update the constructors that the master enumerator needs - if (needs_cons.find(em) == needs_cons.end()) + if (needs_cons.find(e) == needs_cons.end()) { - needs_cons[em] = needs_cons_curr; + needs_cons[e] = 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]; + needs_cons[e][j] = needs_cons[e][j] || needs_cons_curr[j]; } } } diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index 3121a4253..c45d4971e 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -1028,10 +1028,11 @@ bool TermDbSygus::isConstArg( TypeNode tn, int i ) { } } -TypeNode TermDbSygus::getArgType(const DatatypeConstructor& c, unsigned i) +TypeNode TermDbSygus::getArgType(const DatatypeConstructor& c, unsigned i) const { Assert(i < c.getNumArgs()); - return TypeNode::fromType( ((SelectorType)c[i].getType()).getRangeType() ); + return TypeNode::fromType( + static_cast(c[i].getType()).getRangeType()); } /** get first occurrence */ diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h index f108dfb8e..4a3dcb8d6 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.h +++ b/src/theory/quantifiers/sygus/term_database_sygus.h @@ -292,7 +292,7 @@ private: bool isKindArg( TypeNode tn, int i ); bool isConstArg( TypeNode tn, int i ); /** get arg type */ - TypeNode getArgType(const DatatypeConstructor& c, unsigned i); + TypeNode getArgType(const DatatypeConstructor& c, unsigned i) const; /** get first occurrence */ int getFirstArgOccurrence( const DatatypeConstructor& c, TypeNode tn ); /** is type match */ -- 2.30.2