mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 04:48:45 +00:00
Code Activity

port grobner basis

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-09-17 13:54:18 -07:00
parent 490672a5ba
commit cc5a12c5c7
9 changed files with 125 additions and 19 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -40,7 +40,7 @@ bool horner::row_has_monomial_to_refine(const T& row) const {
template <typename T>
bool horner::row_is_interesting(const T& row) const {
TRACE("nla_solver_details", m_core->print_term(row, tout););
if (row.size() > m_core->m_settings.horner_row_length_limit()) {
if (row.size() > m_core->m_nla_settings.horner_row_length_limit()) {
TRACE("nla_solver_details", tout << "disregard\n";);
return false;
}
@ -101,7 +101,7 @@ bool horner::lemmas_on_row(const T& row) {
}
void horner::horner_lemmas() {
if (!c().m_settings.run_horner()) {
if (!c().m_nla_settings.run_horner()) {
TRACE("nla_solver", tout << "not generating horner lemmas\n";);
return;
}

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

@ -88,7 +88,7 @@ public:
order m_order;
monotone m_monotone;
horner m_horner;
nla_settings m_settings;
nla_settings m_nla_settings;
nla_grobner m_grobner;
private:
emonomials m_emons;
@ -142,9 +142,9 @@ public:
lpvar var(const factor& f) const { return f.var(); }
bool need_to_call_horner() const { return lp_settings().stats().m_nla_calls % m_settings.horner_frequency() == 0; }
bool need_to_call_horner() const { return lp_settings().stats().m_nla_calls % m_nla_settings.horner_frequency() == 0; }
bool need_to_call_grobner() const { return lp_settings().stats().m_nla_calls % m_settings.grobner_frequency() == 0; }
bool need_to_call_grobner() const { return lp_settings().stats().m_nla_calls % m_nla_settings.grobner_frequency() == 0; }
lbool incremental_linearization(bool);

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

@ -127,6 +127,56 @@ void nla_grobner::init() {
find_nl_cluster();
}
equation* nla_grobner::pick_next() {
SASSERT(false);
return nullptr;
}
equation* nla_grobner::simplify_using_processed(equation* eq) {
SASSERT(false);
return nullptr;
}
equation* nla_grobner::simplify_processed(equation* eq) {
SASSERT(false);
return nullptr;
}
equation* nla_grobner::simplify_to_process(equation*) {
SASSERT(false);
return nullptr;
}
void nla_grobner::superpose(equation * eq1, equation * eq2) {
SASSERT(false);
}
void nla_grobner::superpose(equation * eq){
SASSERT(false);
}
bool nla_grobner::compute_basis_step() {
equation * eq = pick_next();
if (!eq)
return true;
m_stats.m_num_processed++;
equation * new_eq = simplify_using_processed(eq);
if (new_eq != nullptr && eq != new_eq) {
// equation was updated using non destructive updates
m_equations_to_unfreeze.push_back(eq);
eq = new_eq;
}
if (canceled()) return false;
if (!simplify_processed(eq)) return false;
superpose(eq);
m_processed.insert(eq);
simplify_to_process(eq);
TRACE("grobner", tout << "end of iteration:\n"; display(tout););
return false;
}
void nla_grobner::compute_basis(){
compute_basis_init();
if (!compute_basis_loop()) {
@ -135,12 +185,15 @@ void nla_grobner::compute_basis(){
}
void nla_grobner::compute_basis_init(){
c().lp_settings().stats().m_grobner_basis_computatins++;
m_num_new_equations = 0;
m_num_of_equations = 0;
}
bool nla_grobner::compute_basis_loop(){
SASSERT(false);
while (m_num_of_equations < c().m_nla_settings.grobner_eqs_threshold()) {
if (compute_basis_step())
return true;
}
return false;
}

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

@ -21,9 +21,38 @@
#include "math/lp/nla_common.h"
#include "math/lp/nex.h"
#include "util/dependency.h"
namespace nla {
class core;
struct grobner_stats {
long m_simplify;
long m_superpose;
long m_compute_basis;
long m_num_processed;
void reset() { memset(this, 0, sizeof(grobner_stats)); }
grobner_stats() { reset(); }
};
class equation {
unsigned m_scope_lvl; //!< scope level when this equation was created.
unsigned m_bidx:31; //!< position at m_equations_to_delete
unsigned m_lc:1; //!< true if equation if a linear combination of the input equations.
ptr_vector<monomial> m_monomials; //!< sorted monomials
v_dependency * m_dep; //!< justification for the equality
friend class grobner;
equation() {}
public:
unsigned get_num_monomials() const { return m_monomials.size(); }
monomial const * get_monomial(unsigned idx) const { return m_monomials[idx]; }
monomial * const * get_monomials() const { return m_monomials.c_ptr(); }
v_dependency * get_dependency() const { return m_dep; }
unsigned hash() const { return m_bidx; }
bool is_linear_combination() const { return m_lc; }
};
enum class var_weight {
FIXED = 0,
QUOTED_FIXED = 1,
@ -37,10 +66,18 @@ enum class var_weight {
};
class nla_grobner : common {
typedef obj_hashtable<equation> equation_set;
typedef ptr_vector<equation> equation_vector;
equation_vector m_equations_to_unfreeze;
equation_vector m_equations_to_delete;
lp::int_set m_rows;
lp::int_set m_active_vars;
svector<var_weight> m_active_vars_weights;
unsigned m_num_new_equations;
unsigned m_num_of_equations;
grobner_stats m_stats;
equation_set m_processed;
equation_set m_to_process;
public:
nla_grobner(core *core);
void grobner_lemmas();
@ -58,6 +95,14 @@ private:
bool push_calculation_forward();
void compute_basis_init();
bool compute_basis_loop();
bool compute_basis_step();
equation* simplify_using_processed(equation*);
equation* simplify_processed(equation*);
equation* simplify_to_process(equation*);
equation* pick_next();
void set_gb_exhausted();
bool canceled() { return false; } // todo, implement
void superpose(equation * eq1, equation * eq2);
void superpose(equation * eq);
}; // end of grobner
}

2
src/math/lp/nla_order_lemmas.cpp
View file

@ -28,7 +28,7 @@ namespace nla {
// a > b && c > 0 => ac > bc
void order::order_lemma() {
TRACE("nla_solver", );
if (!c().m_settings.run_order()) {
if (!c().m_nla_settings.run_order()) {
TRACE("nla_solver", tout << "not generating order lemmas\n";);
return;
}

3
src/math/lp/nla_params.pyg
View file

@ -7,7 +7,8 @@ def_module_params('nla',
('horner_frequency', UINT, 4, 'horner\'s call frequency'),
('horner_row_length_limit', UINT, 10, 'row is disregarded by the heuristic if its length is longer than the value'),
('grobner', BOOL, True, 'run grobner\'s heuristic'),
('grobner_frequency', UINT, 5, 'grobner\'s call frequency')
('grobner_frequency', UINT, 5, 'grobner\'s call frequency'),
('grobner_eqs_threshold', UINT, 512, 'grobner\'s maximum number of equalities')
))

8
src/math/lp/nla_settings.h
View file

@ -27,8 +27,10 @@ class nla_settings {
// how often to call the horner heuristic
unsigned m_horner_frequency;
unsigned m_horner_row_length_limit;
// grobner fields
bool m_run_grobner;
unsigned m_grobner_frequency;
unsigned m_grobner_eqs_threshold;
public:
nla_settings() : m_run_order(true),
@ -37,9 +39,13 @@ public:
m_horner_frequency(4),
m_horner_row_length_limit(10),
m_run_grobner(true),
m_grobner_frequency(5)
m_grobner_frequency(5),
m_grobner_eqs_threshold(512)
{}
unsigned grobner_eqs_threshold() const { return m_grobner_eqs_threshold; }
unsigned& grobner_eqs_threshold() { return m_grobner_eqs_threshold; }
bool run_order() const { return m_run_order; }
bool& run_order() { return m_run_order; }

2
src/math/lp/nla_tangent_lemmas.cpp
View file

@ -30,7 +30,7 @@ std::ostream& tangents::print_tangent_domain(const point &a, const point &b, std
return out << "(" << a << ", " << b << ")";
}
void tangents::tangent_lemma() {
if (!c().m_settings.run_tangents()) {
if (!c().m_nla_settings.run_tangents()) {
TRACE("nla_solver", tout << "not generating tangent lemmas\n";);
return;
}

15
src/smt/theory_lra.cpp
View file

@ -448,13 +448,14 @@ class theory_lra::imp {
m_nla->push();
}
nla_params nla(ctx().get_params());
m_nla->get_core()->m_settings.run_order() = nla.order();
m_nla->get_core()->m_settings.run_tangents() = nla.tangents();
m_nla->get_core()->m_settings.run_horner() = nla.horner();
m_nla->get_core()->m_settings.horner_frequency() = nla.horner_frequency();
m_nla->get_core()->m_settings.horner_row_length_limit() = nla.horner_row_length_limit();
m_nla->get_core()->m_settings.grobner_frequency() = nla.grobner_frequency();
m_nla->get_core()->m_settings.run_grobner() = nla.grobner();
m_nla->get_core()->m_nla_settings.run_order() = nla.order();
m_nla->get_core()->m_nla_settings.run_tangents() = nla.tangents();
m_nla->get_core()->m_nla_settings.run_horner() = nla.horner();
m_nla->get_core()->m_nla_settings.horner_frequency() = nla.horner_frequency();
m_nla->get_core()->m_nla_settings.horner_row_length_limit() = nla.horner_row_length_limit();
m_nla->get_core()->m_nla_settings.grobner_frequency() = nla.grobner_frequency();
m_nla->get_core()->m_nla_settings.run_grobner() = nla.grobner();
m_nla->get_core()->m_nla_settings.grobner_eqs_threshold() = nla.grobner_eqs_threshold();
}
}