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

init of m_active_vars_weights and fixes in is_simplified

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-10-07 16:19:28 -07:00
parent b2d1bcc8cd
commit 0c126031b0
12 changed files with 129 additions and 92 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/math/lp/cross_nested.h
View file

@ -34,8 +34,8 @@ class cross_nested {
ptr_vector<nex> m_b_split_vec;
int m_reported;
bool m_random_bit;
nex_creator m_nex_creator;
std::function<nex_scalar*()> m_mk_scalar;
nex_creator& m_nex_creator;
#ifdef Z3DEBUG
nex* m_e_clone;
#endif
@ -45,13 +45,15 @@ public:
cross_nested(std::function<bool (const nex*)> call_on_result,
std::function<bool (unsigned)> var_is_fixed,
std::function<unsigned ()> random) :
std::function<unsigned ()> random,
nex_creator& nex_cr) :
m_call_on_result(call_on_result),
m_var_is_fixed(var_is_fixed),
m_random(random),
m_done(false),
m_reported(0),
m_mk_scalar([this]{return m_nex_creator.mk_scalar(rational(1));})
m_mk_scalar([this]{return m_nex_creator.mk_scalar(rational(1));}),
m_nex_creator(nex_cr)
{}
@ -369,15 +371,15 @@ public:
// all factors of j go to a, the rest to b
void pre_split(nex_sum * e, lpvar j, nex_sum*& a, nex*& b) {
TRACE("nla_cn_details", tout << "e = " << * e << ", j = " << m_nex_creator.ch(j) << std::endl;);
SASSERT(m_nex_creator.is_simplified(e));
a = m_nex_creator.mk_sum();
m_b_split_vec.clear();
for (nex * ce: *e) {
TRACE("nla_cn_details", tout << "ce = " << *ce << "\n";);
if (is_divisible_by_var(ce, j)) {
a->add_child(m_nex_creator.mk_div(ce , j));
} else {
m_b_split_vec.push_back(ce);
TRACE("nla_cn_details", tout << "ce = " << *ce << "\n";);
}
}
TRACE("nla_cn_details", tout << "a = " << *a << "\n";);

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

@ -45,7 +45,7 @@ bool horner::row_is_interesting(const T& row) const {
return false;
}
SASSERT(row_has_monomial_to_refine(row));
c().clear_row_var_set();
c().clear_active_var_set();
for (const auto& p : row) {
lpvar j = p.var();
if (!c().is_monic_var(j))
@ -53,19 +53,19 @@ bool horner::row_is_interesting(const T& row) const {
auto & m = c().emons()[j];
for (lpvar k : m.vars()) {
if (c().row_var_set_contains(k))
if (c().active_var_set_contains(k))
return true;
}
for (lpvar k : m.vars()) {
c().insert_to_row_var_set(k);
c().insert_to_active_var_set(k);
}
}
return false;
}
bool horner::lemmas_on_expr(cross_nested& cn) {
TRACE("nla_horner", tout << "m_row_sum = " << m_row_sum << "\n";);
cn.run(&m_row_sum);
bool horner::lemmas_on_expr(cross_nested& cn, nex_sum* e) {
TRACE("nla_horner", tout << "e = " << *e << "\n";);
cn.run(e);
return cn.done();
}
@ -92,11 +92,15 @@ bool horner::lemmas_on_row(const T& row) {
cross_nested cn(
[this](const nex* n) { return check_cross_nested_expr(n); },
[this](unsigned j) { return c().var_is_fixed(j); },
[this]() { return c().random(); });
[this]() { return c().random(); }, m_nex_creator);
SASSERT (row_is_interesting(row));
create_sum_from_row(row, cn.get_nex_creator(), m_row_sum);
return lemmas_on_expr(cn);
nex* e = m_nex_creator.simplify(&m_row_sum);
if (!e->is_sum())
return false;
return lemmas_on_expr(cn, to_sum(e));
}
void horner::horner_lemmas() {
@ -112,7 +116,7 @@ void horner::horner_lemmas() {
for (auto & s : matrix.m_columns[j])
rows_to_check.insert(s.var());
}
c().prepare_row_var_set();
c().prepare_active_var_set();
svector<unsigned> rows;
for (unsigned i : rows_to_check) {
if (row_is_interesting(matrix.m_rows[i]))

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

@ -53,7 +53,7 @@ public:
intervals::interval interval_of_sum_no_term_with_deps(const nex_sum*);
intervals::interval interval_of_mul_with_deps(const nex_mul*);
void set_var_interval_with_deps(lpvar j, intervals::interval&) const;
bool lemmas_on_expr(cross_nested&);
bool lemmas_on_expr(cross_nested&, nex_sum*);
template <typename T> // T has an iterator of (coeff(), var())
bool row_has_monomial_to_refine(const T&) const;

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

@ -97,7 +97,8 @@ public:
lpvar var() const { return m_j; }
lpvar& var() { return m_j; } // the setter
std::ostream & print(std::ostream& out) const {
out << (char)('a' + m_j);
// out << (char)('a' + m_j);
out << "v" << m_j;
return out;
}

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

@ -288,8 +288,12 @@ bool nex_creator::lt(const nex* a, const nex* b) const {
bool nex_creator::is_sorted(const nex_mul* e) const {
for (unsigned j = 0; j < e->size() - 1; j++) {
if (!(less_than_on_nex_pow((*e)[j], (*e)[j+1])))
if (!(less_than_on_nex_pow((*e)[j], (*e)[j+1]))) {
TRACE("nla_cn_details", tout << "not sorted e " << * e << "\norder is incorrect " <<
(*e)[j] << " >= " << (*e)[j + 1]<< "\n";);
return false;
}
}
return true;
}
@ -298,22 +302,29 @@ bool nex_creator::is_sorted(const nex_mul* e) const {
bool nex_creator::mul_is_simplified(const nex_mul* e) const {
TRACE("nla_cn_details", tout << "e = " << *e << "\n";);
if (e->size() == 1 && e->begin()->pow() == 1)
return false;
std::set<const nex*, nex_lt> s([this](const nex* a, const nex* b) {return lt(a, b); });
for (const auto &p : *e) {
const nex* ee = p.e();
if (p.pow() == 0)
if (p.pow() == 0) {
TRACE("nla_cn_details", tout << "not simplified " << *ee << "\n";);
return false;
if (ee->is_mul())
}
if (ee->is_mul()) {
TRACE("nla_cn_details", tout << "not simplified " << *ee << "\n";);
return false;
if (ee->is_scalar() && to_scalar(ee)->value().is_one())
}
if (ee->is_scalar() && to_scalar(ee)->value().is_one()) {
TRACE("nla_cn_details", tout << "not simplified " << *ee << "\n";);
return false;
}
auto it = s.find(ee);
if (it == s.end()) {
s.insert(ee);
} else {
} else {
TRACE("nla_cn_details", tout << "not simplified " << *ee << "\n";);
return false;
}
@ -340,20 +351,29 @@ nex* nex_creator::simplify_sum(nex_sum *e) {
}
bool nex_creator::sum_is_simplified(const nex_sum* e) const {
if (e->size() < 2) return false;
bool scalar = false;
for (nex * ee : *e) {
if (ee->is_sum())
if (ee->is_sum()) {
TRACE("nla_cn", tout << "not simplified e = " << *e << "\n"
<< " has a child which is a sum " << *ee << "\n";);
return false;
}
if (ee->is_scalar()) {
if (scalar) {
TRACE("nla_cn", tout << "not simplified e = " << *e << "\n"
<< " have more than one scalar " << *ee << "\n";);
return false;
}
if (to_scalar(ee)->value().is_zero()) {
return false;
if (scalar) {
TRACE("nla_cn", tout << "have a zero scalar " << *ee << "\n";);
return false;
}
scalar = true;
}
scalar = true;
}
if (!is_simplified(ee))
return false;

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

@ -57,11 +57,11 @@ class nex_creator {
svector<unsigned> m_active_vars_weights;
public:
static char ch(unsigned j) {
// std::stringstream s;
// s << "v" << j;
// return s.str();
return (char)('a'+j);
static std::string ch(unsigned j) {
std::stringstream s;
s << "v" << j;
return s.str();
// return (char)('a'+j);
}
// assuming that every lpvar is less than this number

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

@ -122,26 +122,32 @@ unsigned common::random() {
return c().random();
}
nex * common::nexvar(lpvar j, nex_creator& cn) const {
nex * common::nexvar(lpvar j, nex_creator& cn) {
// todo: consider deepen the recursion
if (!c().is_monic_var(j))
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) const {
nex * common::nexvar(const rational & coeff, lpvar j, nex_creator& cn) {
// todo: consider deepen the recursion
if (!c().is_monic_var(j))
if (!c().is_monic_var(j)) {
c().insert_to_active_var_set(j);
return cn.mk_mul(cn.mk_scalar(coeff), cn.mk_var(j));
}
const monic& m = c().emons()[j];
nex_mul * e = cn.mk_mul(cn.mk_scalar(coeff));
for (lpvar k : m.vars()) {
c().insert_to_active_var_set(j);
e->add_child(cn.mk_var(k));
CTRACE("nla_horner", c().is_monic_var(k), c().print_var(k, tout) << "\n";);
}
@ -151,6 +157,7 @@ nex * common::nexvar(const rational & coeff, lpvar j, nex_creator& cn) const {
template <typename T> void common::create_sum_from_row(const T& row, nex_creator& cn, nex_sum& sum) {
TRACE("nla_horner", tout << "row="; m_core->print_term(row, tout) << "\n";);
c().prepare_active_var_set();
SASSERT(row.size() > 1);
sum.children().clear();
for (const auto &p : row) {
@ -160,7 +167,43 @@ template <typename T> void common::create_sum_from_row(const T& row, nex_creator
sum.add_child(nexvar(p.coeff(), p.var(), cn));
}
}
set_active_vars_weights();
}
void common::set_active_vars_weights() {
m_nex_creator.set_number_of_vars(c().m_lar_solver.column_count());
for (lpvar j : c().active_var_set()) {
m_nex_creator.set_var_weight(j, static_cast<unsigned>(get_var_weight(j)));
}
}
var_weight common::get_var_weight(lpvar j) const {
var_weight k;
switch (c().m_lar_solver.get_column_type(j)) {
case lp::column_type::fixed:
k = var_weight::FIXED;
break;
case lp::column_type::boxed:
k = var_weight::BOUNDED;
break;
case lp::column_type::lower_bound:
case lp::column_type::upper_bound:
k = var_weight::NOT_FREE;
case lp::column_type::free_column:
k = var_weight::FREE;
break;
default:
UNREACHABLE();
break;
}
if (c().is_monic_var(j)) {
return (var_weight)((int)k + 1);
}
return k;
}
}
template void 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_sum&);

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

@ -45,7 +45,9 @@ inline llc negate(llc cmp) {
class core;
struct common {
core* m_core;
core* m_core;
nex_creator m_nex_creator;
common(core* c): m_core(c) {}
core& c() { return *m_core; }
const core& c() const { return *m_core; }
@ -115,10 +117,11 @@ struct common {
typedef dependency_manager<ci_dependency_config> ci_dependency_manager;
typedef ci_dependency_manager::dependency ci_dependency;
nex* nexvar(lpvar j, nex_creator& ) const;
nex* nexvar(const rational& coeff, lpvar j, nex_creator&) const;
nex* nexvar(lpvar j, nex_creator& );
nex* nexvar(const rational& coeff, lpvar j, nex_creator&);
template <typename T>
void create_sum_from_row(const T&, nex_creator&, nex_sum&);
void set_active_vars_weights();
var_weight get_var_weight(lpvar) const;
};
}

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

@ -79,7 +79,7 @@ public:
class core {
public:
var_eqs<emonics> m_evars;
var_eqs<emonics> m_evars;
lp::lar_solver& m_lar_solver;
vector<lemma> * m_lemma_vec;
lp::int_set m_to_refine;
@ -91,25 +91,25 @@ public:
nla_settings m_nla_settings;
nla_grobner m_grobner;
private:
emonics m_emons;
emonics m_emons;
svector<lpvar> m_add_buffer;
mutable lp::int_set m_row_var_set;
mutable lp::int_set m_active_var_set;
public:
reslimit m_reslim;
const lp::int_set& row_var_set () const { return m_row_var_set;}
bool row_var_set_contains(unsigned j) const { return m_row_var_set.contains(j); }
const lp::int_set& active_var_set () const { return m_active_var_set;}
bool active_var_set_contains(unsigned j) const { return m_active_var_set.contains(j); }
void insert_to_row_var_set(unsigned j) const { m_row_var_set.insert(j); }
void insert_to_active_var_set(unsigned j) const { m_active_var_set.insert(j); }
void clear_row_var_set() const {
m_row_var_set.clear();
void clear_active_var_set() const {
m_active_var_set.clear();
}
void prepare_row_var_set() const {
m_row_var_set.clear();
m_row_var_set.resize(m_lar_solver.number_of_vars());
void prepare_active_var_set() const {
m_active_var_set.clear();
m_active_var_set.resize(m_lar_solver.number_of_vars());
}
reslimit & reslim() { return m_reslim; }

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

@ -75,39 +75,6 @@ void nla_grobner::add_var_and_its_factors_to_q_and_collect_new_rows(lpvar j, std
}
}
var_weight nla_grobner::get_var_weight(lpvar j) const {
var_weight k;
switch (c().m_lar_solver.get_column_type(j)) {
case lp::column_type::fixed:
k = var_weight::FIXED;
break;
case lp::column_type::boxed:
k = var_weight::BOUNDED;
break;
case lp::column_type::lower_bound:
case lp::column_type::upper_bound:
k = var_weight::NOT_FREE;
case lp::column_type::free_column:
k = var_weight::FREE;
break;
default:
UNREACHABLE();
break;
}
if (c().is_monic_var(j)) {
return (var_weight)((int)k + 1);
}
return k;
}
void nla_grobner::set_active_vars_weights() {
m_nex_creator.set_number_of_vars(c().m_lar_solver.column_count());
for (lpvar j : m_active_vars) {
m_nex_creator.set_var_weight(j, static_cast<unsigned>(get_var_weight(j)));
}
}
void nla_grobner::find_nl_cluster() {
prepare_rows_and_active_vars();
std::queue<lpvar> q;

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

@ -89,7 +89,6 @@ class nla_grobner : common {
region m_alloc;
ci_value_manager m_val_manager;
ci_dependency_manager m_dep_manager;
nex_creator m_nex_creator;
nex_lt m_lt;
public:
nla_grobner(core *core);
@ -100,9 +99,7 @@ private:
void prepare_rows_and_active_vars();
void add_var_and_its_factors_to_q_and_collect_new_rows(lpvar j, std::queue<lpvar>& q);
void display(std::ostream&);
void set_active_vars_weights();
void init();
var_weight get_var_weight(lpvar) const;
void compute_basis();
void update_statistics();
bool find_conflict(ptr_vector<equation>& eqs);

14
src/test/lp/lp.cpp
View file

@ -76,20 +76,20 @@ void test_cn_on_expr(nex_sum *t, cross_nested& cn) {
void test_simplify() {
#ifdef Z3DEBUG
nex_creator r;
cross_nested cn(
[](const nex* n) {
TRACE("nla_cn_test", tout << *n << "\n";);
return false;
} ,
[](unsigned) { return false; },
[]() { return 1; } // for random
);
[]() { return 1; }, // for random
r);
// enable_trace("nla_cn");
// enable_trace("nla_cn_details");
// enable_trace("nla_cn_details_");
enable_trace("nla_test");
nex_creator & r = cn.get_nex_creator();
r.set_number_of_vars(3);
for (unsigned j = 0; j < r.get_number_of_vars(); j++)
r.set_var_weight(j, j);
@ -147,6 +147,7 @@ void test_simplify() {
void test_cn_shorter() {
nex_sum *clone;
nex_creator cr;
cross_nested cn(
[](const nex* n) {
TRACE("nla_test", tout <<"cn form = " << *n << "\n";
@ -155,13 +156,12 @@ void test_cn_shorter() {
return false;
} ,
[](unsigned) { return false; },
[]{ return 1; });
[]{ return 1; }, cr);
enable_trace("nla_test");
enable_trace("nla_cn");
enable_trace("nla_cn_test");
enable_trace("nla_cn_details");
enable_trace("nla_test_details");
auto & cr = cn.get_nex_creator();
cr.set_number_of_vars(20);
for (unsigned j = 0; j < cr.get_number_of_vars(); j++)
cr.set_var_weight(j,j);
@ -191,18 +191,18 @@ void test_cn_shorter() {
void test_cn() {
#ifdef Z3DEBUG
test_cn_shorter();
nex_creator cr;
cross_nested cn(
[](const nex* n) {
TRACE("nla_test", tout <<"cn form = " << *n << "\n";);
return false;
} ,
[](unsigned) { return false; },
[]{ return 1; });
[]{ return 1; }, cr);
enable_trace("nla_test");
enable_trace("nla_cn_test");
// enable_trace("nla_cn");
// enable_trace("nla_test_details");
auto & cr = cn.get_nex_creator();
cr.set_number_of_vars(20);
for (unsigned j = 0; j < cr.get_number_of_vars(); j++)
cr.set_var_weight(j, j);