summaryrefslogtreecommitdiff
path: root/src/preprocessing/passes/bv_to_int.h
diff options
context:
space:
mode:
authorGereon Kremer <gereon.kremer@cs.rwth-aachen.de>2021-03-03 17:50:45 +0100
committerGitHub <noreply@github.com>2021-03-03 16:50:45 +0000
commita02a794c383ae2381e1210f53174cefb8d94e615 (patch)
tree0eac511c22ba9eeba1925e3afa4f0542edf5cf60 /src/preprocessing/passes/bv_to_int.h
parent6db84f6e373f9651af48df7b654e3992f68472ac (diff)
More cleanup of includes to reduce compilation times (#6037)
Similar to #6031, this PR implements suggestions from iwyu to reduce the number of includes in header files by introducing forward declarations and moving includes to source files.
Diffstat (limited to 'src/preprocessing/passes/bv_to_int.h')
-rw-r--r--src/preprocessing/passes/bv_to_int.h10
1 files changed, 4 insertions, 6 deletions
diff --git a/src/preprocessing/passes/bv_to_int.h b/src/preprocessing/passes/bv_to_int.h
index dd830d7cf..edcc84622 100644
--- a/src/preprocessing/passes/bv_to_int.h
+++ b/src/preprocessing/passes/bv_to_int.h
@@ -69,10 +69,8 @@
#define __CVC4__PREPROCESSING__PASSES__BV_TO_INT_H
#include "context/cdhashmap.h"
-#include "context/cdo.h"
-#include "context/context.h"
+#include "context/cdhashset.h"
#include "preprocessing/preprocessing_pass.h"
-#include "preprocessing/preprocessing_pass_context.h"
#include "theory/arith/nl/iand_utils.h"
namespace CVC4 {
@@ -104,7 +102,7 @@ class BVToInt : public PreprocessingPass
* @return a node representing the shift.
*
*/
- Node createShiftNode(vector<Node> children,
+ Node createShiftNode(std::vector<Node> children,
uint64_t bvsize,
bool isLeftShift);
@@ -209,7 +207,7 @@ class BVToInt : public PreprocessingPass
*/
Node reconstructNode(Node originalNode,
TypeNode resultType,
- const vector<Node>& translated_children);
+ const std::vector<Node>& translated_children);
/**
* A useful utility function.
@@ -247,7 +245,7 @@ class BVToInt : public PreprocessingPass
* that have children.
*/
Node translateWithChildren(Node original,
- const vector<Node>& translated_children);
+ const std::vector<Node>& translated_children);
/**
* Performs the actual translation to integers for nodes
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback