diff options
author | Liana Hadarean <lianahady@gmail.com> | 2013-04-10 00:03:02 -0400 |
---|---|---|
committer | lianah <lianahady@gmail.com> | 2013-04-30 15:54:24 -0400 |
commit | e4f5359675972341858fe167f454ed5da4d8c115 (patch) | |
tree | 886a38c126ab7c4580087adaa80d2ebaa8ca22ab /src/theory/bv/bv_to_bool.h | |
parent | c52adaace77377e14b2eda5b557d97993e2f97dd (diff) |
more work on boolean lifting
Diffstat (limited to 'src/theory/bv/bv_to_bool.h')
-rw-r--r-- | src/theory/bv/bv_to_bool.h | 30 |
1 files changed, 16 insertions, 14 deletions
diff --git a/src/theory/bv/bv_to_bool.h b/src/theory/bv/bv_to_bool.h index 6e865658f..ef80930b4 100644 --- a/src/theory/bv/bv_to_bool.h +++ b/src/theory/bv/bv_to_bool.h @@ -15,6 +15,7 @@ **/ #include "cvc4_private.h" +#include "theory/bv/theory_bv_utils.h" #ifndef __CVC4__THEORY__BV__BV_TO_BOOL_H #define __CVC4__THEORY__BV__BV_TO_BOOL_H @@ -24,22 +25,25 @@ namespace theory { namespace bv { class BvToBoolVisitor { - typedef unsigned return_type; - typedef __gnu_cxx::hash_set<TNode> TNodeSet; - typedef __gnu_cxx::hash_map<TNode, Node> TNodeNodeMap; - TNodeNodeMap d_bvToBool; + + typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet; + typedef __gnu_cxx::hash_map<TNode, Node, TNodeHashFunction> TNodeNodeMap; + TNodeNodeMap d_cache; TNodeSet d_visited; Node d_one; Node d_zero; - void addBvToBool(TNode bv_term, Node bool_term); - Node toBoolTerm(TNode bv_term) const; - bool hasBoolTerm(TNode bv_term) const; - + void addToCache(TNode bv_term, Node bool_term); + Node getCache(TNode bv_term) const; + bool hasCache(TNode bv_term) const; + + bool isConvertibleToBool(TNode current); + Node convertToBool(TNode current); public: + typedef Node return_type; BvToBoolVisitor() - : d_substitution(), - d_visited, + : d_cache(), + d_visited(), d_one(utils::mkConst(BitVector(1, 1u))), d_zero(utils::mkConst(BitVector(1, 0u))) {} @@ -47,18 +51,16 @@ public: bool alreadyVisited(TNode current, TNode parent); void visit(TNode current, TNode parent); return_type done(TNode node); - Node liftBoolToBV(TNode node); - }; class BvToBoolPreprocessor { BvToBoolVisitor d_visitor; public: BvToBoolPreprocessor() - : d_visitor + : d_visitor() {} ~BvToBoolPreprocessor() {} - Node liftBvToBool(TNode assertion); + Node liftBoolToBV(TNode assertion); }; |