mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

adding nra solver

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-05-24 14:44:16 -07:00
commit d45c56da3f
3 changed files with 18 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1387,8 +1387,14 @@ void lar_solver::shrink_explanation_to_minimum(vector<std::pair<mpq, constraint_
lean_assert(this->explanation_is_correct(explanation));
}
final_check_status check_int_feasibility() {
return final_check_status::GIVEUP;
final_check_status lar_solver::check_int_feasibility() {
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

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

@ -406,6 +406,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();
};

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

@ -42,6 +42,5 @@ namespace nra {
void push();
void pop(unsigned n);
};
}