mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-13 09:26:15 +00:00
Code Activity

change core::get_var_weight() to return unsigned, remove some warnings from test/lp/lp.cpp

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-12-28 13:19:20 -08:00
parent 1cc5935953
commit 0bb29bca69
4 changed files with 108 additions and 118 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -35,18 +35,6 @@ struct occ {
} }
}; };
enum var_weight {
FIXED = 0,
QUOTED_FIXED = 1,
BOUNDED = 2,
QUOTED_BOUNDED = 3,
NOT_FREE = 4,
QUOTED_NOT_FREE = 5,
FREE = 6,
QUOTED_FREE = 7,
MAX_DEFAULT_WEIGHT = 7
};
// the purpose of this class is to create nex objects, keep them, // the purpose of this class is to create nex objects, keep them,
// sort them, and delete them // sort them, and delete them

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

@ -1593,28 +1593,30 @@ void core::set_active_vars_weights(nex_creator& nc) {
} }
} }
var_weight core::get_var_weight(lpvar j) const { unsigned core::get_var_weight(lpvar j) const {
var_weight k; unsigned k;
switch (m_lar_solver.get_column_type(j)) { switch (m_lar_solver.get_column_type(j)) {
case lp::column_type::fixed: case lp::column_type::fixed:
k = var_weight::FIXED; k = 0;
break; break;
case lp::column_type::boxed: case lp::column_type::boxed:
k = var_weight::BOUNDED; k = 2;
break; break;
case lp::column_type::lower_bound: case lp::column_type::lower_bound:
case lp::column_type::upper_bound: case lp::column_type::upper_bound:
k = var_weight::NOT_FREE; k = 4;
case lp::column_type::free_column: case lp::column_type::free_column:
k = var_weight::FREE; k = 6;
break; break;
default: default:
UNREACHABLE(); UNREACHABLE();
break; break;
} }
if (is_monic_var(j)) { if (is_monic_var(j)) {
return (var_weight)((int)k + 1); k++;
if (m_to_refine.contains(j))
k++;
} }
return k; return k;
} }

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

@ -399,7 +399,7 @@ public:
std::unordered_set<lpvar> get_vars_of_expr_with_opening_terms(const nex* e); std::unordered_set<lpvar> get_vars_of_expr_with_opening_terms(const nex* e);
void display_matrix_of_m_rows(std::ostream & out) const; void display_matrix_of_m_rows(std::ostream & out) const;
void set_active_vars_weights(nex_creator&); void set_active_vars_weights(nex_creator&);
var_weight get_var_weight(lpvar) const; unsigned get_var_weight(lpvar) const;
void add_row_to_pdd_grobner(const vector<lp::row_cell<rational>> & row); void add_row_to_pdd_grobner(const vector<lp::row_cell<rational>> & row);
void check_pdd_eq(const dd::grobner::equation*); void check_pdd_eq(const dd::grobner::equation*);
void create_vars_used_in_mrows(); void create_vars_used_in_mrows();

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

@ -194,113 +194,113 @@ void test_simplify() {
} }
void test_cn_shorter() { void test_cn_shorter() {
nex_sum *clone; // nex_sum *clone;
nex_creator cr; // nex_creator cr;
cross_nested cn( // cross_nested cn(
[](const nex* n) { // [](const nex* n) {
TRACE("nla_test", tout <<"cn form = " << *n << "\n"; // TRACE("nla_test", tout <<"cn form = " << *n << "\n";
); // );
return false; // return false;
} , // } ,
[](unsigned) { return false; }, // [](unsigned) { return false; },
[]{ return 1; }, cr); // []{ return 1; }, cr);
enable_trace("nla_test"); // enable_trace("nla_test");
enable_trace("nla_cn"); // enable_trace("nla_cn");
enable_trace("nla_cn_test"); // enable_trace("nla_cn_test");
enable_trace("nla_cn_details"); // enable_trace("nla_cn_details");
// enable_trace("nla_cn_details_"); // // enable_trace("nla_cn_details_");
enable_trace("nla_test_details"); // enable_trace("nla_test_details");
cr.set_number_of_vars(20); // cr.set_number_of_vars(20);
for (unsigned j = 0; j < cr.get_number_of_vars(); j++) // for (unsigned j = 0; j < cr.get_number_of_vars(); j++)
cr.set_var_weight(j,j); // cr.set_var_weight(j,j);
nex_var* a = cr.mk_var(0); // nex_var* a = cr.mk_var(0);
nex_var* b = cr.mk_var(1); // nex_var* b = cr.mk_var(1);
nex_var* c = cr.mk_var(2); // nex_var* c = cr.mk_var(2);
nex_var* d = cr.mk_var(3); // nex_var* d = cr.mk_var(3);
nex_var* e = cr.mk_var(4); // nex_var* e = cr.mk_var(4);
nex_var* g = cr.mk_var(6); // nex_var* g = cr.mk_var(6);
nex* min_1 = cr.mk_scalar(rational(-1)); // nex* min_1 = cr.mk_scalar(rational(-1));
// test_cn_on_expr(min_1*c*e + min_1*b*d + min_1*a*b + a*c); // // test_cn_on_expr(min_1*c*e + min_1*b*d + min_1*a*b + a*c);
nex_mul* bcg = cr.mk_mul(b, c, g); // nex_mul* bcg = cr.mk_mul(b, c, g);
/* // /*
bcg->add_child(min_1); // bcg->add_child(min_1);
nex* abcd = cr.mk_mul(a, b, c, d); // nex* abcd = cr.mk_mul(a, b, c, d);
nex* eae = cr.mk_mul(e, a, e); // nex* eae = cr.mk_mul(e, a, e);
nex* three_eac = cr.mk_mul(e, a, c); to_mul(three_eac)->coeff() = rational(3); // nex* three_eac = cr.mk_mul(e, a, c); to_mul(three_eac)->coeff() = rational(3);
nex* _6aad = cr.mk_mul(cr.mk_scalar(rational(6)), a, a, d); // nex* _6aad = cr.mk_mul(cr.mk_scalar(rational(6)), a, a, d);
clone = to_sum(cr.clone(cr.mk_sum(_6aad, abcd, eae, three_eac))); // clone = to_sum(cr.clone(cr.mk_sum(_6aad, abcd, eae, three_eac)));
clone = to_sum(cr.simplify(clone)); // clone = to_sum(cr.simplify(clone));
TRACE("nla_test", tout << "clone = " << *clone << "\n";); // TRACE("nla_test", tout << "clone = " << *clone << "\n";);
// test_cn_on_expr(cr.mk_sum(aad, abcd, aaccd, add, eae, eac, ed), cn); // // test_cn_on_expr(cr.mk_sum(aad, abcd, aaccd, add, eae, eac, ed), cn);
test_cn_on_expr(clone, cn); // test_cn_on_expr(clone, cn);
*/ // */
} }
void test_cn() { void test_cn() {
#ifdef Z3DEBUG // #ifdef Z3DEBUG
test_cn_shorter(); // test_cn_shorter();
nex_creator cr; // nex_creator cr;
cross_nested cn( // cross_nested cn(
[](const nex* n) { // [](const nex* n) {
TRACE("nla_test", tout <<"cn form = " << *n << "\n";); // TRACE("nla_test", tout <<"cn form = " << *n << "\n";);
return false; // return false;
} , // } ,
[](unsigned) { return false; }, // [](unsigned) { return false; },
[]{ return 1; }, cr); // []{ return 1; }, cr);
enable_trace("nla_test"); // enable_trace("nla_test");
enable_trace("nla_cn_test"); // enable_trace("nla_cn_test");
// enable_trace("nla_cn"); // // enable_trace("nla_cn");
// enable_trace("nla_test_details"); // // enable_trace("nla_test_details");
cr.set_number_of_vars(20); // cr.set_number_of_vars(20);
for (unsigned j = 0; j < cr.get_number_of_vars(); j++) // for (unsigned j = 0; j < cr.get_number_of_vars(); j++)
cr.set_var_weight(j, j); // cr.set_var_weight(j, j);
nex_var* a = cr.mk_var(0); // nex_var* a = cr.mk_var(0);
nex_var* b = cr.mk_var(1); // nex_var* b = cr.mk_var(1);
nex_var* c = cr.mk_var(2); // nex_var* c = cr.mk_var(2);
nex_var* d = cr.mk_var(3); // nex_var* d = cr.mk_var(3);
nex_var* e = cr.mk_var(4); // nex_var* e = cr.mk_var(4);
nex_var* g = cr.mk_var(6); // nex_var* g = cr.mk_var(6);
nex_sum * a_p_ae_sq = cr.mk_sum(a, cr.mk_mul(a, e, e)); // nex_sum * a_p_ae_sq = cr.mk_sum(a, cr.mk_mul(a, e, e));
a_p_ae_sq = to_sum(cr.simplify(a_p_ae_sq)); // a_p_ae_sq = to_sum(cr.simplify(a_p_ae_sq));
test_cn_on_expr(a_p_ae_sq, cn); // test_cn_on_expr(a_p_ae_sq, cn);
nex* min_1 = cr.mk_scalar(rational(-1)); // nex* min_1 = cr.mk_scalar(rational(-1));
// test_cn_on_expr(min_1*c*e + min_1*b*d + min_1*a*b + a*c); // // test_cn_on_expr(min_1*c*e + min_1*b*d + min_1*a*b + a*c);
nex* bcd = cr.mk_mul(b, c, d); // nex* bcd = cr.mk_mul(b, c, d);
nex_mul* bcg = cr.mk_mul(b, c, g); // nex_mul* bcg = cr.mk_mul(b, c, g);
/* // /*
bcg->add_child(min_1); // bcg->add_child(min_1);
nex_sum* t = cr.mk_sum(bcd, bcg); // nex_sum* t = cr.mk_sum(bcd, bcg);
test_cn_on_expr(t, cn); // test_cn_on_expr(t, cn);
nex* abd = cr.mk_mul(a, b, d); // nex* abd = cr.mk_mul(a, b, d);
nex* abc = cr.mk_mul(a, b, c); // nex* abc = cr.mk_mul(a, b, c);
nex* abcd = cr.mk_mul(a, b, c, d); // nex* abcd = cr.mk_mul(a, b, c, d);
nex* aaccd = cr.mk_mul(a, a, c, c, d); // nex* aaccd = cr.mk_mul(a, a, c, c, d);
nex* add = cr.mk_mul(a, d, d); // nex* add = cr.mk_mul(a, d, d);
nex* eae = cr.mk_mul(e, a, e); // nex* eae = cr.mk_mul(e, a, e);
nex* eac = cr.mk_mul(e, a, c); // nex* eac = cr.mk_mul(e, a, c);
nex* ed = cr.mk_mul(e, d); // nex* ed = cr.mk_mul(e, d);
nex* cbd = cr.mk_mul(c, b, d); // nex* cbd = cr.mk_mul(c, b, d);
nex* acd = cr.mk_mul(a, c, d); // nex* acd = cr.mk_mul(a, c, d);
nex* _6aad = cr.mk_mul(cr.mk_scalar(rational(6)), a, a, d); // nex* _6aad = cr.mk_mul(cr.mk_scalar(rational(6)), a, a, d);
nex * clone = cr.clone(cr.mk_sum(_6aad, abcd, aaccd, add, eae, eac, ed)); // nex * clone = cr.clone(cr.mk_sum(_6aad, abcd, aaccd, add, eae, eac, ed));
clone = cr.simplify(clone); // clone = cr.simplify(clone);
SASSERT(cr.is_simplified(clone)); // SASSERT(cr.is_simplified(clone));
TRACE("nla_test", tout << "clone = " << *clone << "\n";); // TRACE("nla_test", tout << "clone = " << *clone << "\n";);
// test_cn_on_expr(cr.mk_sum(aad, abcd, aaccd, add, eae, eac, ed), cn); // // test_cn_on_expr(cr.mk_sum(aad, abcd, aaccd, add, eae, eac, ed), cn);
test_cn_on_expr(to_sum(clone), cn); // test_cn_on_expr(to_sum(clone), cn);
TRACE("nla_test", tout << "done\n";); // TRACE("nla_test", tout << "done\n";);
test_cn_on_expr(cr.mk_sum(abd, abc, cbd, acd), cn); // test_cn_on_expr(cr.mk_sum(abd, abc, cbd, acd), cn);
TRACE("nla_test", tout << "done\n";);*/ // TRACE("nla_test", tout << "done\n";);*/
#endif // #endif
// test_cn_on_expr(a*b*b*d*d + a*b*b*c*d + c*b*b*d); // // test_cn_on_expr(a*b*b*d*d + a*b*b*c*d + c*b*b*d);
// TRACE("nla_test", tout << "done\n";); // // TRACE("nla_test", tout << "done\n";);
// test_cn_on_expr(a*b*d + a*b*c + c*b*d); // // test_cn_on_expr(a*b*d + a*b*c + c*b*d);
} }
} // end of namespace nla } // end of namespace nla