Skip to content

Commit 27fdbe0

Browse files
alanminkoalanminko
committed
Updates to the mapping experiment.
1 parent 2361a02 commit 27fdbe0

File tree

1 file changed

+98
-24
lines changed

1 file changed

+98
-24
lines changed

‎src/aig/gia/giaSatLut.c‎

Lines changed: 98 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,7 @@
2020

2121
#include "gia.h"
2222
#include "misc/tim/tim.h"
23+
#include "misc/util/utilTruth.h"
2324
#include "sat/bsat/satStore.h"
2425
#include "misc/util/utilNam.h"
2526
#include "map/scl/sclCon.h"
@@ -1581,28 +1582,28 @@ int Gia_ManSimpleMapping( Gia_Man_t * p, int nBound, int nBTLimit, int nTimeout,
15811582

15821583
#define KSAT_OBJS 24
15831584
#define KSAT_MINTS 64
1584-
#define KSAT_SPACE (4+3*KSAT_OBJS+KSAT_MINTS)
1585+
#define KSAT_SPACE (4+3*KSAT_OBJS+3*KSAT_MINTS)
15851586

15861587
int Gia_KSatVarInv( int * pMap, int i ) { return pMap[i*KSAT_SPACE+0]; }
15871588
int Gia_KSatVarAnd( int * pMap, int i ) { return pMap[i*KSAT_SPACE+1]; }
15881589
int Gia_KSatVarEqu( int * pMap, int i ) { return pMap[i*KSAT_SPACE+2]; }
15891590
int Gia_KSatVarRef( int * pMap, int i ) { return pMap[i*KSAT_SPACE+3]; }
1590-
int Gia_KSatVarFan( int * pMap, int i, int f, int k ) { return pMap[i*KSAT_SPACE+4+f*KSAT_OBJS+k]; }
1591-
int Gia_KSatVarMin( int * pMap, int i, int m ) { return pMap[i*KSAT_SPACE+4+3*KSAT_OBJS+m]; }
1591+
int Gia_KSatVarFan( int * pMap, int i, int f, int k ) { return pMap[i*KSAT_SPACE+4+f*KSAT_OBJS+k]; }
1592+
int Gia_KSatVarMin( int * pMap, int i, int m, int k ) { return pMap[i*KSAT_SPACE+4+3*KSAT_OBJS+3*m+k]; }
15921593

15931594
void Gia_KSatSetInv( int * pMap, int i, int iVar ) { assert( -1 == pMap[i*KSAT_SPACE+0] ); pMap[i*KSAT_SPACE+0] = iVar; }
15941595
void Gia_KSatSetAnd( int * pMap, int i, int iVar ) { assert( -1 == pMap[i*KSAT_SPACE+1] ); pMap[i*KSAT_SPACE+1] = iVar; }
15951596
void Gia_KSatSetEqu( int * pMap, int i, int iVar ) { assert( -1 == pMap[i*KSAT_SPACE+2] ); pMap[i*KSAT_SPACE+2] = iVar; }
15961597
void Gia_KSatSetRef( int * pMap, int i, int iVar ) { assert( -1 == pMap[i*KSAT_SPACE+3] ); pMap[i*KSAT_SPACE+3] = iVar; }
1597-
void Gia_KSatSetFan( int * pMap, int i, int f, int k, int iVar ) { assert( -1 == pMap[i*KSAT_SPACE+4+f*KSAT_OBJS+k] ); pMap[i*KSAT_SPACE+4+f*KSAT_OBJS+k] = iVar; }
1598-
void Gia_KSatSetMin( int * pMap, int i, int m, int iVar ) { assert( -1 == pMap[i*KSAT_SPACE+4+3*KSAT_OBJS+m] ); pMap[i*KSAT_SPACE+4+3*KSAT_OBJS+m] = iVar; }
1598+
void Gia_KSatSetFan( int * pMap, int i, int f, int k, int iVar ) { assert( -1 == pMap[i*KSAT_SPACE+4+f*KSAT_OBJS+k] ); pMap[i*KSAT_SPACE+4+f*KSAT_OBJS+k] = iVar; }
1599+
void Gia_KSatSetMin( int * pMap, int i, int m, int k, int iVar ) { assert( -1 == pMap[i*KSAT_SPACE+4+3*KSAT_OBJS+3*m+k] ); pMap[i*KSAT_SPACE+4+3*KSAT_OBJS+3*m+k] = iVar; }
15991600

16001601
int Gia_KSatValInv( int * pMap, int i, Vec_Int_t * vRes ) { assert( -1 != pMap[i*KSAT_SPACE+0] ); return Vec_IntEntry( vRes, pMap[i*KSAT_SPACE+0] ); }
16011602
int Gia_KSatValAnd( int * pMap, int i, Vec_Int_t * vRes ) { assert( -1 != pMap[i*KSAT_SPACE+1] ); return Vec_IntEntry( vRes, pMap[i*KSAT_SPACE+1] ); }
16021603
int Gia_KSatValEqu( int * pMap, int i, Vec_Int_t * vRes ) { assert( -1 != pMap[i*KSAT_SPACE+2] ); return Vec_IntEntry( vRes, pMap[i*KSAT_SPACE+2] ); }
16031604
int Gia_KSatValRef( int * pMap, int i, Vec_Int_t * vRes ) { assert( -1 != pMap[i*KSAT_SPACE+3] ); return Vec_IntEntry( vRes, pMap[i*KSAT_SPACE+3] ); }
1604-
int Gia_KSatValFan( int * pMap, int i, int f, int k, Vec_Int_t * vRes ) { assert( -1 != pMap[i*KSAT_SPACE+4+f*KSAT_OBJS+k] ); return Vec_IntEntry( vRes, pMap[i*KSAT_SPACE+4+f*KSAT_OBJS+k] ); }
1605-
int Gia_KSatValMin( int * pMap, int i, int m, Vec_Int_t * vRes ) { assert( -1 != pMap[i*KSAT_SPACE+4+3*KSAT_OBJS+m] ); return Vec_IntEntry( vRes, pMap[i*KSAT_SPACE+4+3*KSAT_OBJS+m] ); }
1605+
int Gia_KSatValFan( int * pMap, int i, int f, int k, Vec_Int_t * vRes ) { assert( -1 != pMap[i*KSAT_SPACE+4+f*KSAT_OBJS+k] ); return Vec_IntEntry( vRes, pMap[i*KSAT_SPACE+4+f*KSAT_OBJS+k] ); }
1606+
int Gia_KSatValMin( int * pMap, int i, int m, int k, Vec_Int_t * vRes ) { assert( -1 != pMap[i*KSAT_SPACE+4+3*KSAT_OBJS+3*m+k] ); return Vec_IntEntry( vRes, pMap[i*KSAT_SPACE+4+3*KSAT_OBJS+3*m+k] ); }
16061607

16071608
int * Gia_KSatMapInit( int nIns, int nNodes, word Truth, int * pnVars )
16081609
{
@@ -1624,10 +1625,13 @@ int * Gia_KSatMapInit( int nIns, int nNodes, word Truth, int * pnVars )
16241625
}
16251626
for ( m = 0; m < (1<<nIns); m++ ) {
16261627
for ( n = 0; n < nIns; n++ )
1627-
Gia_KSatSetMin(pMap, n, m, (m >> n) & 1 );
1628-
Gia_KSatSetMin(pMap, nIns+nNodes-1, m, (Truth >> m) & 1 );
1629-
for ( n = nIns; n < nIns+nNodes-1; n++ )
1630-
Gia_KSatSetMin(pMap, n, m, nVars++);
1628+
Gia_KSatSetMin(pMap, n, m, 0, (m >> n) & 1 );
1629+
Gia_KSatSetMin(pMap, nIns+nNodes-1, m, 0, (Truth >> m) & 1 );
1630+
for ( n = nIns; n < nIns+nNodes; n++ )
1631+
for ( k = 0; k < 3; k++ )
1632+
if ( k || n < nIns+nNodes-1 )
1633+
Gia_KSatSetMin(pMap, n, m, k, nVars++);
1634+
16311635
}
16321636
if ( pnVars ) *pnVars = nVars;
16331637
return pMap;
@@ -1647,7 +1651,7 @@ Gia_Man_t * Gia_ManDeriveKSatMapping( Vec_Int_t * vRes, int * pMap, int nIns, in
16471651
{
16481652
Gia_Man_t * pNew = Gia_ManStart( nIns + nNodes + 2 );
16491653
pNew->pName = Abc_UtilStrsav( "test" );
1650-
int i, pCopy[256] = {0};
1654+
int i, nSave = 0, pCopy[256] = {0};
16511655
for ( i = 1; i <= nIns; i++ )
16521656
pCopy[i] = Gia_ManAppendCi( pNew );
16531657
for ( i = nIns; i < nIns+nNodes; i++ ) {
@@ -1668,8 +1672,11 @@ Gia_Man_t * Gia_ManDeriveKSatMapping( Vec_Int_t * vRes, int * pMap, int nIns, in
16681672
printf( "%sAND( %d, %d )\n", Gia_KSatValInv(pMap, i, vRes) ? "N":"", iFan0, iFan1 );
16691673
else
16701674
printf( "%sOR( %d, %d )\n", Gia_KSatValInv(pMap, i, vRes) ? "N":"", iFan0, iFan1 );
1671-
if ( i == nIns+nNodes-1 )
1675+
nSave += (iFan0 == iFan1) || !Gia_KSatValInv(pMap, i, vRes);
1676+
if ( i == nIns+nNodes-1 ) {
16721677
printf( "CO = %d\n", nIns+nNodes-1 );
1678+
printf( "Solution cost = %d\n", 2*(2*nNodes - nSave) );
1679+
}
16731680
}
16741681
}
16751682
Gia_ManAppendCo( pNew, pCopy[nIns+nNodes] );
@@ -1704,6 +1711,13 @@ Vec_Str_t * Gia_ManKSatCnf( int * pMap, int nIns, int nNodes, int nBound )
17041711
pLits[2] = Abc_Var2Lit( Gia_KSatVarEqu(pMap, n), 0 );
17051712
Gia_SatDumpClause( vStr, pLits, 3 );
17061713
}
1714+
for ( i = 0; i < n; i++ )
1715+
for ( j = i+1; j < n; j++ ) {
1716+
pLits[0] = Abc_Var2Lit( Gia_KSatVarFan(pMap, n, 0, i), 1 );
1717+
pLits[1] = Abc_Var2Lit( Gia_KSatVarFan(pMap, n, 1, j), 1 );
1718+
pLits[2] = Abc_Var2Lit( Gia_KSatVarEqu(pMap, n), 1 );
1719+
Gia_SatDumpClause( vStr, pLits, 3 );
1720+
}
17071721
// if fanins are equal, inv is used
17081722
pLits[0] = Abc_Var2Lit( Gia_KSatVarEqu(pMap, n), 1 );
17091723
pLits[1] = Abc_Var2Lit( Gia_KSatVarInv(pMap, n), 0 );
@@ -1718,11 +1732,16 @@ Vec_Str_t * Gia_ManKSatCnf( int * pMap, int nIns, int nNodes, int nBound )
17181732
}
17191733
for ( n = nIns; n < nIns+nNodes-1; n++ ) {
17201734
// there is a fanout to the node above
1721-
for ( i = n+1; i < nIns+nNodes; i++ )
1722-
for ( f = 0; f < 2; f++ ) {
1723-
pLits[0] = Abc_Var2Lit( Gia_KSatVarFan(pMap, i, f, n), 1 );
1724-
pLits[1] = Abc_Var2Lit( Gia_KSatVarFan(pMap, n, 2, i), 0 );
1725-
Gia_SatDumpClause( vStr, pLits, 2 );
1735+
for ( i = n+1; i < nIns+nNodes; i++ ) {
1736+
for ( f = 0; f < 2; f++ ) {
1737+
pLits[0] = Abc_Var2Lit( Gia_KSatVarFan(pMap, i, f, n), 1 );
1738+
pLits[1] = Abc_Var2Lit( Gia_KSatVarFan(pMap, n, 2, i), 0 );
1739+
Gia_SatDumpClause( vStr, pLits, 2 );
1740+
}
1741+
pLits[0] = Abc_Var2Lit( Gia_KSatVarFan(pMap, i, 0, n), 0 );
1742+
pLits[1] = Abc_Var2Lit( Gia_KSatVarFan(pMap, i, 1, n), 0 );
1743+
pLits[2] = Abc_Var2Lit( Gia_KSatVarFan(pMap, n, 2, i), 1 );
1744+
Gia_SatDumpClause( vStr, pLits, 3 );
17261745
}
17271746
// there is at least one fanout, except the last one
17281747
nLits = 0;
@@ -1755,6 +1774,7 @@ Vec_Str_t * Gia_ManKSatCnf( int * pMap, int nIns, int nNodes, int nBound )
17551774
}
17561775
// the last one always uses inverter
17571776
Gia_SatDumpLiteral( vStr, Abc_Var2Lit( Gia_KSatVarInv(pMap, nIns+nNodes-1), 0 ) );
1777+
/*
17581778
// for each minterm, for each pair of possible fanins, the node's output is determined using and/or and inv (4*N*N*M)
17591779
for ( m = 0; m < (1 << nIns); m++ )
17601780
for ( n = nIns; n < nIns+nNodes; n++ )
@@ -1764,37 +1784,90 @@ Vec_Str_t * Gia_ManKSatCnf( int * pMap, int nIns, int nNodes, int nBound )
17641784
for ( f = 0; f < 2; f++ )
17651785
for ( i = 0; i < n; i++ ) {
17661786
pLits[0] = Abc_Var2Lit( Gia_KSatVarFan(pMap, n, f, i), 1 );
1767-
pLits[1] = Abc_Var2Lit( Gia_KSatVarMin(pMap, i, m), !a );
1787+
pLits[1] = Abc_Var2Lit( Gia_KSatVarMin(pMap, i, m, 0), !a );
17681788
pLits[2] = Abc_Var2Lit( Gia_KSatVarAnd(pMap, n), a );
17691789
pLits[3] = Abc_Var2Lit( Gia_KSatVarInv(pMap, n), c );
1770-
pLits[4] = Abc_Var2Lit( Gia_KSatVarMin(pMap, n, m), a^c );
1790+
pLits[4] = Abc_Var2Lit( Gia_KSatVarMin(pMap, n, m, 0), a^c );
17711791
Gia_SatDumpClause( vStr, pLits, 5 );
17721792
}
17731793
// large clauses: Fan(0) & Fan(1) & !Mint(m) & !Mint(m) & !And & !Inv -> Val0
17741794
for ( i = 0; i < n; i++ )
17751795
for ( j = i; j < n; j++ ) {
17761796
pLits[0] = Abc_Var2Lit( Gia_KSatVarFan(pMap, n, 0, i), 1 );
17771797
pLits[1] = Abc_Var2Lit( Gia_KSatVarFan(pMap, n, 1, j), 1 );
1778-
pLits[2] = Abc_Var2Lit( Gia_KSatVarMin(pMap, i, m), a );
1779-
pLits[3] = Abc_Var2Lit( Gia_KSatVarMin(pMap, j, m), a );
1798+
pLits[2] = Abc_Var2Lit( Gia_KSatVarMin(pMap, i, m, 0), a );
1799+
pLits[3] = Abc_Var2Lit( Gia_KSatVarMin(pMap, j, m, 0), a );
17801800
pLits[4] = Abc_Var2Lit( Gia_KSatVarAnd(pMap, n), a );
17811801
pLits[5] = Abc_Var2Lit( Gia_KSatVarInv(pMap, n), c );
1782-
pLits[6] = Abc_Var2Lit( Gia_KSatVarMin(pMap, n, m), a==c );
1802+
pLits[6] = Abc_Var2Lit( Gia_KSatVarMin(pMap, n, m, 0), a==c );
17831803
Gia_SatDumpClause( vStr, pLits, 7 );
17841804
}
17851805
}
1806+
*/
1807+
// for each minterm, define a fanin variable and use it to get the node's output based on and/or and inv (4*N*N*M)
1808+
for ( m = 0; m < (1 << nIns); m++ )
1809+
for ( n = nIns; n < nIns+nNodes; n++ ) {
1810+
for ( i = 0; i < n; i++ )
1811+
for ( f = 0; f < 2; f++ )
1812+
for ( c = 0; c < 2; c++ ) {
1813+
pLits[0] = Abc_Var2Lit( Gia_KSatVarFan(pMap, n, f, i), 1 );
1814+
pLits[1] = Abc_Var2Lit( Gia_KSatVarMin(pMap, i, m, 0), c );
1815+
pLits[2] = Abc_Var2Lit( Gia_KSatVarMin(pMap, n, m, 1+f), !c );
1816+
Gia_SatDumpClause( vStr, pLits, 3 );
1817+
}
1818+
for ( c = 0; c < 2; c++ )
1819+
for ( a = 0; a < 2; a++ ) {
1820+
// implications: Mint(m,f) & !And & !Inv -> Val1
1821+
for ( f = 0; f < 2; f++ ) {
1822+
pLits[0] = Abc_Var2Lit( Gia_KSatVarMin(pMap, n, m, 1+f), !a );
1823+
pLits[1] = Abc_Var2Lit( Gia_KSatVarAnd(pMap, n), a );
1824+
pLits[2] = Abc_Var2Lit( Gia_KSatVarInv(pMap, n), c );
1825+
pLits[3] = Abc_Var2Lit( Gia_KSatVarMin(pMap, n, m, 0), a^c );
1826+
Gia_SatDumpClause( vStr, pLits, 4 );
1827+
}
1828+
// large clauses: !Mint(m,0) & !Mint(m,1) & !And & !Inv -> Val0
1829+
pLits[0] = Abc_Var2Lit( Gia_KSatVarMin(pMap, n, m, 1), a );
1830+
pLits[1] = Abc_Var2Lit( Gia_KSatVarMin(pMap, n, m, 2), a );
1831+
pLits[2] = Abc_Var2Lit( Gia_KSatVarAnd(pMap, n), a );
1832+
pLits[3] = Abc_Var2Lit( Gia_KSatVarInv(pMap, n), c );
1833+
pLits[4] = Abc_Var2Lit( Gia_KSatVarMin(pMap, n, m, 0), a==c );
1834+
Gia_SatDumpClause( vStr, pLits, 5 );
1835+
}
1836+
}
17861837
// the number of nodes with duplicated fanins and without inv is maximized
1838+
if ( nBound && 2*nNodes > nBound ) {
1839+
Vec_StrPrintF( vStr, "k %d ", 2*nNodes-nBound );
1840+
nLits = 0;
1841+
for ( n = nIns; n < nIns+nNodes; n++ ) {
1842+
pLits[nLits++] = Abc_Var2Lit(Gia_KSatVarEqu(pMap, n), 0);
1843+
pLits[nLits++] = Abc_Var2Lit(Gia_KSatVarInv(pMap, n), 1);
1844+
}
1845+
Gia_SatDumpClause( vStr, pLits, nLits );
1846+
}
17871847
Vec_StrPush( vStr, '\0' );
17881848
return vStr;
17891849
}
17901850

1851+
word Gia_ManGetTruth( Gia_Man_t * p )
1852+
{
1853+
Gia_Obj_t * pObj; int i, Id;
1854+
word pFuncs[256] = {0}, Const[2] = {0, ~(word)0};
1855+
assert( Gia_ManObjNum(p) <= 256 );
1856+
Gia_ManForEachCiId( p, Id, i )
1857+
pFuncs[Id] = s_Truths6[i];
1858+
Gia_ManForEachAnd( p, pObj, i )
1859+
pFuncs[i] = (Const[Gia_ObjFaninC0(pObj)] ^ pFuncs[Gia_ObjFaninId0(pObj, i)]) & (Const[Gia_ObjFaninC1(pObj)] ^ pFuncs[Gia_ObjFaninId1(pObj, i)]);
1860+
pObj = Gia_ManCo(p, 0);
1861+
return Const[Gia_ObjFaninC0(pObj)] ^ pFuncs[Gia_ObjFaninId0p(p, pObj)];
1862+
}
1863+
17911864
Gia_Man_t * Gia_ManKSatMapping( word Truth, int nIns, int nNodes, int nBound, int nBTLimit, int nTimeout, int fVerbose )
17921865
{
17931866
Gia_Man_t * pNew = NULL;
17941867
char * pFileNameI = (char *)"__temp__.cnf";
17951868
char * pFileNameO = (char *)"__temp__.out";
17961869
int nVars = 0, * pMap = Gia_KSatMapInit( nIns, nNodes, Truth, &nVars );
1797-
Vec_Str_t * vStr = Gia_ManKSatCnf( pMap, nIns, nNodes, nBound );
1870+
Vec_Str_t * vStr = Gia_ManKSatCnf( pMap, nIns, nNodes, nBound/2 );
17981871
if ( !Gia_ManDumpCnf(pFileNameI, vStr, nVars) ) {
17991872
Vec_StrFree( vStr );
18001873
return NULL;
@@ -1812,6 +1885,7 @@ Gia_Man_t * Gia_ManKSatMapping( word Truth, int nIns, int nNodes, int nBound, in
18121885
return 0;
18131886
Vec_IntDrop( vRes, 0 );
18141887
pNew = Gia_ManDeriveKSatMapping( vRes, pMap, nIns, nNodes, fVerbose );
1888+
printf( "Verification %s.\n", Truth == Gia_ManGetTruth(pNew) ? "passed" : "failed" );
18151889
Vec_IntFree( vRes );
18161890
ABC_FREE( pMap );
18171891
return pNew;

0 commit comments

Comments
 (0)