feat: add preprocessing-only option

SoftVarE-Group · Feb 7, 2025 · feaf162 · feaf162
1 parent fbc93ac
commit feaf162
Show file tree

Hide file tree

Showing 5 changed files with 12 additions and 2 deletions.
diff --git a/src/config/Config.cpp b/src/config/Config.cpp
@@ -49,6 +49,7 @@ namespace d4 {
     config.isFloat = false;
     config.dump_ddnnf = "";
     config.dump_preproc = "";
+    config.only_preproc = true;
     config.query = "";
     config.projMC_refinement = false;
     config.keyword_output_format_solution = "s";

diff --git a/src/config/Config.hpp b/src/config/Config.hpp
@@ -52,6 +52,7 @@ namespace d4 {
     bool isFloat;
     string dump_ddnnf;
     string dump_preproc;
+    bool only_preproc;
     string query;
     bool projMC_refinement;
     string keyword_output_format_solution;

diff --git a/src/config/ConfigConverter.cpp b/src/config/ConfigConverter.cpp
@@ -66,6 +66,8 @@ namespace d4 {
       config.dump_preproc = "";
     }
 
+    config.only_preproc = vm["only-preproc"].as<bool>();
+
     if (vm.count("query")) {
       config.query = vm["query"].as<string>();
     } else {

diff --git a/src/methods/MethodManager.cpp b/src/methods/MethodManager.cpp
@@ -79,8 +79,6 @@ MethodManager *MethodManager::makeMethodManager(Config &config,
 
   LastBreathPreproc lastBreath;
   ProblemManager *runProblem = runPreproc(config, problem, out, lastBreath);
-  displayInfoVariables(runProblem, out);
-  out << "c [MODE] Panic: " << lastBreath.panic << "\n";
 
   if (!config.dump_preproc.empty()) {
     std::ofstream outFile;
@@ -89,6 +87,13 @@ MethodManager *MethodManager::makeMethodManager(Config &config,
     outFile.close();
   }
 
+  if (config.only_preproc) {
+    exit(0);
+  }
+
+  displayInfoVariables(runProblem, out);
+  out << "c [MODE] Panic: " << lastBreath.panic << "\n";
+
   if (meth == "counting") {
     if (!isFloat)
       return new DpllStyleMethod<mpz::mpz_int, mpz::mpz_int>(

diff --git a/src/option.dsc b/src/option.dsc
@@ -44,6 +44,7 @@
 ("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.")
+("only-preproc", boost::program_options::value<bool>()->default_value(false), "Stop after preprocessing.")
 ("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.")