diff options
Diffstat (limited to 'src/theory/bv/bvintropow2.h')
-rw-r--r-- | src/theory/bv/bvintropow2.h | 34 |
1 files changed, 34 insertions, 0 deletions
diff --git a/src/theory/bv/bvintropow2.h b/src/theory/bv/bvintropow2.h new file mode 100644 index 000000000..3844d03e1 --- /dev/null +++ b/src/theory/bv/bvintropow2.h @@ -0,0 +1,34 @@ + + +#include "cvc4_private.h" +#include "expr/node.h" + +#include <vector> +#include <ext/hash_map> + +#ifndef __CVC4__THEORY__BV__BV_INTRO_POW_H +#define __CVC4__THEORY__BV__BV_INTRO_POW_H + +namespace CVC4 { +namespace theory { +namespace bv { + + +class BVIntroducePow2 { +public: + static void pow2Rewrite(std::vector<Node>& assertionsToPreprocess); + +private: + typedef __gnu_cxx::hash_map<Node, Node, NodeHashFunction> NodeMap; + static Node pow2Rewrite(Node assertionsToPreprocess, NodeMap& cache); +}; + + + +}/* CVC4::theory::bv namespace */ +}/* CVC4::theory namespace */ + +}/* CVC4 namespace */ + + +#endif /* __CVC4__THEORY__BV__BV_INTRO_POW_H */ |