mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 21:08:46 +00:00
Code Activity

use a faster version of get_model in debug checks

Browse source 
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
This commit is contained in:
Lev Nachmanson 2017-07-10 11:57:33 -07:00
parent 86ed01a63b
commit 9dc7ba73eb
2 changed files with 10 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -897,7 +897,7 @@ bool lar_solver::all_constraints_hold() const {
if (m_settings.get_cancel_flag())
return true;
std::unordered_map<var_index, mpq> var_map;
get_model(var_map);
get_model_do_not_care_about_diff_vars(var_map);
for (unsigned i = 0; i < m_constraints.size(); i++) {
if (!constraint_holds(*m_constraints[i], var_map)) {
@ -1137,6 +1137,14 @@ void lar_solver::get_model(std::unordered_map<var_index, mpq> & variable_values)
} while (i != m_mpq_lar_core_solver.m_r_x.size());
}
void lar_solver::get_model_do_not_care_about_diff_vars(std::unordered_map<var_index, mpq> & variable_values) const {
for (unsigned i = 0; i < m_mpq_lar_core_solver.m_r_x.size(); i++ ) {
const impq & rp = m_mpq_lar_core_solver.m_r_x[i];
variable_values[i] = rp.x + rp.y;
}
}
std::string lar_solver::get_variable_name(var_index vi) const {
return get_column_name(vi);
}

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

@ -372,6 +372,7 @@ public:
void get_model(std::unordered_map<var_index, mpq> & variable_values) const;
void get_model_do_not_care_about_diff_vars(std::unordered_map<var_index, mpq> & variable_values) const;
std::string get_variable_name(var_index vi) const;