From 540ef6910a2b7ffeb67bac18dfc489fb4a6115d6 Mon Sep 17 00:00:00 2001
From: Gereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Date: Tue, 9 Mar 2021 13:48:43 +0100
Subject: Some more cleanup of includes (#6083)

This PR does some more cleanup of the includes.
---
 src/theory/arith/congruence_manager.h | 31 +++++++++++++++++++++++--------
 1 file changed, 23 insertions(+), 8 deletions(-)

(limited to 'src/theory/arith/congruence_manager.h')

diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h
index f2aef815f..9815ad9c8 100644
--- a/src/theory/arith/congruence_manager.h
+++ b/src/theory/arith/congruence_manager.h
@@ -19,27 +19,42 @@
 
 #pragma once
 
+#include "context/cdhashmap.h"
 #include "context/cdlist.h"
 #include "context/cdmaybe.h"
-#include "context/cdo.h"
 #include "context/cdtrail_queue.h"
-#include "context/context.h"
-#include "expr/proof_node_manager.h"
 #include "theory/arith/arithvar.h"
+#include "theory/arith/arith_utilities.h"
+#include "theory/arith/callbacks.h"
 #include "theory/arith/constraint_forward.h"
-#include "theory/arith/partial_model.h"
-#include "theory/eager_proof_generator.h"
-#include "theory/ee_setup_info.h"
 #include "theory/trust_node.h"
-#include "theory/uf/equality_engine.h"
-#include "theory/uf/proof_equality_engine.h"
+#include "theory/uf/equality_engine_notify.h"
 #include "util/dense_map.h"
 #include "util/statistics_registry.h"
 
 namespace CVC4 {
+
+class ProofNodeManager;
+
+namespace context {
+class Context;
+class UserContext;
+}
+
 namespace theory {
+
+class EagerProofGenerator;
+struct EeSetupInfo;
+
+namespace eq {
+class ProofEqEngine;
+class EqualityEngine;
+}
+
 namespace arith {
 
+class ArithVariables;
+
 class ArithCongruenceManager {
 private:
   context::CDRaised d_inConflict;
-- 
cgit v1.2.3