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

set lar_solver.m_status = UNKNOWN in the constructor

Browse source 
Signed-off-by: Lev <levnach@hotmail.com>
This commit is contained in:
Lev 2018-09-28 14:14:25 -07:00 committed by Lev Nachmanson
parent 6dcec4ce79
commit 5d586c8fd1
3 changed files with 2 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/util/lp/int_solver.cpp
View file

@ -187,10 +187,6 @@ struct check_return_helper {
~check_return_helper() { ~check_return_helper() {
TRACE("pivoted_rows", tout << "pivoted rows = " << m_lar_solver->m_mpq_lar_core_solver.m_r_solver.m_pivoted_rows->size() << std::endl;); TRACE("pivoted_rows", tout << "pivoted rows = " << m_lar_solver->m_mpq_lar_core_solver.m_r_solver.m_pivoted_rows->size() << std::endl;);
m_lar_solver->set_track_pivoted_rows(m_track_pivoted_rows); m_lar_solver->set_track_pivoted_rows(m_track_pivoted_rows);
if (m_r == lia_move::cut || m_r == lia_move::branch) {
int_solver * s = m_lar_solver->get_int_solver();
// m_lar_solver->adjust_cut_for_terms(*(s->m_t), *(s->m_k));
}
} }
}; };

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

@ -27,7 +27,7 @@ void clear() {lp_assert(false); // not implemented
} }
lar_solver::lar_solver() : m_status(lp_status::OPTIMAL), lar_solver::lar_solver() : m_status(lp_status::UNKNOWN),
m_infeasible_column_index(-1), m_infeasible_column_index(-1),
m_terms_start_index(1000000), m_terms_start_index(1000000),
m_mpq_lar_core_solver(m_settings, *this), m_mpq_lar_core_solver(m_settings, *this),
@ -1174,6 +1174,7 @@ void lar_solver::get_model(std::unordered_map<var_index, mpq> & variable_values)
std::unordered_set<impq> set_of_different_pairs; std::unordered_set<impq> set_of_different_pairs;
std::unordered_set<mpq> set_of_different_singles; std::unordered_set<mpq> set_of_different_singles;
delta = m_mpq_lar_core_solver.find_delta_for_strict_bounds(delta); delta = m_mpq_lar_core_solver.find_delta_for_strict_bounds(delta);
TRACE("get_model", tout << "delta=" << delta << "size = " << m_mpq_lar_core_solver.m_r_x.size() << std::endl;);
for (i = 0; i < m_mpq_lar_core_solver.m_r_x.size(); i++ ) { for (i = 0; i < m_mpq_lar_core_solver.m_r_x.size(); i++ ) {
const numeric_pair<mpq> & rp = m_mpq_lar_core_solver.m_r_x[i]; const numeric_pair<mpq> & rp = m_mpq_lar_core_solver.m_r_x[i];
set_of_different_pairs.insert(rp); set_of_different_pairs.insert(rp);

1
src/util/lp/lar_solver.h
View file

@ -542,7 +542,6 @@ public:
for (const auto & p : columns_to_subs) { for (const auto & p : columns_to_subs) {
auto it = t.m_coeffs.find(p.first); auto it = t.m_coeffs.find(p.first);
lp_assert(it != t.m_coeffs.end()); lp_assert(it != t.m_coeffs.end());
const lar_term& lt = get_term(p.second);
mpq v = it->second; mpq v = it->second;
t.m_coeffs.erase(it); t.m_coeffs.erase(it);
t.m_coeffs[p.second] = v; t.m_coeffs[p.second] = v;