summaryrefslogtreecommitdiffstats
path: root/src/aig
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig')
-rw-r--r--src/aig/aig/aigInter.c29
-rw-r--r--src/aig/fra/fraClass.c8
-rw-r--r--src/aig/fra/fraClaus.c13
-rw-r--r--src/aig/fra/fraCore.c4
-rw-r--r--src/aig/fra/fraInd.c10
-rw-r--r--src/aig/ioa/ioa.h1
-rw-r--r--src/aig/ioa/ioaUtil.c35
7 files changed, 67 insertions, 33 deletions
diff --git a/src/aig/aig/aigInter.c b/src/aig/aig/aigInter.c
index b3bc28b2..c939a38c 100644
--- a/src/aig/aig/aigInter.c
+++ b/src/aig/aig/aigInter.c
@@ -26,6 +26,10 @@
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
+extern int timeCnf;
+extern int timeSat;
+extern int timeInt;
+
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
@@ -51,17 +55,20 @@ Aig_Man_t * Aig_ManInter( Aig_Man_t * pManOn, Aig_Man_t * pManOff, int fVerbose
Vec_Int_t * vVarsAB;
Aig_Obj_t * pObj, * pObj2;
int Lits[3], status, i;
- int clk = clock();
+ int clk;
assert( Aig_ManPiNum(pManOn) == Aig_ManPiNum(pManOff) );
+clk = clock();
// derive CNFs
- pCnfOn = Cnf_Derive( pManOn, 0 );
- pCnfOff = Cnf_Derive( pManOff, 0 );
-// pCnfOn = Cnf_DeriveSimple( pManOn, 0 );
-// pCnfOff = Cnf_DeriveSimple( pManOff, 0 );
+// pCnfOn = Cnf_Derive( pManOn, 0 );
+// pCnfOff = Cnf_Derive( pManOff, 0 );
+ pCnfOn = Cnf_DeriveSimple( pManOn, 0 );
+ pCnfOff = Cnf_DeriveSimple( pManOff, 0 );
Cnf_DataLift( pCnfOff, pCnfOn->nVars );
+timeCnf += clock() - clk;
+clk = clock();
// start the solver
pSat = sat_solver_new();
sat_solver_store_alloc( pSat );
@@ -112,10 +119,6 @@ Aig_Man_t * Aig_ManInter( Aig_Man_t * pManOn, Aig_Man_t * pManOff, int fVerbose
Cnf_DataFree( pCnfOn );
Cnf_DataFree( pCnfOff );
sat_solver_store_mark_roots( pSat );
- if ( fVerbose )
- {
- PRT( "Prepare", clock() - clk );
- }
/*
status = sat_solver_simplify(pSat);
@@ -130,12 +133,8 @@ Aig_Man_t * Aig_ManInter( Aig_Man_t * pManOn, Aig_Man_t * pManOff, int fVerbose
*/
// solve the problem
- clk = clock();
status = sat_solver_solve( pSat, NULL, NULL, (sint64)0, (sint64)0, (sint64)0, (sint64)0 );
- if ( fVerbose )
- {
- PRT( "Solving", clock() - clk );
- }
+timeSat += clock() - clk;
if ( status == l_False )
{
pSatCnf = sat_solver_store_release( pSat );
@@ -158,9 +157,11 @@ Aig_Man_t * Aig_ManInter( Aig_Man_t * pManOn, Aig_Man_t * pManOff, int fVerbose
}
// create the resulting manager
+clk = clock();
pManInter = Inta_ManAlloc();
pRes = Inta_ManInterpolate( pManInter, pSatCnf, vVarsAB, fVerbose );
Inta_ManFree( pManInter );
+timeInt += clock() - clk;
Vec_IntFree( vVarsAB );
Sto_ManFree( pSatCnf );
diff --git a/src/aig/fra/fraClass.c b/src/aig/fra/fraClass.c
index 2d03e65d..baae7c3f 100644
--- a/src/aig/fra/fraClass.c
+++ b/src/aig/fra/fraClass.c
@@ -207,7 +207,7 @@ int Fra_ClassesCountPairs( Fra_Cla_t * p )
SeeAlso []
***********************************************************************/
-void Fra_PrintClass( Aig_Obj_t ** pClass )
+void Fra_PrintClass( Fra_Cla_t * p, Aig_Obj_t ** pClass )
{
Aig_Obj_t * pTemp;
int i;
@@ -215,7 +215,7 @@ void Fra_PrintClass( Aig_Obj_t ** pClass )
assert( Fra_ClassObjRepr(pTemp) == pClass[0] );
printf( "{ " );
for ( i = 0; (pTemp = pClass[i]); i++ )
- printf( "%d(%d) ", pTemp->Id, pTemp->Level );
+ printf( "%d(%d,%d) ", pTemp->Id, pTemp->Level, Aig_SupportSize(p->pAig,pTemp) );
printf( "}\n" );
}
@@ -248,12 +248,12 @@ void Fra_ClassesPrint( Fra_Cla_t * p, int fVeryVerbose )
assert( Fra_ClassObjRepr(pObj) == Aig_ManConst1(p->pAig) );
printf( "Constants { " );
Vec_PtrForEachEntry( p->vClasses1, pObj, i )
- printf( "%d ", pObj->Id );
+ printf( "%d(%d,%d) ", pObj->Id, pObj->Level, Aig_SupportSize(p->pAig,pObj) );
printf( "}\n" );
Vec_PtrForEachEntry( p->vClasses, pClass, i )
{
printf( "%3d (%3d) : ", i, Fra_ClassCount(pClass) );
- Fra_PrintClass( pClass );
+ Fra_PrintClass( p, pClass );
}
printf( "\n" );
}
diff --git a/src/aig/fra/fraClaus.c b/src/aig/fra/fraClaus.c
index d95515d5..c9ea4907 100644
--- a/src/aig/fra/fraClaus.c
+++ b/src/aig/fra/fraClaus.c
@@ -1526,11 +1526,11 @@ Aig_Obj_t * Fra_ClausGetLiteral( Clu_Man_t * p, int * pVar2Id, int Lit )
***********************************************************************/
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], * pName;
+ char * pName;
int * pStart, * pVar2Id;
int Beg, End, i, k;
// create mapping from SAT vars to node IDs
@@ -1560,12 +1560,9 @@ void Fra_ClausWriteIndClauses( Clu_Man_t * p )
}
free( pVar2Id );
Aig_ManCleanup( pNew );
- // write the manager into a file
- 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 );
+ pName = Ioa_FileNameGenericAppend( p->pAig->pName, "_care.aig" );
+ printf( "Care one-hotness clauses will be written into file \"%s\".\n", pName );
+ Ioa_WriteAiger( pNew, pName, 0, 1 );
Aig_ManStop( pNew );
}
diff --git a/src/aig/fra/fraCore.c b/src/aig/fra/fraCore.c
index 0a81105b..67940c4f 100644
--- a/src/aig/fra/fraCore.c
+++ b/src/aig/fra/fraCore.c
@@ -328,6 +328,8 @@ void Fra_FraigSweep( Fra_Man_t * p )
// quit if simulation detected a counter-example for a PO
if ( p->pManFraig->pData )
continue;
+// if ( Aig_SupportSize(p->pManAig,pObj) > 16 )
+// continue;
// perform fraiging
if ( p->pPars->nLevelMax && (int)pObj->Level > p->pPars->nLevelMax )
p->pPars->nBTLimitNode = 5;
@@ -381,6 +383,8 @@ clk = clock();
p->nNodesBeg = Aig_ManNodeNum(pManAig);
p->nRegsBeg = Aig_ManRegNum(pManAig);
// perform fraig sweep
+if ( p->pPars->fVerbose )
+Fra_ClassesPrint( p->pCla, 1 );
Fra_FraigSweep( p );
// call back the procedure to check implications
if ( pManAig->pImpFunc )
diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c
index 7e0d080c..18c9ffcc 100644
--- a/src/aig/fra/fraInd.c
+++ b/src/aig/fra/fraInd.c
@@ -560,16 +560,12 @@ 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], * pStart;
Aig_Man_t * pNew;
+ char * pFileName = Ioa_FileNameGenericAppend( p->pManAig->pName, "_care.aig" );
+ printf( "Care one-hotness clauses will be written into file \"%s\".\n", pFileName );
pManAigNew = Aig_ManDup( pManAig, 1 );
-// pManAigNew->pManExdc = Fra_OneHotCreateExdc( p, p->vOneHots );
pNew = Fra_OneHotCreateExdc( p, p->vOneHots );
- 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 );
+ Ioa_WriteAiger( pNew, pFileName, 0, 1 );
Aig_ManStop( pNew );
}
else
diff --git a/src/aig/ioa/ioa.h b/src/aig/ioa/ioa.h
index e697a729..be8594e7 100644
--- a/src/aig/ioa/ioa.h
+++ b/src/aig/ioa/ioa.h
@@ -66,6 +66,7 @@ extern void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fW
/*=== ioaUtil.c =======================================================*/
extern int Ioa_FileSize( char * pFileName );
extern char * Ioa_FileNameGeneric( char * FileName );
+extern char * Ioa_FileNameGenericAppend( char * pBase, char * pSuffix );
extern char * Ioa_TimeStamp();
#ifdef __cplusplus
diff --git a/src/aig/ioa/ioaUtil.c b/src/aig/ioa/ioaUtil.c
index 79dcca1e..6063d8be 100644
--- a/src/aig/ioa/ioaUtil.c
+++ b/src/aig/ioa/ioaUtil.c
@@ -88,6 +88,41 @@ char * Ioa_FileNameGeneric( char * FileName )
/**Function*************************************************************
+ Synopsis [Returns the composite name of the file.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+char * Ioa_FileNameGenericAppend( char * pBase, char * pSuffix )
+{
+ static char Buffer[1000];
+ char * pDot;
+ if ( pBase == NULL )
+ {
+ strcpy( Buffer, pSuffix );
+ return Buffer;
+ }
+ strcpy( Buffer, pBase );
+ pDot = strstr( Buffer, "." );
+ if ( pDot )
+ *pDot = 0;
+ strcat( Buffer, pSuffix );
+ // find the last occurrance of slash
+ for ( pDot = Buffer + strlen(Buffer) - 1; pDot >= Buffer; pDot-- )
+ if (!((*pDot >= '0' && *pDot <= '9') ||
+ (*pDot >= 'a' && *pDot <= 'z') ||
+ (*pDot >= 'A' && *pDot <= 'Z') ||
+ *pDot == '_' || *pDot == '.') )
+ break;
+ return pDot + 1;
+}
+
+/**Function*************************************************************
+
Synopsis [Returns the time stamp.]
Description [The file should be closed.]
generated by cgit v1.2.3 (git 2.25.1) at 2025-08-06 07:32:52 +0000