diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-11-12 18:36:45 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-11-12 18:36:45 +0000 |
commit | ff1666905d56bf9dff0a22162688ac155200091c (patch) | |
tree | ba34bfd3feeee7ac56196fad946c09a599ee78a0 /src/smt/smt_engine.h | |
parent | 1c2c416b953309279c43c86a46b5690642ff95dd (diff) |
Fix for bug 444, dealing with the placing of set-logic in dumping modes.
CVC4 now produces equivalent output when dumping the SMT1 and SMT2 attachments to that bug report.
This also fixes a memory leak in the new-variable-notification mechanism.
(this commit was certified error- and warning-free by the test-and-commit script.)
Diffstat (limited to 'src/smt/smt_engine.h')
-rw-r--r-- | src/smt/smt_engine.h | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 5c383071a..b2ac0b886 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -149,6 +149,14 @@ class CVC4_PUBLIC SmtEngine { smt::CommandList* d_modelCommands; /** + * A vector of declaration commands waiting to be dumped out. + * Once the SmtEngine is fully initialized, we'll dump them. + * This ensures the declarations come after the set-logic and + * any necessary set-option commands are dumped. + */ + std::vector<Command*> d_dumpCommands; + + /** * The logic we're in. */ LogicInfo d_logic; @@ -295,7 +303,7 @@ class CVC4_PUBLIC SmtEngine { * Add to Model command. This is used for recording a command * that should be reported during a get-model call. */ - void addToModelCommand(Command* c); + void addToModelCommandAndDump(const Command& c, const char* dumpTag = "declarations"); /** * Get the model (only if immediately preceded by a SAT |