Skip to content

Commit 3e7e903

Browse files
committed
use the trail to undo add_term
Signed-off-by: Lev Nachmanson <[email protected]>
1 parent 9c51001 commit 3e7e903

File tree

3 files changed

+16
-9
lines changed

3 files changed

+16
-9
lines changed

src/math/lp/dioph_eq.cpp

+16-5
Original file line numberDiff line numberDiff line change
@@ -387,7 +387,7 @@ namespace lp {
387387
}
388388
};
389389

390-
void remove_term_callback(const lar_term *t) {
390+
void undo_add_term_method(const lar_term *t) {
391391
TRACE("d_undo", tout << "t:"<< t<<", t->j():"<< t->j() << std::endl;);
392392
TRACE("dioph_eq", lra.print_term(*t, tout); tout << ", t->j() =" << t->j() << std::endl;);
393393
if (!contains(m_active_terms, t)) {
@@ -422,8 +422,18 @@ namespace lp {
422422
tout << "and " << m_l_matrix.row_count() << " rows" << std::endl;
423423
print_lar_term_L(*t, tout); tout << "; t->j()=" << t->j() << std::endl;
424424
);
425-
shrink_L_to_sizes();
425+
shrink_matrices();
426426
}
427+
428+
struct undo_add_term : public trail {
429+
imp& m_s;
430+
const lar_term* m_t;
431+
undo_add_term(imp& s, const lar_term *t): m_s(s), m_t(t) {}
432+
433+
void undo() {
434+
m_s.undo_add_term_method(m_t);
435+
}
436+
};
427437

428438
struct undo_fixed_column : public trail {
429439
imp& m_imp;
@@ -504,7 +514,7 @@ namespace lp {
504514
m_l_matrix.add_rows(mpq(1), i, m_l_matrix.row_count() - 1);
505515
}
506516

507-
void shrink_L_to_sizes() {
517+
void shrink_matrices() {
508518
unsigned i = m_l_matrix.row_count() - 1;
509519
eliminate_last_term_column();
510520
remove_last_row_in_matrix(m_l_matrix);
@@ -564,7 +574,9 @@ namespace lp {
564574
TRACE("dioph_eq", tout << "not all vars are integrall\n";);
565575
return;
566576
}
567-
m_added_terms.push_back(t);
577+
m_added_terms.push_back(t);
578+
auto undo = undo_add_term(*this, t);
579+
lra.trail().push(undo);
568580
}
569581

570582
void update_column_bound_callback(unsigned j) {
@@ -578,7 +590,6 @@ namespace lp {
578590
public:
579591
imp(int_solver& lia, lar_solver& lra) : lia(lia), lra(lra) {
580592
lra.m_add_term_callback=[this](const lar_term*t){add_term_callback(t);};
581-
lra.m_remove_term_callback = [this](const lar_term*t){remove_term_callback(t);};
582593
lra.m_update_column_bound_callback = [this](unsigned j){update_column_bound_callback(j);};
583594
}
584595
term_o get_term_from_entry(unsigned i) const {

src/math/lp/lar_solver.cpp

-3
Original file line numberDiff line numberDiff line change
@@ -1558,11 +1558,8 @@ namespace lp {
15581558
if (col.term() != nullptr) {
15591559
if (s.m_need_register_terms)
15601560
s.deregister_normalized_term(*col.term());
1561-
if (s.m_remove_term_callback)
1562-
s.m_remove_term_callback(col.term());
15631561
delete col.term();
15641562
s.m_terms.pop_back();
1565-
15661563
}
15671564
s.remove_last_column_from_tableau();
15681565
s.m_columns.pop_back();

src/math/lp/lar_solver.h

-1
Original file line numberDiff line numberDiff line change
@@ -408,7 +408,6 @@ class lar_solver : public column_namer {
408408

409409
public:
410410
std::function<void (const lar_term*)> m_add_term_callback;
411-
std::function<void (const lar_term*)> m_remove_term_callback;
412411
std::function<void (unsigned)> m_update_column_bound_callback;
413412
bool external_is_used(unsigned) const;
414413
void pop(unsigned k);

0 commit comments

Comments
 (0)