diff options
Diffstat (limited to 'src/theory/quantifiers/sygus')
| -rw-r--r-- | src/theory/quantifiers/sygus/cegis_unif.cpp | 7 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_module.h | 10 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_pbe.cpp | 29 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_pbe.h | 5 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/synth_conjecture.cpp | 50 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/synth_conjecture.h | 12 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/synth_engine.cpp | 3 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/term_database_sygus.cpp | 212 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/term_database_sygus.h | 61 |
9 files changed, 336 insertions, 53 deletions
diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp index 456f44019..d4926311d 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.cpp +++ b/src/theory/quantifiers/sygus/cegis_unif.cpp @@ -166,6 +166,13 @@ bool CegisUnif::processConstructCandidates(const std::vector<Node>& enums, ->toStreamSygus(ss, m_eu); Trace("cegis") << ss.str() << std::endl; } + if (m_eu.isNull()) + { + // A condition enumerator was excluded by symmetry breaking, fail. + // TODO (#2498): either move conditions to getTermList or handle + // partial models in this module. + return false; + } unif_values[index][e].push_back(m_eu); } // inter-enumerator symmetry breaking for return values diff --git a/src/theory/quantifiers/sygus/sygus_module.h b/src/theory/quantifiers/sygus/sygus_module.h index c1b12dfd0..02cf1cdf2 100644 --- a/src/theory/quantifiers/sygus/sygus_module.h +++ b/src/theory/quantifiers/sygus/sygus_module.h @@ -71,6 +71,16 @@ class SygusModule */ virtual void getTermList(const std::vector<Node>& candidates, std::vector<Node>& terms) = 0; + /** allow partial model + * + * This method returns true if this module does not require that all + * terms returned by getTermList have "proper" model values when calling + * constructCandidates. A term may have a model value that is not proper + * if is excluded by symmetry breaking, e.g. x+0 is not proper. All model + * values that are not proper are replaced by "null" when calling + * constructCandidates. + */ + virtual bool allowPartialModel() { return false; } /** construct candidate * * This function takes as input: diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp index 9a6645560..647b16637 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.cpp +++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp @@ -415,6 +415,8 @@ void SygusPbe::getTermList(const std::vector<Node>& candidates, } } +bool SygusPbe::allowPartialModel() { return !options::sygusPbeMultiFair(); } + bool SygusPbe::constructCandidates(const std::vector<Node>& enums, const std::vector<Node>& enum_values, const std::vector<Node>& candidates, @@ -431,10 +433,18 @@ bool SygusPbe::constructCandidates(const std::vector<Node>& enums, Trace("sygus-pbe-enum") << " " << enums[i] << " -> "; TermDbSygus::toStreamSygus("sygus-pbe-enum", enum_values[i]); Trace("sygus-pbe-enum") << std::endl; - unsigned sz = d_tds->getSygusTermSize( enum_values[i] ); - szs.push_back(sz); - if( i==0 || sz<min_term_size ){ - min_term_size = sz; + if (!enum_values[i].isNull()) + { + unsigned sz = d_tds->getSygusTermSize(enum_values[i]); + szs.push_back(sz); + if (i == 0 || sz < min_term_size) + { + min_term_size = sz; + } + } + else + { + szs.push_back(0); } } // Assume two enumerators of types T1 and T2. @@ -448,11 +458,14 @@ bool SygusPbe::constructCandidates(const std::vector<Node>& enums, std::vector<unsigned> enum_consider; for (unsigned i = 0, esize = enums.size(); i < esize; i++) { - Assert(szs[i] >= min_term_size); - int diff = szs[i] - min_term_size; - if (!options::sygusPbeMultiFair() || diff <= diffAllow) + if (!enum_values[i].isNull()) { - enum_consider.push_back( i ); + Assert(szs[i] >= min_term_size); + int diff = szs[i] - min_term_size; + if (!options::sygusPbeMultiFair() || diff <= diffAllow) + { + enum_consider.push_back(i); + } } } diff --git a/src/theory/quantifiers/sygus/sygus_pbe.h b/src/theory/quantifiers/sygus/sygus_pbe.h index 66e19b6c9..b2ad5f63a 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.h +++ b/src/theory/quantifiers/sygus/sygus_pbe.h @@ -117,6 +117,11 @@ class SygusPbe : public SygusModule */ void getTermList(const std::vector<Node>& candidates, std::vector<Node>& terms) override; + /** + * PBE allows partial models to handle multiple enumerators if we are not + * using a strictly fair enumeration strategy. + */ + bool allowPartialModel() override; /** construct candidates * * This function attempts to use unification-based approaches for constructing diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index fde69d196..a29fdcc9f 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -23,6 +23,7 @@ #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" #include "smt/smt_statistics_registry.h" +#include "theory/datatypes/datatypes_rewriter.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/quantifiers_attributes.h" @@ -338,7 +339,14 @@ void SynthConjecture::doCheck(std::vector<Node>& lems) // get the model value of the relevant terms from the master module std::vector<Node> enum_values; - getModelValues(terms, enum_values); + bool fullModel = getModelValues(terms, enum_values); + + // if the master requires a full model and the model is partial, we fail + if (!d_master->allowPartialModel() && !fullModel) + { + Trace("cegqi-check") << "...partial model, fail." << std::endl; + return; + } if (!constructed_cand) { @@ -586,36 +594,54 @@ void SynthConjecture::preregisterConjecture(Node q) d_ceg_si->preregisterConjecture(q); } -void SynthConjecture::getModelValues(std::vector<Node>& n, std::vector<Node>& v) +bool SynthConjecture::getModelValues(std::vector<Node>& n, std::vector<Node>& v) { + bool ret = true; Trace("cegqi-engine") << " * Value is : "; for (unsigned i = 0; i < n.size(); i++) { Node nv = getModelValue(n[i]); v.push_back(nv); + ret = ret && !nv.isNull(); if (Trace.isOn("cegqi-engine")) { - TypeNode tn = nv.getType(); - Trace("cegqi-engine") << n[i] << " -> "; + Node onv = nv.isNull() ? d_qe->getModel()->getValue(n[i]) : nv; + TypeNode tn = onv.getType(); std::stringstream ss; - Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, nv); - Trace("cegqi-engine") << ss.str() << " "; - if (Trace.isOn("cegqi-engine-rr")) + Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, onv); + Trace("cegqi-engine") << n[i] << " -> "; + if (nv.isNull()) + { + Trace("cegqi-engine") << "[EXC: " << ss.str() << "] "; + } + else { - Node bv = d_qe->getTermDatabaseSygus()->sygusToBuiltin(nv, tn); - bv = Rewriter::rewrite(bv); - Trace("cegqi-engine-rr") << " -> " << bv << std::endl; + Trace("cegqi-engine") << ss.str() << " "; + if (Trace.isOn("cegqi-engine-rr")) + { + Node bv = d_qe->getTermDatabaseSygus()->sygusToBuiltin(nv, tn); + bv = Rewriter::rewrite(bv); + Trace("cegqi-engine-rr") << " -> " << bv << std::endl; + } } } - Assert(!nv.isNull()); } Trace("cegqi-engine") << std::endl; + return ret; } Node SynthConjecture::getModelValue(Node n) { Trace("cegqi-mv") << "getModelValue for : " << n << std::endl; - return d_qe->getModel()->getValue(n); + if (n.getAttribute(SygusSymBreakExcAttribute())) + { + // if the current model value of n was excluded by symmetry breaking, then + // it does not have a proper model value that we should consider, thus we + // return null. + return Node::null(); + } + Node mv = d_qe->getModel()->getValue(n); + return mv; } void SynthConjecture::debugPrint(const char* c) diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h index 1cbd4e949..53bc829cf 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.h +++ b/src/theory/quantifiers/sygus/synth_conjecture.h @@ -112,9 +112,15 @@ class SynthConjecture void assign(Node q); /** has a conjecture been assigned to this class */ bool isAssigned() { return !d_embed_quant.isNull(); } - /** get model values for terms n, store in vector v */ - void getModelValues(std::vector<Node>& n, std::vector<Node>& v); - /** get model value for term n */ + /** + * Get model values for terms n, store in vector v. This method returns true + * if and only if all values added to v are non-null. + */ + bool getModelValues(std::vector<Node>& n, std::vector<Node>& v); + /** + * Get model value for term n. If n has a value that was excluded by + * datatypes sygus symmetry breaking, this method returns null. + */ Node getModelValue(Node n); /** get utility for static preprocessing and analysis of conjectures */ diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp index 56844ec1f..296c10ff6 100644 --- a/src/theory/quantifiers/sygus/synth_engine.cpp +++ b/src/theory/quantifiers/sygus/synth_engine.cpp @@ -42,8 +42,7 @@ SynthEngine::~SynthEngine() { delete d_conj; } bool SynthEngine::needsCheck(Theory::Effort e) { - return !d_quantEngine->getTheoryEngine()->needCheck() - && e >= Theory::EFFORT_LAST_CALL; + return e >= Theory::EFFORT_LAST_CALL; } QuantifiersModule::QEffort SynthEngine::needsModel(Theory::Effort e) 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<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) + { + 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<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); + } + } +}; + 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<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(); + } // 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 = static_cast<DatatypeType>(stn.toType()).getDatatype(); - std::map<TypeNode, unsigned>::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<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 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<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); + } + } + } } 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<Node, bool>::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<Node>& mts) { for (std::map<Node, SynthConjecture*>::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<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) 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<Node>& mts); /** Register symmetry breaking lemma @@ -273,6 +280,8 @@ class TermDbSygus { std::map<Node, TypeNode> d_sb_lemma_to_type; /** mapping from symmetry breaking lemmas to size */ std::map<Node, unsigned> d_sb_lemma_to_size; + /** enumerators to whether they are variable agnostic */ + std::map<Node, bool> d_enum_var_agnostic; //------------------------------end enumerators //-----------------------------conversion from sygus to builtin @@ -345,6 +354,17 @@ class TermDbSygus { * 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; @@ -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 |