From d5e06303ef21630ab3b6a69c0d1928a9bb8e055d Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 16 May 2017 17:54:09 -0700 Subject: [PATCH] add queries for integrality of vars Signed-off-by: Lev Nachmanson --- src/util/lp/init_lar_solver.cpp | 1 + src/util/lp/lar_solver.h | 6 ++++++ 2 files changed, 7 insertions(+) diff --git a/src/util/lp/init_lar_solver.cpp b/src/util/lp/init_lar_solver.cpp index 1f004198d..a84d791d5 100644 --- a/src/util/lp/init_lar_solver.cpp +++ b/src/util/lp/init_lar_solver.cpp @@ -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(-1))); add_non_basic_var_to_core_fields(ext_j); lean_assert(sizes_are_correct()); + lean_assert(!column_is_integer(i)); return i; } diff --git a/src/util/lp/lar_solver.h b/src/util/lp/lar_solver.h index 2d2016dbe..78795e0e4 100644 --- a/src/util/lp/lar_solver.h +++ b/src/util/lp/lar_solver.h @@ -396,5 +396,11 @@ public: void pop_tableau(); void clean_inf_set_of_r_solver_after_pop(); void shrink_explanation_to_minimum(vector> & 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); } }; }