Add the option to exit after generating the CNF. Currently only works for bit-vectors...

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@942 e59a4935-1847-0410-ae03-e826735625c1

diff --git a/src/STPManager/UserDefinedFlags.h b/src/STPManager/UserDefinedFlags.h
index 0265915155fd74fbcf13f4409683c8ae54e3ff11..f365ded0becd29c292a64fd1d50b9e47ea13004a 100644 (file)
--- a/src/STPManager/UserDefinedFlags.h
+++ b/src/STPManager/UserDefinedFlags.h
@@ -113,9 +113,10 @@ namespace BEEV
 
     bool bitConstantProp_flag;
 
-
     bool cBitP_propagateForDivisionByZero;
 
+    bool exit_after_CNF;
+
     // Available back-end SAT solvers.
     enum SATSolvers
       {
@@ -227,6 +228,8 @@ namespace BEEV
       // given a/b = c, propagates that c<=a even if b may be zero.
       cBitP_propagateForDivisionByZero =true;
 
+      exit_after_CNF=false;
+
     } //End of constructor for UserDefinedFlags
 
   }; //End of struct UserDefinedFlags

diff --git a/src/main/main.cpp b/src/main/main.cpp
index 1893f57b2a6b217379ef629d2883166ada812e82..3df5e968c98a76863bde58ffa7d374ce193ce9bf 100644 (file)
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -61,7 +61,7 @@ static const intptr_t INITIAL_MEMORY_PREALLOCATION_SIZE = 4000000;
  * step 5. Call SAT to determine if input is SAT or UNSAT
  ********************************************************************/
 
-typedef enum {PRINT_BACK_C=1, PRINT_BACK_CVC, PRINT_BACK_SMTLIB2,PRINT_BACK_SMTLIB1, PRINT_BACK_GDL, PRINT_BACK_DOT, OUTPUT_BENCH, OUTPUT_CNF, USE_SIMPLIFYING_SOLVER, SMT_LIB2_FORMAT, SMT_LIB1_FORMAT, DISABLE_CBITP} OptionType;
+typedef enum {PRINT_BACK_C=1, PRINT_BACK_CVC, PRINT_BACK_SMTLIB2,PRINT_BACK_SMTLIB1, PRINT_BACK_GDL, PRINT_BACK_DOT, OUTPUT_BENCH, OUTPUT_CNF, USE_SIMPLIFYING_SOLVER, SMT_LIB2_FORMAT, SMT_LIB1_FORMAT, DISABLE_CBITP,EXIT_AFTER_CNF} OptionType;
 
 int main(int argc, char ** argv) {
   char * infile = NULL;
@@ -110,7 +110,9 @@ int main(int argc, char ** argv) {
 #ifdef WITHCBITP
   helpstring +=  
       "--disable-cbitp  : disable constant bit propagation\n";
-#endif WITHCBITP
+#endif
+
+  helpstring +=  "--exit-after-CNF : exit after the CNF has been generated\n";
 
   helpstring +=
     "-e  : expand finite-for construct\n";
@@ -183,17 +185,22 @@ helpstring +=
                          lookup.insert(make_pair(tolower("--print-back-GDL"),PRINT_BACK_GDL));
                          lookup.insert(make_pair(tolower("--print-back-dot"),PRINT_BACK_DOT));
                          lookup.insert(make_pair(tolower("--output-CNF"),OUTPUT_CNF));
+                          lookup.insert(make_pair(tolower("--exit-after-CNF"),EXIT_AFTER_CNF));
                          lookup.insert(make_pair(tolower("--output-bench"),OUTPUT_BENCH));
                          lookup.insert(make_pair(tolower("--simplifying-minisat"),USE_SIMPLIFYING_SOLVER));
                          lookup.insert(make_pair(tolower("--SMTLIB2"),SMT_LIB2_FORMAT));
                          lookup.insert(make_pair(tolower("--SMTLIB1"),SMT_LIB1_FORMAT));
                          lookup.insert(make_pair(tolower("--disable-cbitp"),DISABLE_CBITP));
 
+
                          switch(lookup[tolower(argv[i])])
                          {
                          case DISABLE_CBITP:
                                   bm->UserFlags.bitConstantProp_flag = false;
                                   break;
+                         case EXIT_AFTER_CNF:
+                                  bm->UserFlags.exit_after_CNF = true;
+                                  break;
                          case PRINT_BACK_C:
                                  bm->UserFlags.print_STPinput_back_C_flag = true;
                                  onePrintBack = true;

diff --git a/src/to-sat/AIG/ToSATAIG.cpp b/src/to-sat/AIG/ToSATAIG.cpp
index 3adf1e95ef2b93396cfe0ee45f7b2caf3f5097f8..386ba0470853b1eddfe91142932bbc649a7b0517 100644 (file)
--- a/src/to-sat/AIG/ToSATAIG.cpp
+++ b/src/to-sat/AIG/ToSATAIG.cpp
@@ -74,6 +74,9 @@ namespace BEEV
       Cnf_ClearMemory();
       Cnf_DataFree(cnfData);
 
+      if (bm->UserFlags.exit_after_CNF)
+        exit(0);
+
       // cryptominisat treats simplify() as protected.
 #ifndef CRYPTOMINISAT2
       bm->GetRunTimes()->start(RunTimes::SATSimplifying);