diff options
Diffstat (limited to 'src/theory/quantifiers/quant_conflict_find.h')
-rw-r--r-- | src/theory/quantifiers/quant_conflict_find.h | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h index 0469e958b..9fa37a96c 100644 --- a/src/theory/quantifiers/quant_conflict_find.h +++ b/src/theory/quantifiers/quant_conflict_find.h @@ -22,7 +22,7 @@ #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 { @@ -45,8 +45,8 @@ private: 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; |