From 533e9c5837f927359291e48c6684e1c6bf3836c8 Mon Sep 17 00:00:00 2001
From: Arie Gurfinkel <arie.gurfinkel@uwaterloo.ca>
Date: Wed, 1 Aug 2018 11:11:18 +0200
Subject: [PATCH] Expand equality literals when eq_prop is disabled
When equality propagation is disabled for arithmetic,
equality atoms are expanded into inequality for potentially
better generalization with interpolation
---
src/muz/spacer/spacer_context.cpp | 8 ++++++++
src/muz/spacer/spacer_context.h | 9 +++++----
2 files changed, 13 insertions(+), 4 deletions(-)
diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp
index f0e86f1a5..c4e606b77 100644
--- a/src/muz/spacer/spacer_context.cpp
+++ b/src/muz/spacer/spacer_context.cpp
@@ -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) {
diff --git a/src/muz/spacer/spacer_context.h b/src/muz/spacer/spacer_context.h
index 48c27f96d..976259b6d 100644
--- a/src/muz/spacer/spacer_context.h
+++ b/src/muz/spacer/spacer_context.h
@@ -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;}