mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 18:05:21 +00:00
Code Activity

remove pragma once from cpp

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-02-08 15:41:13 -08:00
parent 8d293171d5
commit 3f1f4e0f67
5 changed files with 123 additions and 128 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

22
src/math/lp/gomory.cpp
View file

@ -50,7 +50,7 @@ class create_cut {
const impq & upper_bound(unsigned j) const { return m_int_solver.upper_bound(j); }
constraint_index column_lower_bound_constraint(unsigned j) const { return m_int_solver.column_lower_bound_constraint(j); }
constraint_index column_upper_bound_constraint(unsigned j) const { return m_int_solver.column_upper_bound_constraint(j); }
bool column_is_fixed(unsigned j) const { return m_int_solver.m_lar_solver->column_is_fixed(j); }
bool column_is_fixed(unsigned j) const { return m_int_solver.lra.column_is_fixed(j); }
void int_case_in_gomory_cut(unsigned j) {
lp_assert(m_int_solver.column_is_int(j) && m_fj.is_pos());
@ -217,7 +217,7 @@ class create_cut {
}
for (const auto& p : m_t) {
unsigned v = p.var();
if (m_int_solver.m_lar_solver->is_term(v)) {
if (m_int_solver.lra.is_term(v)) {
dump_declaration(out, v);
}
}
@ -276,7 +276,7 @@ public:
void dump(std::ostream& out) {
out << "applying cut at:\n"; print_linear_combination_indices_only<row_strip<mpq>, mpq>(m_row, out); out << std::endl;
for (auto & p : m_row) {
m_int_solver.m_lar_solver->m_mpq_lar_core_solver.m_r_solver.print_column_info(p.var(), out);
m_int_solver.lra.m_mpq_lar_core_solver.m_r_solver.print_column_info(p.var(), out);
}
out << "inf_col = " << m_inf_col << std::endl;
}
@ -336,7 +336,7 @@ public:
adjust_term_and_k_for_some_ints_case_gomory();
lp_assert(m_int_solver.current_solution_is_inf_on_cut());
TRACE("gomory_cut_detail", dump_cut_and_constraints_as_smt_lemma(tout););
m_int_solver.m_lar_solver->subs_term_columns(m_t);
m_int_solver.lra.subs_term_columns(m_t);
TRACE("gomory_cut", print_linear_combination_of_column_indices_only(m_t.coeffs_as_vector(), tout << "gomory cut:"); tout << " <= " << m_k << std::endl;);
return lia_move::cut;
}
@ -386,16 +386,16 @@ int gomory::find_basic_var() {
// Prefer boxed to non-boxed
// Prefer smaller ranges
for (unsigned j : s.m_lar_solver->r_basis()) {
for (unsigned j : s.lra.r_basis()) {
if (!s.column_is_int_inf(j))
continue;
const row_strip<mpq>& row = s.m_lar_solver->get_row(s.row_of_basic_column(j));
const row_strip<mpq>& row = s.lra.get_row(s.row_of_basic_column(j));
if (!is_gomory_cut_target(row))
continue;
#if 0
if (is_boxed(j) && (min_row_size == UINT_MAX || 4*row.size() < 5*min_row_size)) {
lar_core_solver & lcs = m_lar_solver->m_mpq_lar_core_solver;
lar_core_solver & lcs = lra.m_mpq_lar_core_solver;
auto new_range = lcs.m_r_upper_bounds()[j].x - lcs.m_r_lower_bounds()[j].x;
if (!boxed) {
result = j;
@ -427,8 +427,8 @@ int gomory::find_basic_var() {
}
lia_move gomory::operator()(lar_term & t, mpq & k, explanation* ex, bool& upper) {
if (s.m_lar_solver->move_non_basic_columns_to_bounds()) {
lp_status st = s.m_lar_solver->find_feasible_solution();
if (s.lra.move_non_basic_columns_to_bounds()) {
lp_status st = s.lra.find_feasible_solution();
(void)st;
lp_assert(st == lp_status::FEASIBLE || st == lp_status::OPTIMAL);
}
@ -436,8 +436,8 @@ lia_move gomory::operator()(lar_term & t, mpq & k, explanation* ex, bool& upper)
int j = find_basic_var();
if (j == -1) return lia_move::undef;
unsigned r = s.row_of_basic_column(j);
const row_strip<mpq>& row = s.m_lar_solver->get_row(r);
SASSERT(s.m_lar_solver->row_is_correct(r));
const row_strip<mpq>& row = s.lra.get_row(r);
SASSERT(s.lra.row_is_correct(r));
SASSERT(is_gomory_cut_target(row));
upper = true;
return cut(t, k, ex, j, row);

6
src/math/lp/int_cube.cpp
View file

@ -1,5 +1,5 @@
/*++
Copyright (c) 2017 Microsoft Corporation
Copyright (c) 2020 Microsoft Corporation
Module Name:
@ -15,8 +15,6 @@ Author:
Revision History:
--*/
#pragma once
#include "math/lp/int_solver.h"
#include "math/lp/lar_solver.h"
@ -24,7 +22,7 @@ Revision History:
namespace lp {
int_cube::int_cube(int_solver& lia):lia(lia), lra(*lia.m_lar_solver) {}
int_cube::int_cube(int_solver& lia):lia(lia), lra(lia.lra) {}
lia_move int_cube::operator()() {
lia.settings().stats().m_cube_calls++;

217
src/math/lp/int_solver.cpp
View file

@ -14,7 +14,7 @@ namespace lp {
std::ostream& int_solver::display_inf_rows(std::ostream& out) const {
unsigned num = m_lar_solver->A_r().column_count();
unsigned num = lra.A_r().column_count();
for (unsigned v = 0; v < num; v++) {
if (column_is_int(v) && !get_value(v).is_int()) {
display_column(out, v);
@ -22,11 +22,11 @@ std::ostream& int_solver::display_inf_rows(std::ostream& out) const {
}
num = 0;
for (unsigned i = 0; i < m_lar_solver->A_r().row_count(); i++) {
unsigned j = m_lar_solver->m_mpq_lar_core_solver.m_r_basis[i];
for (unsigned i = 0; i < lra.A_r().row_count(); i++) {
unsigned j = lra.m_mpq_lar_core_solver.m_r_basis[i];
if (column_is_int_inf(j)) {
num++;
m_lar_solver->print_row(m_lar_solver->A_r().m_rows[i], out);
lra.print_row(lra.A_r().m_rows[i], out);
out << "\n";
}
}
@ -34,10 +34,6 @@ std::ostream& int_solver::display_inf_rows(std::ostream& out) const {
return out;
}
bool int_solver::has_inf_int() const {
return m_lar_solver->has_inf_int();
}
int int_solver::find_inf_int_base_column() {
unsigned inf_int_count = 0;
int j = find_inf_int_boxed_base_column_with_smallest_range(inf_int_count);
@ -51,7 +47,7 @@ int int_solver::find_inf_int_base_column() {
}
int int_solver::get_kth_inf_int(unsigned k) const {
for (unsigned j : m_lar_solver->r_basis())
for (unsigned j : lra.r_basis())
if (column_is_int_inf(j) && k-- == 0)
return j;
lp_assert(false);
@ -59,7 +55,7 @@ int int_solver::get_kth_inf_int(unsigned k) const {
}
int int_solver::find_inf_int_nbasis_column() const {
for (unsigned j : m_lar_solver->r_nbasis())
for (unsigned j : lra.r_nbasis())
if (!column_is_int_inf(j)) {
return j;
}
@ -73,9 +69,9 @@ int int_solver::find_inf_int_boxed_base_column_with_smallest_range(unsigned & in
mpq new_range;
mpq small_range_thresold(1024);
unsigned n = 0;
lar_core_solver & lcs = m_lar_solver->m_mpq_lar_core_solver;
lar_core_solver & lcs = lra.m_mpq_lar_core_solver;
for (unsigned j : m_lar_solver->r_basis()) {
for (unsigned j : lra.r_basis()) {
if (!column_is_int_inf(j))
continue;
inf_int_count++;
@ -99,7 +95,7 @@ int int_solver::find_inf_int_boxed_base_column_with_smallest_range(unsigned & in
}
bool int_solver::current_solution_is_inf_on_cut() const {
const auto & x = m_lar_solver->m_mpq_lar_core_solver.m_r_x;
const auto & x = lra.m_mpq_lar_core_solver.m_r_x;
impq v = m_t.apply(x);
mpq sign = m_upper ? one_of_type<mpq>() : -one_of_type<mpq>();
CTRACE("current_solution_is_inf_on_cut", v * sign <= impq(m_k) * sign,
@ -109,28 +105,32 @@ bool int_solver::current_solution_is_inf_on_cut() const {
return v * sign > impq(m_k) * sign;
}
bool int_solver::has_inf_int() const {
return lra.has_inf_int();
}
constraint_index int_solver::column_upper_bound_constraint(unsigned j) const {
return m_lar_solver->get_column_upper_bound_witness(j);
return lra.get_column_upper_bound_witness(j);
}
constraint_index int_solver::column_lower_bound_constraint(unsigned j) const {
return m_lar_solver->get_column_lower_bound_witness(j);
return lra.get_column_lower_bound_witness(j);
}
unsigned int_solver::row_of_basic_column(unsigned j) const {
return m_lar_solver->row_of_basic_column(j);
return lra.row_of_basic_column(j);
}
lp_settings& int_solver::settings() {
return m_lar_solver->settings();
return lra.settings();
}
const lp_settings& int_solver::settings() const {
return m_lar_solver->settings();
return lra.settings();
}
bool int_solver::column_is_int(unsigned j) const {
return m_lar_solver->column_is_int(j);
return lra.column_is_int(j);
}
bool int_solver::is_real(unsigned j) const {
@ -138,24 +138,39 @@ bool int_solver::is_real(unsigned j) const {
}
bool int_solver::value_is_int(unsigned j) const {
return m_lar_solver->column_value_is_int(j);
return lra.column_value_is_int(j);
}
unsigned int_solver::random() {
return lra.get_core_solver().settings().random_next();
}
const impq& int_solver::upper_bound(unsigned j) const {
return lra.column_upper_bound(j);
}
bool int_solver::is_term(unsigned j) const {
return lra.column_corresponds_to_term(j);
}
unsigned int_solver::column_count() const {
return lra.column_count();
}
// this will allow to enable and disable tracking of the pivot rows
struct check_return_helper {
lar_solver * m_lar_solver;
lar_solver& lra;
bool m_track_pivoted_rows;
check_return_helper(lar_solver* ls) :
m_lar_solver(ls),
m_track_pivoted_rows(ls->get_track_pivoted_rows())
check_return_helper(lar_solver& ls) :
lra(ls),
m_track_pivoted_rows(lra.get_track_pivoted_rows())
{
TRACE("pivoted_rows", tout << "pivoted rows = " << ls->m_mpq_lar_core_solver.m_r_solver.m_pivoted_rows->size() << std::endl;);
m_lar_solver->set_track_pivoted_rows(false);
TRACE("pivoted_rows", tout << "pivoted rows = " << lra.m_mpq_lar_core_solver.m_r_solver.m_pivoted_rows->size() << std::endl;);
lra.set_track_pivoted_rows(false);
}
~check_return_helper() {
TRACE("pivoted_rows", tout << "pivoted rows = " << m_lar_solver->m_mpq_lar_core_solver.m_r_solver.m_pivoted_rows->size() << std::endl;);
m_lar_solver->set_track_pivoted_rows(m_track_pivoted_rows);
TRACE("pivoted_rows", tout << "pivoted rows = " << lra.m_mpq_lar_core_solver.m_r_solver.m_pivoted_rows->size() << std::endl;);
lra.set_track_pivoted_rows(m_track_pivoted_rows);
}
};
@ -173,7 +188,6 @@ lia_move int_solver::find_cube() {
}
}
bool int_solver::should_run_gcd_test() {
return settings().m_int_run_gcd_test;
}
@ -208,10 +222,10 @@ lia_move int_solver::gomory_cut() {
void int_solver::try_add_term_to_A_for_hnf(unsigned i) {
mpq rs;
const lar_term* t = m_lar_solver->terms()[i];
const lar_term* t = lra.terms()[i];
constraint_index ci;
bool upper_bound;
if (!hnf_cutter_is_full() && m_lar_solver->get_equality_and_right_side_for_term_on_current_x(i, rs, ci, upper_bound)) {
if (!hnf_cutter_is_full() && lra.get_equality_and_right_side_for_term_on_current_x(i, rs, ci, upper_bound)) {
m_hnf_cutter.add_term(t, rs, ci, upper_bound);
}
}
@ -232,7 +246,7 @@ bool int_solver::hnf_has_var_with_non_integral_value() const {
bool int_solver::init_terms_for_hnf_cut() {
m_hnf_cutter.clear();
for (unsigned i = 0; i < m_lar_solver->terms().size() && !hnf_cutter_is_full(); i++) {
for (unsigned i = 0; i < lra.terms().size() && !hnf_cutter_is_full(); i++) {
try_add_term_to_A_for_hnf(i);
}
return hnf_has_var_with_non_integral_value();
@ -245,12 +259,12 @@ lia_move int_solver::make_hnf_cut() {
settings().stats().m_hnf_cutter_calls++;
TRACE("hnf_cut", tout << "settings().stats().m_hnf_cutter_calls = " << settings().stats().m_hnf_cutter_calls << "\n";
for (unsigned i : m_hnf_cutter.constraints_for_explanation()) {
m_lar_solver->constraints().display(tout, i);
lra.constraints().display(tout, i);
}
tout << m_lar_solver->constraints();
tout << lra.constraints();
);
#ifdef Z3DEBUG
vector<mpq> x0 = m_hnf_cutter.transform_to_local_columns(m_lar_solver->m_mpq_lar_core_solver.m_r_x);
vector<mpq> x0 = m_hnf_cutter.transform_to_local_columns(lra.m_mpq_lar_core_solver.m_r_x);
#else
vector<mpq> x0;
#endif
@ -258,10 +272,10 @@ lia_move int_solver::make_hnf_cut() {
if (r == lia_move::cut) {
TRACE("hnf_cut",
m_lar_solver->print_term(m_t, tout << "cut:");
lra.print_term(m_t, tout << "cut:");
tout << " <= " << m_k << std::endl;
for (unsigned i : m_hnf_cutter.constraints_for_explanation()) {
m_lar_solver->constraints().display(tout, i);
lra.constraints().display(tout, i);
}
);
lp_assert(current_solution_is_inf_on_cut());
@ -293,7 +307,7 @@ lia_move int_solver::hnf_cut() {
}
lia_move int_solver::check(lp::explanation * e) {
SASSERT(m_lar_solver->ax_is_correct());
SASSERT(lra.ax_is_correct());
if (!has_inf_int()) return lia_move::sat;
#define CHECK_RET(fn) \
@ -309,10 +323,10 @@ lia_move int_solver::check(lp::explanation * e) {
CHECK_RET(run_gcd_test());
check_return_helper pc(m_lar_solver);
check_return_helper pc(lra);
if (settings().m_int_pivot_fixed_vars_from_basis)
m_lar_solver->pivot_fixed_vars_from_basis();
lra.pivot_fixed_vars_from_basis();
CHECK_RET(patch_nbasic_columns());
++m_number_of_calls;
@ -335,15 +349,15 @@ int int_solver::find_any_inf_int_column_basis_first() {
void int_solver::set_value_for_nbasic_column_ignore_old_values(unsigned j, const impq & new_val) {
lp_assert(!is_base(j));
auto & x = m_lar_solver->m_mpq_lar_core_solver.m_r_x[j];
auto & x = lra.m_mpq_lar_core_solver.m_r_x[j];
auto delta = new_val - x;
x = new_val;
TRACE("int_solver", tout << "x[" << j << "] = " << x << "\n";);
m_lar_solver->change_basic_columns_dependend_on_a_given_nb_column(j, delta);
lra.change_basic_columns_dependend_on_a_given_nb_column(j, delta);
}
void int_solver::patch_nbasic_column(unsigned j) {
auto & lcs = m_lar_solver->m_mpq_lar_core_solver;
auto & lcs = lra.m_mpq_lar_core_solver;
impq & val = lcs.m_r_x[j];
bool inf_l, inf_u;
impq l, u;
@ -364,12 +378,12 @@ void int_solver::patch_nbasic_column(unsigned j) {
tout << ", ";
if (inf_u) tout << "oo"; else tout << u;
tout << "]";
tout << ", m: " << m << ", val: " << val << ", is_int: " << m_lar_solver->column_is_int(j) << "\n";);
tout << ", m: " << m << ", val: " << val << ", is_int: " << lra.column_is_int(j) << "\n";);
if (!inf_l) {
l = impq(m_is_one ? ceil(l) : m * ceil(l / m));
if (inf_u || l <= u) {
TRACE("patch_int", tout << "patching with l: " << l << '\n';);
m_lar_solver->set_value_for_nbasic_column(j, l);
lra.set_value_for_nbasic_column(j, l);
}
else {
TRACE("patch_int", tout << "not patching " << l << "\n";);
@ -377,11 +391,11 @@ void int_solver::patch_nbasic_column(unsigned j) {
}
else if (!inf_u) {
u = impq(m_is_one ? floor(u) : m * floor(u / m));
m_lar_solver->set_value_for_nbasic_column(j, u);
lra.set_value_for_nbasic_column(j, u);
TRACE("patch_int", tout << "patching with u: " << u << '\n';);
}
else {
m_lar_solver->set_value_for_nbasic_column(j, impq(0));
lra.set_value_for_nbasic_column(j, impq(0));
TRACE("patch_int", tout << "patching with 0\n";);
}
}
@ -389,7 +403,7 @@ void int_solver::patch_nbasic_column(unsigned j) {
lia_move int_solver::patch_nbasic_columns() {
settings().stats().m_patches++;
lp_assert(is_feasible());
for (unsigned j : m_lar_solver->m_mpq_lar_core_solver.m_r_nbasis) {
for (unsigned j : lra.m_mpq_lar_core_solver.m_r_nbasis) {
patch_nbasic_column(j);
}
lp_assert(is_feasible());
@ -410,7 +424,7 @@ mpq get_denominators_lcm(const row_strip<mpq> & row) {
bool int_solver::gcd_test_for_row(static_matrix<mpq, numeric_pair<mpq>> & A, unsigned i) {
auto const& row = A.m_rows[i];
auto & lcs = m_lar_solver->m_mpq_lar_core_solver;
auto & lcs = lra.m_mpq_lar_core_solver;
unsigned basic_var = lcs.m_r_basis[i];
if (!column_is_int(basic_var) || get_value(basic_var).is_int())
@ -424,27 +438,27 @@ bool int_solver::gcd_test_for_row(static_matrix<mpq, numeric_pair<mpq>> & A, uns
for (auto &c : A.m_rows[i]) {
j = c.var();
const mpq& a = c.coeff();
if (m_lar_solver->column_is_fixed(j)) {
if (lra.column_is_fixed(j)) {
mpq aux = lcm_den * a;
consts += aux * m_lar_solver->column_lower_bound(j).x;
consts += aux * lra.column_lower_bound(j).x;
}
else if (m_lar_solver->column_is_real(j)) {
else if (lra.column_is_real(j)) {
return true;
}
else if (gcds.is_zero()) {
gcds = abs(lcm_den * a);
least_coeff = gcds;
least_coeff_is_bounded = m_lar_solver->column_is_bounded(j);
least_coeff_is_bounded = lra.column_is_bounded(j);
}
else {
mpq aux = abs(lcm_den * a);
gcds = gcd(gcds, aux);
if (aux < least_coeff) {
least_coeff = aux;
least_coeff_is_bounded = m_lar_solver->column_is_bounded(j);
least_coeff_is_bounded = lra.column_is_bounded(j);
}
else if (least_coeff_is_bounded && aux == least_coeff) {
least_coeff_is_bounded = m_lar_solver->column_is_bounded(j);
least_coeff_is_bounded = lra.column_is_bounded(j);
}
}
SASSERT(gcds.is_int());
@ -481,20 +495,20 @@ bool int_solver::gcd_test_for_row(static_matrix<mpq, numeric_pair<mpq>> & A, uns
void int_solver::add_to_explanation_from_fixed_or_boxed_column(unsigned j) {
constraint_index lc, uc;
m_lar_solver->get_bound_constraint_witnesses_for_column(j, lc, uc);
lra.get_bound_constraint_witnesses_for_column(j, lc, uc);
m_ex->push_justification(lc);
m_ex->push_justification(uc);
}
void int_solver::fill_explanation_from_fixed_columns(const row_strip<mpq> & row) {
for (const auto & c : row) {
if (!m_lar_solver->column_is_fixed(c.var()))
if (!lra.column_is_fixed(c.var()))
continue;
add_to_explanation_from_fixed_or_boxed_column(c.var());
}
}
bool int_solver::gcd_test() {
auto & A = m_lar_solver->A_r(); // getting the matrix
auto & A = lra.A_r(); // getting the matrix
for (unsigned i = 0; i < A.row_count(); i++)
if (!gcd_test_for_row(A, i))
return false;
@ -505,7 +519,7 @@ bool int_solver::ext_gcd_test(const row_strip<mpq> & row,
mpq const & least_coeff,
mpq const & lcm_den,
mpq const & consts) {
TRACE("ext_gcd_test", tout << "row = "; m_lar_solver->print_row(row, tout););
TRACE("ext_gcd_test", tout << "row = "; lra.print_row(row, tout););
mpq gcds(0);
mpq l(consts);
mpq u(consts);
@ -514,27 +528,27 @@ bool int_solver::ext_gcd_test(const row_strip<mpq> & row,
unsigned j;
for (const auto & c : row) {
j = c.var();
TRACE("ext_gcd_test", tout << "col = "; m_lar_solver->m_mpq_lar_core_solver.m_r_solver.print_column_bound_info(j, tout););
TRACE("ext_gcd_test", tout << "col = "; lra.m_mpq_lar_core_solver.m_r_solver.print_column_bound_info(j, tout););
const mpq & a = c.coeff();
if (m_lar_solver->column_is_fixed(j))
if (lra.column_is_fixed(j))
continue;
SASSERT(!m_lar_solver->column_is_real(j));
SASSERT(!lra.column_is_real(j));
mpq ncoeff = lcm_den * a;
SASSERT(ncoeff.is_int());
mpq abs_ncoeff = abs(ncoeff);
if (abs_ncoeff == least_coeff) {
SASSERT(m_lar_solver->column_is_bounded(j));
SASSERT(lra.column_is_bounded(j));
if (ncoeff.is_pos()) {
// l += ncoeff * m_lar_solver->column_lower_bound(j).x;
l.addmul(ncoeff, m_lar_solver->column_lower_bound(j).x);
// u += ncoeff * m_lar_solver->column_upper_bound(j).x;
u.addmul(ncoeff, m_lar_solver->column_upper_bound(j).x);
// l += ncoeff * lra.column_lower_bound(j).x;
l.addmul(ncoeff, lra.column_lower_bound(j).x);
// u += ncoeff * lra.column_upper_bound(j).x;
u.addmul(ncoeff, lra.column_upper_bound(j).x);
}
else {
// l += ncoeff * upper_bound(j).get_rational();
l.addmul(ncoeff, m_lar_solver->column_upper_bound(j).x);
l.addmul(ncoeff, lra.column_upper_bound(j).x);
// u += ncoeff * lower_bound(j).get_rational();
u.addmul(ncoeff, m_lar_solver->column_lower_bound(j).x);
u.addmul(ncoeff, lra.column_lower_bound(j).x);
}
add_to_explanation_from_fixed_or_boxed_column(j);
}
@ -557,23 +571,21 @@ bool int_solver::ext_gcd_test(const row_strip<mpq> & row,
if (u1 < l1) {
fill_explanation_from_fixed_columns(row);
return false;
}
}
return true;
}
int_solver::int_solver(lar_solver* lar_slv) :
m_lar_solver(lar_slv),
int_solver::int_solver(lar_solver& lar_slv) :
lra(lar_slv),
m_number_of_calls(0),
m_hnf_cutter(settings()),
m_hnf_cut_period(settings().hnf_cut_period()) {
m_lar_solver->set_int_solver(this);
lra.set_int_solver(this);
}
bool int_solver::has_lower(unsigned j) const {
switch (m_lar_solver->m_mpq_lar_core_solver.m_column_types()[j]) {
switch (lra.m_mpq_lar_core_solver.m_column_types()[j]) {
case column_type::fixed:
case column_type::boxed:
case column_type::lower_bound:
@ -584,7 +596,7 @@ bool int_solver::has_lower(unsigned j) const {
}
bool int_solver::has_upper(unsigned j) const {
switch (m_lar_solver->m_mpq_lar_core_solver.m_column_types()[j]) {
switch (lra.m_mpq_lar_core_solver.m_column_types()[j]) {
case column_type::fixed:
case column_type::boxed:
case column_type::upper_bound:
@ -609,7 +621,7 @@ static void set_upper(impq & u, bool & inf_u, impq const & v) {
}
bool int_solver::get_freedom_interval_for_column(unsigned j, bool & inf_l, impq & l, bool & inf_u, impq & u, mpq & m) {
auto & lcs = m_lar_solver->m_mpq_lar_core_solver;
auto & lcs = lra.m_mpq_lar_core_solver;
if (lcs.m_r_heading[j] >= 0) // the basic var
return false;
@ -630,7 +642,7 @@ bool int_solver::get_freedom_interval_for_column(unsigned j, bool & inf_l, impq
unsigned row_index;
lp_assert(settings().use_tableau());
const auto & A = m_lar_solver->A_r();
const auto & A = lra.A_r();
unsigned rounds = 0;
for (const auto &c : A.column(j)) {
row_index = c.var();
@ -684,7 +696,7 @@ bool int_solver::get_freedom_interval_for_column(unsigned j, bool & inf_l, impq
TRACE("freedom_interval",
tout << "freedom variable for:\n";
tout << m_lar_solver->get_variable_name(j);
tout << lra.get_variable_name(j);
tout << "[";
if (inf_l) tout << "-oo"; else tout << l;
tout << "; ";
@ -698,18 +710,18 @@ bool int_solver::get_freedom_interval_for_column(unsigned j, bool & inf_l, impq
bool int_solver::is_feasible() const {
auto & lcs = m_lar_solver->m_mpq_lar_core_solver;
auto & lcs = lra.m_mpq_lar_core_solver;
lp_assert(
lcs.m_r_solver.calc_current_x_is_feasible_include_non_basis() ==
lcs.m_r_solver.current_x_is_feasible());
return lcs.m_r_solver.current_x_is_feasible();
}
const impq & int_solver::get_value(unsigned j) const {
return m_lar_solver->m_mpq_lar_core_solver.m_r_x[j];
return lra.m_mpq_lar_core_solver.m_r_x[j];
}
std::ostream& int_solver::display_column(std::ostream & out, unsigned j) const {
return m_lar_solver->m_mpq_lar_core_solver.m_r_solver.print_column_info(j, out);
return lra.m_mpq_lar_core_solver.m_r_solver.print_column_info(j, out);
return out;
}
@ -718,23 +730,23 @@ bool int_solver::column_is_int_inf(unsigned j) const {
}
bool int_solver::is_base(unsigned j) const {
return m_lar_solver->m_mpq_lar_core_solver.m_r_heading[j] >= 0;
return lra.m_mpq_lar_core_solver.m_r_heading[j] >= 0;
}
bool int_solver::is_boxed(unsigned j) const {
return m_lar_solver->m_mpq_lar_core_solver.m_column_types[j] == column_type::boxed;
return lra.m_mpq_lar_core_solver.m_column_types[j] == column_type::boxed;
}
bool int_solver::is_fixed(unsigned j) const {
return m_lar_solver->m_mpq_lar_core_solver.m_column_types[j] == column_type::fixed;
return lra.m_mpq_lar_core_solver.m_column_types[j] == column_type::fixed;
}
bool int_solver::is_free(unsigned j) const {
return m_lar_solver->m_mpq_lar_core_solver.m_column_types[j] == column_type::free_column;
return lra.m_mpq_lar_core_solver.m_column_types[j] == column_type::free_column;
}
bool int_solver::at_bound(unsigned j) const {
auto & mpq_solver = m_lar_solver->m_mpq_lar_core_solver.m_r_solver;
auto & mpq_solver = lra.m_mpq_lar_core_solver.m_r_solver;
switch (mpq_solver.m_column_types[j] ) {
case column_type::fixed:
case column_type::boxed:
@ -751,7 +763,7 @@ bool int_solver::at_bound(unsigned j) const {
}
bool int_solver::at_lower(unsigned j) const {
auto & mpq_solver = m_lar_solver->m_mpq_lar_core_solver.m_r_solver;
auto & mpq_solver = lra.m_mpq_lar_core_solver.m_r_solver;
switch (mpq_solver.m_column_types[j] ) {
case column_type::fixed:
case column_type::boxed:
@ -763,7 +775,7 @@ bool int_solver::at_lower(unsigned j) const {
}
bool int_solver::at_upper(unsigned j) const {
auto & mpq_solver = m_lar_solver->m_mpq_lar_core_solver.m_r_solver;
auto & mpq_solver = lra.m_mpq_lar_core_solver.m_r_solver;
switch (mpq_solver.m_column_types[j] ) {
case column_type::fixed:
case column_type::boxed:
@ -775,7 +787,7 @@ bool int_solver::at_upper(unsigned j) const {
}
void int_solver::display_row_info(std::ostream & out, unsigned row_index) const {
auto & rslv = m_lar_solver->m_mpq_lar_core_solver.m_r_solver;
auto & rslv = lra.m_mpq_lar_core_solver.m_r_solver;
for (const auto &c: rslv.m_A.m_rows[row_index]) {
if (numeric_traits<mpq>::is_pos(c.coeff()))
out << "+";
@ -788,12 +800,6 @@ void int_solver::display_row_info(std::ostream & out, unsigned row_index) const
rslv.print_column_bound_info(rslv.m_basis[row_index], out);
}
unsigned int_solver::random() {
return m_lar_solver->get_core_solver().settings().random_next();
}
// at this point the
bool int_solver::shift_var(unsigned j, unsigned range) {
if (is_fixed(j) || is_base(j))
return false;
@ -847,7 +853,7 @@ bool int_solver::shift_var(unsigned j, unsigned range) {
}
bool int_solver::non_basic_columns_are_at_bounds() const {
auto & lcs = m_lar_solver->m_mpq_lar_core_solver;
auto & lcs = lra.m_mpq_lar_core_solver;
for (unsigned j :lcs.m_r_nbasis) {
auto & val = lcs.m_r_x[j];
switch (lcs.m_column_types()[j]) {
@ -873,14 +879,14 @@ bool int_solver::non_basic_columns_are_at_bounds() const {
}
const impq& int_solver::lower_bound(unsigned j) const {
return m_lar_solver->column_lower_bound(j);
return lra.column_lower_bound(j);
}
lia_move int_solver::create_branch_on_column(int j) {
TRACE("check_main_int", tout << "branching" << std::endl;);
lp_assert(m_t.is_empty());
lp_assert(j != -1);
m_t.add_monomial(mpq(1), m_lar_solver->adjust_column_index_to_term_index(j));
m_t.add_monomial(mpq(1), lra.adjust_column_index_to_term_index(j));
if (is_free(j)) {
m_upper = random() % 2;
m_k = mpq(0);
@ -898,7 +904,7 @@ lia_move int_solver::create_branch_on_column(int j) {
}
bool int_solver::left_branch_is_more_narrow_than_right(unsigned j) {
switch (m_lar_solver->m_mpq_lar_core_solver.m_r_solver.m_column_types[j] ) {
switch (lra.m_mpq_lar_core_solver.m_r_solver.m_column_types[j] ) {
case column_type::fixed:
return false;
case column_type::boxed:
@ -915,14 +921,5 @@ bool int_solver::left_branch_is_more_narrow_than_right(unsigned j) {
}
}
const impq& int_solver::upper_bound(unsigned j) const {
return m_lar_solver->column_upper_bound(j);
}
bool int_solver::is_term(unsigned j) const {
return m_lar_solver->column_corresponds_to_term(j);
}
unsigned int_solver::column_count() const { return m_lar_solver->column_count(); }
}

4
src/math/lp/int_solver.h
View file

@ -39,7 +39,7 @@ class int_solver {
friend class int_cube;
public:
// fields
lar_solver *m_lar_solver;
lar_solver& lra;
unsigned m_number_of_calls;
lar_term m_t; // the term to return in the cut
mpq m_k; // the right side of the cut
@ -48,7 +48,7 @@ public:
hnf_cutter m_hnf_cutter;
unsigned m_hnf_cut_period;
// methods
int_solver(lar_solver* lp);
int_solver(lar_solver& lp);
// main function to check that the solution provided by lar_solver is valid for integral values,
// or provide a way of how it can be adjusted.

2
src/smt/theory_lra.cpp
View file

@ -407,7 +407,7 @@ class theory_lra::imp {
lp().settings().m_int_run_gcd_test = ctx().get_fparams().m_arith_gcd_test;
lp().settings().set_random_seed(ctx().get_fparams().m_random_seed);
m_switcher.m_use_nla = m_use_nla = lpar.nla();
m_lia = alloc(lp::int_solver, m_solver.get());
m_lia = alloc(lp::int_solver, *m_solver.get());
get_one(true);
get_zero(true);
get_one(false);