mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-02 09:20:22 +00:00
Code Activity

fix splitting in merge

Browse source
This commit is contained in:
Jakob Rath 2023-08-18 17:03:49 +02:00
parent 8a8afcdcb8
commit 1316e1c881
1 changed files with 6 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/math/polysat/slicing.cpp
View file

@ -445,6 +445,7 @@ namespace polysat {
// a base slice is never equivalent to a congruence node. // a base slice is never equivalent to a congruence node.
SASSERT(is_slice(s)); SASSERT(is_slice(s));
SASSERT(!has_sub(s)); SASSERT(!has_sub(s));
SASSERT(cut != null_cut);
// split all slices in the equivalence class // split all slices in the equivalence class
for (enode* n : euf::enode_class(s)) for (enode* n : euf::enode_class(s))
split_core(n, cut); split_core(n, cut);
@ -523,6 +524,7 @@ namespace polysat {
} }
slicing::enode* slicing::mk_value_slice(rational const& val, unsigned bit_width) { slicing::enode* slicing::mk_value_slice(rational const& val, unsigned bit_width) {
SASSERT(bit_width > 0);
SASSERT(0 <= val && val < rational::power_of_two(bit_width)); SASSERT(0 <= val && val < rational::power_of_two(bit_width));
sort* bv_sort = m_bv->mk_sort(bit_width); sort* bv_sort = m_bv->mk_sort(bit_width);
func_decl_ref f(m_ast.mk_fresh_func_decl("val", nullptr, 1, &bv_sort, bv_sort, false), m_ast); func_decl_ref f(m_ast.mk_fresh_func_decl("val", nullptr, 1, &bv_sort, bv_sort, false), m_ast);
@ -1100,7 +1102,8 @@ namespace polysat {
} }
else if (width(x) > width(y)) { else if (width(x) > width(y)) {
if (!has_sub(x)) if (!has_sub(x))
split(x, get_cut(y)); split(x, width(y) - 1);
// split(x, has_sub(y) ? get_cut(y) : (width(y) - 1));
xs.push_back(sub_hi(x)); xs.push_back(sub_hi(x));
xs.push_back(sub_lo(x)); xs.push_back(sub_lo(x));
ys.push_back(y); ys.push_back(y);
@ -1108,7 +1111,8 @@ namespace polysat {
else { else {
SASSERT(width(y) > width(x)); SASSERT(width(y) > width(x));
if (!has_sub(y)) if (!has_sub(y))
split(y, get_cut(x)); split(y, width(x) - 1);
// split(y, has_sub(x) ? get_cut(x) : (width(x) - 1));
ys.push_back(sub_hi(y)); ys.push_back(sub_hi(y));
ys.push_back(sub_lo(y)); ys.push_back(sub_lo(y));
xs.push_back(x); xs.push_back(x);