diff options
Diffstat (limited to 'src/theory/quantifiers/inst_propagator.h')
| -rw-r--r-- | src/theory/quantifiers/inst_propagator.h | 28 |
1 files changed, 16 insertions, 12 deletions
diff --git a/src/theory/quantifiers/inst_propagator.h b/src/theory/quantifiers/inst_propagator.h index dc1bf6908..1ba359228 100644 --- a/src/theory/quantifiers/inst_propagator.h +++ b/src/theory/quantifiers/inst_propagator.h @@ -22,9 +22,9 @@ #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 { @@ -72,17 +72,21 @@ public: 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, |