mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 08:28:44 +00:00
Code Activity

bugfixes

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-12-28 21:02:09 -08:00
parent 15f36f95a4
commit 97225b7d8f
2 changed files with 23 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

22
src/sat/smt/polysat_internalize.cpp
View file

@ -311,6 +311,8 @@ namespace polysat {
axiomatize_int2bv(e, n, x); axiomatize_int2bv(e, n, x);
else if (bv.is_extract(e)) else if (bv.is_extract(e))
axioms_for_extract(e); axioms_for_extract(e);
else if (bv.is_concat(e))
axioms_for_concat(e);
else else
UNREACHABLE(); UNREACHABLE();
} }
@ -638,8 +640,28 @@ namespace polysat {
add_axiom(name, { ~eq0, ~gelo }); add_axiom(name, { ~eq0, ~gelo });
} }
// e = hi lo
// hi = 0 <=> e < 2^|lo|
void solver::axioms_for_concat(app* e) {
if (bv.is_concat(e) && e->get_num_args() == 2) {
expr* hi = e->get_arg(0);
expr* lo = e->get_arg(1);
auto sz_e = bv.get_bv_size(e);
auto sz_l = bv.get_bv_size(lo);
auto sz_h = bv.get_bv_size(hi);
auto name = "concat";
auto eq0 = eq_internalize(hi, bv.mk_numeral(0, sz_h));
auto gtlo = ~mk_literal(bv.mk_ule(bv.mk_numeral(rational::power_of_two(sz_l), sz_e), e));
equiv_axiom(name, eq0, gtlo);
}
else
NOT_IMPLEMENTED_YET();
}
void solver::internalize_concat(app* e) { void solver::internalize_concat(app* e) {
SASSERT(bv.is_concat(e)); SASSERT(bv.is_concat(e));
m_delayed_axioms.push_back(e);
ctx.push(push_back_vector(m_delayed_axioms));
var2pdd(expr2enode(e)->get_th_var(get_id())); var2pdd(expr2enode(e)->get_th_var(get_id()));
} }

1
src/sat/smt/polysat_solver.h
View file

@ -155,6 +155,7 @@ namespace polysat {
void axiomatize_int2bv(app* e, unsigned sz, expr* x); void axiomatize_int2bv(app* e, unsigned sz, expr* x);
void axiomatize_bv2int(app* e, expr* x); void axiomatize_bv2int(app* e, expr* x);
void axioms_for_extract(app* e); void axioms_for_extract(app* e);
void axioms_for_concat(app* e);
expr* rotate_left(app* e, unsigned n, expr* x); expr* rotate_left(app* e, unsigned n, expr* x);
unsigned m_delayed_axioms_qhead = 0; unsigned m_delayed_axioms_qhead = 0;
ptr_vector<app> m_delayed_axioms; ptr_vector<app> m_delayed_axioms;