mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Code Activity

check underflows, aig fixes

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-01-14 19:46:27 -08:00
parent 82cacdf569
commit 0d614b8c36
3 changed files with 16 additions and 33 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

21
src/sat/sat_aig_simplifier.cpp
View file

@ -361,6 +361,7 @@ namespace sat {
literal u(vt[j].first, false);
cut const& c1 = *vt[j].second;
cut nc1(c1);
nc1.negate();
uint64_t t1 = c1.table();
uint64_t n1 = nc1.table();
for (unsigned k = j + 1; k < vt.size(); ++k) {
@ -368,8 +369,7 @@ namespace sat {
cut const& c2 = *vt[k].second;
uint64_t t2 = c2.table();
uint64_t n2 = c2.ntable();
//
if (u.var() == v.var() || t1 == t2 || t1 == n2) {
if (t1 == t2 || t1 == n2) {
// already handled
}
else if ((t1 | t2) == t2) {
@ -390,6 +390,13 @@ namespace sat {
}
void aig_simplifier::learn_implies(big& big, cut const& c, literal u, literal v) {
if (u == ~v) {
assign_unit(c, v);
return;
}
if (u == v) {
return;
}
bin_rel q, p(~u, v);
if (m_bins.find(p, q) && q.op != none)
return;
@ -497,11 +504,11 @@ namespace sat {
}
void aig_simplifier::add_dont_cares(vector<cut_set> const& cuts) {
if (m_config.m_enable_dont_cares) {
cuts2bins(cuts);
bins2dont_cares();
dont_cares2cuts(cuts);
}
if (!m_config.m_enable_dont_cares)
return;
cuts2bins(cuts);
bins2dont_cares();
dont_cares2cuts(cuts);
}
/**

2
src/util/mpq.h
View file

@ -640,6 +640,8 @@ public:
void set(mpq & a, int n, int d) {
SASSERT(d != 0);
if (d < 0) {
SASSERT(d != INT_MIN);
SASSERT(n != INT_MIN);
n = -n;
d = -d;
}

26
src/util/mpz.cpp
View file

@ -97,36 +97,10 @@ unsigned u_gcd(unsigned u, unsigned v) {
if (u == v) return u << shift;
do {
v >>= _trailing_zeros32(v);
#if 1
unsigned diff = u - v;
unsigned mdiff = diff & (unsigned)((int)diff >> 31);
u = v + mdiff; // min
v = diff - 2 * mdiff; // if v <= u: u - v, if v > u: v - u = u - v - 2 * (u - v)
#endif
#if 0
unsigned t = _bit_max(u, v);
u = _bit_min(u, v);
v = t;
v -= u;
#endif
#if 0
unsigned t = std::max(u, v);
u = std::min(u,v);
v = t;
v -= u;
#endif
#if 0
if (u > v) std::swap(u, v);
v -= u;
#endif
#if 0
unsigned d1 = u - v;
unsigned d2 = v - u;
unsigned md21 = d2 & (unsigned)((int)d1 >> 31);
unsigned md12 = d1 & (unsigned)((int)d2 >> 31);
u = _bit_min(u, v);
v = md12 | md21;
#endif
}
while (v != 0);
return u << shift;