diff options
author | yoni206 <yoni206@users.noreply.github.com> | 2018-08-22 14:36:13 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-08-22 14:36:13 -0700 |
commit | 810bd1f79ca8416a24d21f72a18b29689d6b57f6 (patch) | |
tree | dd0425ae0d1424420fadb01fb8091555552e4a68 /src/preprocessing/passes/bv_ackermann.h | |
parent | 923bd039728c972fef1bbf1a24f23f735e295bce (diff) |
Generating less consistency lemmas in bv-ackermann preprocessing pass (#2253)
Diffstat (limited to 'src/preprocessing/passes/bv_ackermann.h')
-rw-r--r-- | src/preprocessing/passes/bv_ackermann.h | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/src/preprocessing/passes/bv_ackermann.h b/src/preprocessing/passes/bv_ackermann.h index 197e92178..5f799ffe4 100644 --- a/src/preprocessing/passes/bv_ackermann.h +++ b/src/preprocessing/passes/bv_ackermann.h @@ -26,16 +26,18 @@ #ifndef __CVC4__PREPROCESSING__PASSES__BV_ACKERMANN_H #define __CVC4__PREPROCESSING__PASSES__BV_ACKERMANN_H +#include <unordered_map> +#include "expr/node.h" #include "preprocessing/preprocessing_pass.h" #include "preprocessing/preprocessing_pass_context.h" -#include <unordered_map> - namespace CVC4 { namespace preprocessing { namespace passes { -typedef std::unordered_map<Node, NodeSet, NodeHashFunction> FunctionToArgsMap; +using TNodeSet = std::unordered_set<TNode, TNodeHashFunction>; +using FunctionToArgsMap = + std::unordered_map<TNode, TNodeSet, TNodeHashFunction>; class BVAckermann : public PreprocessingPass { |