3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-05 09:04:07 +00:00

add outline for interval reasoning

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-01-22 23:28:36 -08:00
parent 273aff5ed6
commit 3b5ae285d9
4 changed files with 70 additions and 4 deletions

View file

@ -39,7 +39,7 @@ def init_project_def():
add_lib('macros', ['rewriter'], 'ast/macros')
add_lib('model', ['macros'])
add_lib('converters', ['model'], 'ast/converters')
add_lib('simplifiers', ['euf', 'normal_forms', 'bit_blaster', 'converters', 'substitution'], 'ast/simplifiers')
add_lib('simplifiers', ['euf', 'normal_forms', 'bit_blaster', 'interval', 'converters', 'substitution'], 'ast/simplifiers')
add_lib('tactic', ['simplifiers'])
add_lib('solver', ['params', 'model', 'tactic', 'proofs'])
add_lib('cmd_context', ['solver', 'rewriter', 'params'])

View file

@ -20,9 +20,10 @@ z3_add_component(simplifiers
solve_context_eqs.cpp
solve_eqs.cpp
COMPONENT_DEPENDENCIES
euf
rewriter
bit_blaster
euf
interval
normal_forms
rewriter
substitution
)

View file

@ -297,6 +297,61 @@ bool bound_simplifier::has_upper(expr* x, rational& n, bool& strict) {
return false;
}
void bound_simplifier::get_bounds(expr* x, scoped_interval& i) {
i.m().reset_upper(i);
i.m().reset_lower(i);
rational n;
if (a.is_numeral(x, n)) {
i.m().set(i, n.to_mpq());
return;
}
if (is_var(x)) {
unsigned v = to_var(x);
bool strict;
if (bp.has_upper(v)) {
mpq const& q = bp.upper(v, strict);
i_cfg.set_upper_is_open(i, strict);
i_cfg.set_upper(i, q);
}
if (bp.has_lower(v)) {
mpq const& q = bp.lower(v, strict);
i_cfg.set_lower_is_open(i, strict);
i_cfg.set_lower(i, q);
}
}
if (a.is_add(x)) {
scoped_interval sum_i(i.m());
scoped_interval arg_i(i.m());
i.m().set(sum_i, mpq(0));
for (expr* arg : *to_app(x)) {
get_bounds(arg, arg_i);
i.m().add(sum_i, arg_i, sum_i);
}
// TODO: intersect
i.m().set(i, sum_i);
}
if (a.is_mul(x)) {
scoped_interval mul_i(i.m());
scoped_interval arg_i(i.m());
i.m().set(mul_i, mpq(1));
for (expr* arg : *to_app(x)) {
get_bounds(arg, arg_i);
i.m().add(mul_i, arg_i, mul_i);
}
// TODO: intersect
i.m().set(i, mul_i);
}
// etc:
// import interval from special case code for lower and upper.
}
void bound_simplifier::reset() {
bp.reset();

View file

@ -23,14 +23,21 @@ Description:
#include "ast/rewriter/th_rewriter.h"
#include "ast/simplifiers/dependent_expr_state.h"
#include "ast/simplifiers/bound_propagator.h"
#include "math/interval/interval.h"
class bound_simplifier : public dependent_expr_simplifier {
typedef interval_manager<im_default_config> interval_manager;
typedef interval_manager::interval interval;
typedef _scoped_interval<interval_manager> scoped_interval;
arith_util a;
th_rewriter m_rewriter;
unsynch_mpq_manager nm;
small_object_allocator m_alloc;
bound_propagator bp;
im_default_config i_cfg;
interval_manager i_manager;
unsigned m_num_vars = 0;
ptr_vector<expr> m_var2expr;
unsigned_vector m_expr2var;
@ -68,6 +75,7 @@ class bound_simplifier : public dependent_expr_simplifier {
bool has_upper(expr* x, rational& n, bool& strict);
bool has_lower(expr* x, rational& n, bool& strict);
void get_bounds(expr* x, scoped_interval&);
// e = x + offset
bool is_offset(expr* e, expr* x, rational& offset);
@ -78,7 +86,9 @@ public:
dependent_expr_simplifier(m, fmls),
a(m),
m_rewriter(m),
bp(nm, m_alloc, p) {
bp(nm, m_alloc, p),
i_cfg(nm),
i_manager(m.limit(), im_default_config(nm)) {
}
char const* name() const override { return "bounds-simplifier"; }