diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp index aa2b7b289..4abaad9f8 100644 --- a/src/cmd_context/basic_cmds.cpp +++ b/src/cmd_context/basic_cmds.cpp @@ -205,7 +205,7 @@ UNARY_CMD(set_logic_cmd, "set-logic", "", "set the background logic.", C if (ctx.set_logic(arg)) ctx.print_success(); else - ctx.print_unsupported(symbol::null); + ctx.print_unsupported(symbol::null, m_line, m_pos); ); UNARY_CMD(pp_cmd, "display", "", "display the given term.", CPK_EXPR, expr *, { @@ -436,7 +436,7 @@ public: virtual void execute(cmd_context & ctx) { if (m_unsupported) - ctx.print_unsupported(m_option); + ctx.print_unsupported(m_option, m_line, m_pos); else ctx.print_success(); } @@ -472,7 +472,7 @@ public: // print_bool(ctx, ); // } else if (opt == m_expand_definitions) { - ctx.print_unsupported(m_expand_definitions); + ctx.print_unsupported(m_expand_definitions, m_line, m_pos); } else if (opt == m_interactive_mode) { print_bool(ctx, ctx.interactive_mode()); @@ -523,7 +523,7 @@ public: ctx.regular_stream() << gparams::get_value(opt) << std::endl; } catch (gparams::exception ex) { - ctx.print_unsupported(opt); + ctx.print_unsupported(opt, m_line, m_pos); } } } @@ -585,7 +585,7 @@ public: ctx.display_statistics(); } else { - ctx.print_unsupported(opt); + ctx.print_unsupported(opt, m_line, m_pos); } } }; diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h index 86563eb9b..516b47e3c 100644 --- a/src/cmd_context/cmd_context.h +++ b/src/cmd_context/cmd_context.h @@ -262,7 +262,7 @@ protected: bool supported_logic(symbol const & s) const; void print_unsupported_msg() { regular_stream() << "unsupported" << std::endl; } - void print_unsupported_info(symbol const& s) { if (s != symbol::null) diagnostic_stream() << "; " << s << std::endl;} + void print_unsupported_info(symbol const& s, int line, int pos) { if (s != symbol::null) diagnostic_stream() << "; " << s << " line: " << line << " position: " << pos << std::endl;} void mk_solver(); @@ -292,7 +292,7 @@ public: void set_print_success(bool flag) { m_print_success = flag; } bool print_success_enabled() const { return m_print_success; } void print_success() { if (print_success_enabled()) regular_stream() << "success" << std::endl; } - void print_unsupported(symbol const & s) { print_unsupported_msg(); print_unsupported_info(s); } + void print_unsupported(symbol const & s, int line, int pos) { print_unsupported_msg(); print_unsupported_info(s, line, pos); } bool global_decls() const { return m_global_decls; } void set_global_decls(bool flag) { SASSERT(!has_manager()); m_global_decls = flag; } unsigned random_seed() const { return m_random_seed; } diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp index aa38db85f..6931a7973 100644 --- a/src/parsers/smt2/smt2parser.cpp +++ b/src/parsers/smt2/smt2parser.cpp @@ -2264,12 +2264,12 @@ namespace smt2 { while (!curr_is_rparen()) { consume_sexpr(); } - m_ctx.print_unsupported(s); + m_ctx.print_unsupported(s, m_scanner.get_line(), m_scanner.get_pos()); next(); return; } - void parse_ext_cmd() { + void parse_ext_cmd(int line, int pos) { symbol s = curr_id(); m_curr_cmd = m_ctx.find_cmd(s); if (m_curr_cmd == 0) { @@ -2283,6 +2283,7 @@ namespace smt2 { unsigned expr_spos = size(m_expr_stack); unsigned sexpr_spos = size(m_sexpr_stack); unsigned sym_spos = m_symbol_stack.size(); + m_curr_cmd->set_line_pos(line, pos); m_curr_cmd->prepare(m_ctx); while (true) { if (curr_is_rparen()) { @@ -2313,6 +2314,8 @@ namespace smt2 { void parse_cmd() { SASSERT(curr_is_lparen()); + int line = m_scanner.get_line(); + int pos = m_scanner.get_pos(); next(); check_identifier("invalid command, symbol expected"); symbol s = curr_id(); @@ -2368,7 +2371,7 @@ namespace smt2 { parse_reset(); return; } - parse_ext_cmd(); + parse_ext_cmd(line, pos); } public: diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp index 0caefd3fe..8dc892f9d 100644 --- a/src/smt/asserted_formulas.cpp +++ b/src/smt/asserted_formulas.cpp @@ -624,7 +624,8 @@ void asserted_formulas::propagate_values() { if (m_manager.proofs_enabled()) new_prs1.push_back(pr); } - TRACE("propagate_values", tout << "found:\n" << mk_pp(lhs, m_manager) << "\n->\n" << mk_pp(rhs, m_manager) << "\nproof: " << mk_pp(pr, m_manager) << "\n";); + TRACE("propagate_values", tout << "found:\n" << mk_pp(lhs, m_manager) << "\n->\n" << mk_pp(rhs, m_manager) << "\n"; + if (pr) tout << "proof: " << mk_pp(pr, m_manager) << "\n";); m_simplifier.cache_result(lhs, rhs, pr); found = true; continue; diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index 7b8a83520..7c637309f 100644 --- a/src/smt/theory_fpa.cpp +++ b/src/smt/theory_fpa.cpp @@ -555,12 +555,11 @@ namespace smt { literal l(ctx.mk_bool_var(atom)); ctx.set_var_theory(l.var(), get_id()); - expr_ref bv_atom(m); - bv_atom = convert_atom(atom); - SASSERT(is_app(bv_atom) && m.is_bool(bv_atom)); - bv_atom = m.mk_and(bv_atom, mk_side_conditions()); - - assert_cnstr(m.mk_iff(atom, bv_atom)); + expr_ref bv_atom(convert_atom(atom)); + expr_ref bv_atom_w_side_c(m); + bv_atom_w_side_c = m.mk_and(bv_atom, mk_side_conditions()); + m_th_rw(bv_atom_w_side_c); + assert_cnstr(m.mk_eq(atom, bv_atom_w_side_c)); return true; } diff --git a/src/util/cmd_context_types.h b/src/util/cmd_context_types.h index bdd7857f8..29ac56a49 100644 --- a/src/util/cmd_context_types.h +++ b/src/util/cmd_context_types.h @@ -82,8 +82,11 @@ typedef std::pair sorted_var; */ class cmd { symbol m_name; +protected: + int m_line; + int m_pos; public: - cmd(char const * n):m_name(n) {} + cmd(char const * n):m_name(n), m_line(0), m_pos(0) {} virtual ~cmd() {} virtual void reset(cmd_context & ctx) {} virtual void finalize(cmd_context & ctx) {} @@ -93,6 +96,7 @@ public: virtual unsigned get_arity() const { return 0; } // command invocation + void set_line_pos(int line, int pos) { m_line = line; m_pos = pos; } virtual void prepare(cmd_context & ctx) {} virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const { UNREACHABLE(); return CPK_UINT; } virtual void set_next_arg(cmd_context & ctx, unsigned val) { UNREACHABLE(); }