mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 03:32:28 +00:00
Code Activity

bugbash

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-01-12 15:09:19 -08:00
parent 22103c0322
commit aefbfc6ca4
3 changed files with 30 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/sat/smt/polysat/fixed_bits.cpp
View file

@ -41,8 +41,8 @@ namespace polysat {
SASSERT(s.offset + s.length <= sz);
rational hi_val = s.value;
rational lo_val = mod(s.value + 1, sbw);
pdd lo = c.value(rational::power_of_two(sz - s.offset - s.length) * lo_val, sz);
pdd hi = c.value(rational::power_of_two(sz - s.offset - s.length) * hi_val, sz);
pdd lo = c.value(rational::power_of_two(sz - s.length) * lo_val, sz);
pdd hi = c.value(rational::power_of_two(sz - s.length) * hi_val, sz);
fi.reset();
fi.interval = eval_interval::proper(lo, lo_val, hi, hi_val);
fi.deps.push_back(dependency({ m_var, s }));
@ -54,6 +54,7 @@ namespace polysat {
// slice, properly contains variable.
// s.offset refers to offset in containing value.
if (s.length > sz && mod(machine_div2k(s.value, s.offset), bw) != val) {
rational hi_val = mod(machine_div2k(s.value, s.offset), bw);
rational lo_val = mod(hi_val + 1, bw);
pdd lo = c.value(lo_val, sz);

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

@ -655,6 +655,7 @@ namespace polysat {
}
void solver::internalize_extract(app* e) {
ensure_pdd_var(e->get_arg(0));
m_delayed_axioms.push_back(e);
ctx.push(push_back_vector(m_delayed_axioms));
var2pdd(expr2enode(e)->get_th_var(get_id()));
@ -696,8 +697,33 @@ namespace polysat {
}
}
void solver::ensure_pdd_var(expr* e) {
auto n = expr2enode(e);
auto v = n->get_th_var(get_id());
auto q = var2pdd(v);
if (q.is_val() || q.is_var())
return;
unsigned bv_size = get_bv_size(v);
pvar pv = m_core.add_var(bv_size);
pdd p = m_core.var(pv);
ctx.push(vector_value_trail(m_var2pdd, v));
m_pddvar2var.setx(pv, v, UINT_MAX);
m_var2pdd[v] = p;
auto sc = m_core.eq(p, q);
dependency d = dependency::axiom();
auto idx = m_core.register_constraint(sc, d);
TRACE("bv", tout << "add definition for " << mk_pp(e, m) << " " << p << ": " << sc << "\n";);
m_core.assign_eh(idx, false);
}
//
// subterms under concatentation and extract need to be variables or constants such that
// viable can perform proper slices.
//
void solver::internalize_concat(app* e) {
SASSERT(bv.is_concat(e));
for (auto arg : *e)
ensure_pdd_var(arg);
m_delayed_axioms.push_back(e);
ctx.push(push_back_vector(m_delayed_axioms));
var2pdd(expr2enode(e)->get_th_var(get_id()));

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

@ -195,6 +195,7 @@ namespace polysat {
void assert_bv2int_axiom(app * n);
void assert_int2bv_axiom(app* n);
void ensure_pdd_var(expr* e);
pdd expr2pdd(expr* e);
pdd var2pdd(euf::theory_var v);
void internalize_set(expr* e, pdd const& p);