diff options
| author | lianah <lianahady@gmail.com> | 2013-03-21 19:25:33 -0400 |
|---|---|---|
| committer | lianah <lianahady@gmail.com> | 2013-03-21 19:25:33 -0400 |
| commit | ff8572914d73449b26edba214ad134c596196e32 (patch) | |
| tree | 8a3d70b2d1b4c703edc9757b2d4417ff6c49e393 /src/theory/bv/slicer.h | |
| parent | 43ed2d4e9575232655db7df249ba9be1fc9eba61 (diff) | |
fixed more equality stuff
Diffstat (limited to 'src/theory/bv/slicer.h')
| -rw-r--r-- | src/theory/bv/slicer.h | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/theory/bv/slicer.h b/src/theory/bv/slicer.h index f63cf7284..ab2d5e88f 100644 --- a/src/theory/bv/slicer.h +++ b/src/theory/bv/slicer.h @@ -224,7 +224,7 @@ class UnionFind : public context::ContextNotifyObj { Assert (id < d_nodes.size()); return d_nodes[id].hasChildren(); } - TermId getTopLevel(TermId id) const; + // TermId getTopLevel(TermId id) const; /// setter methods for the internal nodes void setRepr(TermId id, TermId new_repr, ExplanationId reason) { @@ -338,7 +338,7 @@ public: d_coreSolver(coreSolver) {} - void getBaseDecomposition(TNode node, std::vector<Node>& decomp, std::vector<TNode>& explanation); + void getBaseDecomposition(TNode node, std::vector<Node>& decomp, std::vector<Node>& explanation); void registerEquality(TNode eq); ExtractTerm registerTerm(TNode node); void processEquality(TNode eq); @@ -354,7 +354,7 @@ public: ExplanationId getExplanationId(TNode reason) const; bool termInEqualityEngine(TermId id); - void enqueueSplit(TermId id, Index i); + void enqueueSplit(TermId id, Index i, TermId top, TermId bottom); void getNewSplits(std::vector<Node>& splits); static void splitEqualities(TNode node, std::vector<Node>& equalities); static unsigned d_numAddedEqualities; |