From 567a0f95d3b823c64216d6e141bf03793e41fdcb Mon Sep 17 00:00:00 2001 From: Arijit Shaw Date: Fri, 22 Nov 2024 15:56:23 -0500 Subject: [PATCH] solve memory issue --- include/stp/STPManager/UserDefinedFlags.h | 1 + lib/extlib-abc/aig/cnf/cnfMan.c | 1 + lib/extlib-abc/aig/cnf/cnfWrite.c | 4 ++- tools/stp/main.cpp | 39 ++++++++++++----------- 4 files changed, 25 insertions(+), 20 deletions(-) diff --git a/include/stp/STPManager/UserDefinedFlags.h b/include/stp/STPManager/UserDefinedFlags.h index 66dba8f8..d50a8e4a 100644 --- a/include/stp/STPManager/UserDefinedFlags.h +++ b/include/stp/STPManager/UserDefinedFlags.h @@ -110,6 +110,7 @@ struct UserDefinedFlags // output flags bool output_CNF_flag = false; bool output_bench_flag = false; + bool verbose_in_counting = false; /* Bitblasting options */ diff --git a/lib/extlib-abc/aig/cnf/cnfMan.c b/lib/extlib-abc/aig/cnf/cnfMan.c index 77711f2a..340a23a8 100644 --- a/lib/extlib-abc/aig/cnf/cnfMan.c +++ b/lib/extlib-abc/aig/cnf/cnfMan.c @@ -143,6 +143,7 @@ void Cnf_DataFree( Cnf_Dat_t * p ) free( p->pClauses[0] ); free( p->pClauses ); free( p->pVarNums ); + free( p->lProjVars ); free( p ); } diff --git a/lib/extlib-abc/aig/cnf/cnfWrite.c b/lib/extlib-abc/aig/cnf/cnfWrite.c index 32763234..63abb189 100644 --- a/lib/extlib-abc/aig/cnf/cnfWrite.c +++ b/lib/extlib-abc/aig/cnf/cnfWrite.c @@ -230,11 +230,13 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs ) pCnf->pClauses = ALLOC( int *, nClauses + 1 ); pCnf->pClauses[0] = ALLOC( int, nLiterals ); pCnf->pClauses[nClauses] = pCnf->pClauses[0] + nLiterals; - pCnf->lProjVars = ALLOC( int, nLiterals ); // create room for variable numbers pCnf->pVarNums = ALLOC( int, Aig_ManObjNumMax(p->pManAig) ); memset( pCnf->pVarNums, 0xff, sizeof(int) * Aig_ManObjNumMax(p->pManAig) ); + pCnf->lProjVars = ALLOC( int, Aig_ManObjNumMax(p->pManAig) ); + memset( pCnf->lProjVars, 0xff, sizeof(int) * Aig_ManObjNumMax(p->pManAig) ); + // assign variables to the last (nOutputs) POs Number = 1; if ( nOutputs ) diff --git a/tools/stp/main.cpp b/tools/stp/main.cpp index 6339b4df..7641dafa 100644 --- a/tools/stp/main.cpp +++ b/tools/stp/main.cpp @@ -364,25 +364,26 @@ void ExtraMain::create_options() po::options_description misc_options("Output options"); - misc_options.add_options() - ("exit-after-CNF", - po::bool_switch(&(bm->UserFlags.exit_after_CNF)), - "exit after the CNF has been generated") - - ("max-num-confl,max_num_confl,g", - INT64_ARG(bm->UserFlags.timeout_max_conflicts), - "Number of conflicts after which the SAT solver gives up. " - "-1 means never") - - ("max-time,max_time,k", - INT64_ARG(bm->UserFlags.timeout_max_time), - "Number of seconds after which the SAT solver gives up. " - "-1 means never.") - - ("check-sanity,d", - po::bool_switch(&(bm->UserFlags.check_counterexample_flag)), - "construct counterexample and check it"); - + misc_options.add_options()("exit-after-CNF", + po::bool_switch(&(bm->UserFlags.exit_after_CNF)), + "exit after the CNF has been generated") + + ("max-num-confl,max_num_confl,g", + INT64_ARG(bm->UserFlags.timeout_max_conflicts), + "Number of conflicts after which the SAT solver gives up. " + "-1 means never") + + ("max-time,max_time,k", INT64_ARG(bm->UserFlags.timeout_max_time), + "Number of seconds after which the SAT solver gives up. " + "-1 means never.") + + ("verb-count,x", + po::bool_switch(&(bm->UserFlags.verbose_in_counting)), + "Be verbose in counting/sampling mode") + + ("check-sanity,d", + po::bool_switch(&(bm->UserFlags.check_counterexample_flag)), + "construct counterexample and check it"); #undef BOOL_ARG #undef INT64_ARG