mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 05:18:44 +00:00
Code Activity

Fixed LP tests

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2017-08-01 18:33:40 +01:00
parent ce01895ab3
commit 81a7f37acc
1 changed files with 7 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/test/lp.cpp
View file

@ -2779,7 +2779,7 @@ If b becomes basic variable, then it is likely the old solver ends up with a row
vector<implied_bound> ev;
ls.add_var_bound(a, LE, mpq(1));
ls.solve();
bound_propagator bp(ls);
lp_bound_propagator bp(ls);
ls.propagate_bounds_for_touched_rows(bp);
std::cout << " bound ev from test_bound_propagation_one_small_sample1" << std::endl;
for (auto & be : bp.m_ibounds) {
@ -2832,7 +2832,7 @@ void test_bound_propagation_one_row() {
vector<implied_bound> ev;
ls.add_var_bound(x0, LE, mpq(1));
ls.solve();
bound_propagator bp(ls);
lp_bound_propagator bp(ls);
ls.propagate_bounds_for_touched_rows(bp);
}
void test_bound_propagation_one_row_with_bounded_vars() {
@ -2848,7 +2848,7 @@ void test_bound_propagation_one_row_with_bounded_vars() {
ls.add_var_bound(x0, LE, mpq(3));
ls.add_var_bound(x0, LE, mpq(1));
ls.solve();
bound_propagator bp(ls);
lp_bound_propagator bp(ls);
ls.propagate_bounds_for_touched_rows(bp);
}
void test_bound_propagation_one_row_mixed() {
@ -2862,7 +2862,7 @@ void test_bound_propagation_one_row_mixed() {
vector<implied_bound> ev;
ls.add_var_bound(x1, LE, mpq(1));
ls.solve();
bound_propagator bp(ls);
lp_bound_propagator bp(ls);
ls.propagate_bounds_for_touched_rows(bp);
}
@ -2885,7 +2885,7 @@ void test_bound_propagation_two_rows() {
vector<implied_bound> ev;
ls.add_var_bound(y, LE, mpq(1));
ls.solve();
bound_propagator bp(ls);
lp_bound_propagator bp(ls);
ls.propagate_bounds_for_touched_rows(bp);
}
@ -2905,7 +2905,7 @@ void test_total_case_u() {
vector<implied_bound> ev;
ls.add_var_bound(z, GE, zero_of_type<mpq>());
ls.solve();
bound_propagator bp(ls);
lp_bound_propagator bp(ls);
ls.propagate_bounds_for_touched_rows(bp);
}
bool contains_j_kind(unsigned j, lconstraint_kind kind, const mpq & rs, const vector<implied_bound> & ev) {
@ -2932,7 +2932,7 @@ void test_total_case_l(){
vector<implied_bound> ev;
ls.add_var_bound(z, LE, zero_of_type<mpq>());
ls.solve();
bound_propagator bp(ls);
lp_bound_propagator bp(ls);
ls.propagate_bounds_for_touched_rows(bp);
lean_assert(ev.size() == 4);
lean_assert(contains_j_kind(x, GE, - one_of_type<mpq>(), ev));