From d5e1a5d445f68bdb4895bb735b9568e5f4738c13 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 2 Jan 2025 00:33:22 +0700 Subject: [PATCH] Bug fix in &gencex. --- src/aig/gia/giaPat2.c | 6 ++++++ src/base/abci/abc.c | 2 +- 2 files changed, 7 insertions(+), 1 deletion(-) diff --git a/src/aig/gia/giaPat2.c b/src/aig/gia/giaPat2.c index 93c4b1da9..b0839f5d4 100644 --- a/src/aig/gia/giaPat2.c +++ b/src/aig/gia/giaPat2.c @@ -965,6 +965,12 @@ Vec_Wec_t * Min_ManComputeCexes( Gia_Man_t * p, Vec_Int_t * vOuts0, int nMaxTrie if ( Vec_IntEntry(vStats[2], i) >= nMinCexes || Vec_IntEntry(vStats[1], i) > 10*Vec_IntEntry(vStats[2], i) ) continue; { + assert( Gia_ObjIsCo(pObj) ); + if ( Gia_ObjFaninId0p(p, pObj) == 0 ) { + if ( fVerbose ) + printf( "Output %d is driven by constant %d.\n", Gia_ObjCioId(pObj), Gia_ObjFaninC0(pObj) ); + continue; + } abctime clk = Abc_Clock(); int iObj = Min_ManCo(pNew, i); int Index = Gia_ObjCioId(pObj); diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index cc28e1803..dcfa8a501 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -54262,7 +54262,7 @@ int Abc_CommandAbc9GenCex( Abc_Frame_t * pAbc, int argc, char ** argv ) usage: Abc_Print( -2, "usage: &gencex [-CM num] [-F file] [-stcbvh]\n" ); Abc_Print( -2, "\t generates satisfying assignments for each output of the miter\n" ); - Abc_Print( -2, "\t-C num : the number of timeframes [default = %d]\n", nMinCexes ); + Abc_Print( -2, "\t-C num : the number of satisfying assignments [default = %d]\n", nMinCexes ); Abc_Print( -2, "\t-M num : the max simulation runs before using SAT [default = %d]\n", nMaxTries ); Abc_Print( -2, "\t-F file : the output file name [default = %s]\n", pFileName ); Abc_Print( -2, "\t-s : toggles using reverse simulation [default = %s]\n", fUseSim ? "yes": "no" );