mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

port grobner basis functionality

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-09-18 11:53:17 -07:00
parent 29cc2c5976
commit e8b6b870ac
4 changed files with 81 additions and 34 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -21,7 +21,27 @@
#include "math/lp/nla_core.h"
#include "math/lp/factorization_factory_imp.h"
namespace nla {
nla_grobner::nla_grobner(core *c) : common(c) {}
nla_grobner::nla_grobner(core *c) : common(c), m_nl_gb_exhausted(false) {}
// 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
bool nla_grobner::scan_for_linear(ptr_vector<equation>& eqs) {
bool result = false;
for (nla_grobner::equation* eq : eqs) {
if (!eq->is_linear_combination()) {
TRACE("non_linear", tout << "processing new equality:\n"; display_equation(tout, *eq););
TRACE("non_linear_bug", tout << "processing new equality:\n"; display_equation(tout, *eq););
if (internalize_gb_eq(eq))
result = true;
}
}
return result;
}
bool nla_grobner::internalize_gb_eq(equation* ) {
NOT_IMPLEMENTED_YET();
return false;
}
void nla_grobner::add_var_and_its_factors_to_q_and_collect_new_rows(lpvar j, std::queue<lpvar> & q) {
SASSERT(m_active_vars.contains(j) == false);
@ -122,9 +142,20 @@ void nla_grobner::display(std::ostream & out) {
c().print_term(r, out) << std::endl;
}
}
void nla_grobner::add_row_to_gb(unsigned) {
NOT_IMPLEMENTED_YET();
}
void nla_grobner::add_monomial_def(lpvar) {
NOT_IMPLEMENTED_YET();
}
void nla_grobner::init() {
find_nl_cluster();
for (unsigned i : m_rows) {
add_row_to_gb(i);
}
for (lpvar j : m_active_vars) {
add_monomial_def(j);
}
}
bool nla_grobner::is_trivial(equation* eq) const {
@ -158,7 +189,7 @@ void nla_grobner::del_equation(equation * eq) {
*/
}
equation* nla_grobner::pick_next() {
nla_grobner::equation* nla_grobner::pick_next() {
equation * r = nullptr;
ptr_buffer<equation> to_delete;
for (equation * curr : m_to_process) {
@ -175,18 +206,18 @@ equation* nla_grobner::pick_next() {
return r;
}
equation* nla_grobner::simplify_using_processed(equation* eq) {
SASSERT(false);
nla_grobner::equation* nla_grobner::simplify_using_processed(equation* eq) {
NOT_IMPLEMENTED_YET();
return nullptr;
}
equation* nla_grobner::simplify_processed(equation* eq) {
SASSERT(false);
nla_grobner::equation* nla_grobner::simplify_processed(equation* eq) {
NOT_IMPLEMENTED_YET();
return nullptr;
}
equation* nla_grobner::simplify_to_process(equation*) {
SASSERT(false);
nla_grobner::equation* nla_grobner::simplify_to_process(equation*) {
NOT_IMPLEMENTED_YET();
return nullptr;
}
@ -241,7 +272,7 @@ bool nla_grobner::compute_basis_loop(){
}
void nla_grobner::set_gb_exhausted(){
NOT_IMPLEMENTED_YET();
m_nl_gb_exhausted = true;
}
void nla_grobner::update_statistics(){
@ -288,17 +319,26 @@ void nla_grobner::get_equations(ptr_vector<equation>& result) {
}
bool nla_grobner::push_calculation_forward(){
bool nla_grobner::push_calculation_forward(ptr_vector<equation>& eqs, unsigned & next_weight) {
return scan_for_linear(eqs)
&&
(!m_nl_gb_exhausted) &&
try_to_modify_eqs(eqs, next_weight);
}
bool nla_grobner::try_to_modify_eqs(ptr_vector<equation>& eqs, unsigned& next_weight) {
NOT_IMPLEMENTED_YET();
return false;
}
void nla_grobner::grobner_lemmas() {
c().lp_settings().stats().m_grobner_calls++;
init();
ptr_vector<equation> eqs;
unsigned next_weight =
(unsigned)(var_weight::MAX_DEFAULT_WEIGHT) + 1; // next weight using during perturbation phase.
do {
TRACE("nla_gb", tout << "before:\n"; display(tout););
compute_basis();
@ -307,7 +347,7 @@ void nla_grobner::grobner_lemmas() {
if (find_conflict(eqs))
return;
}
while(push_calculation_forward());
while(push_calculation_forward(eqs, next_weight));
}
void nla_grobner:: del_equations(unsigned old_size) {
SASSERT(m_equations_to_delete.size() >= old_size);

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

@ -50,23 +50,6 @@ public:
lpvar get_var(unsigned idx) const { return m_vars[idx]; }
};
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 nla_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,
@ -80,6 +63,24 @@ enum class var_weight {
};
class nla_grobner : common {
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 nla_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; }
};
typedef obj_hashtable<equation> equation_set;
typedef ptr_vector<equation> equation_vector;
@ -93,10 +94,12 @@ class nla_grobner : common {
grobner_stats m_stats;
equation_set m_processed;
equation_set m_to_process;
bool m_nl_gb_exhausted;
public:
nla_grobner(core *core);
void grobner_lemmas();
private:
bool scan_for_linear(ptr_vector<equation>& eqs);
void find_nl_cluster();
void prepare_rows_and_active_vars();
void add_var_and_its_factors_to_q_and_collect_new_rows(lpvar j, std::queue<lpvar>& q);
@ -109,7 +112,7 @@ private:
bool find_conflict(ptr_vector<equation>& eqs);
bool is_inconsistent(equation*);
bool is_inconsistent2(equation*);
bool push_calculation_forward();
bool push_calculation_forward(ptr_vector<equation>& eqs, unsigned&);
void compute_basis_init();
bool compute_basis_loop();
bool compute_basis_step();
@ -132,5 +135,9 @@ private:
void display(std::ostream & out) const;
void get_equations(ptr_vector<equation>& eqs);
bool try_to_modify_eqs(ptr_vector<equation>& eqs, unsigned& next_weight);
bool internalize_gb_eq(equation*);
void add_row_to_gb(unsigned);
void add_monomial_def(lpvar);
}; // end of grobner
}

2
src/smt/theory_arith.h
View file

@ -1043,7 +1043,7 @@ namespace smt {
void compute_basis(grobner&, bool&);
void update_statistics(grobner&);
void set_gb_exhausted();
bool pass_over_gb_eqs_for_conflict(ptr_vector<grobner::equation>& eqs, grobner&);
bool get_gb_eqs_and_look_for_conflict(ptr_vector<grobner::equation>& eqs, grobner&);
bool 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();

4
src/smt/theory_arith_nl.h
View file

@ -2241,7 +2241,7 @@ void theory_arith<Ext>::set_gb_exhausted() {
// 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) {
bool theory_arith<Ext>::get_gb_eqs_and_look_for_conflict(ptr_vector<grobner::equation>& eqs, grobner& gb) {
eqs.reset();
gb.get_equations(eqs);
TRACE("grobner_bug", tout << "after gb\n";);
@ -2346,7 +2346,7 @@ typename theory_arith<Ext>::gb_result theory_arith<Ext>::compute_grobner(svector
TRACE("non_linear_gb", tout << "after:\n"; gb.display(tout););
if (get_context().get_cancel_flag())
return GB_FAIL;
if (pass_over_gb_eqs_for_conflict(eqs, gb))
if (get_gb_eqs_and_look_for_conflict(eqs, gb))
return GB_PROGRESS;
}
while(scan_for_linear(eqs, gb) && m_params.m_nl_arith_gb_perturbate &&