mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

track which var is an integer

Browse source 
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
This commit is contained in:
Lev Nachmanson 2017-05-16 17:36:32 -07:00
parent e78a799b53
commit 7b433bee2b
5 changed files with 28 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/theory_lra.cpp
View file

@ -487,7 +487,7 @@ namespace smt {
result = m_theory_var2var_index[v];
}
if (result == UINT_MAX) {
result = m_solver->add_var(v);
result = m_solver->add_var(v, false);
m_theory_var2var_index.setx(v, result, UINT_MAX);
m_var_index2theory_var.setx(result, v, UINT_MAX);
m_var_trail.push_back(v);

15
src/util/lp/init_lar_solver.cpp
View file

@ -10,15 +10,15 @@ bool lar_solver::strategy_is_undecided() const {
return m_settings.simplex_strategy() == simplex_strategy_enum::undecided;
}
var_index lar_solver::add_var(unsigned ext_j) {
var_index lar_solver::add_var(unsigned ext_j, bool is_integer) {
var_index i;
lean_assert (ext_j < m_terms_start_index);
if (ext_j >= m_terms_start_index)
throw 0; // todo : what is the right way to exit?
if (try_get_val(m_ext_vars_to_columns, ext_j, i)) {
return i;
auto it = m_ext_vars_to_columns.find(ext_j);
if (it != m_ext_vars_to_columns.end()) {
return it->second.ext_j();
}
lean_assert(m_vars_to_ul_pairs.size() == A_r().column_count());
i = A_r().column_count();
@ -31,7 +31,7 @@ var_index lar_solver::add_var(unsigned ext_j) {
void lar_solver::register_new_ext_var_index(unsigned ext_v) {
lean_assert(!contains(m_ext_vars_to_columns, ext_v));
unsigned j = static_cast<unsigned>(m_ext_vars_to_columns.size());
m_ext_vars_to_columns[ext_v] = j;
m_ext_vars_to_columns.insert(std::make_pair(ext_v, ext_var_info(j)));
lean_assert(m_columns_to_ext_vars_or_term_indices.size() == j);
m_columns_to_ext_vars_or_term_indices.push_back(ext_v);
}
@ -190,8 +190,9 @@ void lar_solver::update_column_type_and_bound(var_index j, lconstraint_kind kind
void lar_solver::add_var_bound_on_constraint_for_term(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index ci) {
lean_assert(is_term(j));
unsigned adjusted_term_index = adjust_term_index(j);
unsigned term_j;
if (try_get_val(m_ext_vars_to_columns, j, term_j)) {
auto it = m_ext_vars_to_columns.find(j);
if (it != m_ext_vars_to_columns.end()) {
unsigned term_j = it->second.ext_j();
mpq rs = right_side - m_orig_terms[adjusted_term_index]->m_v;
m_constraints.push_back(new lar_term_constraint(m_orig_terms[adjusted_term_index], kind, right_side));
update_column_type_and_bound(term_j, kind, rs, ci);

8
src/util/lp/lar_solver.cpp
View file

@ -224,14 +224,18 @@ const lar_base_constraint& lar_solver::get_constraint(unsigned ci) const {
int j_sign = (ib.m_coeff_before_j_is_pos ? 1 :-1) * bound_sign;
unsigned m_j = ib.m_j;
if (is_term(m_j)) {
m_j = m_ext_vars_to_columns[m_j];
auto it = m_ext_vars_to_columns.find(m_j);
lean_assert(it != m_ext_vars_to_columns.end());
m_j = it->second.ext_j();
}
for (auto const& r : A_r().m_rows[i]) {
unsigned j = r.m_j;
mpq const& a = r.get_val();
if (j == m_j) continue;
if (is_term(j)) {
j = m_ext_vars_to_columns[j];
auto it = m_ext_vars_to_columns.find(j);
lean_assert(it != m_ext_vars_to_columns.end());
j = it->second.ext_j();
}
int a_sign = is_pos(a)? 1: -1;
int sign = j_sign * a_sign;

13
src/util/lp/lar_solver.h
View file

@ -35,11 +35,20 @@
namespace lean {
class lar_solver : public column_namer {
class ext_var_info {
unsigned m_ext_j; // the external index
bool m_is_integer;
public:
ext_var_info(unsigned j): ext_var_info(j, false) {}
ext_var_info(unsigned j , bool is_int) : m_ext_j(j), m_is_integer(is_int) {}
unsigned ext_j() const { return m_ext_j;}
bool is_integer() const {return m_is_integer;}
};
//////////////////// fields //////////////////////////
lp_settings m_settings;
stacked_value<lp_status> m_status;
stacked_value<simplex_strategy_enum> m_simplex_strategy;
std::unordered_map<unsigned, var_index> m_ext_vars_to_columns;
std::unordered_map<unsigned, ext_var_info> m_ext_vars_to_columns;
vector<unsigned> m_columns_to_ext_vars_or_term_indices;
stacked_vector<ul_pair> m_vars_to_ul_pairs;
vector<lar_base_constraint*> m_constraints;
@ -74,7 +83,7 @@ public:
// init region
bool strategy_is_undecided() const;
var_index add_var(unsigned ext_j);
var_index add_var(unsigned ext_j, bool is_integer);
void register_new_ext_var_index(unsigned ext_v);

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

@ -20,7 +20,7 @@ void quick_xplain::copy_constraint_and_add_constraint_vars(const lar_constraint&
vector < std::pair<mpq, unsigned>> ls;
for (auto & p : lar_c.get_left_side_coefficients()) {
unsigned j = p.second;
unsigned lj = m_qsol.add_var(j);
unsigned lj = m_qsol.add_var(j, false);
ls.push_back(std::make_pair(p.first, lj));
}
m_constraints_in_local_vars.push_back(lar_constraint(ls, lar_c.m_kind, lar_c.m_right_side));
@ -94,7 +94,7 @@ bool quick_xplain::is_feasible(const vector<unsigned> & x, unsigned k) const {
vector < std::pair<mpq, unsigned>> ls;
const lar_constraint & c = m_constraints_in_local_vars[i];
for (auto & p : c.get_left_side_coefficients()) {
unsigned lj = l.add_var(p.second);
unsigned lj = l.add_var(p.second, false);
ls.push_back(std::make_pair(p.first, lj));
}
l.add_constraint(ls, c.m_kind, c.m_right_side);