mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 02:42:02 +00:00
Code Activity

merge

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-09-19 09:02:37 -07:00
parent 5bbe0508e4
commit ed19af4c4e
3 changed files with 7 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/smt/theory_lra.cpp
View file

@ -1629,6 +1629,7 @@ public:
expr_ref term2expr(lp::lar_term const& term) { expr_ref term2expr(lp::lar_term const& term) {
expr_ref t(m); expr_ref t(m);
expr_ref_vector ts(m); expr_ref_vector ts(m);
ts.push_back(a.mk_numeral(term.m_v, true));
for (auto const& p : term) { for (auto const& p : term) {
lp::var_index wi = p.var(); lp::var_index wi = p.var();
if (m_solver->is_term(wi)) { if (m_solver->is_term(wi)) {

4
src/util/lp/gomory.cpp
View file

@ -168,11 +168,13 @@ public:
mpq one_min_f0 = 1 - f0; mpq one_min_f0 = 1 - f0;
for (const auto & p : m_row) { for (const auto & p : m_row) {
unsigned j = p.var(); unsigned j = p.var();
#if 1
if (column_is_fixed(j)) { if (column_is_fixed(j)) {
m_ex.push_justification(column_lower_bound_constraint(j)); m_ex.push_justification(column_lower_bound_constraint(j));
m_ex.push_justification(column_upper_bound_constraint(j)); m_ex.push_justification(column_upper_bound_constraint(j));
continue; continue;
} }
#endif
if (j == m_inf_col) { if (j == m_inf_col) {
lp_assert(p.coeff() == one_of_type<mpq>()); lp_assert(p.coeff() == one_of_type<mpq>());
TRACE("gomory_cut_detail", tout << "seeing basic var";); TRACE("gomory_cut_detail", tout << "seeing basic var";);
@ -194,7 +196,7 @@ public:
adjust_term_and_k_for_some_ints_case_gomory(lcm_den); adjust_term_and_k_for_some_ints_case_gomory(lcm_den);
lp_assert(m_int_solver.current_solution_is_inf_on_cut()); lp_assert(m_int_solver.current_solution_is_inf_on_cut());
m_int_solver.m_lar_solver->subs_term_columns(m_t, m_k); m_int_solver.m_lar_solver->subs_term_columns(m_t, m_k);
TRACE("gomory_cut", tout<<"gomory cut:"; m_int_solver.m_lar_solver->print_term(m_t, tout); tout << " <= " << m_k << std::endl;); TRACE("gomory_cut", tout<<"gomory cut:"; m_int_solver.m_lar_solver->print_term(m_t, tout) << " <= " << m_k << std::endl;);
return lia_move::cut; return lia_move::cut;
} }
imp(lar_term & t, mpq & k, explanation& ex, unsigned basic_inf_int_j, const row_strip<mpq>& row, const int_solver& int_slv ) : imp(lar_term & t, mpq & k, explanation& ex, unsigned basic_inf_int_j, const row_strip<mpq>& row, const int_solver& int_slv ) :

6
src/util/lp/lp_core_solver_base.h
View file

@ -577,7 +577,7 @@ public:
} }
void print_column_info(unsigned j, std::ostream & out) const { void print_column_info(unsigned j, std::ostream & out) const {
out << "j = " << j << ", name = "<< column_name(j); out << "j = " << j << ",\tname = "<< column_name(j) << "\t";
switch (m_column_types[j]) { switch (m_column_types[j]) {
case column_type::fixed: case column_type::fixed:
case column_type::boxed: case column_type::boxed:
@ -596,11 +596,11 @@ public:
lp_assert(false); lp_assert(false);
} }
// out << "basis heading = " << m_basis_heading[j] << std::endl; // out << "basis heading = " << m_basis_heading[j] << std::endl;
out << " x = " << m_x[j]; out << "\tx = " << m_x[j];
if (m_basis_heading[j] >= 0) if (m_basis_heading[j] >= 0)
out << " base\n"; out << " base\n";
else else
out << " nbas\n"; out << " \n";
} }
bool column_is_free(unsigned j) const { return this->m_column_type[j] == free; } bool column_is_free(unsigned j) const { return this->m_column_type[j] == free; }