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

add an assert

Browse source 
Signed-off-by: Lev <levnach@hotmail.com>
This commit is contained in:
Lev 2018-11-01 15:56:06 -07:00 • committed by Lev Nachmanson
parent c1e0c79a69
commit 9407c4e96f
2 changed files with 13 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1709,8 +1709,19 @@ void lar_solver::push_and_register_term(lar_term* t) {
m_terms.push_back(t);
}
// terms
bool lar_solver::all_vars_are_registered(const vector<std::pair<mpq, var_index>> & coeffs) {
for (const auto & p : coeffs) {
if (p.second >= m_var_register.size()) {
return false;
}
}
return true;
}
var_index lar_solver::add_term(const vector<std::pair<mpq, var_index>> & coeffs) {
lp_assert(all_vars_are_registered(coeffs));
if (strategy_is_undecided())
return add_term_undecided(coeffs);

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

@ -176,6 +176,8 @@ public:
// terms
bool all_vars_are_registered(const vector<std::pair<mpq, var_index>> & coeffs);
var_index add_term(const vector<std::pair<mpq, var_index>> & coeffs);
var_index add_term_undecided(const vector<std::pair<mpq, var_index>> & coeffs);