This moves quantifiers::TermArgTrie in src/theory/quantifiers/term_database to (T)NodeTrie in src/expr, and cleans up all references to it.
node_manager_listeners.cpp
node_manager_listeners.h
node_self_iterator.h
+ node_trie.cpp
+ node_trie.h
node_value.cpp
node_value.h
pickle_data.cpp
--- /dev/null
+/********************* */
+/*! \file node_trie.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 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 a trie class for Nodes and TNodes.
+ **/
+
+#include "expr/node_trie.h"
+
+namespace CVC4 {
+namespace theory {
+
+template <bool ref_count>
+NodeTemplate<ref_count> NodeTemplateTrie<ref_count>::existsTerm(
+ const std::vector<NodeTemplate<ref_count>>& reps) const
+{
+ const NodeTemplateTrie<ref_count>* tnt = this;
+ typename std::map<NodeTemplate<ref_count>,
+ NodeTemplateTrie<ref_count>>::const_iterator it;
+ for (const NodeTemplate<ref_count> r : reps)
+ {
+ it = tnt->d_data.find(r);
+ if (it == tnt->d_data.end())
+ {
+ // didn't find this child, return null
+ return Node::null();
+ }
+ tnt = &it->second;
+ }
+ if (tnt->d_data.empty())
+ {
+ return Node::null();
+ }
+ return tnt->d_data.begin()->first;
+}
+
+template TNode NodeTemplateTrie<false>::existsTerm(
+ const std::vector<TNode>& reps) const;
+template Node NodeTemplateTrie<true>::existsTerm(
+ const std::vector<Node>& reps) const;
+
+template <bool ref_count>
+NodeTemplate<ref_count> NodeTemplateTrie<ref_count>::addOrGetTerm(
+ NodeTemplate<ref_count> n, const std::vector<NodeTemplate<ref_count>>& reps)
+{
+ NodeTemplateTrie<ref_count>* tnt = this;
+ for (const NodeTemplate<ref_count> r : reps)
+ {
+ tnt = &(tnt->d_data[r]);
+ }
+ if (tnt->d_data.empty())
+ {
+ // Store n in d_data. This should be interpretted as the "data" and not as a
+ // reference to a child.
+ tnt->d_data[n].clear();
+ return n;
+ }
+ return tnt->d_data.begin()->first;
+}
+
+template TNode NodeTemplateTrie<false>::addOrGetTerm(
+ TNode n, const std::vector<TNode>& reps);
+template Node NodeTemplateTrie<true>::addOrGetTerm(
+ Node n, const std::vector<Node>& reps);
+
+template <bool ref_count>
+void NodeTemplateTrie<ref_count>::debugPrint(const char* c,
+ unsigned depth) const
+{
+ for (const std::pair<const NodeTemplate<ref_count>,
+ NodeTemplateTrie<ref_count>>& p : d_data)
+ {
+ for (unsigned i = 0; i < depth; i++)
+ {
+ Trace(c) << " ";
+ }
+ Trace(c) << p.first << std::endl;
+ p.second.debugPrint(c, depth + 1);
+ }
+}
+
+template void NodeTemplateTrie<false>::debugPrint(const char* c,
+ unsigned depth) const;
+template void NodeTemplateTrie<true>::debugPrint(const char* c,
+ unsigned depth) const;
+
+} // namespace theory
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file node_trie.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 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 A trie class for Nodes and TNodes.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__EXPR__NODE_TRIE_H
+#define __CVC4__EXPR__NODE_TRIE_H
+
+#include <map>
+#include "expr/node.h"
+
+namespace CVC4 {
+namespace theory {
+
+/** NodeTemplate trie class
+ *
+ * This is a trie data structure whose distinguishing feature is that it has
+ * no "data" members and only references to children. The motivation for having
+ * no data members is efficiency.
+ *
+ * One use of this class is to represent "term indices" or a "signature tables"
+ * for symbols with fixed arities. In this use case, we "index" terms by the
+ * list of representatives of their arguments.
+ *
+ * For example, consider the equivalence classes :
+ *
+ * { a, d, f( d, c ), f( a, c ) }
+ * { b, f( b, d ) }
+ * { c, f( b, b ) }
+ *
+ * where the first elements ( a, b, c ) are the representatives of these
+ * classes. The NodeTemplateTrie t we may build for f is :
+ *
+ * t :
+ * t.d_data[a] :
+ * t.d_data[a].d_data[c] :
+ * t.d_data[a].d_data[c].d_data[f(d,c)] : (leaf)
+ * t.d_data[b] :
+ * t.d_data[b].d_data[b] :
+ * t.d_data[b].d_data[b].d_data[f(b,b)] : (leaf)
+ * t.d_data[b].d_data[d] :
+ * t.d_data[b].d_data[d].d_data[f(b,d)] : (leaf)
+ *
+ * Leaf nodes store the terms that are indexed by the arguments, for example
+ * term f(d,c) is indexed by the representative arguments (a,c), and is stored
+ * as a the (single) key in the data of t.d_data[a].d_data[c].
+ */
+template <bool ref_count>
+class NodeTemplateTrie
+{
+ public:
+ /** The children of this node. */
+ std::map<NodeTemplate<ref_count>, NodeTemplateTrie<ref_count>> d_data;
+ /** For leaf nodes : does this node have data? */
+ bool hasData() const { return !d_data.empty(); }
+ /** For leaf nodes : get the node corresponding to this leaf. */
+ NodeTemplate<ref_count> getData() const { return d_data.begin()->first; }
+ /**
+ * Returns the term that is indexed by reps, if one exists, or
+ * or returns null otherwise.
+ */
+ NodeTemplate<ref_count> existsTerm(
+ const std::vector<NodeTemplate<ref_count>>& reps) const;
+ /**
+ * Returns the term that is previously indexed by reps, if one exists, or
+ * adds n to the trie, indexed by reps, and returns n.
+ */
+ NodeTemplate<ref_count> addOrGetTerm(
+ NodeTemplate<ref_count> n,
+ const std::vector<NodeTemplate<ref_count>>& reps);
+ /**
+ * Returns false if a term is previously indexed by reps.
+ * Returns true if no term is previously indexed by reps,
+ * and adds n to the trie, indexed by reps.
+ */
+ inline bool addTerm(NodeTemplate<ref_count> n,
+ const std::vector<NodeTemplate<ref_count>>& reps);
+ /** Debug print this trie on Trace c with indentation depth. */
+ void debugPrint(const char* c, unsigned depth = 0) const;
+ /** Clear all data from this trie. */
+ void clear() { d_data.clear(); }
+ /** Is this trie empty? */
+ bool empty() const { return d_data.empty(); }
+}; /* class NodeTemplateTrie */
+
+template <bool ref_count>
+bool NodeTemplateTrie<ref_count>::addTerm(
+ NodeTemplate<ref_count> n, const std::vector<NodeTemplate<ref_count>>& reps)
+{
+ return addOrGetTerm(n, reps) == n;
+}
+
+/** Reference-counted version of the above data structure */
+typedef NodeTemplateTrie<true> NodeTrie;
+/** Non-reference-counted version of the above data structure */
+typedef NodeTemplateTrie<false> TNodeTrie;
+
+} // namespace theory
+} // namespace CVC4
+
+#endif /* __CVC4__EXPR__NODE_TRIE_H */
#include "theory/datatypes/datatypes_rewriter.h"
#include "theory/datatypes/theory_datatypes_type_rules.h"
#include "theory/quantifiers_engine.h"
-#include "theory/quantifiers/term_database.h"
#include "theory/theory_model.h"
#include "theory/type_enumerator.h"
#include "theory/valuation.h"
return EQUALITY_FALSE_IN_MODEL;
}
-
-
-void TheoryDatatypes::addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::TermArgTrie * t2, unsigned arity, unsigned depth, unsigned& n_pairs ){
+void TheoryDatatypes::addCarePairs(TNodeTrie* t1,
+ TNodeTrie* t2,
+ unsigned arity,
+ unsigned depth,
+ unsigned& n_pairs)
+{
if( depth==arity ){
if( t2!=NULL ){
- Node f1 = t1->getNodeData();
- Node f2 = t2->getNodeData();
+ Node f1 = t1->getData();
+ Node f2 = t2->getData();
if( !areEqual( f1, f2 ) ){
Trace("dt-cg") << "Check " << f1 << " and " << f2 << std::endl;
vector< pair<TNode, TNode> > currentPairs;
if( t2==NULL ){
if( depth<(arity-1) ){
//add care pairs internal to each child
- for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = t1->d_data.begin(); it != t1->d_data.end(); ++it ){
- addCarePairs( &it->second, NULL, arity, depth+1, n_pairs );
+ for (std::pair<const TNode, TNodeTrie>& tt : t1->d_data)
+ {
+ addCarePairs(&tt.second, nullptr, arity, depth + 1, n_pairs);
}
}
//add care pairs based on each pair of non-disequal arguments
- for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = t1->d_data.begin(); it != t1->d_data.end(); ++it ){
- std::map< TNode, quantifiers::TermArgTrie >::iterator it2 = it;
+ for (std::map<TNode, TNodeTrie>::iterator it = t1->d_data.begin();
+ it != t1->d_data.end();
+ ++it)
+ {
+ std::map<TNode, TNodeTrie>::iterator it2 = it;
++it2;
for( ; it2 != t1->d_data.end(); ++it2 ){
if( !d_equalityEngine.areDisequal(it->first, it2->first, false) ){
}
}else{
//add care pairs based on product of indices, non-disequal arguments
- for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = t1->d_data.begin(); it != t1->d_data.end(); ++it ){
- for( std::map< TNode, quantifiers::TermArgTrie >::iterator it2 = t2->d_data.begin(); it2 != t2->d_data.end(); ++it2 ){
- if( !d_equalityEngine.areDisequal(it->first, it2->first, false) ){
- if( !areCareDisequal(it->first, it2->first) ){
- addCarePairs( &it->second, &it2->second, arity, depth+1, n_pairs );
+ for (std::pair<const TNode, TNodeTrie>& tt1 : t1->d_data)
+ {
+ for (std::pair<const TNode, TNodeTrie>& tt2 : t2->d_data)
+ {
+ if (!d_equalityEngine.areDisequal(tt1.first, tt2.first, false))
+ {
+ if (!areCareDisequal(tt1.first, tt2.first))
+ {
+ addCarePairs(&tt1.second, &tt2.second, arity, depth + 1, n_pairs);
}
}
}
unsigned n_pairs = 0;
Trace("dt-cg-summary") << "Compute graph for dt..." << d_functionTerms.size() << " " << d_sharedTerms.size() << std::endl;
Trace("dt-cg") << "Build indices..." << std::endl;
- std::map< TypeNode, std::map< Node, quantifiers::TermArgTrie > > index;
+ std::map<TypeNode, std::map<Node, TNodeTrie> > index;
std::map< Node, unsigned > arity;
//populate indices
unsigned functionTerms = d_functionTerms.size();
}
}
//for each index
- for( std::map< TypeNode, std::map< Node, quantifiers::TermArgTrie > >::iterator iti = index.begin(); iti != index.end(); ++iti ){
- for( std::map< Node, quantifiers::TermArgTrie >::iterator itii = iti->second.begin(); itii != iti->second.end(); ++itii ){
- Trace("dt-cg") << "Process index " << itii->first << ", " << iti->first << "..." << std::endl;
- addCarePairs( &itii->second, NULL, arity[ itii->first ], 0, n_pairs );
+ for (std::pair<const TypeNode, std::map<Node, TNodeTrie> >& tt : index)
+ {
+ for (std::pair<const Node, TNodeTrie>& t : tt.second)
+ {
+ Trace("dt-cg") << "Process index " << tt.first << ", " << t.first << "..."
+ << std::endl;
+ addCarePairs(&t.second, nullptr, arity[t.first], 0, n_pairs);
}
}
Trace("dt-cg-summary") << "...done, # pairs = " << n_pairs << std::endl;
#include "context/cdlist.h"
#include "expr/attribute.h"
#include "expr/datatype.h"
+#include "expr/node_trie.h"
#include "theory/datatypes/datatypes_sygus.h"
#include "theory/theory.h"
#include "theory/uf/equality_engine.h"
namespace CVC4 {
namespace theory {
-
-namespace quantifiers{
- class TermArgTrie;
-}
-
namespace datatypes {
class TheoryDatatypes : public Theory {
TNode getEqcConstructor( TNode r );
protected:
- void addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::TermArgTrie * t2, unsigned arity, unsigned depth, unsigned& n_pairs );
+ void addCarePairs(TNodeTrie* t1,
+ TNodeTrie* t2,
+ unsigned arity,
+ unsigned depth,
+ unsigned& n_pairs);
/** compute care graph */
void computeCareGraph() override;
Node pv,
Node catom,
std::vector<Node>& arg_reps,
- TermArgTrie* tat,
+ TNodeTrie* tat,
unsigned index,
std::map<Node, int>& match_score)
{
if (index == catom.getNumChildren())
{
- Assert(tat->hasNodeData());
- Node gcatom = tat->getNodeData();
+ Assert(tat->hasData());
+ Node gcatom = tat->getData();
Trace("cegqi-epr") << "Matched : " << catom << " and " << gcatom
<< std::endl;
for (unsigned i = 0, nchild = catom.getNumChildren(); i < nchild; i++)
}
return;
}
- std::map<TNode, TermArgTrie>::iterator it = tat->d_data.find(arg_reps[index]);
+ std::map<TNode, TNodeTrie>::iterator it = tat->d_data.find(arg_reps[index]);
if (it != tat->d_data.end())
{
computeMatchScore(
TermDb* tdb = ci->getQuantifiersEngine()->getTermDatabase();
Node rep = ee->getRepresentative(eqc);
Node op = tdb->getMatchOperator(catom);
- TermArgTrie* tat = tdb->getTermArgTrie(rep, op);
+ TNodeTrie* tat = tdb->getTermArgTrie(rep, op);
Trace("cegqi-epr") << "EPR instantiation match term : " << catom
<< ", check ground terms=" << (tat != NULL) << std::endl;
if (tat)
#include <map>
#include <vector>
+#include "expr/node_trie.h"
#include "theory/quantifiers/cegqi/ceg_instantiator.h"
namespace CVC4 {
namespace theory {
namespace quantifiers {
-class TermArgTrie;
-
/** Effectively Propositional (EPR) Instantiator
*
* This implements a selection function for the EPR fragment.
Node pv,
Node catom,
std::vector<Node>& arg_reps,
- TermArgTrie* tat,
+ TNodeTrie* tat,
unsigned index,
std::map<Node, int>& match_score);
void computeMatchScore(CegInstantiator* ci,
//initial binding
TNode f = s->getTgFunc( d_typ, d_status_num );
Assert( !eqc.isNull() );
- TermArgTrie * tat = s->getTermDatabase()->getTermArgTrie( eqc, f );
+ TNodeTrie* tat = s->getTermDatabase()->getTermArgTrie(eqc, f);
if( tat ){
d_match_children.push_back( tat->d_data.begin() );
d_match_children_end.push_back( tat->d_data.end() );
#define CONJECTURE_GENERATOR_H
#include "context/cdhashmap.h"
+#include "expr/node_trie.h"
#include "theory/quantifiers_engine.h"
#include "theory/type_enumerator.h"
namespace theory {
namespace quantifiers {
-class TermArgTrie;
-
//algorithm for computing candidate subgoals
class ConjectureGenerator;
//2 : variables must map to non-ground terms
unsigned d_match_mode;
//children
- std::vector< std::map< TNode, TermArgTrie >::iterator > d_match_children;
- std::vector< std::map< TNode, TermArgTrie >::iterator > d_match_children_end;
+ std::vector<std::map<TNode, TNodeTrie>::iterator> d_match_children;
+ std::vector<std::map<TNode, TNodeTrie>::iterator> d_match_children_end;
void reset( TermGenEnv * s, TypeNode tn );
bool getNextTerm( TermGenEnv * s, unsigned depth );
}else{
eq::EqualityEngine* ee = d_qe->getEqualityQuery()->getEngine();
if( ee->hasTerm( eqc ) ){
- quantifiers::TermArgTrie * tat = d_qe->getTermDatabase()->getTermArgTrie( eqc, d_op );
+ TNodeTrie* tat = d_qe->getTermDatabase()->getTermArgTrie(eqc, d_op);
if( tat ){
//create an equivalence class iterator in eq class eqc
Node rep = ee->getRepresentative( eqc );
Trigger* tparent)
{
int addedLemmas = 0;
- quantifiers::TermArgTrie* tat;
+ TNodeTrie* tat;
if( d_eqc.isNull() ){
tat = qe->getTermDatabase()->getTermArgTrie( d_op );
}else{
if (tat && !qe->inConflict())
{
Node r = qe->getEqualityQuery()->getRepresentative(d_eqc);
- for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = tat->d_data.begin(); it != tat->d_data.end(); ++it ){
- if( it->first!=r ){
+ for (std::pair<const TNode, TNodeTrie>& t : tat->d_data)
+ {
+ if (t.first != r)
+ {
InstMatch m( q );
- addInstantiations( m, qe, addedLemmas, 0, &(it->second) );
+ addInstantiations(m, qe, addedLemmas, 0, &(t.second));
if( qe->inConflict() ){
break;
}
QuantifiersEngine* qe,
int& addedLemmas,
unsigned argIndex,
- quantifiers::TermArgTrie* tat)
+ TNodeTrie* tat)
{
Debug("simple-trigger-debug") << "Add inst " << argIndex << " " << d_match_pattern << std::endl;
if (argIndex == d_match_pattern.getNumChildren())
{
Assert( !tat->d_data.empty() );
- TNode t = tat->getNodeData();
+ TNode t = tat->getData();
Debug("simple-trigger") << "Actual term is " << t << std::endl;
//convert to actual used terms
for (std::map<unsigned, int>::iterator it = d_var_num.begin();
if( d_match_pattern[argIndex].getKind()==INST_CONSTANT ){
int v = d_var_num[argIndex];
if( v!=-1 ){
- for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = tat->d_data.begin(); it != tat->d_data.end(); ++it ){
- Node t = it->first;
+ for (std::pair<const TNode, TNodeTrie>& tt : tat->d_data)
+ {
+ Node t = tt.first;
Node prev = m.get( v );
//using representatives, just check if equal
Assert( t.getType().isComparableTo( d_match_pattern_arg_types[argIndex] ) );
if( prev.isNull() || prev==t ){
m.setValue( v, t);
- addInstantiations( m, qe, addedLemmas, argIndex+1, &(it->second) );
+ addInstantiations(m, qe, addedLemmas, argIndex + 1, &(tt.second));
m.setValue( v, prev);
if( qe->inConflict() ){
break;
//inst constant from another quantified formula, treat as ground term TODO: remove this?
}
Node r = qe->getEqualityQuery()->getRepresentative( d_match_pattern[argIndex] );
- std::map< TNode, quantifiers::TermArgTrie >::iterator it = tat->d_data.find( r );
+ std::map<TNode, TNodeTrie>::iterator it = tat->d_data.find(r);
if( it!=tat->d_data.end() ){
addInstantiations( m, qe, addedLemmas, argIndex+1, &(it->second) );
}
#define __CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_H
#include <map>
+#include "expr/node_trie.h"
#include "theory/quantifiers/inst_match_trie.h"
namespace CVC4 {
namespace theory {
class QuantifiersEngine;
-namespace quantifiers{
- class TermArgTrie;
-}
namespace inst {
QuantifiersEngine* qe,
int& addedLemmas,
unsigned argIndex,
- quantifiers::TermArgTrie* tat);
+ TNodeTrie* tat);
};/* class InstMatchGeneratorSimple */
}
}
#include <string>
#include <vector>
#include "expr/node.h"
+#include "expr/node_trie.h"
#include "expr/type_node.h"
#include "theory/quantifiers/instantiate.h"
-#include "theory/quantifiers/term_database.h"
#include "theory/quantifiers_engine.h"
namespace CVC4 {
TNode getCongruentTermExp( Node f, std::vector< TNode >& args, std::vector< Node >& exp );
private:
/** term index */
- std::map< Node, TermArgTrie > d_uf_func_map_trie;
- /** union find for terms beyond what is stored in equality engine */
- std::map< Node, Node > d_uf;
- std::map< Node, std::vector< Node > > d_uf_exp;
- Node getUfRepresentative( Node a, std::vector< Node >& exp );
- /** disequality list, stores explanations */
- std::map< Node, std::map< Node, std::vector< Node > > > d_diseq_list;
- /** add arg */
- void addArgument( Node n, std::vector< Node >& args, std::vector< Node >& watch, bool is_watch );
- /** register term */
- void registerUfTerm( TNode n );
+ std::map<Node, TNodeTrie> d_uf_func_map_trie;
+ /** union find for terms beyond what is stored in equality engine */
+ std::map<Node, Node> d_uf;
+ std::map<Node, std::vector<Node> > d_uf_exp;
+ Node getUfRepresentative(Node a, std::vector<Node>& exp);
+ /** disequality list, stores explanations */
+ std::map<Node, std::map<Node, std::vector<Node> > > d_diseq_list;
+ /** add arg */
+ void addArgument(Node n,
+ std::vector<Node>& args,
+ std::vector<Node>& watch,
+ bool is_watch);
+ /** register term */
+ void registerUfTerm(TNode n);
+
public:
enum {
STATUS_CONFLICT,
}
}
-void LtePartialInst::getPartialInstantiations( std::vector< Node >& conj, Node q, Node bvl,
- std::vector< Node >& vars, std::vector< Node >& terms, std::vector< TypeNode >& types, TermArgTrie * curr,
- unsigned pindex, unsigned paindex, unsigned iindex ){
+void LtePartialInst::getPartialInstantiations(std::vector<Node>& conj,
+ Node q,
+ Node bvl,
+ std::vector<Node>& vars,
+ std::vector<Node>& terms,
+ std::vector<TypeNode>& types,
+ TNodeTrie* curr,
+ unsigned pindex,
+ unsigned paindex,
+ unsigned iindex)
+{
if( iindex==vars.size() ){
Node body = q[1].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() );
if( bvl.isNull() ){
//start traversing term index for the operator
curr = d_quantEngine->getTermDatabase()->getTermArgTrie( pat.getOperator() );
}
- for( std::map< TNode, TermArgTrie >::iterator it = curr->d_data.begin(); it != curr->d_data.end(); ++it ){
- terms[d_pat_var_order[q][iindex]] = it->first;
- getPartialInstantiations( conj, q, bvl, vars, terms, types, &it->second, pindex, paindex+1, iindex+1 );
+ for (std::pair<const TNode, TNodeTrie>& t : curr->d_data)
+ {
+ terms[d_pat_var_order[q][iindex]] = t.first;
+ getPartialInstantiations(conj,
+ q,
+ bvl,
+ vars,
+ terms,
+ types,
+ &t.second,
+ pindex,
+ paindex + 1,
+ iindex + 1);
}
}
}else{
#ifndef __CVC4__THEORY__LOCAL_THEORY_EXT_H
#define __CVC4__THEORY__LOCAL_THEORY_EXT_H
-#include "theory/quantifiers_engine.h"
#include "context/cdo.h"
+#include "expr/node_trie.h"
+#include "theory/quantifiers_engine.h"
namespace CVC4 {
namespace theory {
namespace quantifiers {
-class TermArgTrie;
-
class LtePartialInst : public QuantifiersModule {
private:
// was this module invoked
void reset();
/** get instantiations */
void getInstantiations( std::vector< Node >& lemmas );
- void getPartialInstantiations( std::vector< Node >& conj, Node q, Node bvl,
- std::vector< Node >& vars, std::vector< Node >& inst, std::vector< TypeNode >& types, TermArgTrie * curr,
- unsigned pindex, unsigned paindex, unsigned iindex );
+ void getPartialInstantiations(std::vector<Node>& conj,
+ Node q,
+ Node bvl,
+ std::vector<Node>& vars,
+ std::vector<Node>& inst,
+ std::vector<TypeNode>& types,
+ TNodeTrie* curr,
+ unsigned pindex,
+ unsigned paindex,
+ unsigned iindex);
/** get eligible inst variables */
void getEligibleInstVars( Node n, std::map< Node, bool >& vars );
Assert( isHandledUfTerm( d_n ) );
TNode f = getMatchOperator( p, d_n );
Debug("qcf-match-debug") << " reset: Var will match operators of " << f << std::endl;
- TermArgTrie * qni = p->getTermDatabase()->getTermArgTrie( Node::null(), f );
+ TNodeTrie* qni = p->getTermDatabase()->getTermArgTrie(Node::null(), f);
if (qni == nullptr || qni->empty())
{
//inform irrelevant quantifiers
}else{
//binding a variable
d_qni_bound[index] = repVar;
- std::map< TNode, TermArgTrie >::iterator it = d_qn[index]->d_data.begin();
+ std::map<TNode, TNodeTrie>::iterator it =
+ d_qn[index]->d_data.begin();
if( it != d_qn[index]->d_data.end() ) {
d_qni.push_back( it );
//set the match
}
if( !val.isNull() ){
//constrained by val
- std::map< TNode, TermArgTrie >::iterator it = d_qn[index]->d_data.find( val );
+ std::map<TNode, TNodeTrie>::iterator it =
+ d_qn[index]->d_data.find(val);
if( it!=d_qn[index]->d_data.end() ){
Debug("qcf-match-debug") << " Match" << std::endl;
d_qni.push_back( it );
#include "context/cdhashmap.h"
#include "context/cdlist.h"
-#include "theory/quantifiers/term_database.h"
+#include "expr/node_trie.h"
#include "theory/quantifiers_engine.h"
namespace CVC4 {
MatchGen * getChild( int i ) { return &d_children[d_children_order[i]]; }
//MatchGen * getChild( int i ) { return &d_children[i]; }
//current matching information
- std::vector< TermArgTrie * > d_qn;
- std::vector< std::map< TNode, TermArgTrie >::iterator > d_qni;
+ std::vector<TNodeTrie*> d_qn;
+ std::vector<std::map<TNode, TNodeTrie>::iterator> d_qni;
bool doMatching( QuantConflictFind * p, QuantInfo * qi );
//for matching : each index is either a variable or a ground term
unsigned d_qni_size;
namespace theory {
namespace quantifiers {
-TNode TermArgTrie::existsTerm( std::vector< TNode >& reps, int argIndex ) {
- if( argIndex==(int)reps.size() ){
- if( d_data.empty() ){
- return Node::null();
- }else{
- return d_data.begin()->first;
- }
- }else{
- std::map< TNode, TermArgTrie >::iterator it = d_data.find( reps[argIndex] );
- if( it==d_data.end() ){
- return Node::null();
- }else{
- return it->second.existsTerm( reps, argIndex+1 );
- }
- }
-}
-
-bool TermArgTrie::addTerm( TNode n, std::vector< TNode >& reps, int argIndex ){
- return addOrGetTerm( n, reps, argIndex )==n;
-}
-
-TNode TermArgTrie::addOrGetTerm( TNode n, std::vector< TNode >& reps, int argIndex ) {
- if( argIndex==(int)reps.size() ){
- if( d_data.empty() ){
- //store n in d_data (this should be interpretted as the "data" and not as a reference to a child)
- d_data[n].clear();
- return n;
- }else{
- return d_data.begin()->first;
- }
- }else{
- return d_data[reps[argIndex]].addOrGetTerm( n, reps, argIndex+1 );
- }
-}
-
-void TermArgTrie::debugPrint( const char * c, Node n, unsigned depth ) {
- for( std::map< TNode, TermArgTrie >::iterator it = d_data.begin(); it != d_data.end(); ++it ){
- for( unsigned i=0; i<depth; i++ ){ Trace(c) << " "; }
- Trace(c) << it->first << std::endl;
- it->second.debugPrint( c, n, depth+1 );
- }
-}
-
TermDb::TermDb(context::Context* c, context::UserContext* u,
QuantifiersEngine* qe)
: d_quantEngine(qe),
return true;
}
-TermArgTrie * TermDb::getTermArgTrie( Node f ) {
+TNodeTrie* TermDb::getTermArgTrie(Node f)
+{
if( options::ufHo() ){
f = getOperatorRepresentative( f );
}
computeUfTerms( f );
- std::map< Node, TermArgTrie >::iterator itut = d_func_map_trie.find( f );
+ std::map<Node, TNodeTrie>::iterator itut = d_func_map_trie.find(f);
if( itut!=d_func_map_trie.end() ){
return &itut->second;
}else{
}
}
-TermArgTrie * TermDb::getTermArgTrie( Node eqc, Node f ) {
+TNodeTrie* TermDb::getTermArgTrie(Node eqc, Node f)
+{
if( options::ufHo() ){
f = getOperatorRepresentative( f );
}
computeUfEqcTerms( f );
- std::map< Node, TermArgTrie >::iterator itut = d_func_map_eqc_trie.find( f );
+ std::map<Node, TNodeTrie>::iterator itut = d_func_map_eqc_trie.find(f);
if( itut==d_func_map_eqc_trie.end() ){
return NULL;
}else{
if( eqc.isNull() ){
return &itut->second;
}else{
- std::map< TNode, TermArgTrie >::iterator itute = itut->second.d_data.find( eqc );
+ std::map<TNode, TNodeTrie>::iterator itute =
+ itut->second.d_data.find(eqc);
if( itute!=itut->second.d_data.end() ){
return &itute->second;
}else{
f = getOperatorRepresentative( f );
}
computeUfTerms( f );
- std::map< Node, TermArgTrie >::iterator itut = d_func_map_trie.find( f );
+ std::map<Node, TNodeTrie>::iterator itut = d_func_map_trie.find(f);
if( itut!=d_func_map_trie.end() ){
computeArgReps( n );
return itut->second.existsTerm( d_arg_reps[n] );
#include <unordered_set>
#include "expr/attribute.h"
+#include "expr/node_trie.h"
+#include "theory/quantifiers/quant_util.h"
#include "theory/theory.h"
#include "theory/type_enumerator.h"
-#include "theory/quantifiers/quant_util.h"
namespace CVC4 {
namespace theory {
namespace quantifiers {
-/** Term arg trie class
-*
-* This also referred to as a "term index" or a "signature table".
-*
-* This data structure stores a set expressions, indexed by representatives of
-* their arguments.
-*
-* For example, consider the equivalence classes :
-*
-* { a, d, f( d, c ), f( a, c ) }
-* { b, f( b, d ) }
-* { c, f( b, b ) }
-*
-* where the first elements ( a, b, c ) are the representatives of these classes.
-* The TermArgTrie t we may build for f is :
-*
-* t :
-* t.d_data[a] :
-* t.d_data[a].d_data[c] :
-* t.d_data[a].d_data[c].d_data[f(d,c)] : (leaf)
-* t.d_data[b] :
-* t.d_data[b].d_data[b] :
-* t.d_data[b].d_data[b].d_data[f(b,b)] : (leaf)
-* t.d_data[b].d_data[d] :
-* t.d_data[b].d_data[d].d_data[f(b,d)] : (leaf)
-*
-* Leaf nodes store the terms that are indexed by the arguments, for example
-* term f(d,c) is indexed by the representative arguments (a,c), and is stored
-* as a the (single) key in the data of t.d_data[a].d_data[c].
-*/
-class TermArgTrie {
-public:
- /** the data */
- std::map< TNode, TermArgTrie > d_data;
-public:
- /** for leaf nodes : does this trie have data? */
- bool hasNodeData() { return !d_data.empty(); }
- /** for leaf nodes : get term corresponding to this leaf */
- TNode getNodeData() { return d_data.begin()->first; }
- /** exists term
- * Returns the term that is indexed by reps, if one exists, or
- * or returns null otherwise.
- */
- TNode existsTerm(std::vector<TNode>& reps, int argIndex = 0);
- /** add or get term
- * Returns the term that is previously indexed by reps, if one exists, or
- * Adds n to the trie, indexed by reps, and returns n.
- */
- TNode addOrGetTerm(TNode n, std::vector<TNode>& reps, int argIndex = 0);
- /** add term
- * Returns false if a term is previously indexed by reps.
- * Returns true if no term is previously indexed by reps,
- * and adds n to the trie, indexed by reps, and returns n.
- */
- bool addTerm(TNode n, std::vector<TNode>& reps, int argIndex = 0);
- /** debug print this trie */
- void debugPrint(const char* c, Node n, unsigned depth = 0);
- /** clear all data from this trie */
- void clear() { d_data.clear(); }
- /** is empty */
- bool empty() { return d_data.empty(); }
-};/* class TermArgTrie */
-
namespace fmcheck {
class FullModelChecker;
}
* The primary responsibilities for this class are to :
* (1) Maintain a list of all ground terms that exist in the quantifier-free
* solvers, as notified through the master equality engine.
- * (2) Build TermArgTrie objects that index all ground terms, per operator.
+ * (2) Build TNodeTrie objects that index all ground terms, per operator.
*
* Like other utilities, its reset(...) function is called
* at the beginning of full or last call effort checks.
* This initializes the database for the round. However,
- * notice that TermArgTrie objects are computed
+ * notice that TNodeTrie objects are computed
* lazily for performance reasons.
*/
class TermDb : public QuantifiersUtil {
*/
Node getMatchOperator(Node n);
/** get term arg index for all f-applications in the current context */
- TermArgTrie* getTermArgTrie(Node f);
+ TNodeTrie* getTermArgTrie(Node f);
/** get the term arg trie for f-applications in the equivalence class of eqc.
*/
- TermArgTrie* getTermArgTrie(Node eqc, Node f);
+ TNodeTrie* getTermArgTrie(Node eqc, Node f);
/** get congruent term
* If possible, returns a term t such that:
* (1) t is a term that is currently indexed by this database,
/** mapping from terms to representatives of their arguments */
std::map< TNode, std::vector< TNode > > d_arg_reps;
/** map from operators to trie */
- std::map< Node, TermArgTrie > d_func_map_trie;
- std::map< Node, TermArgTrie > d_func_map_eqc_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;
/** has map */
#include "expr/node_algorithm.h"
#include "options/sets_options.h"
#include "smt/smt_statistics_registry.h"
-#include "theory/quantifiers/term_database.h"
#include "theory/sets/normal_form.h"
#include "theory/sets/theory_sets.h"
#include "theory/theory_model.h"
d_equalityEngine.addTriggerTerm(n, THEORY_SETS);
}
-void TheorySetsPrivate::addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::TermArgTrie * t2, unsigned arity, unsigned depth, unsigned& n_pairs ){
+void TheorySetsPrivate::addCarePairs(TNodeTrie* t1,
+ TNodeTrie* t2,
+ unsigned arity,
+ unsigned depth,
+ unsigned& n_pairs)
+{
if( depth==arity ){
if( t2!=NULL ){
- Node f1 = t1->getNodeData();
- Node f2 = t2->getNodeData();
+ Node f1 = t1->getData();
+ Node f2 = t2->getData();
if( !ee_areEqual( f1, f2 ) ){
Trace("sets-cg") << "Check " << f1 << " and " << f2 << std::endl;
vector< pair<TNode, TNode> > currentPairs;
if( t2==NULL ){
if( depth<(arity-1) ){
//add care pairs internal to each child
- for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = t1->d_data.begin(); it != t1->d_data.end(); ++it ){
- addCarePairs( &it->second, NULL, arity, depth+1, n_pairs );
+ for (std::pair<const TNode, TNodeTrie>& t : t1->d_data)
+ {
+ addCarePairs(&t.second, NULL, arity, depth + 1, n_pairs);
}
}
//add care pairs based on each pair of non-disequal arguments
- for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = t1->d_data.begin(); it != t1->d_data.end(); ++it ){
- std::map< TNode, quantifiers::TermArgTrie >::iterator it2 = it;
+ for (std::map<TNode, TNodeTrie>::iterator it = t1->d_data.begin();
+ it != t1->d_data.end();
+ ++it)
+ {
+ std::map<TNode, TNodeTrie>::iterator it2 = it;
++it2;
for( ; it2 != t1->d_data.end(); ++it2 ){
if( !d_equalityEngine.areDisequal(it->first, it2->first, false) ){
}
}else{
//add care pairs based on product of indices, non-disequal arguments
- for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = t1->d_data.begin(); it != t1->d_data.end(); ++it ){
- for( std::map< TNode, quantifiers::TermArgTrie >::iterator it2 = t2->d_data.begin(); it2 != t2->d_data.end(); ++it2 ){
- if( !d_equalityEngine.areDisequal(it->first, it2->first, false) ){
- if( !ee_areCareDisequal(it->first, it2->first) ){
- addCarePairs( &it->second, &it2->second, arity, depth+1, n_pairs );
+ for (std::pair<const TNode, TNodeTrie>& tt1 : t1->d_data)
+ {
+ for (std::pair<const TNode, TNodeTrie>& tt2 : t2->d_data)
+ {
+ if (!d_equalityEngine.areDisequal(tt1.first, tt2.first, false))
+ {
+ if (!ee_areCareDisequal(tt1.first, tt2.first))
+ {
+ addCarePairs(&tt1.second, &tt2.second, arity, depth + 1, n_pairs);
}
}
}
unsigned n_pairs = 0;
Trace("sets-cg-summary") << "Compute graph for sets, op=" << it->first << "..." << it->second.size() << std::endl;
Trace("sets-cg") << "Build index for " << it->first << "..." << std::endl;
- std::map< TypeNode, quantifiers::TermArgTrie > index;
+ std::map<TypeNode, TNodeTrie> index;
unsigned arity = 0;
//populate indices
for( unsigned i=0; i<it->second.size(); i++ ){
}
if( arity>0 ){
//for each index
- for( std::map< TypeNode, quantifiers::TermArgTrie >::iterator iti = index.begin(); iti != index.end(); ++iti ){
- Trace("sets-cg") << "Process index " << iti->first << "..." << std::endl;
- addCarePairs( &iti->second, NULL, arity, 0, n_pairs );
+ for (std::pair<const TypeNode, TNodeTrie>& tt : index)
+ {
+ Trace("sets-cg") << "Process index " << tt.first << "..."
+ << std::endl;
+ addCarePairs(&tt.second, nullptr, arity, 0, n_pairs);
}
}
Trace("sets-cg-summary") << "...done, # pairs = " << n_pairs << std::endl;
#include "context/cdhashset.h"
#include "context/cdqueue.h"
-
+#include "expr/node_trie.h"
+#include "theory/sets/theory_sets_rels.h"
#include "theory/theory.h"
#include "theory/uf/equality_engine.h"
-#include "theory/sets/theory_sets_rels.h"
namespace CVC4 {
namespace theory {
-
-namespace quantifiers{
- class TermArgTrie;
-}
-
namespace sets {
/** Internal classes, forward declared here */
Node getUnivSet( TypeNode tn );
bool hasLemmaCached( Node lem );
bool hasProcessed();
-
- void addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::TermArgTrie * t2, unsigned arity, unsigned depth, unsigned& n_pairs );
-
+
+ void addCarePairs(TNodeTrie* t1,
+ TNodeTrie* t2,
+ unsigned arity,
+ unsigned depth,
+ unsigned& n_pairs);
+
Node d_true;
Node d_false;
Node d_zero;
#include "smt/logic_exception.h"
#include "smt/smt_statistics_registry.h"
#include "theory/ext_theory.h"
-#include "theory/quantifiers/term_database.h"
#include "theory/rewriter.h"
#include "theory/strings/theory_strings_rewriter.h"
#include "theory/strings/type_enumerator.h"
}
}
-void TheoryStrings::addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::TermArgTrie * t2, unsigned arity, unsigned depth ) {
+void TheoryStrings::addCarePairs(TNodeTrie* t1,
+ TNodeTrie* t2,
+ unsigned arity,
+ unsigned depth)
+{
if( depth==arity ){
if( t2!=NULL ){
- Node f1 = t1->getNodeData();
- Node f2 = t2->getNodeData();
+ Node f1 = t1->getData();
+ Node f2 = t2->getData();
if( !d_equalityEngine.areEqual( f1, f2 ) ){
Trace("strings-cg-debug") << "TheoryStrings::computeCareGraph(): checking function " << f1 << " and " << f2 << std::endl;
vector< pair<TNode, TNode> > currentPairs;
if( t2==NULL ){
if( depth<(arity-1) ){
//add care pairs internal to each child
- for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = t1->d_data.begin(); it != t1->d_data.end(); ++it ){
- addCarePairs( &it->second, NULL, arity, depth+1 );
+ for (std::pair<const TNode, TNodeTrie>& tt : t1->d_data)
+ {
+ addCarePairs(&tt.second, nullptr, arity, depth + 1);
}
}
//add care pairs based on each pair of non-disequal arguments
- for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = t1->d_data.begin(); it != t1->d_data.end(); ++it ){
- std::map< TNode, quantifiers::TermArgTrie >::iterator it2 = it;
+ for (std::map<TNode, TNodeTrie>::iterator it = t1->d_data.begin();
+ it != t1->d_data.end();
+ ++it)
+ {
+ std::map<TNode, TNodeTrie>::iterator it2 = it;
++it2;
for( ; it2 != t1->d_data.end(); ++it2 ){
if( !d_equalityEngine.areDisequal(it->first, it2->first, false) ){
}
}else{
//add care pairs based on product of indices, non-disequal arguments
- for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = t1->d_data.begin(); it != t1->d_data.end(); ++it ){
- for( std::map< TNode, quantifiers::TermArgTrie >::iterator it2 = t2->d_data.begin(); it2 != t2->d_data.end(); ++it2 ){
- if( !d_equalityEngine.areDisequal(it->first, it2->first, false) ){
- if( !areCareDisequal(it->first, it2->first) ){
- addCarePairs( &it->second, &it2->second, arity, depth+1 );
+ for (std::pair<const TNode, TNodeTrie>& tt1 : t1->d_data)
+ {
+ for (std::pair<const TNode, TNodeTrie>& tt2 : t2->d_data)
+ {
+ if (!d_equalityEngine.areDisequal(tt1.first, tt2.first, false))
+ {
+ if (!areCareDisequal(tt1.first, tt2.first))
+ {
+ addCarePairs(&tt1.second, &tt2.second, arity, depth + 1);
}
}
}
void TheoryStrings::computeCareGraph(){
//computing the care graph here is probably still necessary, due to operators that take non-string arguments TODO: verify
Trace("strings-cg") << "TheoryStrings::computeCareGraph(): Build term indices..." << std::endl;
- std::map< Node, quantifiers::TermArgTrie > index;
+ std::map<Node, TNodeTrie> index;
std::map< Node, unsigned > arity;
unsigned functionTerms = d_functionsTerms.size();
for (unsigned i = 0; i < functionTerms; ++ i) {
}
}
//for each index
- for( std::map< Node, quantifiers::TermArgTrie >::iterator itii = index.begin(); itii != index.end(); ++itii ){
- Trace("strings-cg") << "TheoryStrings::computeCareGraph(): Process index " << itii->first << "..." << std::endl;
- addCarePairs( &itii->second, NULL, arity[ itii->first ], 0 );
+ for (std::pair<const Node, TNodeTrie>& tt : index)
+ {
+ Trace("strings-cg") << "TheoryStrings::computeCareGraph(): Process index "
+ << tt.first << "..." << std::endl;
+ addCarePairs(&tt.second, nullptr, arity[tt.first], 0);
}
}
#include "context/cdhashset.h"
#include "context/cdlist.h"
#include "expr/attribute.h"
+#include "expr/node_trie.h"
#include "theory/decision_manager.h"
#include "theory/strings/regexp_elim.h"
#include "theory/strings/regexp_operation.h"
namespace CVC4 {
namespace theory {
-
-namespace quantifiers{
- class TermArgTrie;
-}
-
namespace strings {
/**
//--------------------------------end for checkMemberships
private:
- void addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::TermArgTrie * t2, unsigned arity, unsigned depth );
+ void addCarePairs(TNodeTrie* t1,
+ TNodeTrie* t2,
+ unsigned arity,
+ unsigned depth);
public:
/** preregister term */
#include "theory/theory_model.h"
#include "theory/type_enumerator.h"
#include "theory/uf/theory_uf_strong_solver.h"
-#include "theory/quantifiers/term_database.h"
#include "options/theory_options.h"
#include "theory/uf/theory_uf_rewriter.h"
return false;
}
-//TODO: move quantifiers::TermArgTrie to src/theory/
-void TheoryUF::addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::TermArgTrie * t2, unsigned arity, unsigned depth ){
+void TheoryUF::addCarePairs(TNodeTrie* t1,
+ TNodeTrie* t2,
+ unsigned arity,
+ unsigned depth)
+{
if( depth==arity ){
if( t2!=NULL ){
- Node f1 = t1->getNodeData();
- Node f2 = t2->getNodeData();
+ Node f1 = t1->getData();
+ Node f2 = t2->getData();
if( !d_equalityEngine.areEqual( f1, f2 ) ){
Debug("uf::sharing") << "TheoryUf::computeCareGraph(): checking function " << f1 << " and " << f2 << std::endl;
vector< pair<TNode, TNode> > currentPairs;
if( t2==NULL ){
if( depth<(arity-1) ){
//add care pairs internal to each child
- for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = t1->d_data.begin(); it != t1->d_data.end(); ++it ){
- addCarePairs( &it->second, NULL, arity, depth+1 );
+ for (std::pair<const TNode, TNodeTrie>& tt : t1->d_data)
+ {
+ addCarePairs(&tt.second, NULL, arity, depth + 1);
}
}
//add care pairs based on each pair of non-disequal arguments
- for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = t1->d_data.begin(); it != t1->d_data.end(); ++it ){
- std::map< TNode, quantifiers::TermArgTrie >::iterator it2 = it;
+ for (std::map<TNode, TNodeTrie>::iterator it = t1->d_data.begin();
+ it != t1->d_data.end();
+ ++it)
+ {
+ std::map<TNode, TNodeTrie>::iterator it2 = it;
++it2;
for( ; it2 != t1->d_data.end(); ++it2 ){
if( !d_equalityEngine.areDisequal(it->first, it2->first, false) ){
}
}else{
//add care pairs based on product of indices, non-disequal arguments
- for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = t1->d_data.begin(); it != t1->d_data.end(); ++it ){
- for( std::map< TNode, quantifiers::TermArgTrie >::iterator it2 = t2->d_data.begin(); it2 != t2->d_data.end(); ++it2 ){
- if( !d_equalityEngine.areDisequal(it->first, it2->first, false) ){
- if( !areCareDisequal(it->first, it2->first) ){
- addCarePairs( &it->second, &it2->second, arity, depth+1 );
+ for (std::pair<const TNode, TNodeTrie>& tt1 : t1->d_data)
+ {
+ for (std::pair<const TNode, TNodeTrie>& tt2 : t2->d_data)
+ {
+ if (!d_equalityEngine.areDisequal(tt1.first, tt2.first, false))
+ {
+ if (!areCareDisequal(tt1.first, tt2.first))
+ {
+ addCarePairs(&tt1.second, &tt2.second, arity, depth + 1);
}
}
}
if (d_sharedTerms.size() > 0) {
//use term indexing
Debug("uf::sharing") << "TheoryUf::computeCareGraph(): Build term indices..." << std::endl;
- std::map< Node, quantifiers::TermArgTrie > index;
+ std::map<Node, TNodeTrie> index;
std::map< Node, unsigned > arity;
unsigned functionTerms = d_functionsTerms.size();
for (unsigned i = 0; i < functionTerms; ++ i) {
}
}
if( has_trigger_arg ){
- index[op].addTerm( f1, reps, arg_start_index );
+ index[op].addTerm(f1, reps);
arity[op] = reps.size();
}
}
//for each index
- for( std::map< Node, quantifiers::TermArgTrie >::iterator itii = index.begin(); itii != index.end(); ++itii ){
- Debug("uf::sharing") << "TheoryUf::computeCareGraph(): Process index " << itii->first << "..." << std::endl;
- addCarePairs( &itii->second, NULL, arity[ itii->first ], 0 );
+ for (std::pair<const Node, TNodeTrie>& tt : index)
+ {
+ Debug("uf::sharing") << "TheoryUf::computeCareGraph(): Process index "
+ << tt.first << "..." << std::endl;
+ addCarePairs(&tt.second, nullptr, arity[tt.first], 0);
}
Debug("uf::sharing") << "TheoryUf::computeCareGraph(): finished." << std::endl;
}
#ifndef __CVC4__THEORY__UF__THEORY_UF_H
#define __CVC4__THEORY__UF__THEORY_UF_H
+#include "context/cdhashset.h"
+#include "context/cdo.h"
#include "expr/node.h"
-//#include "expr/attribute.h"
-
+#include "expr/node_trie.h"
#include "theory/theory.h"
#include "theory/uf/equality_engine.h"
#include "theory/uf/symmetry_breaker.h"
-#include "context/cdo.h"
-#include "context/cdhashset.h"
-
-
namespace CVC4 {
namespace theory {
-
-namespace quantifiers{
- class TermArgTrie;
-}
-
namespace uf {
class UfTermDb;
}
private:
bool areCareDisequal(TNode x, TNode y);
- void addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::TermArgTrie * t2, unsigned arity, unsigned depth );
+ void addCarePairs(TNodeTrie* t1,
+ TNodeTrie* t2,
+ unsigned arity,
+ unsigned depth);
};/* class TheoryUF */
}/* CVC4::theory::uf namespace */
projects / cvc5.git / commitdiff