Skip to content

Commit ae30e2c

Browse files
committed
more aggressive term tightening
Signed-off-by: Lev Nachmanson <[email protected]>
1 parent e846c2a commit ae30e2c

File tree

3 files changed

+96
-45
lines changed

3 files changed

+96
-45
lines changed

src/math/lp/dioph_eq.cpp

+71-44
Original file line numberDiff line numberDiff line change
@@ -1198,7 +1198,7 @@ namespace lp {
11981198
return false;
11991199
}
12001200

1201-
void subs_qfront_by_fresh(unsigned k, protected_queue& q) {
1201+
lia_move subs_qfront_by_fresh(unsigned k, protected_queue& q, unsigned j) {
12021202
const lar_term& e = m_fresh_k2xt_terms.get_by_key(k).first;
12031203
TRACE("dioph_eq", tout << "k:" << k << ", in ";
12041204
print_term_o(create_term_from_espace(), tout) << std::endl;
@@ -1218,11 +1218,13 @@ namespace lp {
12181218
if (m_espace.has(j) && can_substitute(j))
12191219
q.push(j);
12201220
}
1221+
12211222
// there is no change in m_l_matrix
12221223
TRACE("dioph_eq", tout << "after subs k:" << k << "\n";
12231224
print_term_o(create_term_from_espace(), tout) << std::endl;
12241225
tout << "m_lspace:{"; print_lar_term_L(m_lspace.m_data, tout);
12251226
tout << "}, opened:"; print_ml(m_lspace.to_term(), tout) << std::endl;);
1227+
return tighten_on_espace(j);
12261228
}
12271229

12281230
void add_l_row_to_term_with_index(const mpq& coeff, unsigned ei) {
@@ -1231,7 +1233,7 @@ namespace lp {
12311233
}
12321234
}
12331235

1234-
void subs_qfront_by_S(unsigned k, protected_queue& q) {
1236+
lia_move subs_qfront_by_S(unsigned k, protected_queue& q, unsigned j) {
12351237
const mpq& e = m_sum_of_fixed[m_k2s[k]];
12361238
TRACE("dio", tout << "k:" << k << ", in ";
12371239
print_term_o(create_term_from_espace(), tout) << std::endl;
@@ -1266,6 +1268,8 @@ namespace lp {
12661268
print_term_o(create_term_from_espace(), tout) << std::endl;
12671269
tout << "m_lspace:{"; print_lar_term_L(m_lspace.to_term(), tout);
12681270
tout << "}, opened:"; print_ml(m_lspace.to_term(), tout) << std::endl;);
1271+
1272+
return tighten_on_espace(j);
12691273
}
12701274

12711275
bool is_substituted_by_fresh(unsigned k) const {
@@ -1274,19 +1278,27 @@ namespace lp {
12741278
// The term giving the substitution is in form (+-)x_k + sum {a_i*x_i} + c = 0.
12751279
// We substitute x_k in t by (+-)coeff*(sum {a_i*x_i} + c), where coeff is
12761280
// the coefficient of x_k in t.
1277-
void subs_front_with_S_and_fresh(protected_queue& q) {
1281+
lia_move subs_front_with_S_and_fresh(protected_queue& q, unsigned j) {
1282+
process_fixed_in_espace();
1283+
auto r = tighten_on_espace(j);
1284+
if (r == lia_move::conflict) return lia_move::conflict;
12781285
unsigned k = q.pop_front();
12791286
if (!m_espace.has(k))
1280-
return;
1287+
return lia_move::undef;
12811288
// we might substitute with a term from S or a fresh term
12821289

12831290
SASSERT(can_substitute(k));
1291+
lia_move ret;
12841292
if (is_substituted_by_fresh(k)) {
1285-
subs_qfront_by_fresh(k, q);
1293+
ret = subs_qfront_by_fresh(k, q, j);
12861294
}
12871295
else {
1288-
subs_qfront_by_S(k, q);
1296+
ret = subs_qfront_by_S(k, q, j);
12891297
}
1298+
if (ret == lia_move::conflict)
1299+
return lia_move::conflict;
1300+
if (r == lia_move::continue_with_check) return r;
1301+
return ret;
12901302
}
12911303

12921304
lar_term l_term_from_row(unsigned k) const {
@@ -1355,9 +1367,15 @@ namespace lp {
13551367
return true;
13561368
}
13571369

1358-
void subs_with_S_and_fresh(protected_queue& q) {
1359-
while (!q.empty())
1360-
subs_front_with_S_and_fresh(q);
1370+
lia_move subs_with_S_and_fresh(protected_queue& q, unsigned j) {
1371+
lia_move r = lia_move::undef;
1372+
while (!q.empty()) {
1373+
lia_move ret = subs_front_with_S_and_fresh(q, j);
1374+
if (ret == lia_move::conflict) return lia_move::conflict;
1375+
if (ret == lia_move::continue_with_check)
1376+
r = ret;
1377+
}
1378+
return r;
13611379
}
13621380

13631381
unsigned term_weight(const lar_term& t) const {
@@ -1427,7 +1445,7 @@ namespace lp {
14271445
// Process sorted terms
14281446
TRACE("dio",
14291447
tout << "changed terms:"; for (auto j : sorted_changed_terms) tout << j << " "; tout << std::endl;
1430-
// print_S(tout);
1448+
print_S(tout);
14311449
// print_bounds(tout);
14321450
);
14331451
for (unsigned j : sorted_changed_terms) {
@@ -1490,37 +1508,12 @@ namespace lp {
14901508
m_espace.erase(j);
14911509
}
14921510
}
1493-
/* j is the index of the column representing a term
1494-
Return lia_move::conflict if a conflict was found, lia_move::continue_with_check if j became a fixed variable, and undef
1495-
otherwise
1496-
When we have a constraint x + y <= 8 then after the substitutions with S and fresh variables
1497-
we might have x + y = 7t - 1 <= 8, where t is a term. Then 7t <= 9, or t <= 9/7, and we can enforce t <= floor(9/7) = 1.
1498-
Then x + y = 7*1 - 1 <= 6: the bound is strenthgened. The constraint in this example comes from the upper bound on j, where
1499-
j is the slack variable in x + y - j = 0.
1500-
*/
1501-
lia_move tighten_bounds_for_term_column(unsigned j) {
1502-
// q is the queue of variables that can be substituted in term_to_tighten
1503-
protected_queue q;
1504-
TRACE("dio", tout << "j:" << j << " , intitial term t: "; print_lar_term_L(lra.get_term(j), tout) << std::endl;
1505-
for( const auto& p : lra.get_term(j)) {
1506-
lra.print_column_info(p.var(), tout);
1507-
}
1508-
);
1509-
init_substitutions(lra.get_term(j), q);
1510-
if (q.empty()) // todo: maybe still go ahead and process it?
1511-
return lia_move::undef;
1512-
1513-
TRACE("dio", tout << "t:";
1514-
tout << "m_espace:";
1515-
print_term_o(create_term_from_espace(), tout) << std::endl;
1516-
tout << "m_lspace:";
1517-
print_lar_term_L(m_lspace.to_term(), tout) << std::endl;);
1518-
subs_with_S_and_fresh(q);
1519-
process_fixed_in_espace();
1520-
SASSERT(subs_invariant(j));
1511+
1512+
1513+
lia_move tighten_on_espace(unsigned j) {
15211514
mpq g = gcd_of_coeffs(m_espace.m_data, true);
15221515
TRACE("dio", tout << "after process_q_with_S\nt:"; print_term_o(create_term_from_espace(), tout) << std::endl; tout << "g:" << g << std::endl;);
1523-
1516+
15241517
if (g.is_one())
15251518
return lia_move::undef;
15261519
if (g.is_zero()) {
@@ -1545,6 +1538,40 @@ namespace lp {
15451538
return lia_move::continue_with_check;
15461539
}
15471540
return lia_move::undef;
1541+
1542+
}
1543+
1544+
/* j is the index of the column representing a term
1545+
Return lia_move::conflict if a conflict was found, lia_move::continue_with_check if j became a fixed variable, and undef
1546+
otherwise
1547+
When we have a constraint x + y <= 8 then after the substitutions with S and fresh variables
1548+
we might have x + y = 7t - 1 <= 8, where t is a term. Then 7t <= 9, or t <= 9/7, and we can enforce t <= floor(9/7) = 1.
1549+
Then x + y = 7*1 - 1 <= 6: the bound is strenthgened. The constraint in this example comes from the upper bound on j, where
1550+
j is the slack variable in x + y - j = 0.
1551+
*/
1552+
lia_move tighten_bounds_for_term_column(unsigned j) {
1553+
// q is the queue of variables that can be substituted in term_to_tighten
1554+
protected_queue q;
1555+
TRACE("dio", tout << "j:" << j << " , intitial term t: "; print_lar_term_L(lra.get_term(j), tout) << std::endl;
1556+
for( const auto& p : lra.get_term(j).ext_coeffs()) {
1557+
lra.print_column_info(p.var(), tout);
1558+
}
1559+
);
1560+
init_substitutions(lra.get_term(j), q);
1561+
1562+
TRACE("dio", tout << "t:";
1563+
tout << "m_espace:";
1564+
print_term_o(create_term_from_espace(), tout) << std::endl;
1565+
tout << "in lar_solver indices:\n";
1566+
print_term_o(term_to_lar_solver(create_term_from_espace()), tout) << "\n";
1567+
tout << "m_lspace:";
1568+
print_lar_term_L(m_lspace.to_term(), tout) << std::endl;);
1569+
if (subs_with_S_and_fresh(q, j) == lia_move::conflict)
1570+
return lia_move::conflict;
1571+
1572+
process_fixed_in_espace();
1573+
SASSERT(subs_invariant(j));
1574+
return tighten_on_espace(j);
15481575
}
15491576

15501577
bool should_report_branch() const {
@@ -2492,7 +2519,7 @@ namespace lp {
24922519
out << "x" << j << " ";
24932520
out << "{\n";
24942521

2495-
print_term_o(get_term_from_entry(i), out << "\t") << ",\n";
2522+
print_term_o(get_term_from_entry(i), out << "\t") << " = 0\n";
24962523
if (print_dep) {
24972524
auto l_term = l_term_from_row(i);
24982525
out << "\tm_l:{";
@@ -2515,15 +2542,15 @@ namespace lp {
25152542
for (const auto& p : m_e_matrix[i] ) {
25162543
if (var_is_fresh(p.var())) {
25172544
has_fresh = true;
2518-
out << "has fresh var:" << p.var() << "\n";
25192545
break;
25202546
}
25212547
}
25222548
if (!has_fresh) {
25232549
for (const auto& p : get_term_from_entry(i)) {
2524-
out << "\tlocal(x" << p.var() << ")";
2525-
lra.print_column_info(local_to_lar_solver(p.var()), out);
2526-
}
2550+
out << "\tx" << p.var() << ": " << lra.get_bounds_string(local_to_lar_solver(p.var())) << "\n";
2551+
}
2552+
} else {
2553+
out << "\thas fresh vars\n";
25272554
}
25282555
}
25292556
out << "}\n";

src/math/lp/lar_solver.cpp

+24-1
Original file line numberDiff line numberDiff line change
@@ -2547,7 +2547,30 @@ namespace lp {
25472547
}
25482548
return out;
25492549
}
2550-
2550+
std::string lar_solver::get_bounds_string(unsigned j) const {
2551+
mpq lb, ub;
2552+
bool is_strict_lower = false, is_strict_upper = false;
2553+
u_dependency* dep = nullptr;
2554+
bool has_lower = has_lower_bound(j, dep, lb, is_strict_lower);
2555+
bool has_upper = has_upper_bound(j, dep, ub, is_strict_upper);
2556+
2557+
std::ostringstream oss;
2558+
2559+
if (!has_lower && !has_upper) {
2560+
oss << "(-oo, oo)";
2561+
}
2562+
else if (has_lower && !has_upper) {
2563+
oss << (is_strict_lower ? "(" : "[") << lb << ", oo)";
2564+
}
2565+
else if (!has_lower && has_upper) {
2566+
oss << "(-oo, " << ub << (is_strict_upper ? ")" : "]");
2567+
}
2568+
else { // has both bounds
2569+
oss << (is_strict_lower ? "(" : "[") << lb << ", " << ub << (is_strict_upper ? ")" : "]");
2570+
}
2571+
2572+
return oss.str();
2573+
}
25512574
// Helper function to format constants in SMT2 format
25522575
std::string format_smt2_constant(const mpq& val) {
25532576
if (val.is_neg()) {

src/math/lp/lar_solver.h

+1
Original file line numberDiff line numberDiff line change
@@ -726,6 +726,7 @@ class lar_solver : public column_namer {
726726
return m_usage_in_terms[j];
727727
}
728728

729+
std::string get_bounds_string(unsigned j) const;
729730
void write_bound_lemma(unsigned j, bool is_low, const std::string & location, std::ostream & out) const;
730731

731732
std::function<void (const indexed_uint_set& columns_with_changed_bound)> m_find_monics_with_changed_bounds_func = nullptr;

0 commit comments

Comments
 (0)