return (*this)[name].getSelector();
}
+Type DatatypeConstructor::getArgType(unsigned index) const
+{
+ PrettyCheckArgument(index < getNumArgs(), index, "index out of bounds");
+ return static_cast<SelectorType>((*this)[index].getType()).getRangeType();
+}
+
bool DatatypeConstructor::involvesExternalType() const{
for(const_iterator i = begin(); i != end(); ++i) {
if(! SelectorType((*i).getSelector().getType()).getRangeType().isDatatype()) {
* 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
*
std::map<Node, std::vector<Node>> 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<const Node, std::vector<Node>>& 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<TypeNode, std::vector<Node>> tn_to_strategy_pt;
+ for (const std::pair<const Node, std::vector<Node>>& 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<TypeNode, std::vector<Node>>::iterator itt =
+ tn_to_strategy_pt.find(etn);
+ if (itt != tn_to_strategy_pt.end())
+ {
+ std::vector<Node> disj;
+ for (const Node& sp : itt->second)
+ {
+ std::map<Node, std::vector<Node>>::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;
{
return;
}
+ Trace("sygus-strat-slearn") << "Learn redundant operators " << e << " "
+ << nrole << "..." << std::endl;
visited[e][nrole] = true;
EnumInfo& ei = getEnumInfo(e);
if (ei.isTemplated())
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
+ // 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<unsigned>(cindex)] = false;
for (std::pair<Node, NodeRole>& cec : etis->d_cenum)
{
staticLearnRedundantOps(cec.first, cec.second, visited, needs_cons);
}
}
- // 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
+ // 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())
}
}
// 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];
}
}
}
}
}
-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<SelectorType>(c[i].getType()).getRangeType());
}
/** get first occurrence */
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 */
projects / cvc5.git / commitdiff