mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-04 14:26:10 +00:00
Code Activity

Fix intblast ubv_to_int bug: add bv2int axioms for compound expressions

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-02-25 00:46:13 +00:00
parent 1b68ee5f30
commit 4860d57ae9
4 changed files with 44 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

20
src/sat/smt/intblast_solver.cpp
View file

@ -133,8 +133,26 @@ namespace intblast {
return true; return true;
} }
bool solver::add_bv2int_axioms() {
auto const& bv2int = m_translator.bv2int();
if (m_bv2int_qhead == bv2int.size())
return false;
ctx.push(value_trail(m_bv2int_qhead));
for (; m_bv2int_qhead < bv2int.size(); ++m_bv2int_qhead) {
app* e = bv2int[m_bv2int_qhead];
expr_ref r(m_translator.translated(e), m);
if (r.get() == e)
continue;
ctx.get_rewriter()(r);
auto lit = ctx.mk_literal(m.mk_eq(e, r));
ctx.mark_relevant(lit);
add_unit(lit);
}
return true;
}
bool solver::unit_propagate() { bool solver::unit_propagate() {
return add_bound_axioms() || add_predicate_axioms(); return add_bound_axioms() || add_predicate_axioms() || add_bv2int_axioms();
} }
lbool solver::check_axiom(sat::literal_vector const& lits) { lbool solver::check_axiom(sat::literal_vector const& lits) {

3
src/sat/smt/intblast_solver.h
View file

@ -82,13 +82,14 @@ namespace intblast {
bool add_bound_axioms(); bool add_bound_axioms();
bool add_predicate_axioms(); bool add_predicate_axioms();
bool add_bv2int_axioms();
euf::theory_var mk_var(euf::enode* n) override; euf::theory_var mk_var(euf::enode* n) override;
void add_value_plugin(euf::enode* n, model& mdl, expr_ref_vector& values); void add_value_plugin(euf::enode* n, model& mdl, expr_ref_vector& values);
void add_value_solver(euf::enode* n, model& mdl, expr_ref_vector& values); void add_value_solver(euf::enode* n, model& mdl, expr_ref_vector& values);
unsigned m_vars_qhead = 0, m_preds_qhead = 0; unsigned m_vars_qhead = 0, m_preds_qhead = 0, m_bv2int_qhead = 0;
public: public:

22
src/smt/theory_intblast.cpp
View file

@ -117,13 +117,33 @@ namespace smt {
return true; return true;
} }
bool theory_intblast::add_bv2int_axioms() {
auto const& bv2int = m_translator.bv2int();
if (m_bv2int_qhead == bv2int.size())
return false;
ctx.push_trail(value_trail(m_bv2int_qhead));
for (; m_bv2int_qhead < bv2int.size(); ++m_bv2int_qhead) {
app* e = bv2int[m_bv2int_qhead];
expr_ref r(m_translator.translated(e), m);
if (r.get() == e)
continue;
ctx.get_rewriter()(r);
auto eq = mk_eq(e, r, false);
ctx.mark_as_relevant(eq);
ctx.mk_th_axiom(m_id, 1, &eq);
}
return true;
}
bool theory_intblast::can_propagate() { bool theory_intblast::can_propagate() {
return m_preds_qhead < m_translator.preds().size() || m_vars_qhead < m_translator.vars().size(); return m_preds_qhead < m_translator.preds().size() || m_vars_qhead < m_translator.vars().size() ||
m_bv2int_qhead < m_translator.bv2int().size();
} }
void theory_intblast::propagate() { void theory_intblast::propagate() {
add_bound_axioms(); add_bound_axioms();
add_predicate_axioms(); add_predicate_axioms();
add_bv2int_axioms();
} }
bool theory_intblast::internalize_atom(app * atom, bool gate_ctx) { bool theory_intblast::internalize_atom(app * atom, bool gate_ctx) {

3
src/smt/theory_intblast.h
View file

@ -42,11 +42,12 @@ namespace smt {
bv2int_translator m_translator; bv2int_translator m_translator;
bv_util bv; bv_util bv;
arith_util a; arith_util a;
unsigned m_vars_qhead = 0, m_preds_qhead = 0; unsigned m_vars_qhead = 0, m_preds_qhead = 0, m_bv2int_qhead = 0;
bv_factory * m_factory = nullptr; bv_factory * m_factory = nullptr;
bool add_bound_axioms(); bool add_bound_axioms();
bool add_predicate_axioms(); bool add_predicate_axioms();
bool add_bv2int_axioms();
public: public:
theory_intblast(context& ctx); theory_intblast(context& ctx);