mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

provide access to saturation for selected constraints

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-12-08 19:17:35 -08:00
parent 33902c7c9e
commit a6b49d8b4e
3 changed files with 44 additions and 30 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/math/polysat/conflict.cpp
View file

@ -73,6 +73,10 @@ namespace polysat {
(void)m_saturation.perform(v, core);
}
void infer_lemmas_for_value(pvar v, signed_constraint const& c, conflict& core) {
(void)m_saturation.perform(v, c, core);
}
// Analyse current conflict core to extract additional lemmas
void find_extra_lemmas(conflict& core) {
m_free_variable_elimination.find_lemma(core);
@ -381,10 +385,15 @@ namespace polysat {
#endif
if (!has_decision) {
for (pvar v : c->vars()) {
if (s.is_assigned(v) && s.get_level(v) <= lvl) {
m_vars.insert(v);
// TODO - figure out what to do with constraints from conflict lemma that disappear here.
// if (s.m_bvars.is_false(lit))
// m_resolver->infer_lemmas_for_value(v, ~c, *this);
}
}
remove(c);
for (pvar v : c->vars())
if (s.is_assigned(v) && s.get_level(v) <= lvl)
m_vars.insert(v);
}
SASSERT(!contains(lit));

56
src/math/polysat/saturation.cpp
View file

@ -32,30 +32,35 @@ namespace polysat {
saturation::saturation(solver& s) : s(s), m_lemma(s) {}
bool saturation::perform(pvar v, conflict& core) {
for (auto c : core) {
if (!c->is_ule())
continue;
if (c.is_currently_true(s))
continue;
auto i = inequality::from_ule(c);
if (try_mul_bounds(v, core, i))
return true;
if (try_parity(v, core, i))
return true;
if (try_factor_equality(v, core, i))
return true;
if (try_ugt_x(v, core, i))
return true;
if (try_ugt_y(v, core, i))
return true;
if (try_ugt_z(v, core, i))
return true;
if (try_y_l_ax_and_x_l_z(v, core, i))
return true;
if (try_tangent(v, core, i))
return true;
}
void saturation::perform(pvar v, conflict& core) {
for (auto c : core)
if (perform(v, c, core))
return;
}
bool saturation::perform(pvar v, signed_constraint const& c, conflict& core) {
IF_VERBOSE(0, verbose_stream() << v << " " << c << " " << c.is_currently_true(s) << "\n");
if (!c->is_ule())
return false;
if (c.is_currently_true(s))
return false;
auto i = inequality::from_ule(c);
if (try_mul_bounds(v, core, i))
return true;
if (try_parity(v, core, i))
return true;
if (try_factor_equality(v, core, i))
return true;
if (try_ugt_x(v, core, i))
return true;
if (try_ugt_y(v, core, i))
return true;
if (try_ugt_z(v, core, i))
return true;
if (try_y_l_ax_and_x_l_z(v, core, i))
return true;
if (try_tangent(v, core, i))
return true;
return false;
}
@ -66,7 +71,6 @@ namespace polysat {
return s.ule(lhs, rhs);
}
bool saturation::propagate(conflict& core, inequality const& crit, signed_constraint c) {
if (is_forced_true(c))
return false;
@ -635,7 +639,7 @@ namespace polysat {
bool saturation::try_parity(pvar x, conflict& core, inequality const& axb_l_y) {
set_rule("[x] a*x + b = 0 => (odd(a) & odd(x) <=> odd(b))");
// IF_VERBOSE(0, verbose_stream() << "try parity " << axb_l_y.as_signed_constraint() << "\n");
IF_VERBOSE(0, verbose_stream() << "try parity " << axb_l_y.as_signed_constraint() << "\n");
auto& m = s.var2pdd(x);
unsigned N = m.power_of_2();
pdd y = m.zero();

3
src/math/polysat/saturation.h
View file

@ -113,7 +113,8 @@ namespace polysat {
public:
saturation(solver& s);
bool perform(pvar v, conflict& core);
void perform(pvar v, conflict& core);
bool perform(pvar v, signed_constraint const& sc, conflict& core);
};
/*