mirror of https://github.com/YosysHQ/abc.git
Additional improvements in 'satclp'.
This commit is contained in:
parent
edf3144543
commit
69df5462cb
|
|
@ -2062,6 +2062,41 @@ void Abc_NtkPermute( Abc_Ntk_t * pNtk, int fInputs, int fOutputs, int fFlops, ch
|
|||
Vec_IntFree( vFlops );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Abc_NodeCompareByFanoutCount( Abc_Obj_t ** pp1, Abc_Obj_t ** pp2 )
|
||||
{
|
||||
int Diff = Abc_ObjFanoutNum(*pp2) - Abc_ObjFanoutNum(*pp1);
|
||||
if ( Diff < 0 )
|
||||
return -1;
|
||||
if ( Diff > 0 )
|
||||
return 1;
|
||||
Diff = strcmp( Abc_ObjName(*pp1), Abc_ObjName(*pp2) );
|
||||
if ( Diff < 0 )
|
||||
return -1;
|
||||
if ( Diff > 0 )
|
||||
return 1;
|
||||
return 0;
|
||||
}
|
||||
void Abc_NtkPermutePiUsingFanout( Abc_Ntk_t * pNtk )
|
||||
{
|
||||
Abc_Obj_t * pNode; int i;
|
||||
qsort( (void *)Vec_PtrArray(pNtk->vPis), Vec_PtrSize(pNtk->vPis), sizeof(Abc_Obj_t *),
|
||||
(int (*)(const void *, const void *)) Abc_NodeCompareByFanoutCount );
|
||||
Vec_PtrClear( pNtk->vCis );
|
||||
Vec_PtrForEachEntry( Abc_Obj_t *, pNtk->vPis, pNode, i )
|
||||
Vec_PtrPush( pNtk->vCis, pNode );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
|
|
|||
|
|
@ -20558,15 +20558,17 @@ usage:
|
|||
int Abc_CommandPermute( Abc_Frame_t * pAbc, int argc, char ** argv )
|
||||
{
|
||||
extern Abc_Ntk_t * Abc_NtkRestrashRandom( Abc_Ntk_t * pNtk );
|
||||
extern void Abc_NtkPermutePiUsingFanout( Abc_Ntk_t * pNtk );
|
||||
Abc_Ntk_t * pNtk = pAbc->pNtkCur, * pNtkRes = NULL;
|
||||
char * pFlopPermFile = NULL;
|
||||
int fInputs = 1;
|
||||
int fOutputs = 1;
|
||||
int fFlops = 1;
|
||||
int fNodes = 1;
|
||||
int fFanout = 0;
|
||||
int c;
|
||||
Extra_UtilGetoptReset();
|
||||
while ( ( c = Extra_UtilGetopt( argc, argv, "Fiofnh" ) ) != EOF )
|
||||
while ( ( c = Extra_UtilGetopt( argc, argv, "Fiofnxh" ) ) != EOF )
|
||||
{
|
||||
switch ( c )
|
||||
{
|
||||
|
|
@ -20591,6 +20593,9 @@ int Abc_CommandPermute( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
case 'n':
|
||||
fNodes ^= 1;
|
||||
break;
|
||||
case 'x':
|
||||
fFanout ^= 1;
|
||||
break;
|
||||
case 'h':
|
||||
goto usage;
|
||||
default:
|
||||
|
|
@ -20603,6 +20608,16 @@ int Abc_CommandPermute( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
Abc_Print( -1, "Empty network.\n" );
|
||||
return 1;
|
||||
}
|
||||
if ( fFanout )
|
||||
{
|
||||
if ( Abc_NtkLatchNum(pNtk) )
|
||||
{
|
||||
Abc_Print( -1, "Currently \"permute -x\" works only for combinational networks.\n" );
|
||||
return 1;
|
||||
}
|
||||
Abc_NtkPermutePiUsingFanout( pNtk );
|
||||
return 0;
|
||||
}
|
||||
if ( fNodes && !Abc_NtkIsStrash(pNtk) )
|
||||
{
|
||||
Abc_Print( -1, "To permute nodes, the network should be structurally hashed.\n" );
|
||||
|
|
@ -20622,12 +20637,13 @@ int Abc_CommandPermute( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
return 0;
|
||||
|
||||
usage:
|
||||
Abc_Print( -2, "usage: permute [-iofnh] [-F filename]\n" );
|
||||
Abc_Print( -2, "usage: permute [-iofnxh] [-F filename]\n" );
|
||||
Abc_Print( -2, "\t performs random permutation of inputs/outputs/flops\n" );
|
||||
Abc_Print( -2, "\t-i : toggle permuting primary inputs [default = %s]\n", fInputs? "yes": "no" );
|
||||
Abc_Print( -2, "\t-o : toggle permuting primary outputs [default = %s]\n", fOutputs? "yes": "no" );
|
||||
Abc_Print( -2, "\t-f : toggle permuting flip-flops [default = %s]\n", fFlops? "yes": "no" );
|
||||
Abc_Print( -2, "\t-n : toggle deriving new topological ordering of nodes [default = %s]\n", fNodes? "yes": "no" );
|
||||
Abc_Print( -2, "\t-x : toggle permuting inputs based on their fanout count [default = %s]\n", fFanout? "yes": "no" );
|
||||
Abc_Print( -2, "\t-h : print the command usage\n");
|
||||
Abc_Print( -2, "\t-F <filename> : (optional) file with the flop permutation\n" );
|
||||
return 1;
|
||||
|
|
|
|||
|
|
@ -20,6 +20,7 @@
|
|||
|
||||
#include "base/abc/abc.h"
|
||||
#include "aig/gia/gia.h"
|
||||
#include "misc/vec/vecWec.h"
|
||||
|
||||
#ifdef ABC_USE_CUDD
|
||||
#include "bdd/extrab/extraBdd.h"
|
||||
|
|
@ -290,25 +291,96 @@ Gia_Man_t * Abc_NtkClpOneGia( Abc_Ntk_t * pNtk, int iCo, Vec_Int_t * vSupp )
|
|||
Gia_ManStop( pTemp );
|
||||
return pNew;
|
||||
}
|
||||
Vec_Str_t * Abc_NtkClpOne( Abc_Ntk_t * pNtk, int iCo, int nCubeLim, int nBTLimit, int fVerbose, int fCanon, int fReverse, Vec_Int_t ** pvSupp )
|
||||
Vec_Str_t * Abc_NtkClpOne( Abc_Ntk_t * pNtk, int iCo, int nCubeLim, int nBTLimit, int fVerbose, int fCanon, int fReverse, Vec_Int_t * vSupp )
|
||||
{
|
||||
extern Vec_Int_t * Abc_NtkNodeSupportInt( Abc_Ntk_t * pNtk, int iCo );
|
||||
extern Vec_Str_t * Bmc_CollapseOne( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose );
|
||||
Vec_Int_t * vSupp = Abc_NtkNodeSupportInt( pNtk, iCo );
|
||||
Gia_Man_t * pGia = Abc_NtkClpOneGia( pNtk, iCo, vSupp );
|
||||
Vec_Str_t * vSop;
|
||||
abctime clk = Abc_Clock();
|
||||
extern Vec_Str_t * Bmc_CollapseOne( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose );
|
||||
Gia_Man_t * pGia = Abc_NtkClpOneGia( pNtk, iCo, vSupp );
|
||||
if ( fVerbose )
|
||||
printf( "Output %d:\n", iCo );
|
||||
printf( "Output %d: \n", iCo );
|
||||
vSop = Bmc_CollapseOne( pGia, nCubeLim, nBTLimit, fCanon, fReverse, fVerbose );
|
||||
Gia_ManStop( pGia );
|
||||
*pvSupp = vSupp;
|
||||
if ( vSop == NULL )
|
||||
Vec_IntFree(vSupp);
|
||||
else if ( Vec_StrSize(vSop) == 4 ) // constant
|
||||
return NULL;
|
||||
if ( Vec_StrSize(vSop) == 4 ) // constant
|
||||
Vec_IntClear(vSupp);
|
||||
if ( fVerbose )
|
||||
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
|
||||
return vSop;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Collect structural support for all nodes.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Vec_Wec_t * Abc_NtkCreateCoSupps( Abc_Ntk_t * pNtk, int fVerbose )
|
||||
{
|
||||
abctime clk = Abc_Clock();
|
||||
Abc_Obj_t * pNode; int i;
|
||||
Vec_Wec_t * vSupps = Vec_WecStart( Abc_NtkObjNumMax(pNtk) );
|
||||
Abc_NtkForEachCi( pNtk, pNode, i )
|
||||
Vec_IntPush( Vec_WecEntry(vSupps, pNode->Id), i );
|
||||
Abc_NtkForEachNode( pNtk, pNode, i )
|
||||
Vec_IntTwoMerge2( Vec_WecEntry(vSupps, Abc_ObjFanin0(pNode)->Id),
|
||||
Vec_WecEntry(vSupps, Abc_ObjFanin1(pNode)->Id),
|
||||
Vec_WecEntry(vSupps, pNode->Id) );
|
||||
if ( fVerbose )
|
||||
Abc_PrintTime( 1, "Support computation", Abc_Clock() - clk );
|
||||
return vSupps;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Derive array of COs sorted by cone size in the reverse order.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Abc_NodeCompareByTemp( Abc_Obj_t ** pp1, Abc_Obj_t ** pp2 )
|
||||
{
|
||||
int Diff = (*pp2)->iTemp - (*pp1)->iTemp;
|
||||
if ( Diff < 0 )
|
||||
return -1;
|
||||
if ( Diff > 0 )
|
||||
return 1;
|
||||
Diff = strcmp( Abc_ObjName(*pp1), Abc_ObjName(*pp2) );
|
||||
if ( Diff < 0 )
|
||||
return -1;
|
||||
if ( Diff > 0 )
|
||||
return 1;
|
||||
return 0;
|
||||
}
|
||||
Vec_Ptr_t * Abc_NtkCreateCoOrder( Abc_Ntk_t * pNtk, Vec_Wec_t * vSupps )
|
||||
{
|
||||
Abc_Obj_t * pNode; int i;
|
||||
Vec_Ptr_t * vNodes = Vec_PtrAlloc( Abc_NtkCoNum(pNtk) );
|
||||
Abc_NtkForEachCo( pNtk, pNode, i )
|
||||
{
|
||||
pNode->iTemp = Vec_IntSize( Vec_WecEntry(vSupps, Abc_ObjFanin0(pNode)->Id) );
|
||||
Vec_PtrPush( vNodes, pNode );
|
||||
}
|
||||
// order objects alphabetically
|
||||
qsort( (void *)Vec_PtrArray(vNodes), Vec_PtrSize(vNodes), sizeof(Abc_Obj_t *),
|
||||
(int (*)(const void *, const void *)) Abc_NodeCompareByTemp );
|
||||
// cleanup
|
||||
// Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
|
||||
// printf( "%s %d ", Abc_ObjName(pNode), pNode->iTemp );
|
||||
// printf( "\n" );
|
||||
return vNodes;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [SAT-based collapsing.]
|
||||
|
|
@ -320,14 +392,13 @@ Vec_Str_t * Abc_NtkClpOne( Abc_Ntk_t * pNtk, int iCo, int nCubeLim, int nBTLimit
|
|||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Abc_Obj_t * Abc_NtkFromSopsOne( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, int iCo, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose )
|
||||
Abc_Obj_t * Abc_NtkFromSopsOne( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, int iCo, Vec_Int_t * vSupp, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose )
|
||||
{
|
||||
Abc_Obj_t * pNodeNew;
|
||||
Vec_Int_t * vSupp;
|
||||
Vec_Str_t * vSop;
|
||||
int i, iCi;
|
||||
// compute SOP of the node
|
||||
vSop = Abc_NtkClpOne( pNtk, iCo, nCubeLim, nBTLimit, fVerbose, fCanon, fReverse, &vSupp );
|
||||
vSop = Abc_NtkClpOne( pNtk, iCo, nCubeLim, nBTLimit, fVerbose, fCanon, fReverse, vSupp );
|
||||
if ( vSop == NULL )
|
||||
return NULL;
|
||||
// create a new node
|
||||
|
|
@ -335,7 +406,6 @@ Abc_Obj_t * Abc_NtkFromSopsOne( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, int iCo,
|
|||
// add fanins
|
||||
Vec_IntForEachEntry( vSupp, iCi, i )
|
||||
Abc_ObjAddFanin( pNodeNew, Abc_NtkCi(pNtkNew, iCi) );
|
||||
Vec_IntFree( vSupp );
|
||||
// transfer the function
|
||||
pNodeNew->pData = Abc_SopRegister( (Mem_Flex_t *)pNtkNew->pManFunc, Vec_StrArray(vSop) );
|
||||
Vec_StrFree( vSop );
|
||||
|
|
@ -346,17 +416,37 @@ Abc_Ntk_t * Abc_NtkFromSops( Abc_Ntk_t * pNtk, int nCubeLim, int nBTLimit, int f
|
|||
ProgressBar * pProgress;
|
||||
Abc_Ntk_t * pNtkNew;
|
||||
Abc_Obj_t * pNode, * pDriver, * pNodeNew;
|
||||
Vec_Ptr_t * vDriverCopy;
|
||||
Vec_Ptr_t * vDriverCopy, * vCoNodes;
|
||||
Vec_Int_t * vNodeCoIds;
|
||||
Vec_Wec_t * vSupps;
|
||||
int i;
|
||||
|
||||
// Abc_NtkForEachCi( pNtk, pNode, i )
|
||||
// printf( "%d ", Abc_ObjFanoutNum(pNode) );
|
||||
// printf( "\n" );
|
||||
|
||||
// compute structural supports
|
||||
vSupps = Abc_NtkCreateCoSupps( pNtk, fVerbose );
|
||||
// order CO nodes by support size
|
||||
vCoNodes = Abc_NtkCreateCoOrder( pNtk, vSupps );
|
||||
// collect CO IDs in this order
|
||||
vNodeCoIds = Vec_IntAlloc( Abc_NtkCoNum(pNtk) );
|
||||
Abc_NtkForEachCo( pNtk, pNode, i )
|
||||
pNode->iTemp = i;
|
||||
Vec_PtrForEachEntry( Abc_Obj_t *, vCoNodes, pNode, i )
|
||||
Vec_IntPush( vNodeCoIds, pNode->iTemp );
|
||||
|
||||
// start the new network
|
||||
pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_SOP );
|
||||
// collect driver copies
|
||||
vDriverCopy = Vec_PtrAlloc( Abc_NtkCoNum(pNtk) );
|
||||
Abc_NtkForEachCo( pNtk, pNode, i )
|
||||
// Abc_NtkForEachCo( pNtk, pNode, i )
|
||||
Vec_PtrForEachEntry( Abc_Obj_t *, vCoNodes, pNode, i )
|
||||
Vec_PtrPush( vDriverCopy, Abc_ObjFanin0(pNode)->pCopy );
|
||||
// process the POs
|
||||
pProgress = Extra_ProgressBarStart( stdout, Abc_NtkCoNum(pNtk) );
|
||||
Abc_NtkForEachCo( pNtk, pNode, i )
|
||||
// Abc_NtkForEachCo( pNtk, pNode, i )
|
||||
Vec_PtrForEachEntry( Abc_Obj_t *, vCoNodes, pNode, i )
|
||||
{
|
||||
Extra_ProgressBarUpdate( pProgress, i, NULL );
|
||||
pDriver = Abc_ObjFanin0(pNode);
|
||||
|
|
@ -365,15 +455,14 @@ Abc_Ntk_t * Abc_NtkFromSops( Abc_Ntk_t * pNtk, int nCubeLim, int nBTLimit, int f
|
|||
Abc_ObjAddFanin( pNode->pCopy, (Abc_Obj_t *)Vec_PtrEntry(vDriverCopy, i) );
|
||||
continue;
|
||||
}
|
||||
/*
|
||||
if ( Abc_ObjIsCi(pDriver) )
|
||||
{
|
||||
pNodeNew = Abc_NtkCreateNode( pNtkNew );
|
||||
Abc_ObjAddFanin( pNodeNew, pDriver->pCopy ); // pDriver->pCopy is removed by GIA construction...
|
||||
Abc_ObjAddFanin( pNodeNew, (Abc_Obj_t *)Vec_PtrEntry(vDriverCopy, i) );
|
||||
pNodeNew->pData = Abc_SopRegister( (Mem_Flex_t *)pNtkNew->pManFunc, Abc_ObjFaninC0(pNode) ? "0 1\n" : "1 1\n" );
|
||||
Abc_ObjAddFanin( pNode->pCopy, pNodeNew );
|
||||
continue;
|
||||
}
|
||||
*/
|
||||
if ( pDriver == Abc_AigConst1(pNtk) )
|
||||
{
|
||||
pNodeNew = Abc_NtkCreateNode( pNtkNew );
|
||||
|
|
@ -381,7 +470,7 @@ Abc_Ntk_t * Abc_NtkFromSops( Abc_Ntk_t * pNtk, int nCubeLim, int nBTLimit, int f
|
|||
Abc_ObjAddFanin( pNode->pCopy, pNodeNew );
|
||||
continue;
|
||||
}
|
||||
pNodeNew = Abc_NtkFromSopsOne( pNtkNew, pNtk, i, nCubeLim, nBTLimit, fCanon, fReverse, fVerbose );
|
||||
pNodeNew = Abc_NtkFromSopsOne( pNtkNew, pNtk, Vec_IntEntry(vNodeCoIds, i), Vec_WecEntry(vSupps, Abc_ObjFanin0(pNode)->Id), nCubeLim, nBTLimit, fCanon, fReverse, fVerbose );
|
||||
if ( pNodeNew == NULL )
|
||||
{
|
||||
Abc_NtkDelete( pNtkNew );
|
||||
|
|
@ -391,6 +480,9 @@ Abc_Ntk_t * Abc_NtkFromSops( Abc_Ntk_t * pNtk, int nCubeLim, int nBTLimit, int f
|
|||
Abc_ObjAddFanin( pNode->pCopy, pNodeNew );
|
||||
}
|
||||
Vec_PtrFree( vDriverCopy );
|
||||
Vec_PtrFree( vCoNodes );
|
||||
Vec_IntFree( vNodeCoIds );
|
||||
Vec_WecFree( vSupps );
|
||||
Extra_ProgressBarStop( pProgress );
|
||||
return pNtkNew;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -425,7 +425,7 @@ cleanup:
|
|||
Bmc_CollapseIrredundant( vSop, Vec_StrSize(vSop)/(nVars +3), nVars );
|
||||
return vSop;
|
||||
}
|
||||
Vec_Str_t * Bmc_CollapseOne( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose )
|
||||
Vec_Str_t * Bmc_CollapseOne2( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose )
|
||||
{
|
||||
Vec_Str_t * vSopOn, * vSopOff;
|
||||
int nCubesOn = ABC_INFINITY;
|
||||
|
|
@ -454,6 +454,167 @@ Vec_Str_t * Bmc_CollapseOne( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCan
|
|||
}
|
||||
}
|
||||
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [This code computes on-set and off-set simultaneously.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Vec_Str_t * Bmc_CollapseOne( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose )
|
||||
{
|
||||
int fVeryVerbose = fVerbose;
|
||||
int nVars = Gia_ManCiNum(p);
|
||||
Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( p, 8, 0, 0, 0 );
|
||||
sat_solver * pSat[2] = { (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0), (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0) };
|
||||
sat_solver * pSatClean[2] = { (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0), (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0) };
|
||||
Vec_Str_t * vSop[2] = { Vec_StrAlloc(1000), Vec_StrAlloc(1000) }, * vRes = NULL;
|
||||
Vec_Int_t * vLitsC[2] = { Vec_IntAlloc(nVars), Vec_IntAlloc(nVars) };
|
||||
Vec_Int_t * vVars = Vec_IntAlloc( nVars );
|
||||
Vec_Int_t * vLits = Vec_IntAlloc( nVars );
|
||||
Vec_Int_t * vNums = Vec_IntAlloc( nVars );
|
||||
Vec_Int_t * vCube = Vec_IntAlloc( nVars );
|
||||
int n, v, iVar, iLit, iCiVarBeg, iCube, Start, status;
|
||||
abctime clk, Time[2][2] = {{0}};
|
||||
int fComplete[2] = {0};
|
||||
|
||||
// collect CI variables
|
||||
iCiVarBeg = pCnf->nVars - nVars;// - 1;
|
||||
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++ )
|
||||
{
|
||||
iLit = Abc_Var2Lit( 1, n ); // n=0 => F=1 n=1 => F=0
|
||||
status = sat_solver_solve( pSat[n], &iLit, &iLit + 1, nBTLimit, 0, 0, 0 );
|
||||
if ( status == l_Undef )
|
||||
goto cleanup; // timeout
|
||||
if ( status == l_False )
|
||||
{
|
||||
Vec_StrPrintStr( vSop[0], n ? " 1\n\0" : " 0\n\0" );
|
||||
fComplete[0] = 1;
|
||||
goto cleanup; // const0/1
|
||||
}
|
||||
// start with all negative literals
|
||||
Vec_IntForEachEntry( vVars, iVar, v )
|
||||
Vec_IntPush( vLitsC[n], Abc_Var2Lit(iVar, 1) );
|
||||
// add literals to the solver
|
||||
status = sat_solver_addclause( pSat[n], &iLit, &iLit + 1 );
|
||||
assert( status );
|
||||
status = sat_solver_addclause( pSatClean[n], &iLit, &iLit + 1 );
|
||||
assert( status );
|
||||
// start cover
|
||||
Vec_StrPush( vSop[n], '\0' );
|
||||
}
|
||||
|
||||
// compute cube pairs
|
||||
for ( iCube = 0; iCube < nCubeLim; iCube++ )
|
||||
{
|
||||
for ( n = 0; n < 2; n++ )
|
||||
{
|
||||
if ( fVeryVerbose ) clk = Abc_Clock();
|
||||
// get the assignment
|
||||
if ( fCanon )
|
||||
status = Bmc_ComputeCanonical( pSat[n], vLitsC[n], vCube, nBTLimit );
|
||||
else
|
||||
{
|
||||
sat_solver_clean_polarity( pSat[n], Vec_IntArray(vVars), Vec_IntSize(vVars) );
|
||||
status = sat_solver_solve( pSat[n], NULL, NULL, 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_IntClear( vLitsC[n] );
|
||||
Vec_IntForEachEntry( vVars, iVar, v )
|
||||
{
|
||||
iLit = Abc_Var2Lit(iVar, !sat_solver_var_value(pSat[n], iVar));
|
||||
Vec_IntPush( vLits, iLit );
|
||||
Vec_IntPush( vLitsC[n], iLit );
|
||||
}
|
||||
// expand the values
|
||||
if ( fVeryVerbose ) clk = Abc_Clock();
|
||||
status = Bmc_CollapseExpand( pSatClean[!n], pSat[n], vLits, vNums, vCube, nBTLimit, fCanon );
|
||||
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 )
|
||||
{
|
||||
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
|
||||
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( vLitsC[0] );
|
||||
Vec_IntFree( vLitsC[1] );
|
||||
Vec_IntFree( vNums );
|
||||
Vec_IntFree( vCube );
|
||||
Cnf_DataFree( pCnf );
|
||||
sat_solver_delete( pSat[0] );
|
||||
sat_solver_delete( pSat[1] );
|
||||
sat_solver_delete( pSatClean[0] );
|
||||
sat_solver_delete( pSatClean[1] );
|
||||
assert( !fComplete[0] || !fComplete[1] );
|
||||
if ( fComplete[0] || fComplete[1] ) // one of the cover is computed
|
||||
{
|
||||
vRes = vSop[fComplete[1]]; vSop[fComplete[1]] = NULL;
|
||||
Bmc_CollapseIrredundant( vRes, Vec_StrSize(vRes)/(nVars +3), nVars );
|
||||
if ( fVeryVerbose )
|
||||
{
|
||||
printf( "Processed output with %d supp vars and %d cubes.\n", nVars, 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] );
|
||||
}
|
||||
}
|
||||
Vec_StrFreeP( &vSop[0] );
|
||||
Vec_StrFreeP( &vSop[1] );
|
||||
return vRes;
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
|
|
|||
Loading…
Reference in New Issue