diff options
author | lianah <lianahady@gmail.com> | 2013-01-28 19:04:25 -0500 |
---|---|---|
committer | lianah <lianahady@gmail.com> | 2013-01-28 19:04:25 -0500 |
commit | 5aec0f36fb2e896c24ce122a79bd70678371a249 (patch) | |
tree | e267ea1a4b45af5ab386c1b0fcdebe56d2cb203e /src/theory/bv/slicer.h | |
parent | df01ef792cf9806782b12bc93ddaa139d75346c0 (diff) |
compiling implementation of new slicer finished; need to add debugging information and debug.
Diffstat (limited to 'src/theory/bv/slicer.h')
-rw-r--r-- | src/theory/bv/slicer.h | 127 |
1 files changed, 71 insertions, 56 deletions
diff --git a/src/theory/bv/slicer.h b/src/theory/bv/slicer.h index 288b72bac..7ab40652d 100644 --- a/src/theory/bv/slicer.h +++ b/src/theory/bv/slicer.h @@ -26,7 +26,7 @@ #include "util/bitvector.h" #include "util/statistics_registry.h" - +#include "util/index.h" #include "expr/node.h" #include "theory/bv/theory_bv_utils.h" #ifndef __CVC4__THEORY__BV__SLICER_BV_H @@ -38,10 +38,11 @@ namespace CVC4 { namespace theory { namespace bv { -typedef uint32_t TermId; -typedef uint32_t Index; +typedef Index TermId; +extern const TermId UndefinedId; + /** * Base @@ -51,13 +52,23 @@ class Base { Index d_size; std::vector<uint32_t> d_repr; public: - Base(uint32_t size); + Base(Index size); void sliceAt(Index index); void sliceWith(const Base& other); bool isCutPoint(Index index) const; void diffCutPoints(const Base& other, Base& res) const; bool isEmpty() const; std::string debugPrint() const; + Index getBitwidth() const { return d_size; } + bool operator==(const Base& other) const { + if (other.getBitwidth() != getBitwidth()) + return false; + for (unsigned i = 0; i < d_repr.size(); ++i) { + if (d_repr[i] != other.d_repr[i]) + return false; + } + return true; + } }; /** @@ -72,88 +83,80 @@ struct ExtractTerm { Index high; Index low; ExtractTerm(TermId i, Index h, Index l) - : id (i) - high(h) + : id (i), + high(h), low(l) { - Assert (h >= l && id != -1); + Assert (h >= l && id != UndefinedId); } + Index getBitwidth() const { return high - low + 1; } }; +class UnionFind; + struct NormalForm { Base base; Decomposition decomp; + NormalForm(Index bitwidth) : base(bitwidth), decomp() {} + /** + * Returns the term in the decomposition on which the index i + * falls in + * @param i + * + * @return + */ + TermId getTerm(Index i, const UnionFind& uf) const; }; class UnionFind { class Node { - TermId d_repr; - TermId d_ch1, d_ch2; Index d_bitwidth; + TermId d_ch1, d_ch2; + TermId d_repr; public: Node(Index b) : d_bitwidth(b), - d_ch1(-1), - d_ch2(-1), - d_repr(-1) + d_ch1(UndefinedId), + d_ch2(UndefinedId), + d_repr(UndefinedId) {} TermId getRepr() const { return d_repr; } Index getBitwidth() const { return d_bitwidth; } - bool hasChildren() const { return d_ch1 != -1 && d_ch2 != -1; } + bool hasChildren() const { return d_ch1 != UndefinedId && d_ch2 != UndefinedId; } TermId getChild(Index i) const { Assert (i < 2); - return i == 0? ch1 : ch2; + return i == 0? d_ch1 : d_ch2; } - Index getCutPoint() const { - Assert (d_ch1 != -1 && d_ch2 != -1); - return getNode(d_ch1).getBitwidth(); + Index getCutPoint(const UnionFind& uf) const { + Assert (d_ch1 != UndefinedId && d_ch2 != UndefinedId); + return uf.getNode(d_ch1).getBitwidth(); } void setRepr(TermId id) { - Assert (d_children.empty()); + Assert (! hasChildren()); d_repr = id; } void setChildren(TermId ch1, TermId ch2) { - Assert (d_repr == -1 && d_children.empty()); - markAsNotTopLevel(ch1); - markAsNotTopLevel(ch2); - d_children.push_back(ch1); - d_children.push_back(ch2); + Assert (d_repr == UndefinedId && !hasChildren()); + d_ch1 = ch1; + d_ch2 = ch2; } - - // void setChildren(TermId ch1, TermId ch2, TermId ch3) { - // Assert (d_repr == -1 && d_children.empty()); - // d_children.push_back(ch1); - // d_children.push_back(ch2); - // d_children.push_back(ch3); - // } - }; + /// map from TermId to the nodes that represent them std::vector<Node> d_nodes; - + /// a term is in this set if it is its own representative TermSet d_representatives; - TermSet d_topLevelTerms; - void markAsNotTopLevel(TermId id) { - if (d_topLevelTerms.find(id) != d_topLevelTerms.end()) - d_topLevelTerms.erase(id); - } - - bool isTopLevel(TermId id) { - return d_topLevelTerms.find(id) != d_topLevelTerms.end(); - } - Index getBitwidth(TermId id) { - Assert (id < d_nodes.size()); - return d_nodes[id].getBitwidth(); - } + void getDecomposition(const ExtractTerm& term, Decomposition& decomp); + void handleCommonSlice(const Decomposition& d1, const Decomposition& d2, TermId common); public: UnionFind() @@ -162,32 +165,44 @@ public: {} TermId addTerm(Index bitwidth); + void unionTerms(const ExtractTerm& t1, const ExtractTerm& t2); void merge(TermId t1, TermId t2); - TermId find(TermId t1); - TermId split(TermId term, Index i); - - void getNormalForm(ExtractTerm term, NormalForm& nf); - void alignSlicings(NormalForm& nf1, NormalForm& nf2); + TermId find(TermId t1) const ; + void split(TermId term, Index i); - Node getNode(TermId id) { + void getNormalForm(const ExtractTerm& term, NormalForm& nf); + void alignSlicings(const ExtractTerm& term1, const ExtractTerm& term2); + void ensureSlicing(const ExtractTerm& term); + + Node getNode(TermId id) const { Assert (id < d_nodes.size()); return d_nodes[id]; } + Index getBitwidth(TermId id) const { + Assert (id < d_nodes.size()); + return d_nodes[id].getBitwidth(); + } + }; class Slicer { __gnu_cxx::hash_map<TermId, TNode> d_idToNode; - __gnu_cxx::hash_map<TNode, TermId> d_nodeToId; - UnionFind d_unionFind(); - + __gnu_cxx::hash_map<TNode, TermId, TNodeHashFunction> d_nodeToId; + __gnu_cxx::hash_map<TNode, bool, TNodeHashFunction> d_coreTermCache; + UnionFind d_unionFind; + ExtractTerm registerTerm(TNode node); public: Slicer() - : d_topLevelTerms(), + : d_idToNode(), + d_nodeToId(), + d_coreTermCache(), d_unionFind() {} - void getBaseDecomposition(TNode node, std::vector<Node>& decomp) const; + void getBaseDecomposition(TNode node, std::vector<Node>& decomp); void processEquality(TNode eq); + bool isCoreTerm (TNode node); + static void splitEqualities(TNode node, std::vector<Node>& equalities); }; }/* CVC4::theory::bv namespace */ |