mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-11 03:33:35 +00:00
Code Activity

reuse dio branch

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-04-03 09:47:02 -07:00
parent 8d81a2dcaf
commit f85a5135c0
6 changed files with 124 additions and 29 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/math/lp/CMakeLists.txt
View file

@ -43,6 +43,8 @@ z3_add_component(lp
polynomial
nlsat
smt_params
PYG_FILES
lp_params_helper.pyg
)
include_directories(${src_SOURCE_DIR})

124
src/math/lp/dioph_eq.cpp
View file

@ -596,34 +596,63 @@ namespace lp {
};
struct protected_queue {
std::queue<unsigned> m_q;
indexed_uint_set m_in_q;
std::list<unsigned> m_q;
std::unordered_map<unsigned, std::list<unsigned>::iterator> m_positions;
bool empty() const {
return m_q.empty();
}
unsigned size() const {
return (unsigned)m_q.size();
return static_cast<unsigned>(m_q.size());
}
void push(unsigned j) {
if (m_in_q.contains(j)) return;
m_in_q.insert(j);
m_q.push(j);
if (m_positions.find(j) != m_positions.end()) return;
m_q.push_back(j);
m_positions[j] = std::prev(m_q.end());
}
unsigned pop_front() {
unsigned j = m_q.front();
m_q.pop();
SASSERT(m_in_q.contains(j));
m_in_q.remove(j);
m_q.pop_front();
m_positions.erase(j);
return j;
}
void remove(unsigned j) {
auto it = m_positions.find(j);
if (it != m_positions.end()) {
m_q.erase(it->second);
m_positions.erase(it);
}
if (!invariant()) {
throw std::runtime_error("Invariant violation in protected_queue");
}
}
bool contains(unsigned j) const {
return m_positions.find(j) != m_positions.end();
}
void reset() {
while (!m_q.empty())
m_q.pop();
m_in_q.reset();
m_q.clear();
m_positions.clear();
}
// Invariant method to ensure m_q and m_positions are aligned
bool invariant() const {
if (m_q.size() != m_positions.size())
return false;
for (auto it = m_q.begin(); it != m_q.end(); ++it) {
auto pos_it = m_positions.find(*it);
if (pos_it == m_positions.end())
return false;
if (pos_it->second != it)
return false;
}
return true;
}
};
@ -750,6 +779,12 @@ namespace lp {
std_vector<variable_branch_stats> m_branch_stats;
std_vector<branch> m_branch_stack;
std_vector<constraint_index> m_explanation_of_branches;
bool term_has_big_number(const lar_term* t) const {
for (const auto& p : *t)
if (p.coeff().is_big())
return true;
return false;
}
void add_term_callback(const lar_term* t) {
unsigned j = t->j();
TRACE("dio", tout << "term column t->j():" << j << std::endl; lra.print_term(*t, tout) << std::endl;);
@ -761,8 +796,9 @@ namespace lp {
CTRACE("dio", !lra.column_has_term(j), tout << "added term that is not associated with a column yet" << std::endl;);
if (!lia.column_is_int(t->j())) {
TRACE("dio", tout << "not all vars are integrall\n";);
if (term_has_big_number(t)) {
TRACE("dio", tout << "term_has_big_number\n";);
m_has_non_integral_term = true;
return;
}
m_added_terms.push_back(t);
@ -779,10 +815,12 @@ namespace lp {
void update_column_bound_callback(unsigned j) {
if (!lra.column_is_int(j))
return;
if (lra.column_has_term(j))
if (lra.column_has_term(j) && !term_has_big_number(&lra.get_term(j)))
m_terms_to_tighten.insert(j); // the boundary of the term has changed: we can be successful to tighten this term
if (!lra.column_is_fixed(j))
return;
if (lra.get_lower_bound(j).x.is_big())
return;
TRACE("dio", tout << "j:" << j << "\n"; lra.print_column_info(j, tout););
m_changed_columns.insert(j);
lra.trail().push(undo_fixed_column(*this, j));
@ -1016,6 +1054,7 @@ namespace lp {
void process_changed_columns(std_vector<unsigned> &f_vector) {
find_changed_terms_and_more_changed_rows();
for (unsigned j: m_changed_terms) {
SASSERT(!term_has_big_number(&lra.get_term(j)));
m_terms_to_tighten.insert(j);
if (j < m_l_matrix.column_count()) {
for (const auto& cs : m_l_matrix.column(j)) {
@ -1295,6 +1334,52 @@ namespace lp {
bool is_substituted_by_fresh(unsigned k) const {
return m_fresh_k2xt_terms.has_key(k);
}
// find a variable in q, not neccessarily at the beginning of the queue, that when substituted would create the minimal
// number of non-zeroes
unsigned find_var_to_substitute_on_espace(protected_queue& q) {
// go over all q elements j
// say j is substituted by entry ei = m_k2s[j]
// count the number of variables i in m_e_matrix[ei] that m_espace does not contain i,
// and choose ei where this number is minimal
unsigned best_var = UINT_MAX;
size_t min_new_vars = std::numeric_limits<size_t>::max();
unsigned num_candidates = 0;
for (unsigned j : q.m_q) {
size_t new_vars = 0;
if (!m_espace.has(j)) continue;
if (m_k2s.has_key(j)) {
unsigned ei = m_k2s[j]; // entry index for substitution
for (const auto& p : m_e_matrix.m_rows[ei])
if (p.var() != j && !m_espace.has(p.var()))
++new_vars;
}
else if (m_fresh_k2xt_terms.has_key(j)) {
const lar_term& fresh_term = m_fresh_k2xt_terms.get_by_key(j).first;
for (const auto& p : fresh_term)
if (p.var() != j && !m_espace.has(p.var()))
++new_vars;
}
if (new_vars < min_new_vars) {
min_new_vars = new_vars;
best_var = j;
num_candidates = 1;
}
else if (new_vars == min_new_vars) {
++num_candidates;
if ((lra.settings().random_next() % num_candidates) == 0)
best_var = j;
}
}
if (best_var != UINT_MAX)
q.remove(best_var);
return best_var;
}
// The term giving the substitution is in form (+-)x_k + sum {a_i*x_i} + c = 0.
// We substitute x_k in t by (+-)coeff*(sum {a_i*x_i} + c), where coeff is
// the coefficient of x_k in t.
@ -1303,11 +1388,11 @@ namespace lp {
auto r = tighten_on_espace(j);
if (r == lia_move::conflict)
return lia_move::conflict;
unsigned k = q.pop_front();
if (!m_espace.has(k))
return lia_move::undef;
unsigned k = find_var_to_substitute_on_espace(q);
if (k == UINT_MAX)
return lia_move::undef;
SASSERT(m_espace.has(k));
// we might substitute with a term from S or a fresh term
SASSERT(can_substitute(k));
lia_move ret;
if (is_substituted_by_fresh(k))
@ -2203,6 +2288,7 @@ namespace lp {
public:
lia_move check() {
lra.stats().m_dio_calls++;
std::cout << "check" << std::endl;
TRACE("dio", tout << lra.stats().m_dio_calls << std::endl;);
std_vector<unsigned> f_vector;
lia_move ret;

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

@ -189,7 +189,7 @@ namespace lp {
bool should_gomory_cut() {
bool dio_allows_gomory = !settings().dio_eqs() || settings().dio_enable_gomory_cuts() ||
m_dio.has_non_integral_term();
std::cout << "should_gomory_cut:" << dio_allows_gomory << std::endl;
return dio_allows_gomory && m_number_of_calls % settings().m_int_gomory_cut_period == 0;
}

10
src/math/lp/lp_params_helper.pyg Normal file
View file

@ -0,0 +1,10 @@
def_module_params(module_name='lp',
class_name='lp_params_helper',
description='linear programming parameters',
export=True,
params=(('dio_eqs', BOOL, False, 'use Diophantine equalities'),
('dio_branching_period', UINT, 100, 'Period of calling branching on undef in Diophantine handler'),
('dio_cuts_enable_gomory', BOOL, False, 'enable Gomory cuts together with Diophantine cuts, only relevant when dioph_eq is true'),
('dio_cuts_enable_hnf', BOOL, True, 'enable hnf cuts together with Diophantine cuts, only relevant when dioph_eq is true'),
))

11
src/math/lp/lp_settings.cpp
View file

@ -17,6 +17,7 @@ Revision History:
--*/
#include "math/lp/lp_params_helper.hpp"
#include <memory>
#include "util/vector.h"
#include "smt/params/smt_params_helper.hpp"
@ -25,6 +26,7 @@ template bool lp::vectors_are_equal<lp::mpq>(vector<lp::mpq > const&, vector<lp:
void lp::lp_settings::updt_params(params_ref const& _p) {
smt_params_helper p(_p);
lp_params_helper lp_p(_p);
m_enable_hnf = p.arith_enable_hnf();
m_propagate_eqs = p.arith_propagate_eqs();
print_statistics = p.arith_print_stats();
@ -32,9 +34,8 @@ void lp::lp_settings::updt_params(params_ref const& _p) {
report_frequency = p.arith_rep_freq();
m_simplex_strategy = static_cast<lp::simplex_strategy_enum>(p.arith_simplex_strategy());
m_nlsat_delay = p.arith_nl_delay();
m_dio_eqs = p.arith_lp_dio_eqs();
m_dio_enable_gomory_cuts = p.arith_lp_dio_cuts_enable_gomory();
m_dio_enable_hnf_cuts = p.arith_lp_dio_cuts_enable_hnf();
m_dio_branching_period = p.arith_lp_dio_branching_period();
m_dump_bound_lemmas = p.arith_dump_bound_lemmas();
m_dio_eqs = lp_p.dio_eqs();
m_dio_enable_gomory_cuts = lp_p.dio_cuts_enable_gomory();
m_dio_enable_hnf_cuts = lp_p.dio_cuts_enable_hnf();
m_dio_branching_period = lp_p.dio_branching_period();m_dump_bound_lemmas = p.arith_dump_bound_lemmas();
}

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

@ -57,10 +57,6 @@ def_module_params(module_name='smt',
('bv.solver', UINT, 0, 'bit-vector solver engine: 0 - bit-blasting, 1 - polysat, 2 - intblast, requires sat.smt=true'),
('arith.random_initial_value', BOOL, False, 'use random initial values in the simplex-based procedure for linear arithmetic'),
('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.lp.dio_eqs', BOOL, False, 'use Diophantine equalities'),
('arith.lp.dio_branching_period', UINT, 100, 'Period of calling branching on undef in Diophantine handler'),
('arith.lp.dio_cuts_enable_gomory', BOOL, False, 'enable Gomory cuts together with Diophantine cuts, only relevant when dioph_eq is true'),
('arith.lp.dio_cuts_enable_hnf', BOOL, True, 'enable hnf cuts together with Diophantine cuts, only relevant when dioph_eq is true'),
('arith.nl', BOOL, True, '(incomplete) nonlinear arithmetic support based on Groebner basis and interval propagation, relevant only if smt.arith.solver=2'),
('arith.nl.nra', BOOL, True, 'call nra_solver when incremental linearization does not produce a lemma, this option is ignored when arith.nl=false, relevant only if smt.arith.solver=6'),
('arith.nl.branching', BOOL, True, 'branching on integer variables in non linear clusters'),