diff options
author | lianah <lianahady@gmail.com> | 2014-06-10 13:48:45 -0400 |
---|---|---|
committer | lianah <lianahady@gmail.com> | 2014-06-10 13:48:45 -0400 |
commit | 5f072a19d299191dbedc4b69c8e0eda694cfa957 (patch) | |
tree | 0ebfc27bd05d06b0cdb2fc0813b7d5649d36aee4 /src/theory/bv/bv_to_bool.h | |
parent | db51926b5ce806754fc26c81b1b7d3e739fc4fc5 (diff) |
Merging CAV14 paper bit-vector work.
Diffstat (limited to 'src/theory/bv/bv_to_bool.h')
-rw-r--r-- | src/theory/bv/bv_to_bool.h | 57 |
1 files changed, 25 insertions, 32 deletions
diff --git a/src/theory/bv/bv_to_bool.h b/src/theory/bv/bv_to_bool.h index b34923728..28501ba96 100644 --- a/src/theory/bv/bv_to_bool.h +++ b/src/theory/bv/bv_to_bool.h @@ -16,6 +16,7 @@ #include "cvc4_private.h" #include "theory/bv/theory_bv_utils.h" +#include "util/statistics_registry.h" #ifndef __CVC4__THEORY__BV__BV_TO_BOOL_H #define __CVC4__THEORY__BV__BV_TO_BOOL_H @@ -24,51 +25,43 @@ namespace CVC4 { namespace theory { namespace bv { -typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet; -typedef __gnu_cxx::hash_map<Node, Node, TNodeHashFunction> NodeNodeMap; +typedef __gnu_cxx::hash_map<Node, Node, NodeHashFunction> NodeNodeMap; -class BvToBoolVisitor { - NodeNodeMap d_bvToBoolMap; - NodeNodeMap d_cache; +class BvToBoolPreprocessor { + + struct Statistics { + IntStat d_numTermsLifted; + IntStat d_numAtomsLifted; + IntStat d_numTermsForcedLifted; + Statistics(); + ~Statistics(); + }; + + NodeNodeMap d_liftCache; + NodeNodeMap d_boolCache; Node d_one; Node d_zero; - void addToCache(TNode term, Node new_term); - Node getCache(TNode term) const; - bool hasCache(TNode term) const; + void addToBoolCache(TNode term, Node new_term); + Node getBoolCache(TNode term) const; + bool hasBoolCache(TNode term) const; + + void addToLiftCache(TNode term, Node new_term); + Node getLiftCache(TNode term) const; + bool hasLiftCache(TNode term) const; bool isConvertibleBvTerm(TNode node); bool isConvertibleBvAtom(TNode node); - Node getBoolForBvTerm(TNode node); Node convertBvAtom(TNode node); Node convertBvTerm(TNode node); - void check(TNode current, TNode parent); + Node liftNode(TNode current); + Statistics d_statistics; public: - typedef Node return_type; - BvToBoolVisitor() - : d_bvToBoolMap(), - d_cache(), - d_one(utils::mkConst(BitVector(1, 1u))), - d_zero(utils::mkConst(BitVector(1, 0u))) - {} - void start(TNode node); - bool alreadyVisited(TNode current, TNode parent); - void visit(TNode current, TNode parent); - return_type done(TNode node); - void storeBvToBool(TNode bv_term, TNode bool_term); - bool hasBoolTerm(TNode node); + BvToBoolPreprocessor(); + void liftBvToBool(const std::vector<Node>& assertions, std::vector<Node>& new_assertions); }; -class BvToBoolPreprocessor { - bool matchesBooleanPatern(TNode node); -public: - BvToBoolPreprocessor() - {} - ~BvToBoolPreprocessor() {} - void liftBoolToBV(const std::vector<Node>& assertions, std::vector<Node>& new_assertions); -}; - }/* CVC4::theory::bv namespace */ }/* CVC4::theory namespace */ |