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

Don't access solver_interface directly

Browse source
This commit is contained in:
Jakob Rath 2024-03-20 10:16:40 +01:00
parent a34bb99db3
commit 5339a2f70f
3 changed files with 7 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -504,6 +504,10 @@ namespace polysat {
s.get_bitvector_sub_slices(v, out);
}
void core::get_fixed_subslices(pvar v, fixed_bits_vector& fixed_subslices) {
s.get_fixed_sub_slices(v, fixed_subslices);
}
pdd core::mk_zero_extend(unsigned sz, pdd const& p) {
if (p.is_val())
return value(p.val(), p.manager().power_of_2() + sz);

3
src/sat/smt/polysat/core.h
View file

@ -168,8 +168,9 @@ namespace polysat {
* Viable
*/
void get_bitvector_suffixes(pvar v, offset_slices& out);
void get_fixed_bits(pvar v, fixed_bits_vector& fixed_slice);
void get_fixed_bits(pvar v, fixed_bits_vector& fixed_slices);
void get_subslices(pvar v, offset_slices& out);
void get_fixed_subslices(pvar v, fixed_bits_vector& fixed_subslices);
pdd mk_zero_extend(unsigned sz, pdd const& p);
pdd mk_extract(unsigned hi, unsigned lo, pdd const& p);

2
src/sat/smt/polysat/viable.cpp
View file

@ -691,7 +691,7 @@ namespace polysat {
// although, the max admissible level of fixed slices depends on the child pvar under consideration, so we may not get the optimal interval anymore?
// (pvars on the same slice only differ by level. the fixed value is the same for all. so we can limit by the max level of pvars and then the projection will work for at least one.)
fixed_bits_vector fixed;
c.s.get_fixed_sub_slices(e->var, fixed); // TODO: move into m_fixed bits?
c.get_fixed_subslices(e->var, fixed);
bool has_pvar = any_of(fixed, [](fixed_slice const& f) { return f.child != null_var; });