mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 06:03:23 +00:00
Code Activity

fix context simplification

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-06-09 11:30:56 -07:00
parent d0085b41c1
commit ac00306355
2 changed files with 37 additions and 21 deletions
Download patch file Download diff file Expand all files Collapse all files

52
src/ast/simplifiers/bound_simplifier.cpp
View file

@ -84,42 +84,54 @@ br_status bound_simplifier::reduce_app(func_decl* f, unsigned num_args, expr* co
IF_VERBOSE(2, verbose_stream() << "potentially missed simplification: " << mk_pp(x, m) << " " << lo << " " << hi << " not reduced\n"); IF_VERBOSE(2, verbose_stream() << "potentially missed simplification: " << mk_pp(x, m) << " " << lo << " " << hi << " not reduced\n");
} }
#if 0 expr_ref_buffer new_args(m);
expr* x = nullptr; expr_ref new_arg(m);
bool strict = false; bool change = false;
bool is_upper_bound = for (unsigned i = 0; i < num_args; ++i) {
(a.is_le(f) && a.is_numeral(args[1], N) && (x = args[0], true)) || expr* arg = args[i];
(a.is_ge(f) && a.is_numeral(args[0], N) && (x = args[1], true)); change = reduce_arg(arg, new_arg) || change;
new_args.push_back(new_arg);
}
if (!change)
return BR_FAILED;
result = m.mk_app(f, num_args, new_args.data());
return BR_DONE;
}
bool bound_simplifier::reduce_arg(expr* arg, expr_ref& result) {
result = arg;
expr* x, *y;
rational N, lo, hi;
bool strict;
if ((a.is_le(arg, x, y) && a.is_numeral(y, N)) ||
(a.is_ge(arg, y, x) && a.is_numeral(y, N))) {
if (is_upper_bound) {
if (has_upper(x, hi, strict) && !strict && N >= hi) { if (has_upper(x, hi, strict) && !strict && N >= hi) {
result = m.mk_true(); result = m.mk_true();
return BR_DONE; return true;
} }
if (has_lower(x, lo, strict) && !strict && N < lo) { if (has_lower(x, lo, strict) && !strict && N < lo) {
result = m.mk_false(); result = m.mk_false();
return BR_DONE; return true;
} }
return BR_FAILED; return false;
} }
bool is_lower_bound =
(a.is_le(f) && a.is_numeral(args[0], N) && (x = args[1], true)) ||
(a.is_ge(f) && a.is_numeral(args[1], N) && (x = args[0], true));
if (is_lower_bound) { if ((a.is_le(arg, y, x) && a.is_numeral(y, N)) ||
(a.is_ge(arg, x, y) && a.is_numeral(y, N))) {
if (has_lower(x, lo, strict) && !strict && N <= lo) { if (has_lower(x, lo, strict) && !strict && N <= lo) {
result = m.mk_true(); result = m.mk_true();
return BR_DONE; return true;
} }
if (has_upper(x, hi, strict) && !strict && N > hi) { if (has_upper(x, hi, strict) && !strict && N > hi) {
result = m.mk_false(); result = m.mk_false();
return BR_DONE; return true;
} }
return BR_FAILED; return false;
} }
#endif return false;
return BR_FAILED;
} }
void bound_simplifier::reduce() { void bound_simplifier::reduce() {

4
src/ast/simplifiers/bound_simplifier.h
View file

@ -77,8 +77,12 @@ class bound_simplifier : public dependent_expr_simplifier {
return v; return v;
} }
bool reduce_arg(expr* arg, expr_ref& result);
br_status reduce_app(func_decl* f, unsigned num_args, expr* const* args, expr_ref& result, proof_ref& pr); br_status reduce_app(func_decl* f, unsigned num_args, expr* const* args, expr_ref& result, proof_ref& pr);
void assert_lower(expr* x, rational const& n, bool strict); void assert_lower(expr* x, rational const& n, bool strict);
void assert_upper(expr* x, rational const& n, bool strict); void assert_upper(expr* x, rational const& n, bool strict);