summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/fmf/model_builder.h
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2019-08-05 12:04:02 -0500
committerGitHub <noreply@github.com>2019-08-05 12:04:02 -0500
commitd14fbb0eb27226e3a7d86733c087e469e797d1ef (patch)
tree7c4f0301ca6a103c203156ba7899b15c086b0645 /src/theory/quantifiers/fmf/model_builder.h
parentd3070131bace10028498003c2f6cfd6f40a50358 (diff)
Remove forward declarations in quantifiers engine (#3156)
Diffstat (limited to 'src/theory/quantifiers/fmf/model_builder.h')
-rw-r--r--src/theory/quantifiers/fmf/model_builder.h5
1 files changed, 3 insertions, 2 deletions
diff --git a/src/theory/quantifiers/fmf/model_builder.h b/src/theory/quantifiers/fmf/model_builder.h
index 1b4d24779..c8f59defe 100644
--- a/src/theory/quantifiers/fmf/model_builder.h
+++ b/src/theory/quantifiers/fmf/model_builder.h
@@ -17,9 +17,10 @@
#ifndef CVC4__THEORY__QUANTIFIERS__MODEL_BUILDER_H
#define CVC4__THEORY__QUANTIFIERS__MODEL_BUILDER_H
-#include "theory/quantifiers_engine.h"
+#include "expr/node.h"
+#include "theory/quantifiers/first_order_model.h"
+#include "theory/quantifiers/inst_match.h"
#include "theory/theory_model_builder.h"
-#include "theory/uf/theory_uf_model.h"
namespace CVC4 {
namespace theory {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback