diff options
author | lianah <lianahady@gmail.com> | 2013-04-16 10:57:04 -0400 |
---|---|---|
committer | lianah <lianahady@gmail.com> | 2013-04-30 15:54:24 -0400 |
commit | 95a876e4931b94ab97ff40988ce23e34a046387d (patch) | |
tree | 432749f30643cf5c2cfeaf441130b35c57c3497b /src/theory/bv/bv_to_bool.h | |
parent | 6a86536bd25fc7ffa305f25990cf37b8c6566c52 (diff) |
uncompiling new bv to bool lifting
Diffstat (limited to 'src/theory/bv/bv_to_bool.h')
-rw-r--r-- | src/theory/bv/bv_to_bool.h | 36 |
1 files changed, 17 insertions, 19 deletions
diff --git a/src/theory/bv/bv_to_bool.h b/src/theory/bv/bv_to_bool.h index d5673a295..9b1534b41 100644 --- a/src/theory/bv/bv_to_bool.h +++ b/src/theory/bv/bv_to_bool.h @@ -24,33 +24,31 @@ namespace CVC4 { namespace theory { namespace bv { -class BvToBoolVisitor { +typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet; +typedef __gnu_cxx::hash_map<TNode, Node, TNodeHashFunction> TNodeNodeMap; - typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet; - typedef __gnu_cxx::hash_map<TNode, Node, TNodeHashFunction> TNodeNodeMap; +class BvToBoolVisitor { + TNodeNodeMap d_bvToBoolMap; TNodeNodeMap d_cache; - TNodeNodeMap d_bvToBoolTerm; - TNodeSet d_visited; Node d_one; Node d_zero; - void storeBvToBool(TNode bv_term, Node bool_term); - Node getBoolTerm(TNode bv_term) const; - bool hasBoolTerm(TNode bv_term) const; - void addToCache(TNode term, Node new_term); Node getCache(TNode term) const; bool hasCache(TNode term) const; - - bool isConvertibleToBool(TNode current); - Node convertToBool(TNode current); + bool isConvertibleBvTerm(TNode node); + bool isConvertibleBvAtom(TNode node); + Node getBoolForBvTerm(TNode node); + void storeBvToBool(TNode bv_term, TNode bool_term); + Node convertBvAtom(TNode node); + Node convertBvTerm(TNode node); + void check(TNode current, TNode parent); public: typedef Node return_type; - BvToBoolVisitor() - : d_cache(), - d_bvToBoolTerm(), - d_visited(), + BvToBoolVisitor(TNodeNodeMap& bvToBool) + : d_bvToBoolMap(bvToBool), + d_cache(), d_one(utils::mkConst(BitVector(1, 1u))), d_zero(utils::mkConst(BitVector(1, 0u))) {} @@ -60,14 +58,14 @@ public: return_type done(TNode node); }; + class BvToBoolPreprocessor { - BvToBoolVisitor d_visitor; + bool matchesBooleanPatern(TNode node); public: BvToBoolPreprocessor() - : d_visitor() {} ~BvToBoolPreprocessor() {} - Node liftBoolToBV(TNode assertion); + void liftBoolToBV(const std::vector<TNode>& assertions, std::vector<Node>& new_assertions); }; |