Skip to content

Commit 0ebc9db

Browse files
alanminkoalanminko
committed
Experiments with exact synthesis.
1 parent 839f3e1 commit 0ebc9db

File tree

4 files changed

+50
-25
lines changed

4 files changed

+50
-25
lines changed

‎src/aig/gia/giaSimBase.c‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3199,7 +3199,7 @@ Vec_Int_t * Gia_ManRelDeriveSimple( Gia_Man_t * p, Vec_Wrd_t * vSims, Vec_Int_t
31993199

32003200
void Gia_ManRelSolve( Gia_Man_t * p, Vec_Wrd_t * vSims, Vec_Int_t * vIns, Vec_Int_t * vOuts, Vec_Int_t * vRel, Vec_Int_t * vDivs )
32013201
{
3202-
extern Mini_Aig_t * Exa4_ManGenTest( Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsOut, int nIns, int nDivs, int nOuts, int nNodes, int TimeOut, int fOnlyAnd, int fFancy, int fOrderNodes, int fUniqFans, int fVerbose );
3202+
extern Mini_Aig_t * Exa4_ManGenTest( Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsOut, int nIns, int nDivs, int nOuts, int nNodes, int TimeOut, int fOnlyAnd, int fFancy, int fOrderNodes, int fUniqFans, int fVerbose, int fCard );
32033203

32043204
int i, m, iObj, Entry, iMint = 0, nMints = Vec_IntSize(vRel) - Vec_IntCountEntry(vRel, -1);
32053205
Vec_Wrd_t * vSimsIn = Vec_WrdStart( nMints );
@@ -3232,7 +3232,7 @@ void Gia_ManRelSolve( Gia_Man_t * p, Vec_Wrd_t * vSims, Vec_Int_t * vIns, Vec_In
32323232
}
32333233
assert( iMint == nMints );
32343234
printf( "Created %d minterms.\n", iMint );
3235-
Exa4_ManGenTest( vSimsIn, vSimsOut, Vec_IntSize(vIns), Vec_IntSize(vDivs), Vec_IntSize(vOuts), 10, 0, 0, 0, 0, 0, 1 );
3235+
Exa4_ManGenTest( vSimsIn, vSimsOut, Vec_IntSize(vIns), Vec_IntSize(vDivs), Vec_IntSize(vOuts), 10, 0, 0, 0, 0, 0, 1, 0 );
32363236
Vec_WrdFree( vSimsIn );
32373237
Vec_WrdFree( vSimsOut );
32383238
}

‎src/base/abci/abc.c‎

Lines changed: 7 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -10061,7 +10061,7 @@ int Abc_CommandTwoExact( Abc_Frame_t * pAbc, int argc, char ** argv )
1006110061
Bmc_EsPar_t Pars, * pPars = &Pars;
1006210062
Bmc_EsParSetDefault( pPars );
1006310063
Extra_UtilGetoptReset();
10064-
while ( ( c = Extra_UtilGetopt( argc, argv, "INTGabdconugklvh" ) ) != EOF )
10064+
while ( ( c = Extra_UtilGetopt( argc, argv, "INTGabdconugklmvh" ) ) != EOF )
1006510065
{
1006610066
switch ( c )
1006710067
{
@@ -10139,6 +10139,9 @@ int Abc_CommandTwoExact( Abc_Frame_t * pAbc, int argc, char ** argv )
1013910139
case 'l':
1014010140
fKissat2 ^= 1;
1014110141
break;
10142+
case 'm':
10143+
pPars->fCard ^= 1;
10144+
break;
1014210145
case 'v':
1014310146
pPars->fVerbose ^= 1;
1014410147
break;
@@ -10179,7 +10182,7 @@ int Abc_CommandTwoExact( Abc_Frame_t * pAbc, int argc, char ** argv )
1017910182
}
1018010183
if ( fUseNands )
1018110184
Exa_ManExactSynthesis7( pPars, GateSize );
10182-
else if ( fKissat )
10185+
else if ( fKissat || pPars->fCard )
1018310186
Exa_ManExactSynthesis4( pPars );
1018410187
else if ( fKissat2 )
1018510188
Exa_ManExactSynthesis5( pPars );
@@ -10190,7 +10193,7 @@ int Abc_CommandTwoExact( Abc_Frame_t * pAbc, int argc, char ** argv )
1019010193
return 0;
1019110194

1019210195
usage:
10193-
Abc_Print( -2, "usage: twoexact [-INTG <num>] [-abdconugklvh] <hex>\n" );
10196+
Abc_Print( -2, "usage: twoexact [-INTG <num>] [-abdconugklmvh] <hex>\n" );
1019410197
Abc_Print( -2, "\t exact synthesis of multi-input function using two-input gates\n" );
1019510198
Abc_Print( -2, "\t-I <num> : the number of input variables [default = %d]\n", pPars->nVars );
1019610199
Abc_Print( -2, "\t-N <num> : the number of two-input nodes [default = %d]\n", pPars->nNodes );
@@ -10206,6 +10209,7 @@ int Abc_CommandTwoExact( Abc_Frame_t * pAbc, int argc, char ** argv )
1020610209
Abc_Print( -2, "\t-g : toggle using Glucose 3.0 by Gilles Audemard and Laurent Simon [default = %s]\n", pPars->fGlucose ? "yes" : "no" );
1020710210
Abc_Print( -2, "\t-k : toggle using Kissat by Armin Biere [default = %s]\n", fKissat ? "yes" : "no" );
1020810211
Abc_Print( -2, "\t-l : toggle using Kissat by Armin Biere [default = %s]\n", fKissat2 ? "yes" : "no" );
10212+
Abc_Print( -2, "\t-m : toggle using CaDiCaL by Armin Biere [default = %s]\n", pPars->fCard ? "yes" : "no" );
1020910213
Abc_Print( -2, "\t-v : toggle verbose printout [default = %s]\n", pPars->fVerbose ? "yes" : "no" );
1021010214
Abc_Print( -2, "\t-h : print the command usage\n" );
1021110215
Abc_Print( -2, "\t<hex> : truth table in hex notation\n" );

‎src/sat/bmc/bmc.h‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -57,6 +57,7 @@ struct Bmc_EsPar_t_
5757
int fDynConstr;
5858
int fDumpCnf;
5959
int fGlucose;
60+
int fCard;
6061
int fOrderNodes;
6162
int fEnumSols;
6263
int fFewerVars;

‎src/sat/bmc/bmcMaj.c‎

Lines changed: 40 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -1941,7 +1941,7 @@ static inline int Exa4_ManAddClause4( Exa4_Man_t * p, int Lit0, int Lit1, int Li
19411941
int pLits[4] = { Lit0, Lit1, Lit2, Lit3 };
19421942
return Exa4_ManAddClause( p, pLits, 4 );
19431943
}
1944-
int Exa4_ManGenStart( Exa4_Man_t * p, int fOnlyAnd, int fFancy, int fOrderNodes, int fUniqFans )
1944+
int Exa4_ManGenStart( Exa4_Man_t * p, int fOnlyAnd, int fFancy, int fOrderNodes, int fUniqFans, int fCard )
19451945
{
19461946
int pLits[2*MAJ_NOBJS], i, j, k, n, m, nLits;
19471947
for ( i = p->nDivs; i < p->nDivs + p->nNodes; i++ )
@@ -1955,9 +1955,17 @@ int Exa4_ManGenStart( Exa4_Man_t * p, int fOnlyAnd, int fFancy, int fOrderNodes,
19551955
pLits[nLits++] = Abc_Var2Lit( p->VarMarks[i][k][j], 0 );
19561956
assert( nLits > 0 );
19571957
Exa4_ManAddClause( p, pLits, nLits );
1958-
for ( n = 0; n < nLits; n++ )
1959-
for ( m = n+1; m < nLits; m++ )
1960-
Exa4_ManAddClause4( p, Abc_LitNot(pLits[n]), Abc_LitNot(pLits[m]), 0, 0 );
1958+
if ( !fCard ) {
1959+
for ( n = 0; n < nLits; n++ )
1960+
for ( m = n+1; m < nLits; m++ )
1961+
Exa4_ManAddClause4( p, Abc_LitNot(pLits[n]), Abc_LitNot(pLits[m]), 0, 0 );
1962+
}
1963+
else {
1964+
fprintf( p->pFile, "k %d ", nLits-1 );
1965+
for ( n = 0; n < nLits; n++ )
1966+
pLits[n] = Abc_LitNot(pLits[n]);
1967+
Exa4_ManAddClause( p, pLits, nLits );
1968+
}
19611969
if ( k == 1 )
19621970
break;
19631971
for ( j = 0; j < p->nObjs; j++ ) if ( p->VarMarks[i][0][j] )
@@ -2096,17 +2104,17 @@ void Exa4_ManGenMint( Exa4_Man_t * p, int iMint, int fOnlyAnd, int fFancy )
20962104
Exa4_ManAddClause4( p, Abc_Var2Lit(p->VarMarks[i][0][j], 1), Abc_LitNotCond(VarVals[j], n), Abc_LitNotCond(VarVals[i], !n), 0);
20972105
}
20982106
}
2099-
void Exa4_ManGenCnf( Exa4_Man_t * p, char * pFileName, int fOnlyAnd, int fFancy, int fOrderNodes, int fUniqFans )
2107+
void Exa4_ManGenCnf( Exa4_Man_t * p, char * pFileName, int fOnlyAnd, int fFancy, int fOrderNodes, int fUniqFans, int fCard )
21002108
{
21012109
int m;
21022110
assert( p->pFile == NULL );
21032111
p->pFile = fopen( pFileName, "wb" );
21042112
fputs( "p cnf \n", p->pFile );
2105-
Exa4_ManGenStart( p, fOnlyAnd, fFancy, fOrderNodes, fUniqFans );
2113+
Exa4_ManGenStart( p, fOnlyAnd, fFancy, fOrderNodes, fUniqFans, fCard );
21062114
for ( m = 1; m < Vec_WrdSize(p->vSimsIn); m++ )
21072115
Exa4_ManGenMint( p, m, fOnlyAnd, fFancy );
21082116
rewind( p->pFile );
2109-
fprintf( p->pFile, "p cnf %d %d", p->nCnfVars, p->nCnfClauses );
2117+
fprintf( p->pFile, "p %cnf %d %d", fCard ? 'k' : 'c', p->nCnfVars, p->nCnfClauses );
21102118
fclose( p->pFile );
21112119
}
21122120

@@ -2130,6 +2138,8 @@ static inline int Exa4_ManFindFanin( Exa4_Man_t * p, Vec_Int_t * vValues, int i,
21302138
iVar = j;
21312139
Count++;
21322140
}
2141+
if ( Count != 1 )
2142+
printf( "Fanin count is %d instead of %d.\n", Count, 1 );
21332143
assert( Count == 1 );
21342144
return iVar;
21352145
}
@@ -2268,21 +2278,27 @@ Mini_Aig_t * Exa4_ManMiniAig( Exa4_Man_t * p, Vec_Int_t * vValues, int fFancy )
22682278
SeeAlso []
22692279
22702280
***********************************************************************/
2271-
Mini_Aig_t * Exa4_ManGenTest( Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsOut, int nIns, int nDivs, int nOuts, int nNodes, int TimeOut, int fOnlyAnd, int fFancy, int fOrderNodes, int fUniqFans, int fVerbose )
2281+
Mini_Aig_t * Exa4_ManGenTest( Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsOut, int nIns, int nDivs, int nOuts, int nNodes, int TimeOut, int fOnlyAnd, int fFancy, int fOrderNodes, int fUniqFans, int fVerbose, int fCard )
22722282
{
2283+
extern Vec_Int_t * Gia_RunKadical( char * pFileNameIn, char * pFileNameOut, int nBTLimit, int TimeOut, int fVerbose, int * pStatus );
22732284
Mini_Aig_t * pMini = NULL;
22742285
abctime clkTotal = Abc_Clock();
22752286
Vec_Int_t * vValues = NULL;
2276-
char * pFileNameIn = "_temp_.cnf";
2277-
char * pFileNameOut = "_temp_out.cnf";
2287+
srand(time(NULL));
2288+
int Status = 0, Rand = ((((unsigned)rand()) << 12) ^ ((unsigned)rand())) & 0xFFFFF;
2289+
char pFileNameIn[32]; sprintf( pFileNameIn, "_%05x_.cnf", Rand );
2290+
char pFileNameOut[32]; sprintf( pFileNameOut, "_%05x_.out", Rand );
22782291
Exa4_Man_t * p = Exa4_ManAlloc( vSimsIn, vSimsOut, nIns, nDivs, nOuts, nNodes, fVerbose );
22792292
Exa_ManIsNormalized( vSimsIn, vSimsOut );
2280-
Exa4_ManGenCnf( p, pFileNameIn, fOnlyAnd, fFancy, fOrderNodes, fUniqFans );
2293+
Exa4_ManGenCnf( p, pFileNameIn, fOnlyAnd, fFancy, fOrderNodes, fUniqFans, fCard );
22812294
if ( fVerbose )
22822295
printf( "Timeout = %d. OnlyAnd = %d. Fancy = %d. OrderNodes = %d. UniqueFans = %d. Verbose = %d.\n", TimeOut, fOnlyAnd, fFancy, fOrderNodes, fUniqFans, fVerbose );
22832296
if ( fVerbose )
22842297
printf( "CNF with %d variables and %d clauses was dumped into file \"%s\".\n", p->nCnfVars, p->nCnfClauses, pFileNameIn );
2285-
vValues = Exa4_ManSolve( pFileNameIn, pFileNameOut, TimeOut, fVerbose );
2298+
if ( fCard )
2299+
vValues = Gia_RunKadical( pFileNameIn, pFileNameOut, 0, TimeOut, fVerbose, &Status );
2300+
else
2301+
vValues = Exa4_ManSolve( pFileNameIn, pFileNameOut, TimeOut, fVerbose );
22862302
if ( vValues ) pMini = Exa4_ManMiniAig( p, vValues, fFancy );
22872303
//if ( vValues ) Exa4_ManPrintSolution( p, vValues, fFancy );
22882304
if ( vValues ) Exa_ManMiniPrint( pMini, p->nIns );
@@ -2310,7 +2326,7 @@ void Exa_ManExactSynthesis4_( Bmc_EsPar_t * pPars )
23102326
if ( (m >> i) & 1 )
23112327
Abc_TtSetBit( Vec_WrdEntryP(vSimsIn, m), 1+i );
23122328
}
2313-
pMini = Exa4_ManGenTest( vSimsIn, vSimsOut, 3, 4, 2, pPars->nNodes, pPars->RuntimeLim, pPars->fOnlyAnd, pPars->fFewerVars, pPars->fOrderNodes, pPars->fUniqFans, pPars->fVerbose );
2329+
pMini = Exa4_ManGenTest( vSimsIn, vSimsOut, 3, 4, 2, pPars->nNodes, pPars->RuntimeLim, pPars->fOnlyAnd, pPars->fFewerVars, pPars->fOrderNodes, pPars->fUniqFans, pPars->fVerbose, 0 );
23142330
if ( pMini ) Mini_AigStop( pMini );
23152331
Vec_WrdFree( vSimsIn );
23162332
Vec_WrdFree( vSimsOut );
@@ -2332,7 +2348,7 @@ void Exa_ManExactSynthesis4( Bmc_EsPar_t * pPars )
23322348
Abc_TtSetBit( Vec_WrdEntryP(vSimsIn, m), 1+i );
23332349
}
23342350
assert( Vec_WrdSize(vSimsIn) == (1 << pPars->nVars) );
2335-
pMini = Exa4_ManGenTest( vSimsIn, vSimsOut, pPars->nVars, 1+pPars->nVars, 1, pPars->nNodes, pPars->RuntimeLim, pPars->fOnlyAnd, pPars->fFewerVars, pPars->fOrderNodes, pPars->fUniqFans, pPars->fVerbose );
2351+
pMini = Exa4_ManGenTest( vSimsIn, vSimsOut, pPars->nVars, 1+pPars->nVars, 1, pPars->nNodes, pPars->RuntimeLim, pPars->fOnlyAnd, pPars->fFewerVars, pPars->fOrderNodes, pPars->fUniqFans, pPars->fVerbose, pPars->fCard );
23362352
if ( pMini ) Mini_AigStop( pMini );
23372353
if ( fCompl ) printf( "The resulting circuit, if computed, will be complemented.\n" );
23382354
Vec_WrdFree( vSimsIn );
@@ -2797,8 +2813,10 @@ Mini_Aig_t * Exa5_ManGenTest( Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsOut, int nIn
27972813
abctime clkTotal = Abc_Clock();
27982814
Mini_Aig_t * pMini = NULL;
27992815
Vec_Int_t * vValues = NULL;
2800-
char * pFileNameIn = "_temp_.cnf";
2801-
char * pFileNameOut = "_temp_out.cnf";
2816+
srand(time(NULL));
2817+
int Rand = ((((unsigned)rand()) << 12) ^ ((unsigned)rand())) & 0xFFFFF;
2818+
char pFileNameIn[32]; sprintf( pFileNameIn, "_%05x_.cnf", Rand );
2819+
char pFileNameOut[32]; sprintf( pFileNameOut, "_%05x_.out", Rand );
28022820
Exa5_Man_t * p = Exa5_ManAlloc( vSimsIn, vSimsOut, nIns, nDivs, nOuts, nNodes, fVerbose );
28032821
Exa_ManIsNormalized( vSimsIn, vSimsOut );
28042822
Exa5_ManGenCnf( p, pFileNameIn, fOnlyAnd, fFancy, fOrderNodes, fUniqFans );
@@ -3717,8 +3735,9 @@ Mini_Aig_t * Exa6_ManGenTest( Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsOut, int nIn
37173735
Mini_Aig_t * pMini = NULL;
37183736
abctime clkTotal = Abc_Clock();
37193737
Vec_Int_t * vValues = NULL;
3720-
char * pFileNameIn = "_temp_.cnf";
3721-
char * pFileNameOut = "_temp_out.cnf";
3738+
int Rand = ((((unsigned)rand()) << 12) ^ ((unsigned)rand())) & 0xFFFFF;
3739+
char pFileNameIn[32]; sprintf( pFileNameIn, "_%05x_.cnf", Rand );
3740+
char pFileNameOut[32]; sprintf( pFileNameOut, "_%05x_.out", Rand );
37223741
Exa6_Man_t * p = Exa6_ManAlloc( vSimsIn, vSimsOut, nIns, 1+nIns+nDivs, nOuts, nNodes, fVerbose );
37233742
Exa_ManIsNormalized( vSimsIn, vSimsOut );
37243743
Exa6_ManGenCnf( p, pFileNameIn, fOnlyAnd, fFancy, fOrderNodes, fUniqFans );
@@ -4016,8 +4035,9 @@ void Exa_ManExactSynthesis7( Bmc_EsPar_t * pPars, int GateSize )
40164035
int nV = pPars->nVars + pPars->nNodes;
40174036
word pTruth[16]; Abc_TtReadHex( pTruth, pPars->pTtStr );
40184037
Vec_Int_t * vValues = NULL;
4019-
char * pFileNameIn = "_temp_.cnf";
4020-
char * pFileNameOut = "_temp_out.cnf";
4038+
int Rand = ((((unsigned)rand()) << 12) ^ ((unsigned)rand())) & 0xFFFFF;
4039+
char pFileNameIn[32]; sprintf( pFileNameIn, "_%05x_.cnf", Rand );
4040+
char pFileNameOut[32]; sprintf( pFileNameOut, "_%05x_.out", Rand );
40214041
int nClas = Exa7_ManGenCnf( pFileNameIn, pTruth, pPars->nVars, pPars->nNodes, GateSize );
40224042
if ( pPars->fVerbose )
40234043
printf( "CNF with %d variables and %d clauses was dumped into file \"%s\".\n", nMints * nV * nV, nClas, pFileNameIn );

0 commit comments

Comments
 (0)