From a143ed3bff01bccecde97b52c178381057478f6f Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 18 Feb 2025 16:28:49 -0800
Subject: [PATCH] taking a look at mbp_qel for arrays
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/ast/array_decl_plugin.h | 12 ++++++++++++
src/ast/ast.h | 17 +++++++++++++++--
src/qe/mbp/mbp_qel.cpp | 27 +++++++++++++--------------
src/qe/mbp/mbp_qel_util.cpp | 24 +++++++++++++-----------
4 files changed, 53 insertions(+), 27 deletions(-)
diff --git a/src/ast/array_decl_plugin.h b/src/ast/array_decl_plugin.h
index 9a57476d4..b310b89c4 100644
--- a/src/ast/array_decl_plugin.h
+++ b/src/ast/array_decl_plugin.h
@@ -33,6 +33,18 @@ inline sort* get_array_domain(sort const * s, unsigned idx) {
return to_sort(s->get_parameter(idx).get_ast());
}
+inline expr_container array_select_indices(app* e) {
+ return expr_container(e->get_args() + 1, e->get_args() + e->get_num_args());
+}
+
+inline expr_container array_store_indices(app* e) {
+ return expr_container(e->get_args() + 1, e->get_args() + e->get_num_args() - 1);
+}
+
+inline expr* array_store_elem(app* e) {
+ return e->get_arg(e->get_num_args() - 1);
+}
+
enum array_sort_kind {
ARRAY_SORT,
_SET_SORT
diff --git a/src/ast/ast.h b/src/ast/ast.h
index 039be4130..88c45668a 100644
--- a/src/ast/ast.h
+++ b/src/ast/ast.h
@@ -690,8 +690,21 @@ public:
sort* get_sort() const;
- unsigned get_small_id() const { return get_id(); }
-
+ unsigned get_small_id() const { return get_id(); }
+};
+
+class expr_container {
+ expr* const* m_pos;
+ expr* const* m_end;
+public:
+ expr_container(expr* const* pos, expr* const* end) :m_pos(pos), m_end(end) {}
+ expr_container& operator++() { ++m_pos; return *this; }
+ expr_container operator++(int) { expr_container tmp = *this; ++(*this); return tmp; }
+ bool operator==(expr_container const& it) const { return m_pos == it.m_pos; }
+ bool operator!=(expr_container const& it) const { return m_pos != it.m_pos; }
+ expr* operator*() const { return *m_pos; }
+ expr* const* begin() const { return m_pos; }
+ expr* const* end() const { return m_end; }
};
// -----------------------------------
diff --git a/src/qe/mbp/mbp_qel.cpp b/src/qe/mbp/mbp_qel.cpp
index 5778419c1..33fd6cc04 100644
--- a/src/qe/mbp/mbp_qel.cpp
+++ b/src/qe/mbp/mbp_qel.cpp
@@ -126,6 +126,9 @@ public:
init(vars, fml, mdl);
// Apply MBP rules till saturation
+ TRACE("mbp_tg",
+ tout << "mbp tg " << m_tg.get_lits() << "\nand vars " << vars << "\n";);
+
// First, apply rules without splitting on model
saturate(vars);
@@ -135,18 +138,15 @@ public:
saturate(vars);
TRACE("mbp_tg",
- tout << "mbp tg " << m_tg.get_lits() << " and vars " << vars;);
+ tout << "mbp tg " << m_tg.get_lits() << " and vars " << vars << "\n";);
TRACE("mbp_tg_verbose", obj_hashtable<app> vars_tmp;
collect_uninterp_consts(mk_and(m_tg.get_lits()), vars_tmp);
- for (auto a
- : vars_tmp) tout
- << mk_pp(a->get_decl(), m) << "\n";
- for (auto b
- : m_tg.get_lits()) tout
- << expr_ref(b, m) << "\n";
- for (auto a
- : vars) tout
- << expr_ref(a, m) << " ";);
+ for (auto a : vars_tmp)
+ tout << mk_pp(a->get_decl(), m) << "\n";
+ for (auto b : m_tg.get_lits())
+ tout << expr_ref(b, m) << "\n";
+ for (auto a : vars) tout << expr_ref(a, m) << " ";
+ tout << "\n");
// 1. Apply qe_lite to remove all c-ground variables
// 2. Collect all core variables in the output (variables used as array
@@ -171,11 +171,10 @@ public:
};
expr_sparse_mark red_vars;
for (auto v : vars)
- if (is_red(v)) red_vars.mark(v);
+ if (is_red(v))
+ red_vars.mark(v);
CTRACE("mbp_tg", !core_vars.empty(), tout << "vars not redundant ";
- for (auto v
- : core_vars) tout
- << " " << app_ref(v, m);
+ for (auto v : core_vars) tout << " " << app_ref(v, m);
tout << "\n";);
std::function<bool(expr *)> non_core = [&](expr *e) {
diff --git a/src/qe/mbp/mbp_qel_util.cpp b/src/qe/mbp/mbp_qel_util.cpp
index e6537a1d0..f50444656 100644
--- a/src/qe/mbp/mbp_qel_util.cpp
+++ b/src/qe/mbp/mbp_qel_util.cpp
@@ -80,23 +80,25 @@ struct proc {
obj_hashtable<app> &m_vars;
array_util m_array_util;
datatype_util m_dt_util;
+ bool is_accessor(expr* e) const {
+ return is_app(e) && m_dt_util.is_accessor(to_app(e)->get_decl());
+ }
proc(obj_hashtable<app> &vars, ast_manager &man)
: m(man), m_vars(vars), m_array_util(m), m_dt_util(m) {}
void operator()(expr *n) const {}
void operator()(app *n) {
if (m_array_util.is_select(n)) {
- expr *idx = n->get_arg(1);
- if (is_app(idx) && m_dt_util.is_accessor(to_app(idx)->get_decl()))
- return;
- collect_uninterp_consts(idx, m_vars);
- } else if (m_array_util.is_store(n)) {
- expr *idx = n->get_arg(1), *elem = n->get_arg(2);
- if (!(is_app(idx) &&
- m_dt_util.is_accessor(to_app(idx)->get_decl())))
- collect_uninterp_consts(idx, m_vars);
- if (!(is_app(elem) &&
- m_dt_util.is_accessor(to_app(elem)->get_decl())))
+ for (expr* arg : array_select_indices(n))
+ if (!is_accessor(arg))
+ collect_uninterp_consts(arg, m_vars);
+ }
+ else if (m_array_util.is_store(n)) {
+ expr* elem = array_store_elem(n);
+ if (!is_accessor(elem))
collect_uninterp_consts(elem, m_vars);
+ for (expr* idx : array_store_indices(n))
+ if (!is_accessor(idx))
+ collect_uninterp_consts(idx, m_vars);
}
}
};