diff options
author | Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com> | 2020-09-02 11:50:41 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-09-02 11:50:41 -0500 |
commit | dd912a03113bbc5ad93260babba061362b660acd (patch) | |
tree | a674b912b0bbd178b46b51f09abe5cf7d1c13c6a /src/printer/cvc | |
parent | 95bba975fd13261ca8854d9fb30d03fc7447eb80 (diff) |
Introduce an internal version of Commands. (#4988)
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.
Diffstat (limited to 'src/printer/cvc')
-rw-r--r-- | src/printer/cvc/cvc_printer.cpp | 30 | ||||
-rw-r--r-- | src/printer/cvc/cvc_printer.h | 2 |
2 files changed, 17 insertions, 15 deletions
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 89b516511..b94977cfe 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -33,6 +33,7 @@ #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" @@ -1059,11 +1060,11 @@ void CvcPrinter::toStream(std::ostream& out, const CommandStatus* s) const 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() @@ -1104,11 +1105,12 @@ void DeclareTypeCommandToStream(std::ostream& out, } } -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 @@ -1172,23 +1174,23 @@ void CvcPrinter::toStream(std::ostream& out, const Model& m) const 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; } } diff --git a/src/printer/cvc/cvc_printer.h b/src/printer/cvc/cvc_printer.h index 0fd3d3a49..3c61fb74f 100644 --- a/src/printer/cvc/cvc_printer.h +++ b/src/printer/cvc/cvc_printer.h @@ -177,7 +177,7 @@ class CvcPrinter : public CVC4::Printer 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 */ |