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

add option to enable equality propagation

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-02-21 11:16:13 -08:00
parent 8c538fd3f0
commit 63c138c08e
3 changed files with 19 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

20
src/tactic/bv/bv_bounds_tactic.cpp
View file

@ -155,6 +155,8 @@ class bv_bounds_simplifier : public ctx_simplify_tactic::simplifier {
typedef obj_map<expr, interval> map; typedef obj_map<expr, interval> map;
ast_manager& m; ast_manager& m;
params_ref m_params;
bool m_propagate_eq;
bv_util m_bv; bv_util m_bv;
vector<map> m_scopes; vector<map> m_scopes;
map *m_bound; map *m_bound;
@ -209,9 +211,19 @@ class bv_bounds_simplifier : public ctx_simplify_tactic::simplifier {
public: public:
bv_bounds_simplifier(ast_manager& m) : m(m), m_bv(m) { bv_bounds_simplifier(ast_manager& m, params_ref const& p) : m(m), m_params(p), m_bv(m) {
m_scopes.push_back(map()); m_scopes.push_back(map());
m_bound = &m_scopes.back(); m_bound = &m_scopes.back();
updt_params(p);
}
virtual void updt_params(params_ref const & p) {
m_propagate_eq = p.get_bool("propagate_eq", false);
}
static void get_param_descrs(param_descrs& r) {
r.insert("propagate-eq", CPK_BOOL, "(default: false) propagate equalities from inequalities");
} }
virtual ~bv_bounds_simplifier() {} virtual ~bv_bounds_simplifier() {}
@ -262,7 +274,7 @@ public:
result = m.mk_true(); result = m.mk_true();
} else if (!b.intersect(ctx, intr)) { } else if (!b.intersect(ctx, intr)) {
result = m.mk_false(); result = m.mk_false();
} else if (false && intr.l == intr.h) { } else if (m_propagate_eq && intr.l == intr.h) {
result = m.mk_eq(t1, m_bv.mk_numeral(intr.l, m.get_sort(t1))); result = m.mk_eq(t1, m_bv.mk_numeral(intr.l, m.get_sort(t1)));
} }
} else if (b.is_full() && b.tight) { } else if (b.is_full() && b.tight) {
@ -291,7 +303,7 @@ public:
} }
virtual simplifier * translate(ast_manager & m) { virtual simplifier * translate(ast_manager & m) {
return alloc(bv_bounds_simplifier, m); return alloc(bv_bounds_simplifier, m, m_params);
} }
virtual unsigned scope_level() const { virtual unsigned scope_level() const {
@ -302,5 +314,5 @@ public:
} }
tactic * mk_bv_bounds_tactic(ast_manager & m, params_ref const & p) { tactic * mk_bv_bounds_tactic(ast_manager & m, params_ref const & p) {
return clean(alloc(ctx_simplify_tactic, m, alloc(bv_bounds_simplifier, m), p)); return clean(alloc(ctx_simplify_tactic, m, alloc(bv_bounds_simplifier, m, p), p));
} }

2
src/tactic/core/ctx_simplify_tactic.cpp
View file

@ -198,6 +198,7 @@ struct ctx_simplify_tactic::imp {
m_max_steps = p.get_uint("max_steps", UINT_MAX); m_max_steps = p.get_uint("max_steps", UINT_MAX);
m_max_depth = p.get_uint("max_depth", 1024); m_max_depth = p.get_uint("max_depth", 1024);
m_bail_on_blowup = p.get_bool("bail_on_blowup", false); m_bail_on_blowup = p.get_bool("bail_on_blowup", false);
m_simp->updt_params(p);
} }
void checkpoint() { void checkpoint() {
@ -622,6 +623,7 @@ void ctx_simplify_tactic::get_param_descrs(param_descrs & r) {
insert_max_memory(r); insert_max_memory(r);
insert_max_steps(r); insert_max_steps(r);
r.insert("max_depth", CPK_UINT, "(default: 1024) maximum term depth."); r.insert("max_depth", CPK_UINT, "(default: 1024) maximum term depth.");
r.insert("propagate_eq", CPK_BOOL, "(default: false) enable equality propagation from bounds.");
} }
void ctx_simplify_tactic::operator()(goal_ref const & in, void ctx_simplify_tactic::operator()(goal_ref const & in,

1
src/tactic/core/ctx_simplify_tactic.h
View file

@ -34,6 +34,7 @@ public:
virtual void pop(unsigned num_scopes) = 0; virtual void pop(unsigned num_scopes) = 0;
virtual simplifier * translate(ast_manager & m) = 0; virtual simplifier * translate(ast_manager & m) = 0;
virtual unsigned scope_level() const = 0; virtual unsigned scope_level() const = 0;
virtual void updt_params(params_ref const & p) {}
void set_occs(goal_num_occurs& occs) { m_occs = &occs; }; void set_occs(goal_num_occurs& occs) { m_occs = &occs; };
bool shared(expr* t) const; bool shared(expr* t) const;
}; };