mirror of
https://github.com/Z3Prover/z3
synced 2025-04-23 09:05:31 +00:00
move all saturation functionality into saturation.cpp, differentiate basic multiplication by -1, 1 from other powers of 2.
This commit is contained in:
Nikolaj Bjorner
parent
7bd7faa722
commit
483508d257
6 changed files with 68 additions and 38 deletions
|
|
@ -199,57 +199,52 @@ namespace polysat {
|
|||
}
|
||||
|
||||
sat::check_result core::final_check() {
|
||||
unsigned n = 0;
|
||||
constraint_id conflict_idx = { UINT_MAX };
|
||||
|
||||
lbool r = l_true;
|
||||
switch (m_monomials.refine()) {
|
||||
case l_true:
|
||||
break;
|
||||
case l_false:
|
||||
return sat::check_result::CR_CONTINUE;
|
||||
case l_undef:
|
||||
r = l_undef;
|
||||
break;
|
||||
}
|
||||
|
||||
for (auto idx : m_prop_queue) {
|
||||
auto [sc, d, value] = m_constraint_index[idx.id];
|
||||
SASSERT(value != l_undef);
|
||||
// verbose_stream() << "constraint " << (value == l_true ? sc : ~sc) << "\n";
|
||||
lbool eval_value = eval_unfold(sc);
|
||||
CTRACE("bv", eval_value == l_undef, sc.display(tout << "eval: ") << " evaluates to " << eval_value << "\n"; display(tout););
|
||||
SASSERT(eval_value != l_undef);
|
||||
if (eval_value == value)
|
||||
continue;
|
||||
// verbose_stream() << "violated " << sc << " " << d << " " << eval_value << "\n";
|
||||
if (0 == (m_rand() % (++n)))
|
||||
conflict_idx = idx;
|
||||
|
||||
auto vars = find_conflict_variables(idx);
|
||||
saturation sat(*this);
|
||||
for (auto v : vars)
|
||||
if (sat.resolve(v, idx))
|
||||
return sat::check_result::CR_CONTINUE;
|
||||
saturation saturate(*this);
|
||||
switch (saturate()) {
|
||||
case l_true:
|
||||
break;
|
||||
case l_false:
|
||||
return sat::check_result::CR_CONTINUE;
|
||||
case l_undef:
|
||||
r = l_undef;
|
||||
break;
|
||||
}
|
||||
|
||||
// If all constraints evaluate to true, we are done.
|
||||
if (conflict_idx.is_null())
|
||||
return sat::check_result::CR_DONE;
|
||||
|
||||
switch (m_monomials.bit_blast()) {
|
||||
case l_true:
|
||||
break;
|
||||
case l_false:
|
||||
return sat::check_result::CR_CONTINUE;
|
||||
case l_undef:
|
||||
r = l_undef;
|
||||
break;
|
||||
}
|
||||
|
||||
|
||||
if (r == l_true)
|
||||
return sat::check_result::CR_DONE;
|
||||
|
||||
return sat::check_result::CR_GIVEUP;
|
||||
|
||||
#if 0
|
||||
// If no saturation propagation was possible, explain the conflict using the variable assignment.
|
||||
m_unsat_core = explain_eval_unfold(get_constraint(conflict_idx));
|
||||
m_unsat_core.push_back(get_dependency(conflict_idx));
|
||||
s.set_conflict(m_unsat_core, "polysat-bail-out-conflict");
|
||||
decay_activity();
|
||||
return sat::check_result::CR_CONTINUE;
|
||||
#endif
|
||||
}
|
||||
|
||||
/**
|
||||
|
|
|
|||
|
|
@ -91,7 +91,7 @@ namespace polysat {
|
|||
void add_watch(unsigned idx, unsigned var);
|
||||
|
||||
sat::check_result final_check();
|
||||
svector<pvar> find_conflict_variables(constraint_id idx);
|
||||
|
||||
|
||||
void add_axiom(signed_constraint sc);
|
||||
|
||||
|
|
@ -175,6 +175,7 @@ namespace polysat {
|
|||
lbool eval_unfold(signed_constraint const& sc);
|
||||
dependency_vector explain_eval(signed_constraint const& sc);
|
||||
dependency_vector explain_eval_unfold(signed_constraint const& sc);
|
||||
svector<pvar> find_conflict_variables(constraint_id idx);
|
||||
bool inconsistent() const;
|
||||
|
||||
/*
|
||||
|
|
|
|||
|
|
@ -98,6 +98,8 @@ namespace polysat {
|
|||
shuffle(m_to_refine.size(), m_to_refine.data(), c.rand());
|
||||
if (any_of(m_to_refine, [&](auto i) { return mul0(m_monomials[i]); }))
|
||||
return l_false;
|
||||
if (any_of(m_to_refine, [&](auto i) { return mul1(m_monomials[i]); }))
|
||||
return l_false;
|
||||
if (any_of(m_to_refine, [&](auto i) { return non_overflow_unit(m_monomials[i]); }))
|
||||
return l_false;
|
||||
if (any_of(m_to_refine, [&](auto i) { return parity0(m_monomials[i]); }))
|
||||
|
|
@ -159,13 +161,24 @@ namespace polysat {
|
|||
return false;
|
||||
}
|
||||
|
||||
// check p = 1 => p * q = q, p = -1 => p * q = -q
|
||||
bool monomials::mul1(monomial const& mon) {
|
||||
auto& m = mon.args[0].manager();
|
||||
return mul(mon, [&](rational const& r) { return r == m.max_value() || r == 1; });
|
||||
}
|
||||
|
||||
// check p = k => p * q = k * q
|
||||
bool monomials::mulp2(monomial const& mon) {
|
||||
auto& m = mon.args[0].manager();
|
||||
return mul(mon, [&](rational const& r) { return r == m.max_value() || r.is_power_of_two(); });
|
||||
}
|
||||
|
||||
bool monomials::mul(monomial const& mon, std::function<bool(rational const&)> const& p) {
|
||||
unsigned free_index = UINT_MAX;
|
||||
auto& m = mon.args[0].manager();
|
||||
for (unsigned j = mon.size(); j-- > 0; ) {
|
||||
auto const& arg_val = mon.arg_vals[j];
|
||||
if (arg_val == m.max_value() || arg_val.is_power_of_two())
|
||||
if (p(arg_val))
|
||||
continue;
|
||||
if (free_index != UINT_MAX)
|
||||
return false;
|
||||
|
|
@ -183,7 +196,7 @@ namespace polysat {
|
|||
cs.push_back(C.eq(mon.var, offset));
|
||||
else
|
||||
cs.push_back(C.eq(mon.var, offset * mon.args[free_index]));
|
||||
|
||||
|
||||
c.add_axiom("p = k => p * q = k * q", cs, true);
|
||||
return true;
|
||||
}
|
||||
|
|
@ -283,8 +296,8 @@ namespace polysat {
|
|||
auto x = mon.args[0].var();
|
||||
auto y = mon.args[1].var();
|
||||
offset_slices x_suffixes, y_suffixes;
|
||||
c.get_bitvector_suffixes(x, x_suffixes);
|
||||
c.get_bitvector_suffixes(y, y_suffixes);
|
||||
bool y_computed = false;
|
||||
c.get_bitvector_suffixes(x, x_suffixes);
|
||||
rational x_val, y_val;
|
||||
for (auto const& xslice : x_suffixes) {
|
||||
if (c.size(xslice.v) == mon.num_bits())
|
||||
|
|
@ -294,6 +307,9 @@ namespace polysat {
|
|||
continue;
|
||||
if (!c.try_eval(c.var(xslice.v), x_val) || x_val != mon.arg_vals[0])
|
||||
continue;
|
||||
if (!y_computed)
|
||||
c.get_bitvector_suffixes(y, y_suffixes);
|
||||
y_computed = true;
|
||||
for (auto const& yslice : y_suffixes) {
|
||||
if (c.size(yslice.v) != c.size(xslice.v))
|
||||
continue;
|
||||
|
|
|
|||
|
|
@ -71,7 +71,9 @@ namespace polysat {
|
|||
bool eval_to_false(unsigned i);
|
||||
|
||||
bool mul0(monomial const& mon);
|
||||
bool mul1(monomial const& mon);
|
||||
bool mulp2(monomial const& mon);
|
||||
bool mul(monomial const& mon, std::function<bool(rational const&)> const& p);
|
||||
bool parity(monomial const& mon);
|
||||
bool non_overflow_monotone(monomial const& mon);
|
||||
bool non_overflow_unit(monomial const& mon);
|
||||
|
|
|
|||
|
|
@ -27,13 +27,34 @@ TODO: when we check that 'x' is "unary":
|
|||
#include "sat/smt/polysat/saturation.h"
|
||||
#include "sat/smt/polysat/umul_ovfl_constraint.h"
|
||||
#include "sat/smt/polysat/ule_constraint.h"
|
||||
#include "util/log.h"
|
||||
|
||||
|
||||
namespace polysat {
|
||||
|
||||
saturation::saturation(core& c) : c(c), C(c.cs()) {}
|
||||
|
||||
lbool saturation::operator()() {
|
||||
bool has_conflict = false;
|
||||
for (auto idx : c.assigned_constraints()) {
|
||||
auto sc = c.get_constraint(idx);
|
||||
lbool eval_value = c.eval_unfold(sc);
|
||||
if (eval_value == l_true)
|
||||
continue;
|
||||
|
||||
TRACE("bv", sc.display(tout << "eval: ") << " evaluates to " << eval_value << "\n");
|
||||
SASSERT(eval_value != l_undef);
|
||||
|
||||
has_conflict = true;
|
||||
auto vars = c.find_conflict_variables(idx);
|
||||
for (auto v : vars)
|
||||
if (resolve(v, idx))
|
||||
return l_false;
|
||||
}
|
||||
if (has_conflict)
|
||||
return l_undef;
|
||||
return l_true;
|
||||
}
|
||||
|
||||
bool saturation::resolve(pvar v, constraint_id id) {
|
||||
if (c.eval_unfold(id) == l_true)
|
||||
return false;
|
||||
|
|
@ -59,10 +80,6 @@ namespace polysat {
|
|||
try_ugt_z(v, i);
|
||||
}
|
||||
|
||||
void saturation::propagate(signed_constraint const& sc, std::initializer_list<constraint_id> const& premises) {
|
||||
// c.propagate(sc, constraint_id_vector(premises));
|
||||
}
|
||||
|
||||
void saturation::add_clause(char const* name, clause const& cs, bool is_redundant) {
|
||||
vector<constraint_or_dependency> lemma;
|
||||
for (auto const& e : cs) {
|
||||
|
|
|
|||
|
|
@ -29,7 +29,6 @@ namespace polysat {
|
|||
core& c;
|
||||
constraints& C;
|
||||
|
||||
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 {
|
||||
|
|
@ -62,7 +61,6 @@ namespace polysat {
|
|||
|
||||
bool match_constraints(std::function<bool(signed_constraint const& sc)> const& p, constraint_id& id);
|
||||
|
||||
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);
|
||||
|
|
@ -71,9 +69,10 @@ namespace polysat {
|
|||
signed_constraint ineq(bool is_strict, pdd const& x, pdd const& y);
|
||||
|
||||
void resolve(pvar v, inequality const& i);
|
||||
bool resolve(pvar v, constraint_id cid);
|
||||
|
||||
public:
|
||||
saturation(core& c);
|
||||
bool resolve(pvar v, constraint_id cid);
|
||||
lbool operator()();
|
||||
};
|
||||
}
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue