mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
isolate constraints in a constraint_set
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
4535228fe2
commit
a59745c2f2
|
|
@ -238,7 +238,7 @@ lia_move int_solver::find_cube() {
|
|||
TRACE("cube",
|
||||
for (unsigned j = 0; j < m_lar_solver->A_r().column_count(); j++)
|
||||
display_column(tout, j);
|
||||
m_lar_solver->print_constraints(tout);
|
||||
tout << m_lar_solver->constraints();
|
||||
);
|
||||
|
||||
m_lar_solver->push();
|
||||
|
|
@ -357,9 +357,9 @@ 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->print_constraint(i, tout);
|
||||
m_lar_solver->constraints().display(tout, i);
|
||||
}
|
||||
m_lar_solver->print_constraints(tout);
|
||||
tout << m_lar_solver->constraints();
|
||||
);
|
||||
#ifdef Z3DEBUG
|
||||
vector<mpq> x0 = m_hnf_cutter.transform_to_local_columns(m_lar_solver->m_mpq_lar_core_solver.m_r_x);
|
||||
|
|
@ -373,7 +373,7 @@ lia_move int_solver::make_hnf_cut() {
|
|||
m_lar_solver->print_term(m_t, tout << "cut:");
|
||||
tout << " <= " << m_k << std::endl;
|
||||
for (unsigned i : m_hnf_cutter.constraints_for_explanation()) {
|
||||
m_lar_solver->print_constraint(i, tout);
|
||||
m_lar_solver->constraints().display(tout, i);
|
||||
}
|
||||
);
|
||||
lp_assert(current_solution_is_inf_on_cut());
|
||||
|
|
|
|||
|
|
@ -19,14 +19,17 @@ Revision History:
|
|||
--*/
|
||||
|
||||
#pragma once
|
||||
#include "util/vector.h"
|
||||
#include <utility>
|
||||
#include <unordered_map>
|
||||
#include <string>
|
||||
#include <algorithm>
|
||||
|
||||
#include "util/vector.h"
|
||||
#include "util/region.h"
|
||||
#include "math/lp/lp_utils.h"
|
||||
#include "math/lp/ul_pair.h"
|
||||
#include "math/lp/lar_term.h"
|
||||
#include "math/lp/column_namer.h"
|
||||
#include "math/lp/stacked_value.h"
|
||||
namespace lp {
|
||||
inline lconstraint_kind flip_kind(lconstraint_kind t) {
|
||||
return static_cast<lconstraint_kind>( - static_cast<int>(t));
|
||||
|
|
@ -57,8 +60,9 @@ struct lar_base_constraint {
|
|||
virtual mpq get_free_coeff_of_left_side() const { return zero_of_type<mpq>();}
|
||||
};
|
||||
|
||||
struct lar_var_constraint: public lar_base_constraint {
|
||||
class lar_var_constraint: public lar_base_constraint {
|
||||
unsigned m_j;
|
||||
public:
|
||||
vector<std::pair<mpq, var_index>> coeffs() const override {
|
||||
vector<std::pair<mpq, var_index>> ret;
|
||||
ret.push_back(std::make_pair(one_of_type<mpq>(), m_j));
|
||||
|
|
@ -69,32 +73,136 @@ struct lar_var_constraint: public lar_base_constraint {
|
|||
};
|
||||
|
||||
|
||||
struct lar_term_constraint: public lar_base_constraint {
|
||||
class lar_term_constraint: public lar_base_constraint {
|
||||
const lar_term * m_term;
|
||||
vector<std::pair<mpq, var_index>> coeffs() const override {
|
||||
return m_term->coeffs_as_vector();
|
||||
}
|
||||
public:
|
||||
vector<std::pair<mpq, var_index>> coeffs() const override { return m_term->coeffs_as_vector(); }
|
||||
unsigned size() const override { return m_term->size();}
|
||||
lar_term_constraint(const lar_term *t, lconstraint_kind kind, const mpq& right_side) : lar_base_constraint(kind, right_side), m_term(t) { }
|
||||
// mpq get_free_coeff_of_left_side() const override { return m_term->m_v;}
|
||||
|
||||
};
|
||||
|
||||
|
||||
class lar_constraint : public lar_base_constraint {
|
||||
class constraint_set {
|
||||
region m_region;
|
||||
column_namer& m_namer;
|
||||
vector<lar_base_constraint*> m_constraints;
|
||||
stacked_value<unsigned> m_constraint_count;
|
||||
|
||||
constraint_index add(lar_base_constraint* c) {
|
||||
constraint_index ci = m_constraints.size();
|
||||
m_constraints.push_back(c);
|
||||
return ci;
|
||||
}
|
||||
|
||||
std::ostream& print_left_side_of_constraint(const lar_base_constraint & c, std::ostream & out) const {
|
||||
m_namer.print_linear_combination_of_column_indices(c.coeffs(), out);
|
||||
mpq free_coeff = c.get_free_coeff_of_left_side();
|
||||
if (!is_zero(free_coeff))
|
||||
out << " + " << free_coeff;
|
||||
return out;
|
||||
}
|
||||
|
||||
std::ostream& print_left_side_of_constraint_indices_only(const lar_base_constraint & c, std::ostream & out) const {
|
||||
print_linear_combination_of_column_indices_only(c.coeffs(), out);
|
||||
mpq free_coeff = c.get_free_coeff_of_left_side();
|
||||
if (!is_zero(free_coeff))
|
||||
out << " + " << free_coeff;
|
||||
return out;
|
||||
}
|
||||
|
||||
std::ostream& print_left_side_of_constraint(const lar_base_constraint & c, std::function<std::string (unsigned)>& var_str, std::ostream & out) const {
|
||||
print_linear_combination_customized(c.coeffs(), var_str, out);
|
||||
mpq free_coeff = c.get_free_coeff_of_left_side();
|
||||
if (!is_zero(free_coeff))
|
||||
out << " + " << free_coeff;
|
||||
return out;
|
||||
}
|
||||
|
||||
std::ostream& out_of_bounds(std::ostream& out, constraint_index ci) const {
|
||||
return out << "constraint " << T_to_string(ci) << " is not found" << std::endl;
|
||||
}
|
||||
|
||||
public:
|
||||
vector<std::pair<mpq, var_index>> m_coeffs;
|
||||
lar_constraint(const vector<std::pair<mpq, var_index>> & left_side, lconstraint_kind kind, const mpq & right_side)
|
||||
: lar_base_constraint(kind, right_side), m_coeffs(left_side) {}
|
||||
constraint_set(column_namer& cn):
|
||||
m_namer(cn) {}
|
||||
|
||||
~constraint_set() {
|
||||
for (auto* c : m_constraints)
|
||||
c->~lar_base_constraint();
|
||||
}
|
||||
|
||||
void push() {
|
||||
m_constraint_count = m_constraints.size();
|
||||
m_constraint_count.push();
|
||||
m_region.push_scope();
|
||||
}
|
||||
|
||||
void pop(unsigned k) {
|
||||
m_constraint_count.pop(k);
|
||||
for (unsigned i = m_constraints.size(); i-- > m_constraint_count; )
|
||||
m_constraints[i]->~lar_base_constraint();
|
||||
m_constraints.shrink(m_constraint_count);
|
||||
m_region.pop_scope(k);
|
||||
}
|
||||
|
||||
constraint_index add_var_constraint(var_index j, lconstraint_kind k, mpq const& rhs) {
|
||||
return add(new (m_region) lar_var_constraint(j, k, rhs));
|
||||
}
|
||||
|
||||
constraint_index add_term_constraint(const lar_term* t, lconstraint_kind k, mpq const& rhs) {
|
||||
return add(new (m_region) lar_term_constraint(t, k, rhs));
|
||||
}
|
||||
|
||||
lar_base_constraint const& operator[](constraint_index ci) const { return *m_constraints[ci]; }
|
||||
|
||||
// TBD: would like to make this opaque
|
||||
// and expose just active constraints
|
||||
// constraints need not be active.
|
||||
unsigned size() const { return m_constraints.size(); }
|
||||
vector<lar_base_constraint*>::const_iterator begin() const { return m_constraints.begin(); }
|
||||
vector<lar_base_constraint*>::const_iterator end() const { return m_constraints.end(); }
|
||||
|
||||
std::ostream& display(std::ostream& out) const {
|
||||
out << "number of constraints = " << m_constraints.size() << std::endl;
|
||||
for (auto const* c : *this) {
|
||||
display(out, *c);
|
||||
}
|
||||
return out;
|
||||
}
|
||||
|
||||
std::ostream& display(std::ostream& out, constraint_index ci) const {
|
||||
return (ci >= m_constraints.size()) ? out_of_bounds(out, ci) : display(out, (*this)[ci]);
|
||||
}
|
||||
|
||||
std::ostream& display(std::ostream& out, lar_base_constraint const& c) const {
|
||||
print_left_side_of_constraint(c, out);
|
||||
return out << " " << lconstraint_kind_string(c.m_kind) << " " << c.m_right_side << std::endl;
|
||||
}
|
||||
|
||||
std::ostream& display_indices_only(std::ostream& out, constraint_index ci) const {
|
||||
return (ci >= m_constraints.size()) ? out_of_bounds(out, ci) : display_indices_only(out, (*this)[ci]);
|
||||
}
|
||||
|
||||
std::ostream& display_indices_only(std::ostream& out, lar_base_constraint const& c) const {
|
||||
print_left_side_of_constraint_indices_only(c, out);
|
||||
return out << " " << lconstraint_kind_string(c.m_kind) << " " << c.m_right_side << std::endl;
|
||||
}
|
||||
|
||||
std::ostream& display(std::ostream& out, std::function<std::string (unsigned)> var_str, constraint_index ci) const {
|
||||
return (ci >= m_constraints.size()) ? out_of_bounds(out, ci) : display(out, var_str, (*this)[ci]);
|
||||
}
|
||||
|
||||
std::ostream& display(std::ostream& out, std::function<std::string (unsigned)>& var_str, lar_base_constraint const& c) const {
|
||||
print_left_side_of_constraint(c, var_str, out);
|
||||
return out << " " << lconstraint_kind_string(c.m_kind) << " " << c.m_right_side << std::endl;
|
||||
}
|
||||
|
||||
|
||||
|
||||
lar_constraint(const lar_base_constraint & c) {
|
||||
lp_assert(false); // should not be called : todo!
|
||||
}
|
||||
|
||||
unsigned size() const override {
|
||||
return static_cast<unsigned>(m_coeffs.size());
|
||||
}
|
||||
|
||||
vector<std::pair<mpq, var_index>> coeffs() const override { return m_coeffs; }
|
||||
};
|
||||
|
||||
inline std::ostream& operator<<(std::ostream& out, constraint_set const& cs) {
|
||||
return cs.display(out);
|
||||
}
|
||||
|
||||
}
|
||||
|
|
|
|||
|
|
@ -6,13 +6,6 @@
|
|||
|
||||
namespace lp {
|
||||
|
||||
unsigned lar_solver::constraint_count() const {
|
||||
return m_constraints.size();
|
||||
}
|
||||
const lar_base_constraint& lar_solver::get_constraint(unsigned ci) const {
|
||||
return *(m_constraints[ci]);
|
||||
}
|
||||
|
||||
////////////////// methods ////////////////////////////////
|
||||
static_matrix<mpq, numeric_pair<mpq>> & lar_solver::A_r() { return m_mpq_lar_core_solver.m_r_A;}
|
||||
static_matrix<mpq, numeric_pair<mpq>> const & lar_solver::A_r() const { return m_mpq_lar_core_solver.m_r_A;}
|
||||
|
|
@ -34,6 +27,7 @@ lar_solver::lar_solver() : m_status(lp_status::UNKNOWN),
|
|||
m_terms_start_index(1000000),
|
||||
m_var_register(0),
|
||||
m_term_register(m_terms_start_index),
|
||||
m_constraints(*this),
|
||||
m_need_register_terms(false)
|
||||
{}
|
||||
|
||||
|
|
@ -47,8 +41,6 @@ bool lar_solver::get_track_pivoted_rows() const {
|
|||
|
||||
|
||||
lar_solver::~lar_solver(){
|
||||
for (auto c : m_constraints)
|
||||
delete c;
|
||||
|
||||
for (auto t : m_terms)
|
||||
delete t;
|
||||
|
|
@ -107,7 +99,7 @@ bool lar_solver::implied_bound_is_correctly_explained(implied_bound const & be,
|
|||
for (auto & it : explanation) {
|
||||
mpq coeff = it.first;
|
||||
constraint_index con_ind = it.second;
|
||||
const auto & constr = *m_constraints[con_ind];
|
||||
const auto & constr = m_constraints[con_ind];
|
||||
lconstraint_kind kind = coeff.is_pos() ? constr.m_kind : flip_kind(constr.m_kind);
|
||||
register_in_map(coeff_map, constr, coeff);
|
||||
if (kind == GT || kind == LT)
|
||||
|
|
@ -329,6 +321,7 @@ vector<unsigned> lar_solver::get_list_of_all_var_indices() const {
|
|||
ret.push_back(j);
|
||||
return ret;
|
||||
}
|
||||
|
||||
void lar_solver::push() {
|
||||
m_simplex_strategy = m_settings.simplex_strategy();
|
||||
m_simplex_strategy.push();
|
||||
|
|
@ -337,8 +330,7 @@ void lar_solver::push() {
|
|||
m_mpq_lar_core_solver.push();
|
||||
m_term_count = m_terms.size();
|
||||
m_term_count.push();
|
||||
m_constraint_count = m_constraints.size();
|
||||
m_constraint_count.push();
|
||||
m_constraints.push();
|
||||
}
|
||||
|
||||
void lar_solver::clean_popped_elements(unsigned n, int_set& set) {
|
||||
|
|
@ -383,11 +375,7 @@ void lar_solver::pop(unsigned k) {
|
|||
(!use_tableau()) || m_mpq_lar_core_solver.m_r_solver.reduced_costs_are_correct_tableau());
|
||||
|
||||
|
||||
m_constraint_count.pop(k);
|
||||
for (unsigned i = m_constraint_count; i < m_constraints.size(); i++)
|
||||
delete m_constraints[i];
|
||||
|
||||
m_constraints.resize(m_constraint_count);
|
||||
m_constraints.pop(k);
|
||||
m_term_count.pop(k);
|
||||
for (unsigned i = m_term_count; i < m_terms.size(); i++) {
|
||||
if (m_need_register_terms)
|
||||
|
|
@ -402,14 +390,7 @@ void lar_solver::pop(unsigned k) {
|
|||
lp_assert((!m_settings.use_tableau()) || m_mpq_lar_core_solver.m_r_solver.reduced_costs_are_correct_tableau());
|
||||
set_status(lp_status::UNKNOWN);
|
||||
}
|
||||
|
||||
vector<constraint_index> lar_solver::get_all_constraint_indices() const {
|
||||
vector<constraint_index> ret;
|
||||
constraint_index i = 0;
|
||||
while ( i < m_constraints.size())
|
||||
ret.push_back(i++);
|
||||
return ret;
|
||||
}
|
||||
|
||||
|
||||
bool lar_solver::maximize_term_on_tableau(const lar_term & term,
|
||||
impq &term_max) {
|
||||
|
|
@ -934,9 +915,6 @@ bool lar_solver::var_is_registered(var_index vj) const {
|
|||
return true;
|
||||
}
|
||||
|
||||
unsigned lar_solver::constraint_stack_size() const {
|
||||
return m_constraint_count.stack_size();
|
||||
}
|
||||
|
||||
void lar_solver::fill_last_row_of_A_r(static_matrix<mpq, numeric_pair<mpq>> & A, const lar_term * ls) {
|
||||
lp_assert(A.row_count() > 0);
|
||||
|
|
@ -1003,16 +981,18 @@ bool lar_solver::all_constraints_hold() const {
|
|||
std::unordered_map<var_index, mpq> var_map;
|
||||
get_model_do_not_care_about_diff_vars(var_map);
|
||||
|
||||
for (unsigned i = 0; i < m_constraints.size(); i++) {
|
||||
if (!constraint_holds(*m_constraints[i], var_map)) {
|
||||
unsigned i = 0;
|
||||
for (auto const* c : m_constraints) {
|
||||
if (!constraint_holds(*c, var_map)) {
|
||||
TRACE("lar_solver",
|
||||
tout << "i = " << i << "; ";
|
||||
print_constraint(m_constraints[i], tout) << "\n";
|
||||
for(auto p : m_constraints[i]->coeffs()) {
|
||||
m_constraints.display(tout, *c) << "\n";
|
||||
for (auto p : c->coeffs()) {
|
||||
m_mpq_lar_core_solver.m_r_solver.print_column_info(p.second, tout);
|
||||
});
|
||||
return false;
|
||||
}
|
||||
++i;
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
|
@ -1038,8 +1018,8 @@ bool lar_solver::the_relations_are_of_same_type(const vector<std::pair<mpq, unsi
|
|||
mpq coeff = it.first;
|
||||
constraint_index con_ind = it.second;
|
||||
lconstraint_kind kind = coeff.is_pos() ?
|
||||
m_constraints[con_ind]->m_kind :
|
||||
flip_kind(m_constraints[con_ind]->m_kind);
|
||||
m_constraints[con_ind].m_kind :
|
||||
flip_kind(m_constraints[con_ind].m_kind);
|
||||
if (kind == GT || kind == LT)
|
||||
strict = true;
|
||||
if (kind == GE || kind == GT)
|
||||
|
|
@ -1074,7 +1054,7 @@ bool lar_solver::the_left_sides_sum_to_zero(const vector<std::pair<mpq, unsigned
|
|||
mpq coeff = it.first;
|
||||
constraint_index con_ind = it.second;
|
||||
lp_assert(con_ind < m_constraints.size());
|
||||
register_in_map(coeff_map, *m_constraints[con_ind], coeff);
|
||||
register_in_map(coeff_map, m_constraints[con_ind], coeff);
|
||||
}
|
||||
|
||||
if (!coeff_map.empty()) {
|
||||
|
|
@ -1084,17 +1064,6 @@ bool lar_solver::the_left_sides_sum_to_zero(const vector<std::pair<mpq, unsigned
|
|||
return true;
|
||||
}
|
||||
|
||||
bool lar_solver::the_right_sides_do_not_sum_to_zero(const vector<std::pair<mpq, unsigned>> & evidence) {
|
||||
mpq ret = numeric_traits<mpq>::zero();
|
||||
for (auto & it : evidence) {
|
||||
mpq coeff = it.first;
|
||||
constraint_index con_ind = it.second;
|
||||
lp_assert(con_ind < m_constraints.size());
|
||||
const lar_constraint & constr = *m_constraints[con_ind];
|
||||
ret += constr.m_right_side * coeff;
|
||||
}
|
||||
return !numeric_traits<mpq>::is_zero(ret);
|
||||
}
|
||||
|
||||
bool lar_solver::explanation_is_correct(explanation& explanation) const {
|
||||
return true;
|
||||
|
|
@ -1139,7 +1108,7 @@ mpq lar_solver::sum_of_right_sides_of_explanation(explanation& exp) const {
|
|||
mpq coeff = it.first;
|
||||
constraint_index con_ind = it.second;
|
||||
lp_assert(con_ind < m_constraints.size());
|
||||
ret += (m_constraints[con_ind]->m_right_side - m_constraints[con_ind]->get_free_coeff_of_left_side()) * coeff;
|
||||
ret += (m_constraints[con_ind].m_right_side - m_constraints[con_ind].get_free_coeff_of_left_side()) * coeff;
|
||||
}
|
||||
return ret;
|
||||
}
|
||||
|
|
@ -1318,41 +1287,19 @@ std::string lar_solver::get_variable_name(var_index j) const {
|
|||
|
||||
// ********** print region start
|
||||
std::ostream& lar_solver::print_constraint(constraint_index ci, std::ostream & out) const {
|
||||
if (ci >= m_constraints.size()) {
|
||||
out << "constraint " << T_to_string(ci) << " is not found";
|
||||
out << std::endl;
|
||||
return out;
|
||||
}
|
||||
|
||||
return print_constraint(m_constraints[ci], out);
|
||||
return m_constraints.display(out, ci);
|
||||
}
|
||||
|
||||
std::ostream& lar_solver::print_constraint_indices_only(constraint_index ci, std::ostream & out) const {
|
||||
if (ci >= m_constraints.size()) {
|
||||
out << "constraint " << T_to_string(ci) << " is not found";
|
||||
out << std::endl;
|
||||
return out;
|
||||
}
|
||||
|
||||
return print_constraint_indices_only(m_constraints[ci], out);
|
||||
return m_constraints.display_indices_only(out, ci);
|
||||
}
|
||||
|
||||
std::ostream& lar_solver::print_constraint_indices_only_customized(constraint_index ci, std::function<std::string (unsigned)> var_str, std::ostream & out) const {
|
||||
if (ci >= m_constraints.size()) {
|
||||
out << "constraint " << T_to_string(ci) << " is not found";
|
||||
out << std::endl;
|
||||
return out;
|
||||
}
|
||||
|
||||
return print_constraint_indices_only_customized(m_constraints[ci], var_str, out);
|
||||
return m_constraints.display(out, var_str, ci);
|
||||
}
|
||||
|
||||
std::ostream& lar_solver::print_constraints(std::ostream& out) const {
|
||||
out << "number of constraints = " << m_constraints.size() << std::endl;
|
||||
for (auto c : m_constraints) {
|
||||
print_constraint(c, out);
|
||||
}
|
||||
return out;
|
||||
return out << m_constraints;
|
||||
}
|
||||
|
||||
std::ostream& lar_solver::print_terms(std::ostream& out) const {
|
||||
|
|
@ -1362,22 +1309,6 @@ std::ostream& lar_solver::print_terms(std::ostream& out) const {
|
|||
return out;
|
||||
}
|
||||
|
||||
std::ostream& lar_solver::print_left_side_of_constraint(const lar_base_constraint * c, std::ostream & out) const {
|
||||
print_linear_combination_of_column_indices(c->coeffs(), out);
|
||||
mpq free_coeff = c->get_free_coeff_of_left_side();
|
||||
if (!is_zero(free_coeff))
|
||||
out << " + " << free_coeff;
|
||||
return out;
|
||||
}
|
||||
|
||||
std::ostream& lar_solver::print_left_side_of_constraint_indices_only(const lar_base_constraint * c, std::ostream & out) const {
|
||||
print_linear_combination_of_column_indices_only(c->coeffs(), out);
|
||||
mpq free_coeff = c->get_free_coeff_of_left_side();
|
||||
if (!is_zero(free_coeff))
|
||||
out << " + " << free_coeff;
|
||||
return out;
|
||||
}
|
||||
|
||||
std::ostream& lar_solver::print_term(lar_term const& term, std::ostream & out) const {
|
||||
if (term.size() == 0){
|
||||
out << "0";
|
||||
|
|
@ -1419,21 +1350,6 @@ mpq lar_solver::get_left_side_val(const lar_base_constraint & cns, const std::u
|
|||
return ret;
|
||||
}
|
||||
|
||||
std::ostream& lar_solver::print_constraint(const lar_base_constraint * c, std::ostream & out) const {
|
||||
print_left_side_of_constraint(c, out);
|
||||
return out << " " << lconstraint_kind_string(c->m_kind) << " " << c->m_right_side << std::endl;
|
||||
}
|
||||
|
||||
std::ostream& lar_solver::print_constraint_indices_only(const lar_base_constraint * c, std::ostream & out) const {
|
||||
print_left_side_of_constraint_indices_only(c, out);
|
||||
return out << " " << lconstraint_kind_string(c->m_kind) << " " << c->m_right_side << std::endl;
|
||||
}
|
||||
|
||||
std::ostream& lar_solver::print_constraint_indices_only_customized(const lar_base_constraint * c,
|
||||
std::function<std::string (unsigned)> var_str, std::ostream & out) const {
|
||||
print_linear_combination_customized(c->coeffs(), var_str, out);
|
||||
return out << " " << lconstraint_kind_string(c->m_kind) << " " << c->m_right_side << std::endl;
|
||||
}
|
||||
|
||||
void lar_solver::fill_var_set_for_random_update(unsigned sz, var_index const * vars, vector<unsigned>& column_list) {
|
||||
for (unsigned i = 0; i < sz; i++) {
|
||||
|
|
@ -1867,15 +1783,14 @@ bool lar_solver::bound_is_integer_for_integer_column(unsigned j, const mpq & rig
|
|||
|
||||
constraint_index lar_solver::add_var_bound(var_index j, lconstraint_kind kind, const mpq & right_side) {
|
||||
TRACE("lar_solver", tout << "j = " << j << " " << lconstraint_kind_string(kind) << " " << right_side<< std::endl;);
|
||||
constraint_index ci = m_constraints.size();
|
||||
constraint_index ci;
|
||||
if (!is_term(j)) { // j is a var
|
||||
lp_assert(bound_is_integer_for_integer_column(j, right_side));
|
||||
auto vc = new lar_var_constraint(j, kind, right_side);
|
||||
m_constraints.push_back(vc);
|
||||
ci = m_constraints.add_var_constraint(j, kind, right_side);
|
||||
update_column_type_and_bound(j, kind, right_side, ci);
|
||||
}
|
||||
else {
|
||||
add_var_bound_on_constraint_for_term(j, kind, right_side, ci);
|
||||
ci = add_var_bound_on_constraint_for_term(j, kind, right_side);
|
||||
}
|
||||
lp_assert(sizes_are_correct());
|
||||
return ci;
|
||||
|
|
@ -1908,28 +1823,31 @@ void lar_solver::update_column_type_and_bound(var_index j, lconstraint_kind kind
|
|||
update_column_type_and_bound_with_no_ub(j, kind, right_side, constr_index);
|
||||
}
|
||||
|
||||
void lar_solver::add_var_bound_on_constraint_for_term(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index ci) {
|
||||
constraint_index lar_solver::add_var_bound_on_constraint_for_term(var_index j, lconstraint_kind kind, const mpq & right_side) {
|
||||
lp_assert(is_term(j));
|
||||
unsigned adjusted_term_index = adjust_term_index(j);
|
||||
// lp_assert(!term_is_int(m_terms[adjusted_term_index]) || right_side.is_int());
|
||||
unsigned term_j;
|
||||
constraint_index ci;
|
||||
if (m_var_register.external_is_used(j, term_j)) {
|
||||
m_constraints.push_back(new lar_term_constraint(m_terms[adjusted_term_index], kind, right_side));
|
||||
ci = m_constraints.add_term_constraint(m_terms[adjusted_term_index], kind, right_side);
|
||||
update_column_type_and_bound(term_j, kind, right_side, ci);
|
||||
}
|
||||
else {
|
||||
add_constraint_from_term_and_create_new_column_row(j, m_terms[adjusted_term_index], kind, right_side);
|
||||
ci = add_constraint_from_term_and_create_new_column_row(j, m_terms[adjusted_term_index], kind, right_side);
|
||||
}
|
||||
return ci;
|
||||
}
|
||||
|
||||
void lar_solver::add_constraint_from_term_and_create_new_column_row(unsigned term_j, const lar_term* term,
|
||||
constraint_index lar_solver::add_constraint_from_term_and_create_new_column_row(unsigned term_j, const lar_term* term,
|
||||
lconstraint_kind kind, const mpq & right_side) {
|
||||
|
||||
add_row_from_term_no_constraint(term, term_j);
|
||||
unsigned j = A_r().column_count() - 1;
|
||||
constraint_index ci = m_constraints.add_term_constraint(term, kind, right_side);
|
||||
update_column_type_and_bound(j, kind, right_side, m_constraints.size());
|
||||
m_constraints.push_back(new lar_term_constraint(term, kind, right_side));
|
||||
lp_assert(A_r().column_count() == m_mpq_lar_core_solver.m_r_solver.m_costs.size());
|
||||
return ci;
|
||||
}
|
||||
|
||||
void lar_solver::decide_on_strategy_and_adjust_initial_state() {
|
||||
|
|
|
|||
|
|
@ -25,15 +25,15 @@ Revision History:
|
|||
#include <unordered_map>
|
||||
#include <unordered_set>
|
||||
#include <string>
|
||||
#include "math/lp/lar_constraints.h"
|
||||
#include <functional>
|
||||
#include "math/lp/lar_core_solver.h"
|
||||
#include <algorithm>
|
||||
#include <stack>
|
||||
#include <functional>
|
||||
#include "math/lp/lar_constraints.h"
|
||||
#include "math/lp/lar_core_solver.h"
|
||||
#include "math/lp/numeric_pair.h"
|
||||
#include "math/lp/scaler.h"
|
||||
#include "math/lp/lp_primal_core_solver.h"
|
||||
#include "math/lp/random_updater.h"
|
||||
#include <stack>
|
||||
#include "math/lp/stacked_value.h"
|
||||
#include "math/lp/stacked_vector.h"
|
||||
#include "math/lp/implied_bound.h"
|
||||
|
|
@ -91,8 +91,11 @@ public:
|
|||
var_register m_var_register;
|
||||
var_register m_term_register;
|
||||
stacked_vector<ul_pair> m_columns_to_ul_pairs;
|
||||
constraint_set m_constraints;
|
||||
#if 0
|
||||
vector<lar_base_constraint*> m_constraints;
|
||||
stacked_value<unsigned> m_constraint_count;
|
||||
#endif
|
||||
// the set of column indices j such that bounds have changed for j
|
||||
int_set m_columns_with_changed_bound;
|
||||
int_set m_rows_with_changed_bounds;
|
||||
|
|
@ -112,7 +115,7 @@ public:
|
|||
unsigned terms_start_index() const { return m_terms_start_index; }
|
||||
const vector<lar_term*> & terms() const { return m_terms; }
|
||||
lar_term const& term(unsigned i) const { return *m_terms[i]; }
|
||||
const vector<lar_base_constraint*>& constraints() const {
|
||||
constraint_set const& constraints() const {
|
||||
return m_constraints;
|
||||
}
|
||||
void set_int_solver(int_solver * int_slv) {
|
||||
|
|
@ -121,8 +124,7 @@ public:
|
|||
int_solver * get_int_solver() {
|
||||
return m_int_solver;
|
||||
}
|
||||
unsigned constraint_count() const;
|
||||
const lar_base_constraint& get_constraint(unsigned ci) const;
|
||||
const lar_base_constraint& get_constraint(unsigned ci) const { return m_constraints[ci]; }
|
||||
////////////////// methods ////////////////////////////////
|
||||
static_matrix<mpq, numeric_pair<mpq>> & A_r();
|
||||
static_matrix<mpq, numeric_pair<mpq>> const & A_r() const;
|
||||
|
|
@ -204,15 +206,15 @@ public:
|
|||
void update_bound_with_no_ub_lb(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index constr_index);
|
||||
void update_bound_with_ub_no_lb(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index constr_index);
|
||||
void update_bound_with_no_ub_no_lb(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index constr_index);
|
||||
|
||||
void add_var_bound_on_constraint_for_term(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index ci);
|
||||
|
||||
constraint_index add_var_bound_on_constraint_for_term(var_index j, lconstraint_kind kind, const mpq & right_side);
|
||||
|
||||
void set_infeasible_column(unsigned j) {
|
||||
set_status(lp_status::INFEASIBLE);
|
||||
m_infeasible_column = j;
|
||||
}
|
||||
|
||||
void add_constraint_from_term_and_create_new_column_row(unsigned term_j, const lar_term* term,
|
||||
constraint_index add_constraint_from_term_and_create_new_column_row(unsigned term_j, const lar_term* term,
|
||||
lconstraint_kind kind, const mpq & right_side);
|
||||
|
||||
unsigned row_of_basic_column(unsigned) const;
|
||||
|
|
@ -342,8 +344,6 @@ public:
|
|||
|
||||
void pop(unsigned k);
|
||||
|
||||
vector<constraint_index> get_all_constraint_indices() const;
|
||||
|
||||
bool maximize_term_on_tableau(const lar_term & term,
|
||||
impq &term_max);
|
||||
|
||||
|
|
@ -432,8 +432,6 @@ public:
|
|||
|
||||
bool var_is_registered(var_index vj) const;
|
||||
|
||||
unsigned constraint_stack_size() const;
|
||||
|
||||
void fill_last_row_of_A_r(static_matrix<mpq, numeric_pair<mpq>> & A, const lar_term * ls);
|
||||
|
||||
template <typename U, typename V>
|
||||
|
|
@ -491,6 +489,7 @@ public:
|
|||
void set_variable_name(var_index vi, std::string);
|
||||
|
||||
// ********** print region start
|
||||
private:
|
||||
std::ostream& print_constraint(constraint_index ci, std::ostream & out) const;
|
||||
|
||||
std::ostream& print_constraints(std::ostream& out) const ;
|
||||
|
|
@ -500,18 +499,14 @@ public:
|
|||
std::ostream& print_constraint_indices_only_customized(constraint_index ci, std::function<std::string (unsigned)> var_str, std::ostream & out) const;
|
||||
|
||||
std::ostream& print_constraint_indices_only_customized(const lar_base_constraint * c, std::function<std::string (unsigned)> var_str, std::ostream & out) const;
|
||||
public:
|
||||
|
||||
std::ostream& print_terms(std::ostream& out) const;
|
||||
|
||||
std::ostream& print_left_side_of_constraint(const lar_base_constraint * c, std::ostream & out) const;
|
||||
|
||||
std::ostream& print_left_side_of_constraint_indices_only(const lar_base_constraint * c, std::ostream & out) const;
|
||||
|
||||
std::ostream& print_term(lar_term const& term, std::ostream & out) const;
|
||||
|
||||
static std::ostream& print_term_as_indices(lar_term const& term, std::ostream & out);
|
||||
|
||||
std::ostream& print_constraint(const lar_base_constraint * c, std::ostream & out) const;
|
||||
std::ostream& print_constraint_indices_only(const lar_base_constraint * c, std::ostream & out) const;
|
||||
|
||||
std::ostream& print_implied_bound(const implied_bound& be, std::ostream & out) const;
|
||||
|
|
|
|||
|
|
@ -286,9 +286,7 @@ std::ostream& core::print_explanation(const lp::explanation& exp, std::ostream&
|
|||
unsigned i = 0;
|
||||
for (auto &p : exp) {
|
||||
out << "(" << p.second << ")";
|
||||
m_lar_solver.print_constraint_indices_only_customized(p.second,
|
||||
[this](lpvar j) { return var_str(j);},
|
||||
out);
|
||||
m_lar_solver.constraints().display(out, [this](lpvar j) { return var_str(j);}, p.second);
|
||||
if (++i < exp.size())
|
||||
out << " ";
|
||||
}
|
||||
|
|
@ -520,8 +518,8 @@ void core:: fill_explanation_and_lemma_sign(const monic& a, const monic & b, rat
|
|||
TRACE("nla_solver",
|
||||
tout << "used constraints: ";
|
||||
for (auto &p : current_expl())
|
||||
m_lar_solver.print_constraint(p.second, tout); tout << "\n";
|
||||
);
|
||||
m_lar_solver.constraints().display(tout, p.second); tout << "\n";
|
||||
);
|
||||
SASSERT(current_ineqs().size() == 0);
|
||||
mk_ineq(rational(1), a.var(), -sign, b.var(), llc::EQ, rational::zero());
|
||||
TRACE("nla_solver", print_lemma(tout););
|
||||
|
|
@ -1258,7 +1256,7 @@ bool core::done() const {
|
|||
}
|
||||
|
||||
lbool core::incremental_linearization(bool constraint_derived) {
|
||||
TRACE("nla_solver_details", print_terms(tout); m_lar_solver.print_constraints(tout););
|
||||
TRACE("nla_solver_details", print_terms(tout); tout << m_lar_solver.constraints(););
|
||||
for (int search_level = 0; search_level < 3 && !done(); search_level++) {
|
||||
TRACE("nla_solver", tout << "constraint_derived = " << constraint_derived << ", search_level = " << search_level << "\n";);
|
||||
if (search_level == 0) {
|
||||
|
|
|
|||
|
|
@ -92,7 +92,7 @@ typedef nla::variable_map_type variable_map_type;
|
|||
vector<nlsat::assumption, false> core;
|
||||
|
||||
// add linear inequalities from lra_solver
|
||||
for (unsigned i = 0; i < s.constraint_count(); ++i) {
|
||||
for (unsigned i = 0; i < s.constraints().size(); ++i) {
|
||||
add_constraint(i);
|
||||
}
|
||||
|
||||
|
|
@ -154,7 +154,7 @@ typedef nla::variable_map_type variable_map_type;
|
|||
}
|
||||
|
||||
void add_constraint(unsigned idx) {
|
||||
auto& c = s.get_constraint(idx);
|
||||
auto& c = s.constraints()[idx];
|
||||
auto& pm = m_nlsat->pm();
|
||||
auto k = c.m_kind;
|
||||
auto rhs = c.m_right_side;
|
||||
|
|
|
|||
|
|
@ -841,7 +841,7 @@ class theory_lra::imp {
|
|||
m_constraint_sources.setx(index, inequality_source, null_source);
|
||||
m_inequalities.setx(index, lit, null_literal);
|
||||
++m_stats.m_add_rows;
|
||||
TRACE("arith", lp().print_constraint(index, tout) << " m_stats.m_add_rows = " << m_stats.m_add_rows << "\n";);
|
||||
TRACE("arith", lp().constraints().display(tout, index) << " m_stats.m_add_rows = " << m_stats.m_add_rows << "\n";);
|
||||
}
|
||||
|
||||
void add_def_constraint(lp::constraint_index index) {
|
||||
|
|
@ -1288,7 +1288,7 @@ public:
|
|||
add_def_constraint(lp().add_var_bound(register_theory_var_in_lar_solver(v), lp::GE, rational::zero()));
|
||||
add_def_constraint(lp().add_var_bound(register_theory_var_in_lar_solver(v), lp::LT, abs(r)));
|
||||
SASSERT(!is_infeasible());
|
||||
TRACE("arith", lp().print_constraints(tout << term << "\n"););
|
||||
TRACE("arith", tout << term << "\n" << lp().constraints(););
|
||||
}
|
||||
|
||||
void mk_idiv_mod_axioms(expr * p, expr * q) {
|
||||
|
|
@ -2029,7 +2029,7 @@ public:
|
|||
}
|
||||
|
||||
expr_ref constraint2fml(lp::constraint_index ci) {
|
||||
lp::lar_base_constraint const& c = *lp().constraints()[ci];
|
||||
lp::lar_base_constraint const& c = lp().constraints()[ci];
|
||||
expr_ref fml(m);
|
||||
expr_ref_vector ts(m);
|
||||
rational rhs = c.m_right_side;
|
||||
|
|
@ -2063,7 +2063,7 @@ public:
|
|||
}
|
||||
}
|
||||
for (auto const& ev : ex) {
|
||||
lp().print_constraint(ev.second, out << ev.first << ": ");
|
||||
lp().constraints().display(out << ev.first << ": ", ev.second);
|
||||
}
|
||||
expr_ref_vector fmls(m);
|
||||
for (auto const& ev : ex) {
|
||||
|
|
@ -3242,7 +3242,7 @@ public:
|
|||
}
|
||||
|
||||
lbool make_feasible() {
|
||||
TRACE("pcs", lp().print_constraints(tout););
|
||||
TRACE("pcs", tout << lp().constraints(););
|
||||
auto status = lp().find_feasible_solution();
|
||||
TRACE("arith_verbose", display(tout););
|
||||
switch (status) {
|
||||
|
|
@ -3787,7 +3787,7 @@ public:
|
|||
|
||||
void display(std::ostream & out) {
|
||||
if (m_solver) {
|
||||
lp().print_constraints(out);
|
||||
out << lp().constraints();
|
||||
lp().print_terms(out);
|
||||
// the tableau
|
||||
auto pp = lp ::core_solver_pretty_printer<lp::mpq, lp::impq>(
|
||||
|
|
@ -3842,7 +3842,7 @@ public:
|
|||
}
|
||||
}
|
||||
for (auto const& ev : evidence) {
|
||||
lp().print_constraint(ev.second, out << ev.first << ": ");
|
||||
lp().constraints().display(out << ev.first << ": ", ev.second);
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
|||
Loading…
Reference in a new issue