summaryrefslogtreecommitdiff
path: root/src/theory/arith/arith_preprocess.h
diff options
context:
space:
mode:
authorGereon Kremer <gereon.kremer@cs.rwth-aachen.de>2021-03-09 13:48:43 +0100
committerGitHub <noreply@github.com>2021-03-09 13:48:43 +0100
commit540ef6910a2b7ffeb67bac18dfc489fb4a6115d6 (patch)
tree23b0c78b126cb5b1584b75eca14fe648624a023a /src/theory/arith/arith_preprocess.h
parentb302cb1f92aae1c0954c86065469e5c2b7206e74 (diff)
Some more cleanup of includes (#6083)
This PR does some more cleanup of the includes.
Diffstat (limited to 'src/theory/arith/arith_preprocess.h')
-rw-r--r--src/theory/arith/arith_preprocess.h9
1 files changed, 6 insertions, 3 deletions
diff --git a/src/theory/arith/arith_preprocess.h b/src/theory/arith/arith_preprocess.h
index 69cc02bb9..db0fd7d5e 100644
--- a/src/theory/arith/arith_preprocess.h
+++ b/src/theory/arith/arith_preprocess.h
@@ -18,16 +18,19 @@
#define CVC4__THEORY__ARITH__ARITH_PREPROCESS_H
#include "context/cdhashmap.h"
-#include "theory/arith/arith_state.h"
-#include "theory/arith/inference_manager.h"
#include "theory/arith/operator_elim.h"
#include "theory/logic_info.h"
-#include "theory/skolem_lemma.h"
namespace CVC4 {
namespace theory {
+
+class SkolemLemma;
+
namespace arith {
+class ArithState;
+class InferenceManager;
+
/**
* This module can be used for (on demand) elimination of extended arithmetic
* operators like div, mod, to_int, is_int, sqrt, and so on. It uses the
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback