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();
*/
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
std::map<Node, size_t> 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
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
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())
}
computeArgReps(n);
+ std::vector<TNode>& 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<std::vector<TNode> >& 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<TNode>& 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))
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<Node, std::vector<std::vector<TNode> > >::const_iterator it =
+ d_fmapRelDom.find(f);
+ if (it != d_fmapRelDom.end())
+ {
+ Assert(i < it->second.size());
+ const std::vector<TNode>& rd = it->second[i];
+ return std::find(rd.begin(), rd.end(), r) != rd.end();
}
+ return false;
}
bool TermDb::isTermActive( Node n ) {
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();
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<TNode>& args)
+{
f = getOperatorRepresentative(f);
computeUfTerms( f );
return d_func_map_trie[f].existsTerm( args );
* 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.
*/
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<TNode>& 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<TNode>& 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:
/** map from operators to trie */
std::map<Node, TNodeTrie> d_func_map_trie;
std::map<Node, TNodeTrie> 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<Node, std::vector<std::vector<TNode>>> d_fmapRelDom;
/** has map */
std::map< Node, bool > d_has_map;
/** map from reps to a term in eqc in d_has_map */
projects / cvc5.git / commitdiff