Support TCN input and dump preprocessed TCN

include/common_solving.hpp

@@ -6,6 +6,7 @@
 #include <atomic>
 #include <algorithm>
 #include <chrono>
+#include <fstream>
 #include <thread>
 #include <csignal>
 #include <random>
@@ -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 <class F>
   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<BasicAllocator>(), {0,1,2});
     battery::vector<F> 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);

include/config.hpp

@@ -26,7 +26,8 @@ enum class FixpointKind {
 
 enum class InputFormat {
   XCSP3,
-  FLATZINC
+  FLATZINC,
+  TCN
 };
 
 template<class Allocator>
@@ -52,6 +53,7 @@ struct Configuration {
   FixpointKind fixpoint;
   size_t wac1_threshold;
   size_t seed;
+  battery::string<allocator_type> dump_preprocessed_tcn;
   battery::string<allocator_type> eps_var_order;
   battery::string<allocator_type> eps_value_order;
   battery::string<allocator_type> 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);
     }
   }

src/config.cpp

@@ -9,7 +9,7 @@
 #include <algorithm>
 
 void usage_and_exit(const std::string& program_name) {
-  std::cout << "usage: " << program_name << " [-t 2000] [-a] [-n 10] [-i] [-f] [-s] [-v] [-p <i>] [-arch <cpu|hybrid|gpu|barebones>] [-p 48] [-or 48] [-sub 12] [-stack 100] [-fp <ac1|wac1>] [-wac1_threshold 0] [-eps_var_order <input_order|first_fail|anti_first_fail|smallest|largest>] [-eps_value_order <min|max|split|reverse_split>] [-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 <i>] [-arch <cpu|hybrid|gpu|barebones>] [-p 48] [-or 48] [-sub 12] [-stack 100] [-fp <ac1|wac1>] [-wac1_threshold 0] [-dump_preprocessed_tcn path.tcn] [-eps_var_order <input_order|first_fail|anti_first_fail|smallest|largest>] [-eps_value_order <min|max|split|reverse_split>] [-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<battery::standard_allocator> 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<battery::standard_allocator>(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<battery::standard_allocator>(eps_var_order.data());