summaryrefslogtreecommitdiff
path: root/src/expr
diff options
context:
space:
mode:
Diffstat (limited to 'src/expr')
-rw-r--r--src/expr/command.cpp8
-rw-r--r--src/expr/expr_manager_template.cpp4
-rw-r--r--src/expr/expr_template.cpp2
-rw-r--r--src/expr/node_manager.cpp63
-rw-r--r--src/expr/node_manager.h133
-rw-r--r--src/expr/symbol_table.cpp20
6 files changed, 170 insertions, 60 deletions
diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index 53ca266f4..8b61e92d3 100644
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -479,8 +479,6 @@ Type DeclareFunctionCommand::getType() const throw() {
}
void DeclareFunctionCommand::invoke(SmtEngine* smtEngine) throw() {
- Dump("declarations") << *this;
- smtEngine->addToModelCommand( clone(), Model::COMMAND_DECLARE_FUN );
d_commandStatus = CommandSuccess::instance();
}
@@ -511,8 +509,6 @@ Type DeclareTypeCommand::getType() const throw() {
}
void DeclareTypeCommand::invoke(SmtEngine* smtEngine) throw() {
- Dump("declarations") << *this;
- smtEngine->addToModelCommand( clone(), Model::COMMAND_DECLARE_SORT );
d_commandStatus = CommandSuccess::instance();
}
@@ -552,7 +548,6 @@ Type DefineTypeCommand::getType() const throw() {
}
void DefineTypeCommand::invoke(SmtEngine* smtEngine) throw() {
- Dump("declarations") << *this;
d_commandStatus = CommandSuccess::instance();
}
@@ -602,7 +597,6 @@ Expr DefineFunctionCommand::getFormula() const throw() {
}
void DefineFunctionCommand::invoke(SmtEngine* smtEngine) throw() {
- //Dump("declarations") << *this; -- done by SmtEngine
try {
if(!d_func.isNull()) {
smtEngine->defineFunction(d_func, d_formals, d_formula);
@@ -1275,8 +1269,6 @@ DatatypeDeclarationCommand::getDatatypes() const throw() {
}
void DatatypeDeclarationCommand::invoke(SmtEngine* smtEngine) throw() {
- Dump("declarations") << *this;
- smtEngine->addToModelCommand( clone(), Model::COMMAND_DECLARE_DATATYPES );
d_commandStatus = CommandSuccess::instance();
}
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 804d3af9a..03f3a04b0 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -646,6 +646,10 @@ ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes,
checkResolvedDatatype(*i);
}
+ for(std::vector<NodeManagerListener*>::iterator i = d_nodeManager->d_listeners.begin(); i != d_nodeManager->d_listeners.end(); ++i) {
+ (*i)->nmNotifyNewDatatypes(dtts);
+ }
+
return dtts;
}
diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index 08c3a2b1e..c607ca0a7 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -140,7 +140,7 @@ Node exportInternal(TNode n, ExprManager* from, ExprManager* to, ExprManagerMapC
// skolems are only available at the Node level (not the Expr level)
TypeNode typeNode = TypeNode::fromType(type);
NodeManager* to_nm = NodeManager::fromExprManager(to);
- Node n = to_nm->mkSkolem(name, typeNode);// FIXME thread safety
+ Node n = to_nm->mkSkolem(name, typeNode, "is a skolem variable imported from another ExprManager");// FIXME thread safety
to_e = n.toExpr();
} else {
Unhandled();
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index fc2eec774..82242cb1c 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -139,7 +139,7 @@ NodeManager::~NodeManager() {
poolRemove( &expr::NodeValue::s_null );
if(Debug.isOn("gc:leaks")) {
- Debug("gc:leaks") << "still in pool:" << std::endl;
+ Debug("gc:leaks") << "still in pool:" << endl;
for(NodeValuePool::const_iterator i = d_nodeValuePool.begin(),
iend = d_nodeValuePool.end();
i != iend;
@@ -147,9 +147,9 @@ NodeManager::~NodeManager() {
Debug("gc:leaks") << " " << *i
<< " id=" << (*i)->d_id
<< " rc=" << (*i)->d_rc
- << " " << **i << std::endl;
+ << " " << **i << endl;
}
- Debug("gc:leaks") << ":end:" << std::endl;
+ Debug("gc:leaks") << ":end:" << endl;
}
delete d_statisticsRegistry;
@@ -183,10 +183,10 @@ void NodeManager::reclaimZombies() {
vector<NodeValue*> zombies;
zombies.reserve(d_zombies.size());
- std::remove_copy_if(d_zombies.begin(),
- d_zombies.end(),
- std::back_inserter(zombies),
- NodeValueReferenceCountNonZero());
+ remove_copy_if(d_zombies.begin(),
+ d_zombies.end(),
+ back_inserter(zombies),
+ NodeValueReferenceCountNonZero());
d_zombies.clear();
for(vector<NodeValue*>::iterator i = zombies.begin();
@@ -200,7 +200,7 @@ void NodeManager::reclaimZombies() {
Debug("gc") << "deleting node value " << nv
<< " [" << nv->d_id << "]: ";
nv->printAst(Debug("gc"));
- Debug("gc") << std::endl;
+ Debug("gc") << endl;
}
// remove from the pool
@@ -251,7 +251,7 @@ TypeNode NodeManager::getType(TNode n, bool check)
bool hasType = getAttribute(n, TypeAttr(), typeNode);
bool needsCheck = check && !getAttribute(n, TypeCheckedAttr());
- Debug("getType") << "getting type for " << n << std::endl;
+ Debug("getType") << "getting type for " << n << endl;
if(needsCheck && !(*d_options)[options::earlyTypeChecking]) {
/* Iterate and compute the children bottom up. This avoids stack
@@ -295,28 +295,57 @@ TypeNode NodeManager::getType(TNode n, bool check)
/* The check should have happened, if we asked for it. */
Assert( !check || getAttribute(n, TypeCheckedAttr()) );
- Debug("getType") << "type of " << n << " is " << typeNode << std::endl;
+ Debug("getType") << "type of " << n << " is " << typeNode << endl;
return typeNode;
}
+Node NodeManager::mkSkolem(const std::string& name, const TypeNode& type, const std::string& comment, int flags) {
+ Node n = NodeBuilder<0>(this, kind::SKOLEM);
+ setAttribute(n, TypeAttr(), type);
+ setAttribute(n, TypeCheckedAttr(), true);
+ if((flags & SKOLEM_EXACT_NAME) == 0) {
+ size_t pos = name.find("$$");
+ if(pos != string::npos) {
+ // replace a "$$" with the node ID
+ stringstream id;
+ id << n.getId();
+ string newName = name;
+ newName.replace(pos, 2, id.str());
+ setAttribute(n, expr::VarNameAttr(), newName);
+ } else {
+ stringstream newName;
+ newName << name << '_' << n.getId();
+ setAttribute(n, expr::VarNameAttr(), newName.str());
+ }
+ } else {
+ setAttribute(n, expr::VarNameAttr(), name);
+ }
+ if((flags & SKOLEM_NO_NOTIFY) == 0) {
+ for(vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
+ (*i)->nmNotifyNewSkolem(n, comment);
+ }
+ }
+ return n;
+}
+
TypeNode NodeManager::mkConstructorType(const DatatypeConstructor& constructor,
TypeNode range) {
- std::vector<TypeNode> sorts;
- Debug("datatypes") << "ctor name: " << constructor.getName() << std::endl;
+ vector<TypeNode> sorts;
+ Debug("datatypes") << "ctor name: " << constructor.getName() << endl;
for(DatatypeConstructor::const_iterator i = constructor.begin();
i != constructor.end();
++i) {
TypeNode selectorType = *(*i).getSelector().getType().d_typeNode;
- Debug("datatypes") << selectorType << std::endl;
+ Debug("datatypes") << selectorType << endl;
TypeNode sort = selectorType[1];
// should be guaranteed here already, but just in case
Assert(!sort.isFunctionLike());
- Debug("datatypes") << "ctor sort: " << sort << std::endl;
+ Debug("datatypes") << "ctor sort: " << sort << endl;
sorts.push_back(sort);
}
- Debug("datatypes") << "ctor range: " << range << std::endl;
+ Debug("datatypes") << "ctor range: " << range << endl;
CheckArgument(!range.isFunctionLike(), range,
"cannot create higher-order function types");
sorts.push_back(range);
@@ -335,7 +364,7 @@ TypeNode NodeManager::mkPredicateSubtype(Expr lambda)
TypeNode tn = lambdan.getType();
if(! tn.isPredicateLike() ||
tn.getArgTypes().size() != 1) {
- std::stringstream ss;
+ stringstream ss;
ss << "expected a predicate of one argument to define predicate subtype, but got type `" << tn << "'";
throw TypeCheckingExceptionPrivate(lambdan, ss.str());
}
@@ -355,7 +384,7 @@ TypeNode NodeManager::mkPredicateSubtype(Expr lambda, Expr witness)
TypeNode tn = lambdan.getType();
if(! tn.isPredicateLike() ||
tn.getArgTypes().size() != 1) {
- std::stringstream ss;
+ stringstream ss;
ss << "expected a predicate of one argument to define predicate subtype, but got type `" << tn << "'";
throw TypeCheckingExceptionPrivate(lambdan, ss.str());
}
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 27d77a646..893fde64b 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -63,6 +63,21 @@ typedef Attribute<attr::SortArityTag, uint64_t> SortArityAttr;
}/* CVC4::expr namespace */
+/**
+ * An interface that an interested party can implement and then subscribe
+ * to NodeManager events via NodeManager::subscribeEvents(this).
+ */
+class NodeManagerListener {
+public:
+ virtual ~NodeManagerListener() { }
+ virtual void nmNotifyNewSort(TypeNode tn) { }
+ virtual void nmNotifyNewSortConstructor(TypeNode tn) { }
+ virtual void nmNotifyInstantiateSortConstructor(TypeNode ctor, TypeNode sort) { }
+ virtual void nmNotifyNewDatatypes(const std::vector<DatatypeType>& datatypes) { }
+ virtual void nmNotifyNewVar(TNode n) { }
+ virtual void nmNotifyNewSkolem(TNode n, const std::string& comment) { }
+};/* class NodeManagerListener */
+
class NodeManager {
template <unsigned nchild_thresh> friend class CVC4::NodeBuilder;
friend class NodeManagerScope;
@@ -70,8 +85,11 @@ class NodeManager {
friend class expr::TypeChecker;
// friends so they can access mkVar() here, which is private
- friend Expr ExprManager::mkVar(const std::string& name, Type type);
- friend Expr ExprManager::mkVar(Type type);
+ friend Expr ExprManager::mkVar(const std::string&, Type);
+ friend Expr ExprManager::mkVar(Type);
+
+ // friend so it can access NodeManager's d_listeners and notify clients
+ friend std::vector<DatatypeType> ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>&, const std::set<Type>&);
/** Predicate for use with STL algorithms */
struct NodeValueReferenceCountNonZero {
@@ -138,6 +156,11 @@ class NodeManager {
Node d_operators[kind::LAST_KIND];
/**
+ * A list of subscribers for NodeManager events.
+ */
+ std::vector<NodeManagerListener*> d_listeners;
+
+ /**
* Look up a NodeValue in the pool associated to this NodeManager.
* The NodeValue argument need not be a "completely-constructed"
* NodeValue. In particular, "non-inlined" constants are permitted
@@ -299,6 +322,19 @@ public:
return d_statisticsRegistry;
}
+ /** Subscribe to NodeManager events */
+ void subscribeEvents(NodeManagerListener* listener) {
+ Assert(std::find(d_listeners.begin(), d_listeners.end(), listener) == d_listeners.end(), "listener already subscribed");
+ d_listeners.push_back(listener);
+ }
+
+ /** Unsubscribe from NodeManager events */
+ void unsubscribeEvents(NodeManagerListener* listener) {
+ std::vector<NodeManagerListener*>::iterator elt = std::find(d_listeners.begin(), d_listeners.end(), listener);
+ Assert(elt != d_listeners.end(), "listener not subscribed");
+ d_listeners.erase(elt);
+ }
+
// general expression-builders
/** Create a node with one child. */
@@ -371,9 +407,39 @@ public:
Node mkBoundVar(const TypeNode& type);
Node* mkBoundVarPtr(const TypeNode& type);
- /** Create a skolem constant with the given type. */
- Node mkSkolem(const TypeNode& type);
- Node mkSkolem(const std::string& name, const TypeNode& type);
+ /**
+ * Optional flags used to control behavior of NodeManager::mkSkolem().
+ * They should be composed with a bitwise OR (e.g.,
+ * "SKOLEM_NO_NOTIFY | SKOLEM_EXACT_NAME"). Of course, SKOLEM_DEFAULT
+ * cannot be composed in such a manner.
+ */
+ enum SkolemFlags {
+ SKOLEM_DEFAULT = 0, /**< default behavior */
+ SKOLEM_NO_NOTIFY = 1, /**< do not notify subscribers */
+ SKOLEM_EXACT_NAME = 2 /**< do not make the name unique by adding the id */
+ };/* enum SkolemFlags */
+
+ /**
+ * Create a skolem constant with the given name, type, and comment.
+ *
+ * @param name the name of the new skolem variable. This name can
+ * contain the special character sequence "$$", in which case the
+ * $$ is replaced with the Node ID. That way a family of skolem
+ * variables can be made with unique identifiers, used in dump,
+ * tracing, and debugging output. By convention, you should probably
+ * call mkSkolem() with a custom name appended with "_$$".
+ *
+ * @param type the type of the skolem variable to create
+ *
+ * @param comment a comment for dumping output; if declarations are
+ * being dumped, this is included in a comment before the declaration
+ * and can be quite useful for debugging
+ *
+ * @param flags an optional mask of bits from SkolemFlags to control
+ * mkSkolem() behavior
+ */
+ Node mkSkolem(const std::string& name, const TypeNode& type,
+ const std::string& comment = "", int flags = SKOLEM_DEFAULT);
/** Create a instantiation constant with the given type. */
Node mkInstConstant(const TypeNode& type);
@@ -1118,13 +1184,23 @@ inline TypeNode NodeManager::mkSort() {
NodeBuilder<1> nb(this, kind::SORT_TYPE);
Node sortTag = NodeBuilder<0>(this, kind::SORT_TAG);
nb << sortTag;
- return nb.constructTypeNode();
+ TypeNode tn = nb.constructTypeNode();
+ for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
+ (*i)->nmNotifyNewSort(tn);
+ }
+ return tn;
}
inline TypeNode NodeManager::mkSort(const std::string& name) {
- TypeNode type = mkSort();
- setAttribute(type, expr::VarNameAttr(), name);
- return type;
+ NodeBuilder<1> nb(this, kind::SORT_TYPE);
+ Node sortTag = NodeBuilder<0>(this, kind::SORT_TAG);
+ nb << sortTag;
+ TypeNode tn = nb.constructTypeNode();
+ setAttribute(tn, expr::VarNameAttr(), name);
+ for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
+ (*i)->nmNotifyNewSort(tn);
+ }
+ return tn;
}
inline TypeNode NodeManager::mkSort(TypeNode constructor,
@@ -1145,6 +1221,9 @@ inline TypeNode NodeManager::mkSort(TypeNode constructor,
nb.append(children);
TypeNode type = nb.constructTypeNode();
setAttribute(type, expr::VarNameAttr(), name);
+ for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
+ (*i)->nmNotifyInstantiateSortConstructor(constructor, type);
+ }
return type;
}
@@ -1157,6 +1236,9 @@ inline TypeNode NodeManager::mkSortConstructor(const std::string& name,
TypeNode type = nb.constructTypeNode();
setAttribute(type, expr::VarNameAttr(), name);
setAttribute(type, expr::SortArityAttr(), arity);
+ for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
+ (*i)->nmNotifyNewSortConstructor(type);
+ }
return type;
}
@@ -1368,15 +1450,25 @@ inline TypeNode NodeManager::mkTypeNode(Kind kind,
inline Node NodeManager::mkVar(const std::string& name, const TypeNode& type) {
- Node n = mkVar(type);
+ Node n = NodeBuilder<0>(this, kind::VARIABLE);
+ setAttribute(n, TypeAttr(), type);
+ setAttribute(n, TypeCheckedAttr(), true);
setAttribute(n, expr::VarNameAttr(), name);
+ for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
+ (*i)->nmNotifyNewVar(n);
+ }
return n;
}
inline Node* NodeManager::mkVarPtr(const std::string& name,
const TypeNode& type) {
- Node* n = mkVarPtr(type);
+ Node* n = NodeBuilder<0>(this, kind::VARIABLE).constructNodePtr();
+ setAttribute(*n, TypeAttr(), type);
+ setAttribute(*n, TypeCheckedAttr(), true);
setAttribute(*n, expr::VarNameAttr(), name);
+ for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
+ (*i)->nmNotifyNewVar(*n);
+ }
return n;
}
@@ -1397,6 +1489,9 @@ inline Node NodeManager::mkVar(const TypeNode& type) {
Node n = NodeBuilder<0>(this, kind::VARIABLE);
setAttribute(n, TypeAttr(), type);
setAttribute(n, TypeCheckedAttr(), true);
+ for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
+ (*i)->nmNotifyNewVar(n);
+ }
return n;
}
@@ -1404,6 +1499,9 @@ inline Node* NodeManager::mkVarPtr(const TypeNode& type) {
Node* n = NodeBuilder<0>(this, kind::VARIABLE).constructNodePtr();
setAttribute(*n, TypeAttr(), type);
setAttribute(*n, TypeCheckedAttr(), true);
+ for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
+ (*i)->nmNotifyNewVar(*n);
+ }
return n;
}
@@ -1421,19 +1519,6 @@ inline Node* NodeManager::mkBoundVarPtr(const TypeNode& type) {
return n;
}
-inline Node NodeManager::mkSkolem(const std::string& name, const TypeNode& type) {
- Node n = mkSkolem(type);
- setAttribute(n, expr::VarNameAttr(), name);
- return n;
-}
-
-inline Node NodeManager::mkSkolem(const TypeNode& type) {
- Node n = NodeBuilder<0>(this, kind::SKOLEM);
- setAttribute(n, TypeAttr(), type);
- setAttribute(n, TypeCheckedAttr(), true);
- return n;
-}
-
inline Node NodeManager::mkInstConstant(const TypeNode& type) {
Node n = NodeBuilder<0>(this, kind::INST_CONSTANT);
n.setAttribute(TypeAttr(), type);
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: "
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback