diff options
Diffstat (limited to 'src/smt/listeners.cpp')
| -rw-r--r-- | src/smt/listeners.cpp | 19 |
1 files changed, 9 insertions, 10 deletions
diff --git a/src/smt/listeners.cpp b/src/smt/listeners.cpp index 539d6ba2f..52ddcf156 100644 --- a/src/smt/listeners.cpp +++ b/src/smt/listeners.cpp @@ -18,7 +18,7 @@ #include "expr/expr.h" #include "expr/node_manager_attributes.h" #include "options/smt_options.h" -#include "smt/command.h" +#include "smt/node_command.h" #include "smt/dump.h" #include "smt/dump_manager.h" #include "smt/smt_engine.h" @@ -40,7 +40,7 @@ SmtNodeManagerListener::SmtNodeManagerListener(DumpManager& dm) : d_dm(dm) {} void SmtNodeManagerListener::nmNotifyNewSort(TypeNode tn, uint32_t flags) { - DeclareTypeCommand c(tn.getAttribute(expr::VarNameAttr()), 0, tn.toType()); + DeclareTypeNodeCommand c(tn.getAttribute(expr::VarNameAttr()), 0, tn); if ((flags & ExprManager::SORT_FLAG_PLACEHOLDER) == 0) { d_dm.addToModelCommandAndDump(c, flags); @@ -50,9 +50,9 @@ void SmtNodeManagerListener::nmNotifyNewSort(TypeNode tn, uint32_t flags) void SmtNodeManagerListener::nmNotifyNewSortConstructor(TypeNode tn, uint32_t flags) { - DeclareTypeCommand c(tn.getAttribute(expr::VarNameAttr()), - tn.getAttribute(expr::SortArityAttr()), - tn.toType()); + DeclareTypeNodeCommand c(tn.getAttribute(expr::VarNameAttr()), + tn.getAttribute(expr::SortArityAttr()), + tn); if ((flags & ExprManager::SORT_FLAG_PLACEHOLDER) == 0) { d_dm.addToModelCommandAndDump(c); @@ -68,17 +68,16 @@ void SmtNodeManagerListener::nmNotifyNewDatatypes( for (const TypeNode& dt : dtts) { Assert(dt.isDatatype()); - types.push_back(dt.toType()); } - DatatypeDeclarationCommand c(types); + DeclareDatatypeNodeCommand c(dtts); d_dm.addToModelCommandAndDump(c); } } void SmtNodeManagerListener::nmNotifyNewVar(TNode n, uint32_t flags) { - DeclareFunctionCommand c( - n.getAttribute(expr::VarNameAttr()), n.toExpr(), n.getType().toType()); + DeclareFunctionNodeCommand c( + n.getAttribute(expr::VarNameAttr()), n, n.getType()); if ((flags & ExprManager::VAR_FLAG_DEFINED) == 0) { d_dm.addToModelCommandAndDump(c, flags); @@ -90,7 +89,7 @@ void SmtNodeManagerListener::nmNotifyNewSkolem(TNode n, uint32_t flags) { std::string id = n.getAttribute(expr::VarNameAttr()); - DeclareFunctionCommand c(id, n.toExpr(), n.getType().toType()); + DeclareFunctionNodeCommand c(id, n, n.getType()); if (Dump.isOn("skolems") && comment != "") { Dump("skolems") << CommentCommand(id + " is " + comment); |