summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/context/cdlist.h6
-rw-r--r--src/expr/command.cpp8
-rw-r--r--src/expr/expr_manager_template.cpp4
-rw-r--r--src/expr/expr_template.cpp2
-rw-r--r--src/expr/node_manager.cpp63
-rw-r--r--src/expr/node_manager.h133
-rw-r--r--src/expr/symbol_table.cpp20
-rw-r--r--src/parser/smt2/smt2.cpp3
-rw-r--r--src/printer/ast/ast_printer.cpp2
-rw-r--r--src/printer/ast/ast_printer.h2
-rw-r--r--src/printer/cvc/cvc_printer.cpp41
-rw-r--r--src/printer/cvc/cvc_printer.h2
-rw-r--r--src/printer/dagification_visitor.cpp2
-rw-r--r--src/printer/printer.cpp4
-rw-r--r--src/printer/printer.h2
-rw-r--r--src/printer/smt/smt_printer.cpp4
-rw-r--r--src/printer/smt/smt_printer.h2
-rw-r--r--src/printer/smt2/smt2_printer.cpp14
-rw-r--r--src/printer/smt2/smt2_printer.h2
-rw-r--r--src/smt/Makefile.am2
-rw-r--r--src/smt/command_list.cpp33
-rw-r--r--src/smt/command_list.h41
-rw-r--r--src/smt/options_handlers.h11
-rw-r--r--src/smt/smt_engine.cpp103
-rw-r--r--src/smt/smt_engine.h27
-rw-r--r--src/theory/arith/dio_solver.cpp2
-rw-r--r--src/theory/arrays/theory_arrays.cpp4
-rw-r--r--src/theory/builtin/theory_builtin_type_rules.h2
-rw-r--r--src/theory/bv/theory_bv_utils.h2
-rw-r--r--src/theory/ite_simplifier.cpp2
-rw-r--r--src/theory/model.cpp6
-rw-r--r--src/theory/model.h4
-rw-r--r--src/theory/quantifiers/quantifiers_rewriter.cpp4
-rw-r--r--src/theory/quantifiers/term_database.cpp6
-rw-r--r--src/theory/rep_set.cpp2
-rw-r--r--src/theory/rewriterules/theory_rewriterules.cpp2
-rw-r--r--src/theory/theory_engine.cpp6
-rw-r--r--src/theory/uf/theory_uf_strong_solver.cpp2
-rw-r--r--src/theory/unconstrained_simplifier.cpp3
-rw-r--r--src/util/datatype.cpp12
-rw-r--r--src/util/dump.h11
-rw-r--r--src/util/ite_removal.cpp4
-rw-r--r--src/util/model.cpp31
-rw-r--r--src/util/model.h43
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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback