summaryrefslogtreecommitdiffstats
path: root/src/map/if
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2014-09-17 18:58:20 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2014-09-17 18:58:20 -0700
commit023e92c4700283d4de6e60c5b5054c2d2452b98f (patch)
treeb323c355a95384893ec038af9dcec9f50eff6db2 /src/map/if
parent69827a5a8848ada3ef70bcf25f4f523aed97bded (diff)
downloadabc-023e92c4700283d4de6e60c5b5054c2d2452b98f.tar.gz
abc-023e92c4700283d4de6e60c5b5054c2d2452b98f.tar.bz2
abc-023e92c4700283d4de6e60c5b5054c2d2452b98f.zip
Improvements to Boolean matching.
Diffstat (limited to 'src/map/if')
-rw-r--r--src/map/if/if.h1
-rw-r--r--src/map/if/ifDsd.c65
-rw-r--r--src/map/if/ifTune.c185
3 files changed, 191 insertions, 60 deletions
diff --git a/src/map/if/if.h b/src/map/if/if.h
index 5e0dd1b7..0f217d20 100644
--- a/src/map/if/if.h
+++ b/src/map/if/if.h
@@ -539,6 +539,7 @@ extern If_DsdMan_t * If_DsdManAlloc( int nVars, int nLutSize );
extern void If_DsdManAllocIsops( If_DsdMan_t * p, int nLutSize );
extern void If_DsdManPrint( If_DsdMan_t * p, char * pFileName, int Number, int Support, int fOccurs, int fTtDump, int fVerbose );
extern void If_DsdManTune( If_DsdMan_t * p, int LutSize, int fFast, int fAdd, int fSpec, int fVerbose );
+extern void Id_DsdManTuneStr( If_DsdMan_t * p, char * pStruct, int nConfls, int fVerbose );
extern void If_DsdManFree( If_DsdMan_t * p, int fVerbose );
extern void If_DsdManSave( If_DsdMan_t * p, char * pFileName );
extern If_DsdMan_t * If_DsdManLoad( char * pFileName );
diff --git a/src/map/if/ifDsd.c b/src/map/if/ifDsd.c
index 8fd5e393..d6d0f801 100644
--- a/src/map/if/ifDsd.c
+++ b/src/map/if/ifDsd.c
@@ -2253,6 +2253,71 @@ void If_DsdManTune( If_DsdMan_t * p, int LutSize, int fFast, int fAdd, int fSpec
}
+typedef struct Ifn_Ntk_t_ Ifn_Ntk_t;
+
+extern Ifn_Ntk_t * Ifn_NtkParse( char * pStr );
+extern int Ifn_NtkMatch( Ifn_Ntk_t * p, word * pTruth, int nVars, int nConfls, int fVerbose, int fVeryVerbose );
+extern void Ifn_NtkPrint( Ifn_Ntk_t * p );
+extern int Ifn_NtkLutSizeMax( Ifn_Ntk_t * p );
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Id_DsdManTuneStr( If_DsdMan_t * p, char * pStruct, int nConfls, int fVerbose )
+{
+ int fVeryVerbose = 0;
+ ProgressBar * pProgress = NULL;
+ If_DsdObj_t * pObj;
+ word * pTruth;
+ int i, nVars, Value, LutSize;
+ abctime clk = Abc_Clock();
+ // parse the structure
+ Ifn_Ntk_t * pNtk = Ifn_NtkParse( pStruct );
+ LutSize = Ifn_NtkLutSizeMax(pNtk);
+ // print
+ if ( fVerbose )
+ {
+ printf( "Considering programmable cell: " );
+ Ifn_NtkPrint( pNtk );
+ printf( "Largest LUT size = %d.\n", LutSize );
+ }
+ // clean the attributes
+ If_DsdVecForEachObj( &p->vObjs, pObj, i )
+ pObj->fMark = 0;
+ pProgress = Extra_ProgressBarStart( stdout, Vec_PtrSize(&p->vObjs) );
+ If_DsdVecForEachObj( &p->vObjs, pObj, i )
+ {
+ Extra_ProgressBarUpdate( pProgress, i, NULL );
+ nVars = If_DsdObjSuppSize(pObj);
+ if ( nVars <= LutSize )
+ continue;
+ pTruth = If_DsdManComputeTruth( p, Abc_Var2Lit(i, 0), NULL );
+ if ( fVeryVerbose )
+ Dau_DsdPrintFromTruth( pTruth, nVars );
+ if ( fVerbose )
+ printf( "%6d : %2d ", i, nVars );
+ Value = Ifn_NtkMatch( pNtk, pTruth, nVars, nConfls, fVerbose, fVeryVerbose );
+ if ( fVeryVerbose )
+ printf( "\n" );
+ if ( Value == 0 )
+ continue;
+ If_DsdVecObjSetMark( &p->vObjs, i );
+ }
+ Extra_ProgressBarStop( pProgress );
+ printf( "Finished matching %d functions. ", Vec_PtrSize(&p->vObjs) );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+ if ( fVeryVerbose )
+ If_DsdManPrintDistrib( p );
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/map/if/ifTune.c b/src/map/if/ifTune.c
index 400520e6..817b0a2e 100644
--- a/src/map/if/ifTune.c
+++ b/src/map/if/ifTune.c
@@ -57,10 +57,10 @@ static char * Ifn_Symbs[16] = {
"{}" // 6: PRIME
};
-typedef struct Ift_Obj_t_ Ift_Obj_t;
-typedef struct Ift_Ntk_t_ Ift_Ntk_t;
+typedef struct Ifn_Obj_t_ Ifn_Obj_t;
+typedef struct Ifn_Ntk_t_ Ifn_Ntk_t;
-struct Ift_Obj_t_
+struct Ifn_Obj_t_
{
unsigned Type : 3; // node type
unsigned nFanins : 5; // fanin counter
@@ -68,12 +68,12 @@ struct Ift_Obj_t_
unsigned Var : 16; // current variable
int Fanins[IFN_INS]; // fanin IDs
};
-struct Ift_Ntk_t_
+struct Ifn_Ntk_t_
{
// cell structure
int nInps; // inputs
int nObjs; // objects
- Ift_Obj_t Nodes[2*IFN_INS]; // nodes
+ Ifn_Obj_t Nodes[2*IFN_INS]; // nodes
// constraints
int pConstr[IFN_INS]; // constraint pairs
int nConstr; // number of pairs
@@ -90,8 +90,8 @@ struct Ift_Ntk_t_
word pTtObjs[2*IFN_INS*IFN_WRD]; // object truth tables
};
-static inline word * Ift_ElemTruth( Ift_Ntk_t * p, int i ) { return p->pTtElems + i * Abc_TtWordNum(p->nInps); }
-static inline word * Ift_ObjTruth( Ift_Ntk_t * p, int i ) { return p->pTtObjs + i * p->nWords; }
+static inline word * Ifn_ElemTruth( Ifn_Ntk_t * p, int i ) { return p->pTtElems + i * Abc_TtWordNum(p->nInps); }
+static inline word * Ifn_ObjTruth( Ifn_Ntk_t * p, int i ) { return p->pTtObjs + i * p->nWords; }
// variable ordering
// - primary inputs [0; p->nInps)
@@ -114,7 +114,7 @@ static inline word * Ift_ObjTruth( Ift_Ntk_t * p, int i ) { return p->pTt
SeeAlso []
***********************************************************************/
-int Ifn_Prepare( Ift_Ntk_t * p, word * pTruth, int nVars )
+int Ifn_Prepare( Ifn_Ntk_t * p, word * pTruth, int nVars )
{
int i, fVerbose = 0;
assert( nVars <= p->nInps );
@@ -140,7 +140,7 @@ int Ifn_Prepare( Ift_Ntk_t * p, word * pTruth, int nVars )
memset( p->Values, 0xFF, sizeof(int) * p->nPars );
return p->nPars;
}
-void Ifn_NtkPrint( Ift_Ntk_t * p )
+void Ifn_NtkPrint( Ifn_Ntk_t * p )
{
int i, k;
if ( p == NULL )
@@ -158,6 +158,14 @@ void Ifn_NtkPrint( Ift_Ntk_t * p )
}
printf( "\n" );
}
+int Ifn_NtkLutSizeMax( Ifn_Ntk_t * p )
+{
+ int i, LutSize = 0;
+ for ( i = p->nInps; i < p->nObjs; i++ )
+ if ( p->Nodes[i].Type == IF_DSD_PRIME )
+ LutSize = Abc_MaxInt( LutSize, (int)p->Nodes[i].nFanins );
+ return LutSize;
+}
/**Function*************************************************************
@@ -181,6 +189,8 @@ int Ifn_ManStrCheck( char * pStr, int * pnInps, int * pnObjs )
pStr[i] == '<' || pStr[i] == '>' ||
pStr[i] == '{' || pStr[i] == '}' )
continue;
+ if ( pStr[i] >= 'A' && pStr[i] <= 'Z' )
+ continue;
if ( pStr[i] >= 'a' && pStr[i] <= 'z' )
{
if ( pStr[i+1] == '=' )
@@ -200,6 +210,8 @@ int Ifn_ManStrCheck( char * pStr, int * pnInps, int * pnObjs )
pStr[i] == '<' || pStr[i] == '>' ||
pStr[i] == '{' || pStr[i] == '}' )
continue;
+ if ( pStr[i] >= 'A' && pStr[i] <= 'Z' )
+ continue;
if ( pStr[i] >= 'a' && pStr[i] <= 'z' )
{
if ( pStr[i+1] != '=' && Marks[pStr[i] - 'a'] != 2 )
@@ -228,11 +240,11 @@ int Ifn_ManStrCheck( char * pStr, int * pnInps, int * pnObjs )
*pnObjs = MaxDef;
return 1;
}
-Ift_Ntk_t * Ifn_ManStrParse( char * pStr )
+Ifn_Ntk_t * Ifn_NtkParse( char * pStr )
{
int i, k, n, f, nFans, iFan;
- static Ift_Ntk_t P, * p = &P;
- memset( p, 0, sizeof(Ift_Ntk_t) );
+ static Ifn_Ntk_t P, * p = &P;
+ memset( p, 0, sizeof(Ifn_Ntk_t) );
if ( !Ifn_ManStrCheck(pStr, &p->nInps, &p->nObjs) )
return NULL;
if ( p->nInps > IFN_INS )
@@ -293,6 +305,18 @@ Ift_Ntk_t * Ifn_ManStrParse( char * pStr )
}
// truth tables
Abc_TtElemInit2( p->pTtElems, p->nInps );
+ // parse constraints
+ p->nConstr = 0;
+ for ( i = 0; i < p->nInps; i++ )
+ for ( k = 0; pStr[k]; k++ )
+ if ( pStr[k] == 'A' + i && pStr[k-1] == ';' )
+ {
+ p->pConstr[p->nConstr++] = ((int)(pStr[k] - 'A') << 16) | (int)(pStr[k+1] - 'A');
+// printf( "Added constraint (%c < %c)\n", pStr[k], pStr[k+1] );
+ }
+// if ( p->nConstr )
+// printf( "Total constraints = %d\n", p->nConstr );
+
/*
// constraints
p->nConstr = 5;
@@ -318,7 +342,7 @@ Ift_Ntk_t * Ifn_ManStrParse( char * pStr )
SeeAlso []
***********************************************************************/
-word * Ift_NtkDeriveTruth( Ift_Ntk_t * p, int * pValues )
+word * Ifn_NtkDeriveTruth( Ifn_Ntk_t * p, int * pValues )
{
int i, v, f, iVar, iStart;
// elementary variables
@@ -330,35 +354,35 @@ word * Ift_NtkDeriveTruth( Ift_Ntk_t * p, int * pValues )
if ( p->Values[iStart+v] )
iVar += (1 << v);
// assign variable
- Abc_TtCopy( Ift_ObjTruth(p, i), Ift_ElemTruth(p, iVar), p->nWords, 0 );
+ Abc_TtCopy( Ifn_ObjTruth(p, i), Ifn_ElemTruth(p, iVar), p->nWords, 0 );
}
// internal variables
for ( i = p->nInps; i < p->nObjs; i++ )
{
int nFans = p->Nodes[i].nFanins;
int * pFans = p->Nodes[i].Fanins;
- word * pTruth = Ift_ObjTruth( p, i );
+ word * pTruth = Ifn_ObjTruth( p, i );
if ( p->Nodes[i].Type == IF_DSD_AND )
{
Abc_TtFill( pTruth, p->nWords );
for ( f = 0; f < nFans; f++ )
- Abc_TtAnd( pTruth, pTruth, Ift_ObjTruth(p, pFans[f]), p->nWords, 0 );
+ Abc_TtAnd( pTruth, pTruth, Ifn_ObjTruth(p, pFans[f]), p->nWords, 0 );
}
else if ( p->Nodes[i].Type == IF_DSD_XOR )
{
Abc_TtClear( pTruth, p->nWords );
for ( f = 0; f < nFans; f++ )
- Abc_TtXor( pTruth, pTruth, Ift_ObjTruth(p, pFans[f]), p->nWords, 0 );
+ Abc_TtXor( pTruth, pTruth, Ifn_ObjTruth(p, pFans[f]), p->nWords, 0 );
}
else if ( p->Nodes[i].Type == IF_DSD_MUX )
{
assert( nFans == 3 );
- Abc_TtMux( pTruth, Ift_ObjTruth(p, pFans[0]), Ift_ObjTruth(p, pFans[1]), Ift_ObjTruth(p, pFans[2]), p->nWords );
+ Abc_TtMux( pTruth, Ifn_ObjTruth(p, pFans[0]), Ifn_ObjTruth(p, pFans[1]), Ifn_ObjTruth(p, pFans[2]), p->nWords );
}
else if ( p->Nodes[i].Type == IF_DSD_PRIME )
{
int nValues = (1 << nFans);
- word * pTemp = Ift_ObjTruth(p, p->nObjs);
+ word * pTemp = Ifn_ObjTruth(p, p->nObjs);
Abc_TtClear( pTruth, p->nWords );
for ( v = 0; v < nValues; v++ )
{
@@ -367,16 +391,16 @@ word * Ift_NtkDeriveTruth( Ift_Ntk_t * p, int * pValues )
Abc_TtFill( pTemp, p->nWords );
for ( f = 0; f < nFans; f++ )
if ( (v >> f) & 1 )
- Abc_TtAnd( pTemp, pTemp, Ift_ObjTruth(p, pFans[f]), p->nWords, 0 );
+ Abc_TtAnd( pTemp, pTemp, Ifn_ObjTruth(p, pFans[f]), p->nWords, 0 );
else
- Abc_TtSharp( pTemp, pTemp, Ift_ObjTruth(p, pFans[f]), p->nWords );
+ Abc_TtSharp( pTemp, pTemp, Ifn_ObjTruth(p, pFans[f]), p->nWords );
Abc_TtOr( pTruth, pTruth, pTemp, p->nWords );
}
}
else assert( 0 );
//Dau_DsdPrintFromTruth( pTruth, p->nVars );
}
- return Ift_ObjTruth(p, p->nObjs-1);
+ return Ifn_ObjTruth(p, p->nObjs-1);
}
/**Function*************************************************************
@@ -390,7 +414,7 @@ word * Ift_NtkDeriveTruth( Ift_Ntk_t * p, int * pValues )
SeeAlso []
***********************************************************************/
-void Ift_TtComparisonConstr( word * pTruth, int nVars, int fMore, int fEqual )
+void Ifn_TtComparisonConstr( word * pTruth, int nVars, int fMore, int fEqual )
{
word Cond[4], Equa[4], Temp[4];
word s_TtElems[8][4] = {
@@ -433,7 +457,7 @@ void Ift_TtComparisonConstr( word * pTruth, int nVars, int fMore, int fEqual )
SeeAlso []
***********************************************************************/
-void Ift_AddClause( sat_solver * pSat, int * pBeg, int * pEnd )
+void Ifn_AddClause( sat_solver * pSat, int * pBeg, int * pEnd )
{
int fVerbose = 0;
int RetValue = sat_solver_addclause( pSat, pBeg, pEnd );
@@ -445,7 +469,7 @@ void Ift_AddClause( sat_solver * pSat, int * pBeg, int * pEnd )
}
assert( RetValue );
}
-void Ift_NtkAddConstrOne( sat_solver * pSat, Vec_Int_t * vCover, int * pVars, int nVars )
+void Ifn_NtkAddConstrOne( sat_solver * pSat, Vec_Int_t * vCover, int * pVars, int nVars )
{
int k, c, Cube, Literal, nLits, pLits[IFN_INS];
Vec_IntForEachEntry( vCover, Cube, c )
@@ -461,12 +485,12 @@ void Ift_NtkAddConstrOne( sat_solver * pSat, Vec_Int_t * vCover, int * pVars, in
else if ( Literal != 0 )
assert( 0 );
}
- Ift_AddClause( pSat, pLits, pLits + nLits );
+ Ifn_AddClause( pSat, pLits, pLits + nLits );
}
}
-void Ift_NtkAddConstraints( Ift_Ntk_t * p, sat_solver * pSat )
+void Ifn_NtkAddConstraints( Ifn_Ntk_t * p, sat_solver * pSat )
{
- int fAddConstr = 0;
+ int fAddConstr = 1;
Vec_Int_t * vCover = Vec_IntAlloc( 0 );
word uTruth = Abc_Tt6Stretch( ~Abc_Tt6Mask(p->nVars), p->nParsVNum );
assert( p->nParsVNum <= 4 );
@@ -481,7 +505,7 @@ void Ift_NtkAddConstraints( Ift_Ntk_t * p, sat_solver * pSat )
{
for ( k = 0; k < p->nParsVNum; k++ )
pVars[k] = p->nParsVIni + i * p->nParsVNum + k;
- Ift_NtkAddConstrOne( pSat, vCover, pVars, p->nParsVNum );
+ Ifn_NtkAddConstrOne( pSat, vCover, pVars, p->nParsVNum );
}
}
// ordering constraints
@@ -490,7 +514,7 @@ void Ift_NtkAddConstraints( Ift_Ntk_t * p, sat_solver * pSat )
word pTruth[4];
int i, k, RetValue, pVars[2*IFN_INS];
int fForceDiff = (p->nVars == p->nInps);
- Ift_TtComparisonConstr( pTruth, p->nParsVNum, fForceDiff, fForceDiff );
+ Ifn_TtComparisonConstr( pTruth, p->nParsVNum, fForceDiff, fForceDiff );
RetValue = Kit_TruthIsop( (unsigned *)pTruth, 2*p->nParsVNum, vCover, 0 );
assert( RetValue == 0 );
// Kit_TruthIsopPrintCover( vCover, 2*p->nParsVNum, 0 );
@@ -503,7 +527,7 @@ void Ift_NtkAddConstraints( Ift_Ntk_t * p, sat_solver * pSat )
pVars[2*k+0] = p->nParsVIni + iVar1 * p->nParsVNum + k;
pVars[2*k+1] = p->nParsVIni + iVar2 * p->nParsVNum + k;
}
- Ift_NtkAddConstrOne( pSat, vCover, pVars, 2*p->nParsVNum );
+ Ifn_NtkAddConstrOne( pSat, vCover, pVars, 2*p->nParsVNum );
// printf( "added constraint with %d clauses for %d and %d\n", Vec_IntSize(vCover), iVar1, iVar2 );
}
}
@@ -521,7 +545,7 @@ void Ift_NtkAddConstraints( Ift_Ntk_t * p, sat_solver * pSat )
SeeAlso []
***********************************************************************/
-int Ift_NtkAddClauses( Ift_Ntk_t * p, int * pValues, sat_solver * pSat )
+int Ifn_NtkAddClauses( Ifn_Ntk_t * p, int * pValues, sat_solver * pSat )
{
int i, f, v, nLits, pLits[IFN_INS+2], pLits2[IFN_INS+2];
// assign new variables
@@ -548,7 +572,7 @@ int Ift_NtkAddClauses( Ift_Ntk_t * p, int * pValues, sat_solver * pSat )
// add clause literals
for ( f = 0; f < p->nParsVNum; f++ )
pLits[f+1] = Abc_Var2Lit( iParStart + f, (v >> f) & 1 );
- Ift_AddClause( pSat, pLits, pLits+p->nParsVNum+1 );
+ Ifn_AddClause( pSat, pLits, pLits+p->nParsVNum+1 );
}
}
//printf( "\n" );
@@ -566,18 +590,50 @@ int Ift_NtkAddClauses( Ift_Ntk_t * p, int * pValues, sat_solver * pSat )
// add small clause
pLits2[0] = Abc_Var2Lit( p->Nodes[i].Var, 1 );
pLits2[1] = Abc_Var2Lit( p->Nodes[pFans[f]].Var, 0 );
- Ift_AddClause( pSat, pLits2, pLits2 + 2 );
+ Ifn_AddClause( pSat, pLits2, pLits2 + 2 );
}
// add big clause
- Ift_AddClause( pSat, pLits, pLits + nLits );
+ Ifn_AddClause( pSat, pLits, pLits + nLits );
}
else if ( p->Nodes[i].Type == IF_DSD_XOR )
{
- assert( 0 );
+ int m, nMints = (1 << (nFans+1));
+ for ( m = 0; m < nMints; m++ )
+ {
+ // skip even
+ int Count = 0;
+ for ( v = 0; v <= nFans; v++ )
+ Count += ((m >> v) & 1);
+ if ( (Count & 1) == 0 )
+ continue;
+ // generate minterm
+ pLits[0] = Abc_Var2Lit( p->Nodes[i].Var, (m >> nFans) & 1 );
+ for ( v = 0; v < nFans; v++ )
+ pLits[v+1] = Abc_Var2Lit( p->Nodes[pFans[v]].Var, (m >> v) & 1 );
+ Ifn_AddClause( pSat, pLits, pLits + nFans + 1 );
+ }
}
else if ( p->Nodes[i].Type == IF_DSD_MUX )
{
- assert( 0 );
+ pLits[0] = Abc_Var2Lit( p->Nodes[i].Var, 0 );
+ pLits[1] = Abc_Var2Lit( p->Nodes[pFans[0]].Var, 1 ); // ctrl
+ pLits[2] = Abc_Var2Lit( p->Nodes[pFans[1]].Var, 1 );
+ Ifn_AddClause( pSat, pLits, pLits + 3 );
+
+ pLits[0] = Abc_Var2Lit( p->Nodes[i].Var, 1 );
+ pLits[1] = Abc_Var2Lit( p->Nodes[pFans[0]].Var, 1 ); // ctrl
+ pLits[2] = Abc_Var2Lit( p->Nodes[pFans[1]].Var, 0 );
+ Ifn_AddClause( pSat, pLits, pLits + 3 );
+
+ pLits[0] = Abc_Var2Lit( p->Nodes[i].Var, 0 );
+ pLits[1] = Abc_Var2Lit( p->Nodes[pFans[0]].Var, 0 ); // ctrl
+ pLits[2] = Abc_Var2Lit( p->Nodes[pFans[2]].Var, 1 );
+ Ifn_AddClause( pSat, pLits, pLits + 3 );
+
+ pLits[0] = Abc_Var2Lit( p->Nodes[i].Var, 1 );
+ pLits[1] = Abc_Var2Lit( p->Nodes[pFans[0]].Var, 0 ); // ctrl
+ pLits[2] = Abc_Var2Lit( p->Nodes[pFans[2]].Var, 0 );
+ Ifn_AddClause( pSat, pLits, pLits + 3 );
}
else if ( p->Nodes[i].Type == IF_DSD_PRIME )
{
@@ -598,9 +654,9 @@ int Ift_NtkAddClauses( Ift_Ntk_t * p, int * pValues, sat_solver * pSat )
pLits2[nLits] = Abc_Var2Lit( iParStart + v, 0 );
nLits++;
if ( pValues[i] != 0 )
- Ift_AddClause( pSat, pLits2, pLits2 + nLits );
+ Ifn_AddClause( pSat, pLits2, pLits2 + nLits );
if ( pValues[i] != 1 )
- Ift_AddClause( pSat, pLits, pLits + nLits );
+ Ifn_AddClause( pSat, pLits, pLits + nLits );
}
}
else assert( 0 );
@@ -620,7 +676,7 @@ int Ift_NtkAddClauses( Ift_Ntk_t * p, int * pValues, sat_solver * pSat )
SeeAlso []
***********************************************************************/
-void Ift_SatPrintStatus( sat_solver * p, int Iter, int status, int iMint, int Value, abctime clk )
+void Ifn_SatPrintStatus( sat_solver * p, int Iter, int status, int iMint, int Value, abctime clk )
{
printf( "Iter = %5d ", Iter );
printf( "Mint = %5d ", iMint );
@@ -636,19 +692,23 @@ void Ift_SatPrintStatus( sat_solver * p, int Iter, int status, int iMint, int Va
printf( "status = undec" );
Abc_PrintTime( 1, "", clk );
}
-void Ift_SatPrintConfig( Ift_Ntk_t * p, sat_solver * pSat )
+void Ifn_SatPrintConfig( Ifn_Ntk_t * p, sat_solver * pSat )
{
- int v;
+ int v, i;
for ( v = p->nObjs; v < p->nPars; v++ )
{
- if ( v >= p->nParsVIni && (v - p->nParsVIni) % p->nParsVNum == 0 )
+ for ( i = p->nInps; i < p->nObjs; i++ )
+ if ( p->Nodes[i].Type == IF_DSD_PRIME && (int)p->Nodes[i].iFirst == v )
+ break;
+ if ( i < p->nObjs )
+ printf( " " );
+ else if ( v >= p->nParsVIni && (v - p->nParsVIni) % p->nParsVNum == 0 )
printf( " %d=", (v - p->nParsVIni) / p->nParsVNum );
printf( "%d", sat_solver_var_value(pSat, v) );
}
- printf( "\n" );
}
-int Ift_NtkMatch( Ift_Ntk_t * p, word * pTruth, int nVars, int fVerbose )
+int Ifn_NtkMatch( Ifn_Ntk_t * p, word * pTruth, int nVars, int nConfls, int fVerbose, int fVeryVerbose )
{
word * pTruth1;
int RetValue = 0;
@@ -659,9 +719,9 @@ int Ift_NtkMatch( Ift_Ntk_t * p, word * pTruth, int nVars, int fVerbose )
sat_solver * pSat = sat_solver_new();
Ifn_Prepare( p, pTruth, nVars );
sat_solver_setnvars( pSat, p->nPars );
- Ift_NtkAddConstraints( p, pSat );
- if ( fVerbose )
- Ift_SatPrintStatus( pSat, 0, l_True, -1, -1, Abc_Clock() - clk );
+ Ifn_NtkAddConstraints( p, pSat );
+ if ( fVeryVerbose )
+ Ifn_SatPrintStatus( pSat, 0, l_True, -1, -1, Abc_Clock() - clk );
for ( i = 0; i < nIterMax; i++ )
{
// get variable assignment
@@ -669,37 +729,41 @@ int Ift_NtkMatch( Ift_Ntk_t * p, word * pTruth, int nVars, int fVerbose )
p->Values[v] = v < p->nVars ? (iMint >> v) & 1 : -1;
p->Values[p->nObjs-1] = Abc_TtGetBit( pTruth, iMint );
// derive clauses
- if ( !Ift_NtkAddClauses( p, p->Values, pSat ) )
+ if ( !Ifn_NtkAddClauses( p, p->Values, pSat ) )
break;
// find assignment of parameters
// clk2 = Abc_Clock();
- status = sat_solver_solve( pSat, NULL, NULL, 0, 0, 0, 0 );
+ status = sat_solver_solve( pSat, NULL, NULL, nConfls, 0, 0, 0 );
// clkSat += Abc_Clock() - clk2;
- if ( fVerbose )
- Ift_SatPrintStatus( pSat, i+1, status, iMint, p->Values[p->nObjs-1], Abc_Clock() - clk );
- if ( status == l_False )
+ if ( fVeryVerbose )
+ Ifn_SatPrintStatus( pSat, i+1, status, iMint, p->Values[p->nObjs-1], Abc_Clock() - clk );
+ if ( status != l_True )
break;
- assert( status == l_True );
// collect assignment
for ( v = p->nObjs; v < p->nPars; v++ )
p->Values[v] = sat_solver_var_value(pSat, v);
// find truth table
// clk2 = Abc_Clock();
- pTruth1 = Ift_NtkDeriveTruth( p, p->Values );
+ pTruth1 = Ifn_NtkDeriveTruth( p, p->Values );
// clkTru += Abc_Clock() - clk2;
Abc_TtXor( pTruth1, pTruth1, p->pTruth, p->nWords, 0 );
// find mismatch if present
iMint = Abc_TtFindFirstBit( pTruth1, p->nVars );
if ( iMint == -1 )
{
- Ift_SatPrintConfig( p, pSat );
RetValue = 1;
break;
}
}
assert( i < nIterMax );
+ if ( fVerbose )
+ {
+ printf( "%s Iter =%4d. Confl = %6d. ", RetValue ? "yes":"no ", i, sat_solver_nconflicts(pSat) );
+ if ( RetValue )
+ Ifn_SatPrintConfig( p, pSat );
+ printf( "\n" );
+ }
sat_solver_delete( pSat );
- printf( "Matching = %d Iters = %d. ", RetValue, i );
// Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
// Abc_PrintTime( 1, "Sat", clkSat );
// Abc_PrintTime( 1, "Tru", clkTru );
@@ -731,15 +795,16 @@ void Ifn_NtkRead()
// word * pTruth = Dau_DsdToTruth( "(abc)", nVars );
// char * pStr = "e={abc};f={ed};";
// char * pStr = "d={ab};e={cd};";
- char * pStr = "j=(ab);k={jcde};l=(kf);m={lghi};";
+// char * pStr = "j=(ab);k={jcde};l=(kf);m={lghi};";
// char * pStr = "i={abc};j={ide};k={ifg};l={jkh};";
// char * pStr = "h={abcde};i={abcdf};j=<ghi>;";
// char * pStr = "g=<abc>;h=<ade>;i={fgh};";
- Ift_Ntk_t * p = Ifn_ManStrParse( pStr );
+ char * pStr = "i=<abc>;j=(def);k=[gh];l={ijk};";
+ Ifn_Ntk_t * p = Ifn_NtkParse( pStr );
Ifn_NtkPrint( p );
Dau_DsdPrintFromTruth( pTruth, nVars );
// get the given function
- RetValue = Ift_NtkMatch( p, pTruth, nVars, 1 );
+ RetValue = Ifn_NtkMatch( p, pTruth, nVars, 0, 1, 1 );
}
////////////////////////////////////////////////////////////////////////