mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-12-02 01:59:05 +00:00
Code Activity

integrating changes from master related to work with polynomials

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-11-24 13:00:43 -10:00
parent 6cbc6f4f84
commit ddba2cc381
9 changed files with 390 additions and 530 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/math/lp/CMakeLists.txt
View file

@ -24,6 +24,7 @@ z3_add_component(lp
monomial_bounds.cpp
nex_creator.cpp
nla_basics_lemmas.cpp
nla_coi.cpp
nla_common.cpp
nla_core.cpp
nla_divisions.cpp
@ -32,6 +33,7 @@ z3_add_component(lp
nla_monotone_lemmas.cpp
nla_order_lemmas.cpp
nla_powers.cpp
nla_pp.cpp
nla_solver.cpp
nla_tangent_lemmas.cpp
nla_throttle.cpp

320
src/math/lp/nla_core.cpp
View file

@ -1,4 +1,4 @@
/*++
/*++
Copyright (c) 2017 Microsoft Corporation
Module Name:
@ -17,6 +17,7 @@ Author:
#include "math/grobner/pdd_solver.h"
#include "math/dd/pdd_interval.h"
#include "math/dd/pdd_eval.h"
using namespace nla;
typedef lp::lar_term term;
@ -38,7 +39,7 @@ core::core(lp::lar_solver& s, params_ref const& p, reslimit & lim) :
m_grobner(this),
m_emons(m_evars),
m_use_nra_model(false),
m_nra(s, m_nra_lim, *this),
m_nra(s, m_nra_lim, *this, p),
m_throttle(lra.trail(),
lra.settings().stats()) {
m_nlsat_delay_bound = lp_settings().nlsat_delay();
@ -51,6 +52,10 @@ core::core(lp::lar_solver& s, params_ref const& p, reslimit & lim) :
}
};
}
void core::updt_params(params_ref const& p) {
// grobner updt_params is a no-op on this branch
}
bool core::compare_holds(const rational& ls, llc cmp, const rational& rs) const {
switch(cmp) {
@ -88,13 +93,6 @@ lpvar core::map_to_root(lpvar j) const {
return m_evars.find(j).var();
}
// Reduce a single variable to its root and provide the reduction sign.
lpvar core::reduce_var_to_rooted(lpvar j, rational & sign) const {
auto root = m_evars.find(j);
sign = rational(root.sign() ? -1 : 1);
return root.var();
}
svector<lpvar> core::sorted_rvars(const factor& f) const {
if (f.is_var()) {
svector<lpvar> r; r.push_back(map_to_root(f.var()));
@ -179,108 +177,6 @@ bool core::check_monic(const monic& m) const {
}
template <typename T>
std::ostream& core::print_product(const T & m, std::ostream& out) const {
bool first = true;
for (lpvar v : m) {
if (!first) out << "*"; else first = false;
if (lp_settings().print_external_var_name())
out << "(" << lra.get_variable_name(v) << "=" << val(v) << ")";
else
out << "(j" << v << " = " << val(v) << ")";
}
return out;
}
template <typename T>
std::string core::product_indices_str(const T & m) const {
std::stringstream out;
bool first = true;
for (lpvar v : m) {
if (!first)
out << "*";
else
first = false;
out << "j" << v;;
}
return out.str();
}
std::ostream & core::print_factor(const factor& f, std::ostream& out) const {
if (f.sign())
out << "- ";
if (f.is_var()) {
out << "VAR, " << pp(f.var());
} else {
out << "MON, v" << m_emons[f.var()] << " = ";
print_product(m_emons[f.var()].rvars(), out);
}
out << "\n";
return out;
}
std::ostream & core::print_factor_with_vars(const factor& f, std::ostream& out) const {
if (f.is_var()) {
out << pp(f.var());
}
else {
out << " MON = " << pp_mon_with_vars(*this, m_emons[f.var()]);
}
return out;
}
std::ostream& core::print_monic(const monic& m, std::ostream& out) const {
if (lp_settings().print_external_var_name())
out << "([" << m.var() << "] = " << lra.get_variable_name(m.var()) << " = " << val(m.var()) << " = ";
else
out << "(j" << m.var() << " = " << val(m.var()) << " = ";
print_product(m.vars(), out) << ")\n";
return out;
}
std::ostream& core::print_bfc(const factorization& m, std::ostream& out) const {
SASSERT(m.size() == 2);
out << "( x = " << pp(m[0]) << "* y = " << pp(m[1]) << ")";
return out;
}
std::ostream& core::print_monic_with_vars(lpvar v, std::ostream& out) const {
return print_monic_with_vars(m_emons[v], out);
}
template <typename T>
std::ostream& core::print_product_with_vars(const T& m, std::ostream& out) const {
print_product(m, out) << "\n";
for (unsigned k = 0; k < m.size(); k++) {
print_var(m[k], out);
}
return out;
}
std::ostream& core::print_monic_with_vars(const monic& m, std::ostream& out) const {
out << "[" << pp(m.var()) << "]\n";
out << "vars:"; print_product_with_vars(m.vars(), out) << "\n";
if (m.vars() == m.rvars())
out << "same rvars, and m.rsign = " << m.rsign() << " of course\n";
else {
out << "rvars:"; print_product_with_vars(m.rvars(), out) << "\n";
out << "rsign:" << m.rsign() << "\n";
}
return out;
}
std::ostream& core::print_explanation(const lp::explanation& exp, std::ostream& out) const {
out << "expl: ";
unsigned i = 0;
for (auto p : exp) {
out << "(" << p.ci() << ")";
lra.constraints().display(out, [this](lpvar j) { return var_str(j);}, p.ci());
if (++i < exp.size())
out << " ";
}
return out;
}
bool core::explain_upper_bound(const lp::lar_term& t, const rational& rs, lp::explanation& e) const {
rational b(0); // the bound
for (lp::lar_term::ival p : t) {
@ -558,69 +454,6 @@ bool core::var_is_free(lpvar j) const {
return lra.column_is_free(j);
}
std::ostream & core::print_ineq(const ineq & in, std::ostream & out) const {
lra.print_term_as_indices(in.term(), out);
return out << " " << lconstraint_kind_string(in.cmp()) << " " << in.rs();
}
std::ostream & core::print_var(lpvar j, std::ostream & out) const {
if (is_monic_var(j))
print_monic(m_emons[j], out);
lra.print_column_info(j, out);
signed_var jr = m_evars.find(j);
out << "root=";
if (jr.sign()) {
out << "-";
}
out << lra.get_variable_name(jr.var()) << "\n";
return out;
}
std::ostream & core::print_monics(std::ostream & out) const {
for (auto &m : m_emons) {
print_monic_with_vars(m, out);
}
return out;
}
std::ostream & core::print_ineqs(const lemma& l, std::ostream & out) const {
std::unordered_set<lpvar> vars;
out << "ineqs: ";
if (l.ineqs().size() == 0) {
out << "conflict\n";
} else {
for (unsigned i = 0; i < l.ineqs().size(); i++) {
auto & in = l.ineqs()[i];
print_ineq(in, out);
if (i + 1 < l.ineqs().size()) out << " or ";
for (lp::lar_term::ival p: in.term())
vars.insert(p.j());
}
out << std::endl;
for (lpvar j : vars) {
print_var(j, out);
}
out << "\n";
}
return out;
}
std::ostream & core::print_factorization(const factorization& f, std::ostream& out) const {
if (f.is_mon()){
out << "is_mon " << pp_mon(*this, f.mon());
}
else {
for (unsigned k = 0; k < f.size(); k++ ) {
out << "(" << pp(f[k]) << ")";
if (k < f.size() - 1)
out << "*";
}
}
return out;
}
bool core::find_canonical_monic_of_vars(const svector<lpvar>& vars, lpvar & i) const {
monic const* sv = m_emons.find_canonical(vars);
return sv && (i = sv->var(), true);
@ -630,16 +463,6 @@ bool core::is_canonical_monic(lpvar j) const {
return m_emons.is_canonical_monic(j);
}
void core::trace_print_monic_and_factorization(const monic& rm, const factorization& f, std::ostream& out) const {
out << "rooted vars: ";
print_product(rm.rvars(), out) << "\n";
out << "mon: " << pp_mon(*this, rm.var()) << "\n";
out << "value: " << var_val(rm) << "\n";
print_factorization(f, out << "fact: ") << "\n";
}
bool core::var_has_positive_lower_bound(lpvar j) const {
return lra.column_has_lower_bound(j) && lra.get_lower_bound(j) > lp::zero_of_type<lp::impq>();
}
@ -778,35 +601,6 @@ bool core::vars_are_roots(const T& v) const {
}
template <typename T>
void core::trace_print_rms(const T& p, std::ostream& out) {
out << "p = {\n";
for (auto j : p) {
out << "j = " << j << ", rm = " << m_emons[j] << "\n";
}
out << "}";
}
void core::print_monic_stats(const monic& m, std::ostream& out) {
if (m.size() == 2) return;
monic_coeff mc = canonize_monic(m);
for(unsigned i = 0; i < mc.vars().size(); i++){
if (abs(val(mc.vars()[i])) == rational(1)) {
auto vv = mc.vars();
vv.erase(vv.begin()+i);
monic const* sv = m_emons.find_canonical(vv);
if (!sv) {
out << "nf length" << vv.size() << "\n"; ;
}
}
}
}
void core::print_stats(std::ostream& out) {
}
void core::clear() {
m_lemmas.clear();
m_literals.clear();
@ -1055,7 +849,6 @@ lemma_builder::lemma_builder(core& c, const char* name):name(name), c(c) {
lemma_builder& lemma_builder::operator|=(ineq const& ineq) {
if (!c.explain_ineq(*this, ineq.term(), ineq.cmp(), ineq.rs())) {
CTRACE(nla_solver, c.ineq_holds(ineq), c.print_ineq(ineq, tout) << "\n";);
CTRACE(nra, c.ineq_holds(ineq), c.print_ineq(ineq, tout) << "\n";);
SASSERT(c.m_use_nra_model || !c.ineq_holds(ineq));
current().push_back(ineq);
}
@ -1515,6 +1308,10 @@ lbool core::check() {
if (no_effect())
m_monomial_bounds.propagate();
if (no_effect() && refine_pseudo_linear())
return l_false;
{
std::function<void(void)> check1 = [&]() { if (no_effect() && run_horner) m_horner.horner_lemmas(); };
@ -1537,9 +1334,9 @@ lbool core::check() {
scoped_limits sl(m_reslim);
sl.push_child(&m_nra_lim);
ret = m_nra.check_assignment();
IF_VERBOSE(1, verbose_stream() << "nra check_assignment returned " << ret << "\n";);
}
else if (no_effect() && should_run_bounded_nlsat())
}
if (no_effect() && should_run_bounded_nlsat())
ret = bounded_nlsat();
if (no_effect())
@ -1551,6 +1348,7 @@ lbool core::check() {
if (no_effect())
m_divisions.check();
if (no_effect()) {
std::function<void(void)> check1 = [&]() { m_order.order_lemma();
};
@ -1577,10 +1375,7 @@ lbool core::check() {
lp_settings().stats().m_nra_calls++;
}
if (ret == l_undef)
return l_undef;
if (!no_effect() && m_reslim.inc())
if (ret == l_undef && !no_effect() && m_reslim.inc())
ret = l_false;
lp_settings().stats().m_nla_lemmas += m_lemmas.size();
@ -1588,6 +1383,8 @@ lbool core::check() {
TRACE(nla_solver, tout << "ret = " << ret << ", lemmas count = " << m_lemmas.size() << "\n";);
IF_VERBOSE(5, if(ret == l_undef) {verbose_stream() << "Monomials\n"; print_monics(verbose_stream());});
CTRACE(nla_solver, ret == l_undef, tout << "Monomials\n"; print_monics(tout););
CTRACE(nla_solver, ret == l_undef, display_smt(tout););
// if (ret == l_undef) IF_VERBOSE(0, display_smt(verbose_stream()));
return ret;
}
@ -1600,18 +1397,13 @@ bool core::should_run_bounded_nlsat() {
}
lbool core::bounded_nlsat() {
params_ref p;
lbool ret;
p.set_uint("max_conflicts", 100);
m_nra.updt_params(p);
{
scoped_limits sl(m_reslim);
sl.push_child(&m_nra_lim);
scoped_rlimit sr(m_nra_lim, 100000);
ret = m_nra.check();
}
p.set_uint("max_conflicts", UINT_MAX);
m_nra.updt_params(p);
lp_settings().stats().m_nra_calls++;
if (ret == l_undef)
++m_nlsat_delay_bound;
@ -1635,40 +1427,11 @@ bool core::no_lemmas_hold() const {
return true;
}
lbool core::test_check() {
lra.set_status(lp::lp_status::OPTIMAL);
return check();
}
std::ostream& core::print_terms(std::ostream& out) const {
for (const auto * t: lra.terms()) {
out << "term:"; print_term(*t, out) << std::endl;
print_var(t->j(), out);
}
return out;
}
std::string core::var_str(lpvar j) const {
std::string result;
if (is_monic_var(j))
result += product_indices_str(m_emons[j].vars()) + (check_monic(m_emons[j])? "": "_");
else
result += std::string("j") + lp::T_to_string(j);
// result += ":w" + lp::T_to_string(get_var_weight(j));
return result;
}
std::ostream& core::print_term( const lp::lar_term& t, std::ostream& out) const {
return lp::print_linear_combination_customized(
t.coeffs_as_vector(),
[this](lpvar j) { return var_str(j); },
out);
}
std::unordered_set<lpvar> core::get_vars_of_expr_with_opening_terms(const nex *e ) {
auto ret = get_vars_of_expr(e);
auto & ls = lra;
@ -1691,12 +1454,10 @@ std::unordered_set<lpvar> core::get_vars_of_expr_with_opening_terms(const nex *e
return ret;
}
bool core::is_nl_var(lpvar j) const {
return is_monic_var(j) || m_emons.is_used_in_monic(j);
}
unsigned core::get_var_weight(lpvar j) const {
unsigned k = 0;
switch (lra.get_column_type(j)) {
@ -1765,6 +1526,49 @@ void core::simplify() {
}
bool core::is_pseudo_linear(monic const& m) const {
bool has_unbounded = false;
for (auto v : m.vars()) {
if (lra.column_is_bounded(v) && lra.var_is_int(v)) {
auto lb = lra.get_lower_bound(v);
auto ub = lra.get_upper_bound(v);
if (ub - lb <= rational(4))
continue;
}
if (has_unbounded)
return false;
has_unbounded = true;
}
return true;
}
bool core::refine_pseudo_linear() {
// Parameter support for this optimization is unavailable in this branch.
return false;
}
void core::refine_pseudo_linear(monic const& m) {
lemma_builder lemma(*this, "nla-pseudo-linear");
lpvar nlvar = null_lpvar;
rational prod(1);
for (unsigned i = 0; i < m.vars().size(); ++i) {
auto v = m.vars()[i];
if (i == m.vars().size() - 1 && nlvar == null_lpvar) {
nlvar = v;
break;
}
if (lra.column_is_bounded(v) && lra.var_is_int(v)) {
auto lb = lra.get_lower_bound(v);
auto ub = lra.get_upper_bound(v);
if (ub - lb <= rational(4)) {
lemma |= ineq(v, llc::NE, val(v));
prod *= val(v);
continue;
}
}
SASSERT(nlvar == null_lpvar);
nlvar = v;
}
SASSERT(nlvar != null_lpvar);
lemma |= ineq(lp::lar_term(m.var(), rational(-prod), nlvar), llc::EQ, rational(0));
}

27
src/math/lp/nla_core.h
View file

@ -113,7 +113,12 @@ class core {
void check_weighted(unsigned sz, std::pair<unsigned, std::function<void(void)>>* checks);
void add_bounds();
bool refine_pseudo_linear();
bool is_pseudo_linear(monic const& m) const;
void refine_pseudo_linear(monic const& m);
std::ostream& display_constraint_smt(std::ostream& out, unsigned id, lp::lar_base_constraint const& c) const;
std::ostream& display_declarations_smt(std::ostream& out) const;
public:
// constructor
@ -121,6 +126,8 @@ public:
const auto& monics_with_changed_bounds() const { return m_monics_with_changed_bounds; }
void insert_to_refine(lpvar j);
void erase_from_to_refine(lpvar j);
void updt_params(params_ref const& p);
const indexed_uint_set& active_var_set () const { return m_active_var_set;}
bool active_var_set_contains(unsigned j) const { return m_active_var_set.contains(j); }
@ -228,6 +235,9 @@ public:
bool check_monic(const monic& m) const;
std::ostream & display_row(std::ostream& out, lp::row_strip<lp::mpq> const& row) const;
std::ostream & display(std::ostream& out);
std::ostream& display_smt(std::ostream& out);
std::ostream & print_ineq(const ineq & in, std::ostream & out) const;
std::ostream & print_var(lpvar j, std::ostream & out) const;
std::ostream & print_monics(std::ostream & out) const;
@ -285,12 +295,8 @@ public:
svector<lpvar> reduce_monic_to_rooted(const svector<lpvar> & vars, rational & sign) const;
// Reduce a single variable to its canonical root under current equalities
// and return the convertion sign as either 1 or -1
lpvar reduce_var_to_rooted(lpvar v, rational & sign) const;
monic_coeff canonize_monic(monic const& m) const;
int vars_sign(const svector<lpvar>& v);
bool has_upper_bound(lpvar j) const;
bool has_lower_bound(lpvar j) const;
@ -365,6 +371,10 @@ public:
template <typename T>
bool vars_are_roots(const T& v) const;
void register_monic_in_tables(unsigned i_mon);
void register_monics_in_tables();
void clear();
void init_search();
@ -444,6 +454,12 @@ public:
nla_throttle& throttle() { return m_throttle; }
const nla_throttle& throttle() const { return m_throttle; }
lp::lar_solver& lra_solver() { return lra; }
indexed_uint_set const& to_refine() const {
return m_to_refine;
}
}; // end of core
struct pp_mon {
@ -466,4 +482,3 @@ inline std::ostream& operator<<(std::ostream& out, pp_factorization const& f) {
inline std::ostream& operator<<(std::ostream& out, pp_var const& v) { return v.c.print_var(v.v, out); }
} // end of namespace nla

4
src/math/lp/nla_grobner.cpp
View file

@ -98,6 +98,10 @@ namespace nla {
return m_solver.equations();
}
void grobner::updt_params(params_ref const&) {
// placeholder: nl2lin branch does not expose grobner-specific params from master
}
bool grobner::is_conflicting() {
for (auto eq : m_solver.equations()) {
if (is_conflicting(*eq)) {

2
src/math/lp/nla_grobner.h
View file

@ -12,6 +12,7 @@
#include "math/lp/nla_intervals.h"
#include "math/lp/nex.h"
#include "math/lp/cross_nested.h"
#include "util/params.h"
#include "util/uint_set.h"
#include "math/grobner/pdd_solver.h"
@ -73,6 +74,7 @@ namespace nla {
public:
grobner(core *core);
void operator()();
void updt_params(params_ref const& p);
dd::solver::equation_vector const& core_equations(bool all_eqs);
};
}

6
src/math/lp/nla_solver.cpp
View file

@ -35,6 +35,10 @@ namespace nla {
void solver::set_relevant(std::function<bool(lpvar)>& is_relevant) {
m_core->set_relevant(is_relevant);
}
void solver::updt_params(params_ref const& p) {
m_core->updt_params(p);
}
bool solver::is_monic_var(lpvar v) const {
return m_core->is_monic_var(v);
@ -71,7 +75,7 @@ namespace nla {
}
std::ostream& solver::display(std::ostream& out) const {
m_core->print_monics(out);
m_core->display(out);
if (use_nra_model())
m_core->m_nra.display(out);
return out;

1
src/math/lp/nla_solver.h
View file

@ -33,6 +33,7 @@ namespace nla {
void add_bounded_division(lpvar q, lpvar x, lpvar y);
void check_bounded_divisions();
void set_relevant(std::function<bool(lpvar)>& is_relevant);
void updt_params(params_ref const& p);
void push();
void pop(unsigned scopes);
bool need_check();

554
src/math/lp/nra_solver.cpp
View file

@ -9,6 +9,7 @@
#include <fstream>
#include "math/lp/lar_solver.h"
#include "math/lp/nra_solver.h"
#include "math/lp/nla_coi.h"
#include "nlsat/nlsat_solver.h"
#include "nlsat/nlsat_assignment.h"
#include "math/polynomial/polynomial.h"
@ -16,7 +17,6 @@
#include "util/map.h"
#include "util/uint_set.h"
#include "math/lp/nla_core.h"
#include "math/lp/monic.h"
#include "params/smt_params_helper.hpp"
@ -27,174 +27,82 @@ typedef nla::mon_eq mon_eq;
typedef nla::variable_map_type variable_map_type;
struct solver::imp {
lp::lar_solver& lra;
reslimit& m_limit;
params_ref m_params;
u_map<polynomial::var> m_lp2nl; // map from lar_solver variables to nlsat::solver variables
indexed_uint_set m_term_set;
scoped_ptr<nlsat::solver> m_nlsat;
scoped_ptr<scoped_anum_vector> m_values; // values provided by LRA solver
scoped_ptr<scoped_anum> m_tmp1, m_tmp2;
nla::coi m_coi;
svector<lp::constraint_index> m_literal2constraint;
struct eq {
bool operator()(unsigned_vector const &a, unsigned_vector const &b) const {
return a == b;
}
};
map<unsigned_vector, unsigned, svector_hash<unsigned_hash>, eq> m_vars2mon;
nla::core& m_nla_core;
imp(lp::lar_solver& s, reslimit& lim, params_ref const& p, nla::core& nla_core):
lra(s),
m_limit(lim),
m_params(p),
m_coi(nla_core),
m_nla_core(nla_core) {}
bool need_check() {
return m_nla_core.m_to_refine.size() != 0;
}
indexed_uint_set m_mon_set, m_constraint_set;
struct occurs {
unsigned_vector constraints;
unsigned_vector monics;
unsigned_vector terms;
};
void init_cone_of_influence() {
indexed_uint_set visited;
unsigned_vector todo;
vector<occurs> var2occurs;
m_term_set.reset();
m_mon_set.reset();
m_constraint_set.reset();
for (auto ci : lra.constraints().indices()) {
auto const& c = lra.constraints()[ci];
if (c.is_auxiliary())
continue;
for (auto const& [coeff, v] : c.coeffs()) {
var2occurs.reserve(v + 1);
var2occurs[v].constraints.push_back(ci);
}
}
for (auto const& m : m_nla_core.emons()) {
for (auto v : m.vars()) {
var2occurs.reserve(v + 1);
var2occurs[v].monics.push_back(m.var());
}
}
for (const auto *t : lra.terms() ) {
for (auto const iv : *t) {
auto v = iv.j();
var2occurs.reserve(v + 1);
var2occurs[v].terms.push_back(t->j());
}
}
for (auto const& m : m_nla_core.m_to_refine)
todo.push_back(m);
for (unsigned i = 0; i < todo.size(); ++i) {
auto v = todo[i];
if (visited.contains(v))
continue;
visited.insert(v);
var2occurs.reserve(v + 1);
for (auto ci : var2occurs[v].constraints) {
m_constraint_set.insert(ci);
auto const& c = lra.constraints()[ci];
for (auto const& [coeff, w] : c.coeffs())
todo.push_back(w);
}
for (auto w : var2occurs[v].monics)
todo.push_back(w);
for (auto ti : var2occurs[v].terms) {
for (auto iv : lra.get_term(ti))
todo.push_back(iv.j());
todo.push_back(ti);
}
if (lra.column_has_term(v)) {
m_term_set.insert(v);
for (auto kv : lra.get_term(v))
todo.push_back(kv.j());
}
if (m_nla_core.is_monic_var(v)) {
m_mon_set.insert(v);
for (auto w : m_nla_core.emons()[v])
todo.push_back(w);
}
}
}
void reset() {
m_values = nullptr;
m_tmp1 = nullptr; m_tmp2 = nullptr;
m_nlsat = alloc(nlsat::solver, m_limit, m_params, false);
m_values = alloc(scoped_anum_vector, am());
m_term_set.reset();
m_lp2nl.reset();
}
void setup_solver() {
SASSERT(need_check());
reset();
init_cone_of_influence();
// add linear inequalities from lra_solver
for (auto ci : m_constraint_set)
add_constraint(ci);
// add polynomial definitions.
for (auto const& m : m_mon_set)
add_monic_eq(m_nla_core.emons()[m]);
// add term definitions.
for (unsigned i : m_term_set)
add_term(i);
TRACE(nra, m_nlsat->display(tout));
log_nl();
}
void log_nl() {
smt_params_helper p(m_params);
if (p.arith_nl_log()) {
static unsigned id = 0;
std::stringstream strm;
#ifndef SINGLE_THREAD
std::thread::id this_id = std::this_thread::get_id();
strm << "nla_" << this_id << "." << (++id) << ".smt2";
#else
strm << "nla_" << (++id) << ".smt2";
#endif
std::ofstream out(strm.str());
m_nlsat->display_smt2(out);
out << "(check-sat)\n";
out.close();
}
}
//
// This setup is for check_assignment which is better suitated for working with input polynomials diretly.
// First slice the set of constraints to remove clusters that are satisfied by the current assignment.
// Then initialize each variable as either a polynomial variable or as a definition for a term or monomial.
// Finally process all constraints and use the definitions to represent these into the nlsat solver.
//
svector<lp::constraint_index> m_literal2constraint;
struct eq {
bool operator()(unsigned_vector const &a, unsigned_vector const &b) const {
return a == b;
}
};
map<unsigned_vector, unsigned, svector_hash<unsigned_hash>, eq> m_vars2mon;
// Create polynomial definition for variable v used in setup_assignment_solver.
// Side-effects: updates m_vars2mon when v is a monic variable.
void mk_definition(unsigned v, polynomial_ref_vector & definitions) {
void mk_definition(unsigned v, polynomial_ref_vector &definitions, vector<rational>& denominators) {
auto &pm = m_nlsat->pm();
polynomial::polynomial_ref p(pm);
rational den(1);
if (m_nla_core.emons().is_monic_var(v)) {
auto const &m = m_nla_core.emons()[v];
for (auto v2 : m.vars()) {
polynomial_ref pw(definitions.get(v2), m_nlsat->pm());
if (!p)
p = pw;
else
p = p * pw;
}
}
else if (lra.column_has_term(v)) {
for (auto const &[w, coeff] : lra.get_term(v)) {
den = lcm(denominator(coeff), den);
}
for (auto const &[w, coeff] : lra.get_term(v)) {
auto coeff1 = den * coeff;
polynomial_ref pw(definitions.get(w), m_nlsat->pm());
if (!p)
p = constant(coeff1) * pw;
else
p = p + (constant(coeff1) * pw);
}
}
else {
p = pm.mk_polynomial(lp2nl(v)); // nlsat var index equals v (verified above when created)
}
definitions.push_back(p);
denominators.push_back(den);
}
// Create polynomial definition for variable v used in setup_assignment_solver.
// Side-effects: updates m_vars2mon when v is a monic variable.
void mk_definition_assignment(unsigned v, polynomial_ref_vector &definitions) {
auto &pm = m_nlsat->pm();
polynomial::polynomial_ref p(pm);
if (m_nla_core.emons().is_monic_var(v)) {
@ -209,95 +117,94 @@ struct solver::imp {
else
p = pm.mul(p, pv);
}
}
else if (lra.column_has_term(v)) {
// Scale coefficients by a common denominator so that they become integers.
}
else if (lra.column_has_term(v)) {
rational den(1);
for (auto const& [w, coeff] : lra.get_term(v))
den = lcm(den, denominator(coeff));
for (auto const& [w, coeff] : lra.get_term(v)) {
auto pw = definitions.get(w);
if (!p)
p = pm.mul(den*coeff, pw);
p = pm.mul(den * coeff, pw);
else
p = pm.add(p, pm.mul(den*coeff, pw));
p = pm.add(p, pm.mul(den * coeff, pw));
}
}
else {
p = pm.mk_polynomial(v); // nlsat var index equals v (verified above when created)
}
else {
p = pm.mk_polynomial(lp2nl(v));
}
definitions.push_back(p);
}
void setup_assignment_solver() {
SASSERT(need_check());
reset();
m_literal2constraint.reset();
m_vars2mon.reset();
init_cone_of_influence();
void setup_solver_poly() {
m_coi.init();
auto &pm = m_nlsat->pm();
polynomial_ref_vector definitions(pm);
vector<rational> denominators;
for (unsigned v = 0; v < lra.number_of_vars(); ++v) {
auto j = m_nlsat->mk_var(lra.var_is_int(v));
VERIFY(j == v);
m_lp2nl.insert(v, j); // we don't really need this. It is going to be the identify map.
scoped_anum a(am());
am().set(a, m_nla_core.val(v).to_mpq());
m_values->push_back(a);
mk_definition(v, definitions);
if (m_coi.vars().contains(v)) {
auto j = m_nlsat->mk_var(lra.var_is_int(v));
m_lp2nl.insert(v, j); // we don't really need this. It is going to be the identify map.
mk_definition(v, definitions, denominators);
}
else {
definitions.push_back(nullptr);
denominators.push_back(rational(0));
}
}
// we rely on that all information encoded into the tableau is present as a constraint.
for (auto ci : m_constraint_set) {
for (auto ci : m_coi.constraints()) {
auto &c = lra.constraints()[ci];
auto &pm = m_nlsat->pm();
auto k = c.kind();
auto rhs = c.rhs();
auto lhs = c.coeffs();
rational den = denominator(rhs);
for (auto [coeff, v] : lhs)
den = lcm(den, denominator(coeff));
for (auto [coeff, v] : lhs)
den = lcm(lcm(den, denominator(coeff)), denominators[v]);
polynomial::polynomial_ref p(pm);
p = pm.mk_const(-den * rhs);
for (auto [coeff, v] : lhs) {
polynomial_ref poly(pm);
poly = pm.mul(den * coeff, definitions.get(v));
poly = definitions.get(v);
poly = poly * constant(den * coeff / denominators[v]);
p = p + poly;
}
auto lit = add_constraint(p, ci, k);
m_literal2constraint.setx(lit.index(), ci, lp::null_ci);
}
log_nl();
definitions.reset();
}
void validate_constraints() {
for (lp::constraint_index ci : lra.constraints().indices())
if (!check_constraint(ci)) {
IF_VERBOSE(0, verbose_stream() << "constraint " << ci << " violated\n";
lra.constraints().display(verbose_stream()));
UNREACHABLE();
return;
}
for (auto const& m : m_nla_core.emons()) {
if (!check_monic(m)) {
IF_VERBOSE(0, verbose_stream() << "monic " << m << " violated\n";
lra.constraints().display(verbose_stream()));
UNREACHABLE();
return;
}
}
void setup_solver_terms() {
m_coi.init();
// add linear inequalities from lra_solver
for (auto ci : m_coi.constraints())
add_constraint(ci);
// add polynomial definitions.
for (auto const &m : m_coi.mons())
add_monic_eq(m_nla_core.emons()[m]);
// add term definitions.
for (unsigned i : m_coi.terms())
add_term(i);
}
bool check_constraints() {
for (lp::constraint_index ci : lra.constraints().indices())
if (!check_constraint(ci))
return false;
for (auto const& m : m_nla_core.emons())
if (!check_monic(m))
return false;
return true;
polynomial::polynomial_ref sub(polynomial::polynomial *a, polynomial::polynomial *b) {
return polynomial_ref(m_nlsat->pm().sub(a, b), m_nlsat->pm());
}
polynomial::polynomial_ref mul(polynomial::polynomial *a, polynomial::polynomial *b) {
return polynomial_ref(m_nlsat->pm().mul(a, b), m_nlsat->pm());
}
polynomial::polynomial_ref var(lp::lpvar v) {
return polynomial_ref(m_nlsat->pm().mk_polynomial(lp2nl(v)), m_nlsat->pm());
}
polynomial::polynomial_ref constant(rational const& r) {
return polynomial_ref(m_nlsat->pm().mk_const(r), m_nlsat->pm());
}
/**
@ -312,7 +219,32 @@ struct solver::imp {
TBD: explore more incremental ways of applying nlsat (using assumptions)
*/
lbool check() {
setup_solver();
SASSERT(need_check());
reset();
vector<nlsat::assumption, false> core;
smt_params_helper p(m_params);
setup_solver_poly();
TRACE(nra, m_nlsat->display(tout));
if (p.arith_nl_log()) {
static unsigned id = 0;
std::stringstream strm;
#ifndef SINGLE_THREAD
std::thread::id this_id = std::this_thread::get_id();
strm << "nla_" << this_id << "." << (++id) << ".smt2";
#else
strm << "nla_" << (++id) << ".smt2";
#endif
std::ofstream out(strm.str());
m_nlsat->display_smt2(out);
out << "(check-sat)\n";
out.close();
}
lbool r = l_undef;
statistics& st = m_nla_core.lp_settings().stats().m_st;
try {
@ -328,19 +260,43 @@ struct solver::imp {
}
}
m_nlsat->collect_statistics(st);
TRACE(nra, m_nlsat->display(tout << r << "\n"););
TRACE(nra, tout << "nra result " << r << "\n");
CTRACE(nra, false,
m_nlsat->display(tout << r << "\n");
display(tout);
for (auto [j, x] : m_lp2nl) tout << "j" << j << " := x" << x << "\n";);
switch (r) {
case l_true:
m_nla_core.set_use_nra_model(true);
lra.init_model();
validate_constraints();
for (lp::constraint_index ci : lra.constraints().indices())
if (!check_constraint(ci)) {
IF_VERBOSE(0, verbose_stream() << "constraint " << ci << " violated\n";
lra.constraints().display(verbose_stream()));
UNREACHABLE();
return l_undef;
}
for (auto const &m : m_nla_core.emons()) {
if (!check_monic(m)) {
IF_VERBOSE(0, verbose_stream() << "monic " << m << " violated\n";
lra.constraints().display(verbose_stream()));
UNREACHABLE();
return l_undef;
}
}
break;
case l_false: {
lp::explanation ex;
constraint_core2ex(ex);
m_nlsat->get_core(core);
nla::lemma_builder lemma(m_nla_core, __FUNCTION__);
for (auto c : core) {
unsigned idx = static_cast<unsigned>(static_cast<imp *>(c) - this);
ex.push_back(idx);
}
lemma &= ex;
m_nla_core.set_use_nra_model(true);
TRACE(nra, tout << lemma << "\n");
break;
}
case l_undef:
@ -349,13 +305,51 @@ struct solver::imp {
return r;
}
void setup_assignment_solver() {
SASSERT(need_check());
reset();
m_literal2constraint.reset();
m_vars2mon.reset();
m_coi.init();
auto &pm = m_nlsat->pm();
polynomial_ref_vector definitions(pm);
for (unsigned v = 0; v < lra.number_of_vars(); ++v) {
auto j = m_nlsat->mk_var(lra.var_is_int(v));
VERIFY(j == v);
m_lp2nl.insert(v, j);
scoped_anum a(am());
am().set(a, m_nla_core.val(v).to_mpq());
m_values->push_back(a);
mk_definition_assignment(v, definitions);
}
for (auto ci : m_coi.constraints()) {
auto &c = lra.constraints()[ci];
auto &pm = m_nlsat->pm();
auto k = c.kind();
auto rhs = c.rhs();
auto lhs = c.coeffs();
rational den = denominator(rhs);
for (auto [coeff, v] : lhs)
den = lcm(den, denominator(coeff));
polynomial::polynomial_ref p(pm);
p = pm.mk_const(-den * rhs);
for (auto [coeff, v] : lhs) {
polynomial_ref poly(pm);
poly = pm.mul(den * coeff, definitions.get(v));
p = p + poly;
}
auto lit = add_constraint(p, ci, k);
m_literal2constraint.setx(lit.index(), ci, lp::null_ci);
}
}
void process_polynomial_check_assignment(polynomial::polynomial const* p, rational& bound, const u_map<lp::lpvar>& nl2lp, lp::lar_term& t) {
polynomial::manager& pm = m_nlsat->pm();
for (unsigned i = 0; i < pm.size(p); ++i) {
polynomial::monomial* m = pm.get_monomial(p, i);
TRACE(nra, tout << "monomial: "; pm.display(tout, m); tout << "\n";);
auto& coeff = pm.coeff(p, i);
TRACE(nra, tout << "coeff:"; pm.m().display(tout, coeff););
unsigned num_vars = pm.size(m);
// add mon * coeff to t;
@ -378,7 +372,6 @@ struct solver::imp {
v = m_vars2mon[vars];
else
v = m_nla_core.add_mul_def(vars.size(), vars.data());
TRACE(nra, tout << " vars=" << vars << "\n");
t.add_monomial(coeff, v);
break;
}
@ -394,7 +387,6 @@ struct solver::imp {
}
lbool check_assignment() {
IF_VERBOSE(1, verbose_stream() << "nra::solver::check_assignment\n";);
setup_assignment_solver();
lbool r = l_undef;
statistics &st = m_nla_core.lp_settings().stats().m_st;
@ -418,13 +410,16 @@ struct solver::imp {
}
}
m_nlsat->collect_statistics(st);
TRACE(nra, m_nlsat->display(tout << r << "\n"); display(tout); tout << "m_lp2nl:\n";
for (auto [j, x] : m_lp2nl) tout << "j" << j << " := x" << x << "\n";);
switch (r) {
case l_true:
m_nla_core.set_use_nra_model(true);
lra.init_model();
validate_constraints();
for (lp::constraint_index ci : lra.constraints().indices())
if (!check_constraint(ci))
return l_undef;
for (auto const& m : m_nla_core.emons())
if (!check_monic(m))
return l_undef;
m_nla_core.set_use_nra_model(true);
break;
case l_false:
@ -449,22 +444,17 @@ struct solver::imp {
continue;
}
nlsat::atom *a = m_nlsat->bool_var2atom(l.var());
TRACE(nra, tout << "atom: "; m_nlsat->display(tout, *a); tout << "\n";);
SASSERT(!a->is_root_atom());
SASSERT(a->is_ineq_atom());
auto &ia = *to_ineq_atom(a);
if (ia.size() != 1) {
return l_undef; // levnach: not sure what to do here
return l_undef; // factored polynomials not handled here
}
// VERIFY(ia.size() == 1); // deal with factored polynomials later
// a is an inequality atom, i.e., p > 0, p < 0, or p = 0.
polynomial::polynomial const *p = ia.p(0);
TRACE(nra, tout << "polynomial: "; pm.display(tout, p); tout << "\n";);
rational bound(0);
lp::lar_term t;
process_polynomial_check_assignment(p, bound, nl2lp, t);
// Introduce a single ineq variable and assign it per case; common handling after switch.
nla::ineq inq(lp::lconstraint_kind::EQ, t, bound); // initial value overwritten in cases below
switch (a->get_kind()) {
case nlsat::atom::EQ:
@ -480,26 +470,14 @@ struct solver::imp {
UNREACHABLE();
return l_undef;
}
// Ignore a lemma which is satisfied
if (m_nla_core.ineq_holds(inq))
return l_undef;
lemma |= inq;
}
IF_VERBOSE(1, verbose_stream() << "linear lemma: " << lemma << "\n");
this->m_nla_core.m_check_feasible = true;
return l_false;
}
void constraint_core2ex(lp::explanation& ex) {
vector<nlsat::assumption, false> core;
m_nlsat->get_core(core);
for (auto c : core) {
unsigned idx = static_cast<unsigned>(static_cast<imp*>(c) - this);
ex.push_back(idx);
TRACE(nra, lra.display_constraint(tout << "ex: " << idx << ": ", idx) << "\n";);
}
}
void add_monic_eq_bound(mon_eq const& m) {
if (!lra.column_has_lower_bound(m.var()) &&
@ -533,15 +511,28 @@ struct solver::imp {
coeffs.push_back(mpz(1));
coeffs.push_back(mpz(-1));
polynomial::polynomial_ref p(pm.mk_polynomial(2, coeffs.data(), mls), pm);
polynomial::polynomial* ps[1] = { p };
bool even[1] = { false };
nlsat::literal lit = m_nlsat->mk_ineq_literal(nlsat::atom::kind::EQ, 1, ps, even);
auto lit = mk_literal(p.get(), lp::lconstraint_kind::EQ);
nlsat::assumption a = nullptr;
m_nlsat->mk_clause(1, &lit, nullptr);
}
nlsat::literal mk_literal(polynomial::polynomial *p, lp::lconstraint_kind k) {
polynomial::polynomial *ps[1] = { p };
bool is_even[1] = { false };
switch (k) {
case lp::lconstraint_kind::LE: return ~m_nlsat->mk_ineq_literal(nlsat::atom::kind::GT, 1, ps, is_even);
case lp::lconstraint_kind::GE: return ~m_nlsat->mk_ineq_literal(nlsat::atom::kind::LT, 1, ps, is_even);
case lp::lconstraint_kind::LT: return m_nlsat->mk_ineq_literal(nlsat::atom::kind::LT, 1, ps, is_even);
case lp::lconstraint_kind::GT: return m_nlsat->mk_ineq_literal(nlsat::atom::kind::GT, 1, ps, is_even);
case lp::lconstraint_kind::EQ: return m_nlsat->mk_ineq_literal(nlsat::atom::kind::EQ, 1, ps, is_even);
default: UNREACHABLE(); // unreachable
}
throw default_exception("uexpected operator");
}
void add_constraint(unsigned idx) {
auto &c = lra.constraints()[idx];
auto &pm = m_nlsat->pm();
auto& c = lra.constraints()[idx];
auto& pm = m_nlsat->pm();
auto k = c.kind();
auto rhs = c.rhs();
auto lhs = c.coeffs();
@ -558,32 +549,23 @@ struct solver::imp {
}
rhs *= den;
polynomial::polynomial_ref p(pm.mk_linear(sz, coeffs.data(), vars.data(), -rhs), pm);
add_constraint(p, idx, k);
nlsat::literal lit = mk_literal(p.get(), k);
nlsat::assumption a = this + idx;
m_nlsat->mk_clause(1, &lit, a);
}
nlsat::literal add_constraint(polynomial::polynomial* p, unsigned idx, lp::lconstraint_kind k) {
polynomial::polynomial* ps[1] = { p };
bool is_even[1] = { false };
nlsat::literal add_constraint(polynomial::polynomial *p, unsigned idx, lp::lconstraint_kind k) {
polynomial::polynomial *ps[1] = {p};
bool is_even[1] = {false};
nlsat::literal lit;
nlsat::assumption a = this + idx;
switch (k) {
case lp::lconstraint_kind::LE:
lit = ~m_nlsat->mk_ineq_literal(nlsat::atom::kind::GT, 1, ps, is_even);
break;
case lp::lconstraint_kind::GE:
lit = ~m_nlsat->mk_ineq_literal(nlsat::atom::kind::LT, 1, ps, is_even);
break;
case lp::lconstraint_kind::LT:
lit = m_nlsat->mk_ineq_literal(nlsat::atom::kind::LT, 1, ps, is_even);
break;
case lp::lconstraint_kind::GT:
lit = m_nlsat->mk_ineq_literal(nlsat::atom::kind::GT, 1, ps, is_even);
break;
case lp::lconstraint_kind::EQ:
lit = m_nlsat->mk_ineq_literal(nlsat::atom::kind::EQ, 1, ps, is_even);
break;
default:
UNREACHABLE(); // unreachable
case lp::lconstraint_kind::LE: lit = ~m_nlsat->mk_ineq_literal(nlsat::atom::kind::GT, 1, ps, is_even); break;
case lp::lconstraint_kind::GE: lit = ~m_nlsat->mk_ineq_literal(nlsat::atom::kind::LT, 1, ps, is_even); break;
case lp::lconstraint_kind::LT: lit = m_nlsat->mk_ineq_literal(nlsat::atom::kind::LT, 1, ps, is_even); break;
case lp::lconstraint_kind::GT: lit = m_nlsat->mk_ineq_literal(nlsat::atom::kind::GT, 1, ps, is_even); break;
case lp::lconstraint_kind::EQ: lit = m_nlsat->mk_ineq_literal(nlsat::atom::kind::EQ, 1, ps, is_even); break;
default: UNREACHABLE(); // unreachable
}
m_nlsat->mk_clause(1, &lit, a);
return lit;
@ -636,7 +618,7 @@ struct solver::imp {
for (auto const& m : m_nla_core.emons())
if (any_of(m.vars(), [&](lp::lpvar v) { return m_lp2nl.contains(v); }))
add_monic_eq_bound(m);
for (unsigned i : m_term_set)
for (unsigned i : m_coi.terms())
add_term(i);
for (auto const& [v, w] : m_lp2nl) {
if (lra.column_has_lower_bound(v))
@ -665,8 +647,12 @@ struct solver::imp {
case l_true:
m_nla_core.set_use_nra_model(true);
lra.init_model();
if (!check_constraints())
return l_undef;
for (lp::constraint_index ci : lra.constraints().indices())
if (!check_constraint(ci))
return l_undef;
for (auto const& m : m_nla_core.emons())
if (!check_monic(m))
return l_undef;
break;
case l_false: {
lp::explanation ex;
@ -680,6 +666,7 @@ struct solver::imp {
ex.push_back(ci);
nla::lemma_builder lemma(m_nla_core, __FUNCTION__);
lemma &= ex;
TRACE(nra, tout << lemma << "\n");
break;
}
case l_undef:
@ -816,8 +803,8 @@ struct solver::imp {
if (!m_lp2nl.find(v, r)) {
r = m_nlsat->mk_var(is_int(v));
m_lp2nl.insert(v, r);
if (!m_term_set.contains(v) && lra.column_has_term(v)) {
m_term_set.insert(v);
if (!m_coi.terms().contains(v) && lra.column_has_term(v)) {
m_coi.terms().insert(v);
}
}
return r;
@ -848,20 +835,55 @@ struct solver::imp {
m_nlsat->mk_clause(1, &lit, nullptr);
}
nlsat::anum const& value(lp::lpvar v) {
polynomial::var pv;
if (m_lp2nl.find(v, pv))
return m_nlsat->value(pv);
else {
for (unsigned w = m_values->size(); w <= v; ++w) {
scoped_anum a(am());
am().set(a, m_nla_core.val(w).to_mpq());
nlsat::anum const &value(lp::lpvar v) {
init_values(v + 1);
return (*m_values)[v];
}
void init_values(unsigned sz) {
if (m_values->size() >= sz)
return;
unsigned w;
scoped_anum a(am());
for (unsigned v = m_values->size(); v < sz; ++v) {
if (m_nla_core.emons().is_monic_var(v)) {
am().set(a, 1);
auto &m = m_nla_core.emon(v);
for (auto x : m.vars())
am().mul(a, (*m_values)[x], a);
m_values->push_back(a);
}
return (*m_values)[v];
}
else if (lra.column_has_term(v)) {
scoped_anum b(am());
am().set(a, 0);
for (auto const &[w, coeff] : lra.get_term(v)) {
am().set(b, coeff.to_mpq());
am().mul(b, (*m_values)[w], b);
am().add(a, b, a);
}
m_values->push_back(a);
}
else if (m_lp2nl.find(v, w)) {
m_values->push_back(m_nlsat->value(w));
}
else {
am().set(a, m_nla_core.val(v).to_mpq());
m_values->push_back(a);
}
}
}
void set_value(lp::lpvar v, rational const& value) {
if (!m_values)
m_values = alloc(scoped_anum_vector, am());
scoped_anum a(am());
am().set(a, value.to_mpq());
while (m_values->size() <= v)
m_values->push_back(a);
am().set((*m_values)[v], a);
}
nlsat::anum_manager& am() {
return m_nlsat->am();
}
@ -919,7 +941,7 @@ lbool solver::check(dd::solver::equation_vector const& eqs) {
lbool solver::check_assignment() {
return m_imp->check_assignment();
}
}
bool solver::need_check() {
return m_imp->need_check();
@ -946,4 +968,8 @@ void solver::updt_params(params_ref& p) {
m_imp->updt_params(p);
}
void solver::set_value(lp::lpvar v, rational const& value) {
m_imp->set_value(v, value);
}
}

4
src/math/lp/nra_solver.h
View file

@ -48,7 +48,7 @@ namespace nra {
lbool check(dd::solver::equation_vector const& eqs);
/**
\brief Check feasibility moduo current value assignment.
\brief Check feasibility modulo current value assignment.
*/
lbool check_assignment();
@ -64,6 +64,8 @@ namespace nra {
nlsat::anum_manager& am();
void set_value(lp::lpvar v, rational const &value);
scoped_anum& tmp1();
scoped_anum& tmp2();