diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-11-14 22:58:53 +0000 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-11-14 22:58:53 +0000 |
| commit | 8a672c060d2b3946c542c82bd6ca8f89892216ee (patch) | |
| tree | 6a79291dfb1fa21c2394af6d11a4f1b478a63b12 /src/theory/quantifiers_engine.cpp | |
| parent | 73bf2532d70177ee768c508ef971b969994cea2c (diff) | |
replaced all static member data from rewrite rule triggers, added infrastructure for recognizing quantifier macros
Diffstat (limited to 'src/theory/quantifiers_engine.cpp')
| -rw-r--r-- | src/theory/quantifiers_engine.cpp | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 3f6ba8a0f..b4e046506 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -26,6 +26,7 @@ #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/term_database.h" #include "theory/rewriterules/efficient_e_matching.h" +#include "theory/rewriterules/rr_trigger.h" using namespace std; using namespace CVC4; @@ -40,6 +41,7 @@ d_quant_rel( false ){ //currently do not care about relevance d_eq_query = new EqualityQueryQuantifiersEngine( this ); d_term_db = new quantifiers::TermDb( this ); d_tr_trie = new inst::TriggerTrie; + d_rr_tr_trie = new rrinst::TriggerTrie; d_eem = new EfficientEMatcher( this ); d_hasAddedLemma = false; |