mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

optimization of phase

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-08-12 09:50:31 -07:00
parent 75962173ff
commit 876cfb4dc9
1 changed files with 4 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
src/util/lp/lar_solver.cpp
View file

@ -1242,7 +1242,7 @@ void lar_solver::get_infeasibility_explanation_for_inf_sign(
}
void lar_solver::get_model(std::unordered_map<var_index, mpq> & variable_values) const {
lp_assert(m_status == lp_status::OPTIMAL);
lp_assert(m_mpq_lar_core_solver.m_r_solver.calc_current_x_is_feasible_include_non_basis());
mpq delta = mpq(1, 2); // start from 0.5 to have less clashes
unsigned i;
do {
@ -1778,16 +1778,9 @@ constraint_index lar_solver::add_var_bound(var_index j, lconstraint_kind kind, c
}
bool lar_solver::compare_values(var_index j, lconstraint_kind k, const mpq & rhs) {
if (is_term(j)) { // j is a term
impq lhs = 0;
for (auto const& cv : get_term(j)) {
lhs += cv.coeff() * get_column_value(cv.var());
}
return compare_values(lhs, k, rhs);
}
else {
return compare_values(get_column_value(j), k, rhs);
}
if (is_term(j))
j = to_column(j);
return compare_values(get_column_value(j), k, rhs);
}
bool lar_solver::compare_values(impq const& lhs, lconstraint_kind k, const mpq & rhs) {