mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-30 07:53:15 +00:00
Code Activity

dep

Browse source
This commit is contained in:
Jakob Rath 2024-03-19 14:23:44 +01:00
parent adc5313916
commit 489a1495d2
1 changed files with 3 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/sat/smt/polysat_egraph.cpp
View file

@ -138,11 +138,12 @@ namespace polysat {
rational value; rational value;
VERIFY(bv.is_numeral(r->get_expr(), value)); VERIFY(bv.is_numeral(r->get_expr(), value));
unsigned level = merge_level(n, r); unsigned level = merge_level(n, r); // TODO: WRONG -- n is not actually guaranteed to be the subslice of pv
euf::theory_var u = n->get_th_var(get_id()); euf::theory_var u = n->get_th_var(get_id());
// dependency dep = (u == euf::null_theory_var || u == w) ? dependency::axiom() : dependency(u, w); // TODO: probably need an enode_pair instead? // dependency dep = (u == euf::null_theory_var || u == w) ? dependency::axiom() : dependency(u, w); // TODO: probably need an enode_pair instead?
dependency dep = dependency(n, r); // dependency dep = dependency(n, r);
dependency dep = fixed_claim(pv, null_var, value, offset, length);
#if GET_FIXED_SUB_SLICES_DISPLAY #if GET_FIXED_SUB_SLICES_DISPLAY
verbose_stream() << " " << value << "[" << length << "]@" << offset; verbose_stream() << " " << value << "[" << length << "]@" << offset;