mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity

force int bound on int columns, call term_is_int() after subst

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2024-01-17 13:53:59 -10:00
parent 4f75153186
commit c591a7a3e7
1 changed files with 7 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1641,12 +1641,12 @@ namespace lp {
var_index lar_solver::add_term(const vector<std::pair<mpq, var_index>>& coeffs, unsigned ext_i) {
TRACE("lar_solver_terms", print_linear_combination_of_column_indices_only(coeffs, tout) << ", ext_i =" << ext_i << "\n";);
SASSERT(!m_var_register.external_is_used(ext_i));
m_term_register.add_var(ext_i, term_is_int(coeffs));
lp_assert(all_vars_are_registered(coeffs));
if (strategy_is_undecided())
return add_term_undecided(coeffs);
SASSERT(all_vars_are_registered(coeffs));
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);
SASSERT(m_terms.size() == m_term_register.size());
unsigned adjusted_term_index = m_terms.size() - 1;
@ -1938,10 +1938,11 @@ namespace lp {
tout << std::endl;
}
});
mpq rs = adjust_bound_for_int(j, kind, right_side);
if (column_has_upper_bound(j))
update_column_type_and_bound_with_ub(j, kind, right_side, dep);
update_column_type_and_bound_with_ub(j, kind, rs, dep);
else
update_column_type_and_bound_with_no_ub(j, kind, right_side, dep);
update_column_type_and_bound_with_no_ub(j, kind, rs, dep);
if (is_base(j) && column_is_fixed(j))
m_fixed_base_var_set.insert(j);