diff options
| author | lianah <lianahady@gmail.com> | 2013-04-12 16:15:30 -0400 |
|---|---|---|
| committer | lianah <lianahady@gmail.com> | 2013-04-30 15:54:24 -0400 |
| commit | 6a86536bd25fc7ffa305f25990cf37b8c6566c52 (patch) | |
| tree | 197b931f8f391a21eebbf097fd0f4b5adeb53c09 /src/theory/bv/bv_to_bool.h | |
| parent | e4f5359675972341858fe167f454ed5da4d8c115 (diff) | |
finished implementing bv to bool lifting and added --bv-to-bool option
Diffstat (limited to 'src/theory/bv/bv_to_bool.h')
| -rw-r--r-- | src/theory/bv/bv_to_bool.h | 13 |
1 files changed, 10 insertions, 3 deletions
diff --git a/src/theory/bv/bv_to_bool.h b/src/theory/bv/bv_to_bool.h index ef80930b4..d5673a295 100644 --- a/src/theory/bv/bv_to_bool.h +++ b/src/theory/bv/bv_to_bool.h @@ -29,20 +29,27 @@ class BvToBoolVisitor { typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet; typedef __gnu_cxx::hash_map<TNode, Node, TNodeHashFunction> TNodeNodeMap; TNodeNodeMap d_cache; + TNodeNodeMap d_bvToBoolTerm; TNodeSet d_visited; Node d_one; Node d_zero; - void addToCache(TNode bv_term, Node bool_term); - Node getCache(TNode bv_term) const; - bool hasCache(TNode bv_term) const; + 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); public: typedef Node return_type; BvToBoolVisitor() : d_cache(), + d_bvToBoolTerm(), d_visited(), d_one(utils::mkConst(BitVector(1, 1u))), d_zero(utils::mkConst(BitVector(1, 0u))) |