From b9cddd75ada97b4e1808b907125e366c3c03c412 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 24 Sep 2018 23:00:32 -0500 Subject: [PATCH] Infrastructure for variable agnostic sygus enumerators (#2511) --- .../quantifiers/sygus/term_database_sygus.cpp | 212 +++++++++++++++--- .../quantifiers/sygus/term_database_sygus.h | 61 ++++- 2 files changed, 245 insertions(+), 28 deletions(-) diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index 1f4e34c1f..a10ecc566 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -343,6 +343,7 @@ void TermDbSygus::registerSygusType( TypeNode tn ) { } }else{ // no arguments to synthesis functions + d_var_list[tn].clear(); } // register connected types for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++) @@ -421,11 +422,51 @@ void TermDbSygus::registerSygusType( TypeNode tn ) { } } +/** 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) + { + 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); + } + /** + * 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) + { + 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); + } + } +}; + void TermDbSygus::registerEnumerator(Node e, Node f, SynthConjecture* conj, bool mkActiveGuard, - bool useSymbolicCons) + bool useSymbolicCons, + bool isVarAgnostic) { if (d_enum_to_conjecture.find(e) != d_enum_to_conjecture.end()) { @@ -441,15 +482,7 @@ void TermDbSygus::registerEnumerator(Node e, NodeManager* nm = NodeManager::currentNM(); if( mkActiveGuard ){ // make the guard - Node eg = Rewriter::rewrite(nm->mkSkolem("eG", nm->booleanType())); - eg = d_quantEngine->getValuation().ensureLiteral( eg ); - AlwaysAssert( !eg.isNull() ); - d_quantEngine->getOutputChannel().requirePhase( eg, true ); - //add immediate lemma - Node lem = nm->mkNode(OR, eg, eg.negate()); - Trace("cegqi-lemma") << "Cegqi::Lemma : enumerator : " << lem << std::endl; - d_quantEngine->getOutputChannel().lemma( lem ); - d_enum_to_active_guard[e] = eg; + d_enum_to_active_guard[e] = nm->mkSkolem("eG", nm->booleanType()); } Trace("sygus-db") << " registering symmetry breaking clauses..." @@ -459,35 +492,47 @@ void TermDbSygus::registerEnumerator(Node e, // breaking lemma templates for each relevant subtype of the grammar 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(); + } // 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 = static_cast(stn.toType()).getDatatype(); - std::map::iterator itsa = - d_sym_cons_any_constant.find(stn); - if (itsa != d_sym_cons_any_constant.end()) + const Datatype& dt = stn.getDatatype(); + int anyC = getAnyConstantConsNum(stn); + for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++) { - if (!useSymbolicCons) + 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 we are not using the any constant constructor // do not use the symbolic constructor - rm_indices.push_back(itsa->second); + rm_indices.push_back(i); } - else + else if (anyC != -1 && !isAnyC && useSymbolicCons) { - // can remove all other concrete constant constructors - for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++) + // if we are using the any constant constructor, do not use any + // concrete constant + Node c_op = getConsNumConst(stn, i); + if (!c_op.isNull()) { - if (i != itsa->second) - { - Node c_op = getConsNumConst(stn, i); - if (!c_op.isNull()) - { - rm_indices.push_back(i); - } - } + rm_indices.push_back(i); } } } @@ -515,6 +560,33 @@ void TermDbSygus::registerEnumerator(Node e, } } Trace("sygus-db") << " ...finished" << std::endl; + + 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); + } + } + } } bool TermDbSygus::isEnumerator(Node e) const @@ -561,6 +633,16 @@ bool TermDbSygus::usingSymbolicConsForEnumerator(Node e) const return false; } +bool TermDbSygus::isVariableAgnosticEnumerator(Node e) const +{ + std::map::const_iterator itus = d_enum_var_agnostic.find(e); + if (itus != d_enum_var_agnostic.end()) + { + return itus->second; + } + return false; +} + void TermDbSygus::getEnumerators(std::vector& mts) { for (std::map::iterator itm = @@ -881,6 +963,82 @@ 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) diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h index b7bdba3ab..361c6bae0 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.h +++ b/src/theory/quantifiers/sygus/term_database_sygus.h @@ -69,6 +69,10 @@ class TermDbSygus { * (see d_enum_to_active_guard), * useSymbolicCons : whether we want model values for e to include symbolic * constructors like the "any constant" variable. + * isVarAgnostic : if this flag is true, the enumerator will only generate + * values whose variables are in canonical order (for example, only x1-x2 + * and not x2-x1 will be generated, assuming x1 and x2 are in the same + * "subclass", see getSubclassForVar). * * Notice that enumerator e may not be one-to-one with f in * synthesis-through-unification approaches (e.g. decision tree construction @@ -78,7 +82,8 @@ class TermDbSygus { Node f, SynthConjecture* conj, bool mkActiveGuard = false, - bool useSymbolicCons = false); + bool useSymbolicCons = false, + bool isVarAgnostic = false); /** is e an enumerator registered with this class? */ bool isEnumerator(Node e) const; /** return the conjecture e is associated with */ @@ -89,6 +94,8 @@ class TermDbSygus { Node getActiveGuardForEnumerator(Node e) const; /** are we using symbolic constructors for enumerator e? */ bool usingSymbolicConsForEnumerator(Node e) const; + /** is this enumerator agnostic to variables? */ + bool isVariableAgnosticEnumerator(Node e) const; /** get all registered enumerators */ void getEnumerators(std::vector& mts); /** Register symmetry breaking lemma @@ -273,6 +280,8 @@ class TermDbSygus { std::map d_sb_lemma_to_type; /** mapping from symmetry breaking lemmas to size */ std::map d_sb_lemma_to_size; + /** enumerators to whether they are variable agnostic */ + std::map d_enum_var_agnostic; //------------------------------end enumerators //-----------------------------conversion from sygus to builtin @@ -345,6 +354,17 @@ class TermDbSygus { * 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; @@ -390,6 +410,45 @@ class TermDbSygus { * 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 -- 2.30.2