From 4028b6cb2ef920edfee4a47af999281126149820 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Fri, 9 Jul 2010 08:28:46 +0000 Subject: [PATCH] Add the option to exit after generating the CNF. Currently only works for bit-vectors (which don't have abstraction refinement). git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@942 e59a4935-1847-0410-ae03-e826735625c1 --- src/STPManager/UserDefinedFlags.h | 5 ++++- src/main/main.cpp | 11 +++++++++-- src/to-sat/AIG/ToSATAIG.cpp | 3 +++ 3 files changed, 16 insertions(+), 3 deletions(-) diff --git a/src/STPManager/UserDefinedFlags.h b/src/STPManager/UserDefinedFlags.h index 0265915..f365ded 100644 --- 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 1893f57..3df5e96 100644 --- 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 3adf1e9..386ba04 100644 --- 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); -- 2.47.3