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

sign and zero extend

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-12-10 23:15:03 -08:00
parent dc690307ff
commit 286932684a
1 changed files with 2 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -289,9 +289,7 @@ namespace polysat {
unsigned sz = bv.get_bv_size(e);
unsigned arg_sz = bv.get_bv_size(arg);
unsigned sz2 = sz - arg_sz;
var2pdd(expr2enode(e)->get_th_var(get_id()));
if (arg_sz == sz)
add_clause(eq_internalize(e, arg), false);
else {
@ -299,7 +297,7 @@ namespace polysat {
// arg < 0 ==> e = concat(arg, 1...1)
// arg >= 0 ==> e = concat(arg, 0...0)
add_clause(lt0, eq_internalize(e, bv.mk_concat(arg, bv.mk_numeral(rational::power_of_two(sz2) - 1, sz2))), false);
add_clause(~lt0, eq_internalize(e, bv.mk_concat(arg, bv.mk_numeral(0, sz - arg_sz))), false);
add_clause(~lt0, eq_internalize(e, bv.mk_concat(arg, bv.mk_numeral(0, sz2))), false);
}
}
@ -313,7 +311,7 @@ namespace polysat {
add_clause(eq_internalize(e, arg), false);
else
// e = concat(arg, 0...0)
add_clause(eq_internalize(e, bv.mk_concat(arg, bv.mk_numeral(0, sz - arg_sz))), false);
add_clause(eq_internalize(e, bv.mk_concat(arg, bv.mk_numeral(0, sz2))), false);
}
void solver::internalize_div_rem(app* e, bool is_div) {