From 0b77c620f11d51a3a061b84a06a45c1a3ec53926 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 26 Apr 2022 18:38:14 -0500 Subject: [PATCH] Minor improvements to quantifiers utilities (#8661) --- src/expr/term_canonize.cpp | 2 +- src/expr/term_canonize.h | 12 ++--- src/theory/quantifiers/term_database.cpp | 59 +++++++++++++----------- src/theory/quantifiers/term_database.h | 28 +++++++---- 4 files changed, 57 insertions(+), 44 deletions(-) diff --git a/src/expr/term_canonize.cpp b/src/expr/term_canonize.cpp index 2cb5a0fe7..3660497d6 100644 --- a/src/expr/term_canonize.cpp +++ b/src/expr/term_canonize.cpp @@ -96,7 +96,7 @@ bool TermCanonize::getTermOrder(Node a, Node b) return false; } -Node TermCanonize::getCanonicalFreeVar(TypeNode tn, unsigned i, uint32_t tc) +Node TermCanonize::getCanonicalFreeVar(TypeNode tn, size_t i, uint32_t tc) { Assert(!tn.isNull()); NodeManager* nm = NodeManager::currentNM(); diff --git a/src/expr/term_canonize.h b/src/expr/term_canonize.h index a46f20f99..67fbee903 100644 --- a/src/expr/term_canonize.h +++ b/src/expr/term_canonize.h @@ -71,7 +71,12 @@ class TermCanonize */ bool getTermOrder(Node a, Node b); /** get canonical free variable #i of type tn */ - Node getCanonicalFreeVar(TypeNode tn, unsigned i, uint32_t tc = 0); + Node getCanonicalFreeVar(TypeNode tn, size_t i, uint32_t tc = 0); + /** + * Return the range of the free variable in the above map, or 0 if it does not + * exist. + */ + size_t getIndexForFreeVariable(Node v) const; /** get canonical term * * This returns a canonical (alpha-equivalent) version of n, where @@ -115,11 +120,6 @@ class TermCanonize std::map d_fvIndex; /** Get type class */ uint32_t getTypeClass(TNode v); - /** - * Return the range of the free variable in the above map, or 0 if it does not - * exist. - */ - size_t getIndexForFreeVariable(Node v) const; /** get canonical term * * This is a helper function for getCanonicalTerm above. We maintain a diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 432b6cca1..ee755b550 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -183,7 +183,8 @@ Node TermDb::getOrMakeTypeFreshVariable(TypeNode tn) return it->second; } -Node TermDb::getMatchOperator( Node n ) { +Node TermDb::getMatchOperator(TNode n) +{ Kind k = n.getKind(); //datatype operators may be parametric, always assume they are if (k == SELECT || k == STORE || k == SET_UNION || k == SET_INTER @@ -208,11 +209,12 @@ Node TermDb::getMatchOperator( Node n ) { else if (inst::TriggerTermInfo::isAtomicTriggerKind(k)) { return n.getOperator(); - }else{ - return Node::null(); } + return Node::null(); } +bool TermDb::isMatchable(TNode n) { return !getMatchOperator(n).isNull(); } + void TermDb::addTerm(Node n) { if (d_processed.find(n) != d_processed.end()) @@ -360,23 +362,27 @@ void TermDb::computeUfTerms( TNode f ) { } computeArgReps(n); + std::vector& reps = d_arg_reps[n]; Trace("term-db-debug") << "Adding term " << n << " with arg reps : "; - for (unsigned i = 0, size = d_arg_reps[n].size(); i < size; i++) + std::vector >& frds = d_fmapRelDom[f]; + size_t rsize = reps.size(); + // ensure the relevant domain vector has been allocated + frds.resize(rsize); + for (size_t i = 0; i < rsize; i++) { - Trace("term-db-debug") << d_arg_reps[n][i] << " "; - if (std::find(d_func_map_rel_dom[f][i].begin(), - d_func_map_rel_dom[f][i].end(), - d_arg_reps[n][i]) - == d_func_map_rel_dom[f][i].end()) + TNode r = reps[i]; + Trace("term-db-debug") << r << " "; + std::vector& frd = frds[i]; + if (std::find(frd.begin(), frd.end(), r) == frd.end()) { - d_func_map_rel_dom[f][i].push_back(d_arg_reps[n][i]); + frd.push_back(r); } } Trace("term-db-debug") << std::endl; Assert(d_qstate.hasTerm(n)); Trace("term-db-debug") << " and value : " << d_qstate.getRepresentative(n) << std::endl; - Node at = d_func_map_trie[f].addOrGetTerm(n, d_arg_reps[n]); + Node at = d_func_map_trie[f].addOrGetTerm(n, reps); Assert(d_qstate.hasTerm(at)); Trace("term-db-debug2") << "...add term returned " << at << std::endl; if (at != n && d_qstate.areEqual(at, n)) @@ -444,23 +450,22 @@ bool TermDb::checkCongruentDisequal(TNode a, TNode b, std::vector& exp) return false; } -bool TermDb::inRelevantDomain( TNode f, unsigned i, TNode r ) { +bool TermDb::inRelevantDomain(TNode f, size_t i, TNode r) +{ // notice if we are not higher-order, getOperatorRepresentative is a no-op f = getOperatorRepresentative(f); - computeUfTerms( f ); + computeUfTerms(f); Assert(!d_qstate.getEqualityEngine()->hasTerm(r) || d_qstate.getEqualityEngine()->getRepresentative(r) == r); - std::map< Node, std::map< unsigned, std::vector< Node > > >::iterator it = d_func_map_rel_dom.find( f ); - if( it != d_func_map_rel_dom.end() ){ - std::map< unsigned, std::vector< Node > >::iterator it2 = it->second.find( i ); - if( it2!=it->second.end() ){ - return std::find( it2->second.begin(), it2->second.end(), r )!=it2->second.end(); - }else{ - return false; - } - }else{ - return false; + std::map > >::const_iterator it = + d_fmapRelDom.find(f); + if (it != d_fmapRelDom.end()) + { + Assert(i < it->second.size()); + const std::vector& rd = it->second[i]; + return std::find(rd.begin(), rd.end(), r) != rd.end(); } + return false; } bool TermDb::isTermActive( Node n ) { @@ -591,7 +596,7 @@ bool TermDb::reset( Theory::Effort effort ){ d_arg_reps.clear(); d_func_map_trie.clear(); d_func_map_eqc_trie.clear(); - d_func_map_rel_dom.clear(); + d_fmapRelDom.clear(); d_consistent_ee = true; eq::EqualityEngine* ee = d_qstate.getEqualityEngine(); @@ -692,12 +697,12 @@ TNode TermDb::getCongruentTerm( Node f, Node n ) { if( itut!=d_func_map_trie.end() ){ computeArgReps( n ); return itut->second.existsTerm( d_arg_reps[n] ); - }else{ - return TNode::null(); } + return TNode::null(); } -TNode TermDb::getCongruentTerm( Node f, std::vector< TNode >& args ) { +TNode TermDb::getCongruentTerm(Node f, const std::vector& args) +{ f = getOperatorRepresentative(f); computeUfTerms( f ); return d_func_map_trie[f].existsTerm( args ); diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 949037c6d..9d01f54a7 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -151,7 +151,9 @@ class TermDb : public QuantifiersUtil { * If n has a kind that we do not index (like ADD), * then this function returns Node::null(). */ - Node getMatchOperator(Node n); + Node getMatchOperator(TNode n); + /** Is matchable? true if the above method is non-null */ + bool isMatchable(TNode n); /** get term arg index for all f-applications in the current context */ TNodeTrie* getTermArgTrie(Node f); /** get the term arg trie for f-applications in the equivalence class of eqc. @@ -165,19 +167,20 @@ class TermDb : public QuantifiersUtil { */ TNode getCongruentTerm(Node f, Node n); /** get congruent term - * If possible, returns a term t such that: - * (1) t is a term that is currently indexed by this database, - * (2) t is of the form f( t1, ..., tk ) where ti is in the - * equivalence class of args[i] for i=1...k. - */ - TNode getCongruentTerm(Node f, std::vector& args); + * If possible, returns a term t such that: + * (1) t is a term that is currently indexed by this database, + * (2) t is of the form f( t1, ..., tk ) where ti is in the + * equivalence class of args[i] for i=1...k. + * If not possible, return the null node. + */ + TNode getCongruentTerm(Node f, const std::vector& args); /** in relevant domain * Returns true if there is at least one term t such that: * (1) t is a term that is currently indexed by this database, * (2) t is of the form f( t1, ..., tk ) and ti is in the * equivalence class of r. */ - bool inRelevantDomain(TNode f, unsigned i, TNode r); + bool inRelevantDomain(TNode f, size_t i, TNode r); /** is the term n active in the current context? * * By default, all terms are active. A term is inactive if: @@ -246,8 +249,13 @@ class TermDb : public QuantifiersUtil { /** map from operators to trie */ std::map d_func_map_trie; std::map d_func_map_eqc_trie; - /** mapping from operators to their representative relevant domains */ - std::map< Node, std::map< unsigned, std::vector< Node > > > d_func_map_rel_dom; + /** + * Mapping from operators to their representative relevant domains. The + * size of the range is equal to the arity of the domain symbol. The + * terms in each vector are the representatives that occur in a term for + * that argument position (see inRelevantDomain). + */ + std::map>> d_fmapRelDom; /** has map */ std::map< Node, bool > d_has_map; /** map from reps to a term in eqc in d_has_map */ -- 2.30.2