1 /********************* */
2 /*! \file bvintropow2.h
4 ** Top contributors (to current version):
5 ** Liana Hadarean, Morgan Deters, Paul Meng
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
8 ** in the top-level source directory) and their institutional affiliations.
9 ** All rights reserved. See the file COPYING in the top-level source
10 ** directory for licensing information.\endverbatim
12 ** \brief [[ Add one-line brief description here ]]
14 ** [[ Add lengthier description here ]]
15 ** \todo document this file
20 #include "cvc4_private.h"
21 #include "expr/node.h"
24 #include <unordered_map>
26 #ifndef __CVC4__THEORY__BV__BV_INTRO_POW_H
27 #define __CVC4__THEORY__BV__BV_INTRO_POW_H
34 class BVIntroducePow2
{
36 static void pow2Rewrite(std::vector
<Node
>& assertionsToPreprocess
);
39 typedef std::unordered_map
<Node
, Node
, NodeHashFunction
> NodeMap
;
40 static Node
pow2Rewrite(Node assertionsToPreprocess
, NodeMap
& cache
);
45 }/* CVC4::theory::bv namespace */
46 }/* CVC4::theory namespace */
51 #endif /* __CVC4__THEORY__BV__BV_INTRO_POW_H */