mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
consolidate parameters, add comment (#102)
* updates Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * code review of nla_intervals: combine functionality Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * tidy Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * formatting Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * add comments Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * merge issue Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * tired of looking at compiler warning Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
580f229a16
commit
0535e24dd1
|
@ -24,15 +24,15 @@ using namespace nla;
|
|||
|
||||
grobner::grobner(core *c, intervals *s)
|
||||
: common(c, s),
|
||||
m_gc(m_nex_creator,
|
||||
c->m_reslim,
|
||||
c->m_nla_settings.grobner_eqs_threshold(),
|
||||
c->m_nla_settings.grobner_expr_size_limit()
|
||||
),
|
||||
m_gc(m_nex_creator, c->m_reslim),
|
||||
m_look_for_fixed_vars_in_rows(false) {
|
||||
std::function<void (lp::explanation const& e, std::ostream & out)> de;
|
||||
de = [this](lp::explanation const& e, std::ostream& out) { m_core->print_explanation(e, out); };
|
||||
grobner_core::params p;
|
||||
p.m_expr_size_limit = c->m_nla_settings.grobner_expr_size_limit();
|
||||
p.m_grobner_eqs_threshold = c->m_nla_settings.grobner_eqs_threshold();
|
||||
m_gc = de;
|
||||
m_gc = p;
|
||||
}
|
||||
|
||||
void grobner::grobner_lemmas() {
|
||||
|
@ -183,6 +183,22 @@ void grobner::add_row(unsigned i) {
|
|||
/// -------------------------------
|
||||
/// grobner_core
|
||||
|
||||
/***
|
||||
The main algorithm maintains two sets (S, A),
|
||||
where S is m_to_superpose, and A is m_to_simplify.
|
||||
Initially S is empty and A contains the initial equations.
|
||||
|
||||
Each step proceeds as follows:
|
||||
- pick a in A, and remove a from A
|
||||
- simplify a using S
|
||||
- simplify S using a
|
||||
- for s in S:
|
||||
b = superpose(a, s)
|
||||
add b to A
|
||||
- add a to S
|
||||
- simplify A using a
|
||||
*/
|
||||
|
||||
bool grobner_core::compute_basis_loop() {
|
||||
while (!done()) {
|
||||
if (compute_basis_step()) {
|
||||
|
@ -205,20 +221,22 @@ bool grobner_core::compute_basis_step() {
|
|||
}
|
||||
m_stats.m_compute_steps++;
|
||||
simplify_using_to_superpose(*eq);
|
||||
|
||||
if (equation_is_too_complex(eq))
|
||||
return false;
|
||||
if (!canceled() && simplify_to_superpose_with_eq(eq)) {
|
||||
TRACE("grobner", tout << "eq = "; display_equation(tout, *eq););
|
||||
superpose(eq);
|
||||
if (equation_is_too_complex(eq)) {
|
||||
TRACE("grobner", display_equation(tout, *eq) << " is too complex: deleting it\n;";);
|
||||
del_equation(eq);
|
||||
} else {
|
||||
insert_to_superpose(eq);
|
||||
simplify_m_to_simplify(eq);
|
||||
TRACE("grobner", tout << "end of iteration:\n"; display(tout););
|
||||
}
|
||||
if (!simplify_to_superpose_with_eq(eq)) {
|
||||
return false;
|
||||
}
|
||||
TRACE("grobner", tout << "eq = "; display_equation(tout, *eq););
|
||||
superpose(eq);
|
||||
if (equation_is_too_complex(eq)) {
|
||||
TRACE("grobner", display_equation(tout, *eq) << " is too complex: deleting it\n;";);
|
||||
del_equation(eq);
|
||||
return false;
|
||||
}
|
||||
insert_to_superpose(eq);
|
||||
simplify_m_to_simplify(eq);
|
||||
TRACE("grobner", tout << "end of iteration:\n"; display(tout););
|
||||
return false;
|
||||
}
|
||||
|
||||
|
@ -241,6 +259,26 @@ grobner_core::equation* grobner_core::pick_next() {
|
|||
return r;
|
||||
}
|
||||
|
||||
void grobner_core::simplify_using_to_superpose(equation& eq) {
|
||||
bool simplified;
|
||||
TRACE("grobner", tout << "simplifying: "; display_equation(tout, eq); tout << "using equalities of m_to_superpose of size " << m_to_superpose.size() << "\n";);
|
||||
do {
|
||||
simplified = false;
|
||||
for (equation* p : m_to_superpose) {
|
||||
if (simplify_source_target(*p, eq)) {
|
||||
simplified = true;
|
||||
}
|
||||
if (canceled() || eq.expr()->is_scalar()) {
|
||||
break;
|
||||
}
|
||||
}
|
||||
} while (simplified && !eq.expr()->is_scalar());
|
||||
|
||||
TRACE("grobner",
|
||||
if (simplified) { tout << "simplification result: "; display_equation(tout, eq); }
|
||||
else { tout << "no simplification\n"; });
|
||||
}
|
||||
|
||||
grobner_core::equation_set const& grobner_core::equations() {
|
||||
m_all_eqs.reset();
|
||||
for (auto e : m_to_simplify) m_all_eqs.insert(e);
|
||||
|
@ -279,29 +317,7 @@ void grobner_core::del_equation(equation * eq) {
|
|||
SASSERT(m_equations_to_delete[eq->m_bidx] == eq);
|
||||
m_equations_to_delete[eq->m_bidx] = nullptr;
|
||||
dealloc(eq);
|
||||
}
|
||||
|
||||
void grobner_core::simplify_using_to_superpose(equation& eq) {
|
||||
bool simplified;
|
||||
TRACE("grobner", tout << "simplifying: "; display_equation(tout, eq); tout << "using equalities of m_to_superpose of size " << m_to_superpose.size() << "\n";);
|
||||
do {
|
||||
simplified = false;
|
||||
for (equation* p : m_to_superpose) {
|
||||
if (simplify_source_target(*p, eq)) {
|
||||
simplified = true;
|
||||
}
|
||||
if (canceled() || eq.expr()->is_scalar()) {
|
||||
break;
|
||||
}
|
||||
}
|
||||
}
|
||||
while (simplified && !eq.expr()->is_scalar());
|
||||
|
||||
TRACE("grobner",
|
||||
if (simplified) { tout << "simplification result: "; display_equation(tout, eq);}
|
||||
else {tout << "no simplification\n";});
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
const nex* grobner_core::get_highest_monomial(const nex* e) const {
|
||||
switch (e->type()) {
|
||||
|
@ -725,7 +741,7 @@ bool grobner_core::canceled() {
|
|||
}
|
||||
|
||||
bool grobner_core::done() {
|
||||
return num_of_equations() >= m_grobner_eqs_threshold || canceled();
|
||||
return num_of_equations() >= m_params.m_grobner_eqs_threshold || canceled();
|
||||
}
|
||||
|
||||
void grobner_core::del_equations(unsigned old_size) {
|
||||
|
|
|
@ -38,6 +38,11 @@ struct grobner_stats {
|
|||
|
||||
class grobner_core {
|
||||
public:
|
||||
struct params {
|
||||
unsigned m_grobner_eqs_threshold;
|
||||
unsigned m_expr_size_limit;
|
||||
};
|
||||
|
||||
class equation {
|
||||
unsigned m_bidx; //!< position at m_equations_to_delete
|
||||
nex * m_expr; // simplified expressionted monomials
|
||||
|
@ -88,16 +93,14 @@ private:
|
|||
nex_lt m_lt;
|
||||
bool m_changed_leading_term;
|
||||
equation_set m_all_eqs;
|
||||
unsigned m_grobner_eqs_threshold;
|
||||
unsigned m_expr_size_limit;
|
||||
params m_params;
|
||||
|
||||
public:
|
||||
grobner_core(nex_creator& nc, reslimit& lim, unsigned eqs_threshold, unsigned expr_size_limit) :
|
||||
grobner_core(nex_creator& nc, reslimit& lim) :
|
||||
m_nex_creator(nc),
|
||||
m_limit(lim),
|
||||
m_dep_manager(m_val_manager, m_alloc),
|
||||
m_changed_leading_term(false),
|
||||
m_grobner_eqs_threshold(eqs_threshold),
|
||||
m_expr_size_limit(expr_size_limit)
|
||||
m_changed_leading_term(false)
|
||||
{}
|
||||
|
||||
~grobner_core();
|
||||
|
@ -112,6 +115,7 @@ public:
|
|||
std::ostream& display(std::ostream& out) const;
|
||||
|
||||
void operator=(print_expl_t& pe) { m_print_explanation = pe; }
|
||||
void operator=(params const& p) { m_params = p; }
|
||||
|
||||
private:
|
||||
bool compute_basis_step();
|
||||
|
@ -160,7 +164,7 @@ private:
|
|||
std::ostream& print_stats(std::ostream&) const;
|
||||
std::ostream& display_dependency(std::ostream& out, common::ci_dependency*) const;
|
||||
bool equation_is_too_complex(const equation* eq) const {
|
||||
return eq->expr()->size() > m_expr_size_limit;
|
||||
return eq->expr()->size() > m_params.m_expr_size_limit;
|
||||
}
|
||||
#ifdef Z3DEBUG
|
||||
bool test_find_b_c(const nex* ab, const nex* ac, const nex_mul* b, const nex_mul* c);
|
||||
|
|
|
@ -5,6 +5,7 @@
|
|||
|
||||
namespace nla {
|
||||
|
||||
|
||||
typedef intervals::interval interv;
|
||||
typedef enum intervals::with_deps_t e_with_deps;
|
||||
|
||||
|
|
|
@ -293,6 +293,7 @@ public:
|
|||
if (wd == with_deps) {
|
||||
i.m_lower_dep = a.m_lower_dep;
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
template <enum with_deps_t wd>
|
||||
|
@ -313,8 +314,10 @@ public:
|
|||
}
|
||||
|
||||
template <enum with_deps_t wd>
|
||||
|
||||
bool interval_from_term(const nex& e, interval& i) const;
|
||||
|
||||
|
||||
template <enum with_deps_t wd>
|
||||
interval interval_of_sum_no_term(const nex_sum& e);
|
||||
|
||||
|
|
|
@ -2171,7 +2171,7 @@ public:
|
|||
for(const nla::lemma & l : lv) {
|
||||
m_lemma = l; //todo avoid the copy
|
||||
m_explanation = l.expl();
|
||||
m_stats.m_nla_explanations += l.expl().size();
|
||||
m_stats.m_nla_explanations += static_cast<unsigned>(l.expl().size());
|
||||
false_case_of_check_nla();
|
||||
}
|
||||
break;
|
||||
|
|
Loading…
Reference in a new issue