@@ -52,62 +52,62 @@ bool ConstraintSystem::eliminateUsingFM() {
52
52
for (unsigned R1 = 0 ; R1 < NumRemainingConstraints; R1++) {
53
53
// FIXME do not use copy
54
54
for (unsigned R2 = R1 + 1 ; R2 < NumRemainingConstraints; R2++) {
55
- if (R1 == R2)
56
- continue ;
57
-
58
55
int64_t UpperLast = getLastCoefficient (RemainingRows[R2], LastIdx);
59
56
int64_t LowerLast = getLastCoefficient (RemainingRows[R1], LastIdx);
60
57
assert (
61
58
UpperLast != 0 && LowerLast != 0 &&
62
59
" RemainingRows should only contain rows where the variable is != 0" );
63
60
61
+ // ensure signs are different then swap if necessary to only
62
+ // deal with UpperLast > 0
64
63
if ((LowerLast < 0 && UpperLast < 0 ) || (LowerLast > 0 && UpperLast > 0 ))
65
64
continue ;
66
-
67
65
unsigned LowerR = R1;
68
66
unsigned UpperR = R2;
69
67
if (UpperLast < 0 ) {
70
68
std::swap (LowerR, UpperR);
71
69
std::swap (LowerLast, UpperLast);
72
70
}
73
71
72
+ // The following loop does the element-wise operation on sparse
73
+ // vectors:
74
+ //
75
+ // NR = - UpperRow * LowerLast + LowerRow * UpperLast
74
76
SmallVector<Entry, 8 > NR;
75
77
unsigned IdxUpper = 0 ;
76
78
unsigned IdxLower = 0 ;
77
79
auto &LowerRow = RemainingRows[LowerR];
78
80
auto &UpperRow = RemainingRows[UpperR];
79
- while (true ) {
80
- if (IdxUpper >= UpperRow.size () || IdxLower >= LowerRow.size ())
81
- break ;
81
+
82
+ while (IdxUpper < UpperRow.size () && IdxLower < LowerRow.size ()) {
82
83
int64_t M1, M2, N;
83
84
int64_t UpperV = 0 ;
84
85
int64_t LowerV = 0 ;
85
- uint16_t CurrentId = std::numeric_limits<uint16_t >::max ();
86
- if (IdxUpper < UpperRow.size ()) {
87
- CurrentId = std::min (UpperRow[IdxUpper].Id , CurrentId);
88
- }
89
- if (IdxLower < LowerRow.size ()) {
90
- CurrentId = std::min (LowerRow[IdxLower].Id , CurrentId);
91
- }
86
+ uint16_t CurrentId =
87
+ std::min (UpperRow[IdxUpper].Id , LowerRow[IdxLower].Id );
92
88
93
- if (IdxUpper < UpperRow. size () && UpperRow[IdxUpper].Id == CurrentId) {
89
+ if (UpperRow[IdxUpper].Id == CurrentId) {
94
90
UpperV = UpperRow[IdxUpper].Coefficient ;
95
- IdxUpper++;
91
+ IdxUpper += 1 ;
92
+ }
93
+ if (LowerRow[IdxLower].Id == CurrentId) {
94
+ LowerV = LowerRow[IdxLower].Coefficient ;
95
+ IdxLower += 1 ;
96
96
}
97
97
98
98
if (MulOverflow (UpperV, -1 * LowerLast, M1))
99
99
return false ;
100
- if (IdxLower < LowerRow.size () && LowerRow[IdxLower].Id == CurrentId) {
101
- LowerV = LowerRow[IdxLower].Coefficient ;
102
- IdxLower++;
103
- }
104
100
105
101
if (MulOverflow (LowerV, UpperLast, M2))
106
102
return false ;
103
+
107
104
if (AddOverflow (M1, M2, N))
108
105
return false ;
106
+
107
+ // useless to add a 0 to a sparse vector
109
108
if (N == 0 )
110
109
continue ;
110
+
111
111
NR.emplace_back (N, CurrentId);
112
112
}
113
113
if (NR.empty ())
0 commit comments