mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

progress with horner's heuristic

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-07-03 14:30:36 -07:00
parent 7f9d57e6fa
commit 2181c982e8
7 changed files with 73 additions and 36 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -41,8 +41,9 @@ void horner::lemma_on_row(const T& row) {
return;
nex e = create_expr_from_row(row);
TRACE("nla_cn", tout << "cross nested e = " << e << std::endl;);
intervals::interval inter = interval_of_expr(e);
check_interval_for_conflict(inter);
intervals::interval a = interval_of_expr(e);
TRACE("nla_cn", tout << "interval a = "; m_intervals.display(tout, a) << "\n";);
check_interval_for_conflict(a, row);
}
void horner::horner_lemmas() {
@ -120,7 +121,7 @@ unsigned horner::random_most_occured_var(std::unordered_map<lpvar, unsigned>& oc
// j -> the number of expressions j appears in
void horner::get_occurences_map(const nla_expr<rational>& e, std::unordered_map<lpvar, unsigned>& occurences) const {
TRACE("nla_cn", tout << "e = " << e << std::endl;);
TRACE("nla_cn_details", tout << "e = " << e << std::endl;);
SASSERT(e.type() == expr_type::SUM);
for (const auto & ce : e.children()) {
std::unordered_set<lpvar> seen;
@ -183,7 +184,6 @@ nex horner::split_with_var(const nex& e, lpvar j) {
}
nex horner::cross_nested_of_sum(const nex& e) {
TRACE("nla_cn", );
if (!e.is_sum())
return e;
std::unordered_map<lpvar, unsigned> occurences;
@ -218,19 +218,22 @@ template <typename T> nex horner::create_expr_from_row(const T& row) {
return e;
}
template <typename T>
void horner::set_interval_for_scalar(interv& a, const T& 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);
}
intervals::interval horner::interval_of_expr(const nex& e) {
TRACE("nla_cn", tout << e.type() << " e=" << e << std::endl;);
TRACE("nla_cn_details", tout << e.type() << " e=" << e << std::endl;);
interv a;
switch (e.type()) {
case expr_type::SCALAR:
m_intervals.set_lower(a, e.value());
m_intervals.set_upper(a, e.value());
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);
TRACE("nla_cn", tout << "e.value() = " << e.value() << "\n"; m_intervals.display(tout, a) << '\n';);
set_interval_for_scalar(a, e.value());
return a;
case expr_type::SUM:
return interval_of_sum(e.children());
@ -238,7 +241,6 @@ intervals::interval horner::interval_of_expr(const nex& e) {
return interval_of_mul(e.children());
case expr_type::VAR:
set_var_interval(e.var(), a);
TRACE("nla_cn", tout << "a = "; m_intervals.display(tout, a) << "\n";);
return a;
default:
TRACE("nla_cn", tout << e.type() << "\n";);
@ -250,14 +252,14 @@ template <typename T>
interv horner::interval_of_mul(const vector<nla_expr<T>>& es) {
interv a = interval_of_expr(es[0]);
if (m_intervals.is_zero(a)) {
TRACE("nla_cn", tout << "got zero\n";);
TRACE("nla_cn", m_intervals.display(tout, a) << "\ngot zero for " << es[0] << "\n";);
return a;
}
TRACE("nla_cn", tout << "es[0]= "<< es[0] << std::endl << "a = "; m_intervals.display(tout, a); tout << "\n";);
for (unsigned k = 1; k < es.size(); k++) {
interv b = interval_of_expr(es[k]);
if (m_intervals.is_zero(b)) {
TRACE("nla_cn", tout << "got zero\n";);
TRACE("nla_cn", m_intervals.display(tout, b) << "\ngot zero for " << es[k] << "\n";);
return b;
}
interv c;
@ -265,21 +267,24 @@ interv horner::interval_of_mul(const vector<nla_expr<T>>& es) {
m_intervals.mul(a, b, c, deps);
m_intervals.set(a, c);
m_intervals.add_deps(a, b, deps, a);
TRACE("nla_cn", tout << "a = "; m_intervals.display(tout, a); tout << "\n";);
}
TRACE("nla_cn",
for (const auto &e : es) tout << e;
tout << " interv a = ";
m_intervals.display(tout, a) << "\n";);
return a;
}
template <typename T>
interv horner::interval_of_sum(const vector<nla_expr<T>>& es) {
interv a = interval_of_expr(es[0]);
TRACE("nla_cn", tout << "es[0]= " << es[0] << "\n"; m_intervals.display(tout, a) << "\n";);
TRACE("nla_cn_details", tout << "es[0]= " << es[0] << "\n"; m_intervals.display(tout, a) << "\n";);
if (m_intervals.is_inf(a)) {
return a;
}
for (unsigned k = 1; k < es.size(); k++) {
TRACE("nla_cn", tout << "es[" << k << "]= " << es[k] << "\n";);
TRACE("nla_cn_details", tout << "es[" << k << "]= " << es[k] << "\n";);
interv b = interval_of_expr(es[k]);
if (m_intervals.is_inf(b)) {
TRACE("nla_cn", tout << "got inf\n";);
@ -290,9 +295,9 @@ interv horner::interval_of_sum(const vector<nla_expr<T>>& es) {
m_intervals.add(a, b, c, deps);
m_intervals.set(a, c);
m_intervals.add_deps(a, b, deps, a);
TRACE("nla_cn", tout << "interv = "; m_intervals.display(tout, a); tout << "\n";);
TRACE("nla_cn_details", tout << "interv = "; m_intervals.display(tout, a); tout << "\n";);
if (m_intervals.is_inf(a)) {
TRACE("nla_cn", tout << "got infinity\n";);
TRACE("nla_cn_details", tout << "got infinity\n";);
return a;
}
}
@ -301,11 +306,16 @@ interv horner::interval_of_sum(const vector<nla_expr<T>>& es) {
// sets the dependencies also
void horner::set_var_interval(lpvar v, interv& b) {
m_intervals.set_var_interval_with_deps(v, b);
TRACE("nla_cn", tout << "v = "; print_var(v, tout); tout << "\n";);
TRACE("nla_cn", tout << "v = "; print_var(v, tout) << "\n"; m_intervals.display(tout, b)<< '\n';);
}
void horner::check_interval_for_conflict(const intervals::interval& i) {
m_intervals.check_interval_for_conflict_on_zero(i);
template <typename T>
void horner::check_interval_for_conflict(const intervals::interval& i, const T& row) {
if (m_intervals.check_interval_for_conflict_on_zero(i)) {
TRACE("nla_cn", print_lemma(tout););
} else {
TRACE("nla_cn", tout << "no lemma\n";);
}
}
}

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

@ -35,11 +35,11 @@ public:
void horner_lemmas();
template <typename T> // T has an iterator of (coeff(), var())
void lemma_on_row(const T&);
template <typename T>
bool row_is_interesting(const T&) const;
template <typename T> bool row_is_interesting(const T&) const;
template <typename T> nla_expr<rational> create_expr_from_row(const T&);
intervals::interval interval_of_expr(const nla_expr<rational>& e);
void check_interval_for_conflict(const intervals::interval&);
template <typename T> void check_interval_for_conflict(const intervals::interval&, const T&);
bool check_interval_for_conflict_lower_bound(const intervals::interval&);
bool check_interval_for_conflict_upper_bound(const intervals::interval&);
nla_expr<rational> nexvar(lpvar j) const;
@ -53,5 +53,7 @@ public:
intervals::interval interval_of_sum(const vector<nla_expr<T>>&);
template <typename T>
intervals::interval interval_of_mul(const vector<nla_expr<T>>&);
template <typename T>
void set_interval_for_scalar(intervals::interval&, const T&);
}; // end of horner
}

7
src/math/lp/lar_solver.h
View file

@ -607,7 +607,12 @@ public:
}
std::ostream& print_column_info(unsigned j, std::ostream& out) const {
return m_mpq_lar_core_solver.m_r_solver.print_column_info(j, out);
m_mpq_lar_core_solver.m_r_solver.print_column_info(j, out);
if( !column_corresponds_to_term(j))
return out;
const lar_term& t = * m_terms[m_var_register.local_to_external(j) - m_terms_start_index];
print_term_as_indices(t, out) << "\n";
return out;
}
bool has_int_var() const;

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

@ -433,6 +433,14 @@ void core::mk_ineq(lp::lar_term& t, llc cmp, const rational& rs) {
}
}
void core::mk_ineq_no_expl_check(lp::lar_term& t, llc cmp, const rational& rs) {
TRACE("nla_solver_details", m_lar_solver.print_term_as_indices(t, tout << "t = "););
m_lar_solver.subs_term_columns(t);
current_lemma().push_back(ineq(cmp, t, rs));
CTRACE("nla_solver", ineq_holds(ineq(cmp, t, rs)), print_ineq(ineq(cmp, t, rs), tout) << "\n";);
SASSERT(!ineq_holds(ineq(cmp, t, rs)));
}
void core::mk_ineq(const rational& a, lpvar j, const rational& b, lpvar k, llc cmp, const rational& rs) {
lp::lar_term t;
t.add_coeff_var(a, j);
@ -1246,7 +1254,7 @@ lbool core:: inner_check(bool derived) {
return l_false;
}
TRACE("nla_cn", print_terms(tout););
TRACE("nla_cn_details", print_terms(tout););
for (int search_level = 0; search_level < 3 && !done(); search_level++) {
TRACE("nla_solver", tout << "derived = " << derived << ", search_level = " << search_level << "\n";);
if (search_level == 0) {

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

@ -201,6 +201,7 @@ public:
void mk_ineq(lp::lar_term& t, llc cmp, const rational& rs);
void mk_ineq_no_expl_check(lp::lar_term& t, llc cmp, const rational& rs);
void mk_ineq(const rational& a, lpvar j, const rational& b, lpvar k, llc cmp, const rational& rs);
void mk_ineq(bool a, lpvar j, bool b, lpvar k, llc cmp, const rational& rs);
void mk_ineq(bool a, lpvar j, bool b, lpvar k, llc cmp);

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

@ -75,10 +75,8 @@ void intervals::set_var_interval_with_deps(lpvar v, interval& b) {
}
}
void intervals::check_interval_for_conflict_on_zero(const interval & i) {
if (check_interval_for_conflict_on_zero_lower(i))
return;
check_interval_for_conflict_on_zero_upper(i);
bool intervals::check_interval_for_conflict_on_zero(const interval & i) {
return check_interval_for_conflict_on_zero_lower(i) || check_interval_for_conflict_on_zero_upper(i);
}
bool intervals::check_interval_for_conflict_on_zero_upper(const interval & i) {
@ -98,7 +96,7 @@ bool intervals::check_interval_for_conflict_on_zero_upper(const interval & i) {
bool intervals::check_interval_for_conflict_on_zero_lower(const interval & i) {
if (lower_is_inf(i))
return false;
if (unsynch_mpq_manager::is_pos(lower(i)))
if (unsynch_mpq_manager::is_neg(lower(i)))
return false;
if (unsynch_mpq_manager::is_zero(lower(i)) && !m_config.lower_is_open(i))
return false;
@ -126,6 +124,19 @@ std::ostream& intervals::display(std::ostream& out, const interval& i) const {
} else {
out << rational(m_imanager.upper(i)) << (m_imanager.lower_is_open(i)? ")":"]");
}
svector<lp::constraint_index> expl;
m_dep_manager.linearize(i.m_lower_dep, expl);
out << "\nlower constraints (\n";
for (lp::constraint_index c: expl)
m_core->m_lar_solver.print_constraint_indices_only(c, out);
out << ")\n";
expl.clear();
m_dep_manager.linearize(i.m_upper_dep, expl);
out << "upper constraints (\n";
for (lp::constraint_index c: expl)
m_core->m_lar_solver.print_constraint_indices_only(c, out);
out << ")\n";
return out;
}

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

@ -193,7 +193,7 @@ public:
bool lower_is_inf(const interval& a) const { return m_config.lower_is_inf(a); }
void set_var_interval_with_deps(lpvar, interval &);
bool is_inf(const interval& i) const { return m_config.is_inf(i); }
void check_interval_for_conflict_on_zero(const interval & i);
bool check_interval_for_conflict_on_zero(const interval & i);
bool check_interval_for_conflict_on_zero_lower(const interval & i);
bool check_interval_for_conflict_on_zero_upper(const interval & i);
mpq const & lower(interval const & a) const { return m_config.lower(a); }