diff options
author | Mathias Soeken <mathias.soeken@epfl.ch> | 2016-08-29 22:40:30 +0200 |
---|---|---|
committer | Mathias Soeken <mathias.soeken@epfl.ch> | 2016-08-29 22:40:30 +0200 |
commit | a46af9de7b8fd6465f4a89e0842bf8f3313b06b0 (patch) | |
tree | 43cd7fc613f4e92470586ab8c40f7d93a11f8643 /src | |
parent | 7e3032c0dd5333f449d76056663408357e750706 (diff) | |
download | abc-a46af9de7b8fd6465f4a89e0842bf8f3313b06b0.tar.gz abc-a46af9de7b8fd6465f4a89e0842bf8f3313b06b0.tar.bz2 abc-a46af9de7b8fd6465f4a89e0842bf8f3313b06b0.zip |
Improvements to BMS.
Diffstat (limited to 'src')
-rw-r--r-- | src/base/abci/abcExact.c | 273 |
1 files changed, 211 insertions, 62 deletions
diff --git a/src/base/abci/abcExact.c b/src/base/abci/abcExact.c index 0ba83e84..6a7becb8 100644 --- a/src/base/abci/abcExact.c +++ b/src/base/abci/abcExact.c @@ -205,12 +205,14 @@ struct Ses_Man_t_ int fExtractVerbose; /* be verbose about solution extraction */ int fSatVerbose; /* be verbose about SAT solving */ int fReasonVerbose; /* be verbose about give-up reasons */ + word pTtValues[4]; /* truth table values to assign */ int nGates; /* number of gates */ int nStartGates; /* number of gates to start search (-1), i.e., to start from 1 gate, one needs to specify 0 */ int nMaxGates; /* maximum number of gates given max. delay and arrival times */ int fDecStructure; /* set to 1 or higher if nSpecFunc = 1 and f = x_i OP g(X \ {x_i}), otherwise 0 (determined when solving) */ int pDecVars; /* mask of variables that can be decomposed at top-level */ + word pTtObjs[100]; /* temporary truth tables */ int nSimVars; /* number of simulation vars x(i, t) */ int nOutputVars; /* number of output variables g(h, i) */ @@ -965,6 +967,52 @@ static inline int Ses_ManDepthVar( Ses_Man_t * pSes, int i, int j ) /**Function************************************************************* + Synopsis [Compute truth table from a solution.] + +***********************************************************************/ +static word * Ses_ManDeriveTruth( Ses_Man_t * pSes, char * pSol, int fInvert ) +{ + int i, f, j, k, w, nGates = pSol[ABC_EXACT_SOL_NGATES]; + char * p; + word * pTruth, * pTruth0, * pTruth1; + assert( pSol[ABC_EXACT_SOL_NFUNC] == 1 ); + + p = pSol + 3; + + memset( pSes->pTtObjs, 0, sizeof( word ) * 4 * nGates ); + + for ( i = 0; i < nGates; ++i ) + { + f = *p++; + assert( *p++ == 2 ); + j = *p++; + k = *p++; + + pTruth0 = j < pSes->nSpecVars ? &s_Truths8[j << 2] : &pSes->pTtObjs[( j - pSes->nSpecVars ) << 2]; + pTruth1 = k < pSes->nSpecVars ? &s_Truths8[k << 2] : &pSes->pTtObjs[( k - pSes->nSpecVars ) << 2]; + + pTruth = &pSes->pTtObjs[i << 2]; + + if ( f & 1 ) + for ( w = 0; w < pSes->nSpecWords; ++w ) + pTruth[w] |= ~pTruth0[w] & pTruth1[w]; + if ( ( f >> 1 ) & 1 ) + for ( w = 0; w < pSes->nSpecWords; ++w ) + pTruth[w] |= pTruth0[w] & ~pTruth1[w]; + if ( ( f >> 2 ) & 1 ) + for ( w = 0; w < pSes->nSpecWords; ++w ) + pTruth[w] |= pTruth0[w] & pTruth1[w]; + } + + assert( Abc_Lit2Var( *p ) == nGates - 1 ); + if ( fInvert && Abc_LitIsCompl( *p ) ) + Abc_TtNot( pTruth, pSes->nSpecWords ); + + return pTruth; +} + +/**Function************************************************************* + Synopsis [Setup variables to find network with nGates gates.] ***********************************************************************/ @@ -1033,6 +1081,47 @@ static inline void Ses_ManCreateMainClause( Ses_Man_t * pSes, int t, int i, int sat_solver_addclause( pSes->pSat, pLits, pLits + ctr ); } +static int inline Ses_ManCreateTruthTableClause( Ses_Man_t * pSes, int t ) +{ + int i, j, k, h; + int pLits[3]; + + for ( i = 0; i < pSes->nGates; ++i ) + { + /* main clauses */ + for ( j = 0; j < pSes->nSpecVars + i; ++j ) + for ( k = j + 1; k < pSes->nSpecVars + i; ++k ) + { + Ses_ManCreateMainClause( pSes, t, i, j, k, 0, 0, 1 ); + Ses_ManCreateMainClause( pSes, t, i, j, k, 0, 1, 0 ); + Ses_ManCreateMainClause( pSes, t, i, j, k, 0, 1, 1 ); + Ses_ManCreateMainClause( pSes, t, i, j, k, 1, 0, 0 ); + Ses_ManCreateMainClause( pSes, t, i, j, k, 1, 0, 1 ); + Ses_ManCreateMainClause( pSes, t, i, j, k, 1, 1, 0 ); + Ses_ManCreateMainClause( pSes, t, i, j, k, 1, 1, 1 ); + } + + /* output clauses */ + if ( pSes->nSpecFunc != 1 ) + for ( h = 0; h < pSes->nSpecFunc; ++h ) + { + pLits[0] = Abc_Var2Lit( Ses_ManOutputVar( pSes, h, i ), 1 ); + pLits[1] = Abc_Var2Lit( Ses_ManSimVar( pSes, i, t ), 1 - Abc_TtGetBit( &pSes->pSpec[h << 2], t + 1 ) ); + if ( !sat_solver_addclause( pSes->pSat, pLits, pLits + 2 ) ) + return 0; + } + } + + if ( pSes->nSpecFunc == 1 ) + { + pLits[0] = Abc_Var2Lit( Ses_ManSimVar( pSes, pSes->nGates - 1, t ), 1 - Abc_TtGetBit( pSes->pSpec, t + 1 ) ); + if ( !sat_solver_addclause( pSes->pSat, pLits, pLits + 1 ) ) + return 0; + } + + return 1; +} + static int Ses_ManCreateClauses( Ses_Man_t * pSes ) { extern int Extra_TruthVarsSymm( unsigned * pTruth, int nVars, int iVar0, int iVar1 ); @@ -1043,38 +1132,9 @@ static int Ses_ManCreateClauses( Ses_Man_t * pSes ) for ( t = 0; t < pSes->nRows; ++t ) { - for ( i = 0; i < pSes->nGates; ++i ) - { - /* main clauses */ - for ( j = 0; j < pSes->nSpecVars + i; ++j ) - for ( k = j + 1; k < pSes->nSpecVars + i; ++k ) - { - Ses_ManCreateMainClause( pSes, t, i, j, k, 0, 0, 1 ); - Ses_ManCreateMainClause( pSes, t, i, j, k, 0, 1, 0 ); - Ses_ManCreateMainClause( pSes, t, i, j, k, 0, 1, 1 ); - Ses_ManCreateMainClause( pSes, t, i, j, k, 1, 0, 0 ); - Ses_ManCreateMainClause( pSes, t, i, j, k, 1, 0, 1 ); - Ses_ManCreateMainClause( pSes, t, i, j, k, 1, 1, 0 ); - Ses_ManCreateMainClause( pSes, t, i, j, k, 1, 1, 1 ); - } - - /* output clauses */ - if ( pSes->nSpecFunc != 1 ) - for ( h = 0; h < pSes->nSpecFunc; ++h ) - { - pLits[0] = Abc_Var2Lit( Ses_ManOutputVar( pSes, h, i ), 1 ); - pLits[1] = Abc_Var2Lit( Ses_ManSimVar( pSes, i, t ), 1 - Abc_TtGetBit( &pSes->pSpec[h << 2], t + 1 ) ); - if ( !sat_solver_addclause( pSes->pSat, pLits, pLits + 2 ) ) - return 0; - } - } - - if ( pSes->nSpecFunc == 1 ) - { - pLits[0] = Abc_Var2Lit( Ses_ManSimVar( pSes, pSes->nGates - 1, t ), 1 - Abc_TtGetBit( pSes->pSpec, t + 1 ) ); - if ( !sat_solver_addclause( pSes->pSat, pLits, pLits + 1 ) ) + if ( Abc_TtGetBit( pSes->pTtValues, t ) ) + if ( !Ses_ManCreateTruthTableClause( pSes, t ) ) return 0; - } } /* if there is only one output, we know it must point to the last gate */ @@ -1541,6 +1601,10 @@ static char * Ses_ManExtractSolution( Ses_Man_t * pSes ) /* have we used all the fields? */ assert( ( p - pSol ) == nSol ); + /* printf( "found network: " ); */ + /* Abc_TtPrintHexRev( stdout, Ses_ManDeriveTruth( pSes, pSol, 1 ), pSes->nSpecVars ); */ + /* printf( "\n" ); */ + return pSol; } @@ -1980,11 +2044,52 @@ static void Ses_AdjustDepthAndArrivalTimes( Ses_Man_t * pSes, int nGates ) Abc_ExactAdjustDepthAndArrivalTimes( pSes->nSpecVars, nGates, pSes->nMaxDepthTmp, &pSes->nMaxDepth, pSes->pArrTimeProfileTmp, pSes->pArrTimeProfile, pSes->nArrTimeMax - 1 ); } -static int Ses_ManFindMinimumSize( Ses_Man_t * pSes ) +/* return: (2: continue, 1: found, 0: gave up) */ +static int Ses_ManFindNetworkExact( Ses_Man_t * pSes, int nGates ) { - int nGates = pSes->nStartGates, f, fRes, fSat, nOffset = 0, fFirst = 1; + int f, fSat; abctime timeStart; + /* solve */ + timeStart = Abc_Clock(); + Ses_ManCreateVars( pSes, nGates ); + f = Ses_ManCreateDepthClauses( pSes ); + pSes->timeInstance += ( Abc_Clock() - timeStart ); + if ( !f ) return 2; /* proven UNSAT while creating clauses */ + + /* first solve */ + fSat = Ses_ManSolve( pSes ); + if ( fSat == 0 ) + return 2; /* UNSAT, continue with next # of gates */ + else if ( fSat == 2 ) + { + pSes->fHitResLimit = 1; + return 0; + } + + timeStart = Abc_Clock(); + f = Ses_ManCreateClauses( pSes ); + pSes->timeInstance += ( Abc_Clock() - timeStart ); + if ( !f ) return 2; /* proven UNSAT while creating clauses */ + + fSat = Ses_ManSolve( pSes ); + if ( fSat == 1 ) + return 1; + else if ( fSat == 2 ) + { + pSes->fHitResLimit = 1; + return 0; + } + + return 2; /* UNSAT continue */ +} + +static int Ses_ManFindMinimumSize( Ses_Man_t * pSes ) +{ + int nGates = pSes->nStartGates, fRes, fSat, nOffset = 0, fFirst = 1, iMint; + char * pSol; + word pTruth[4]; + /* store whether call was unsuccessful due to resource limit and not due to impossible constraint */ pSes->fHitResLimit = 0; @@ -1999,6 +2104,9 @@ static int Ses_ManFindMinimumSize( Ses_Man_t * pSes ) //Ses_ManStoreDepthAndArrivalTimes( pSes ); + //memset( pSes->pTtValues, (word)~0, 4 * sizeof( word ) ); + memset( pSes->pTtValues, 0, 4 * sizeof( word ) ); + while ( true ) { ++nGates; @@ -2016,41 +2124,82 @@ static int Ses_ManFindMinimumSize( Ses_Man_t * pSes ) break; } - /* solve */ - timeStart = Abc_Clock(); - Ses_ManCreateVars( pSes, nGates ); - f = Ses_ManCreateDepthClauses( pSes ); - pSes->timeInstance += ( Abc_Clock() - timeStart ); - if ( !f ) continue; /* proven UNSAT while creating clauses */ - - /* first solve */ - fSat = Ses_ManSolve( pSes ); - if ( fSat == 0 ) - continue; /* UNSAT, continue with next # of gates */ - else if ( fSat == 2 ) + fRes = Ses_ManFindNetworkExact( pSes, nGates ); + if ( fRes == 2 ) continue; /* unsat */ + if ( fRes == 0 ) break; /* undef */ + + while ( true ) { - pSes->fHitResLimit = 1; - fRes = 0; - break; - } + pSol = Ses_ManExtractSolution( pSes ); + Abc_TtXor( pTruth, Ses_ManDeriveTruth( pSes, pSol, 0 ), pSes->pSpec, pSes->nSpecWords, 0 ); + ABC_FREE( pSol ); + iMint = Abc_TtFindFirstBit( pTruth, pSes->nSpecVars ); - timeStart = Abc_Clock(); - f = Ses_ManCreateClauses( pSes ); - pSes->timeInstance += ( Abc_Clock() - timeStart ); - if ( !f ) continue; /* proven UNSAT while creating clauses */ + if ( iMint == -1 ) + { + assert( fRes == 1 ); + break; + } + + assert( iMint ); + Abc_TtSetBit( pSes->pTtValues, iMint - 1 ); + if ( !Ses_ManCreateTruthTableClause( pSes, iMint - 1 ) ) /* UNSAT, continue */ + { + fRes = 2; + break; + } + + if ( ( fSat = Ses_ManSolve( pSes ) ) == 1 ) continue; + + if ( fSat == 0 ) + fRes = 2; + else if ( fSat == 2 ) + { + pSes->fHitResLimit = 1; + fRes = 0; + } - fSat = Ses_ManSolve( pSes ); - if ( fSat == 1 ) - { - fRes = 1; break; } - else if ( fSat == 2 ) - { - pSes->fHitResLimit = 1; - fRes = 0; + + if ( fRes != 2 ) break; - } + + /* /\* solve *\/ */ + /* timeStart = Abc_Clock(); */ + /* Ses_ManCreateVars( pSes, nGates ); */ + /* f = Ses_ManCreateDepthClauses( pSes ); */ + /* pSes->timeInstance += ( Abc_Clock() - timeStart ); */ + /* if ( !f ) continue; /\* proven UNSAT while creating clauses *\/ */ + + /* /\* first solve *\/ */ + /* fSat = Ses_ManSolve( pSes ); */ + /* if ( fSat == 0 ) */ + /* continue; /\* UNSAT, continue with next # of gates *\/ */ + /* else if ( fSat == 2 ) */ + /* { */ + /* pSes->fHitResLimit = 1; */ + /* fRes = 0; */ + /* break; */ + /* } */ + + /* timeStart = Abc_Clock(); */ + /* f = Ses_ManCreateClauses( pSes ); */ + /* pSes->timeInstance += ( Abc_Clock() - timeStart ); */ + /* if ( !f ) continue; /\* proven UNSAT while creating clauses *\/ */ + + /* fSat = Ses_ManSolve( pSes ); */ + /* if ( fSat == 1 ) */ + /* { */ + /* fRes = 1; */ + /* break; */ + /* } */ + /* else if ( fSat == 2 ) */ + /* { */ + /* pSes->fHitResLimit = 1; */ + /* fRes = 0; */ + /* break; */ + /* } */ /* UNSAT => continue */ } |