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

merged dependency.h from main repo

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-12-18 21:01:45 -10:00
parent 1dbffe7367
commit 0039b68ca3
6 changed files with 51 additions and 59 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/math/lp/nla_common.cpp
View file

@ -161,15 +161,15 @@ nex * common::nexvar(const rational & coeff, lpvar j, nex_creator& cn, bool fixe
} }
template <typename T> common::ci_dependency* common::create_sum_from_row(const T& row, template <typename T> u_dependency* common::create_sum_from_row(const T& row,
nex_creator& cn, nex_creator& cn,
nex_creator::sum_factory& sum, nex_creator::sum_factory& sum,
bool fixed_as_scalars, bool fixed_as_scalars,
ci_dependency_manager* dep_manager u_dependency_manager* dep_manager
) { ) {
TRACE("nla_horner", tout << "row="; m_core->print_term(row, tout) << "\n";); TRACE("nla_horner", tout << "row="; m_core->print_term(row, tout) << "\n";);
ci_dependency * dep = nullptr; u_dependency * dep = nullptr;
SASSERT(row.size() > 1); SASSERT(row.size() > 1);
sum.reset(); sum.reset();
for (const auto &p : row) { for (const auto &p : row) {
@ -190,9 +190,9 @@ template <typename T> common::ci_dependency* common::create_sum_from_row(const T
} }
template <typename T> template <typename T>
common::ci_dependency* common::get_fixed_vars_dep_from_row(const T& row, ci_dependency_manager& dep_manager) { u_dependency* common::get_fixed_vars_dep_from_row(const T& row, u_dependency_manager& dep_manager) {
TRACE("nla_horner", tout << "row="; m_core->print_term(row, tout) << "\n";); TRACE("nla_horner", tout << "row="; m_core->print_term(row, tout) << "\n";);
ci_dependency* dep = nullptr; u_dependency* dep = nullptr;
for (const auto &p : row) { for (const auto &p : row) {
lpvar j = p.var(); lpvar j = p.var();
if (!c().is_monic_var(j)) { if (!c().is_monic_var(j)) {
@ -256,6 +256,5 @@ var_weight common::get_var_weight(lpvar j) const {
} }
template nla::common::ci_dependency* nla::common::create_sum_from_row<old_vector<lp::row_cell<rational>, true, unsigned int> >(old_vector<lp::row_cell<rational>, true, unsigned int> const&, nla::nex_creator&, nla::nex_creator::sum_factory&, bool, ci_dependency_manager*); template u_dependency* nla::common::create_sum_from_row<old_vector<lp::row_cell<rational>, true, unsigned int> >(old_vector<lp::row_cell<rational>, true, unsigned int> const&, nla::nex_creator&, nla::nex_creator::sum_factory&, bool, u_dependency_manager*);
template dependency_manager<scoped_dependency_manager<unsigned int>::config>::dependency* nla::common::get_fixed_vars_dep_from_row<old_vector<lp::row_cell<rational>, true, unsigned int> >(old_vector<lp::row_cell<rational>, true, unsigned int> const&, scoped_dependency_manager<unsigned int>&);
template dependency_manager<nla::common::ci_dependency_config>::dependency* nla::common::get_fixed_vars_dep_from_row<old_vector<lp::row_cell<rational>, true, unsigned int> >(old_vector<lp::row_cell<rational>, true, unsigned int> const&, dependency_manager<nla::common::ci_dependency_config>&);

9
src/math/lp/nla_common.h
View file

@ -109,22 +109,19 @@ struct common {
} }
}; };
struct ci_dependency_config { struct u_dependency_config {
typedef ci_value_manager value_manager; typedef ci_value_manager value_manager;
typedef region allocator; typedef region allocator;
static const bool ref_count = false; static const bool ref_count = false;
typedef lp::constraint_index value; typedef lp::constraint_index value;
}; };
typedef dependency_manager<ci_dependency_config> ci_dependency_manager;
typedef ci_dependency_manager::dependency ci_dependency;
// nex* nexvar(lpvar j, nex_creator&, svector<lp::constraint_index> & fixed_vars_constraints); // nex* nexvar(lpvar j, nex_creator&, svector<lp::constraint_index> & fixed_vars_constraints);
nex* nexvar(const rational& coeff, lpvar j, nex_creator&, bool); nex* nexvar(const rational& coeff, lpvar j, nex_creator&, bool);
template <typename T> template <typename T>
ci_dependency* create_sum_from_row(const T&, nex_creator&, nex_creator::sum_factory&, bool, ci_dependency_manager*); u_dependency* create_sum_from_row(const T&, nex_creator&, nex_creator::sum_factory&, bool, u_dependency_manager*);
template <typename T> template <typename T>
ci_dependency* get_fixed_vars_dep_from_row(const T&, ci_dependency_manager& dep_manager); u_dependency* get_fixed_vars_dep_from_row(const T&, u_dependency_manager& dep_manager);
void set_active_vars_weights(); void set_active_vars_weights();
var_weight get_var_weight(lpvar) const; var_weight get_var_weight(lpvar) const;
}; };

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

@ -174,7 +174,7 @@ void grobner::add_row(unsigned i) {
TRACE("grobner", tout << "adding row to gb\n"; c().m_lar_solver.print_row(row, tout) << '\n'; TRACE("grobner", tout << "adding row to gb\n"; c().m_lar_solver.print_row(row, tout) << '\n';
for (auto p : row) c().print_var(p.var(), tout) << "\n"; ); for (auto p : row) c().print_var(p.var(), tout) << "\n"; );
nex_creator::sum_factory sf(m_nex_creator); nex_creator::sum_factory sf(m_nex_creator);
ci_dependency* dep = create_sum_from_row(row, m_nex_creator, sf, m_look_for_fixed_vars_in_rows, &m_gc.dep()); u_dependency* dep = create_sum_from_row(row, m_nex_creator, sf, m_look_for_fixed_vars_in_rows, &m_gc.dep());
nex* e = m_nex_creator.simplify(sf.mk()); nex* e = m_nex_creator.simplify(sf.mk());
TRACE("grobner", tout << "e = " << *e << "\n";); TRACE("grobner", tout << "e = " << *e << "\n";);
m_gc.assert_eq_0(e, dep); m_gc.assert_eq_0(e, dep);
@ -792,7 +792,7 @@ std::ostream& grobner_core::display(std::ostream& out) const {
return out; return out;
} }
void grobner_core::assert_eq_0(nex* e, common::ci_dependency * dep) { void grobner_core::assert_eq_0(nex* e, u_dependency * dep) {
if (e == nullptr || is_zero_scalar(e)) if (e == nullptr || is_zero_scalar(e))
return; return;
equation * eq = alloc(equation); equation * eq = alloc(equation);
@ -807,7 +807,7 @@ void grobner_core::assert_eq_0(nex* e, common::ci_dependency * dep) {
update_stats_max_degree_and_size(eq); update_stats_max_degree_and_size(eq);
} }
void grobner_core::init_equation(equation* eq, nex*e, common::ci_dependency * dep) { void grobner_core::init_equation(equation* eq, nex*e, u_dependency * dep) {
eq->m_bidx = m_equations_to_delete.size(); eq->m_bidx = m_equations_to_delete.size();
eq->m_dep = dep; eq->m_dep = dep;
eq->m_expr = e; eq->m_expr = e;
@ -819,7 +819,7 @@ grobner_core::~grobner_core() {
del_equations(0); del_equations(0);
} }
std::ostream& grobner_core::display_dependency(std::ostream& out, common::ci_dependency* dep) const { std::ostream& grobner_core::display_dependency(std::ostream& out, u_dependency* dep) const {
svector<lp::constraint_index> expl; svector<lp::constraint_index> expl;
m_dep_manager.linearize(dep, expl); m_dep_manager.linearize(dep, expl);
lp::explanation e(expl); lp::explanation e(expl);

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

@ -77,7 +77,7 @@ public:
class equation { class equation {
unsigned m_bidx; //!< position at m_equations_to_delete unsigned m_bidx; //!< position at m_equations_to_delete
nex * m_expr; // simplified expressionted monomials nex * m_expr; // simplified expressionted monomials
common::ci_dependency * m_dep; //!< justification for the equality u_dependency * m_dep; //!< justification for the equality
public: public:
unsigned get_num_monomials() const { unsigned get_num_monomials() const {
switch(m_expr->type()) { switch(m_expr->type()) {
@ -102,7 +102,7 @@ public:
} }
} }
const nex* expr() const { return m_expr; } const nex* expr() const { return m_expr; }
common::ci_dependency * dep() const { return m_dep; } u_dependency * dep() const { return m_dep; }
unsigned hash() const { return m_bidx; } unsigned hash() const { return m_bidx; }
friend class grobner_core; friend class grobner_core;
}; };
@ -119,8 +119,7 @@ private:
equation_set m_to_superpose; equation_set m_to_superpose;
equation_set m_to_simplify; equation_set m_to_simplify;
region m_alloc; region m_alloc;
common::ci_value_manager m_val_manager; mutable u_dependency_manager m_dep_manager;
mutable common::ci_dependency_manager m_dep_manager;
nex_lt m_lt; nex_lt m_lt;
bool m_changed_leading_term; bool m_changed_leading_term;
params m_params; params m_params;
@ -129,16 +128,16 @@ public:
grobner_core(nex_creator& nc, reslimit& lim) : grobner_core(nex_creator& nc, reslimit& lim) :
m_nex_creator(nc), m_nex_creator(nc),
m_limit(lim), m_limit(lim),
m_dep_manager(m_val_manager, m_alloc), m_dep_manager(),
m_changed_leading_term(false) m_changed_leading_term(false)
{} {}
~grobner_core(); ~grobner_core();
void reset(); void reset();
bool compute_basis_loop(); bool compute_basis_loop();
void assert_eq_0(nex*, common::ci_dependency * dep); void assert_eq_0(nex*, u_dependency * dep);
concat<equation_set, equation_set, equation*> equations(); concat<equation_set, equation_set, equation*> equations();
common::ci_dependency_manager& dep() const { return m_dep_manager; } u_dependency_manager& dep() const { return m_dep_manager; }
void display_equations_no_deps(std::ostream& out, equation_set const& v, char const* header) const; void display_equations_no_deps(std::ostream& out, equation_set const& v, char const* header) const;
void display_equations(std::ostream& out, equation_set const& v, char const* header) const; void display_equations(std::ostream& out, equation_set const& v, char const* header) const;
@ -167,7 +166,7 @@ private:
bool is_simpler(equation * eq1, equation * eq2); bool is_simpler(equation * eq1, equation * eq2);
void del_equations(unsigned old_size); void del_equations(unsigned old_size);
void del_equation(equation * eq); void del_equation(equation * eq);
void init_equation(equation* eq, nex*, common::ci_dependency* d); void init_equation(equation* eq, nex*, u_dependency* d);
void insert_to_simplify(equation *eq) { void insert_to_simplify(equation *eq) {
TRACE("grobner", display_equation(tout, *eq);); TRACE("grobner", display_equation(tout, *eq););
@ -193,7 +192,7 @@ private:
void update_stats_max_degree_and_size(const equation*); void update_stats_max_degree_and_size(const equation*);
std::ostream& print_stats(std::ostream&) const; std::ostream& print_stats(std::ostream&) const;
std::ostream& display_dependency(std::ostream& out, common::ci_dependency*) const; std::ostream& display_dependency(std::ostream& out, u_dependency*) const;
bool equation_is_too_complex(const equation* eq) const { bool equation_is_too_complex(const equation* eq) const {
return eq->expr()->size() > m_params.m_expr_size_limit; return eq->expr()->size() > m_params.m_expr_size_limit;
} }

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

@ -66,7 +66,7 @@ const nex* intervals::get_zero_interval_child(const nex_mul& e) const {
return nullptr; return nullptr;
} }
std::ostream & intervals::print_dependencies(ci_dependency* deps , std::ostream& out) const { std::ostream & intervals::print_dependencies(u_dependency* deps , std::ostream& out) const {
svector<lp::constraint_index> expl; svector<lp::constraint_index> expl;
m_dep_manager.linearize(deps, expl); m_dep_manager.linearize(deps, expl);
{ {
@ -82,7 +82,7 @@ std::ostream & intervals::print_dependencies(ci_dependency* deps , std::ostream&
} }
// return true iff the interval of n is does not contain 0 // return true iff the interval of n is does not contain 0
bool intervals::check_nex(const nex* n, ci_dependency* initial_deps) { bool intervals::check_nex(const nex* n, u_dependency* initial_deps) {
m_core->lp_settings().stats().m_cross_nested_forms++; m_core->lp_settings().stats().m_cross_nested_forms++;
auto i = interval_of_expr<without_deps>(n, 1); auto i = interval_of_expr<without_deps>(n, 1);
if (!separated_from_zero(i)) { if (!separated_from_zero(i)) {
@ -221,13 +221,13 @@ bool intervals::separated_from_zero_on_upper(const interval& i) const {
return true; return true;
} }
bool intervals::check_interval_for_conflict_on_zero(const interval & i, ci_dependency* dep) { bool 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); return check_interval_for_conflict_on_zero_lower(i, dep) || check_interval_for_conflict_on_zero_upper(i, dep);
} }
bool intervals::check_interval_for_conflict_on_zero_upper( bool intervals::check_interval_for_conflict_on_zero_upper(
const interval & i, const interval & i,
ci_dependency* dep) { u_dependency* dep) {
if (!separated_from_zero_on_upper(i)) if (!separated_from_zero_on_upper(i))
return false; return false;
@ -241,7 +241,7 @@ bool intervals::check_interval_for_conflict_on_zero_upper(
return true; return true;
} }
bool intervals::check_interval_for_conflict_on_zero_lower(const interval & i, ci_dependency* dep) { bool intervals::check_interval_for_conflict_on_zero_lower(const interval & i, u_dependency* dep) {
if (!separated_from_zero_on_lower(i)) { if (!separated_from_zero_on_lower(i)) {
return false; return false;
} }
@ -255,12 +255,12 @@ bool intervals::check_interval_for_conflict_on_zero_lower(const interval & i, ci
return true; return true;
} }
common::ci_dependency *intervals::mk_dep(lp::constraint_index ci) const { u_dependency *intervals::mk_dep(lp::constraint_index ci) const {
return m_dep_manager.mk_leaf(ci); return m_dep_manager.mk_leaf(ci);
} }
common::ci_dependency *intervals::mk_dep(const lp::explanation& expl) const { u_dependency *intervals::mk_dep(const lp::explanation& expl) const {
intervals::ci_dependency * r = nullptr; u_dependency * r = nullptr;
for (auto p : expl) { for (auto p : expl) {
if (r == nullptr) { if (r == nullptr) {
r = m_dep_manager.mk_leaf(p.second); r = m_dep_manager.mk_leaf(p.second);

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

@ -29,12 +29,9 @@ namespace nla {
class core; class core;
class intervals { class intervals {
typedef common::ci_dependency_manager ci_dependency_manager;
typedef ci_dependency_manager::dependency ci_dependency;
class im_config { class im_config {
unsynch_mpq_manager& m_manager; unsynch_mpq_manager& m_manager;
common::ci_dependency_manager& m_dep_manager; u_dependency_manager& m_dep_manager;
public: public:
typedef unsynch_mpq_manager numeral_manager; typedef unsynch_mpq_manager numeral_manager;
@ -52,8 +49,8 @@ class intervals {
unsigned m_upper_open : 1; unsigned m_upper_open : 1;
unsigned m_lower_inf : 1; unsigned m_lower_inf : 1;
unsigned m_upper_inf : 1; unsigned m_upper_inf : 1;
ci_dependency* m_lower_dep; // justification for the lower bound u_dependency* m_lower_dep; // justification for the lower bound
ci_dependency* m_upper_dep; // justification for the upper bound u_dependency* m_upper_dep; // justification for the upper bound
}; };
void add_deps(interval const& a, interval const& b, void add_deps(interval const& a, interval const& b,
@ -105,10 +102,10 @@ class intervals {
// Reference to numeral manager // Reference to numeral manager
numeral_manager& m() const { return m_manager; } numeral_manager& m() const { return m_manager; }
im_config(numeral_manager& m, ci_dependency_manager& d) :m_manager(m), m_dep_manager(d) {} im_config(numeral_manager& m, u_dependency_manager& d) :m_manager(m), m_dep_manager(d) {}
private: private:
ci_dependency* mk_dependency(interval const& a, interval const& b, deps_combine_rule bd) const { u_dependency* mk_dependency(interval const& a, interval const& b, deps_combine_rule bd) const {
ci_dependency* dep = nullptr; u_dependency* dep = nullptr;
if (dep_in_lower1(bd)) { if (dep_in_lower1(bd)) {
dep = m_dep_manager.mk_join(dep, a.m_lower_dep); dep = m_dep_manager.mk_join(dep, a.m_lower_dep);
} }
@ -124,8 +121,8 @@ class intervals {
return dep; return dep;
} }
ci_dependency* mk_dependency(interval const& a, deps_combine_rule bd) const { u_dependency* mk_dependency(interval const& a, deps_combine_rule bd) const {
ci_dependency* dep = nullptr; u_dependency* dep = nullptr;
if (dep_in_lower1(bd)) { if (dep_in_lower1(bd)) {
dep = m_dep_manager.mk_join(dep, a.m_lower_dep); dep = m_dep_manager.mk_join(dep, a.m_lower_dep);
} }
@ -140,17 +137,17 @@ class intervals {
region m_alloc; region m_alloc;
common::ci_value_manager m_val_manager; common::ci_value_manager m_val_manager;
mutable unsynch_mpq_manager m_num_manager; mutable unsynch_mpq_manager m_num_manager;
mutable ci_dependency_manager m_dep_manager; mutable u_dependency_manager m_dep_manager;
im_config m_config; im_config m_config;
mutable interval_manager<im_config> m_imanager; mutable interval_manager<im_config> m_imanager;
core* m_core; core* m_core;
public: public:
ci_dependency_manager& dep_manager() { return m_dep_manager; } u_dependency_manager& dep_manager() { return m_dep_manager; }
typedef interval_manager<im_config>::interval interval; typedef interval_manager<im_config>::interval interval;
private: private:
ci_dependency* mk_dep(lp::constraint_index ci) const; u_dependency* mk_dep(lp::constraint_index ci) const;
ci_dependency* mk_dep(lp::explanation const&) const; u_dependency* mk_dep(lp::explanation const&) const;
lp::lar_solver& ls(); lp::lar_solver& ls();
const lp::lar_solver& ls() const; const lp::lar_solver& ls() const;
public: public:
@ -158,15 +155,15 @@ public:
intervals(core* c, reslimit& lim) : intervals(core* c, reslimit& lim) :
m_alloc(), m_alloc(),
m_dep_manager(m_val_manager, m_alloc), m_dep_manager(),
m_config(m_num_manager, m_dep_manager), m_config(m_num_manager, m_dep_manager),
m_imanager(lim, im_config(m_num_manager, m_dep_manager)), m_imanager(lim, im_config(m_num_manager, m_dep_manager)),
m_core(c) m_core(c)
{} {}
ci_dependency* mk_join(ci_dependency* a, ci_dependency* b) { return m_dep_manager.mk_join(a, b); } u_dependency* mk_join(u_dependency* a, u_dependency* b) { return m_dep_manager.mk_join(a, b); }
ci_dependency* mk_leaf(lp::constraint_index ci) { return m_dep_manager.mk_leaf(ci); } u_dependency* mk_leaf(lp::constraint_index ci) { return m_dep_manager.mk_leaf(ci); }
std::ostream& print_dependencies(ci_dependency*, std::ostream&) const; std::ostream& print_dependencies(u_dependency*, std::ostream&) const;
std::ostream& display(std::ostream& out, const intervals::interval& i) const; std::ostream& display(std::ostream& out, const intervals::interval& i) const;
void set_lower(interval& a, rational const& n) const { m_config.set_lower(a, n.to_mpq()); } void set_lower(interval& a, rational const& n) const { m_config.set_lower(a, n.to_mpq()); }
void set_upper(interval& a, rational const& n) const { m_config.set_upper(a, n.to_mpq()); } void set_upper(interval& a, rational const& n) const { m_config.set_upper(a, n.to_mpq()); }
@ -345,9 +342,9 @@ public:
return separated_from_zero_on_upper(i) || return separated_from_zero_on_upper(i) ||
separated_from_zero_on_lower(i); separated_from_zero_on_lower(i);
} }
bool check_interval_for_conflict_on_zero(const interval& i, ci_dependency*); bool check_interval_for_conflict_on_zero(const interval& i, u_dependency*);
bool check_interval_for_conflict_on_zero_lower(const interval& i, ci_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, ci_dependency*); bool check_interval_for_conflict_on_zero_upper(const interval& i, u_dependency*);
mpq const& lower(interval const& a) const { return m_config.lower(a); } mpq const& lower(interval const& a) const { return m_config.lower(a); }
mpq const& upper(interval const& a) const { return m_config.upper(a); } mpq const& upper(interval const& a) const { return m_config.upper(a); }
inline bool is_empty(interval const& a) const { inline bool is_empty(interval const& a) const {
@ -362,7 +359,7 @@ public:
return false; return false;
} }
void reset() { m_alloc.reset(); } void reset() { m_alloc.reset(); }
bool check_nex(const nex*, ci_dependency*); bool check_nex(const nex*, u_dependency*);
typedef interval interv; typedef interval interv;
void set_interval_for_scalar(interv&, const rational&); void set_interval_for_scalar(interv&, const rational&);
const nex* get_zero_interval_child(const nex_mul&) const; const nex* get_zero_interval_child(const nex_mul&) const;