luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Improvements to 'satclp' (unfinished).

This commit is contained in:
Alan Mishchenko 2015-11-06 09:05:17 -08:00
parent 83da5a0384
commit dd365cbaf3
3 changed files with 457 additions and 11 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/aig/gia/gia.h
View File

@ -1038,6 +1038,8 @@ static inline int Gia_ObjCellId( Gia_Man_t * p, int iLit ) { re
for ( i = 0; (i < Vec_IntSize(p->vCis)) && ((pObj) = Gia_ManCi(p, i)); i++ )
#define Gia_ManForEachCiId( p, Id, i ) \
for ( i = 0; (i < Vec_IntSize(p->vCis)) && ((Id) = Gia_ObjId(p, Gia_ManCi(p, i))); i++ )
#define Gia_ManForEachCiVec( vVec, p, pObj, i ) \
for ( i = 0; (i < Vec_IntSize(vVec)) && ((pObj) = Gia_ManCi(p, Vec_IntEntry(vVec,i))); i++ )
#define Gia_ManForEachCiReverse( p, pObj, i ) \
for ( i = Vec_IntSize(p->vCis) - 1; (i >= 0) && ((pObj) = Gia_ManCi(p, i)); i-- )
#define Gia_ManForEachCo( p, pObj, i ) \

114
src/base/abci/abcCollapse.c
View File

@ -21,6 +21,8 @@
#include "base/abc/abc.h"
#include "aig/gia/gia.h"
#include "misc/vec/vecWec.h"
#include "sat/cnf/cnf.h"
#include "sat/bsat/satStore.h"
#ifdef ABC_USE_CUDD
#include "bdd/extrab/extraBdd.h"
@ -535,6 +537,8 @@ extern Vec_Wec_t * Gia_ManCreateCoSupps( Gia_Man_t * p, int fVerbose );
extern int Gia_ManCoLargestSupp( Gia_Man_t * p, Vec_Wec_t * vSupps );
extern Vec_Wec_t * Gia_ManIsoStrashReduceInt( Gia_Man_t * p, Vec_Wec_t * vSupps, int fVerbose );
extern Cnf_Dat_t * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fVerbose );
/**Function*************************************************************
Synopsis [Derives GIA for the network.]
@ -622,10 +626,65 @@ int Abc_NtkCollapseCountVars( Vec_Str_t * vSop, Vec_Int_t * vSupp )
Vec_IntWriteEntry( vSupp, j++, iVar );
Vec_IntShrink( vSupp, j );
Vec_IntFree( vPres );
// if ( Vec_IntSize(vSupp) != Abc_SopGetVarNum(Vec_StrArray(vSop)) )
// printf( "Mismatch!!!\n" );
return 1;
}
/**Function*************************************************************
Synopsis [Derives SAT solver for one output from the shared CNF.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
sat_solver * Abc_NtkClpDeriveSatSolver( Cnf_Dat_t * pCnf, int iCoObjId, Vec_Int_t * vSupp, Vec_Int_t * vAnds, Vec_Int_t * vMap, sat_solver ** ppSat )
{
int i, k, iObj, status, nVars = 2;
Vec_Int_t * vLits = Vec_IntAlloc( 16 );
sat_solver * pSat = sat_solver_new();
if ( ppSat ) *ppSat = sat_solver_new();
// assign SAT variable numbers
Vec_IntWriteEntry( vMap, iCoObjId, nVars++ );
Vec_IntForEachEntry( vSupp, iObj, k )
Vec_IntWriteEntry( vMap, iObj, nVars++ );
Vec_IntForEachEntry( vAnds, iObj, k )
if ( pCnf->pObj2Clause[iObj] != -1 )
Vec_IntWriteEntry( vMap, iObj, nVars++ );
// create clauses for the internal nodes and for the output
sat_solver_setnvars( pSat, nVars );
if ( ppSat ) sat_solver_setnvars( *ppSat, nVars );
Vec_IntPush( vAnds, iCoObjId );
Vec_IntForEachEntry( vAnds, iObj, k )
{
int iClaBeg, iClaEnd, * pLit;
if ( pCnf->pObj2Clause[iObj] == -1 )
continue;
iClaBeg = pCnf->pObj2Clause[iObj];
iClaEnd = iClaBeg + pCnf->pObj2Count[iObj];
assert( iClaBeg < iClaEnd );
for ( i = iClaBeg; i < iClaEnd; i++ )
{
Vec_IntClear( vLits );
for ( pLit = pCnf->pClauses[i]; pLit < pCnf->pClauses[i+1]; pLit++ )
Vec_IntPush( vLits, Abc_Lit2LitV(Vec_IntArray(vMap), *pLit) );
status = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits)+Vec_IntSize(vLits) );
assert( status );
(void) status;
if ( ppSat ) sat_solver_addclause( *ppSat, Vec_IntArray(vLits), Vec_IntArray(vLits)+Vec_IntSize(vLits) );
}
}
Vec_IntPop( vAnds );
Vec_IntFree( vLits );
assert( nVars == sat_solver_nvars(pSat) );
return pSat;
}
/**Function*************************************************************
Synopsis [Computes SOPs for each output.]
@ -651,8 +710,43 @@ Vec_Str_t * Abc_NtkClpGiaOne( Gia_Man_t * p, int iCo, int nCubeLim, int nBTLimit
return NULL;
if ( Vec_StrSize(vSop) == 4 ) // constant
Vec_IntClear(vSupp);
else
Abc_NtkCollapseCountVars( vSop, vSupp );
// else
// Abc_NtkCollapseCountVars( vSop, vSupp );
if ( fVerbose )
printf( "Supp new = %4d. Sop = %4d. ", Vec_IntSize(vSupp), Vec_StrSize(vSop)/(Vec_IntSize(vSupp) +3) );
if ( fVerbose )
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
return vSop;
}
Vec_Str_t * Abc_NtkClpGiaOne2( Cnf_Dat_t * pCnf, Gia_Man_t * p, int iCo, int nCubeLim, int nBTLimit, int fVerbose, int fCanon, int fReverse, Vec_Int_t * vSupp, Vec_Int_t * vMap )
{
Vec_Str_t * vSop;
sat_solver * pSat, * pSat2 = NULL;
Gia_Obj_t * pObj;
abctime clk = Abc_Clock();
extern Vec_Str_t * Bmc_CollapseOne_int( sat_solver * pSat, sat_solver * pSat2, int nVars, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose );
int i, iCoObjId = Gia_ObjId( p, Gia_ManCo(p, iCo) );
Vec_Int_t * vAnds = Vec_IntAlloc( 100 );
Vec_Int_t * vSuppObjs = Vec_IntAlloc( 100 );
Gia_ManForEachCiVec( vSupp, p, pObj, i )
Vec_IntPush( vSuppObjs, Gia_ObjId(p, pObj) );
Gia_ManIncrementTravId( p );
Gia_ManCollectAnds( p, &iCoObjId, 1, vAnds );
assert( Vec_IntSize(vAnds) > 0 );
pSat = Abc_NtkClpDeriveSatSolver( pCnf, iCoObjId, vSuppObjs, vAnds, vMap, &pSat2 );
Vec_IntFree( vSuppObjs );
if ( fVerbose )
printf( "Output %4d: Supp = %4d. Cone =%6d.\n", iCo, Vec_IntSize(vSupp), Vec_IntSize(vAnds) );
vSop = Bmc_CollapseOne_int( pSat, pSat2, Vec_IntSize(vSupp), nCubeLim, nBTLimit, fCanon, fReverse, fVerbose );
sat_solver_delete( pSat );
sat_solver_delete( pSat2 );
Vec_IntFree( vAnds );
if ( vSop == NULL )
return NULL;
if ( Vec_StrSize(vSop) == 4 ) // constant
Vec_IntClear(vSupp);
// else
// Abc_NtkCollapseCountVars( vSop, vSupp );
if ( fVerbose )
printf( "Supp new = %4d. Sop = %4d. ", Vec_IntSize(vSupp), Vec_StrSize(vSop)/(Vec_IntSize(vSupp) +3) );
if ( fVerbose )
@ -667,6 +761,8 @@ Vec_Ptr_t * Abc_GiaDeriveSops( Abc_Ntk_t * pNtkNew, Gia_Man_t * p, Vec_Wec_t * v
Vec_Int_t * vReprs, * vClass, * vReprSuppSizes;
int i, k, Entry, iCo, * pOrder;
Vec_Wec_t * vClasses;
Cnf_Dat_t * pCnf;
Vec_Int_t * vMap;
// derive classes of outputs
vClasses = Gia_ManIsoStrashReduceInt( p, vSupps, 0 );
if ( fVerbose )
@ -682,6 +778,8 @@ Vec_Ptr_t * Abc_GiaDeriveSops( Abc_Ntk_t * pNtkNew, Gia_Man_t * p, Vec_Wec_t * v
pOrder = Abc_MergeSortCost( Vec_IntArray(vReprSuppSizes), Vec_IntSize(vReprSuppSizes) );
Vec_IntFree( vReprSuppSizes );
// consider SOPs for representatives
vMap = Vec_IntStartFull( Gia_ManObjNum(p) );
pCnf = Mf_ManGenerateCnf( p, 8, 1, 0, 0 );
vSopsRepr = Vec_PtrStart( Vec_IntSize(vReprs) );
pProgress = Extra_ProgressBarStart( stdout, Vec_IntSize(vReprs) );
Extra_ProgressBarUpdate( pProgress, 0, NULL );
@ -690,7 +788,14 @@ Vec_Ptr_t * Abc_GiaDeriveSops( Abc_Ntk_t * pNtkNew, Gia_Man_t * p, Vec_Wec_t * v
int iEntry = pOrder[Vec_IntSize(vReprs) - 1 - i];
int iCoThis = Vec_IntEntry( vReprs, iEntry );
Vec_Int_t * vSupp = Vec_WecEntry( vSupps, iCoThis );
Vec_Str_t * vSop = Abc_NtkClpGiaOne( p, iCoThis, nCubeLim, nBTLimit, i ? 0 : fVerbose, fCanon, fReverse, vSupp );
Vec_Str_t * vSop;
if ( Vec_IntSize(vSupp) < 2 )
{
Vec_PtrWriteEntry( vSopsRepr, iEntry, (void *)(ABC_PTRINT_T)1 );
continue;
}
// vSop = Abc_NtkClpGiaOne( p, iCoThis, nCubeLim, nBTLimit, i ? 0 : fVerbose, fCanon, fReverse, vSupp );
vSop = Abc_NtkClpGiaOne2( pCnf, p, iCoThis, nCubeLim, nBTLimit, i ? 0 : fVerbose, fCanon, fReverse, vSupp, vMap );
if ( vSop == NULL )
goto finish;
assert( Vec_IntSize( Vec_WecEntry(vSupps, iCoThis) ) == Abc_SopGetVarNum(Vec_StrArray(vSop)) );
@ -699,6 +804,8 @@ Vec_Ptr_t * Abc_GiaDeriveSops( Abc_Ntk_t * pNtkNew, Gia_Man_t * p, Vec_Wec_t * v
Vec_StrFree( vSop );
}
Extra_ProgressBarStop( pProgress );
Cnf_DataFree( pCnf );
Vec_IntFree( vMap );
// derive SOPs for each output
vSops = Vec_PtrStart( Gia_ManCoNum(p) );
Vec_WecForEachLevel ( vClasses, vClass, i )
@ -787,6 +894,7 @@ Abc_Ntk_t * Abc_NtkFromSopsInt( Abc_Ntk_t * pNtk, int nCubeLim, int nBTLimit, in
Vec_IntForEachEntry( vSupp, iCi, k )
Abc_ObjAddFanin( pNodeNew, Abc_NtkCi(pNtkNew, iCi) );
pNodeNew->pData = Vec_PtrEntry( vSops, i );
assert( pNodeNew->pData != (void *)(ABC_PTRINT_T)1 );
Abc_ObjAddFanin( pNode->pCopy, pNodeNew );
}
Vec_WecFree( vSupps );

352
src/sat/bmc/bmcClp.c
View File

@ -355,7 +355,7 @@ int Bmc_CollapseIrredundantFull( Vec_Str_t * vSop, int nCubes, int nVars )
SeeAlso []
***********************************************************************/
int Bmc_CollapseExpandRound( sat_solver * pSat, sat_solver * pSatOn, Vec_Int_t * vLits, Vec_Int_t * vNums, Vec_Int_t * vTemp, int nBTLimit, int fCanon )
int Bmc_CollapseExpandRound( sat_solver * pSat, sat_solver * pSatOn, Vec_Int_t * vLits, Vec_Int_t * vNums, Vec_Int_t * vTemp, int nBTLimit, int fCanon, int fOnOffSetLit )
{
int fProfile = 0;
int k, n, iLit, status;
@ -369,6 +369,7 @@ int Bmc_CollapseExpandRound( sat_solver * pSat, sat_solver * pSatOn, Vec_Int_t *
// check if this literal when expanded overlaps with the on-set
if ( pSatOn )
{
assert( fOnOffSetLit == -1 );
// it is ok to skip the first round if the literal is positive
if ( fCanon && !Abc_LitIsCompl(Save) )
continue;
@ -399,9 +400,13 @@ int Bmc_CollapseExpandRound( sat_solver * pSat, sat_solver * pSatOn, Vec_Int_t *
if ( iLit != -1 )
Vec_IntPush( vTemp, iLit );
// check against offset
if ( fOnOffSetLit >= 0 )
Vec_IntPush( vTemp, fOnOffSetLit );
if ( fProfile ) clk = Abc_Clock();
status = sat_solver_solve( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp), nBTLimit, 0, 0, 0 );
if ( fProfile ) clkCheck2 += Abc_Clock() - clk;
if ( fOnOffSetLit >= 0 )
Vec_IntPop( vTemp );
if ( status == l_Undef )
return -1;
if ( status == l_True )
@ -428,14 +433,18 @@ int Bmc_CollapseExpandRound( sat_solver * pSat, sat_solver * pSatOn, Vec_Int_t *
SeeAlso []
***********************************************************************/
int Bmc_CollapseExpand( sat_solver * pSat, sat_solver * pSatOn, Vec_Int_t * vLits, Vec_Int_t * vNums, Vec_Int_t * vTemp, int nBTLimit, int fCanon )
int Bmc_CollapseExpand( sat_solver * pSat, sat_solver * pSatOn, Vec_Int_t * vLits, Vec_Int_t * vNums, Vec_Int_t * vTemp, int nBTLimit, int fCanon, int fOnOffSetLit )
{
// perform one quick reduction if it is non-canonical
if ( !fCanon )
{
int i, k, iLit, status, nFinal, * pFinal;
// check against offset
if ( fOnOffSetLit >= 0 )
Vec_IntPush( vLits, fOnOffSetLit );
status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits), nBTLimit, 0, 0, 0 );
if ( fOnOffSetLit >= 0 )
Vec_IntPop( vLits );
if ( status == l_Undef )
return -1;
assert( status == l_False );
@ -450,12 +459,12 @@ int Bmc_CollapseExpand( sat_solver * pSat, sat_solver * pSatOn, Vec_Int_t * vLit
if ( k == nFinal )
Vec_IntWriteEntry( vLits, i, -1 );
}
Bmc_CollapseExpandRound( pSat, NULL, vLits, vNums, vTemp, nBTLimit, fCanon );
Bmc_CollapseExpandRound( pSat, NULL, vLits, vNums, vTemp, nBTLimit, fCanon, fOnOffSetLit );
}
else
{
Bmc_CollapseExpandRound( pSat, pSatOn, vLits, vNums, vTemp, nBTLimit, fCanon );
Bmc_CollapseExpandRound( pSat, NULL, vLits, vNums, vTemp, nBTLimit, fCanon );
Bmc_CollapseExpandRound( pSat, pSatOn, vLits, vNums, vTemp, nBTLimit, fCanon, -1 );
Bmc_CollapseExpandRound( pSat, NULL, vLits, vNums, vTemp, nBTLimit, fCanon, -1 );
}
{
// put into new array
@ -625,7 +634,7 @@ Vec_Str_t * Bmc_CollapseOneInt( Gia_Man_t * p, int nCubeLim, int nBTLimit, int f
printf( "\n" );
}
// expand the values
status = Bmc_CollapseExpand( pSat[1], fCanon ? pSat[2] : pSat[0], vLits, vNums, vCube, nBTLimit, fCanon );
status = Bmc_CollapseExpand( pSat[1], fCanon ? pSat[2] : pSat[0], vLits, vNums, vCube, nBTLimit, fCanon, -1 );
if ( status < 0 )
{
Vec_StrFreeP( &vSop );
@ -719,7 +728,7 @@ Vec_Str_t * Bmc_CollapseOne2( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCa
SeeAlso []
***********************************************************************/
Vec_Str_t * Bmc_CollapseOne( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose )
Vec_Str_t * Bmc_CollapseOne3( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose )
{
int fVeryVerbose = fVerbose;
int nVars = Gia_ManCiNum(p);
@ -805,7 +814,7 @@ Vec_Str_t * Bmc_CollapseOne( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCan
}
// expand the values
if ( fVeryVerbose ) clk = Abc_Clock();
status = Bmc_CollapseExpand( pSatClean[!n], pSat[n], vLits, vNums, vCube, nBTLimit, fCanon );
status = Bmc_CollapseExpand( pSatClean[!n], pSat[n], vLits, vNums, vCube, nBTLimit, fCanon, -1 );
if ( fVeryVerbose ) Time[n][1] += Abc_Clock() - clk;
if ( status < 0 )
goto cleanup; // timeout
@ -884,6 +893,333 @@ cleanup:
return vRes;
}
/**Function*************************************************************
Synopsis [This code computes on-set and off-set simultaneously.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Str_t * Bmc_CollapseOne_int2( sat_solver * pSat, int nVars, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose )
{
int fVeryVerbose = fVerbose;
Vec_Str_t * vSop[2] = { Vec_StrAlloc(1000), Vec_StrAlloc(1000) }, * vRes = NULL;
Vec_Int_t * vVars = Vec_IntAlloc( nVars+1 );
Vec_Int_t * vLits = Vec_IntAlloc( nVars+1 );
Vec_Int_t * vNums = Vec_IntAlloc( nVars+1 );
Vec_Int_t * vCube = Vec_IntAlloc( nVars+1 );
int n, v, iVar, pLits[2], iCube = 0, Start, status;
abctime clk = 0, Time[2][2] = {{0}};
int fComplete[2] = {0};
// variables
int iOutVar = 2;
int iOOVars[2] = {0, 1};
// int iOutVar = 1;
// int iOOVars[2] = {sat_solver_nvars(pSat) - 5, sat_solver_nvars(pSat) - 5 + 1};
// collect CI variables (0 = onset enable, 1 = offset enable, 2 = output)
int iCiVarBeg = 3;
// int iCiVarBeg = sat_solver_nvars(pSat) - 5 - nVars;
if ( fReverse )
for ( v = nVars - 1; v >= 0; v-- )
Vec_IntPush( vVars, iCiVarBeg + v );
else
for ( v = 0; v < nVars; v++ )
Vec_IntPush( vVars, iCiVarBeg + v );
// check that on-set/off-set is sat
for ( n = 0; n < 2; n++ )
{
pLits[0] = Abc_Var2Lit( iOutVar, n ); // n=0 => F=1 n=1 => F=0
status = sat_solver_solve( pSat, pLits, pLits + 1, nBTLimit, 0, 0, 0 );
if ( status == l_Undef )
goto cleanup; // timeout
if ( status == l_False )
{
Vec_StrClear( vSop[0] );
Vec_StrPrintStr( vSop[0], n ? " 1\n" : " 0\n" );
Vec_StrPush( vSop[0], '\0' );
fComplete[0] = 1;
goto cleanup; // const0/1
}
// start cover
Vec_StrPush( vSop[n], '\0' );
}
// compute cube pairs
for ( iCube = 0; nCubeLim == 0 || iCube < nCubeLim; iCube++ )
{
for ( n = 0; n < 2; n++ )
{
if ( fVeryVerbose ) clk = Abc_Clock();
// get the assignment
sat_solver_clean_polarity( pSat, Vec_IntArray(vVars), Vec_IntSize(vVars) );
pLits[0] = Abc_Var2Lit( iOutVar, n ); // set output
pLits[1] = Abc_Var2Lit( iOOVars[n], 1 ); // enable clauses
status = sat_solver_solve( pSat, pLits, pLits + 2, 0, 0, 0, 0 );
if ( fVeryVerbose ) Time[n][0] += Abc_Clock() - clk;
if ( status == l_Undef )
goto cleanup; // timeout
if ( status == l_False )
{
fComplete[n] = 1;
break;
}
// collect values
Vec_IntClear( vLits );
Vec_IntForEachEntry( vVars, iVar, v )
Vec_IntPush( vLits, Abc_Var2Lit(iVar, !sat_solver_var_value(pSat, iVar)) );
// expand the values
if ( fVeryVerbose ) clk = Abc_Clock();
status = Bmc_CollapseExpand( pSat, NULL, vLits, vNums, vCube, nBTLimit, fCanon, Abc_Var2Lit(iOutVar, !n) );
if ( fVeryVerbose ) Time[n][1] += Abc_Clock() - clk;
if ( status < 0 )
goto cleanup; // timeout
// collect cube
Vec_StrPop( vSop[n] );
Start = Vec_StrSize( vSop[n] );
Vec_StrFillExtra( vSop[n], Start + nVars + 4, '-' );
Vec_StrWriteEntry( vSop[n], Start + nVars + 0, ' ' );
Vec_StrWriteEntry( vSop[n], Start + nVars + 1, (char)(n ? '0' : '1') );
Vec_StrWriteEntry( vSop[n], Start + nVars + 2, '\n' );
Vec_StrWriteEntry( vSop[n], Start + nVars + 3, '\0' );
Vec_IntClear( vCube );
Vec_IntForEachEntry( vNums, iVar, v )
{
int iLit = Vec_IntEntry( vLits, iVar );
Vec_IntPush( vCube, Abc_LitNot(iLit) );
if ( fReverse )
Vec_StrWriteEntry( vSop[n], Start + nVars - iVar - 1, (char)('0' + !Abc_LitIsCompl(iLit)) );
else
Vec_StrWriteEntry( vSop[n], Start + iVar, (char)('0' + !Abc_LitIsCompl(iLit)) );
}
// add cube
Vec_IntPush( vCube, Abc_Var2Lit( iOOVars[n], 0 ) );
status = sat_solver_addclause( pSat, Vec_IntArray(vCube), Vec_IntLimit(vCube) );
if ( status == 0 )
{
fComplete[n] = 1;
break;
}
assert( status == 1 );
}
if ( fComplete[0] || fComplete[1] )
break;
}
cleanup:
Vec_IntFree( vVars );
Vec_IntFree( vLits );
Vec_IntFree( vNums );
Vec_IntFree( vCube );
assert( !fComplete[0] || !fComplete[1] );
if ( fComplete[0] || fComplete[1] ) // one of the cover is computed
{
vRes = vSop[fComplete[1]]; vSop[fComplete[1]] = NULL;
if ( iCube > 1 )
// Bmc_CollapseIrredundant( vRes, Vec_StrSize(vRes)/(nVars +3), nVars );
Bmc_CollapseIrredundantFull( vRes, Vec_StrSize(vRes)/(nVars +3), nVars );
}
if ( fVeryVerbose )
{
int fProfile = 0;
printf( "Processed output with %d supp vars. ", nVars );
if ( vRes == NULL )
printf( "The resulting SOP exceeded %d cubes.\n", nCubeLim );
else
printf( "The best cover contains %d cubes.\n", Vec_StrSize(vRes)/(nVars +3) );
Abc_PrintTime( 1, "Onset minterm", Time[0][0] );
Abc_PrintTime( 1, "Onset expand ", Time[0][1] );
Abc_PrintTime( 1, "Offset minterm", Time[1][0] );
Abc_PrintTime( 1, "Offset expand ", Time[1][1] );
if ( fProfile )
{
Abc_PrintTime( 1, "Expand check1 ", clkCheck1 ); clkCheck1 = 0;
Abc_PrintTime( 1, "Expand check2 ", clkCheck2 ); clkCheck2 = 0;
Abc_PrintTime( 1, "Expand sat ", clkCheckS ); clkCheckS = 0;
Abc_PrintTime( 1, "Expand unsat ", clkCheckU ); clkCheckU = 0;
}
}
Vec_StrFreeP( &vSop[0] );
Vec_StrFreeP( &vSop[1] );
return vRes;
}
Vec_Str_t * Bmc_CollapseOne( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose )
{
Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( p, 8, 0, 0, 0 );
sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0);
Vec_Str_t * vSop = Bmc_CollapseOne_int2( pSat, Gia_ManCiNum(p), nCubeLim, nBTLimit, fCanon, fReverse, fVerbose );
sat_solver_delete( pSat );
Cnf_DataFree( pCnf );
return vSop;
}
/**Function*************************************************************
Synopsis [This code computes on-set and off-set simultaneously.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Str_t * Bmc_CollapseOne_int( sat_solver * pSat1, sat_solver * pSat2, int nVars, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose )
{
int fVeryVerbose = fVerbose;
sat_solver * pSat[2] = { pSat1, pSat2 };
Vec_Str_t * vSop[2] = { Vec_StrAlloc(1000), Vec_StrAlloc(1000) }, * vRes = NULL;
Vec_Int_t * vVars = Vec_IntAlloc( nVars+1 );
Vec_Int_t * vLits = Vec_IntAlloc( nVars+1 );
Vec_Int_t * vNums = Vec_IntAlloc( nVars+1 );
Vec_Int_t * vCube = Vec_IntAlloc( nVars+1 );
int n, v, iVar, pLits[2], iCube = 0, Start, status;
abctime clk = 0, Time[2][2] = {{0}};
int fComplete[2] = {0};
// variables
int iOutVar = 2;
int iOOVars[2] = {0, 1};
// int iOutVar = 1;
// int iOOVars[2] = {sat_solver_nvars(pSat) - 5, sat_solver_nvars(pSat) - 5 + 1};
// collect CI variables (0 = onset enable, 1 = offset enable, 2 = output)
int iCiVarBeg = 3;
// int iCiVarBeg = sat_solver_nvars(pSat) - 5 - nVars;
if ( fReverse )
for ( v = nVars - 1; v >= 0; v-- )
Vec_IntPush( vVars, iCiVarBeg + v );
else
for ( v = 0; v < nVars; v++ )
Vec_IntPush( vVars, iCiVarBeg + v );
// check that on-set/off-set is sat
for ( n = 0; n < 2; n++ )
{
pLits[0] = Abc_Var2Lit( iOutVar, n ); // n=0 => F=1 n=1 => F=0
status = sat_solver_solve( pSat[n], pLits, pLits + 1, nBTLimit, 0, 0, 0 );
if ( status == l_Undef )
goto cleanup; // timeout
if ( status == l_False )
{
Vec_StrClear( vSop[0] );
Vec_StrPrintStr( vSop[0], n ? " 1\n" : " 0\n" );
Vec_StrPush( vSop[0], '\0' );
fComplete[0] = 1;
goto cleanup; // const0/1
}
// add literals to the solver
status = sat_solver_addclause( pSat[n], pLits, pLits + 1 );
assert( status );
// start cover
Vec_StrPush( vSop[n], '\0' );
}
// compute cube pairs
for ( iCube = 0; nCubeLim == 0 || iCube < nCubeLim; iCube++ )
{
for ( n = 0; n < 2; n++ )
{
if ( fVeryVerbose ) clk = Abc_Clock();
// get the assignment
sat_solver_clean_polarity( pSat[n], Vec_IntArray(vVars), Vec_IntSize(vVars) );
pLits[0] = Abc_Var2Lit( iOOVars[n], 1 ); // enable clauses
// pLits[1] = Abc_Var2Lit( iOutVar, n ); // set output
// status = sat_solver_solve( pSat, pLits, pLits + 2, 0, 0, 0, 0 );
status = sat_solver_solve( pSat[n], pLits, pLits + 1, 0, 0, 0, 0 );
if ( fVeryVerbose ) Time[n][0] += Abc_Clock() - clk;
if ( status == l_Undef )
goto cleanup; // timeout
if ( status == l_False )
{
fComplete[n] = 1;
break;
}
// collect values
Vec_IntClear( vLits );
Vec_IntForEachEntry( vVars, iVar, v )
Vec_IntPush( vLits, Abc_Var2Lit(iVar, !sat_solver_var_value(pSat[n], iVar)) );
// expand the values
if ( fVeryVerbose ) clk = Abc_Clock();
// status = Bmc_CollapseExpand( pSat, NULL, vLits, vNums, vCube, nBTLimit, fCanon, Abc_Var2Lit(iOutVar, !n) );
status = Bmc_CollapseExpand( pSat[!n], NULL, vLits, vNums, vCube, nBTLimit, fCanon, -1 );
if ( fVeryVerbose ) Time[n][1] += Abc_Clock() - clk;
if ( status < 0 )
goto cleanup; // timeout
// collect cube
Vec_StrPop( vSop[n] );
Start = Vec_StrSize( vSop[n] );
Vec_StrFillExtra( vSop[n], Start + nVars + 4, '-' );
Vec_StrWriteEntry( vSop[n], Start + nVars + 0, ' ' );
Vec_StrWriteEntry( vSop[n], Start + nVars + 1, (char)(n ? '0' : '1') );
Vec_StrWriteEntry( vSop[n], Start + nVars + 2, '\n' );
Vec_StrWriteEntry( vSop[n], Start + nVars + 3, '\0' );
Vec_IntClear( vCube );
Vec_IntForEachEntry( vNums, iVar, v )
{
int iLit = Vec_IntEntry( vLits, iVar );
Vec_IntPush( vCube, Abc_LitNot(iLit) );
if ( fReverse )
Vec_StrWriteEntry( vSop[n], Start + nVars - iVar - 1, (char)('0' + !Abc_LitIsCompl(iLit)) );
else
Vec_StrWriteEntry( vSop[n], Start + iVar, (char)('0' + !Abc_LitIsCompl(iLit)) );
}
// add cube
Vec_IntPush( vCube, Abc_Var2Lit( iOOVars[n], 0 ) );
// status = sat_solver_addclause( pSat, Vec_IntArray(vCube), Vec_IntLimit(vCube) );
status = sat_solver_addclause( pSat[n], Vec_IntArray(vCube), Vec_IntLimit(vCube) );
if ( status == 0 )
{
fComplete[n] = 1;
break;
}
assert( status == 1 );
}
if ( fComplete[0] || fComplete[1] )
break;
}
cleanup:
Vec_IntFree( vVars );
Vec_IntFree( vLits );
Vec_IntFree( vNums );
Vec_IntFree( vCube );
assert( !fComplete[0] || !fComplete[1] );
if ( fComplete[0] || fComplete[1] ) // one of the cover is computed
{
vRes = vSop[fComplete[1]]; vSop[fComplete[1]] = NULL;
if ( iCube > 1 )
// Bmc_CollapseIrredundant( vRes, Vec_StrSize(vRes)/(nVars +3), nVars );
Bmc_CollapseIrredundantFull( vRes, Vec_StrSize(vRes)/(nVars +3), nVars );
}
if ( fVeryVerbose )
{
int fProfile = 0;
printf( "Processed output with %d supp vars. ", nVars );
if ( vRes == NULL )
printf( "The resulting SOP exceeded %d cubes.\n", nCubeLim );
else
printf( "The best cover contains %d cubes.\n", Vec_StrSize(vRes)/(nVars +3) );
Abc_PrintTime( 1, "Onset minterm", Time[0][0] );
Abc_PrintTime( 1, "Onset expand ", Time[0][1] );
Abc_PrintTime( 1, "Offset minterm", Time[1][0] );
Abc_PrintTime( 1, "Offset expand ", Time[1][1] );
if ( fProfile )
{
Abc_PrintTime( 1, "Expand check1 ", clkCheck1 ); clkCheck1 = 0;
Abc_PrintTime( 1, "Expand check2 ", clkCheck2 ); clkCheck2 = 0;
Abc_PrintTime( 1, "Expand sat ", clkCheckS ); clkCheckS = 0;
Abc_PrintTime( 1, "Expand unsat ", clkCheckU ); clkCheckU = 0;
}
}
Vec_StrFreeP( &vSop[0] );
Vec_StrFreeP( &vSop[1] );
return vRes;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////