mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

shortcut in add_value

Browse source 
otherwise, with literal x == a for constant a, we will create unnecessary value nodes.
(because slicing will propagate x := a to the solver, which calls add_value in turn)
This commit is contained in:
Jakob Rath 2023-08-18 15:00:00 +02:00
parent 2d0120c621
commit d3b5974448
1 changed files with 4 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1385,6 +1385,8 @@ namespace polysat {
bool slicing::add_value(pvar v, rational const& value, sat::literal lit) {
enode* const sv = var2slice(v);
if (get_value_node(sv) && get_value(get_value_node(sv)) == value)
return true;
enode* const sval = mk_value_slice(value, width(sv));
return merge(sv, sval, mk_var_dep(v, sv, lit));
}
@ -1635,16 +1637,14 @@ namespace polysat {
if (!s->is_root())
continue;
bool const sub = has_sub(s);
enode_vector s_base;
get_base(s, s_base);
enode_vector const s_base = get_base(s);
for (enode* n : euf::enode_class(s)) {
// equivalence class only contains slices of equal length
VERIFY_EQ(width(s), width(n));
// either all nodes in the class have subslices or none do
SASSERT_EQ(sub, has_sub(n));
// bases of equivalent nodes are equivalent
enode_vector n_base;
get_base(n, n_base);
enode_vector const n_base = get_base(n);
VERIFY_EQ(s_base.size(), n_base.size());
for (unsigned i = s_base.size(); i-- > 0; ) {
VERIFY_EQ(s_base[i]->get_root(), n_base[i]->get_root());