mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-20 23:56:37 +00:00
Code Activity

fix compile error

Browse source
This commit is contained in:
Jakob Rath 2023-11-29 13:42:02 +01:00
parent 79d77bc690
commit 923e4b4bd9
2 changed files with 27 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/math/polysat/viable.cpp
View file

@ -1511,7 +1511,15 @@ namespace polysat {
return {nullptr, false};
}
lbool viable::find_on_layers(pvar const v, unsigned_vector const& widths, pvar_vector const& overlaps, fixed_bits_info const& fbi, rational const& to_cover_lo, rational const& to_cover_hi, rational& val) {
lbool viable::find_on_layers(
pvar const v,
unsigned_vector const& widths,
pvar_vector const& overlaps,
fixed_bits_info const& fbi,
rational const& to_cover_lo,
rational const& to_cover_hi,
rational& val
) {
ptr_vector<entry> refine_todo;
// max number of interval refinements before falling back to the univariate solver

20
src/math/polysat/viable.h
View file

@ -207,8 +207,24 @@ namespace polysat {
public:
lbool find_viable2_new(pvar v, rational& out_lo, rational& out_hi);
lbool viable::find_on_layers(pvar v, unsigned_vector const& widths, pvar_vector const& overlaps, fixed_bits_info const& fbi, rational const& to_cover_lo, rational const& to_cover_hi, rational& out_val);
lbool find_on_layer(pvar v, unsigned w_idx, unsigned_vector const& widths, pvar_vector const& overlaps, fixed_bits_info const& fbi, rational const& to_cover_lo, rational const& to_cover_hi, rational& out_val, ptr_vector<entry>& refine_todo);
lbool find_on_layers(
pvar v,
unsigned_vector const& widths,
pvar_vector const& overlaps,
fixed_bits_info const& fbi,
rational const& to_cover_lo,
rational const& to_cover_hi,
rational& out_val);
lbool find_on_layer(
pvar v,
unsigned w_idx,
unsigned_vector const& widths,
pvar_vector const& overlaps,
fixed_bits_info const& fbi,
rational const& to_cover_lo,
rational const& to_cover_hi,
rational& out_val,
ptr_vector<entry>& refine_todo);
std::pair<entry*, bool> find_value(rational const& val, entry* entries);