diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-01-11 09:46:28 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-01-11 09:46:28 -0600 |
| commit | b8841e768a37131c492508cd0e12b9acd8bf4c2b (patch) | |
| tree | a4de18a51ac37abcf874265bea431154f18cc2ac /src/smt/dump_manager.h | |
| parent | ae82eb306143ade54a6f99b2aae0b62b8c77cd35 (diff) | |
Further simplifications in preparation for removing Expr layer (#5756)
This deletes variable flags from NodeManager::mkVar and moves ExprManager sort flags to NodeManager.
These flags are used for determining when a variable or sort should be printed via the old dump infrastructure. The old dump infrastructure is simplified in this PR accordingly.
This PR should preserve behavior of the previous dumping with a minor exception that the internal trace "declarations" will also included symbols introduced from define-fun. This will be further refactored later. This is in preparation for removing the includes expr.h/expr_manager.h from node_manager.h.
Diffstat (limited to 'src/smt/dump_manager.h')
| -rw-r--r-- | src/smt/dump_manager.h | 9 |
1 files changed, 3 insertions, 6 deletions
diff --git a/src/smt/dump_manager.h b/src/smt/dump_manager.h index 3238d3a8d..192bb2324 100644 --- a/src/smt/dump_manager.h +++ b/src/smt/dump_manager.h @@ -49,13 +49,10 @@ class DumpManager */ void resetAssertions(); /** - * Add to Model command. This is used for recording a command - * that should be reported during a get-model call. + * Add to dump command. This is used for recording a command + * that should be reported via the dumpTag trace. */ - void addToModelCommandAndDump(const NodeCommand& c, - uint32_t flags = 0, - bool userVisible = true, - const char* dumpTag = "declarations"); + void addToDump(const NodeCommand& c, const char* dumpTag = "declarations"); /** * Set that function f should print in the model if and only if p is true. |