theory/quantifiers/sygus/synth_engine.h
theory/quantifiers/sygus/term_database_sygus.cpp
theory/quantifiers/sygus/term_database_sygus.h
+ theory/quantifiers/sygus/type_info.cpp
+ theory/quantifiers/sygus/type_info.h
+ theory/quantifiers/sygus/type_node_id_trie.cpp
+ theory/quantifiers/sygus/type_node_id_trie.h
theory/quantifiers/sygus/transition_inference.cpp
theory/quantifiers/sygus/transition_inference.h
theory/quantifiers/sygus_sampler.cpp
if( options::sygusFair()==SYGUS_FAIR_DIRECT ){
if( dt[tindex].getNumArgs()>0 ){
+ quantifiers::SygusTypeInfo& nti = d_tds->getTypeInfo(ntn);
// consider lower bounds for size of types
- unsigned lb_add = d_tds->getMinConsTermSize( ntn, tindex );
- unsigned lb_rem = n==a ? 0 : d_tds->getMinTermSize( ntn );
+ unsigned lb_add = nti.getMinConsTermSize(tindex);
+ unsigned lb_rem = n == a ? 0 : nti.getMinTermSize();
Assert( lb_add>=lb_rem );
d_currTermSize[a].set( d_currTermSize[a].get() + ( lb_add - lb_rem ) );
}
<< "Simple symmetry breaking for " << dt.getName() << ", constructor "
<< dt[tindex].getName() << ", at depth " << depth << std::endl;
+ quantifiers::SygusTypeInfo& ti = d_tds->getTypeInfo(tn);
// get the sygus operator
Node sop = Node::fromExpr(dt[tindex].getSygusOp());
// get the kind of the constructor operator
- Kind nk = d_tds->getConsNumKind(tn, tindex);
+ Kind nk = ti.getConsNumKind(tindex);
// is this the any-constant constructor?
bool isAnyConstant = sop.getAttribute(SygusAnyConstAttribute());
// for each variable in the sygus type
for (const Node& var : svl)
{
- unsigned sc = d_tds->getSubclassForVar(etn, var);
- if (d_tds->getNumSubclassVars(etn, sc) == 1)
+ quantifiers::SygusTypeInfo& eti = d_tds->getTypeInfo(etn);
+ unsigned sc = eti.getSubclassForVar(var);
+ if (eti.getNumSubclassVars(sc) == 1)
{
// unique variable in singleton subclass, skip
continue;
// Compute the "predecessor" variable in the subclass of var.
Node predVar;
unsigned scindex = 0;
- if (d_tds->getIndexInSubclassForVar(etn, var, scindex))
+ if (eti.getIndexInSubclassForVar(var, scindex))
{
if (scindex > 0)
{
- predVar = d_tds->getVarSubclassIndex(etn, sc, scindex - 1);
+ predVar = eti.getVarSubclassIndex(sc, scindex - 1);
}
}
Node preParentOp = getTraversalPredicate(tn, var, true);
Node finish = nm->mkNode(APPLY_UF, postParent, n);
// check if we are constructing the symmetry breaking predicate for the
// variable in question. If so, is-{x_i}( z ) is true.
- int varCn = d_tds->getOpConsNum(tn, var);
+ int varCn = ti.getOpConsNum(var);
if (varCn == static_cast<int>(tindex))
{
// the post value is true
// cannot do division since we have to consider when both are zero
if (!req_const.isNull())
{
- if (d_tds->hasConst(tn, req_const))
+ if (ti.hasConst(req_const))
{
argDeq = true;
}
bool exp_not_all_const_valid = dt_index_nargs > 0;
// does the parent have an any constant constructor?
bool usingAnyConstCons =
- usingSymCons && (d_tds->getAnyConstantConsNum(tn) != -1);
+ usingSymCons && (ti.getAnyConstantConsNum() != -1);
for (unsigned j = 0; j < dt_index_nargs; j++)
{
Node nc = children[j];
continue;
}
TypeNode tnc = nc.getType();
- int anyc_cons_num = d_tds->getAnyConstantConsNum(tnc);
+ quantifiers::SygusTypeInfo& cti = d_tds->getTypeInfo(tnc);
+ int anyc_cons_num = cti.getAnyConstantConsNum();
const Datatype& cdt =
static_cast<DatatypeType>(tnc.toType()).getDatatype();
std::vector<Node> exp_const;
for (unsigned k = 0, ncons = cdt.getNumConstructors(); k < ncons; k++)
{
- Kind nck = d_tds->getConsNumKind(tnc, k);
+ Kind nck = cti.getConsNumKind(k);
bool red = false;
Node tester = DatatypesRewriter::mkTester(nc, k, cdt);
// check if the argument is redundant
}
else
{
- Node cc = d_tds->getConsNumConst(tnc, k);
+ Node cc = cti.getConsNumConst(k);
if (!cc.isNull())
{
Trace("sygus-sb-simple-debug")
// variables occur pre-traversal at top-level
Node varList = Node::fromExpr(dt.getSygusVarList());
std::vector<Node> constraints;
+ quantifiers::SygusTypeInfo& eti = d_tds->getTypeInfo(etn);
for (const Node& v : varList)
{
- unsigned sc = d_tds->getSubclassForVar(etn, v);
+ unsigned sc = eti.getSubclassForVar(v);
// no symmetry breaking occurs for variables in singleton subclasses
- if (d_tds->getNumSubclassVars(etn, sc) > 1)
+ if (eti.getNumSubclassVars(sc) > 1)
{
Node preRootOp = getTraversalPredicate(etn, v, true);
Node preRoot = nm->mkNode(APPLY_UF, preRootOp, e);
{
if (!d_req_const.isNull())
{
- if (!tdb->hasConst(tn, d_req_const))
+ quantifiers::SygusTypeInfo& sti = tdb->getTypeInfo(tn);
+ if (!sti.hasConst(d_req_const))
{
return false;
}
{
const Datatype& pdt = ((DatatypeType)(tnp).toType()).getDatatype();
const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
- Assert(d_tds->hasKind(tn, k));
- Assert(d_tds->hasKind(tnp, pk));
+ quantifiers::SygusTypeInfo& ti = d_tds->getTypeInfo(tn);
+ quantifiers::SygusTypeInfo& pti = d_tds->getTypeInfo(tnp);
+ Assert(ti.hasKind(k));
+ Assert(pti.hasKind(pk));
Trace("sygus-sb-debug") << "Consider sygus arg kind " << k << ", pk = " << pk
<< ", arg = " << arg << " in " << tnp << "?"
<< std::endl;
- int c = d_tds->getKindConsNum(tn, k);
- int pc = d_tds->getKindConsNum(tnp, pk);
+ int c = ti.getKindConsNum(k);
+ int pc = pti.getKindConsNum(pk);
// check for associativity
if (k == pk && quantifiers::TermUtil::isAssoc(k))
{
}
if (!rt.empty() && (reqk != UNDEFINED_KIND || !reqkc.empty()))
{
- int pcr = d_tds->getKindConsNum(tnp, rt.d_req_kind);
+ int pcr = pti.getKindConsNum(rt.d_req_kind);
if (pcr != -1)
{
Assert(pcr < static_cast<int>(pdt.getNumConstructors()));
return false;
}
// this can probably be made child grammar independent
- int pc = d_tds->getKindConsNum(tnp, pk);
+ quantifiers::SygusTypeInfo& ti = d_tds->getTypeInfo(tn);
+ quantifiers::SygusTypeInfo& pti = d_tds->getTypeInfo(tnp);
+ int pc = pti.getKindConsNum(pk);
if (pdt[pc].getNumArgs() == 2)
{
Kind ok;
{
Trace("sygus-sb-simple-debug")
<< pk << " has offset arg " << ok << " " << offset << std::endl;
- int ok_arg = d_tds->getKindConsNum(tnp, ok);
+ int ok_arg = pti.getKindConsNum(ok);
if (ok_arg != -1)
{
Trace("sygus-sb-simple-debug")
<< ", status=" << status << std::endl;
if (status == 0 && !co.isNull())
{
- if (d_tds->hasConst(tn, co))
+ if (ti.hasConst(co))
{
Trace("sygus-sb-simple")
<< " sb-simple : by offset reasoning, do not consider const "
bool SygusSimpleSymBreak::considerConst(
const Datatype& pdt, TypeNode tnp, Node c, Kind pk, int arg)
{
- Assert(d_tds->hasKind(tnp, pk));
- int pc = d_tds->getKindConsNum(tnp, pk);
+ quantifiers::SygusTypeInfo& pti = d_tds->getTypeInfo(tnp);
+ Assert(pti.hasKind(pk));
+ int pc = pti.getKindConsNum(pk);
bool ret = true;
Trace("sygus-sb-debug") << "Consider sygus const " << c << ", parent = " << pk
<< ", arg = " << arg << "?" << std::endl;
Node sc = d_tutil->isSingularArg(c, pk, arg);
if (!sc.isNull())
{
- if (d_tds->hasConst(tnp, sc))
+ if (pti.hasConst(sc))
{
Trace("sygus-sb-simple")
<< " sb-simple : " << c << " is singular arg " << arg << " of "
d_rcons_to_status[stn][t] = -1;
TypeNode tn = t.getType();
Assert( stn.isDatatype() );
- const Datatype& dt = ((DatatypeType)(stn).toType()).getDatatype();
+ const Datatype& dt = stn.getDatatype();
+ TermDbSygus* tds = d_qe->getTermDatabaseSygus();
+ SygusTypeInfo& sti = tds->getTypeInfo(stn);
Assert( dt.isSygus() );
Trace("csi-rcons-debug") << "Check reconstruct " << t << ", sygus type " << dt.getName() << ", kind " << t.getKind() << ", id : " << id << std::endl;
int carg = -1;
Node min_t = minimizeBuiltinTerm(t);
Trace("csi-rcons-debug") << "Minimized term is : " << min_t << std::endl;
//check if op is in syntax sort
- carg = d_qe->getTermDatabaseSygus()->getOpConsNum( stn, min_t );
+
+ carg = sti.getOpConsNum(min_t);
if( carg!=-1 ){
Trace("csi-rcons-debug") << " Type has operator." << std::endl;
d_reconstruct[id] = NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, Node::fromExpr( dt[carg].getConstructor() ) );
status = 0;
}else{
//check if kind is in syntax sort
- karg = d_qe->getTermDatabaseSygus()->getKindConsNum( stn, min_t.getKind() );
+ karg = sti.getKindConsNum(min_t.getKind());
if( karg!=-1 ){
//collect the children of min_t
std::vector< Node > tchildren;
}
//get decompositions
for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
- Kind k = d_qe->getTermDatabaseSygus()->getConsNumKind( stn, i );
+ Kind k = sti.getConsNumKind(i);
getEquivalentTerms( k, min_t, equiv );
}
//assign ids to terms
}
TermDbSygus* tds = d_qe->getTermDatabaseSygus();
NodeManager* nm = NodeManager::currentNM();
+ SygusTypeInfo& ti = tds->getTypeInfo(tn);
Node sc;
d_builtin_const_to_sygus[tn][c] = sc;
Assert(c.isConst());
}
else
{
- int carg = tds->getOpConsNum(tn, c);
+ int carg = ti.getOpConsNum(c);
if (carg != -1)
{
sc = nm->mkNode(APPLY_CONSTRUCTOR,
Kind pk = getPlusKind(TypeNode::fromType(dt.getSygusType()));
if (pk != UNDEFINED_KIND)
{
- int arg = tds->getKindConsNum(tn, pk);
+ int arg = ti.getKindConsNum(pk);
if (arg != -1)
{
Kind ck =
TermDbSygus* tds = d_qe->getTermDatabaseSygus();
// ensure it is registered
tds->registerSygusType(tn);
- const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+ const Datatype& dt = tn.getDatatype();
+ Assert(dt.isSygus());
TypeNode btn = TypeNode::fromType(dt.getSygusType());
// for constant reconstruction
Kind ck = getComparisonKind(btn);
{
TypeNode ctn = candidates[i].getType();
d_tds->registerSygusType(ctn);
- if (d_tds->hasSubtermSymbolicCons(ctn))
+ SygusTypeInfo& cti = d_tds->getTypeInfo(ctn);
+ if (cti.hasSubtermSymbolicCons())
{
do_repair_const = true;
// remember that we are doing grammar-based repair
Node var_list = Node::fromExpr(tn.getDatatype().getSygusVarList());
NodeManager* nm = NodeManager::currentNM();
// get subtypes in value's type
+ SygusTypeInfo& ti = d_tds->getTypeInfo(tn);
std::vector<TypeNode> sf_types;
- d_tds->getSubfieldTypes(tn, sf_types);
+ ti.getSubfieldTypes(sf_types);
// associate variables with constructors in all subfield types
std::map<Node, Node> cons_var;
for (const Node& v : var_list)
if (seen_vars.insert(var).second)
{
// do not add repeated vars
- d_var_classes[d_tds->getSubclassForVar(tn, var)].push_back(var);
+ d_var_classes[ti.getSubclassForVar(var)].push_back(var);
}
}
for (const std::pair<unsigned, std::vector<Node>>& p : d_var_classes)
Node var_list = Node::fromExpr(tn.getDatatype().getSygusVarList());
// get subtypes in value's type
NodeManager* nm = NodeManager::currentNM();
+ SygusTypeInfo& ti = d_tds->getTypeInfo(tn);
std::vector<TypeNode> sf_types;
- d_tds->getSubfieldTypes(tn, sf_types);
+ ti.getSubfieldTypes(sf_types);
// associate variables with constructors in all subfield types
for (const Node& v : var_list)
{
// split initial variables into classes
for (const Node& v : var_list)
{
- Assert(d_tds->getSubclassForVar(tn, v) > 0);
- d_var_classes[d_tds->getSubclassForVar(tn, v)].push_back(v);
+ Assert(ti.getSubclassForVar(v) > 0);
+ d_var_classes[ti.getSubclassForVar(v)].push_back(v);
}
}
namespace theory {
namespace quantifiers {
-void TypeNodeIdTrie::add(Node v, std::vector<TypeNode>& types)
-{
- TypeNodeIdTrie* tnt = this;
- for (unsigned i = 0, size = types.size(); i < size; i++)
- {
- tnt = &tnt->d_children[types[i]];
- }
- tnt->d_data.push_back(v);
-}
-
-void TypeNodeIdTrie::assignIds(std::map<Node, unsigned>& assign,
- unsigned& idCount)
-{
- if (!d_data.empty())
- {
- for (const Node& v : d_data)
- {
- assign[v] = idCount;
- }
- idCount++;
- }
- for (std::pair<const TypeNode, TypeNodeIdTrie>& c : d_children)
- {
- c.second.assignIds(assign, idCount);
- }
-}
-
std::ostream& operator<<(std::ostream& os, EnumeratorRole r)
{
switch (r)
std::map<Node, Node>::iterator it = d_proxy_vars[tn].find(c);
if (it == d_proxy_vars[tn].end())
{
- int anyC = getAnyConstantConsNum(tn);
+ SygusTypeInfo& ti = getTypeInfo(tn);
+ int anyC = ti.getAnyConstantConsNum();
Node k;
if (anyC == -1)
{
return ret;
}
-Node TermDbSygus::sygusSubstituted( TypeNode tn, Node n, std::vector< Node >& args ) {
- Assert( d_var_list[tn].size()==args.size() );
- return n.substitute( d_var_list[tn].begin(), d_var_list[tn].end(), args.begin(), args.end() );
-}
-
unsigned TermDbSygus::getSygusTermSize( Node n ){
if (n.getKind() != APPLY_CONSTRUCTOR)
{
return weight + sum;
}
-void TermDbSygus::registerSygusType( TypeNode tn ) {
- std::map< TypeNode, TypeNode >::iterator itr = d_register.find( tn );
- if( itr==d_register.end() ){
- d_register[tn] = TypeNode::null();
- if( tn.isDatatype() ){
- const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
- Trace("sygus-db") << "Register type " << dt.getName() << "..." << std::endl;
- TypeNode btn = TypeNode::fromType( dt.getSygusType() );
- d_register[tn] = btn;
- if( !d_register[tn].isNull() ){
- // get the sygus variable list
- Node var_list = Node::fromExpr( dt.getSygusVarList() );
- if( !var_list.isNull() ){
- for( unsigned j=0; j<var_list.getNumChildren(); j++ ){
- Node sv = var_list[j];
- SygusVarNumAttribute svna;
- sv.setAttribute( svna, j );
- d_var_list[tn].push_back( sv );
- }
- }else{
- // no arguments to synthesis functions
- d_var_list[tn].clear();
- }
- // register connected types
- for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
- {
- for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++)
- {
- TypeNode ctn = TypeNode::fromType(dt[i].getArgType(j));
- registerSygusType(ctn);
- // carry type attributes
- if (d_has_subterm_sym_cons.find(ctn)
- != d_has_subterm_sym_cons.end())
- {
- d_has_subterm_sym_cons[tn] = true;
- }
- }
- }
- //iterate over constructors
- for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
- Expr sop = dt[i].getSygusOp();
- Assert( !sop.isNull() );
- Node n = Node::fromExpr( sop );
- Trace("sygus-db") << " Operator #" << i << " : " << sop;
- if( sop.getKind() == kind::BUILTIN ){
- Kind sk = NodeManager::operatorToKind( n );
- Trace("sygus-db") << ", kind = " << sk;
- d_kinds[tn][sk] = i;
- d_arg_kind[tn][i] = sk;
- if (sk == ITE)
- {
- // mark that this type has an ITE
- d_hasIte[tn] = true;
- }
- }
- else if (sop.isConst() && dt[i].getNumArgs() == 0)
- {
- Trace("sygus-db") << ", constant";
- d_consts[tn][n] = i;
- d_arg_const[tn][i] = n;
- }
- else if (sop.getKind() == LAMBDA)
- {
- // do type checking
- Assert(sop[0].getNumChildren() == dt[i].getNumArgs());
- for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++)
- {
- TypeNode ct = TypeNode::fromType(dt[i].getArgType(j));
- TypeNode cbt = sygusToBuiltinType(ct);
- TypeNode lat = TypeNode::fromType(sop[0][j].getType());
- CVC4_CHECK(cbt.isSubtypeOf(lat))
- << "In sygus datatype " << dt.getName()
- << ", argument to a lambda constructor is not " << lat
- << std::endl;
- }
- if (sop[0].getKind() == ITE)
- {
- // mark that this type has an ITE
- d_hasIte[tn] = true;
- }
- }
- // symbolic constructors
- if (n.getAttribute(SygusAnyConstAttribute()))
- {
- d_sym_cons_any_constant[tn] = i;
- d_has_subterm_sym_cons[tn] = true;
- }
- // TODO (as part of #1170): we still do not properly catch type
- // errors in sygus grammars for arguments of builtin operators.
- // The challenge is that we easily ask for expected argument types of
- // builtin operators e.g. PLUS. Hence the call to mkGeneric below
- // will throw a type exception.
- d_ops[tn][n] = i;
- d_arg_ops[tn][i] = n;
- Trace("sygus-db") << std::endl;
- // ensure that terms that this constructor encodes are
- // of the type specified in the datatype. This will fail if
- // e.g. bitvector-and is a constructor of an integer grammar.
- Node g = mkGeneric(dt, i);
- TypeNode gtn = g.getType();
- CVC4_CHECK(gtn.isSubtypeOf(btn))
- << "Sygus datatype " << dt.getName()
- << " encodes terms that are not of type " << btn << std::endl;
- Trace("sygus-db") << "...done register Operator #" << i << std::endl;
- }
- // compute min type depth information
- computeMinTypeDepthInternal(tn, tn, 0);
- }
- }
+bool TermDbSygus::registerSygusType(TypeNode tn)
+{
+ std::map<TypeNode, bool>::iterator it = d_registerStatus.find(tn);
+ if (it != d_registerStatus.end())
+ {
+ // already registered
+ return it->second;
+ }
+ d_registerStatus[tn] = false;
+ // it must be a sygus datatype
+ if (!tn.isDatatype())
+ {
+ return false;
}
+ const Datatype& dt = tn.getDatatype();
+ if (!dt.isSygus())
+ {
+ return false;
+ }
+ d_registerStatus[tn] = true;
+ SygusTypeInfo& sti = d_tinfo[tn];
+ sti.initialize(this, tn);
+ return true;
}
void TermDbSygus::registerEnumerator(Node e,
d_enum_to_using_sym_cons[e] = useSymbolicCons;
// depending on if we are using symbolic constructors, introduce symmetry
// breaking lemma templates for each relevant subtype of the grammar
+ SygusTypeInfo& eti = getTypeInfo(et);
std::vector<TypeNode> sf_types;
- getSubfieldTypes(et, sf_types);
- // maps variables to the list of subfield types they occur in
- std::map<Node, std::vector<TypeNode> > type_occurs;
- std::map<TypeNode, std::vector<Node> >::iterator itv = d_var_list.find(et);
- Assert(itv != d_var_list.end());
- for (const Node& v : itv->second)
- {
- type_occurs[v].clear();
- }
+ eti.getSubfieldTypes(sf_types);
// for each type of subfield type of this enumerator
for (unsigned i = 0, ntypes = sf_types.size(); i < ntypes; i++)
{
std::vector<unsigned> rm_indices;
TypeNode stn = sf_types[i];
Assert(stn.isDatatype());
+ SygusTypeInfo& sti = getTypeInfo(stn);
const Datatype& dt = stn.getDatatype();
- int anyC = getAnyConstantConsNum(stn);
+ int anyC = sti.getAnyConstantConsNum();
for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
{
Expr sop = dt[i].getSygusOp();
Assert(!sop.isNull());
bool isAnyC = static_cast<int>(i) == anyC;
- Node sopn = Node::fromExpr(sop);
- if (type_occurs.find(sopn) != type_occurs.end())
- {
- // if it is a variable, store that it occurs in stn
- type_occurs[sopn].push_back(stn);
- }
- else if (isAnyC && !useSymbolicCons)
+ if (isAnyC && !useSymbolicCons)
{
// if we are not using the any constant constructor
// do not use the symbolic constructor
{
// if we are using the any constant constructor, do not use any
// concrete constant
- Node c_op = getConsNumConst(stn, i);
+ Node c_op = sti.getConsNumConst(i);
if (!c_op.isNull())
{
rm_indices.push_back(i);
// solution" clauses.
const Datatype& dt = et.getDatatype();
if (options::sygusStream()
- || (!hasIte(et) && !dt.getSygusType().isBoolean()))
+ || (!eti.hasIte() && !dt.getSygusType().isBoolean()))
{
isActiveGen = true;
}
d_enum_var_agnostic[e] = isVarAgnostic;
if (isVarAgnostic)
{
- // if not done so already, compute type class identifiers for each variable
- if (d_var_subclass_id.find(et) == d_var_subclass_id.end())
- {
- d_var_subclass_id[et].clear();
- TypeNodeIdTrie tnit;
- for (std::pair<const Node, std::vector<TypeNode> >& to : type_occurs)
- {
- tnit.add(to.first, to.second);
- }
- // 0 is reserved for "no type class id"
- unsigned typeIdCount = 1;
- tnit.assignIds(d_var_subclass_id[et], typeIdCount);
- // assign the list and reverse map to index
- for (std::pair<const Node, std::vector<TypeNode> >& to : type_occurs)
- {
- Node v = to.first;
- unsigned sc = d_var_subclass_id[et][v];
- Trace("sygus-db") << v << " has subclass id " << sc << std::endl;
- d_var_subclass_list_index[et][v] = d_var_subclass_list[et][sc].size();
- d_var_subclass_list[et][sc].push_back(v);
- }
- }
+ // requires variable subclasses
+ eti.initializeVarSubclasses();
// If no subclass has more than one variable, do not use variable agnostic
// enumeration
- bool useVarAgnostic = false;
- for (std::pair<const unsigned, std::vector<Node> >& p :
- d_var_subclass_list[et])
- {
- if (p.second.size() > 1)
- {
- useVarAgnostic = true;
- }
- }
+ bool useVarAgnostic = !eti.isSubclassVarTrivial();
if (!useVarAgnostic)
{
Trace("sygus-db")
bool TermDbSygus::isRegistered(TypeNode tn) const
{
- return d_register.find( tn )!=d_register.end();
+ return d_tinfo.find(tn) != d_tinfo.end();
}
TypeNode TermDbSygus::sygusToBuiltinType( TypeNode tn ) {
- Assert( isRegistered( tn ) );
- return d_register[tn];
+ std::map<TypeNode, SygusTypeInfo>::iterator it = d_tinfo.find(tn);
+ Assert(it != d_tinfo.end());
+ return it->second.getBuiltinType();
}
void TermDbSygus::toStreamSygus(const char* c, Node n)
}
}
-void TermDbSygus::computeMinTypeDepthInternal( TypeNode root_tn, TypeNode tn, unsigned type_depth ) {
- std::map< TypeNode, unsigned >::iterator it = d_min_type_depth[root_tn].find( tn );
- if( it==d_min_type_depth[root_tn].end() || type_depth<it->second ){
- if (!tn.isDatatype())
- {
- // do not recurse to non-datatype types
- return;
- }
- const Datatype& dt = tn.getDatatype();
- if( !dt.isSygus() )
- {
- // do not recurse to non-sygus datatype types
- return;
- }
- d_min_type_depth[root_tn][tn] = type_depth;
- //compute for connected types
- for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
- for( unsigned j=0; j<dt[i].getNumArgs(); j++ ){
- computeMinTypeDepthInternal( root_tn, getArgType( dt[i], j ), type_depth+1 );
- }
- }
- }
-}
-
-unsigned TermDbSygus::getMinTypeDepth( TypeNode root_tn, TypeNode tn ){
- std::map< TypeNode, unsigned >::iterator it = d_min_type_depth[root_tn].find( tn );
- if( it==d_min_type_depth[root_tn].end() ){
- Assert( d_min_type_depth[root_tn].find( tn )!=d_min_type_depth[root_tn].end() );
- return d_min_type_depth[root_tn][tn];
- }else{
- return it->second;
- }
-}
-
-unsigned TermDbSygus::getMinTermSize( TypeNode tn ) {
- Assert( isRegistered( tn ) );
- std::map< TypeNode, unsigned >::iterator it = d_min_term_size.find( tn );
- if( it==d_min_term_size.end() ){
- const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
- for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
- if (dt[i].getNumArgs() == 0)
- {
- d_min_term_size[tn] = 0;
- return 0;
- }
- }
- // TODO : improve
- d_min_term_size[tn] = 1;
- return 1;
- }else{
- return it->second;
- }
-}
-
-unsigned TermDbSygus::getMinConsTermSize( TypeNode tn, unsigned cindex ) {
- Assert( isRegistered( tn ) );
- std::map< unsigned, unsigned >::iterator it = d_min_cons_term_size[tn].find( cindex );
- if( it==d_min_cons_term_size[tn].end() ){
- const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
- Assert( cindex<dt.getNumConstructors() );
- unsigned ret = 0;
- if( dt[cindex].getNumArgs()>0 ){
- ret = 1;
- for( unsigned i=0; i<dt[cindex].getNumArgs(); i++ ){
- ret += getMinTermSize( getArgType( dt[cindex], i ) );
- }
- }
- d_min_cons_term_size[tn][cindex] = ret;
- return ret;
- }else{
- return it->second;
- }
+SygusTypeInfo& TermDbSygus::getTypeInfo(TypeNode tn)
+{
+ AlwaysAssert(d_tinfo.find(tn) != d_tinfo.end());
+ return d_tinfo[tn];
}
unsigned TermDbSygus::getSelectorWeight(TypeNode tn, Node sel)
return itsw->second[sel];
}
-void TermDbSygus::getSubfieldTypes(TypeNode tn, std::vector<TypeNode>& sf_types)
-{
- std::map<TypeNode, std::map<TypeNode, unsigned> >::iterator it =
- d_min_type_depth.find(tn);
- Assert(it != d_min_type_depth.end());
- for (const std::pair<const TypeNode, unsigned>& st : it->second)
- {
- sf_types.push_back(st.first);
- }
-}
-
-int TermDbSygus::getKindConsNum( TypeNode tn, Kind k ) {
- Assert( isRegistered( tn ) );
- std::map< TypeNode, std::map< Kind, int > >::iterator itt = d_kinds.find( tn );
- if( itt!=d_kinds.end() ){
- std::map< Kind, int >::iterator it = itt->second.find( k );
- if( it!=itt->second.end() ){
- return it->second;
- }
- }
- return -1;
-}
-
-int TermDbSygus::getConstConsNum( TypeNode tn, Node n ){
- Assert( isRegistered( tn ) );
- std::map< TypeNode, std::map< Node, int > >::iterator itt = d_consts.find( tn );
- if( itt!=d_consts.end() ){
- std::map< Node, int >::iterator it = itt->second.find( n );
- if( it!=itt->second.end() ){
- return it->second;
- }
- }
- return -1;
-}
-
-int TermDbSygus::getOpConsNum( TypeNode tn, Node n ) {
- std::map< Node, int >::iterator it = d_ops[tn].find( n );
- if( it!=d_ops[tn].end() ){
- return it->second;
- }else{
- return -1;
- }
-}
-
-bool TermDbSygus::hasKind( TypeNode tn, Kind k ) {
- return getKindConsNum( tn, k )!=-1;
-}
-bool TermDbSygus::hasIte(TypeNode tn) const
-{
- return d_hasIte.find(tn) != d_hasIte.end();
-}
-bool TermDbSygus::hasConst( TypeNode tn, Node n ) {
- return getConstConsNum( tn, n )!=-1;
-}
-bool TermDbSygus::hasOp( TypeNode tn, Node n ) {
- return getOpConsNum( tn, n )!=-1;
-}
-
-Node TermDbSygus::getConsNumOp( TypeNode tn, int i ) {
- Assert( isRegistered( tn ) );
- std::map< TypeNode, std::map< int, Node > >::iterator itt = d_arg_ops.find( tn );
- if( itt!=d_arg_ops.end() ){
- std::map< int, Node >::iterator itn = itt->second.find( i );
- if( itn!=itt->second.end() ){
- return itn->second;
- }
- }
- return Node::null();
-}
-
-Node TermDbSygus::getConsNumConst( TypeNode tn, int i ) {
- Assert( isRegistered( tn ) );
- std::map< TypeNode, std::map< int, Node > >::iterator itt = d_arg_const.find( tn );
- if( itt!=d_arg_const.end() ){
- std::map< int, Node >::iterator itn = itt->second.find( i );
- if( itn!=itt->second.end() ){
- return itn->second;
- }
- }
- return Node::null();
-}
-
-Kind TermDbSygus::getConsNumKind( TypeNode tn, int i ) {
- Assert( isRegistered( tn ) );
- std::map< TypeNode, std::map< int, Kind > >::iterator itt = d_arg_kind.find( tn );
- if( itt!=d_arg_kind.end() ){
- std::map< int, Kind >::iterator itk = itt->second.find( i );
- if( itk!=itt->second.end() ){
- return itk->second;
- }
- }
- return UNDEFINED_KIND;
-}
-
-bool TermDbSygus::isKindArg( TypeNode tn, int i ) {
- return getConsNumKind( tn, i )!=UNDEFINED_KIND;
-}
-
-bool TermDbSygus::isConstArg( TypeNode tn, int i ) {
- Assert( isRegistered( tn ) );
- std::map< TypeNode, std::map< int, Node > >::iterator itt = d_arg_const.find( tn );
- if( itt!=d_arg_const.end() ){
- return itt->second.find( i )!=itt->second.end();
- }else{
- return false;
- }
-}
-
TypeNode TermDbSygus::getArgType(const DatatypeConstructor& c, unsigned i) const
{
Assert(i < c.getNumArgs());
}
}
-int TermDbSygus::getAnyConstantConsNum(TypeNode tn) const
-{
- Assert(isRegistered(tn));
- std::map<TypeNode, unsigned>::const_iterator itt =
- d_sym_cons_any_constant.find(tn);
- if (itt != d_sym_cons_any_constant.end())
- {
- return static_cast<int>(itt->second);
- }
- return -1;
-}
-
-bool TermDbSygus::hasSubtermSymbolicCons(TypeNode tn) const
-{
- return d_has_subterm_sym_cons.find(tn) != d_has_subterm_sym_cons.end();
-}
-
-unsigned TermDbSygus::getSubclassForVar(TypeNode tn, Node n) const
-{
- std::map<TypeNode, std::map<Node, unsigned> >::const_iterator itc =
- d_var_subclass_id.find(tn);
- if (itc == d_var_subclass_id.end())
- {
- Assert(false);
- return 0;
- }
- std::map<Node, unsigned>::const_iterator itcc = itc->second.find(n);
- if (itcc == itc->second.end())
- {
- Assert(false);
- return 0;
- }
- return itcc->second;
-}
-
-unsigned TermDbSygus::getNumSubclassVars(TypeNode tn, unsigned sc) const
-{
- std::map<TypeNode, std::map<unsigned, std::vector<Node> > >::const_iterator
- itv = d_var_subclass_list.find(tn);
- if (itv == d_var_subclass_list.end())
- {
- Assert(false);
- return 0;
- }
- std::map<unsigned, std::vector<Node> >::const_iterator itvv =
- itv->second.find(sc);
- if (itvv == itv->second.end())
- {
- Assert(false);
- return 0;
- }
- return itvv->second.size();
-}
-Node TermDbSygus::getVarSubclassIndex(TypeNode tn,
- unsigned sc,
- unsigned i) const
-{
- std::map<TypeNode, std::map<unsigned, std::vector<Node> > >::const_iterator
- itv = d_var_subclass_list.find(tn);
- if (itv == d_var_subclass_list.end())
- {
- Assert(false);
- return Node::null();
- }
- std::map<unsigned, std::vector<Node> >::const_iterator itvv =
- itv->second.find(sc);
- if (itvv == itv->second.end() || i >= itvv->second.size())
- {
- Assert(false);
- return Node::null();
- }
- return itvv->second[i];
-}
-
-bool TermDbSygus::getIndexInSubclassForVar(TypeNode tn,
- Node v,
- unsigned& index) const
-{
- std::map<TypeNode, std::map<Node, unsigned> >::const_iterator itv =
- d_var_subclass_list_index.find(tn);
- if (itv == d_var_subclass_list_index.end())
- {
- return false;
- }
- std::map<Node, unsigned>::const_iterator itvv = itv->second.find(v);
- if (itvv == itv->second.end())
- {
- return false;
- }
- index = itvv->second;
- return true;
-}
-
bool TermDbSygus::isSymbolicConsApp(Node n) const
{
if (n.getKind() != APPLY_CONSTRUCTOR)
std::vector<TypeNode>& argts,
bool aggr)
{
- int c = getKindConsNum(tn, k);
+ Assert(isRegistered(tn));
+ SygusTypeInfo& ti = getTypeInfo(tn);
+ int c = ti.getKindConsNum(k);
const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
if (c != -1)
{
std::vector<Node>& args,
bool tryEval)
{
- if( !args.empty() ){
- std::map< TypeNode, std::vector< Node > >::iterator it = d_var_list.find( tn );
- Assert( it!=d_var_list.end() );
- Assert( it->second.size()==args.size() );
-
- Node res;
- if (tryEval && options::sygusEvalOpt())
- {
- // Try evaluating, which is much faster than substitution+rewriting.
- // This may fail if there is a subterm of bn under the
- // substitution that is not constant, or if an operator in bn is not
- // supported by the evaluator
- res = d_eval->eval(bn, it->second, args);
- }
- if (!res.isNull())
- {
- Assert(res
- == Rewriter::rewrite(bn.substitute(it->second.begin(),
- it->second.end(),
- args.begin(),
- args.end())));
- return res;
- }
- else
- {
- return Rewriter::rewrite(bn.substitute(
- it->second.begin(), it->second.end(), args.begin(), args.end()));
- }
- }else{
+ if (args.empty())
+ {
return Rewriter::rewrite( bn );
}
+ Assert(isRegistered(tn));
+ SygusTypeInfo& ti = getTypeInfo(tn);
+ const std::vector<Node>& varlist = ti.getVarList();
+ Assert(varlist.size() == args.size());
+
+ Node res;
+ if (tryEval && options::sygusEvalOpt())
+ {
+ // Try evaluating, which is much faster than substitution+rewriting.
+ // This may fail if there is a subterm of bn under the
+ // substitution that is not constant, or if an operator in bn is not
+ // supported by the evaluator
+ res = d_eval->eval(bn, varlist, args);
+ }
+ if (!res.isNull())
+ {
+ Assert(res
+ == Rewriter::rewrite(bn.substitute(
+ varlist.begin(), varlist.end(), args.begin(), args.end())));
+ return res;
+ }
+ res = bn.substitute(varlist.begin(), varlist.end(), args.begin(), args.end());
+ return Rewriter::rewrite(res);
}
Node TermDbSygus::evaluateWithUnfolding(
#include "theory/quantifiers/extended_rewrite.h"
#include "theory/quantifiers/sygus/sygus_eval_unfold.h"
#include "theory/quantifiers/sygus/sygus_explain.h"
+#include "theory/quantifiers/sygus/type_info.h"
#include "theory/quantifiers/term_database.h"
namespace CVC4 {
class SynthConjecture;
-/** A trie indexed by types that assigns unique identifiers to nodes. */
-class TypeNodeIdTrie
-{
- public:
- /** children of this node */
- std::map<TypeNode, TypeNodeIdTrie> d_children;
- /** the data stored at this node */
- std::vector<Node> d_data;
- /** add v to this trie, indexed by types */
- void add(Node v, std::vector<TypeNode>& types);
- /**
- * Assign each node in this trie an identifier such that
- * assign[v1] = assign[v2] iff v1 and v2 are indexed by the same values.
- */
- void assignIds(std::map<Node, unsigned>& assign, unsigned& idCount);
-};
-
/** role for registering an enumerator */
enum EnumeratorRole
{
*
* This initializes this database for sygus datatype type tn. This may
* throw an assertion failure if the sygus grammar has type errors. Otherwise,
- * after registering a sygus type, the query functions in this class (such
- * as sygusToBuiltinType, getKindConsNum, etc.) can be called for tn.
+ * after registering a sygus type, the query function getTypeInfo can be
+ * called for tn.
+ *
+ * This method returns true if tn is a sygus datatype type and false
+ * otherwise.
*/
- void registerSygusType(TypeNode tn);
+ bool registerSygusType(TypeNode tn);
//------------------------------utilities
/** get the explanation utility */
*/
TypeNode sygusToBuiltinType(TypeNode tn);
//-----------------------------end conversion from sygus to builtin
+ /**
+ * Get type information about sygus datatype type tn. The type tn should be
+ * (a subfield type of) a type that has been registered to this class.
+ */
+ SygusTypeInfo& getTypeInfo(TypeNode tn);
/** print to sygus stream n on trace c */
static void toStreamSygus(const char* c, Node n);
/** cache of getProxyVariable */
std::map<TypeNode, std::map<Node, Node> > d_proxy_vars;
//-----------------------------end conversion from sygus to builtin
-
// TODO :issue #1235 : below here needs refactor
-
public:
Node d_true;
Node d_false;
bool involvesDivByZero( Node n, std::map< Node, bool >& visited );
private:
- // information for sygus types
- std::map<TypeNode, TypeNode> d_register; // stores sygus -> builtin type
- std::map<TypeNode, std::vector<Node> > d_var_list;
- std::map<TypeNode, std::map<int, Kind> > d_arg_kind;
- std::map<TypeNode, std::map<Kind, int> > d_kinds;
/**
- * Whether this sygus type has a constructors whose sygus operator is ITE,
- * or is a lambda whose body is ITE.
+ * Maps types that we have called registerSygusType to a flag indicating
+ * whether that type is a sygus datatype type. Sygus datatype types that
+ * are in this map have initialized type information stored in the map below.
*/
- std::map<TypeNode, bool> d_hasIte;
- std::map<TypeNode, std::map<int, Node> > d_arg_const;
- std::map<TypeNode, std::map<Node, int> > d_consts;
- std::map<TypeNode, std::map<Node, int> > d_ops;
- std::map<TypeNode, std::map<int, Node> > d_arg_ops;
- std::map<TypeNode, std::map<Node, Node> > d_semantic_skolem;
- // grammar information
- // root -> type -> _
+ std::map<TypeNode, bool> d_registerStatus;
/**
- * For each sygus type t1, this maps datatype types t2 to the smallest size of
- * a term of type t1 that includes t2 as a subterm. For example, for grammar:
- * A -> B+B | 0 | B-D
- * B -> C+C
- * ...
- * we have that d_min_type_depth[A] = { A -> 0, B -> 1, C -> 2, D -> 1 }.
+ * The type information for each sygus datatype type that has been registered
+ * to this class.
*/
- std::map<TypeNode, std::map<TypeNode, unsigned> > d_min_type_depth;
- // std::map< TypeNode, std::map< Node, std::map< std::map< int, bool > > >
- // d_consider_const;
- // type -> cons -> _
- std::map<TypeNode, unsigned> d_min_term_size;
- std::map<TypeNode, std::map<unsigned, unsigned> > d_min_cons_term_size;
+ std::map<TypeNode, SygusTypeInfo> d_tinfo;
/** a cache for getSelectorWeight */
std::map<TypeNode, std::map<Node, unsigned> > d_sel_weight;
- /**
- * For each sygus type, the index of the "any constant" constructor, if it
- * has one.
- */
- std::map<TypeNode, unsigned> d_sym_cons_any_constant;
- /**
- * Whether any subterm of this type contains a symbolic constructor. This
- * corresponds to whether sygus repair techniques will ever have any effect
- * for this type.
- */
- std::map<TypeNode, bool> d_has_subterm_sym_cons;
- /**
- * Map from sygus types and bound variables to their type subclass id. Note
- * type class identifiers are computed for each type of registered sygus
- * enumerators, but not all sygus types. For details, see getSubclassIdForVar.
- */
- std::map<TypeNode, std::map<Node, unsigned> > d_var_subclass_id;
- /** the list of variables with given subclass */
- std::map<TypeNode, std::map<unsigned, std::vector<Node> > >
- d_var_subclass_list;
- /** the index of each variable in the above list */
- std::map<TypeNode, std::map<Node, unsigned> > d_var_subclass_list_index;
public: // general sygus utilities
bool isRegistered(TypeNode tn) const;
- // get the minimum depth of type in its parent grammar
- unsigned getMinTypeDepth( TypeNode root_tn, TypeNode tn );
- // get the minimum size for a constructor term
- unsigned getMinTermSize( TypeNode tn );
- unsigned getMinConsTermSize( TypeNode tn, unsigned cindex );
/** get the weight of the selector, where tn is the domain of sel */
unsigned getSelectorWeight(TypeNode tn, Node sel);
- /** get subfield types
- *
- * This adds all "subfield types" of tn to sf_types. A type tnc is a subfield
- * type of tn if there exists a selector chain S1( ... Sn( x )...) that has
- * type tnc, where x has type tn. In other words, tnc is the type of some
- * subfield of terms of type tn, at any depth.
- */
- void getSubfieldTypes(TypeNode tn, std::vector<TypeNode>& sf_types);
-
- public:
- int getKindConsNum( TypeNode tn, Kind k );
- int getConstConsNum( TypeNode tn, Node n );
- int getOpConsNum( TypeNode tn, Node n );
- bool hasKind( TypeNode tn, Kind k );
- /**
- * Returns true if this sygus type has a constructors whose sygus operator is
- * ITE, or is a lambda whose body is ITE.
- */
- bool hasIte(TypeNode tn) const;
- bool hasConst( TypeNode tn, Node n );
- bool hasOp( TypeNode tn, Node n );
- Node getConsNumConst( TypeNode tn, int i );
- Node getConsNumOp( TypeNode tn, int i );
- Kind getConsNumKind( TypeNode tn, int i );
- bool isKindArg( TypeNode tn, int i );
- bool isConstArg( TypeNode tn, int i );
/** get arg type */
TypeNode getArgType(const DatatypeConstructor& c, unsigned i) const;
- /** is type match */
+ /** Do constructors c1 and c2 have the same type? */
bool isTypeMatch( const DatatypeConstructor& c1, const DatatypeConstructor& c2 );
- /**
- * Get the index of the "any constant" constructor of type tn if it has one,
- * or returns -1 otherwise.
- */
- int getAnyConstantConsNum(TypeNode tn) const;
- /** has subterm symbolic constructor
- *
- * Returns true if any subterm of type tn can be a symbolic constructor.
- */
- bool hasSubtermSymbolicCons(TypeNode tn) const;
- //--------------------------------- variable subclasses
- /** Get subclass id for variable
- *
- * This returns the "subclass" identifier for variable v in sygus
- * type tn. A subclass identifier groups variables based on the sygus
- * types they occur in:
- * A -> A + B | C + C | x | y | z | w | u
- * B -> y | z
- * C -> u
- * The variables in this grammar can be grouped according to the sygus types
- * they appear in:
- * { x,w } occur in A
- * { y,z } occur in A,B
- * { u } occurs in A,C
- * We say that e.g. x, w are in the same subclass.
- *
- * If this method returns 0, then v is not a variable in sygus type tn.
- * Otherwise, this method returns a positive value n, such that
- * getSubclassIdForVar[v1] = getSubclassIdForVar[v2] iff v1 and v2 are in the
- * same subclass.
- *
- * The type tn should be the type of an enumerator registered to this
- * database, where notice that we do not compute this information for the
- * subfield types of the enumerator.
- */
- unsigned getSubclassForVar(TypeNode tn, Node v) const;
- /**
- * Get the number of variable in the subclass with identifier sc for type tn.
- */
- unsigned getNumSubclassVars(TypeNode tn, unsigned sc) const;
- /** Get the i^th variable in the subclass with identifier sc for type tn */
- Node getVarSubclassIndex(TypeNode tn, unsigned sc, unsigned i) const;
- /**
- * Get the a variable's index in its subclass list. This method returns true
- * iff variable v has been assigned a subclass in tn. It updates index to
- * be v's index iff the method returns true.
- */
- bool getIndexInSubclassForVar(TypeNode tn, Node v, unsigned& index) const;
- //--------------------------------- end variable subclasses
/** return whether n is an application of a symbolic constructor */
bool isSymbolicConsApp(Node n) const;
/** can construct kind
bool aggr = false);
TypeNode getSygusTypeForVar( Node v );
- Node sygusSubstituted( TypeNode tn, Node n, std::vector< Node >& args );
Node getSygusNormalized( Node n, std::map< TypeNode, int >& var_count, std::map< Node, Node >& subs );
Node getNormalized(TypeNode t, Node prog);
unsigned getSygusTermSize( Node n );
--- /dev/null
+/********************* */
+/*! \file type_info.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 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 type info class
+ **/
+
+#include "theory/quantifiers/sygus/type_info.h"
+
+#include "base/cvc4_check.h"
+#include "theory/datatypes/datatypes_rewriter.h"
+#include "theory/quantifiers/sygus/term_database_sygus.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+SygusTypeInfo::SygusTypeInfo()
+ : d_hasIte(false),
+ d_min_term_size(0),
+ d_sym_cons_any_constant(-1),
+ d_has_subterm_sym_cons(false)
+{
+}
+
+void SygusTypeInfo::initialize(TermDbSygus* tds, TypeNode tn)
+{
+ d_this = tn;
+ Assert(tn.isDatatype());
+ const Datatype& dt = tn.getDatatype();
+ Assert(dt.isSygus());
+ Trace("sygus-db") << "Register type " << dt.getName() << "..." << std::endl;
+ TypeNode btn = TypeNode::fromType(dt.getSygusType());
+ d_btype = btn;
+ Assert(!d_btype.isNull());
+ // get the sygus variable list
+ Node var_list = Node::fromExpr(dt.getSygusVarList());
+ if (!var_list.isNull())
+ {
+ for (unsigned j = 0; j < var_list.getNumChildren(); j++)
+ {
+ Node sv = var_list[j];
+ SygusVarNumAttribute svna;
+ sv.setAttribute(svna, j);
+ d_var_list.push_back(sv);
+ }
+ }
+ else
+ {
+ // no arguments to synthesis functions
+ d_var_list.clear();
+ }
+
+ // compute min term size information: this must be computed before registering
+ // subfield types
+ d_min_term_size = 1;
+ for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
+ {
+ if (dt[i].getNumArgs() == 0)
+ {
+ d_min_term_size = 0;
+ }
+ }
+
+ // register connected types
+ for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
+ {
+ for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++)
+ {
+ TypeNode ctn = TypeNode::fromType(dt[i].getArgType(j));
+ Trace("sygus-db") << " register subfield type " << ctn << std::endl;
+ if (tds->registerSygusType(ctn))
+ {
+ SygusTypeInfo& stic = tds->getTypeInfo(ctn);
+ // carry type attributes
+ if (stic.d_has_subterm_sym_cons)
+ {
+ d_has_subterm_sym_cons = true;
+ }
+ }
+ }
+ }
+ // iterate over constructors
+ for (unsigned i = 0; i < dt.getNumConstructors(); i++)
+ {
+ Expr sop = dt[i].getSygusOp();
+ Assert(!sop.isNull());
+ Node n = Node::fromExpr(sop);
+ Trace("sygus-db") << " Operator #" << i << " : " << sop;
+ if (sop.getKind() == kind::BUILTIN)
+ {
+ Kind sk = NodeManager::operatorToKind(n);
+ Trace("sygus-db") << ", kind = " << sk;
+ d_kinds[sk] = i;
+ d_arg_kind[i] = sk;
+ if (sk == ITE)
+ {
+ // mark that this type has an ITE
+ d_hasIte = true;
+ }
+ }
+ else if (sop.isConst() && dt[i].getNumArgs() == 0)
+ {
+ Trace("sygus-db") << ", constant";
+ d_consts[n] = i;
+ d_arg_const[i] = n;
+ }
+ else if (sop.getKind() == LAMBDA)
+ {
+ // do type checking
+ Assert(sop[0].getNumChildren() == dt[i].getNumArgs());
+ for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++)
+ {
+ TypeNode ct = TypeNode::fromType(dt[i].getArgType(j));
+ TypeNode cbt = tds->sygusToBuiltinType(ct);
+ TypeNode lat = TypeNode::fromType(sop[0][j].getType());
+ CVC4_CHECK(cbt.isSubtypeOf(lat))
+ << "In sygus datatype " << dt.getName()
+ << ", argument to a lambda constructor is not " << lat << std::endl;
+ }
+ if (sop[0].getKind() == ITE)
+ {
+ // mark that this type has an ITE
+ d_hasIte = true;
+ }
+ }
+ // symbolic constructors
+ if (n.getAttribute(SygusAnyConstAttribute()))
+ {
+ d_sym_cons_any_constant = i;
+ d_has_subterm_sym_cons = true;
+ }
+ // TODO (as part of #1170): we still do not properly catch type
+ // errors in sygus grammars for arguments of builtin operators.
+ // The challenge is that we easily ask for expected argument types of
+ // builtin operators e.g. PLUS. Hence the call to mkGeneric below
+ // will throw a type exception.
+ d_ops[n] = i;
+ d_arg_ops[i] = n;
+ Trace("sygus-db") << std::endl;
+ // ensure that terms that this constructor encodes are
+ // of the type specified in the datatype. This will fail if
+ // e.g. bitvector-and is a constructor of an integer grammar.
+ Node g = tds->mkGeneric(dt, i);
+ TypeNode gtn = g.getType();
+ CVC4_CHECK(gtn.isSubtypeOf(btn))
+ << "Sygus datatype " << dt.getName()
+ << " encodes terms that are not of type " << btn << std::endl;
+ Trace("sygus-db") << "...done register Operator #" << i << std::endl;
+ }
+ // compute minimum type depth information
+ computeMinTypeDepthInternal(tn, 0);
+ // compute minimum term size information
+ d_min_term_size = 1;
+ for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
+ {
+ unsigned csize = 0;
+ if (dt[i].getNumArgs() > 0)
+ {
+ csize = 1;
+ for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++)
+ {
+ TypeNode ct = TypeNode::fromType(dt[i].getArgType(j));
+ if (ct == tn)
+ {
+ csize += d_min_term_size;
+ }
+ else if (tds->isRegistered(ct))
+ {
+ SygusTypeInfo& stic = tds->getTypeInfo(ct);
+ csize += stic.getMinTermSize();
+ }
+ else
+ {
+ Assert(!ct.isDatatype() || !ct.getDatatype().isSygus());
+ }
+ }
+ }
+ d_min_cons_term_size[i] = csize;
+ }
+}
+
+void SygusTypeInfo::initializeVarSubclasses()
+{
+ if (d_var_list.empty())
+ {
+ // no variables
+ return;
+ }
+ if (!d_var_subclass_id.empty())
+ {
+ // already computed
+ return;
+ }
+ // compute variable subclasses
+ std::vector<TypeNode> sf_types;
+ getSubfieldTypes(sf_types);
+ // maps variables to the list of subfield types they occur in
+ std::map<Node, std::vector<TypeNode> > type_occurs;
+ for (const Node& v : d_var_list)
+ {
+ type_occurs[v].clear();
+ }
+ // for each type of subfield type of this enumerator
+ for (unsigned i = 0, ntypes = sf_types.size(); i < ntypes; i++)
+ {
+ std::vector<unsigned> rm_indices;
+ TypeNode stn = sf_types[i];
+ Assert(stn.isDatatype());
+ const Datatype& dt = stn.getDatatype();
+ for (unsigned j = 0, ncons = dt.getNumConstructors(); j < ncons; j++)
+ {
+ Expr sop = dt[j].getSygusOp();
+ Assert(!sop.isNull());
+ Node sopn = Node::fromExpr(sop);
+ if (type_occurs.find(sopn) != type_occurs.end())
+ {
+ // if it is a variable, store that it occurs in stn
+ type_occurs[sopn].push_back(stn);
+ }
+ }
+ }
+ TypeNodeIdTrie tnit;
+ for (std::pair<const Node, std::vector<TypeNode> >& to : type_occurs)
+ {
+ tnit.add(to.first, to.second);
+ }
+ // 0 is reserved for "no type class id"
+ unsigned typeIdCount = 1;
+ tnit.assignIds(d_var_subclass_id, typeIdCount);
+ // assign the list and reverse map to index
+ for (std::pair<const Node, std::vector<TypeNode> >& to : type_occurs)
+ {
+ Node v = to.first;
+ unsigned sc = d_var_subclass_id[v];
+ Trace("sygus-db") << v << " has subclass id " << sc << std::endl;
+ d_var_subclass_list_index[v] = d_var_subclass_list[sc].size();
+ d_var_subclass_list[sc].push_back(v);
+ }
+}
+
+TypeNode SygusTypeInfo::getBuiltinType() const { return d_btype; }
+
+const std::vector<Node>& SygusTypeInfo::getVarList() const
+{
+ return d_var_list;
+}
+
+void SygusTypeInfo::computeMinTypeDepthInternal(TypeNode tn,
+ unsigned type_depth)
+{
+ std::map<TypeNode, unsigned>::iterator it = d_min_type_depth.find(tn);
+ if (it != d_min_type_depth.end() && type_depth >= it->second)
+ {
+ // no new information
+ return;
+ }
+ if (!tn.isDatatype())
+ {
+ // do not recurse to non-datatype types
+ return;
+ }
+ const Datatype& dt = tn.getDatatype();
+ if (!dt.isSygus())
+ {
+ // do not recurse to non-sygus datatype types
+ return;
+ }
+ d_min_type_depth[tn] = type_depth;
+ // compute for connected types
+ for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
+ {
+ for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++)
+ {
+ TypeNode at = TypeNode::fromType(dt[i].getArgType(j));
+ computeMinTypeDepthInternal(at, type_depth + 1);
+ }
+ }
+}
+
+unsigned SygusTypeInfo::getMinTypeDepth(TypeNode tn) const
+{
+ std::map<TypeNode, unsigned>::const_iterator it = d_min_type_depth.find(tn);
+ if (it != d_min_type_depth.end())
+ {
+ Assert(false);
+ return 0;
+ }
+ return it->second;
+}
+
+unsigned SygusTypeInfo::getMinTermSize() const { return d_min_term_size; }
+
+unsigned SygusTypeInfo::getMinConsTermSize(unsigned cindex)
+{
+ std::map<unsigned, unsigned>::iterator it = d_min_cons_term_size.find(cindex);
+ if (it != d_min_cons_term_size.end())
+ {
+ return it->second;
+ }
+ Assert(false);
+ return 0;
+}
+
+void SygusTypeInfo::getSubfieldTypes(std::vector<TypeNode>& sf_types) const
+{
+ for (const std::pair<const TypeNode, unsigned>& st : d_min_type_depth)
+ {
+ sf_types.push_back(st.first);
+ }
+}
+
+int SygusTypeInfo::getKindConsNum(Kind k) const
+{
+ std::map<Kind, unsigned>::const_iterator it = d_kinds.find(k);
+ if (it != d_kinds.end())
+ {
+ return static_cast<int>(it->second);
+ }
+ return -1;
+}
+
+int SygusTypeInfo::getConstConsNum(Node n) const
+{
+ std::map<Node, unsigned>::const_iterator it = d_consts.find(n);
+ if (it != d_consts.end())
+ {
+ return static_cast<int>(it->second);
+ }
+ return -1;
+}
+
+int SygusTypeInfo::getOpConsNum(Node n) const
+{
+ std::map<Node, unsigned>::const_iterator it = d_ops.find(n);
+ if (it != d_ops.end())
+ {
+ return static_cast<int>(it->second);
+ }
+ return -1;
+}
+
+bool SygusTypeInfo::hasKind(Kind k) const { return getKindConsNum(k) != -1; }
+bool SygusTypeInfo::hasIte() const { return d_hasIte; }
+bool SygusTypeInfo::hasConst(Node n) const { return getConstConsNum(n) != -1; }
+bool SygusTypeInfo::hasOp(Node n) const { return getOpConsNum(n) != -1; }
+
+Node SygusTypeInfo::getConsNumOp(unsigned i) const
+{
+ std::map<unsigned, Node>::const_iterator itn = d_arg_ops.find(i);
+ if (itn != d_arg_ops.end())
+ {
+ return itn->second;
+ }
+ return Node::null();
+}
+
+Node SygusTypeInfo::getConsNumConst(unsigned i) const
+{
+ std::map<unsigned, Node>::const_iterator itn = d_arg_const.find(i);
+ if (itn != d_arg_const.end())
+ {
+ return itn->second;
+ }
+ return Node::null();
+}
+
+Kind SygusTypeInfo::getConsNumKind(unsigned i) const
+{
+ std::map<unsigned, Kind>::const_iterator itk = d_arg_kind.find(i);
+ if (itk != d_arg_kind.end())
+ {
+ return itk->second;
+ }
+ return UNDEFINED_KIND;
+}
+
+bool SygusTypeInfo::isKindArg(unsigned i) const
+{
+ return getConsNumKind(i) != UNDEFINED_KIND;
+}
+
+bool SygusTypeInfo::isConstArg(unsigned i) const
+{
+ return d_arg_const.find(i) != d_arg_const.end();
+}
+
+int SygusTypeInfo::getAnyConstantConsNum() const
+{
+ return d_sym_cons_any_constant;
+}
+
+bool SygusTypeInfo::hasSubtermSymbolicCons() const
+{
+ return d_has_subterm_sym_cons;
+}
+
+unsigned SygusTypeInfo::getSubclassForVar(Node n) const
+{
+ std::map<Node, unsigned>::const_iterator itcc = d_var_subclass_id.find(n);
+ if (itcc == d_var_subclass_id.end())
+ {
+ Assert(false);
+ return 0;
+ }
+ return itcc->second;
+}
+
+unsigned SygusTypeInfo::getNumSubclassVars(unsigned sc) const
+{
+ std::map<unsigned, std::vector<Node> >::const_iterator itvv =
+ d_var_subclass_list.find(sc);
+ if (itvv == d_var_subclass_list.end())
+ {
+ Assert(false);
+ return 0;
+ }
+ return itvv->second.size();
+}
+Node SygusTypeInfo::getVarSubclassIndex(unsigned sc, unsigned i) const
+{
+ std::map<unsigned, std::vector<Node> >::const_iterator itvv =
+ d_var_subclass_list.find(sc);
+ if (itvv == d_var_subclass_list.end() || i >= itvv->second.size())
+ {
+ Assert(false);
+ return Node::null();
+ }
+ return itvv->second[i];
+}
+
+bool SygusTypeInfo::getIndexInSubclassForVar(Node v, unsigned& index) const
+{
+ std::map<Node, unsigned>::const_iterator itvv =
+ d_var_subclass_list_index.find(v);
+ if (itvv == d_var_subclass_list_index.end())
+ {
+ return false;
+ }
+ index = itvv->second;
+ return true;
+}
+
+bool SygusTypeInfo::isSubclassVarTrivial() const
+{
+ for (const std::pair<const unsigned, std::vector<Node> >& p :
+ d_var_subclass_list)
+ {
+ if (p.second.size() > 1)
+ {
+ return false;
+ }
+ }
+ return true;
+}
+
+} // namespace quantifiers
+} // namespace theory
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file type_info.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 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 type info data structure
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS__TYPE_INFO_H
+#define CVC4__THEORY__QUANTIFIERS__SYGUS__TYPE_INFO_H
+
+#include <map>
+#include <unordered_set>
+
+#include "expr/node.h"
+#include "theory/quantifiers/sygus/type_node_id_trie.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+class TermDbSygus;
+
+/**
+ * This data structure stores statically computed information regarding a sygus
+ * datatype type.
+ *
+ * To use an instance of this class x, call x.initialize(tn); where tn is a
+ * sygus datatype type. Then, most of the query methods on x can be called.
+ * As an exception, the variable subclass queries require that additionally
+ * x.initializeVarSubclasses() is called.
+ *
+ */
+class SygusTypeInfo
+{
+ public:
+ SygusTypeInfo();
+ //-------------------------------------------- initialize
+ /** initialize this information for sygus datatype type tn */
+ void initialize(TermDbSygus* tds, TypeNode tn);
+ /**
+ * Initialize the variable subclass information for this class. Must have
+ * called initialize(...) prior to calling this method.
+ */
+ void initializeVarSubclasses();
+ //-------------------------------------------- end initialize
+ /** Get the builtin type that this sygus type encodes */
+ TypeNode getBuiltinType() const;
+ /** Get the variable list (formal argument list) for the sygus type */
+ const std::vector<Node>& getVarList() const;
+ /**
+ * Return the index of the constructor of this sygus type that encodes
+ * application of the builtin Kind k, or -1 if one does not exist.
+ */
+ int getKindConsNum(Kind k) const;
+ /**
+ * Return the index of the constructor of this sygus type that encodes
+ * constant c, or -1 if one does not exist.
+ */
+ int getConstConsNum(Node c) const;
+ /**
+ * Return the index of the constructor of this sygus type whose builtin
+ * operator is n, or -1 if one does not exist.
+ */
+ int getOpConsNum(Node n) const;
+ /** Is there a constructor that encodes application of builtin Kind k? */
+ bool hasKind(Kind k) const;
+ /** Is there a constructor that encodes constant c? */
+ bool hasConst(Node c) const;
+ /** Is there a constructor whose builtin operator is n? */
+ bool hasOp(Node n) const;
+ /**
+ * Returns true if this sygus type has a constructor whose sygus operator is
+ * ITE, or is a lambda whose body is ITE.
+ */
+ bool hasIte() const;
+ /**
+ * Get the builtin kind for the i^th constructor of this sygus type. If the
+ * i^th constructor does not encode an application of a builtin kind, this
+ * method returns UNDEFINED_KIND.
+ */
+ Kind getConsNumKind(unsigned i) const;
+ /**
+ * Get the construct for the i^th constructor of this sygus type. If the
+ * i^th constructor does not encode a builtin constant, this method returns
+ * the null node.
+ */
+ Node getConsNumConst(unsigned i) const;
+ /** Get the builtin operator of the i^th constructor of this sygus type */
+ Node getConsNumOp(unsigned i) const;
+ /**
+ * Returns true if the i^th constructor encodes application of a builtin Kind.
+ */
+ bool isKindArg(unsigned i) const;
+ /**
+ * Returns true if the i^th constructor encodes a builtin constant.
+ */
+ bool isConstArg(unsigned i) const;
+ /**
+ * Get the index of the "any constant" constructor of type tn if it has one,
+ * or returns -1 otherwise.
+ */
+ int getAnyConstantConsNum() const;
+ /** has subterm symbolic constructor
+ *
+ * Returns true if any subterm of type tn can be a symbolic constructor.
+ */
+ bool hasSubtermSymbolicCons() const;
+ /** get subfield types
+ *
+ * This adds all "subfield types" of tn to sf_types. A type tnc is a subfield
+ * type of tn if there exists a selector chain S1( ... Sn( x )...) that has
+ * type tnc, where x has type tn. In other words, tnc is the type of some
+ * subfield of terms of type tn, at any depth.
+ */
+ void getSubfieldTypes(std::vector<TypeNode>& sf_types) const;
+ //--------------------------------- variable subclasses
+ /** Get subclass id for variable
+ *
+ * This returns the "subclass" identifier for variable v in sygus
+ * type tn. A subclass identifier groups variables based on the sygus
+ * types they occur in:
+ * A -> A + B | C + C | x | y | z | w | u
+ * B -> y | z
+ * C -> u
+ * The variables in this grammar can be grouped according to the sygus types
+ * they appear in:
+ * { x,w } occur in A
+ * { y,z } occur in A,B
+ * { u } occurs in A,C
+ * We say that e.g. x, w are in the same subclass.
+ *
+ * If this method returns 0, then v is not a variable in sygus type tn.
+ * Otherwise, this method returns a positive value n, such that
+ * getSubclassIdForVar[v1] = getSubclassIdForVar[v2] iff v1 and v2 are in the
+ * same subclass.
+ *
+ * The type tn should be the type of an enumerator registered to this
+ * database, where notice that we do not compute this information for the
+ * subfield types of the enumerator.
+ */
+ unsigned getSubclassForVar(Node v) const;
+ /**
+ * Get the number of variable in the subclass with identifier sc for type tn.
+ */
+ unsigned getNumSubclassVars(unsigned sc) const;
+ /** Get the i^th variable in the subclass with identifier sc for type tn */
+ Node getVarSubclassIndex(unsigned sc, unsigned i) const;
+ /**
+ * Get the a variable's index in its subclass list. This method returns true
+ * iff variable v has been assigned a subclass in tn. It updates index to
+ * be v's index iff the method returns true.
+ */
+ bool getIndexInSubclassForVar(Node v, unsigned& index) const;
+ /**
+ * Are the variable subclasses a trivial partition (each variable subclass
+ * has a single variable)?
+ */
+ bool isSubclassVarTrivial() const;
+ //--------------------------------- end variable subclasses
+ /**
+ * Get the minimum depth of type in this grammar
+ *
+ */
+ unsigned getMinTypeDepth(TypeNode tn) const;
+ /** Get the minimum size for a term of this sygus type */
+ unsigned getMinTermSize() const;
+ /**
+ * Get the minimum size for a term that is an application of a constructor of
+ * this type.
+ */
+ unsigned getMinConsTermSize(unsigned cindex);
+
+ private:
+ /** The sygus type that this class is for */
+ TypeNode d_this;
+ /** The builtin type that this sygus type encodes */
+ TypeNode d_btype;
+ /** The variable list of the sygus type */
+ std::vector<Node> d_var_list;
+ /**
+ * Maps constructor indices to the (builtin) Kind that they encode, if any.
+ */
+ std::map<unsigned, Kind> d_arg_kind;
+ /** Reverse of the above map */
+ std::map<Kind, unsigned> d_kinds;
+ /**
+ * Whether this sygus type has a constructors whose sygus operator is ITE,
+ * or is a lambda whose body is ITE.
+ */
+ bool d_hasIte;
+ /**
+ * Maps constructor indices to the constant that they encode, if any.
+ */
+ std::map<unsigned, Node> d_arg_const;
+ /** Reverse of the above map */
+ std::map<Node, unsigned> d_consts;
+ /**
+ * Maps constructor indices to the operator they encode.
+ */
+ std::map<unsigned, Node> d_arg_ops;
+ /** Reverse of the above map */
+ std::map<Node, unsigned> d_ops;
+ /**
+ * This maps the subfield datatype types T to the smallest size of a term of
+ * this sygus type that includes T as a subterm. For example, for type A with
+ * grammar:
+ * A -> B+B | 0 | B-D
+ * B -> C+C
+ * ...
+ * we have that d_min_type_depth = { A -> 0, B -> 1, C -> 2, D -> 1 }.
+ */
+ std::map<TypeNode, unsigned> d_min_type_depth;
+ /** The minimimum size term of this type */
+ unsigned d_min_term_size;
+ /**
+ * Maps constructors to the minimum size term that is an application of that
+ * constructor.
+ */
+ std::map<unsigned, unsigned> d_min_cons_term_size;
+ /** a cache for getSelectorWeight */
+ std::map<Node, unsigned> d_sel_weight;
+ /**
+ * For each sygus type, the index of the "any constant" constructor, if it
+ * has one, or -1 otherwise.
+ */
+ int d_sym_cons_any_constant;
+ /**
+ * Whether any subterm of this type contains a symbolic constructor. This
+ * corresponds to whether sygus repair techniques will ever have any effect
+ * for this type.
+ */
+ bool d_has_subterm_sym_cons;
+ /**
+ * Map from sygus types and bound variables to their type subclass id. Note
+ * type class identifiers are computed for each type of registered sygus
+ * enumerators, but not all sygus types. For details, see getSubclassIdForVar.
+ */
+ std::map<Node, unsigned> d_var_subclass_id;
+ /** the list of variables with given subclass */
+ std::map<unsigned, std::vector<Node> > d_var_subclass_list;
+ /** the index of each variable in the above list */
+ std::map<Node, unsigned> d_var_subclass_list_index;
+ /** computes the map d_min_type_depth */
+ void computeMinTypeDepthInternal(TypeNode root_tn, unsigned type_depth);
+};
+
+} // namespace quantifiers
+} // namespace theory
+} // namespace CVC4
+
+#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS__TYPE_INFO_H */
--- /dev/null
+/********************* */
+/*! \file type_node_id_trie.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 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 type node identifier trie
+ **/
+
+#include "theory/quantifiers/sygus/type_node_id_trie.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+void TypeNodeIdTrie::add(Node v, std::vector<TypeNode>& types)
+{
+ TypeNodeIdTrie* tnt = this;
+ for (unsigned i = 0, size = types.size(); i < size; i++)
+ {
+ tnt = &tnt->d_children[types[i]];
+ }
+ tnt->d_data.push_back(v);
+}
+
+void TypeNodeIdTrie::assignIds(std::map<Node, unsigned>& assign,
+ unsigned& idCount)
+{
+ if (!d_data.empty())
+ {
+ for (const Node& v : d_data)
+ {
+ assign[v] = idCount;
+ }
+ idCount++;
+ }
+ for (std::pair<const TypeNode, TypeNodeIdTrie>& c : d_children)
+ {
+ c.second.assignIds(assign, idCount);
+ }
+}
+
+} // namespace quantifiers
+} // namespace theory
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file type_node_id_trie.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 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 Type node identifier trie data structure
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS__TYPE_NODE_ID_TRIE_H
+#define CVC4__THEORY__QUANTIFIERS__SYGUS__TYPE_NODE_ID_TRIE_H
+
+#include <map>
+#include <vector>
+
+#include "expr/node.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+class TermDbSygus;
+
+/**
+ * A trie indexed by types that assigns unique identifiers to nodes based on
+ * a vector of types.
+ */
+class TypeNodeIdTrie
+{
+ public:
+ /** children of this node */
+ std::map<TypeNode, TypeNodeIdTrie> d_children;
+ /** the data stored at this node */
+ std::vector<Node> d_data;
+ /** add v to this trie, indexed by types */
+ void add(Node v, std::vector<TypeNode>& types);
+ /**
+ * Assign each node in this trie an identifier such that
+ * assign[v1] = assign[v2] iff v1 and v2 are indexed by the same values.
+ */
+ void assignIds(std::map<Node, unsigned>& assign, unsigned& idCount);
+};
+
+} // namespace quantifiers
+} // namespace theory
+} // namespace CVC4
+
+#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS__TYPE_NODE_ID_TRIE_H */
projects / cvc5.git / commitdiff