diff --git a/src/search/cartesian_abstractions/cegar.cc b/src/search/cartesian_abstractions/cegar.cc index 71e2613b6..b33e01b43 100644 --- a/src/search/cartesian_abstractions/cegar.cc +++ b/src/search/cartesian_abstractions/cegar.cc @@ -158,6 +158,9 @@ void CEGAR::refinement_loop() { assert(abstraction->get_num_states() == 1); const AbstractState *current = &abstraction->get_initial_state(); for (FactProxy goal : task_proxy.get_goals()) { + if (!may_keep_refining()) { + break; + } FactPair fact = goal.get_pair(); auto pair = abstraction->refine(*current, fact.var, {fact.value}); current = &abstraction->get_state(pair.second); diff --git a/src/search/cartesian_abstractions/flaw.h b/src/search/cartesian_abstractions/flaw.h index 6d842c358..eb0680af8 100644 --- a/src/search/cartesian_abstractions/flaw.h +++ b/src/search/cartesian_abstractions/flaw.h @@ -38,7 +38,7 @@ struct FlawedState { } friend std::ostream &operator<<(std::ostream &os, const FlawedState &s) { - return os << "Flawed abstract state: id=" << s.abs_id << ", h=" << s.h + return os << "id=" << s.abs_id << ", h=" << s.h << ", states=" << s.concrete_states.size(); } diff --git a/src/search/cartesian_abstractions/flaw_search.cc b/src/search/cartesian_abstractions/flaw_search.cc index b083cb093..309016a45 100644 --- a/src/search/cartesian_abstractions/flaw_search.cc +++ b/src/search/cartesian_abstractions/flaw_search.cc @@ -477,7 +477,7 @@ unique_ptr FlawSearch::get_min_h_batch_split(const utils::CountdownTimer &cegar_timer) { assert(pick_flawed_abstract_state == PickFlawedAbstractState::BATCH_MIN_H); if (last_refined_flawed_state != FlawedState::no_state) { - // Handle flaws of the last refined abstract state. + // Recycle flaws of the last refined abstract state. Cost old_h = last_refined_flawed_state.h; for (const StateID &state_id : last_refined_flawed_state.concrete_states) { State state = state_registry->lookup_state(state_id); @@ -499,10 +499,6 @@ FlawSearch::get_min_h_batch_split(const utils::CountdownTimer &cegar_timer) { } } - if (log.is_at_least_debug()) { - log << "Use flawed state: " << flawed_state << " with h=" << flawed_state.h << endl; - } - // Memory padding if (search_status == TIMEOUT) return nullptr; @@ -511,6 +507,10 @@ FlawSearch::get_min_h_batch_split(const utils::CountdownTimer &cegar_timer) { // There are flaws to refine. assert(flawed_state != FlawedState::no_state); + if (log.is_at_least_debug()) { + log << "Use flawed state: " << flawed_state << endl; + } + unique_ptr split; split = create_split(flawed_state.concrete_states, flawed_state.abs_id);