This PR is a step towards the migration of Commands to the public API. Node versions of some Commands are introduced for internal use (as necessary). The DumpManager is refactored to make use of those commands.
smt/model_core_builder.h
smt/model_blocker.cpp
smt/model_blocker.h
+ smt/node_command.cpp
+ smt/node_command.h
smt/options_manager.cpp
smt/options_manager.h
smt/quant_elim_solver.cpp
#include "options/language.h" // for LANG_AST
#include "printer/dagification_visitor.h"
#include "smt/command.h"
+#include "smt/node_command.h"
#include "theory/substitutions.h"
using namespace std;
void AstPrinter::toStream(std::ostream& out,
const Model& m,
- const Command* c) const
+ const NodeCommand* c) const
{
// shouldn't be called; only the non-Command* version above should be
Unreachable();
void toStream(std::ostream& out, TNode n, int toDepth, bool types) const;
void toStream(std::ostream& out,
const Model& m,
- const Command* c) const override;
+ const NodeCommand* c) const override;
}; /* class AstPrinter */
} // namespace ast
#include "options/smt_options.h"
#include "printer/dagification_visitor.h"
#include "smt/command.h"
+#include "smt/node_command.h"
#include "smt/smt_engine.h"
#include "theory/arrays/theory_arrays_rewriter.h"
#include "theory/substitutions.h"
namespace {
-void DeclareTypeCommandToStream(std::ostream& out,
- const theory::TheoryModel& model,
- const DeclareTypeCommand& command)
+void DeclareTypeNodeCommandToStream(std::ostream& out,
+ const theory::TheoryModel& model,
+ const DeclareTypeNodeCommand& command)
{
- TypeNode type_node = TypeNode::fromType(command.getType());
+ TypeNode type_node = command.getType();
const std::vector<Node>* type_reps =
model.getRepSet()->getTypeRepsOrNull(type_node);
if (options::modelUninterpDtEnum() && type_node.isSort()
}
}
-void DeclareFunctionCommandToStream(std::ostream& out,
- const theory::TheoryModel& model,
- const DeclareFunctionCommand& command)
+void DeclareFunctionNodeCommandToStream(
+ std::ostream& out,
+ const theory::TheoryModel& model,
+ const DeclareFunctionNodeCommand& command)
{
- Node n = Node::fromExpr(command.getFunction());
+ Node n = command.getFunction();
if (n.getKind() == kind::SKOLEM)
{
// don't print out internal stuff
void CvcPrinter::toStream(std::ostream& out,
const Model& model,
- const Command* command) const
+ const NodeCommand* command) const
{
const auto* theory_model = dynamic_cast<const theory::TheoryModel*>(&model);
AlwaysAssert(theory_model != nullptr);
if (const auto* declare_type_command =
- dynamic_cast<const DeclareTypeCommand*>(command))
+ dynamic_cast<const DeclareTypeNodeCommand*>(command))
{
- DeclareTypeCommandToStream(out, *theory_model, *declare_type_command);
+ DeclareTypeNodeCommandToStream(out, *theory_model, *declare_type_command);
}
else if (const auto* dfc =
- dynamic_cast<const DeclareFunctionCommand*>(command))
+ dynamic_cast<const DeclareFunctionNodeCommand*>(command))
{
- DeclareFunctionCommandToStream(out, *theory_model, *dfc);
+ DeclareFunctionNodeCommandToStream(out, *theory_model, *dfc);
}
else
{
- out << command << std::endl;
+ out << *command << std::endl;
}
}
std::ostream& out, TNode n, int toDepth, bool types, bool bracket) const;
void toStream(std::ostream& out,
const Model& m,
- const Command* c) const override;
+ const NodeCommand* c) const override;
bool d_cvc3Mode;
}; /* class CvcPrinter */
#include "printer/cvc/cvc_printer.h"
#include "printer/smt2/smt2_printer.h"
#include "printer/tptp/tptp_printer.h"
+#include "smt/node_command.h"
using namespace std;
void Printer::toStream(std::ostream& out, const Model& m) const
{
for(size_t i = 0; i < m.getNumCommands(); ++i) {
- const Command* cmd = m.getCommand(i);
- const DeclareFunctionCommand* dfc = dynamic_cast<const DeclareFunctionCommand*>(cmd);
- if (dfc != NULL && !m.isModelCoreSymbol(dfc->getFunction()))
+ const NodeCommand* cmd = m.getCommand(i);
+ const DeclareFunctionNodeCommand* dfc =
+ dynamic_cast<const DeclareFunctionNodeCommand*>(cmd);
+ if (dfc != NULL && !m.isModelCoreSymbol(dfc->getFunction().toExpr()))
{
continue;
}
namespace CVC4 {
+class NodeCommand;
+
class Printer
{
public:
/** write model response to command */
virtual void toStream(std::ostream& out,
const Model& m,
- const Command* c) const = 0;
+ const NodeCommand* c) const = 0;
/** write model response to command using another language printer */
void toStreamUsing(OutputLanguage lang,
std::ostream& out,
const Model& m,
- const Command* c) const
+ const NodeCommand* c) const
{
getPrinter(lang)->toStream(out, m, c);
}
#include "options/printer_options.h"
#include "options/smt_options.h"
#include "printer/dagification_visitor.h"
+#include "smt/node_command.h"
#include "smt/smt_engine.h"
#include "smt_util/boolean_simplification.h"
#include "theory/arrays/theory_arrays_rewriter.h"
-#include "theory/quantifiers/quantifiers_attributes.h"
#include "theory/datatypes/sygus_datatype_utils.h"
+#include "theory/quantifiers/quantifiers_attributes.h"
#include "theory/substitutions.h"
#include "theory/theory_model.h"
#include "util/smt2_quote_string.h"
void Smt2Printer::toStream(std::ostream& out,
const Model& model,
- const Command* command) const
+ const NodeCommand* command) const
{
const theory::TheoryModel* theory_model =
dynamic_cast<const theory::TheoryModel*>(&model);
AlwaysAssert(theory_model != nullptr);
- if (const DeclareTypeCommand* dtc =
- dynamic_cast<const DeclareTypeCommand*>(command))
+ if (const DeclareTypeNodeCommand* dtc =
+ dynamic_cast<const DeclareTypeNodeCommand*>(command))
{
// print out the DeclareTypeCommand
- Type t = (*dtc).getType();
- if (!t.isSort())
+ TypeNode tn = dtc->getType();
+ if (!tn.isSort())
{
out << (*dtc) << endl;
}
else
{
- std::vector<Expr> elements = theory_model->getDomainElements(t);
+ std::vector<Expr> elements = theory_model->getDomainElements(tn.toType());
if (options::modelUninterpDtEnum())
{
if (isVariant_2_6(d_variant))
else
{
// print the cardinality
- out << "; cardinality of " << t << " is " << elements.size() << endl;
+ out << "; cardinality of " << tn << " is " << elements.size() << endl;
out << (*dtc) << endl;
// print the representatives
for (const Expr& type_ref : elements)
Node trn = Node::fromExpr(type_ref);
if (trn.isVar())
{
- out << "(declare-fun " << quoteSymbol(trn) << " () " << t << ")"
+ out << "(declare-fun " << quoteSymbol(trn) << " () " << tn << ")"
<< endl;
}
else
}
}
}
- else if (const DeclareFunctionCommand* dfc =
- dynamic_cast<const DeclareFunctionCommand*>(command))
+ else if (const DeclareFunctionNodeCommand* dfc =
+ dynamic_cast<const DeclareFunctionNodeCommand*>(command))
{
// print out the DeclareFunctionCommand
- Node n = Node::fromExpr((*dfc).getFunction());
+ Node n = dfc->getFunction();
if ((*dfc).getPrintInModelSetByUser())
{
if (!(*dfc).getPrintInModel())
out << ")" << endl;
}
}
- else if (const DatatypeDeclarationCommand* datatype_declaration_command =
- dynamic_cast<const DatatypeDeclarationCommand*>(command))
+ else if (const DeclareDatatypeNodeCommand* declare_datatype_command =
+ dynamic_cast<const DeclareDatatypeNodeCommand*>(command))
{
- out << datatype_declaration_command;
+ out << *declare_datatype_command;
}
else
{
#ifndef CVC4__PRINTER__SMT2_PRINTER_H
#define CVC4__PRINTER__SMT2_PRINTER_H
-#include <iostream>
-
#include "printer/printer.h"
namespace CVC4 {
std::ostream& out, TNode n, int toDepth, bool types, TypeNode nt) const;
void toStream(std::ostream& out,
const Model& m,
- const Command* c) const override;
+ const NodeCommand* c) const override;
void toStream(std::ostream& out, const SExpr& sexpr) const;
void toStream(std::ostream& out, const DType& dt) const;
#include <typeinfo>
#include <vector>
-#include "expr/expr.h" // for ExprSetDepth etc..
-#include "expr/node_manager.h" // for VarNameAttr
-#include "options/language.h" // for LANG_AST
-#include "options/smt_options.h" // for unsat cores
-#include "smt/smt_engine.h"
+#include "expr/expr.h" // for ExprSetDepth etc..
+#include "expr/node_manager.h" // for VarNameAttr
+#include "options/language.h" // for LANG_AST
+#include "options/smt_options.h" // for unsat cores
#include "smt/command.h"
+#include "smt/node_command.h"
+#include "smt/smt_engine.h"
using namespace std;
void TptpPrinter::toStream(std::ostream& out,
const Model& m,
- const Command* c) const
+ const NodeCommand* c) const
{
// shouldn't be called; only the non-Command* version above should be
Unreachable();
private:
void toStream(std::ostream& out,
const Model& m,
- const Command* c) const override;
+ const NodeCommand* c) const override;
}; /* class TptpPrinter */
#include "base/output.h"
#include "smt/command.h"
+#include "smt/node_command.h"
namespace CVC4 {
return *this;
}
+ /** A convenience function for dumping internal commands.
+ *
+ * Since Commands are now part of the public API, internal code should use
+ * NodeCommands and this function (instead of the one above) to dump them.
+ */
+ CVC4dumpstream& operator<<(const NodeCommand& nc)
+ {
+ if (d_os != nullptr)
+ {
+ (*d_os) << nc << std::endl;
+ }
+ return *this;
+ }
+
private:
std::ostream* d_os;
}; /* class CVC4dumpstream */
CVC4dumpstream() {}
CVC4dumpstream(std::ostream& os) {}
CVC4dumpstream& operator<<(const Command& c) { return *this; }
+ CVC4dumpstream& operator<<(const NodeCommand& nc) { return *this; }
}; /* class CVC4dumpstream */
#endif /* CVC4_DUMPING && !CVC4_MUZZLE */
void DumpManager::resetAssertions() { d_modelGlobalCommands.clear(); }
-void DumpManager::addToModelCommandAndDump(const Command& c,
+void DumpManager::addToModelCommandAndDump(const NodeCommand& c,
uint32_t flags,
bool userVisible,
const char* dumpTag)
{
if (flags & ExprManager::VAR_FLAG_GLOBAL)
{
- d_modelGlobalCommands.push_back(std::unique_ptr<Command>(c.clone()));
+ d_modelGlobalCommands.push_back(std::unique_ptr<NodeCommand>(c.clone()));
}
else
{
- Command* cc = c.clone();
+ NodeCommand* cc = c.clone();
d_modelCommands.push_back(cc);
// also remember for memory management purposes
- d_modelCommandsAlloc.push_back(std::unique_ptr<Command>(cc));
+ d_modelCommandsAlloc.push_back(std::unique_ptr<NodeCommand>(cc));
}
}
if (Dump.isOn(dumpTag))
}
else
{
- d_dumpCommands.push_back(std::unique_ptr<Command>(c.clone()));
+ d_dumpCommands.push_back(std::unique_ptr<NodeCommand>(c.clone()));
}
}
}
void DumpManager::setPrintFuncInModel(Node f, bool p)
{
Trace("setp-model") << "Set printInModel " << f << " to " << p << std::endl;
- for (std::unique_ptr<Command>& c : d_modelGlobalCommands)
+ for (std::unique_ptr<NodeCommand>& c : d_modelGlobalCommands)
{
DeclareFunctionCommand* dfc =
dynamic_cast<DeclareFunctionCommand*>(c.get());
}
}
}
- for (Command* c : d_modelCommands)
+ for (NodeCommand* c : d_modelCommands)
{
DeclareFunctionCommand* dfc = dynamic_cast<DeclareFunctionCommand*>(c);
if (dfc != NULL)
return d_modelCommands.size() + d_modelGlobalCommands.size();
}
-const Command* DumpManager::getModelCommand(size_t i) const
+const NodeCommand* DumpManager::getModelCommand(size_t i) const
{
Assert(i < getNumModelCommands());
// index the global commands first, then the locals
#include "context/cdlist.h"
#include "expr/node.h"
-#include "smt/command.h"
+#include "smt/node_command.h"
namespace CVC4 {
namespace smt {
*/
class DumpManager
{
- typedef context::CDList<Command*> CommandList;
+ typedef context::CDList<NodeCommand*> CommandList;
public:
DumpManager(context::UserContext* u);
* Add to Model command. This is used for recording a command
* that should be reported during a get-model call.
*/
- void addToModelCommandAndDump(const Command& c,
+ void addToModelCommandAndDump(const NodeCommand& c,
uint32_t flags = 0,
bool userVisible = true,
const char* dumpTag = "declarations");
/** get number of commands to report in a model */
size_t getNumModelCommands() const;
/** get model command at index i */
- const Command* getModelCommand(size_t i) const;
+ const NodeCommand* getModelCommand(size_t i) const;
private:
/** Fully inited */
* regardless of push/pop). Only maintained if produce-models option
* is on.
*/
- std::vector<std::unique_ptr<Command>> d_modelGlobalCommands;
+ std::vector<std::unique_ptr<NodeCommand>> d_modelGlobalCommands;
/**
* A list of commands that should be in the Model locally (i.e.,
* A list of model commands allocated to d_modelCommands at any time. This
* is maintained for memory management purposes.
*/
- std::vector<std::unique_ptr<Command>> d_modelCommandsAlloc;
+ std::vector<std::unique_ptr<NodeCommand>> d_modelCommandsAlloc;
/**
* A vector of declaration commands waiting to be dumped out.
* This ensures the declarations come after the set-logic and
* any necessary set-option commands are dumped.
*/
- std::vector<std::unique_ptr<Command>> d_dumpCommands;
+ std::vector<std::unique_ptr<NodeCommand>> d_dumpCommands;
};
} // namespace smt
#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"
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);
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);
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);
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);
#include "expr/expr_iomanip.h"
#include "options/base_options.h"
#include "printer/printer.h"
-#include "smt/command.h"
#include "smt/dump_manager.h"
+#include "smt/node_command.h"
#include "smt/smt_engine.h"
#include "smt/smt_engine_scope.h"
return d_smt.getDumpManager()->getNumModelCommands();
}
-const Command* Model::getCommand(size_t i) const
+const NodeCommand* Model::getCommand(size_t i) const
{
return d_smt.getDumpManager()->getModelCommand(i);
}
namespace CVC4 {
-class Command;
+class NodeCommand;
class SmtEngine;
class Model;
/** get number of commands to report */
size_t getNumCommands() const;
/** get command */
- const Command* getCommand(size_t i) const;
+ const NodeCommand* getCommand(size_t i) const;
/** get the smt engine that this model is hooked up to */
SmtEngine* getSmtEngine() { return &d_smt; }
/** get the smt engine (as a pointer-to-const) that this model is hooked up to */
--- /dev/null
+/********************* */
+/*! \file node_command.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Abdalrhman Mohamed
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of NodeCommand functions.
+ **
+ ** Implementation of NodeCommand functions.
+ **/
+
+#include "smt/node_command.h"
+
+#include "printer/printer.h"
+
+namespace CVC4 {
+
+/* -------------------------------------------------------------------------- */
+/* class NodeCommand */
+/* -------------------------------------------------------------------------- */
+
+NodeCommand::~NodeCommand() {}
+
+std::string NodeCommand::toString() const
+{
+ std::stringstream ss;
+ toStream(ss);
+ return ss.str();
+}
+
+std::ostream& operator<<(std::ostream& out, const NodeCommand& nc)
+{
+ nc.toStream(out,
+ Node::setdepth::getDepth(out),
+ Node::printtypes::getPrintTypes(out),
+ Node::dag::getDag(out),
+ Node::setlanguage::getLanguage(out));
+ return out;
+}
+
+/* -------------------------------------------------------------------------- */
+/* class DeclareFunctionNodeCommand */
+/* -------------------------------------------------------------------------- */
+
+DeclareFunctionNodeCommand::DeclareFunctionNodeCommand(const std::string& id,
+ Node expr,
+ TypeNode type)
+ : d_id(id),
+ d_fun(expr),
+ d_type(type),
+ d_printInModel(true),
+ d_printInModelSetByUser(false)
+{
+}
+
+void DeclareFunctionNodeCommand::toStream(std::ostream& out,
+ int toDepth,
+ bool types,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdDeclareFunction(out, d_id, d_type);
+}
+
+NodeCommand* DeclareFunctionNodeCommand::clone() const
+{
+ return new DeclareFunctionNodeCommand(d_id, d_fun, d_type);
+}
+
+const Node& DeclareFunctionNodeCommand::getFunction() const { return d_fun; }
+
+bool DeclareFunctionNodeCommand::getPrintInModel() const
+{
+ return d_printInModel;
+}
+
+bool DeclareFunctionNodeCommand::getPrintInModelSetByUser() const
+{
+ return d_printInModelSetByUser;
+}
+
+void DeclareFunctionNodeCommand::setPrintInModel(bool p)
+{
+ d_printInModel = p;
+ d_printInModelSetByUser = true;
+}
+
+/* -------------------------------------------------------------------------- */
+/* class DeclareTypeNodeCommand */
+/* -------------------------------------------------------------------------- */
+
+DeclareTypeNodeCommand::DeclareTypeNodeCommand(const std::string& id,
+ size_t arity,
+ TypeNode type)
+ : d_id(id), d_arity(arity), d_type(type)
+{
+}
+
+void DeclareTypeNodeCommand::toStream(std::ostream& out,
+ int toDepth,
+ bool types,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdDeclareType(
+ out, d_id, d_arity, d_type);
+}
+
+NodeCommand* DeclareTypeNodeCommand::clone() const
+{
+ return new DeclareTypeNodeCommand(d_id, d_arity, d_type);
+}
+
+const std::string DeclareTypeNodeCommand::getSymbol() const { return d_id; }
+
+const TypeNode& DeclareTypeNodeCommand::getType() const { return d_type; }
+
+/* -------------------------------------------------------------------------- */
+/* class DeclareDatatypeNodeCommand */
+/* -------------------------------------------------------------------------- */
+
+DeclareDatatypeNodeCommand::DeclareDatatypeNodeCommand(
+ const std::vector<TypeNode>& datatypes)
+ : d_datatypes(datatypes)
+{
+}
+
+void DeclareDatatypeNodeCommand::toStream(std::ostream& out,
+ int toDepth,
+ bool types,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdDatatypeDeclaration(out,
+ d_datatypes);
+}
+
+NodeCommand* DeclareDatatypeNodeCommand::clone() const
+{
+ return new DeclareDatatypeNodeCommand(d_datatypes);
+}
+
+/* -------------------------------------------------------------------------- */
+/* class DefineFunctionNodeCommand */
+/* -------------------------------------------------------------------------- */
+
+DefineFunctionNodeCommand::DefineFunctionNodeCommand(
+ const std::string& id,
+ Node fun,
+ const std::vector<Node>& formals,
+ Node formula)
+ : d_id(id), d_fun(fun), d_formals(formals), d_formula(formula)
+{
+}
+
+void DefineFunctionNodeCommand::toStream(std::ostream& out,
+ int toDepth,
+ bool types,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdDefineFunction(
+ out,
+ d_fun.toString(),
+ d_formals,
+ d_fun.getType().getRangeType(),
+ d_formula);
+}
+
+NodeCommand* DefineFunctionNodeCommand::clone() const
+{
+ return new DefineFunctionNodeCommand(d_id, d_fun, d_formals, d_formula);
+}
+
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file node_command.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Abdalrhman Mohamed
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Datastructures used for printing commands internally.
+ **
+ ** Datastructures used for printing commands internally.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__SMT__NODE_COMMAND_H
+#define CVC4__SMT__NODE_COMMAND_H
+
+#include <string>
+
+#include "expr/node.h"
+#include "expr/type_node.h"
+#include "options/language.h"
+
+namespace CVC4 {
+
+/**
+ * A node version of Command. DO NOT use this version unless there is a need
+ * to buffer commands for later use (e.g., printing models).
+ */
+class NodeCommand
+{
+ public:
+ /** Destructor */
+ virtual ~NodeCommand();
+
+ /** Print this NodeCommand to output stream */
+ virtual void toStream(
+ std::ostream& out,
+ int toDepth = -1,
+ bool types = false,
+ size_t dag = 1,
+ OutputLanguage language = language::output::LANG_AUTO) const = 0;
+
+ /** Get a string representation of this NodeCommand */
+ std::string toString() const;
+
+ /** Clone this NodeCommand (make a shallow copy). */
+ virtual NodeCommand* clone() const = 0;
+};
+
+std::ostream& operator<<(std::ostream& out, const NodeCommand& nc);
+
+/**
+ * Declare n-ary function symbol.
+ * SMT-LIB: ( declare-fun <id> ( <type.getArgTypes()> ) <type.getRangeType()> )
+ */
+class DeclareFunctionNodeCommand : public NodeCommand
+{
+ public:
+ DeclareFunctionNodeCommand(const std::string& id, Node fun, TypeNode type);
+ void toStream(
+ std::ostream& out,
+ int toDepth = -1,
+ bool types = false,
+ size_t dag = 1,
+ OutputLanguage language = language::output::LANG_AUTO) const override;
+ NodeCommand* clone() const override;
+ const Node& getFunction() const;
+ bool getPrintInModel() const;
+ bool getPrintInModelSetByUser() const;
+ void setPrintInModel(bool p);
+
+ private:
+ std::string d_id;
+ Node d_fun;
+ TypeNode d_type;
+ bool d_printInModel;
+ bool d_printInModelSetByUser;
+};
+
+/**
+ * Create datatype sort.
+ * SMT-LIB: ( declare-datatypes ( <datatype decls>{n+1} ) ( <datatypes>{n+1} ) )
+ */
+class DeclareDatatypeNodeCommand : public NodeCommand
+{
+ public:
+ DeclareDatatypeNodeCommand(const std::vector<TypeNode>& datatypes);
+ void toStream(
+ std::ostream& out,
+ int toDepth = -1,
+ bool types = false,
+ size_t dag = 1,
+ OutputLanguage language = language::output::LANG_AUTO) const override;
+ NodeCommand* clone() const override;
+
+ private:
+ std::vector<TypeNode> d_datatypes;
+};
+
+/**
+ * Declare uninterpreted sort.
+ * SMT-LIB: ( declare-sort <id> <arity> )
+ */
+class DeclareTypeNodeCommand : public NodeCommand
+{
+ public:
+ DeclareTypeNodeCommand(const std::string& id, size_t arity, TypeNode type);
+ void toStream(
+ std::ostream& out,
+ int toDepth = -1,
+ bool types = false,
+ size_t dag = 1,
+ OutputLanguage language = language::output::LANG_AUTO) const override;
+ NodeCommand* clone() const override;
+ const std::string getSymbol() const;
+ const TypeNode& getType() const;
+
+ private:
+ std::string d_id;
+ size_t d_arity;
+ TypeNode d_type;
+};
+
+/**
+ * Define n-ary function.
+ * SMT-LIB: ( define-fun <id> ( <formals> ) <fun.getType()> <formula> )
+ */
+class DefineFunctionNodeCommand : public NodeCommand
+{
+ public:
+ DefineFunctionNodeCommand(const std::string& id,
+ Node fun,
+ const std::vector<Node>& formals,
+ Node formula);
+ void toStream(
+ std::ostream& out,
+ int toDepth = -1,
+ bool types = false,
+ size_t dag = 1,
+ OutputLanguage language = language::output::LANG_AUTO) const override;
+ NodeCommand* clone() const override;
+
+ private:
+ std::string d_id;
+ Node d_fun;
+ std::vector<Node> d_formals;
+ Node d_formula;
+};
+
+} // namespace CVC4
+
+#endif /* CVC4__SMT__NODE_COMMAND_H */
ss << language::SetLanguage(
language::SetLanguage::getLanguage(Dump.getStream()))
<< func;
- DefineFunctionCommand c(ss.str(), func, formals, formula, global);
+ std::vector<Node> nFormals;
+ nFormals.reserve(formals.size());
+
+ for (const Expr& formal : formals)
+ {
+ nFormals.push_back(formal.getNode());
+ }
+
+ DefineFunctionNodeCommand nc(
+ ss.str(), func.getNode(), nFormals, formula.getNode());
d_dumpm->addToModelCommandAndDump(
- c, ExprManager::VAR_FLAG_DEFINED, true, "declarations");
+ nc, ExprManager::VAR_FLAG_DEFINED, true, "declarations");
// type check body
debugCheckFunctionBody(formula, formals, func);
projects / cvc5.git / commitdiff