summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/term_database.cpp
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2012-11-30 20:38:45 +0000
committerAndrew Reynolds <andrew.j.reynolds@gmail.com>2012-11-30 20:38:45 +0000
commitf28bab562105548413cfca93de5c9b047157a076 (patch)
treebfbe95b9aed35f91b6bd9e3af50fad03ab86f23b /src/theory/quantifiers/term_database.cpp
parent6369830eec077ef112e6cc806cd910c7209eb2db (diff)
quantifiers now uses master equality engine, preparation work to cleanup code
Diffstat (limited to 'src/theory/quantifiers/term_database.cpp')
-rw-r--r--src/theory/quantifiers/term_database.cpp1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 2c2ee0bfe..9a26878b5 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -19,6 +19,7 @@
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/options.h"
#include "theory/rewriterules/efficient_e_matching.h"
+#include "theory/quantifiers/theory_quantifiers.h"
using namespace std;
using namespace CVC4;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback