mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 03:32:28 +00:00
Code Activity
z3/src/nlsat/nlsat_explain.cpp
Lev Nachmanson f8a1f98fce try Lazard project 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-10-26 12:15:50 -07:00

2286 lines
88 KiB
C++
Raw Blame History

/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
nlsat_explain.cpp
Abstract:
Functor that implements the "explain" procedure defined in Dejan and Leo's paper.
Author:
Leonardo de Moura (leonardo) 2012-01-13.
Revision History:
--*/
#include "nlsat/nlsat_explain.h"
#include "nlsat/nlsat_assignment.h"
#include "nlsat/nlsat_evaluator.h"
#include "math/polynomial/algebraic_numbers.h"
#include "util/ref_buffer.h"
namespace nlsat {
typedef polynomial::polynomial_ref_vector polynomial_ref_vector;
typedef ref_buffer<poly, pmanager> polynomial_ref_buffer;
struct explain::imp {
solver & m_solver;
assignment const & m_assignment;
atom_vector const & m_atoms;
atom_vector const & m_x2eq;
anum_manager & m_am;
polynomial::cache & m_cache;
pmanager & m_pm;
polynomial_ref_vector m_ps;
polynomial_ref_vector m_ps2;
polynomial_ref_vector m_psc_tmp;
polynomial_ref_vector m_factors, m_factors_save;
scoped_anum_vector m_roots_tmp;
bool m_simplify_cores;
bool m_full_dimensional;
bool m_minimize_cores;
bool m_factor;
bool m_add_all_coeffs;
bool m_signed_project;
bool m_cell_sample;
bool m_lazard;
struct todo_set {
polynomial::cache & m_cache;
polynomial_ref_vector m_set;
svector<char> m_in_set;
todo_set(polynomial::cache & u):m_cache(u), m_set(u.pm()) {}
void reset() {
pmanager & pm = m_set.m();
unsigned sz = m_set.size();
for (unsigned i = 0; i < sz; i++) {
m_in_set[pm.id(m_set.get(i))] = false;
}
m_set.reset();
}
void insert(poly * p) {
pmanager & pm = m_set.m();
p = m_cache.mk_unique(p);
unsigned pid = pm.id(p);
if (m_in_set.get(pid, false))
return;
m_in_set.setx(pid, true, false);
m_set.push_back(p);
}
bool empty() const { return m_set.empty(); }
// Return max variable in todo_set
var max_var() const {
pmanager & pm = m_set.m();
var max = null_var;
unsigned sz = m_set.size();
for (unsigned i = 0; i < sz; i++) {
var x = pm.max_var(m_set.get(i));
SASSERT(x != null_var);
if (max == null_var || x > max)
max = x;
}
return max;
}
/**
\brief Remove the maximal polynomials from the set and store
them in max_polys. Return the maximal variable
*/
var extract_max_polys(polynomial_ref_vector & max_polys) {
max_polys.reset();
var x = max_var();
pmanager & pm = m_set.m();
unsigned sz = m_set.size();
unsigned j = 0;
for (unsigned i = 0; i < sz; i++) {
poly * p = m_set.get(i);
var y = pm.max_var(p);
SASSERT(y <= x);
if (y == x) {
max_polys.push_back(p);
m_in_set[pm.id(p)] = false;
}
else {
m_set.set(j, p);
j++;
}
}
m_set.shrink(j);
return x;
}
};
// temporary field for store todo set of polynomials
todo_set m_todo;
// temporary fields for preprocessing core
scoped_literal_vector m_core1;
scoped_literal_vector m_core2;
// temporary fields for storing the result
scoped_literal_vector * m_result = nullptr;
svector<char> m_already_added_literal;
evaluator & m_evaluator;
imp(solver & s, assignment const & x2v, polynomial::cache & u, atom_vector const & atoms, atom_vector const & x2eq,
evaluator & ev, bool is_sample, bool use_lazard):
m_solver(s),
m_assignment(x2v),
m_atoms(atoms),
m_x2eq(x2eq),
m_am(x2v.am()),
m_cache(u),
m_pm(u.pm()),
m_ps(m_pm),
m_ps2(m_pm),
m_psc_tmp(m_pm),
m_factors(m_pm),
m_factors_save(m_pm),
m_roots_tmp(m_am),
m_cell_sample(is_sample),
m_lazard(use_lazard),
m_todo(u),
m_core1(s),
m_core2(s),
m_evaluator(ev) {
m_simplify_cores = false;
m_full_dimensional = false;
m_minimize_cores = false;
m_add_all_coeffs = true;
m_signed_project = false;
}
std::ostream& display(std::ostream & out, polynomial_ref const & p) const {
m_pm.display(out, p, m_solver.display_proc());
return out;
}
std::ostream& display(std::ostream & out, polynomial_ref_vector const & ps, char const * delim = "\n") const {
for (unsigned i = 0; i < ps.size(); i++) {
if (i > 0)
out << delim;
m_pm.display(out, ps.get(i), m_solver.display_proc());
}
return out;
}
std::ostream& display(std::ostream & out, literal l) const { return m_solver.display(out, l); }
std::ostream& display_var(std::ostream & out, var x) const { return m_solver.display(out, x); }
std::ostream& display(std::ostream & out, unsigned sz, literal const * ls) const { return m_solver.display(out, sz, ls); }
std::ostream& display(std::ostream & out, literal_vector const & ls) const { return display(out, ls.size(), ls.data()); }
std::ostream& display(std::ostream & out, scoped_literal_vector const & ls) const { return display(out, ls.size(), ls.data()); }
/**
\brief Add literal to the result vector.
*/
void add_literal(literal l) {
SASSERT(m_result != 0);
SASSERT(l != true_literal);
if (l == false_literal)
return;
unsigned lidx = l.index();
if (m_already_added_literal.get(lidx, false))
return;
TRACE(nlsat_explain, tout << "adding literal: " << lidx << "\n"; m_solver.display(tout, l) << "\n";);
m_already_added_literal.setx(lidx, true, false);
m_result->push_back(l);
}
/**
\brief Reset m_already_added vector using m_result
*/
void reset_already_added() {
SASSERT(m_result != nullptr);
for (literal lit : *m_result)
m_already_added_literal[lit.index()] = false;
SASSERT(check_already_added());
}
/**
\brief evaluate the given polynomial in the current interpretation.
max_var(p) must be assigned in the current interpretation.
*/
::sign sign(polynomial_ref const & p) {
SASSERT(max_var(p) == null_var || m_assignment.is_assigned(max_var(p)));
auto s = m_am.eval_sign_at(p, m_assignment);
TRACE(nlsat_explain, tout << "p: " << p << " var: " << max_var(p) << " sign: " << s << "\n";);
return s;
}
/**
\brief Wrapper for factorization
*/
void factor(polynomial_ref & p, polynomial_ref_vector & fs) {
// TODO: add params, caching
TRACE(nlsat_factor, tout << "factor\n" << p << "\n";);
fs.reset();
m_cache.factor(p.get(), fs);
}
/**
\brief Wrapper for psc chain computation
*/
void psc_chain(polynomial_ref & p, polynomial_ref & q, unsigned x, polynomial_ref_vector & result) {
// TODO caching
SASSERT(max_var(p) == max_var(q));
SASSERT(max_var(p) == x);
m_cache.psc_chain(p, q, x, result);
}
/**
\brief Store in ps the polynomials occurring in the given literals.
*/
void collect_polys(unsigned num, literal const * ls, polynomial_ref_vector & ps) {
ps.reset();
for (unsigned i = 0; i < num; i++) {
atom * a = m_atoms[ls[i].var()];
SASSERT(a != 0);
if (a->is_ineq_atom()) {
unsigned sz = to_ineq_atom(a)->size();
for (unsigned j = 0; j < sz; j++)
ps.push_back(to_ineq_atom(a)->p(j));
}
else {
ps.push_back(to_root_atom(a)->p());
}
}
}
/**
\brief Add literal p != 0 into m_result.
*/
ptr_vector<poly> m_zero_fs;
bool_vector m_is_even;
struct restore_factors {
polynomial_ref_vector& m_factors, &m_factors_save;
unsigned num_saved = 0;
restore_factors(polynomial_ref_vector&f, polynomial_ref_vector& fs):
m_factors(f), m_factors_save(fs)
{
num_saved = m_factors_save.size();
m_factors_save.append(m_factors);
}
~restore_factors() {
m_factors.reset();
m_factors.append(m_factors_save.size() - num_saved, m_factors_save.data() + num_saved);
m_factors_save.shrink(num_saved);
}
};
void add_zero_assumption(polynomial_ref& p) {
// If p is of the form p1^n1 * ... * pk^nk,
// then only the factors that are zero in the current interpretation needed to be considered.
// I don't want to create a nested conjunction in the clause.
// Then, I assert p_i1 * ... * p_im != 0
{
restore_factors _restore(m_factors, m_factors_save);
factor(p, m_factors);
unsigned num_factors = m_factors.size();
m_zero_fs.reset();
m_is_even.reset();
polynomial_ref f(m_pm);
for (unsigned i = 0; i < num_factors; i++) {
f = m_factors.get(i);
if (is_zero(sign(f))) {
m_zero_fs.push_back(m_factors.get(i));
m_is_even.push_back(false);
}
}
}
SASSERT(!m_zero_fs.empty()); // one of the factors must be zero in the current interpretation, since p is zero in it.
literal l = m_solver.mk_ineq_literal(atom::EQ, m_zero_fs.size(), m_zero_fs.data(), m_is_even.data());
l.neg();
TRACE(nlsat_explain, tout << "adding (zero assumption) literal:\n"; display(tout, l); tout << "\n";);
add_literal(l);
}
void add_simple_assumption(atom::kind k, poly * p, bool sign = false) {
SASSERT(k == atom::EQ || k == atom::LT || k == atom::GT);
bool is_even = false;
bool_var b = m_solver.mk_ineq_atom(k, 1, &p, &is_even);
literal l(b, !sign);
add_literal(l);
}
void add_assumption(atom::kind k, poly * p, bool sign = false) {
// TODO: factor
add_simple_assumption(k, p, sign);
}
/**
\brief Eliminate "vanishing leading coefficients" of p.
That is, coefficients that vanish in the current
interpretation. The resultant p is a reduct of p s.t. its
leading coefficient does not vanish in the current
interpretation. If all coefficients of p vanish, then
the resultant p is the zero polynomial.
*/
void elim_vanishing(polynomial_ref & p) {
SASSERT(!is_const(p));
var x = max_var(p);
unsigned k = degree(p, x);
SASSERT(k > 0);
polynomial_ref lc(m_pm);
polynomial_ref reduct(m_pm);
while (true) {
if (is_const(p))
return;
if (k == 0) {
// x vanished from p, peek next maximal variable
x = max_var(p);
SASSERT(x != null_var);
k = degree(p, x);
}
if (m_pm.nonzero_const_coeff(p, x, k)) {
TRACE(nlsat_explain, tout << "nonzero const x" << x << "\n";);
return; // lc is a nonzero constant
}
lc = m_pm.coeff(p, x, k, reduct);
TRACE(nlsat_explain, tout << "lc: " << lc << " reduct: " << reduct << "\n";);
if (!is_zero(lc)) {
if (!::is_zero(sign(lc))) {
TRACE(nlsat_explain, tout << "lc does no vaninsh\n";);
return;
}
TRACE(nlsat_explain, tout << "got a zero sign on lc\n";);
// lc is not the zero polynomial, but it vanished in the current interpretation.
// so we keep searching...
TRACE(nlsat_explain, tout << "adding zero assumption for var:"; m_solver.display_var(tout, x); tout << ", degree k:" << k << ", p:" ; display(tout, p) << "\n";);
add_zero_assumption(lc);
}
if (k == 0) {
// all coefficients of p vanished in the current interpretation,
// and were added as assumptions.
p = m_pm.mk_zero();
TRACE(nlsat_explain, tout << "all coefficients of p vanished\n";);
return;
}
k--;
p = reduct;
}
}
/**
Eliminate vanishing coefficients of polynomials in ps.
The coefficients that are zero (i.e., vanished) are added
as assumptions into m_result.
*/
void elim_vanishing(polynomial_ref_vector & ps) {
unsigned j = 0;
unsigned sz = ps.size();
polynomial_ref p(m_pm);
for (unsigned i = 0; i < sz; i++) {
p = ps.get(i);
elim_vanishing(p);
if (!is_const(p)) {
ps.set(j, p);
j++;
}
}
ps.shrink(j);
}
/**
Normalize literal with respect to given maximal variable.
The basic idea is to eliminate vanishing (leading) coefficients from a (arithmetic) literal,
and factors from lower stages.
The vanishing coefficients and factors from lower stages are added as assumptions to the lemma
being generated.
Example 1)
Assume
- l is of the form (y^2 - 2)*x^3 + y*x + 1 > 0
- x is the maximal variable
- y is assigned to sqrt(2)
Thus, (y^2 - 2) the coefficient of x^3 vanished. This method returns
y*x + 1 > 0 and adds the assumption (y^2 - 2) = 0 to the lemma
Example 2)
Assume
- l is of the form (x + 2)*(y - 1) > 0
- x is the maximal variable
- y is assigned to 0
(x + 2) < 0 is returned and assumption (y - 1) < 0 is added as an assumption.
Remark: root atoms are not normalized
*/
literal normalize(literal l, var max) {
bool_var b = l.var();
if (b == true_bool_var)
return l;
SASSERT(m_atoms[b] != 0);
if (m_atoms[b]->is_ineq_atom()) {
polynomial_ref_buffer ps(m_pm);
sbuffer<bool> is_even;
polynomial_ref p(m_pm);
ineq_atom * a = to_ineq_atom(m_atoms[b]);
int atom_sign = 1;
unsigned sz = a->size();
bool normalized = false; // true if the literal needs to be normalized
for (unsigned i = 0; i < sz; i++) {
p = a->p(i);
if (max_var(p) == max)
elim_vanishing(p); // eliminate vanishing coefficients of max
if (is_const(p) || max_var(p) < max) {
int s = sign(p);
if (!is_const(p)) {
SASSERT(max_var(p) != null_var);
SASSERT(max_var(p) < max);
// factor p is a lower stage polynomial, so we should add assumption to justify p being eliminated
if (s == 0)
add_simple_assumption(atom::EQ, p); // add assumption p = 0
else if (a->is_even(i))
add_simple_assumption(atom::EQ, p, true); // add assumption p != 0
else if (s < 0)
add_simple_assumption(atom::LT, p); // add assumption p < 0
else
add_simple_assumption(atom::GT, p); // add assumption p > 0
}
if (s == 0) {
bool atom_val = a->get_kind() == atom::EQ;
bool lit_val = l.sign() ? !atom_val : atom_val;
return lit_val ? true_literal : false_literal;
}
else if (s < 0 && a->is_odd(i)) {
atom_sign = -atom_sign;
}
normalized = true;
}
else {
if (p != a->p(i)) {
SASSERT(!m_pm.eq(p, a->p(i)));
normalized = true;
}
is_even.push_back(a->is_even(i));
ps.push_back(p);
}
}
if (ps.empty()) {
SASSERT(atom_sign != 0);
// LHS is positive or negative. It is positive if atom_sign > 0 and negative if atom_sign < 0
bool atom_val;
if (a->get_kind() == atom::EQ)
atom_val = false;
else if (a->get_kind() == atom::LT)
atom_val = atom_sign < 0;
else
atom_val = atom_sign > 0;
bool lit_val = l.sign() ? !atom_val : atom_val;
return lit_val ? true_literal : false_literal;
}
else if (normalized) {
atom::kind new_k = a->get_kind();
if (atom_sign < 0)
new_k = atom::flip(new_k);
literal new_l = m_solver.mk_ineq_literal(new_k, ps.size(), ps.data(), is_even.data());
if (l.sign())
new_l.neg();
return new_l;
}
else {
SASSERT(atom_sign > 0);
return l;
}
}
else {
return l;
}
}
/**
Normalize literals (in the conflicting core) with respect
to given maximal variable. The basic idea is to eliminate
vanishing (leading) coefficients (and factors from lower
stages) from (arithmetic) literals,
*/
void normalize(scoped_literal_vector & C, var max) {
unsigned sz = C.size();
unsigned j = 0;
for (unsigned i = 0; i < sz; i++) {
literal new_l = normalize(C[i], max);
if (new_l == true_literal)
continue;
if (new_l == false_literal) {
// false literal was created. The assumptions added are sufficient for implying the conflict.
C.reset();
return;
}
C.set(j, new_l);
j++;
}
C.shrink(j);
}
var max_var(poly const * p) { return m_pm.max_var(p); }
/**
\brief Return the maximal variable in a set of nonconstant polynomials.
*/
var max_var(polynomial_ref_vector const & ps) {
if (ps.empty())
return null_var;
var max = max_var(ps.get(0));
SASSERT(max != null_var); // there are no constant polynomials in ps
unsigned sz = ps.size();
for (unsigned i = 1; i < sz; i++) {
var curr = m_pm.max_var(ps.get(i));
SASSERT(curr != null_var);
if (curr > max)
max = curr;
}
return max;
}
polynomial::var max_var(literal l) {
atom * a = m_atoms[l.var()];
if (a != nullptr)
return a->max_var();
else
return null_var;
}
/**
\brief Return the maximal variable in the given set of literals
*/
var max_var(unsigned sz, literal const * ls) {
var max = null_var;
for (unsigned i = 0; i < sz; i++) {
literal l = ls[i];
atom * a = m_atoms[l.var()];
if (a != nullptr) {
var x = a->max_var();
SASSERT(x != null_var);
if (max == null_var || x > max)
max = x;
}
}
return max;
}
/**
\brief Move the polynomials in q in ps that do not contain x to qs.
*/
void keep_p_x(polynomial_ref_vector & ps, var x, polynomial_ref_vector & qs) {
unsigned sz = ps.size();
unsigned j = 0;
for (unsigned i = 0; i < sz; i++) {
poly * q = ps.get(i);
if (max_var(q) != x) {
qs.push_back(q);
}
else {
ps.set(j, q);
j++;
}
}
ps.shrink(j);
}
/**
\brief Add factors of p to todo
*/
void insert_fresh_factors_in_todo(polynomial_ref & p) {
if (is_const(p))
return;
elim_vanishing(p);
if (is_const(p))
return;
if (m_factor) {
restore_factors _restore(m_factors, m_factors_save);
factor(p, m_factors);
TRACE(nlsat_explain, display(tout << "adding factors of\n", p); tout << "\n" << m_factors << "\n";);
polynomial_ref f(m_pm);
for (unsigned i = 0; i < m_factors.size(); i++) {
f = m_factors.get(i);
elim_vanishing(f);
if (!is_const(f)) {
TRACE(nlsat_explain, tout << "adding factor:\n"; display(tout, f); tout << "\n";);
m_todo.insert(f);
}
}
}
else {
m_todo.insert(p);
}
}
// The monomials have to be square free according to
//"An improved projection operation for cylindrical algebraic decomposition of three-dimensional space", by McCallum, Scott
bool is_square_free(polynomial_ref_vector &ps, var x) {
if (m_add_all_coeffs)
return false;
polynomial_ref p(m_pm);
polynomial_ref lc_poly(m_pm);
polynomial_ref disc_poly(m_pm);
for (unsigned i = 0; i < ps.size(); i++) {
p = ps.get(i);
unsigned k_deg = m_pm.degree(p, x);
if (k_deg == 0)
continue;
// p depends on x
disc_poly = discriminant(p, x); // Use global helper
if (sign(disc_poly) == 0) { // Discriminant is zero
TRACE(nlsat_explain, tout << "p is not square free:\n ";
display(tout, p); tout << "\ndiscriminant: "; display(tout, disc_poly) << "\n";
m_solver.display_assignment(tout) << '\n';
m_solver.display_var(tout << "x:", x) << '\n';
);
return false;
}
}
return true;
}
// If each p from ps is square-free then add the leading coefficents to the projection.
// Otherwise, add each coefficient of each p to the projection.
void add_lcs(polynomial_ref_vector &ps, var x) {
polynomial_ref p(m_pm);
polynomial_ref coeff(m_pm);
bool sqf = is_square_free(ps, x);
// Add the leading or all coeffs, depening on being square-free
for (unsigned i = 0; i < ps.size(); i++) {
p = ps.get(i);
unsigned k_deg = m_pm.degree(p, x);
if (k_deg == 0) continue;
// p depends on x
TRACE(nlsat_explain, tout << "processing poly of degree " << k_deg << " w.r.t x" << x << ": "; display(tout, p) << "\n";);
for (unsigned j_coeff_deg = k_deg; j_coeff_deg >= 1; j_coeff_deg--) {
coeff = m_pm.coeff(p, x, j_coeff_deg);
TRACE(nlsat_explain, tout << " coeff deg " << j_coeff_deg << ": "; display(tout, coeff) << "\n";);
insert_fresh_factors_in_todo(coeff);
if (sqf)
break;
}
}
}
void psc_resultant_sample(polynomial_ref_vector &ps, var x, polynomial_ref_vector & samples){
polynomial_ref p(m_pm);
polynomial_ref q(m_pm);
SASSERT(samples.size() <= 2);
for (unsigned i = 0; i < ps.size(); i++){
p = ps.get(i);
for (unsigned j = 0; j < samples.size(); j++){
q = samples.get(j);
if (!m_pm.eq(p, q)) {
psc(p, q, x);
}
}
}
}
void add_zero_assumption_on_factor(polynomial_ref& f) {
display(std::cout << "zero factors \n", f);
}
// this function also explains the value 0, if met
bool coeffs_are_zeroes(polynomial_ref &s) {
restore_factors _restore(m_factors, m_factors_save);
factor(s, m_factors);
unsigned num_factors = m_factors.size();
m_zero_fs.reset();
m_is_even.reset();
polynomial_ref f(m_pm);
bool have_zero = false;
for (unsigned i = 0; i < num_factors; i++) {
f = m_factors.get(i);
if (coeffs_are_zeroes_in_factor(f)) {
have_zero = true;
break;
}
}
if (!have_zero)
return false;
var x = max_var(f);
unsigned n = degree(f, x);
auto c = polynomial_ref(this->m_pm);
for (unsigned j = 0; j <= n; j++) {
c = m_pm.coeff(s, x, j);
SASSERT(sign(c) == 0);
ensure_sign(c);
}
return true;
}
bool coeffs_are_zeroes_in_factor(polynomial_ref & s) {
var x = max_var(s);
unsigned n = degree(s, x);
auto c = polynomial_ref(this->m_pm);
for (unsigned j = 0; j <= n; j++) {
c = m_pm.coeff(s, x, j);
if (sign(c) != 0)
return false;
}
return true;
}
/**
\brief Add v-psc(p, q, x) into m_todo
*/
void psc(polynomial_ref & p, polynomial_ref & q, var x) {
polynomial_ref_vector & S = m_psc_tmp;
polynomial_ref s(m_pm);
psc_chain(p, q, x, S);
unsigned sz = S.size();
TRACE(nlsat_explain, tout << "computing psc of\n"; display(tout, p); tout << "\n"; display(tout, q); tout << "\n";
for (unsigned i = 0; i < sz; ++i) {
s = S.get(i);
tout << "psc: " << s << "\n";
});
for (unsigned i = 0; i < sz; i++) {
s = S.get(i);
TRACE(nlsat_explain, display(tout << "processing psc(" << i << ")\n", s) << "\n";);
if (is_zero(s)) {
TRACE(nlsat_explain, tout << "skipping psc is the zero polynomial\n";);
continue;
}
if (is_const(s)) {
TRACE(nlsat_explain, tout << "done, psc is a constant\n";);
return;
}
if (is_zero(sign(s))) {
TRACE(nlsat_explain, tout << "psc vanished, adding zero assumption\n";);
add_zero_assumption(s);
continue;
}
TRACE(nlsat_explain,
tout << "adding v-psc of\n";
display(tout, p);
tout << "\n";
display(tout, q);
tout << "\n---->\n";
display(tout, s);
tout << "\n";);
// s did not vanish completely, but its leading coefficient may have vanished
insert_fresh_factors_in_todo(s);
return;
}
}
/**
\brief For each p in ps, add v-psc(x, p, p') into m_todo
\pre all polynomials in ps contain x
Remark: the leading coefficients do not vanish in the current model,
since all polynomials in ps were pre-processed using elim_vanishing.
*/
void psc_discriminant(polynomial_ref_vector & ps, var x) {
polynomial_ref p(m_pm);
polynomial_ref p_prime(m_pm);
unsigned sz = ps.size();
for (unsigned i = 0; i < sz; i++) {
p = ps.get(i);
if (degree(p, x) < 2)
continue;
p_prime = derivative(p, x);
psc(p, p_prime, x);
}
}
/**
\brief For each p and q in ps, p != q, add v-psc(x, p, q) into m_todo
\pre all polynomials in ps contain x
Remark: the leading coefficients do not vanish in the current model,
since all polynomials in ps were pre-processed using elim_vanishing.
*/
void psc_resultant(polynomial_ref_vector & ps, var x) {
polynomial_ref p(m_pm);
polynomial_ref q(m_pm);
unsigned sz = ps.size();
for (unsigned i = 0; i < sz - 1; i++) {
p = ps.get(i);
for (unsigned j = i + 1; j < sz; j++) {
q = ps.get(j);
psc(p, q, x);
}
}
}
void process_projection_polynomial(polynomial_ref & s) {
if (is_zero(s)) {
TRACE(nlsat_explain, tout << "projection polynomial is zero\n";);
return;
}
if (is_const(s)) {
TRACE(nlsat_explain, tout << "projection polynomial is constant: "; display(tout, s) << "\n";);
return;
}
if (is_zero(sign(s))) {
TRACE(nlsat_explain, tout << "projection polynomial vanished, adding zero assumption\n"; display(tout, s) << "\n";);
add_zero_assumption(s);
return;
}
TRACE(nlsat_explain, tout << "adding projection polynomial\n"; display(tout, s) << "\n";);
insert_fresh_factors_in_todo(s);
}
void lazard_discriminant(polynomial_ref_vector & ps, var x) {
polynomial_ref p(m_pm);
polynomial_ref disc(m_pm);
unsigned sz = ps.size();
for (unsigned i = 0; i < sz; ++i) {
p = ps.get(i);
if (max_var(p) != x)
continue;
unsigned deg = degree(p, x);
if (deg < 2)
continue;
disc = discriminant(p, x);
TRACE(nlsat_explain, tout << "Lazard discriminant of "; display(tout, p); tout << "\n -> "; display(tout, disc); tout << "\n";);
process_projection_polynomial(disc);
}
}
void lazard_resultant(polynomial_ref_vector & ps, var x) {
polynomial_ref p(m_pm);
polynomial_ref q(m_pm);
polynomial_ref res(m_pm);
unsigned sz = ps.size();
for (unsigned i = 0; i < sz; ++i) {
p = ps.get(i);
if (max_var(p) != x || degree(p, x) == 0)
continue;
for (unsigned j = i + 1; j < sz; ++j) {
q = ps.get(j);
if (max_var(q) != x || degree(q, x) == 0)
continue;
res = resultant(p, q, x);
TRACE(nlsat_explain, tout << "Lazard resultant of\n"; display(tout, p); tout << "\nand\n"; display(tout, q); tout << "\n -> "; display(tout, res); tout << "\n";);
process_projection_polynomial(res);
}
}
}
void test_root_literal(atom::kind k, var y, unsigned i, poly * p, scoped_literal_vector& result) {
m_result = &result;
add_root_literal(k, y, i, p);
reset_already_added();
m_result = nullptr;
}
void add_root_literal(atom::kind k, var y, unsigned i, poly * p) {
polynomial_ref pr(p, m_pm);
TRACE(nlsat_explain,
display(tout << "x" << y << " " << k << "[" << i << "](", pr); tout << ")\n";);
if (!mk_linear_root(k, y, i, p) &&
!mk_quadratic_root(k, y, i, p)) {
bool_var b = m_solver.mk_root_atom(k, y, i, p);
literal l(b, true);
TRACE(nlsat_explain, tout << "adding literal\n"; display(tout, l); tout << "\n";);
add_literal(l);
}
}
/**
* literal can be expressed using a linear ineq_atom
*/
bool mk_linear_root(atom::kind k, var y, unsigned i, poly * p) {
scoped_mpz c(m_pm.m());
if (m_pm.degree(p, y) == 1 && m_pm.const_coeff(p, y, 1, c)) {
SASSERT(!m_pm.m().is_zero(c));
mk_linear_root(k, y, i, p, m_pm.m().is_neg(c));
return true;
}
return false;
}
/**
Create pseudo-linear root depending on the sign of the coefficient to y.
*/
bool mk_plinear_root(atom::kind k, var y, unsigned i, poly * p) {
if (m_pm.degree(p, y) != 1) {
return false;
}
polynomial_ref c(m_pm);
c = m_pm.coeff(p, y, 1);
int s = sign(c);
if (s == 0) {
return false;
}
ensure_sign(c);
mk_linear_root(k, y, i, p, s < 0);
return true;
}
/**
Encode root conditions for quadratic polynomials.
Basically implements Thom's theorem. The roots are characterized by the sign of polynomials and their derivatives.
b^2 - 4ac = 0:
- there is only one root, which is -b/2a.
- relation to root is a function of the sign of
- 2ax + b
b^2 - 4ac > 0:
- assert i == 1 or i == 2
- relation to root is a function of the signs of:
- 2ax + b
- ax^2 + bx + c
*/
bool mk_quadratic_root(atom::kind k, var y, unsigned i, poly * p) {
if (m_pm.degree(p, y) != 2) {
return false;
}
if (i != 1 && i != 2) {
return false;
}
SASSERT(m_assignment.is_assigned(y));
polynomial_ref A(m_pm), B(m_pm), C(m_pm), q(m_pm), p_diff(m_pm), yy(m_pm);
A = m_pm.coeff(p, y, 2);
B = m_pm.coeff(p, y, 1);
C = m_pm.coeff(p, y, 0);
// TBD throttle based on degree of q?
q = (B*B) - (4*A*C);
yy = m_pm.mk_polynomial(y);
p_diff = 2*A*yy + B;
p_diff = m_pm.normalize(p_diff);
int sq = ensure_sign(q);
if (sq < 0) {
return false;
}
int sa = ensure_sign(A);
if (sa == 0) {
q = B*yy + C;
return mk_plinear_root(k, y, i, q);
}
ensure_sign(p_diff);
if (sq > 0) {
polynomial_ref pr(p, m_pm);
ensure_sign(pr);
}
return true;
}
int ensure_sign(polynomial_ref & p) {
#if 0
polynomial_ref f(m_pm);
factor(p, m_factors);
m_is_even.reset();
unsigned num_factors = m_factors.size();
int s = 1;
for (unsigned i = 0; i < num_factors; i++) {
f = m_factors.get(i);
s *= sign(f);
m_is_even.push_back(false);
}
if (num_factors > 0) {
atom::kind k = atom::EQ;
if (s == 0) k = atom::EQ;
if (s < 0) k = atom::LT;
if (s > 0) k = atom::GT;
bool_var b = m_solver.mk_ineq_atom(k, num_factors, m_factors.c_ptr(), m_is_even.c_ptr());
add_literal(literal(b, true));
}
return s;
#else
int s = sign(p);
if (!is_const(p)) {
TRACE(nlsat_explain, tout << p << "\n";);
add_simple_assumption(s == 0 ? atom::EQ : (s < 0 ? atom::LT : atom::GT), p);
}
return s;
#endif
}
/**
Auxiliary function to linear roots.
y > root[1](-2*y - z)
y > -z/2
y + z/2 > 0
2y + z > 0
*/
void mk_linear_root(atom::kind k, var y, unsigned i, poly * p, bool mk_neg) {
TRACE(nlsat_explain, display_var(tout, y); m_pm.display(tout << ": ", p, m_solver.display_proc()); tout << "\n");
polynomial_ref p_prime(m_pm);
p_prime = p;
bool lsign = false;
if (mk_neg)
p_prime = neg(p_prime);
p = p_prime.get();
switch (k) {
case atom::ROOT_EQ: k = atom::EQ; lsign = false; break;
case atom::ROOT_LT: k = atom::LT; lsign = false; break;
case atom::ROOT_GT: k = atom::GT; lsign = false; break;
case atom::ROOT_LE: k = atom::GT; lsign = true; break;
case atom::ROOT_GE: k = atom::LT; lsign = true; break;
default:
UNREACHABLE();
break;
}
add_simple_assumption(k, p, lsign);
}
void cac_add_cell_lits(polynomial_ref_vector & ps, var y, polynomial_ref_vector & res) {
res.reset();
SASSERT(m_assignment.is_assigned(y));
bool lower_inf = true;
bool upper_inf = true;
scoped_anum_vector & roots = m_roots_tmp;
scoped_anum lower(m_am);
scoped_anum upper(m_am);
anum const & y_val = m_assignment.value(y);
TRACE(nlsat_explain, tout << "adding literals for "; display_var(tout, y); tout << " -> ";
m_am.display_decimal(tout, y_val); tout << "\n";);
polynomial_ref p_lower(m_pm);
unsigned i_lower = UINT_MAX;
polynomial_ref p_upper(m_pm);
unsigned i_upper = UINT_MAX;
polynomial_ref p(m_pm);
unsigned sz = ps.size();
for (unsigned k = 0; k < sz; k++) {
p = ps.get(k);
if (max_var(p) != y)
continue;
roots.reset();
// Variable y is assigned in m_assignment. We must temporarily unassign it.
// Otherwise, the isolate_roots procedure will assume p is a constant polynomial.
m_am.isolate_roots(p, undef_var_assignment(m_assignment, y), roots);
unsigned num_roots = roots.size();
bool all_lt = true;
for (unsigned i = 0; i < num_roots; i++) {
int s = m_am.compare(y_val, roots[i]);
TRACE(nlsat_explain,
m_am.display_decimal(tout << "comparing root: ", roots[i]); tout << "\n";
m_am.display_decimal(tout << "with y_val:", y_val);
tout << "\nsign " << s << "\n";
tout << "poly: " << p << "\n";
);
if (s == 0) {
// y_val == roots[i]
// add literal
// ! (y = root_i(p))
add_root_literal(atom::ROOT_EQ, y, i+1, p);
res.push_back(p);
return;
}
else if (s < 0) {
// y_val < roots[i]
if (i > 0) {
// y_val > roots[j]
int j = i - 1;
if (lower_inf || m_am.lt(lower, roots[j])) {
lower_inf = false;
m_am.set(lower, roots[j]);
p_lower = p;
i_lower = j + 1;
}
}
if (upper_inf || m_am.lt(roots[i], upper)) {
upper_inf = false;
m_am.set(upper, roots[i]);
p_upper = p;
i_upper = i + 1;
}
all_lt = false;
break;
}
}
if (all_lt && num_roots > 0) {
int j = num_roots - 1;
if (lower_inf || m_am.lt(lower, roots[j])) {
lower_inf = false;
m_am.set(lower, roots[j]);
p_lower = p;
i_lower = j + 1;
}
}
}
if (!lower_inf) {
res.push_back(p_lower);
add_root_literal(m_full_dimensional ? atom::ROOT_GE : atom::ROOT_GT, y, i_lower, p_lower);
}
if (!upper_inf) {
res.push_back(p_upper);
add_root_literal(m_full_dimensional ? atom::ROOT_LE : atom::ROOT_LT, y, i_upper, p_upper);
}
}
/**
Add one or two literals that specify in which cell of variable y the current interpretation is.
One literal is added for the cases:
- y in (-oo, min) where min is the minimal root of the polynomials p2 in ps
We add literal
! (y < root_1(p2))
- y in (max, oo) where max is the maximal root of the polynomials p1 in ps
We add literal
! (y > root_k(p1)) where k is the number of real roots of p
- y = r where r is the k-th root of a polynomial p in ps
We add literal
! (y = root_k(p))
Two literals are added when
- y in (l, u) where (l, u) does not contain any root of polynomials p in ps, and
l is the i-th root of a polynomial p1 in ps, and u is the j-th root of a polynomial p2 in ps.
We add literals
! (y > root_i(p1)) or !(y < root_j(p2))
*/
void add_cell_lits(polynomial_ref_vector & ps, var y) {
SASSERT(m_assignment.is_assigned(y));
bool lower_inf = true;
bool upper_inf = true;
scoped_anum_vector & roots = m_roots_tmp;
scoped_anum lower(m_am);
scoped_anum upper(m_am);
anum const & y_val = m_assignment.value(y);
TRACE(nlsat_explain, tout << "adding literals for "; display_var(tout, y); tout << " -> ";
m_am.display_decimal(tout, y_val); tout << "\n";);
polynomial_ref p_lower(m_pm);
unsigned i_lower = UINT_MAX;
polynomial_ref p_upper(m_pm);
unsigned i_upper = UINT_MAX;
polynomial_ref p(m_pm);
unsigned sz = ps.size();
for (unsigned k = 0; k < sz; k++) {
p = ps.get(k);
if (max_var(p) != y)
continue;
roots.reset();
// Variable y is assigned in m_assignment. We must temporarily unassign it.
// Otherwise, the isolate_roots procedure will assume p is a constant polynomial.
m_am.isolate_roots(p, undef_var_assignment(m_assignment, y), roots);
unsigned num_roots = roots.size();
bool all_lt = true;
for (unsigned i = 0; i < num_roots; i++) {
int s = m_am.compare(y_val, roots[i]);
TRACE(nlsat_explain,
m_am.display_decimal(tout << "comparing root: ", roots[i]); tout << "\n";
m_am.display_decimal(tout << "with y_val:", y_val);
tout << "\nsign " << s << "\n";
tout << "poly: " << p << "\n";
);
if (s == 0) {
// y_val == roots[i]
// add literal
// ! (y = root_i(p))
add_root_literal(atom::ROOT_EQ, y, i+1, p);
return;
}
else if (s < 0) {
// y_val < roots[i]
if (i > 0) {
// y_val > roots[j]
int j = i - 1;
if (lower_inf || m_am.lt(lower, roots[j])) {
lower_inf = false;
m_am.set(lower, roots[j]);
p_lower = p;
i_lower = j + 1;
}
}
if (upper_inf || m_am.lt(roots[i], upper)) {
upper_inf = false;
m_am.set(upper, roots[i]);
p_upper = p;
i_upper = i + 1;
}
all_lt = false;
break;
}
}
if (all_lt && num_roots > 0) {
int j = num_roots - 1;
if (lower_inf || m_am.lt(lower, roots[j])) {
lower_inf = false;
m_am.set(lower, roots[j]);
p_lower = p;
i_lower = j + 1;
}
}
}
if (!lower_inf) {
add_root_literal(m_full_dimensional ? atom::ROOT_GE : atom::ROOT_GT, y, i_lower, p_lower);
}
if (!upper_inf) {
add_root_literal(m_full_dimensional ? atom::ROOT_LE : atom::ROOT_LT, y, i_upper, p_upper);
}
}
/**
\brief Return true if all polynomials in ps are univariate in x.
*/
bool all_univ(polynomial_ref_vector const & ps, var x) {
unsigned sz = ps.size();
for (unsigned i = 0; i < sz; i++) {
poly * p = ps.get(i);
if (max_var(p) != x)
return false;
if (!m_pm.is_univariate(p))
return false;
}
return true;
}
/**
\brief Apply model-based projection operation defined in our paper.
*/
void project_original(polynomial_ref_vector & ps, var max_x) {
if (ps.empty())
return;
m_todo.reset();
for (poly* p : ps) {
m_todo.insert(p);
}
var x = m_todo.extract_max_polys(ps);
// Remark: after vanishing coefficients are eliminated, ps may not contain max_x anymore
if (x < max_x)
add_cell_lits(ps, x);
while (true) {
if (all_univ(ps, x) && m_todo.empty()) {
m_todo.reset();
break;
}
TRACE(nlsat_explain, tout << "project loop, processing var "; display_var(tout, x);
tout << "\npolynomials\n";
display(tout, ps); tout << "\n";);
add_lcs(ps, x);
psc_discriminant(ps, x);
psc_resultant(ps, x);
if (m_todo.empty())
break;
x = m_todo.extract_max_polys(ps);
add_cell_lits(ps, x);
}
}
void project_lazard(polynomial_ref_vector & ps, var max_x) {
if (ps.empty())
return;
m_todo.reset();
for (poly* p : ps) {
m_todo.insert(p);
}
var x = m_todo.extract_max_polys(ps);
if (x < max_x)
add_cell_lits(ps, x);
while (true) {
if (all_univ(ps, x) && m_todo.empty()) {
m_todo.reset();
break;
}
TRACE(nlsat_explain, tout << "Lazard project loop, processing var "; display_var(tout, x);
tout << "\npolynomials\n"; display(tout, ps); tout << "\n";);
add_lcs(ps, x);
lazard_discriminant(ps, x);
lazard_resultant(ps, x);
if (m_todo.empty())
break;
x = m_todo.extract_max_polys(ps);
add_cell_lits(ps, x);
}
}
/**
* Sample Projection
* Reference:
* Haokun Li and Bican Xia.
* "Solving Satisfiability of Polynomial Formulas By Sample - Cell Projection"
* https://arxiv.org/abs/2003.00409
*/
void project_cdcac(polynomial_ref_vector & ps, var max_x) {
bool first = true;
if (ps.empty())
return;
m_todo.reset();
for (unsigned i = 0; i < ps.size(); i++) {
polynomial_ref p(m_pm);
p = ps.get(i);
insert_fresh_factors_in_todo(p);
}
// replace ps by the fresh factors
ps.reset();
for (auto p: m_todo.m_set)
ps.push_back(p);
var x = m_todo.extract_max_polys(ps);
// Remark: after vanishing coefficients are eliminated, ps may not contain max_x anymore
polynomial_ref_vector samples(m_pm);
if (x < max_x)
cac_add_cell_lits(ps, x, samples);
while (true) {
if (all_univ(ps, x) && m_todo.empty()) {
m_todo.reset();
break;
}
TRACE(nlsat_explain, tout << "project loop, processing var "; display_var(tout, x); tout << "\npolynomials\n";
display(tout, ps); tout << "\n";);
if (first) { // The first run is special because x is not constrained by the sample, we cannot surround it by the root functions.
// we make the polynomials in ps delinable
add_lcs(ps, x);
psc_discriminant(ps, x);
psc_resultant(ps, x);
first = false;
}
else {
add_lcs(ps, x);
psc_discriminant(ps, x);
psc_resultant_sample(ps, x, samples);
}
if (m_todo.empty())
break;
x = m_todo.extract_max_polys(ps);
cac_add_cell_lits(ps, x, samples);
}
}
void project(polynomial_ref_vector & ps, var max_x) {
if (m_lazard) {
project_lazard(ps, max_x);
}
else if (m_cell_sample) {
project_cdcac(ps, max_x);
}
else {
project_original(ps, max_x);
}
}
bool check_already_added() const {
for (bool b : m_already_added_literal) {
(void)b;
SASSERT(!b);
}
return true;
}
/*
Conflicting core simplification using equations.
The idea is to use equations to reduce the complexity of the
conflicting core.
Basic idea:
Let l be of the form
h > 0
and eq of the form
p = 0
Using pseudo-division we have that:
lc(p)^d h = q p + r
where q and r are the pseudo-quotient and pseudo-remainder
d is the integer returned by the pseudo-division algorithm.
lc(p) is the leading coefficient of p
If d is even or sign(lc(p)) > 0, we have that
sign(h) = sign(r)
Otherwise
sign(h) = -sign(r) flipped the sign
We have the following rules
If
(C and h > 0) implies false
Then
1. (C and p = 0 and lc(p) != 0 and r > 0) implies false if d is even
2. (C and p = 0 and lc(p) > 0 and r > 0) implies false if lc(p) > 0 and d is odd
3. (C and p = 0 and lc(p) < 0 and r < 0) implies false if lc(p) < 0 and d is odd
If
(C and h = 0) implies false
Then
(C and p = 0 and lc(p) != 0 and r = 0) implies false
If
(C and h < 0) implies false
Then
1. (C and p = 0 and lc(p) != 0 and r < 0) implies false if d is even
2. (C and p = 0 and lc(p) > 0 and r < 0) implies false if lc(p) > 0 and d is odd
3. (C and p = 0 and lc(p) < 0 and r > 0) implies false if lc(p) < 0 and d is odd
Good cases:
- lc(p) is a constant
- p = 0 is already in the conflicting core
- p = 0 is linear
We only use equations from the conflicting core and lower stages.
Equations from lower stages are automatically added to the lemma.
*/
struct eq_info {
poly const * m_eq;
polynomial::var m_x;
unsigned m_k;
poly * m_lc;
int m_lc_sign;
bool m_lc_const;
bool m_lc_add;
bool m_lc_add_ineq;
void add_lc_ineq() {
m_lc_add = true;
m_lc_add_ineq = true;
}
void add_lc_diseq() {
if (!m_lc_add) {
m_lc_add = true;
m_lc_add_ineq = false;
}
}
};
void simplify(literal l, eq_info & info, var max, scoped_literal & new_lit) {
bool_var b = l.var();
atom * a = m_atoms[b];
SASSERT(a);
if (a->is_root_atom()) {
new_lit = l;
return;
}
ineq_atom * _a = to_ineq_atom(a);
unsigned num_factors = _a->size();
if (num_factors == 1 && _a->p(0) == info.m_eq) {
new_lit = l;
return;
}
TRACE(nlsat_simplify_core, display(tout << "trying to simplify literal\n", l) << "\nusing equation\n";
m_pm.display(tout, info.m_eq, m_solver.display_proc()); tout << "\n";);
int atom_sign = 1;
bool modified_lit = false;
polynomial_ref_buffer new_factors(m_pm);
sbuffer<bool> new_factors_even;
polynomial_ref new_factor(m_pm);
for (unsigned s = 0; s < num_factors; s++) {
poly * f = _a->p(s);
bool is_even = _a->is_even(s);
if (m_pm.degree(f, info.m_x) < info.m_k) {
new_factors.push_back(f);
new_factors_even.push_back(is_even);
continue;
}
modified_lit = true;
unsigned d;
m_pm.pseudo_remainder(f, info.m_eq, info.m_x, d, new_factor);
polynomial_ref fact(f, m_pm), eq(const_cast<poly*>(info.m_eq), m_pm);
TRACE(nlsat_simplify_core, tout << "d: " << d << " factor " << fact << " eq " << eq << " new factor " << new_factor << "\n";);
// adjust sign based on sign of lc of eq
if (d % 2 == 1 && // d is odd
!is_even && // degree of the factor is odd
info.m_lc_sign < 0) { // lc of the eq is negative
atom_sign = -atom_sign; // flipped the sign of the current literal
TRACE(nlsat_simplify_core, tout << "odd degree\n";);
}
if (is_const(new_factor)) {
TRACE(nlsat_simplify_core, tout << "new factor is const\n";);
auto s = sign(new_factor);
if (is_zero(s)) {
bool atom_val = a->get_kind() == atom::EQ;
bool lit_val = l.sign() ? !atom_val : atom_val;
new_lit = lit_val ? true_literal : false_literal;
TRACE(nlsat_simplify_core, tout << "zero sign: " << info.m_lc_const << "\n";);
if (!info.m_lc_const) {
// We have essentially shown the current factor must be zero If the leading coefficient is not zero.
// Note that, if the current factor is zero, then the whole polynomial is zero.
// The atom is true if it is an equality, and false otherwise.
// The sign of the leading coefficient (info.m_lc) of info.m_eq doesn't matter.
// However, we have to store the fact it is not zero.
info.add_lc_diseq();
}
return;
}
else {
TRACE(nlsat_simplify_core, tout << "non-zero sign: " << info.m_lc_const << "\n";);
// We have shown the current factor is a constant MODULO the sign of the leading coefficient (of the equation used to rewrite the factor).
if (!info.m_lc_const) {
// If the leading coefficient is not a constant, we must store this information as an extra assumption.
if (d % 2 == 0 || // d is even
is_even || // rewriting a factor of even degree, sign flip doesn't matter
_a->get_kind() == atom::EQ) // rewriting an equation, sign flip doesn't matter
info.add_lc_diseq();
else
info.add_lc_ineq();
}
if (s < 0 && !is_even) {
atom_sign = -atom_sign;
}
}
}
else {
new_factors.push_back(new_factor);
new_factors_even.push_back(is_even);
if (!info.m_lc_const) {
if (d % 2 == 0 || // d is even
is_even || // rewriting a factor of even degree, sign flip doesn't matter
_a->get_kind() == atom::EQ) // rewriting an equation, sign flip doesn't matter
info.add_lc_diseq();
else
info.add_lc_ineq();
}
}
}
if (modified_lit) {
atom::kind new_k = _a->get_kind();
if (atom_sign < 0)
new_k = atom::flip(new_k);
new_lit = m_solver.mk_ineq_literal(new_k, new_factors.size(), new_factors.data(), new_factors_even.data());
if (l.sign())
new_lit.neg();
TRACE(nlsat_simplify_core, tout << "simplified literal:\n"; display(tout, new_lit) << " " << m_solver.value(new_lit) << "\n";);
if (max_var(new_lit) < max) {
if (m_solver.value(new_lit) == l_true) {
new_lit = l;
}
else {
add_literal(new_lit);
new_lit = true_literal;
}
}
else {
new_lit = normalize(new_lit, max);
TRACE(nlsat_simplify_core, tout << "simplified literal after normalization:\n"; display(tout, new_lit); tout << " " << m_solver.value(new_lit) << "\n";);
}
}
else {
new_lit = l;
}
}
bool simplify(scoped_literal_vector & C, poly const * eq, var max) {
bool modified_core = false;
eq_info info;
info.m_eq = eq;
info.m_x = m_pm.max_var(info.m_eq);
info.m_k = m_pm.degree(eq, info.m_x);
polynomial_ref lc_eq(m_pm);
lc_eq = m_pm.coeff(eq, info.m_x, info.m_k);
info.m_lc = lc_eq.get();
info.m_lc_sign = sign(lc_eq);
info.m_lc_add = false;
info.m_lc_add_ineq = false;
info.m_lc_const = m_pm.is_const(lc_eq);
SASSERT(info.m_lc != 0);
scoped_literal new_lit(m_solver);
unsigned sz = C.size();
unsigned j = 0;
for (unsigned i = 0; i < sz; i++) {
literal l = C[i];
new_lit = null_literal;
simplify(l, info, max, new_lit);
SASSERT(new_lit != null_literal);
if (l == new_lit) {
C.set(j, l);
j++;
continue;
}
modified_core = true;
if (new_lit == true_literal)
continue;
if (new_lit == false_literal) {
// false literal was created. The assumptions added are sufficient for implying the conflict.
j = 0; // force core to be reset
break;
}
C.set(j, new_lit);
j++;
}
C.shrink(j);
if (info.m_lc_add) {
if (info.m_lc_add_ineq)
add_assumption(info.m_lc_sign < 0 ? atom::LT : atom::GT, info.m_lc);
else
add_assumption(atom::EQ, info.m_lc, true);
}
return modified_core;
}
/**
\brief (try to) Select an equation from C. Returns 0 if C does not contain any equality.
This method selects the equation of minimal degree in max.
*/
poly * select_eq(scoped_literal_vector & C, var max) {
poly * r = nullptr;
unsigned min_d = UINT_MAX;
unsigned sz = C.size();
for (unsigned i = 0; i < sz; i++) {
literal l = C[i];
if (l.sign())
continue;
bool_var b = l.var();
atom * a = m_atoms[b];
SASSERT(a != 0);
if (a->get_kind() != atom::EQ)
continue;
ineq_atom * _a = to_ineq_atom(a);
if (_a->size() > 1)
continue;
if (_a->is_even(0))
continue;
unsigned d = m_pm.degree(_a->p(0), max);
SASSERT(d > 0);
if (d < min_d) {
r = _a->p(0);
min_d = d;
if (min_d == 1)
break;
}
}
return r;
}
/**
\brief Select an equation eq s.t.
max_var(eq) < max, and
it can be used to rewrite a literal in C.
Return 0, if such equation was not found.
*/
var_vector m_select_tmp;
ineq_atom * select_lower_stage_eq(scoped_literal_vector & C, var max) {
var_vector & xs = m_select_tmp;
for (literal l : C) {
bool_var b = l.var();
atom * a = m_atoms[b];
if (a->is_root_atom())
continue; // we don't rewrite root atoms
ineq_atom * _a = to_ineq_atom(a);
unsigned num_factors = _a->size();
for (unsigned j = 0; j < num_factors; j++) {
poly * p = _a->p(j);
xs.reset();
m_pm.vars(p, xs);
for (var y : xs) {
if (y >= max)
continue;
atom * eq = m_x2eq[y];
if (eq == nullptr)
continue;
SASSERT(eq->is_ineq_atom());
SASSERT(to_ineq_atom(eq)->size() == 1);
SASSERT(!to_ineq_atom(eq)->is_even(0));
poly * eq_p = to_ineq_atom(eq)->p(0);
SASSERT(m_pm.degree(eq_p, y) > 0);
// TODO: create a parameter
// In the current experiments, using equations with non constant coefficients produces a blowup
if (!m_pm.nonzero_const_coeff(eq_p, y, m_pm.degree(eq_p, y)))
continue;
if (m_pm.degree(p, y) >= m_pm.degree(eq_p, y))
return to_ineq_atom(eq);
}
}
}
return nullptr;
}
/**
\brief Simplify the core using equalities.
*/
void simplify(scoped_literal_vector & C, var max) {
// Simplify using equations in the core
while (!C.empty()) {
poly * eq = select_eq(C, max);
if (eq == nullptr)
break;
TRACE(nlsat_simplify_core, tout << "using equality for simplifying core\n";
m_pm.display(tout, eq, m_solver.display_proc()); tout << "\n";);
if (!simplify(C, eq, max))
break;
}
// Simplify using equations using variables from lower stages.
while (!C.empty()) {
ineq_atom * eq = select_lower_stage_eq(C, max);
if (eq == nullptr)
break;
SASSERT(eq->size() == 1);
SASSERT(!eq->is_even(0));
poly * eq_p = eq->p(0);
VERIFY(simplify(C, eq_p, max));
// add equation as an assumption
TRACE(nlsat_simpilfy_core, display(tout << "adding equality as assumption ", literal(eq->bvar(), true)); tout << "\n";);
add_literal(literal(eq->bvar(), true));
}
}
/**
\brief Main procedure. The explain the given unsat core, and store the result in m_result
*/
void main(unsigned num, literal const * ls) {
if (num == 0)
return;
collect_polys(num, ls, m_ps);
var max_x = max_var(m_ps);
TRACE(nlsat_explain, tout << "polynomials in the conflict:\n"; display(tout, m_ps); tout << "\n";);
elim_vanishing(m_ps);
TRACE(nlsat_explain, tout << "elim vanishing\n"; display(tout, m_ps); tout << "\n";);
project(m_ps, max_x);
TRACE(nlsat_explain, tout << "after projection\n"; display(tout, m_ps); tout << "\n";);
}
void process2(unsigned num, literal const * ls) {
if (m_simplify_cores) {
m_core2.reset();
m_core2.append(num, ls);
var max = max_var(num, ls);
SASSERT(max != null_var);
normalize(m_core2, max);
TRACE(nlsat_explain, display(tout << "core after normalization\n", m_core2) << "\n";);
simplify(m_core2, max);
TRACE(nlsat_explain, display(tout << "core after simplify\n", m_core2) << "\n";);
main(m_core2.size(), m_core2.data());
m_core2.reset();
}
else {
main(num, ls);
}
}
// Auxiliary method for core minimization.
literal_vector m_min_newtodo;
bool minimize_core(literal_vector & todo, literal_vector & core) {
SASSERT(!todo.empty());
literal_vector & new_todo = m_min_newtodo;
new_todo.reset();
interval_set_manager & ism = m_evaluator.ism();
interval_set_ref r(ism);
// Copy the union of the infeasible intervals of core into r.
unsigned sz = core.size();
for (unsigned i = 0; i < sz; i++) {
literal l = core[i];
atom * a = m_atoms[l.var()];
SASSERT(a != 0);
interval_set_ref inf = m_evaluator.infeasible_intervals(a, l.sign(), nullptr);
r = ism.mk_union(inf, r);
if (ism.is_full(r)) {
// Done
return false;
}
}
TRACE(nlsat_minimize, tout << "interval set after adding partial core:\n" << r << "\n";);
if (todo.size() == 1) {
// Done
core.push_back(todo[0]);
return false;
}
// Copy the union of the infeasible intervals of todo into r until r becomes full.
sz = todo.size();
for (unsigned i = 0; i < sz; i++) {
literal l = todo[i];
atom * a = m_atoms[l.var()];
SASSERT(a != 0);
interval_set_ref inf = m_evaluator.infeasible_intervals(a, l.sign(), nullptr);
r = ism.mk_union(inf, r);
if (ism.is_full(r)) {
// literal l must be in the core
core.push_back(l);
new_todo.swap(todo);
return !todo.empty();
}
else {
new_todo.push_back(l);
}
}
UNREACHABLE();
return true;
}
literal_vector m_min_todo;
literal_vector m_min_core;
void minimize(unsigned num, literal const * ls, scoped_literal_vector & r) {
literal_vector & todo = m_min_todo;
literal_vector & core = m_min_core;
todo.reset(); core.reset();
todo.append(num, ls);
while (true) {
TRACE(nlsat_minimize, tout << "core minimization:\n"; display(tout, todo); tout << "\nCORE:\n"; display(tout, core) << "\n";);
if (!minimize_core(todo, core))
break;
std::reverse(todo.begin(), todo.end());
TRACE(nlsat_minimize, tout << "core minimization:\n"; display(tout, todo); tout << "\nCORE:\n"; display(tout, core) << "\n";);
if (!minimize_core(todo, core))
break;
}
TRACE(nlsat_minimize, tout << "core:\n"; display(tout, core););
r.append(core.size(), core.data());
}
void process(unsigned num, literal const * ls) {
if (m_minimize_cores && num > 1) {
m_core1.reset();
minimize(num, ls, m_core1);
process2(m_core1.size(), m_core1.data());
m_core1.reset();
}
else {
process2(num, ls);
}
}
void operator()(unsigned num, literal const * ls, scoped_literal_vector & result) {
SASSERT(check_already_added());
SASSERT(num > 0);
TRACE(nlsat_explain,
tout << "[explain] set of literals is infeasible in the current interpretation\n";
display(tout, num, ls) << "\n";
m_solver.display_assignment(tout);
);
m_result = &result;
process(num, ls);
reset_already_added();
m_result = nullptr;
TRACE(nlsat_explain, display(tout << "[explain] result\n", result) << "\n";);
CASSERT("nlsat", check_already_added());
}
void project(var x, unsigned num, literal const * ls, scoped_literal_vector & result) {
m_result = &result;
svector<literal> lits;
TRACE(nlsat, tout << "project x" << x << "\n";
m_solver.display(tout, num, ls);
m_solver.display(tout););
#ifdef Z3DEBUG
for (unsigned i = 0; i < num; ++i) {
SASSERT(m_solver.value(ls[i]) == l_true);
atom* a = m_atoms[ls[i].var()];
SASSERT(!a || m_evaluator.eval(a, ls[i].sign()));
}
#endif
split_literals(x, num, ls, lits);
collect_polys(lits.size(), lits.data(), m_ps);
var mx_var = max_var(m_ps);
if (!m_ps.empty()) {
svector<var> renaming;
if (x != mx_var) {
for (var i = 0; i < m_solver.num_vars(); ++i) {
renaming.push_back(i);
}
std::swap(renaming[x], renaming[mx_var]);
m_solver.reorder(renaming.size(), renaming.data());
TRACE(qe, tout << "x: " << x << " max: " << mx_var << " num_vars: " << m_solver.num_vars() << "\n";
m_solver.display(tout););
}
elim_vanishing(m_ps);
if (m_signed_project) {
signed_project(m_ps, mx_var);
}
else {
project(m_ps, mx_var);
}
reset_already_added();
m_result = nullptr;
if (x != mx_var) {
m_solver.restore_order();
}
}
else {
reset_already_added();
m_result = nullptr;
}
for (unsigned i = 0; i < result.size(); ++i) {
result.set(i, ~result[i]);
}
#ifdef Z3DEBUG
TRACE(nlsat, m_solver.display(tout, result.size(), result.data()) << "\n"; );
for (literal l : result) {
CTRACE(nlsat, l_true != m_solver.value(l), m_solver.display(tout, l) << " " << m_solver.value(l) << "\n";);
SASSERT(l_true == m_solver.value(l));
}
#endif
}
void split_literals(var x, unsigned n, literal const* ls, svector<literal>& lits) {
var_vector vs;
for (unsigned i = 0; i < n; ++i) {
vs.reset();
m_solver.vars(ls[i], vs);
if (vs.contains(x)) {
lits.push_back(ls[i]);
}
else {
add_literal(~ls[i]);
}
}
}
/**
Signed projection.
Assumptions:
- any variable in ps is at most x.
- root expressions are satisfied (positive literals)
Effect:
- if x not in p, then
- if sign(p) < 0: p < 0
- if sign(p) = 0: p = 0
- if sign(p) > 0: p > 0
else:
- let roots_j be the roots of p_j or roots_j[i]
- let L = { roots_j[i] | M(roots_j[i]) < M(x) }
- let U = { roots_j[i] | M(roots_j[i]) > M(x) }
- let E = { roots_j[i] | M(roots_j[i]) = M(x) }
- let glb in L, s.t. forall l in L . M(glb) >= M(l)
- let lub in U, s.t. forall u in U . M(lub) <= M(u)
- if root in E, then
- add E x . x = root & x > lb for lb in L
- add E x . x = root & x < ub for ub in U
- add E x . x = root & x = root2 for root2 in E \ { root }
- else
- assume |L| <= |U| (other case is symmetric)
- add E x . lb <= x & x <= glb for lb in L
- add E x . x = glb & x < ub for ub in U
*/
void signed_project(polynomial_ref_vector& ps, var x) {
TRACE(nlsat_explain, tout << "Signed projection\n";);
polynomial_ref p(m_pm);
unsigned eq_index = 0;
bool eq_valid = false;
unsigned eq_degree = 0;
for (unsigned i = 0; i < ps.size(); ++i) {
p = ps.get(i);
int s = sign(p);
if (max_var(p) != x) {
atom::kind k = (s == 0)?(atom::EQ):((s < 0)?(atom::LT):(atom::GT));
add_simple_assumption(k, p, false);
ps[i] = ps.back();
ps.pop_back();
--i;
}
else if (s == 0) {
if (!eq_valid || degree(p, x) < eq_degree) {
eq_index = i;
eq_valid = true;
eq_degree = degree(p, x);
}
}
}
if (ps.empty()) {
return;
}
if (ps.size() == 1) {
project_single(x, ps.get(0));
return;
}
// ax + b = 0, p(x) > 0 ->
if (eq_valid) {
p = ps.get(eq_index);
if (degree(p, x) == 1) {
// ax + b = 0
// let d be maximal degree of x in p.
// p(x) -> a^d*p(-b/a), a
// perform virtual substitution with equality.
solve_eq(x, eq_index, ps);
}
else {
add_zero_assumption(p);
for (unsigned j = 0; j < ps.size(); ++j) {
if (j == eq_index)
continue;
p = ps.get(j);
int s = sign(p);
atom::kind k = (s == 0)?(atom::EQ):((s < 0)?(atom::LT):(atom::GT));
add_simple_assumption(k, p, false);
}
}
return;
}
unsigned num_lub = 0, num_glb = 0;
unsigned glb_index = 0, lub_index = 0;
scoped_anum lub(m_am), glb(m_am), x_val(m_am);
x_val = m_assignment.value(x);
bool glb_valid = false, lub_valid = false;
for (unsigned i = 0; i < ps.size(); ++i) {
p = ps.get(i);
scoped_anum_vector & roots = m_roots_tmp;
roots.reset();
m_am.isolate_roots(p, undef_var_assignment(m_assignment, x), roots);
for (auto const& r : roots) {
int s = m_am.compare(x_val, r);
SASSERT(s != 0);
if (s < 0 && (!lub_valid || m_am.lt(r, lub))) {
lub_index = i;
m_am.set(lub, r);
lub_valid = true;
}
if (s > 0 && (!glb_valid || m_am.lt(glb, r))) {
glb_index = i;
m_am.set(glb, r);
glb_valid = true;
}
if (s < 0) ++num_lub;
if (s > 0) ++num_glb;
}
}
TRACE(nlsat_explain, tout << "glb: " << num_glb << " lub: " << num_lub << "\n" << lub_index << "\n" << glb_index << "\n" << ps << "\n";);
if (num_lub == 0) {
project_plus_infinity(x, ps);
return;
}
if (num_glb == 0) {
project_minus_infinity(x, ps);
return;
}
if (num_lub <= num_glb) {
glb_index = lub_index;
}
project_pairs(x, glb_index, ps);
}
void project_plus_infinity(var x, polynomial_ref_vector const& ps) {
polynomial_ref p(m_pm), lc(m_pm);
for (unsigned i = 0; i < ps.size(); ++i) {
p = ps.get(i);
unsigned d = degree(p, x);
lc = m_pm.coeff(p, x, d);
if (!is_const(lc)) {
int s = sign(p);
SASSERT(s != 0);
atom::kind k = (s > 0)?(atom::GT):(atom::LT);
add_simple_assumption(k, lc);
}
}
}
void project_minus_infinity(var x, polynomial_ref_vector const& ps) {
polynomial_ref p(m_pm), lc(m_pm);
for (unsigned i = 0; i < ps.size(); ++i) {
p = ps.get(i);
unsigned d = degree(p, x);
lc = m_pm.coeff(p, x, d);
if (!is_const(lc)) {
int s = sign(p);
TRACE(nlsat_explain, tout << "degree: " << d << " " << lc << " sign: " << s << "\n";);
SASSERT(s != 0);
atom::kind k;
if (s > 0) {
k = (d % 2 == 0)?(atom::GT):(atom::LT);
}
else {
k = (d % 2 == 0)?(atom::LT):(atom::GT);
}
add_simple_assumption(k, lc);
}
}
}
void project_pairs(var x, unsigned idx, polynomial_ref_vector const& ps) {
TRACE(nlsat_explain, tout << "project pairs\n";);
polynomial_ref p(m_pm);
p = ps.get(idx);
for (unsigned i = 0; i < ps.size(); ++i) {
if (i != idx) {
project_pair(x, ps.get(i), p);
}
}
}
void project_pair(var x, polynomial::polynomial* p1, polynomial::polynomial* p2) {
m_ps2.reset();
m_ps2.push_back(p1);
m_ps2.push_back(p2);
project(m_ps2, x);
}
void project_single(var x, polynomial::polynomial* p) {
m_ps2.reset();
m_ps2.push_back(p);
project(m_ps2, x);
}
void solve_eq(var x, unsigned idx, polynomial_ref_vector const& ps) {
polynomial_ref p(m_pm), A(m_pm), B(m_pm), C(m_pm), D(m_pm), E(m_pm), q(m_pm), r(m_pm);
polynomial_ref_vector As(m_pm), Bs(m_pm);
p = ps.get(idx);
SASSERT(degree(p, x) == 1);
A = m_pm.coeff(p, x, 1);
B = m_pm.coeff(p, x, 0);
As.push_back(m_pm.mk_const(rational(1)));
Bs.push_back(m_pm.mk_const(rational(1)));
B = neg(B);
TRACE(nlsat_explain, tout << "p: " << p << " A: " << A << " B: " << B << "\n";);
// x = B/A
for (unsigned i = 0; i < ps.size(); ++i) {
if (i != idx) {
q = ps.get(i);
unsigned d = degree(q, x);
D = m_pm.mk_const(rational(1));
E = D;
r = m_pm.mk_zero();
for (unsigned j = As.size(); j <= d; ++j) {
D = As.back(); As.push_back(A * D);
D = Bs.back(); Bs.push_back(B * D);
}
for (unsigned j = 0; j <= d; ++j) {
// A^d*p0 + A^{d-1}*B*p1 + ... + B^j*A^{d-j}*pj + ... + B^d*p_d
C = m_pm.coeff(q, x, j);
TRACE(nlsat_explain, tout << "coeff: q" << j << ": " << C << "\n";);
if (!is_zero(C)) {
D = As.get(d - j);
E = Bs.get(j);
r = r + D*E*C;
}
}
TRACE(nlsat_explain, tout << "p: " << p << " q: " << q << " r: " << r << "\n";);
ensure_sign(r);
}
else {
ensure_sign(A);
}
}
}
void maximize(var x, unsigned num, literal const * ls, scoped_anum& val, bool& unbounded) {
svector<literal> lits;
polynomial_ref p(m_pm);
split_literals(x, num, ls, lits);
collect_polys(lits.size(), lits.data(), m_ps);
unbounded = true;
scoped_anum x_val(m_am);
x_val = m_assignment.value(x);
for (unsigned i = 0; i < m_ps.size(); ++i) {
p = m_ps.get(i);
scoped_anum_vector & roots = m_roots_tmp;
roots.reset();
m_am.isolate_roots(p, undef_var_assignment(m_assignment, x), roots);
for (unsigned j = 0; j < roots.size(); ++j) {
int s = m_am.compare(x_val, roots[j]);
if (s <= 0 && (unbounded || m_am.compare(roots[j], val) <= 0)) {
unbounded = false;
val = roots[j];
}
}
}
}
};
explain::explain(solver & s, assignment const & x2v, polynomial::cache & u,
atom_vector const& atoms, atom_vector const& x2eq, evaluator & ev, bool use_cell_sample, bool use_lazard) {
m_imp = alloc(imp, s, x2v, u, atoms, x2eq, ev, use_cell_sample, use_lazard);
}
explain::~explain() {
dealloc(m_imp);
}
void explain::reset() {
m_imp->m_core1.reset();
m_imp->m_core2.reset();
}
void explain::set_simplify_cores(bool f) {
m_imp->m_simplify_cores = f;
}
void explain::set_full_dimensional(bool f) {
m_imp->m_full_dimensional = f;
}
void explain::set_minimize_cores(bool f) {
m_imp->m_minimize_cores = f;
}
void explain::set_factor(bool f) {
m_imp->m_factor = f;
}
void explain::set_add_all_coeffs(bool f) {
m_imp->m_add_all_coeffs = f;
}
void explain::set_signed_project(bool f) {
m_imp->m_signed_project = f;
}
void explain::set_lazard(bool f) {
m_imp->m_lazard = f;
}
void explain::main_operator(unsigned n, literal const * ls, scoped_literal_vector & result) {
(*m_imp)(n, ls, result);
}
void explain::project(var x, unsigned n, literal const * ls, scoped_literal_vector & result) {
m_imp->project(x, n, ls, result);
}
void explain::maximize(var x, unsigned n, literal const * ls, scoped_anum& val, bool& unbounded) {
m_imp->maximize(x, n, ls, val, unbounded);
}
void explain::test_root_literal(atom::kind k, var y, unsigned i, poly* p, scoped_literal_vector & result) {
m_imp->test_root_literal(k, y, i, p, result);
}
};
#ifdef Z3DEBUG
#include <iostream>
void pp(nlsat::explain::imp & ex, unsigned num, nlsat::literal const * ls) {
ex.display(std::cout, num, ls);
}
void pp(nlsat::explain::imp & ex, nlsat::scoped_literal_vector & ls) {
ex.display(std::cout, ls);
}
void pp(nlsat::explain::imp & ex, polynomial_ref const & p) {
ex.display(std::cout, p);
std::cout << std::endl;
}
void pp(nlsat::explain::imp & ex, polynomial::polynomial * p) {
polynomial_ref _p(p, ex.m_pm);
ex.display(std::cout, _p);
std::cout << std::endl;
}
void pp(nlsat::explain::imp & ex, polynomial_ref_vector const & ps) {
ex.display(std::cout, ps);
}
void pp_var(nlsat::explain::imp & ex, nlsat::var x) {
ex.display(std::cout, x);
std::cout << std::endl;
}
void pp_lit(nlsat::explain::imp & ex, nlsat::literal l) {
ex.display(std::cout, l);
std::cout << std::endl;
}
#endif
View git blame Copy permalink