summaryrefslogtreecommitdiff
path: root/src/theory/arrays
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/arrays')
-rw-r--r--src/theory/arrays/array_info.h3
-rw-r--r--src/theory/arrays/proof_checker.h1
-rw-r--r--src/theory/arrays/theory_arrays.h1
3 files changed, 0 insertions, 5 deletions
diff --git a/src/theory/arrays/array_info.h b/src/theory/arrays/array_info.h
index 5adb0e783..499f96bfb 100644
--- a/src/theory/arrays/array_info.h
+++ b/src/theory/arrays/array_info.h
@@ -18,14 +18,11 @@
#ifndef CVC4__THEORY__ARRAYS__ARRAY_INFO_H
#define CVC4__THEORY__ARRAYS__ARRAY_INFO_H
-#include <iostream>
-#include <map>
#include <tuple>
#include <unordered_map>
#include "context/backtrackable.h"
#include "context/cdlist.h"
-#include "context/cdhashmap.h"
#include "expr/node.h"
#include "util/statistics_registry.h"
diff --git a/src/theory/arrays/proof_checker.h b/src/theory/arrays/proof_checker.h
index a8d1407a8..053502788 100644
--- a/src/theory/arrays/proof_checker.h
+++ b/src/theory/arrays/proof_checker.h
@@ -19,7 +19,6 @@
#include "expr/node.h"
#include "expr/proof_checker.h"
-#include "expr/proof_node.h"
namespace CVC4 {
namespace theory {
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index 34a7a71b9..689e72a44 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -33,7 +33,6 @@
#include "theory/theory.h"
#include "theory/theory_state.h"
#include "theory/uf/equality_engine.h"
-#include "theory/uf/proof_equality_engine.h"
#include "util/statistics_registry.h"
namespace CVC4 {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback