mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 08:35:31 +00:00
Code Activity

fix srem encoding

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-01-13 17:04:18 -08:00
parent 01c5a09575
commit b7306f3c0c
1 changed files with 1 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/sat/smt/polysat_internalize.cpp
View file

@ -413,7 +413,7 @@ namespace polysat {
unsigned sz = bv.get_bv_size(x);
sat::literal y_eq0 = eq_internalize(y, bv.mk_zero(sz));
add_axiom("srem", { ~y_eq0, eq_internalize(e, x) });
add_axiom("srem", { y_eq0, eq_internalize(e, bv.mk_bv_mul(bv.mk_bv_sdiv(x, y), y)) });
add_axiom("srem", { y_eq0, eq_internalize(e, bv.mk_bv_sub(x, bv.mk_bv_mul(bv.mk_bv_sdiv(x, y), y))) });
}
// u := umod(x, y)
@ -513,8 +513,6 @@ namespace polysat {
void solver::quot_rem(expr* quot, expr* rem, expr* x, expr* y) {
pdd a = expr2pdd(x);
pdd b = expr2pdd(y);
euf::enode* qn = expr2enode(quot);
euf::enode* rn = expr2enode(rem);
auto& m = a.manager();
unsigned sz = m.power_of_2();
verbose_stream() << "quot-rem " << a << " " << b << "\n";