diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2008-02-07 08:01:00 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2008-02-07 08:01:00 -0800 |
commit | 5a6924060bffb688101f54711f967305fc3fa480 (patch) | |
tree | 388d896072828c76216de12f3fdac7775f6160f7 /src/aig/fra | |
parent | 7174787abafe80437892b55a53f994da85a37342 (diff) | |
download | abc-5a6924060bffb688101f54711f967305fc3fa480.tar.gz abc-5a6924060bffb688101f54711f967305fc3fa480.tar.bz2 abc-5a6924060bffb688101f54711f967305fc3fa480.zip |
Version abc80207
Diffstat (limited to 'src/aig/fra')
-rw-r--r-- | src/aig/fra/fra.h | 2 | ||||
-rw-r--r-- | src/aig/fra/fraClaus.c | 6 | ||||
-rw-r--r-- | src/aig/fra/fraHot.c | 2 | ||||
-rw-r--r-- | src/aig/fra/fraInd.c | 6 |
4 files changed, 10 insertions, 6 deletions
diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h index 339fd810..64268358 100644 --- a/src/aig/fra/fra.h +++ b/src/aig/fra/fra.h @@ -39,7 +39,7 @@ extern "C" { #include "aig.h" #include "dar.h" #include "satSolver.h" -//#include "bar.h" +#include "ioa.h" //////////////////////////////////////////////////////////////////////// /// PARAMETERS /// diff --git a/src/aig/fra/fraClaus.c b/src/aig/fra/fraClaus.c index a35e1169..8e3a03e1 100644 --- a/src/aig/fra/fraClaus.c +++ b/src/aig/fra/fraClaus.c @@ -1530,7 +1530,7 @@ void Fra_ClausWriteIndClauses( Clu_Man_t * p ) extern void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int fCompact ); Aig_Man_t * pNew; Aig_Obj_t * pClause, * pLiteral; - char Buffer[500]; + char Buffer[500], * pName; int * pStart, * pVar2Id; int Beg, End, i, k; // create mapping from SAT vars to node IDs @@ -1561,7 +1561,9 @@ void Fra_ClausWriteIndClauses( Clu_Man_t * p ) free( pVar2Id ); Aig_ManCleanup( pNew ); // write the manager into a file - sprintf( Buffer, "%s_care.aig", p->pAig->pName ); + pName = Ioa_FileNameGeneric(p->pAig->pName); + sprintf( Buffer, "%s_care.aig", pName ); + free( pName ); printf( "Care clauses are written into file \"%s\".\n", Buffer ); Ioa_WriteAiger( pNew, Buffer, 0, 1 ); Aig_ManStop( pNew ); diff --git a/src/aig/fra/fraHot.c b/src/aig/fra/fraHot.c index 4a3f9b03..8796f827 100644 --- a/src/aig/fra/fraHot.c +++ b/src/aig/fra/fraHot.c @@ -130,7 +130,7 @@ int Fra_OneHotNodesAreClause( Fra_Sml_t * pSeq, Aig_Obj_t * pObj1, Aig_Obj_t * p ***********************************************************************/ Vec_Int_t * Fra_OneHotCompute( Fra_Man_t * p, Fra_Sml_t * pSim ) { - int fSkipConstEqu = 1; + int fSkipConstEqu = 0; Vec_Int_t * vOneHots; Aig_Obj_t * pObj1, * pObj2; int i, k; diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c index 07044b52..ea17706c 100644 --- a/src/aig/fra/fraInd.c +++ b/src/aig/fra/fraInd.c @@ -471,12 +471,14 @@ clk2 = clock(); if ( p->pPars->fWriteImps && p->vOneHots && Fra_OneHotCount(p, p->vOneHots) ) { extern void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int fCompact ); - char Buffer[500]; + char Buffer[500], * pStart; Aig_Man_t * pNew; pManAigNew = Aig_ManDup( pManAig, 1 ); // pManAigNew->pManExdc = Fra_OneHotCreateExdc( p, p->vOneHots ); pNew = Fra_OneHotCreateExdc( p, p->vOneHots ); - sprintf( Buffer, "%s_care.aig", p->pManAig->pName ); + pStart = Ioa_FileNameGeneric(p->pManAig->pName); + sprintf( Buffer, "%s_care.aig", pStart ); + free( pStart ); printf( "Care one-hotness clauses are written into file \"%s\".\n", Buffer ); Ioa_WriteAiger( pNew, Buffer, 0, 1 ); Aig_ManStop( pNew ); |