mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 20:38:43 +00:00
Code Activity

use regien to allocate and delete interval dependencies

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-08-09 11:00:01 -07:00
parent ae7e7333a6
commit 22e2ad6824
3 changed files with 53 additions and 57 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -25,7 +25,7 @@
namespace nla {
typedef intervals::interval interv;
horner::horner(core * c) : common(c) {}
horner::horner(core * c) : common(c), m_intervals(c, c->reslim()) {}
template <typename T>
bool horner::row_has_monomial_to_refine(const T& row) const {
@ -67,13 +67,12 @@ bool horner::lemmas_on_expr(nex& e) {
TRACE("nla_horner", tout << "e = " << e << "\n";);
bool conflict = false;
cross_nested cn(e, [this, & conflict](const nex& n) {
intervals ivs(&c(), c().reslim());
set_intervals(& ivs);
TRACE("nla_horner", tout << "cross-nested n = " << n << "\n";);
auto i = interval_of_expr(n);
TRACE("nla_horner", tout << "callback n = " << n << "\ni="; ivs.display(tout, i) << "\n";);
TRACE("nla_horner", tout << "callback n = " << n << "\ni="; m_intervals.display(tout, i) << "\n";);
conflict = ivs.check_interval_for_conflict_on_zero(i);
conflict = m_intervals.check_interval_for_conflict_on_zero(i);
m_intervals.reset(); // clean the memory allocated by the interval bound dependencies
return conflict;
},
[this](unsigned j) { return c().var_is_fixed(j); }
@ -145,12 +144,12 @@ template <typename T> nex horner::create_sum_from_row(const T& row) {
void horner::set_interval_for_scalar(interv& a, const rational& v) {
m_intervals->set_lower(a, v);
m_intervals->set_upper(a, v);
m_intervals->set_lower_is_open(a, false);
m_intervals->set_lower_is_inf(a, false);
m_intervals->set_upper_is_open(a, false);
m_intervals->set_upper_is_inf(a, false);
m_intervals.set_lower(a, v);
m_intervals.set_upper(a, v);
m_intervals.set_lower_is_open(a, false);
m_intervals.set_lower_is_inf(a, false);
m_intervals.set_upper_is_open(a, false);
m_intervals.set_upper_is_inf(a, false);
}
interv horner::interval_of_expr(const nex& e) {
@ -176,33 +175,33 @@ interv horner::interval_of_mul(const nex& e) {
SASSERT(e.is_mul());
auto & es = e.children();
interv a = interval_of_expr(es[0]);
if (m_intervals->is_zero(a)) {
m_intervals->set_zero_interval_deps_for_mult(a);
TRACE("nla_horner_details", tout << "es[0]= "<< es[0] << std::endl << "a = "; m_intervals->display(tout, a); );
if (m_intervals.is_zero(a)) {
m_intervals.set_zero_interval_deps_for_mult(a);
TRACE("nla_horner_details", tout << "es[0]= "<< es[0] << std::endl << "a = "; m_intervals.display(tout, a); );
return a;
}
TRACE("nla_horner_details", tout << "es[0]= "<< es[0] << std::endl << "a = "; m_intervals->display(tout, a); );
TRACE("nla_horner_details", tout << "es[0]= "<< es[0] << std::endl << "a = "; m_intervals.display(tout, a); );
for (unsigned k = 1; k < es.size(); k++) {
interv b = interval_of_expr(es[k]);
if (m_intervals->is_zero(b)) {
m_intervals->set_zero_interval_deps_for_mult(b);
TRACE("nla_horner_details", tout << "es[k]= "<< es[k] << std::endl << ", "; m_intervals->display(tout, b); );
if (m_intervals.is_zero(b)) {
m_intervals.set_zero_interval_deps_for_mult(b);
TRACE("nla_horner_details", tout << "es[k]= "<< es[k] << std::endl << ", "; m_intervals.display(tout, b); );
TRACE("nla_horner_details", tout << "got zero\n"; );
return b;
}
TRACE("nla_horner_details", tout << "es[" << k << "] "<< es[k] << ", "; m_intervals->display(tout, b); );
TRACE("nla_horner_details", tout << "es[" << k << "] "<< es[k] << ", "; m_intervals.display(tout, b); );
interv c;
interval_deps_combine_rule comb_rule;
m_intervals->mul(a, b, c, comb_rule);
TRACE("nla_horner_details", tout << "c before combine_deps() "; m_intervals->display(tout, c););
m_intervals->combine_deps(a, b, comb_rule, c);
TRACE("nla_horner_details", tout << "a "; m_intervals->display(tout, a););
TRACE("nla_horner_details", tout << "c "; m_intervals->display(tout, c););
m_intervals->set(a, c);
TRACE("nla_horner_details", tout << "part mult "; m_intervals->display(tout, a););
m_intervals.mul(a, b, c, comb_rule);
TRACE("nla_horner_details", tout << "c before combine_deps() "; m_intervals.display(tout, c););
m_intervals.combine_deps(a, b, comb_rule, c);
TRACE("nla_horner_details", tout << "a "; m_intervals.display(tout, a););
TRACE("nla_horner_details", tout << "c "; m_intervals.display(tout, c););
m_intervals.set(a, c);
TRACE("nla_horner_details", tout << "part mult "; m_intervals.display(tout, a););
}
TRACE("nla_horner_details", tout << "e=" << e << "\n";
tout << " return "; m_intervals->display(tout, a););
tout << " return "; m_intervals.display(tout, a););
return a;
}
@ -307,34 +306,34 @@ lpvar horner::find_term_column(const nex& e, rational& a, rational& b) const {
interv horner::interval_of_sum_no_terms(const nex& e) {
auto & es = e.children();
interv a = interval_of_expr(es[0]);
if (m_intervals->is_inf(a)) {
if (m_intervals.is_inf(a)) {
TRACE("nla_horner_details", tout << "e=" << e << "\n";
tout << " interv = "; m_intervals->display(tout, a););
tout << " interv = "; m_intervals.display(tout, a););
return a;
}
for (unsigned k = 1; k < es.size(); k++) {
TRACE("nla_horner_details_sum", tout << "es[" << k << "]= " << es[k] << "\n";);
interv b = interval_of_expr(es[k]);
if (m_intervals->is_inf(b)) {
if (m_intervals.is_inf(b)) {
TRACE("nla_horner_details", tout << "got inf\n";);
return b;
}
interv c;
interval_deps_combine_rule combine_rule;
TRACE("nla_horner_details_sum", tout << "a = "; m_intervals->display(tout, a) << "\nb = "; m_intervals->display(tout, b) << "\n";);
m_intervals->add(a, b, c, combine_rule);
m_intervals->combine_deps(a, b, combine_rule, c);
m_intervals->set(a, c);
TRACE("nla_horner_details_sum", tout << "a = "; m_intervals.display(tout, a) << "\nb = "; m_intervals.display(tout, b) << "\n";);
m_intervals.add(a, b, c, combine_rule);
m_intervals.combine_deps(a, b, combine_rule, c);
m_intervals.set(a, c);
TRACE("nla_horner_details_sum", tout << es[k] << ", ";
m_intervals->display(tout, a); tout << "\n";);
if (m_intervals->is_inf(a)) {
m_intervals.display(tout, a); tout << "\n";);
if (m_intervals.is_inf(a)) {
TRACE("nla_horner_details", tout << "got infinity\n";);
return a;
}
}
TRACE("nla_horner_details", tout << "e=" << e << "\n";
tout << " interv = "; m_intervals->display(tout, a););
tout << " interv = "; m_intervals.display(tout, a););
return a;
}
@ -347,14 +346,14 @@ bool horner::interval_from_term(const nex& e, interv & i) const {
set_var_interval(j, i);
interv bi;
m_intervals->mul(a, i, bi);
m_intervals->add(b, bi);
m_intervals->set(i, bi);
m_intervals.mul(a, i, bi);
m_intervals.add(b, bi);
m_intervals.set(i, bi);
TRACE("nla_horner",
c().m_lar_solver.print_column_info(j, tout) << "\n";
tout << "a=" << a << ", b=" << b << "\n";
tout << e << ", interval = "; m_intervals->display(tout, i););
tout << e << ", interval = "; m_intervals.display(tout, i););
return true;
}
@ -366,9 +365,9 @@ interv horner::interval_of_sum(const nex& e) {
if (e.sum_is_a_linear_term()) {
interv i_from_term ;
if (interval_from_term(e, i_from_term)) {
interv r = m_intervals->intersect(i_e, i_from_term);
TRACE("nla_horner_details", tout << "intersection="; m_intervals->display(tout, r) << "\n";);
if (m_intervals->is_empty(r)) {
interv r = m_intervals.intersect(i_e, i_from_term);
TRACE("nla_horner_details", tout << "intersection="; m_intervals.display(tout, r) << "\n";);
if (m_intervals.is_empty(r)) {
SASSERT(false); // not implemented
}
return r;
@ -380,8 +379,8 @@ interv horner::interval_of_sum(const nex& e) {
// sets the dependencies also
void horner::set_var_interval(lpvar v, interv& b) const{
m_intervals->set_var_interval_with_deps(v, b);
TRACE("nla_horner_details_var", tout << "v = "; print_var(v, tout) << "\n"; m_intervals->display(tout, b););
m_intervals.set_var_interval_with_deps(v, b);
TRACE("nla_horner_details_var", tout << "v = "; print_var(v, tout) << "\n"; m_intervals.display(tout, b););
}

5
src/math/lp/horner.h
View file

@ -28,13 +28,10 @@ class core;
class horner : common {
intervals *m_intervals;
intervals m_intervals;
public:
typedef nla_expr<rational> nex;
typedef intervals::interval interv;
void set_intervals( intervals * i) {
m_intervals = i;
}
horner(core *core);
void horner_lemmas();
template <typename T> // T has an iterator of (coeff(), var())

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

@ -19,7 +19,7 @@
--*/
#pragma once
#include "util/dependency.h"
#include "util/small_object_allocator.h"
#include "util/region.h"
#include "math/lp/nla_common.h"
#include "math/lp/lar_solver.h"
#include "math/interval/interval.h"
@ -40,7 +40,7 @@ class intervals : common {
struct ci_dependency_config {
typedef ci_value_manager value_manager;
typedef small_object_allocator allocator;
typedef region allocator;
static const bool ref_count = false;
typedef lp::constraint_index value;
};
@ -135,13 +135,13 @@ class intervals : common {
}
};
small_object_allocator m_alloc;
ci_value_manager m_val_manager;
region m_alloc;
ci_value_manager m_val_manager;
mutable unsynch_mpq_manager m_num_manager;
mutable ci_dependency_manager m_dep_manager;
im_config m_config;
mutable interval_manager<im_config> m_imanager;
region m_region;
region m_region;
public:
typedef interval_manager<im_config>::interval interval;
@ -153,7 +153,7 @@ private:
public:
intervals(core* c, reslimit& lim) :
common(c),
m_alloc("intervals"),
m_alloc(),
m_dep_manager(m_val_manager, m_alloc),
m_config(m_num_manager, m_dep_manager),
m_imanager(lim, im_config(m_num_manager, m_dep_manager))
@ -319,6 +319,6 @@ public:
return true;
return false;
}
void reset() { m_alloc.reset(); }
}; // end of intervals
} // end of namespace nla