mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 10:55:50 +00:00
Code Activity

enforce arithmetic normalization

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-08-26 10:41:25 -07:00
parent 0d5cfe9292
commit 82a937d1af
5 changed files with 27 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/api/api_context.cpp
View file

@ -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() {

8
src/ast/ast_smt2_pp.cpp
View file

@ -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);

2
src/ast/rewriter/arith_rewriter.cpp
View file

@ -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;

17
src/ast/rewriter/poly_rewriter_def.h
View file

@ -704,8 +704,10 @@ br_status poly_rewriter<Config>::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<Config>::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<Config>::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;
}

9
src/smt/asserted_formulas_new.cpp
View file

@ -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, vector<justifie
}
else if (m.is_not(e, e1) && m.is_or(e1)) {
for (unsigned i = 0; i < to_app(e1)->get_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<justifie
void asserted_formulas_new::set_eliminate_and(bool flag) {
params_ref p;
p.set_bool("elim_and", true);
p.set_bool("arith_lhs", true);
m_rewriter.updt_params(p);
flush_cache();
}
@ -430,7 +436,6 @@ void asserted_formulas_new::propagate_values() {
m_scoped_substitution.push();
unsigned prop = num_prop;
TRACE("propagate_values", tout << "before:\n"; display(tout););
IF_IVERBOSE(10, verbose_stream() << "(smt.propagate-values)\n";);
unsigned i = m_qhead;
unsigned sz = m_formulas.size();
for (; i < sz; i++) {