mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Code Activity

fixes in nex expressions simplifications

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-10-18 14:24:20 -07:00
parent 7fbf3e0707
commit 64b189d932
6 changed files with 207 additions and 45 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -99,6 +99,9 @@ bool horner::lemmas_on_row(const T& row) {
create_sum_from_row(row, cn.get_nex_creator(), m_row_sum, m_fixed_var_constraints_for_row);
set_active_vars_weights(); // without this call the comparisons will be incorrect
nex* e = m_nex_creator.simplify(&m_row_sum);
TRACE("nla_horner", tout << "e = " << * e << "\n";);
if (e->get_degree() < 2)
return false;
if (!e->is_sum())
return false;

20
src/math/lp/nex.h
View file

@ -162,6 +162,13 @@ public:
friend std::ostream& operator<<(std::ostream& out, const nex_pow & p) { out << p.to_string(); return out; }
};
inline unsigned get_degree_children(const vector<nex_pow>& children) {
int degree = 0;
for (const auto& p : children) {
degree += p.e()->get_degree() * p.pow();
}
return degree;
}
class nex_mul : public nex {
rational m_coeff;
@ -169,6 +176,9 @@ class nex_mul : public nex {
public:
nex_mul() : m_coeff(rational(1)) {}
template <typename T>
nex_mul() : m_coeff() {}
const rational& coeff() const {
return m_coeff;
}
@ -258,13 +268,9 @@ public:
}
int get_degree() const {
int degree = 0;
for (const auto& p : *this) {
degree += p.e()->get_degree() * p.pow();
}
return degree;
}
return get_degree_children(children());
}
bool is_linear() const {
return get_degree() < 2; // todo: make it more efficient
}

153
src/math/lp/nex_creator.cpp
View file

@ -114,8 +114,69 @@ void nex_creator::simplify_children_of_mul(vector<nex_pow> & children, rational&
TRACE("nla_cn_details", print_vector(children, tout););
}
bool nex_creator:: less_than_on_powers_mul_same_degree(const vector<nex_pow>& a, const nex_mul* b) const {
bool inside_a_p = false; // inside_a_p is true means we still compare the old position of it_a
bool inside_b_p = false; // inside_b_p is true means we still compare the old position of it_b
auto it_a = a.begin();
auto it_b = b->begin();
auto a_end = a.end();
auto b_end = b->end();
unsigned a_pow, b_pow;
int ret = - 1;
do {
if (!inside_a_p) { a_pow = it_a->pow(); }
if (!inside_b_p) { b_pow = it_b->pow(); }
if (lt(it_a->e(), it_b->e())){
ret = true;
break;
}
if (lt(it_b->e(), it_a->e())) {
ret = false;
break;
}
bool nex_creator::less_than_on_mul_mul_same_degree_iterate(const nex_mul* a, const nex_mul* b) const {
if (a_pow == b_pow) {
inside_a_p = inside_b_p = false;
it_a++; it_b++;
if (it_a == a_end) {
ret = false;
break;
}
if (it_b == b_end) { // it_a is not at the end
ret = false;
break;
}
// no iterator reached the end
continue;
}
if (a_pow > b_pow) {
it_a++;
if (it_a == a_end) {
ret = true;
break;
}
inside_a_p = false;
inside_b_p = true;
b_pow -= a_pow;
} else {
SASSERT(a_pow < b_pow);
a_pow -= b_pow;
it_b++;
if (it_b == b_end) {
ret = false;
break;
}
inside_a_p = true;
inside_b_p = false;
}
} while (true);
if (ret == -1)
ret = true;
TRACE("nla_cn_details", tout << "a = "; print_vector(a, tout) << (ret == 1?" < ":" >= ") << *b << "\n";);
return ret;
}
bool nex_creator::less_than_on_mul_mul_same_degree(const nex_mul* a, const nex_mul* b) const {
bool inside_a_p = false; // inside_a_p is true means we still compare the old position of it_a
bool inside_b_p = false; // inside_b_p is true means we still compare the old position of it_b
auto it_a = a->begin();
@ -182,11 +243,29 @@ bool nex_creator::less_than_on_mul_mul_same_degree_iterate(const nex_mul* a, con
return ret;
}
bool nex_creator::less_than_on_mul_mul_same_degree(const nex_mul* a, const nex_mul* b) const {
SASSERT(a->get_degree() == b->get_degree());
SASSERT(a->size() && b->size());
return less_than_on_mul_mul_same_degree_iterate(a, b);
bool nex_creator::children_are_simplified(const vector<nex_pow>& children) const {
for (auto c : children)
if (!is_simplified(c.e()) || c.pow() == 0)
return false;
return true;
}
bool nex_creator::less_than_on_powers_mul(const vector<nex_pow>& children, const nex_mul* b) const {
TRACE("nla_cn_details", tout << "children = "; print_vector(children, tout) << " , b = " << *b << "\n";);
SASSERT(children_are_simplified(children) && is_simplified(b));
unsigned a_deg = get_degree_children(children);
unsigned b_deg = b->get_degree();
bool ret;
if (a_deg > b_deg) {
ret = true;
} else if (a_deg < b_deg) {
ret = false;
} else {
ret = less_than_on_powers_mul_same_degree(children, b);
}
return ret;
}
bool nex_creator::less_than_on_mul_mul(const nex_mul* a, const nex_mul* b) const {
TRACE("nla_cn_details", tout << "a = " << *a << " , b = " << *b << "\n";);
@ -230,6 +309,30 @@ bool nex_creator::less_than_on_var_nex(const nex_var* a, const nex* b) const {
}
}
bool nex_creator::lt_nex_powers(const vector<nex_pow>& children, const nex* b) const {
switch(b->type()) {
case expr_type::SCALAR: return false;
case expr_type::VAR:
{
if (get_degree_children(children) > 1)
return true;
auto it = children.begin();
const nex_pow & c = *it;
SASSERT(c.pow() == 1);
const nex * f = c.e();
SASSERT(!f->is_scalar());
return lt(f, b);
}
case expr_type::MUL:
return less_than_on_powers_mul(children, to_mul(b));
case expr_type::SUM:
return lt_nex_powers(children, (*to_sum(b))[0]);
default:
UNREACHABLE();
return false;
}
}
bool nex_creator::less_than_on_mul_nex(const nex_mul* a, const nex* b) const {
switch(b->type()) {
@ -267,6 +370,40 @@ bool nex_creator::less_than_on_sum_sum(const nex_sum* a, const nex_sum* b) const
}
// the only difference with lt() that it disregards the coefficient in nex_mul
bool nex_creator::lt_for_sort_join_sum(const nex* a, const nex* b) const {
TRACE("nla_cn_details_", tout << *a << " ? " << *b << "\n";);
if (a == b)
return false;
bool ret;
switch (a->type()) {
case expr_type::VAR:
ret = less_than_on_var_nex(to_var(a), b);
break;
case expr_type::SCALAR: {
if (b->is_scalar())
ret = to_scalar(a)->value() > to_scalar(b)->value();
else
ret = false; // the scalars are the largest
break;
}
case expr_type::MUL: {
ret = lt_nex_powers(to_mul(a)->children(), b);
break;
}
case expr_type::SUM: {
if (b->is_sum())
return less_than_on_sum_sum(to_sum(a), to_sum(b));
return lt((*to_sum(a))[0], b);
}
default:
UNREACHABLE();
return false;
}
TRACE("nla_cn_details_", tout << *a << (ret?" < ":" >= ") << *b << "\n";);
return ret;
}
bool nex_creator::lt(const nex* a, const nex* b) const {
TRACE("nla_cn_details_", tout << *a << " ? " << *b << "\n";);
if (a == b)
@ -296,11 +433,8 @@ bool nex_creator::lt(const nex* a, const nex* b) const {
UNREACHABLE();
return false;
}
TRACE("nla_cn_details_", tout << *a << (ret?" < ":" >= ") << *b << "\n";);
return ret;
}
bool nex_creator::is_sorted(const nex_mul* e) const {
@ -513,7 +647,7 @@ bool nex_creator::fill_join_map_for_sum(ptr_vector<nex> & children,
void nex_creator::sort_join_sum(ptr_vector<nex> & children) {
TRACE("nla_cn_details", print_vector_of_ptrs(children, tout););
std::map<nex*, rational, nex_lt> map([this](const nex *a , const nex *b)
{ return lt(a, b); });
{ return lt_for_sort_join_sum(a, b); });
std::unordered_set<nex*> existing_nex; // handling (nex*) as numbers
nex_scalar * common_scalar;
fill_join_map_for_sum(children, map, existing_nex, common_scalar);
@ -526,6 +660,7 @@ void nex_creator::sort_join_sum(ptr_vector<nex> & children) {
for (auto& p : map) {
process_map_pair(p.first, p.second, children, existing_nex);
}
TRACE("nla_cn_details", for (auto & p : map ) { tout << "(" << *p.first << ", " << p.second << ") ";});
}
bool is_zero_scalar(nex *e) {

6
src/math/lp/nex_creator.h
View file

@ -250,10 +250,14 @@ public:
bool eat_scalar_pow(rational& r, const nex_pow& p, unsigned);
void simplify_children_of_mul(vector<nex_pow> & children, lt_on_vars lt, std::function<nex_scalar*()> mk_scalar);
bool children_are_simplified(const vector<nex_pow>& children) const;
bool lt(const nex* a, const nex* b) const;
bool lt_nex_powers(const vector<nex_pow>&, const nex* b) const;
bool less_than_on_powers_mul(const vector<nex_pow>&, const nex_mul* b) const;
bool less_than_on_powers_mul_same_degree(const vector<nex_pow>&, const nex_mul* b) const;
bool lt_for_sort_join_sum(const nex* a, const nex* b) const;
bool less_than_on_mul_mul(const nex_mul* a, const nex_mul* b) const;
bool less_than_on_mul_mul_same_degree(const nex_mul* a, const nex_mul* b) const;
bool less_than_on_mul_mul_same_degree_iterate(const nex_mul* a, const nex_mul* b) const;
bool less_than_on_var_nex(const nex_var* a, const nex* b) const;
bool less_than_on_mul_nex(const nex_mul* a, const nex* b) const;
bool less_than_on_sum_sum(const nex_sum* a, const nex_sum* b) const;

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

@ -124,22 +124,6 @@ unsigned common::random() {
// it also inserts variables into m_active_vars
// and updates fixed_var_deps
nex * common::nexvar(lpvar j, nex_creator& cn, svector<lp::constraint_index> & fixed_vars_constraints) {
// todo: consider deepen the recursion
if (!c().is_monic_var(j)) {
c().insert_to_active_var_set(j);
return cn.mk_var(j);
}
const monic& m = c().emons()[j];
nex_mul * e = cn.mk_mul();
for (lpvar k : m.vars()) {
c().insert_to_active_var_set(k);
e->add_child(cn.mk_var(k));
CTRACE("nla_horner", c().is_monic_var(k), c().print_var(k, tout) << "\n";);
}
return e;
}
nex * common::nexvar(const rational & coeff, lpvar j, nex_creator& cn,
svector<lp::constraint_index> & fixed_vars_constraints) {
if (!c().is_monic_var(j)) {
@ -148,7 +132,7 @@ nex * common::nexvar(const rational & coeff, lpvar j, nex_creator& cn,
c().m_lar_solver.get_bound_constraint_witnesses_for_column(j, lc, uc);
fixed_vars_constraints.push_back(lc);
fixed_vars_constraints.push_back(uc);
return cn.mk_scalar(c().m_lar_solver.get_lower_bound(j).x);
return cn.mk_scalar(coeff * c().m_lar_solver.get_lower_bound(j).x);
}
c().insert_to_active_var_set(j);
return cn.mk_mul(cn.mk_scalar(coeff), cn.mk_var(j));
@ -156,15 +140,15 @@ nex * common::nexvar(const rational & coeff, lpvar j, nex_creator& cn,
const monic& m = c().emons()[j];
nex_mul * e = cn.mk_mul(cn.mk_scalar(coeff));
for (lpvar k : m.vars()) {
if (c().var_is_fixed(j)) {
if (c().var_is_fixed(k)) {
lp::constraint_index lc,uc;
c().m_lar_solver.get_bound_constraint_witnesses_for_column(j, lc, uc);
c().m_lar_solver.get_bound_constraint_witnesses_for_column(k, lc, uc);
fixed_vars_constraints.push_back(lc);
fixed_vars_constraints.push_back(uc);
e->coeff() *= c().m_lar_solver.get_lower_bound(j).x;
e->coeff() *= c().m_lar_solver.get_lower_bound(k).x;
continue;
}
c().insert_to_active_var_set(j);
c().insert_to_active_var_set(k);
e->add_child(cn.mk_var(k));
CTRACE("nla_horner", c().is_monic_var(k), c().print_var(k, tout) << "\n";);
}
@ -181,14 +165,40 @@ template <typename T> void common::create_sum_from_row(const T& row, nex_creator
SASSERT(row.size() > 1);
sum.children().clear();
for (const auto &p : row) {
if (p.coeff().is_one()) {
nex* e = nexvar(p.var(), cn, fixed_vars_constraints);
sum.add_child(e);
} else {
nex* e = nexvar(p.coeff(), p.var(), cn, fixed_vars_constraints);
sum.add_child(e);
nex* e = nexvar(p.coeff(), p.var(), cn, fixed_vars_constraints);
sum.add_child(e);
}
TRACE("nla_horner", tout << "sum =" << sum << "\n";);
}
template <typename T>
common::ci_dependency* common::get_fixed_vars_dep_from_row(const T& row, ci_dependency_manager& dep_manager) {
TRACE("nla_horner", tout << "row="; m_core->print_term(row, tout) << "\n";);
ci_dependency* dep = nullptr;
for (const auto &p : row) {
lpvar j = p.var();
if (!c().is_monic_var(j)) {
if (c().var_is_fixed(j)) {
lp::constraint_index lc,uc;
c().m_lar_solver.get_bound_constraint_witnesses_for_column(j, lc, uc);
dep = dep_manager.mk_join(dep, dep_manager.mk_leaf(lc));
dep = dep_manager.mk_join(dep, dep_manager.mk_leaf(uc));
} else {
const monic& m = c().emons()[j];
for (lpvar k : m.vars()) {
if (!c().var_is_fixed(k))
continue;
lp::constraint_index lc,uc;
c().m_lar_solver.get_bound_constraint_witnesses_for_column(k, lc, uc);
c().m_lar_solver.get_bound_constraint_witnesses_for_column(k, lc, uc);
dep = dep_manager.mk_join(dep, dep_manager.mk_leaf(lc));
dep = dep_manager.mk_join(dep, dep_manager.mk_leaf(uc));
}
}
}
}
return dep;
}
void common::set_active_vars_weights() {
@ -198,6 +208,8 @@ void common::set_active_vars_weights() {
}
}
var_weight common::get_var_weight(lpvar j) const {
var_weight k;
switch (c().m_lar_solver.get_column_type(j)) {

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

@ -117,11 +117,13 @@ struct common {
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&, svector<lp::constraint_index> & fixed_vars_constraints);
template <typename T>
void create_sum_from_row(const T&, nex_creator&, nex_sum&,
svector<lp::constraint_index> & fixed_vars_constraints);
template <typename T>
ci_dependency* get_fixed_vars_dep_from_row(const T&, ci_dependency_manager& dep_manager);
void set_active_vars_weights();
var_weight get_var_weight(lpvar) const;
};