mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Code Activity

Expand equality literals when eq_prop is disabled

Browse source 
When equality propagation is disabled for arithmetic,
equality atoms are expanded into inequality for potentially
better generalization with interpolation
This commit is contained in:
Arie Gurfinkel 2018-08-01 11:11:18 +02:00
parent e8a78ec696
commit 533e9c5837
2 changed files with 13 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/muz/spacer/spacer_context.cpp
View file

@ -1344,6 +1344,14 @@ lbool pred_transformer::is_reachable(pob& n, expr_ref_vector* core,
expr_ref_vector post (m), reach_assumps (m);
post.push_back (n.post ());
flatten_and(post);
// if equality propagation is disabled in arithmetic, expand
// equality literals into two inequalities to increase the space
// for interpolation
if (!ctx.use_eq_prop()) {
expand_literals(m, post);
}
// populate reach_assumps
if (n.level () > 0 && !m_all_init) {

9
src/muz/spacer/spacer_context.h
View file

@ -1027,11 +1027,12 @@ public:
const fp_params &get_params() const { return m_params; }
bool use_native_mbp () {return m_use_native_mbp;}
bool use_ground_pob () {return m_ground_pob;}
bool use_instantiate () {return m_instantiate;}
bool use_eq_prop() {return m_use_eq_prop;}
bool use_native_mbp() {return m_use_native_mbp;}
bool use_ground_pob() {return m_ground_pob;}
bool use_instantiate() {return m_instantiate;}
bool weak_abs() {return m_weak_abs;}
bool use_qlemmas () {return m_use_qlemmas;}
bool use_qlemmas() {return m_use_qlemmas;}
bool use_euf_gen() {return m_use_euf_gen;}
bool simplify_pob() {return m_simplify_pob;}
bool use_ctp() {return m_use_ctp;}