mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-24 06:43:40 +00:00
Code Activity

fix mul inverse

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-08-27 13:40:09 -07:00
parent ed0ffc1b49
commit b1f7965697
3 changed files with 10 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1002,11 +1002,13 @@ namespace bv {
* 8*e = a*(2b), then a = 4e*b^-1 * 8*e = a*(2b), then a = 4e*b^-1
*/ */
bool sls_eval::try_repair_mul(bvect const& e, bvval& a, bvect const& b) { bool sls_eval::try_repair_mul(bvect const& e, bvval& a, bvect const& b) {
verbose_stream() << e << " := " << a << " * " << b << "\n"; //verbose_stream() << e << " := " << a << " * " << b << "\n";
unsigned parity_e = a.parity(e); unsigned parity_e = a.parity(e);
unsigned parity_b = a.parity(b); unsigned parity_b = a.parity(b);
if (a.is_zero(b)) { if (a.is_zero(b)) {
if (a.try_set(e))
return true;
a.get_variant(m_tmp, m_rand); a.get_variant(m_tmp, m_rand);
if (m_rand(10) != 0) if (m_rand(10) != 0)
for (unsigned i = 0; i < b.bw - parity_b; ++i) for (unsigned i = 0; i < b.bw - parity_b; ++i)
@ -1044,14 +1046,18 @@ namespace bv {
// x*ta + y*tb = x // x*ta + y*tb = x
y.set_bw(a.bw);
b.copy_to(a.nw, y); b.copy_to(a.nw, y);
//verbose_stream() << "a.nw " << a.nw << " b.nw " << b.nw << " b " << b << " y.nw " << y.nw << " y " << y << "\n";
if (parity_b > 0) { if (parity_b > 0) {
a.shift_right(y, parity_b); a.shift_right(y, parity_b);
#if 0 #if 0
for (unsigned i = parity_b; i < b.bw; ++i) for (unsigned i = parity_b; i < b.bw; ++i)
y.set(i, m_rand(2) == 0); y.set(i, m_rand(2) == 0);
#endif #endif
} }
//verbose_stream() << parity_b << " y " << y << "\n";
y[a.nw] = 0; y[a.nw] = 0;
x[a.nw] = 0; x[a.nw] = 0;
@ -1094,7 +1100,7 @@ namespace bv {
b.copy_to(a.nw, y); b.copy_to(a.nw, y);
if (parity_b > 0) if (parity_b > 0)
a.shift_right(y, parity_b); a.shift_right(y, parity_b);
a.set_mul(m_tmp, tb, y); a.set_mul(m_tmp, tb, y, false);
SASSERT(a.is_one(m_tmp)); SASSERT(a.is_one(m_tmp));
#endif #endif
e.copy_to(b.nw, m_tmp2); e.copy_to(b.nw, m_tmp2);

2
src/ast/sls/sls_bv_plugin.cpp
View file

@ -148,7 +148,7 @@ namespace sls {
ctx.new_value_eh(e); ctx.new_value_eh(e);
} }
else if (bv.is_bv(e)) { else if (bv.is_bv(e)) {
IF_VERBOSE(2, verbose_stream() << "repair-up "; trace_repair(true, e)); IF_VERBOSE(5, verbose_stream() << "repair-up "; trace_repair(true, e));
m_eval.set_random(e); m_eval.set_random(e);
ctx.new_value_eh(e); ctx.new_value_eh(e);
} }

2
src/ast/sls/sls_valuation.cpp
View file

@ -487,7 +487,7 @@ namespace bv {
void sls_valuation::shift_right(bvect& out, unsigned shift) const { void sls_valuation::shift_right(bvect& out, unsigned shift) const {
SASSERT(shift < bw); SASSERT(shift < bw);
for (unsigned i = 0; i < bw; ++i) for (unsigned i = 0; i < bw; ++i)
out.set(i, i + shift < bw ? m_bits.get(i + shift) : false); out.set(i, i + shift < bw ? out.get(i + shift) : false);
SASSERT(well_formed()); SASSERT(well_formed());
} }