mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-25 07:13:41 +00:00
Code Activity

minor comments, skolem = false

Browse source
This commit is contained in:
Jakob Rath 2023-08-17 17:59:40 +02:00
parent 3e7f7ef605
commit 19c1c7aa73
2 changed files with 3 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/math/polysat/univariate/univariate_solver.cpp
View file

@ -345,13 +345,14 @@ namespace polysat {
parity = mk_numeral(get_parity(get_offset(v_coeff))); parity = mk_numeral(get_parity(get_offset(v_coeff)));
return parity; return parity;
} }
parity = m.mk_fresh_const("parity", bv->mk_sort(bit_width)); parity = m.mk_fresh_const("parity", bv->mk_sort(bit_width), false);
expr* parity_1 = bv->mk_bv_add(parity, mk_numeral(1)); expr* parity_1 = bv->mk_bv_add(parity, mk_numeral(1));
// if v = 0 // if v = 0
// then parity = N // then parity = N
// else v = (v >> parity) << parity // else v = (v >> parity) << parity
// && v != (v >> parity+1) << parity+1 // && v != (v >> parity+1) << parity+1
// TODO: what about: v[k:] = 0 && v[k+1:] != 0 ==> parity = k for each k? // TODO: what about: v[k:] = 0 && v[k+1:] != 0 ==> parity = k for each k?
// TODO: helper axioms like parity <= N etc.?
add(m.mk_ite( add(m.mk_ite(
m.mk_eq(v, mk_numeral(0)), m.mk_eq(v, mk_numeral(0)),
m.mk_eq(parity, mk_numeral(bit_width)), m.mk_eq(parity, mk_numeral(bit_width)),

2
src/math/polysat/univariate/univariate_solver.h
View file

@ -74,7 +74,7 @@ namespace polysat {
bool find_max(rational& out_max); bool find_max(rational& out_max);
/** /**
* Find up to two viable values. * Find up to two models.
* *
* Precondition: check() returned l_true * Precondition: check() returned l_true
* returns: true on success, false on resource out * returns: true on success, false on resource out