From 0eb82499822544f96877f317bbbcd4cb7c644614 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Sat, 27 Feb 2010 23:43:24 +0000 Subject: A bag of unrelated fixes to bring trunk more in-line with recent policy discussion (no dead code, no unimplemented unit tests...), and other fixes: * src/expr/node_builder.h: uncomment AndNodeBuilder, OrNodeBuilder, PlusNodeBuilder, and MultNodeBuilder. (These had been dead code for awhile.) * src/expr/node_value.cpp: toString() is much more reasonable now, printing S-exprs and using variable names (instead of printing raw pointer values). Next, we'll want to define a pretty-printing theory interface and perhaps hook this up to that. * test/unit/expr/node_black.h: implement testIterator(), testToString(), and testToStream(). * test/unit/expr/node_builder_black.h: implement testIterator() and testAppend(), and add some code to avoid the warnings on clear() for unused NodeBuilders. * src/expr/node_builder.h: redefine "iterator" to be over Nodes rather than over NodeValues. Doesn't make sense to expose the underlying NodeValues. This shouldn't affect anyone, no one was using NodeBuilder iterators. * fix some comments in source code --- src/theory/theoryof_table_middle.h | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'src/theory/theoryof_table_middle.h') diff --git a/src/theory/theoryof_table_middle.h b/src/theory/theoryof_table_middle.h index 17a945d01..f3ad433a3 100644 --- a/src/theory/theoryof_table_middle.h +++ b/src/theory/theoryof_table_middle.h @@ -10,7 +10,8 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** - ** The theoryOf table. + ** The middle section for the automatically-generated theoryOf table. + ** See the mktheoryof script. **/ namespace CVC4 { -- cgit v1.2.3