diff options
| author | Tim King <taking@cs.nyu.edu> | 2010-02-26 18:58:17 +0000 |
|---|---|---|
| committer | Tim King <taking@cs.nyu.edu> | 2010-02-26 18:58:17 +0000 |
| commit | 3311e8276fb6221d9e100be2b1eec88d8f119fef (patch) | |
| tree | ef0ceebcd85b1153a25af7438c4bae96fe5aecb8 /src/theory/uf/theory_uf.h | |
| parent | 12cc3d32407cabbc8c3ed3d980199a020b61a883 (diff) | |
TheoryUFWhite tests are added. There are also accompanying bug fixes. These currently do not pass. (See bug 39.) I modified node.h/cpp to get gdb debug printing working again
Diffstat (limited to 'src/theory/uf/theory_uf.h')
| -rw-r--r-- | src/theory/uf/theory_uf.h | 9 |
1 files changed, 2 insertions, 7 deletions
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index 4fc835223..34b6719d7 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -33,15 +33,10 @@ class TheoryUF : public TheoryImpl<TheoryUF> { private: - + //TODO document + context::CDList<Node> d_assertions; /** - * The associated context. Needed for allocating context dependent objects - * and objects in context dependent memory. - */ - context::Context* d_context; - - /** * List of pending equivalence class merges. * * Tricky part: |