mirror of
https://github.com/Z3Prover/z3
synced 2025-04-20 07:36:38 +00:00
adding some content to the new check_int_feasibility()
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
parent
93a3c486b0
commit
09530bb6bc
|
@ -1382,8 +1382,13 @@ void lar_solver::shrink_explanation_to_minimum(vector<std::pair<mpq, constraint_
|
|||
}
|
||||
|
||||
final_check_status lar_solver::check_int_feasibility() {
|
||||
std::cout << "lar_solver::check_int_feasibility()\n";
|
||||
return final_check_status::GIVEUP;
|
||||
unsigned n = A_r().column_count();
|
||||
for (unsigned j = 0; j < n; j++) {
|
||||
if (column_is_integer(j) && column_value_is_integer(j))
|
||||
continue;
|
||||
return final_check_status::GIVEUP;
|
||||
}
|
||||
return final_check_status::DONE;
|
||||
}
|
||||
} // namespace lean
|
||||
|
||||
|
|
|
@ -401,6 +401,16 @@ public:
|
|||
unsigned ext_var = m_columns_to_ext_vars_or_term_indices[j];
|
||||
return m_ext_vars_to_columns.find(ext_var)->second.is_integer();
|
||||
}
|
||||
|
||||
static bool impq_is_int(const impq& v) {
|
||||
return v.x.is_int() && is_zero(v.y);
|
||||
}
|
||||
|
||||
inline
|
||||
bool column_value_is_integer(unsigned j) const {
|
||||
const impq & v = m_mpq_lar_core_solver.m_r_x[j];
|
||||
return impq_is_int(v);
|
||||
}
|
||||
inline bool column_is_real(unsigned j) const { return !column_is_integer(j); }
|
||||
final_check_status check_int_feasibility();
|
||||
};
|
||||
|
|
Loading…
Reference in a new issue