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

add some validation

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-09-07 23:44:30 +02:00
parent d8f0926620
commit eddc03b2eb
3 changed files with 35 additions and 144 deletions
Download patch file Download diff file Expand all files Collapse all files

133
src/math/polysat/explain.cpp
View file

@ -88,62 +88,6 @@ namespace polysat {
// LOG_H3("Attempting to explain conflict for v" << v);
// m_var = v;
// m_cjust_v = cjust;
// for (auto* c : cjust)
// m_conflict.push_back(c);
// for (auto* c : m_conflict.units())
// LOG("Constraint: " << show_deref(c));
// for (auto* c : m_conflict.clauses())
// LOG("Clause: " << show_deref(c));
// // TODO: this is a temporary workaround! we should not get any undef constraints at this point
// constraints_and_clauses confl = std::move(m_conflict);
// SASSERT(m_conflict.empty());
// for (auto* c : confl.units())
// if (!c->is_undef())
// m_conflict.push_back(c);
// for (auto* c : confl.clauses())
// m_conflict.push_back(c);
// // Collect unit constraints
// //
// // TODO: the distinction between units and unit clauses is a bit awkward; maybe it should be removed.
// // We could then also remove the hybrid container 'constraints_and_clauses' by a clause_ref_vector
// SASSERT(m_conflict_units.empty());
// for (constraint* c : m_conflict.units())
// // if (c->is_eq())
// m_conflict_units.push_back(c);
// for (auto clause : m_conflict.clauses()) {
// if (clause->size() == 1) {
// sat::literal lit = (*clause)[0];
// constraint* c = m_solver.m_constraints.lookup(lit.var());
// LOG("unit clause: " << show_deref(c));
// // Morally, a derived unit clause is always asserted at the base level.
// // (Even if we don't want to keep this one around. But maybe we should? Do we want to reconstruct proofs?)
// c->set_unit_clause(clause);
// c->assign(!lit.sign());
// // this clause is really a unit.
// // if (c->is_eq()) {
// m_conflict_units.push_back(c);
// // }
// }
// }
// // TODO: we should share work done for examining constraints between different resolution methods
// clause_ref lemma;
// if (!lemma) lemma = by_polynomial_superposition();
// if (!lemma) lemma = by_ugt_x();
// if (!lemma) lemma = by_ugt_y();
// if (!lemma) lemma = by_ugt_z();
// if (!lemma) lemma = y_ule_ax_and_x_ule_z();
// DEBUG_CODE({
// if (lemma) {
// LOG("New lemma: " << *lemma);
@ -179,81 +123,4 @@ namespace polysat {
// /// [z] z <= y' /\ zx > yx ==> Ω*(x,y') \/ y'x > yx
// /// [z] z <= y' /\ yx <= zx ==> Ω*(x,y') \/ yx <= y'x
// clause_ref conflict_explainer::by_ugt_z() {
// LOG_H3("Try z <= y' && zx > yx where z := v" << m_var);
// pdd const z = m_solver.var(m_var);
// unsigned const sz = m_solver.size(m_var);
// pdd const zero = m_solver.sz2pdd(sz).zero();
// // Collect constraints of shape "z <= _"
// vector<inequality> ds;
// for (auto* d1 : m_conflict.units()) {
// auto d = d1->as_inequality();
// // TODO: a*y where 'a' divides 'x' should also be easy to handle (assuming for now they're numbers)
// // TODO: also z < y' should follow the same pattern.
// if (d.lhs != z)
// continue;
// LOG("z <= y' candidate: " << show_deref(d.src));
// ds.push_back(std::move(d));
// }
// if (ds.empty())
// return nullptr;
// // Find constraint of shape: yx <= zx
// for (auto* c1 : m_conflict.units()) {
// auto c = c1->as_inequality();
// if (c.rhs.degree(m_var) != 1)
// continue;
// pdd x = zero;
// pdd rest = zero;
// c.rhs.factor(m_var, 1, x, rest);
// if (!rest.is_zero())
// continue;
// // TODO: in principle, 'x' could be any polynomial. However, we need to divide the lhs by x, and we don't have general polynomial division yet.
// // so for now we just allow the form 'value*variable'.
// // (extension to arbitrary monomials for 'x' should be fairly easy too)
// if (!x.is_unary())
// continue;
// unsigned x_var = x.var();
// rational x_coeff = x.hi().val();
// pdd xy = zero;
// if (!c.lhs.try_div(x_coeff, xy))
// continue;
// pdd y = zero;
// xy.factor(x_var, 1, y, rest);
// if (!rest.is_zero())
// continue;
// LOG("zx > yx: " << show_deref(c.src));
// // TODO: for now, we just try all ds
// for (auto const& d : ds) {
// unsigned const lvl = std::max(c.src->level(), d.src->level());
// pdd const& y_prime = d.rhs;
// clause_builder clause(m_solver);
// clause.push_literal(~c.src->blit());
// clause.push_literal(~d.src->blit());
// // Omega^*(x, y')
// if (!push_omega_mul(clause, lvl, sz, x, y_prime))
// continue;
// // yx <= y'x
// constraint_literal yx_le_ypx;
// if (c.is_strict || d.is_strict)
// yx_le_ypx = m_solver.m_constraints.ult(lvl, y*x, y_prime*x);
// else
// yx_le_ypx = m_solver.m_constraints.ule(lvl, y*x, y_prime*x);
// LOG("y'x>yx: " << show_deref(yx_le_ypx));
// clause.push_new_constraint(std::move(yx_le_ypx));
// return clause.build();
// }
// }
// return nullptr;
// }
}

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

@ -16,6 +16,11 @@ TODO:
- per calculus it really adds a propagation to the stack
- then it adds the propagated literal to the core and removes the premise that needed to be simplified from core.
TODO: preserve falsification
- each rule selects a certain premise that is problematic,
We assume that problematic premises are false in the current assignment
The derived consequence should also be false in the current assignment to be effective, but simpler so that we can resolve.
TODO:
- remove level information from created constraints.
-
@ -83,7 +88,6 @@ namespace polysat {
}
bool inf_saturate::perform(pvar v, conflict_core& core) {
for (auto c1 : core) {
auto c = c1.as_inequality();
if (try_ugt_x(v, core, c))
@ -209,11 +213,16 @@ namespace polysat {
/*
* Match [x] y <= a*x
*/
bool inf_saturate::is_y_l_ax(pvar x, inequality const& d, pdd& a, pdd& y) {
bool inf_saturate::is_Y_l_Ax(pvar x, inequality const& d, pdd& a, pdd& y) {
y = d.lhs;
return d.rhs.degree(x) == 1 && d.rhs.factor(x, 1, a);
}
bool inf_saturate::verify_Y_l_Ax(pvar x, inequality const& d, pdd const& a, pdd const& y) {
pdd A = a, Y = y;
return is_Y_l_Ax(x, d, A, Y) && a == A && y == Y;
}
/**
* Match [v] v*x <= z*x
*/
@ -240,6 +249,13 @@ namespace polysat {
return true;
}
bool inf_saturate::verify_Xy_l_XZ(pvar v, inequality const& c, pdd const& x, pdd const& z) {
pdd X = x, Z = z;
return is_Xy_l_XZ(v, c, X, Z) && x == X && z == Z;
}
/**
* Match [z] yx <= zx
*/
@ -260,6 +276,11 @@ namespace polysat {
return c.lhs.try_div(x_coeff, xy) && xy.factor(x_var, 1, y);
}
bool inf_saturate::verify_YX_l_zX(pvar z, inequality const& c, pdd const& x, pdd const& y) {
pdd X = x, Y = y;
return is_YX_l_zX(z, c, X, Y) && x == X && y == Y;
}
/// [y] z' <= y /\ zx > yx ==> Ω*(x,y) \/ zx > z'x
/// [y] z' <= y /\ yx <= zx ==> Ω*(x,y) \/ z'x <= zx
bool inf_saturate::try_ugt_y(pvar v, conflict_core& core, inequality const& le_y, inequality const& yx_l_zx, pdd const& x, pdd const& z) {
@ -267,7 +288,7 @@ namespace polysat {
pdd const y = s().var(v);
SASSERT(is_l_v(v, le_y));
// SASSERT(is_yx_l_zx(v, yx_l_zx, x, z));
SASSERT(verify_Xy_l_XZ(v, yx_l_zx, x, z));
unsigned const lvl = std::max(yx_l_zx.src->level(), le_y.src->level());
pdd const& z_prime = le_y.lhs;
@ -308,7 +329,7 @@ namespace polysat {
pdd a = y;
for (auto dd : core) {
auto d = dd.as_inequality();
if (is_y_l_ax(x, d, a, y) && try_y_l_ax_and_x_l_z(x, core, c, d, a, y))
if (is_Y_l_Ax(x, d, a, y) && try_y_l_ax_and_x_l_z(x, core, c, d, a, y))
return true;
}
return false;
@ -317,7 +338,7 @@ namespace polysat {
bool inf_saturate::try_y_l_ax_and_x_l_z(pvar x, conflict_core& core, inequality const& x_l_z, inequality const& y_l_ax, pdd const& a, pdd const& y) {
SASSERT(is_g_v(x, x_l_z));
// SASSERT(is_y_l_ax(x, y_l_ax, a, y));
SASSERT(verify_Y_l_Ax(x, y_l_ax, a, y));
LOG_H3("Try y <= ax && x <= z where x := v" << x);
pdd z = x_l_z.rhs;
@ -356,7 +377,7 @@ namespace polysat {
bool inf_saturate::try_ugt_z(pvar z, conflict_core& core, inequality const& c, inequality const& d, pdd const& x, pdd const& y) {
LOG_H3("Try z <= y' && zx > yx where z := v" << z);
SASSERT(is_g_v(z, c));
// SASSERT(is_YX_l_zX(x, d, x, y));
SASSERT(verify_YX_l_zX(z, d, x, y));
unsigned const lvl = std::max(c.src->level(), d.src->level());
pdd const& y_prime = c.rhs;

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

@ -43,7 +43,9 @@ namespace polysat {
class inf_saturate : public inference_engine {
bool push_omega_mul(conflict_core& core, unsigned level, pdd const& x, pdd const& y);
void push_l(conflict_core& core, unsigned level, bool strict, pdd const& lhs, pdd const& rhs);
bool try_ugt_x(pvar v, conflict_core& core, inequality const& c);
bool try_ugt_y(pvar v, conflict_core& core, inequality const& c);
bool try_ugt_y(pvar v, conflict_core& core, inequality const& l_y, inequality const& yx_l_zx, pdd const& x, pdd const& z);
@ -62,20 +64,21 @@ namespace polysat {
// c := X*y ~ X*Z
bool is_Xy_l_XZ(pvar y, inequality const& c, pdd& x, pdd& z);
bool verify_Xy_l_XZ(pvar y, inequality const& c, pdd const& x, pdd const& z);
// c := Y ~ Ax
bool is_y_l_ax(pvar x, inequality const& d, pdd& a, pdd& y);
bool is_Y_l_Ax(pvar x, inequality const& d, pdd& a, pdd& y);
bool verify_Y_l_Ax(pvar x, inequality const& d, pdd const& a, pdd const& y);
// c := Y*X ~ z*X
bool is_YX_l_zX(pvar z, inequality const& c, pdd& x, pdd& y);
bool verify_YX_l_zX(pvar z, inequality const& c, pdd const& x, pdd const& y);
public:
bool perform(pvar v, conflict_core& core) override;
};
// TODO: other rules
// clause_ref by_ugt_z();
/*
* TODO: we could resolve constraints in cjust[v] against each other to
* obtain stronger propagation. Example: