diff --git a/include/common_solving.hpp b/include/common_solving.hpp index f2d0a8a2..4ca859a8 100644 --- a/include/common_solving.hpp +++ b/include/common_solving.hpp @@ -6,6 +6,7 @@ #include #include #include +#include #include #include #include @@ -31,6 +32,8 @@ #include "lala/interpretation.hpp" #include "lala/flatzinc_parser.hpp" +#include "lala/tcn_parser.hpp" +#include "lala/tcn_writer.hpp" #ifdef WITH_XCSP3PARSER #include "lala/XCSP3_parser.hpp" @@ -310,6 +313,36 @@ struct AbstractDomains { } private: + CUDA void dump_preprocessed_tcn_if_needed() { +#ifdef __CUDA_ARCH__ + return; +#else +#ifndef TURBO_IPC_ABSTRACT_DOMAIN + if(config.dump_preprocessed_tcn.size() == 0) { + return; + } + if(store->is_bot() || iprop->is_bot()) { + std::cerr << "Cannot dump preprocessed TCN because the abstract state is bottom." << std::endl; + exit(EXIT_FAILURE); + } + std::ofstream out(config.dump_preprocessed_tcn.data()); + if(!out) { + std::cerr << "Cannot open preprocessed TCN output file " << config.dump_preprocessed_tcn.data() << std::endl; + exit(EXIT_FAILURE); + } + write_preprocessed_tcn(out, *store, *iprop, *bab); + if(config.verbose_solving) { + printf("%% Preprocessed TCN written to %s\n", config.dump_preprocessed_tcn.data()); + } +#else + if(config.dump_preprocessed_tcn.size() != 0) { + std::cerr << "-dump_preprocessed_tcn is only supported with the PIR/TCN abstract domain." << std::endl; + exit(EXIT_FAILURE); + } +#endif +#endif + } + // Mainly to interpret the IN constraint in IProp instead of only over-approximating in intervals. template CUDA void typing(F& f, bool toplevel = true) const { @@ -413,6 +446,9 @@ struct AbstractDomains { f = parse_xcsp3(config.problem_path.data(), solver_output); } #endif + else if(config.input_format() == InputFormat::TCN) { + f = parse_tcn(config.problem_path.data(), solver_output); + } if(!f) { std::cerr << "Could not parse input file." << std::endl; exit(EXIT_FAILURE); @@ -519,6 +555,21 @@ struct AbstractDomains { stats.print_array_stat("preprocessing_eliminated_variables", preprocessing_stats.eliminated_useless_variables_, [](auto v) { return std::to_string(v); }); } + /** Load a TCN file directly into the abstract domain, skipping ternarization, + * normalization and simplification. Constraints are interpreted in the exact + * order they appear in the file. */ + void load_tcn(F& f) { + size_t num_vars = num_quantified_vars(f); + allocate(num_vars, true); + iprop->disable_sort_bytecodes(); + if(!interpret(f)) { + exit(EXIT_FAILURE); + } + analyze_tcn("tcn"); + simplifier->init_env(env); + simplifier->initialize(num_vars, 0); + } + void preprocess_tcn(F& f) { f = ternarize(f, VarEnv(), {0,1,2}); battery::vector extra; @@ -622,12 +673,16 @@ struct AbstractDomains { #else constexpr bool use_ipc = false; #endif - if(use_ipc && !config.force_ternarize) { + if(config.input_format() == InputFormat::TCN) { + load_tcn(*f_ptr); + } + else if(use_ipc && !config.force_ternarize) { preprocess_ipc(*f_ptr); } else { preprocess_tcn(*f_ptr); } + dump_preprocessed_tcn_if_needed(); push_eps_strategy(); std::mt19937 random_generator(config.seed); split->shuffle_random_strategies(random_generator); diff --git a/include/config.hpp b/include/config.hpp index 6474e220..4bc26e8d 100644 --- a/include/config.hpp +++ b/include/config.hpp @@ -26,7 +26,8 @@ enum class FixpointKind { enum class InputFormat { XCSP3, - FLATZINC + FLATZINC, + TCN }; template @@ -52,6 +53,7 @@ struct Configuration { FixpointKind fixpoint; size_t wac1_threshold; size_t seed; + battery::string dump_preprocessed_tcn; battery::string eps_var_order; battery::string eps_value_order; battery::string problem_path; @@ -97,6 +99,7 @@ struct Configuration { ), wac1_threshold(0), seed(0), + dump_preprocessed_tcn(alloc), eps_value_order("default", alloc), eps_var_order("default", alloc), problem_path(alloc), @@ -129,6 +132,7 @@ struct Configuration { fixpoint(other.fixpoint), wac1_threshold(other.wac1_threshold), seed(other.seed), + dump_preprocessed_tcn(other.dump_preprocessed_tcn, alloc), eps_var_order(other.eps_var_order, alloc), eps_value_order(other.eps_value_order, alloc), problem_path(other.problem_path, alloc), @@ -158,11 +162,13 @@ struct Configuration { fixpoint = other.fixpoint; wac1_threshold = other.wac1_threshold; seed = other.seed; + dump_preprocessed_tcn = other.dump_preprocessed_tcn; eps_var_order = other.eps_var_order; eps_value_order = other.eps_value_order; problem_path = other.problem_path; version = other.version; hardware = other.hardware; + return *this; } CUDA void print_commandline(const char* program_name) { @@ -193,6 +199,9 @@ struct Configuration { if(fixpoint == FixpointKind::WAC1) { printf("-wac1_threshold %" PRIu64 " ", wac1_threshold); } + if(dump_preprocessed_tcn.size() != 0) { + printf("-dump_preprocessed_tcn %s ", dump_preprocessed_tcn.data()); + } printf("-seed %" PRIu64 " ", seed); printf("-eps_var_order %s ", eps_var_order.data()); printf("-eps_value_order %s ", eps_value_order.data()); @@ -241,6 +250,9 @@ struct Configuration { printf("%%%%%%mzn-stat: hardware=\"%s\"\n", (hardware.size() == 0) ? "unspecified" : hardware.data()); printf("%%%%%%mzn-stat: arch=\"%s\"\n", name_of_arch(arch)); printf("%%%%%%mzn-stat: fixpoint=\"%s\"\n", name_of_fixpoint(fixpoint)); + if(dump_preprocessed_tcn.size() != 0) { + printf("%%%%%%mzn-stat: dump_preprocessed_tcn=\"%s\"\n", dump_preprocessed_tcn.data()); + } // printf("%%%%%%mzn-stat: subproblems_power=\"%d\"\n", subproblems_power); // do not print because it must be printed before it is modified in barebones. printf("%%%%%%mzn-stat: subproblems_factor=%" PRIu64 "\n", subproblems_factor); if(fixpoint == FixpointKind::WAC1) { @@ -272,8 +284,11 @@ struct Configuration { else if(problem_path.ends_with(".xml")) { return InputFormat::XCSP3; } + else if(problem_path.ends_with(".tcn")) { + return InputFormat::TCN; + } else { - printf("ERROR: Unknown input format for the file %s [supported extension: .xml and .fzn].\n", problem_path.data()); + printf("ERROR: Unknown input format for the file %s [supported extensions: .xml, .fzn, .tcn].\n", problem_path.data()); exit(EXIT_FAILURE); } } diff --git a/src/config.cpp b/src/config.cpp index 832cdff3..2b0e29b6 100644 --- a/src/config.cpp +++ b/src/config.cpp @@ -9,7 +9,7 @@ #include void usage_and_exit(const std::string& program_name) { - std::cout << "usage: " << program_name << " [-t 2000] [-a] [-n 10] [-i] [-f] [-s] [-v] [-p ] [-arch ] [-p 48] [-or 48] [-sub 12] [-stack 100] [-fp ] [-wac1_threshold 0] [-eps_var_order ] [-eps_value_order ] [-seed 0] [-network_analysis] [-cutnodes 0] [-disable_simplify] [-force_ternarize] [-globalmem] [-version 1.0.0] [xcsp3instance.xml | fzninstance.fzn]" << std::endl; + std::cout << "usage: " << program_name << " [-t 2000] [-a] [-n 10] [-i] [-f] [-s] [-v] [-p ] [-arch ] [-p 48] [-or 48] [-sub 12] [-stack 100] [-fp ] [-wac1_threshold 0] [-dump_preprocessed_tcn path.tcn] [-eps_var_order ] [-eps_value_order ] [-seed 0] [-network_analysis] [-cutnodes 0] [-disable_simplify] [-force_ternarize] [-globalmem] [-version 1.0.0] [xcsp3instance.xml | fzninstance.fzn | instance.tcn]" << std::endl; std::cout << "\t-t 2000: Run the solver with a timeout of 2000 milliseconds." << std::endl; std::cout << "\t-timeout 2000: Same as -t, but if both -t and -timeout are specified, -timeout overrides -t." << std::endl; std::cout << "\t-a: Instructs the solver to report all solutions in the case of satisfaction problems, or print intermediate solutions of increasing quality in the case of optimisation problems." << std::endl; @@ -25,6 +25,7 @@ void usage_and_exit(const std::string& program_name) { std::cout << "\t\t ac1: All propagators are executed in parallel at each iteration." << std::endl; std::cout << "\t\t wac1: Behave as ac1 when the number of active propagators is less than wac1_threshold. Otherwise, each warp must reach a local fixpoint before executing the next 32 propagators (not compatible with -arch cpu)." << std::endl; std::cout << "\t-wac1_threshold 4096: Threshold below which we select AC1 instead of WAC1 (default: 0)." << std::endl; + std::cout << "\t-dump_preprocessed_tcn path.tcn: Dump the preprocessed ternary constraint network in the TCN text format (operators: +, *, A, I, L, =, M, D)." << std::endl; std::cout << "\t-or 48: Run the subproblems on 48 streaming multiprocessors (SMs) (only for GPU architecture). Default: -or 0 for automatic selection of the number of SMs." << std::endl; std::cout << "\t-sub 12: Create 2^12 subproblems to be solved in turns by the blocks (embarrasingly parallel search). The special value `-1` leaves Turbo to decide on the number of subproblems (at least 30 * number of blocks). Default: -sub -1." << std::endl; std::cout << "\t-subfactor 300: Create B * 300 subproblems to be solved in turns by `B` blocks (embarrasingly parallel search). Default: -subfactor 300." << std::endl; @@ -193,6 +194,10 @@ Configuration parse_args(int argc, char** argv) { } } input.read_size_t("-wac1_threshold", config.wac1_threshold); + std::string dump_preprocessed_tcn; + if(input.read_string("-dump_preprocessed_tcn", dump_preprocessed_tcn)) { + config.dump_preprocessed_tcn = battery::string(dump_preprocessed_tcn.data()); + } std::string eps_var_order; if(input.read_string("-eps_var_order", eps_var_order)) { config.eps_var_order = battery::string(eps_var_order.data());