mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 20:38:43 +00:00
Code Activity

Merge branch 'master' of https://github.com/z3prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2018-10-01 20:22:10 -07:00
parent 9d0aa4d02d 3c7e7a7ffd
commit 5eb24d3118
3 changed files with 5 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/util/lp/lar_core_solver.h
View file

@ -817,7 +817,7 @@ public:
}
const bool column_is_bounded(unsigned j) const {
bool column_is_bounded(unsigned j) const {
switch(m_column_types()[j]) {
case column_type::fixed:
case column_type::boxed:

1
src/util/lp/lp_core_solver_base.cpp
View file

@ -84,6 +84,7 @@ template lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::lp_core_s
const vector<lp::numeric_pair<lp::mpq> >&);
template bool lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::print_statistics_with_cost_and_check_that_the_time_is_over(lp::numeric_pair<lp::mpq>, std::ostream&);
template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::snap_xN_to_bounds_and_fill_xB();
template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::solve_Ax_eq_b();
template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::solve_Bd(unsigned int);
template bool lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::update_basis_and_x(int, int, lp::numeric_pair<lp::mpq> const&);
template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::update_x(unsigned int, const lp::numeric_pair<lp::mpq>&);

6
src/util/lp/numeric_pair.h
View file

@ -57,10 +57,10 @@ public:
template <> class numeric_traits<int> {
public:
static bool precise() { return true; }
static int const zero() { return 0; }
static int const one() { return 1; }
static int zero() { return 0; }
static int one() { return 1; }
static bool is_zero(int v) { return v == 0; }
static double const get_double(int const & d) { return d; }
static double get_double(int const & d) { return d; }
static bool is_int(int) {return true;}
static bool is_pos(int j) {return j > 0;}
static bool is_neg(int j) {return j < 0;}