summaryrefslogtreecommitdiff
path: root/src/theory/arith/arith_preprocess.h
diff options
context:
space:
mode:
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