mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-30 12:25:51 +00:00
Code Activity

take care of strategy undecided, Nikolaj's comments

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2024-01-17 14:17:07 -10:00
parent 6e9a938533
commit d084a19630
2 changed files with 2 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1577,12 +1577,6 @@ namespace lp {
}
}
var_index lar_solver::add_term_undecided(const vector<std::pair<mpq, var_index>>& coeffs) {
push_term(new lar_term(coeffs));
return tv::mask_term(m_terms.size() - 1);
}
#if Z3DEBUG_CHECK_UNIQUE_TERMS
bool lar_solver::term_coeffs_are_ok(const vector<std::pair<mpq, var_index>>& coeffs) {
@ -1645,9 +1639,9 @@ namespace lp {
lar_term* t = new lar_term(coeffs);
subst_known_terms(t);
m_term_register.add_var(ext_i, term_is_int(t));
if (strategy_is_undecided())
return add_term_undecided(coeffs);
push_term(t);
if (strategy_is_undecided())
return tv::mask_term(m_terms.size() - 1);
SASSERT(m_terms.size() == m_term_register.size());
unsigned adjusted_term_index = m_terms.size() - 1;
var_index ret = tv::mask_term(adjusted_term_index);

1
src/math/lp/lar_solver.h
View file

@ -137,7 +137,6 @@ class lar_solver : public column_namer {
// terms
bool all_vars_are_registered(const vector<std::pair<mpq, var_index>>& coeffs);
var_index add_term_undecided(const vector<std::pair<mpq, var_index>>& coeffs);
bool term_coeffs_are_ok(const vector<std::pair<mpq, var_index>>& coeffs);
void push_term(lar_term* t);
void add_row_from_term_no_constraint(const lar_term* term, unsigned term_ext_index);