mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-05 21:53:23 +00:00
Code Activity

fixes to fixed

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-08-26 18:42:32 -07:00
parent 9fcddc5774
commit 6488e33915
2 changed files with 73 additions and 70 deletions
Download patch file Download diff file Expand all files Collapse all files

14
src/ast/sls/bv_sls_eval.cpp
View file

@ -363,13 +363,13 @@ namespace bv {
break;
}
case OP_CONCAT: {
SASSERT(e->get_num_args() == 2);
auto const& a = wval(e->get_arg(0));
auto const& b = wval(e->get_arg(1));
for (unsigned i = 0; i < b.bw; ++i)
val.eval.set(i, b.get_bit(i));
for (unsigned i = 0; i < a.bw; ++i)
val.eval.set(i + b.bw, a.get_bit(i));
unsigned bw = 0;
for (unsigned i = e->get_num_args(); i-- > 0; ) {
auto const& a = wval(e->get_arg(i));
for (unsigned j = 0; j < a.bw; ++j)
val.eval.set(j + bw, a.get_bit(j));
bw += a.bw;
}
break;
}
case OP_EXTRACT: {

43
src/ast/sls/bv_sls_fixed.cpp
View file

@ -340,26 +340,18 @@ namespace bv {
break;
}
case OP_BADD: {
SASSERT(e->get_num_args() == 2);
auto& a = ev.wval(e->get_arg(0));
auto& b = ev.wval(e->get_arg(1));
bool pfixed = true;
for (unsigned i = 0; i < v.bw; ++i) {
if (pfixed && a.fixed.get(i) && b.fixed.get(i))
v.fixed.set(i, true);
else if (!pfixed && a.fixed.get(i) && b.fixed.get(i) &&
!a.get_bit(i) && !b.get_bit(i)) {
pfixed = true;
v.fixed.set(i, false);
}
else {
pfixed = false;
v.fixed.set(i, false);
for (unsigned j = 0; pfixed && j < e->get_num_args(); ++j) {
auto& a = ev.wval(e->get_arg(j));
pfixed &= a.fixed.get(i);
}
v.fixed.set(i, pfixed);
}
break;
}
case OP_BMUL: {
if (e->get_num_args() == 2) {
SASSERT(e->get_num_args() == 2);
auto& a = ev.wval(e->get_arg(0));
auto& b = ev.wval(e->get_arg(1));
@ -409,16 +401,27 @@ namespace bv {
v.fixed.set(i, true);
}
}
}
else {
bool pfixed = true;
for (unsigned i = 0; i < v.bw; ++i) {
for (unsigned j = 0; pfixed && j < e->get_num_args(); ++j) {
auto& a = ev.wval(e->get_arg(j));
pfixed &= a.fixed.get(i);
}
v.fixed.set(i, pfixed);
}
}
break;
}
case OP_CONCAT: {
SASSERT(e->get_num_args() == 2);
auto& a = ev.wval(e->get_arg(0));
auto& b = ev.wval(e->get_arg(1));
for (unsigned i = 0; i < b.bw; ++i)
v.fixed.set(i, b.fixed.get(i));
for (unsigned i = 0; i < a.bw; ++i)
v.fixed.set(i + b.bw, a.fixed.get(i));
unsigned bw = 0;
for (unsigned i = e->get_num_args(); i-- > 0; ) {
auto& a = ev.wval(e->get_arg(i));
for (unsigned j = 0; j < a.bw; ++j)
v.fixed.set(bw + j, a.fixed.get(j));
bw += a.bw;
}
break;
}
case OP_EXTRACT: {