mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-02 04:11:21 +00:00
Code Activity

tabs

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2015-09-17 13:16:35 +01:00
parent 4d39108808
commit 2e071e89b0
1 changed files with 17 additions and 17 deletions
Download patch file Download diff file Expand all files Collapse all files

34
src/parsers/smt2/smt2parser.cpp
View file

@ -822,10 +822,10 @@ namespace smt2 {
check_rparen("invalid datatype declaration"); check_rparen("invalid datatype declaration");
unsigned sz = new_dt_decls.size(); unsigned sz = new_dt_decls.size();
if (sz == 0) { if (sz == 0) {
m_ctx.print_success(); m_ctx.print_success();
next(); next();
return; return;
} }
else if (sz == 1) { else if (sz == 1) {
symbol missing; symbol missing;
if (new_dt_decls[0]->has_missing_refs(missing)) { if (new_dt_decls[0]->has_missing_refs(missing)) {
@ -868,7 +868,7 @@ namespace smt2 {
TRACE("declare_datatypes", tout << "i: " << i << " new_dt_decls.size(): " << sz << "\n"; TRACE("declare_datatypes", tout << "i: " << i << " new_dt_decls.size(): " << sz << "\n";
for (unsigned i = 0; i < sz; i++) tout << new_dt_decls[i]->get_name() << "\n";); for (unsigned i = 0; i < sz; i++) tout << new_dt_decls[i]->get_name() << "\n";);
m_ctx.print_success(); m_ctx.print_success();
next(); next();
} }
void name_expr(expr * n, symbol const & s) { void name_expr(expr * n, symbol const & s) {
@ -1789,9 +1789,9 @@ namespace smt2 {
m_ctx.insert(decl); m_ctx.insert(decl);
next(); next();
check_rparen("invalid sort declaration, ')' expected"); check_rparen("invalid sort declaration, ')' expected");
} }
m_ctx.print_success(); m_ctx.print_success();
next(); next();
} }
void parse_define_sort() { void parse_define_sort() {
@ -1811,7 +1811,7 @@ namespace smt2 {
m_ctx.insert(decl); m_ctx.insert(decl);
check_rparen("invalid sort definition, ')' expected"); check_rparen("invalid sort definition, ')' expected");
m_ctx.print_success(); m_ctx.print_success();
next(); next();
} }
void parse_define_fun() { void parse_define_fun() {
@ -1840,7 +1840,7 @@ namespace smt2 {
SASSERT(num_vars == m_num_bindings); SASSERT(num_vars == m_num_bindings);
m_num_bindings = 0; m_num_bindings = 0;
m_ctx.print_success(); m_ctx.print_success();
next(); next();
} }
void parse_define_const() { void parse_define_const() {
@ -1860,7 +1860,7 @@ namespace smt2 {
expr_stack().pop_back(); expr_stack().pop_back();
sort_stack().pop_back(); sort_stack().pop_back();
m_ctx.print_success(); m_ctx.print_success();
next(); next();
} }
void parse_declare_fun() { void parse_declare_fun() {
@ -1879,7 +1879,7 @@ namespace smt2 {
m_ctx.insert(f); m_ctx.insert(f);
check_rparen("invalid function declaration, ')' expected"); check_rparen("invalid function declaration, ')' expected");
m_ctx.print_success(); m_ctx.print_success();
next(); next();
} }
void parse_declare_const() { void parse_declare_const() {
@ -1899,7 +1899,7 @@ namespace smt2 {
m_ctx.insert(c); m_ctx.insert(c);
check_rparen("invalid constant declaration, ')' expected"); check_rparen("invalid constant declaration, ')' expected");
m_ctx.print_success(); m_ctx.print_success();
next(); next();
} }
unsigned parse_opt_unsigned(unsigned def) { unsigned parse_opt_unsigned(unsigned def) {
@ -1928,7 +1928,7 @@ namespace smt2 {
m_ctx.push(num); m_ctx.push(num);
check_rparen("invalid push command, ')' expected"); check_rparen("invalid push command, ')' expected");
m_ctx.print_success(); m_ctx.print_success();
next(); next();
} }
void parse_pop() { void parse_pop() {
@ -1939,7 +1939,7 @@ namespace smt2 {
m_ctx.pop(num); m_ctx.pop(num);
check_rparen("invalid pop command, ')' expected"); check_rparen("invalid pop command, ')' expected");
m_ctx.print_success(); m_ctx.print_success();
next(); next();
TRACE("after_pop", tout << "expr_stack.size: " << expr_stack().size() << "\n"; m_ctx.dump_assertions(tout);); TRACE("after_pop", tout << "expr_stack.size: " << expr_stack().size() << "\n"; m_ctx.dump_assertions(tout););
} }
@ -1975,7 +1975,7 @@ namespace smt2 {
expr_stack().pop_back(); expr_stack().pop_back();
check_rparen("invalid assert command, ')' expected"); check_rparen("invalid assert command, ')' expected");
m_ctx.print_success(); m_ctx.print_success();
next(); next();
} }
void parse_check_sat() { void parse_check_sat() {
@ -2062,7 +2062,7 @@ namespace smt2 {
} }
m_ctx.regular_stream() << ")" << std::endl; m_ctx.regular_stream() << ")" << std::endl;
expr_stack().shrink(spos); expr_stack().shrink(spos);
next(); next();
} }
void parse_reset() { void parse_reset() {
@ -2073,7 +2073,7 @@ namespace smt2 {
m_ctx.reset(); m_ctx.reset();
reset(); reset();
m_ctx.print_success(); m_ctx.print_success();
next(); next();
} }
void parse_option_value() { void parse_option_value() {