4
4
#include " math/lp/lp_utils.h"
5
5
#include < list>
6
6
#include < queue>
7
+ /*
8
+ Following paper: "A Practical Approach to Satisfiability Modulo Linear Integer Arithmetic"
9
+ by Alberto Griggio([email protected] )
10
+ Data structures are:
11
+ -- term_o: inherits lar_term and differs from it by having a constant, while lar_term is just
12
+ a sum of monomials
13
+ -- entry : has a dependency lar_term, keeping the history of the entry updates, the rational constant
14
+ of the corresponding term_o, and the entry status that is in {F,S, NO_S_NO_F}. The entry status is used for efficiency
15
+ reasons. It allows quickly check if an entry belongs to F, S, or neither.
16
+ dioph_eq::imp main fields are
17
+ -- lra: pointer to lar_solver.
18
+ -- lia: point to int_solver.
19
+ -- m_entries: it keeps all "entry" objects.
20
+ -- m_e_matrix: i-th row of this matrix keeps the term corresponding to m_entries[i].
21
+ The actual term is the sum of the matrix row and the constant m_c of the entry.
22
+ The column j of the matrix corresponds to j column of lar_solver if j < lra.column_count().
23
+ Otherwise, j is a fresh column. It has to change in the interactive version.
24
+ Implementation remarks:
25
+ -- get_term_from_entry(unsigned i) return a term corresponding i-th entry. If t = get_term_from_entry(i)
26
+ then we have equality t = 0. Initially get_term_from_entry(i) is set to initt(j) = lra.get_term(j) - j,
27
+ for some column j,where all fixed variables are replaced by their values.
28
+ To track the explanations of equality t = 0 we initially set m_entries[i].m_l = lar_term(j), and update m_l
29
+ accordingly with the pivot operations. The explanation is obtained by replacing term m_l = sum(aj*j) by the linear
30
+ combination sum (aj*initt(j)) and joining the explanations of all fixed variables in the latter sum.
31
+ entry_invariant(i) guarantees the validity of entry i.
32
+ */
7
33
namespace lp {
8
34
// This class represents a term with an added constant number c, in form sum {x_i*a_i} + c.
9
35
class dioph_eq ::imp {
@@ -161,7 +187,7 @@ namespace lp {
161
187
mpq m_c; // the constant of the term, the term is taken from the row of m_e_matrix with the same index as the entry
162
188
entry_status m_entry_status;
163
189
};
164
- std_vector<entry> m_eprime ;
190
+ std_vector<entry> m_entries ;
165
191
// the terms are stored in m_A and m_c
166
192
static_matrix<mpq, mpq> m_e_matrix; // the rows of the matrix are the terms, without the constant part
167
193
int_solver& lia;
@@ -182,29 +208,29 @@ namespace lp {
182
208
183
209
std_vector<unsigned > m_k2s;
184
210
std_vector<unsigned > m_fresh_definitions; // seems only needed in the debug version in remove_fresh_vars
185
- unsigned m_conflict_index = -1 ; // m_eprime [m_conflict_index] gives the conflict
211
+ unsigned m_conflict_index = -1 ; // m_entries [m_conflict_index] gives the conflict
186
212
public:
187
213
imp (int_solver& lia, lar_solver& lra): lia(lia), lra(lra) {}
188
214
term_o get_term_from_entry (unsigned i) const {
189
215
term_o t;
190
216
for (const auto & p: m_e_matrix.m_rows [i]) {
191
217
t.add_monomial (p.coeff (), p.var ());
192
218
}
193
- t.c () = m_eprime [i].m_c ;
219
+ t.c () = m_entries [i].m_c ;
194
220
return t;
195
221
}
196
222
// the term has form sum(a_i*x_i) - t.j() = 0,
197
223
// i is the index of the term in the lra.m_terms
198
224
void fill_entry (const lar_term& t) {
199
225
TRACE (" dioph_eq" , print_lar_term_L (t, tout) << std::endl;);
200
- unsigned i = static_cast <unsigned >(m_eprime .size ());
226
+ unsigned i = static_cast <unsigned >(m_entries .size ());
201
227
entry te = {lar_term (t.j ()), mpq (0 ), entry_status::NO_S_NO_F};
202
- unsigned entry_index = m_eprime .size ();
228
+ unsigned entry_index = m_entries .size ();
203
229
m_f.push_back (entry_index);
204
- m_eprime .push_back (te);
205
- entry& e = m_eprime .back ();
230
+ m_entries .push_back (te);
231
+ entry& e = m_entries .back ();
206
232
m_e_matrix.add_row ();
207
- SASSERT (m_e_matrix.row_count () == m_eprime .size ());
233
+ SASSERT (m_e_matrix.row_count () == m_entries .size ());
208
234
209
235
for (const auto & p: t) {
210
236
SASSERT (p.coeff ().is_int ());
@@ -247,7 +273,7 @@ namespace lp {
247
273
m_conflict_index = -1 ;
248
274
m_infeas_explanation.clear ();
249
275
lia.get_term ().clear ();
250
- m_eprime .clear ();
276
+ m_entries .clear ();
251
277
for (unsigned j = 0 ; j < lra.column_count (); j++) {
252
278
if (!lra.column_is_int (j)|| !lra.column_has_term (j)) continue ;
253
279
const lar_term& t = lra.get_term (j);
@@ -320,7 +346,7 @@ namespace lp {
320
346
// it is needed by the next steps
321
347
// the conflict can be used to report "cuts from proofs"
322
348
bool normalize_e_by_gcd (unsigned ei) {
323
- entry& e = m_eprime [ei];
349
+ entry& e = m_entries [ei];
324
350
TRACE (" dioph_eq" , print_entry (ei, tout) << std::endl;);
325
351
mpq g = gcd_of_coeffs (m_e_matrix.m_rows [ei]);
326
352
if (g.is_zero () || g.is_one ()) {
@@ -333,7 +359,7 @@ namespace lp {
333
359
for (auto & p: m_e_matrix.m_rows [ei]) {
334
360
p.coeff () /= g;
335
361
}
336
- m_eprime [ei].m_c = c_g;
362
+ m_entries [ei].m_c = c_g;
337
363
e.m_l *= (1 /g);
338
364
TRACE (" dioph_eq" , tout << " ep_m_e:" ; print_entry (ei, tout) << std::endl;);
339
365
SASSERT (entry_invariant (ei));
@@ -426,7 +452,7 @@ namespace lp {
426
452
return ret;
427
453
}
428
454
const entry& entry_for_subs (unsigned k) const {
429
- return m_eprime [m_k2s[k]];
455
+ return m_entries [m_k2s[k]];
430
456
}
431
457
432
458
const unsigned sub_index (unsigned k) const {
@@ -714,7 +740,7 @@ namespace lp {
714
740
// j is the variable to eliminate, it appears in row e.m_e_matrix with
715
741
// a coefficient equal to +-1
716
742
void eliminate_var_in_f (unsigned ei, unsigned j, int j_sign) {
717
- entry& e = m_eprime [ei];
743
+ entry& e = m_entries [ei];
718
744
TRACE (" dioph_eq" , tout << " eliminate var:" << j << " by using:" ; print_entry (ei, tout) << std::endl;);
719
745
auto &column = m_e_matrix.m_columns [j];
720
746
int pivot_col_cell_index = -1 ;
@@ -738,7 +764,7 @@ namespace lp {
738
764
unsigned cell_to_process = column.size () - 1 ;
739
765
while (cell_to_process > 0 ) {
740
766
auto & c = column[cell_to_process];
741
- if (m_eprime [c.var ()].m_entry_status != entry_status::F) {
767
+ if (m_entries [c.var ()].m_entry_status != entry_status::F) {
742
768
cell_to_process--;
743
769
continue ;
744
770
}
@@ -747,14 +773,14 @@ namespace lp {
747
773
mpq coeff = m_e_matrix.get_val (c);
748
774
unsigned i = c.var ();
749
775
TRACE (" dioph_eq" , tout << " before pivot entry :" ; print_entry (i, tout) << std::endl;);
750
- m_eprime [i].m_c -= j_sign * coeff*e.m_c ;
776
+ m_entries [i].m_c -= j_sign * coeff*e.m_c ;
751
777
m_e_matrix.pivot_row_to_row_given_cell_with_sign (ei, c, j, j_sign);
752
- m_eprime [i].m_l -= j_sign * coeff * e.m_l ;
778
+ m_entries [i].m_l -= j_sign * coeff * e.m_l ;
753
779
TRACE (" dioph_eq" , tout << " after pivoting c_row:" ; print_entry (i, tout););
754
780
CTRACE (" dioph_eq" , !entry_invariant (i),
755
781
tout << " invariant delta:" ;
756
782
{
757
- const auto & e = m_eprime [i];
783
+ const auto & e = m_entries [i];
758
784
print_term_o (get_term_from_entry (ei) - fix_vars (open_ml (e.m_l )), tout) << std::endl;
759
785
}
760
786
);
@@ -764,7 +790,7 @@ namespace lp {
764
790
}
765
791
766
792
bool entry_invariant (unsigned ei) const {
767
- const auto &e = m_eprime [ei];
793
+ const auto &e = m_entries [ei];
768
794
bool ret = remove_fresh_vars (get_term_from_entry (ei)) == fix_vars (open_ml (e.m_l ));
769
795
if (ret) return true ;
770
796
TRACE (" dioph_eq" ,
@@ -846,13 +872,13 @@ namespace lp {
846
872
Then -xt + x_k + sum {qi*x_i)| i != k} + c_q will be the fresh row
847
873
eh = ahk*xt + sum {ri*x_i | i != k} + c_r is the row m_e_matrix[e.m_row_index]
848
874
*/
849
- auto & e = m_eprime [h];
875
+ auto & e = m_entries [h];
850
876
mpq q, r;
851
877
q = machine_div_rem (e.m_c , ahk, r);
852
878
e.m_c = r;
853
879
m_e_matrix.add_new_element (h, xt, ahk);
854
880
855
- m_eprime .push_back ({lar_term (), q, entry_status::NO_S_NO_F});
881
+ m_entries .push_back ({lar_term (), q, entry_status::NO_S_NO_F});
856
882
m_e_matrix.add_new_element (fresh_row, xt, -mpq (1 ));
857
883
m_e_matrix.add_new_element (fresh_row, k, mpq (1 ));
858
884
for (unsigned i: m_indexed_work_vector.m_index ) {
@@ -877,8 +903,8 @@ namespace lp {
877
903
}
878
904
879
905
std::ostream& print_entry (unsigned i, std::ostream& out, bool print_dep = true ) {
880
- out << " m_eprime [" << i << " ]:" ;
881
- return print_entry (i, m_eprime [i], out, print_dep);
906
+ out << " m_entries [" << i << " ]:" ;
907
+ return print_entry (i, m_entries [i], out, print_dep);
882
908
}
883
909
884
910
std::ostream& print_entry (unsigned ei, const entry& e, std::ostream& out, bool need_print_dep = true ) {
@@ -907,8 +933,8 @@ namespace lp {
907
933
908
934
// k is the index of the variable that is being substituted
909
935
void move_entry_from_f_to_s (unsigned k, unsigned h) {
910
- SASSERT (m_eprime [h].m_entry_status == entry_status::F);
911
- m_eprime [h].m_entry_status = entry_status::S;
936
+ SASSERT (m_entries [h].m_entry_status == entry_status::F);
937
+ m_entries [h].m_entry_status = entry_status::S;
912
938
if (k >= m_k2s.size ()) { // k is a fresh variable
913
939
m_k2s.resize (k+1 , -1 );
914
940
}
@@ -924,7 +950,7 @@ namespace lp {
924
950
auto it = m_f.begin ();
925
951
while (it != m_f.end ()) {
926
952
if (m_e_matrix.m_rows [*it].size () == 0 ) {
927
- if (m_eprime [*it].m_c .is_zero ()) {
953
+ if (m_entries [*it].m_c .is_zero ()) {
928
954
it = m_f.erase (it);
929
955
continue ;
930
956
} else {
@@ -961,7 +987,7 @@ namespace lp {
961
987
}
962
988
SASSERT (ex.empty ());
963
989
TRACE (" dioph_eq" , tout << " conflict:" ; print_entry (m_conflict_index, tout, true ) << std::endl;);
964
- auto & ep = m_eprime [m_conflict_index];
990
+ auto & ep = m_entries [m_conflict_index];
965
991
for (auto ci: lra.flatten (explain_fixed_in_meta_term (ep.m_l ))) {
966
992
ex.push_back (ci);
967
993
}
0 commit comments