mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 19:52:29 +00:00
Code Activity

Merge branch 'master' of https://github.com/Z3Prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2015-11-02 08:19:11 -08:00
commit 728df41966
6 changed files with 25 additions and 18 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/cmd_context/basic_cmds.cpp
View file

@ -205,7 +205,7 @@ UNARY_CMD(set_logic_cmd, "set-logic", "<symbol>", "set the background logic.", C
if (ctx.set_logic(arg)) if (ctx.set_logic(arg))
ctx.print_success(); ctx.print_success();
else else
ctx.print_unsupported(symbol::null); ctx.print_unsupported(symbol::null, m_line, m_pos);
); );
UNARY_CMD(pp_cmd, "display", "<term>", "display the given term.", CPK_EXPR, expr *, { UNARY_CMD(pp_cmd, "display", "<term>", "display the given term.", CPK_EXPR, expr *, {
@ -436,7 +436,7 @@ public:
virtual void execute(cmd_context & ctx) { virtual void execute(cmd_context & ctx) {
if (m_unsupported) if (m_unsupported)
ctx.print_unsupported(m_option); ctx.print_unsupported(m_option, m_line, m_pos);
else else
ctx.print_success(); ctx.print_success();
} }
@ -472,7 +472,7 @@ public:
// print_bool(ctx, ); // print_bool(ctx, );
// } // }
else if (opt == m_expand_definitions) { 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) { else if (opt == m_interactive_mode) {
print_bool(ctx, ctx.interactive_mode()); print_bool(ctx, ctx.interactive_mode());
@ -523,7 +523,7 @@ public:
ctx.regular_stream() << gparams::get_value(opt) << std::endl; ctx.regular_stream() << gparams::get_value(opt) << std::endl;
} }
catch (gparams::exception ex) { catch (gparams::exception ex) {
ctx.print_unsupported(opt); ctx.print_unsupported(opt, m_line, m_pos);
} }
} }
} }
@ -585,7 +585,7 @@ public:
ctx.display_statistics(); ctx.display_statistics();
} }
else { else {
ctx.print_unsupported(opt); ctx.print_unsupported(opt, m_line, m_pos);
} }
} }
}; };

4
src/cmd_context/cmd_context.h
View file

@ -262,7 +262,7 @@ protected:
bool supported_logic(symbol const & s) const; bool supported_logic(symbol const & s) const;
void print_unsupported_msg() { regular_stream() << "unsupported" << std::endl; } 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(); void mk_solver();
@ -292,7 +292,7 @@ public:
void set_print_success(bool flag) { m_print_success = flag; } void set_print_success(bool flag) { m_print_success = flag; }
bool print_success_enabled() const { return m_print_success; } bool print_success_enabled() const { return m_print_success; }
void print_success() { if (print_success_enabled()) regular_stream() << "success" << std::endl; } 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; } bool global_decls() const { return m_global_decls; }
void set_global_decls(bool flag) { SASSERT(!has_manager()); m_global_decls = flag; } void set_global_decls(bool flag) { SASSERT(!has_manager()); m_global_decls = flag; }
unsigned random_seed() const { return m_random_seed; } unsigned random_seed() const { return m_random_seed; }

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

@ -2264,12 +2264,12 @@ namespace smt2 {
while (!curr_is_rparen()) { while (!curr_is_rparen()) {
consume_sexpr(); consume_sexpr();
} }
m_ctx.print_unsupported(s); m_ctx.print_unsupported(s, m_scanner.get_line(), m_scanner.get_pos());
next(); next();
return; return;
} }
void parse_ext_cmd() { void parse_ext_cmd(int line, int pos) {
symbol s = curr_id(); symbol s = curr_id();
m_curr_cmd = m_ctx.find_cmd(s); m_curr_cmd = m_ctx.find_cmd(s);
if (m_curr_cmd == 0) { if (m_curr_cmd == 0) {
@ -2283,6 +2283,7 @@ namespace smt2 {
unsigned expr_spos = size(m_expr_stack); unsigned expr_spos = size(m_expr_stack);
unsigned sexpr_spos = size(m_sexpr_stack); unsigned sexpr_spos = size(m_sexpr_stack);
unsigned sym_spos = m_symbol_stack.size(); unsigned sym_spos = m_symbol_stack.size();
m_curr_cmd->set_line_pos(line, pos);
m_curr_cmd->prepare(m_ctx); m_curr_cmd->prepare(m_ctx);
while (true) { while (true) {
if (curr_is_rparen()) { if (curr_is_rparen()) {
@ -2313,6 +2314,8 @@ namespace smt2 {
void parse_cmd() { void parse_cmd() {
SASSERT(curr_is_lparen()); SASSERT(curr_is_lparen());
int line = m_scanner.get_line();
int pos = m_scanner.get_pos();
next(); next();
check_identifier("invalid command, symbol expected"); check_identifier("invalid command, symbol expected");
symbol s = curr_id(); symbol s = curr_id();
@ -2368,7 +2371,7 @@ namespace smt2 {
parse_reset(); parse_reset();
return; return;
} }
parse_ext_cmd(); parse_ext_cmd(line, pos);
} }
public: public:

3
src/smt/asserted_formulas.cpp
View file

@ -624,7 +624,8 @@ void asserted_formulas::propagate_values() {
if (m_manager.proofs_enabled()) if (m_manager.proofs_enabled())
new_prs1.push_back(pr); 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); m_simplifier.cache_result(lhs, rhs, pr);
found = true; found = true;
continue; continue;

11
src/smt/theory_fpa.cpp
View file

@ -555,12 +555,11 @@ namespace smt {
literal l(ctx.mk_bool_var(atom)); literal l(ctx.mk_bool_var(atom));
ctx.set_var_theory(l.var(), get_id()); ctx.set_var_theory(l.var(), get_id());
expr_ref bv_atom(m); expr_ref bv_atom(convert_atom(atom));
bv_atom = convert_atom(atom); expr_ref bv_atom_w_side_c(m);
SASSERT(is_app(bv_atom) && m.is_bool(bv_atom)); bv_atom_w_side_c = m.mk_and(bv_atom, mk_side_conditions());
bv_atom = 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));
assert_cnstr(m.mk_iff(atom, bv_atom));
return true; return true;
} }

6
src/util/cmd_context_types.h
View file

@ -82,8 +82,11 @@ typedef std::pair<symbol, sort*> sorted_var;
*/ */
class cmd { class cmd {
symbol m_name; symbol m_name;
protected:
int m_line;
int m_pos;
public: public:
cmd(char const * n):m_name(n) {} cmd(char const * n):m_name(n), m_line(0), m_pos(0) {}
virtual ~cmd() {} virtual ~cmd() {}
virtual void reset(cmd_context & ctx) {} virtual void reset(cmd_context & ctx) {}
virtual void finalize(cmd_context & ctx) {} virtual void finalize(cmd_context & ctx) {}
@ -93,6 +96,7 @@ public:
virtual unsigned get_arity() const { return 0; } virtual unsigned get_arity() const { return 0; }
// command invocation // command invocation
void set_line_pos(int line, int pos) { m_line = line; m_pos = pos; }
virtual void prepare(cmd_context & ctx) {} virtual void prepare(cmd_context & ctx) {}
virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const { UNREACHABLE(); return CPK_UINT; } 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(); } virtual void set_next_arg(cmd_context & ctx, unsigned val) { UNREACHABLE(); }