From c2d9c466e9dfc620584aa31edc07472ab9a1964a Mon Sep 17 00:00:00 2001 From: vijay_ganesh Date: Tue, 8 Dec 2009 18:05:26 +0000 Subject: [PATCH] completed the cnf dumping feature. it works git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@486 e59a4935-1847-0410-ae03-e826735625c1 --- src/STPManager/STP.cpp | 2 +- src/STPManager/UserDefinedFlags.h | 2 ++ src/main/main.cpp | 3 +++ 3 files changed, 6 insertions(+), 1 deletion(-) diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp index 3e710a3..623b625 100644 --- a/src/STPManager/STP.cpp +++ b/src/STPManager/STP.cpp @@ -28,7 +28,7 @@ namespace BEEV { MINISAT::Solver NewSolver; if(bm->UserFlags.print_cnf_flag) { - newS.needLibraryCNFFile("output.cnf"); + NewSolver.needLibraryCNFFile(bm->UserFlags.cnf_dump_filename); } #endif diff --git a/src/STPManager/UserDefinedFlags.h b/src/STPManager/UserDefinedFlags.h index 359df1f..5fbb988 100644 --- a/src/STPManager/UserDefinedFlags.h +++ b/src/STPManager/UserDefinedFlags.h @@ -67,6 +67,7 @@ namespace BEEV //Flag that allows the printing of the DIMACS format of the input bool print_cnf_flag; + char * cnf_dump_filename; //flag to decide whether to print "valid/invalid" or not bool print_output_flag; @@ -146,6 +147,7 @@ namespace BEEV //Flag that allows the printing of the DIMACS format of the //input print_cnf_flag = false; + cnf_dump_filename = (char*)"stp-input.cnf"; //flag to decide whether to print "valid/invalid" or not print_output_flag = false; diff --git a/src/main/main.cpp b/src/main/main.cpp index f4e7ab4..9a2d45c 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -91,6 +91,8 @@ int main(int argc, char ** argv) { "-h : help\n"; helpstring += "-i : Randomize STP's satisfiable output. Random_seed is an integer >= 0.\n"; + helpstring += + "-j : CNF Dumping. Creates a DIMACS equivalent file of the input STP file\n"; helpstring += "-m : use the SMTLIB parser\n"; helpstring += @@ -169,6 +171,7 @@ int main(int argc, char ** argv) { break; case 'j': bm->UserFlags.print_cnf_flag = true; + bm->UserFlags.cnf_dump_filename = argv[++i]; break; case 'n': bm->UserFlags.print_output_flag = true; -- 2.47.3