diff options
| author | Tim King <taking@cs.nyu.edu> | 2010-02-25 21:55:17 +0000 |
|---|---|---|
| committer | Tim King <taking@cs.nyu.edu> | 2010-02-25 21:55:17 +0000 |
| commit | 175741488a4dd986ad69ee644617ff735b855031 (patch) | |
| tree | 9773d9eaf87793d11570a78618eacaf6b67885b2 /src/theory/uf/theory_uf.h | |
| parent | 374e28dcc625f1694cfc87f7b4c376dc329694c4 (diff) | |
Updated uf to reflect APPLY structure after conversation with Chris. Also corrected conflict generation to reflect this morning's discussion.
Diffstat (limited to 'src/theory/uf/theory_uf.h')
| -rw-r--r-- | src/theory/uf/theory_uf.h | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index 4bb18bd43..4fc835223 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -126,6 +126,9 @@ private: /** Performs Congruence Closure to reflect the new additions to d_pending. */ void merge(); + /** Constructs a conflict from an inconsistent disequality. */ + Node constructConflict(TNode diseq); + }; |