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, 20 insertions, 7 deletions

diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 9614c8ced..2fa60104c 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -44,12 +44,13 @@
 
 namespace CVC4 {
 
-
 template <bool ref_count> class NodeTemplate;
 typedef NodeTemplate<true> Node;
 typedef NodeTemplate<false> TNode;
 class NodeHashFunction;
 
+class Command;
+
 class DecisionEngine;
 class TheoryEngine;
 
@@ -77,6 +78,9 @@ namespace smt {
   class SmtScope;
 
   void beforeSearch(std::string, bool, SmtEngine*) throw(ModalException);
+
+  struct CommandCleanup;
+  typedef context::CDList<Command*, CommandCleanup> CommandList;
 }/* CVC4::smt namespace */
 
 // TODO: SAT layer (esp. CNF- versus non-clausal solvers under the
@@ -132,6 +136,12 @@ class CVC4_PUBLIC SmtEngine {
   AssignmentSet* d_assignments;
 
   /**
+   * A list of commands that should be in the Model.  Only maintained
+   * if produce-models option is on.
+   */
+  smt::CommandList* d_modelCommands;
+
+  /**
    * The logic we're in.
    */
   LogicInfo d_logic;
@@ -264,6 +274,9 @@ class CVC4_PUBLIC SmtEngine {
   friend class ::CVC4::smt::SmtEnginePrivate;
   friend class ::CVC4::smt::SmtScope;
   friend void ::CVC4::smt::beforeSearch(std::string, bool, SmtEngine*) throw(ModalException);
+  // to access d_modelCommands
+  friend size_t ::CVC4::Model::getNumCommands() const;
+  friend const Command* ::CVC4::Model::getCommand(size_t) const;
 
   StatisticsRegistry* d_statisticsRegistry;
 
@@ -293,6 +306,12 @@ class CVC4_PUBLIC SmtEngine {
   /** time spent in checkModel() */
   TimerStat d_checkModelTime;
 
+  /**
+   * Add to Model command.  This is used for recording a command that should be reported
+   * during a get-model call.
+   */
+  void addToModelCommand(Command* c);
+
 public:
 
   /**
@@ -413,12 +432,6 @@ public:
   CVC4::SExpr getAssignment() throw(ModalException, AssertionException);
 
   /**
-   * Add to Model command.  This is used for recording a command that should be reported
-   * during a get-model call.
-   */
-  void addToModelCommand( Command* c, int c_type );
-
-  /**
    * Get the model (only if immediately preceded by a SAT
    * or INVALID query).  Only permitted if CVC4 was built with model
    * support and produce-models is on.