mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

prepare to hook up pdd_grobner

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-12-26 12:31:32 -08:00
parent 610a2837ea
commit c6ea5c2263
8 changed files with 71 additions and 39 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/math/dd/pdd_interval.h
View file

@ -63,9 +63,10 @@ public:
return ret;
}
}
bool separated_from_zero(pdd const& p, u_dependency*& dep) {
return m_dep_intervals.check_interval_for_conflict_on_zero(get_interval<w_dep::with_deps>(p), dep);
// f meant to be called when the separation happens
template <typename T>
bool separated_from_zero(pdd const& p, u_dependency*& dep, std::function<void (const T)>& f) {
return m_dep_intervals.check_interval_for_conflict_on_zero(get_interval<w_dep::with_deps>(p), dep, f);
}
};

22
src/math/interval/dep_intervals.cpp
View file

@ -86,28 +86,6 @@ bool dep_intervals::separated_from_zero_on_upper(const interval& i) const {
return true;
}
bool dep_intervals::check_interval_for_conflict_on_zero(const interval & i, u_dependency*& dep) {
return check_interval_for_conflict_on_zero_lower(i, dep) || check_interval_for_conflict_on_zero_upper(i, dep);
}
bool dep_intervals::check_interval_for_conflict_on_zero_upper(const interval & i, u_dependency*& dep) {
if (!separated_from_zero_on_upper(i))
return false;
TRACE("dep_intervals", display(tout, i););
dep = m_dep_manager.mk_join(dep, i.m_upper_dep);
return true;
}
bool dep_intervals::check_interval_for_conflict_on_zero_lower(const interval & i, u_dependency*& dep) {
if (!separated_from_zero_on_lower(i)) {
return false;
}
TRACE("dep_intervals", display(tout, i););
dep = m_dep_manager.mk_join(dep, i.m_lower_dep);
return true;
}
std::ostream& dep_intervals::display(std::ostream& out, const interval& i) const {
if (m_imanager.lower_is_inf(i)) {
out << "(-oo";

37
src/math/interval/dep_intervals.h
View file

@ -255,15 +255,44 @@ public:
inline bool separated_from_zero(const interval& i) const {
return separated_from_zero_on_upper(i) || separated_from_zero_on_lower(i);
}
bool check_interval_for_conflict_on_zero(const interval& i, u_dependency*&);
bool check_interval_for_conflict_on_zero_lower(const interval& i, u_dependency*&);
bool check_interval_for_conflict_on_zero_upper(const interval& i, u_dependency*&);
template <typename T>
bool check_interval_for_conflict_on_zero(const interval& i, u_dependency*& dep, std::function<void (const T&)> f) {
return check_interval_for_conflict_on_zero_lower(i, dep, f) || check_interval_for_conflict_on_zero_upper(i, dep, f);
}
template <typename T>
bool check_interval_for_conflict_on_zero_lower(const interval& i, u_dependency*& dep, std::function<void (const T&)> f) {
if (!separated_from_zero_on_lower(i)) {
return false;
}
TRACE("dep_intervals", display(tout, i););
dep = m_dep_manager.mk_join(dep, i.m_lower_dep);
T expl;
linearize(dep, expl);
f(expl);
return true;
}
template <typename T>
bool check_interval_for_conflict_on_zero_upper(const interval& i, u_dependency*& dep, std::function<void (const T&)> f) {
if (!separated_from_zero_on_upper(i))
return false;
TRACE("dep_intervals", display(tout, i););
dep = m_dep_manager.mk_join(dep, i.m_upper_dep);
T expl;
linearize(dep, expl);
f(expl);
return true;
}
mpq const& lower(interval const& a) const { return m_config.lower(a); }
mpq const& upper(interval const& a) const { return m_config.upper(a); }
bool is_empty(interval const& a) const;
void set_interval_for_scalar(interval&, const rational&);
template <typename T>
void linearize(u_dependency* dep, T& expl) const { m_dep_manager.linearize(dep, expl); }
void linearize(u_dependency* dep, T& expl) const {
vector<unsigned, false> v;
m_dep_manager.linearize(dep, v);
for (unsigned ci: v)
expl.push_back(ci);
}
void reset() { m_dep_manager.reset(); }

3
src/math/lp/explanation.h
View file

@ -41,6 +41,9 @@ public:
m_explanation.push_back(std::make_pair(one_of_type<mpq>(), j));
}
void push_back(constraint_index j) {
push_justification(j);
}
void add(const explanation& e) { for (auto j: e.m_set_of_ci) add(j); }
template <typename T>

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

@ -1284,9 +1284,11 @@ lbool core::incremental_linearization(bool constraint_derived) {
lbool core::inner_check(bool constraint_derived) {
if (constraint_derived) {
if (need_to_call_algebraic_methods())
if (m_horner.horner_lemmas()) {
switch( m_nla_settings.run_grobner()) {
case nla_settings::BOTH_GROBNER:
if (!m_horner.horner_lemmas()) {
clear_and_resize_active_var_set();
find_nl_cluster();
switch(m_nla_settings.run_grobner()) {
case nla_settings::NEX_AND_BDD_GROBNER:
init_nex_grobner(m_nex_grobner.get_nex_creator());
m_nex_grobner.grobner_lemmas();
run_pdd_grobner();
@ -1410,6 +1412,16 @@ std::ostream& core::print_term( const lp::lar_term& t, std::ostream& out) const
void core::run_pdd_grobner() {
m_pdd_manager.resize(m_lar_solver.number_of_vars());
for (unsigned i : m_rows) {
add_row_to_pdd_grobner(m_lar_solver.A_r().m_rows[i]);
}
m_pdd_grobner.saturate();
for (auto eq : m_pdd_grobner.equations()) {
check_pdd_eq(eq);
}
}
void core::check_pdd_eq(const dd::grobner::equation* e) {
NOT_IMPLEMENTED_YET();
}
@ -1442,7 +1454,12 @@ void core::add_var_and_its_factors_to_q_and_collect_new_rows(lpvar j, svector<lp
}
}
void core::find_nl_cluster(nex_creator& nc) {
void core::add_row_to_pdd_grobner(const vector<lp::row_cell<rational>> & row) {
NOT_IMPLEMENTED_YET();
}
void core::find_nl_cluster() {
prepare_rows_and_active_vars();
svector<lpvar> q;
for (lpvar j : m_to_refine) {
@ -1455,7 +1472,6 @@ void core::find_nl_cluster(nex_creator& nc) {
q.pop_back();
add_var_and_its_factors_to_q_and_collect_new_rows(j, q);
}
set_active_vars_weights(nc);
TRACE("grobner", display_matrix_of_m_rows(tout););
}
@ -1498,9 +1514,8 @@ void core::display_matrix_of_m_rows(std::ostream & out) const {
}
void core::init_nex_grobner(nex_creator & nc) {
find_nl_cluster(nc);
clear_and_resize_active_var_set();
TRACE("grobner", tout << "m_rows.size() = " << m_rows.size() << "\n";);
set_active_vars_weights(nc);
for (unsigned i : m_rows) {
m_nex_grobner.add_row(m_lar_solver.A_r().m_rows[i]);
}

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

@ -391,7 +391,7 @@ public:
std::ostream& print_terms(std::ostream&) const;
std::ostream& print_term( const lp::lar_term&, std::ostream&) const;
void run_pdd_grobner();
void find_nl_cluster(nex_creator&);
void find_nl_cluster();
void prepare_rows_and_active_vars();
void add_var_and_its_factors_to_q_and_collect_new_rows(lpvar j, svector<lpvar>& q);
void init_nex_grobner(nex_creator&);
@ -399,6 +399,8 @@ public:
void display_matrix_of_m_rows(std::ostream & out) const;
void set_active_vars_weights(nex_creator&);
var_weight get_var_weight(lpvar) const;
void add_row_to_pdd_grobner(const vector<lp::row_cell<rational>> & row);
void check_pdd_eq(const dd::grobner::equation*);
}; // end of core
struct pp_mon {

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

@ -79,7 +79,11 @@ bool intervals::check_nex(const nex* n, u_dependency* initial_deps) {
}
auto interv_wd = interval_of_expr<e_with_deps::with_deps>(n, 1);
TRACE("grobner", tout << "conflict: interv_wd = "; display(tout, interv_wd ) <<"expr = " << *n << "\n, initial deps\n"; print_dependencies(initial_deps, tout););
m_dep_intervals.check_interval_for_conflict_on_zero(interv_wd, initial_deps);
std::function<void (const lp::explanation&)> f = [this](const lp::explanation& e) {
m_core->add_empty_lemma();
m_core->current_expl().add(e);
};
m_dep_intervals.check_interval_for_conflict_on_zero(interv_wd, initial_deps, f);
m_dep_intervals.reset(); // clean the memory allocated by the interval bound dependencies
return true;
}

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

@ -23,7 +23,7 @@ namespace nla {
class nla_settings {
public:
enum run_grobner_enum {
NO_GROBNER, NEX_GROBNER, PDD_GROBNER, BOTH_GROBNER };
NO_GROBNER, NEX_GROBNER, PDD_GROBNER, NEX_AND_BDD_GROBNER };
private:
bool m_run_order;
bool m_run_tangents;