mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-22 05:43:39 +00:00
Code Activity

start porting grobner basis functionality

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-09-05 14:14:37 -07:00
parent 06dbc623c7
commit 26b4294bce
3 changed files with 2244 additions and 2213 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -80,9 +80,6 @@ void nla_grobner::prepare_rows_and_active_vars() {
void nla_grobner::grobner_lemmas() {
c().lp_settings().st().m_grobner_calls++;
if (c().lp_settings().st().m_grobner_calls == 2)
SASSERT(false);
find_rows();
@ -96,9 +93,10 @@ void nla_grobner::grobner_lemmas() {
tout << "the matrix =\n";
for (const auto & r : matrix.m_rows) {
c().print_term(r, tout) << "\n";
c().print_term(r, tout) << std::endl;
}
}
);
SASSERT(false);
}
} // end of nla namespace

5
src/smt/theory_arith.h
View file

@ -1039,6 +1039,11 @@ namespace smt {
bool internalize_gb_eq(grobner::equation const * eq);
enum gb_result { GB_PROGRESS, GB_NEW_EQ, GB_FAIL };
gb_result compute_grobner(svector<theory_var> const & nl_cluster);
void update_statistics(grobner&);
void set_gb_exhausted(bool r);
bool pass_over_gb_eqs_for_conflict(ptr_vector<grobner::equation>& eqs, grobner&);
gb_result scan_for_linear(ptr_vector<grobner::equation>& eqs, grobner&);
bool try_to_modify_eqs(ptr_vector<grobner::equation>& eqs, grobner&, unsigned &);
bool max_min_nl_vars();
final_check_status process_non_linear();

156
src/smt/theory_arith_nl.h
View file

@ -811,12 +811,14 @@ namespace smt {
bool theory_arith<Ext>::is_monomial_linear(expr * m) const {
SASSERT(is_pure_monomial(m));
unsigned num_nl_vars = 0;
for (expr* arg : *to_app(m)) {
for (unsigned i = 0; i < to_app(m)->get_num_args(); i++) {
expr * arg = to_app(m)->get_arg(i);
theory_var _var = expr2var(arg);
if (!is_fixed(_var)) {
num_nl_vars++;
}
else if (lower_bound(_var).is_zero()) {
else {
if (lower_bound(_var).is_zero())
return true;
}
}
@ -1217,8 +1219,10 @@ namespace smt {
m_var2num_occs.insert(VAR, occs); \
}
for (coeff_expr const& kv : p) {
expr * m = kv.second;
typename sbuffer<coeff_expr>::const_iterator it = p.begin();
typename sbuffer<coeff_expr>::const_iterator end = p.end();
for (; it != end; ++it) {
expr * m = it->second;
if (is_pure_monomial(m)) {
unsigned num_vars = get_num_vars_in_monomial(m);
for (unsigned i = 0; i < num_vars; i++) {
@ -1233,8 +1237,8 @@ namespace smt {
ADD_OCC(m);
}
else {
ctx.internalize(m, false);
ADD_OCC(m);
TRACE("non_linear", tout << mk_pp(m, get_manager()) << "\n";);
UNREACHABLE();
}
}
@ -1251,6 +1255,7 @@ namespace smt {
template<typename Ext>
expr * theory_arith<Ext>::p2expr(sbuffer<coeff_expr> & p) {
SASSERT(!p.empty());
TRACE("p2expr_bug", display_coeff_exprs(tout, p););
ptr_buffer<expr> args;
for (coeff_expr const& ce : p) {
rational const & c = ce.first;
@ -1272,7 +1277,6 @@ namespace smt {
SASSERT(!args.empty());
expr * r = mk_nary_add(args.size(), args.c_ptr());
m_nl_new_exprs.push_back(r);
TRACE("p2expr_bug", display_coeff_exprs(tout, p); tout << mk_pp(r, get_manager()) << "\n";);
return r;
}
@ -1483,7 +1487,6 @@ namespace smt {
r.push_back(coeff_expr(kv.first, f));
}
}
expr * s = cross_nested(e, nullptr);
if (!r.empty()) {
expr * q = horner(r, var);
@ -1534,7 +1537,7 @@ namespace smt {
rational a, b;
unsigned n = UINT_MAX;
unsigned nm = UINT_MAX;
if (in_monovariate_monomials(p, var, i1, a, n, i2, b, nm) && n != nm) {
if (in_monovariate_monomials(p, var, i1, a, n, i2, b, nm)) {
CTRACE("in_monovariate_monomials", n == nm,
for (unsigned i = 0; i < p.size(); i++) {
if (i > 0) tout << " + "; tout << p[i].first << "*" << mk_pp(p[i].second, get_manager());
@ -1694,9 +1697,11 @@ namespace smt {
TRACE("non_linear", tout << "check problematic row:\n"; display_row(tout, r); display_row(tout, r, false););
sbuffer<coeff_expr> p;
for (row_entry const& re : r) {
if (!re.is_dead())
p.push_back(coeff_expr(re.m_coeff.to_rational() * c, var2expr(re.m_var)));
typename vector<row_entry>::const_iterator it = r.begin_entries();
typename vector<row_entry>::const_iterator end = r.end_entries();
for (; it != end; ++it) {
if (!it->is_dead())
p.push_back(coeff_expr(it->m_coeff.to_rational() * c, var2expr(it->m_var)));
}
SASSERT(!p.empty());
CTRACE("cross_nested_bug", !c.is_one(), tout << "c: " << c << "\n"; display_row(tout, r); tout << "---> p (coeffs, exprs):\n"; display_coeff_exprs(tout, p););
@ -2219,78 +2224,42 @@ namespace smt {
return true;
}
/**
\brief Compute Grobner basis, return true if a conflict or new fixed variables were detected.
*/
template<typename Ext>
typename theory_arith<Ext>::gb_result theory_arith<Ext>::compute_grobner(svector<theory_var> const & nl_cluster) {
if (m_nl_gb_exhausted)
return GB_FAIL;
grobner gb(get_manager(), m_dep_manager);
init_grobner(nl_cluster, gb);
TRACE("non_linear", display(tout););
bool warn = false;
unsigned next_weight = MAX_DEFAULT_WEIGHT + 1; // next weight using during perturbation phase.
ptr_vector<grobner::equation> eqs;
while (true) {
TRACE("non_linear_gb", tout << "before:\n"; gb.display(tout););
bool r = false;
gb.compute_basis_init();
while (!r && gb.get_num_new_equations() < m_params.m_nl_arith_gb_threshold) {
if (get_context().get_cancel_flag()) {
warn = true;
break;
}
r = gb.compute_basis_step();
}
void theory_arith<Ext>::update_statistics(grobner & gb) {
m_stats.m_gb_simplify += gb.m_stats.m_simplify;
m_stats.m_gb_superpose += gb.m_stats.m_superpose;
m_stats.m_gb_num_processed += gb.m_stats.m_num_processed;
m_stats.m_gb_compute_basis++;
if (!r && !warn) {
}
template<typename Ext>
void theory_arith<Ext>::set_gb_exhausted(bool r) {
if (!r) {
IF_VERBOSE(3, verbose_stream() << "Grobner basis computation interrupted. Increase threshold using NL_ARITH_GB_THRESHOLD=<limit>\n";);
get_context().push_trail(value_trail<context, bool>(m_nl_gb_exhausted));
m_nl_gb_exhausted = true;
warn = true;
}
if (get_context().get_cancel_flag()) {
return GB_FAIL;
}
TRACE("non_linear_gb", tout << "after:\n"; gb.display(tout););
// Scan the grobner basis eqs, and look for inconsistencies.
template<typename Ext>
bool theory_arith<Ext>::pass_over_gb_eqs_for_conflict(ptr_vector<grobner::equation>& eqs, grobner& gb) {
eqs.reset();
gb.get_equations(eqs);
TRACE("grobner_bug", tout << "after gb\n";);
for (grobner::equation* eq : eqs) {
TRACE("grobner_bug", gb.display_equation(tout, *eq););
if (is_inconsistent(eq, gb))
return GB_PROGRESS;
if (is_inconsistent2(eq, gb))
return GB_PROGRESS;
if (is_inconsistent(eq, gb) || is_inconsistent2(eq, gb))
return true;
}
// Scan the grobner basis eqs for equations of the form x - k = 0 or x = 0 is found, and x is not fixed,
// then assert bounds for x, and continue
gb_result result = GB_FAIL;
if (m_params.m_nl_arith_gb_eqs) {
for (grobner::equation* eq : eqs) {
if (!eq->is_linear_combination()) {
TRACE("non_linear", tout << "processing new equality:\n"; gb.display_equation(tout, *eq););
TRACE("non_linear_bug", tout << "processing new equality:\n"; gb.display_equation(tout, *eq););
if (internalize_gb_eq(eq))
result = GB_NEW_EQ;
return false;
}
}
}
if (result != GB_FAIL)
return result;
if (!m_params.m_nl_arith_gb_perturbate)
return result;
if (m_nl_gb_exhausted)
return result;
// Try to change the variable order... in such a way the leading term is modified.
// I only consider linear equations... (HACK)
// Moreover, I do not change the weight of a variable more than once in this loop.
template<typename Ext>
bool theory_arith<Ext>::try_to_modify_eqs(ptr_vector<grobner::equation>& eqs, grobner& gb, unsigned & next_weight) {
bool modified = false;
for (grobner::equation const* eq : eqs) {
@ -2318,9 +2287,68 @@ namespace smt {
if (modified)
break;
}
if (!modified)
return modified;
}
// Scan the grobner basis eqs for equations of the form x - k = 0 or x = 0 is found, and x is not fixed,
// then assert bounds for x, and continue
template<typename Ext>
typename theory_arith<Ext>::gb_result theory_arith<Ext>::scan_for_linear(ptr_vector<grobner::equation>& eqs, grobner& gb) {
gb_result result = GB_FAIL;
if (m_params.m_nl_arith_gb_eqs) {
for (grobner::equation* eq : eqs) {
if (!eq->is_linear_combination()) {
TRACE("non_linear", tout << "processing new equality:\n"; gb.display_equation(tout, *eq););
TRACE("non_linear_bug", tout << "processing new equality:\n"; gb.display_equation(tout, *eq););
if (internalize_gb_eq(eq))
result = GB_NEW_EQ;
}
}
}
return result;
}
/**
\brief Compute Grobner basis, return true if a conflict or new fixed variables were detected.
*/
template<typename Ext>
typename theory_arith<Ext>::gb_result theory_arith<Ext>::compute_grobner(svector<theory_var> const & nl_cluster) {
if (m_nl_gb_exhausted)
return GB_FAIL;
grobner gb(get_manager(), m_dep_manager);
init_grobner(nl_cluster, gb);
TRACE("non_linear", display(tout););
unsigned next_weight = MAX_DEFAULT_WEIGHT + 1; // next weight using during perturbation phase.
ptr_vector<grobner::equation> eqs;
while (true) {
TRACE("non_linear_gb", tout << "before:\n"; gb.display(tout););
bool r = false;
gb.compute_basis_init();
while (!r && gb.get_num_new_equations() < m_params.m_nl_arith_gb_threshold) {
if (get_context().get_cancel_flag()) {
return GB_FAIL;
}
r = gb.compute_basis_step();
}
update_statistics(gb);
set_gb_exhausted(r);
if (get_context().get_cancel_flag()) {
return GB_FAIL;
}
TRACE("non_linear_gb", tout << "after:\n"; gb.display(tout););
if (pass_over_gb_eqs_for_conflict(eqs, gb))
return GB_PROGRESS;
gb_result result = scan_for_linear(eqs, gb);
if ( result != GB_FAIL ||
(!m_params.m_nl_arith_gb_perturbate) ||
m_nl_gb_exhausted ||
(!try_to_modify_eqs(eqs, gb, next_weight))
) {
return result;
}
}
}
/**