diff --git a/.gitignore b/.gitignore new file mode 100644 index 00000000..fff4bea7 --- /dev/null +++ b/.gitignore @@ -0,0 +1,3 @@ +build/ +.vscode/ +cmdline.* diff --git a/src/.gitignore b/src/.gitignore new file mode 100644 index 00000000..32dd20fa --- /dev/null +++ b/src/.gitignore @@ -0,0 +1,6 @@ +.vscode/ +build/ +cmake-build-debug +cmake-build-* +.idea/ +src/.idea \ No newline at end of file diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 6bc8a5e5..9a92df16 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -115,3 +115,6 @@ endif (SAT) ## must be added *after* SAT due to the use of the printMemory function, which is currently defined in the SAT module ... this is probably not a good idea. target_link_libraries(pandaPIengine PUBLIC intDataStructures) + +# add plan verifiers +add_subdirectory(verifier) \ No newline at end of file diff --git a/src/sat/CMakeLists.txt b/src/sat/CMakeLists.txt index a2a323f2..4efa8a79 100644 --- a/src/sat/CMakeLists.txt +++ b/src/sat/CMakeLists.txt @@ -1,7 +1,16 @@ file(GLOB sat_SRC "*.h" "*.cpp") -add_library(sat ${sat_SRC}) +add_library(sat + ${sat_SRC} + ${pandaPIengine_SOURCE_DIR}/Util.cpp + ${pandaPIengine_SOURCE_DIR}/Debug.cpp + ${pandaPIengine_SOURCE_DIR}/Invariants.cpp) + target_compile_options(sat PUBLIC ${compiler_flags}) target_link_options(sat PUBLIC ${linker_flags}) +target_include_directories(sat + PUBLIC + ${pandaPIengine_SOURCE_DIR}/) +find_package(cryptominisat5) target_link_libraries(sat ipasircryptominisat5) diff --git a/src/sat/pdt.cpp b/src/sat/pdt.cpp index 225fe53b..6fbe7747 100644 --- a/src/sat/pdt.cpp +++ b/src/sat/pdt.cpp @@ -4,7 +4,7 @@ #include #include "pdt.h" #include "ipasir.h" -#include "../Util.h" +#include "Util.h" void printMemory(); @@ -675,12 +675,12 @@ void PDT::printDecomposition(Model * htn){ if (outputTask < htn->numActions) return; cout << outputID << " " << htn->taskNames[outputTask] << " -> " << - htn->methodNames[outputMethod]; + htn->methodNames[outputMethod] << endl; // output children for (PDT* & child : children){ int sub = child->getNextOutputTask(); - if (sub != -1) cout << " " << sub; + if (sub != -1) cout << "- " << sub << " " << htn->taskNames[child->outputTask] << endl; } cout << endl; diff --git a/src/sat/state_formula.cpp b/src/sat/state_formula.cpp index 955d8f5e..7489e7c4 100644 --- a/src/sat/state_formula.cpp +++ b/src/sat/state_formula.cpp @@ -1,6 +1,6 @@ #include "state_formula.h" #include "ipasir.h" -#include "../Invariants.h" +#include "Invariants.h" #include #include diff --git a/src/verifier/CMakeLists.txt b/src/verifier/CMakeLists.txt new file mode 100644 index 00000000..ca5ba5fa --- /dev/null +++ b/src/verifier/CMakeLists.txt @@ -0,0 +1,98 @@ +project(verifier) + + +# commands for the util library +file(GLOB UTIL_SOURCE_FILES "util/src/*.cpp") + +add_library(util + ${UTIL_SOURCE_FILES} + util/src/distribution.cpp) + +target_include_directories(util + PUBLIC + ${pandaPIengine_SOURCE_DIR} + util/include +) + +target_link_libraries(util + PUBLIC + intDataStructures +) + +add_library(sat_verifier + sat_verifier/src/sat_verifier.cpp + sat_verifier/src/variables.cpp + sat_verifier/src/constraints.cpp + ${pandaPIengine_SOURCE_DIR}/Model.cpp + ${pandaPIengine_SOURCE_DIR}/Util.cpp + ${pandaPIengine_SOURCE_DIR}/Debug.cpp + ${pandaPIengine_SOURCE_DIR}/ProgressionNetwork.cpp + ${pandaPIengine_SOURCE_DIR}/Invariants.cpp sat_verifier/src/depth.cpp sat_verifier/src/marker.cpp) + +target_include_directories(sat_verifier + PUBLIC + ${PROJECT_SOURCE_DIR}/include + ${PROJECT_SOURCE_DIR}/sat_verifier/include + ${pandaPIengine_SOURCE_DIR}/ +) + +target_link_libraries(sat_verifier + PUBLIC + util + intDataStructures + sat +) + +# commands for command-line arguments +find_program(GENGETOPT gengetopt) + +add_custom_command( + OUTPUT ${PROJECT_SOURCE_DIR}/cmdline.h ${PROJECT_SOURCE_DIR}/cmdline.c + COMMAND gengetopt --include-getopt --default-optional --unamed-opts -i options.ggo + DEPENDS options.ggo + WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR} + COMMENT "Generating getopt parser code (cmdline.{h,c}) ..." + VERBATIM +) + +add_custom_target(cmd + DEPENDS cmdline.h cmdline.c +) + +file(GLOB VERIFIER_SOUCE_FILES "src/*.cpp") + +add_executable(run_verifier ${VERIFIER_SOUCE_FILES} cmdline.c cmdline.h) + +target_link_libraries(run_verifier + PUBLIC + sat_verifier +) + +target_include_directories(run_verifier + PUBLIC + ${PROJECT_SOURCE_DIR} + ${PROJECT_SOURCE_DIR}/include +) + +add_subdirectory(test) +enable_testing() +add_executable(test_util + ${CMAKE_CURRENT_SOURCE_DIR}/test/test_util.cpp) +target_link_libraries(test_util + PUBLIC + test_main + catch2 + util) + +add_executable(test_depth + ${CMAKE_CURRENT_SOURCE_DIR}/test/test_depth.cpp + ${pandaPIengine_SOURCE_DIR}/ProgressionNetwork.cpp) + +target_link_libraries(test_depth + PUBLIC + test_main + catch2 + sat_verifier) +target_include_directories(test_depth + PUBLIC + ${pandaPIengine_SOURCE_DIR}/) \ No newline at end of file diff --git a/src/verifier/cmdline.c b/src/verifier/cmdline.c new file mode 100644 index 00000000..13c597a2 --- /dev/null +++ b/src/verifier/cmdline.c @@ -0,0 +1,768 @@ +/* + File autogenerated by gengetopt version 2.23 + generated with the following command: + gengetopt --string-parser -u + + The developers of gengetopt consider the fixed text that goes in all + gengetopt output files to be in the public domain: + we make no copyright claims on it. +*/ + +/* If we use autoconf. */ +#ifdef HAVE_CONFIG_H +#include "config.h" +#endif + +#include +#include +#include + +#ifndef FIX_UNUSED +#define FIX_UNUSED(X) (void) (X) /* avoid warnings for unused params */ +#endif + +#include + +#include "cmdline.h" + +const char *gengetopt_args_info_purpose = "Plan Verification"; + +const char *gengetopt_args_info_usage = "Usage: ./runVerifier [options]"; + +const char *gengetopt_args_info_versiontext = ""; + +const char *gengetopt_args_info_description = ""; + +const char *gengetopt_args_info_help[] = { + " --help Print help and exit", + " -V, --version Print version and exit", + " -h, --htn=STRING the path to the input HTN problem file", + " -p, --plan=STRING the path to the input plan file", + " -o, --optimizeDepth calculating optimal depth (default=off)", + 0 +}; + +typedef enum {ARG_NO + , ARG_FLAG + , ARG_STRING +} cmdline_parser_arg_type; + +static +void clear_given (struct gengetopt_args_info *args_info); +static +void clear_args (struct gengetopt_args_info *args_info); + +static int +cmdline_parser_internal (int argc, char **argv, struct gengetopt_args_info *args_info, + struct cmdline_parser_params *params, const char *additional_error); + +static int +cmdline_parser_required2 (struct gengetopt_args_info *args_info, const char *prog_name, const char *additional_error); +struct line_list +{ + char * string_arg; + struct line_list * next; +}; + +static struct line_list *cmd_line_list = 0; +static struct line_list *cmd_line_list_tmp = 0; + +static void +free_cmd_list(void) +{ + /* free the list of a previous call */ + if (cmd_line_list) + { + while (cmd_line_list) { + cmd_line_list_tmp = cmd_line_list; + cmd_line_list = cmd_line_list->next; + free (cmd_line_list_tmp->string_arg); + free (cmd_line_list_tmp); + } + } +} + + +static char * +gengetopt_strdup (const char *s); + +static +void clear_given (struct gengetopt_args_info *args_info) +{ + args_info->help_given = 0 ; + args_info->version_given = 0 ; + args_info->htn_given = 0 ; + args_info->plan_given = 0 ; + args_info->optimizeDepth_given = 0 ; +} + +static +void clear_args (struct gengetopt_args_info *args_info) +{ + FIX_UNUSED (args_info); + args_info->htn_arg = NULL; + args_info->htn_orig = NULL; + args_info->plan_arg = NULL; + args_info->plan_orig = NULL; + args_info->optimizeDepth_flag = 0; + +} + +static +void init_args_info(struct gengetopt_args_info *args_info) +{ + + + args_info->help_help = gengetopt_args_info_help[0] ; + args_info->version_help = gengetopt_args_info_help[1] ; + args_info->htn_help = gengetopt_args_info_help[2] ; + args_info->plan_help = gengetopt_args_info_help[3] ; + args_info->optimizeDepth_help = gengetopt_args_info_help[4] ; + +} + +void +cmdline_parser_print_version (void) +{ + printf ("%s %s\n", + (strlen(CMDLINE_PARSER_PACKAGE_NAME) ? CMDLINE_PARSER_PACKAGE_NAME : CMDLINE_PARSER_PACKAGE), + CMDLINE_PARSER_VERSION); + + if (strlen(gengetopt_args_info_versiontext) > 0) + printf("\n%s\n", gengetopt_args_info_versiontext); +} + +static void print_help_common(void) +{ + size_t len_purpose = strlen(gengetopt_args_info_purpose); + size_t len_usage = strlen(gengetopt_args_info_usage); + + if (len_usage > 0) { + printf("%s\n", gengetopt_args_info_usage); + } + if (len_purpose > 0) { + printf("%s\n", gengetopt_args_info_purpose); + } + + if (len_usage || len_purpose) { + printf("\n"); + } + + if (strlen(gengetopt_args_info_description) > 0) { + printf("%s\n\n", gengetopt_args_info_description); + } +} + +void +cmdline_parser_print_help (void) +{ + int i = 0; + print_help_common(); + while (gengetopt_args_info_help[i]) + printf("%s\n", gengetopt_args_info_help[i++]); +} + +void +cmdline_parser_init (struct gengetopt_args_info *args_info) +{ + clear_given (args_info); + clear_args (args_info); + init_args_info (args_info); + + args_info->inputs = 0; + args_info->inputs_num = 0; +} + +void +cmdline_parser_params_init(struct cmdline_parser_params *params) +{ + if (params) + { + params->override = 0; + params->initialize = 1; + params->check_required = 1; + params->check_ambiguity = 0; + params->print_errors = 1; + } +} + +struct cmdline_parser_params * +cmdline_parser_params_create(void) +{ + struct cmdline_parser_params *params = + (struct cmdline_parser_params *)malloc(sizeof(struct cmdline_parser_params)); + cmdline_parser_params_init(params); + return params; +} + +static void +free_string_field (char **s) +{ + if (*s) + { + free (*s); + *s = 0; + } +} + + +static void +cmdline_parser_release (struct gengetopt_args_info *args_info) +{ + unsigned int i; + free_string_field (&(args_info->htn_arg)); + free_string_field (&(args_info->htn_orig)); + free_string_field (&(args_info->plan_arg)); + free_string_field (&(args_info->plan_orig)); + + + for (i = 0; i < args_info->inputs_num; ++i) + free (args_info->inputs [i]); + + if (args_info->inputs_num) + free (args_info->inputs); + + clear_given (args_info); +} + + +static void +write_into_file(FILE *outfile, const char *opt, const char *arg, const char *values[]) +{ + FIX_UNUSED (values); + if (arg) { + fprintf(outfile, "%s=\"%s\"\n", opt, arg); + } else { + fprintf(outfile, "%s\n", opt); + } +} + + +int +cmdline_parser_dump(FILE *outfile, struct gengetopt_args_info *args_info) +{ + int i = 0; + + if (!outfile) + { + fprintf (stderr, "%s: cannot dump options to stream\n", CMDLINE_PARSER_PACKAGE); + return EXIT_FAILURE; + } + + if (args_info->help_given) + write_into_file(outfile, "help", 0, 0 ); + if (args_info->version_given) + write_into_file(outfile, "version", 0, 0 ); + if (args_info->htn_given) + write_into_file(outfile, "htn", args_info->htn_orig, 0); + if (args_info->plan_given) + write_into_file(outfile, "plan", args_info->plan_orig, 0); + if (args_info->optimizeDepth_given) + write_into_file(outfile, "optimizeDepth", 0, 0 ); + + + i = EXIT_SUCCESS; + return i; +} + +int +cmdline_parser_file_save(const char *filename, struct gengetopt_args_info *args_info) +{ + FILE *outfile; + int i = 0; + + outfile = fopen(filename, "w"); + + if (!outfile) + { + fprintf (stderr, "%s: cannot open file for writing: %s\n", CMDLINE_PARSER_PACKAGE, filename); + return EXIT_FAILURE; + } + + i = cmdline_parser_dump(outfile, args_info); + fclose (outfile); + + return i; +} + +void +cmdline_parser_free (struct gengetopt_args_info *args_info) +{ + cmdline_parser_release (args_info); +} + +/** @brief replacement of strdup, which is not standard */ +char * +gengetopt_strdup (const char *s) +{ + char *result = 0; + if (!s) + return result; + + result = (char*)malloc(strlen(s) + 1); + if (result == (char*)0) + return (char*)0; + strcpy(result, s); + return result; +} + +int +cmdline_parser (int argc, char **argv, struct gengetopt_args_info *args_info) +{ + return cmdline_parser2 (argc, argv, args_info, 0, 1, 1); +} + +int +cmdline_parser_ext (int argc, char **argv, struct gengetopt_args_info *args_info, + struct cmdline_parser_params *params) +{ + int result; + result = cmdline_parser_internal (argc, argv, args_info, params, 0); + + if (result == EXIT_FAILURE) + { + cmdline_parser_free (args_info); + exit (EXIT_FAILURE); + } + + return result; +} + +int +cmdline_parser2 (int argc, char **argv, struct gengetopt_args_info *args_info, int override, int initialize, int check_required) +{ + int result; + struct cmdline_parser_params params; + + params.override = override; + params.initialize = initialize; + params.check_required = check_required; + params.check_ambiguity = 0; + params.print_errors = 1; + + result = cmdline_parser_internal (argc, argv, args_info, ¶ms, 0); + + if (result == EXIT_FAILURE) + { + cmdline_parser_free (args_info); + exit (EXIT_FAILURE); + } + + return result; +} + +int +cmdline_parser_required (struct gengetopt_args_info *args_info, const char *prog_name) +{ + int result = EXIT_SUCCESS; + + if (cmdline_parser_required2(args_info, prog_name, 0) > 0) + result = EXIT_FAILURE; + + if (result == EXIT_FAILURE) + { + cmdline_parser_free (args_info); + exit (EXIT_FAILURE); + } + + return result; +} + +int +cmdline_parser_required2 (struct gengetopt_args_info *args_info, const char *prog_name, const char *additional_error) +{ + int error_occurred = 0; + FIX_UNUSED (additional_error); + + /* checks for required options */ + if (! args_info->htn_given) + { + fprintf (stderr, "%s: '--htn' ('-h') option required%s\n", prog_name, (additional_error ? additional_error : "")); + error_occurred = 1; + } + + if (! args_info->plan_given) + { + fprintf (stderr, "%s: '--plan' ('-p') option required%s\n", prog_name, (additional_error ? additional_error : "")); + error_occurred = 1; + } + + + /* checks for dependences among options */ + + return error_occurred; +} + + +static char *package_name = 0; + +/** + * @brief updates an option + * @param field the generic pointer to the field to update + * @param orig_field the pointer to the orig field + * @param field_given the pointer to the number of occurrence of this option + * @param prev_given the pointer to the number of occurrence already seen + * @param value the argument for this option (if null no arg was specified) + * @param possible_values the possible values for this option (if specified) + * @param default_value the default value (in case the option only accepts fixed values) + * @param arg_type the type of this option + * @param check_ambiguity @see cmdline_parser_params.check_ambiguity + * @param override @see cmdline_parser_params.override + * @param no_free whether to free a possible previous value + * @param multiple_option whether this is a multiple option + * @param long_opt the corresponding long option + * @param short_opt the corresponding short option (or '-' if none) + * @param additional_error possible further error specification + */ +static +int update_arg(void *field, char **orig_field, + unsigned int *field_given, unsigned int *prev_given, + char *value, const char *possible_values[], + const char *default_value, + cmdline_parser_arg_type arg_type, + int check_ambiguity, int override, + int no_free, int multiple_option, + const char *long_opt, char short_opt, + const char *additional_error) +{ + char *stop_char = 0; + const char *val = value; + int found; + char **string_field; + FIX_UNUSED (field); + + stop_char = 0; + found = 0; + + if (!multiple_option && prev_given && (*prev_given || (check_ambiguity && *field_given))) + { + if (short_opt != '-') + fprintf (stderr, "%s: `--%s' (`-%c') option given more than once%s\n", + package_name, long_opt, short_opt, + (additional_error ? additional_error : "")); + else + fprintf (stderr, "%s: `--%s' option given more than once%s\n", + package_name, long_opt, + (additional_error ? additional_error : "")); + return 1; /* failure */ + } + + FIX_UNUSED (default_value); + + if (field_given && *field_given && ! override) + return 0; + if (prev_given) + (*prev_given)++; + if (field_given) + (*field_given)++; + if (possible_values) + val = possible_values[found]; + + switch(arg_type) { + case ARG_FLAG: + *((int *)field) = !*((int *)field); + break; + case ARG_STRING: + if (val) { + string_field = (char **)field; + if (!no_free && *string_field) + free (*string_field); /* free previous string */ + *string_field = gengetopt_strdup (val); + } + break; + default: + break; + }; + + FIX_UNUSED(stop_char); + + /* store the original value */ + switch(arg_type) { + case ARG_NO: + case ARG_FLAG: + break; + default: + if (value && orig_field) { + if (no_free) { + *orig_field = value; + } else { + if (*orig_field) + free (*orig_field); /* free previous string */ + *orig_field = gengetopt_strdup (value); + } + } + }; + + return 0; /* OK */ +} + + +int +cmdline_parser_internal ( + int argc, char **argv, struct gengetopt_args_info *args_info, + struct cmdline_parser_params *params, const char *additional_error) +{ + int c; /* Character of the parsed option. */ + + int error_occurred = 0; + struct gengetopt_args_info local_args_info; + + int override; + int initialize; + int check_required; + int check_ambiguity; + + package_name = argv[0]; + + /* TODO: Why is this here? It is not used anywhere. */ + override = params->override; + FIX_UNUSED(override); + + initialize = params->initialize; + check_required = params->check_required; + + /* TODO: Why is this here? It is not used anywhere. */ + check_ambiguity = params->check_ambiguity; + FIX_UNUSED(check_ambiguity); + + if (initialize) + cmdline_parser_init (args_info); + + cmdline_parser_init (&local_args_info); + + optarg = 0; + optind = 0; + opterr = params->print_errors; + optopt = '?'; + + while (1) + { + int option_index = 0; + + static struct option long_options[] = { + { "help", 0, NULL, 0 }, + { "version", 0, NULL, 'V' }, + { "htn", 1, NULL, 'h' }, + { "plan", 1, NULL, 'p' }, + { "optimizeDepth", 0, NULL, 'o' }, + { 0, 0, 0, 0 } + }; + + c = getopt_long (argc, argv, "Vh:p:o", long_options, &option_index); + + if (c == -1) break; /* Exit from `while (1)' loop. */ + + switch (c) + { + case 'V': /* Print version and exit. */ + cmdline_parser_print_version (); + cmdline_parser_free (&local_args_info); + exit (EXIT_SUCCESS); + + case 'h': /* the path to the input HTN problem file. */ + + + if (update_arg( (void *)&(args_info->htn_arg), + &(args_info->htn_orig), &(args_info->htn_given), + &(local_args_info.htn_given), optarg, 0, 0, ARG_STRING, + check_ambiguity, override, 0, 0, + "htn", 'h', + additional_error)) + goto failure; + + break; + case 'p': /* the path to the input plan file. */ + + + if (update_arg( (void *)&(args_info->plan_arg), + &(args_info->plan_orig), &(args_info->plan_given), + &(local_args_info.plan_given), optarg, 0, 0, ARG_STRING, + check_ambiguity, override, 0, 0, + "plan", 'p', + additional_error)) + goto failure; + + break; + case 'o': /* calculating optimal depth. */ + + + if (update_arg((void *)&(args_info->optimizeDepth_flag), 0, &(args_info->optimizeDepth_given), + &(local_args_info.optimizeDepth_given), optarg, 0, 0, ARG_FLAG, + check_ambiguity, override, 1, 0, "optimizeDepth", 'o', + additional_error)) + goto failure; + + break; + + case 0: /* Long option with no short option */ + if (strcmp (long_options[option_index].name, "help") == 0) { + cmdline_parser_print_help (); + cmdline_parser_free (&local_args_info); + exit (EXIT_SUCCESS); + } + + case '?': /* Invalid option. */ + /* `getopt_long' already printed an error message. */ + goto failure; + + default: /* bug: option not considered. */ + fprintf (stderr, "%s: option unknown: %c%s\n", CMDLINE_PARSER_PACKAGE, c, (additional_error ? additional_error : "")); + abort (); + } /* switch */ + } /* while */ + + + + if (check_required) + { + error_occurred += cmdline_parser_required2 (args_info, argv[0], additional_error); + } + + cmdline_parser_release (&local_args_info); + + if ( error_occurred ) + return (EXIT_FAILURE); + + if (optind < argc) + { + int i = 0 ; + int found_prog_name = 0; + /* whether program name, i.e., argv[0], is in the remaining args + (this may happen with some implementations of getopt, + but surely not with the one included by gengetopt) */ + + i = optind; + while (i < argc) + if (argv[i++] == argv[0]) { + found_prog_name = 1; + break; + } + i = 0; + + args_info->inputs_num = argc - optind - found_prog_name; + args_info->inputs = + (char **)(malloc ((args_info->inputs_num)*sizeof(char *))) ; + while (optind < argc) + if (argv[optind++] != argv[0]) + args_info->inputs[ i++ ] = gengetopt_strdup (argv[optind-1]) ; + } + + return 0; + +failure: + + cmdline_parser_release (&local_args_info); + return (EXIT_FAILURE); +} + +static unsigned int +cmdline_parser_create_argv(const char *cmdline_, char ***argv_ptr, const char *prog_name) +{ + char *cmdline, *p; + size_t n = 0, j; + int i; + + if (prog_name) { + cmd_line_list_tmp = (struct line_list *) malloc (sizeof (struct line_list)); + cmd_line_list_tmp->next = cmd_line_list; + cmd_line_list = cmd_line_list_tmp; + cmd_line_list->string_arg = gengetopt_strdup (prog_name); + + ++n; + } + + cmdline = gengetopt_strdup(cmdline_); + p = cmdline; + + while (p && strlen(p)) + { + j = strcspn(p, " \t"); + ++n; + if (j && j < strlen(p)) + { + p[j] = '\0'; + + cmd_line_list_tmp = (struct line_list *) malloc (sizeof (struct line_list)); + cmd_line_list_tmp->next = cmd_line_list; + cmd_line_list = cmd_line_list_tmp; + cmd_line_list->string_arg = gengetopt_strdup (p); + + p += (j+1); + p += strspn(p, " \t"); + } + else + { + cmd_line_list_tmp = (struct line_list *) malloc (sizeof (struct line_list)); + cmd_line_list_tmp->next = cmd_line_list; + cmd_line_list = cmd_line_list_tmp; + cmd_line_list->string_arg = gengetopt_strdup (p); + + break; + } + } + + *argv_ptr = (char **) malloc((n + 1) * sizeof(char *)); + cmd_line_list_tmp = cmd_line_list; + for (i = (n-1); i >= 0; --i) + { + (*argv_ptr)[i] = cmd_line_list_tmp->string_arg; + cmd_line_list_tmp = cmd_line_list_tmp->next; + } + + (*argv_ptr)[n] = 0; + + free(cmdline); + return n; +} + +int +cmdline_parser_string(const char *cmdline, struct gengetopt_args_info *args_info, const char *prog_name) +{ + return cmdline_parser_string2(cmdline, args_info, prog_name, 0, 1, 1); +} + +int +cmdline_parser_string2(const char *cmdline, struct gengetopt_args_info *args_info, const char *prog_name, + int override, int initialize, int check_required) +{ + struct cmdline_parser_params params; + + params.override = override; + params.initialize = initialize; + params.check_required = check_required; + params.check_ambiguity = 0; + params.print_errors = 1; + + return cmdline_parser_string_ext(cmdline, args_info, prog_name, ¶ms); +} + +int +cmdline_parser_string_ext(const char *cmdline, struct gengetopt_args_info *args_info, const char *prog_name, + struct cmdline_parser_params *params) +{ + char **argv_ptr = 0; + int result; + unsigned int argc; + + argc = cmdline_parser_create_argv(cmdline, &argv_ptr, prog_name); + + result = + cmdline_parser_internal (argc, argv_ptr, args_info, params, 0); + + if (argv_ptr) + { + free (argv_ptr); + } + + free_cmd_list(); + + if (result == EXIT_FAILURE) + { + cmdline_parser_free (args_info); + exit (EXIT_FAILURE); + } + + return result; +} + +/* vim: set ft=c noet ts=8 sts=8 sw=8 tw=80 nojs spell : */ diff --git a/src/verifier/cmdline.h b/src/verifier/cmdline.h new file mode 100644 index 00000000..dfdfd693 --- /dev/null +++ b/src/verifier/cmdline.h @@ -0,0 +1,224 @@ +/** @file cmdline.h + * @brief The header file for the command line option parser + * generated by GNU Gengetopt version 2.23 + * http://www.gnu.org/software/gengetopt. + * DO NOT modify this file, since it can be overwritten + * @author GNU Gengetopt */ + +#ifndef CMDLINE_H +#define CMDLINE_H + +/* If we use autoconf. */ +#ifdef HAVE_CONFIG_H +#include "config.h" +#endif + +#include /* for FILE */ + +#ifdef __cplusplus +extern "C" { +#endif /* __cplusplus */ + +#ifndef CMDLINE_PARSER_PACKAGE +/** @brief the program name (used for printing errors) */ +#define CMDLINE_PARSER_PACKAGE "planVerifier" +#endif + +#ifndef CMDLINE_PARSER_PACKAGE_NAME +/** @brief the complete program name (used for help and version) */ +#define CMDLINE_PARSER_PACKAGE_NAME "planVerifier" +#endif + +#ifndef CMDLINE_PARSER_VERSION +/** @brief the program version */ +#define CMDLINE_PARSER_VERSION "0.1" +#endif + +/** @brief Where the command line options are stored */ +struct gengetopt_args_info +{ + const char *help_help; /**< @brief Print help and exit help description. */ + const char *version_help; /**< @brief Print version and exit help description. */ + char * htn_arg; /**< @brief the path to the input HTN problem file. */ + char * htn_orig; /**< @brief the path to the input HTN problem file original value given at command line. */ + const char *htn_help; /**< @brief the path to the input HTN problem file help description. */ + char * plan_arg; /**< @brief the path to the input plan file. */ + char * plan_orig; /**< @brief the path to the input plan file original value given at command line. */ + const char *plan_help; /**< @brief the path to the input plan file help description. */ + int optimizeDepth_flag; /**< @brief calculating optimal depth (default=off). */ + const char *optimizeDepth_help; /**< @brief calculating optimal depth help description. */ + + unsigned int help_given ; /**< @brief Whether help was given. */ + unsigned int version_given ; /**< @brief Whether version was given. */ + unsigned int htn_given ; /**< @brief Whether htn was given. */ + unsigned int plan_given ; /**< @brief Whether plan was given. */ + unsigned int optimizeDepth_given ; /**< @brief Whether optimizeDepth was given. */ + + char **inputs ; /**< @brief unnamed options (options without names) */ + unsigned inputs_num ; /**< @brief unnamed options number */ +} ; + +/** @brief The additional parameters to pass to parser functions */ +struct cmdline_parser_params +{ + int override; /**< @brief whether to override possibly already present options (default 0) */ + int initialize; /**< @brief whether to initialize the option structure gengetopt_args_info (default 1) */ + int check_required; /**< @brief whether to check that all required options were provided (default 1) */ + int check_ambiguity; /**< @brief whether to check for options already specified in the option structure gengetopt_args_info (default 0) */ + int print_errors; /**< @brief whether getopt_long should print an error message for a bad option (default 1) */ +} ; + +/** @brief the purpose string of the program */ +extern const char *gengetopt_args_info_purpose; +/** @brief the usage string of the program */ +extern const char *gengetopt_args_info_usage; +/** @brief the description string of the program */ +extern const char *gengetopt_args_info_description; +/** @brief all the lines making the help output */ +extern const char *gengetopt_args_info_help[]; + +/** + * The command line parser + * @param argc the number of command line options + * @param argv the command line options + * @param args_info the structure where option information will be stored + * @return 0 if everything went fine, NON 0 if an error took place + */ +int cmdline_parser (int argc, char **argv, + struct gengetopt_args_info *args_info); + +/** + * The command line parser (version with additional parameters - deprecated) + * @param argc the number of command line options + * @param argv the command line options + * @param args_info the structure where option information will be stored + * @param override whether to override possibly already present options + * @param initialize whether to initialize the option structure my_args_info + * @param check_required whether to check that all required options were provided + * @return 0 if everything went fine, NON 0 if an error took place + * @deprecated use cmdline_parser_ext() instead + */ +int cmdline_parser2 (int argc, char **argv, + struct gengetopt_args_info *args_info, + int override, int initialize, int check_required); + +/** + * The command line parser (version with additional parameters) + * @param argc the number of command line options + * @param argv the command line options + * @param args_info the structure where option information will be stored + * @param params additional parameters for the parser + * @return 0 if everything went fine, NON 0 if an error took place + */ +int cmdline_parser_ext (int argc, char **argv, + struct gengetopt_args_info *args_info, + struct cmdline_parser_params *params); + +/** + * Save the contents of the option struct into an already open FILE stream. + * @param outfile the stream where to dump options + * @param args_info the option struct to dump + * @return 0 if everything went fine, NON 0 if an error took place + */ +int cmdline_parser_dump(FILE *outfile, + struct gengetopt_args_info *args_info); + +/** + * Save the contents of the option struct into a (text) file. + * This file can be read by the config file parser (if generated by gengetopt) + * @param filename the file where to save + * @param args_info the option struct to save + * @return 0 if everything went fine, NON 0 if an error took place + */ +int cmdline_parser_file_save(const char *filename, + struct gengetopt_args_info *args_info); + +/** + * Print the help + */ +void cmdline_parser_print_help(void); +/** + * Print the version + */ +void cmdline_parser_print_version(void); + +/** + * Initializes all the fields a cmdline_parser_params structure + * to their default values + * @param params the structure to initialize + */ +void cmdline_parser_params_init(struct cmdline_parser_params *params); + +/** + * Allocates dynamically a cmdline_parser_params structure and initializes + * all its fields to their default values + * @return the created and initialized cmdline_parser_params structure + */ +struct cmdline_parser_params *cmdline_parser_params_create(void); + +/** + * Initializes the passed gengetopt_args_info structure's fields + * (also set default values for options that have a default) + * @param args_info the structure to initialize + */ +void cmdline_parser_init (struct gengetopt_args_info *args_info); +/** + * Deallocates the string fields of the gengetopt_args_info structure + * (but does not deallocate the structure itself) + * @param args_info the structure to deallocate + */ +void cmdline_parser_free (struct gengetopt_args_info *args_info); + +/** + * The string parser (interprets the passed string as a command line) + * @param cmdline the command line stirng + * @param args_info the structure where option information will be stored + * @param prog_name the name of the program that will be used to print + * possible errors + * @return 0 if everything went fine, NON 0 if an error took place + */ +int cmdline_parser_string (const char *cmdline, struct gengetopt_args_info *args_info, + const char *prog_name); +/** + * The string parser (version with additional parameters - deprecated) + * @param cmdline the command line stirng + * @param args_info the structure where option information will be stored + * @param prog_name the name of the program that will be used to print + * possible errors + * @param override whether to override possibly already present options + * @param initialize whether to initialize the option structure my_args_info + * @param check_required whether to check that all required options were provided + * @return 0 if everything went fine, NON 0 if an error took place + * @deprecated use cmdline_parser_string_ext() instead + */ +int cmdline_parser_string2 (const char *cmdline, struct gengetopt_args_info *args_info, + const char *prog_name, + int override, int initialize, int check_required); +/** + * The string parser (version with additional parameters) + * @param cmdline the command line stirng + * @param args_info the structure where option information will be stored + * @param prog_name the name of the program that will be used to print + * possible errors + * @param params additional parameters for the parser + * @return 0 if everything went fine, NON 0 if an error took place + */ +int cmdline_parser_string_ext (const char *cmdline, struct gengetopt_args_info *args_info, + const char *prog_name, + struct cmdline_parser_params *params); + +/** + * Checks that all the required options were specified + * @param args_info the structure to check + * @param prog_name the name of the program that will be used to print + * possible errors + * @return + */ +int cmdline_parser_required (struct gengetopt_args_info *args_info, + const char *prog_name); + + +#ifdef __cplusplus +} +#endif /* __cplusplus */ +#endif /* CMDLINE_H */ diff --git a/src/verifier/include/verifier.h b/src/verifier/include/verifier.h new file mode 100644 index 00000000..87a76d3d --- /dev/null +++ b/src/verifier/include/verifier.h @@ -0,0 +1,86 @@ +#ifndef _VERIFIER_H_ +#define _VERIFIER_H_ +#include "Model.h" +#include "util.h" +#include +#include +#include +#include +#include + +class Verifier { + public: + Verifier(string htnFile, string planFile) { + this->readHTNFile(htnFile); + vector planStr = this->readPlanFile(planFile); + this->plan = this->parsePlan(planStr); + this->result = false; + } + virtual bool getResult() {return this->result;} + + protected: + Model *htn; + vector plan; + bool result; + + private: + void readHTNFile(string htnFile) { + cout << "read model from" << htnFile << "\n"; + std::ifstream *fileInput = new std::ifstream(htnFile); + if(!fileInput->good()) { + std::cerr << "Unable to open input file " << htnFile << ": " << strerror (errno) << std::endl; + exit(-1); + } + std::istream * inputStream; + inputStream = fileInput; + + bool useTaskHash = true; + /* Read model */ + // todo: the correct value of maintainTaskRechability depends on the heuristic + eMaintainTaskReachability reachability = mtrALL; + bool trackContainedTasks = useTaskHash; + this->htn = new Model(trackContainedTasks, reachability, true, true); + this->htn->filename = htnFile; + this->htn->read(inputStream); + cout << "reading htn file completed" << endl; + } + + vector parsePlan(vector planStr) { + cout << "Converting plan" << endl; + vector planNum; + unordered_map taskToIndex; + for (int i = 0; i < this->htn->numTasks; i++) { + string taskName = this->htn->taskNames[i]; + std::transform(taskName.begin(), taskName.end(), taskName.begin(), ::tolower); + taskToIndex.insert({taskName, i}); + } + for (int i = 0; i < planStr.size(); i++) { + if (!taskToIndex.count(planStr[i])) { + std::cerr << "Plan contains unreachable actions, plan is not a solution" << endl; + exit(-1); + } + planNum.push_back(taskToIndex[planStr[i]]); + } + cout << "Converting plan done" << endl; + return planNum; + } + + vector readPlanFile(string planFile) { + cout << "Read plan from " << planFile << endl; + vector plan; + ifstream fin(planFile); + if(!fin.good()) { + std::cerr << "Unable to open input file " << planFile << ": " << strerror (errno) << std::endl; + exit(-1); + } + string action; + while(std::getline(fin, action, ';')) { + action.erase(std::remove(action.begin(), action.end(), '\n'), action.end()); + std::transform(action.begin(), action.end(), action.begin(), ::tolower); + plan.push_back(action); + } + cout << "Read plan file complete" << endl; + return plan; + } +}; +#endif \ No newline at end of file diff --git a/src/verifier/options.ggo b/src/verifier/options.ggo new file mode 100644 index 00000000..3d98bf06 --- /dev/null +++ b/src/verifier/options.ggo @@ -0,0 +1,12 @@ +package "planVerifier" +version "0.1" +purpose "Plan Verification" +usage "./runVerifier [options]" +description "" +versiontext "" + +args "--string-parser -u" + +option "htn" h "the path to the input HTN problem file" string required +option "plan" p "the path to the input plan file" string required +option "optimizeDepth" o "calculating optimal depth" flag off diff --git a/src/verifier/sat_verifier/include/constraints.h b/src/verifier/sat_verifier/include/constraints.h new file mode 100644 index 00000000..57983b15 --- /dev/null +++ b/src/verifier/sat_verifier/include/constraints.h @@ -0,0 +1,52 @@ +// +// Created by u6162630 on 4/3/23. +// + +#ifndef _CONSTRAINTS_H_ +#define _CONSTRAINTS_H_ +#include "variables.h" +#include "sog.h" +#include "execution.h" +#include "sat_encoder.h" + +class ConstraintsOnMapping { +public: + ConstraintsOnMapping( + void *solver, + sat_capsule &capsule, + vector &plan, + PlanToSOGVars *mapping, + SOG *sog); +}; + +class ConstraintsOnStates { +public: + ConstraintsOnStates( + void *solver, + Model *htn, + StateVariables *vars, + PlanExecution *execution); +}; + +class ConstraintsOnSequence { +public: + ConstraintsOnSequence( + void *solver, + Model *htn, + int length, + SOG *sog, + StateVariables *stateVars, + PlanToSOGVars *mapping) { + for (int pos = 0; pos < length; pos++) + for (int a = 0; a < htn->numActions; a++) { + int var = mapping->getSequenceVar(pos, a); + if (var == -1) continue; + for (int i = 0; i < htn->numPrecs[a]; i++) { + int prop = htn->precLists[a][i]; + int propVar = stateVars->get(pos, prop); + implies(solver, var, propVar); + } + } + } +}; +#endif diff --git a/src/verifier/sat_verifier/include/depth.h b/src/verifier/sat_verifier/include/depth.h new file mode 100644 index 00000000..b8028411 --- /dev/null +++ b/src/verifier/sat_verifier/include/depth.h @@ -0,0 +1,25 @@ +// +// Created by lst19 on 4/16/2023. +// + +#ifndef PANDAPIENGINE_DEPTH_H +#define PANDAPIENGINE_DEPTH_H +#include "Model.h" +#include "marker.h" +#include "distribution.h" +#include "fstream" +#include +class Depth { +public: + Depth(Model *htn, int length); + int get(int task, int length) {return this->depth[task][length];} + int get() {return this->depth[this->htn->initialTask][this->maxLength];} +private: + Model *htn; + int maxLength; + vector distributions; + vector> depth; + void depthPerSCC(int length, int scc); + void update(int length, int scc, bool allowEmptiness); +}; +#endif //PANDAPIENGINE_DEPTH_H diff --git a/src/verifier/sat_verifier/include/marker.h b/src/verifier/sat_verifier/include/marker.h new file mode 100644 index 00000000..1e33d649 --- /dev/null +++ b/src/verifier/sat_verifier/include/marker.h @@ -0,0 +1,26 @@ +// +// Created by lst19 on 4/16/2023. +// + +#ifndef PANDAPIENGINE_MARKER_H +#define PANDAPIENGINE_MARKER_H +#include "Model.h" + +class TaskMarker{ +public: + TaskMarker(Model *htn) { + this->htn = htn; + this->nullable.assign(htn->numTasks, false); + this->visited.assign(htn->numTasks, false); + for (int task = 0; task < htn->numTasks; task++) + this->dfs(task); + } + bool isNullable(int task) {return this->nullable[task];} + +private: + Model *htn; + vector nullable; + vector visited; + void dfs(int task); +}; +#endif //PANDAPIENGINE_MARKER_H diff --git a/src/verifier/sat_verifier/include/sat_verifier.h b/src/verifier/sat_verifier/include/sat_verifier.h new file mode 100644 index 00000000..e86fd90d --- /dev/null +++ b/src/verifier/sat_verifier/include/sat_verifier.h @@ -0,0 +1,81 @@ +#include "Model.h" +#include "sog.h" +#include "pdt.h" +#include "ipasir.h" +#include "verifier.h" +#include "depth.h" +#include "execution.h" +#include "variables.h" +#include "constraints.h" +#include "sat_encoder.h" + +class SATVerifier : public Verifier { + public: + SATVerifier( + string htnFile, + string planFile, + bool optimizeDepth=false) : Verifier(htnFile, planFile) { + this->execution = new PlanExecution(this->htn, this->plan); + this->htn->computeTransitiveClosureOfMethodOrderings(); + this->htn->buildOrderingDatastructures(); + this->htn->isTotallyOrdered = false; + if (!this->execution->isExecutable()) { + this->result = false; + return; + } + PDT *pdt = new PDT(this->htn); + int maxDepth = 2 * (this->plan.size()) * (this->htn->numTasks - this->htn->numActions); + if (optimizeDepth) { + string prefix = "[Computing optimal depth]"; + Depth *depth = new Depth( + this->htn, + this->plan.size()); + int optimalDepth = depth->get(); +#ifndef NDEBUG + if (optimalDepth > maxDepth) + cout << prefix << " Higher optimal depth!" << endl; +#endif + maxDepth = min(maxDepth, optimalDepth); + cout << prefix << " Max depth: " << maxDepth << endl; + } + for (int depth = 1; depth <= maxDepth; depth++) { + this->solver = ipasir_init(); + int state = 20; + if (this->generateSATFormula(depth, pdt)) { + string prefix = "[Solving the SAT formula] "; + std::clock_t before = std::clock(); + state = ipasir_solve(this->solver); + std::clock_t after = std::clock(); + double elapsed = 1000.0 * (after - before) / CLOCKS_PER_SEC; + if (state == 10) { + cout << prefix << "Solved!" << endl; + this->result = true; + cout << prefix << "Time: " << to_string(elapsed) << endl; +#ifndef NDEBUG + this->print(solver, pdt); +#endif + ipasir_release(this->solver); + return; + } else {cout << prefix << "Unsolvable" << endl;} + cout << prefix << "Time: " << to_string(elapsed) << endl; + } + ipasir_release(this->solver); + } + } + + private: + sat_capsule capsule; + PlanExecution *execution; + void *solver; + +#ifndef NDEBUG + PlanToSOGVars *mapping; + SOG *sog; +#endif + + bool generateSATFormula(int depth, PDT *pdt); + +#ifndef NDEBUG + void print(void *solver, PDT *pdt); +#endif +}; \ No newline at end of file diff --git a/src/verifier/sat_verifier/include/variables.h b/src/verifier/sat_verifier/include/variables.h new file mode 100644 index 00000000..2e014914 --- /dev/null +++ b/src/verifier/sat_verifier/include/variables.h @@ -0,0 +1,66 @@ +#ifndef _VARIABLES_H_ +#define _VARIABLES_H_ +#include "Model.h" +#include "execution.h" +#include "sat_encoder.h" +#include "sog.h" +#include "pdt.h" + +class StateVariables { +public: + StateVariables( + vector &plan, + Model *htn, + sat_capsule &capsule) { + for (int pos = 0; pos < plan.size(); pos++) { + vector varsPerPos; + int total = htn->numStateBits; + for (int prop = 0; prop < total; prop++) { + int v = capsule.new_variable(); + string propName = htn->factStrs[prop]; + string varName = propName + "@" + to_string(pos); + DEBUG(capsule.registerVariable(v, varName)); + varsPerPos.push_back(v); + } + this->vars.push_back(varsPerPos); + } + } + int get(int pos, int prop) {return this->vars[pos][prop];} + vector::iterator begin(int pos) {return this->vars[pos].begin();} + vector::iterator end(int pos) {return this->vars[pos].end();} +private: + vector> vars; +}; + +class PlanToSOGVars { +public: + PlanToSOGVars( + vector &plan, + SOG *sog, + Model *htn, + sat_capsule &capsule); + int getMatchedVar(int pos) {return this->matched[pos];} + int getPosToVertexVar(int pos, int v) {return this->posToVertex[pos][v];} + int getVertexToPosVar(int v, int pos) {return this->vertexToPos[v][pos];} + int getForbiddenVar(int pos, int v) {return this->forbidden[pos][v];} + int getTaskVar(int pos, int v) {return this->tasks[pos][v];} + int getActivatedVar(int v) {return this->activated[v];} + int getSequenceVar(int pos, int prim) {return this->sequence[pos][prim];} + bool vertexHasArtiPrim(int v) {return this->hasArtiPrim[v];} + vector::iterator abegin(int v) {return this->artificialPrims[v].begin();} + vector::iterator aend(int v) {return this->artificialPrims[v].end();} + int getArtificialVar(int v, int action) {return this->artificial[v][action];} + +private: + vector matched; + vector> posToVertex; + vector> vertexToPos; + vector> forbidden; + vector> tasks; + vector activated; + vector> artificial; + vector> artificialPrims; + vector> sequence; + vector hasArtiPrim; +}; +#endif \ No newline at end of file diff --git a/src/verifier/sat_verifier/src/constraints.cpp b/src/verifier/sat_verifier/src/constraints.cpp new file mode 100644 index 00000000..ef555f0e --- /dev/null +++ b/src/verifier/sat_verifier/src/constraints.cpp @@ -0,0 +1,129 @@ +// +// Created by u6162630 on 4/3/23. +// + +#include "constraints.h" +ConstraintsOnStates::ConstraintsOnStates( + void *solver, + Model *htn, + StateVariables *vars, + PlanExecution *execution) { + int length = execution->getStateSeqLen(); + int numProps = htn->numStateBits; + for (int pos = 0; pos < length - 1; pos++) { + for (int prop = 0; prop < numProps; prop++) { + int var = vars->get(pos, prop); + if (execution->isPropTrue(pos, prop)) { + assertYes(solver, var); + } else {assertNot(solver, var);} + } + } +} + +ConstraintsOnMapping::ConstraintsOnMapping( + void *solver, + sat_capsule &capsule, + vector &plan, + PlanToSOGVars *mapping, + SOG *sog) { + vector> mappingPerVertex(sog->numberOfVertices); + for (int pos = 0; pos < plan.size(); pos++) { + // get the variable indicating whether + // the plan step is matched to a vertex + int matchedVar = mapping->getMatchedVar(pos); + // every plan step must match to some vertex + assertYes(solver, matchedVar); + vector possibleMappings; + for (int v = 0; v < sog->numberOfVertices; v++){ + // get the variable representing the mapping + // from a plan step to a vertex + int posToVertex = mapping->getPosToVertexVar(pos, v); + int taskVar = mapping->getTaskVar(pos, v); + if (taskVar == -1) { + assertNot(solver, posToVertex); + } else { + implies(solver, posToVertex, taskVar); + possibleMappings.push_back(posToVertex); + } + // get the variable representing the mapping + // from the vertex to the plan step + int vertexToPos = mapping->getVertexToPosVar(v, pos); + if (!mapping->vertexHasArtiPrim(v)) { + // if the vertex does not have any artificial + // action, then the mapping from the vertex + // to the position cannot be activated + assertNot(solver, vertexToPos); + } else { + vector vars; + vector::iterator iter; + // iterate through all artificial actions in the vertex + for (iter = mapping->abegin(v); iter < mapping->aend(v); iter++) { + int var = mapping->getArtificialVar(v, *iter); + assert(var != -1); + vars.push_back(var); + int varAtSeq = mapping->getSequenceVar(pos, *iter); + // if the vertex is mapped to the position and the artificial + // action is activated, then the respective action in the + // position should also be activated + impliesAnd(solver, vertexToPos, var, varAtSeq); + } + // if the mapping from the vertex to the position + // is activated, then some artificial action in the + // vertex should also be activated + impliesOr(solver, vertexToPos, vars); + } + mappingPerVertex[v].push_back(posToVertex); + mappingPerVertex[v].push_back(vertexToPos); + // get the variable representing that the mapping + // between the position and the vertex is forbidden + int forbiddenVar = mapping->getForbiddenVar(pos, v); + // if the mapping is forbidden, then neither the mapping + // from the position to the vertex nor the mapping from + // the vertex to the position is allowed + impliesNot(solver, forbiddenVar, posToVertex); + impliesNot(solver, forbiddenVar, vertexToPos); + // if the mapping between the position and the vertex + // exists, then all the successors of the vertex are + // forbidden to be mapped to the previous position + for (const int successor : sog->adj[v]) { + int forbidNext = mapping->getForbiddenVar( + pos, successor); + implies(solver, forbiddenVar, forbidNext); + if (pos == 0) break; + int forbidPrevNext = mapping->getForbiddenVar( + pos - 1, successor); + implies(solver, + posToVertex, forbidPrevNext); + implies(solver, + vertexToPos, forbidPrevNext); + } + if (pos == 0) continue; + int forbiddenPrev = mapping->getForbiddenVar( + pos - 1, v); + implies(solver, forbiddenVar, forbiddenPrev); + } + // every plan step can be mapped to at most one + // vertex that has the respective action + atMostOne(solver, capsule, possibleMappings); + // if the plan step is matched, then it must be mapped + // to some vertex that has the respective action + impliesOr(solver, matchedVar, possibleMappings); + } + for (int v = 0; v < sog->numberOfVertices; v++) { + atMostOne(solver, capsule, mappingPerVertex[v]); + int activatedVar = mapping->getActivatedVar(v); + // if the vertex is activated, it must be mapped + // to some plan step + impliesOr(solver, activatedVar, mappingPerVertex[v]); + vector primVars; + PDT *pdt = sog->leafOfNode[v]; + for (int i = 0; i < pdt->possiblePrimitives.size(); i++) { + int primVar = pdt->primitiveVariable[i]; + primVars.push_back(primVar); + } + // if the vertex is not activated, then all actions + // in this vertex cannot be activated + // impliesOr(solver, activatedVar, primVars); + notImpliesAllNot(solver, activatedVar, primVars); + } +} \ No newline at end of file diff --git a/src/verifier/sat_verifier/src/depth.cpp b/src/verifier/sat_verifier/src/depth.cpp new file mode 100644 index 00000000..3591e713 --- /dev/null +++ b/src/verifier/sat_verifier/src/depth.cpp @@ -0,0 +1,68 @@ +// +// Created by lst19 on 4/16/2023. +// +#include +#include "depth.h" +#include "util.h" + +Depth::Depth(Model *htn, int length) { + this->maxLength = length; + this->htn = htn; + this->htn->calcSCCs(); + this->htn->calcSCCGraph(); + this->htn->analyseSCCcyclicity(); + this->depth.resize(this->htn->numTasks); + for (int t = 0; t < this->htn->numTasks; t++) + this->depth[t].assign(length + 1, -1); + this->distributions.resize(this->htn->numMethods); + for (int m = 0; m < this->htn->numMethods; m++) + this->distributions[m] = new Distributions( + m, length, this->htn); + for (int i = 0; i < this->htn->numSCCs; i++) { + int scc = htn->sccTopOrder[i]; + this->depthPerSCC( + length, scc); + } +} + +void Depth::depthPerSCC( + int length, + int scc) { + int size = htn->sccSize[scc]; + for (int i = 1; i <= length; i++) { + this->update(length, scc, false); + for (int j = 1; j <= size - 1; j++) + this->update(length, scc, true); + } +} + +void Depth::update( + int length, + int scc, + bool allowEmptiness) { + for (int l = 0; l <= length; l++) { + int size = this->htn->sccSize[scc]; + for (int tInd = 0; tInd < size; tInd++) { + int task = this->htn->sccToTasks[scc][tInd]; + if (this->htn->isPrimitive[task]) { + assert(size == 1); + string name = this->htn->taskNames[task]; + if (Util::isPrecondition(name)) + this->depth[task][0] = 0; + else + this->depth[task][1] = 0; + continue; + } + int numMethods = this->htn->numMethodsForTask[task]; + for (int mInd = 0; mInd < numMethods; mInd++) { + int m = this->htn->taskToMethods[task][mInd]; + this->distributions[m]->update( + l, this->depth, allowEmptiness); + if (this->distributions[m]->isDistributable(l)) + this->depth[task][l] = max( + this->depth[task][l], + 1 + this->distributions[m]->maxDepth(l)); + } + } + } +} \ No newline at end of file diff --git a/src/verifier/sat_verifier/src/marker.cpp b/src/verifier/sat_verifier/src/marker.cpp new file mode 100644 index 00000000..5145a405 --- /dev/null +++ b/src/verifier/sat_verifier/src/marker.cpp @@ -0,0 +1,35 @@ +// +// Created by lst19 on 4/16/2023. +// +#include "marker.h" +#include "util.h" + +void TaskMarker::dfs(int task) { + if (this->visited[task]) + return; + this->visited[task] = true; + if (this->htn->isPrimitive[task]) { + string taskName = this->htn->taskNames[task]; + if (Util::isPrecondition(taskName)) + this->nullable[task]; + } else { + int numMethods = this->htn->numMethodsForTask[task]; + for (int mInd = 0; mInd < numMethods; mInd++) { + int method = this->htn->taskToMethods[task][mInd]; + int numSubTasks = this->htn->numSubTasks[method]; + bool nullableTask = true; + for (int tInd = 0; tInd < numSubTasks; tInd++) { + int subTask = this->htn->subTasks[method][tInd]; + this->dfs(subTask); + if (!this->nullable[subTask]) { + nullableTask = false; + break; + } + } + if (nullableTask) { + this->nullable[task] = true; + break; + } + } + } +} diff --git a/src/verifier/sat_verifier/src/sat_verifier.cpp b/src/verifier/sat_verifier/src/sat_verifier.cpp new file mode 100644 index 00000000..31886372 --- /dev/null +++ b/src/verifier/sat_verifier/src/sat_verifier.cpp @@ -0,0 +1,179 @@ +#include "sat_verifier.h" +#include "state_formula.h" + +bool SATVerifier::generateSATFormula(int depth, PDT *pdt) { + string prefix; + std::clock_t before, after; + double elapsed; + long numVariables, numVarsBefore, numVarsAfter; + long numClauses, numClausesBefore, numClausesAfter; + + prefix = "[Generating the PDT] "; + cout << prefix << "Depth: " << to_string(depth) << endl; + before = std::clock(); + pdt->expandPDTUpToLevel(depth, this->htn, false); + after = std::clock(); + elapsed = 1000.0 * (after - before) / CLOCKS_PER_SEC; + cout << prefix << "Done! Time: " << to_string(elapsed) << endl; + pdt->resetPruning(this->htn); + + prefix = "[Extracting the SOG] "; + before = std::clock(); + vector leafs; + pdt->getLeafs(leafs); + SOG *sog = pdt->getLeafSOG(); + after = std::clock(); + elapsed = 1000.0 * (after - before) / CLOCKS_PER_SEC; +#ifndef NDEBUG + this->sog = sog; +#endif + int numVertices = sog->numberOfVertices; + cout << prefix << "Num vertices: " << to_string(numVertices) << endl; + cout << prefix << "Done! Time: " << to_string(elapsed) << endl; + if (numVertices < this->plan.size()) return false; + + prefix = "[Generating variables for the PDT] "; + numVarsBefore = capsule.number_of_variables; + before = std::clock(); + pdt->assignVariableIDs(this->capsule, this->htn); + after = std::clock(); + numVarsAfter = capsule.number_of_variables; + numVariables = numVarsAfter - numVarsBefore; + elapsed = 1000.0 * (after - before) / CLOCKS_PER_SEC; + cout << prefix << "Num of variables: " << to_string(numVariables) << endl; + cout << prefix << "Done! Time: " << to_string(elapsed) << endl; + + prefix = "[Generating clauses for decomposition] "; + numClausesBefore = get_number_of_clauses(); + before = std::clock(); + assertYes(solver,pdt->abstractVariable[0]); + pdt->addDecompositionClauses(this->solver, this->capsule, this->htn); + no_abstract_in_leaf(this->solver, leafs, this->htn); + after = std::clock(); + elapsed = 1000.0 * (after - before) / CLOCKS_PER_SEC; + numClausesAfter = get_number_of_clauses(); + numClauses = numClausesAfter - numClausesBefore; + cout << prefix << "Num clauses: " << to_string(numClauses) << endl; + cout << prefix << "Done! Time: " << to_string(elapsed) << endl; + + prefix = "[Generating state variables] "; + numVarsBefore = this->capsule.number_of_variables; + before = std::clock(); + StateVariables *stateVars = new StateVariables(this->plan, + this->htn, + this->capsule); + after = std::clock(); + numVarsAfter = this->capsule.number_of_variables; + numVariables = numVarsAfter - numVarsBefore; + elapsed = 1000.0 * (after - before) / CLOCKS_PER_SEC; + cout << prefix << "Num variables: " << to_string(numVariables) << endl; + cout << prefix << "Done! Time: " << to_string(elapsed) << endl; + + prefix = "[Generating mapping variables] "; + numVarsBefore = this->capsule.number_of_variables; + before = std::clock(); + PlanToSOGVars *mapping = new PlanToSOGVars(this->plan, + sog, + this->htn, + this->capsule); + after = std::clock(); +#ifndef NDEBUG + this->mapping = mapping; +#endif + numVarsAfter = this->capsule.number_of_variables; + numVariables = numVarsAfter - numVarsBefore; + elapsed = 1000.0 * (after - before) / CLOCKS_PER_SEC; + cout << prefix << "Num variables: " << to_string(numVariables) << endl; + cout << prefix << "Done! Time: " << to_string(elapsed) << endl; + + prefix = "[Generating constraints on states] "; + numClausesBefore = get_number_of_clauses(); + before = std::clock(); + ConstraintsOnStates(this->solver, + this->htn, + stateVars, + this->execution); + after = std::clock(); + elapsed = 1000.0 * (after - before) / CLOCKS_PER_SEC; + numClausesAfter = get_number_of_clauses(); + numClauses = numClausesAfter - numClausesBefore; + cout << prefix << "Num clauses: " << to_string(numClauses) << endl; + cout << prefix << "Done! Time: " << to_string(elapsed) << endl; + + prefix = "[Generating constraints on mapping] "; + numClausesBefore = get_number_of_clauses(); + before = std::clock(); + ConstraintsOnMapping(this->solver, + this->capsule, + this->plan, + mapping, + sog); + after = std::clock(); + elapsed = 1000.0 * (after - before) / CLOCKS_PER_SEC; + numClausesAfter = get_number_of_clauses(); + numClauses = numClausesAfter - numClausesBefore; + cout << prefix << "Num clauses: " << to_string(numClauses) << endl; + cout << prefix << "Done! Time: " << to_string(elapsed) << endl; + + prefix = "[Generating constraints on plan execution] "; + numClausesBefore = get_number_of_clauses(); + before = std::clock(); + ConstraintsOnSequence(this->solver, + this->htn, + this->plan.size(), + sog, + stateVars, + mapping); + after = std::clock(); + elapsed = 1000.0 * (after - before) / CLOCKS_PER_SEC; + numClausesAfter = get_number_of_clauses(); + numClauses = numClausesAfter - numClausesBefore; + cout << prefix << "Num clauses: " << to_string(numClauses) << endl; + cout << prefix << "Done! Time: " << to_string(elapsed) << endl; + return true; +} + +#ifndef NDEBUG +void SATVerifier::print(void *solver, PDT *pdt) { + int currentID = 0; + vector leafs; + pdt->getLeafs(leafs); + pdt->assignOutputNumbers(solver, currentID, this->htn); + cout << "- Mappings between the plan and the leafs" << endl; + for (int pos = 0; pos < this->plan.size(); pos++) { + for (int v = 0; v < this->sog->numberOfVertices; v++) { + PDT *leaf = sog->leafOfNode[v]; + int posToVertex = this->mapping->getPosToVertexVar(pos, v); + int prim = -1; + if (ipasir_val(solver, posToVertex) > 0) { + for (int i = 0; i < leaf->possiblePrimitives.size(); i++) { + prim = leaf->possiblePrimitives[i]; + if (prim == this->plan[pos]) { + int var = leaf->primitiveVariable[i]; + assert(ipasir_val(solver, var) > 0); + break; + } + } + assert(prim == this->plan[pos]); + int outID = leaf->outputID; + string name = this->htn->taskNames[prim]; + cout << pos << "->" << v << "|" << outID << " " << name << endl; + } + int vertexToPos = this->mapping->getVertexToPosVar(v, pos); + if (ipasir_val(solver, vertexToPos) > 0) { + for (int i = 0; i < leaf->possiblePrimitives.size(); i++) { + prim = leaf->possiblePrimitives[i]; + int var = leaf->primitiveVariable[i]; + if (ipasir_val(solver, var) > 0) { + int outID = leaf->outputID; + string name = this->htn->taskNames[prim]; + cout << pos << "<-" << v << "|" << outID << " " << name << endl; + } + } + } + } + } + cout << "- Decomposition hierarchy" << endl; + pdt->printDecomposition(this->htn); +} +#endif \ No newline at end of file diff --git a/src/verifier/sat_verifier/src/variables.cpp b/src/verifier/sat_verifier/src/variables.cpp new file mode 100644 index 00000000..825f2a19 --- /dev/null +++ b/src/verifier/sat_verifier/src/variables.cpp @@ -0,0 +1,86 @@ +#include "variables.h" +#include "util.h" + +PlanToSOGVars::PlanToSOGVars( + vector &plan, + SOG *sog, + Model *htn, + sat_capsule &capsule) { + int var; + string name; + this->artificial.resize(sog->numberOfVertices); + this->artificialPrims.resize(sog->numberOfVertices); + this->hasArtiPrim.assign(sog->numberOfVertices, false); + for (int v = 0; v < sog->numberOfVertices; v++) { + this->artificial[v].assign(htn->numActions, -1); + PDT *pdt = sog->leafOfNode[v]; + for (int i = 0; i < pdt->possiblePrimitives.size(); i++) { + int action = pdt->possiblePrimitives[i]; + string actionName = htn->taskNames[action]; + if (Util::isPrecondition(actionName)) { + var = pdt->primitiveVariable[i]; + this->artificial[v][action] = var; + this->artificialPrims[v].push_back(action); + this->hasArtiPrim[v] = true; + } + } + var = capsule.new_variable(); + name = "activated[" + to_string(v) + "]"; + DEBUG(capsule.registerVariable(var, name)); + this->activated.push_back(var); + } + assert(this->activated.size() == sog->numberOfVertices); + this->vertexToPos.resize(sog->numberOfVertices); + this->sequence.resize(plan.size()); + for (int pos = 0; pos < plan.size(); pos++) { + int p = plan[pos]; + vector mappingPerPos; + mappingPerPos.assign(sog->numberOfVertices, -1); + vector forbiddenPerPos; + forbiddenPerPos.assign(sog->numberOfVertices, -1); + vector taskPerPos; + taskPerPos.assign(sog->numberOfVertices, -1); + this->sequence[pos].assign(htn->numActions, -1); + + var = capsule.new_variable(); + name = "matched[" + to_string(pos) + "]"; + DEBUG(capsule.registerVariable(var, name)); + this->matched.push_back(var); + + for (int v = 0; v < sog->numberOfVertices; v++) { + for (const int prim : this->artificialPrims[v]) { + if (this->sequence[pos][v] != -1) continue; + var = capsule.new_variable(); + name = htn->taskNames[prim] + "@" + to_string(pos); + DEBUG(capsule.registerVariable(var, name)); + this->sequence[pos][prim] = var; + } + PDT *pdt = sog->leafOfNode[v]; + for (size_t t = 0; t < pdt->possiblePrimitives.size(); t++) { + int action = pdt->possiblePrimitives[t]; + string actionName = htn->taskNames[action]; + if (action == p) { + taskPerPos[v] = pdt->primitiveVariable[t]; + break; + } + } + var = capsule.new_variable(); + name = "vertex_pos[" + to_string(v) + ";" + to_string(pos) + "]"; + DEBUG(capsule.registerVariable(var, name)); + this->vertexToPos[v].push_back(var); + + var = capsule.new_variable(); + name = "pos_vertex[" + to_string(pos) + ";" + to_string(v) + "]"; + DEBUG(capsule.registerVariable(var, name)); + mappingPerPos[v] = var; + + var = capsule.new_variable(); + name = "forbidden[" + to_string(pos) + ";" + to_string(v) + "]"; + DEBUG(capsule.registerVariable(var, name)); + forbiddenPerPos[v] = var; + } + this->posToVertex.push_back(mappingPerPos); + this->forbidden.push_back(forbiddenPerPos); + this->tasks.push_back(taskPerPos); + } +} \ No newline at end of file diff --git a/src/verifier/src/run_verifier.cpp b/src/verifier/src/run_verifier.cpp new file mode 100644 index 00000000..310ba082 --- /dev/null +++ b/src/verifier/src/run_verifier.cpp @@ -0,0 +1,30 @@ +#include +#include +#include "cmdline.h" +#include "verifier.h" +#include "sat_verifier.h" + +int main(int argc, char *argv[]) { + gengetopt_args_info args_info; + if (cmdline_parser(argc, argv, &args_info) != 0) return 1; + + string htnFile = args_info.htn_arg; + string planFile = args_info.plan_arg; + std::clock_t beforeVerify = std::clock(); + bool optimizeDepth = args_info.optimizeDepth_given; + Verifier *verifier = new SATVerifier(htnFile, planFile, optimizeDepth); + std::clock_t afterVerify = std::clock(); + double prepTime = 1000.0 * (afterVerify - beforeVerify) / CLOCKS_PER_SEC; + cout << "Information about the verification" << endl; + cout << "- Time for verifying the plan: " << prepTime << endl; + bool result = verifier->getResult(); + + if (result) { + cout << "The given plan is a solution" << endl; + } + else { + cout << "The given plan is not a solution" << endl; + } + + return 0; +} \ No newline at end of file diff --git a/src/verifier/test/CMakeLists.txt b/src/verifier/test/CMakeLists.txt new file mode 100644 index 00000000..33a9ff0d --- /dev/null +++ b/src/verifier/test/CMakeLists.txt @@ -0,0 +1,15 @@ +add_library(catch2 INTERFACE) + +target_include_directories(catch2 INTERFACE ${CMAKE_CURRENT_SOURCE_DIR}/catch2) + +add_library(test_main + OBJECT + ${CMAKE_CURRENT_SOURCE_DIR}/test_main.cpp + ${CMAKE_CURRENT_SOURCE_DIR}/catch2/catch.hpp + ) + +target_include_directories(test_main + PUBLIC + ${CMAKE_CURRENT_SOURCE_DIR}/catch2 + ) + diff --git a/src/verifier/test/catch2/catch.hpp b/src/verifier/test/catch2/catch.hpp new file mode 100644 index 00000000..9b309bdd --- /dev/null +++ b/src/verifier/test/catch2/catch.hpp @@ -0,0 +1,17976 @@ +/* + * Catch v2.13.10 + * Generated: 2022-10-16 11:01:23.452308 + * ---------------------------------------------------------- + * This file has been merged from multiple headers. Please don't edit it directly + * Copyright (c) 2022 Two Blue Cubes Ltd. All rights reserved. + * + * Distributed under the Boost Software License, Version 1.0. (See accompanying + * file LICENSE_1_0.txt or copy at http://www.boost.org/LICENSE_1_0.txt) + */ +#ifndef TWOBLUECUBES_SINGLE_INCLUDE_CATCH_HPP_INCLUDED +#define TWOBLUECUBES_SINGLE_INCLUDE_CATCH_HPP_INCLUDED +// start catch.hpp + + +#define CATCH_VERSION_MAJOR 2 +#define CATCH_VERSION_MINOR 13 +#define CATCH_VERSION_PATCH 10 + +#ifdef __clang__ +# pragma clang system_header +#elif defined __GNUC__ +# pragma GCC system_header +#endif + +// start catch_suppress_warnings.h + +#ifdef __clang__ +# ifdef __ICC // icpc defines the __clang__ macro +# pragma warning(push) +# pragma warning(disable: 161 1682) +# else // __ICC +# pragma clang diagnostic push +# pragma clang diagnostic ignored "-Wpadded" +# pragma clang diagnostic ignored "-Wswitch-enum" +# pragma clang diagnostic ignored "-Wcovered-switch-default" +# endif +#elif defined __GNUC__ + // Because REQUIREs trigger GCC's -Wparentheses, and because still + // supported version of g++ have only buggy support for _Pragmas, + // Wparentheses have to be suppressed globally. +# pragma GCC diagnostic ignored "-Wparentheses" // See #674 for details + +# pragma GCC diagnostic push +# pragma GCC diagnostic ignored "-Wunused-variable" +# pragma GCC diagnostic ignored "-Wpadded" +#endif +// end catch_suppress_warnings.h +#if defined(CATCH_CONFIG_MAIN) || defined(CATCH_CONFIG_RUNNER) +# define CATCH_IMPL +# define CATCH_CONFIG_ALL_PARTS +#endif + +// In the impl file, we want to have access to all parts of the headers +// Can also be used to sanely support PCHs +#if defined(CATCH_CONFIG_ALL_PARTS) +# define CATCH_CONFIG_EXTERNAL_INTERFACES +# if defined(CATCH_CONFIG_DISABLE_MATCHERS) +# undef CATCH_CONFIG_DISABLE_MATCHERS +# endif +# if !defined(CATCH_CONFIG_ENABLE_CHRONO_STRINGMAKER) +# define CATCH_CONFIG_ENABLE_CHRONO_STRINGMAKER +# endif +#endif + +#if !defined(CATCH_CONFIG_IMPL_ONLY) +// start catch_platform.h + +// See e.g.: +// https://opensource.apple.com/source/CarbonHeaders/CarbonHeaders-18.1/TargetConditionals.h.auto.html +#ifdef __APPLE__ +# include +# if (defined(TARGET_OS_OSX) && TARGET_OS_OSX == 1) || \ + (defined(TARGET_OS_MAC) && TARGET_OS_MAC == 1) +# define CATCH_PLATFORM_MAC +# elif (defined(TARGET_OS_IPHONE) && TARGET_OS_IPHONE == 1) +# define CATCH_PLATFORM_IPHONE +# endif + +#elif defined(linux) || defined(__linux) || defined(__linux__) +# define CATCH_PLATFORM_LINUX + +#elif defined(WIN32) || defined(__WIN32__) || defined(_WIN32) || defined(_MSC_VER) || defined(__MINGW32__) +# define CATCH_PLATFORM_WINDOWS +#endif + +// end catch_platform.h + +#ifdef CATCH_IMPL +# ifndef CLARA_CONFIG_MAIN +# define CLARA_CONFIG_MAIN_NOT_DEFINED +# define CLARA_CONFIG_MAIN +# endif +#endif + +// start catch_user_interfaces.h + +namespace Catch { + unsigned int rngSeed(); +} + +// end catch_user_interfaces.h +// start catch_tag_alias_autoregistrar.h + +// start catch_common.h + +// start catch_compiler_capabilities.h + +// Detect a number of compiler features - by compiler +// The following features are defined: +// +// CATCH_CONFIG_COUNTER : is the __COUNTER__ macro supported? +// CATCH_CONFIG_WINDOWS_SEH : is Windows SEH supported? +// CATCH_CONFIG_POSIX_SIGNALS : are POSIX signals supported? +// CATCH_CONFIG_DISABLE_EXCEPTIONS : Are exceptions enabled? +// **************** +// Note to maintainers: if new toggles are added please document them +// in configuration.md, too +// **************** + +// In general each macro has a _NO_ form +// (e.g. CATCH_CONFIG_NO_POSIX_SIGNALS) which disables the feature. +// Many features, at point of detection, define an _INTERNAL_ macro, so they +// can be combined, en-mass, with the _NO_ forms later. + +#ifdef __cplusplus + +# if (__cplusplus >= 201402L) || (defined(_MSVC_LANG) && _MSVC_LANG >= 201402L) +# define CATCH_CPP14_OR_GREATER +# endif + +# if (__cplusplus >= 201703L) || (defined(_MSVC_LANG) && _MSVC_LANG >= 201703L) +# define CATCH_CPP17_OR_GREATER +# endif + +#endif + +// Only GCC compiler should be used in this block, so other compilers trying to +// mask themselves as GCC should be ignored. +#if defined(__GNUC__) && !defined(__clang__) && !defined(__ICC) && !defined(__CUDACC__) && !defined(__LCC__) +# define CATCH_INTERNAL_START_WARNINGS_SUPPRESSION _Pragma( "GCC diagnostic push" ) +# define CATCH_INTERNAL_STOP_WARNINGS_SUPPRESSION _Pragma( "GCC diagnostic pop" ) + +# define CATCH_INTERNAL_IGNORE_BUT_WARN(...) (void)__builtin_constant_p(__VA_ARGS__) + +#endif + +#if defined(__clang__) + +# define CATCH_INTERNAL_START_WARNINGS_SUPPRESSION _Pragma( "clang diagnostic push" ) +# define CATCH_INTERNAL_STOP_WARNINGS_SUPPRESSION _Pragma( "clang diagnostic pop" ) + +// As of this writing, IBM XL's implementation of __builtin_constant_p has a bug +// which results in calls to destructors being emitted for each temporary, +// without a matching initialization. In practice, this can result in something +// like `std::string::~string` being called on an uninitialized value. +// +// For example, this code will likely segfault under IBM XL: +// ``` +// REQUIRE(std::string("12") + "34" == "1234") +// ``` +// +// Therefore, `CATCH_INTERNAL_IGNORE_BUT_WARN` is not implemented. +# if !defined(__ibmxl__) && !defined(__CUDACC__) +# define CATCH_INTERNAL_IGNORE_BUT_WARN(...) (void)__builtin_constant_p(__VA_ARGS__) /* NOLINT(cppcoreguidelines-pro-type-vararg, hicpp-vararg) */ +# endif + +# define CATCH_INTERNAL_SUPPRESS_GLOBALS_WARNINGS \ + _Pragma( "clang diagnostic ignored \"-Wexit-time-destructors\"" ) \ + _Pragma( "clang diagnostic ignored \"-Wglobal-constructors\"") + +# define CATCH_INTERNAL_SUPPRESS_PARENTHESES_WARNINGS \ + _Pragma( "clang diagnostic ignored \"-Wparentheses\"" ) + +# define CATCH_INTERNAL_SUPPRESS_UNUSED_WARNINGS \ + _Pragma( "clang diagnostic ignored \"-Wunused-variable\"" ) + +# define CATCH_INTERNAL_SUPPRESS_ZERO_VARIADIC_WARNINGS \ + _Pragma( "clang diagnostic ignored \"-Wgnu-zero-variadic-macro-arguments\"" ) + +# define CATCH_INTERNAL_SUPPRESS_UNUSED_TEMPLATE_WARNINGS \ + _Pragma( "clang diagnostic ignored \"-Wunused-template\"" ) + +#endif // __clang__ + +//////////////////////////////////////////////////////////////////////////////// +// Assume that non-Windows platforms support posix signals by default +#if !defined(CATCH_PLATFORM_WINDOWS) + #define CATCH_INTERNAL_CONFIG_POSIX_SIGNALS +#endif + +//////////////////////////////////////////////////////////////////////////////// +// We know some environments not to support full POSIX signals +#if defined(__CYGWIN__) || defined(__QNX__) || defined(__EMSCRIPTEN__) || defined(__DJGPP__) + #define CATCH_INTERNAL_CONFIG_NO_POSIX_SIGNALS +#endif + +#ifdef __OS400__ +# define CATCH_INTERNAL_CONFIG_NO_POSIX_SIGNALS +# define CATCH_CONFIG_COLOUR_NONE +#endif + +//////////////////////////////////////////////////////////////////////////////// +// Android somehow still does not support std::to_string +#if defined(__ANDROID__) +# define CATCH_INTERNAL_CONFIG_NO_CPP11_TO_STRING +# define CATCH_INTERNAL_CONFIG_ANDROID_LOGWRITE +#endif + +//////////////////////////////////////////////////////////////////////////////// +// Not all Windows environments support SEH properly +#if defined(__MINGW32__) +# define CATCH_INTERNAL_CONFIG_NO_WINDOWS_SEH +#endif + +//////////////////////////////////////////////////////////////////////////////// +// PS4 +#if defined(__ORBIS__) +# define CATCH_INTERNAL_CONFIG_NO_NEW_CAPTURE +#endif + +//////////////////////////////////////////////////////////////////////////////// +// Cygwin +#ifdef __CYGWIN__ + +// Required for some versions of Cygwin to declare gettimeofday +// see: http://stackoverflow.com/questions/36901803/gettimeofday-not-declared-in-this-scope-cygwin +# define _BSD_SOURCE +// some versions of cygwin (most) do not support std::to_string. Use the libstd check. +// https://gcc.gnu.org/onlinedocs/gcc-4.8.2/libstdc++/api/a01053_source.html line 2812-2813 +# if !((__cplusplus >= 201103L) && defined(_GLIBCXX_USE_C99) \ + && !defined(_GLIBCXX_HAVE_BROKEN_VSWPRINTF)) + +# define CATCH_INTERNAL_CONFIG_NO_CPP11_TO_STRING + +# endif +#endif // __CYGWIN__ + +//////////////////////////////////////////////////////////////////////////////// +// Visual C++ +#if defined(_MSC_VER) + +// Universal Windows platform does not support SEH +// Or console colours (or console at all...) +# if defined(WINAPI_FAMILY) && (WINAPI_FAMILY == WINAPI_FAMILY_APP) +# define CATCH_CONFIG_COLOUR_NONE +# else +# define CATCH_INTERNAL_CONFIG_WINDOWS_SEH +# endif + +# if !defined(__clang__) // Handle Clang masquerading for msvc + +// MSVC traditional preprocessor needs some workaround for __VA_ARGS__ +// _MSVC_TRADITIONAL == 0 means new conformant preprocessor +// _MSVC_TRADITIONAL == 1 means old traditional non-conformant preprocessor +# if !defined(_MSVC_TRADITIONAL) || (defined(_MSVC_TRADITIONAL) && _MSVC_TRADITIONAL) +# define CATCH_INTERNAL_CONFIG_TRADITIONAL_MSVC_PREPROCESSOR +# endif // MSVC_TRADITIONAL + +// Only do this if we're not using clang on Windows, which uses `diagnostic push` & `diagnostic pop` +# define CATCH_INTERNAL_START_WARNINGS_SUPPRESSION __pragma( warning(push) ) +# define CATCH_INTERNAL_STOP_WARNINGS_SUPPRESSION __pragma( warning(pop) ) +# endif // __clang__ + +#endif // _MSC_VER + +#if defined(_REENTRANT) || defined(_MSC_VER) +// Enable async processing, as -pthread is specified or no additional linking is required +# define CATCH_INTERNAL_CONFIG_USE_ASYNC +#endif // _MSC_VER + +//////////////////////////////////////////////////////////////////////////////// +// Check if we are compiled with -fno-exceptions or equivalent +#if defined(__EXCEPTIONS) || defined(__cpp_exceptions) || defined(_CPPUNWIND) +# define CATCH_INTERNAL_CONFIG_EXCEPTIONS_ENABLED +#endif + +//////////////////////////////////////////////////////////////////////////////// +// DJGPP +#ifdef __DJGPP__ +# define CATCH_INTERNAL_CONFIG_NO_WCHAR +#endif // __DJGPP__ + +//////////////////////////////////////////////////////////////////////////////// +// Embarcadero C++Build +#if defined(__BORLANDC__) + #define CATCH_INTERNAL_CONFIG_POLYFILL_ISNAN +#endif + +//////////////////////////////////////////////////////////////////////////////// + +// Use of __COUNTER__ is suppressed during code analysis in +// CLion/AppCode 2017.2.x and former, because __COUNTER__ is not properly +// handled by it. +// Otherwise all supported compilers support COUNTER macro, +// but user still might want to turn it off +#if ( !defined(__JETBRAINS_IDE__) || __JETBRAINS_IDE__ >= 20170300L ) + #define CATCH_INTERNAL_CONFIG_COUNTER +#endif + +//////////////////////////////////////////////////////////////////////////////// + +// RTX is a special version of Windows that is real time. +// This means that it is detected as Windows, but does not provide +// the same set of capabilities as real Windows does. +#if defined(UNDER_RTSS) || defined(RTX64_BUILD) + #define CATCH_INTERNAL_CONFIG_NO_WINDOWS_SEH + #define CATCH_INTERNAL_CONFIG_NO_ASYNC + #define CATCH_CONFIG_COLOUR_NONE +#endif + +#if !defined(_GLIBCXX_USE_C99_MATH_TR1) +#define CATCH_INTERNAL_CONFIG_GLOBAL_NEXTAFTER +#endif + +// Various stdlib support checks that require __has_include +#if defined(__has_include) + // Check if string_view is available and usable + #if __has_include() && defined(CATCH_CPP17_OR_GREATER) + # define CATCH_INTERNAL_CONFIG_CPP17_STRING_VIEW + #endif + + // Check if optional is available and usable + # if __has_include() && defined(CATCH_CPP17_OR_GREATER) + # define CATCH_INTERNAL_CONFIG_CPP17_OPTIONAL + # endif // __has_include() && defined(CATCH_CPP17_OR_GREATER) + + // Check if byte is available and usable + # if __has_include() && defined(CATCH_CPP17_OR_GREATER) + # include + # if defined(__cpp_lib_byte) && (__cpp_lib_byte > 0) + # define CATCH_INTERNAL_CONFIG_CPP17_BYTE + # endif + # endif // __has_include() && defined(CATCH_CPP17_OR_GREATER) + + // Check if variant is available and usable + # if __has_include() && defined(CATCH_CPP17_OR_GREATER) + # if defined(__clang__) && (__clang_major__ < 8) + // work around clang bug with libstdc++ https://bugs.llvm.org/show_bug.cgi?id=31852 + // fix should be in clang 8, workaround in libstdc++ 8.2 + # include + # if defined(__GLIBCXX__) && defined(_GLIBCXX_RELEASE) && (_GLIBCXX_RELEASE < 9) + # define CATCH_CONFIG_NO_CPP17_VARIANT + # else + # define CATCH_INTERNAL_CONFIG_CPP17_VARIANT + # endif // defined(__GLIBCXX__) && defined(_GLIBCXX_RELEASE) && (_GLIBCXX_RELEASE < 9) + # else + # define CATCH_INTERNAL_CONFIG_CPP17_VARIANT + # endif // defined(__clang__) && (__clang_major__ < 8) + # endif // __has_include() && defined(CATCH_CPP17_OR_GREATER) +#endif // defined(__has_include) + +#if defined(CATCH_INTERNAL_CONFIG_COUNTER) && !defined(CATCH_CONFIG_NO_COUNTER) && !defined(CATCH_CONFIG_COUNTER) +# define CATCH_CONFIG_COUNTER +#endif +#if defined(CATCH_INTERNAL_CONFIG_WINDOWS_SEH) && !defined(CATCH_CONFIG_NO_WINDOWS_SEH) && !defined(CATCH_CONFIG_WINDOWS_SEH) && !defined(CATCH_INTERNAL_CONFIG_NO_WINDOWS_SEH) +# define CATCH_CONFIG_WINDOWS_SEH +#endif +// This is set by default, because we assume that unix compilers are posix-signal-compatible by default. +#if defined(CATCH_INTERNAL_CONFIG_POSIX_SIGNALS) && !defined(CATCH_INTERNAL_CONFIG_NO_POSIX_SIGNALS) && !defined(CATCH_CONFIG_NO_POSIX_SIGNALS) && !defined(CATCH_CONFIG_POSIX_SIGNALS) +# define CATCH_CONFIG_POSIX_SIGNALS +#endif +// This is set by default, because we assume that compilers with no wchar_t support are just rare exceptions. +#if !defined(CATCH_INTERNAL_CONFIG_NO_WCHAR) && !defined(CATCH_CONFIG_NO_WCHAR) && !defined(CATCH_CONFIG_WCHAR) +# define CATCH_CONFIG_WCHAR +#endif + +#if !defined(CATCH_INTERNAL_CONFIG_NO_CPP11_TO_STRING) && !defined(CATCH_CONFIG_NO_CPP11_TO_STRING) && !defined(CATCH_CONFIG_CPP11_TO_STRING) +# define CATCH_CONFIG_CPP11_TO_STRING +#endif + +#if defined(CATCH_INTERNAL_CONFIG_CPP17_OPTIONAL) && !defined(CATCH_CONFIG_NO_CPP17_OPTIONAL) && !defined(CATCH_CONFIG_CPP17_OPTIONAL) +# define CATCH_CONFIG_CPP17_OPTIONAL +#endif + +#if defined(CATCH_INTERNAL_CONFIG_CPP17_STRING_VIEW) && !defined(CATCH_CONFIG_NO_CPP17_STRING_VIEW) && !defined(CATCH_CONFIG_CPP17_STRING_VIEW) +# define CATCH_CONFIG_CPP17_STRING_VIEW +#endif + +#if defined(CATCH_INTERNAL_CONFIG_CPP17_VARIANT) && !defined(CATCH_CONFIG_NO_CPP17_VARIANT) && !defined(CATCH_CONFIG_CPP17_VARIANT) +# define CATCH_CONFIG_CPP17_VARIANT +#endif + +#if defined(CATCH_INTERNAL_CONFIG_CPP17_BYTE) && !defined(CATCH_CONFIG_NO_CPP17_BYTE) && !defined(CATCH_CONFIG_CPP17_BYTE) +# define CATCH_CONFIG_CPP17_BYTE +#endif + +#if defined(CATCH_CONFIG_EXPERIMENTAL_REDIRECT) +# define CATCH_INTERNAL_CONFIG_NEW_CAPTURE +#endif + +#if defined(CATCH_INTERNAL_CONFIG_NEW_CAPTURE) && !defined(CATCH_INTERNAL_CONFIG_NO_NEW_CAPTURE) && !defined(CATCH_CONFIG_NO_NEW_CAPTURE) && !defined(CATCH_CONFIG_NEW_CAPTURE) +# define CATCH_CONFIG_NEW_CAPTURE +#endif + +#if !defined(CATCH_INTERNAL_CONFIG_EXCEPTIONS_ENABLED) && !defined(CATCH_CONFIG_DISABLE_EXCEPTIONS) +# define CATCH_CONFIG_DISABLE_EXCEPTIONS +#endif + +#if defined(CATCH_INTERNAL_CONFIG_POLYFILL_ISNAN) && !defined(CATCH_CONFIG_NO_POLYFILL_ISNAN) && !defined(CATCH_CONFIG_POLYFILL_ISNAN) +# define CATCH_CONFIG_POLYFILL_ISNAN +#endif + +#if defined(CATCH_INTERNAL_CONFIG_USE_ASYNC) && !defined(CATCH_INTERNAL_CONFIG_NO_ASYNC) && !defined(CATCH_CONFIG_NO_USE_ASYNC) && !defined(CATCH_CONFIG_USE_ASYNC) +# define CATCH_CONFIG_USE_ASYNC +#endif + +#if defined(CATCH_INTERNAL_CONFIG_ANDROID_LOGWRITE) && !defined(CATCH_CONFIG_NO_ANDROID_LOGWRITE) && !defined(CATCH_CONFIG_ANDROID_LOGWRITE) +# define CATCH_CONFIG_ANDROID_LOGWRITE +#endif + +#if defined(CATCH_INTERNAL_CONFIG_GLOBAL_NEXTAFTER) && !defined(CATCH_CONFIG_NO_GLOBAL_NEXTAFTER) && !defined(CATCH_CONFIG_GLOBAL_NEXTAFTER) +# define CATCH_CONFIG_GLOBAL_NEXTAFTER +#endif + +// Even if we do not think the compiler has that warning, we still have +// to provide a macro that can be used by the code. +#if !defined(CATCH_INTERNAL_START_WARNINGS_SUPPRESSION) +# define CATCH_INTERNAL_START_WARNINGS_SUPPRESSION +#endif +#if !defined(CATCH_INTERNAL_STOP_WARNINGS_SUPPRESSION) +# define CATCH_INTERNAL_STOP_WARNINGS_SUPPRESSION +#endif +#if !defined(CATCH_INTERNAL_SUPPRESS_PARENTHESES_WARNINGS) +# define CATCH_INTERNAL_SUPPRESS_PARENTHESES_WARNINGS +#endif +#if !defined(CATCH_INTERNAL_SUPPRESS_GLOBALS_WARNINGS) +# define CATCH_INTERNAL_SUPPRESS_GLOBALS_WARNINGS +#endif +#if !defined(CATCH_INTERNAL_SUPPRESS_UNUSED_WARNINGS) +# define CATCH_INTERNAL_SUPPRESS_UNUSED_WARNINGS +#endif +#if !defined(CATCH_INTERNAL_SUPPRESS_ZERO_VARIADIC_WARNINGS) +# define CATCH_INTERNAL_SUPPRESS_ZERO_VARIADIC_WARNINGS +#endif + +// The goal of this macro is to avoid evaluation of the arguments, but +// still have the compiler warn on problems inside... +#if !defined(CATCH_INTERNAL_IGNORE_BUT_WARN) +# define CATCH_INTERNAL_IGNORE_BUT_WARN(...) +#endif + +#if defined(__APPLE__) && defined(__apple_build_version__) && (__clang_major__ < 10) +# undef CATCH_INTERNAL_SUPPRESS_UNUSED_TEMPLATE_WARNINGS +#elif defined(__clang__) && (__clang_major__ < 5) +# undef CATCH_INTERNAL_SUPPRESS_UNUSED_TEMPLATE_WARNINGS +#endif + +#if !defined(CATCH_INTERNAL_SUPPRESS_UNUSED_TEMPLATE_WARNINGS) +# define CATCH_INTERNAL_SUPPRESS_UNUSED_TEMPLATE_WARNINGS +#endif + +#if defined(CATCH_CONFIG_DISABLE_EXCEPTIONS) +#define CATCH_TRY if ((true)) +#define CATCH_CATCH_ALL if ((false)) +#define CATCH_CATCH_ANON(type) if ((false)) +#else +#define CATCH_TRY try +#define CATCH_CATCH_ALL catch (...) +#define CATCH_CATCH_ANON(type) catch (type) +#endif + +#if defined(CATCH_INTERNAL_CONFIG_TRADITIONAL_MSVC_PREPROCESSOR) && !defined(CATCH_CONFIG_NO_TRADITIONAL_MSVC_PREPROCESSOR) && !defined(CATCH_CONFIG_TRADITIONAL_MSVC_PREPROCESSOR) +#define CATCH_CONFIG_TRADITIONAL_MSVC_PREPROCESSOR +#endif + +// end catch_compiler_capabilities.h +#define INTERNAL_CATCH_UNIQUE_NAME_LINE2( name, line ) name##line +#define INTERNAL_CATCH_UNIQUE_NAME_LINE( name, line ) INTERNAL_CATCH_UNIQUE_NAME_LINE2( name, line ) +#ifdef CATCH_CONFIG_COUNTER +# define INTERNAL_CATCH_UNIQUE_NAME( name ) INTERNAL_CATCH_UNIQUE_NAME_LINE( name, __COUNTER__ ) +#else +# define INTERNAL_CATCH_UNIQUE_NAME( name ) INTERNAL_CATCH_UNIQUE_NAME_LINE( name, __LINE__ ) +#endif + +#include +#include +#include + +// We need a dummy global operator<< so we can bring it into Catch namespace later +struct Catch_global_namespace_dummy {}; +std::ostream& operator<<(std::ostream&, Catch_global_namespace_dummy); + +namespace Catch { + + struct CaseSensitive { enum Choice { + Yes, + No + }; }; + + class NonCopyable { + NonCopyable( NonCopyable const& ) = delete; + NonCopyable( NonCopyable && ) = delete; + NonCopyable& operator = ( NonCopyable const& ) = delete; + NonCopyable& operator = ( NonCopyable && ) = delete; + + protected: + NonCopyable(); + virtual ~NonCopyable(); + }; + + struct SourceLineInfo { + + SourceLineInfo() = delete; + SourceLineInfo( char const* _file, std::size_t _line ) noexcept + : file( _file ), + line( _line ) + {} + + SourceLineInfo( SourceLineInfo const& other ) = default; + SourceLineInfo& operator = ( SourceLineInfo const& ) = default; + SourceLineInfo( SourceLineInfo&& ) noexcept = default; + SourceLineInfo& operator = ( SourceLineInfo&& ) noexcept = default; + + bool empty() const noexcept { return file[0] == '\0'; } + bool operator == ( SourceLineInfo const& other ) const noexcept; + bool operator < ( SourceLineInfo const& other ) const noexcept; + + char const* file; + std::size_t line; + }; + + std::ostream& operator << ( std::ostream& os, SourceLineInfo const& info ); + + // Bring in operator<< from global namespace into Catch namespace + // This is necessary because the overload of operator<< above makes + // lookup stop at namespace Catch + using ::operator<<; + + // Use this in variadic streaming macros to allow + // >> +StreamEndStop + // as well as + // >> stuff +StreamEndStop + struct StreamEndStop { + std::string operator+() const; + }; + template + T const& operator + ( T const& value, StreamEndStop ) { + return value; + } +} + +#define CATCH_INTERNAL_LINEINFO \ + ::Catch::SourceLineInfo( __FILE__, static_cast( __LINE__ ) ) + +// end catch_common.h +namespace Catch { + + struct RegistrarForTagAliases { + RegistrarForTagAliases( char const* alias, char const* tag, SourceLineInfo const& lineInfo ); + }; + +} // end namespace Catch + +#define CATCH_REGISTER_TAG_ALIAS( alias, spec ) \ + CATCH_INTERNAL_START_WARNINGS_SUPPRESSION \ + CATCH_INTERNAL_SUPPRESS_GLOBALS_WARNINGS \ + namespace{ Catch::RegistrarForTagAliases INTERNAL_CATCH_UNIQUE_NAME( AutoRegisterTagAlias )( alias, spec, CATCH_INTERNAL_LINEINFO ); } \ + CATCH_INTERNAL_STOP_WARNINGS_SUPPRESSION + +// end catch_tag_alias_autoregistrar.h +// start catch_test_registry.h + +// start catch_interfaces_testcase.h + +#include + +namespace Catch { + + class TestSpec; + + struct ITestInvoker { + virtual void invoke () const = 0; + virtual ~ITestInvoker(); + }; + + class TestCase; + struct IConfig; + + struct ITestCaseRegistry { + virtual ~ITestCaseRegistry(); + virtual std::vector const& getAllTests() const = 0; + virtual std::vector const& getAllTestsSorted( IConfig const& config ) const = 0; + }; + + bool isThrowSafe( TestCase const& testCase, IConfig const& config ); + bool matchTest( TestCase const& testCase, TestSpec const& testSpec, IConfig const& config ); + std::vector filterTests( std::vector const& testCases, TestSpec const& testSpec, IConfig const& config ); + std::vector const& getAllTestCasesSorted( IConfig const& config ); + +} + +// end catch_interfaces_testcase.h +// start catch_stringref.h + +#include +#include +#include +#include + +namespace Catch { + + /// A non-owning string class (similar to the forthcoming std::string_view) + /// Note that, because a StringRef may be a substring of another string, + /// it may not be null terminated. + class StringRef { + public: + using size_type = std::size_t; + using const_iterator = const char*; + + private: + static constexpr char const* const s_empty = ""; + + char const* m_start = s_empty; + size_type m_size = 0; + + public: // construction + constexpr StringRef() noexcept = default; + + StringRef( char const* rawChars ) noexcept; + + constexpr StringRef( char const* rawChars, size_type size ) noexcept + : m_start( rawChars ), + m_size( size ) + {} + + StringRef( std::string const& stdString ) noexcept + : m_start( stdString.c_str() ), + m_size( stdString.size() ) + {} + + explicit operator std::string() const { + return std::string(m_start, m_size); + } + + public: // operators + auto operator == ( StringRef const& other ) const noexcept -> bool; + auto operator != (StringRef const& other) const noexcept -> bool { + return !(*this == other); + } + + auto operator[] ( size_type index ) const noexcept -> char { + assert(index < m_size); + return m_start[index]; + } + + public: // named queries + constexpr auto empty() const noexcept -> bool { + return m_size == 0; + } + constexpr auto size() const noexcept -> size_type { + return m_size; + } + + // Returns the current start pointer. If the StringRef is not + // null-terminated, throws std::domain_exception + auto c_str() const -> char const*; + + public: // substrings and searches + // Returns a substring of [start, start + length). + // If start + length > size(), then the substring is [start, size()). + // If start > size(), then the substring is empty. + auto substr( size_type start, size_type length ) const noexcept -> StringRef; + + // Returns the current start pointer. May not be null-terminated. + auto data() const noexcept -> char const*; + + constexpr auto isNullTerminated() const noexcept -> bool { + return m_start[m_size] == '\0'; + } + + public: // iterators + constexpr const_iterator begin() const { return m_start; } + constexpr const_iterator end() const { return m_start + m_size; } + }; + + auto operator += ( std::string& lhs, StringRef const& sr ) -> std::string&; + auto operator << ( std::ostream& os, StringRef const& sr ) -> std::ostream&; + + constexpr auto operator "" _sr( char const* rawChars, std::size_t size ) noexcept -> StringRef { + return StringRef( rawChars, size ); + } +} // namespace Catch + +constexpr auto operator "" _catch_sr( char const* rawChars, std::size_t size ) noexcept -> Catch::StringRef { + return Catch::StringRef( rawChars, size ); +} + +// end catch_stringref.h +// start catch_preprocessor.hpp + + +#define CATCH_RECURSION_LEVEL0(...) __VA_ARGS__ +#define CATCH_RECURSION_LEVEL1(...) CATCH_RECURSION_LEVEL0(CATCH_RECURSION_LEVEL0(CATCH_RECURSION_LEVEL0(__VA_ARGS__))) +#define CATCH_RECURSION_LEVEL2(...) CATCH_RECURSION_LEVEL1(CATCH_RECURSION_LEVEL1(CATCH_RECURSION_LEVEL1(__VA_ARGS__))) +#define CATCH_RECURSION_LEVEL3(...) CATCH_RECURSION_LEVEL2(CATCH_RECURSION_LEVEL2(CATCH_RECURSION_LEVEL2(__VA_ARGS__))) +#define CATCH_RECURSION_LEVEL4(...) CATCH_RECURSION_LEVEL3(CATCH_RECURSION_LEVEL3(CATCH_RECURSION_LEVEL3(__VA_ARGS__))) +#define CATCH_RECURSION_LEVEL5(...) CATCH_RECURSION_LEVEL4(CATCH_RECURSION_LEVEL4(CATCH_RECURSION_LEVEL4(__VA_ARGS__))) + +#ifdef CATCH_CONFIG_TRADITIONAL_MSVC_PREPROCESSOR +#define INTERNAL_CATCH_EXPAND_VARGS(...) __VA_ARGS__ +// MSVC needs more evaluations +#define CATCH_RECURSION_LEVEL6(...) CATCH_RECURSION_LEVEL5(CATCH_RECURSION_LEVEL5(CATCH_RECURSION_LEVEL5(__VA_ARGS__))) +#define CATCH_RECURSE(...) CATCH_RECURSION_LEVEL6(CATCH_RECURSION_LEVEL6(__VA_ARGS__)) +#else +#define CATCH_RECURSE(...) CATCH_RECURSION_LEVEL5(__VA_ARGS__) +#endif + +#define CATCH_REC_END(...) +#define CATCH_REC_OUT + +#define CATCH_EMPTY() +#define CATCH_DEFER(id) id CATCH_EMPTY() + +#define CATCH_REC_GET_END2() 0, CATCH_REC_END +#define CATCH_REC_GET_END1(...) CATCH_REC_GET_END2 +#define CATCH_REC_GET_END(...) CATCH_REC_GET_END1 +#define CATCH_REC_NEXT0(test, next, ...) next CATCH_REC_OUT +#define CATCH_REC_NEXT1(test, next) CATCH_DEFER ( CATCH_REC_NEXT0 ) ( test, next, 0) +#define CATCH_REC_NEXT(test, next) CATCH_REC_NEXT1(CATCH_REC_GET_END test, next) + +#define CATCH_REC_LIST0(f, x, peek, ...) , f(x) CATCH_DEFER ( CATCH_REC_NEXT(peek, CATCH_REC_LIST1) ) ( f, peek, __VA_ARGS__ ) +#define CATCH_REC_LIST1(f, x, peek, ...) , f(x) CATCH_DEFER ( CATCH_REC_NEXT(peek, CATCH_REC_LIST0) ) ( f, peek, __VA_ARGS__ ) +#define CATCH_REC_LIST2(f, x, peek, ...) f(x) CATCH_DEFER ( CATCH_REC_NEXT(peek, CATCH_REC_LIST1) ) ( f, peek, __VA_ARGS__ ) + +#define CATCH_REC_LIST0_UD(f, userdata, x, peek, ...) , f(userdata, x) CATCH_DEFER ( CATCH_REC_NEXT(peek, CATCH_REC_LIST1_UD) ) ( f, userdata, peek, __VA_ARGS__ ) +#define CATCH_REC_LIST1_UD(f, userdata, x, peek, ...) , f(userdata, x) CATCH_DEFER ( CATCH_REC_NEXT(peek, CATCH_REC_LIST0_UD) ) ( f, userdata, peek, __VA_ARGS__ ) +#define CATCH_REC_LIST2_UD(f, userdata, x, peek, ...) f(userdata, x) CATCH_DEFER ( CATCH_REC_NEXT(peek, CATCH_REC_LIST1_UD) ) ( f, userdata, peek, __VA_ARGS__ ) + +// Applies the function macro `f` to each of the remaining parameters, inserts commas between the results, +// and passes userdata as the first parameter to each invocation, +// e.g. CATCH_REC_LIST_UD(f, x, a, b, c) evaluates to f(x, a), f(x, b), f(x, c) +#define CATCH_REC_LIST_UD(f, userdata, ...) CATCH_RECURSE(CATCH_REC_LIST2_UD(f, userdata, __VA_ARGS__, ()()(), ()()(), ()()(), 0)) + +#define CATCH_REC_LIST(f, ...) CATCH_RECURSE(CATCH_REC_LIST2(f, __VA_ARGS__, ()()(), ()()(), ()()(), 0)) + +#define INTERNAL_CATCH_EXPAND1(param) INTERNAL_CATCH_EXPAND2(param) +#define INTERNAL_CATCH_EXPAND2(...) INTERNAL_CATCH_NO## __VA_ARGS__ +#define INTERNAL_CATCH_DEF(...) INTERNAL_CATCH_DEF __VA_ARGS__ +#define INTERNAL_CATCH_NOINTERNAL_CATCH_DEF +#define INTERNAL_CATCH_STRINGIZE(...) INTERNAL_CATCH_STRINGIZE2(__VA_ARGS__) +#ifndef CATCH_CONFIG_TRADITIONAL_MSVC_PREPROCESSOR +#define INTERNAL_CATCH_STRINGIZE2(...) #__VA_ARGS__ +#define INTERNAL_CATCH_STRINGIZE_WITHOUT_PARENS(param) INTERNAL_CATCH_STRINGIZE(INTERNAL_CATCH_REMOVE_PARENS(param)) +#else +// MSVC is adding extra space and needs another indirection to expand INTERNAL_CATCH_NOINTERNAL_CATCH_DEF +#define INTERNAL_CATCH_STRINGIZE2(...) INTERNAL_CATCH_STRINGIZE3(__VA_ARGS__) +#define INTERNAL_CATCH_STRINGIZE3(...) #__VA_ARGS__ +#define INTERNAL_CATCH_STRINGIZE_WITHOUT_PARENS(param) (INTERNAL_CATCH_STRINGIZE(INTERNAL_CATCH_REMOVE_PARENS(param)) + 1) +#endif + +#define INTERNAL_CATCH_MAKE_NAMESPACE2(...) ns_##__VA_ARGS__ +#define INTERNAL_CATCH_MAKE_NAMESPACE(name) INTERNAL_CATCH_MAKE_NAMESPACE2(name) + +#define INTERNAL_CATCH_REMOVE_PARENS(...) INTERNAL_CATCH_EXPAND1(INTERNAL_CATCH_DEF __VA_ARGS__) + +#ifndef CATCH_CONFIG_TRADITIONAL_MSVC_PREPROCESSOR +#define INTERNAL_CATCH_MAKE_TYPE_LIST2(...) decltype(get_wrapper()) +#define INTERNAL_CATCH_MAKE_TYPE_LIST(...) INTERNAL_CATCH_MAKE_TYPE_LIST2(INTERNAL_CATCH_REMOVE_PARENS(__VA_ARGS__)) +#else +#define INTERNAL_CATCH_MAKE_TYPE_LIST2(...) INTERNAL_CATCH_EXPAND_VARGS(decltype(get_wrapper())) +#define INTERNAL_CATCH_MAKE_TYPE_LIST(...) INTERNAL_CATCH_EXPAND_VARGS(INTERNAL_CATCH_MAKE_TYPE_LIST2(INTERNAL_CATCH_REMOVE_PARENS(__VA_ARGS__))) +#endif + +#define INTERNAL_CATCH_MAKE_TYPE_LISTS_FROM_TYPES(...)\ + CATCH_REC_LIST(INTERNAL_CATCH_MAKE_TYPE_LIST,__VA_ARGS__) + +#define INTERNAL_CATCH_REMOVE_PARENS_1_ARG(_0) INTERNAL_CATCH_REMOVE_PARENS(_0) +#define INTERNAL_CATCH_REMOVE_PARENS_2_ARG(_0, _1) INTERNAL_CATCH_REMOVE_PARENS(_0), INTERNAL_CATCH_REMOVE_PARENS_1_ARG(_1) +#define INTERNAL_CATCH_REMOVE_PARENS_3_ARG(_0, _1, _2) INTERNAL_CATCH_REMOVE_PARENS(_0), INTERNAL_CATCH_REMOVE_PARENS_2_ARG(_1, _2) +#define INTERNAL_CATCH_REMOVE_PARENS_4_ARG(_0, _1, _2, _3) INTERNAL_CATCH_REMOVE_PARENS(_0), INTERNAL_CATCH_REMOVE_PARENS_3_ARG(_1, _2, _3) +#define INTERNAL_CATCH_REMOVE_PARENS_5_ARG(_0, _1, _2, _3, _4) INTERNAL_CATCH_REMOVE_PARENS(_0), INTERNAL_CATCH_REMOVE_PARENS_4_ARG(_1, _2, _3, _4) +#define INTERNAL_CATCH_REMOVE_PARENS_6_ARG(_0, _1, _2, _3, _4, _5) INTERNAL_CATCH_REMOVE_PARENS(_0), INTERNAL_CATCH_REMOVE_PARENS_5_ARG(_1, _2, _3, _4, _5) +#define INTERNAL_CATCH_REMOVE_PARENS_7_ARG(_0, _1, _2, _3, _4, _5, _6) INTERNAL_CATCH_REMOVE_PARENS(_0), INTERNAL_CATCH_REMOVE_PARENS_6_ARG(_1, _2, _3, _4, _5, _6) +#define INTERNAL_CATCH_REMOVE_PARENS_8_ARG(_0, _1, _2, _3, _4, _5, _6, _7) INTERNAL_CATCH_REMOVE_PARENS(_0), INTERNAL_CATCH_REMOVE_PARENS_7_ARG(_1, _2, _3, _4, _5, _6, _7) +#define INTERNAL_CATCH_REMOVE_PARENS_9_ARG(_0, _1, _2, _3, _4, _5, _6, _7, _8) INTERNAL_CATCH_REMOVE_PARENS(_0), INTERNAL_CATCH_REMOVE_PARENS_8_ARG(_1, _2, _3, _4, _5, _6, _7, _8) +#define INTERNAL_CATCH_REMOVE_PARENS_10_ARG(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9) INTERNAL_CATCH_REMOVE_PARENS(_0), INTERNAL_CATCH_REMOVE_PARENS_9_ARG(_1, _2, _3, _4, _5, _6, _7, _8, _9) +#define INTERNAL_CATCH_REMOVE_PARENS_11_ARG(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10) INTERNAL_CATCH_REMOVE_PARENS(_0), INTERNAL_CATCH_REMOVE_PARENS_10_ARG(_1, _2, _3, _4, _5, _6, _7, _8, _9, _10) + +#define INTERNAL_CATCH_VA_NARGS_IMPL(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, N, ...) N + +#define INTERNAL_CATCH_TYPE_GEN\ + template struct TypeList {};\ + template\ + constexpr auto get_wrapper() noexcept -> TypeList { return {}; }\ + template class...> struct TemplateTypeList{};\ + template class...Cs>\ + constexpr auto get_wrapper() noexcept -> TemplateTypeList { return {}; }\ + template\ + struct append;\ + template\ + struct rewrap;\ + template class, typename...>\ + struct create;\ + template class, typename>\ + struct convert;\ + \ + template \ + struct append { using type = T; };\ + template< template class L1, typename...E1, template class L2, typename...E2, typename...Rest>\ + struct append, L2, Rest...> { using type = typename append, Rest...>::type; };\ + template< template class L1, typename...E1, typename...Rest>\ + struct append, TypeList, Rest...> { using type = L1; };\ + \ + template< template class Container, template class List, typename...elems>\ + struct rewrap, List> { using type = TypeList>; };\ + template< template class Container, template class List, class...Elems, typename...Elements>\ + struct rewrap, List, Elements...> { using type = typename append>, typename rewrap, Elements...>::type>::type; };\ + \ + template