From: Andrew Reynolds Date: Mon, 16 Sep 2019 20:58:50 +0000 (-0500) Subject: Sygus type info class (#3187) X-Git-Tag: cvc5-1.0.0~3949 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=57301bf1db0febc6bf5b205c0ecbb2e249601bd0;p=cvc5.git Sygus type info class (#3187) --- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 20458219e..d062e99c0 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -595,6 +595,10 @@ libcvc4_add_sources( 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 diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp index 334b3d638..cf05a6029 100644 --- a/src/theory/datatypes/datatypes_sygus.cpp +++ b/src/theory/datatypes/datatypes_sygus.cpp @@ -244,9 +244,10 @@ void SygusSymBreakNew::assertTesterInternal( int tindex, TNode n, Node exp, std: 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 ) ); } @@ -558,10 +559,11 @@ Node SygusSymBreakNew::getSimpleSymBreakPred(Node e, << "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()); @@ -621,8 +623,9 @@ Node SygusSymBreakNew::getSimpleSymBreakPred(Node e, // 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; @@ -630,11 +633,11 @@ Node SygusSymBreakNew::getSimpleSymBreakPred(Node e, // 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); @@ -656,7 +659,7 @@ Node SygusSymBreakNew::getSimpleSymBreakPred(Node e, 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(tindex)) { // the post value is true @@ -749,7 +752,7 @@ Node SygusSymBreakNew::getSimpleSymBreakPred(Node e, // 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; } @@ -806,7 +809,7 @@ Node SygusSymBreakNew::getSimpleSymBreakPred(Node e, 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]; @@ -816,13 +819,14 @@ Node SygusSymBreakNew::getSimpleSymBreakPred(Node e, 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(tnc.toType()).getDatatype(); std::vector 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 @@ -838,7 +842,7 @@ Node SygusSymBreakNew::getSimpleSymBreakPred(Node e, } else { - Node cc = d_tds->getConsNumConst(tnc, k); + Node cc = cti.getConsNumConst(k); if (!cc.isNull()) { Trace("sygus-sb-simple-debug") @@ -1355,11 +1359,12 @@ void SygusSymBreakNew::registerSizeTerm(Node e, std::vector& lemmas) // variables occur pre-traversal at top-level Node varList = Node::fromExpr(dt.getSygusVarList()); std::vector 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); diff --git a/src/theory/datatypes/sygus_simple_sym.cpp b/src/theory/datatypes/sygus_simple_sym.cpp index fb8bd7515..f1e8949af 100644 --- a/src/theory/datatypes/sygus_simple_sym.cpp +++ b/src/theory/datatypes/sygus_simple_sym.cpp @@ -95,7 +95,8 @@ class ReqTrie { 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; } @@ -154,13 +155,15 @@ bool SygusSimpleSymBreak::considerArgKind( { 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)) { @@ -294,7 +297,7 @@ bool SygusSimpleSymBreak::considerArgKind( } 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(pdt.getNumConstructors())); @@ -429,7 +432,9 @@ bool SygusSimpleSymBreak::considerConst( 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; @@ -438,7 +443,7 @@ bool SygusSimpleSymBreak::considerConst( { 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") @@ -453,7 +458,7 @@ bool SygusSimpleSymBreak::considerConst( << ", 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 " @@ -474,8 +479,9 @@ bool SygusSimpleSymBreak::considerConst( 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; @@ -499,7 +505,7 @@ bool SygusSimpleSymBreak::considerConst( 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 " diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp index fea2ce15a..d349e8ad4 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp @@ -225,7 +225,9 @@ int CegSingleInvSol::collectReconstructNodes(Node t, TypeNode stn, int& status) 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; @@ -234,14 +236,15 @@ int CegSingleInvSol::collectReconstructNodes(Node t, TypeNode stn, int& status) 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; @@ -374,7 +377,7 @@ int CegSingleInvSol::collectReconstructNodes(Node t, TypeNode stn, int& status) } //get decompositions for( unsigned i=0; igetTermDatabaseSygus()->getConsNumKind( stn, i ); + Kind k = sti.getConsNumKind(i); getEquivalentTerms( k, min_t, equiv ); } //assign ids to terms @@ -683,6 +686,7 @@ Node CegSingleInvSol::builtinToSygusConst(Node c, TypeNode tn, int rcons_depth) } 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()); @@ -709,7 +713,7 @@ Node CegSingleInvSol::builtinToSygusConst(Node c, TypeNode tn, int rcons_depth) } else { - int carg = tds->getOpConsNum(tn, c); + int carg = ti.getOpConsNum(c); if (carg != -1) { sc = nm->mkNode(APPLY_CONSTRUCTOR, @@ -743,7 +747,7 @@ Node CegSingleInvSol::builtinToSygusConst(Node c, TypeNode tn, int rcons_depth) 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 = @@ -815,7 +819,8 @@ void CegSingleInvSol::registerType(TypeNode tn) TermDbSygus* tds = d_qe->getTermDatabaseSygus(); // ensure it is registered tds->registerSygusType(tn); - const Datatype& dt = static_cast(tn.toType()).getDatatype(); + const Datatype& dt = tn.getDatatype(); + Assert(dt.isSygus()); TypeNode btn = TypeNode::fromType(dt.getSygusType()); // for constant reconstruction Kind ck = getComparisonKind(btn); diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp index 1e8012697..c319d7a37 100644 --- a/src/theory/quantifiers/sygus/cegis.cpp +++ b/src/theory/quantifiers/sygus/cegis.cpp @@ -85,7 +85,8 @@ bool Cegis::processInitialize(Node conj, { 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 diff --git a/src/theory/quantifiers/sygus/enum_stream_substitution.cpp b/src/theory/quantifiers/sygus/enum_stream_substitution.cpp index b568b8f53..0cdfe4307 100644 --- a/src/theory/quantifiers/sygus/enum_stream_substitution.cpp +++ b/src/theory/quantifiers/sygus/enum_stream_substitution.cpp @@ -48,8 +48,9 @@ void EnumStreamPermutation::reset(Node value) 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 sf_types; - d_tds->getSubfieldTypes(tn, sf_types); + ti.getSubfieldTypes(sf_types); // associate variables with constructors in all subfield types std::map cons_var; for (const Node& v : var_list) @@ -84,7 +85,7 @@ void EnumStreamPermutation::reset(Node value) 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>& p : d_var_classes) @@ -339,8 +340,9 @@ void EnumStreamSubstitution::initialize(TypeNode tn) 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 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) { @@ -361,8 +363,8 @@ void EnumStreamSubstitution::initialize(TypeNode tn) // 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); } } diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index 208c8b9a0..ed3eec145 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -31,33 +31,6 @@ namespace CVC4 { namespace theory { namespace quantifiers { -void TypeNodeIdTrie::add(Node v, std::vector& 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& assign, - unsigned& idCount) -{ - if (!d_data.empty()) - { - for (const Node& v : d_data) - { - assign[v] = idCount; - } - idCount++; - } - for (std::pair& c : d_children) - { - c.second.assignIds(assign, idCount); - } -} - std::ostream& operator<<(std::ostream& os, EnumeratorRole r) { switch (r) @@ -159,7 +132,8 @@ Node TermDbSygus::getProxyVariable(TypeNode tn, Node c) std::map::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) { @@ -340,11 +314,6 @@ Node TermDbSygus::sygusToBuiltin(Node n, TypeNode tn) 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) { @@ -362,116 +331,29 @@ unsigned TermDbSygus::getSygusTermSize( Node n ){ 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::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, @@ -498,36 +380,24 @@ 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 sf_types; - getSubfieldTypes(et, sf_types); - // maps variables to the list of subfield types they occur in - std::map > type_occurs; - std::map >::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 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(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 @@ -537,7 +407,7 @@ void TermDbSygus::registerEnumerator(Node e, { // 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); @@ -612,7 +482,7 @@ void TermDbSygus::registerEnumerator(Node e, // solution" clauses. const Datatype& dt = et.getDatatype(); if (options::sygusStream() - || (!hasIte(et) && !dt.getSygusType().isBoolean())) + || (!eti.hasIte() && !dt.getSygusType().isBoolean())) { isActiveGen = true; } @@ -637,39 +507,11 @@ void TermDbSygus::registerEnumerator(Node e, 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 >& 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 >& 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 >& p : - d_var_subclass_list[et]) - { - if (p.second.size() > 1) - { - useVarAgnostic = true; - } - } + bool useVarAgnostic = !eti.isSubclassVarTrivial(); if (!useVarAgnostic) { Trace("sygus-db") @@ -841,12 +683,13 @@ void TermDbSygus::clearSymBreakLemmas(Node e) { d_enum_to_sb_lemmas.erase(e); } 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::iterator it = d_tinfo.find(tn); + Assert(it != d_tinfo.end()); + return it->second.getBuiltinType(); } void TermDbSygus::toStreamSygus(const char* c, Node n) @@ -866,78 +709,10 @@ 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_depthsecond ){ - 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::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; isecond; - } -} - -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( cindex0 ){ - ret = 1; - for( unsigned i=0; isecond; - } +SygusTypeInfo& TermDbSygus::getTypeInfo(TypeNode tn) +{ + AlwaysAssert(d_tinfo.find(tn) != d_tinfo.end()); + return d_tinfo[tn]; } unsigned TermDbSygus::getSelectorWeight(TypeNode tn, Node sel) @@ -971,114 +746,6 @@ unsigned TermDbSygus::getSelectorWeight(TypeNode tn, Node sel) return itsw->second[sel]; } -void TermDbSygus::getSubfieldTypes(TypeNode tn, std::vector& sf_types) -{ - std::map >::iterator it = - d_min_type_depth.find(tn); - Assert(it != d_min_type_depth.end()); - for (const std::pair& 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()); @@ -1099,99 +766,6 @@ bool TermDbSygus::isTypeMatch( const DatatypeConstructor& c1, const DatatypeCons } } -int TermDbSygus::getAnyConstantConsNum(TypeNode tn) const -{ - Assert(isRegistered(tn)); - std::map::const_iterator itt = - d_sym_cons_any_constant.find(tn); - if (itt != d_sym_cons_any_constant.end()) - { - return static_cast(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 >::const_iterator itc = - d_var_subclass_id.find(tn); - if (itc == d_var_subclass_id.end()) - { - Assert(false); - return 0; - } - std::map::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 > >::const_iterator - itv = d_var_subclass_list.find(tn); - if (itv == d_var_subclass_list.end()) - { - Assert(false); - return 0; - } - std::map >::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 > >::const_iterator - itv = d_var_subclass_list.find(tn); - if (itv == d_var_subclass_list.end()) - { - Assert(false); - return Node::null(); - } - std::map >::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 >::const_iterator itv = - d_var_subclass_list_index.find(tn); - if (itv == d_var_subclass_list_index.end()) - { - return false; - } - std::map::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) @@ -1213,7 +787,9 @@ bool TermDbSygus::canConstructKind(TypeNode tn, std::vector& 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(tn.toType()).getDatatype(); if (c != -1) { @@ -1513,37 +1089,33 @@ Node TermDbSygus::evaluateBuiltin(TypeNode tn, std::vector& 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& 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( diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h index e0312c516..6c62d7a1b 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.h +++ b/src/theory/quantifiers/sygus/term_database_sygus.h @@ -23,6 +23,7 @@ #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 { @@ -31,23 +32,6 @@ namespace quantifiers { class SynthConjecture; -/** A trie indexed by types that assigns unique identifiers to nodes. */ -class TypeNodeIdTrie -{ - public: - /** children of this node */ - std::map d_children; - /** the data stored at this node */ - std::vector d_data; - /** add v to this trie, indexed by types */ - void add(Node v, std::vector& 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& assign, unsigned& idCount); -}; - /** role for registering an enumerator */ enum EnumeratorRole { @@ -78,10 +62,13 @@ class TermDbSygus { * * 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 */ @@ -304,6 +291,11 @@ class TermDbSygus { */ 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); @@ -375,9 +367,7 @@ class TermDbSygus { /** cache of getProxyVariable */ std::map > d_proxy_vars; //-----------------------------end conversion from sygus to builtin - // TODO :issue #1235 : below here needs refactor - public: Node d_true; Node d_false; @@ -388,150 +378,28 @@ class TermDbSygus { bool involvesDivByZero( Node n, std::map< Node, bool >& visited ); private: - // information for sygus types - std::map d_register; // stores sygus -> builtin type - std::map > d_var_list; - std::map > d_arg_kind; - std::map > 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 d_hasIte; - std::map > d_arg_const; - std::map > d_consts; - std::map > d_ops; - std::map > d_arg_ops; - std::map > d_semantic_skolem; - // grammar information - // root -> type -> _ + std::map 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 > d_min_type_depth; - // std::map< TypeNode, std::map< Node, std::map< std::map< int, bool > > > - // d_consider_const; - // type -> cons -> _ - std::map d_min_term_size; - std::map > d_min_cons_term_size; + std::map d_tinfo; /** a cache for getSelectorWeight */ std::map > d_sel_weight; - /** - * For each sygus type, the index of the "any constant" constructor, if it - * has one. - */ - std::map 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 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 > d_var_subclass_id; - /** the list of variables with given subclass */ - std::map > > - d_var_subclass_list; - /** the index of each variable in the above list */ - std::map > 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& 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 @@ -560,7 +428,6 @@ class TermDbSygus { 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 ); diff --git a/src/theory/quantifiers/sygus/type_info.cpp b/src/theory/quantifiers/sygus/type_info.cpp new file mode 100644 index 000000000..070e2ad9a --- /dev/null +++ b/src/theory/quantifiers/sygus/type_info.cpp @@ -0,0 +1,468 @@ +/********************* */ +/*! \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 sf_types; + getSubfieldTypes(sf_types); + // maps variables to the list of subfield types they occur in + std::map > 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 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 >& 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 >& 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& SygusTypeInfo::getVarList() const +{ + return d_var_list; +} + +void SygusTypeInfo::computeMinTypeDepthInternal(TypeNode tn, + unsigned type_depth) +{ + std::map::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::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::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& sf_types) const +{ + for (const std::pair& st : d_min_type_depth) + { + sf_types.push_back(st.first); + } +} + +int SygusTypeInfo::getKindConsNum(Kind k) const +{ + std::map::const_iterator it = d_kinds.find(k); + if (it != d_kinds.end()) + { + return static_cast(it->second); + } + return -1; +} + +int SygusTypeInfo::getConstConsNum(Node n) const +{ + std::map::const_iterator it = d_consts.find(n); + if (it != d_consts.end()) + { + return static_cast(it->second); + } + return -1; +} + +int SygusTypeInfo::getOpConsNum(Node n) const +{ + std::map::const_iterator it = d_ops.find(n); + if (it != d_ops.end()) + { + return static_cast(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::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::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::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::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 >::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 >::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::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 >& p : + d_var_subclass_list) + { + if (p.second.size() > 1) + { + return false; + } + } + return true; +} + +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/quantifiers/sygus/type_info.h b/src/theory/quantifiers/sygus/type_info.h new file mode 100644 index 000000000..9ac93f7ae --- /dev/null +++ b/src/theory/quantifiers/sygus/type_info.h @@ -0,0 +1,260 @@ +/********************* */ +/*! \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 +#include + +#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& 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& 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 d_var_list; + /** + * Maps constructor indices to the (builtin) Kind that they encode, if any. + */ + std::map d_arg_kind; + /** Reverse of the above map */ + std::map 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 d_arg_const; + /** Reverse of the above map */ + std::map d_consts; + /** + * Maps constructor indices to the operator they encode. + */ + std::map d_arg_ops; + /** Reverse of the above map */ + std::map 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 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 d_min_cons_term_size; + /** a cache for getSelectorWeight */ + std::map 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 d_var_subclass_id; + /** the list of variables with given subclass */ + std::map > d_var_subclass_list; + /** the index of each variable in the above list */ + std::map 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 */ diff --git a/src/theory/quantifiers/sygus/type_node_id_trie.cpp b/src/theory/quantifiers/sygus/type_node_id_trie.cpp new file mode 100644 index 000000000..ffe2f533d --- /dev/null +++ b/src/theory/quantifiers/sygus/type_node_id_trie.cpp @@ -0,0 +1,52 @@ +/********************* */ +/*! \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& 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& assign, + unsigned& idCount) +{ + if (!d_data.empty()) + { + for (const Node& v : d_data) + { + assign[v] = idCount; + } + idCount++; + } + for (std::pair& c : d_children) + { + c.second.assignIds(assign, idCount); + } +} + +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/quantifiers/sygus/type_node_id_trie.h b/src/theory/quantifiers/sygus/type_node_id_trie.h new file mode 100644 index 000000000..d0798c7a9 --- /dev/null +++ b/src/theory/quantifiers/sygus/type_node_id_trie.h @@ -0,0 +1,55 @@ +/********************* */ +/*! \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 +#include + +#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 d_children; + /** the data stored at this node */ + std::vector d_data; + /** add v to this trie, indexed by types */ + void add(Node v, std::vector& 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& assign, unsigned& idCount); +}; + +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 + +#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS__TYPE_NODE_ID_TRIE_H */