Skip to content

Commit 3e49d9f

Browse files
committed
reuse dio branch
Signed-off-by: Lev Nachmanson <[email protected]>
1 parent e31e981 commit 3e49d9f

File tree

6 files changed

+124
-29
lines changed

6 files changed

+124
-29
lines changed

src/math/lp/CMakeLists.txt

+2
Original file line numberDiff line numberDiff line change
@@ -43,6 +43,8 @@ z3_add_component(lp
4343
polynomial
4444
nlsat
4545
smt_params
46+
PYG_FILES
47+
lp_params_helper.pyg
4648
)
4749

4850
include_directories(${src_SOURCE_DIR})

src/math/lp/dioph_eq.cpp

+105-19
Original file line numberDiff line numberDiff line change
@@ -596,34 +596,63 @@ namespace lp {
596596
};
597597

598598
struct protected_queue {
599-
std::queue<unsigned> m_q;
600-
indexed_uint_set m_in_q;
599+
std::list<unsigned> m_q;
600+
std::unordered_map<unsigned, std::list<unsigned>::iterator> m_positions;
601+
601602
bool empty() const {
602603
return m_q.empty();
603604
}
604605

605606
unsigned size() const {
606-
return (unsigned)m_q.size();
607+
return static_cast<unsigned>(m_q.size());
607608
}
608609

609610
void push(unsigned j) {
610-
if (m_in_q.contains(j)) return;
611-
m_in_q.insert(j);
612-
m_q.push(j);
611+
if (m_positions.find(j) != m_positions.end()) return;
612+
m_q.push_back(j);
613+
m_positions[j] = std::prev(m_q.end());
613614
}
614615

615616
unsigned pop_front() {
616617
unsigned j = m_q.front();
617-
m_q.pop();
618-
SASSERT(m_in_q.contains(j));
619-
m_in_q.remove(j);
618+
m_q.pop_front();
619+
m_positions.erase(j);
620620
return j;
621621
}
622622

623+
void remove(unsigned j) {
624+
auto it = m_positions.find(j);
625+
if (it != m_positions.end()) {
626+
m_q.erase(it->second);
627+
m_positions.erase(it);
628+
}
629+
if (!invariant()) {
630+
throw std::runtime_error("Invariant violation in protected_queue");
631+
}
632+
}
633+
634+
bool contains(unsigned j) const {
635+
return m_positions.find(j) != m_positions.end();
636+
}
637+
623638
void reset() {
624-
while (!m_q.empty())
625-
m_q.pop();
626-
m_in_q.reset();
639+
m_q.clear();
640+
m_positions.clear();
641+
}
642+
// Invariant method to ensure m_q and m_positions are aligned
643+
bool invariant() const {
644+
if (m_q.size() != m_positions.size())
645+
return false;
646+
647+
for (auto it = m_q.begin(); it != m_q.end(); ++it) {
648+
auto pos_it = m_positions.find(*it);
649+
if (pos_it == m_positions.end())
650+
return false;
651+
if (pos_it->second != it)
652+
return false;
653+
}
654+
655+
return true;
627656
}
628657
};
629658

@@ -750,6 +779,12 @@ namespace lp {
750779
std_vector<variable_branch_stats> m_branch_stats;
751780
std_vector<branch> m_branch_stack;
752781
std_vector<constraint_index> m_explanation_of_branches;
782+
bool term_has_big_number(const lar_term* t) const {
783+
for (const auto& p : *t)
784+
if (p.coeff().is_big())
785+
return true;
786+
return false;
787+
}
753788
void add_term_callback(const lar_term* t) {
754789
unsigned j = t->j();
755790
TRACE("dio", tout << "term column t->j():" << j << std::endl; lra.print_term(*t, tout) << std::endl;);
@@ -761,8 +796,9 @@ namespace lp {
761796

762797
CTRACE("dio", !lra.column_has_term(j), tout << "added term that is not associated with a column yet" << std::endl;);
763798

764-
if (!lia.column_is_int(t->j())) {
765-
TRACE("dio", tout << "not all vars are integrall\n";);
799+
if (term_has_big_number(t)) {
800+
TRACE("dio", tout << "term_has_big_number\n";);
801+
m_has_non_integral_term = true;
766802
return;
767803
}
768804
m_added_terms.push_back(t);
@@ -779,10 +815,12 @@ namespace lp {
779815
void update_column_bound_callback(unsigned j) {
780816
if (!lra.column_is_int(j))
781817
return;
782-
if (lra.column_has_term(j))
818+
if (lra.column_has_term(j) && !term_has_big_number(&lra.get_term(j)))
783819
m_terms_to_tighten.insert(j); // the boundary of the term has changed: we can be successful to tighten this term
784820
if (!lra.column_is_fixed(j))
785821
return;
822+
if (lra.get_lower_bound(j).x.is_big())
823+
return;
786824
TRACE("dio", tout << "j:" << j << "\n"; lra.print_column_info(j, tout););
787825
m_changed_columns.insert(j);
788826
lra.trail().push(undo_fixed_column(*this, j));
@@ -1016,6 +1054,7 @@ namespace lp {
10161054
void process_changed_columns(std_vector<unsigned> &f_vector) {
10171055
find_changed_terms_and_more_changed_rows();
10181056
for (unsigned j: m_changed_terms) {
1057+
SASSERT(!term_has_big_number(&lra.get_term(j)));
10191058
m_terms_to_tighten.insert(j);
10201059
if (j < m_l_matrix.column_count()) {
10211060
for (const auto& cs : m_l_matrix.column(j)) {
@@ -1295,6 +1334,52 @@ namespace lp {
12951334
bool is_substituted_by_fresh(unsigned k) const {
12961335
return m_fresh_k2xt_terms.has_key(k);
12971336
}
1337+
1338+
// find a variable in q, not neccessarily at the beginning of the queue, that when substituted would create the minimal
1339+
// number of non-zeroes
1340+
unsigned find_var_to_substitute_on_espace(protected_queue& q) {
1341+
// go over all q elements j
1342+
// say j is substituted by entry ei = m_k2s[j]
1343+
// count the number of variables i in m_e_matrix[ei] that m_espace does not contain i,
1344+
// and choose ei where this number is minimal
1345+
1346+
unsigned best_var = UINT_MAX;
1347+
size_t min_new_vars = std::numeric_limits<size_t>::max();
1348+
unsigned num_candidates = 0;
1349+
1350+
for (unsigned j : q.m_q) {
1351+
size_t new_vars = 0;
1352+
if (!m_espace.has(j)) continue;
1353+
if (m_k2s.has_key(j)) {
1354+
unsigned ei = m_k2s[j]; // entry index for substitution
1355+
for (const auto& p : m_e_matrix.m_rows[ei])
1356+
if (p.var() != j && !m_espace.has(p.var()))
1357+
++new_vars;
1358+
}
1359+
else if (m_fresh_k2xt_terms.has_key(j)) {
1360+
const lar_term& fresh_term = m_fresh_k2xt_terms.get_by_key(j).first;
1361+
for (const auto& p : fresh_term)
1362+
if (p.var() != j && !m_espace.has(p.var()))
1363+
++new_vars;
1364+
}
1365+
if (new_vars < min_new_vars) {
1366+
min_new_vars = new_vars;
1367+
best_var = j;
1368+
num_candidates = 1;
1369+
}
1370+
else if (new_vars == min_new_vars) {
1371+
++num_candidates;
1372+
if ((lra.settings().random_next() % num_candidates) == 0)
1373+
best_var = j;
1374+
}
1375+
}
1376+
1377+
if (best_var != UINT_MAX)
1378+
q.remove(best_var);
1379+
1380+
return best_var;
1381+
}
1382+
12981383
// The term giving the substitution is in form (+-)x_k + sum {a_i*x_i} + c = 0.
12991384
// We substitute x_k in t by (+-)coeff*(sum {a_i*x_i} + c), where coeff is
13001385
// the coefficient of x_k in t.
@@ -1303,11 +1388,11 @@ namespace lp {
13031388
auto r = tighten_on_espace(j);
13041389
if (r == lia_move::conflict)
13051390
return lia_move::conflict;
1306-
unsigned k = q.pop_front();
1307-
if (!m_espace.has(k))
1308-
return lia_move::undef;
1391+
unsigned k = find_var_to_substitute_on_espace(q);
1392+
if (k == UINT_MAX)
1393+
return lia_move::undef;
1394+
SASSERT(m_espace.has(k));
13091395
// we might substitute with a term from S or a fresh term
1310-
13111396
SASSERT(can_substitute(k));
13121397
lia_move ret;
13131398
if (is_substituted_by_fresh(k))
@@ -2203,6 +2288,7 @@ namespace lp {
22032288
public:
22042289
lia_move check() {
22052290
lra.stats().m_dio_calls++;
2291+
std::cout << "check" << std::endl;
22062292
TRACE("dio", tout << lra.stats().m_dio_calls << std::endl;);
22072293
std_vector<unsigned> f_vector;
22082294
lia_move ret;

src/math/lp/int_solver.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -189,7 +189,7 @@ namespace lp {
189189
bool should_gomory_cut() {
190190
bool dio_allows_gomory = !settings().dio_eqs() || settings().dio_enable_gomory_cuts() ||
191191
m_dio.has_non_integral_term();
192-
192+
std::cout << "should_gomory_cut:" << dio_allows_gomory << std::endl;
193193
return dio_allows_gomory && m_number_of_calls % settings().m_int_gomory_cut_period == 0;
194194
}
195195

src/math/lp/lp_params_helper.pyg

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

src/math/lp/lp_settings.cpp

+6-5
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,7 @@ Revision History:
1717
1818
1919
--*/
20+
#include "math/lp/lp_params_helper.hpp"
2021
#include <memory>
2122
#include "util/vector.h"
2223
#include "smt/params/smt_params_helper.hpp"
@@ -25,16 +26,16 @@ template bool lp::vectors_are_equal<lp::mpq>(vector<lp::mpq > const&, vector<lp:
2526

2627
void lp::lp_settings::updt_params(params_ref const& _p) {
2728
smt_params_helper p(_p);
29+
lp_params_helper lp_p(_p);
2830
m_enable_hnf = p.arith_enable_hnf();
2931
m_propagate_eqs = p.arith_propagate_eqs();
3032
print_statistics = p.arith_print_stats();
3133
m_print_external_var_name = p.arith_print_ext_var_names();
3234
report_frequency = p.arith_rep_freq();
3335
m_simplex_strategy = static_cast<lp::simplex_strategy_enum>(p.arith_simplex_strategy());
3436
m_nlsat_delay = p.arith_nl_delay();
35-
m_dio_eqs = p.arith_lp_dio_eqs();
36-
m_dio_enable_gomory_cuts = p.arith_lp_dio_cuts_enable_gomory();
37-
m_dio_enable_hnf_cuts = p.arith_lp_dio_cuts_enable_hnf();
38-
m_dio_branching_period = p.arith_lp_dio_branching_period();
39-
m_dump_bound_lemmas = p.arith_dump_bound_lemmas();
37+
m_dio_eqs = lp_p.dio_eqs();
38+
m_dio_enable_gomory_cuts = lp_p.dio_cuts_enable_gomory();
39+
m_dio_enable_hnf_cuts = lp_p.dio_cuts_enable_hnf();
40+
m_dio_branching_period = lp_p.dio_branching_period();m_dump_bound_lemmas = p.arith_dump_bound_lemmas();
4041
}

src/smt/params/smt_params_helper.pyg

-4
Original file line numberDiff line numberDiff line change
@@ -57,10 +57,6 @@ def_module_params(module_name='smt',
5757
('bv.solver', UINT, 0, 'bit-vector solver engine: 0 - bit-blasting, 1 - polysat, 2 - intblast, requires sat.smt=true'),
5858
('arith.random_initial_value', BOOL, False, 'use random initial values in the simplex-based procedure for linear arithmetic'),
5959
('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'),
60-
('arith.lp.dio_eqs', BOOL, False, 'use Diophantine equalities'),
61-
('arith.lp.dio_branching_period', UINT, 100, 'Period of calling branching on undef in Diophantine handler'),
62-
('arith.lp.dio_cuts_enable_gomory', BOOL, False, 'enable Gomory cuts together with Diophantine cuts, only relevant when dioph_eq is true'),
63-
('arith.lp.dio_cuts_enable_hnf', BOOL, True, 'enable hnf cuts together with Diophantine cuts, only relevant when dioph_eq is true'),
6460
('arith.nl', BOOL, True, '(incomplete) nonlinear arithmetic support based on Groebner basis and interval propagation, relevant only if smt.arith.solver=2'),
6561
('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'),
6662
('arith.nl.branching', BOOL, True, 'branching on integer variables in non linear clusters'),

0 commit comments

Comments
 (0)