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

fix test build

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-09-20 18:57:47 -07:00
parent d75b6fd9c1
commit 91dbcbc36f
2 changed files with 13 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/test/lp/gomory_test.h
View file

@ -185,7 +185,6 @@ struct gomory_test {
}
void print_term(lar_term & t, std::ostream & out) {
lp_assert(is_zero(t.m_v));
vector<std::pair<mpq, unsigned>> row;
for (auto p : t.m_coeffs)
row.push_back(std::make_pair(p.second, p.first));

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

@ -2667,13 +2667,20 @@ void test_term() {
lar_solver solver;
unsigned _x = 0;
unsigned _y = 1;
unsigned _one = 2;
var_index x = solver.add_var(_x, false);
var_index y = solver.add_var(_y, false);
var_index one = solver.add_var(_one, false);
vector<std::pair<mpq, var_index>> term_one;
term_one.push_back(std::make_pair((int)1, one));
solver.add_constraint(term_one, lconstraint_kind::EQ, mpq(0));
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>((int)1, y));
var_index z = solver.add_term(term_ls, mpq(3));
term_ls.push_back(std::make_pair((int)3, one));
var_index z = solver.add_term(term_ls);
vector<std::pair<mpq, var_index>> ls;
ls.push_back(std::pair<mpq, var_index>((int)1, x));
@ -2743,10 +2750,10 @@ void test_bound_propagation_one_small_sample1() {
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>(-1, c));
ls.add_term(coeffs, zero_of_type<mpq>());
ls.add_term(coeffs);
coeffs.pop_back();
coeffs.push_back(std::pair<mpq, var_index>(-1, b));
ls.add_term(coeffs, zero_of_type<mpq>());
ls.add_term(coeffs);
coeffs.clear();
coeffs.push_back(std::pair<mpq, var_index>(1, a));
coeffs.push_back(std::pair<mpq, var_index>(-1, b));
@ -3485,12 +3492,12 @@ void test_maximize_term() {
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>((int)-1, y));
unsigned term_x_min_y = solver.add_term(term_ls, mpq(0));
unsigned term_x_min_y = solver.add_term(term_ls);
term_ls.clear();
term_ls.push_back(std::pair<mpq, var_index>((int)2, x));
term_ls.push_back(std::pair<mpq, var_index>((int)2, y));
unsigned term_2x_pl_2y = solver.add_term(term_ls, mpq(0));
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_2x_pl_2y, LE, mpq((int)5));
solver.find_feasible_solution();
@ -3502,8 +3509,7 @@ void test_maximize_term() {
std::cout<< "v[" << p.first << "] = " << p.second << std::endl;
}
std::cout << "calling int_solver\n";
lar_term t; mpq k; explanation ex; bool upper;
lia_move lm = i_solver.check(t, k, ex, upper);
lia_move lm = i_solver.check();
VERIFY(lm == lia_move::sat);
impq term_max;
lp_status st = solver.maximize_term(term_2x_pl_2y, term_max);