mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-29 09:28:45 +00:00
Code Activity

elaborate on narrow

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-12-15 10:17:42 -08:00
parent a6684824c1
commit 4eb3f5c630
1 changed files with 7 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

14
src/math/polysat/op_constraint.cpp
View file

@ -3,7 +3,7 @@ Copyright (c) 2021 Microsoft Corporation
Module Name: Module Name:
polysat shift right constraint. polysat constraints for bit operations.
Author: Author:
@ -167,25 +167,25 @@ namespace polysat {
auto qv = q().subst_val(s.assignment()); auto qv = q().subst_val(s.assignment());
auto rv = r().subst_val(s.assignment()); auto rv = r().subst_val(s.assignment());
unsigned K = p().manager().power_of_2(); unsigned K = p().manager().power_of_2();
signed_constraint lshl(this, true); signed_constraint lshr(this, true);
// r <= p // r <= p
if (pv.is_val() && rv.is_val() && rv.val() > pv.val()) { if (pv.is_val() && rv.is_val() && rv.val() > pv.val()) {
s.add_clause(~lshl, s.ule(r(), p()), true); s.add_clause(~lshr, s.ule(r(), p()), true);
return; return;
} }
// q >= K -> r = 0 // q >= K -> r = 0
if (qv.is_val() && qv.val() >= K && rv.is_val() && !rv.is_zero()) { if (qv.is_val() && qv.val() >= K && rv.is_val() && !rv.is_zero()) {
s.add_clause(~lshl, ~s.ule(K, q()), s.eq(r()), true); s.add_clause(~lshr, ~s.ule(K, q()), s.eq(r()), true);
return; return;
} }
// q = 0 => r = p // q = 0 => r = p
if (qv.is_zero() && pv.is_val() && rv.is_val() && pv != rv) { if (qv.is_zero() && pv.is_val() && rv.is_val() && pv != rv) {
s.add_clause(~lshl, ~s.eq(q()), s.eq(p(), r()), true); s.add_clause(~lshr, ~s.eq(q()), s.eq(p(), r()), true);
return; return;
} }
// q != 0 & p > 0 => r < p // q != 0 & p > 0 => r < p
if (qv.is_val() && !qv.is_zero() && pv.is_val() && rv.is_val() && pv <= rv) { if (qv.is_val() && !qv.is_zero() && pv.is_val() && rv.is_val() && !pv.is_zero() && pv <= rv) {
s.add_clause(~lshl, s.eq(q()), s.ule(p, 0), s.ult(r(), p()), true); s.add_clause(~lshr, s.eq(q()), s.ule(p, 0), s.ult(r(), p()), true);
return; return;
} }
NOT_IMPLEMENTED_YET(); NOT_IMPLEMENTED_YET();