From 9ea921ba8ea38941c7675dffd62cf6b1c232367c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 11 Feb 2025 17:38:56 -0800 Subject: [PATCH] update spacer projection for arrays to allow ackerman reduction for non-integer arrays Signed-off-by: Nikolaj Bjorner --- src/muz/spacer/spacer_qe_project.cpp | 28 ++++++++++++++++++---------- 1 file changed, 18 insertions(+), 10 deletions(-) diff --git a/src/muz/spacer/spacer_qe_project.cpp b/src/muz/spacer/spacer_qe_project.cpp index e52e909ae..de14de5af 100644 --- a/src/muz/spacer/spacer_qe_project.cpp +++ b/src/muz/spacer/spacer_qe_project.cpp @@ -2070,7 +2070,8 @@ namespace spacer_qe { * update sub with val consts for sel terms */ void ackermann (ptr_vector const& sel_terms) { - if (sel_terms.empty ()) return; + if (sel_terms.empty ()) + return; expr* v = sel_terms.get (0)->get_arg (0); // array variable sort* v_sort = v->get_sort (); @@ -2118,10 +2119,19 @@ namespace spacer_qe { // sort reprs by their value and add a chain of strict inequalities unsigned num_reprs = m_idx_reprs.size () - start; - if (num_reprs == 0) return; + if (num_reprs == 0) + return; + + if (!m_ari_u.is_real(idx_sort) && !m_ari_u.is_int(idx_sort)) { + expr_ref_vector args(m); + for (unsigned i = start; i < m_idx_reprs.size(); ++i) + args.push_back(m_idx_reprs.get(i)); + for (unsigned i = 0; i < args.size(); ++i) + for (unsigned j = i + 1; j < args.size(); ++j) + m_idx_lits.push_back(m.mk_not(m.mk_eq(args.get(i), args.get(j)))); + return; + } - SASSERT ((m_ari_u.is_real (idx_sort) || m_ari_u.is_int (idx_sort)) - && "Unsupported index sort: neither real nor int"); // using insertion sort unsigned end = start + num_reprs; @@ -2173,13 +2183,11 @@ namespace spacer_qe { collect_selects (fml); // model based ackermannization - sel_map::iterator begin = m_sel_terms.begin (), - end = m_sel_terms.end (); - for (sel_map::iterator it = begin; it != end; it++) { + for (auto const& [key, value] : m_sel_terms) { TRACE ("qe", - tout << "ackermann for var: " << mk_pp (it->m_key, m) << "\n"; - ); - ackermann (*(it->m_value)); + tout << "ackermann for var: " << mk_pp (key, m) << "\n"; + ); + ackermann (*value); } TRACE ("qe",