Skip to content

Commit 38ba7d7

Browse files
alanminkoalanminko
committed
Experiment with mapping.
1 parent f058e15 commit 38ba7d7

File tree

3 files changed

+456
-2
lines changed

3 files changed

+456
-2
lines changed

‎src/aig/gia/giaSatLut.c‎

Lines changed: 331 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -25,6 +25,12 @@
2525
#include "map/scl/sclCon.h"
2626
#include "misc/vec/vecHsh.h"
2727

28+
#ifdef _MSC_VER
29+
#define unlink _unlink
30+
#else
31+
#include <unistd.h>
32+
#endif
33+
2834
ABC_NAMESPACE_IMPL_START
2935

3036

@@ -1216,6 +1222,331 @@ void Gia_ManLutSat( Gia_Man_t * pGia, int LutSize, int nNumber, int nImproves, i
12161222
Vec_IntFreeP( &pGia->vPacking );
12171223
}
12181224

1225+
/**Function*************************************************************
1226+
1227+
Synopsis []
1228+
1229+
Description []
1230+
1231+
SideEffects []
1232+
1233+
SeeAlso []
1234+
1235+
***********************************************************************/
1236+
Vec_Int_t * Gia_RunKadical( char * pFileNameIn, char * pFileNameOut, int TimeOut, int fVerbose )
1237+
{
1238+
extern Vec_Int_t * Exa4_ManParse( char *pFileName );
1239+
int fVerboseSolver = 0;
1240+
abctime clkTotal = Abc_Clock();
1241+
Vec_Int_t * vRes = NULL;
1242+
#ifdef _WIN32
1243+
char * pKadical = "kadical.exe";
1244+
#else
1245+
char * pKadical = "kadical";
1246+
#endif
1247+
char Command[1000], * pCommand = (char *)&Command;
1248+
if ( TimeOut )
1249+
sprintf( pCommand, "%s -t %d %s %s > %s", pKadical, TimeOut, fVerboseSolver ? "": "-q", pFileNameIn, pFileNameOut );
1250+
else
1251+
sprintf( pCommand, "%s %s %s > %s", pKadical, fVerboseSolver ? "": "-q", pFileNameIn, pFileNameOut );
1252+
#ifdef __wasm
1253+
if ( 1 )
1254+
#else
1255+
if ( system( pCommand ) == -1 )
1256+
#endif
1257+
{
1258+
fprintf( stdout, "Command \"%s\" did not succeed.\n", pCommand );
1259+
return 0;
1260+
}
1261+
vRes = Exa4_ManParse( pFileNameOut );
1262+
if ( fVerbose )
1263+
{
1264+
if ( vRes )
1265+
printf( "The problem has a solution. " );
1266+
else if ( vRes == NULL && TimeOut == 0 )
1267+
printf( "The problem has no solution. " );
1268+
else if ( vRes == NULL )
1269+
printf( "The problem has no solution or timed out after %d sec. ", TimeOut );
1270+
Abc_PrintTime( 1, "SAT solver time", Abc_Clock() - clkTotal );
1271+
}
1272+
return vRes;
1273+
}
1274+
1275+
/**Function*************************************************************
1276+
1277+
Synopsis []
1278+
1279+
Description []
1280+
1281+
SideEffects []
1282+
1283+
SeeAlso []
1284+
1285+
***********************************************************************/
1286+
int Gia_SatVarReqPos( int i ) { return i*7+0; } // p
1287+
int Gia_SatVarReqNeg( int i ) { return i*7+1; } // n
1288+
int Gia_SatVarAckPos( int i ) { return i*7+2; } // P
1289+
int Gia_SatVarAckNeg( int i ) { return i*7+3; } // N
1290+
int Gia_SatVarInv ( int i ) { return i*7+4; } // i
1291+
int Gia_SatVarFan0 ( int i ) { return i*7+5; } // 0
1292+
int Gia_SatVarFan1 ( int i ) { return i*7+6; } // 1
1293+
1294+
int Gia_SatValReqPos( Vec_Int_t * p, int i ) { return Vec_IntEntry(p, i*7+0); } // p
1295+
int Gia_SatValReqNeg( Vec_Int_t * p, int i ) { return Vec_IntEntry(p, i*7+1); } // n
1296+
int Gia_SatValAckPos( Vec_Int_t * p, int i ) { return Vec_IntEntry(p, i*7+2); } // P
1297+
int Gia_SatValAckNeg( Vec_Int_t * p, int i ) { return Vec_IntEntry(p, i*7+3); } // N
1298+
int Gia_SatValInv ( Vec_Int_t * p, int i ) { return Vec_IntEntry(p, i*7+4); } // i
1299+
int Gia_SatValFan0 ( Vec_Int_t * p, int i ) { return Vec_IntEntry(p, i*7+5); } // 0
1300+
int Gia_SatValFan1 ( Vec_Int_t * p, int i ) { return Vec_IntEntry(p, i*7+6); } // 1
1301+
1302+
void Gia_SatDumpClause( Vec_Str_t * vStr, int * pLits, int nLits )
1303+
{
1304+
for ( int i = 0; i < nLits; i++ )
1305+
Vec_StrPrintF( vStr, "%d ", Abc_LitIsCompl(pLits[i]) ? -Abc_Lit2Var(pLits[i])-1 : Abc_Lit2Var(pLits[i])+1 );
1306+
Vec_StrPrintF( vStr, "0\n" );
1307+
}
1308+
void Gia_SatDumpLiteral( Vec_Str_t * vStr, int Lit )
1309+
{
1310+
Gia_SatDumpClause( vStr, &Lit, 1 );
1311+
}
1312+
void Gia_SatDumpKlause( Vec_Str_t * vStr, int nIns, int nAnds, int nBound )
1313+
{
1314+
int i, nVars = nIns + 7*nAnds;
1315+
Vec_StrPrintF( vStr, "k %d ", nVars - nBound );
1316+
// counting primary inputs: n
1317+
for ( i = 0; i < nIns; i++ )
1318+
Vec_StrPrintF( vStr, "-%d ", Gia_SatVarReqNeg(1+i)+1 );
1319+
// counting internal nodes: p, n, P, N, i, 0, 1
1320+
for ( i = 0; i < 7*nAnds; i++ )
1321+
Vec_StrPrintF( vStr, "-%d ", (1+nIns)*7+i+1 );
1322+
Vec_StrPrintF( vStr, "0\n" );
1323+
}
1324+
1325+
Vec_Str_t * Gia_ManSimpleCnf( Gia_Man_t * p, int nBound )
1326+
{
1327+
Vec_Str_t * vStr = Vec_StrAlloc( 10000 );
1328+
Gia_SatDumpKlause( vStr, Gia_ManCiNum(p), Gia_ManAndNum(p), nBound );
1329+
int i, n, m, Id, pLits[4]; Gia_Obj_t * pObj;
1330+
for ( n = 0; n < 7; n++ )
1331+
Gia_SatDumpLiteral( vStr, Abc_Var2Lit(n, 1) );
1332+
// acknowledge positive PI literals
1333+
Gia_ManForEachCiId( p, Id, i )
1334+
for ( n = 0; n < 7; n++ ) if ( n != 1 )
1335+
Gia_SatDumpLiteral( vStr, Abc_Var2Lit(Gia_SatVarReqPos(Id)+n, n>0) );
1336+
// require driving PO literals
1337+
Gia_ManForEachCo( p, pObj, i )
1338+
Gia_SatDumpLiteral( vStr, Abc_Var2Lit( Gia_SatVarReqPos(Gia_ObjFaninId0p(p, pObj)) + Gia_ObjFaninC0(pObj), 0 ) );
1339+
// internal nodes
1340+
Gia_ManForEachAnd( p, pObj, i ) {
1341+
int fCompl[2] = { Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj) };
1342+
int iFans[2] = { Gia_ObjFaninId0(pObj, i), Gia_ObjFaninId1(pObj, i) };
1343+
Gia_Obj_t * pFans[2] = { Gia_ObjFanin0(pObj), Gia_ObjFanin1(pObj) };
1344+
// require inverter: p & !n & N -> i, n & !p & P -> i
1345+
for ( n = 0; n < 2; n++ ) {
1346+
pLits[0] = Abc_Var2Lit( Gia_SatVarReqPos(i)+n, 1 );
1347+
pLits[1] = Abc_Var2Lit( Gia_SatVarReqNeg(i)-n, 0 );
1348+
pLits[2] = Abc_Var2Lit( Gia_SatVarAckNeg(i)-n, 1 );
1349+
pLits[3] = Abc_Var2Lit( Gia_SatVarInv (i), 0 );
1350+
Gia_SatDumpClause( vStr, pLits, 4 );
1351+
}
1352+
// exclusive acknowledge: !P + !N
1353+
pLits[0] = Abc_Var2Lit( Gia_SatVarAckPos(i), 1 );
1354+
pLits[1] = Abc_Var2Lit( Gia_SatVarAckNeg(i), 1 );
1355+
Gia_SatDumpClause( vStr, pLits, 2 );
1356+
// required acknowledge: p -> P + N, n -> P + N
1357+
pLits[1] = Abc_Var2Lit( Gia_SatVarAckPos(i), 0 );
1358+
pLits[2] = Abc_Var2Lit( Gia_SatVarAckNeg(i), 0 );
1359+
pLits[0] = Abc_Var2Lit( Gia_SatVarReqPos(i), 1 );
1360+
Gia_SatDumpClause( vStr, pLits, 3 );
1361+
pLits[0] = Abc_Var2Lit( Gia_SatVarReqNeg(i), 1 );
1362+
Gia_SatDumpClause( vStr, pLits, 3 );
1363+
// forbid acknowledge: !p & !n -> !P, !p & !n -> !N
1364+
pLits[0] = Abc_Var2Lit( Gia_SatVarReqPos(i), 0 );
1365+
pLits[1] = Abc_Var2Lit( Gia_SatVarReqNeg(i), 0 );
1366+
pLits[2] = Abc_Var2Lit( Gia_SatVarAckPos(i), 1 );
1367+
Gia_SatDumpClause( vStr, pLits, 3 );
1368+
pLits[2] = Abc_Var2Lit( Gia_SatVarAckNeg(i), 1 );
1369+
Gia_SatDumpClause( vStr, pLits, 3 );
1370+
// when fanins can be used: !N & !P -> !0, !N & !P -> !1
1371+
pLits[0] = Abc_Var2Lit( Gia_SatVarAckPos(i), 0 );
1372+
pLits[1] = Abc_Var2Lit( Gia_SatVarAckNeg(i), 0 );
1373+
pLits[2] = Abc_Var2Lit( Gia_SatVarFan0(i), 1 );
1374+
Gia_SatDumpClause( vStr, pLits, 3 );
1375+
pLits[2] = Abc_Var2Lit( Gia_SatVarFan1(i), 1 );
1376+
Gia_SatDumpClause( vStr, pLits, 3 );
1377+
// when fanins are not used: 0 -> !N, 0 -> !P, 1 -> !N, 1 -> !P
1378+
for ( m = 0; m < 2; m++ )
1379+
for ( n = 0; n < 2; n++ ) {
1380+
pLits[0] = Abc_Var2Lit( Gia_SatVarFan0(i)+n, 1 );
1381+
pLits[1] = Abc_Var2Lit( Gia_SatVarReqPos(iFans[n])+m, 1 );
1382+
Gia_SatDumpClause( vStr, pLits, 2 );
1383+
}
1384+
// can only extend both when both complemented: !(C0 & C1) -> !0 + !1
1385+
pLits[0] = Abc_Var2Lit( Gia_SatVarFan0(i), 1 );
1386+
pLits[1] = Abc_Var2Lit( Gia_SatVarFan1(i), 1 );
1387+
if ( !fCompl[0] || !fCompl[1] )
1388+
Gia_SatDumpClause( vStr, pLits, 2 );
1389+
// if fanin is a primary input, cannot extend it (pi -> !0 or pi -> !1)
1390+
for ( n = 0; n < 2; n++ )
1391+
if ( Gia_ObjIsCi(pFans[n]) )
1392+
Gia_SatDumpLiteral( vStr, Abc_Var2Lit( Gia_SatVarFan0(i)+n, 1 ) );
1393+
// propagating assignments when fanin is not used
1394+
// P & !0 -> C0 ? P0 : N0
1395+
// N & !0 -> C0 ? N0 : P0
1396+
// P & !1 -> C1 ? P1 : N1
1397+
// N & !1 -> C1 ? N1 : P1
1398+
for ( m = 0; m < 2; m++ )
1399+
for ( n = 0; n < 2; n++ ) {
1400+
pLits[0] = Abc_Var2Lit( Gia_SatVarAckPos(i)+m, 1 );
1401+
pLits[1] = Abc_Var2Lit( Gia_SatVarFan0(i)+n, 0 );
1402+
pLits[2] = Abc_Var2Lit( Gia_SatVarReqPos(iFans[n]) + !(m ^ fCompl[n]), 0 );
1403+
Gia_SatDumpClause( vStr, pLits, 3 );
1404+
}
1405+
// propagating assignments when fanins are used
1406+
// P & 0 -> (C0 ^ C00) ? P00 : N00
1407+
// P & 0 -> (C0 ^ C01) ? P01 : N01
1408+
// N & 0 -> (C0 ^ C00) ? N00 : P00
1409+
// N & 0 -> (C0 ^ C01) ? N01 : P01
1410+
// P & 1 -> (C1 ^ C10) ? P10 : N10
1411+
// P & 1 -> (C1 ^ C11) ? P11 : N11
1412+
// N & 1 -> (C1 ^ C10) ? N10 : P10
1413+
// N & 1 -> (C1 ^ C11) ? N11 : P11
1414+
for ( m = 0; m < 2; m++ )
1415+
for ( n = 0; n < 2; n++ )
1416+
if ( Gia_ObjIsAnd(pFans[n]) ) {
1417+
pLits[0] = Abc_Var2Lit( Gia_SatVarAckPos(i)+m, 1 );
1418+
pLits[1] = Abc_Var2Lit( Gia_SatVarFan0(i)+n, 1 );
1419+
pLits[2] = Abc_Var2Lit( Gia_SatVarReqPos(Gia_ObjFaninId0p(p, pFans[n])) + !(m ^ fCompl[n] ^ Gia_ObjFaninC0(pFans[n])), 0 );
1420+
Gia_SatDumpClause( vStr, pLits, 3 );
1421+
pLits[2] = Abc_Var2Lit( Gia_SatVarReqPos(Gia_ObjFaninId1p(p, pFans[n])) + !(m ^ fCompl[n] ^ Gia_ObjFaninC1(pFans[n])), 0 );
1422+
Gia_SatDumpClause( vStr, pLits, 3 );
1423+
}
1424+
}
1425+
Vec_StrPush( vStr, '\0' );
1426+
return vStr;
1427+
}
1428+
1429+
typedef enum {
1430+
GIA_GATE_ZERO, // 0:
1431+
GIA_GATE_ONE, // 1:
1432+
GIA_GATE_BUF, // 2:
1433+
GIA_GATE_INV, // 3:
1434+
GIA_GATE_NAN2, // 4:
1435+
GIA_GATE_NOR2, // 5:
1436+
GIA_GATE_AOI21, // 6:
1437+
GIA_GATE_NAN3, // 7:
1438+
GIA_GATE_NOR3, // 8:
1439+
GIA_GATE_OAI21, // 9:
1440+
GIA_GATE_AOI22, // 10:
1441+
GIA_GATE_OAI22, // 11:
1442+
RTM_VAL_VOID // 12: unused value
1443+
} Gia_ManGate_t;
1444+
1445+
Vec_Int_t * Gia_ManDeriveSimpleMapping( Gia_Man_t * p, Vec_Int_t * vRes )
1446+
{
1447+
Vec_Int_t * vMapping = Vec_IntStart( 2*Gia_ManObjNum(p) );
1448+
int i, Id; Gia_Obj_t * pObj;
1449+
Gia_ManForEachCiId( p, Id, i )
1450+
if ( Gia_SatValReqNeg(vRes, Id) )
1451+
Vec_IntWriteEntry( vMapping, Abc_Var2Lit(Id, 1), -1 );
1452+
Gia_ManForEachAnd( p, pObj, i )
1453+
{
1454+
if ( Gia_SatValAckPos(vRes, i) + Gia_SatValAckNeg(vRes, i) == 0 )
1455+
continue;
1456+
assert( Gia_SatValAckPos(vRes, i) != Gia_SatValAckNeg(vRes, i) );
1457+
if ( (Gia_SatValReqPos(vRes, i) && Gia_SatValReqNeg(vRes, i)) || Gia_SatValInv(vRes, i) )
1458+
Vec_IntWriteEntry( vMapping, Abc_Var2Lit(i, Gia_SatValAckPos(vRes, i)), -1 );
1459+
int fComp = Gia_SatValAckNeg(vRes, i);
1460+
int fFan0 = Gia_SatValFan0(vRes, i);
1461+
int fFan1 = Gia_SatValFan1(vRes, i);
1462+
Gia_Obj_t * pFans[2] = { Gia_ObjFanin0(pObj), Gia_ObjFanin1(pObj) };
1463+
Vec_IntWriteEntry( vMapping, Abc_Var2Lit(i, fComp), Vec_IntSize(vMapping) );
1464+
if ( fFan0 && fFan1 ) {
1465+
assert( Gia_ObjFaninC0(pObj) && Gia_ObjFaninC1(pObj) );
1466+
Vec_IntPush( vMapping, 4 );
1467+
Vec_IntPush( vMapping, Abc_Var2Lit(Gia_ObjFaninId0p(p, pFans[0]), !(fComp ^ Gia_ObjFaninC0(pObj) ^ Gia_ObjFaninC0(pFans[0]))) );
1468+
Vec_IntPush( vMapping, Abc_Var2Lit(Gia_ObjFaninId1p(p, pFans[0]), !(fComp ^ Gia_ObjFaninC0(pObj) ^ Gia_ObjFaninC1(pFans[0]))) );
1469+
Vec_IntPush( vMapping, Abc_Var2Lit(Gia_ObjFaninId0p(p, pFans[1]), !(fComp ^ Gia_ObjFaninC1(pObj) ^ Gia_ObjFaninC0(pFans[1]))) );
1470+
Vec_IntPush( vMapping, Abc_Var2Lit(Gia_ObjFaninId1p(p, pFans[1]), !(fComp ^ Gia_ObjFaninC1(pObj) ^ Gia_ObjFaninC1(pFans[1]))) );
1471+
Vec_IntPush( vMapping, fComp ? GIA_GATE_OAI22 : GIA_GATE_AOI22 );
1472+
} else if ( fFan0 ) {
1473+
Vec_IntPush( vMapping, 3 );
1474+
Vec_IntPush( vMapping, Abc_Var2Lit(Gia_ObjFaninId0p(p, pFans[0]), !(fComp ^ Gia_ObjFaninC0(pObj) ^ Gia_ObjFaninC0(pFans[0]))) );
1475+
Vec_IntPush( vMapping, Abc_Var2Lit(Gia_ObjFaninId1p(p, pFans[0]), !(fComp ^ Gia_ObjFaninC0(pObj) ^ Gia_ObjFaninC1(pFans[0]))) );
1476+
Vec_IntPush( vMapping, Abc_Var2Lit(Gia_ObjFaninId1p(p, pObj), !(fComp ^ Gia_ObjFaninC1(pObj))) );
1477+
if ( Gia_ObjFaninC0(pObj) )
1478+
Vec_IntPush( vMapping, fComp ? GIA_GATE_OAI21 : GIA_GATE_AOI21 );
1479+
else
1480+
Vec_IntPush( vMapping, fComp ? GIA_GATE_NAN3 : GIA_GATE_NOR3 );
1481+
} else if ( fFan1 ) {
1482+
Vec_IntPush( vMapping, 3 );
1483+
Vec_IntPush( vMapping, Abc_Var2Lit(Gia_ObjFaninId0p(p, pFans[1]), !(fComp ^ Gia_ObjFaninC1(pObj) ^ Gia_ObjFaninC0(pFans[1]))) );
1484+
Vec_IntPush( vMapping, Abc_Var2Lit(Gia_ObjFaninId1p(p, pFans[1]), !(fComp ^ Gia_ObjFaninC1(pObj) ^ Gia_ObjFaninC1(pFans[1]))) );
1485+
Vec_IntPush( vMapping, Abc_Var2Lit(Gia_ObjFaninId0p(p, pObj), !(fComp ^ Gia_ObjFaninC0(pObj))) );
1486+
if ( Gia_ObjFaninC1(pObj) )
1487+
Vec_IntPush( vMapping, fComp ? GIA_GATE_OAI21 : GIA_GATE_AOI21 );
1488+
else
1489+
Vec_IntPush( vMapping, fComp ? GIA_GATE_NAN3 : GIA_GATE_NOR3 );
1490+
} else {
1491+
Vec_IntPush( vMapping, 2 );
1492+
Vec_IntPush( vMapping, Abc_Var2Lit(Gia_ObjFaninId0p(p, pObj), !(fComp ^ Gia_ObjFaninC0(pObj))) );
1493+
Vec_IntPush( vMapping, Abc_Var2Lit(Gia_ObjFaninId1p(p, pObj), !(fComp ^ Gia_ObjFaninC1(pObj))) );
1494+
Vec_IntPush( vMapping, fComp ? GIA_GATE_NAN2 : GIA_GATE_NOR2 );
1495+
}
1496+
}
1497+
return vMapping;
1498+
}
1499+
void Gia_ManSimplePrintMapping( Vec_Int_t * vRes, int nIns )
1500+
{
1501+
int i, k, nObjs = Vec_IntSize(vRes)/7, nSteps = Abc_Base10Log(nObjs);
1502+
int nCard = Vec_IntSum(vRes) - nIns; char NumStr[10];
1503+
printf( "Solution with cardinality %d:\n", nCard );
1504+
for ( k = 0; k < nSteps; k++ ) {
1505+
printf( " " );
1506+
for ( i = 0; i < nObjs; i++ ) {
1507+
sprintf( NumStr, "%02d", i );
1508+
printf( "%c", NumStr[k] );
1509+
}
1510+
printf( "\n" );
1511+
}
1512+
for ( k = 0; k < 7; k++ ) {
1513+
printf( "%c ", "pnPNi01"[k] );
1514+
for ( i = 0; i < nObjs; i++ )
1515+
if ( Vec_IntEntry( vRes, i*7+k ) == 0 )
1516+
printf( " " );
1517+
else
1518+
printf( "1" );
1519+
printf( "\n" );
1520+
}
1521+
}
1522+
int Gia_ManSimpleMapping( Gia_Man_t * p, int nBTLimit, int nBound, int fVerbose )
1523+
{
1524+
char * pFileNameI = (char *)"__temp__.cnf";
1525+
char * pFileNameO = (char *)"__temp__.out";
1526+
FILE * pFile = fopen( pFileNameI, "wb" );
1527+
if ( pFile == NULL ) { printf( "Cannot open input file \"%s\".\n", pFileNameI ); return 0; }
1528+
if ( nBound == 0 )
1529+
nBound = 2 * (Gia_ManCiNum(p) + 3 * Gia_ManAndNum(p));
1530+
Vec_Str_t * vStr = Gia_ManSimpleCnf( p, nBound/2 );
1531+
if ( fVerbose )
1532+
printf( "SAT variables = %d. SAT clauses = %d. Candinality bound = %d.\n", 7*(Gia_ManObjNum(p)-Gia_ManCoNum(p)), Vec_StrCountEntry(vStr, '\n'), nBound );
1533+
fprintf( pFile, "p knf %d %d\n%s\n", 7*(Gia_ManObjNum(p)-Gia_ManCoNum(p)), Vec_StrCountEntry(vStr, '\n'), Vec_StrArray(vStr) );
1534+
Vec_StrFree( vStr );
1535+
fclose( pFile );
1536+
Vec_Int_t * vRes = Gia_RunKadical( pFileNameI, pFileNameO, 0, 1 );
1537+
unlink( pFileNameI );
1538+
//unlink( pFileNameO );
1539+
if ( vRes == NULL )
1540+
return 0;
1541+
Vec_IntFreeP( &p->vCellMapping );
1542+
assert( p->vCellMapping == NULL );
1543+
Vec_IntDrop( vRes, 0 );
1544+
if ( fVerbose ) Gia_ManSimplePrintMapping( vRes, Gia_ManCiNum(p) );
1545+
p->vCellMapping = Gia_ManDeriveSimpleMapping( p, vRes );
1546+
Vec_IntFree( vRes );
1547+
return 1;
1548+
}
1549+
12191550
////////////////////////////////////////////////////////////////////////
12201551
/// END OF FILE ///
12211552
////////////////////////////////////////////////////////////////////////

0 commit comments

Comments
 (0)