Output flags for bench format, and a rough CNF.

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

diff --git a/src/STPManager/UserDefinedFlags.h b/src/STPManager/UserDefinedFlags.h
index 8a0a55bb6b46a3e54ef573e03585634230a86a46..ea3340f842520025c1a5717136275df0b8d68d90 100644 (file)
--- a/src/STPManager/UserDefinedFlags.h
+++ b/src/STPManager/UserDefinedFlags.h
@@ -93,6 +93,10 @@ namespace BEEV
     bool print_STPinput_back_dot_flag;
     bool print_STPinput_back_GDL_flag;
     
+    // output flags
+    bool output_CNF_flag;
+    bool output_bench_flag;
+
     //Flag to switch on the smtlib parser
     bool smtlib_parser_flag;
     
@@ -132,6 +136,9 @@ namespace BEEV
       print_counterexample_flag = false;
       print_binary_flag = false;
       
+      output_CNF_flag = false;
+      output_bench_flag = false;
+
       //Expands out the finite for-construct completely
       expand_finitefor_flag = false;
       

diff --git a/src/main/main.cpp b/src/main/main.cpp
index 251add57de9702d8d1f5ed819fc2c6058d83e0f5..e7944fc02eeac264e89b1c61ee77f932a925987b 100644 (file)
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -44,7 +44,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_SMTLIB, PRINT_BACK_GDL, PRINT_BACK_DOT} OptionType;
+typedef enum {PRINT_BACK_C=1, PRINT_BACK_CVC, PRINT_BACK_SMTLIB, PRINT_BACK_GDL, PRINT_BACK_DOT, OUTPUT_BENCH, OUTPUT_CNF} OptionType;
 
 int main(int argc, char ** argv) {
   char * infile;
@@ -102,6 +102,10 @@ int main(int argc, char ** argv) {
     "-j <filename>  : CNF Dumping. Creates a DIMACS equivalent file of the input STP file\n";
   helpstring +=  
     "-m  : use the SMTLIB parser\n";
+
+  helpstring +=  "--output-CNF : save the CNF into output.cnf\n";
+  helpstring +=  "--output-bench : save in ABC's bench format to output.bench\n";
+
   helpstring +=  
     "-p  : print counterexample\n";
   // I haven't checked that this works so don't want to include it by default.
@@ -143,6 +147,8 @@ int main(int argc, char ** argv) {
                          lookup.insert(make_pair("--print-back-SMTLIB",PRINT_BACK_SMTLIB));
                          lookup.insert(make_pair("--print-back-GDL",PRINT_BACK_GDL));
                          lookup.insert(make_pair("--print-back-dot",PRINT_BACK_DOT));
+                         lookup.insert(make_pair("--output-CNF",OUTPUT_CNF));
+                         lookup.insert(make_pair("--output-bench",OUTPUT_BENCH));
 
                          switch(lookup[argv[i]])
                          {
@@ -166,6 +172,13 @@ int main(int argc, char ** argv) {
                                  bm->UserFlags.print_STPinput_back_dot_flag = true;
                                  onePrintBack = true;
                                  break;
+                         case OUTPUT_CNF:
+                                 bm->UserFlags.output_CNF_flag = true;
+                                 //bm->UserFlags.print_cnf_flag = true;
+                                 break;
+                         case OUTPUT_BENCH:
+                                 bm->UserFlags.output_bench_flag = true;
+                                 break;
 
                          default:
                                  fprintf(stderr,usage,prog);

diff --git a/src/to-sat/ToSAT.cpp b/src/to-sat/ToSAT.cpp
index c3c2de5cc9e8988554175ce222a1434f6b051e89..19c5aa180826a8c2c143406c32b98955dafa0a6c 100644 (file)
--- a/src/to-sat/ToSAT.cpp
+++ b/src/to-sat/ToSAT.cpp
@@ -9,6 +9,9 @@
 #include "ToSAT.h"
 #include "ToSAT.h"
 #include "BitBlastNew.h"
+#include "../printer/printers.h"
+#include <iostream>
+#include <fstream>
 
 namespace BEEV
 {
@@ -161,7 +164,8 @@ namespace BEEV
 //         flag  = 1;
 //         bm->GetRunTimes()->start(RunTimes::SendingToSAT);
 //       }
-        if (newSolver.okay())
+
+       if (newSolver.okay())
           {
             continue;
           }     
@@ -174,6 +178,48 @@ namespace BEEV
           }     
       } // End of For-loop adding the clauses 
 
+    // output a CNF
+    // Because we use the SAT solver incrementally, this may ouput little pieces of the
+    // CNF that need to be joined together. Nicer would be to read it out of the solver each time.
+       if (bm->UserFlags.output_CNF_flag && true)
+       {
+                       #if defined CRYPTOMINISAT2
+                               cerr << "The -j option will give you the xor clauses that this one doesn't" << endl;
+                       #endif
+
+               ofstream file;
+               stringstream fileName;
+               fileName << "output_" << CNFFileNameCounter++ << ".cnf";
+               file.open(fileName.str().c_str());
+
+               file << "p cnf " << newSolver.nVars() << " " << cll.size() << endl;
+               i = cll.begin(), iend = cll.end();
+               for (; i != iend; i++)
+               {
+                       vector<const ASTNode*>::iterator j = (*i)->begin(), jend =
+                                       (*i)->end();
+                       for (; j != jend; j++)
+                       {
+                               const ASTNode& node = *(*j);
+                   bool negate = (NOT == node.GetKind()) ? true : false;
+                   ASTNode n = negate ? node[0] : node;
+
+                   ASTtoSATMap::iterator it =  _ASTNode_to_SATVar_Map.find(n);
+                   assert(it != _ASTNode_to_SATVar_Map.end());
+
+                   MINISAT::Var v = it->second;
+
+                               if (negate)
+                                       file << -(v + 1) << " ";
+                               else
+                                       file << (v + 1) << " ";
+                       }
+                       file << "0" << endl;
+               }
+               file.close();
+
+       }
+
     // Free the clause list before SAT solving.
     CNFMgr::DeleteClauseList(cll);
 
@@ -263,6 +309,14 @@ namespace BEEV
     bm->ASTNodeStats("after bitblasting: ", BBFormula);
     bm->GetRunTimes()->stop(RunTimes::BitBlasting);
 
+    if (bm->UserFlags.output_bench_flag)
+    {
+               ofstream file;
+               stringstream fileName;
+               fileName << "output_" << benchFileNameCounter++ << ".bench";
+               file.open(fileName.str().c_str());
+    }
+
     CNFMgr cm(bm);
     ClauseList* cl = cm.convertToCNF(BBFormula);
 

diff --git a/src/to-sat/ToSAT.h b/src/to-sat/ToSAT.h
index ddea9d8cec15b1e2767bd2de4bb4453b992e84ad..9e413d5b0a49ba68f1ac57c0171ad8a5d7753b4a 100644 (file)
--- a/src/to-sat/ToSAT.h
+++ b/src/to-sat/ToSAT.h
@@ -50,6 +50,8 @@ namespace BEEV
 
     // Ptr to STPManager
     STPMgr * bm;
+    int CNFFileNameCounter;
+    int benchFileNameCounter;
 
 #if 0
     // Memo table to check the functioning of bitblaster and CNF
@@ -111,6 +113,9 @@ namespace BEEV
       ASTTrue      = bm->CreateNode(TRUE);
       ASTFalse     = bm->CreateNode(FALSE);
       ASTUndefined = bm->CreateNode(UNDEFINED);
+      CNFFileNameCounter = 0;
+      benchFileNameCounter = 0;
+
     }
 
     // Bitblasts, CNF conversion and calls toSATandSolve()