added missing negation of numeric constraints in negation normal form. improve argparsing according to issue #16

Author: drexlerd

exe/loki.cpp

@@ -22,15 +22,14 @@
 
 int main(int argc, char** argv)
 {
-    auto program = argparse::ArgumentParser("AStar search.");
-    program.add_argument("-D", "--domain-filepath").required().help("The path to the PDDL domain file.");
-    program.add_argument("-P", "--problem-filepath").default_value("").help("The path to the PDDL problem file.");
-    program.add_argument("-OD", "--out-domain-filepath").default_value("").help("The path to the output PDDL domain file.");
-    program.add_argument("-OP", "--out-problem-filepath").default_value("").help("The path to the output PDDL problem file.");
+    auto program = argparse::ArgumentParser("loki");
+    program.add_argument("domain").required().help("The path to the PDDL domain file.");
+    program.add_argument("problem").default_value("").help("The path to the PDDL problem file.");
+    program.add_argument("-OD", "--out-domain").default_value("").help("The path to the output PDDL domain file.");
+    program.add_argument("-OP", "--out-problem").default_value("").help("The path to the output PDDL problem file.");
     program.add_argument("-S", "--strict").default_value(false).implicit_value(true).help("Enable strict parsing mode.");
-    program.add_argument("-Q", "--quiet").default_value(true).implicit_value(false).help("Disable quiet mode.");
-    /* TODO(Dominik): add translator options */
-    program.add_argument("-T", "--remove-typing").default_value(false).implicit_value(true).help("Enable removal of typing.");
+    program.add_argument("-V", "--verbose").default_value(false).implicit_value(true).help("Verbose prints.");
+    program.add_argument("--remove-typing").default_value(false).implicit_value(true).help("Enable removal of typing.");
 
     try
     {
@@ -43,13 +42,13 @@ int main(int argc, char** argv)
         std::exit(1);
     }
 
-    auto domain_filepath = program.get<std::string>("--domain-filepath");
-    auto problem_filepath = program.get<std::string>("--problem-filepath");
-    auto out_domain_filepath = program.get<std::string>("--out-domain-filepath");
-    auto out_problem_filepath = program.get<std::string>("--out-problem-filepath");
+    auto domain_filepath = program.get<std::string>("domain");
+    auto problem_filepath = program.get<std::string>("problem");
+    auto out_domain_filepath = program.get<std::string>("--out-domain");
+    auto out_problem_filepath = program.get<std::string>("--out-problem");
 
     auto parser_options = loki::ParserOptions();
-    parser_options.quiet = program.get<bool>("--quiet");
+    parser_options.verbose = program.get<bool>("--verbose");
     parser_options.strict = program.get<bool>("--strict");
 
     auto translator_options = loki::TranslatorOptions();
@@ -59,7 +58,8 @@ int main(int argc, char** argv)
     const auto domain = parser.get_domain();
 
     const auto domain_translation_result = loki::translate(domain, translator_options);
-    std::cout << *domain_translation_result.get_translated_domain() << std::endl;
+    if (parser_options.verbose)
+        std::cout << *domain_translation_result.get_translated_domain() << std::endl;
 
     if (!out_domain_filepath.empty())
     {
@@ -73,7 +73,8 @@ int main(int argc, char** argv)
         auto problem = parser.parse_problem(problem_filepath, parser_options);
 
         const auto translated_problem = loki::translate(problem, domain_translation_result, translator_options);
-        std::cout << *translated_problem << std::endl;
+        if (parser_options.verbose)
+            std::cout << *translated_problem << std::endl;
 
         if (!out_problem_filepath.empty())
         {

include/loki/details/ast/ast.hpp

@@ -99,6 +99,7 @@ struct BinaryOperator;
 struct BinaryComparatorGreater;
 struct BinaryComparatorLess;
 struct BinaryComparatorEqual;
+struct BinaryComparatorUnequal;
 struct BinaryComparatorGreaterEqual;
 struct BinaryComparatorLessEqual;
 struct BinaryComparator;
@@ -573,6 +574,10 @@ struct BinaryComparatorEqual : x3::position_tagged
 {
 };
 
+struct BinaryComparatorUnequal : x3::position_tagged
+{
+};
+
 struct BinaryComparatorGreaterEqual : x3::position_tagged
 {
 };
@@ -583,7 +588,12 @@ struct BinaryComparatorLessEqual : x3::position_tagged
 
 struct BinaryComparator :
     x3::position_tagged,
-    x3::variant<BinaryComparatorGreater, BinaryComparatorLess, BinaryComparatorEqual, BinaryComparatorGreaterEqual, BinaryComparatorLessEqual>
+    x3::variant<BinaryComparatorGreater,
+                BinaryComparatorLess,
+                BinaryComparatorEqual,
+                BinaryComparatorGreaterEqual,
+                BinaryComparatorUnequal,
+                BinaryComparatorLessEqual>
 {
     using base_type::base_type;
     using base_type::operator=;

include/loki/details/ast/printer.hpp

@@ -187,6 +187,8 @@ void write(const ast::BinaryComparatorLess& node, T formatter, std::ostream& out
 template<Formatter T>
 void write(const ast::BinaryComparatorEqual& node, T formatter, std::ostream& out);
 template<Formatter T>
+void write(const ast::BinaryComparatorUnequal& node, T formatter, std::ostream& out);
+template<Formatter T>
 void write(const ast::BinaryComparatorGreaterEqual& node, T formatter, std::ostream& out);
 template<Formatter T>
 void write(const ast::BinaryComparatorLessEqual& node, T formatter, std::ostream& out);

include/loki/details/pddl/domain_builder.hpp

@@ -53,6 +53,11 @@ class DomainBuilder
     /// @return the resulting `Domain`.
     Domain get_result();
 
+    /// @brief Finalizes the `Domain`, verify indexing schemes, and returns it.
+    /// The `DomainBuilder` is in an invalid state afterwards.
+    /// @return the resulting `Domain`.
+    Domain get_result_checked();
+
     /**
      * Get and modify components of the domain.
      */

include/loki/details/pddl/function_expressions.hpp

@@ -30,12 +30,14 @@ enum class BinaryComparatorEnum
     GREATER,        ///< ">"
     LESS,           ///< "<"
     EQUAL,          ///< "="
+    UNEQUAL,        ///< "!="
     GREATER_EQUAL,  ///< ">="
     LESS_EQUAL,     ///< "<="
 };
 
 extern std::unordered_map<BinaryComparatorEnum, std::string> binary_comparator_enum_to_string;
 extern std::ostream& operator<<(std::ostream& out, BinaryComparatorEnum element);
+extern BinaryComparatorEnum negate(BinaryComparatorEnum element);
 
 enum class BinaryOperatorEnum
 {

include/loki/details/pddl/parser_options.hpp

@@ -23,9 +23,9 @@ namespace loki
 struct ParserOptions
 {
     bool strict;
-    bool quiet;
+    bool verbose;
 
-    ParserOptions() : strict(false), quiet(true) {}
+    ParserOptions() : strict(false), verbose(false) {}
 };
 }
 

include/loki/details/pddl/problem_builder.hpp

@@ -47,22 +47,18 @@ class ProblemBuilder
 
 public:
     /// @brief Create a `ProblemBuilder` for a given `Domain`.
-    ///
-    /// Copies all elements from the domain repositories as external elements into the problem repositories.
-    /// We use canonical representations to retrieve syntactically equivalent elements from the domain in most cases,
-    /// especially for the critial ones such as Type, Predicate, FunctionSkeleton, Object and all of its nested elements.
-    /// We do not yet have a canonical representation for Condition, FunctionExpression, and Effect, meaning that there can be semantic duplicates.
-    ///
-    /// The canonical representation is important during translation to ensure that we can decouple the domain from the problem translation.
-    /// Let's assume we translate the domain first, meaning that we get new addresses for all elements and that we now translate a problem.
-    /// The copy step ensures that we reuse elements of the translated domain during the problem translation.
     explicit ProblemBuilder(Domain domain);
 
     /// @brief Finalizes the `Problem` and returns it.
     /// The `ProblemBuilder` is in an invalid state afterwards.
     /// @return the resulting `Problem`.
     Problem get_result(size_t problem_index);
 
+    /// @brief Finalizes the `Problem`, verify indexing schemes, and returns it.
+    /// The `ProblemBuilder` is in an invalid state afterwards.
+    /// @return the resulting `Problem`.
+    Problem get_result_checked(size_t problem_index);
+
     /**
      * Get and modify components of the problem.
      */

include/loki/details/pddl/translator.hpp

@@ -28,14 +28,12 @@ class DomainTranslationResult
 {
 private:
     Domain original_domain;  ///< used to check that a problem can be translated with this result.
-    Domain translated_typed_domain;
     Domain translated_domain;
 
 public:
-    DomainTranslationResult(Domain original_domain, Domain translated_typed_domain, Domain translated_domain);
+    DomainTranslationResult(Domain original_domain, Domain translated_domain);
 
     const Domain& get_original_domain() const;
-    const Domain& get_translated_typed_domain() const;
     const Domain& get_translated_domain() const;
 };
 

src/ast/parser.hpp

@@ -113,6 +113,7 @@ struct BinaryOperatorClass;
 struct BinaryComparatorGreaterClass;
 struct BinaryComparatorLessClass;
 struct BinaryComparatorEqualClass;
+struct BinaryComparatorUnequalClass;
 struct BinaryComparatorGreaterEqualClass;
 struct BinaryComparatorLessEqualClass;
 struct BinaryComparatorClass;
@@ -312,6 +313,7 @@ typedef x3::rule<BinaryOperatorClass, ast::BinaryOperator> binary_operator_type;
 typedef x3::rule<BinaryComparatorGreaterClass, ast::BinaryComparatorGreater> binary_comparator_greater_type;
 typedef x3::rule<BinaryComparatorLessClass, ast::BinaryComparatorLess> binary_comparator_less_type;
 typedef x3::rule<BinaryComparatorEqualClass, ast::BinaryComparatorEqual> binary_comparator_equal_type;
+typedef x3::rule<BinaryComparatorUnequalClass, ast::BinaryComparatorUnequal> binary_comparator_unequal_type;
 typedef x3::rule<BinaryComparatorGreaterEqualClass, ast::BinaryComparatorGreaterEqual> binary_comparator_greater_equal_type;
 typedef x3::rule<BinaryComparatorLessEqualClass, ast::BinaryComparatorLessEqual> binary_comparator_less_equal_type;
 typedef x3::rule<BinaryComparatorClass, ast::BinaryComparator> binary_comparator_type;
@@ -503,6 +505,7 @@ BOOST_SPIRIT_DECLARE(multi_operator_mul_type,
 BOOST_SPIRIT_DECLARE(binary_comparator_greater_type,
                      binary_comparator_less_type,
                      binary_comparator_equal_type,
+                     binary_comparator_unequal_type,
                      binary_comparator_greater_equal_type,
                      binary_comparator_less_equal_type,
                      binary_comparator_type)
@@ -680,6 +683,7 @@ parser::binary_operator_type const& binary_operator();
 parser::binary_comparator_greater_type const& binary_comparator_greater();
 parser::binary_comparator_less_type const& binary_comparator_less();
 parser::binary_comparator_equal_type const& binary_comparator_equal();
+parser::binary_comparator_unequal_type const& binary_comparator_unequal();
 parser::binary_comparator_greater_equal_type const& binary_comparator_greater_equal();
 parser::binary_comparator_less_equal_type const& binary_comparator_less_equal();
 parser::binary_comparator_type const& binary_comparator();

src/ast/parser_def.hpp

@@ -129,6 +129,7 @@ binary_operator_type const binary_operator = "binary_operator";
 binary_comparator_greater_type const binary_comparator_greater = "binary_comparator_greater";
 binary_comparator_less_type const binary_comparator_less = "binary_comparator_less";
 binary_comparator_equal_type const binary_comparator_equal = "binary_comparator_equal";
+binary_comparator_unequal_type const binary_comparator_unequal = "binary_comparator_unequal";
 binary_comparator_greater_equal_type const binary_comparator_greater_equal = "binary_comparator_greater_equal";
 binary_comparator_less_equal_type const binary_comparator_less_equal = "binary_comparator_less_equal";
 binary_comparator_type const binary_comparator = "binary_comparator";
@@ -334,10 +335,11 @@ const auto binary_operator_def = binary_operator_minus | binary_operator_div | m
 const auto binary_comparator_greater_def = lit('>') > x3::attr(ast::BinaryComparatorGreater {});
 const auto binary_comparator_less_def = lit('<') > x3::attr(ast::BinaryComparatorLess {});
 const auto binary_comparator_equal_def = lit('=') > x3::attr(ast::BinaryComparatorEqual {});
+const auto binary_comparator_unequal_def = lit('=') > x3::attr(ast::BinaryComparatorUnequal {});
 const auto binary_comparator_greater_equal_def = lit(">=") > x3::attr(ast::BinaryComparatorGreaterEqual {});
 const auto binary_comparator_less_equal_def = lit("<=") > x3::attr(ast::BinaryComparatorLessEqual {});
-const auto binary_comparator_def =
-    binary_comparator_greater_equal | binary_comparator_less_equal | binary_comparator_greater | binary_comparator_less | binary_comparator_equal;
+const auto binary_comparator_def = binary_comparator_greater_equal | binary_comparator_less_equal | binary_comparator_greater | binary_comparator_less
+                                   | binary_comparator_equal | binary_comparator_unequal;
 
 const auto function_head_def = (((lit('(') >> function_symbol) > *term) > lit(')'));
 const auto function_expression_def =
@@ -542,6 +544,7 @@ BOOST_SPIRIT_DEFINE(multi_operator_mul, multi_operator_plus, multi_operator, bin
 BOOST_SPIRIT_DEFINE(binary_comparator_greater,
                     binary_comparator_less,
                     binary_comparator_equal,
+                    binary_comparator_unequal,
                     binary_comparator_greater_equal,
                     binary_comparator_less_equal,
                     binary_comparator)
@@ -831,6 +834,9 @@ struct BinaryComparatorLessClass : x3::annotate_on_success
 struct BinaryComparatorEqualClass : x3::annotate_on_success
 {
 };
+struct BinaryComparatorUnequalClass : x3::annotate_on_success
+{
+};
 struct BinaryComparatorGreaterEqualClass : x3::annotate_on_success
 {
 };
@@ -1260,6 +1266,7 @@ parser::binary_operator_type const& binary_operator() { return parser::binary_op
 parser::binary_comparator_greater_type const& binary_comparator_greater() { return parser::binary_comparator_greater; }
 parser::binary_comparator_less_type const& binary_comparator_less() { return parser::binary_comparator_less; }
 parser::binary_comparator_equal_type const& binary_comparator_equal() { return parser::binary_comparator_equal; }
+parser::binary_comparator_unequal_type const& binary_comparator_unequal() { return parser::binary_comparator_unequal; }
 parser::binary_comparator_greater_equal_type const& binary_comparator_greater_equal() { return parser::binary_comparator_greater_equal; }
 parser::binary_comparator_less_equal_type const& binary_comparator_less_equal() { return parser::binary_comparator_less_equal; }
 parser::binary_comparator_type const& binary_comparator() { return parser::binary_comparator; }