mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-28 08:58:44 +00:00
Code Activity

add queries for integrality of vars

Browse source 
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
This commit is contained in:
Lev Nachmanson 2017-05-16 17:54:09 -07:00
parent 7b433bee2b
commit d5e06303ef
2 changed files with 7 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -25,6 +25,7 @@ var_index lar_solver::add_var(unsigned ext_j, bool is_integer) {
m_vars_to_ul_pairs.push_back (ul_pair(static_cast<unsigned>(-1))); m_vars_to_ul_pairs.push_back (ul_pair(static_cast<unsigned>(-1)));
add_non_basic_var_to_core_fields(ext_j); add_non_basic_var_to_core_fields(ext_j);
lean_assert(sizes_are_correct()); lean_assert(sizes_are_correct());
lean_assert(!column_is_integer(i));
return i; return i;
} }

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

@ -396,5 +396,11 @@ public:
void pop_tableau(); void pop_tableau();
void clean_inf_set_of_r_solver_after_pop(); void clean_inf_set_of_r_solver_after_pop();
void shrink_explanation_to_minimum(vector<std::pair<mpq, constraint_index>> & explanation) const; void shrink_explanation_to_minimum(vector<std::pair<mpq, constraint_index>> & explanation) const;
inline
bool column_is_integer(unsigned j) const {
unsigned ext_var = m_columns_to_ext_vars_or_term_indices[j];
return m_ext_vars_to_columns.find(ext_var)->second.is_integer();
}
inline bool column_is_real(unsigned j) const { return !column_is_integer(j); }
}; };
} }