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

some code simplifications in mpn

Browse source 
plus remove duplicated assertion
This commit is contained in:
Nuno Lopes 2023-12-22 15:27:57 +00:00
parent 4fe423482a
commit ab22e763d7
2 changed files with 12 additions and 26 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

37
src/util/mpn.cpp
View file

@ -21,24 +21,20 @@ Revision History:
#include "util/buffer.h"
#include "util/mpn.h"
#define max(a,b) (((a) > (b)) ? (a) : (b))
typedef uint64_t mpn_double_digit;
static_assert(sizeof(mpn_double_digit) == 2 * sizeof(mpn_digit), "size alignment");
const mpn_digit mpn_manager::zero = 0;
int mpn_manager::compare(mpn_digit const * a, unsigned lnga,
mpn_digit const * b, unsigned lngb) const {
int res = 0;
trace(a, lnga);
unsigned j = max(lnga, lngb);
unsigned j = std::max(lnga, lngb);
for (; j-- > 0 && res == 0;) {
mpn_digit const & u_j = (j < lnga) ? a[j] : zero;
mpn_digit const & v_j = (j < lngb) ? b[j] : zero;
if (u_j > v_j)
mpn_digit u_j = (j < lnga) ? a[j] : 0;
mpn_digit v_j = (j < lngb) ? b[j] : 0;
if (u_j > v_j)
res = 1;
else if (u_j < v_j)
res = -1;
@ -56,14 +52,14 @@ bool mpn_manager::add(mpn_digit const * a, unsigned lnga,
unsigned * plngc) const {
trace(a, lnga, b, lngb, "+");
// Essentially Knuth's Algorithm A
unsigned len = max(lnga, lngb);
unsigned len = std::max(lnga, lngb);
SASSERT(lngc_alloc == len+1 && len > 0);
mpn_digit k = 0;
mpn_digit r;
bool c1, c2;
for (unsigned j = 0; j < len; j++) {
mpn_digit const & u_j = (j < lnga) ? a[j] : zero;
mpn_digit const & v_j = (j < lngb) ? b[j] : zero;
mpn_digit u_j = (j < lnga) ? a[j] : 0;
mpn_digit v_j = (j < lngb) ? b[j] : 0;
r = u_j + v_j; c1 = r < u_j;
c[j] = r + k; c2 = c[j] < r;
k = c1 | c2;
@ -81,13 +77,13 @@ bool mpn_manager::sub(mpn_digit const * a, unsigned lnga,
mpn_digit * c, mpn_digit * pborrow) const {
trace(a, lnga, b, lngb, "-");
// Essentially Knuth's Algorithm S
unsigned len = max(lnga, lngb);
unsigned len = std::max(lnga, lngb);
mpn_digit & k = *pborrow; k = 0;
mpn_digit r;
bool c1, c2;
for (unsigned j = 0; j < len; j++) {
mpn_digit const & u_j = (j < lnga) ? a[j] : zero;
mpn_digit const & v_j = (j < lngb) ? b[j] : zero;
mpn_digit u_j = (j < lnga) ? a[j] : 0;
mpn_digit v_j = (j < lngb) ? b[j] : 0;
r = u_j - v_j; c1 = r > u_j;
c[j] = r - k; c2 = c[j] > r;
k = c1 | c2;
@ -112,14 +108,14 @@ bool mpn_manager::mul(mpn_digit const * a, unsigned lnga,
c[i] = 0;
for (unsigned j = 0; j < lngb; j++) {
mpn_digit const & v_j = b[j];
mpn_digit v_j = b[j];
if (v_j == 0) { // This branch may be omitted according to Knuth.
c[j+lnga] = 0;
}
else {
k = 0;
for (i = 0; i < lnga; i++) {
mpn_digit const & u_i = a[i];
mpn_digit u_i = a[i];
mpn_double_digit t;
t = ((mpn_double_digit)u_i * (mpn_double_digit)v_j) +
(mpn_double_digit) c[i+j] +
@ -156,15 +152,6 @@ bool mpn_manager::div(mpn_digit const * numer, unsigned lnum,
return false;
}
bool all_zero = true;
for (unsigned i = 0; i < lden && all_zero; i++)
if (denom[i] != zero) all_zero = false;
if (all_zero) {
UNREACHABLE();
return res;
}
SASSERT(denom[lden-1] != 0);
if (lnum == 1 && lden == 1) {

1
src/util/mpn.h
View file

@ -53,7 +53,6 @@ public:
private:
using mpn_sbuffer = sbuffer<mpn_digit>;
static const mpn_digit zero;
void display_raw(std::ostream & out, mpn_digit const * a, unsigned lng) const;
unsigned div_normalize(mpn_digit const * numer, unsigned lnum,