diff options
| author | Morgan Deters <mdeters@gmail.com> | 2012-09-19 21:21:00 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2012-09-19 21:21:00 +0000 |
| commit | 46c12d84290f3ed23bd0b435c6e8e5852ab1af39 (patch) | |
| tree | 64c2d2175eb814b9187d8cc6ccecbddf90151b2a | |
| parent | 7a15b2c1fb45f0cc7480466473f344f8b1f5ed94 (diff) | |
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.)
49 files changed, 551 insertions, 269 deletions
@@ -7,9 +7,10 @@ The core authors and designers of CVC4 are: Morgan Deters <mdeters@cs.nyu.edu>, New York University Yeting Ge <yeting@cs.nyu.edu>, New York University Liana Hadarean <lianah@cs.nyu.edu>, New York University - Tim King <taking@cs.nyu.edu>, New York University Mina Jeong <mjeong@cs.nyu.edu>, New York University Dejan Jovanovic <dejan@cs.nyu.edu>, New York University + Tim King <taking@cs.nyu.edu>, New York University + Andrew Reynolds <andrew.j.reynolds@gmail.com>, University of Iowa Cesare Tinelli <tinelli@cs.uiowa.edu>, University of Iowa CVC4 is the fourth in the CVC series of tools (CVC, CVC Lite, CVC3) but does diff --git a/src/context/cdlist.h b/src/context/cdlist.h index a63bd2d21..4d8aea6cb 100644 --- a/src/context/cdlist.h +++ b/src/context/cdlist.h @@ -226,9 +226,9 @@ public: * Main constructor: d_list starts as NULL, size is 0 */ CDList(Context* context, - bool callDestructor = true, - const CleanUp& cleanup = CleanUp(), - const Allocator& alloc = Allocator()) : + bool callDestructor = true, + const CleanUp& cleanup = CleanUp(), + const Allocator& alloc = Allocator()) : ContextObj(context), d_list(NULL), d_size(0), 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: " diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 6fe55e50e..9bdadc440 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -63,9 +63,6 @@ void Smt2::addTheory(Theory theory) { break; case THEORY_ARRAYS: - // FIXME: should define a paramterized type 'Array' with 2 arguments - mkSort("Array"); - addOperator(kind::SELECT); addOperator(kind::STORE); break; diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp index 85742feef..f8e754868 100644 --- a/src/printer/ast/ast_printer.cpp +++ b/src/printer/ast/ast_printer.cpp @@ -187,7 +187,7 @@ void AstPrinter::toStream(std::ostream& out, const CommandStatus* s) const throw }/* AstPrinter::toStream(CommandStatus*) */ -void AstPrinter::toStream(std::ostream& out, Model* m, Command* c, int c_type ) const throw(){ +void AstPrinter::toStream(std::ostream& out, Model* m, const Command* c) const throw() { out << "Model()"; } diff --git a/src/printer/ast/ast_printer.h b/src/printer/ast/ast_printer.h index 1cac966df..d5701c088 100644 --- a/src/printer/ast/ast_printer.h +++ b/src/printer/ast/ast_printer.h @@ -36,7 +36,7 @@ public: void toStream(std::ostream& out, const Command* c, int toDepth, bool types, size_t dag) const throw(); void toStream(std::ostream& out, const CommandStatus* s) const throw(); //for models - void toStream(std::ostream& out, Model* m, Command* c, int c_type ) const throw(); + void toStream(std::ostream& out, Model* m, const Command* c) const throw(); };/* class AstPrinter */ }/* CVC4::printer::ast namespace */ diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 7f66d6fa0..6791b6c51 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -738,10 +738,10 @@ void CvcPrinter::toStream(std::ostream& out, const CommandStatus* s) const throw }/* CvcPrinter::toStream(CommandStatus*) */ -void CvcPrinter::toStream(std::ostream& out, Model* m, Command* c, int c_type ) const throw(){ +void CvcPrinter::toStream(std::ostream& out, Model* m, const Command* c) const throw() { theory::TheoryModel* tm = (theory::TheoryModel*)m; - if( c_type==Model::COMMAND_DECLARE_SORT ){ - TypeNode tn = TypeNode::fromType( ((DeclareTypeCommand*)c)->getType() ); + if(dynamic_cast<const DeclareTypeCommand*>(c) != NULL) { + TypeNode tn = TypeNode::fromType( ((const DeclareTypeCommand*)c)->getType() ); if( tn.isSort() ){ //print the cardinality if( tm->d_rep_set.d_type_reps.find( tn )!=tm->d_rep_set.d_type_reps.end() ){ @@ -761,8 +761,8 @@ void CvcPrinter::toStream(std::ostream& out, Model* m, Command* c, int c_type ) } } } - }else if( c_type==Model::COMMAND_DECLARE_FUN ){ - Node n = Node::fromExpr( ((DeclareFunctionCommand*)c)->getFunction() ); + } else if(dynamic_cast<const DeclareFunctionCommand*>(c) != NULL) { + Node n = Node::fromExpr( ((const DeclareFunctionCommand*)c)->getFunction() ); TypeNode tn = n.getType(); out << n << " : "; if( tn.isFunction() || tn.isPredicate() ){ @@ -959,12 +959,41 @@ static void toStream(std::ostream& out, const GetOptionCommand* c) throw() { static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c) throw() { const vector<DatatypeType>& datatypes = c->getDatatypes(); + out << "DATATYPE" << endl; + bool firstDatatype = true; for(vector<DatatypeType>::const_iterator i = datatypes.begin(), i_end = datatypes.end(); i != i_end; ++i) { - out << *i; + if(! firstDatatype) { + out << ',' << endl; + } + const Datatype& dt = (*i).getDatatype(); + out << " " << dt.getName() << " = "; + bool firstConstructor = true; + for(Datatype::const_iterator j = dt.begin(); j != dt.end(); ++j) { + if(! firstConstructor) { + out << " | "; + } + firstConstructor = false; + const DatatypeConstructor& c = *j; + out << c.getName(); + if(c.getNumArgs() > 0) { + out << '('; + bool firstSelector = true; + for(DatatypeConstructor::const_iterator k = c.begin(); k != c.end(); ++k) { + if(! firstSelector) { + out << ", "; + } + firstSelector = false; + const DatatypeConstructorArg& selector = *k; + out << selector.getName() << ": " << selector.getType(); + } + out << ')'; + } + } } + out << endl << "END;" << endl; } static void toStream(std::ostream& out, const CommentCommand* c) throw() { diff --git a/src/printer/cvc/cvc_printer.h b/src/printer/cvc/cvc_printer.h index c868025ef..72564f24d 100644 --- a/src/printer/cvc/cvc_printer.h +++ b/src/printer/cvc/cvc_printer.h @@ -39,7 +39,7 @@ public: void toStream(std::ostream& out, const Command* c, int toDepth, bool types, size_t dag) const throw(); void toStream(std::ostream& out, const CommandStatus* s) const throw(); //for models - void toStream(std::ostream& out, Model* m, Command* c, int c_type ) const throw(); + void toStream(std::ostream& out, Model* m, const Command* c) const throw(); };/* class CvcPrinter */ }/* CVC4::printer::cvc namespace */ diff --git a/src/printer/dagification_visitor.cpp b/src/printer/dagification_visitor.cpp index 40b532612..98d6a26bb 100644 --- a/src/printer/dagification_visitor.cpp +++ b/src/printer/dagification_visitor.cpp @@ -136,7 +136,7 @@ void DagificationVisitor::done(TNode node) { // construct the let binder std::stringstream ss; ss << d_letVarPrefix << d_letVar++; - Node letvar = NodeManager::currentNM()->mkSkolem(ss.str(), (*i).getType()); + Node letvar = NodeManager::currentNM()->mkSkolem(ss.str(), (*i).getType(), "dagification", NodeManager::SKOLEM_NO_NOTIFY | NodeManager::SKOLEM_EXACT_NAME); // apply previous substitutions to the rhs, enabling cascading LETs Node n = d_substitutions->apply(*i); diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp index 54482a8c3..eed9842e2 100644 --- a/src/printer/printer.cpp +++ b/src/printer/printer.cpp @@ -128,8 +128,8 @@ void Printer::toStream(std::ostream& out, const SExpr& sexpr) const throw() { }/* Printer::toStream(SExpr) */ void Printer::toStream(std::ostream& out, Model* m) const throw() { - for(size_t i = 0; i < m->getNumCommands(); i++ ){ - toStream(out, m, m->getCommand(i), m->getCommandType(i)); + for(size_t i = 0; i < m->getNumCommands(); ++i) { + toStream(out, m, m->getCommand(i)); } }/* Printer::toStream(Model) */ diff --git a/src/printer/printer.h b/src/printer/printer.h index 6fedc854c..778c21f1f 100644 --- a/src/printer/printer.h +++ b/src/printer/printer.h @@ -83,7 +83,7 @@ public: //for models /** write model response to command */ - virtual void toStream(std::ostream& out, Model* m, Command* c, int c_type ) const throw() = 0; + virtual void toStream(std::ostream& out, Model* m, const Command* c) const throw() = 0; };/* class Printer */ }/* CVC4 namespace */ diff --git a/src/printer/smt/smt_printer.cpp b/src/printer/smt/smt_printer.cpp index 14a680a1e..bc61368c1 100644 --- a/src/printer/smt/smt_printer.cpp +++ b/src/printer/smt/smt_printer.cpp @@ -51,8 +51,8 @@ void SmtPrinter::toStream(std::ostream& out, const SExpr& sexpr) const throw() { Printer::getPrinter(language::output::LANG_SMTLIB_V2)->toStream(out, sexpr); }/* SmtPrinter::toStream() */ -void SmtPrinter::toStream(std::ostream& out, Model* m, Command* c, int c_type ) const throw(){ - Printer::getPrinter(language::output::LANG_SMTLIB_V2)->toStream(out, m, c, c_type); +void SmtPrinter::toStream(std::ostream& out, Model* m, const Command* c) const throw() { + Printer::getPrinter(language::output::LANG_SMTLIB_V2)->toStream(out, m, c); } }/* CVC4::printer::smt namespace */ diff --git a/src/printer/smt/smt_printer.h b/src/printer/smt/smt_printer.h index 1cf7fcf50..a3d62a287 100644 --- a/src/printer/smt/smt_printer.h +++ b/src/printer/smt/smt_printer.h @@ -36,7 +36,7 @@ public: void toStream(std::ostream& out, const CommandStatus* s) const throw(); void toStream(std::ostream& out, const SExpr& sexpr) const throw(); //for models - void toStream(std::ostream& out, Model* m, Command* c, int c_type ) const throw(); + void toStream(std::ostream& out, Model* m, const Command* c) const throw(); };/* class SmtPrinter */ }/* CVC4::printer::smt namespace */ diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index e41fd9c65..28ecc11c4 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -320,8 +320,8 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, // output that support for the kind needs to be added here. out << n.getKind() << ' '; } - if(n.getMetaKind() == kind::metakind::PARAMETERIZED && - stillNeedToPrintParams) { + if( n.getMetaKind() == kind::metakind::PARAMETERIZED && + stillNeedToPrintParams ) { if(toDepth != 0) { toStream(out, n.getOperator(), toDepth < 0 ? toDepth : toDepth - 1, types); } else { @@ -528,10 +528,10 @@ void Smt2Printer::toStream(std::ostream& out, const CommandStatus* s) const thro }/* Smt2Printer::toStream(CommandStatus*) */ -void Smt2Printer::toStream(std::ostream& out, Model* m, Command* c, int c_type ) const throw(){ +void Smt2Printer::toStream(std::ostream& out, Model* m, const Command* c) const throw() { theory::TheoryModel* tm = (theory::TheoryModel*)m; - if( c_type==Model::COMMAND_DECLARE_SORT ){ - TypeNode tn = TypeNode::fromType( ((DeclareTypeCommand*)c)->getType() ); + if(dynamic_cast<const DeclareTypeCommand*>(c) != NULL) { + TypeNode tn = TypeNode::fromType( ((const DeclareTypeCommand*)c)->getType() ); if( tn.isSort() ){ //print the cardinality if( tm->d_rep_set.d_type_reps.find( tn )!=tm->d_rep_set.d_type_reps.end() ){ @@ -551,8 +551,8 @@ void Smt2Printer::toStream(std::ostream& out, Model* m, Command* c, int c_type ) } } } - }else if( c_type==Model::COMMAND_DECLARE_FUN ){ - Node n = Node::fromExpr( ((DeclareFunctionCommand*)c)->getFunction() ); + } else if(dynamic_cast<const DeclareFunctionCommand*>(c) != NULL) { + Node n = Node::fromExpr( ((const DeclareFunctionCommand*)c)->getFunction() ); Node val = tm->getValue( n ); if(val.getKind() == kind::LAMBDA) { out << "(define-fun " << n << " " << val[0] diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h index 475479095..ce48f36f3 100644 --- a/src/printer/smt2/smt2_printer.h +++ b/src/printer/smt2/smt2_printer.h @@ -36,7 +36,7 @@ public: void toStream(std::ostream& out, const Command* c, int toDepth, bool types, size_t dag) const throw(); void toStream(std::ostream& out, const CommandStatus* s) const throw(); //for models - void toStream(std::ostream& out, Model* m, Command* c, int c_type ) const throw(); + void toStream(std::ostream& out, Model* m, const Command* c) const throw(); void toStream(std::ostream& out, const Result& r) const throw(); };/* class Smt2Printer */ diff --git a/src/smt/Makefile.am b/src/smt/Makefile.am index 333c887ee..8aa3e1630 100644 --- a/src/smt/Makefile.am +++ b/src/smt/Makefile.am @@ -10,6 +10,8 @@ libsmt_la_SOURCES = \ smt_engine.h \ smt_engine_scope.cpp \ smt_engine_scope.h \ + command_list.cpp \ + command_list.h \ modal_exception.h \ simplification_mode.h \ simplification_mode.cpp \ diff --git a/src/smt/command_list.cpp b/src/smt/command_list.cpp new file mode 100644 index 000000000..7fb6cf013 --- /dev/null +++ b/src/smt/command_list.cpp @@ -0,0 +1,33 @@ +/********************* */ +/*! \file command_list.cpp + ** \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. + **/ + +// we include both of these to make sure they agree on the typedef +#include "smt/command_list.h" +#include "smt/smt_engine.h" + +#include "expr/command.h" + +namespace CVC4 { +namespace smt { + +void CommandCleanup::operator()(Command** c) { + delete *c; +} + +}/* CVC4::smt namespace */ +}/* CVC4 namespace */ 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 */ diff --git a/src/smt/options_handlers.h b/src/smt/options_handlers.h index 2c20e06bb..4f214ddd1 100644 --- a/src/smt/options_handlers.h +++ b/src/smt/options_handlers.h @@ -73,7 +73,7 @@ benchmark\n\ modes.\n\ \n\ declarations\n\ -+ Dump declarations. Implied by all following modes.\n\ ++ Dump user declarations. Implied by all following modes.\n\ \n\ assertions\n\ + Output the assertions after non-clausal simplification and static\n\ @@ -82,6 +82,11 @@ assertions\n\ (--simplification=none --no-static-learning), the output\n\ will closely resemble the input (with term-level ITEs removed).\n\ \n\ +skolems\n\ ++ Dump internally-created skolem variable declarations. These can\n\ + arise from preprocessing simplifications, existential elimination,\n\ + and a number of other things. Implied by all following modes.\n\ +\n\ learned\n\ + Output the assertions after non-clausal simplification, static\n\ learning, and presolve-time T-lemmas. This should include all eager\n\ @@ -172,6 +177,7 @@ inline void dumpMode(std::string option, std::string optarg, SmtEngine* smt) { if(!strcmp(optargPtr, "benchmark")) { } else if(!strcmp(optargPtr, "declarations")) { } else if(!strcmp(optargPtr, "assertions")) { + } else if(!strcmp(optargPtr, "skolems")) { } else if(!strcmp(optargPtr, "learned")) { } else if(!strcmp(optargPtr, "clauses")) { } else if(!strcmp(optargPtr, "t-conflicts") || @@ -219,6 +225,9 @@ inline void dumpMode(std::string option, std::string optarg, SmtEngine* smt) { Dump.on("benchmark"); if(strcmp(optargPtr, "benchmark")) { Dump.on("declarations"); + if(strcmp(optargPtr, "declarations") && strcmp(optargPtr, "assertions")) { + Dump.on("skolems"); + } } } free(optargPtr); diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 55ea09de4..e28520e70 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -47,6 +47,7 @@ #include "util/boolean_simplification.h" #include "util/configuration.h" #include "util/exception.h" +#include "smt/command_list.h" #include "smt/options.h" #include "options/option_exception.h" #include "util/output.h" @@ -110,7 +111,7 @@ public: * one) becomes an "interface shell" which simply acts as a forwarder * of method calls. */ -class SmtEnginePrivate { +class SmtEnginePrivate : public NodeManagerListener { SmtEngine& d_smt; /** The assertions yet to be preprocessed */ @@ -198,6 +199,51 @@ public: d_propagator(d_nonClausalLearnedLiterals, true, true), d_topLevelSubstitutions(smt.d_userContext), d_lastSubstitutionPos(smt.d_userContext, d_topLevelSubstitutions.end()) { + d_smt.d_nodeManager->subscribeEvents(this); + } + + void nmNotifyNewSort(TypeNode tn) { + DeclareTypeCommand c(tn.getAttribute(expr::VarNameAttr()), + 0, + tn.toType()); + Dump("declarations") << c; + d_smt.addToModelCommand(c.clone()); + } + + void nmNotifyNewSortConstructor(TypeNode tn) { + DeclareTypeCommand c(tn.getAttribute(expr::VarNameAttr()), + tn.getAttribute(expr::SortArityAttr()), + tn.toType()); + Dump("declarations") << c; + d_smt.addToModelCommand(c.clone()); + } + + void nmNotifyNewDatatypes(const std::vector<DatatypeType>& dtts) { + DatatypeDeclarationCommand c(dtts); + Dump("declarations") << c; + d_smt.addToModelCommand(c.clone()); + } + + void nmNotifyNewVar(TNode n) { + DeclareFunctionCommand c(n.getAttribute(expr::VarNameAttr()), + n.toExpr(), + n.getType().toType()); + Dump("declarations") << c; + d_smt.addToModelCommand(c.clone()); + } + + void nmNotifyNewSkolem(TNode n, std::string comment) { + std::string id = n.getAttribute(expr::VarNameAttr()); + DeclareFunctionCommand c(id, + n.toExpr(), + n.getType().toType()); + if(Dump.isOn("skolems")) { + if(comment != "") { + Dump("skolems") << CommentCommand(id + " is " + comment); + } + Dump("skolems") << c; + } + d_smt.addToModelCommand(c.clone()); } Node applySubstitutions(TNode node) const { @@ -254,6 +300,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) : d_definedFunctions(NULL), d_assertionList(NULL), d_assignments(NULL), + d_modelCommands(NULL), d_logic(), d_pendingPops(0), d_fullyInited(false), @@ -316,6 +363,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) : d_context->push(); d_definedFunctions = new(true) DefinedFunctionMap(d_userContext); + d_modelCommands = new(true) smt::CommandList(d_userContext); } void SmtEngine::finishInit() { @@ -388,33 +436,33 @@ void SmtEngine::finalOptionsAreSet() { } void SmtEngine::shutdown() { - if(Dump.isOn("benchmark")) { - Dump("benchmark") << QuitCommand(); - } - doPendingPops(); + while(options::incrementalSolving() && d_userContext->getLevel() > 1) { + internalPop(true); + } + // check to see if a postsolve() is pending if(d_needPostsolve) { d_theoryEngine->postsolve(); d_needPostsolve = false; } - if(d_propEngine != NULL) d_propEngine->shutdown(); - if(d_theoryEngine != NULL) d_theoryEngine->shutdown(); - if(d_decisionEngine != NULL) d_decisionEngine->shutdown(); + if(d_propEngine != NULL) { + d_propEngine->shutdown(); + } + if(d_theoryEngine != NULL) { + d_theoryEngine->shutdown(); + } + if(d_decisionEngine != NULL) { + d_decisionEngine->shutdown(); + } } SmtEngine::~SmtEngine() throw() { SmtScope smts(this); try { - doPendingPops(); - - while(options::incrementalSolving() && d_userContext->getLevel() > 1) { - internalPop(true); - } - shutdown(); // global push/pop around everything, to ensure proper destruction @@ -430,6 +478,10 @@ SmtEngine::~SmtEngine() throw() { d_assertionList->deleteSelf(); } + if(d_modelCommands != NULL) { + d_modelCommands->deleteSelf(); + } + d_definedFunctions->deleteSelf(); StatisticsRegistry::unregisterStat(&d_definitionExpansionTime); @@ -1918,13 +1970,20 @@ CVC4::SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) } -void SmtEngine::addToModelCommand( Command* c, int c_type ){ - Trace("smt") << "SMT addToModelCommand(" << c << ", " << c_type << ")" << endl; +void SmtEngine::addToModelCommand(Command* c) { + Trace("smt") << "SMT addToModelCommand(" << c << ")" << endl; SmtScope smts(this); - finalOptionsAreSet(); - doPendingPops(); - if( options::produceModels() ) { - d_theoryEngine->getModel()->addCommand( c, c_type ); + // If we aren't yet fully inited, the user might still turn on + // produce-models. So let's keep any commands around just in + // case. This is useful in two cases: (1) SMT-LIBv1 auto-declares + // sort "U" in QF_UF before setLogic() is run and we still want to + // support finding card(U) with --finite-model-find, and (2) to + // decouple SmtEngine and ExprManager if the user does a few + // ExprManager::mkSort() before SmtEngine::setOption("produce-models") + // and expects to find their cardinalities in the model. + if( ! d_fullyInited || options::produceModels() ) { + doPendingPops(); + d_modelCommands->push_back(c); } } @@ -1978,7 +2037,7 @@ void SmtEngine::checkModel() throw(InternalErrorException) { theory::SubstitutionMap substitutions(&fakeContext); for(size_t k = 0; k < m->getNumCommands(); ++k) { - DeclareFunctionCommand* c = dynamic_cast<DeclareFunctionCommand*>(m->getCommand(k)); + const DeclareFunctionCommand* c = dynamic_cast<const DeclareFunctionCommand*>(m->getCommand(k)); Notice() << "SmtEngine::checkModel(): model command " << k << " : " << m->getCommand(k) << endl; if(c == NULL) { // we don't care about DECLARE-DATATYPES, DECLARE-SORT, ... @@ -2015,7 +2074,7 @@ void SmtEngine::checkModel() throw(InternalErrorException) { // [func->func2] and checking equality of the Nodes. // (this just a way to check if func is in n.) theory::SubstitutionMap subs(&fakeContext); - Node func2 = NodeManager::currentNM()->mkSkolem(TypeNode::fromType(func.getType())); + Node func2 = NodeManager::currentNM()->mkSkolem("", TypeNode::fromType(func.getType()), "", NodeManager::SKOLEM_NO_NOTIFY); subs.addSubstitution(func, func2); if(subs.apply(n) != n) { Notice() << "SmtEngine::checkModel(): *** PROBLEM: MODEL VALUE DEFINED IN TERMS OF ITSELF ***" << endl; 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. diff --git a/src/theory/arith/dio_solver.cpp b/src/theory/arith/dio_solver.cpp index 83ba49257..c70bc911b 100644 --- a/src/theory/arith/dio_solver.cpp +++ b/src/theory/arith/dio_solver.cpp @@ -28,7 +28,7 @@ namespace arith { inline Node makeIntegerVariable(){ NodeManager* curr = NodeManager::currentNM(); - return curr->mkSkolem(curr->integerType()); + return curr->mkSkolem("intvar", curr->integerType(), "is an integer variable created by the dio solver"); } DioSolver::DioSolver(context::Context* ctxt) : diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 0ec8e1384..e1f93158f 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -737,9 +737,7 @@ void TheoryArrays::check(Effort e) { TNode k; std::hash_map<TNode, Node, TNodeHashFunction>::iterator it = d_diseqCache.find(fact); if (it == d_diseqCache.end()) { - Node newk = nm->mkSkolem(indexType); - Dump.declareVar(newk.toExpr(), - "an extensional lemma index variable from the theory of arrays"); + Node newk = nm->mkSkolem("array_ext_index_$$", indexType, "an extensional lemma index variable from the theory of arrays"); d_diseqCache[fact] = newk; k = newk; } diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h index 7bc1d956d..b7fd3c351 100644 --- a/src/theory/builtin/theory_builtin_type_rules.h +++ b/src/theory/builtin/theory_builtin_type_rules.h @@ -175,7 +175,7 @@ public: } inline static Node mkGroundTerm(TypeNode type) { Assert(type.getKind() == kind::SORT_TYPE); - return NodeManager::currentNM()->mkSkolem( type ); + return NodeManager::currentNM()->mkSkolem("groundTerm_$$", type, "a ground term created for type " + type.toString()); } };/* class SortProperties */ diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h index 8349a1479..d20107958 100644 --- a/src/theory/bv/theory_bv_utils.h +++ b/src/theory/bv/theory_bv_utils.h @@ -68,7 +68,7 @@ inline Node mkFalse() { inline Node mkVar(unsigned size) { NodeManager* nm = NodeManager::currentNM(); - return nm->mkSkolem(nm->mkBitVectorType(size)); + return nm->mkSkolem("bv_$$", nm->mkBitVectorType(size), "is a variable created by the theory of bitvectors"); } inline Node mkAnd(std::vector<TNode>& children) { diff --git a/src/theory/ite_simplifier.cpp b/src/theory/ite_simplifier.cpp index 6eb777ad5..dd87557f2 100644 --- a/src/theory/ite_simplifier.cpp +++ b/src/theory/ite_simplifier.cpp @@ -148,7 +148,7 @@ Node ITESimplifier::getSimpVar(TypeNode t) return (*it).second; } else { - Node var = NodeManager::currentNM()->mkSkolem(t); + Node var = NodeManager::currentNM()->mkSkolem("iteSimp_$$", t, "is a variable resulting from ITE simplification"); d_simpVars[t] = var; return var; } diff --git a/src/theory/model.cpp b/src/theory/model.cpp index 42654b74c..8aec39309 100644 --- a/src/theory/model.cpp +++ b/src/theory/model.cpp @@ -53,14 +53,14 @@ Node TheoryModel::getValue( TNode n ){ return getModelValue( nn ); } -Expr TheoryModel::getValue( const Expr& expr ){ +Expr TheoryModel::getValue( Expr expr ){ Node n = Node::fromExpr( expr ); Node ret = getValue( n ); return ret.toExpr(); } /** get cardinality for sort */ -Cardinality TheoryModel::getCardinality( const Type& t ){ +Cardinality TheoryModel::getCardinality( Type t ){ TypeNode tn = TypeNode::fromType( t ); //for now, we only handle cardinalities for uninterpreted sorts if( tn.isSort() ){ @@ -373,7 +373,7 @@ Node DefaultModel::getInterpretedValue( TNode n ){ } if( default_v.isNull() ){ //choose default value from model if none exists - default_v = getInterpretedValue( NodeManager::currentNM()->mkSkolem( type.getRangeType() ) ); + default_v = getInterpretedValue( NodeManager::currentNM()->mkSkolem( "defaultValue_$$", type.getRangeType(), "a default value term from model construction" ) ); } ufmt.setDefaultValue( this, default_v ); ufmt.simplify(); diff --git a/src/theory/model.h b/src/theory/model.h index 85f5dd31b..adf97df9e 100644 --- a/src/theory/model.h +++ b/src/theory/model.h @@ -115,9 +115,9 @@ public: bool areDisequal( Node a, Node b ); public: /** get value function for Exprs. */ - Expr getValue( const Expr& expr ); + Expr getValue( Expr expr ); /** get cardinality for sort */ - Cardinality getCardinality( const Type& t ); + Cardinality getCardinality( Type t ); /** to stream function */ void toStream( std::ostream& out ); public: diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index b0728de29..c6987a85a 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -384,7 +384,7 @@ Node QuantifiersRewriter::computeCNF( Node n, std::vector< Node >& args, NodeBui TypeNode typ = NodeManager::currentNM()->mkFunctionType( argTypes, NodeManager::currentNM()->booleanType() ); std::stringstream ss; ss << "cnf_" << n.getKind() << "_" << n.getId(); - Node op = NodeManager::currentNM()->mkSkolem( ss.str(), typ ); + Node op = NodeManager::currentNM()->mkSkolem( ss.str(), typ, "was created by the quantifiers rewriter" ); std::vector< Node > predArgs; predArgs.push_back( op ); predArgs.insert( predArgs.end(), activeArgs.begin(), activeArgs.end() ); @@ -486,7 +486,7 @@ Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, b terms.push_back( body[0][i] ); //make the new function symbol TypeNode typ = NodeManager::currentNM()->mkFunctionType( argTypes, body[0][i].getType() ); - Node op = NodeManager::currentNM()->mkSkolem( typ ); + Node op = NodeManager::currentNM()->mkSkolem( "op_$$", typ, "was created by the quantifiers rewriter" ); std::vector< Node > funcArgs; funcArgs.push_back( op ); funcArgs.insert( funcArgs.end(), args.begin(), args.end() ); diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index bd6b03a78..7b5d9e6e2 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -198,7 +198,7 @@ Node TermDb::getModelBasisTerm( TypeNode tn, int i ){ std::stringstream ss; ss << Expr::setlanguage(options::outputLanguage()); ss << "e_" << tn; - mbt = NodeManager::currentNM()->mkSkolem( ss.str(), tn ); + mbt = NodeManager::currentNM()->mkSkolem( ss.str(), tn, "is a model basis term" ); Trace("mkVar") << "ModelBasis:: Make variable " << mbt << " : " << tn << std::endl; }else{ mbt = d_type_map[ tn ][ 0 ]; @@ -307,7 +307,7 @@ Node TermDb::getSkolemizedBody( Node f ){ if( d_skolem_body.find( f )==d_skolem_body.end() ){ std::vector< Node > vars; for( int i=0; i<(int)f[0].getNumChildren(); i++ ){ - Node skv = NodeManager::currentNM()->mkSkolem( f[0][i].getType() ); + Node skv = NodeManager::currentNM()->mkSkolem( "skv_$$", f[0][i].getType(), "is a termdb-created skolemized body" ); d_skolem_constants[ f ].push_back( skv ); vars.push_back( f[0][i] ); } @@ -343,7 +343,7 @@ Node TermDb::getFreeVariableForInstConstant( Node n ){ d_free_vars[tn] = NodeManager::currentNM()->mkConst( z ); }else{ if( d_type_map[ tn ].empty() ){ - d_free_vars[tn] = NodeManager::currentNM()->mkSkolem( tn ); + d_free_vars[tn] = NodeManager::currentNM()->mkSkolem( "freevar_$$", tn, "is a free variable created by termdb" ); Trace("mkVar") << "FreeVar:: Make variable " << d_free_vars[tn] << " : " << tn << std::endl; }else{ d_free_vars[tn] = d_type_map[ tn ][ 0 ]; diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp index aaca53464..4a5bb2247 100644 --- a/src/theory/rep_set.cpp +++ b/src/theory/rep_set.cpp @@ -112,7 +112,7 @@ void RepSetIterator::initialize(){ TypeNode tn = d_types[i];
if( tn.isSort() ){
if( !d_rep_set->hasType( tn ) ){
- Node var = NodeManager::currentNM()->mkSkolem( tn );
+ Node var = NodeManager::currentNM()->mkSkolem( "repSet_$$", tn, "is a variable created by the RepSetIterator" );
Trace("mkVar") << "RepSetIterator:: Make variable " << var << " : " << tn << std::endl;
d_rep_set->add( var );
}
diff --git a/src/theory/rewriterules/theory_rewriterules.cpp b/src/theory/rewriterules/theory_rewriterules.cpp index 5ffd4ac4a..f94a373d7 100644 --- a/src/theory/rewriterules/theory_rewriterules.cpp +++ b/src/theory/rewriterules/theory_rewriterules.cpp @@ -434,7 +434,7 @@ Node skolemizeBody( Node f ){ std::vector< Node > vars; std::vector< Node > csts; for( int i=0; i<(int)f[0].getNumChildren(); i++ ){ - csts.push_back( NodeManager::currentNM()->mkSkolem( f[0][i].getType()) ); + csts.push_back( NodeManager::currentNM()->mkSkolem( "skolem_$$", f[0][i].getType(), "is from skolemizing the body of a rewrite rule" ) ); vars.push_back( f[0][i] ); } return f[ 1 ].substitute( vars.begin(), vars.end(), diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index c9fb36830..d69f43908 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -580,12 +580,12 @@ void TheoryEngine::collectModelInfo( theory::TheoryModel* m, bool fullModel ){ } /* get model */ -TheoryModel* TheoryEngine::getModel(){ +TheoryModel* TheoryEngine::getModel() { Debug("model") << "TheoryEngine::getModel()" << std::endl; - if( d_logicInfo.isQuantified() ){ + if( d_logicInfo.isQuantified() ) { Debug("model") << "Get model from quantifiers engine." << std::endl; return d_quantEngine->getModel(); - }else{ + } else { Debug("model") << "Get default model." << std::endl; return d_curr_model; } diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp index de7061022..3f82a6948 100644 --- a/src/theory/uf/theory_uf_strong_solver.cpp +++ b/src/theory/uf/theory_uf_strong_solver.cpp @@ -921,7 +921,7 @@ void StrongSolverTheoryUf::SortRepModel::allocateCardinality( OutputChannel* out //must generate new cardinality lemma term std::stringstream ss; ss << "_c_" << d_aloc_cardinality; - Node var = NodeManager::currentNM()->mkSkolem( ss.str(), d_type ); + Node var = NodeManager::currentNM()->mkSkolem( ss.str(), d_type, "is a cardinality lemma term" ); d_totality_terms[0].push_back( var ); Trace("mkVar") << "allocateCardinality, mkVar : " << var << " : " << d_type << std::endl; //must be distinct from all other cardinality terms diff --git a/src/theory/unconstrained_simplifier.cpp b/src/theory/unconstrained_simplifier.cpp index c23a72c91..636e61a6d 100644 --- a/src/theory/unconstrained_simplifier.cpp +++ b/src/theory/unconstrained_simplifier.cpp @@ -93,8 +93,7 @@ void UnconstrainedSimplifier::visitAll(TNode assertion) Node UnconstrainedSimplifier::newUnconstrainedVar(TypeNode t, TNode var) { - Node n = NodeManager::currentNM()->mkSkolem(t); - Dump.declareVar(n.toExpr(), "a new var introduced because of unconstrained variable " + var.toString()); + Node n = NodeManager::currentNM()->mkSkolem("unconstrained_$$", t, "a new var introduced because of unconstrained variable " + var.toString()); return n; } diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp index bdb3f6cf6..522bcd935 100644 --- a/src/util/datatype.cpp +++ b/src/util/datatype.cpp @@ -414,7 +414,7 @@ void DatatypeConstructor::resolve(ExprManager* em, DatatypeType self, string typeName = (*i).d_name.substr((*i).d_name.find('\0') + 1); (*i).d_name.resize((*i).d_name.find('\0')); if(typeName == "") { - (*i).d_selector = nm->mkSkolem((*i).d_name, nm->mkSelectorType(selfTypeNode, selfTypeNode)).toExpr(); + (*i).d_selector = nm->mkSkolem((*i).d_name, nm->mkSelectorType(selfTypeNode, selfTypeNode), "is a selector").toExpr(); } else { map<string, DatatypeType>::const_iterator j = resolutions.find(typeName); if(j == resolutions.end()) { @@ -424,7 +424,7 @@ void DatatypeConstructor::resolve(ExprManager* em, DatatypeType self, << "of constructor \"" << d_name << "\""; throw DatatypeResolutionException(msg.str()); } else { - (*i).d_selector = nm->mkSkolem((*i).d_name, nm->mkSelectorType(selfTypeNode, TypeNode::fromType((*j).second))).toExpr(); + (*i).d_selector = nm->mkSkolem((*i).d_name, nm->mkSelectorType(selfTypeNode, TypeNode::fromType((*j).second)), "is a selector").toExpr(); } } } else { @@ -437,7 +437,7 @@ void DatatypeConstructor::resolve(ExprManager* em, DatatypeType self, if(!paramTypes.empty() ) { range = doParametricSubstitution( range, paramTypes, paramReplacements ); } - (*i).d_selector = nm->mkSkolem((*i).d_name, nm->mkSelectorType(selfTypeNode, TypeNode::fromType(range))).toExpr(); + (*i).d_selector = nm->mkSkolem((*i).d_name, nm->mkSelectorType(selfTypeNode, TypeNode::fromType(range)), "is a selector").toExpr(); } Node::fromExpr((*i).d_selector).setAttribute(DatatypeIndexAttr(), index++); (*i).d_resolved = true; @@ -450,8 +450,8 @@ void DatatypeConstructor::resolve(ExprManager* em, DatatypeType self, // fails above, we want Constuctor::isResolved() to remain "false". // Further, mkConstructorType() iterates over the selectors, so // should get the results of any resolutions we did above. - d_tester = nm->mkSkolem(getTesterName(), nm->mkTesterType(selfTypeNode)).toExpr(); - d_constructor = nm->mkSkolem(getName(), nm->mkConstructorType(*this, selfTypeNode)).toExpr(); + d_tester = nm->mkSkolem(getTesterName(), nm->mkTesterType(selfTypeNode), "is a tester").toExpr(); + d_constructor = nm->mkSkolem(getName(), nm->mkConstructorType(*this, selfTypeNode), "is a constructor").toExpr(); // associate constructor with all selectors for(iterator i = begin(), i_end = end(); i != i_end; ++i) { (*i).d_constructor = d_constructor; @@ -521,7 +521,7 @@ void DatatypeConstructor::addArg(std::string selectorName, Type selectorType) { // we're using some internals, so we have to set up this library context ExprManagerScope ems(selectorType); - Expr type = NodeManager::currentNM()->mkSkolem(TypeNode::fromType(selectorType)).toExpr(); + Expr type = NodeManager::currentNM()->mkSkolem("unresolved_" + selectorName + "_$$", TypeNode::fromType(selectorType), "is an unresolved selector type placeholder").toExpr(); Debug("datatypes") << type << endl; d_args.push_back(DatatypeConstructorArg(selectorName, type)); } diff --git a/src/util/dump.h b/src/util/dump.h index 382092474..8e81086b2 100644 --- a/src/util/dump.h +++ b/src/util/dump.h @@ -96,17 +96,6 @@ public: void clear() { d_commands.clear(); } const CommandSequence& getCommands() const { return d_commands; } - void declareVar(Expr e, std::string comment) { - if(isOn("declarations")) { - std::stringstream ss; - ss << Expr::setlanguage(Expr::setlanguage::getLanguage(getStream())) << e; - std::string s = ss.str(); - CVC4dumpstream(getStream(), d_commands) - << CommentCommand(s + " is " + comment) - << DeclareFunctionCommand(s, e, e.getType()); - } - } - bool on (const char* tag) { d_tags.insert(std::string(tag)); return true; } bool on (std::string tag) { d_tags.insert(tag); return true; } bool off(const char* tag) { d_tags.erase (std::string(tag)); return false; } diff --git a/src/util/ite_removal.cpp b/src/util/ite_removal.cpp index 50713e2b4..e8a539615 100644 --- a/src/util/ite_removal.cpp +++ b/src/util/ite_removal.cpp @@ -55,9 +55,7 @@ Node RemoveITE::run(TNode node, std::vector<Node>& output, TypeNode nodeType = node.getType(); if(!nodeType.isBoolean()) { // Make the skolem to represent the ITE - Node skolem = nodeManager->mkSkolem(nodeType); - - Dump.declareVar(skolem.toExpr(), "a variable introduced due to term-level ITE removal"); + Node skolem = nodeManager->mkSkolem("termITE_$$", nodeType, "a variable introduced due to term-level ITE removal"); // The new assertion Node newAssertion = diff --git a/src/util/model.cpp b/src/util/model.cpp index 50683fdff..8b0e956cf 100644 --- a/src/util/model.cpp +++ b/src/util/model.cpp @@ -2,14 +2,39 @@ /*! \file model.cpp ** \verbatim ** Original author: ajreynol - ** Major contributors: none + ** Major contributors: mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** 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 implementation of Model class - **/
\ No newline at end of file + **/ + +#include "util/model.h" +#include "expr/command.h" +#include "smt/smt_engine_scope.h" +#include "smt/command_list.h" + +#include <vector> + +using namespace std; + +namespace CVC4 { + +Model::Model() : + d_smt(*smt::currentSmtEngine()) { +} + +size_t Model::getNumCommands() const { + return d_smt.d_modelCommands->size(); +} + +const Command* Model::getCommand(size_t i) const { + return (*d_smt.d_modelCommands)[i]; +} + +}/* CVC4 namespace */ diff --git a/src/util/model.h b/src/util/model.h index 36a5464b4..97010dd45 100644 --- a/src/util/model.h +++ b/src/util/model.h @@ -2,10 +2,10 @@ /*! \file model.h ** \verbatim ** Original author: ajreynol - ** Major contributors: none + ** Major contributors: mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** 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 @@ -27,41 +27,28 @@ namespace CVC4 { -class Command; +class CVC4_PUBLIC Command; +class CVC4_PUBLIC SmtEngine; -class Model -{ -public: - //types of commands that are recorded for get-model - enum { - COMMAND_DECLARE_SORT, //DeclareTypeCommand - COMMAND_DECLARE_FUN, //DeclareFunctionCommand - COMMAND_DECLARE_DATATYPES, //DatatypeDeclarationCommand - }; +class CVC4_PUBLIC Model { private: - //list of commands that the model must report when calling get model - std::vector< Command* > d_commands; - std::vector< int > d_command_types; + /** The SmtEngine we're associated to */ + const SmtEngine& d_smt; public: + /** construct the base class */ + Model(); /** virtual destructor */ - virtual ~Model() {} - /** add command */ - virtual void addCommand( Command* c, int c_type ){ - d_commands.push_back( c ); - d_command_types.push_back( c_type ); - } + virtual ~Model() { } /** get number of commands to report */ - size_t getNumCommands() { return d_commands.size(); } + size_t getNumCommands() const; /** get command */ - Command* getCommand( int i ) { return d_commands[i]; } - /** get type of command */ - int getCommandType( int i ) { return d_command_types[i]; } + const Command* getCommand(size_t i) const; public: /** get value for expression */ - virtual Expr getValue( const Expr& expr ) = 0; + virtual Expr getValue(Expr expr) = 0; /** get cardinality for sort */ - virtual Cardinality getCardinality( const Type& t ) = 0; - /** to stream function */ + virtual Cardinality getCardinality(Type t) = 0; + /** write the model to a stream */ virtual void toStream(std::ostream& out) = 0; };/* class Model */ diff --git a/test/unit/expr/attribute_black.h b/test/unit/expr/attribute_black.h index 93fbe049a..02de21635 100644 --- a/test/unit/expr/attribute_black.h +++ b/test/unit/expr/attribute_black.h @@ -74,7 +74,7 @@ public: void testDeallocation() { TypeNode booleanType = d_nodeManager->booleanType(); - Node* node = new Node(d_nodeManager->mkSkolem(booleanType)); + Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType)); MyData* data; MyData* data1; MyDataAttribute attr; @@ -92,7 +92,7 @@ public: typedef expr::CDAttribute<CDPrimitiveIntAttributeId,uint64_t> CDPrimitiveIntAttribute; void testInts(){ TypeNode booleanType = d_nodeManager->booleanType(); - Node* node = new Node(d_nodeManager->mkSkolem(booleanType)); + Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType)); const uint64_t val = 63489; uint64_t data0 = 0; uint64_t data1 = 0; @@ -120,9 +120,9 @@ public: typedef expr::CDAttribute<CDTNodeAttributeId, TNode> CDTNodeAttribute; void testTNodes(){ TypeNode booleanType = d_nodeManager->booleanType(); - Node* node = new Node(d_nodeManager->mkSkolem(booleanType)); + Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType)); - Node val(d_nodeManager->mkSkolem(booleanType)); + Node val(d_nodeManager->mkSkolem("b", booleanType)); TNode data0; TNode data1; @@ -155,7 +155,7 @@ public: typedef expr::CDAttribute<CDPtrAttributeId, Foo*> CDPtrAttribute; void testPtrs(){ TypeNode booleanType = d_nodeManager->booleanType(); - Node* node = new Node(d_nodeManager->mkSkolem(booleanType)); + Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType)); Foo* val = new Foo(63489); Foo* data0 = NULL; @@ -186,7 +186,7 @@ public: typedef expr::CDAttribute<CDConstPtrAttributeId, const Foo*> CDConstPtrAttribute; void testConstPtrs(){ TypeNode booleanType = d_nodeManager->booleanType(); - Node* node = new Node(d_nodeManager->mkSkolem(booleanType)); + Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType)); const Foo* val = new Foo(63489); const Foo* data0 = NULL; @@ -216,7 +216,7 @@ public: typedef expr::CDAttribute<CDStringAttributeId, std::string> CDStringAttribute; void testStrings(){ TypeNode booleanType = d_nodeManager->booleanType(); - Node* node = new Node(d_nodeManager->mkSkolem(booleanType)); + Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType)); std::string val("63489"); std::string data0; @@ -245,7 +245,7 @@ public: typedef expr::CDAttribute<CDBoolAttributeId, bool> CDBoolAttribute; void testBools(){ TypeNode booleanType = d_nodeManager->booleanType(); - Node* node = new Node(d_nodeManager->mkSkolem(booleanType)); + Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType)); bool val = true; bool data0 = false; diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h index 53af9db53..1518efadf 100644 --- a/test/unit/expr/node_black.h +++ b/test/unit/expr/node_black.h @@ -102,12 +102,12 @@ public: void testOperatorEquals() { Node a, b, c; - b = d_nodeManager->mkSkolem(*d_booleanType); + b = d_nodeManager->mkSkolem("b", *d_booleanType); a = b; c = a; - Node d = d_nodeManager->mkSkolem(*d_booleanType); + Node d = d_nodeManager->mkSkolem("d", *d_booleanType); TS_ASSERT(a==a); TS_ASSERT(a==b); @@ -142,12 +142,12 @@ public: Node a, b, c; - b = d_nodeManager->mkSkolem(*d_booleanType); + b = d_nodeManager->mkSkolem("b", *d_booleanType); a = b; c = a; - Node d = d_nodeManager->mkSkolem(*d_booleanType); + Node d = d_nodeManager->mkSkolem("d", *d_booleanType); /*structed assuming operator == works */ TS_ASSERT(iff(a!=a, !(a==a))); @@ -204,7 +204,7 @@ public: /*tests: Node& operator=(const Node&); */ void testOperatorAssign() { Node a, b; - Node c = d_nodeManager->mkNode(NOT, d_nodeManager->mkSkolem(*d_booleanType)); + Node c = d_nodeManager->mkNode(NOT, d_nodeManager->mkSkolem("c", *d_booleanType)); b = c; TS_ASSERT(b==c); @@ -268,8 +268,8 @@ public: /* Node eqNode(const Node& right) const; */ TypeNode t = d_nodeManager->mkSort(); - Node left = d_nodeManager->mkSkolem(t); - Node right = d_nodeManager->mkSkolem(t); + Node left = d_nodeManager->mkSkolem("left", t); + Node right = d_nodeManager->mkSkolem("right", t); Node eq = left.eqNode(right); TS_ASSERT(EQUAL == eq.getKind()); @@ -326,8 +326,8 @@ public: void testIteNode() { /*Node iteNode(const Node& thenpart, const Node& elsepart) const;*/ - Node a = d_nodeManager->mkSkolem(*d_booleanType); - Node b = d_nodeManager->mkSkolem(*d_booleanType); + Node a = d_nodeManager->mkSkolem("a", *d_booleanType); + Node b = d_nodeManager->mkSkolem("b", *d_booleanType); Node cnd = d_nodeManager->mkNode(OR, a, b); Node thenBranch = d_nodeManager->mkConst(true); @@ -389,8 +389,8 @@ public: void testGetKind() { /*inline Kind getKind() const; */ - Node a = d_nodeManager->mkSkolem(*d_booleanType); - Node b = d_nodeManager->mkSkolem(*d_booleanType); + Node a = d_nodeManager->mkSkolem("a", *d_booleanType); + Node b = d_nodeManager->mkSkolem("b", *d_booleanType); Node n = d_nodeManager->mkNode(NOT, a); TS_ASSERT(NOT == n.getKind()); @@ -398,8 +398,8 @@ public: n = d_nodeManager->mkNode(IFF, a, b); TS_ASSERT(IFF == n.getKind()); - Node x = d_nodeManager->mkSkolem(*d_realType); - Node y = d_nodeManager->mkSkolem(*d_realType); + Node x = d_nodeManager->mkSkolem("x", *d_realType); + Node y = d_nodeManager->mkSkolem("y", *d_realType); n = d_nodeManager->mkNode(PLUS, x, y); TS_ASSERT(PLUS == n.getKind()); @@ -413,8 +413,8 @@ public: TypeNode booleanType = d_nodeManager->booleanType(); TypeNode predType = d_nodeManager->mkFunctionType(sort, booleanType); - Node f = d_nodeManager->mkSkolem(predType); - Node a = d_nodeManager->mkSkolem(sort); + Node f = d_nodeManager->mkSkolem("f", predType); + Node a = d_nodeManager->mkSkolem("a", sort); Node fa = d_nodeManager->mkNode(kind::APPLY_UF, f, a); TS_ASSERT( fa.hasOperator() ); @@ -476,9 +476,9 @@ public: // test iterators void testIterator() { NodeBuilder<> b; - Node x = d_nodeManager->mkSkolem(*d_booleanType); - Node y = d_nodeManager->mkSkolem(*d_booleanType); - Node z = d_nodeManager->mkSkolem(*d_booleanType); + Node x = d_nodeManager->mkSkolem("x", *d_booleanType); + Node y = d_nodeManager->mkSkolem("y", *d_booleanType); + Node z = d_nodeManager->mkSkolem("z", *d_booleanType); Node n = b << x << y << z << kind::AND; { // iterator @@ -525,10 +525,10 @@ public: void testToString() { TypeNode booleanType = d_nodeManager->booleanType(); - Node w = d_nodeManager->mkSkolem("w", booleanType); - Node x = d_nodeManager->mkSkolem("x", booleanType); - Node y = d_nodeManager->mkSkolem("y", booleanType); - Node z = d_nodeManager->mkSkolem("z", booleanType); + Node w = d_nodeManager->mkSkolem("w", booleanType, "", NodeManager::SKOLEM_EXACT_NAME); + Node x = d_nodeManager->mkSkolem("x", booleanType, "", NodeManager::SKOLEM_EXACT_NAME); + Node y = d_nodeManager->mkSkolem("y", booleanType, "", NodeManager::SKOLEM_EXACT_NAME); + Node z = d_nodeManager->mkSkolem("z", booleanType, "", NodeManager::SKOLEM_EXACT_NAME); Node m = NodeBuilder<>() << w << x << kind::OR; Node n = NodeBuilder<>() << m << y << z << kind::AND; @@ -538,10 +538,10 @@ public: void testToStream() { TypeNode booleanType = d_nodeManager->booleanType(); - Node w = d_nodeManager->mkSkolem("w", booleanType); - Node x = d_nodeManager->mkSkolem("x", booleanType); - Node y = d_nodeManager->mkSkolem("y", booleanType); - Node z = d_nodeManager->mkSkolem("z", booleanType); + Node w = d_nodeManager->mkSkolem("w", booleanType, "", NodeManager::SKOLEM_EXACT_NAME); + Node x = d_nodeManager->mkSkolem("x", booleanType, "", NodeManager::SKOLEM_EXACT_NAME); + Node y = d_nodeManager->mkSkolem("y", booleanType, "", NodeManager::SKOLEM_EXACT_NAME); + Node z = d_nodeManager->mkSkolem("z", booleanType, "", NodeManager::SKOLEM_EXACT_NAME); Node m = NodeBuilder<>() << x << y << kind::OR; Node n = NodeBuilder<>() << w << m << z << kind::AND; Node o = NodeBuilder<>() << n << n << kind::XOR; @@ -600,10 +600,10 @@ public: TypeNode intType = d_nodeManager->integerType(); TypeNode fnType = d_nodeManager->mkFunctionType(intType, intType); - Node x = d_nodeManager->mkSkolem("x", intType); - Node y = d_nodeManager->mkSkolem("y", intType); - Node f = d_nodeManager->mkSkolem("f", fnType); - Node g = d_nodeManager->mkSkolem("g", fnType); + Node x = d_nodeManager->mkSkolem("x", intType, "", NodeManager::SKOLEM_EXACT_NAME); + Node y = d_nodeManager->mkSkolem("y", intType, "", NodeManager::SKOLEM_EXACT_NAME); + Node f = d_nodeManager->mkSkolem("f", fnType, "", NodeManager::SKOLEM_EXACT_NAME); + Node g = d_nodeManager->mkSkolem("g", fnType, "", NodeManager::SKOLEM_EXACT_NAME); Node fx = d_nodeManager->mkNode(APPLY_UF, f, x); Node fy = d_nodeManager->mkNode(APPLY_UF, f, y); Node gx = d_nodeManager->mkNode(APPLY_UF, g, x); @@ -644,7 +644,7 @@ public: // This is for demonstrating what a certain type of user error looks like. // Node level0(){ // NodeBuilder<> nb(kind::AND); -// Node x = d_nodeManager->mkSkolem(*d_booleanType); +// Node x = d_nodeManager->mkSkolem("x", *d_booleanType); // nb << x; // nb << x; // return Node(nb.constructNode()); diff --git a/test/unit/expr/node_builder_black.h b/test/unit/expr/node_builder_black.h index fc9fdd2a6..97abddc00 100644 --- a/test/unit/expr/node_builder_black.h +++ b/test/unit/expr/node_builder_black.h @@ -246,9 +246,9 @@ public: void testIterator() { NodeBuilder<> b; - Node x = d_nm->mkSkolem(*d_booleanType); - Node y = d_nm->mkSkolem(*d_booleanType); - Node z = d_nm->mkSkolem(*d_booleanType); + Node x = d_nm->mkSkolem("x", *d_booleanType); + Node y = d_nm->mkSkolem("z", *d_booleanType); + Node z = d_nm->mkSkolem("y", *d_booleanType); b << x << y << z << AND; { @@ -274,7 +274,7 @@ public: NodeBuilder<> noKind; TS_ASSERT_EQUALS(noKind.getKind(), UNDEFINED_KIND); - Node x( d_nm->mkSkolem( *d_integerType ) ); + Node x( d_nm->mkSkolem( "x", *d_integerType ) ); noKind << x << x; // push_back(noKind, K); TS_ASSERT_EQUALS(noKind.getKind(), UNDEFINED_KIND); @@ -297,7 +297,7 @@ public: void testGetNumChildren() { /* unsigned getNumChildren() const; */ - Node x( d_nm->mkSkolem( *d_integerType ) ); + Node x( d_nm->mkSkolem( "x", *d_integerType ) ); NodeBuilder<> nb; #ifdef CVC4_ASSERTIONS @@ -515,16 +515,16 @@ public: } void testAppend() { - Node x = d_nm->mkSkolem(*d_booleanType); - Node y = d_nm->mkSkolem(*d_booleanType); - Node z = d_nm->mkSkolem(*d_booleanType); + Node x = d_nm->mkSkolem("x", *d_booleanType); + Node y = d_nm->mkSkolem("y", *d_booleanType); + Node z = d_nm->mkSkolem("z", *d_booleanType); Node m = d_nm->mkNode(AND, y, z, x); Node n = d_nm->mkNode(OR, d_nm->mkNode(NOT, x), y, z); Node o = d_nm->mkNode(XOR, y, x); - Node r = d_nm->mkSkolem(*d_realType); - Node s = d_nm->mkSkolem(*d_realType); - Node t = d_nm->mkSkolem(*d_realType); + Node r = d_nm->mkSkolem("r", *d_realType); + Node s = d_nm->mkSkolem("s", *d_realType); + Node t = d_nm->mkSkolem("t", *d_realType); Node p = d_nm->mkNode(EQUAL, d_nm->mkConst<Rational>(0), d_nm->mkNode(PLUS, r, d_nm->mkNode(UMINUS, s), t)); @@ -599,13 +599,13 @@ public: void testLeftistBuilding() { NodeBuilder<> nb; - Node a = d_nm->mkSkolem(*d_booleanType); + Node a = d_nm->mkSkolem("a", *d_booleanType); - Node b = d_nm->mkSkolem(*d_booleanType); - Node c = d_nm->mkSkolem(*d_booleanType); + Node b = d_nm->mkSkolem("b", *d_booleanType); + Node c = d_nm->mkSkolem("c", *d_booleanType); - Node d = d_nm->mkSkolem(*d_realType); - Node e = d_nm->mkSkolem(*d_realType); + Node d = d_nm->mkSkolem("d", *d_realType); + Node e = d_nm->mkSkolem("e", *d_realType); nb << a << NOT << b << c << OR @@ -628,14 +628,14 @@ public: } void testConvenienceBuilders() { - Node a = d_nm->mkSkolem(*d_booleanType); + Node a = d_nm->mkSkolem("a", *d_booleanType); - Node b = d_nm->mkSkolem(*d_booleanType); - Node c = d_nm->mkSkolem(*d_booleanType); + Node b = d_nm->mkSkolem("b", *d_booleanType); + Node c = d_nm->mkSkolem("c", *d_booleanType); - Node d = d_nm->mkSkolem(*d_realType); - Node e = d_nm->mkSkolem(*d_realType); - Node f = d_nm->mkSkolem(*d_realType); + Node d = d_nm->mkSkolem("d", *d_realType); + Node e = d_nm->mkSkolem("e", *d_realType); + Node f = d_nm->mkSkolem("f", *d_realType); Node m = a && b; TS_ASSERT_EQUALS(m, d_nm->mkNode(AND, a, b)); diff --git a/test/unit/expr/node_manager_black.h b/test/unit/expr/node_manager_black.h index d392050f8..75c3618ff 100644 --- a/test/unit/expr/node_manager_black.h +++ b/test/unit/expr/node_manager_black.h @@ -144,17 +144,9 @@ public: } } - void testMkVarWithNoName() { - TypeNode booleanType = d_nodeManager->booleanType(); - Node x = d_nodeManager->mkSkolem(booleanType); - TS_ASSERT_EQUALS(x.getKind(),SKOLEM); - TS_ASSERT_EQUALS(x.getNumChildren(),0u); - TS_ASSERT_EQUALS(x.getType(),booleanType); - } - void testMkVarWithName() { TypeNode booleanType = d_nodeManager->booleanType(); - Node x = d_nodeManager->mkSkolem("x", booleanType); + Node x = d_nodeManager->mkSkolem("x", booleanType, "", NodeManager::SKOLEM_EXACT_NAME); TS_ASSERT_EQUALS(x.getKind(),SKOLEM); TS_ASSERT_EQUALS(x.getNumChildren(),0u); TS_ASSERT_EQUALS(x.getAttribute(VarNameAttr()),"x"); @@ -337,7 +329,7 @@ public: /* This test is only valid if assertions are enabled. */ void testMkNodeTooFew() { #ifdef CVC4_ASSERTIONS - Node x = d_nodeManager->mkSkolem( d_nodeManager->booleanType() ); + Node x = d_nodeManager->mkSkolem( "x", d_nodeManager->booleanType() ); TS_ASSERT_THROWS( d_nodeManager->mkNode(AND, x), AssertionException ); #endif } @@ -349,7 +341,7 @@ public: const unsigned int max = metakind::getUpperBoundForKind(AND); TypeNode boolType = d_nodeManager->booleanType(); for( unsigned int i = 0; i <= max; ++i ) { - vars.push_back( d_nodeManager->mkSkolem(boolType) ); + vars.push_back( d_nodeManager->mkSkolem("i", boolType) ); } TS_ASSERT_THROWS( d_nodeManager->mkNode(AND, vars), AssertionException ); #endif |