feat: enable to dump the preprocessed input

Author: uulm-janbaudisch

src/config/Config.cpp

@@ -48,6 +48,7 @@ namespace d4 {
     config.float_precision = 128;
     config.isFloat = false;
     config.dump_ddnnf = "";
+    config.dump_preproc = "";
     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_preproc;
     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-preproc")) {
+      config.dump_preproc = vm["dump-preproc"].as<string>();
+    } else {
+      config.dump_preproc = "";
+    }
+
     if (vm.count("query")) {
       config.query = vm["query"].as<string>();
     } else {

src/methods/MethodManager.cpp

@@ -82,6 +82,13 @@ MethodManager *MethodManager::makeMethodManager(Config &config,
   displayInfoVariables(runProblem, out);
   out << "c [MODE] Panic: " << lastBreath.panic << "\n";
 
+  if (!config.dump_preproc.empty()) {
+    std::ofstream outFile;
+    outFile.open(config.dump_preproc);
+    runProblem->display(outFile);
+    outFile.close();
+  }
+
   if (meth == "counting") {
     if (!isFloat)
       return new DpllStyleMethod<mpz::mpz_int, mpz::mpz_int>(

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-preproc", boost::program_options::value<std::string>(), "Print out the preprocessed CNF in a 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/problem/cnf/ProblemManagerCnf.cpp

@@ -197,7 +197,7 @@ ProblemManagerCnf::getConditionedFormula(std::vector<Lit> &units) {
  */
 
 void ProblemManagerCnf::display(std::ostream &out) {
-  out << "weight list: ";
+  out << "c weight list: ";
   for (unsigned i = 1; i <= m_nbVar; i++) {
     Lit l = Lit::makeLit(i, false);
     out << i << "[" << m_weightVar[i] << "] ";