From 91dbcbc36f1fe3ba51d6804e774ee70dd7b880cc Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 20 Sep 2018 18:57:47 -0700
Subject: [PATCH] fix test build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/test/lp/gomory_test.h | 1 -
src/test/lp/lp.cpp | 20 +++++++++++++-------
2 files changed, 13 insertions(+), 8 deletions(-)
diff --git a/src/test/lp/gomory_test.h b/src/test/lp/gomory_test.h
index 501ad9e1a..972466dc3 100644
--- a/src/test/lp/gomory_test.h
+++ b/src/test/lp/gomory_test.h
@@ -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));
diff --git a/src/test/lp/lp.cpp b/src/test/lp/lp.cpp
index 6e418fe68..ff9de0e58 100644
--- a/src/test/lp/lp.cpp
+++ b/src/test/lp/lp.cpp
@@ -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);