General subscriber infrastructure for NodeManager, as discussed in the

meeting last week.  The SmtEngine now subscribes to NodeManager events,
does appropriate dumping of variable declarations, and notifies the Model
class.

The way to create a skolem is now:

  nodeManager->mkSkolem("myvar_$$", TypeNode, "is a variable created by the theory of Foo")

The first argument is the name of the skolem, and the (optional) "$$" is a
placeholder for the node id (to get a unique name).  Without a "$$", a "_$$"
is automatically appended to the given name.

The second argument is the type.

The (optional, but recommended) third argument is a comment, used by the
dump infrastructure to indicate what the variable is for / who owns it.

An optional fourth argument (not shown) allows you to specify flags that
control the behavior (e.g., don't do notification, and/or don't make a
unique name).  Look at the documentation for details on these.

In particular, the above means you can't just do a mkSkolem(boolType) for
example---you have to specify a name and (hopefully also,
but it's optional) a comment.  This leads to easier debugging than the
anonymous skolems before, since we'll be able to track where the skolems
came from.

Much of the Model and Dump stuff, as well as some Command stuff, is cleaned up
by this commit.  Some remains to be cleaned up.

(this commit was certified error- and warning-free by the test-and-commit script.)

1 files changed, 41 insertions, 0 deletions

diff --git a/src/smt/command_list.h b/src/smt/command_list.h
new file mode 100644
index 000000000..954ef9629
--- /dev/null
+++ b/src/smt/command_list.h
@@ -0,0 +1,41 @@
+/*********************                                                        */
+/*! \file command_list.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief A context-sensitive list of Commands, and their cleanup
+ **
+ ** A context-sensitive list of Commands, and their cleanup.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__SMT__COMMAND_LIST_H
+#define __CVC4__SMT__COMMAND_LIST_H
+
+#include "context/cdlist.h"
+
+namespace CVC4 {
+
+class Command;
+
+namespace smt {
+
+struct CommandCleanup {
+  void operator()(Command** c);
+};/* struct CommandCleanup */
+
+typedef context::CDList<Command*, CommandCleanup> CommandList;
+
+}/* CVC4::smt namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__SMT__COMMAND_LIST_H */