diff --git a/src/sat/smt/polysat/core.cpp b/src/sat/smt/polysat/core.cpp index 23cdcc24c..61f52ab59 100644 --- a/src/sat/smt/polysat/core.cpp +++ b/src/sat/smt/polysat/core.cpp @@ -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); diff --git a/src/sat/smt/polysat/core.h b/src/sat/smt/polysat/core.h index d3290dedc..30e50b534 100644 --- a/src/sat/smt/polysat/core.h +++ b/src/sat/smt/polysat/core.h @@ -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); diff --git a/src/sat/smt/polysat/viable.cpp b/src/sat/smt/polysat/viable.cpp index 026d191f0..25602c149 100644 --- a/src/sat/smt/polysat/viable.cpp +++ b/src/sat/smt/polysat/viable.cpp @@ -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; });