From 46c12d84290f3ed23bd0b435c6e8e5852ab1af39 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Wed, 19 Sep 2012 21:21:00 +0000
Subject: 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.)
---
 src/expr/symbol_table.cpp | 20 ++++++++++----------
 1 file changed, 10 insertions(+), 10 deletions(-)

(limited to 'src/expr/symbol_table.cpp')

diff --git a/src/expr/symbol_table.cpp b/src/expr/symbol_table.cpp
index c9234b5e0..e3bd898ef 100644
--- a/src/expr/symbol_table.cpp
+++ b/src/expr/symbol_table.cpp
@@ -50,7 +50,7 @@ SymbolTable::~SymbolTable() {
 }
 
 void SymbolTable::bind(const std::string& name, Expr obj,
-                            bool levelZero) throw(AssertionException) {
+                       bool levelZero) throw(AssertionException) {
   CheckArgument(!obj.isNull(), obj, "cannot bind to a null Expr");
   ExprManagerScope ems(obj);
   if(levelZero) d_exprMap->insertAtContextLevelZero(name, obj);
@@ -58,7 +58,7 @@ void SymbolTable::bind(const std::string& name, Expr obj,
 }
 
 void SymbolTable::bindDefinedFunction(const std::string& name, Expr obj,
-                            bool levelZero) throw(AssertionException) {
+                                      bool levelZero) throw(AssertionException) {
   CheckArgument(!obj.isNull(), obj, "cannot bind to a null Expr");
   ExprManagerScope ems(obj);
   if(levelZero){
@@ -89,18 +89,18 @@ Expr SymbolTable::lookup(const std::string& name) const throw(AssertionException
 }
 
 void SymbolTable::bindType(const std::string& name, Type t,
-                                bool levelZero) throw() {
-  if(levelZero){
+                           bool levelZero) throw() {
+  if(levelZero) {
     d_typeMap->insertAtContextLevelZero(name, make_pair(vector<Type>(), t));
-  }else{
+  } else {
     d_typeMap->insert(name, make_pair(vector<Type>(), t));
   }
 }
 
 void SymbolTable::bindType(const std::string& name,
-                                const std::vector<Type>& params,
-                                Type t,
-                                bool levelZero) throw() {
+                           const std::vector<Type>& params,
+                           Type t,
+                           bool levelZero) throw() {
   if(Debug.isOn("sort")) {
     Debug("sort") << "bindType(" << name << ", [";
     if(params.size() > 0) {
@@ -110,7 +110,7 @@ void SymbolTable::bindType(const std::string& name,
     }
     Debug("sort") << "], " << t << ")" << endl;
   }
-  if(levelZero){
+  if(levelZero) {
     d_typeMap->insertAtContextLevelZero(name, make_pair(params, t));
   } else {
     d_typeMap->insert(name, make_pair(params, t));
@@ -131,7 +131,7 @@ Type SymbolTable::lookupType(const std::string& name) const throw(AssertionExcep
 }
 
 Type SymbolTable::lookupType(const std::string& name,
-                                  const std::vector<Type>& params) const throw(AssertionException) {
+                             const std::vector<Type>& params) const throw(AssertionException) {
   pair<vector<Type>, Type> p = (*d_typeMap->find(name)).second;
   Assert(p.first.size() == params.size(),
          "type constructor arity is wrong: "
-- 
cgit v1.2.3