From: trevor_hansen Date: Thu, 18 Mar 2010 15:04:33 +0000 (+0000) Subject: Output flags for bench format, and a rough CNF. X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=736617175bfb9da0ed169fbed969173946229bcc;p=francis%2Fstp.git 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 8a0a55b..ea3340f 100644 --- 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 251add5..e7944fc 100644 --- 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 : 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 c3c2de5..19c5aa1 100644 --- 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 +#include 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::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 ddea9d8..9e413d5 100644 --- 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()