mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Code Activity

tidy

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-12-31 17:09:49 -08:00
parent 30b5b3bd15
commit 09b3d99db1
2 changed files with 6 additions and 16 deletions
Download patch file Download diff file Expand all files Collapse all files

18
src/sat/smt/polysat/op_constraint.cpp
View file

@ -9,14 +9,6 @@ Author:
Jakob Rath, Nikolaj Bjorner (nbjorner) 2021-12-09
Notes:
Additional possible functionality on constraints:
- bit-wise assignments - narrow based on bit assignment, not entire word assignment.
- integration with congruence tables
- integration with conflict resolution
--*/
#include "util/log.h"
@ -428,12 +420,10 @@ namespace polysat {
unsigned k = qv.val().get_unsigned();
// q = k -> r[i+k] = p[i] for 0 <= i < N - k
for (unsigned i = 0; i < N - k; ++i) {
if (rv.val().get_bit(i + k) && !pv.val().get_bit(i)) {
c.add_axiom("q = k -> p>>q[i+k] = p[i] for 0 <= i < N - k", { ~C.eq(q, k), ~C.bit(r, i + k), C.bit(p, i) }, true);
}
if (!rv.val().get_bit(i + k) && pv.val().get_bit(i)) {
c.add_axiom("q = k -> p>>q[i+k] = p[i] for 0 <= i < N - k", { ~C.eq(q, k), C.bit(r, i + k), ~C.bit(p, i) }, true);
}
if (rv.val().get_bit(i + k) && !pv.val().get_bit(i))
c.add_axiom("q = k -> p>>q[i+k] = p[i] for 0 <= i < N - k", { ~C.eq(q, k), ~C.bit(r, i + k), C.bit(p, i) }, true);
else if (!rv.val().get_bit(i + k) && pv.val().get_bit(i))
c.add_axiom("q = k -> p>>q[i+k] = p[i] for 0 <= i < N - k", { ~C.eq(q, k), C.bit(r, i + k), ~C.bit(p, i) }, true);
}
}
else {

4
src/sat/smt/polysat/umul_ovfl_constraint.cpp
View file

@ -138,7 +138,7 @@ namespace polysat {
SASSERT(p_bound * q_bound >= M);
SASSERT(p_bound * (q_bound - 1) < M);
// LOG("p_bound: " << p.manager().mk_val(p_bound));
c.add_axiom("~Ovfl(p, q) & p <= p_bound ==> q < q_bound", { d, ~C.ule(p0, p_bound), C.ule(q_bound, q0) }, false);
c.add_axiom("~Ovfl(p, q) & p <= p_bound -> q < q_bound", { d, ~C.ule(p0, p_bound), C.ule(q_bound, q0) }, true);
}
else {
// Find lowest bound for p such that q_bound is still correct.
@ -148,7 +148,7 @@ namespace polysat {
SASSERT(p_bound * q_bound >= M);
SASSERT(p_bound * (q_bound - 1) < M);
// LOG("p_bound: " << p.manager().mk_val(p_bound));
c.add_axiom("~Ovfl(p, q) & p >= p_bound ==> q < q_bound", { d, ~C.ule(p_bound, p0), C.ult(q0, q_bound) }, false);
c.add_axiom("~Ovfl(p, q) & p >= p_bound -> q < q_bound", { d, ~C.ule(p_bound, p0), C.ult(q0, q_bound) }, true);
}
return true;
}