From 82a937d1af25f9466556670684ac9283023ef586 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 26 Aug 2017 10:41:25 -0700 Subject: [PATCH] enforce arithmetic normalization Signed-off-by: Nikolaj Bjorner --- src/api/api_context.cpp | 3 ++- src/ast/ast_smt2_pp.cpp | 8 ++++---- src/ast/rewriter/arith_rewriter.cpp | 2 +- src/ast/rewriter/poly_rewriter_def.h | 17 +++++++++++++---- src/smt/asserted_formulas_new.cpp | 9 +++++++-- 5 files changed, 27 insertions(+), 12 deletions(-) diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index c99d3f0c8..1e3f7a0a4 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -150,8 +150,9 @@ namespace api { void context::set_error_code(Z3_error_code err) { m_error_code = err; - if (err != Z3_OK) + if (err != Z3_OK) { invoke_error_handler(err); + } } void context::check_searching() { diff --git a/src/ast/ast_smt2_pp.cpp b/src/ast/ast_smt2_pp.cpp index 5c3eb93c2..51ccc1e7d 100644 --- a/src/ast/ast_smt2_pp.cpp +++ b/src/ast/ast_smt2_pp.cpp @@ -1222,15 +1222,15 @@ mk_ismt2_pp::mk_ismt2_pp(ast * t, ast_manager & m, unsigned indent, unsigned num std::ostream& operator<<(std::ostream& out, mk_ismt2_pp const & p) { smt2_pp_environment_dbg env(p.m_manager); - if (is_expr(p.m_ast)) { + if (p.m_ast == 0) { + out << "null"; + } + else if (is_expr(p.m_ast)) { ast_smt2_pp(out, to_expr(p.m_ast), env, p.m_params, p.m_indent, p.m_num_vars, p.m_var_prefix); } else if (is_sort(p.m_ast)) { ast_smt2_pp(out, to_sort(p.m_ast), env, p.m_params, p.m_indent); } - else if (p.m_ast == 0) { - out << "null"; - } else { SASSERT(is_func_decl(p.m_ast)); ast_smt2_pp(out, to_func_decl(p.m_ast), env, p.m_params, p.m_indent); diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp index 18556b71b..4b00cde45 100644 --- a/src/ast/rewriter/arith_rewriter.cpp +++ b/src/ast/rewriter/arith_rewriter.cpp @@ -371,7 +371,7 @@ br_status arith_rewriter::mk_le_ge_eq_core(expr * arg1, expr * arg2, op_kind kin (is_zero(arg2) && is_reduce_power_target(arg1, kind == EQ))) return reduce_power(arg1, arg2, kind, result); br_status st = cancel_monomials(arg1, arg2, m_arith_lhs, new_arg1, new_arg2); - TRACE("mk_le_bug", tout << "st: " << st << "\n";); + TRACE("mk_le_bug", tout << "st: " << st << " " << new_arg1 << " " << new_arg2 << "\n";); if (st != BR_FAILED) { arg1 = new_arg1; arg2 = new_arg2; diff --git a/src/ast/rewriter/poly_rewriter_def.h b/src/ast/rewriter/poly_rewriter_def.h index 731a0538a..2a6bd2c50 100644 --- a/src/ast/rewriter/poly_rewriter_def.h +++ b/src/ast/rewriter/poly_rewriter_def.h @@ -704,8 +704,10 @@ br_status poly_rewriter::cancel_monomials(expr * lhs, expr * rhs, bool m } } - if (move && num_coeffs == 0 && is_numeral(rhs)) + if (move && num_coeffs == 0 && is_numeral(rhs)) { + TRACE("mk_le_bug", tout << "no coeffs\n";); return BR_FAILED; + } for (unsigned i = 0; i < rhs_sz; i++) { expr * arg = rhs_monomials[i]; @@ -723,15 +725,21 @@ br_status poly_rewriter::cancel_monomials(expr * lhs, expr * rhs, bool m } normalize(c); - + + TRACE("mk_le_bug", tout << c << "\n";); + if (!has_multiple && num_coeffs <= 1) { if (move) { - if (is_numeral(rhs)) + if (is_numeral(rhs)) { + TRACE("mk_le_bug", tout << "rhs is numeral\n";); return BR_FAILED; + } } else { - if (num_coeffs == 0 || is_numeral(rhs)) + if (num_coeffs == 0 || is_numeral(rhs)) { + TRACE("mk_le_bug", tout << "rhs is numeral or no coeffs\n";); return BR_FAILED; + } } } @@ -847,6 +855,7 @@ br_status poly_rewriter::cancel_monomials(expr * lhs, expr * rhs, bool m new_lhs_monomials[0] = insert_c_lhs ? mk_numeral(c) : NULL; lhs_result = mk_add_app(new_lhs_monomials.size() - lhs_offset, new_lhs_monomials.c_ptr() + lhs_offset); rhs_result = mk_add_app(new_rhs_monomials.size() - rhs_offset, new_rhs_monomials.c_ptr() + rhs_offset); + TRACE("mk_le_bug", tout << lhs_result << " " << rhs_result << "\n";); return BR_DONE; } diff --git a/src/smt/asserted_formulas_new.cpp b/src/smt/asserted_formulas_new.cpp index 39c432b61..5d4783bf8 100644 --- a/src/smt/asserted_formulas_new.cpp +++ b/src/smt/asserted_formulas_new.cpp @@ -59,6 +59,11 @@ asserted_formulas_new::asserted_formulas_new(ast_manager & m, smt_params & p): m_apply_quasi_macros(*this) { m_macro_finder = alloc(macro_finder, m, m_macro_manager); + + params_ref pa; + pa.set_bool("arith_lhs", true); + m_rewriter.updt_params(pa); + } void asserted_formulas_new::setup() { @@ -103,7 +108,7 @@ void asserted_formulas_new::push_assertion(expr * e, proof * pr, vectorget_num_args(); ++i) { - expr* arg = to_app(e1)->get_arg(i), *e2; + expr* arg = to_app(e1)->get_arg(i); proof_ref _pr(m.mk_not_or_elim(pr, i), m); expr_ref narg(mk_not(m, arg), m); push_assertion(narg, _pr, result); @@ -117,6 +122,7 @@ void asserted_formulas_new::push_assertion(expr * e, proof * pr, vector