Skip to content

Commit aaba1b9

Browse files
alanminkoalanminko
committed
Experiments with mapping.
1 parent d55735d commit aaba1b9

File tree

3 files changed

+260
-75
lines changed

3 files changed

+260
-75
lines changed

‎src/aig/gia/giaSatLut.c‎

Lines changed: 198 additions & 63 deletions
Original file line numberDiff line numberDiff line change
@@ -1234,7 +1234,7 @@ void Gia_ManLutSat( Gia_Man_t * pGia, int LutSize, int nNumber, int nImproves, i
12341234
SeeAlso []
12351235
12361236
***********************************************************************/
1237-
Vec_Int_t * Gia_RunKadical( char * pFileNameIn, char * pFileNameOut, int nBTLimit, int TimeOut, int fVerbose )
1237+
Vec_Int_t * Gia_RunKadical( char * pFileNameIn, char * pFileNameOut, int nBTLimit, int TimeOut, int fVerbose, int * pStatus )
12381238
{
12391239
extern Vec_Int_t * Exa4_ManParse( char *pFileName );
12401240
int fVerboseSolver = 0;
@@ -1271,11 +1271,11 @@ Vec_Int_t * Gia_RunKadical( char * pFileNameIn, char * pFileNameOut, int nBTLimi
12711271
if ( fVerbose )
12721272
{
12731273
if ( vRes )
1274-
printf( "The problem has a solution. " );
1274+
printf( "The problem has a solution. " ), *pStatus = 0;
12751275
else if ( vRes == NULL && TimeOut == 0 )
1276-
printf( "The problem has no solution. " );
1276+
printf( "The problem has no solution. " ), *pStatus = 1;
12771277
else if ( vRes == NULL )
1278-
printf( "The problem has no solution or reached a resource limit after %d sec. ", TimeOut );
1278+
printf( "The problem has no solution or reached a resource limit after %d sec. ", TimeOut ), *pStatus = -1;
12791279
Abc_PrintTime( 1, "SAT solver time", Abc_Clock() - clkTotal );
12801280
}
12811281
return vRes;
@@ -1536,10 +1536,41 @@ int Gia_ManDumpCnf( char * pFileName, Vec_Str_t * vStr, int nVars )
15361536
fclose( pFile );
15371537
return 1;
15381538
}
1539-
int Gia_ManSimpleMapping( Gia_Man_t * p, int nBound, int nBTLimit, int nTimeout, int fVerbose )
1539+
int Gia_ManDumpCnf2( Vec_Str_t * vStr, int nVars, int argc, char ** argv, abctime Time, int Status )
15401540
{
1541-
char * pFileNameI = (char *)"__temp__.cnf";
1542-
char * pFileNameO = (char *)"__temp__.out";
1541+
Vec_Str_t * vFileName = Vec_StrAlloc( 100 ); int c;
1542+
Vec_StrPrintF( vFileName, "%s", argv[0] );
1543+
for ( c = 1; c < argc; c++ )
1544+
Vec_StrPrintF( vFileName, "_%s", argv[c] + (argv[c][0] == '-') );
1545+
Vec_StrPrintF( vFileName, ".cnf" );
1546+
Vec_StrPush( vFileName, '\0' );
1547+
FILE * pFile = fopen( Vec_StrArray(vFileName), "wb" );
1548+
if ( pFile == NULL ) { printf( "Cannot open output file \"%s\".\n", Vec_StrArray(vFileName) ); Vec_StrFree(vFileName); return 0; }
1549+
Vec_StrFree(vFileName);
1550+
fprintf( pFile, "c ABC command line: \"" );
1551+
fprintf( pFile, "%s", argv[0] );
1552+
for ( c = 1; c < argc; c++ )
1553+
fprintf( pFile, " %s", argv[c] );
1554+
fprintf( pFile, "\" " );
1555+
if ( Status == 1 )
1556+
fprintf( pFile, "UNSAT after " );
1557+
if ( Status == 0 )
1558+
fprintf( pFile, "SAT after " );
1559+
if ( Status == -1 )
1560+
fprintf( pFile, "UNDECIDED after " );
1561+
fprintf( pFile, "%.2f sec by CaDiCal on ", 1.0*((double)(Time))/((double)CLOCKS_PER_SEC) );
1562+
fprintf( pFile, "%s\n", Gia_TimeStamp() );
1563+
fprintf( pFile, "p knf %d %d\n%s\n", nVars, Vec_StrCountEntry(vStr, '\n'), Vec_StrArray(vStr) );
1564+
fclose( pFile );
1565+
return 1;
1566+
}
1567+
int Gia_ManSimpleMapping( Gia_Man_t * p, int nBound, int nBTLimit, int nTimeout, int fVerbose, int fKeepFile, int argc, char ** argv )
1568+
{
1569+
abctime clkStart = Abc_Clock();
1570+
srand(time(NULL));
1571+
int Status, Rand = ((((unsigned)rand()) << 12) ^ ((unsigned)rand())) & 0xFFFFFF;
1572+
char pFileNameI[32]; sprintf( pFileNameI, "_%06x_.cnf", Rand );
1573+
char pFileNameO[32]; sprintf( pFileNameO, "_%06x_.out", Rand );
15431574
if ( nBound == 0 )
15441575
nBound = 5 * Gia_ManAndNum(p);
15451576
Vec_Str_t * vStr = Gia_ManSimpleCnf( p, nBound/2 );
@@ -1551,12 +1582,11 @@ int Gia_ManSimpleMapping( Gia_Man_t * p, int nBound, int nBTLimit, int nTimeout,
15511582
if ( fVerbose )
15521583
printf( "SAT variables = %d. SAT clauses = %d. Cardinality bound = %d. Conflict limit = %d. Timeout = %d.\n",
15531584
nVars, Vec_StrCountEntry(vStr, '\n'), nBound, nBTLimit, nTimeout );
1554-
//char pFileName[100]; sprintf( pFileName, "temp%02d.cnf", nBound/2 );
1555-
//Gia_ManDumpCnf( pFileName, vStr, nVars );
1556-
Vec_StrFree( vStr );
1557-
Vec_Int_t * vRes = Gia_RunKadical( pFileNameI, pFileNameO, nBTLimit, nTimeout, 1 );
1585+
Vec_Int_t * vRes = Gia_RunKadical( pFileNameI, pFileNameO, nBTLimit, nTimeout, 1, &Status );
15581586
unlink( pFileNameI );
15591587
//unlink( pFileNameO );
1588+
if ( fKeepFile ) Gia_ManDumpCnf2( vStr, nVars, argc, argv, Abc_Clock() - clkStart, Status );
1589+
Vec_StrFree( vStr );
15601590
if ( vRes == NULL )
15611591
return 0;
15621592
Vec_IntFreeP( &p->vCellMapping );
@@ -1565,6 +1595,7 @@ int Gia_ManSimpleMapping( Gia_Man_t * p, int nBound, int nBTLimit, int nTimeout,
15651595
if ( fVerbose ) Gia_ManSimplePrintMapping( vRes, Gia_ManCiNum(p) );
15661596
p->vCellMapping = Gia_ManDeriveSimpleMapping( p, vRes );
15671597
Vec_IntFree( vRes );
1598+
Abc_PrintTime( 0, "Total time", Abc_Clock() - clkStart );
15681599
return 1;
15691600
}
15701601

@@ -1647,43 +1678,7 @@ int Gia_KSatFindFan( int * pMap, int i, int f, Vec_Int_t * vRes )
16471678
return -1;
16481679
}
16491680

1650-
Gia_Man_t * Gia_ManDeriveKSatMapping( Vec_Int_t * vRes, int * pMap, int nIns, int nNodes, int fVerbose )
1651-
{
1652-
Gia_Man_t * pNew = Gia_ManStart( nIns + nNodes + 2 );
1653-
pNew->pName = Abc_UtilStrsav( "test" );
1654-
int i, nSave = 0, pCopy[256] = {0};
1655-
for ( i = 1; i <= nIns; i++ )
1656-
pCopy[i] = Gia_ManAppendCi( pNew );
1657-
for ( i = nIns; i < nIns+nNodes; i++ ) {
1658-
int iFan0 = Gia_KSatFindFan( pMap, i, 0, vRes );
1659-
int iFan1 = Gia_KSatFindFan( pMap, i, 1, vRes );
1660-
if ( iFan0 == iFan1 )
1661-
pCopy[i+1] = pCopy[iFan0+1];
1662-
else if ( Gia_KSatValAnd(pMap, i, vRes) )
1663-
pCopy[i+1] = Gia_ManAppendAnd( pNew, pCopy[iFan0+1], pCopy[iFan1+1] );
1664-
else
1665-
pCopy[i+1] = Gia_ManAppendOr( pNew, pCopy[iFan0+1], pCopy[iFan1+1] );
1666-
pCopy[i+1] = Abc_LitNotCond( pCopy[i+1], Gia_KSatValInv(pMap, i, vRes) );
1667-
if ( fVerbose ) {
1668-
printf( "%d = ", i );
1669-
if ( iFan0 == iFan1 )
1670-
printf( "INV( %d )\n", iFan0 );
1671-
else if ( Gia_KSatValAnd(pMap, i, vRes) )
1672-
printf( "%sAND( %d, %d )\n", Gia_KSatValInv(pMap, i, vRes) ? "N":"", iFan0, iFan1 );
1673-
else
1674-
printf( "%sOR( %d, %d )\n", Gia_KSatValInv(pMap, i, vRes) ? "N":"", iFan0, iFan1 );
1675-
nSave += (iFan0 == iFan1) || !Gia_KSatValInv(pMap, i, vRes);
1676-
if ( i == nIns+nNodes-1 ) {
1677-
printf( "CO = %d\n", nIns+nNodes-1 );
1678-
printf( "Solution cost = %d\n", 2*(2*nNodes - nSave) );
1679-
}
1680-
}
1681-
}
1682-
Gia_ManAppendCo( pNew, pCopy[nIns+nNodes] );
1683-
return pNew;
1684-
}
1685-
1686-
Vec_Str_t * Gia_ManKSatCnf( int * pMap, int nIns, int nNodes, int nBound )
1681+
Vec_Str_t * Gia_ManKSatCnf( int * pMap, int nIns, int nNodes, int nBound, int fMultiLevel )
16871682
{
16881683
Vec_Str_t * vStr = Vec_StrAlloc( 10000 );
16891684
int i, j, m, n, f, c, a, nLits = 0, pLits[256] = {0};
@@ -1764,12 +1759,14 @@ Vec_Str_t * Gia_ManKSatCnf( int * pMap, int nIns, int nNodes, int nBound )
17641759
pLits[1] = Abc_Var2Lit( Gia_KSatVarInv(pMap, n), 0 );
17651760
Gia_SatDumpClause( vStr, pLits, 2 );
17661761
// if inv is not used, its fanins' invs are used
1767-
pLits[0] = Abc_Var2Lit( Gia_KSatVarInv(pMap, n), 0 );
1768-
for ( i = nIns; i < n; i++ )
1769-
for ( f = 0; f < 2; f++ ) {
1770-
pLits[1] = Abc_Var2Lit( Gia_KSatVarFan(pMap, n, f, i), 1 );
1771-
pLits[2] = Abc_Var2Lit( Gia_KSatVarInv(pMap, i), 0 );
1772-
Gia_SatDumpClause( vStr, pLits, 3 );
1762+
if ( !fMultiLevel ) {
1763+
pLits[0] = Abc_Var2Lit( Gia_KSatVarInv(pMap, n), 0 );
1764+
for ( i = nIns; i < n; i++ )
1765+
for ( f = 0; f < 2; f++ ) {
1766+
pLits[1] = Abc_Var2Lit( Gia_KSatVarFan(pMap, n, f, i), 1 );
1767+
pLits[2] = Abc_Var2Lit( Gia_KSatVarInv(pMap, i), 0 );
1768+
Gia_SatDumpClause( vStr, pLits, 3 );
1769+
}
17731770
}
17741771
}
17751772
// the last one always uses inverter
@@ -1848,6 +1845,141 @@ Vec_Str_t * Gia_ManKSatCnf( int * pMap, int nIns, int nNodes, int nBound )
18481845
return vStr;
18491846
}
18501847

1848+
1849+
typedef enum {
1850+
GIA_GATE2_ZERO, // 0:
1851+
GIA_GATE2_ONE, // 1:
1852+
GIA_GATE2_BUF, // 2:
1853+
GIA_GATE2_INV, // 3:
1854+
GIA_GATE2_NAN2, // 4:
1855+
GIA_GATE2_NOR2, // 5:
1856+
GIA_GATE2_AOI21, // 6:
1857+
GIA_GATE2_NAN3, // 7:
1858+
GIA_GATE2_NOR3, // 8:
1859+
GIA_GATE2_OAI21, // 9:
1860+
GIA_GATE2_NOR4, // 10:
1861+
GIA_GATE2_AOI211, // 11:
1862+
GIA_GATE2_AOI22, // 12:
1863+
GIA_GATE2_NAN4, // 13:
1864+
GIA_GATE2_OAI211, // 14:
1865+
GIA_GATE2_OAI22, // 15:
1866+
GIA_GATE2_VOID // 16: unused value
1867+
} Gia_ManGate2_t;
1868+
1869+
Vec_Int_t * Gia_ManDeriveKSatMappingArray( Gia_Man_t * p, Vec_Int_t * vRes )
1870+
{
1871+
Vec_Int_t * vMapping = Vec_IntStart( 2*Gia_ManObjNum(p) );
1872+
int i, Id; Gia_Obj_t * pObj;
1873+
Gia_ManForEachCiId( p, Id, i )
1874+
if ( Vec_IntEntry(vRes, Id) )
1875+
Vec_IntWriteEntry( vMapping, Abc_Var2Lit(Id, 1), -1 );
1876+
Gia_ManForEachAnd( p, pObj, i ) {
1877+
assert( Vec_IntEntry(vRes, i) > 0 );
1878+
if ( (Vec_IntEntry(vRes, i) & 2) == 0 ) {
1879+
assert( (Vec_IntEntry(vRes, i) & 1) == 0 );
1880+
continue;
1881+
}
1882+
Gia_Obj_t * pFans[2] = { Gia_ObjFanin0(pObj), Gia_ObjFanin1(pObj) };
1883+
int fComp = ((Vec_IntEntry(vRes, i) >> 2) & 1) != 0;
1884+
int fFan0 = ((Vec_IntEntry(vRes, Gia_ObjFaninId0(pObj, i)) >> 1) & 1) == 0 && Gia_ObjIsAnd(pFans[0]);
1885+
int fFan1 = ((Vec_IntEntry(vRes, Gia_ObjFaninId1(pObj, i)) >> 1) & 1) == 0 && Gia_ObjIsAnd(pFans[1]);
1886+
if ( Vec_IntEntry(vRes, i) & 1 )
1887+
Vec_IntWriteEntry( vMapping, Abc_Var2Lit(i, !fComp), -1 );
1888+
Vec_IntWriteEntry( vMapping, Abc_Var2Lit(i, fComp), Vec_IntSize(vMapping) );
1889+
if ( fFan0 && fFan1 ) {
1890+
Vec_IntPush( vMapping, 4 );
1891+
if ( !Gia_ObjFaninC0(pObj) && Gia_ObjFaninC1(pObj) ) {
1892+
Vec_IntPush( vMapping, Abc_Var2Lit(Gia_ObjFaninId0p(p, pFans[1]), !(fComp ^ Gia_ObjFaninC1(pObj) ^ Gia_ObjFaninC0(pFans[1]))) );
1893+
Vec_IntPush( vMapping, Abc_Var2Lit(Gia_ObjFaninId1p(p, pFans[1]), !(fComp ^ Gia_ObjFaninC1(pObj) ^ Gia_ObjFaninC1(pFans[1]))) );
1894+
Vec_IntPush( vMapping, Abc_Var2Lit(Gia_ObjFaninId0p(p, pFans[0]), !(fComp ^ Gia_ObjFaninC0(pObj) ^ Gia_ObjFaninC0(pFans[0]))) );
1895+
Vec_IntPush( vMapping, Abc_Var2Lit(Gia_ObjFaninId1p(p, pFans[0]), !(fComp ^ Gia_ObjFaninC0(pObj) ^ Gia_ObjFaninC1(pFans[0]))) );
1896+
}
1897+
else {
1898+
Vec_IntPush( vMapping, Abc_Var2Lit(Gia_ObjFaninId0p(p, pFans[0]), !(fComp ^ Gia_ObjFaninC0(pObj) ^ Gia_ObjFaninC0(pFans[0]))) );
1899+
Vec_IntPush( vMapping, Abc_Var2Lit(Gia_ObjFaninId1p(p, pFans[0]), !(fComp ^ Gia_ObjFaninC0(pObj) ^ Gia_ObjFaninC1(pFans[0]))) );
1900+
Vec_IntPush( vMapping, Abc_Var2Lit(Gia_ObjFaninId0p(p, pFans[1]), !(fComp ^ Gia_ObjFaninC1(pObj) ^ Gia_ObjFaninC0(pFans[1]))) );
1901+
Vec_IntPush( vMapping, Abc_Var2Lit(Gia_ObjFaninId1p(p, pFans[1]), !(fComp ^ Gia_ObjFaninC1(pObj) ^ Gia_ObjFaninC1(pFans[1]))) );
1902+
}
1903+
if ( Gia_ObjFaninC0(pObj) && Gia_ObjFaninC1(pObj) )
1904+
Vec_IntPush( vMapping, fComp ? GIA_GATE2_OAI22 : GIA_GATE2_AOI22 );
1905+
else if ( !Gia_ObjFaninC0(pObj) && !Gia_ObjFaninC1(pObj) )
1906+
Vec_IntPush( vMapping, fComp ? GIA_GATE2_NAN4 : GIA_GATE2_NOR4 );
1907+
else
1908+
Vec_IntPush( vMapping, fComp ? GIA_GATE2_OAI211 : GIA_GATE2_AOI211 );
1909+
} else if ( fFan0 ) {
1910+
Vec_IntPush( vMapping, 3 );
1911+
Vec_IntPush( vMapping, Abc_Var2Lit(Gia_ObjFaninId0p(p, pFans[0]), !(fComp ^ Gia_ObjFaninC0(pObj) ^ Gia_ObjFaninC0(pFans[0]))) );
1912+
Vec_IntPush( vMapping, Abc_Var2Lit(Gia_ObjFaninId1p(p, pFans[0]), !(fComp ^ Gia_ObjFaninC0(pObj) ^ Gia_ObjFaninC1(pFans[0]))) );
1913+
Vec_IntPush( vMapping, Abc_Var2Lit(Gia_ObjFaninId1p(p, pObj), !(fComp ^ Gia_ObjFaninC1(pObj))) );
1914+
if ( Gia_ObjFaninC0(pObj) )
1915+
Vec_IntPush( vMapping, fComp ? GIA_GATE2_OAI21 : GIA_GATE2_AOI21 );
1916+
else
1917+
Vec_IntPush( vMapping, fComp ? GIA_GATE2_NAN3 : GIA_GATE2_NOR3 );
1918+
} else if ( fFan1 ) {
1919+
Vec_IntPush( vMapping, 3 );
1920+
Vec_IntPush( vMapping, Abc_Var2Lit(Gia_ObjFaninId0p(p, pFans[1]), !(fComp ^ Gia_ObjFaninC1(pObj) ^ Gia_ObjFaninC0(pFans[1]))) );
1921+
Vec_IntPush( vMapping, Abc_Var2Lit(Gia_ObjFaninId1p(p, pFans[1]), !(fComp ^ Gia_ObjFaninC1(pObj) ^ Gia_ObjFaninC1(pFans[1]))) );
1922+
Vec_IntPush( vMapping, Abc_Var2Lit(Gia_ObjFaninId0p(p, pObj), !(fComp ^ Gia_ObjFaninC0(pObj))) );
1923+
if ( Gia_ObjFaninC1(pObj) )
1924+
Vec_IntPush( vMapping, fComp ? GIA_GATE2_OAI21 : GIA_GATE2_AOI21 );
1925+
else
1926+
Vec_IntPush( vMapping, fComp ? GIA_GATE2_NAN3 : GIA_GATE2_NOR3 );
1927+
} else {
1928+
Vec_IntPush( vMapping, 2 );
1929+
Vec_IntPush( vMapping, Abc_Var2Lit(Gia_ObjFaninId0p(p, pObj), !(fComp ^ Gia_ObjFaninC0(pObj))) );
1930+
Vec_IntPush( vMapping, Abc_Var2Lit(Gia_ObjFaninId1p(p, pObj), !(fComp ^ Gia_ObjFaninC1(pObj))) );
1931+
Vec_IntPush( vMapping, fComp ? GIA_GATE2_NAN2 : GIA_GATE2_NOR2 );
1932+
}
1933+
}
1934+
return vMapping;
1935+
}
1936+
1937+
Gia_Man_t * Gia_ManDeriveKSatMapping( Vec_Int_t * vRes, int * pMap, int nIns, int nNodes, int fVerbose )
1938+
{
1939+
Vec_Int_t * vGuide = Vec_IntStart( 1000 );
1940+
Gia_Man_t * pNew = Gia_ManStart( nIns + nNodes + 2 );
1941+
pNew->pName = Abc_UtilStrsav( "test" );
1942+
int i, nSave = 0, pCopy[256] = {0};
1943+
for ( i = 1; i <= nIns; i++ )
1944+
pCopy[i] = Gia_ManAppendCi( pNew );
1945+
for ( i = nIns; i < nIns+nNodes; i++ ) {
1946+
int iFan0 = Gia_KSatFindFan( pMap, i, 0, vRes );
1947+
int iFan1 = Gia_KSatFindFan( pMap, i, 1, vRes );
1948+
if ( iFan0 == iFan1 )
1949+
pCopy[i+1] = pCopy[iFan0+1];
1950+
else if ( Gia_KSatValAnd(pMap, i, vRes) )
1951+
pCopy[i+1] = Gia_ManAppendAnd( pNew, pCopy[iFan0+1], pCopy[iFan1+1] );
1952+
else
1953+
pCopy[i+1] = Gia_ManAppendOr( pNew, pCopy[iFan0+1], pCopy[iFan1+1] );
1954+
pCopy[i+1] = Abc_LitNotCond( pCopy[i+1], Gia_KSatValInv(pMap, i, vRes) );
1955+
if ( iFan0 == iFan1 )
1956+
*Vec_IntEntryP(vGuide, Abc_Lit2Var(pCopy[i+1])) ^= 1;
1957+
else if ( Gia_KSatValAnd(pMap, i, vRes) )
1958+
*Vec_IntEntryP(vGuide, Abc_Lit2Var(pCopy[i+1])) ^= 4 | (2*Gia_KSatValInv(pMap, i, vRes));
1959+
else
1960+
*Vec_IntEntryP(vGuide, Abc_Lit2Var(pCopy[i+1])) ^= 8 | (2*Gia_KSatValInv(pMap, i, vRes));
1961+
if ( fVerbose ) {
1962+
if ( i == nIns+nNodes-1 )
1963+
printf( " F = " );
1964+
else
1965+
printf( "%2d = ", i );
1966+
if ( iFan0 == iFan1 )
1967+
printf( "INV( %d )\n", iFan0 );
1968+
else if ( Gia_KSatValAnd(pMap, i, vRes) )
1969+
printf( "%sAND( %d, %d )\n", Gia_KSatValInv(pMap, i, vRes) ? "N":"", iFan0, iFan1 );
1970+
else
1971+
printf( "%sOR( %d, %d )\n", Gia_KSatValInv(pMap, i, vRes) ? "N":"", iFan0, iFan1 );
1972+
nSave += (iFan0 == iFan1) || !Gia_KSatValInv(pMap, i, vRes);
1973+
if ( i == nIns+nNodes-1 )
1974+
printf( "Solution cost = %d\n", 2*(2*nNodes - nSave) );
1975+
}
1976+
}
1977+
Gia_ManAppendCo( pNew, pCopy[nIns+nNodes] );
1978+
//pNew->vCellMapping = Gia_ManDeriveKSatMappingArray( pNew, vGuide );
1979+
Vec_IntFree( vGuide );
1980+
return pNew;
1981+
}
1982+
18511983
word Gia_ManGetTruth( Gia_Man_t * p )
18521984
{
18531985
Gia_Obj_t * pObj; int i, Id;
@@ -1861,31 +1993,34 @@ word Gia_ManGetTruth( Gia_Man_t * p )
18611993
return Const[Gia_ObjFaninC0(pObj)] ^ pFuncs[Gia_ObjFaninId0p(p, pObj)];
18621994
}
18631995

1864-
Gia_Man_t * Gia_ManKSatMapping( word Truth, int nIns, int nNodes, int nBound, int nBTLimit, int nTimeout, int fVerbose )
1996+
Gia_Man_t * Gia_ManKSatMapping( word Truth, int nIns, int nNodes, int nBound, int fMultiLevel, int nBTLimit, int nTimeout, int fVerbose, int fKeepFile, int argc, char ** argv )
18651997
{
1998+
abctime clkStart = Abc_Clock();
18661999
Gia_Man_t * pNew = NULL;
1867-
char * pFileNameI = (char *)"__temp__.cnf";
1868-
char * pFileNameO = (char *)"__temp__.out";
2000+
srand(time(NULL));
2001+
int Status, Rand = ((((unsigned)rand()) << 12) ^ ((unsigned)rand())) & 0xFFFFFF;
2002+
char pFileNameI[32]; sprintf( pFileNameI, "_%06x_.cnf", Rand );
2003+
char pFileNameO[32]; sprintf( pFileNameO, "_%06x_.out", Rand );
18692004
int nVars = 0, * pMap = Gia_KSatMapInit( nIns, nNodes, Truth, &nVars );
1870-
Vec_Str_t * vStr = Gia_ManKSatCnf( pMap, nIns, nNodes, nBound/2 );
2005+
Vec_Str_t * vStr = Gia_ManKSatCnf( pMap, nIns, nNodes, nBound/2, fMultiLevel );
18712006
if ( !Gia_ManDumpCnf(pFileNameI, vStr, nVars) ) {
18722007
Vec_StrFree( vStr );
18732008
return NULL;
18742009
}
18752010
if ( fVerbose )
18762011
printf( "Vars = %d. Nodes = %d. Cardinality bound = %d. SAT vars = %d. SAT clauses = %d. Conflict limit = %d. Timeout = %d.\n",
18772012
nIns, nNodes, nBound, nVars, Vec_StrCountEntry(vStr, '\n'), nBTLimit, nTimeout );
1878-
//char pFileName[100]; sprintf( pFileName, "temp%02d.cnf", nBound/2 );
1879-
//Gia_ManDumpCnf( pFileName, vStr, nVars );
1880-
Vec_StrFree( vStr );
1881-
Vec_Int_t * vRes = Gia_RunKadical( pFileNameI, pFileNameO, nBTLimit, nTimeout, 1 );
2013+
Vec_Int_t * vRes = Gia_RunKadical( pFileNameI, pFileNameO, nBTLimit, nTimeout, 1, &Status );
18822014
unlink( pFileNameI );
18832015
//unlink( pFileNameO );
2016+
if ( fKeepFile ) Gia_ManDumpCnf2( vStr, nVars, argc, argv, Abc_Clock() - clkStart, Status );
2017+
Vec_StrFree( vStr );
18842018
if ( vRes == NULL )
18852019
return 0;
18862020
Vec_IntDrop( vRes, 0 );
18872021
pNew = Gia_ManDeriveKSatMapping( vRes, pMap, nIns, nNodes, fVerbose );
1888-
printf( "Verification %s.\n", Truth == Gia_ManGetTruth(pNew) ? "passed" : "failed" );
2022+
printf( "Verification %s. ", Truth == Gia_ManGetTruth(pNew) ? "passed" : "failed" );
2023+
Abc_PrintTime( 0, "Total time", Abc_Clock() - clkStart );
18892024
Vec_IntFree( vRes );
18902025
ABC_FREE( pMap );
18912026
return pNew;

0 commit comments

Comments
 (0)