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

fix the build lp.cpp in test

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-03-19 15:56:09 -07:00
parent 885d640301
commit eae4fd6afd
1 changed files with 44 additions and 43 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -2673,25 +2673,25 @@ void test_term() {
var_index one = solver.add_var(_one, false); var_index one = solver.add_var(_one, false);
vector<std::pair<mpq, var_index>> term_one; vector<std::pair<mpq, var_index>> term_one;
term_one.push_back(std::make_pair((int)1, one)); term_one.push_back(std::make_pair(mpq(1), one));
solver.add_constraint(term_one, lconstraint_kind::EQ, mpq(0)); solver.add_constraint(term_one, lconstraint_kind::EQ, mpq(0));
vector<std::pair<mpq, var_index>> term_ls; vector<std::pair<mpq, var_index>> term_ls;
term_ls.push_back(std::pair<mpq, var_index>((int)1, x)); term_ls.push_back(std::pair<mpq, var_index>(mpq(1), x));
term_ls.push_back(std::pair<mpq, var_index>((int)1, y)); term_ls.push_back(std::pair<mpq, var_index>(mpq(1), y));
term_ls.push_back(std::make_pair((int)3, one)); term_ls.push_back(std::make_pair(mpq(3), one));
var_index z = solver.add_term(term_ls); var_index z = solver.add_term(term_ls);
vector<std::pair<mpq, var_index>> ls; vector<std::pair<mpq, var_index>> ls;
ls.push_back(std::pair<mpq, var_index>((int)1, x)); ls.push_back(std::pair<mpq, var_index>(mpq(1), x));
ls.push_back(std::pair<mpq, var_index>((int)1, y)); ls.push_back(std::pair<mpq, var_index>(mpq(1), y));
ls.push_back(std::pair<mpq, var_index>((int)1, z)); ls.push_back(std::pair<mpq, var_index>(mpq(1), z));
solver.add_constraint(ls, lconstraint_kind::EQ, mpq(0)); solver.add_constraint(ls, lconstraint_kind::EQ, mpq(0));
ls.clear(); ls.clear();
ls.push_back(std::pair<mpq, var_index>((int)1, x)); ls.push_back(std::pair<mpq, var_index>(mpq(1), x));
solver.add_constraint(ls, lconstraint_kind::LT, mpq(0)); solver.add_constraint(ls, lconstraint_kind::LT, mpq(0));
ls.push_back(std::pair<mpq, var_index>((int)2, y)); ls.push_back(std::pair<mpq, var_index>(mpq(2), y));
solver.add_constraint(ls, lconstraint_kind::GT, mpq(0)); solver.add_constraint(ls, lconstraint_kind::GT, mpq(0));
auto status = solver.solve(); auto status = solver.solve();
std::cout << lp_status_to_string(status) << std::endl; std::cout << lp_status_to_string(status) << std::endl;
@ -2711,15 +2711,15 @@ void test_evidence_for_total_inf_simple(argument_parser & args_parser) {
lar_solver solver; lar_solver solver;
var_index x = solver.add_var(0, false); var_index x = solver.add_var(0, false);
var_index y = solver.add_var(1, false); var_index y = solver.add_var(1, false);
solver.add_var_bound(x, LE, -mpq(1)); solver.add_var_bound(x, LE, mpq(-1));
solver.add_var_bound(y, GE, mpq(0)); solver.add_var_bound(y, GE, mpq(0));
vector<std::pair<mpq, var_index>> ls; vector<std::pair<mpq, var_index>> ls;
ls.push_back(std::pair<mpq, var_index>((int)1, x)); ls.push_back(std::pair<mpq, var_index>(mpq(1), x));
ls.push_back(std::pair<mpq, var_index>((int)1, y)); ls.push_back(std::pair<mpq, var_index>(mpq(1), y));
solver.add_constraint(ls, GE, mpq(1)); solver.add_constraint(ls, GE, mpq(1));
ls.pop_back(); ls.pop_back();
ls.push_back(std::pair<mpq, var_index>(-(int)1, y)); ls.push_back(std::pair<mpq, var_index>(- mpq(1), y));
solver.add_constraint(ls, lconstraint_kind::GE, mpq(0)); solver.add_constraint(ls, lconstraint_kind::GE, mpq(0));
auto status = solver.solve(); auto status = solver.solve();
std::cout << lp_status_to_string(status) << std::endl; std::cout << lp_status_to_string(status) << std::endl;
@ -2748,19 +2748,20 @@ void test_bound_propagation_one_small_sample1() {
unsigned b = ls.add_var(1, false); unsigned b = ls.add_var(1, false);
unsigned c = ls.add_var(2, false); unsigned c = ls.add_var(2, false);
vector<std::pair<mpq, var_index>> coeffs; vector<std::pair<mpq, var_index>> coeffs;
coeffs.push_back(std::pair<mpq, var_index>(1, a)); coeffs.push_back(std::pair<mpq, var_index>(mpq(1), a));
coeffs.push_back(std::pair<mpq, var_index>(-1, c)); coeffs.push_back(std::pair<mpq, var_index>(mpq(-1), c));
ls.add_term(coeffs); ls.add_term(coeffs);
coeffs.pop_back(); coeffs.pop_back();
coeffs.push_back(std::pair<mpq, var_index>(-1, b)); coeffs.push_back(std::pair<mpq, var_index>(mpq(-1), b));
ls.add_term(coeffs); ls.add_term(coeffs);
coeffs.clear(); coeffs.clear();
coeffs.push_back(std::pair<mpq, var_index>(1, a)); coeffs.push_back(std::pair<mpq, var_index>(mpq(1), a));
coeffs.push_back(std::pair<mpq, var_index>(-1, b)); coeffs.push_back(std::pair<mpq, var_index>(mpq(-1), b));
ls.add_constraint(coeffs, LE, zero_of_type<mpq>()); ls.add_constraint(coeffs, LE, zero_of_type<mpq>());
coeffs.clear(); coeffs.clear();
coeffs.push_back(std::pair<mpq, var_index>(1, b)); coeffs.push_back(std::pair<mpq, var_index>(mpq(1), b));
coeffs.push_back(std::pair<mpq, var_index>(-1, c)); coeffs.push_back(std::pair<mpq, var_index>(mpq(-1), c));
ls.add_constraint(coeffs, LE, zero_of_type<mpq>()); ls.add_constraint(coeffs, LE, zero_of_type<mpq>());
vector<implied_bound> ev; vector<implied_bound> ev;
ls.add_var_bound(a, LE, mpq(1)); ls.add_var_bound(a, LE, mpq(1));
@ -2812,8 +2813,8 @@ void test_bound_propagation_one_row() {
unsigned x0 = ls.add_var(0, false); unsigned x0 = ls.add_var(0, false);
unsigned x1 = ls.add_var(1, false); unsigned x1 = ls.add_var(1, false);
vector<std::pair<mpq, var_index>> c; vector<std::pair<mpq, var_index>> c;
c.push_back(std::pair<mpq, var_index>(1, x0)); c.push_back(std::pair<mpq, var_index>(mpq(1), x0));
c.push_back(std::pair<mpq, var_index>(-1, x1)); c.push_back(std::pair<mpq, var_index>(mpq(-1), x1));
ls.add_constraint(c, EQ, one_of_type<mpq>()); ls.add_constraint(c, EQ, one_of_type<mpq>());
vector<implied_bound> ev; vector<implied_bound> ev;
ls.add_var_bound(x0, LE, mpq(1)); ls.add_var_bound(x0, LE, mpq(1));
@ -2826,8 +2827,8 @@ void test_bound_propagation_one_row_with_bounded_vars() {
unsigned x0 = ls.add_var(0, false); unsigned x0 = ls.add_var(0, false);
unsigned x1 = ls.add_var(1, false); unsigned x1 = ls.add_var(1, false);
vector<std::pair<mpq, var_index>> c; vector<std::pair<mpq, var_index>> c;
c.push_back(std::pair<mpq, var_index>(1, x0)); c.push_back(std::pair<mpq, var_index>(mpq(1), x0));
c.push_back(std::pair<mpq, var_index>(-1, x1)); c.push_back(std::pair<mpq, var_index>(mpq(-1), x1));
ls.add_constraint(c, EQ, one_of_type<mpq>()); ls.add_constraint(c, EQ, one_of_type<mpq>());
vector<implied_bound> ev; vector<implied_bound> ev;
ls.add_var_bound(x0, GE, mpq(-3)); ls.add_var_bound(x0, GE, mpq(-3));
@ -2842,8 +2843,8 @@ void test_bound_propagation_one_row_mixed() {
unsigned x0 = ls.add_var(0, false); unsigned x0 = ls.add_var(0, false);
unsigned x1 = ls.add_var(1, false); unsigned x1 = ls.add_var(1, false);
vector<std::pair<mpq, var_index>> c; vector<std::pair<mpq, var_index>> c;
c.push_back(std::pair<mpq, var_index>(1, x0)); c.push_back(std::pair<mpq, var_index>(mpq(1), x0));
c.push_back(std::pair<mpq, var_index>(-1, x1)); c.push_back(std::pair<mpq, var_index>(mpq(-1), x1));
ls.add_constraint(c, EQ, one_of_type<mpq>()); ls.add_constraint(c, EQ, one_of_type<mpq>());
vector<implied_bound> ev; vector<implied_bound> ev;
ls.add_var_bound(x1, LE, mpq(1)); ls.add_var_bound(x1, LE, mpq(1));
@ -2858,14 +2859,14 @@ void test_bound_propagation_two_rows() {
unsigned y = ls.add_var(1, false); unsigned y = ls.add_var(1, false);
unsigned z = ls.add_var(2, false); unsigned z = ls.add_var(2, false);
vector<std::pair<mpq, var_index>> c; vector<std::pair<mpq, var_index>> c;
c.push_back(std::pair<mpq, var_index>(1, x)); c.push_back(std::pair<mpq, var_index>(mpq(1), x));
c.push_back(std::pair<mpq, var_index>(2, y)); c.push_back(std::pair<mpq, var_index>(mpq(2), y));
c.push_back(std::pair<mpq, var_index>(3, z)); c.push_back(std::pair<mpq, var_index>(mpq(3), z));
ls.add_constraint(c, GE, one_of_type<mpq>()); ls.add_constraint(c, GE, one_of_type<mpq>());
c.clear(); c.clear();
c.push_back(std::pair<mpq, var_index>(3, x)); c.push_back(std::pair<mpq, var_index>(mpq(3), x));
c.push_back(std::pair<mpq, var_index>(2, y)); c.push_back(std::pair<mpq, var_index>(mpq(2), y));
c.push_back(std::pair<mpq, var_index>(1, z)); c.push_back(std::pair<mpq, var_index>(mpq(y), z));
ls.add_constraint(c, GE, one_of_type<mpq>()); ls.add_constraint(c, GE, one_of_type<mpq>());
ls.add_var_bound(x, LE, mpq(2)); ls.add_var_bound(x, LE, mpq(2));
vector<implied_bound> ev; vector<implied_bound> ev;
@ -2882,9 +2883,9 @@ void test_total_case_u() {
unsigned y = ls.add_var(1, false); unsigned y = ls.add_var(1, false);
unsigned z = ls.add_var(2, false); unsigned z = ls.add_var(2, false);
vector<std::pair<mpq, var_index>> c; vector<std::pair<mpq, var_index>> c;
c.push_back(std::pair<mpq, var_index>(1, x)); c.push_back(std::pair<mpq, var_index>(mpq(1), x));
c.push_back(std::pair<mpq, var_index>(2, y)); c.push_back(std::pair<mpq, var_index>(mpq(2), y));
c.push_back(std::pair<mpq, var_index>(3, z)); c.push_back(std::pair<mpq, var_index>(mpq(3), z));
ls.add_constraint(c, LE, one_of_type<mpq>()); ls.add_constraint(c, LE, one_of_type<mpq>());
ls.add_var_bound(x, GE, zero_of_type<mpq>()); ls.add_var_bound(x, GE, zero_of_type<mpq>());
ls.add_var_bound(y, GE, zero_of_type<mpq>()); ls.add_var_bound(y, GE, zero_of_type<mpq>());
@ -2908,9 +2909,9 @@ void test_total_case_l(){
unsigned y = ls.add_var(1, false); unsigned y = ls.add_var(1, false);
unsigned z = ls.add_var(2, false); unsigned z = ls.add_var(2, false);
vector<std::pair<mpq, var_index>> c; vector<std::pair<mpq, var_index>> c;
c.push_back(std::pair<mpq, var_index>(1, x)); c.push_back(std::pair<mpq, var_index>(mpq(1), x));
c.push_back(std::pair<mpq, var_index>(2, y)); c.push_back(std::pair<mpq, var_index>(mpq(2), y));
c.push_back(std::pair<mpq, var_index>(3, z)); c.push_back(std::pair<mpq, var_index>(mpq(3), z));
ls.add_constraint(c, GE, one_of_type<mpq>()); ls.add_constraint(c, GE, one_of_type<mpq>());
ls.add_var_bound(x, LE, one_of_type<mpq>()); ls.add_var_bound(x, LE, one_of_type<mpq>());
ls.add_var_bound(y, LE, one_of_type<mpq>()); ls.add_var_bound(y, LE, one_of_type<mpq>());
@ -3490,16 +3491,16 @@ void test_maximize_term() {
var_index x = solver.add_var(_x, false); var_index x = solver.add_var(_x, false);
var_index y = solver.add_var(_y, true); var_index y = solver.add_var(_y, true);
vector<std::pair<mpq, var_index>> term_ls; vector<std::pair<mpq, var_index>> term_ls;
term_ls.push_back(std::pair<mpq, var_index>((int)1, x)); term_ls.push_back(std::pair<mpq, var_index>(mpq(1), x));
term_ls.push_back(std::pair<mpq, var_index>((int)-1, y)); term_ls.push_back(std::pair<mpq, var_index>(mpq(-1), y));
unsigned term_x_min_y = solver.add_term(term_ls); unsigned term_x_min_y = solver.add_term(term_ls);
term_ls.clear(); term_ls.clear();
term_ls.push_back(std::pair<mpq, var_index>((int)2, x)); term_ls.push_back(std::pair<mpq, var_index>(mpq(2), x));
term_ls.push_back(std::pair<mpq, var_index>((int)2, y)); term_ls.push_back(std::pair<mpq, var_index>(mpq(2), y));
unsigned term_2x_pl_2y = solver.add_term(term_ls); unsigned term_2x_pl_2y = solver.add_term(term_ls);
solver.add_var_bound(term_x_min_y, LE, zero_of_type<mpq>()); solver.add_var_bound(term_x_min_y, LE, zero_of_type<mpq>());
solver.add_var_bound(term_2x_pl_2y, LE, mpq((int)5)); solver.add_var_bound(term_2x_pl_2y, LE, mpq(5));
solver.find_feasible_solution(); solver.find_feasible_solution();
lp_assert(solver.get_status() == lp_status::OPTIMAL); lp_assert(solver.get_status() == lp_status::OPTIMAL);
solver.print_constraints(std::cout); solver.print_constraints(std::cout);