diff options
author | Tim King <taking@cs.nyu.edu> | 2013-05-01 14:59:39 -0400 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2013-05-01 14:59:39 -0400 |
commit | 94decb8503be1fcc894094a0f2656e25d8aef251 (patch) | |
tree | da7c9cffe109cc3249e45d44f6db1599d496b2b7 /src/theory/arith/linear_equality.cpp | |
parent | 88ce3a56088e4f3f509b565944ef8c6d36545423 (diff) |
Working on the new explanation system.
Diffstat (limited to 'src/theory/arith/linear_equality.cpp')
-rw-r--r-- | src/theory/arith/linear_equality.cpp | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/src/theory/arith/linear_equality.cpp b/src/theory/arith/linear_equality.cpp index 4779b1012..bde771102 100644 --- a/src/theory/arith/linear_equality.cpp +++ b/src/theory/arith/linear_equality.cpp @@ -581,7 +581,7 @@ void LinearEqualityModule::propagateNonbasics(ArithVar basic, Constraint c){ << basic << ") done" << endl; } -void LinearEqualityModule::propagateRow(RowIndex ridx, bool rowUp, Constraint c){ +void LinearEqualityModule::propagateRow(vector<Constraint>& into, RowIndex ridx, bool rowUp, Constraint c){ Assert(!c->assertedToTheTheory()); Assert(c->canBePropagated()); Assert(!c->hasProof()); @@ -589,7 +589,7 @@ void LinearEqualityModule::propagateRow(RowIndex ridx, bool rowUp, Constraint c) ArithVar v = c->getVariable(); Debug("arith::explainNonbasics") << "LinearEqualityModule::explainNonbasics(" << v <<") start" << endl; - vector<Constraint> bounds; + //vector<Constraint> bounds; Tableau::RowIterator iter = d_tableau.ridRowIterator(ridx); for(; !iter.atEnd(); ++iter){ @@ -608,9 +608,8 @@ void LinearEqualityModule::propagateRow(RowIndex ridx, bool rowUp, Constraint c) Assert(bound != NullConstraint); Debug("arith::explainNonbasics") << "explainNonbasics" << bound << " for " << c << endl; - bounds.push_back(bound); + into.push_back(bound); } - c->impliedBy(bounds); Debug("arith::explainNonbasics") << "LinearEqualityModule::explainNonbasics(" << v << ") done" << endl; } |