mirror of
https://github.com/Z3Prover/z3
synced 2025-09-03 16:48:06 +00:00
Nl2lin (#7827)
* fix linear projection * fix linear projection * use an explicit cell description in check_assignment
This commit is contained in:
ValentinPromies
GitHub
parent
6ef8a0b7bb
commit
187f013224
4 changed files with 48 additions and 41 deletions
|
|
@ -256,6 +256,7 @@ struct solver::imp {
|
|||
lbool r = l_undef;
|
||||
statistics& st = m_nla_core.lp_settings().stats().m_st;
|
||||
nlsat::atom_vector clause;
|
||||
nlsat::literal_vector cell;
|
||||
polynomial::manager& pm = m_nlsat->pm();
|
||||
try {
|
||||
nlsat::assignment rvalues(m_nlsat->am());
|
||||
|
|
@ -264,8 +265,7 @@ struct solver::imp {
|
|||
am().set(a, m_nla_core.val(j).to_mpq());
|
||||
rvalues.set(x, a);
|
||||
}
|
||||
r = m_nlsat->check(rvalues, clause);
|
||||
|
||||
r = m_nlsat->check(rvalues, clause, cell);
|
||||
}
|
||||
catch (z3_exception&) {
|
||||
if (m_limit.is_canceled()) {
|
||||
|
|
@ -294,8 +294,11 @@ struct solver::imp {
|
|||
u_map<lp::lpvar> nl2lp;
|
||||
for (auto [j, x] : m_lp2nl)
|
||||
nl2lp.insert(x, j);
|
||||
for (auto a : clause) {
|
||||
// a cannot be a root object.
|
||||
|
||||
nla::lemma_builder lemma(m_nla_core, __FUNCTION__);
|
||||
lemma &= ex;
|
||||
|
||||
auto translate_atom = [&](nlsat::atom* a, bool negated){
|
||||
SASSERT(!a->is_root_atom());
|
||||
SASSERT(a->is_ineq_atom());
|
||||
auto& ia = *to_ineq_atom(a);
|
||||
|
|
@ -305,9 +308,6 @@ struct solver::imp {
|
|||
unsigned num_mon = pm.size(p);
|
||||
rational bound(0);
|
||||
lp::lar_term t;
|
||||
|
||||
nla::lemma_builder lemma(m_nla_core, __FUNCTION__);
|
||||
lemma &= ex;
|
||||
for (unsigned i = 0; i < num_mon; ++i) {
|
||||
polynomial::monomial* m = pm.get_monomial(p, i);
|
||||
auto& coeff = pm.coeff(p, i);
|
||||
|
|
@ -336,7 +336,6 @@ struct solver::imp {
|
|||
v = mon->var();
|
||||
else {
|
||||
NOT_IMPLEMENTED_YET();
|
||||
return l_undef;
|
||||
// this one is for Lev Nachmanson: lar_solver relies on internal variables
|
||||
// to have terms from outside. The solver doesn't get to create
|
||||
// its own monomials.
|
||||
|
|
@ -349,24 +348,29 @@ struct solver::imp {
|
|||
break;
|
||||
}
|
||||
}
|
||||
}
|
||||
TRACE(nra, this->lra.print_term(t, tout << "t:") << std::endl;);
|
||||
}
|
||||
switch (a->get_kind()) {
|
||||
case nlsat::atom::EQ:
|
||||
lemma |= nla::ineq(lp::lconstraint_kind::EQ, t, bound);
|
||||
break;
|
||||
case nlsat::atom::LT:
|
||||
lemma |= nla::ineq(lp::lconstraint_kind::LT, t, bound);
|
||||
break;
|
||||
case nlsat::atom::GT:
|
||||
lemma |= nla::ineq(lp::lconstraint_kind::GT, t, bound);
|
||||
break;
|
||||
case nlsat::atom::EQ:
|
||||
return nla::ineq(negated ? lp::lconstraint_kind::NE : lp::lconstraint_kind::EQ, t, bound);
|
||||
case nlsat::atom::LT:
|
||||
return nla::ineq(negated ? lp::lconstraint_kind::GE : lp::lconstraint_kind::LT, t, bound);
|
||||
case nlsat::atom::GT:
|
||||
return nla::ineq(negated ? lp::lconstraint_kind::LE : lp::lconstraint_kind::GT, t, bound);
|
||||
default:
|
||||
UNREACHABLE();
|
||||
}
|
||||
};
|
||||
|
||||
IF_VERBOSE(1, verbose_stream() << "linear lemma: " << lemma << "\n");
|
||||
|
||||
for (auto a : clause) {
|
||||
lemma |= translate_atom(a, true);
|
||||
}
|
||||
|
||||
for (nlsat::literal l : cell) {
|
||||
lemma |= translate_atom( m_nlsat->bool_var2atom(l.var()), l.sign());
|
||||
}
|
||||
|
||||
IF_VERBOSE(1, verbose_stream() << "linear lemma: " << lemma << "\n");
|
||||
m_nla_core.set_use_nra_model(true);
|
||||
break;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1287,7 +1287,6 @@ namespace nlsat {
|
|||
bool lower_inf = true, upper_inf = true;
|
||||
scoped_anum lower(m_am), upper(m_am);
|
||||
polynomial_ref p_lower(m_pm), p_upper(m_pm);
|
||||
unsigned i_lower = UINT_MAX, i_upper = UINT_MAX;
|
||||
|
||||
scoped_anum_vector & roots = m_roots_tmp;
|
||||
polynomial_ref p(m_pm);
|
||||
|
|
@ -1317,7 +1316,6 @@ namespace nlsat {
|
|||
// roots[i] == x_val
|
||||
ps_equal.push_back(p);
|
||||
p_lower = p;
|
||||
i_lower = i+1;
|
||||
break; // TODO: choose the best among multiple section polynomials?
|
||||
}
|
||||
else if (s < 0) {
|
||||
|
|
@ -1327,7 +1325,6 @@ namespace nlsat {
|
|||
upper_inf = false;
|
||||
m_am.set(upper, roots[i]);
|
||||
p_upper = p;
|
||||
i_upper = i + 1;
|
||||
}
|
||||
}
|
||||
// in any case, roots[i-1] might provide a lower bound if it exists
|
||||
|
|
@ -1338,7 +1335,6 @@ namespace nlsat {
|
|||
lower_inf = false;
|
||||
m_am.set(lower, roots[i-1]);
|
||||
p_lower = p;
|
||||
i_lower = i;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -1354,7 +1350,7 @@ namespace nlsat {
|
|||
rational bound;
|
||||
m_am.to_rational(x_val, bound);
|
||||
p_lower = m_pm.mk_polynomial(x);
|
||||
p_lower = p_lower - bound;
|
||||
p_lower = denominator(bound)*p_lower - numerator(bound);
|
||||
}
|
||||
add_root_literal(atom::ROOT_EQ, x, 1, p_lower);
|
||||
// make sure bounding poly is at the back of the vector
|
||||
|
|
@ -1369,9 +1365,9 @@ namespace nlsat {
|
|||
rational new_bound;
|
||||
m_am.to_rational(between, new_bound);
|
||||
p_lower = m_pm.mk_polynomial(x);
|
||||
p_lower = p_lower - new_bound;
|
||||
p_lower = denominator(new_bound)*p_lower - numerator(new_bound);
|
||||
}
|
||||
add_root_literal((approximate || m_full_dimensional) ? atom::ROOT_GE : atom::ROOT_GT, x, 1, p_lower);
|
||||
add_root_literal((/*approximate ||*/ m_full_dimensional) ? atom::ROOT_GE : atom::ROOT_GT, x, 1, p_lower);
|
||||
// make sure bounding poly is at the back of the vector
|
||||
ps_below.push_back(p_lower);
|
||||
}
|
||||
|
|
@ -1383,11 +1379,11 @@ namespace nlsat {
|
|||
rational new_bound;
|
||||
m_am.to_rational(between, new_bound);
|
||||
p_upper = m_pm.mk_polynomial(x);
|
||||
p_upper = p_upper - new_bound;
|
||||
p_upper = denominator(new_bound)*p_upper - numerator(new_bound);
|
||||
}
|
||||
add_root_literal((approximate || m_full_dimensional) ? atom::ROOT_LE : atom::ROOT_LT, x, 1, p_upper);
|
||||
add_root_literal((/*approximate ||*/ m_full_dimensional) ? atom::ROOT_LE : atom::ROOT_LT, x, 1, p_upper);
|
||||
// make sure bounding poly is at the back of the vector
|
||||
ps_below.push_back(p_upper);
|
||||
ps_above.push_back(p_upper);
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -1424,7 +1420,7 @@ namespace nlsat {
|
|||
polynomial_ref_vector ps_above_sample(m_pm);
|
||||
polynomial_ref_vector ps_equal_sample(m_pm);
|
||||
var x = m_todo.extract_max_polys(ps);
|
||||
if (x == max_x) {
|
||||
if (!m_assignment.is_assigned(x)) {
|
||||
// top level projection like original
|
||||
// we could also do a covering-style projection, sparing some resultants
|
||||
add_lcs(ps, x);
|
||||
|
|
@ -1433,7 +1429,7 @@ namespace nlsat {
|
|||
x = m_todo.extract_max_polys(ps);
|
||||
}
|
||||
|
||||
while (!m_todo.empty()) {
|
||||
while (true) {
|
||||
add_cell_lits_linear(ps, x, ps_below_sample, ps_above_sample, ps_equal_sample);
|
||||
if (all_univ(ps, x) && m_todo.empty()) {
|
||||
m_todo.reset();
|
||||
|
|
@ -1463,6 +1459,8 @@ namespace nlsat {
|
|||
}
|
||||
}
|
||||
}
|
||||
if (m_todo.empty())
|
||||
break;
|
||||
x = m_todo.extract_max_polys(ps);
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -2034,7 +2034,7 @@ namespace nlsat {
|
|||
m_assignment.reset();
|
||||
}
|
||||
|
||||
lbool check(assignment const& rvalues, atom_vector& core) {
|
||||
lbool check(assignment const& rvalues, atom_vector& core, literal_vector& cell) {
|
||||
// temporarily set m_assignment to the given one
|
||||
assignment tmp = m_assignment;
|
||||
m_assignment.reset();
|
||||
|
|
@ -2042,7 +2042,6 @@ namespace nlsat {
|
|||
|
||||
// check whether the asserted atoms are satisfied by rvalues
|
||||
literal best_literal = null_literal;
|
||||
unsigned sz = m_clauses.size();
|
||||
lbool satisfied = l_true;
|
||||
for (auto cp : m_clauses) {
|
||||
auto& c = *cp;
|
||||
|
|
@ -2077,17 +2076,22 @@ namespace nlsat {
|
|||
|
||||
// assignment does not satisfy the constraints -> create lemma
|
||||
SASSERT(best_literal != null_literal);
|
||||
cell.reset();
|
||||
m_lazy_clause.reset();
|
||||
m_explain.set_linear_project(true);
|
||||
m_explain.main_operator(1, &best_literal, m_lazy_clause);
|
||||
m_explain.set_linear_project(false);
|
||||
m_lazy_clause.push_back(~best_literal);
|
||||
|
||||
core.clear();
|
||||
for (literal l : m_lazy_clause) {
|
||||
core.push_back(m_atoms[l.var()]);
|
||||
for (auto l : m_lazy_clause) {
|
||||
cell.push_back(l);
|
||||
}
|
||||
|
||||
m_lemma_assumptions = nullptr;
|
||||
|
||||
core.clear();
|
||||
SASSERT(!best_literal.sign());
|
||||
core.push_back(m_atoms[best_literal.var()]);
|
||||
|
||||
m_assignment.reset();
|
||||
m_assignment.copy(tmp);
|
||||
return l_false;
|
||||
|
|
@ -4163,8 +4167,8 @@ namespace nlsat {
|
|||
return m_imp->check(assumptions);
|
||||
}
|
||||
|
||||
lbool solver::check(assignment const& rvalues, atom_vector& clause) {
|
||||
return m_imp->check(rvalues, clause);
|
||||
lbool solver::check(assignment const& rvalues, atom_vector& clause, literal_vector& cell) {
|
||||
return m_imp->check(rvalues, clause, cell);
|
||||
}
|
||||
|
||||
void solver::get_core(vector<assumption, false>& assumptions) {
|
||||
|
|
|
|||
|
|
@ -228,8 +228,9 @@ namespace nlsat {
|
|||
// clause is a list of atoms. Their negations conjoined with core literals are unsatisfiable.
|
||||
// Different implementations of check are possible. One where core comprises of linear polynomials could
|
||||
// produce lemmas that are friendly to linear arithmetic solvers.
|
||||
// TODO: update
|
||||
//
|
||||
lbool check(assignment const& rvalues, atom_vector& clause);
|
||||
lbool check(assignment const& rvalues, atom_vector& clause, literal_vector& cell);
|
||||
|
||||
// -----------------------
|
||||
//
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue