solve memory issue

meelgroup · Nov 22, 2024 · 567a0f9 · 567a0f9
1 parent 73d1247
commit 567a0f9
Show file tree

Hide file tree

Showing 4 changed files with 25 additions and 20 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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