Home
last modified time | relevance | path

Searched refs:m_r_basis (Results 1 – 10 of 10) sorted by relevance

/dports/math/z3/z3-z3-4.8.13/src/math/lp/
H A Dlar_core_solver.h42 vector<unsigned> m_r_basis; variable
142 m_r_basis = m_r_pushed_basis(); in pop_basis()
148 m_d_basis = m_r_basis; in pop_basis()
167 push_vector(m_r_pushed_basis, m_r_basis); in push()
461 m_d_basis = m_r_basis; in solve_on_signature_tableau()
576 init_factorization(m_r_solver.m_factorization, m_r_A, m_r_basis, settings()); in solve_on_signature()
584 m_d_basis = m_r_basis; in solve_on_signature()
615 basis_d = m_r_basis; in fill_basis_d()
805 const vector<unsigned>& r_basis() const { return m_r_basis; } in r_basis()
H A Dlar_core_solver_def.h24 m_r_basis, in lar_core_solver()
98 unsigned bj = m_r_basis[m_r_solver.m_inf_row_index_for_tableau]; in fill_not_improvable_zero_sum_from_inf_row()
H A Dint_solver.cpp180 unsigned j = lrac.m_r_basis[i]; in display_inf_rows()
353 unsigned i = lrac.m_r_basis[row_index]; in get_freedom_interval_for_column()
364 unsigned i = lrac.m_r_basis[row_index]; in get_freedom_interval_for_column()
H A Dlar_solver.h419 unsigned bj = m_mpq_lar_core_solver.m_r_basis[c.var()]; in change_basic_columns_dependend_on_a_given_nb_column_report()
437 unsigned bj = m_mpq_lar_core_solver.m_r_basis[i]; in change_basic_columns_dependend_on_a_given_nb_column_report()
473 unsigned rj = m_mpq_lar_core_solver.m_r_basis[row_index]; in try_to_patch()
H A Dlar_solver.cpp672 …ver", !is_zero(r), tout << "row = " << i << ", j = " << m_mpq_lar_core_solver.m_r_basis[i] << "\n"; in row_is_correct()
703 unsigned bj = m_mpq_lar_core_solver.m_r_basis[c.var()]; in change_basic_columns_dependend_on_a_given_nb_column()
719 unsigned bj = m_mpq_lar_core_solver.m_r_basis[i]; in change_basic_columns_dependend_on_a_given_nb_column()
1658 m_mpq_lar_core_solver.m_r_heading.push_back(m_mpq_lar_core_solver.m_r_basis.size()); in add_new_var_to_core_fields_for_mpq()
1659 m_mpq_lar_core_solver.m_r_basis.push_back(j); in add_new_var_to_core_fields_for_mpq()
2028 m_mpq_lar_core_solver.m_d_basis = m_mpq_lar_core_solver.m_r_basis; in adjust_initial_state_for_lu()
/dports/math/py-z3-solver/z3-z3-4.8.10/src/math/lp/
H A Dlar_core_solver.h42 vector<unsigned> m_r_basis; variable
142 m_r_basis = m_r_pushed_basis(); in pop_basis()
148 m_d_basis = m_r_basis; in pop_basis()
167 push_vector(m_r_pushed_basis, m_r_basis); in push()
461 m_d_basis = m_r_basis; in solve_on_signature_tableau()
576 init_factorization(m_r_solver.m_factorization, m_r_A, m_r_basis, settings()); in solve_on_signature()
584 m_d_basis = m_r_basis; in solve_on_signature()
615 basis_d = m_r_basis; in fill_basis_d()
805 const vector<unsigned>& r_basis() const { return m_r_basis; } in r_basis()
H A Dlar_core_solver_def.h24 m_r_basis, in lar_core_solver()
98 unsigned bj = m_r_basis[m_r_solver.m_inf_row_index_for_tableau]; in fill_not_improvable_zero_sum_from_inf_row()
H A Dint_solver.cpp180 unsigned j = lrac.m_r_basis[i]; in display_inf_rows()
353 unsigned i = lrac.m_r_basis[row_index]; in get_freedom_interval_for_column()
364 unsigned i = lrac.m_r_basis[row_index]; in get_freedom_interval_for_column()
H A Dlar_solver.h418 unsigned bj = m_mpq_lar_core_solver.m_r_basis[c.var()]; in change_basic_columns_dependend_on_a_given_nb_column_report()
436 unsigned bj = m_mpq_lar_core_solver.m_r_basis[i]; in change_basic_columns_dependend_on_a_given_nb_column_report()
472 unsigned rj = m_mpq_lar_core_solver.m_r_basis[row_index]; in try_to_patch()
H A Dlar_solver.cpp661 …ver", !is_zero(r), tout << "row = " << i << ", j = " << m_mpq_lar_core_solver.m_r_basis[i] << "\n"; in row_is_correct()
692 unsigned bj = m_mpq_lar_core_solver.m_r_basis[c.var()]; in change_basic_columns_dependend_on_a_given_nb_column()
708 unsigned bj = m_mpq_lar_core_solver.m_r_basis[i]; in change_basic_columns_dependend_on_a_given_nb_column()
1640 m_mpq_lar_core_solver.m_r_heading.push_back(m_mpq_lar_core_solver.m_r_basis.size()); in add_new_var_to_core_fields_for_mpq()
1641 m_mpq_lar_core_solver.m_r_basis.push_back(j); in add_new_var_to_core_fields_for_mpq()
1988 m_mpq_lar_core_solver.m_d_basis = m_mpq_lar_core_solver.m_r_basis; in adjust_initial_state_for_lu()