diff options
author | Tim King <taking@google.com> | 2016-11-13 20:34:10 -0800 |
---|---|---|
committer | Tim King <taking@google.com> | 2016-11-13 20:34:10 -0800 |
commit | a3050a31487c9115293f1ee9a097ce27dae31218 (patch) | |
tree | 5f04e894d8cc763e34d8672877d88e4c040d75de /src/parser/smt2/smt2.h | |
parent | 31c0d3b5f464983eab6e72d234934b29ef2027b6 (diff) |
Adding garbage collection for the Smt2 Parser for Commands when exceptions are thrown.
Diffstat (limited to 'src/parser/smt2/smt2.h')
-rw-r--r-- | src/parser/smt2/smt2.h | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index b99e142ba..fc930dc79 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -295,7 +295,8 @@ public: case kind::BITVECTOR_MULT: case kind::BITVECTOR_PLUS: if(numArgs != 2) { - parseError("Operator requires exact 2 arguments in strict SMT-LIB compliance mode: " + kindToString(kind)); + parseError("Operator requires exact 2 arguments in strict SMT-LIB " + "compliance mode: " + kindToString(kind)); } break; default: @@ -304,6 +305,12 @@ public: } } + // Throw a ParserException with msg appended with the current logic. + inline void parseErrorLogic(const std::string& msg) throw(ParserException) { + const std::string withLogic = msg + getLogic().getLogicString(); + parseError(withLogic); + } + private: std::map< CVC4::Expr, CVC4::Type > d_sygus_bound_var_type; std::map< CVC4::Expr, std::vector< CVC4::Expr > > d_sygus_let_func_to_vars; |