summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/base/abc/abcNtk.c35
-rw-r--r--src/base/abci/abc.c20
-rw-r--r--src/base/abci/abcCollapse.c130
-rw-r--r--src/sat/bmc/bmcClp.c163
4 files changed, 326 insertions, 22 deletions
diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c
index 19d6ef79..a2f5e138 100644
--- a/src/base/abc/abcNtk.c
+++ b/src/base/abc/abcNtk.c
@@ -2073,6 +2073,41 @@ void Abc_NtkPermute( Abc_Ntk_t * pNtk, int fInputs, int fOutputs, int fFlops, ch
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 []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
void Abc_NtkUnpermute( Abc_Ntk_t * pNtk )
{
Vec_Ptr_t * vTemp, * vTemp2, * vLatch;
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index d6a9b1cc..49924f14 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -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;
diff --git a/src/base/abci/abcCollapse.c b/src/base/abci/abcCollapse.c
index b78a1206..cc610998 100644
--- a/src/base/abci/abcCollapse.c
+++ b/src/base/abci/abcCollapse.c
@@ -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,27 +291,98 @@ 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 );
+ 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 );
- Vec_Int_t * vSupp = Abc_NtkNodeSupportInt( pNtk, iCo );
Gia_Man_t * pGia = Abc_NtkClpOneGia( pNtk, iCo, vSupp );
- Vec_Str_t * vSop;
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.]
Description []
@@ -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;
}
diff --git a/src/sat/bmc/bmcClp.c b/src/sat/bmc/bmcClp.c
index 10892530..d5610840 100644
--- a/src/sat/bmc/bmcClp.c
+++ b/src/sat/bmc/bmcClp.c
@@ -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 ///
////////////////////////////////////////////////////////////////////////
generated by cgit v1.2.3 (git 2.25.1) at 2025-11-04 03:23:29 +0000