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/smt/dump_manager.h | |
| 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/smt/dump_manager.h')
| -rw-r--r-- | src/smt/dump_manager.h | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/src/smt/dump_manager.h b/src/smt/dump_manager.h index 6f2ee37a1..2ce0570e4 100644 --- a/src/smt/dump_manager.h +++ b/src/smt/dump_manager.h @@ -22,7 +22,7 @@ #include "context/cdlist.h" #include "expr/node.h" -#include "smt/command.h" +#include "smt/node_command.h" namespace CVC4 { namespace smt { @@ -36,7 +36,7 @@ namespace smt { */ class DumpManager { - typedef context::CDList<Command*> CommandList; + typedef context::CDList<NodeCommand*> CommandList; public: DumpManager(context::UserContext* u); @@ -54,7 +54,7 @@ class DumpManager * 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"); @@ -66,7 +66,7 @@ class DumpManager /** 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 */ @@ -77,7 +77,7 @@ class DumpManager * 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., @@ -89,7 +89,7 @@ class DumpManager * 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. @@ -97,7 +97,7 @@ class DumpManager * 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 |