summaryrefslogtreecommitdiff
path: root/src/parser/smt2/smt2.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/parser/smt2/smt2.cpp')
-rw-r--r--src/parser/smt2/smt2.cpp18
1 files changed, 18 insertions, 0 deletions
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 21b6a1e5b..62814ca25 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -233,6 +233,24 @@ bool Smt2::logicIsSet() {
return d_logicSet;
}
+void Smt2::reset() {
+ d_logicSet = false;
+ d_logic = LogicInfo();
+ operatorKindMap.clear();
+ d_lastNamedTerm = std::pair<Expr, std::string>();
+ d_unsatCoreNames = std::stack< std::map<Expr, std::string> >();
+ this->Parser::reset();
+
+ d_unsatCoreNames.push(std::map<Expr, std::string>());
+ if( !strictModeEnabled() ) {
+ addTheory(Smt2::THEORY_CORE);
+ }
+}
+
+void Smt2::resetAssertions() {
+ this->Parser::reset();
+}
+
void Smt2::setLogic(const std::string& name) {
d_logicSet = true;
if(logicIsForced()) {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback