diff options
Diffstat (limited to 'src')
44 files changed, 485 insertions, 196 deletions
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 */ |