[issue1201] Check whether a configuration guarantees completeness

docs/exit-codes.md

@@ -24,9 +24,10 @@ termination which prevents the execution of further components.
 
 | **Code** | **Name** | **Meaning** |
 | -------- | -------- | ----------- |
-| 10 | TRANSLATE_UNSOLVABLE | Translator proved task to be unsolvable. Currently not used |
-| 11 | SEARCH_UNSOLVABLE | Task is provably unsolvable with current bound. Currently only used by hillclimbing search. See also [issue377](http://issues.fast-downward.org/issue377). |
+| 10 | TRANSLATE_UNSOLVABLE | Translator proved task to be unsolvable. Currently not used. |
+| 11 | SEARCH_UNSOLVABLE | Task is provably unsolvable. |
 | 12 | SEARCH_UNSOLVED_INCOMPLETE | Search ended without finding a solution. |
+| 13 | SEARCH_UNSOLVABLE_WITHIN_BOUND | Task is provably unsolvable with current bound. |
 
 The third block (20-29) represents expected failures which prevent the
 execution of further components.

driver/returncodes.py

@@ -14,6 +14,7 @@
 TRANSLATE_UNSOLVABLE = 10
 SEARCH_UNSOLVABLE = 11
 SEARCH_UNSOLVED_INCOMPLETE = 12
+SEARCH_UNSOLVABLE_WITHIN_BOUND = 13
 
 TRANSLATE_OUT_OF_MEMORY = 20
 TRANSLATE_OUT_OF_TIME = 21

misc/tests/benchmarks/blocks-unsolvable/domain.pddl

@@ -0,0 +1,48 @@
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;; 4 Op-blocks world
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(define (domain BLOCKS)
+  (:requirements :strips)
+  (:predicates (on ?x ?y)
+	       (ontable ?x)
+	       (clear ?x)
+	       (handempty)
+	       (holding ?x)
+	       )
+
+  (:action pick-up
+	     :parameters (?x)
+	     :precondition (and (clear ?x) (ontable ?x) (handempty))
+	     :effect
+	     (and (not (ontable ?x))
+		   (not (clear ?x))
+		   (not (handempty))
+		   (holding ?x)))
+
+  (:action put-down
+	     :parameters (?x)
+	     :precondition (holding ?x)
+	     :effect
+	     (and (not (holding ?x))
+		   (clear ?x)
+		   (handempty)
+		   (ontable ?x)))
+  (:action stack
+	     :parameters (?x ?y)
+	     :precondition (and (holding ?x) (clear ?y))
+	     :effect
+	     (and (not (holding ?x))
+		   (not (clear ?y))
+		   (clear ?x)
+		   (handempty)
+		   (on ?x ?y)))
+  (:action unstack
+	     :parameters (?x ?y)
+	     :precondition (and (on ?x ?y) (clear ?x) (handempty))
+	     :effect
+	     (and (holding ?x)
+		   (clear ?y)
+		   (not (clear ?x))
+		   (not (handempty))
+		   (not (on ?x ?y)))))

misc/tests/benchmarks/blocks-unsolvable/probBLOCKS-4-0.pddl

@@ -0,0 +1,7 @@
+(define (problem BLOCKS-4-0)
+(:domain BLOCKS)
+(:objects D B A C )
+(:INIT (CLEAR C) (CLEAR A) (CLEAR B) (CLEAR D) (ONTABLE C) (ONTABLE A)
+ (ONTABLE B) (ONTABLE D) (HANDEMPTY))
+(:goal (AND (ON D C) (ON C B) (ON B A) (ON A D)))
+)

misc/tests/test-exitcodes.py

@@ -38,6 +38,7 @@
     "strips": "miconic/s1-0.pddl",
     "axioms": "philosophers/p01-phil2.pddl",
     "cond-eff": "miconic-simpleadl/s1-0.pddl",
+    "unsolvable": "blocks-unsolvable/probBLOCKS-4-0.pddl",
     "large": "satellite/p25-HC-pfile5.pddl",
 }
 
@@ -121,6 +122,36 @@
         defaultdict(lambda: returncodes.SEARCH_UNSUPPORTED)),
     ("cond-eff", [], MERGE_AND_SHRINK,
         defaultdict(lambda: returncodes.SUCCESS)),
+    ("unsolvable", [], "astar(blind())",
+        defaultdict(lambda: returncodes.SEARCH_UNSOLVABLE)),
+    ("unsolvable", [], "astar(lmcut())",
+        defaultdict(lambda: returncodes.SEARCH_UNSOLVABLE)),
+    ("unsolvable", [], "lazy(single(lmcut()))",
+        defaultdict(lambda: returncodes.SEARCH_UNSOLVABLE)),
+    ("unsolvable", [], "eager(alt([single(const(infinity)),single(const(1))]))",
+        defaultdict(lambda: returncodes.SEARCH_UNSOLVABLE)),
+    ("unsolvable", [], "eager(type_based([const(infinity),const(1)]))",
+        defaultdict(lambda: returncodes.SEARCH_UNSOLVABLE)),
+    ("unsolvable", [], "eager(pareto([const(infinity),const(1)]))",
+        defaultdict(lambda: returncodes.SEARCH_UNSOLVABLE)),
+    ("unsolvable", [], "eager(tiebreaking([const(infinity),const(1)],unsafe_pruning=false))",
+        defaultdict(lambda: returncodes.SEARCH_UNSOLVABLE)),
+    ("unsolvable", [], "astar(blind(),bound=2)",
+        defaultdict(lambda: returncodes.SEARCH_UNSOLVABLE_WITHIN_BOUND)),
+    ("unsolvable", [], "ehc(blind())",
+        defaultdict(lambda: returncodes.SEARCH_UNSOLVED_INCOMPLETE)),
+    ("unsolvable", [], "eager(single(blind(),pref_only=true))",
+        defaultdict(lambda: returncodes.SEARCH_UNSOLVED_INCOMPLETE)),
+    ("unsolvable", [], "eager(pareto([blind()],pref_only=true))",
+        defaultdict(lambda: returncodes.SEARCH_UNSOLVED_INCOMPLETE)),
+    ("unsolvable", [], "eager(pareto([cg(),cea()]))",
+        defaultdict(lambda: returncodes.SEARCH_UNSOLVED_INCOMPLETE)),
+    ("unsolvable", [], "eager(tiebreaking([const(infinity),blind()]))",
+        defaultdict(lambda: returncodes.SEARCH_UNSOLVED_INCOMPLETE)),
+    ("unsolvable", [], "eager(alt([single(cg()),single(const(infinity))]))",
+        defaultdict(lambda: returncodes.SEARCH_UNSOLVED_INCOMPLETE)),
+    ("unsolvable", [], "lazy(type_based([cg(),const(infinity)]))",
+        defaultdict(lambda: returncodes.SEARCH_UNSOLVED_INCOMPLETE)),
     # We cannot set/enforce memory limits on Windows/macOS and thus expect
     # DRIVER_UNSUPPORTED as exit code in those cases.
     ("large", ["--search-memory-limit", "100M"], MERGE_AND_SHRINK,

src/search/evaluator.cc

@@ -19,7 +19,7 @@ Evaluator::Evaluator(
       log(utils::get_log_for_verbosity(verbosity)) {
 }
 
-bool Evaluator::dead_ends_are_reliable() const {
+bool Evaluator::is_safe() const {
     return true;
 }
 

src/search/evaluator.h

@@ -29,12 +29,12 @@ class Evaluator {
     virtual ~Evaluator() = default;
 
     /*
-      dead_ends_are_reliable should return true if the evaluator is
-      "safe", i.e., infinite estimates can be trusted.
+      is_safe returns true if the evaluator reports dead ends reliably,
+      i.e., if its infinite estimates can be trusted.
 
       The default implementation returns true.
     */
-    virtual bool dead_ends_are_reliable() const;
+    virtual bool is_safe() const;
 
     /*
       get_path_dependent_evaluators should insert all path-dependent

src/search/evaluators/combining_evaluator.cc

@@ -15,14 +15,14 @@ CombiningEvaluator::CombiningEvaluator(
     : Evaluator(false, false, false, description, verbosity),
       subevaluators(evals) {
     utils::verify_list_not_empty(evals, "evals");
-    all_dead_ends_are_reliable = true;
+    all_subevaluators_are_safe = true;
     for (const shared_ptr<Evaluator> &subevaluator : subevaluators)
-        if (!subevaluator->dead_ends_are_reliable())
-            all_dead_ends_are_reliable = false;
+        if (!subevaluator->is_safe())
+            all_subevaluators_are_safe = false;
 }
 
-bool CombiningEvaluator::dead_ends_are_reliable() const {
-    return all_dead_ends_are_reliable;
+bool CombiningEvaluator::is_safe() const {
+    return all_subevaluators_are_safe;
 }
 
 EvaluationResult CombiningEvaluator::compute_result(

src/search/evaluators/combining_evaluator.h

@@ -15,7 +15,7 @@ namespace combining_evaluator {
 */
 class CombiningEvaluator : public Evaluator {
     std::vector<std::shared_ptr<Evaluator>> subevaluators;
-    bool all_dead_ends_are_reliable;
+    bool all_subevaluators_are_safe;
 protected:
     virtual int combine_values(const std::vector<int> &values) = 0;
 public:
@@ -24,19 +24,18 @@ class CombiningEvaluator : public Evaluator {
         const std::string &description, utils::Verbosity verbosity);
 
     /*
-      Note: dead_ends_are_reliable() is a state-independent method, so
-      it only returns true if all subevaluators report dead ends reliably.
+      Note: is_safe() is a state-independent method, so
+      it only returns true if all subevaluators are safe.
 
       Note that we could get more fine-grained information when
       considering of reliability for a given evaluated state. For
-      example, if we use h1 (unreliable) and h2 (reliable) and have a
+      example, if we use h1 (unsafe) and h2 (safe) and have a
       state where h1 is finite and h2 is infinite, then we can
-      *reliably* mark the state as a dead end. There is currently no
+      *safely* mark the state as a dead end. There is currently no
       way to exploit such state-based information, and hence we do not
       compute it.
     */
-
-    virtual bool dead_ends_are_reliable() const override;
+    virtual bool is_safe() const override;
     virtual EvaluationResult compute_result(
         EvaluationContext &eval_context) override;
 

src/search/evaluators/const_evaluator.cc

@@ -1,5 +1,7 @@
 #include "const_evaluator.h"
 
+#include "../evaluation_result.h"
+
 #include "../plugins/plugin.h"
 
 using namespace std;
@@ -15,6 +17,9 @@ EvaluationResult ConstEvaluator::compute_result(EvaluationContext &) {
     result.set_evaluator_value(value);
     return result;
 }
+bool ConstEvaluator::is_safe() const {
+    return value < EvaluationResult::INFTY;
+}
 
 class ConstEvaluatorFeature
     : public plugins::TypedFeature<Evaluator, ConstEvaluator> {

src/search/evaluators/const_evaluator.h

@@ -21,6 +21,7 @@ class ConstEvaluator : public Evaluator {
     virtual void get_path_dependent_evaluators(
         std::set<Evaluator *> &) override {
     }
+    virtual bool is_safe() const override;
 };
 }
 

src/search/evaluators/weighted_evaluator.cc

@@ -19,8 +19,14 @@ WeightedEvaluator::WeightedEvaluator(
       weight(weight) {
 }
 
-bool WeightedEvaluator::dead_ends_are_reliable() const {
-    return evaluator->dead_ends_are_reliable();
+bool WeightedEvaluator::is_safe() const {
+    if (weight == 0) {
+        return true;
+    }
+    if (weight == EvaluationResult::INFTY) {
+        return false;
+    }
+    return evaluator->is_safe();
 }
 
 EvaluationResult WeightedEvaluator::compute_result(

src/search/evaluators/weighted_evaluator.h

@@ -19,7 +19,7 @@ class WeightedEvaluator : public Evaluator {
         const std::shared_ptr<Evaluator> &eval, int weight,
         const std::string &description, utils::Verbosity verbosity);
 
-    virtual bool dead_ends_are_reliable() const override;
+    virtual bool is_safe() const override;
     virtual EvaluationResult compute_result(
         EvaluationContext &eval_context) override;
     virtual void get_path_dependent_evaluators(

src/search/heuristics/cea_heuristic.cc

@@ -445,7 +445,7 @@ ContextEnhancedAdditiveHeuristic::~ContextEnhancedAdditiveHeuristic() {
         delete problem;
 }
 
-bool ContextEnhancedAdditiveHeuristic::dead_ends_are_reliable() const {
+bool ContextEnhancedAdditiveHeuristic::is_safe() const {
     return false;
 }
 

src/search/heuristics/cea_heuristic.h

@@ -58,7 +58,7 @@ class ContextEnhancedAdditiveHeuristic : public Heuristic {
         const std::shared_ptr<AbstractTask> &transform, bool cache_estimates,
         const std::string &description, utils::Verbosity verbosity);
     ~ContextEnhancedAdditiveHeuristic();
-    virtual bool dead_ends_are_reliable() const override;
+    virtual bool is_safe() const override;
 };
 }
 

src/search/heuristics/cg_heuristic.cc

@@ -44,7 +44,7 @@ CGHeuristic::CGHeuristic(
     transition_graphs = factory.build_dtgs();
 }
 
-bool CGHeuristic::dead_ends_are_reliable() const {
+bool CGHeuristic::is_safe() const {
     return false;
 }
 

src/search/heuristics/cg_heuristic.h

@@ -45,7 +45,7 @@ class CGHeuristic : public Heuristic {
         int max_cache_size, tasks::AxiomHandlingType axiom_hanlding,
         const std::shared_ptr<AbstractTask> &transform, bool cache_estimates,
         const std::string &description, utils::Verbosity verbosity);
-    virtual bool dead_ends_are_reliable() const override;
+    virtual bool is_safe() const override;
 };
 }
 

src/search/heuristics/hm_heuristic.cc

@@ -27,7 +27,7 @@ HMHeuristic::HMHeuristic(
     generate_all_tuples();
 }
 
-bool HMHeuristic::dead_ends_are_reliable() const {
+bool HMHeuristic::is_safe() const {
     return !task_properties::has_axioms(task_proxy) && !has_cond_effects;
 }
 

src/search/heuristics/hm_heuristic.h

@@ -67,7 +67,7 @@ class HMHeuristic : public Heuristic {
         bool cache_estimates, const std::string &description,
         utils::Verbosity verbosity);
 
-    virtual bool dead_ends_are_reliable() const override;
+    virtual bool is_safe() const override;
 };
 }
 

src/search/heuristics/relaxation_heuristic.cc

@@ -110,7 +110,7 @@ RelaxationHeuristic::RelaxationHeuristic(
     }
 }
 
-bool RelaxationHeuristic::dead_ends_are_reliable() const {
+bool RelaxationHeuristic::is_safe() const {
     return !task_properties::has_axioms(task_proxy);
 }
 

src/search/heuristics/relaxation_heuristic.h

@@ -116,7 +116,7 @@ class RelaxationHeuristic : public Heuristic {
         const std::shared_ptr<AbstractTask> &transform, bool cache_estimates,
         const std::string &description, utils::Verbosity verbosity);
 
-    virtual bool dead_ends_are_reliable() const override;
+    virtual bool is_safe() const override;
 };
 
 extern void add_relaxation_heuristic_options_to_feature(

src/search/landmarks/landmark_cost_partitioning_heuristic.cc

@@ -78,7 +78,7 @@ int LandmarkCostPartitioningHeuristic::get_heuristic_value(
     }
 }
 
-bool LandmarkCostPartitioningHeuristic::dead_ends_are_reliable() const {
+bool LandmarkCostPartitioningHeuristic::is_safe() const {
     return true;
 }
 

src/search/landmarks/landmark_cost_partitioning_heuristic.h

@@ -32,7 +32,7 @@ class LandmarkCostPartitioningHeuristic : public LandmarkHeuristic {
         CostPartitioningMethod cost_partitioning, bool alm,
         lp::LPSolverType lpsolver);
 
-    virtual bool dead_ends_are_reliable() const override;
+    virtual bool is_safe() const override;
 };
 }
 

src/search/landmarks/landmark_sum_heuristic.cc

@@ -103,7 +103,7 @@ int LandmarkSumHeuristic::get_heuristic_value(const State &ancestor_state) {
     return h;
 }
 
-bool LandmarkSumHeuristic::dead_ends_are_reliable() const {
+bool LandmarkSumHeuristic::is_safe() const {
     return dead_ends_reliable;
 }
 

src/search/landmarks/landmark_sum_heuristic.h

@@ -29,7 +29,7 @@ class LandmarkSumHeuristic : public LandmarkHeuristic {
         const std::string &description, utils::Verbosity verbosity,
         tasks::AxiomHandlingType axioms);
 
-    virtual bool dead_ends_are_reliable() const override;
+    virtual bool is_safe() const override;
 };
 }
 

src/search/open_list.h

@@ -122,6 +122,11 @@ class OpenList {
     virtual bool is_dead_end(EvaluationContext &eval_context) const = 0;
     virtual bool is_reliable_dead_end(
         EvaluationContext &eval_context) const = 0;
+    /*
+      If for some solvable task no reachable goal state is ever inserted
+      into the open list then it is not complete, i.e. is_complete is false.
+    */
+    virtual bool is_complete() const = 0;
 };
 
 using StateOpenListEntry = StateID;