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
* 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),
}
void DeclareFunctionCommand::invoke(SmtEngine* smtEngine) throw() {
- Dump("declarations") << *this;
- smtEngine->addToModelCommand( clone(), Model::COMMAND_DECLARE_FUN );
d_commandStatus = CommandSuccess::instance();
}
}
void DeclareTypeCommand::invoke(SmtEngine* smtEngine) throw() {
- Dump("declarations") << *this;
- smtEngine->addToModelCommand( clone(), Model::COMMAND_DECLARE_SORT );
d_commandStatus = CommandSuccess::instance();
}
}
void DefineTypeCommand::invoke(SmtEngine* smtEngine) throw() {
- Dump("declarations") << *this;
d_commandStatus = CommandSuccess::instance();
}
}
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);
}
void DatatypeDeclarationCommand::invoke(SmtEngine* smtEngine) throw() {
- Dump("declarations") << *this;
- smtEngine->addToModelCommand( clone(), Model::COMMAND_DECLARE_DATATYPES );
d_commandStatus = CommandSuccess::instance();
}
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;
}
// 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();
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;
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;
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();
Debug("gc") << "deleting node value " << nv
<< " [" << nv->d_id << "]: ";
nv->printAst(Debug("gc"));
- Debug("gc") << std::endl;
+ Debug("gc") << endl;
}
// remove from the pool
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
/* 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);
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());
}
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());
}
}/* 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;
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 {
*/
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"
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. */
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);
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,
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;
}
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;
}
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;
}
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;
}
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;
}
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);
}
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);
}
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){
}
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) {
}
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));
}
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: "
break;
case THEORY_ARRAYS:
- // FIXME: should define a paramterized type 'Array' with 2 arguments
- mkSort("Array");
-
addOperator(kind::SELECT);
addOperator(kind::STORE);
break;
}/* 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()";
}
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 */
}/* 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() ){
}
}
}
- }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() ){
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() {
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 */
// 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);
}/* 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) */
//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 */
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 */
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 */
// 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 {
}/* 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() ){
}
}
}
- }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]
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 */
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 \
--- /dev/null
+/********************* */
+/*! \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 */
--- /dev/null
+/********************* */
+/*! \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 */
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\
(--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\
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") ||
Dump.on("benchmark");
if(strcmp(optargPtr, "benchmark")) {
Dump.on("declarations");
+ if(strcmp(optargPtr, "declarations") && strcmp(optargPtr, "assertions")) {
+ Dump.on("skolems");
+ }
}
}
free(optargPtr);
#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"
* 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 */
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 {
d_definedFunctions(NULL),
d_assertionList(NULL),
d_assignments(NULL),
+ d_modelCommands(NULL),
d_logic(),
d_pendingPops(0),
d_fullyInited(false),
d_context->push();
d_definedFunctions = new(true) DefinedFunctionMap(d_userContext);
+ d_modelCommands = new(true) smt::CommandList(d_userContext);
}
void SmtEngine::finishInit() {
}
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
d_assertionList->deleteSelf();
}
+ if(d_modelCommands != NULL) {
+ d_modelCommands->deleteSelf();
+ }
+
d_definedFunctions->deleteSelf();
StatisticsRegistry::unregisterStat(&d_definitionExpansionTime);
}
-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);
}
}
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, ...
// [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;
namespace CVC4 {
-
template <bool ref_count> class NodeTemplate;
typedef NodeTemplate<true> Node;
typedef NodeTemplate<false> TNode;
class NodeHashFunction;
+class Command;
+
class DecisionEngine;
class TheoryEngine;
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
*/
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.
*/
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;
/** 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:
/**
*/
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
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) :
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;
}
}
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 */
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) {
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;
}
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() ){
}
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();
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:
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() );
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() );
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 ];
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] );
}
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 ];
TypeNode tn = d_types[i];\r
if( tn.isSort() ){\r
if( !d_rep_set->hasType( tn ) ){\r
- Node var = NodeManager::currentNM()->mkSkolem( tn );\r
+ Node var = NodeManager::currentNM()->mkSkolem( "repSet_$$", tn, "is a variable created by the RepSetIterator" );\r
Trace("mkVar") << "RepSetIterator:: Make variable " << var << " : " << tn << std::endl;\r
d_rep_set->add( var );\r
}\r
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(),
}
/* 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;
}
//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
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;
}
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()) {
<< "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 {
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;
// 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;
// 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));
}
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; }
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 =
/*! \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 */
/*! \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
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 */
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;
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;
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;
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;
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;
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;
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;
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);
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)));
/*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);
/* 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());
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);
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());
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());
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() );
// 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
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;
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;
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);
// 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());
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;
{
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);
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
}
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));
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
}
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));
}
}
- 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");
/* 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
}
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
projects / cvc5.git / commitdiff