From 47cbc746b5060df2a789ea36582c75df9aa4b023 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 18 Mar 2026 13:24:10 -1000 Subject: [PATCH] fix #9036: expand bounded integer quantifiers in qe-light After qe-light's equation solver (eq_der) eliminates variables from linear equations, remaining bounded integer quantifiers may still have non-unit coefficients that prevent Fourier-Motzkin elimination. Add a bounded quantifier expansion step: when the remaining quantified integer variables all have explicit finite bounds and the product of domain sizes is <= 10000, expand the quantifier into a finite disjunction. This turns e.g. exists y0 in [0,10), y1 in [0,15): P(x,y0,y1) into P(x,0,0) | P(x,0,1) | ... | P(x,9,14), which is 150 disjuncts. The SMT solver handles the resulting quantifier-free formula instantly, whereas the previous QSAT/MBP approach timed out due to weak integer projections from the (|a|-1)*(|b|-1) slack in Fourier-Motzkin resolution with non-unit coefficients. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- src/qe/lite/qe_lite_tactic.cpp | 300 +++++++++++++++++++++++++++++++++ 1 file changed, 300 insertions(+) diff --git a/src/qe/lite/qe_lite_tactic.cpp b/src/qe/lite/qe_lite_tactic.cpp index 9a4ba46bc..440d1a043 100644 --- a/src/qe/lite/qe_lite_tactic.cpp +++ b/src/qe/lite/qe_lite_tactic.cpp @@ -2236,6 +2236,21 @@ class qe_lite::impl { if (q->get_kind() != lambda_k) { m_imp(indices, true, result); } + // After eq_der + FM, try to expand remaining bounded + // integer quantifiers into finite disjunctions. + // If expansion succeeds, the result is quantifier-free + // so we return it directly without re-wrapping. + if (is_exists(q) || is_forall(q)) { + expr_ref expanded(m); + if (m_imp.try_expand_bounded_quantifier(q, result, expanded)) { + if (is_forall(q)) + expanded = push_not(expanded); + m_imp.m_rewriter(expanded, result, result_pr); + if (m.proofs_enabled()) + result_pr = m.mk_rewrite(q, result); + return true; + } + } if (is_forall(q)) { result = push_not(result); } @@ -2271,6 +2286,8 @@ private: th_rewriter m_rewriter; bool m_use_array_der; + static const unsigned EXPAND_BOUND_LIMIT = 10000; + bool has_unique_non_ground(expr_ref_vector const& fmls, unsigned& index) { index = fmls.size(); if (index <= 1) { @@ -2287,6 +2304,289 @@ private: return index < fmls.size(); } + // Try to extract a tight integer bound from a conjunct for de Bruijn variable idx. + // Returns true if the conjunct is a bound for var(idx). + // Sets is_lower=true for lower bounds, is_lower=false for upper bounds. + // Sets bound_val to the bound value, inclusive. + bool extract_var_bound(expr* e, unsigned idx, unsigned num_decls, arith_util& a_util, + bool& is_lower, rational& bound_val) { + expr *atom, *lhs, *rhs; + rational val; + bool is_neg = m.is_not(e, atom); + if (is_neg) + e = atom; + + if (a_util.is_le(e, lhs, rhs)) { + // lhs <= rhs + if (is_var(lhs) && to_var(lhs)->get_idx() == idx && a_util.is_numeral(rhs, val)) { + // var(idx) <= val, possibly negated + if (!is_neg) { + is_lower = false; + bound_val = val; + return true; + } + // Not(var(idx) <= val) => var(idx) >= val + 1 + is_lower = true; + bound_val = val + 1; + return true; + } + if (is_var(rhs) && to_var(rhs)->get_idx() == idx && a_util.is_numeral(lhs, val)) { + // val <= var(idx), possibly negated + if (!is_neg) { + is_lower = true; + bound_val = val; + return true; + } + // Not(val <= var(idx)) => var(idx) <= val - 1 + is_lower = false; + bound_val = val - 1; + return true; + } + } + + if (a_util.is_ge(e, lhs, rhs)) { + // lhs >= rhs, i.e., rhs <= lhs + if (is_var(lhs) && to_var(lhs)->get_idx() == idx && a_util.is_numeral(rhs, val)) { + // var(idx) >= val, possibly negated + if (!is_neg) { + is_lower = true; + bound_val = val; + return true; + } + // Not(var(idx) >= val) => var(idx) <= val - 1 + is_lower = false; + bound_val = val - 1; + return true; + } + if (is_var(rhs) && to_var(rhs)->get_idx() == idx && a_util.is_numeral(lhs, val)) { + // val >= var(idx) => var(idx) <= val, possibly negated + if (!is_neg) { + is_lower = false; + bound_val = val; + return true; + } + // Not(val >= var(idx)) => var(idx) >= val + 1 + is_lower = true; + bound_val = val + 1; + return true; + } + } + + if (a_util.is_lt(e, lhs, rhs)) { + // lhs < rhs + if (is_var(lhs) && to_var(lhs)->get_idx() == idx && a_util.is_numeral(rhs, val)) { + if (!is_neg) { + // var(idx) < val => var(idx) <= val - 1 + is_lower = false; + bound_val = val - 1; + return true; + } + // Not(var(idx) < val) => var(idx) >= val + is_lower = true; + bound_val = val; + return true; + } + if (is_var(rhs) && to_var(rhs)->get_idx() == idx && a_util.is_numeral(lhs, val)) { + if (!is_neg) { + // val < var(idx) => var(idx) >= val + 1 + is_lower = true; + bound_val = val + 1; + return true; + } + // Not(val < var(idx)) => var(idx) <= val + is_lower = false; + bound_val = val; + return true; + } + } + + if (a_util.is_gt(e, lhs, rhs)) { + // lhs > rhs + if (is_var(lhs) && to_var(lhs)->get_idx() == idx && a_util.is_numeral(rhs, val)) { + if (!is_neg) { + // var(idx) > val => var(idx) >= val + 1 + is_lower = true; + bound_val = val + 1; + return true; + } + // Not(var(idx) > val) => var(idx) <= val + is_lower = false; + bound_val = val; + return true; + } + if (is_var(rhs) && to_var(rhs)->get_idx() == idx && a_util.is_numeral(lhs, val)) { + if (!is_neg) { + // val > var(idx) => var(idx) <= val - 1 + is_lower = false; + bound_val = val - 1; + return true; + } + // Not(val > var(idx)) => var(idx) >= val + is_lower = true; + bound_val = val; + return true; + } + } + + return false; + } + + // Try to expand a bounded existential quantifier into a finite disjunction. + // The body has been processed by eq_der + FM already. + // Works at the de Bruijn variable level. + // Returns true if expansion succeeded. + bool try_expand_bounded_quantifier(quantifier* q, expr* body, expr_ref& result) { + unsigned num_decls = q->get_num_decls(); + if (num_decls == 0) + return false; + + arith_util a_util(m); + + // Check which variables still appear in the body + used_vars uv; + uv(body); + unsigned remaining = 0; + for (unsigned i = 0; i < num_decls; ++i) + if (uv.contains(i)) + remaining++; + if (remaining == 0) + return false; + + // Only handle integer variables + for (unsigned i = 0; i < num_decls; ++i) { + if (!uv.contains(i)) + continue; + if (!a_util.is_int(q->get_decl_sort(i))) + return false; + } + + // Flatten body into conjuncts + expr_ref_vector conjs(m); + flatten_and(body, conjs); + + // Extract bounds for each remaining variable + vector lbs, ubs; + bool_vector has_lb, has_ub; + lbs.resize(num_decls); + ubs.resize(num_decls); + has_lb.resize(num_decls, false); + has_ub.resize(num_decls, false); + + // Track which conjuncts are pure bounds, to separate from the payload + bool_vector is_bound_conj; + is_bound_conj.resize(conjs.size(), false); + + for (unsigned ci = 0; ci < conjs.size(); ++ci) { + for (unsigned vi = 0; vi < num_decls; ++vi) { + if (!uv.contains(vi)) + continue; + bool is_lower; + rational bval; + if (extract_var_bound(conjs[ci].get(), vi, num_decls, a_util, is_lower, bval)) { + if (is_lower) { + if (!has_lb[vi] || bval > lbs[vi]) + lbs[vi] = bval; + has_lb[vi] = true; + } + else { + if (!has_ub[vi] || bval < ubs[vi]) + ubs[vi] = bval; + has_ub[vi] = true; + } + is_bound_conj[ci] = true; + } + } + } + + // Check all remaining variables are bounded + rational domain_product(1); + for (unsigned i = 0; i < num_decls; ++i) { + if (!uv.contains(i)) + continue; + if (!has_lb[i] || !has_ub[i]) + return false; + rational size = ubs[i] - lbs[i] + 1; + if (size <= rational(0)) { + result = m.mk_false(); + return true; + } + domain_product *= size; + if (domain_product > rational(EXPAND_BOUND_LIMIT)) + return false; + } + + IF_VERBOSE(2, verbose_stream() << "(qe-lite :expand-bounded-quantifier" + << " :vars " << remaining + << " :domain-size " << domain_product << ")\n"); + + // Collect the non-bound conjuncts as the payload + expr_ref_vector payload(m); + for (unsigned ci = 0; ci < conjs.size(); ++ci) + if (!is_bound_conj[ci]) + payload.push_back(conjs[ci].get()); + + // Collect the remaining variables in order, with their bounds + unsigned_vector var_indices; + vector var_lbs, var_ubs; + for (unsigned i = 0; i < num_decls; ++i) { + if (!uv.contains(i)) continue; + var_indices.push_back(i); + var_lbs.push_back(lbs[i]); + var_ubs.push_back(ubs[i]); + } + + // Build substitution array: one entry per de Bruijn variable + expr_ref_vector subst_map(m); + subst_map.resize(num_decls); + // Initialize non-remaining variables to themselves + for (unsigned i = 0; i < num_decls; ++i) + if (!uv.contains(i)) + subst_map.set(i, m.mk_var(i, q->get_decl_sort(i))); + + // Enumerate all value combinations + unsigned nv = var_indices.size(); + vector cur_vals; + cur_vals.resize(nv); + for (unsigned i = 0; i < nv; ++i) + cur_vals[i] = var_lbs[i]; + + var_subst vs(m, false); + expr_ref_vector disjuncts(m); + + while (true) { + // Set up substitution for current values + for (unsigned i = 0; i < nv; ++i) + subst_map.set(var_indices[i], a_util.mk_int(cur_vals[i])); + + // Substitute in each payload conjunct and combine + expr_ref_vector inst_conjs(m); + for (expr* p : payload) { + expr_ref inst(m); + inst = vs(p, subst_map.size(), subst_map.data()); + inst_conjs.push_back(inst); + } + expr_ref inst_body(m); + bool_rewriter(m).mk_and(inst_conjs.size(), inst_conjs.data(), inst_body); + disjuncts.push_back(inst_body); + + // Increment to next value combination, rightmost first + unsigned carry = nv; + for (unsigned i = nv; i-- > 0; ) { + cur_vals[i] += 1; + if (cur_vals[i] <= var_ubs[i]) { + carry = i; + break; + } + cur_vals[i] = var_lbs[i]; + } + if (carry == nv) + break; + } + + bool_rewriter(m).mk_or(disjuncts.size(), disjuncts.data(), result); + return true; + } + public: impl(ast_manager & m, params_ref const & p, bool use_array_der): m(m),