mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-27 01:39:22 +00:00
Code Activity

Update extend_by_bits argument

Browse source
This commit is contained in:
Jakob Rath 2023-11-24 11:37:30 +01:00
parent a805e1f27d
commit bd48a63a07
2 changed files with 10 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -436,12 +436,12 @@ namespace polysat {
template<bool FORWARD>
bool viable::refine_bits(pvar v, rational const& val, fixed_bits_info const& fbi) {
pdd v_pdd = s.var(v);
pdd_manager& m = s.var2pdd(v);
unsigned const k = s.size(v);
// TODO: We might also extend simultaneously up and downwards if we want the actual interval (however, this might make use of more fixed bits and is weaker - worse - therefore)
entry* ne = alloc_entry();
rational new_val = extend_by_bits<FORWARD>(v_pdd, val, fbi, ne->src, ne->side_cond);
rational new_val = extend_by_bits<FORWARD>(k, val, fbi, ne->src, ne->side_cond);
if (new_val == val) {
m_alloc.push_back(ne);
@ -450,18 +450,18 @@ namespace polysat {
// TODO: Extend in both directions? (Less justifications vs. bigger intervals)
// TODO: could also try to extend backwards as much as we can without introducing new justifications?
rational new_val2 = extend_by_bits<!FORWARD>(v_pdd, val, fbi, ne->src, ne->side_cond);
rational new_val2 = extend_by_bits<!FORWARD>(k, val, fbi, ne->src, ne->side_cond);
ne->refined = true;
ne->coeff = 1;
ne->bit_width = s.size(v);
if (FORWARD) {
LOG("refine-bits FORWARD for v" << v << " = " << val << " to [" << new_val2 << ", " << new_val << "[");
ne->interval = eval_interval::proper(v_pdd.manager().mk_val(new_val2), new_val2, v_pdd.manager().mk_val(new_val), new_val);
ne->interval = eval_interval::proper(m.mk_val(new_val2), new_val2, m.mk_val(new_val), new_val);
}
else {
LOG("refine-bits BACKWARD for v" << v << " = " << val << " to [" << new_val << ", " << new_val2 << "[");
ne->interval = eval_interval::proper(v_pdd.manager().mk_val(new_val), new_val, v_pdd.manager().mk_val(new_val2), new_val2);
ne->interval = eval_interval::proper(m.mk_val(new_val), new_val, m.mk_val(new_val2), new_val2);
}
SASSERT(ne->interval.currently_contains(val));
intersect(v, ne);
@ -713,15 +713,10 @@ namespace polysat {
}
// Skips all values that are not feasible w.r.t. fixed bits
template<bool FORWARD>
rational viable::extend_by_bits(pdd const& var, rational const& bound, fixed_bits_info const& fbi, vector<signed_constraint>& src, vector<signed_constraint>& side_cond) const {
unsigned const k = var.power_of_2();
if (fbi.is_empty()) // TODO: this check doesn't do anything.
return bound;
template <bool FORWARD>
rational viable::extend_by_bits(unsigned k, rational const& bound, fixed_bits_info const& fbi, vector<signed_constraint>& src, vector<signed_constraint>& side_cond) const {
svector<lbool> const& fixed = fbi.fixed;
SASSERT(k == fixed.size());
SASSERT(k <= fixed.size());
sat::literal_set added_src;
sat::literal_set added_side_cond;

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

@ -167,7 +167,7 @@ namespace polysat {
bool refine_disequal_lin(pvar v, rational const& val);
template<bool FORWARD>
rational extend_by_bits(pdd const& var, rational const& bounds, fixed_bits_info const& fbi, vector<signed_constraint>& out_src, vector<signed_constraint>& out_side_cond) const;
rational extend_by_bits(unsigned num_bits, rational const& bounds, fixed_bits_info const& fbi, vector<signed_constraint>& out_src, vector<signed_constraint>& out_side_cond) const;
bool collect_bit_information(pvar v, bool add_conflict, fixed_bits_info& out_fbi);