Add option to dump the variable mapping

src/config/Config.cpp

@@ -48,6 +48,7 @@ namespace d4 {
     config.float_precision = 128;
     config.isFloat = false;
     config.dump_ddnnf = "";
+    config.dump_gmap = "";
     config.query = "";
     config.projMC_refinement = false;
     config.keyword_output_format_solution = "s";

src/config/Config.hpp

@@ -51,6 +51,7 @@ namespace d4 {
     int float_precision;
     bool isFloat;
     string dump_ddnnf;
+    string dump_gmap;
     string query;
     bool projMC_refinement;
     string keyword_output_format_solution;

src/config/ConfigConverter.cpp

@@ -60,6 +60,12 @@ namespace d4 {
       config.dump_ddnnf = "";
     }
 
+    if (vm.count("dump-gmap")) {
+      config.dump_gmap = vm["dump-gmap"].as<string>();
+    } else {
+      config.dump_gmap = "";
+    }
+
     if (vm.count("query")) {
       config.query = vm["query"].as<string>();
     } else {

src/methods/DecisionDNNFOperation.hpp

@@ -137,6 +137,19 @@ class DecisionDNNFOperation : public Operation<T, U> {
      @param[in] out, the output stream.
   */
   void manageResult(U &result, Config &config, std::ostream &out) {
+    if (!config.dump_gmap.empty()) {
+      std::string fileName = config.dump_gmap;
+
+      std::ofstream outFile;
+      outFile.open(fileName);
+
+      for (auto literal : m_problem->gmap()) {
+        outFile << literal << "\n";
+      }
+
+      outFile.close();
+    }
+
     if (!config.dump_ddnnf.empty()) {
       std::ofstream outFile;
       std::string fileName = config.dump_ddnnf;

src/option.dsc

@@ -43,6 +43,7 @@
 ("float-precision,fp", boost::program_options::value<int>()->default_value(128), "The precision for the float.")
 ("float,f", boost::program_options::value<bool>()->default_value(false), "If the count is computed as a float or not.")
 ("dump-ddnnf", boost::program_options::value<std::string>(), "Print out the decision DNNF formula in a given file.")
+("dump-gmap", boost::program_options::value<std::string>(), "Print out the variable mapping to the given file.")
 ("query,q", boost::program_options::value<std::string>(), "Perform the queries given in a file (m l1 l2 ... ln 0 for a model counting query, and d l1 l2 ... ln 0 for a satisfiability query).")
 ("projMC-refinement", boost::program_options::value<bool>()->default_value(false), "Try to reduce the set of selector by computing a MSS.")
 ("keyword-output-format-solution", boost::program_options::value<std::string>()->default_value("s"), "The keyword prints in front of the solution when it is printed out.")

src/preprocs/cnf/PreprocProj.cpp

@@ -17,7 +17,7 @@ PreprocProj::PreprocProj(Config &d4Config, std::ostream &out) {
   config.ve_only_simpical = d4Config.preproc_ve_only_simpical;
   config.ve_prefer_simpical = d4Config.preproc_ve_prefer_simpical;
   config.ve_limit = d4Config.preproc_ve_limit;
-  keep_map = false;
+  keep_map = !d4Config.dump_gmap.empty();
 } // constructor
 
 /**