mirror of
https://github.com/Z3Prover/z3
synced 2025-04-23 17:15:31 +00:00
updates to saturation
This commit is contained in:
Nikolaj Bjorner
parent
fbbad72c29
commit
50358e43ed
6 changed files with 131 additions and 1913 deletions
|
|
@ -304,11 +304,11 @@ namespace euf {
|
|||
void solver::get_eq_antecedents(enode* a, enode* b, literal_vector& r) {
|
||||
m_egraph.begin_explain();
|
||||
m_explain.reset();
|
||||
m_egraph.explain_eq<size_t>(m_explain, nullptr, a, b);
|
||||
for (unsigned qhead = 0; qhead < m_explain.size(); ++qhead) {
|
||||
size_t* e = m_explain[qhead];
|
||||
if (is_literal(e))
|
||||
r.push_back(get_literal(e));
|
||||
m_egraph.explain_eq<size_t>(m_explain, nullptr, a, b);
|
||||
for (unsigned qhead = 0; qhead < m_explain.size(); ++qhead) {
|
||||
size_t* e = m_explain[qhead];
|
||||
if (is_literal(e))
|
||||
r.push_back(get_literal(e));
|
||||
else {
|
||||
size_t idx = get_justification(e);
|
||||
auto* ext = sat::constraint_base::to_extension(idx);
|
||||
|
|
|
|||
|
|
@ -193,32 +193,7 @@ namespace polysat {
|
|||
}
|
||||
|
||||
sat::check_result core::final_check() {
|
||||
constraint_id conflict_idx = find_conflicting_constraint();
|
||||
|
||||
// If all constraints evaluate to true, we are done.
|
||||
if (conflict_idx.is_null())
|
||||
return sat::check_result::CR_DONE;
|
||||
|
||||
// Extract variables that are of level or above of conflicting constraint and contradict the constraint
|
||||
auto vars = find_conflict_variables(conflict_idx);
|
||||
saturation sat(*this);
|
||||
for (auto v: vars)
|
||||
if (sat.propagate(v, conflict_idx))
|
||||
return sat::check_result::CR_CONTINUE;
|
||||
|
||||
// If no saturation propagation was possible, explain the conflict using the variable assignment.
|
||||
m_unsat_core = explain_eval(get_constraint(conflict_idx));
|
||||
m_unsat_core.push_back(conflict_idx);
|
||||
propagate_unsat_core();
|
||||
return sat::check_result::CR_CONTINUE;
|
||||
}
|
||||
|
||||
/**
|
||||
* Identify a conflicting constraint, if any, that evaluates to false under
|
||||
* the current assignment.
|
||||
*/
|
||||
constraint_id core::find_conflicting_constraint() {
|
||||
unsigned conflict_level = UINT_MAX;
|
||||
unsigned n = 0;
|
||||
constraint_id conflict_idx = { UINT_MAX };
|
||||
for (auto idx : m_prop_queue) {
|
||||
auto [sc, d, value] = m_constraint_index[idx.id];
|
||||
|
|
@ -227,17 +202,25 @@ namespace polysat {
|
|||
SASSERT(eval_value != l_undef);
|
||||
if (eval_value == value)
|
||||
continue;
|
||||
auto explain = explain_eval(sc);
|
||||
unsigned new_conflict_level = d.level();
|
||||
for (auto idx2 : explain)
|
||||
new_conflict_level = std::max(new_conflict_level, m_constraint_index[idx2.id].d.level());
|
||||
if (0 == (m_rand() % (++n)))
|
||||
conflict_idx = idx;
|
||||
|
||||
if (new_conflict_level >= conflict_level)
|
||||
continue;
|
||||
conflict_idx = idx;
|
||||
conflict_level = new_conflict_level;
|
||||
auto vars = find_conflict_variables(idx);
|
||||
saturation sat(*this);
|
||||
for (auto v : vars)
|
||||
if (sat.resolve(v, conflict_idx))
|
||||
return sat::check_result::CR_CONTINUE;
|
||||
}
|
||||
return conflict_idx;
|
||||
|
||||
// If all constraints evaluate to true, we are done.
|
||||
if (conflict_idx.is_null())
|
||||
return sat::check_result::CR_DONE;
|
||||
|
||||
// If no saturation propagation was possible, explain the conflict using the variable assignment.
|
||||
m_unsat_core = explain_eval(get_constraint(conflict_idx));
|
||||
m_unsat_core.push_back(conflict_idx);
|
||||
propagate_unsat_core();
|
||||
return sat::check_result::CR_CONTINUE;
|
||||
}
|
||||
|
||||
/**
|
||||
|
|
@ -397,6 +380,10 @@ namespace polysat {
|
|||
s.get_fixed_bits(v, fixed_bits);
|
||||
}
|
||||
|
||||
void core::get_subslices(pvar v, offset_slices& out) {
|
||||
s.get_bitvector_sub_slices(v, out);
|
||||
}
|
||||
|
||||
bool core::inconsistent() const {
|
||||
return s.inconsistent();
|
||||
}
|
||||
|
|
|
|||
|
|
@ -57,6 +57,7 @@ namespace polysat {
|
|||
constraint_id_vector m_prop_queue;
|
||||
svector<constraint_info> m_constraint_index; // index of constraints
|
||||
constraint_id_vector m_unsat_core;
|
||||
random_gen m_rand;
|
||||
|
||||
|
||||
// attributes associated with variables
|
||||
|
|
@ -83,16 +84,14 @@ namespace polysat {
|
|||
void propagate_unsat_core();
|
||||
void propagate(constraint_id id, signed_constraint& sc, lbool value, dependency const& d);
|
||||
|
||||
void get_bitvector_suffixes(pvar v, offset_slices& out);
|
||||
void get_fixed_bits(pvar v, fixed_bits_vector& fixed_bits);
|
||||
bool inconsistent() const;
|
||||
|
||||
|
||||
|
||||
void add_watch(unsigned idx, unsigned var);
|
||||
|
||||
|
||||
|
||||
sat::check_result final_check();
|
||||
constraint_id find_conflicting_constraint();
|
||||
svector<pvar> find_conflict_variables(constraint_id idx);
|
||||
|
||||
void add_axiom(signed_constraint sc);
|
||||
|
|
@ -147,6 +146,13 @@ namespace polysat {
|
|||
|
||||
std::ostream& display(std::ostream& out) const;
|
||||
|
||||
/*
|
||||
* Viable
|
||||
*/
|
||||
void get_bitvector_suffixes(pvar v, offset_slices& out);
|
||||
void get_fixed_bits(pvar v, fixed_bits_vector& fixed_bits);
|
||||
void get_subslices(pvar v, offset_slices& out);
|
||||
|
||||
/*
|
||||
* Saturation
|
||||
*/
|
||||
|
|
@ -159,6 +165,7 @@ namespace polysat {
|
|||
dependency propagate(signed_constraint const& sc, constraint_id_vector const& ids) { return s.propagate(sc, ids); }
|
||||
lbool eval(signed_constraint const& sc);
|
||||
constraint_id_vector explain_eval(signed_constraint const& sc);
|
||||
bool inconsistent() const;
|
||||
|
||||
/*
|
||||
* Constraints
|
||||
|
|
|
|||
File diff suppressed because it is too large
Load diff
|
|
@ -25,142 +25,58 @@ namespace polysat {
|
|||
*/
|
||||
class saturation {
|
||||
|
||||
using clause = std::initializer_list<constraint_id_or_constraint>;
|
||||
using clause = std::initializer_list<constraint_or_dependency>;
|
||||
core& c;
|
||||
constraints& C;
|
||||
bool m_propagated = false;
|
||||
|
||||
void propagate(signed_constraint const& sc, std::initializer_list<constraint_id> const& premises);
|
||||
void add_clause(char const* name, clause const& cs, bool is_redundant);
|
||||
|
||||
struct constraint_filter {
|
||||
core& c;
|
||||
std::function<bool(signed_constraint const& sc)> const& m_filter;
|
||||
unsigned m_index;
|
||||
unsigned m_end;
|
||||
void fwd() {
|
||||
for (; m_index < m_end && !m_filter(c.get_constraint(c.assigned_constraints()[m_index])); ++m_index);
|
||||
if (c.inconsistent())
|
||||
m_index = m_end;
|
||||
}
|
||||
constraint_filter(core& c, std::function<bool(signed_constraint const& sc)> const& filter, unsigned i) :
|
||||
c(c), m_filter(filter), m_index(i), m_end(c.assigned_constraints().size()) {
|
||||
fwd();
|
||||
}
|
||||
|
||||
bool operator!=(constraint_filter const& other) const { return m_index != other.m_index; }
|
||||
constraint_filter& operator++() { ++m_index; fwd(); return *this; }
|
||||
constraint_id operator*() const { return c.assigned_constraints()[m_index]; }
|
||||
};
|
||||
struct constraint_iterator {
|
||||
core& c;
|
||||
std::function<bool(signed_constraint const& sc)> const& m_filter;
|
||||
constraint_iterator(core& c, std::function<bool(signed_constraint const& sc)> const& filter) :
|
||||
c(c), m_filter(filter) {}
|
||||
constraint_filter begin() const { return constraint_filter(c, m_filter, 0); }
|
||||
constraint_filter end() const { return constraint_filter(c, m_filter, c.assigned_constraints().size()); }
|
||||
};
|
||||
|
||||
|
||||
bool match_core(std::function<bool(signed_constraint const& sc)> const& p, constraint_id& id);
|
||||
bool match_constraints(std::function<bool(signed_constraint const& sc)> const& p, constraint_id& id);
|
||||
|
||||
|
||||
// a * b does not overflow
|
||||
bool is_non_overflow(pdd const& a, pdd const& b);
|
||||
bool is_non_overflow(pdd const& x, pdd const& y, signed_constraint& c);
|
||||
|
||||
|
||||
void propagate_infer_equality(pvar x, inequality const& a_l_b);
|
||||
void try_ugt_x(pvar v, inequality const& i);
|
||||
void try_ugt_y(pvar v, inequality const& i);
|
||||
void try_ugt_z(pvar z, inequality const& i);
|
||||
void try_nonzero_upper_extract(pvar y);
|
||||
void try_umul_ovfl(pvar v, umul_ovfl const& sc);
|
||||
|
||||
signed_constraint ineq(bool is_strict, pdd const& x, pdd const& y);
|
||||
|
||||
#if 0
|
||||
parity_tracker m_parity_tracker;
|
||||
unsigned_vector m_occ;
|
||||
unsigned_vector m_occ_cnt;
|
||||
signed_constraint ineq(bool is_strict, pdd const& x, pdd const& y);
|
||||
|
||||
|
||||
|
||||
|
||||
signed_constraint ineq(bool strict, pdd const& lhs, pdd const& rhs);
|
||||
|
||||
void log_lemma(pvar v, conflict& core);
|
||||
bool propagate(pvar v, conflict& core, signed_constraint crit1, signed_constraint c);
|
||||
bool propagate(pvar v, conflict& core, inequality const& crit1, signed_constraint c);
|
||||
bool propagate(pvar v, conflict& core, signed_constraint c);
|
||||
bool add_conflict(pvar v, conflict& core, inequality const& crit1, signed_constraint c);
|
||||
bool add_conflict(pvar v, conflict& core, inequality const& crit1, inequality const& crit2, signed_constraint c);
|
||||
|
||||
bool try_ugt_x(pvar v, conflict& core, inequality const& c);
|
||||
|
||||
bool try_ugt_y(pvar v, conflict& core, inequality const& c);
|
||||
bool try_ugt_y(pvar v, conflict& core, inequality const& l_y, inequality const& yx_l_zx, pdd const& x, pdd const& z);
|
||||
|
||||
bool try_y_l_ax_and_x_l_z(pvar x, conflict& core, inequality const& c);
|
||||
bool try_y_l_ax_and_x_l_z(pvar x, conflict& core, inequality const& x_l_z, inequality const& y_l_ax, pdd const& a, pdd const& y);
|
||||
|
||||
bool try_ugt_z(pvar z, conflict& core, inequality const& c);
|
||||
bool try_ugt_z(pvar z, conflict& core, inequality const& x_l_z0, inequality const& yz_l_xz, pdd const& y, pdd const& x);
|
||||
|
||||
bool try_parity(pvar x, conflict& core, inequality const& axb_l_y);
|
||||
bool try_parity_diseq(pvar x, conflict& core, inequality const& axb_l_y);
|
||||
bool try_mul_bounds(pvar x, conflict& core, inequality const& axb_l_y);
|
||||
bool try_factor_equality(pvar x, conflict& core, inequality const& a_l_b);
|
||||
bool try_infer_equality(pvar x, conflict& core, inequality const& a_l_b);
|
||||
bool try_mul_eq_1(pvar x, conflict& core, inequality const& axb_l_y);
|
||||
bool try_mul_odd(pvar x, conflict& core, inequality const& axb_l_y);
|
||||
bool try_mul_eq_bound(pvar x, conflict& core, inequality const& axb_l_y);
|
||||
bool try_transitivity(pvar x, conflict& core, inequality const& axb_l_y);
|
||||
bool try_tangent(pvar v, conflict& core, inequality const& c);
|
||||
bool try_add_overflow_bound(pvar x, conflict& core, inequality const& axb_l_y);
|
||||
bool try_add_mul_bound(pvar x, conflict& core, inequality const& axb_l_y);
|
||||
bool try_infer_parity_equality(pvar x, conflict& core, inequality const& a_l_b);
|
||||
bool try_div_monotonicity(conflict& core);
|
||||
|
||||
bool try_nonzero_upper_extract(pvar v, conflict& core, inequality const& i);
|
||||
bool try_congruence(pvar v, conflict& core, inequality const& i);
|
||||
|
||||
|
||||
rational round(rational const& M, rational const& x);
|
||||
bool eval_round(rational const& M, pdd const& p, rational& r);
|
||||
bool extract_linear_form(pdd const& q, pvar& y, rational& a, rational& b);
|
||||
bool extract_bilinear_form(pvar x, pdd const& p, pvar& y, bilinear& b);
|
||||
bool adjust_bound(rational const& x_min, rational const& x_max, rational const& y0, rational const& M,
|
||||
bilinear& b, rational& x_split);
|
||||
bool update_min(rational& y_min, rational const& x_min, rational const& x_max,
|
||||
bilinear const& b);
|
||||
bool update_max(rational& y_max, rational const& x_min, rational const& x_max,
|
||||
bilinear const& b);
|
||||
bool update_bounds_for_xs(rational const& x_min, rational const& x_max, rational& y_min, rational& y_max,
|
||||
rational const& y0, bilinear b1, bilinear b2,
|
||||
rational const& M, inequality const& a_l_b);
|
||||
void fix_values(pvar x, pvar y, pdd const& p);
|
||||
void fix_values(pvar y, pdd const& p);
|
||||
|
||||
|
||||
|
||||
bool is_add_overflow(pvar x, inequality const& i, pdd& y, bool& is_minus);
|
||||
|
||||
bool has_upper_bound(pvar x, conflict& core, rational& bound, vector<signed_constraint>& x_ge_bound);
|
||||
|
||||
bool has_lower_bound(pvar x, conflict& core, rational& bound, vector<signed_constraint>& x_le_bound);
|
||||
|
||||
// inequality i implies x != 0
|
||||
bool is_nonzero_by(pvar x, inequality const& i);
|
||||
|
||||
// determine min/max parity of polynomial
|
||||
unsigned min_parity(pdd const& p, vector<signed_constraint>& explain);
|
||||
unsigned max_parity(pdd const& p, vector<signed_constraint>& explain);
|
||||
unsigned min_parity(pdd const& p) { vector<signed_constraint> ex; return min_parity(p, ex); }
|
||||
unsigned max_parity(pdd const& p) { vector<signed_constraint> ex; return max_parity(p, ex); }
|
||||
|
||||
lbool get_multiple(const pdd& p1, const pdd& p2, pdd& out);
|
||||
|
||||
bool is_forced_eq(pdd const& p, rational const& val);
|
||||
bool is_forced_eq(pdd const& p, int i) { return is_forced_eq(p, rational(i)); }
|
||||
|
||||
bool is_forced_diseq(pdd const& p, rational const& val, signed_constraint& c);
|
||||
bool is_forced_diseq(pdd const& p, int i, signed_constraint& c) { return is_forced_diseq(p, rational(i), c); }
|
||||
|
||||
bool is_forced_odd(pdd const& p, signed_constraint& c);
|
||||
|
||||
bool is_forced_false(signed_constraint const& sc);
|
||||
|
||||
bool is_forced_true(signed_constraint const& sc);
|
||||
|
||||
|
||||
|
||||
bool try_umul_ovfl(pvar v, signed_constraint c);
|
||||
bool try_umul_ovfl_noovfl(pvar v, signed_constraint c);
|
||||
bool try_umul_noovfl_lo(pvar v, signed_constraint c);
|
||||
bool try_umul_noovfl_bounds(pvar v, signed_constraint c);
|
||||
bool try_umul_ovfl_bounds(pvar v, signed_constraint c);
|
||||
|
||||
bool try_op(pvar v, signed_constraint c);
|
||||
#endif
|
||||
|
||||
|
||||
void propagate(pvar v, inequality const& i);
|
||||
void resolve(pvar v, inequality const& i);
|
||||
|
||||
public:
|
||||
saturation(core& c);
|
||||
void propagate(pvar v);
|
||||
bool propagate(pvar v, constraint_id cid);
|
||||
bool resolve(pvar v, constraint_id cid);
|
||||
};
|
||||
}
|
||||
|
|
|
|||
|
|
@ -199,8 +199,11 @@ namespace polysat {
|
|||
unsigned level = 0;
|
||||
for (auto c : core)
|
||||
level = std::max(level, s().lvl(c));
|
||||
if (!eqs.empty()) // over-approximate propagation level if it uses equalities.
|
||||
level = level = s().scope_lvl();
|
||||
sat::literal_vector eqlits;
|
||||
for (auto [n1, n2] : eqs)
|
||||
ctx.get_eq_antecedents(n1, n2, eqlits);
|
||||
for (auto lit : eqlits)
|
||||
level = std::max(level, s().lvl(lit));
|
||||
ctx.propagate(lit, ex);
|
||||
return dependency(lit, level);
|
||||
}
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue