summaryrefslogtreecommitdiff
path: root/src/parser/smt2/smt2.h
diff options
context:
space:
mode:
authorTim King <taking@google.com>2016-11-13 20:34:10 -0800
committerTim King <taking@google.com>2016-11-13 20:34:10 -0800
commita3050a31487c9115293f1ee9a097ce27dae31218 (patch)
tree5f04e894d8cc763e34d8672877d88e4c040d75de /src/parser/smt2/smt2.h
parent31c0d3b5f464983eab6e72d234934b29ef2027b6 (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.h9
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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback