Skip to content

Commit

Permalink
Fix issue #34.
Browse files Browse the repository at this point in the history
 * (Asynchronous) SequentialSolve failed to handle interruptions
   occuring between the initial attach and the actual start of the
   solve loop.
  • Loading branch information
BenKaufmann committed Jun 22, 2018
1 parent 4c76c96 commit 406ba13
Showing 1 changed file with 3 additions and 3 deletions.
6 changes: 3 additions & 3 deletions src/solve_algorithms.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -392,9 +392,9 @@ void SequentialSolve::doStart(SharedContext& ctx, const LitVec& gp) {
if (!enumerator().start(solve_->solver(), gp)) { SequentialSolve::doStop(); }
}
int SequentialSolve::doNext(int last) {
if (term_ > 0 || !solve_.get()) { return solve_.get() ? value_free : value_false; }
if (interrupted() || !solve_.get()) { return solve_.get() ? value_free : value_false; }
Solver& s = solve_->solver();
for (InterruptHandler term(term_ == 0 ? &s : (Solver*)0, &term_);;) {
for (InterruptHandler term(term_ >= 0 ? &s : (Solver*)0, &term_);;) {
if (last != value_free) { enumerator().update(s); }
last = solve_->solve();
if (last != value_true) {
Expand Down Expand Up @@ -424,7 +424,7 @@ bool SequentialSolve::doSolve(SharedContext& ctx, const LitVec& gp) {
// under the current assumptions but not necessarily unsat.
Solver& s = solve.solver();
bool more = !interrupted() && ctx.attach(s) && enumerator().start(s, gp);
for (InterruptHandler term(term_ == 0 ? &s : (Solver*)0, &term_); more;) {
for (InterruptHandler term(term_ >= 0 ? &s : (Solver*)0, &term_); more;) {
ValueRep res;
while ((res = solve.solve()) == value_true && (!enumerator().commitModel(s) || reportModel(s))) {
enumerator().update(s);
Expand Down

0 comments on commit 406ba13

Please sign in to comment.