Merge scorpion branches.

jendrikseipp · Oct 2, 2023 · 3e206ba · 3e206ba
2 parents 46f2b16 + 6e1f1c5
commit 3e206ba
Show file tree

Hide file tree

Showing 3 changed files with 9 additions and 6 deletions.
diff --git 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
@@ -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
@@ -477,7 +477,7 @@ unique_ptr<Split>
 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;
         split = create_split(flawed_state.concrete_states, flawed_state.abs_id);