diff options
| author | Morgan Deters <mdeters@gmail.com> | 2010-02-25 18:26:22 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2010-02-25 18:26:22 +0000 |
| commit | 374e28dcc625f1694cfc87f7b4c376dc329694c4 (patch) | |
| tree | 0f65baaf336a8033617dd2c1cdaa1ffccc10d3f7 /src/theory/output_channel.h | |
| parent | 826f583ee14b922f39666dc827a5624fff753724 (diff) | |
* src/expr/node_builder.h: fixed some overly-aggressive refcount decrementing.
There remain memory leaks (and some over-decrementing of refcounts) that
I've identified; another commit forthcoming.
* src/expr/attribute.h: keys are now NodeValue* instead of TNode
* src/theory/output_channel.h: change OutputChannel::conflict() to the
negation of what we had before: it now takes an AND of TRUE literals
as a conflict clause rather than an OR of FALSE ones.
* src/expr/node.cpp: (non-template) CVC4::expr::debugPrint() routine
for use inside gdb
* src/expr/node.h: remove Node::debugPrint() member (now a function
instead of a member function, since Node is now a template it wasn't
being properly instantiated(?) and couldn't be called from gdb)
* src/expr/Makefile.am: add node.cpp
* src/expr/node_manager.h: code formatting
Diffstat (limited to 'src/theory/output_channel.h')
| -rw-r--r-- | src/theory/output_channel.h | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h index ad558e115..efd2911ef 100644 --- a/src/theory/output_channel.h +++ b/src/theory/output_channel.h @@ -58,8 +58,9 @@ public: * Indicate a theory conflict has arisen. * * @param n - a conflict at the current decision level. This should - * be an OR-kinded node of literals that are false in the current - * assignment. + * be an AND-kinded node of literals that are TRUE in the current + * assignment and are in conflict (i.e., at least one must be + * assigned false). * * @param safe - whether it is safe to be interrupted */ |