From 11cd2c081eafe6c5822e1f1991b64fb738cf67ea Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Tue, 21 Apr 2026 20:02:20 +0000 Subject: [PATCH 1/3] Initial plan From 1fb59201cd99022b71f37ed7635b56e8a8abf99e Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Tue, 21 Apr 2026 20:33:15 +0000 Subject: [PATCH 2/3] qe-lite: case-split BV vars constrained by constant equalities Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/53219443-a721-4e6d-a7c3-21a6387b3396 Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/qe/lite/qe_lite_tactic.cpp | 140 ++++++++++++++++++++++++++++++++- src/test/qe_arith.cpp | 54 +++++++++++++ 2 files changed, 193 insertions(+), 1 deletion(-) diff --git a/src/qe/lite/qe_lite_tactic.cpp b/src/qe/lite/qe_lite_tactic.cpp index 4f234a58e..5aea40a7e 100644 --- a/src/qe/lite/qe_lite_tactic.cpp +++ b/src/qe/lite/qe_lite_tactic.cpp @@ -2242,7 +2242,8 @@ class qe_lite::impl { // 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 (m_imp.try_expand_bounded_quantifier(q, result, expanded) || + m_imp.try_expand_bv_eq_quantifier(q, result, expanded)) { if (is_forall(q)) expanded = push_not(expanded); m_imp.m_rewriter(expanded, result, result_pr); @@ -2287,6 +2288,8 @@ private: bool m_use_array_der; static const unsigned EXPAND_BOUND_LIMIT = 10000; + static const unsigned BV_EQ_CASE_SPLIT_LIMIT = 256; + static const unsigned BV_EQ_CASES_PER_VAR_LIMIT = 8; bool has_unique_non_ground(expr_ref_vector const& fmls, unsigned& index) { index = fmls.size(); @@ -2503,6 +2506,141 @@ private: return true; } + bool collect_bv_eq_constants(expr* e, unsigned idx, obj_hashtable& values) { + ptr_buffer todo; + ast_mark visited; + todo.push_back(e); + while (!todo.empty()) { + expr* n = todo.back(); + todo.pop_back(); + if (visited.is_marked(n)) + continue; + visited.mark(n, true); + if (is_var(n)) { + if (to_var(n)->get_idx() == idx) + return false; + continue; + } + if (is_quantifier(n)) + return false; + if (!is_app(n)) + continue; + expr *lhs = nullptr, *rhs = nullptr; + if (m.is_eq(n, lhs, rhs)) { + bool lhs_is_var = is_var(lhs) && to_var(lhs)->get_idx() == idx; + bool rhs_is_var = is_var(rhs) && to_var(rhs)->get_idx() == idx; + if (lhs_is_var || rhs_is_var) { + if (lhs_is_var == rhs_is_var) + return false; + expr* c = lhs_is_var ? rhs : lhs; + if (!m.is_value(c)) + return false; + values.insert(c); + continue; + } + } + todo.append(to_app(n)->get_num_args(), to_app(n)->get_args()); + } + return true; + } + + bool mk_bv_default_case(unsigned bv_size, obj_hashtable const& values, expr_ref& value) { + bv_util bv(m); + uint64_t max_num = values.size() + 1; + if (bv_size < 63) + max_num = std::min(max_num, uint64_t(1) << bv_size); + for (uint64_t i = 0; i < max_num; ++i) { + value = bv.mk_numeral(rational(static_cast(i)), bv_size); + if (!values.contains(value)) + return true; + } + return false; + } + + bool try_expand_bv_eq_quantifier(quantifier* q, expr* body, expr_ref& result) { + unsigned num_decls = q->get_num_decls(); + if (num_decls == 0) + return false; + + used_vars uv; + uv(body); + + struct bv_var_cases { + unsigned idx; + expr_ref_vector values; + bv_var_cases(ast_manager& m, unsigned i): idx(i), values(m) {} + }; + + vector case_vars; + rational num_cases(1); + + for (unsigned i = 0; i < num_decls; ++i) { + if (!uv.contains(i)) + continue; + sort* s = uv.contains(i); + if (!s) + return false; + bv_util bv(m); + if (!bv.is_bv_sort(s)) + return false; + obj_hashtable values; + if (!collect_bv_eq_constants(body, i, values) || values.empty()) + return false; + if (values.size() > BV_EQ_CASES_PER_VAR_LIMIT) + return false; + case_vars.push_back(bv_var_cases(m, i)); + auto& var_cases = case_vars.back(); + for (expr* v : values) + var_cases.values.push_back(v); + expr_ref other(m); + if (mk_bv_default_case(bv.get_bv_size(s), values, other)) + var_cases.values.push_back(other); + if (var_cases.values.empty()) + return false; + num_cases *= rational(var_cases.values.size()); + if (num_cases > rational(BV_EQ_CASE_SPLIT_LIMIT)) + return false; + } + + if (case_vars.empty()) + return false; + + expr_ref_vector subst_map(m); + subst_map.resize(num_decls); + for (unsigned i = 0; i < num_decls; ++i) + if (!uv.contains(i)) + subst_map.set(i, m.mk_var(i, q->get_decl_sort(num_decls - i - 1))); + + unsigned_vector case_ix; + case_ix.resize(case_vars.size(), 0); + + var_subst vs(m, false); + expr_ref_vector disjuncts(m); + while (true) { + for (unsigned i = 0; i < case_vars.size(); ++i) { + auto& c = case_vars[i]; + subst_map.set(c.idx, c.values.get(case_ix[i])); + } + expr_ref inst(vs(body, subst_map.size(), subst_map.data()), m); + m_rewriter(inst); + disjuncts.push_back(inst); + + unsigned j = case_ix.size(); + while (j > 0) { + --j; + ++case_ix[j]; + if (case_ix[j] < case_vars[j].values.size()) + break; + case_ix[j] = 0; + } + if (j == 0 && case_ix[0] == 0) + 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), diff --git a/src/test/qe_arith.cpp b/src/test/qe_arith.cpp index af32b2c47..9cdfdf670 100644 --- a/src/test/qe_arith.cpp +++ b/src/test/qe_arith.cpp @@ -6,12 +6,14 @@ Copyright (c) 2015 Microsoft Corporation #include "qe/mbp/mbp_arith.h" #include "qe/qe.h" +#include "qe/lite/qe_lite_tactic.h" #include "ast/rewriter/th_rewriter.h" #include "parsers/smt2/smt2parser.h" #include "ast/arith_decl_plugin.h" #include "ast/reg_decl_plugins.h" #include "ast/rewriter/arith_rewriter.h" #include "ast/ast_pp.h" +#include "ast/for_each_expr.h" #include "smt/smt_context.h" #include "ast/expr_abstract.h" #include "ast/rewriter/expr_safe_replace.h" @@ -42,6 +44,57 @@ static expr_ref parse_fml(ast_manager& m, char const* str) { return result; } +static expr_ref parse_smt2_assertion(ast_manager& m, char const* script) { + expr_ref result(m); + cmd_context ctx(false, &m); + ctx.set_ignore_check(true); + std::istringstream is(script); + VERIFY(parse_smt2_commands(ctx, is)); + result = ctx.assertions().get(0); + return result; +} + +namespace qe_arith_test { + struct find_q_proc { + quantifier* m_q = nullptr; + void operator()(var*) {} + void operator()(app*) {} + void operator()(quantifier* q) { m_q = q; } + }; +} + +static quantifier* find_quantifier(expr* n) { + qe_arith_test::find_q_proc p; + for_each_expr(p, n); + return p.m_q; +} + +static void test_qe_lite_bv_eq_cases() { + ast_manager m; + reg_decl_plugins(m); + expr_ref fml = parse_smt2_assertion(m, R"( +(set-logic BV) +(declare-const cv1 (_ BitVec 1)) +(assert + (exists ((x (_ BitVec 48)) (y (_ BitVec 9))) + (and + (not (= y (_ bv511 9))) + (not (= x (_ bv1 48))) + (not (and (= x (_ bv1 48)) (= cv1 (_ bv1 1)))) + (not (and (= x (_ bv1 48)) (not (= cv1 (_ bv1 1)))))))) +)"); + expr_ref original(fml, m); + qe_lite qel(m, params_ref()); + proof_ref pr(m); + qel(fml, pr); + VERIFY(find_quantifier(fml) == nullptr); + + smt_params params; + smt::context ctx(m, params); + ctx.assert_expr(m.mk_not(m.mk_iff(original, fml))); + VERIFY(ctx.check() == l_false); +} + static char const* example1 = "(and (<= x 3.0) (<= (* 3.0 x) y) (<= z y))"; static char const* example2 = "(and (<= z x) (<= x 3.0) (<= (* 3.0 x) y) (<= z y))"; static char const* example3 = "(and (<= z x) (<= x 3.0) (< (* 3.0 x) y) (<= z y))"; @@ -594,6 +647,7 @@ static void test_project() { void tst_qe_arith() { test_project(); + test_qe_lite_bv_eq_cases(); return; check_random_ineqs(); return; From e503ead008ecd3d9a8ca4df612924493b450e40f Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Tue, 21 Apr 2026 20:37:53 +0000 Subject: [PATCH 3/3] Address review feedback for qe-lite BV case split changes Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/53219443-a721-4e6d-a7c3-21a6387b3396 Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/qe/lite/qe_lite_tactic.cpp | 30 +++++++++++++++--------------- src/test/qe_arith.cpp | 18 +----------------- 2 files changed, 16 insertions(+), 32 deletions(-) diff --git a/src/qe/lite/qe_lite_tactic.cpp b/src/qe/lite/qe_lite_tactic.cpp index 5aea40a7e..3321196c3 100644 --- a/src/qe/lite/qe_lite_tactic.cpp +++ b/src/qe/lite/qe_lite_tactic.cpp @@ -2546,11 +2546,11 @@ private: bool mk_bv_default_case(unsigned bv_size, obj_hashtable const& values, expr_ref& value) { bv_util bv(m); - uint64_t max_num = values.size() + 1; - if (bv_size < 63) - max_num = std::min(max_num, uint64_t(1) << bv_size); - for (uint64_t i = 0; i < max_num; ++i) { - value = bv.mk_numeral(rational(static_cast(i)), bv_size); + unsigned max_num = values.size() + 1; + if (bv_size < sizeof(unsigned) * 8) + max_num = std::min(max_num, (1u << bv_size)); + for (unsigned i = 0; i < max_num; ++i) { + value = bv.mk_numeral(rational(i), bv_size); if (!values.contains(value)) return true; } @@ -2577,11 +2577,9 @@ private: for (unsigned i = 0; i < num_decls; ++i) { if (!uv.contains(i)) continue; - sort* s = uv.contains(i); - if (!s) - return false; + sort* var_sort = q->get_decl_sort(num_decls - i - 1); bv_util bv(m); - if (!bv.is_bv_sort(s)) + if (!bv.is_bv_sort(var_sort)) return false; obj_hashtable values; if (!collect_bv_eq_constants(body, i, values) || values.empty()) @@ -2593,7 +2591,7 @@ private: for (expr* v : values) var_cases.values.push_back(v); expr_ref other(m); - if (mk_bv_default_case(bv.get_bv_size(s), values, other)) + if (mk_bv_default_case(bv.get_bv_size(var_sort), values, other)) var_cases.values.push_back(other); if (var_cases.values.empty()) return false; @@ -2625,15 +2623,17 @@ private: m_rewriter(inst); disjuncts.push_back(inst); - unsigned j = case_ix.size(); - while (j > 0) { - --j; + // Increment mixed-radix counter over case_ix; if all positions wrap, stop. + bool wrapped = true; + for (unsigned j = case_ix.size(); j-- > 0; ) { ++case_ix[j]; - if (case_ix[j] < case_vars[j].values.size()) + if (case_ix[j] < case_vars[j].values.size()) { + wrapped = false; break; + } case_ix[j] = 0; } - if (j == 0 && case_ix[0] == 0) + if (wrapped) break; } diff --git a/src/test/qe_arith.cpp b/src/test/qe_arith.cpp index 9cdfdf670..c944c0b25 100644 --- a/src/test/qe_arith.cpp +++ b/src/test/qe_arith.cpp @@ -13,7 +13,6 @@ Copyright (c) 2015 Microsoft Corporation #include "ast/reg_decl_plugins.h" #include "ast/rewriter/arith_rewriter.h" #include "ast/ast_pp.h" -#include "ast/for_each_expr.h" #include "smt/smt_context.h" #include "ast/expr_abstract.h" #include "ast/rewriter/expr_safe_replace.h" @@ -54,21 +53,6 @@ static expr_ref parse_smt2_assertion(ast_manager& m, char const* script) { return result; } -namespace qe_arith_test { - struct find_q_proc { - quantifier* m_q = nullptr; - void operator()(var*) {} - void operator()(app*) {} - void operator()(quantifier* q) { m_q = q; } - }; -} - -static quantifier* find_quantifier(expr* n) { - qe_arith_test::find_q_proc p; - for_each_expr(p, n); - return p.m_q; -} - static void test_qe_lite_bv_eq_cases() { ast_manager m; reg_decl_plugins(m); @@ -87,7 +71,7 @@ static void test_qe_lite_bv_eq_cases() { qe_lite qel(m, params_ref()); proof_ref pr(m); qel(fml, pr); - VERIFY(find_quantifier(fml) == nullptr); + VERIFY(!has_quantifiers(fml)); smt_params params; smt::context ctx(m, params);