mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-16 15:15:35 +00:00
Code Activity

Address review feedback for qe-lite BV case split changes

Browse source 
Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/53219443-a721-4e6d-a7c3-21a6387b3396

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-04-21 20:37:53 +00:00 • committed by GitHub
parent 1fb59201cd
commit e503ead008
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 16 additions and 32 deletions
Download patch file Download diff file Expand all files Collapse all files

30
src/qe/lite/qe_lite_tactic.cpp
View file

@ -2546,11 +2546,11 @@ private:
bool mk_bv_default_case(unsigned bv_size, obj_hashtable<expr> const& values, expr_ref& value) {
bv_util bv(m);
uint64_t max_num = values.size() + 1;
if (bv_size < 63)
max_num = std::min<uint64_t>(max_num, uint64_t(1) << bv_size);
for (uint64_t i = 0; i < max_num; ++i) {
value = bv.mk_numeral(rational(static_cast<unsigned>(i)), bv_size);
unsigned max_num = values.size() + 1;
if (bv_size < sizeof(unsigned) * 8)
max_num = std::min<unsigned>(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<expr> 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;
}

18
src/test/qe_arith.cpp
View file

@ -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);