mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 09:34:08 +00:00
Code Activity

introduce ul_pair associated_with_row

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-05-05 15:59:09 -07:00
parent d20259b57a
commit f2449df06e
3 changed files with 21 additions and 16 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1365,7 +1365,7 @@ void lar_solver::pop() {
}
bool lar_solver::column_represents_row_in_tableau(unsigned j) {
return m_columns_to_ul_pairs()[j].m_i != UINT_MAX;
return m_columns_to_ul_pairs()[j].associated_with_row();
}
void lar_solver::make_sure_that_the_bottom_right_elem_not_zero_in_tableau(unsigned i, unsigned j) {
@ -1602,7 +1602,7 @@ var_index lar_solver::add_var(unsigned ext_j, bool is_int) {
return local_j;
lp_assert(m_columns_to_ul_pairs.size() == A_r().column_count());
local_j = A_r().column_count();
m_columns_to_ul_pairs.push_back(ul_pair(UINT_MAX));
m_columns_to_ul_pairs.push_back(ul_pair(false)); // not associated with a row
while (m_usage_in_terms.size() <= ext_j) {
m_usage_in_terms.push_back(0);
}
@ -1628,7 +1628,7 @@ void lar_solver::add_non_basic_var_to_core_fields(unsigned ext_j, bool is_int) {
register_new_ext_var_index(ext_j, is_int);
m_mpq_lar_core_solver.m_column_types.push_back(column_type::free_column);
m_columns_with_changed_bound.increase_size_by_one();
add_new_var_to_core_fields_for_mpq(false);
add_new_var_to_core_fields_for_mpq(false); // false for not adding a row
if (use_lu())
add_new_var_to_core_fields_for_doubles(false);
}
@ -1759,7 +1759,7 @@ void lar_solver::add_row_from_term_no_constraint(const lar_term * term, unsigned
register_new_ext_var_index(term_ext_index, term_is_int(term));
// j will be a new variable
unsigned j = A_r().column_count();
ul_pair ul(j);
ul_pair ul(true); // to mark this column as associated_with_row
m_columns_to_ul_pairs.push_back(ul);
add_basic_var_to_core_fields();
if (use_tableau()) {

27
src/math/lp/ul_pair.h
View file

@ -50,12 +50,12 @@ inline bool compare(const std::pair<mpq, var_index> & a, const std::pair<mpq, va
class ul_pair {
constraint_index m_lower_bound_witness;
constraint_index m_upper_bound_witness;
bool m_associated_with_row;
public:
constraint_index& lower_bound_witness() {return m_lower_bound_witness;}
constraint_index lower_bound_witness() const {return m_lower_bound_witness;}
constraint_index& upper_bound_witness() { return m_upper_bound_witness;}
constraint_index upper_bound_witness() const {return m_upper_bound_witness;}
row_index m_i;
bool operator!=(const ul_pair & p) const {
return !(*this == p);
}
@ -63,19 +63,24 @@ public:
bool operator==(const ul_pair & p) const {
return m_lower_bound_witness == p.m_lower_bound_witness
&& m_upper_bound_witness == p.m_upper_bound_witness &&
m_i == p.m_i;
m_associated_with_row == p.m_associated_with_row;
}
// empty constructor
ul_pair() :
m_lower_bound_witness(static_cast<constraint_index>(-1)),
m_upper_bound_witness(static_cast<constraint_index>(-1)),
m_i(static_cast<row_index>(-1))
{}
ul_pair(row_index ri) :
m_lower_bound_witness(static_cast<constraint_index>(-1)),
m_upper_bound_witness(static_cast<constraint_index>(-1)),
m_i(ri) {}
ul_pair(const ul_pair & o): m_lower_bound_witness(o.m_lower_bound_witness), m_upper_bound_witness(o.m_upper_bound_witness), m_i(o.m_i) {}
m_lower_bound_witness(UINT_MAX),
m_upper_bound_witness(UINT_MAX),
m_associated_with_row(false) {}
ul_pair(bool associated_with_row) :
m_lower_bound_witness(UINT_MAX),
m_upper_bound_witness(UINT_MAX),
m_associated_with_row(associated_with_row) {}
ul_pair(const ul_pair & o):
m_lower_bound_witness(o.m_lower_bound_witness),
m_upper_bound_witness(o.m_upper_bound_witness),
m_associated_with_row(o.m_associated_with_row) {}
bool associated_with_row() const { return m_associated_with_row; }
};
}

2
src/smt/params/smt_params_helper.pyg
View file

@ -41,7 +41,7 @@ def_module_params(module_name='smt',
('bv.reflect', BOOL, True, 'create enode for every bit-vector term'),
('bv.enable_int2bv', BOOL, True, 'enable support for int2bv and bv2int operators'),
('arith.random_initial_value', BOOL, False, 'use random initial values in the simplex-based procedure for linear arithmetic'),
('arith.solver', UINT, 2, 'arithmetic solver: 0 - no solver, 1 - bellman-ford based solver (diff. logic only), 2 - simplex based solver, 3 - floyd-warshall based solver (diff. logic only) and no theory combination 4 - utvpi, 5 - infinitary lra, 6 - lra solver'),
('arith.solver', UINT, 6, 'arithmetic solver: 0 - no solver, 1 - bellman-ford based solver (diff. logic only), 2 - simplex based solver, 3 - floyd-warshall based solver (diff. logic only) and no theory combination 4 - utvpi, 5 - infinitary lra, 6 - lra solver'),
('arith.nl', BOOL, True, '(incomplete) nonlinear arithmetic support based on Groebner basis and interval propagation, relevant only if smt.arith.solver=2'),
('arith.nl.gb', BOOL, True, 'groebner Basis computation, this option is ignored when arith.nl=false, relevant only if smt.arith.solver=2'),
('arith.nl.branching', BOOL, True, 'branching on integer variables in non linear clusters, relevant only if smt.arith.solver=2'),