summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/parser/parser.cpp10
-rw-r--r--src/parser/parser.h6
2 files changed, 13 insertions, 3 deletions
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index ac93c93d2..2377b8a44 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -61,6 +61,16 @@ Parser::Parser(ExprManager* exprManager, Input* input, bool strictMode,
d_input->setParser(*this);
}
+Parser::~Parser() {
+ for (std::list<Command*>::iterator iter = d_commandQueue.begin();
+ iter != d_commandQueue.end(); ++iter) {
+ Command* command = *iter;
+ delete command;
+ }
+ d_commandQueue.clear();
+ delete d_input;
+}
+
Expr Parser::getSymbol(const std::string& name, SymbolType type) {
checkDeclaration(name, CHECK_DECLARED, type);
assert(isDeclared(name, type));
diff --git a/src/parser/parser.h b/src/parser/parser.h
index 351aa858a..b310456bd 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -230,6 +230,8 @@ class CVC4_PUBLIC Parser {
* "Preemption commands": extra commands implied by subterms that
* should be issued before the currently-being-parsed command is
* issued. Used to support SMT-LIBv2 ":named" attribute on terms.
+ *
+ * Owns the memory of the Commands in the queue.
*/
std::list<Command*> d_commandQueue;
@@ -254,9 +256,7 @@ protected:
public:
- virtual ~Parser() {
- delete d_input;
- }
+ virtual ~Parser();
/** Get the associated <code>ExprManager</code>. */
inline ExprManager* getExprManager() const {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback