summaryrefslogtreecommitdiffstats
path: root/src/opt
diff options
context:
space:
mode:
Diffstat (limited to 'src/opt')
-rw-r--r--src/opt/dau/dauGia.c50
-rw-r--r--src/opt/dsc/dsc.c525
-rw-r--r--src/opt/dsc/dsc.h91
-rw-r--r--src/opt/dsc/module.make1
-rw-r--r--src/opt/sbd/module.make5
-rw-r--r--src/opt/sbd/sbd.c53
-rw-r--r--src/opt/sbd/sbd.h75
-rw-r--r--src/opt/sbd/sbdCnf.c147
-rw-r--r--src/opt/sbd/sbdCore.c1520
-rw-r--r--src/opt/sbd/sbdInt.h78
-rw-r--r--src/opt/sbd/sbdSat.c797
-rw-r--r--src/opt/sbd/sbdSim.c310
-rw-r--r--src/opt/sbd/sbdWin.c283
13 files changed, 3923 insertions, 12 deletions
diff --git a/src/opt/dau/dauGia.c b/src/opt/dau/dauGia.c
index b75ded61..5e74ad21 100644
--- a/src/opt/dau/dauGia.c
+++ b/src/opt/dau/dauGia.c
@@ -238,12 +238,28 @@ int Dau_DsdBalance( Gia_Man_t * pGia, int * pFans, int nFans, int fAnd )
assert( nFans > 1 );
iFan0 = pFans[--nFans];
iFan1 = pFans[--nFans];
- if ( fAnd )
- iFan = Gia_ManHashAnd( pGia, iFan0, iFan1 );
- else if ( pGia->pMuxes )
- iFan = Gia_ManHashXorReal( pGia, iFan0, iFan1 );
- else
- iFan = Gia_ManHashXor( pGia, iFan0, iFan1 );
+ if ( pGia->pHTable == NULL )
+ {
+ if ( fAnd )
+ iFan = Gia_ManAppendAnd( pGia, iFan0, iFan1 );
+ else if ( pGia->pMuxes )
+ {
+ int fCompl = Abc_LitIsCompl(iFan0) ^ Abc_LitIsCompl(iFan1);
+ iFan = Gia_ManAppendXorReal( pGia, Abc_LitRegular(iFan0), Abc_LitRegular(iFan1) );
+ iFan = Abc_LitNotCond( iFan, fCompl );
+ }
+ else
+ iFan = Gia_ManAppendXor( pGia, iFan0, iFan1 );
+ }
+ else
+ {
+ if ( fAnd )
+ iFan = Gia_ManHashAnd( pGia, iFan0, iFan1 );
+ else if ( pGia->pMuxes )
+ iFan = Gia_ManHashXorReal( pGia, iFan0, iFan1 );
+ else
+ iFan = Gia_ManHashXor( pGia, iFan0, iFan1 );
+ }
pObj = Gia_ManObj(pGia, Abc_Lit2Var(iFan));
if ( Gia_ObjIsAnd(pObj) )
{
@@ -340,14 +356,24 @@ int Dau_DsdToGia_rec( Gia_Man_t * pGia, char * pStr, char ** p, int * pMatches,
assert( **p == '{' && *q == '}' );
*p = q;
}
- if ( pGia->pMuxes )
- Res = Gia_ManHashMuxReal( pGia, Temp[0], Temp[1], Temp[2] );
+ if ( pGia->pHTable == NULL )
+ {
+ if ( pGia->pMuxes )
+ Res = Gia_ManAppendMux( pGia, Temp[0], Temp[1], Temp[2] );
+ else
+ Res = Gia_ManAppendMux( pGia, Temp[0], Temp[1], Temp[2] );
+ }
else
- Res = Gia_ManHashMux( pGia, Temp[0], Temp[1], Temp[2] );
+ {
+ if ( pGia->pMuxes )
+ Res = Gia_ManHashMuxReal( pGia, Temp[0], Temp[1], Temp[2] );
+ else
+ Res = Gia_ManHashMux( pGia, Temp[0], Temp[1], Temp[2] );
+ }
pObj = Gia_ManObj(pGia, Abc_Lit2Var(Res));
if ( Gia_ObjIsAnd(pObj) )
{
- if ( pGia->pMuxes )
+ if ( pGia->pMuxes && pGia->pHTable != NULL )
Gia_ObjSetMuxLevel( pGia, pObj );
else
{
@@ -377,7 +403,7 @@ int Dau_DsdToGia_rec( Gia_Man_t * pGia, char * pStr, char ** p, int * pMatches,
vLeaves.nSize = nVars;
vLeaves.pArray = Fanins;
nObjOld = Gia_ManObjNum(pGia);
- Res = Kit_TruthToGia( pGia, (unsigned *)pFunc, nVars, vCover, &vLeaves, 1 );
+ Res = Kit_TruthToGia( pGia, (unsigned *)pFunc, nVars, vCover, &vLeaves, pGia->pHTable != NULL );
// assert( nVars <= 6 );
// Res = Dau_DsdToGiaCompose_rec( pGia, pFunc[0], Fanins, nVars );
for ( i = nObjOld; i < Gia_ManObjNum(pGia); i++ )
@@ -434,7 +460,7 @@ int Dsm_ManTruthToGia( void * p, word * pTruth, Vec_Int_t * vLeaves, Vec_Int_t *
if ( nSizeNonDec )
m_NonDsd++;
// printf( "%s\n", pDsd );
- if ( fDelayBalance )
+ if ( fDelayBalance && pGia->vLevels )
return Dau_DsdToGia( pGia, pDsd, Vec_IntArray(vLeaves), vCover );
else
return Dau_DsdToGia2( pGia, pDsd, Vec_IntArray(vLeaves), vCover );
diff --git a/src/opt/dsc/dsc.c b/src/opt/dsc/dsc.c
new file mode 100644
index 00000000..ce180fe3
--- /dev/null
+++ b/src/opt/dsc/dsc.c
@@ -0,0 +1,525 @@
+/**CFile****************************************************************
+
+ FileName [dsc.h]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Disjoint support decomposition - ICCD'15]
+
+ Synopsis [Disjoint-support decomposition with cofactoring and boolean difference analysis
+ from V. Callegaro, F. S. Marranghello, M. G. A. Martins, R. P. Ribas and A. I. Reis,
+ "Bottom-up disjoint-support decomposition based on cofactor and boolean difference analysis," ICCD'15]
+
+ Author [Vinicius Callegaro, Mayler G. A. Martins, Felipe S. Marranghello, Renato P. Ribas and Andre I. Reis]
+
+ Affiliation [UFRGS - Federal University of Rio Grande do Sul - Brazil]
+
+ Date [Ver. 1.0. Started - October 24, 2014.]
+
+ Revision [$Id: dsc.h,v 1.00 2014/10/24 00:00:00 vcallegaro Exp $]
+
+***********************************************************************/
+
+#include "dsc.h"
+#include <assert.h>
+#include "misc/util/utilTruth.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+/*
+ This code performs truth-table-based decomposition for 6-variable functions.
+ Representation of operations:
+ ! = not;
+ (ab) = a and b;
+ [ab] = a xor b;
+*/
+typedef struct Dsc_node_t_ Dsc_node_t;
+struct Dsc_node_t_
+{
+ word *pNegCof;
+ word *pPosCof;
+ word *pBoolDiff;
+ unsigned int on[DSC_MAX_VAR+1]; // pos cofactor spec - first element denotes the size of the array
+ unsigned int off[DSC_MAX_VAR+1]; // neg cofactor spec - first element denotes the size of the array
+ char exp[DSC_MAX_STR];
+};
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+inline void xorInPlace( word * pOut, word * pIn2, int nWords)
+{
+ int w;
+ for ( w = 0; w < nWords; w++ )
+ pOut[w] ^= pIn2[w];
+}
+
+void dsc_debug_node(Dsc_node_t * pNode, int nVars, const int TRUTH_WORDS) {
+ int i;
+ printf("Node:\t%s\n",pNode->exp);
+ printf("\tneg cof:\t");Abc_TtPrintHexRev(stdout, pNode->pNegCof, nVars);
+ printf("\tpos cof:\t");Abc_TtPrintHexRev(stdout, pNode->pPosCof, nVars);
+ printf("\tbool diff:\t");Abc_TtPrintHexRev(stdout, pNode->pBoolDiff, nVars);
+ printf("\toff:\t");
+ for (i=1;i<=(int)pNode->off[0];i++) {
+ printf("%c%c", (pNode->off[i] & 1U) ? ' ' : '!', 'a'+(pNode->off[i] >> 1));
+ }
+ printf("\ton:\t");
+ for (i=1;i<=(int)pNode->on[0];i++) {
+ printf("%c%c", (pNode->on[i] & 1U) ? ' ' : '!', 'a'+(pNode->on[i] >> 1));
+ }
+ printf("\n");
+}
+
+inline int dsc_and_test(Dsc_node_t *ni, Dsc_node_t *nj, const int TRUTH_WORDS, int* ci, int* cj) {
+ if (Abc_TtEqual(ni->pNegCof, nj->pNegCof, TRUTH_WORDS)) {*ci=1; *cj=1; return 1;}
+ else if (Abc_TtEqual(ni->pNegCof, nj->pPosCof, TRUTH_WORDS)) {*ci=1; *cj=0; return 1;}
+ else if (Abc_TtEqual(ni->pPosCof, nj->pNegCof, TRUTH_WORDS)) {*ci=0; *cj=1; return 1;}
+ else if (Abc_TtEqual(ni->pPosCof, nj->pPosCof, TRUTH_WORDS)) {*ci=0; *cj=0; return 1;}
+ return 0;
+}
+
+inline int dsc_xor_test(Dsc_node_t *ni, Dsc_node_t *nj, const int TRUTH_WORDS) {
+ return Abc_TtEqual(ni->pBoolDiff, nj->pBoolDiff, TRUTH_WORDS);
+}
+
+void concat(char* target, char begin, char end, char* s1, int s1Polarity, char* s2, int s2Polarity) {
+ *target++ = begin;
+ //s1
+ if (!s1Polarity)
+ *target++ = '!';
+ while (*s1 != '\0')
+ *target++ = *s1++;
+ // s2
+ if (!s2Polarity)
+ *target++ = '!';
+ while (*s2 != '\0')
+ *target++ = *s2++;
+ // end
+ *target++ = end;
+ *target = '\0';
+}
+
+void cubeCofactor(word * const pTruth, const unsigned int * const cubeCof, const int TRUTH_WORDS) {
+ int size = cubeCof[0];
+ int i;
+ for (i = 1; i <= size; i++) {
+ unsigned int c = cubeCof[i];
+ if (c & 1U) {
+ Abc_TtCofactor1(pTruth, TRUTH_WORDS, c >> 1);
+ } else {
+ Abc_TtCofactor0(pTruth, TRUTH_WORDS, c >> 1);
+ }
+ }
+}
+
+void merge(unsigned int * const pOut, const unsigned int * const pIn) {
+ const int elementsToCopy = pIn[0];
+ int i, j;
+ for (i = pOut[0]+1, j = 1; j <= elementsToCopy; i++, j++) {
+ pOut[i] = pIn[j];
+ }
+ pOut[0] += elementsToCopy;
+}
+
+void dsc_and_group(Dsc_node_t * pOut, Dsc_node_t * ni, int niPolarity, Dsc_node_t * nj, int njPolarity, int nVars, const int TRUTH_WORDS) {
+ unsigned int* xiOFF, * xiON, * xjOFF, * xjON;
+ // expression
+ concat(pOut->exp, '(', ')', ni->exp, niPolarity, nj->exp, njPolarity);
+ // ON-OFF
+ if (niPolarity) {
+ xiOFF = ni->off;
+ xiON = ni->on;
+ } else {
+ xiOFF = ni->on;
+ xiON = ni->off;
+ }
+ if (njPolarity) {
+ xjOFF = nj->off;
+ xjON = nj->on;
+ } else {
+ xjOFF = nj->on;
+ xjON = nj->off;
+ }
+ // creating both the new OFF specification and negative cofactor of the new group
+ {
+ // first element of the array represents the size of the cube-cofactor
+ int xiOFFSize = xiOFF[0];
+ int xjOFFSize = xjOFF[0];
+ if (xiOFFSize <= xjOFFSize) {
+ int i;
+ pOut->off[0] = xiOFFSize; // set the number of elements
+ for (i = 1; i <= xiOFFSize; i++) {
+ pOut->off[i] = xiOFF[i];
+ }
+ } else {
+ int i;
+ pOut->off[0] = xjOFFSize; // set the number of elements
+ for (i = 1; i <= xjOFFSize; i++) {
+ pOut->off[i] = xjOFF[i];
+ }
+ }
+ // set the negative cofactor of the new group
+ pOut->pNegCof = niPolarity ? ni->pNegCof : ni->pPosCof;
+ }
+ // creating both new ON specification and positive cofactor of the new group
+ {
+ int i;
+ int j;
+ unsigned int xiONSize = xiON[0];
+ unsigned int xjONSize = xjON[0];
+ pOut->on[0] = xiONSize + xjONSize;
+ for (i = 1; i <= (int)xiONSize; i++) {
+ pOut->on[i] = xiON[i];
+ }
+ for (j = 1; j <= (int)xjONSize; j++) {
+ pOut->on[i++] = xjON[j];
+ }
+ // set the positive cofactor of the new group
+ if (xiONSize >= xjONSize) {
+ pOut->pPosCof = niPolarity ? ni->pPosCof : ni->pNegCof;
+ cubeCofactor(pOut->pPosCof, xjON, TRUTH_WORDS);
+ } else {
+ pOut->pPosCof = njPolarity ? nj->pPosCof : nj->pNegCof;
+ cubeCofactor(pOut->pPosCof, xiON, TRUTH_WORDS);
+ }
+ }
+ // set the boolean difference of the new group
+ pOut->pBoolDiff = njPolarity ? nj->pNegCof : nj->pPosCof;
+ xorInPlace(pOut->pBoolDiff, pOut->pPosCof, TRUTH_WORDS);
+}
+
+void dsc_xor_group(Dsc_node_t * pOut, Dsc_node_t * ni, Dsc_node_t * nj, int nVars, const int TRUTH_WORDS) {
+ //
+ const unsigned int * xiOFF = ni->off;
+ const unsigned int * xiON = ni->on;
+ const unsigned int * xjOFF = nj->off;
+ const unsigned int * xjON = nj->on;
+ //
+ const int xiOFFSize = xiOFF[0];
+ const int xiONSize = xiON[0];
+ const int xjOFFSize = xjOFF[0];
+ const int xjONSize = xjON[0];
+ // minCubeCofs
+ int minCCSize = xiOFFSize;
+ int minCCPolarity = 0;
+ Dsc_node_t * minCCNode = ni;
+ // expression
+ concat(pOut->exp, '[', ']', ni->exp, 1, nj->exp, 1);
+ if (minCCSize > xiONSize) {
+ minCCSize = xiONSize;
+ minCCPolarity = 1;
+ //minCCNode = ni;
+ }
+ if (minCCSize > xjOFFSize) {
+ minCCSize = xjOFFSize;
+ minCCPolarity = 0;
+ minCCNode = nj;
+ }
+ if (minCCSize > xjONSize) {
+ minCCSize = xjONSize;
+ minCCPolarity = 1;
+ minCCNode = nj;
+ }
+ //
+ if (minCCNode == ni) {
+ if (minCCPolarity) {
+ // gOFF = xiON, xjON
+ pOut->pNegCof = nj->pPosCof;
+ cubeCofactor(pOut->pNegCof, xiON, TRUTH_WORDS);
+ // gON = xiON, xjOFF
+ pOut->pPosCof = nj->pNegCof;
+ cubeCofactor(pOut->pPosCof, xiON, TRUTH_WORDS);
+ } else {
+ // gOFF = xiOFF, xjOFF
+ pOut->pNegCof = nj->pNegCof;
+ cubeCofactor(pOut->pNegCof, xiOFF, TRUTH_WORDS);
+ // gON = xiOFF, xjON
+ pOut->pPosCof = nj->pPosCof;
+ cubeCofactor(pOut->pPosCof, xiOFF, TRUTH_WORDS);
+ }
+ }else {
+ if (minCCPolarity) {
+ // gOFF = xjON, xiON
+ pOut->pNegCof = ni->pPosCof;
+ cubeCofactor(pOut->pNegCof, xjON, TRUTH_WORDS);
+ // gON = xjON, xiOFF
+ pOut->pPosCof = ni->pNegCof;
+ cubeCofactor(pOut->pPosCof, xjON, TRUTH_WORDS);
+ } else {
+ // gOFF = xjOFF, xiOFF
+ pOut->pNegCof = ni->pNegCof;
+ cubeCofactor(pOut->pNegCof, xjOFF, TRUTH_WORDS);
+ // gON = xjOFF, xiON
+ pOut->pPosCof = ni->pPosCof;
+ cubeCofactor(pOut->pPosCof, xjOFF, TRUTH_WORDS);
+ }
+ }
+ // bool diff
+ pOut->pBoolDiff = ni->pBoolDiff;
+ // evaluating specs
+ // off spec
+ pOut->off[0] = 0;
+ if ((xiOFFSize+xjOFFSize) <= (xiONSize+xjONSize)) {
+ merge(pOut->off, xiOFF);
+ merge(pOut->off, xjOFF);
+ } else {
+ merge(pOut->off, xiON);
+ merge(pOut->off, xjON);
+ }
+ // on spec
+ pOut->on[0] = 0;
+ if ((xiOFFSize+xjONSize) <= (xiONSize+xjOFFSize)) {
+ merge(pOut->on, xiOFF);
+ merge(pOut->on, xjON);
+ } else {
+ merge(pOut->on, xiON);
+ merge(pOut->on, xjOFF);
+ }
+}
+
+/**
+ * memory allocator with a capacity of storing 3*nVars
+ * truth-tables for negative and positive cofactors and
+ * the boolean difference for each input variable
+ */
+extern word * Dsc_alloc_pool(int nVars) {
+ return ABC_ALLOC(word, 3 * Abc_TtWordNum(nVars) * nVars);
+}
+
+/**
+ * just free the memory pool
+ */
+extern void Dsc_free_pool(word * pool) {
+ ABC_FREE(pool);
+}
+
+/**
+ * This method implements the paper proposed by V. Callegaro, F. S. Marranghello, M. G. A. Martins, R. P. Ribas and A. I. Reis,
+ * entitled "Bottom-up disjoint-support decomposition based on cofactor and boolean difference analysis", presented at ICCD 2015.
+ * pTruth: pointer for the truth table representing the target function.
+ * nVarsInit: the number of variables of the truth table of the target function.
+ * pRes: pointer for storing the resulting decomposition, whenever a decomposition can be found.
+ * pool: NULL or a pointer for with a capacity of storing 3*nVars truth-tables. IF NULL, the function will allocate and free the memory of each call.
+ * (the results presented on ICCD paper are running this method with NULL for the memory pool).
+ * The method returns 0 if a full decomposition was found and a negative value otherwise.
+ */
+extern int Dsc_Decompose(word * pTruth, const int nVarsInit, char * const pRes, word *pool) {
+ const int TRUTH_WORDS = Abc_TtWordNum(nVarsInit);
+ const int NEED_POOL_ALLOC = (pool == NULL);
+
+ Dsc_node_t nodes[DSC_MAX_VAR];
+ Dsc_node_t *newNodes[DSC_MAX_VAR];
+ Dsc_node_t *oldNodes[DSC_MAX_VAR];
+
+ Dsc_node_t freeNodes[DSC_MAX_VAR]; // N is the maximum number of possible groups.
+ int f = 0; // f represent the next free position in the freeNodes array
+ int o = 0; // o stands for the number of already tested nodes
+ int n = 0; // n will represent the number of current nodes (i.e. support)
+
+ pRes[0] = '\0';
+ pRes[1] = '\0';
+
+ if (NEED_POOL_ALLOC)
+ pool = ABC_ALLOC(word, 3 * TRUTH_WORDS * nVarsInit);
+
+ // block for the node data allocation
+ {
+ // pointer for the next free truth word
+ word *pNextTruth = pool;
+ int iVar;
+ for (iVar = 0; iVar < nVarsInit; iVar++) {
+ // negative cofactor
+ Abc_TtCofactor0p(pNextTruth, pTruth, TRUTH_WORDS, iVar);
+ // dont care test
+ if (!Abc_TtEqual(pNextTruth, pTruth, TRUTH_WORDS)) {
+ Dsc_node_t *node = &nodes[iVar];
+ node->pNegCof = pNextTruth;
+ // increment next truth pointer
+ pNextTruth += TRUTH_WORDS;
+ // positive cofactor
+ node->pPosCof = pNextTruth;
+ Abc_TtCofactor1p(node->pPosCof, pTruth, TRUTH_WORDS, iVar);
+ // increment next truth pointer
+ pNextTruth += TRUTH_WORDS;
+ // boolean difference
+ node->pBoolDiff = pNextTruth;
+ Abc_TtXor(node->pBoolDiff, node->pNegCof, node->pPosCof, TRUTH_WORDS, 0);
+ // increment next truth pointer
+ pNextTruth += TRUTH_WORDS;
+ // define on spec -
+ node->on[0] = 1; node->on[1] = (iVar << 1) | 1u; // lit = i*2+1, when polarity=true
+ // define off spec
+ node->off[0] = 1; node->off[1] = iVar << 1;// lit=i*2 otherwise
+ // store the node expression
+ node->exp[0] = 'a'+iVar; // TODO fix the variable names
+ node->exp[1] = '\0';
+ // add the node to the newNodes array
+ newNodes[n++] = node;
+ }
+ }
+ }
+ //const int initialSupport = n;
+ if (n == 0) {
+ if (NEED_POOL_ALLOC)
+ ABC_FREE(pool);
+ if (Abc_TtIsConst0(pTruth, TRUTH_WORDS)) {
+ { if ( pRes ) pRes[0] = '0', pRes[1] = '\0'; }
+ return 0;
+ } else if (Abc_TtIsConst1(pTruth, TRUTH_WORDS)) {
+ { if ( pRes ) pRes[0] = '1', pRes[1] = '\0'; }
+ return 0;
+ } else {
+ Abc_Print(-1, "ERROR. No variable in the support of f, but f isn't constant!\n");
+ return -1;
+ }
+ }
+ while (n > 0) {
+ int tempN = 0;
+ int i, j, iPolarity, jPolarity;
+ Dsc_node_t *ni, *nj, *newNode = NULL;
+ for (i = 0; i < n; i++) {
+ ni = newNodes[i];
+ newNode = NULL;
+ j = 0;
+ while (j < o) {
+ nj = oldNodes[j];
+ if (dsc_and_test(ni, nj, TRUTH_WORDS, &iPolarity, &jPolarity)) {
+ newNode = &freeNodes[f++];
+ dsc_and_group(newNode, ni, iPolarity, nj, jPolarity, nVarsInit, TRUTH_WORDS);
+ }
+ // XOR test
+ if ((newNode == NULL) && (dsc_xor_test(ni, nj, TRUTH_WORDS))) {
+ newNode = &freeNodes[f++];
+ dsc_xor_group(newNode, ni, nj, nVarsInit, TRUTH_WORDS);
+ }
+ if (newNode != NULL) {
+ oldNodes[j] = oldNodes[--o];
+ break;
+ } else {
+ j++;
+ }
+ }
+ if (newNode != NULL) {
+ newNodes[tempN++] = newNode;
+ } else {
+ oldNodes[o++] = ni;
+ }
+ }
+ n = tempN;
+ }
+ if (o == 1) {
+ Dsc_node_t * solution = oldNodes[0];
+ if (Abc_TtIsConst0(solution->pNegCof, TRUTH_WORDS) && Abc_TtIsConst1(solution->pPosCof, TRUTH_WORDS)) {
+ // Direct solution found
+ if ( pRes )
+ strcpy( pRes, solution->exp);
+ if (NEED_POOL_ALLOC)
+ ABC_FREE(pool);
+ return 0;
+ } else if (Abc_TtIsConst1(solution->pNegCof, TRUTH_WORDS) && Abc_TtIsConst0(solution->pPosCof, TRUTH_WORDS)) {
+ // Complementary solution found
+ if ( pRes ) {
+ pRes[0] = '!';
+ strcpy( &pRes[1], solution->exp);
+ }
+ if (NEED_POOL_ALLOC)
+ ABC_FREE(pool);
+ return 0;
+ } else {
+ printf("DSC ERROR: Final DSC node found, but differs from target function.\n");
+ if (NEED_POOL_ALLOC)
+ ABC_FREE(pool);
+ return -1;
+ }
+ }
+ if (NEED_POOL_ALLOC)
+ ABC_FREE(pool);
+ return -1;
+}
+
+
+/**Function*************************************************************
+ Synopsis [DSD formula manipulation.]
+ Description [Code copied from dauDsd.c but changed DAU_MAX_VAR to DSC_MAX_VAR]
+***********************************************************************/
+int * Dsc_ComputeMatches( char * p )
+{
+ static int pMatches[DSC_MAX_VAR];
+ int pNested[DSC_MAX_VAR];
+ int v, nNested = 0;
+ for ( v = 0; p[v]; v++ )
+ {
+ pMatches[v] = 0;
+ if ( p[v] == '(' || p[v] == '[' || p[v] == '<' || p[v] == '{' )
+ pNested[nNested++] = v;
+ else if ( p[v] == ')' || p[v] == ']' || p[v] == '>' || p[v] == '}' )
+ pMatches[pNested[--nNested]] = v;
+ assert( nNested < DSC_MAX_VAR );
+ }
+ assert( nNested == 0 );
+ return pMatches;
+}
+
+/**Function*************************************************************
+ Synopsis [DSD formula manipulation.]
+ Description [Code copied from dauDsd.c but changed DAU_MAX_VAR to DSC_MAX_VAR]
+***********************************************************************/
+int Dsc_CountAnds_rec( char * pStr, char ** p, int * pMatches )
+{
+ if ( **p == '!' )
+ (*p)++;
+ while ( (**p >= 'A' && **p <= 'F') || (**p >= '0' && **p <= '9') )
+ (*p)++;
+ if ( **p == '<' )
+ {
+ char * q = pStr + pMatches[*p - pStr];
+ if ( *(q+1) == '{' )
+ *p = q+1;
+ }
+ if ( **p >= 'a' && **p <= 'z' ) // var
+ return 0;
+ if ( **p == '(' || **p == '[' ) // and/or/xor
+ {
+ int Counter = 0, AddOn = (**p == '(')? 1 : 3;
+ char * q = pStr + pMatches[ *p - pStr ];
+ assert( *q == **p + 1 + (**p != '(') );
+ for ( (*p)++; *p < q; (*p)++ )
+ Counter += AddOn + Dsc_CountAnds_rec( pStr, p, pMatches );
+ assert( *p == q );
+ return Counter - AddOn;
+ }
+ if ( **p == '<' || **p == '{' ) // mux
+ {
+ int Counter = 3;
+ char * q = pStr + pMatches[ *p - pStr ];
+ assert( *q == **p + 1 + (**p != '(') );
+ for ( (*p)++; *p < q; (*p)++ )
+ Counter += Dsc_CountAnds_rec( pStr, p, pMatches );
+ assert( *p == q );
+ return Counter;
+ }
+ assert( 0 );
+ return 0;
+}
+/**Function*************************************************************
+ Synopsis [DSD formula manipulation.]
+ Description [Code copied from dauDsd.c but changed DAU_MAX_VAR to DSC_MAX_VAR]
+***********************************************************************/
+extern int Dsc_CountAnds( char * pDsd )
+{
+ if ( pDsd[1] == 0 )
+ return 0;
+ return Dsc_CountAnds_rec( pDsd, &pDsd, Dsc_ComputeMatches(pDsd) );
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
diff --git a/src/opt/dsc/dsc.h b/src/opt/dsc/dsc.h
new file mode 100644
index 00000000..bf8958ea
--- /dev/null
+++ b/src/opt/dsc/dsc.h
@@ -0,0 +1,91 @@
+/**CFile****************************************************************
+
+ FileName [dsc.h]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Disjoint support decomposition - ICCD'15]
+
+ Synopsis [Disjoint-support decomposition with cofactoring and boolean difference analysis
+ from V. Callegaro, F. S. Marranghello, M. G. A. Martins, R. P. Ribas and A. I. Reis,
+ "Bottom-up disjoint-support decomposition based on cofactor and boolean difference analysis," ICCD'15]
+
+ Author [Vinicius Callegaro, Mayler G. A. Martins, Felipe S. Marranghello, Renato P. Ribas and Andre I. Reis]
+
+ Affiliation [UFRGS - Federal University of Rio Grande do Sul - Brazil]
+
+ Date [Ver. 1.0. Started - October 24, 2014.]
+
+ Revision [$Id: dsc.h,v 1.00 2014/10/24 00:00:00 vcallegaro Exp $]
+
+***********************************************************************/
+
+#ifndef ABC__DSC___h
+#define ABC__DSC___h
+
+
+////////////////////////////////////////////////////////////////////////
+/// INCLUDES ///
+////////////////////////////////////////////////////////////////////////
+#include <stdio.h>
+#include <string.h>
+#include "misc/util/abc_global.h"
+
+////////////////////////////////////////////////////////////////////////
+/// PARAMETERS ///
+////////////////////////////////////////////////////////////////////////
+
+ABC_NAMESPACE_HEADER_START
+
+#define DSC_MAX_VAR 16 // should be 6 or more, i.e. DSC_MAX_VAR >= 6
+#define DSC_MAX_STR DSC_MAX_VAR << 2 // DSC_MAX_VAR * 4
+
+////////////////////////////////////////////////////////////////////////
+/// BASIC TYPES ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// MACRO DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== dsc.c ==========================================================*/
+
+/**
+ * memory allocator with a capacity of storing 3*nVars
+ * truth-tables for negative and positive cofactors and
+ * the boolean difference for each input variable
+ */
+extern word * Dsc_alloc_pool(int nVars);
+
+/**
+ * This method implements the paper proposed by V. Callegaro, F. S. Marranghello, M. G. A. Martins, R. P. Ribas and A. I. Reis,
+ * entitled "Bottom-up disjoint-support decomposition based on cofactor and boolean difference analysis", presented at ICCD 2015.
+ * pTruth: pointer for the truth table representing the target function.
+ * nVarsInit: the number of variables of the truth table of the target function.
+ * pRes: pointer for storing the resulting decomposition, whenever a decomposition can be found.
+ * pool: NULL or a pointer for with a capacity of storing 3*nVars truth-tables. IF NULL, the function will allocate and free the memory of each call.
+ * (the results presented on ICCD paper are running this method with NULL for the memory pool).
+ * The method returns 0 if a full decomposition was found and a negative value otherwise.
+ */
+extern int Dsc_Decompose(word * pTruth, const int nVarsInit, char * const pRes, word *pool);
+
+/**
+ * just free the memory pool
+ */
+extern void Dsc_free_pool(word * pool);
+
+int * Dsc_ComputeMatches( char * p );
+int Dsc_CountAnds_rec( char * pStr, char ** p, int * pMatches );
+extern int Dsc_CountAnds( char * pDsd );
+
+ABC_NAMESPACE_HEADER_END
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/dsc/module.make b/src/opt/dsc/module.make
new file mode 100644
index 00000000..b2fd70c4
--- /dev/null
+++ b/src/opt/dsc/module.make
@@ -0,0 +1 @@
+SRC += src/opt/dsc/dsc.c
diff --git a/src/opt/sbd/module.make b/src/opt/sbd/module.make
new file mode 100644
index 00000000..d966e577
--- /dev/null
+++ b/src/opt/sbd/module.make
@@ -0,0 +1,5 @@
+SRC += src/opt/sbd/sbd.c \
+ src/opt/sbd/sbdCnf.c \
+ src/opt/sbd/sbdCore.c \
+ src/opt/sbd/sbdSat.c \
+ src/opt/sbd/sbdWin.c
diff --git a/src/opt/sbd/sbd.c b/src/opt/sbd/sbd.c
new file mode 100644
index 00000000..4d86d2ee
--- /dev/null
+++ b/src/opt/sbd/sbd.c
@@ -0,0 +1,53 @@
+/**CFile****************************************************************
+
+ FileName [sbd.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [SAT-based optimization using internal don't-cares.]
+
+ Synopsis []
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: sbd.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "sbdInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/opt/sbd/sbd.h b/src/opt/sbd/sbd.h
new file mode 100644
index 00000000..89d29958
--- /dev/null
+++ b/src/opt/sbd/sbd.h
@@ -0,0 +1,75 @@
+/**CFile****************************************************************
+
+ FileName [sbd.h]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [SAT-based optimization using internal don't-cares.]
+
+ Synopsis [External declarations.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: sbd.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#ifndef ABC__opt_sbd__h
+#define ABC__opt_sbd__h
+
+////////////////////////////////////////////////////////////////////////
+/// INCLUDES ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// PARAMETERS ///
+////////////////////////////////////////////////////////////////////////
+
+ABC_NAMESPACE_HEADER_START
+
+////////////////////////////////////////////////////////////////////////
+/// BASIC TYPES ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Sbd_Par_t_ Sbd_Par_t;
+struct Sbd_Par_t_
+{
+ int nLutSize; // target LUT size
+ int nTfoLevels; // the number of TFO levels (windowing)
+ int nTfoFanMax; // the max number of fanouts (windowing)
+ int nWinSizeMax; // maximum window size (windowing)
+ int nBTLimit; // maximum number of SAT conflicts
+ int nWords; // simulation word count
+ int fArea; // area-oriented optimization
+ int fCover; // use complete cover procedure
+ int fVerbose; // verbose flag
+ int fVeryVerbose; // verbose flag
+};
+
+
+////////////////////////////////////////////////////////////////////////
+/// MACRO DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== sbdCnf.c ==========================================================*/
+/*=== sbdCore.c ==========================================================*/
+extern void Sbd_ParSetDefault( Sbd_Par_t * pPars );
+extern Gia_Man_t * Sbd_NtkPerform( Gia_Man_t * p, Sbd_Par_t * pPars );
+
+
+ABC_NAMESPACE_HEADER_END
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/opt/sbd/sbdCnf.c b/src/opt/sbd/sbdCnf.c
new file mode 100644
index 00000000..6291baed
--- /dev/null
+++ b/src/opt/sbd/sbdCnf.c
@@ -0,0 +1,147 @@
+/**CFile****************************************************************
+
+ FileName [sbdCnf.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [SAT-based optimization using internal don't-cares.]
+
+ Synopsis [CNF computation.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: sbdCnf.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "sbdInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Sbd_PrintCnf( Vec_Str_t * vCnf )
+{
+ char Entry;
+ int i, Lit;
+ Vec_StrForEachEntry( vCnf, Entry, i )
+ {
+ Lit = (int)Entry;
+ if ( Lit == -1 )
+ printf( "\n" );
+ else
+ printf( "%s%d ", Abc_LitIsCompl(Lit) ? "-":"", Abc_Lit2Var(Lit) );
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Sbd_TruthToCnf( word Truth, int nVars, Vec_Int_t * vCover, Vec_Str_t * vCnf )
+{
+ Vec_StrClear( vCnf );
+ if ( Truth == 0 || ~Truth == 0 )
+ {
+// assert( nVars == 0 );
+ Vec_StrPush( vCnf, (char)(Truth == 0) );
+ Vec_StrPush( vCnf, (char)-1 );
+ return 1;
+ }
+ else
+ {
+ int i, k, c, RetValue, Literal, Cube, nCubes = 0;
+ assert( nVars > 0 );
+ for ( c = 0; c < 2; c ++ )
+ {
+ Truth = c ? ~Truth : Truth;
+ RetValue = Kit_TruthIsop( (unsigned *)&Truth, nVars, vCover, 0 );
+ assert( RetValue == 0 );
+ nCubes += Vec_IntSize( vCover );
+ Vec_IntForEachEntry( vCover, Cube, i )
+ {
+ for ( k = 0; k < nVars; k++ )
+ {
+ Literal = 3 & (Cube >> (k << 1));
+ if ( Literal == 1 ) // '0' -> pos lit
+ Vec_StrPush( vCnf, (char)Abc_Var2Lit(k, 0) );
+ else if ( Literal == 2 ) // '1' -> neg lit
+ Vec_StrPush( vCnf, (char)Abc_Var2Lit(k, 1) );
+ else if ( Literal != 0 )
+ assert( 0 );
+ }
+ Vec_StrPush( vCnf, (char)Abc_Var2Lit(nVars, c) );
+ Vec_StrPush( vCnf, (char)-1 );
+ }
+ }
+ return nCubes;
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Sbd_TranslateCnf( Vec_Wec_t * vRes, Vec_Str_t * vCnf, Vec_Int_t * vFaninMap, int iPivotVar )
+{
+ Vec_Int_t * vClause;
+ char Entry;
+ int i, Lit;
+ Vec_WecClear( vRes );
+ vClause = Vec_WecPushLevel( vRes );
+ Vec_StrForEachEntry( vCnf, Entry, i )
+ {
+ if ( (int)Entry == -1 )
+ {
+ vClause = Vec_WecPushLevel( vRes );
+ continue;
+ }
+ Lit = Abc_Lit2LitV( Vec_IntArray(vFaninMap), (int)Entry );
+ Lit = Abc_LitNotCond( Lit, Abc_Lit2Var(Lit) == iPivotVar );
+ Vec_IntPush( vClause, Lit );
+ }
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/opt/sbd/sbdCore.c b/src/opt/sbd/sbdCore.c
new file mode 100644
index 00000000..b6ec70f9
--- /dev/null
+++ b/src/opt/sbd/sbdCore.c
@@ -0,0 +1,1520 @@
+/**CFile****************************************************************
+
+ FileName [sbd.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [SAT-based optimization using internal don't-cares.]
+
+ Synopsis []
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: sbd.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "sbdInt.h"
+#include "opt/dau/dau.h"
+#include "misc/tim/tim.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+#define SBD_MAX_LUTSIZE 6
+
+
+typedef struct Sbd_Man_t_ Sbd_Man_t;
+struct Sbd_Man_t_
+{
+ Sbd_Par_t * pPars; // user's parameters
+ Gia_Man_t * pGia; // user's AIG manager (will be modified by adding nodes)
+ Vec_Wec_t * vTfos; // TFO for each node (roots are marked) (windowing)
+ Vec_Int_t * vLutLevs; // LUT level for each node after resynthesis
+ Vec_Int_t * vLutCuts; // LUT cut for each nodes after resynthesis
+ Vec_Int_t * vMirrors; // alternative node
+ Vec_Wrd_t * vSims[4]; // simulation information (main, backup, controlability)
+ Vec_Int_t * vCover; // temporary
+ Vec_Int_t * vLits; // temporary
+ int nConsts; // constants
+ int nChanges; // changes
+ abctime timeWin;
+ abctime timeCnf;
+ abctime timeSat;
+ abctime timeCov;
+ abctime timeEnu;
+ abctime timeOther;
+ abctime timeTotal;
+ // target node
+ int Pivot; // target node
+ Vec_Int_t * vTfo; // TFO (excludes node, includes roots) - precomputed
+ Vec_Int_t * vRoots; // TFO root nodes
+ Vec_Int_t * vWinObjs; // TFI + Pivot + sideTFI + TFO (including roots)
+ Vec_Int_t * vObj2Var; // SAT variables for the window (indexes of objects in vWinObjs)
+ Vec_Int_t * vDivVars; // divisor variables
+ Vec_Int_t * vDivValues; // SAT variables values for the divisor variables
+ Vec_Wec_t * vDivLevels; // divisors collected by levels
+ Vec_Int_t * vCounts[2]; // counters of zeros and ones
+ Vec_Wrd_t * vMatrix; // covering matrix
+ sat_solver * pSat; // SAT solver
+};
+
+static inline int * Sbd_ObjCut( Sbd_Man_t * p, int i ) { return Vec_IntEntryP( p->vLutCuts, (p->pPars->nLutSize + 1) * i ); }
+
+static inline word * Sbd_ObjSim0( Sbd_Man_t * p, int i ) { return Vec_WrdEntryP( p->vSims[0], p->pPars->nWords * i ); }
+static inline word * Sbd_ObjSim1( Sbd_Man_t * p, int i ) { return Vec_WrdEntryP( p->vSims[1], p->pPars->nWords * i ); }
+static inline word * Sbd_ObjSim2( Sbd_Man_t * p, int i ) { return Vec_WrdEntryP( p->vSims[2], p->pPars->nWords * i ); }
+static inline word * Sbd_ObjSim3( Sbd_Man_t * p, int i ) { return Vec_WrdEntryP( p->vSims[3], p->pPars->nWords * i ); }
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Sbd_ParSetDefault( Sbd_Par_t * pPars )
+{
+ memset( pPars, 0, sizeof(Sbd_Par_t) );
+ pPars->nLutSize = 4; // target LUT size
+ pPars->nTfoLevels = 2; // the number of TFO levels (windowing)
+ pPars->nTfoFanMax = 4; // the max number of fanouts (windowing)
+ pPars->nWinSizeMax = 0; // maximum window size (windowing)
+ pPars->nBTLimit = 0; // maximum number of SAT conflicts
+ pPars->nWords = 1; // simulation word count
+ pPars->fArea = 0; // area-oriented optimization
+ pPars->fCover = 0; // use complete cover procedure
+ pPars->fVerbose = 0; // verbose flag
+ pPars->fVeryVerbose = 0; // verbose flag
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes TFO and window roots for all nodes.]
+
+ Description [TFO does not include the node itself. If TFO is empty,
+ it means that the node itself is its own root, which may happen if
+ the node is pointed by a PO or if it has too many fanouts.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Wec_t * Sbd_ManWindowRoots( Gia_Man_t * p, int nTfoLevels, int nTfoFanMax )
+{
+ Vec_Wec_t * vTfos = Vec_WecStart( Gia_ManObjNum(p) ); // TFO nodes with roots marked
+ Vec_Wec_t * vTemp = Vec_WecStart( Gia_ManObjNum(p) ); // storage
+ Vec_Int_t * vNodes, * vNodes0, * vNodes1;
+ Vec_Bit_t * vPoDrivers = Vec_BitStart( Gia_ManObjNum(p) );
+ int i, k, k2, Id, Fan;
+ Gia_ManLevelNum( p );
+ Gia_ManCreateRefs( p );
+ Gia_ManCleanMark0( p );
+ Gia_ManForEachCiId( p, Id, i )
+ {
+ vNodes = Vec_WecEntry( vTemp, Id );
+ Vec_IntGrow( vNodes, 1 );
+ Vec_IntPush( vNodes, Id );
+ }
+ Gia_ManForEachCoDriverId( p, Id, i )
+ Vec_BitWriteEntry( vPoDrivers, Id, 1 );
+ Gia_ManForEachAndId( p, Id )
+ {
+ int fAlwaysRoot = Vec_BitEntry(vPoDrivers, Id) || (Gia_ObjRefNumId(p, Id) >= nTfoFanMax);
+ vNodes0 = Vec_WecEntry( vTemp, Gia_ObjFaninId0(Gia_ManObj(p, Id), Id) );
+ vNodes1 = Vec_WecEntry( vTemp, Gia_ObjFaninId1(Gia_ManObj(p, Id), Id) );
+ vNodes = Vec_WecEntry( vTemp, Id );
+ Vec_IntTwoMerge2( vNodes0, vNodes1, vNodes );
+ k2 = 0;
+ Vec_IntForEachEntry( vNodes, Fan, k )
+ {
+ int fRoot = fAlwaysRoot || (Gia_ObjLevelId(p, Id) - Gia_ObjLevelId(p, Fan) >= nTfoLevels);
+ Vec_WecPush( vTfos, Fan, Abc_Var2Lit(Id, fRoot) );
+ if ( !fRoot ) Vec_IntWriteEntry( vNodes, k2++, Fan );
+ }
+ Vec_IntShrink( vNodes, k2 );
+ if ( !fAlwaysRoot )
+ Vec_IntPush( vNodes, Id );
+ }
+ Vec_WecFree( vTemp );
+ Vec_BitFree( vPoDrivers );
+
+ // print the results
+ if ( 0 )
+ Vec_WecForEachLevel( vTfos, vNodes, i )
+ {
+ if ( !Gia_ObjIsAnd(Gia_ManObj(p, i)) )
+ continue;
+ printf( "Node %3d : ", i );
+ Vec_IntForEachEntry( vNodes, Fan, k )
+ printf( "%d%s ", Abc_Lit2Var(Fan), Abc_LitIsCompl(Fan)? "*":"" );
+ printf( "\n" );
+ }
+
+ return vTfos;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Manager manipulation.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Sbd_Man_t * Sbd_ManStart( Gia_Man_t * pGia, Sbd_Par_t * pPars )
+{
+ int i, w, Id;
+ Sbd_Man_t * p = ABC_CALLOC( Sbd_Man_t, 1 );
+ p->timeTotal = Abc_Clock();
+ p->pPars = pPars;
+ p->pGia = pGia;
+ p->vTfos = Sbd_ManWindowRoots( pGia, pPars->nTfoLevels, pPars->nTfoFanMax );
+ p->vLutLevs = Vec_IntStart( Gia_ManObjNum(pGia) );
+ p->vLutCuts = Vec_IntStart( Gia_ManObjNum(pGia) * (p->pPars->nLutSize + 1) );
+ p->vMirrors = Vec_IntStartFull( Gia_ManObjNum(pGia) );
+ for ( i = 0; i < 4; i++ )
+ p->vSims[i] = Vec_WrdStart( Gia_ManObjNum(pGia) * p->pPars->nWords );
+ // target node
+ p->vCover = Vec_IntAlloc( 100 );
+ p->vLits = Vec_IntAlloc( 100 );
+ p->vRoots = Vec_IntAlloc( 100 );
+ p->vWinObjs = Vec_IntAlloc( Gia_ManObjNum(pGia) );
+ p->vObj2Var = Vec_IntStart( Gia_ManObjNum(pGia) );
+ p->vDivVars = Vec_IntAlloc( 100 );
+ p->vDivValues = Vec_IntAlloc( 100 );
+ p->vDivLevels = Vec_WecAlloc( 100 );
+ p->vCounts[0] = Vec_IntAlloc( 100 );
+ p->vCounts[1] = Vec_IntAlloc( 100 );
+ p->vMatrix = Vec_WrdAlloc( 100 );
+ // start input cuts
+ Gia_ManForEachCiId( pGia, Id, i )
+ {
+ int * pCut = Sbd_ObjCut( p, Id );
+ pCut[0] = 1;
+ pCut[1] = Id;
+ }
+ // generate random input
+ Gia_ManRandom( 1 );
+ Gia_ManForEachCiId( pGia, Id, i )
+ for ( w = 0; w < p->pPars->nWords; w++ )
+ Sbd_ObjSim0(p, Id)[w] = Gia_ManRandomW( 0 );
+ return p;
+}
+void Sbd_ManStop( Sbd_Man_t * p )
+{
+ int i;
+ Vec_WecFree( p->vTfos );
+ Vec_IntFree( p->vLutLevs );
+ Vec_IntFree( p->vLutCuts );
+ Vec_IntFree( p->vMirrors );
+ for ( i = 0; i < 4; i++ )
+ Vec_WrdFree( p->vSims[i] );
+ Vec_IntFree( p->vCover );
+ Vec_IntFree( p->vLits );
+ Vec_IntFree( p->vRoots );
+ Vec_IntFree( p->vWinObjs );
+ Vec_IntFree( p->vObj2Var );
+ Vec_IntFree( p->vDivVars );
+ Vec_IntFree( p->vDivValues );
+ Vec_WecFree( p->vDivLevels );
+ Vec_IntFree( p->vCounts[0] );
+ Vec_IntFree( p->vCounts[1] );
+ Vec_WrdFree( p->vMatrix );
+ if ( p->pSat ) sat_solver_delete( p->pSat );
+ ABC_FREE( p );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Constructing window.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Sbd_ManPropagateControlOne( Sbd_Man_t * p, int Node )
+{
+ Gia_Obj_t * pNode = Gia_ManObj(p->pGia, Node); int w;
+ int iObj0 = Gia_ObjFaninId0(pNode, Node);
+ int iObj1 = Gia_ObjFaninId1(pNode, Node);
+
+// word * pSims = Sbd_ObjSim0(p, Node);
+// word * pSims0 = Sbd_ObjSim0(p, iObj0);
+// word * pSims1 = Sbd_ObjSim0(p, iObj1);
+
+ word * pCtrl = Sbd_ObjSim2(p, Node);
+ word * pCtrl0 = Sbd_ObjSim2(p, iObj0);
+ word * pCtrl1 = Sbd_ObjSim2(p, iObj1);
+
+ word * pDtrl = Sbd_ObjSim3(p, Node);
+ word * pDtrl0 = Sbd_ObjSim3(p, iObj0);
+ word * pDtrl1 = Sbd_ObjSim3(p, iObj1);
+
+// Gia_ObjPrint( p->pGia, pNode );
+// printf( "Node %2d : %d %d\n\n", Node, (int)(pSims[0] & 1), (int)(pCtrl[0] & 1) );
+
+ for ( w = 0; w < p->pPars->nWords; w++ )
+ {
+// word Sim0 = Gia_ObjFaninC0(pNode) ? ~pSims0[w] : pSims0[w];
+// word Sim1 = Gia_ObjFaninC1(pNode) ? ~pSims1[w] : pSims1[w];
+
+ pCtrl0[w] |= pCtrl[w];// & (pSims[w] | Sim1 | (~Sim0 & ~Sim1));
+ pCtrl1[w] |= pCtrl[w];// & (pSims[w] | Sim0 | (~Sim0 & ~Sim1));
+
+ pDtrl0[w] |= pDtrl[w];// & (pSims[w] | Sim1 | (~Sim0 & ~Sim1));
+ pDtrl1[w] |= pDtrl[w];// & (pSims[w] | Sim0 | (~Sim0 & ~Sim1));
+ }
+}
+void Sbd_ManPropagateControl( Sbd_Man_t * p, int Pivot )
+{
+ abctime clk = Abc_Clock();
+ int i, Node;
+ Abc_TtCopy( Sbd_ObjSim3(p, Pivot), Sbd_ObjSim2(p, Pivot), p->pPars->nWords, 0 );
+ // clean controlability
+ for ( i = 0; i < Vec_IntEntry(p->vObj2Var, Pivot) && ((Node = Vec_IntEntry(p->vWinObjs, i)), 1); i++ )
+ {
+ Abc_TtClear( Sbd_ObjSim2(p, Node), p->pPars->nWords );
+ Abc_TtClear( Sbd_ObjSim3(p, Node), p->pPars->nWords );
+ //printf( "Clearing node %d.\n", Node );
+ }
+ // propagate controlability to fanins for the TFI nodes starting from the pivot
+ for ( i = Vec_IntEntry(p->vObj2Var, Pivot); i >= 0 && ((Node = Vec_IntEntry(p->vWinObjs, i)), 1); i-- )
+ if ( Gia_ObjIsAnd(Gia_ManObj(p->pGia, Node)) )
+ Sbd_ManPropagateControlOne( p, Node );
+ p->timeWin += Abc_Clock() - clk;
+}
+void Sbd_ManUpdateOrder( Sbd_Man_t * p, int Pivot )
+{
+ int i, k, Node;
+ Vec_Int_t * vLevel;
+ int nTimeValidDivs = 0;
+ // collect divisors by logic level
+ int LevelMax = Vec_IntEntry(p->vLutLevs, Pivot);
+ Vec_WecClear( p->vDivLevels );
+ Vec_WecInit( p->vDivLevels, LevelMax + 1 );
+ Vec_IntForEachEntry( p->vWinObjs, Node, i )
+ Vec_WecPush( p->vDivLevels, Vec_IntEntry(p->vLutLevs, Node), Node );
+ // sort primary inputs
+ Vec_IntSort( Vec_WecEntry(p->vDivLevels, 0), 0 );
+ // reload divisors
+ Vec_IntClear( p->vWinObjs );
+ Vec_WecForEachLevel( p->vDivLevels, vLevel, i )
+ {
+ Vec_IntForEachEntry( vLevel, Node, k )
+ {
+ Vec_IntWriteEntry( p->vObj2Var, Node, Vec_IntSize(p->vWinObjs) );
+ Vec_IntPush( p->vWinObjs, Node );
+ }
+ // remember divisor cutoff
+ if ( i == LevelMax - 2 )
+ nTimeValidDivs = Vec_IntSize(p->vWinObjs);
+ }
+ assert( nTimeValidDivs > 0 );
+ Vec_IntFill( p->vDivValues, Abc_MinInt(63, nTimeValidDivs), 0 );
+ //printf( "%d ", Abc_MinInt(63, nTimeValidDivs) );
+}
+void Sbd_ManWindowSim_rec( Sbd_Man_t * p, int NodeInit )
+{
+ Gia_Obj_t * pObj;
+ int Node = NodeInit;
+ if ( Vec_IntEntry(p->vMirrors, Node) >= 0 )
+ Node = Abc_Lit2Var( Vec_IntEntry(p->vMirrors, Node) );
+ if ( Gia_ObjIsTravIdCurrentId(p->pGia, Node) )
+ return;
+ Gia_ObjSetTravIdCurrentId(p->pGia, Node);
+ pObj = Gia_ManObj( p->pGia, Node );
+ if ( Gia_ObjIsAnd(pObj) )
+ {
+ Sbd_ManWindowSim_rec( p, Gia_ObjFaninId0(pObj, Node) );
+ Sbd_ManWindowSim_rec( p, Gia_ObjFaninId1(pObj, Node) );
+ }
+ if ( !pObj->fMark0 )
+ {
+ Vec_IntWriteEntry( p->vObj2Var, Node, Vec_IntSize(p->vWinObjs) );
+ Vec_IntPush( p->vWinObjs, Node );
+ }
+ if ( Gia_ObjIsCi(pObj) )
+ return;
+ // simulate
+ assert( Gia_ObjIsAnd(pObj) );
+ if ( Gia_ObjIsXor(pObj) )
+ {
+ Abc_TtXor( Sbd_ObjSim0(p, Node),
+ Sbd_ObjSim0(p, Gia_ObjFaninId0(pObj, Node)),
+ Sbd_ObjSim0(p, Gia_ObjFaninId1(pObj, Node)),
+ p->pPars->nWords,
+ Gia_ObjFaninC0(pObj) ^ Gia_ObjFaninC1(pObj) );
+
+ if ( pObj->fMark0 )
+ Abc_TtXor( Sbd_ObjSim1(p, Node),
+ Gia_ObjFanin0(pObj)->fMark0 ? Sbd_ObjSim1(p, Gia_ObjFaninId0(pObj, Node)) : Sbd_ObjSim0(p, Gia_ObjFaninId0(pObj, Node)),
+ Gia_ObjFanin1(pObj)->fMark0 ? Sbd_ObjSim1(p, Gia_ObjFaninId1(pObj, Node)) : Sbd_ObjSim0(p, Gia_ObjFaninId1(pObj, Node)),
+ p->pPars->nWords,
+ Gia_ObjFaninC0(pObj) ^ Gia_ObjFaninC1(pObj) );
+ }
+ else
+ {
+ Abc_TtAndCompl( Sbd_ObjSim0(p, Node),
+ Sbd_ObjSim0(p, Gia_ObjFaninId0(pObj, Node)), Gia_ObjFaninC0(pObj),
+ Sbd_ObjSim0(p, Gia_ObjFaninId1(pObj, Node)), Gia_ObjFaninC1(pObj),
+ p->pPars->nWords );
+
+ if ( pObj->fMark0 )
+ Abc_TtAndCompl( Sbd_ObjSim1(p, Node),
+ Gia_ObjFanin0(pObj)->fMark0 ? Sbd_ObjSim1(p, Gia_ObjFaninId0(pObj, Node)) : Sbd_ObjSim0(p, Gia_ObjFaninId0(pObj, Node)), Gia_ObjFaninC0(pObj),
+ Gia_ObjFanin1(pObj)->fMark0 ? Sbd_ObjSim1(p, Gia_ObjFaninId1(pObj, Node)) : Sbd_ObjSim0(p, Gia_ObjFaninId1(pObj, Node)), Gia_ObjFaninC1(pObj),
+ p->pPars->nWords );
+ }
+ if ( Node != NodeInit )
+ Abc_TtCopy( Sbd_ObjSim0(p, NodeInit), Sbd_ObjSim0(p, Node), p->pPars->nWords, Abc_LitIsCompl(Vec_IntEntry(p->vMirrors, NodeInit)) );
+}
+int Sbd_ManWindow( Sbd_Man_t * p, int Pivot )
+{
+ abctime clk = Abc_Clock();
+ int i, Node;
+ // assign pivot and TFO (assume siminfo is assigned at the PIs)
+ p->Pivot = Pivot;
+ p->vTfo = Vec_WecEntry( p->vTfos, Pivot );
+ // add constant node
+ Vec_IntClear( p->vWinObjs );
+ Vec_IntWriteEntry( p->vObj2Var, 0, Vec_IntSize(p->vWinObjs) );
+ Vec_IntPush( p->vWinObjs, 0 );
+ // simulate TFI cone
+ Gia_ManIncrementTravId( p->pGia );
+ Gia_ObjSetTravIdCurrentId(p->pGia, 0);
+ Sbd_ManWindowSim_rec( p, Pivot );
+ Sbd_ManUpdateOrder( p, Pivot );
+ // simulate node
+ Gia_ManObj(p->pGia, Pivot)->fMark0 = 1;
+ Abc_TtCopy( Sbd_ObjSim1(p, Pivot), Sbd_ObjSim0(p, Pivot), p->pPars->nWords, 1 );
+ // mark TFO and simulate extended TFI without adding TFO nodes
+ Vec_IntClear( p->vRoots );
+ Vec_IntForEachEntry( p->vTfo, Node, i )
+ {
+ Gia_ManObj(p->pGia, Abc_Lit2Var(Node))->fMark0 = 1;
+ if ( !Abc_LitIsCompl(Node) )
+ continue;
+ Sbd_ManWindowSim_rec( p, Abc_Lit2Var(Node) );
+ Vec_IntPush( p->vRoots, Abc_Lit2Var(Node) );
+ }
+ // add TFO nodes and remove marks
+ Gia_ManObj(p->pGia, Pivot)->fMark0 = 0;
+ Vec_IntForEachEntry( p->vTfo, Node, i )
+ {
+ Gia_ManObj(p->pGia, Abc_Lit2Var(Node))->fMark0 = 0;
+ Vec_IntWriteEntry( p->vObj2Var, Abc_Lit2Var(Node), Vec_IntSize(p->vWinObjs) );
+ Vec_IntPush( p->vWinObjs, Abc_Lit2Var(Node) );
+ }
+ // compute controlability for node
+ if ( Vec_IntSize(p->vTfo) == 0 )
+ Abc_TtFill( Sbd_ObjSim2(p, Pivot), p->pPars->nWords );
+ else
+ Abc_TtClear( Sbd_ObjSim2(p, Pivot), p->pPars->nWords );
+ Vec_IntForEachEntry( p->vTfo, Node, i )
+ if ( Abc_LitIsCompl(Node) ) // root
+ Abc_TtOrXor( Sbd_ObjSim2(p, Pivot), Sbd_ObjSim0(p, Abc_Lit2Var(Node)), Sbd_ObjSim1(p, Abc_Lit2Var(Node)), p->pPars->nWords );
+ p->timeWin += Abc_Clock() - clk;
+ // propagate controlability to fanins for the TFI nodes starting from the pivot
+ Sbd_ManPropagateControl( p, Pivot );
+ assert( Vec_IntSize(p->vDivValues) < 64 );
+ return (int)(Vec_IntSize(p->vDivValues) >= 64);
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Sbd_ManCheckConst( Sbd_Man_t * p, int Pivot )
+{
+ extern void Sbd_ManPrintObj( Sbd_Man_t * p, int Pivot );
+ int nMintCount = 1;
+ Vec_Ptr_t * vSims;
+ word * pSims = Sbd_ObjSim0( p, Pivot );
+ word * pCtrl = Sbd_ObjSim2( p, Pivot );
+ int PivotVar = Vec_IntEntry(p->vObj2Var, Pivot);
+ int RetValue, i, iObj, Ind, fFindOnset, nCares[2] = {0};
+ abctime clk = Abc_Clock();
+ extern int Sbd_ManCollectConstants( sat_solver * pSat, int nCareMints[2], int PivotVar, word * pVarSims[], Vec_Int_t * vInds );
+ extern sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, Vec_Int_t * vMirrors, int Pivot, Vec_Int_t * vWinObjs, Vec_Int_t * vObj2Var, Vec_Int_t * vTfo, Vec_Int_t * vRoots );
+ p->pSat = Sbd_ManSatSolver( p->pSat, p->pGia, p->vMirrors, Pivot, p->vWinObjs, p->vObj2Var, p->vTfo, p->vRoots );
+ p->timeCnf += Abc_Clock() - clk;
+ if ( p->pSat == NULL )
+ {
+ if ( p->pPars->fVerbose )
+ printf( "Found stuck-at-%d node %d.\n", 0, Pivot );
+ Vec_IntWriteEntry( p->vLutLevs, Pivot, 0 );
+ p->nConsts++;
+ return 0;
+ }
+ //return -1;
+ //Sbd_ManPrintObj( p, Pivot );
+
+ // count the number of on-set and off-set care-set minterms
+ Vec_IntClear( p->vLits );
+ for ( i = 0; i < 64; i++ )
+ if ( Abc_TtGetBit(pCtrl, i) )
+ nCares[Abc_TtGetBit(pSims, i)]++;
+ else
+ Vec_IntPush( p->vLits, i );
+ fFindOnset = (int)(nCares[0] < nCares[1]);
+ if ( nCares[0] >= nMintCount && nCares[1] >= nMintCount )
+ return -1;
+ // find how many do we need
+ nCares[0] = nCares[0] < nMintCount ? nMintCount - nCares[0] : 0;
+ nCares[1] = nCares[1] < nMintCount ? nMintCount - nCares[1] : 0;
+
+ if ( p->pPars->fVerbose )
+ printf( "Computing %d offset and %d onset minterms for node %d.\n", nCares[0], nCares[1], Pivot );
+
+ if ( Vec_IntSize(p->vLits) >= nCares[0] + nCares[1] )
+ Vec_IntShrink( p->vLits, nCares[0] + nCares[1] );
+ else
+ {
+ // collect places to insert new minterms
+ for ( i = 0; i < 64 && Vec_IntSize(p->vLits) < nCares[0] + nCares[1]; i++ )
+ if ( fFindOnset == Abc_TtGetBit(pSims, i) )
+ Vec_IntPush( p->vLits, i );
+ }
+ // collect simulation pointers
+ vSims = Vec_PtrAlloc( PivotVar + 1 );
+ Vec_IntForEachEntry( p->vWinObjs, iObj, i )
+ {
+ Vec_PtrPush( vSims, Sbd_ObjSim0(p, iObj) );
+ if ( iObj == Pivot )
+ break;
+ }
+ assert( i == PivotVar );
+ // compute patterns
+ RetValue = Sbd_ManCollectConstants( p->pSat, nCares, PivotVar, (word **)Vec_PtrArray(vSims), p->vLits );
+ // print computed miterms
+ if ( 0 && RetValue < 0 )
+ {
+ Vec_Int_t * vPis = Vec_WecEntry(p->vDivLevels, 0);
+ int i, k, Ind;
+ printf( "Additional minterms:\n" );
+ Vec_IntForEachEntry( p->vLits, Ind, k )
+ {
+ for ( i = 0; i < Vec_IntSize(vPis); i++ )
+ printf( "%d", Abc_TtGetBit( (word *)Vec_PtrEntry(vSims, Vec_IntEntry(p->vWinObjs, i)), Ind ) );
+ printf( "\n" );
+ }
+ }
+ Vec_PtrFree( vSims );
+ if ( RetValue >= 0 )
+ {
+ if ( p->pPars->fVerbose )
+ printf( "Found stuck-at-%d node %d.\n", RetValue, Pivot );
+ Vec_IntWriteEntry( p->vLutLevs, Pivot, 0 );
+ p->nConsts++;
+ return RetValue;
+ }
+ // set controlability of these minterms
+ Vec_IntForEachEntry( p->vLits, Ind, i )
+ Abc_TtSetBit( pCtrl, Ind );
+ // propagate controlability to fanins for the TFI nodes starting from the pivot
+ Sbd_ManPropagateControl( p, Pivot );
+ // double check that we now have enough minterms
+ for ( i = 0; i < 64; i++ )
+ if ( Abc_TtGetBit(pCtrl, i) )
+ nCares[Abc_TtGetBit(pSims, i)]++;
+ assert( nCares[0] >= nMintCount && nCares[1] >= nMintCount );
+ return -1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Transposing 64-bit matrix.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Sbd_TransposeMatrix64( word A[64] )
+{
+ int j, k;
+ word t, m = 0x00000000FFFFFFFF;
+ for ( j = 32; j != 0; j = j >> 1, m = m ^ (m << j) )
+ {
+ for ( k = 0; k < 64; k = (k + j + 1) & ~j )
+ {
+ t = (A[k] ^ (A[k+j] >> j)) & m;
+ A[k] = A[k] ^ t;
+ A[k+j] = A[k+j] ^ (t << j);
+ }
+ }
+}
+static inline void Sbd_PrintMatrix64( word A[64] )
+{
+ int j, k;
+ for ( j = 0; j < 64; j++, printf("\n") )
+ for ( k = 0; k < 64; k++ )
+ printf( "%d", (int)((A[j] >> k) & 1) );
+ printf( "\n" );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Profiling divisor candidates.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Sbd_ManPrintObj( Sbd_Man_t * p, int Pivot )
+{
+ int nDivs = Vec_IntEntry(p->vObj2Var, Pivot) + 1;
+ int i, k, k0, k1, Id, Bit0, Bit1;
+
+ Vec_IntForEachEntryStop( p->vWinObjs, Id, i, nDivs )
+ printf( "%3d : ", Id ), Extra_PrintBinary( stdout, (unsigned *)Sbd_ObjSim0(p, Id), 64 ), printf( "\n" );
+
+ assert( p->Pivot == Pivot );
+ Vec_IntClear( p->vCounts[0] );
+ Vec_IntClear( p->vCounts[1] );
+
+ printf( "Node %d. Useful divisors = %d.\n", Pivot, Vec_IntSize(p->vDivValues) );
+ printf( "Lev : " );
+ Vec_IntForEachEntryStop( p->vWinObjs, Id, i, nDivs )
+ {
+ if ( i == nDivs-1 )
+ printf( " " );
+ printf( "%d", Vec_IntEntry(p->vLutLevs, Id) );
+ }
+ printf( "\n" );
+ printf( "\n" );
+
+ if ( nDivs > 99 )
+ {
+ printf( " : " );
+ Vec_IntForEachEntryStop( p->vWinObjs, Id, i, nDivs )
+ {
+ if ( i == nDivs-1 )
+ printf( " " );
+ printf( "%d", Id / 100 );
+ }
+ printf( "\n" );
+ }
+ if ( nDivs > 9 )
+ {
+ printf( " : " );
+ Vec_IntForEachEntryStop( p->vWinObjs, Id, i, nDivs )
+ {
+ if ( i == nDivs-1 )
+ printf( " " );
+ printf( "%d", (Id % 100) / 10 );
+ }
+ printf( "\n" );
+ }
+ if ( nDivs > 0 )
+ {
+ printf( " : " );
+ Vec_IntForEachEntryStop( p->vWinObjs, Id, i, nDivs )
+ {
+ if ( i == nDivs-1 )
+ printf( " " );
+ printf( "%d", Id % 10 );
+ }
+ printf( "\n" );
+ printf( "\n" );
+ }
+
+ // sampling matrix
+ for ( k = 0; k < p->pPars->nWords * 64; k++ )
+ {
+ if ( !Abc_TtGetBit(Sbd_ObjSim2(p, Pivot), k) )
+ continue;
+
+ printf( "%3d : ", k );
+ Vec_IntForEachEntryStop( p->vWinObjs, Id, i, nDivs )
+ {
+ word * pSims = Sbd_ObjSim0( p, Id );
+ word * pCtrl = Sbd_ObjSim2( p, Id );
+ if ( i == nDivs-1 )
+ {
+ if ( Abc_TtGetBit(pCtrl, k) )
+ Vec_IntPush( p->vCounts[Abc_TtGetBit(pSims, k)], k );
+ printf( " " );
+ }
+ printf( "%c", Abc_TtGetBit(pCtrl, k) ? '0' + Abc_TtGetBit(pSims, k) : '.' );
+ }
+ printf( "\n" );
+
+ printf( "%3d : ", k );
+ Vec_IntForEachEntryStop( p->vWinObjs, Id, i, nDivs )
+ {
+ word * pSims = Sbd_ObjSim0( p, Id );
+ word * pCtrl = Sbd_ObjSim3( p, Id );
+ if ( i == nDivs-1 )
+ {
+ if ( Abc_TtGetBit(pCtrl, k) )
+ Vec_IntPush( p->vCounts[Abc_TtGetBit(pSims, k)], k );
+ printf( " " );
+ }
+ printf( "%c", Abc_TtGetBit(pCtrl, k) ? '0' + Abc_TtGetBit(pSims, k) : '.' );
+ }
+ printf( "\n" );
+
+ printf( "Sims: " );
+ Vec_IntForEachEntryStop( p->vWinObjs, Id, i, nDivs )
+ {
+ word * pSims = Sbd_ObjSim0( p, Id );
+ //word * pCtrl = Sbd_ObjSim2( p, Id );
+ if ( i == nDivs-1 )
+ printf( " " );
+ printf( "%c", '0' + Abc_TtGetBit(pSims, k) );
+ }
+ printf( "\n" );
+
+ printf( "Ctrl: " );
+ Vec_IntForEachEntryStop( p->vWinObjs, Id, i, nDivs )
+ {
+ //word * pSims = Sbd_ObjSim0( p, Id );
+ word * pCtrl = Sbd_ObjSim2( p, Id );
+ if ( i == nDivs-1 )
+ printf( " " );
+ printf( "%c", '0' + Abc_TtGetBit(pCtrl, k) );
+ }
+ printf( "\n" );
+
+
+ printf( "\n" );
+ }
+ // covering table
+ printf( "Exploring %d x %d covering table.\n", Vec_IntSize(p->vCounts[0]), Vec_IntSize(p->vCounts[1]) );
+/*
+ Vec_IntForEachEntryStop( p->vCounts[0], Bit0, k0, Abc_MinInt(Vec_IntSize(p->vCounts[0]), 8) )
+ Vec_IntForEachEntryStop( p->vCounts[1], Bit1, k1, Abc_MinInt(Vec_IntSize(p->vCounts[1]), 8) )
+ {
+ printf( "%3d %3d : ", Bit0, Bit1 );
+ Vec_IntForEachEntryStop( p->vWinObjs, Id, i, nDivs )
+ {
+ word * pSims = Sbd_ObjSim0( p, Id );
+ word * pCtrl = Sbd_ObjSim2( p, Id );
+ if ( i == nDivs-1 )
+ printf( " " );
+ printf( "%c", (Abc_TtGetBit(pCtrl, Bit0) && Abc_TtGetBit(pCtrl, Bit1) && Abc_TtGetBit(pSims, Bit0) != Abc_TtGetBit(pSims, Bit1)) ? '1' : '.' );
+ }
+ printf( "\n" );
+ }
+*/
+ Vec_WrdClear( p->vMatrix );
+ Vec_IntForEachEntryStop( p->vCounts[0], Bit0, k0, Abc_MinInt(Vec_IntSize(p->vCounts[0]), 64) )
+ Vec_IntForEachEntryStop( p->vCounts[1], Bit1, k1, Abc_MinInt(Vec_IntSize(p->vCounts[1]), 64) )
+ {
+ word Row = 0;
+ Vec_IntForEachEntryStop( p->vWinObjs, Id, i, nDivs )
+ {
+ word * pSims = Sbd_ObjSim0( p, Id );
+ word * pCtrl = Sbd_ObjSim2( p, Id );
+ if ( Abc_TtGetBit(pCtrl, Bit0) && Abc_TtGetBit(pCtrl, Bit1) && Abc_TtGetBit(pSims, Bit0) != Abc_TtGetBit(pSims, Bit1) )
+ Abc_TtXorBit( &Row, i );
+ }
+ if ( Vec_WrdPushUnique( p->vMatrix, Row ) )
+ continue;
+ for ( i = 0; i < nDivs; i++ )
+ printf( "%d", (int)((Row >> i) & 1) );
+ printf( "\n" );
+ }
+}
+
+void Sbd_ManMatrPrint( word Cover[64], int nCol, int nRows )
+{
+ int i, k;
+ for ( i = 0; i <= nCol; i++ )
+ {
+ printf( "%2d : ", i );
+ for ( k = 0; k < nRows; k++ )
+ for ( k = 0; k < nRows; k++ )
+ printf( "%d", (int)((Cover[i] >> k) & 1) );
+ printf( "\n");
+ }
+ printf( "\n");
+}
+static inline void Sbd_ManCoverReverseOrder( word Cover[64] )
+{
+ int i;
+ for ( i = 0; i < 32; i++ )
+ {
+ word Cube = Cover[i];
+ Cover[i] = Cover[63-i];
+ Cover[63-i] = Cube;
+ }
+}
+
+static inline int Sbd_ManAddCube1( word Cover[64], int nRows, word Cube )
+{
+ int n, m;
+ if ( 0 )
+ {
+ printf( "Adding cube: " );
+ for ( n = 0; n < 64; n++ )
+ printf( "%d", (int)((Cube >> n) & 1) );
+ printf( "\n" );
+ }
+ // do not add contained Cube
+ assert( nRows <= 64 );
+ for ( n = 0; n < nRows; n++ )
+ if ( (Cover[n] & Cube) == Cover[n] ) // Cube is contained
+ return nRows;
+ // remove rows contained by Cube
+ for ( n = m = 0; n < nRows; n++ )
+ if ( (Cover[n] & Cube) != Cube ) // Cover[n] is not contained
+ Cover[m++] = Cover[n];
+ if ( m < 64 )
+ Cover[m++] = Cube;
+ for ( n = m; n < nRows; n++ )
+ Cover[n] = 0;
+ nRows = m;
+ return nRows;
+}
+static inline int Sbd_ManAddCube2( word Cover[2][64], int nRows, word Cube[2] )
+{
+ int n, m;
+ // do not add contained Cube
+ assert( nRows <= 64 );
+ for ( n = 0; n < nRows; n++ )
+ if ( (Cover[0][n] & Cube[0]) == Cover[0][n] && (Cover[1][n] & Cube[1]) == Cover[1][n] ) // Cube is contained
+ return nRows;
+ // remove rows contained by Cube
+ for ( n = m = 0; n < nRows; n++ )
+ if ( (Cover[0][n] & Cube[0]) != Cube[0] || (Cover[1][n] & Cube[1]) != Cube[1] ) // Cover[n] is not contained
+ {
+ Cover[0][m] = Cover[0][n];
+ Cover[1][m] = Cover[1][n];
+ m++;
+ }
+ if ( m < 64 )
+ {
+ Cover[0][m] = Cube[0];
+ Cover[1][m] = Cube[1];
+ m++;
+ }
+ for ( n = m; n < nRows; n++ )
+ Cover[0][n] = Cover[1][n] = 0;
+ nRows = m;
+ return nRows;
+}
+
+static inline int Sbd_ManFindCandsSimple( Sbd_Man_t * p, word Cover[64], int nDivs )
+{
+ int c0, c1, c2, c3;
+ word Target = Cover[nDivs];
+ Vec_IntClear( p->vDivVars );
+ for ( c0 = 0; c0 < nDivs; c0++ )
+ if ( Cover[c0] == Target )
+ {
+ Vec_IntPush( p->vDivVars, c0 );
+ return 1;
+ }
+
+ for ( c0 = 0; c0 < nDivs; c0++ )
+ for ( c1 = c0+1; c1 < nDivs; c1++ )
+ if ( (Cover[c0] | Cover[c1]) == Target )
+ {
+ Vec_IntPush( p->vDivVars, c0 );
+ Vec_IntPush( p->vDivVars, c1 );
+ return 1;
+ }
+
+ for ( c0 = 0; c0 < nDivs; c0++ )
+ for ( c1 = c0+1; c1 < nDivs; c1++ )
+ for ( c2 = c1+1; c2 < nDivs; c2++ )
+ if ( (Cover[c0] | Cover[c1] | Cover[c2]) == Target )
+ {
+ Vec_IntPush( p->vDivVars, c0 );
+ Vec_IntPush( p->vDivVars, c1 );
+ Vec_IntPush( p->vDivVars, c2 );
+ return 1;
+ }
+
+ for ( c0 = 0; c0 < nDivs; c0++ )
+ for ( c1 = c0+1; c1 < nDivs; c1++ )
+ for ( c2 = c1+1; c2 < nDivs; c2++ )
+ for ( c3 = c2+1; c3 < nDivs; c3++ )
+ {
+ if ( (Cover[c0] | Cover[c1] | Cover[c2] | Cover[c3]) == Target )
+ {
+ Vec_IntPush( p->vDivVars, c0 );
+ Vec_IntPush( p->vDivVars, c1 );
+ Vec_IntPush( p->vDivVars, c2 );
+ Vec_IntPush( p->vDivVars, c3 );
+ return 1;
+ }
+ }
+ return 0;
+}
+
+static inline int Sbd_ManFindCands( Sbd_Man_t * p, word Cover[64], int nDivs )
+{
+ int Ones[64], Order[64];
+ int Limits[4] = { nDivs/4+1, nDivs/3+2, nDivs/2+3, nDivs };
+ int c0, c1, c2, c3;
+ word Target = Cover[nDivs];
+
+ if ( nDivs < 8 || p->pPars->fCover )
+ return Sbd_ManFindCandsSimple( p, Cover, nDivs );
+
+ Vec_IntClear( p->vDivVars );
+ for ( c0 = 0; c0 < nDivs; c0++ )
+ if ( Cover[c0] == Target )
+ {
+ Vec_IntPush( p->vDivVars, c0 );
+ return 1;
+ }
+
+ for ( c0 = 0; c0 < nDivs; c0++ )
+ for ( c1 = c0+1; c1 < nDivs; c1++ )
+ if ( (Cover[c0] | Cover[c1]) == Target )
+ {
+ Vec_IntPush( p->vDivVars, c0 );
+ Vec_IntPush( p->vDivVars, c1 );
+ return 1;
+ }
+
+ // count ones
+ for ( c0 = 0; c0 < nDivs; c0++ )
+ Ones[c0] = Abc_TtCountOnes( Cover[c0] );
+
+ // sort by the number of ones
+ for ( c0 = 0; c0 < nDivs; c0++ )
+ Order[c0] = c0;
+ Vec_IntSelectSortCost2Reverse( Order, nDivs, Ones );
+
+ // sort with limits
+ for ( c0 = 0; c0 < Limits[0]; c0++ )
+ for ( c1 = c0+1; c1 < Limits[1]; c1++ )
+ for ( c2 = c1+1; c2 < Limits[2]; c2++ )
+ if ( (Cover[Order[c0]] | Cover[Order[c1]] | Cover[Order[c2]]) == Target )
+ {
+ Vec_IntPush( p->vDivVars, Order[c0] );
+ Vec_IntPush( p->vDivVars, Order[c1] );
+ Vec_IntPush( p->vDivVars, Order[c2] );
+ return 1;
+ }
+
+ for ( c0 = 0; c0 < Limits[0]; c0++ )
+ for ( c1 = c0+1; c1 < Limits[1]; c1++ )
+ for ( c2 = c1+1; c2 < Limits[2]; c2++ )
+ for ( c3 = c2+1; c3 < Limits[3]; c3++ )
+ {
+ if ( (Cover[Order[c0]] | Cover[Order[c1]] | Cover[Order[c2]] | Cover[Order[c3]]) == Target )
+ {
+ Vec_IntPush( p->vDivVars, Order[c0] );
+ Vec_IntPush( p->vDivVars, Order[c1] );
+ Vec_IntPush( p->vDivVars, Order[c2] );
+ Vec_IntPush( p->vDivVars, Order[c3] );
+ return 1;
+ }
+ }
+ return 0;
+}
+
+
+int Sbd_ManExplore( Sbd_Man_t * p, int Pivot, word * pTruth )
+{
+ int fVerbose = 0;
+ abctime clk, clkSat = 0, clkEnu = 0, clkAll = Abc_Clock();
+ int nIters, nItersMax = 32;
+ extern word Sbd_ManSolve( sat_solver * pSat, int PivotVar, int FreeVar, Vec_Int_t * vDivVars, Vec_Int_t * vValues, Vec_Int_t * vTemp );
+
+ word MatrS[64] = {0}, MatrC[2][64] = {{0}}, Cubes[2][2][64] = {{{0}}}, Cover[64] = {0}, Cube, CubeNew[2];
+ int i, k, n, Index, nCubes[2] = {0}, nRows = 0, nRowsOld;
+
+ int nDivs = Vec_IntSize(p->vDivValues);
+ int PivotVar = Vec_IntEntry(p->vObj2Var, Pivot);
+ int FreeVar = Vec_IntSize(p->vWinObjs) + Vec_IntSize(p->vTfo) + Vec_IntSize(p->vRoots);
+ int RetValue = 0;
+
+ if ( p->pPars->fVerbose )
+ printf( "Node %d. Useful divisors = %d.\n", Pivot, nDivs );
+
+ if ( fVerbose )
+ Sbd_ManPrintObj( p, Pivot );
+
+ // collect bit-matrices
+ for ( i = 0; i < nDivs; i++ )
+ {
+ MatrS[63-i] = *Sbd_ObjSim0( p, Vec_IntEntry(p->vWinObjs, i) );
+ MatrC[0][63-i] = *Sbd_ObjSim2( p, Vec_IntEntry(p->vWinObjs, i) );
+ MatrC[1][63-i] = *Sbd_ObjSim3( p, Vec_IntEntry(p->vWinObjs, i) );
+ }
+ MatrS[63-i] = *Sbd_ObjSim0( p, Pivot );
+ MatrC[0][63-i] = *Sbd_ObjSim2( p, Pivot );
+ MatrC[1][63-i] = *Sbd_ObjSim3( p, Pivot );
+
+ //Sbd_PrintMatrix64( MatrS );
+ Sbd_TransposeMatrix64( MatrS );
+ Sbd_TransposeMatrix64( MatrC[0] );
+ Sbd_TransposeMatrix64( MatrC[1] );
+ //Sbd_PrintMatrix64( MatrS );
+
+ // collect cubes
+ for ( i = 0; i < 64; i++ )
+ {
+ assert( Abc_TtGetBit(&MatrC[0][i], nDivs) == Abc_TtGetBit(&MatrC[1][i], nDivs) );
+ if ( !Abc_TtGetBit(&MatrC[0][i], nDivs) )
+ continue;
+ Index = Abc_TtGetBit(&MatrS[i], nDivs); // Index==0 offset; Index==1 onset
+ for ( n = 0; n < 2; n++ )
+ {
+ if ( n && MatrC[0][i] == MatrC[1][i] )
+ continue;
+ assert( MatrC[n][i] );
+ CubeNew[0] = ~MatrS[i] & MatrC[n][i];
+ CubeNew[1] = MatrS[i] & MatrC[n][i];
+ assert( CubeNew[0] || CubeNew[1] );
+ nCubes[Index] = Sbd_ManAddCube2( Cubes[Index], nCubes[Index], CubeNew );
+ }
+ }
+
+ if ( p->pPars->fVerbose )
+ printf( "Generated matrix with %d x %d entries.\n", nCubes[0], nCubes[1] );
+
+ if ( p->pPars->fVerbose )
+ for ( n = 0; n < 2; n++ )
+ {
+ printf( "%s:\n", n ? "Onset" : "Offset" );
+ for ( i = 0; i < nCubes[n]; i++, printf( "\n" ) )
+ for ( k = 0; k < 64; k++ )
+ if ( Abc_TtGetBit(&Cubes[n][0][i], k) )
+ printf( "0" );
+ else if ( Abc_TtGetBit(&Cubes[n][1][i], k) )
+ printf( "1" );
+ else
+ printf( "." );
+ printf( "\n" );
+ }
+
+ // create covering table
+ nRows = 0;
+ for ( i = 0; i < nCubes[0] && nRows < 32; i++ )
+ for ( k = 0; k < nCubes[1] && nRows < 32; k++ )
+ {
+ Cube = (Cubes[0][1][i] & Cubes[1][0][k]) | (Cubes[0][0][i] & Cubes[1][1][k]);
+ assert( Cube );
+ nRows = Sbd_ManAddCube1( Cover, nRows, Cube );
+ }
+
+ Sbd_ManCoverReverseOrder( Cover );
+
+ if ( p->pPars->fVerbose )
+ printf( "Generated cover with %d entries.\n", nRows );
+
+ //if ( p->pPars->fVerbose )
+ //Sbd_PrintMatrix64( Cover );
+ Sbd_TransposeMatrix64( Cover );
+ //if ( p->pPars->fVerbose )
+ //Sbd_PrintMatrix64( Cover );
+
+ Sbd_ManCoverReverseOrder( Cover );
+
+ nRowsOld = nRows;
+ for ( nIters = 0; nIters < nItersMax && nRows < 64; nIters++ )
+ {
+ if ( p->pPars->fVerbose )
+ Sbd_ManMatrPrint( Cover, nDivs, nRows );
+
+ clk = Abc_Clock();
+ if ( !Sbd_ManFindCands( p, Cover, nDivs ) )
+ {
+ if ( p->pPars->fVerbose )
+ printf( "Cannot find a feasible cover.\n" );
+ clkEnu += Abc_Clock() - clk;
+ clkAll = Abc_Clock() - clkAll - clkSat - clkEnu;
+ p->timeSat += clkSat;
+ p->timeCov += clkAll;
+ p->timeEnu += clkEnu;
+ return RetValue;
+ }
+ clkEnu += Abc_Clock() - clk;
+
+ if ( p->pPars->fVerbose )
+ printf( "Candidate support: " ),
+ Vec_IntPrint( p->vDivVars );
+
+ clk = Abc_Clock();
+ *pTruth = Sbd_ManSolve( p->pSat, PivotVar, FreeVar+nIters, p->vDivVars, p->vDivValues, p->vLits );
+ clkSat += Abc_Clock() - clk;
+
+ if ( *pTruth == SBD_SAT_UNDEC )
+ printf( "Node %d: Undecided.\n", Pivot );
+ else if ( *pTruth == SBD_SAT_SAT )
+ {
+ if ( p->pPars->fVerbose )
+ {
+ int i;
+ printf( "Node %d: SAT.\n", Pivot );
+ for ( i = 0; i < nDivs; i++ )
+ printf( "%d", i % 10 );
+ printf( "\n" );
+ for ( i = 0; i < nDivs; i++ )
+ printf( "%c", (Vec_IntEntry(p->vDivValues, i) & 0x4) ? '0' + (Vec_IntEntry(p->vDivValues, i) & 1) : 'x' );
+ printf( "\n" );
+ for ( i = 0; i < nDivs; i++ )
+ printf( "%c", (Vec_IntEntry(p->vDivValues, i) & 0x8) ? '0' + ((Vec_IntEntry(p->vDivValues, i) >> 1) & 1) : 'x' );
+ printf( "\n" );
+ }
+ // add row to the covering table
+ for ( i = 0; i < nDivs; i++ )
+ if ( Vec_IntEntry(p->vDivValues, i) == 0xE || Vec_IntEntry(p->vDivValues, i) == 0xD )
+ Cover[i] |= ((word)1 << nRows);
+ Cover[nDivs] |= ((word)1 << nRows);
+ nRows++;
+ }
+ else
+ {
+ if ( p->pPars->fVerbose )
+ {
+ printf( "Node %d: UNSAT.\n", Pivot );
+ Extra_PrintBinary( stdout, (unsigned *)pTruth, 1 << Vec_IntSize(p->vDivVars) ), printf( "\n" );
+ }
+ RetValue = 1;
+ break;
+ }
+ //break;
+ }
+ //printf( "Node %4d : Iter = %4d Start table = %4d Final table = %4d\n", Pivot, nIters, nRowsOld, nRows );
+ clkAll = Abc_Clock() - clkAll - clkSat - clkEnu;
+ p->timeSat += clkSat;
+ p->timeCov += clkAll;
+ p->timeEnu += clkEnu;
+ return RetValue;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes delay-oriented k-feasible cut at the node.]
+
+ Description [Return 1 if node's LUT level does not exceed those of the fanins.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Sbd_CutMergeSimple( Sbd_Man_t * p, int * pCut1, int * pCut2, int * pCut )
+{
+ int * pBeg = pCut + 1;
+ int * pBeg1 = pCut1 + 1;
+ int * pBeg2 = pCut2 + 1;
+ int * pEnd1 = pCut1 + 1 + pCut1[0];
+ int * pEnd2 = pCut2 + 1 + pCut2[0];
+ while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 )
+ {
+ if ( *pBeg1 == *pBeg2 )
+ *pBeg++ = *pBeg1++, pBeg2++;
+ else if ( *pBeg1 < *pBeg2 )
+ *pBeg++ = *pBeg1++;
+ else
+ *pBeg++ = *pBeg2++;
+ }
+ while ( pBeg1 < pEnd1 )
+ *pBeg++ = *pBeg1++;
+ while ( pBeg2 < pEnd2 )
+ *pBeg++ = *pBeg2++;
+ return (pCut[0] = pBeg - pCut - 1);
+}
+/*
+int Sbd_ManMergeCuts( Sbd_Man_t * p, int Node )
+{
+ int Result = 1; // no need to resynthesize
+ int pCut[2*SBD_MAX_LUTSIZE+1];
+ int iFan0 = Gia_ObjFaninId0( Gia_ManObj(p->pGia, Node), Node );
+ int iFan1 = Gia_ObjFaninId1( Gia_ManObj(p->pGia, Node), Node );
+ int Level0 = Vec_IntEntry( p->vLutLevs, iFan0 );
+ int Level1 = Vec_IntEntry( p->vLutLevs, iFan1 );
+ int LevMax = (Level0 || Level1) ? Abc_MaxInt(Level0, Level1) : 1;
+ int * pCut0 = Sbd_ObjCut( p, iFan0 );
+ int * pCut1 = Sbd_ObjCut( p, iFan1 );
+ int nSize = Sbd_CutMergeSimple( p, pCut0, pCut1, pCut );
+ if ( nSize > p->pPars->nLutSize )
+ {
+ if ( Level0 != Level1 )
+ {
+ int Cut0[2] = {1, iFan0}, * pCut0Temp = Level0 < LevMax ? Cut0 : pCut0;
+ int Cut1[2] = {1, iFan1}, * pCut1Temp = Level1 < LevMax ? Cut1 : pCut1;
+ nSize = Sbd_CutMergeSimple( p, pCut0Temp, pCut1Temp, pCut );
+ }
+ if ( nSize > p->pPars->nLutSize )
+ {
+ pCut[0] = 2;
+ pCut[1] = iFan0 < iFan1 ? iFan0 : iFan1;
+ pCut[2] = iFan0 < iFan1 ? iFan1 : iFan0;
+ Result = LevMax ? 0 : 1;
+ LevMax++;
+ }
+ }
+ assert( iFan0 != iFan1 );
+ assert( Vec_IntEntry(p->vLutLevs, Node) == 0 );
+ Vec_IntWriteEntry( p->vLutLevs, Node, LevMax );
+ memcpy( Sbd_ObjCut(p, Node), pCut, sizeof(int) * (pCut[0] + 1) );
+ //printf( "Setting node %d with delay %d (result = %d).\n", Node, LevMax, Result );
+ return Result;
+}
+*/
+int Sbd_ManMergeCuts( Sbd_Man_t * p, int Node )
+{
+ int pCut11[2*SBD_MAX_LUTSIZE+1];
+ int pCut01[2*SBD_MAX_LUTSIZE+1];
+ int pCut10[2*SBD_MAX_LUTSIZE+1];
+ int pCut00[2*SBD_MAX_LUTSIZE+1];
+ int iFan0 = Gia_ObjFaninId0( Gia_ManObj(p->pGia, Node), Node );
+ int iFan1 = Gia_ObjFaninId1( Gia_ManObj(p->pGia, Node), Node );
+ int Level0 = Vec_IntEntry( p->vLutLevs, iFan0 ) ? Vec_IntEntry( p->vLutLevs, iFan0 ) : 1;
+ int Level1 = Vec_IntEntry( p->vLutLevs, iFan1 ) ? Vec_IntEntry( p->vLutLevs, iFan1 ) : 1;
+ int * pCut0 = Sbd_ObjCut( p, iFan0 );
+ int * pCut1 = Sbd_ObjCut( p, iFan1 );
+ int Cut0[2] = {1, iFan0};
+ int Cut1[2] = {1, iFan1};
+ int nSize11 = Sbd_CutMergeSimple( p, pCut0, pCut1, pCut11 );
+ int nSize01 = Sbd_CutMergeSimple( p, Cut0, pCut1, pCut01 );
+ int nSize10 = Sbd_CutMergeSimple( p, pCut0, Cut1, pCut10 );
+ int nSize00 = Sbd_CutMergeSimple( p, Cut0, Cut1, pCut00 );
+ int Lev11 = nSize11 <= p->pPars->nLutSize ? Abc_MaxInt(Level0, Level1) : ABC_INFINITY;
+ int Lev01 = nSize01 <= p->pPars->nLutSize ? Abc_MaxInt(Level0+1, Level1) : ABC_INFINITY;
+ int Lev10 = nSize10 <= p->pPars->nLutSize ? Abc_MaxInt(Level0, Level1+1) : ABC_INFINITY;
+ int Lev00 = nSize00 <= p->pPars->nLutSize ? Abc_MaxInt(Level0+1, Level1+1) : ABC_INFINITY;
+ int * pCutRes = pCut11;
+ int LevCur = Lev11;
+ if ( Lev01 < LevCur || (Lev01 == LevCur && pCut01[0] < pCutRes[0]) )
+ {
+ pCutRes = pCut01;
+ LevCur = Lev01;
+ }
+ if ( Lev10 < LevCur || (Lev10 == LevCur && pCut10[0] < pCutRes[0]) )
+ {
+ pCutRes = pCut10;
+ LevCur = Lev10;
+ }
+ if ( Lev00 < LevCur || (Lev00 == LevCur && pCut00[0] < pCutRes[0]) )
+ {
+ pCutRes = pCut00;
+ LevCur = Lev00;
+ }
+ assert( iFan0 != iFan1 );
+ assert( Vec_IntEntry(p->vLutLevs, Node) == 0 );
+ Vec_IntWriteEntry( p->vLutLevs, Node, LevCur );
+ assert( pCutRes[0] <= p->pPars->nLutSize );
+ memcpy( Sbd_ObjCut(p, Node), pCutRes, sizeof(int) * (pCutRes[0] + 1) );
+ //printf( "Setting node %d with delay %d.\n", Node, LevCur );
+ return LevCur == 1; // LevCur == Abc_MaxInt(Level0, Level1);
+}
+int Sbd_ManDelay( Sbd_Man_t * p )
+{
+ int i, Id, Delay = 0;
+ Gia_ManForEachCoDriverId( p->pGia, Id, i )
+ Delay = Abc_MaxInt( Delay, Vec_IntEntry(p->vLutLevs, Id) );
+ return Delay;
+}
+void Sbd_ManMergeTest( Sbd_Man_t * p )
+{
+ int Node;
+ Gia_ManForEachAndId( p->pGia, Node )
+ Sbd_ManMergeCuts( p, Node );
+ printf( "Delay %d.\n", Sbd_ManDelay(p) );
+}
+
+void Sbd_ManFindCut_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
+{
+ if ( pObj->fMark1 )
+ return;
+ pObj->fMark1 = 1;
+ if ( pObj->fMark0 )
+ return;
+ assert( Gia_ObjIsAnd(pObj) );
+ Sbd_ManFindCut_rec( p, Gia_ObjFanin0(pObj) );
+ Sbd_ManFindCut_rec( p, Gia_ObjFanin1(pObj) );
+}
+void Sbd_ManFindCutUnmark_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
+{
+ if ( !pObj->fMark1 )
+ return;
+ pObj->fMark1 = 0;
+ if ( pObj->fMark0 )
+ return;
+ assert( Gia_ObjIsAnd(pObj) );
+ Sbd_ManFindCutUnmark_rec( p, Gia_ObjFanin0(pObj) );
+ Sbd_ManFindCutUnmark_rec( p, Gia_ObjFanin1(pObj) );
+}
+void Sbd_ManFindCut( Sbd_Man_t * p, int Node, Vec_Int_t * vCutLits )
+{
+ int pCut[SBD_MAX_LUTSIZE+1];
+ int i, LevelMax = 0;
+ // label reachable nodes
+ Gia_Obj_t * pTemp, * pObj = Gia_ManObj(p->pGia, Node);
+ Sbd_ManFindCut_rec( p->pGia, pObj );
+ // collect
+ pCut[0] = 0;
+ Gia_ManForEachObjVec( vCutLits, p->pGia, pTemp, i )
+ if ( pTemp->fMark1 )
+ {
+ LevelMax = Abc_MaxInt( LevelMax, Vec_IntEntry(p->vLutLevs, Gia_ObjId(p->pGia, pTemp)) );
+ pCut[1+pCut[0]++] = Gia_ObjId(p->pGia, pTemp);
+ }
+ assert( pCut[0] <= p->pPars->nLutSize );
+ // unlabel reachable nodes
+ Sbd_ManFindCutUnmark_rec( p->pGia, pObj );
+ // create cut
+ assert( Vec_IntEntry(p->vLutLevs, Node) == 0 );
+ Vec_IntWriteEntry( p->vLutLevs, Node, LevelMax+1 );
+ memcpy( Sbd_ObjCut(p, Node), pCut, sizeof(int) * (pCut[0] + 1) );
+}
+
+int Sbd_ManImplement( Sbd_Man_t * p, int Pivot, word Truth )
+{
+ Gia_Obj_t * pObj;
+ int i, k, w, iLit, Entry, Node;
+ int iObjLast = Gia_ManObjNum(p->pGia);
+ int iCurLev = Vec_IntEntry(p->vLutLevs, Pivot);
+ int iNewLev;
+ // collect leaf literals
+ Vec_IntClear( p->vLits );
+ Vec_IntForEachEntry( p->vDivVars, Node, i )
+ {
+ Node = Vec_IntEntry( p->vWinObjs, Node );
+ if ( Vec_IntEntry(p->vMirrors, Node) >= 0 )
+ Vec_IntPush( p->vLits, Vec_IntEntry(p->vMirrors, Node) );
+ else
+ Vec_IntPush( p->vLits, Abc_Var2Lit(Node, 0) );
+ }
+ // pretend to have MUXes
+// assert( p->pGia->pMuxes == NULL );
+ if ( p->pGia->nXors && p->pGia->pMuxes == NULL )
+ p->pGia->pMuxes = (unsigned *)p;
+ // derive new function of the node
+ iLit = Dsm_ManTruthToGia( p->pGia, &Truth, p->vLits, p->vCover );
+ if ( p->pGia->pMuxes == (unsigned *)p )
+ p->pGia->pMuxes = NULL;
+ // remember this function
+ assert( Vec_IntEntry(p->vMirrors, Pivot) == -1 );
+ Vec_IntWriteEntry( p->vMirrors, Pivot, iLit );
+ if ( p->pPars->fVerbose )
+ printf( "Replacing node %d by literal %d.\n", Pivot, iLit );
+ // translate literals into variables
+ Vec_IntForEachEntry( p->vLits, Entry, i )
+ Vec_IntWriteEntry( p->vLits, i, Abc_Lit2Var(Entry) );
+ // label inputs
+ Gia_ManForEachObjVec( p->vLits, p->pGia, pObj, i )
+ pObj->fMark0 = 1;
+ // extend data-structure to accommodate new nodes
+ assert( Vec_IntSize(p->vLutLevs) == iObjLast );
+ for ( i = iObjLast; i < Gia_ManObjNum(p->pGia); i++ )
+ {
+ Vec_IntPush( p->vLutLevs, 0 );
+ Vec_IntPush( p->vObj2Var, 0 );
+ Vec_IntPush( p->vMirrors, -1 );
+ Vec_IntFillExtra( p->vLutCuts, Vec_IntSize(p->vLutCuts) + p->pPars->nLutSize + 1, 0 );
+ Sbd_ManFindCut( p, i, p->vLits );
+ for ( k = 0; k < 4; k++ )
+ for ( w = 0; w < p->pPars->nWords; w++ )
+ Vec_WrdPush( p->vSims[k], 0 );
+ }
+ // unlabel inputs
+ Gia_ManForEachObjVec( p->vLits, p->pGia, pObj, i )
+ pObj->fMark0 = 0;
+ // make sure delay reduction is achieved
+ iNewLev = Vec_IntEntry( p->vLutLevs, Abc_Lit2Var(iLit) );
+ assert( iNewLev < iCurLev );
+ // update delay of the initial node
+ assert( Vec_IntEntry(p->vLutLevs, Pivot) == iCurLev );
+ Vec_IntWriteEntry( p->vLutLevs, Pivot, iNewLev );
+ p->nChanges++;
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Derives new AIG after resynthesis.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Sbd_ManDerive_rec( Gia_Man_t * pNew, Gia_Man_t * p, int Node, Vec_Int_t * vMirrors )
+{
+ Gia_Obj_t * pObj;
+ int Obj = Node;
+ if ( Vec_IntEntry(vMirrors, Node) >= 0 )
+ Obj = Abc_Lit2Var( Vec_IntEntry(vMirrors, Node) );
+ pObj = Gia_ManObj( p, Obj );
+ if ( !~pObj->Value )
+ {
+ assert( Gia_ObjIsAnd(pObj) );
+ Sbd_ManDerive_rec( pNew, p, Gia_ObjFaninId0(pObj, Obj), vMirrors );
+ Sbd_ManDerive_rec( pNew, p, Gia_ObjFaninId1(pObj, Obj), vMirrors );
+ if ( Gia_ObjIsXor(pObj) )
+ pObj->Value = Gia_ManHashXorReal( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+ else
+ pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+ }
+ // set the original node as well
+ if ( Obj != Node )
+ Gia_ManObj(p, Node)->Value = Abc_LitNotCond( pObj->Value, Abc_LitIsCompl(Vec_IntEntry(vMirrors, Node)) );
+}
+Gia_Man_t * Sbd_ManDerive( Gia_Man_t * p, Vec_Int_t * vMirrors )
+{
+ Gia_Man_t * pNew;
+ Gia_Obj_t * pObj;
+ int i;
+ Gia_ManFillValue( p );
+ pNew = Gia_ManStart( Gia_ManObjNum(p) );
+ pNew->pName = Abc_UtilStrsav( p->pName );
+ pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+ if ( p->pMuxes )
+ pNew->pMuxes = ABC_CALLOC( unsigned, Gia_ManObjNum(p) );
+ Gia_ManConst0(p)->Value = 0;
+ Gia_ManHashAlloc( pNew );
+ Gia_ManForEachCi( p, pObj, i )
+ pObj->Value = Gia_ManAppendCi(pNew);
+ Gia_ManForEachCo( p, pObj, i )
+ Sbd_ManDerive_rec( pNew, p, Gia_ObjFaninId0p(p, pObj), vMirrors );
+ Gia_ManForEachCo( p, pObj, i )
+ pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+ Gia_ManHashStop( pNew );
+ Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+ Gia_ManTransferTiming( pNew, p );
+ return pNew;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs delay optimization for the given LUT size.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Sbd_NtkPerformOne( Sbd_Man_t * p, int Pivot )
+{
+ int RetValue; word Truth = 0;
+ if ( Sbd_ManMergeCuts( p, Pivot ) )
+ return;
+ //if ( Pivot != 344 )
+ // continue;
+ if ( p->pPars->fVerbose )
+ printf( "\nLooking at node %d\n", Pivot );
+ if ( Sbd_ManWindow( p, Pivot ) )
+ return;
+ RetValue = Sbd_ManCheckConst( p, Pivot );
+ if ( RetValue >= 0 )
+ Vec_IntWriteEntry( p->vMirrors, Pivot, RetValue );
+ else if ( Sbd_ManExplore( p, Pivot, &Truth ) )
+ Sbd_ManImplement( p, Pivot, Truth );
+}
+Gia_Man_t * Sbd_NtkPerform( Gia_Man_t * pGia, Sbd_Par_t * pPars )
+{
+ Gia_Man_t * pNew;
+ Gia_Obj_t * pObj;
+ Sbd_Man_t * p = Sbd_ManStart( pGia, pPars );
+ int nNodesOld = Gia_ManObjNum(pGia);//, Count = 0;
+ int k, Pivot;
+ assert( pPars->nLutSize <= 6 );
+ //Sbd_ManMergeTest( p );
+ //return NULL;
+ if ( pGia->pManTime != NULL && Tim_ManBoxNum((Tim_Man_t*)pGia->pManTime) )
+ {
+ Vec_Int_t * vNodes = Gia_ManOrderWithBoxes( pGia );
+ Tim_Man_t * pTimOld = (Tim_Man_t *)pGia->pManTime;
+ pGia->pManTime = Tim_ManDup( pTimOld, 1 );
+ Tim_ManIncrementTravId( (Tim_Man_t *)pGia->pManTime );
+ Gia_ManForEachObjVec( vNodes, pGia, pObj, k )
+ {
+ Pivot = Gia_ObjId( pGia, pObj );
+ if ( Pivot >= nNodesOld )
+ continue;
+ if ( Gia_ObjIsAnd(pObj) )
+ Sbd_NtkPerformOne( p, Pivot );
+ else if ( Gia_ObjIsCi(pObj) )
+ {
+ int arrTime = Tim_ManGetCiArrival( (Tim_Man_t*)pGia->pManTime, Gia_ObjCioId(pObj) );
+ Vec_IntWriteEntry( p->vLutLevs, Pivot, arrTime );
+ }
+ else if ( Gia_ObjIsCo(pObj) )
+ {
+ int arrTime = Vec_IntEntry( p->vLutLevs, Gia_ObjFaninId0(pObj, Pivot) );
+ Tim_ManSetCoArrival( (Tim_Man_t*)pGia->pManTime, Gia_ObjCioId(pObj), arrTime );
+ }
+ else if ( !Gia_ObjIsConst0(pObj) )
+ assert( 0 );
+ }
+ //Tim_ManPrint( pGia->pManTime );
+ Tim_ManStop( (Tim_Man_t *)pGia->pManTime );
+ pGia->pManTime = pTimOld;
+ Vec_IntFree( vNodes );
+ }
+ else
+ {
+ Gia_ManForEachAndId( pGia, Pivot )
+ if ( Pivot < nNodesOld )
+ Sbd_NtkPerformOne( p, Pivot );
+ }
+ printf( "Found %d constants and %d replacements with delay %d. ", p->nConsts, p->nChanges, Sbd_ManDelay(p) );
+ p->timeTotal = Abc_Clock() - p->timeTotal;
+ Abc_PrintTime( 1, "Time", p->timeTotal );
+ pNew = Sbd_ManDerive( pGia, p->vMirrors );
+ // print runtime statistics
+ p->timeOther = p->timeTotal - p->timeWin - p->timeCnf - p->timeSat - p->timeCov - p->timeEnu;
+ if ( 0 )
+ {
+ ABC_PRTP( "Win", p->timeWin , p->timeTotal );
+ ABC_PRTP( "Cnf", p->timeCnf , p->timeTotal );
+ ABC_PRTP( "Sat", p->timeSat , p->timeTotal );
+ ABC_PRTP( "Cov", p->timeCov , p->timeTotal );
+ ABC_PRTP( "Enu", p->timeEnu , p->timeTotal );
+ ABC_PRTP( "Oth", p->timeOther, p->timeTotal );
+ ABC_PRTP( "ALL", p->timeTotal, p->timeTotal );
+ }
+ Sbd_ManStop( p );
+ return pNew;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/opt/sbd/sbdInt.h b/src/opt/sbd/sbdInt.h
new file mode 100644
index 00000000..4c553fb4
--- /dev/null
+++ b/src/opt/sbd/sbdInt.h
@@ -0,0 +1,78 @@
+/**CFile****************************************************************
+
+ FileName [rsbInt.h]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [SAT-based optimization using internal don't-cares.]
+
+ Synopsis [Internal declarations.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: rsbInt.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#ifndef ABC__opt_sbdInt__h
+#define ABC__opt_sbdInt__h
+
+
+////////////////////////////////////////////////////////////////////////
+/// INCLUDES ///
+////////////////////////////////////////////////////////////////////////
+
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include <assert.h>
+
+#include "misc/vec/vec.h"
+#include "sat/bsat/satSolver.h"
+#include "misc/util/utilNam.h"
+#include "misc/util/utilTruth.h"
+#include "map/scl/sclLib.h"
+#include "map/scl/sclCon.h"
+#include "bool/kit/kit.h"
+#include "misc/st/st.h"
+#include "map/mio/mio.h"
+#include "base/abc/abc.h"
+#include "sbd.h"
+
+////////////////////////////////////////////////////////////////////////
+/// PARAMETERS ///
+////////////////////////////////////////////////////////////////////////
+
+ABC_NAMESPACE_HEADER_START
+
+#define SBD_SAT_UNDEC 0x1234567812345678
+#define SBD_SAT_SAT 0x8765432187654321
+
+////////////////////////////////////////////////////////////////////////
+/// BASIC TYPES ///
+////////////////////////////////////////////////////////////////////////
+
+
+////////////////////////////////////////////////////////////////////////
+/// MACRO DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== sbdCnf.c ==========================================================*/
+
+ABC_NAMESPACE_HEADER_END
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/opt/sbd/sbdSat.c b/src/opt/sbd/sbdSat.c
new file mode 100644
index 00000000..ae865627
--- /dev/null
+++ b/src/opt/sbd/sbdSat.c
@@ -0,0 +1,797 @@
+/**CFile****************************************************************
+
+ FileName [sbd.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [SAT-based optimization using internal don't-cares.]
+
+ Synopsis []
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: sbd.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "sbdInt.h"
+#include "misc/util/utilTruth.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+#define MAX_M 8 // max inputs
+#define MAX_N 30 // max nodes
+#define MAX_K 6 // max lutsize
+#define MAX_D 8 // max delays
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+#define SBD_LUTS_MAX 2
+#define SBD_SIZE_MAX 4
+#define SBD_DIV_MAX 16
+
+// new AIG manager
+typedef struct Sbd_Pro_t_ Sbd_Pro_t;
+struct Sbd_Pro_t_
+{
+ int nLuts; // LUT count
+ int nSize; // LUT size
+ int nDivs; // divisor count
+ int nVars; // intermediate variables (nLuts * nSize)
+ int nPars; // total parameter count (nLuts * (1 << nSize) + nLuts * nSize * nDivs)
+ int pPars1[SBD_LUTS_MAX][1<<SBD_SIZE_MAX]; // lut parameters
+ int pPars2[SBD_LUTS_MAX][SBD_SIZE_MAX][SBD_DIV_MAX]; // topo parameters
+ int pVars[SBD_LUTS_MAX][SBD_SIZE_MAX+1]; // internal variables
+ int pDivs[SBD_DIV_MAX]; // divisor variables (external)
+};
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Sbd_ProblemSetup( Sbd_Pro_t * p, int nLuts, int nSize, int nDivs )
+{
+ Vec_Int_t * vCnf = Vec_IntAlloc( 1000 );
+ int i, k, d, v, n, iVar = 0;
+ assert( nLuts >= 1 && nLuts <= 2 );
+ memset( p, 0, sizeof(Sbd_Pro_t) );
+ p->nLuts = nLuts;
+ p->nSize = nSize;
+ p->nDivs = nDivs;
+ p->nVars = nLuts * nSize;
+ p->nPars = nLuts * (1 << nSize) + nLuts * nSize * nDivs;
+ // set parameters
+ for ( i = 0; i < nLuts; i++ )
+ for ( k = 0; k < (1 << nSize); k++ )
+ p->pPars1[i][k] = iVar++;
+ for ( i = 0; i < nLuts; i++ )
+ for ( k = 0; k < nSize; k++ )
+ for ( d = 0; d < nDivs; d++ )
+ p->pPars2[i][k][d] = iVar++;
+ // set intermediate variables
+ for ( i = 0; i < nLuts; i++ )
+ for ( k = 0; k < nSize; k++ )
+ p->pVars[i][k] = iVar++;
+ // set top variables
+ for ( i = 1; i < nLuts; i++ )
+ p->pVars[i][nSize] = p->pVars[i-1][0];
+ // set divisor variables
+ for ( d = 0; d < nDivs; d++ )
+ p->pDivs[d] = iVar++;
+ assert( iVar == p->nPars + p->nVars + p->nDivs );
+
+ // input compatiblity clauses
+ for ( i = 0; i < nLuts; i++ )
+ for ( k = (i > 0); k < nSize; k++ )
+ for ( d = 0; d < nDivs; d++ )
+ for ( n = 0; n < nDivs; n++ )
+ {
+ if ( n < d )
+ {
+ Vec_IntPush( vCnf, Abc_Var2Lit(p->pPars2[i][k][d], 0) );
+ Vec_IntPush( vCnf, Abc_Var2Lit(p->pPars2[i][k][n], 0) );
+ Vec_IntPush( vCnf, -1 );
+ }
+ else if ( k < nSize-1 )
+ {
+ Vec_IntPush( vCnf, Abc_Var2Lit(p->pPars2[i][k][d], 0) );
+ Vec_IntPush( vCnf, Abc_Var2Lit(p->pPars2[i][k+1][n], 0) );
+ Vec_IntPush( vCnf, -1 );
+ }
+ }
+
+ // create LUT clauses
+ for ( i = 0; i < nLuts; i++ )
+ for ( k = 0; k < (1 << nSize); k++ )
+ for ( n = 0; n < 2; n++ )
+ {
+ for ( v = 0; v < nSize; v++ )
+ Vec_IntPush( vCnf, Abc_Var2Lit(p->pPars1[i][v], (k >> v) & 1) );
+ Vec_IntPush( vCnf, Abc_Var2Lit(p->pVars[i][nSize], n) );
+ Vec_IntPush( vCnf, Abc_Var2Lit(p->pPars1[i][k], !n) );
+ Vec_IntPush( vCnf, -1 );
+ }
+
+ // create input clauses
+ for ( i = 0; i < nLuts; i++ )
+ for ( k = (i > 0); k < nSize; k++ )
+ for ( d = 0; d < nDivs; d++ )
+ for ( n = 0; n < 2; n++ )
+ {
+ Vec_IntPush( vCnf, Abc_Var2Lit(p->pPars2[i][k][d], 0) );
+ Vec_IntPush( vCnf, Abc_Var2Lit(p->pPars1[i][k], n) );
+ Vec_IntPush( vCnf, Abc_Var2Lit(p->pDivs[d], !n) );
+ Vec_IntPush( vCnf, -1 );
+ }
+
+ return vCnf;
+}
+// add clauses to the don't-care computation solver
+void Sbd_ProblemLoad1( Sbd_Pro_t * p, Vec_Int_t * vCnf, int iStartVar, int * pDivVars, int iTopVar, sat_solver * pSat )
+{
+ int pLits[8], nLits, i, k, iLit, RetValue;
+ int ThisTopVar = p->pVars[0][p->nSize];
+ int FirstDivVar = p->nPars + p->nVars;
+ // add clauses
+ for ( i = 0; i < Vec_IntSize(vCnf); i++ )
+ {
+ assert( Vec_IntEntry(vCnf, i) != -1 );
+ for ( k = i+1; k < Vec_IntSize(vCnf); k++ )
+ if ( Vec_IntEntry(vCnf, i) == -1 )
+ break;
+ nLits = 0;
+ Vec_IntForEachEntryStartStop( vCnf, iLit, i, i, k ) {
+ if ( Abc_Lit2Var(iLit) == ThisTopVar )
+ pLits[nLits++] = Abc_Var2Lit( ThisTopVar, Abc_LitIsCompl(iLit) );
+ else if ( Abc_Lit2Var(iLit) >= FirstDivVar )
+ pLits[nLits++] = Abc_Var2Lit( pDivVars[Abc_Lit2Var(iLit)-FirstDivVar], Abc_LitIsCompl(iLit) );
+ else
+ pLits[nLits++] = iLit + 2 * iStartVar;
+ }
+ assert( nLits <= 8 );
+ RetValue = sat_solver_addclause( pSat, pLits, pLits + nLits );
+ assert( RetValue );
+ }
+}
+// add clauses to the functionality evaluation solver
+void Sbd_ProblemLoad2( Sbd_Pro_t * p, Vec_Wec_t * vCnf, int iStartVar, int * pDivVarValues, int iTopVarValue, sat_solver * pSat )
+{
+ Vec_Int_t * vLevel;
+ int pLits[8], nLits, i, k, iLit, RetValue;
+ int ThisTopVar = p->pVars[0][p->nSize];
+ int FirstDivVar = p->nPars + p->nVars;
+ int FirstIntVar = p->nPars;
+ // add clauses
+ Vec_WecForEachLevel( vCnf, vLevel, i )
+ {
+ nLits = 0;
+ Vec_IntForEachEntry( vLevel, iLit, k ) {
+ if ( Abc_Lit2Var(iLit) == ThisTopVar )
+ {
+ if ( Abc_LitIsCompl(iLit) == iTopVarValue )
+ break;
+ continue;
+ }
+ else if ( Abc_Lit2Var(iLit) >= FirstDivVar )
+ {
+ if ( Abc_LitIsCompl(iLit) == pDivVarValues[Abc_Lit2Var(iLit)-FirstDivVar] )
+ break;
+ continue;
+ }
+ else if ( Abc_Lit2Var(iLit) >= FirstIntVar )
+ pLits[nLits++] = iLit + 2 * iStartVar;
+ else
+ pLits[nLits++] = iLit;
+ }
+ if ( k < Vec_IntSize(vLevel) )
+ continue;
+ assert( nLits <= 8 );
+ RetValue = sat_solver_addclause( pSat, pLits, pLits + nLits );
+ assert( RetValue );
+ }
+}
+
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+sat_solver * Sbd_SolverTopo( int M, int N, int K, int pVars[MAX_N][MAX_M+MAX_N][MAX_K], int pVars2[MAX_M+MAX_N][MAX_D], int pDelays[], int Req, int * pnVars ) // inputs, nodes, lutsize
+{
+ sat_solver * pSat = NULL;
+ Vec_Int_t * vTemp = Vec_IntAlloc(100);
+ // assign vars
+ int RetValue, n, i, j, j2, k, k2, d, Count, nVars = 0;
+ for ( n = 0; n < N; n++ )
+ for ( i = 0; i < M+N; i++ )
+ for ( k = 0; k < K; k++ )
+ pVars[n][i][k] = -1;
+ for ( n = 0; n < N; n++ )
+ for ( i = 0; i < M+n; i++ )
+ for ( k = 0; k < K; k++ )
+ pVars[n][i][k] = nVars++;
+ printf( "Number of topo vars = %d.\n", nVars );
+ *pnVars = nVars;
+ // add constraints
+ pSat = sat_solver_new();
+ sat_solver_setnvars( pSat, nVars );
+ // each node is used
+ for ( i = 0; i < M+N-1; i++ )
+ {
+ Vec_IntClear( vTemp );
+ for ( n = 0; n < N; n++ )
+ for ( k = 0; k < K; k++ )
+ if ( pVars[n][i][k] >= 0 )
+ Vec_IntPush( vTemp, Abc_Var2Lit(pVars[n][i][k], 0) );
+ RetValue = sat_solver_addclause( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp) );
+ assert( RetValue );
+ }
+ printf( "Added %d node connectivity constraints.\n", i );
+ // each fanin of each node is connected exactly once
+ Count = 0;
+ for ( n = 0; n < N; n++ )
+ for ( k = 0; k < K; k++ )
+ {
+ // connected
+ Vec_IntClear( vTemp );
+ for ( i = 0; i < M+n; i++ )
+ Vec_IntPush( vTemp, Abc_Var2Lit(pVars[n][i][k], 0) );
+ RetValue = sat_solver_addclause( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp) );
+ assert( RetValue );
+ // exactly once
+ for ( i = 0; i < M+n; i++ )
+ for ( j = i+1; j < M+n; j++ )
+ {
+ Vec_IntFillTwo( vTemp, 2, Abc_Var2Lit(pVars[n][i][k], 1), Abc_Var2Lit(pVars[n][j][k], 1) );
+ RetValue = sat_solver_addclause( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp) );
+ assert( RetValue );
+ Count++;
+ }
+ }
+ printf( "Added %d fanin connectivity constraints.\n", Count );
+ // node fanins are unique
+ Count = 0;
+ for ( n = 0; n < N; n++ )
+ for ( i = 0; i < M+n; i++ )
+ for ( k = 0; k < K; k++ )
+ for ( j = i; j < M+n; j++ )
+ for ( k2 = k+1; k2 < K; k2++ )
+ {
+ Vec_IntFillTwo( vTemp, 2, Abc_Var2Lit(pVars[n][i][k], 1), Abc_Var2Lit(pVars[n][j][k2], 1) );
+ RetValue = sat_solver_addclause( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp) );
+ assert( RetValue );
+ Count++;
+ }
+ printf( "Added %d fanin exclusivity constraints.\n", Count );
+ // nodes are ordered
+ Count = 0;
+ for ( n = 1; n < N; n++ )
+ for ( i = 0; i < M+n-1; i++ )
+ {
+ // first of n cannot be smaller than first of n-1 (but can be equal)
+ for ( j = i+1; j < M+n-1; j++ )
+ {
+ Vec_IntFillTwo( vTemp, 2, Abc_Var2Lit(pVars[n][i][0], 1), Abc_Var2Lit(pVars[n-1][j][0], 1) );
+ RetValue = sat_solver_addclause( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp) );
+ assert( RetValue );
+ Count++;
+ }
+ // if first nodes of n and n-1 are equal, second nodes are ordered
+ Vec_IntFillTwo( vTemp, 2, Abc_Var2Lit(pVars[n][i][0], 1), Abc_Var2Lit(pVars[n-1][i][0], 1) );
+ for ( j = 0; j < i; j++ )
+ for ( j2 = j+1; j2 < i; j2++ )
+ {
+ Vec_IntPushTwo( vTemp, Abc_Var2Lit(pVars[n][j][1], 1), Abc_Var2Lit(pVars[n-1][j2][1], 1) );
+ RetValue = sat_solver_addclause( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp) );
+ assert( RetValue );
+ Vec_IntShrink( vTemp, 2 );
+ Count++;
+ }
+ }
+ printf( "Added %d node ordering constraints.\n", Count );
+ // exclude fanins of two-input nodes
+ Count = 0;
+ if ( K == 2 )
+ for ( n = 1; n < N; n++ )
+ for ( i = M; i < M+n; i++ )
+ for ( j = 0; j < i; j++ )
+ for ( k = 0; k < K; k++ )
+ {
+ Vec_IntClear( vTemp );
+ Vec_IntPush( vTemp, Abc_Var2Lit(pVars[n][i][0], 1) );
+ Vec_IntPush( vTemp, Abc_Var2Lit(pVars[n][j][1], 1) );
+ Vec_IntPush( vTemp, Abc_Var2Lit(pVars[i-M][j][k], 1) );
+ RetValue = sat_solver_addclause( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp) );
+ assert( RetValue );
+ Count++;
+ }
+ printf( "Added %d two-node non-triviality constraints.\n", Count );
+
+
+ // assign delay vars
+ assert( Req < MAX_D-1 );
+ for ( i = 0; i < M+N; i++ )
+ for ( d = 0; d < MAX_D; d++ )
+ pVars2[i][d] = nVars++;
+ printf( "Number of total vars = %d.\n", nVars );
+ // set input delays
+ for ( i = 0; i < M; i++ )
+ {
+ assert( pDelays[i] < MAX_D-2 );
+ Vec_IntFill( vTemp, 1, Abc_Var2Lit(pVars2[i][pDelays[i]], 0) );
+ RetValue = sat_solver_addclause( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp) );
+ assert( RetValue );
+ }
+ // set output delay
+ for ( k = Req; k < MAX_D; k++ )
+ {
+ Vec_IntFill( vTemp, 1, Abc_Var2Lit(pVars2[M+N-1][Req+1], 1) );
+ RetValue = sat_solver_addclause( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp) );
+ assert( RetValue );
+ }
+ // set internal nodes
+ for ( n = 0; n < N; n++ )
+ for ( i = 0; i < M+n; i++ )
+ for ( k = 0; k < K; k++ )
+ for ( d = 0; d < MAX_D-1; d++ )
+ {
+ Vec_IntFill( vTemp, 1, Abc_Var2Lit(pVars[n][i][k], 1) );
+ Vec_IntPush( vTemp, Abc_Var2Lit(pVars2[i][d], 1) );
+ Vec_IntPush( vTemp, Abc_Var2Lit(pVars2[M+n][d+1], 0) );
+ RetValue = sat_solver_addclause( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp) );
+ assert( RetValue );
+ }
+
+
+ Vec_IntFree( vTemp );
+ return pSat;
+}
+void Sbd_SolverTopoPrint( sat_solver * pSat, int M, int N, int K, int pVars[MAX_N][MAX_M+MAX_N][MAX_K] )
+{
+ int n, i, k;
+ printf( "Solution:\n" );
+ printf( " | " );
+ for ( n = 0; n < N; n++ )
+ printf( "%2d ", M+n );
+ printf( "\n" );
+ for ( i = M+N-2; i >= 0; i-- )
+ {
+ printf( "%2d %c | ", i, i < M ? 'i' : ' ' );
+ for ( n = 0; n < N; n++ )
+ {
+ for ( k = K-1; k >= 0; k-- )
+ if ( pVars[n][i][k] == -1 )
+ printf( " " );
+ else
+ printf( "%c", sat_solver_var_value(pSat, pVars[n][i][k]) ? '*' : '.' );
+ printf( " " );
+ }
+ printf( "\n" );
+ }
+}
+void Sbd_SolverTopoTest()
+{
+ int M = 8; // 6; // inputs
+ int N = 3; // 16; // nodes
+ int K = 4; // 2; // lutsize
+ int status, v, nVars, nIter, nSols = 0;
+ int pVars[MAX_N][MAX_M+MAX_N][MAX_K]; // 20 x 32 x 6 = 3840
+ int pVars2[MAX_M+MAX_N][MAX_D]; // 20 x 32 x 6 = 3840
+ int pDelays[MAX_M] = {1,0,0,0,1};
+ abctime clk = Abc_Clock();
+ Vec_Int_t * vLits = Vec_IntAlloc(100);
+ sat_solver * pSat = Sbd_SolverTopo( M, N, K, pVars, pVars2, pDelays, 2, &nVars );
+ for ( nIter = 0; nIter < 1000000; nIter++ )
+ {
+ // find onset minterm
+ status = sat_solver_solve( pSat, NULL, NULL, 0, 0, 0, 0 );
+ if ( status == l_Undef )
+ break;
+ if ( status == l_False )
+ break;
+ assert( status == l_True );
+ nSols++;
+ // print solution
+ if ( nIter < 5 )
+ Sbd_SolverTopoPrint( pSat, M, N, K, pVars );
+ // remember variable values
+ Vec_IntClear( vLits );
+ for ( v = 0; v < nVars; v++ )
+ if ( sat_solver_var_value(pSat, v) )
+ Vec_IntPush( vLits, Abc_Var2Lit(v, 1) );
+ // add breaking clause
+ status = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits) );
+ if ( status == 0 )
+ break;
+ //if ( nIter == 5 )
+ // break;
+ }
+ sat_solver_delete( pSat );
+ Vec_IntFree( vLits );
+ printf( "Found %d solutions. ", nSols );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+}
+
+
+
+/**Function*************************************************************
+
+ Synopsis [Synthesize random topology.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Sbd_SolverSynth( int M, int N, int K, int pLuts[MAX_N][MAX_K] )
+{
+ int Used[MAX_M+MAX_N] = {0};
+ int nUnused = M;
+ int n, iFan0, iFan1;
+ srand( time(NULL) );
+ for ( n = 0; nUnused < N - n; n++ )
+ {
+ iFan0 = iFan1 = 0;
+ while ( (iFan0 = rand() % (M + n)) == (iFan1 = rand() % (M + n)) )
+ ;
+ pLuts[n][0] = iFan0;
+ pLuts[n][1] = iFan1;
+ if ( Used[iFan0] == 0 )
+ {
+ Used[iFan0] = 1;
+ nUnused--;
+ }
+ if ( Used[iFan1] == 0 )
+ {
+ Used[iFan1] = 1;
+ nUnused--;
+ }
+ nUnused++;
+ }
+ if ( nUnused == N - n )
+ {
+ // undo the first one
+ for ( iFan0 = 0; iFan0 < M+n; iFan0++ )
+ if ( Used[iFan0] )
+ {
+ Used[iFan0] = 0;
+ nUnused++;
+ break;
+ }
+
+ }
+ assert( nUnused == N - n + 1 );
+ for ( ; n < N; n++ )
+ {
+ for ( iFan0 = 0; iFan0 < M+n; iFan0++ )
+ if ( Used[iFan0] == 0 )
+ {
+ Used[iFan0] = 1;
+ break;
+ }
+ assert( iFan0 < M+n );
+ for ( iFan1 = 0; iFan1 < M+n; iFan1++ )
+ if ( Used[iFan1] == 0 )
+ {
+ Used[iFan1] = 1;
+ break;
+ }
+ assert( iFan1 < M+n );
+ pLuts[n][0] = iFan0;
+ pLuts[n][1] = iFan1;
+ }
+
+ printf( "{\n" );
+ for ( n = 0; n < N; n++ )
+ printf( " {%d, %d}%s // %d\n", pLuts[n][0], pLuts[n][1], n==N-1 ? "" :",", M+n );
+ printf( "};\n" );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Compute truth table for the given parameter settings.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+word Sbd_SolverTruth( int M, int N, int K, int pLuts[MAX_N][MAX_K], int pValues[MAX_N*((1<<MAX_K)-1)] )
+{
+ int i, k, v, nLutPars = (1 << K) - 1;
+ word Truths[MAX_M+MAX_N];
+ assert( M <= 6 && N <= MAX_N );
+ for ( i = 0; i < M; i++ )
+ Truths[i] = s_Truths6[i];
+ for ( i = 0; i < N; i++ )
+ {
+ word Truth = 0, Mint;
+ for ( k = 1; k <= nLutPars; k++ )
+ {
+ if ( !pValues[i*nLutPars+k-1] )
+ continue;
+ Mint = ~(word)0;
+ for ( v = 0; v < K; v++ )
+ Mint &= ((k >> v) & 1) ? Truths[pLuts[i][v]] : ~Truths[pLuts[i][v]];
+ Truth |= Mint;
+ }
+ Truths[M+i] = Truth;
+ }
+ return Truths[M+N-1];
+}
+word * Sbd_SolverTruthWord( int M, int N, int K, int pLuts[MAX_N][MAX_K], int pValues[MAX_N*((1<<MAX_K)-1)], word * pTruthsElem, int fCompl )
+{
+ int i, k, v, nLutPars = (1 << K) - 1;
+ int nWords = Abc_TtWordNum( M );
+ word * pRes = pTruthsElem + (M+N-1)*nWords;
+ assert( M <= MAX_M && N <= MAX_N );
+ for ( i = 0; i < N; i++ )
+ {
+ word * pMint, * pTruth = pTruthsElem + (M+i)*nWords;
+ Abc_TtClear( pTruth, nWords );
+ for ( k = 1; k <= nLutPars; k++ )
+ {
+ if ( !pValues[i*nLutPars+k-1] )
+ continue;
+ pMint = pTruthsElem + (M+N)*nWords;
+ Abc_TtFill( pMint, nWords );
+ for ( v = 0; v < K; v++ )
+ {
+ word * pFanin = pTruthsElem + pLuts[i][v]*nWords;
+ Abc_TtAndSharp( pMint, pMint, pFanin, nWords, ((k >> v) & 1) == 0 );
+ }
+ Abc_TtOr( pTruth, pTruth, pMint, nWords );
+ }
+ }
+ if ( fCompl )
+ Abc_TtNot( pRes, nWords );
+ return pRes;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Sbd_SolverFunc( int M, int N, int K, int pLuts[MAX_N][MAX_K], word * pTruthInit, int * pValues )
+{
+ int fVerbose = 0;
+ abctime clk = Abc_Clock();
+ abctime clk2, clkOther = 0;
+ sat_solver * pSat = NULL;
+ int nWords = Abc_TtWordNum(M);
+ int pLits[MAX_K+2], pLits2[MAX_K+2], nLits;
+ int nLutPars = (1 << K) - 1, nVars = N * nLutPars;
+ int i, k, m, status, iMint, Iter, fCompl = (int)(pTruthInit[0] & 1);
+ // create truth tables
+ word * pTruthNew, * pTruths = ABC_ALLOC( word, Abc_TtWordNum(MAX_N) * (MAX_M + MAX_N + 1) );
+ Abc_TtElemInit2( pTruths, M );
+ // create solver
+ pSat = sat_solver_new();
+ sat_solver_setnvars( pSat, nVars );
+ printf( "Number of parameters %d x %d = %d.\n", N, nLutPars, nVars );
+ // start with the last minterm
+// iMint = (1 << M) - 1;
+ iMint = 1;
+ for ( Iter = 0; Iter < (1 << M); Iter++ )
+ {
+ // assign the first intermediate variable
+ int nVarStart = sat_solver_nvars(pSat);
+ sat_solver_setnvars( pSat, nVarStart + N - 1 );
+ // add clauses for nodes
+ //if ( fVerbose )
+ printf( "Iter %3d : Mint = %3d. Conflicts =%8d.\n", Iter, iMint, sat_solver_nconflicts(pSat) );
+ for ( i = 0; i < N; i++ )
+ for ( m = 0; m <= nLutPars; m++ )
+ {
+ if ( fVerbose )
+ printf( "i = %d. m = %d.\n", i, m );
+ // selector variables
+ nLits = 0;
+ for ( k = 0; k < K; k++ )
+ {
+ if ( pLuts[i][k] >= M )
+ {
+ assert( pLuts[i][k] - M < N - 1 );
+ pLits[nLits] = pLits2[nLits] = Abc_Var2Lit( nVarStart + pLuts[i][k] - M, (m >> k) & 1 );
+ nLits++;
+ }
+ else if ( ((iMint >> pLuts[i][k]) & 1) != ((m >> k) & 1) )
+ break;
+ }
+ if ( k < K )
+ continue;
+ // add parameter
+ if ( m )
+ {
+ pLits[nLits] = Abc_Var2Lit( i*nLutPars + m-1, 1 );
+ pLits2[nLits] = Abc_Var2Lit( i*nLutPars + m-1, 0 );
+ nLits++;
+ }
+ // node variable
+ if ( i != N - 1 )
+ {
+ pLits[nLits] = Abc_Var2Lit( nVarStart + i, 0 );
+ pLits2[nLits] = Abc_Var2Lit( nVarStart + i, 1 );
+ nLits++;
+ }
+ // add clauses
+ if ( i != N - 1 || Abc_TtGetBit(pTruthInit, iMint) != fCompl )
+ {
+ status = sat_solver_addclause( pSat, pLits2, pLits2 + nLits );
+ if ( status == 0 )
+ {
+ fCompl = -1;
+ goto finish;
+ }
+ }
+ if ( (i != N - 1 || Abc_TtGetBit(pTruthInit, iMint) == fCompl) && m > 0 )
+ {
+ status = sat_solver_addclause( pSat, pLits, pLits + nLits );
+ if ( status == 0 )
+ {
+ fCompl = -1;
+ goto finish;
+ }
+ }
+ }
+
+ // run SAT solver
+ status = sat_solver_solve( pSat, NULL, NULL, 0, 0, 0, 0 );
+ if ( status == l_Undef )
+ break;
+ if ( status == l_False )
+ {
+ fCompl = -1;
+ goto finish;
+ }
+ assert( status == l_True );
+
+ // collect values
+ for ( i = 0; i < nVars; i++ )
+ pValues[i] = sat_solver_var_value(pSat, i);
+
+ clk2 = Abc_Clock();
+ pTruthNew = Sbd_SolverTruthWord( M, N, K, pLuts, pValues, pTruths, fCompl );
+ clkOther += Abc_Clock() - clk2;
+
+ if ( fVerbose )
+ {
+ for ( i = 0; i < nVars; i++ )
+ printf( "%d=%d ", i, pValues[i] );
+ printf( " " );
+ for ( i = nVars; i < sat_solver_nvars(pSat); i++ )
+ printf( "%d=%d ", i, sat_solver_var_value(pSat, i) );
+ printf( "\n" );
+ Extra_PrintBinary( stdout, (unsigned *)pTruthInit, (1 << M) ); printf( "\n" );
+ Extra_PrintBinary( stdout, (unsigned *)pTruthNew, (1 << M) ); printf( "\n" );
+ }
+ if ( Abc_TtEqual(pTruthInit, pTruthNew, nWords) )
+ break;
+
+ // get new minterm
+ iMint = Abc_TtFindFirstDiffBit( pTruthInit, pTruthNew, M );
+ }
+finish:
+ printf( "Finished after %d iterations and %d conflicts. ", Iter, sat_solver_nconflicts(pSat) );
+ sat_solver_delete( pSat );
+ ABC_FREE( pTruths );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+ Abc_PrintTime( 1, "Time", clkOther );
+ return fCompl;
+}
+void Sbd_SolverFuncTest()
+{
+// int M = 4; // 6; // inputs
+// int N = 3; // 16; // nodes
+// int K = 2; // 2; // lutsize
+// word Truth = ~((word)3 << 8);
+// int pLuts[MAX_N][MAX_K] = { {0,1}, {2,3}, {4,5}, {6,7}, {8,9} };
+
+/*
+ int M = 6; // 6; // inputs
+ int N = 19; // 16; // nodes
+ int K = 2; // 2; // lutsize
+ word pTruth[4] = { ABC_CONST(0x9ef7a8d9c7193a0f), 0, 0, 0 };
+ int pLuts[MAX_N][MAX_K] = {
+ {3, 5}, {1, 6}, {0, 5}, {8, 2}, {7, 9},
+ {0, 1}, {2, 11}, {5, 12}, {3, 13}, {1, 14},
+ {10, 15}, {11, 2}, {3, 17}, {9, 18}, {0, 13},
+ {20, 7}, {19, 21}, {4, 16}, {23, 22}
+ };
+*/
+
+/*
+ int M = 6; // 6; // inputs
+ int N = 5; // 16; // nodes
+ int K = 4; // 2; // lutsize
+ word Truth = ABC_CONST(0x9ef7a8d9c7193a0f);
+ int pLuts[MAX_N][MAX_K] = {
+ {0, 1, 2, 3}, // 6
+ {1, 2, 3, 4}, // 7
+ {2, 3, 4, 5}, // 8
+ {0, 1, 4, 5}, // 9
+ {6, 7, 8, 9} // 10
+ };
+*/
+
+/*
+ int M = 8; // 6; // inputs
+ int N = 7; // 16; // nodes
+ int K = 2; // 2; // lutsize
+// word pTruth[4] = { 0, 0, 0, ABC_CONST(0x8000000000000000) };
+// word pTruth[4] = { ABC_CONST(0x0000000000000001), 0, 0, 0 };
+ word pTruth[4] = { 0, 0, 0, ABC_CONST(0x0000000000020000) };
+ int pLuts[MAX_N][MAX_K] = { {0,1}, {2,3}, {4,5}, {6,7}, {8,9}, {10,11}, {12,13} };
+*/
+
+ int M = 8; // 6; // inputs
+ int N = 7; // 16; // nodes
+ int K = 2; // 2; // lutsize
+ word pTruth[4] = { ABC_CONST(0x0000080000020000), ABC_CONST(0x0000000000020000), ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000020000) };
+ int pLuts[MAX_N][MAX_K] = { {0,1}, {2,3}, {4,5}, {6,7}, {8,9}, {10,11}, {12,13} };
+
+ int pValues[MAX_N*((1<<MAX_K)-1)];
+ int Res, i, k, nLutPars = (1 << K) - 1;
+
+ //Sbd_SolverSynth( M, N, K, pLuts );
+
+ Res = Sbd_SolverFunc( M, N, K, pLuts, pTruth, pValues );
+ if ( Res == -1 )
+ {
+ printf( "Solution does not exist.\n" );
+ return;
+ }
+ printf( "Result (compl = %d):\n", Res );
+ for ( i = 0; i < N; i++ )
+ {
+ for ( k = nLutPars-1; k >= 0; k-- )
+ printf( "%d", pValues[i*nLutPars+k] );
+ printf( "0\n" );
+ }
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/opt/sbd/sbdSim.c b/src/opt/sbd/sbdSim.c
new file mode 100644
index 00000000..3bb44159
--- /dev/null
+++ b/src/opt/sbd/sbdSim.c
@@ -0,0 +1,310 @@
+/**CFile****************************************************************
+
+ FileName [sbdSim.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [SAT-based optimization using internal don't-cares.]
+
+ Synopsis [Simulation.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: sbdSim.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "sbdInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+static inline word * Sbd_ObjSims( Gia_Man_t * p, int i ) { return Vec_WrdEntryP( p->vSims, p->iPatsPi * i ); }
+static inline word * Sbd_ObjCtrl( Gia_Man_t * p, int i ) { return Vec_WrdEntryP( p->vSimsPi, p->iPatsPi * i ); }
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [This does not work.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Sbd_GiaSimRoundBack2( Gia_Man_t * p )
+{
+ int nWords = p->iPatsPi;
+ Gia_Obj_t * pObj;
+ int w, i, Id;
+ // init primary outputs
+ Gia_ManForEachCoId( p, Id, i )
+ for ( w = 0; w < nWords; w++ )
+ Sbd_ObjSims(p, Id)[w] = Gia_ManRandomW(0);
+ // transfer to nodes
+ Gia_ManForEachCo( p, pObj, i )
+ {
+ word * pSims = Sbd_ObjSims(p, Gia_ObjId(p, pObj));
+ Abc_TtCopy( Sbd_ObjSims(p, Gia_ObjFaninId0p(p, pObj)), pSims, nWords, Gia_ObjFaninC0(pObj) );
+ }
+ // simulate nodes
+ Gia_ManForEachAndReverse( p, pObj, i )
+ {
+ word * pSims = Sbd_ObjSims(p, i);
+ word * pSims0 = Sbd_ObjSims(p, Gia_ObjFaninId0(pObj, i));
+ word * pSims1 = Sbd_ObjSims(p, Gia_ObjFaninId1(pObj, i));
+ word Rand = Gia_ManRandomW(0);
+ for ( w = 0; w < nWords; w++ )
+ {
+ pSims0[w] = pSims[w] | Rand;
+ pSims1[w] = pSims[w] | ~Rand;
+ }
+ if ( Gia_ObjFaninC0(pObj) ) Abc_TtNot( pSims0, nWords );
+ if ( Gia_ObjFaninC1(pObj) ) Abc_TtNot( pSims1, nWords );
+ }
+ // primary inputs are initialized
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Tries to falsify a sequence of two-literal SAT problems.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Sbd_GiaSatOne_rec( Gia_Man_t * p, Gia_Obj_t * pObj, int Value, int fFirst, int iPat )
+{
+ if ( Gia_ObjIsTravIdCurrent(p, pObj) )
+ return (int)pObj->fMark0 == Value;
+ Gia_ObjSetTravIdCurrent(p, pObj);
+ pObj->fMark0 = Value;
+ if ( Gia_ObjIsCi(pObj) )
+ {
+ word * pSims = Sbd_ObjSims(p, Gia_ObjId(p, pObj));
+ if ( Abc_TtGetBit( pSims, iPat ) != Value )
+ Abc_TtXorBit( pSims, iPat );
+ return 1;
+ }
+ assert( Gia_ObjIsAnd(pObj) );
+ assert( !Gia_ObjIsXor(pObj) );
+ if ( Value )
+ return Sbd_GiaSatOne_rec( p, Gia_ObjFanin0(pObj), !Gia_ObjFaninC0(pObj), fFirst, iPat ) &&
+ Sbd_GiaSatOne_rec( p, Gia_ObjFanin1(pObj), !Gia_ObjFaninC1(pObj), fFirst, iPat );
+ if ( fFirst )
+ return Sbd_GiaSatOne_rec( p, Gia_ObjFanin0(pObj), Gia_ObjFaninC0(pObj), fFirst, iPat );
+ else
+ return Sbd_GiaSatOne_rec( p, Gia_ObjFanin1(pObj), Gia_ObjFaninC1(pObj), fFirst, iPat );
+}
+int Sbd_GiaSatOne( Gia_Man_t * p, Vec_Int_t * vPairs )
+{
+ int k, n, Var1, Var2, iPat = 0;
+ //Gia_ManSetPhase( p );
+ Vec_IntForEachEntryDouble( vPairs, Var1, Var2, k )
+ {
+ Gia_Obj_t * pObj1 = Gia_ManObj( p, Var1 );
+ Gia_Obj_t * pObj2 = Gia_ManObj( p, Var2 );
+ assert( Var2 > 0 );
+ if ( Var1 == 0 )
+ {
+ for ( n = 0; n < 2; n++ )
+ {
+ Gia_ManIncrementTravId( p );
+ if ( Sbd_GiaSatOne_rec(p, pObj2, !pObj2->fPhase, n, iPat) )
+ {
+ iPat++;
+ break;
+ }
+ }
+ printf( "%c", n == 2 ? '.' : 'c' );
+ }
+ else
+ {
+ for ( n = 0; n < 2; n++ )
+ {
+ Gia_ManIncrementTravId( p );
+ if ( Sbd_GiaSatOne_rec(p, pObj1, !pObj1->fPhase, n, iPat) && Sbd_GiaSatOne_rec(p, pObj2, pObj2->fPhase, n, iPat) )
+ {
+ iPat++;
+ break;
+ }
+ Gia_ManIncrementTravId( p );
+ if ( Sbd_GiaSatOne_rec(p, pObj1, pObj1->fPhase, n, iPat) && Sbd_GiaSatOne_rec(p, pObj2, !pObj2->fPhase, n, iPat) )
+ {
+ iPat++;
+ break;
+ }
+ }
+ printf( "%c", n == 2 ? '.' : 'e' );
+ }
+ if ( iPat == 64 * p->iPatsPi - 1 )
+ break;
+ }
+ printf( "\n" );
+ return iPat;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Sbd_GiaSimRoundBack( Gia_Man_t * p )
+{
+ extern void Sbd_GiaSimRound( Gia_Man_t * p, int fTry, Vec_Int_t ** pvMap );
+ Vec_Int_t * vReprs = Vec_IntStart( Gia_ManObjNum(p) );
+ Vec_Int_t * vPairs = Vec_IntAlloc( 1000 );
+ Vec_Int_t * vMap; // maps each node into its class
+ int i, nConsts = 0, nClasses = 0, nPats;
+ Sbd_GiaSimRound( p, 0, &vMap );
+ Gia_ManForEachAndId( p, i )
+ {
+ if ( Vec_IntEntry(vMap, i) == 0 )
+ Vec_IntPushTwo( vPairs, 0, i ), nConsts++;
+ else if ( Vec_IntEntry(vReprs, Vec_IntEntry(vMap, i)) == 0 )
+ Vec_IntWriteEntry( vReprs, Vec_IntEntry(vMap, i), i );
+ else if ( Vec_IntEntry(vReprs, Vec_IntEntry(vMap, i)) != -1 )
+ {
+ Vec_IntPushTwo( vPairs, Vec_IntEntry(vReprs, Vec_IntEntry(vMap, i)), i );
+ Vec_IntWriteEntry( vReprs, Vec_IntEntry(vMap, i), -1 );
+ nClasses++;
+ }
+ }
+ Vec_IntFree( vMap );
+ Vec_IntFree( vReprs );
+ printf( "Constants = %d. Classes = %d.\n", nConsts, nClasses );
+
+ nPats = Sbd_GiaSatOne( p, vPairs );
+ Vec_IntFree( vPairs );
+
+ printf( "Generated %d patterns.\n", nPats );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Sbd_GiaSimRound( Gia_Man_t * p, int fTry, Vec_Int_t ** pvMap )
+{
+ int nWords = p->iPatsPi;
+ Vec_Mem_t * vStore;
+ Gia_Obj_t * pObj;
+ Vec_Int_t * vMap = Vec_IntStart( Gia_ManObjNum(p) );
+ int w, i, Id, fCompl, RetValue;
+ // init primary inputs
+ if ( fTry )
+ {
+ Sbd_GiaSimRoundBack( p );
+ Gia_ManForEachCiId( p, Id, i )
+ Sbd_ObjSims(p, Id)[0] <<= 1;
+ }
+ else
+ {
+ Gia_ManForEachCiId( p, Id, i )
+ for ( w = 0; w < nWords; w++ )
+ Sbd_ObjSims(p, Id)[w] = Gia_ManRandomW(0) << !w;
+ }
+ // simulate internal nodes
+ vStore = Vec_MemAlloc( nWords, 16 ); // 2^12 N-word entries per page
+ Vec_MemHashAlloc( vStore, 1 << 16 );
+ RetValue = Vec_MemHashInsert( vStore, Sbd_ObjSims(p, 0) ); // const zero
+ assert( RetValue == 0 );
+ Gia_ManForEachAnd( p, pObj, i )
+ {
+ word * pSims = Sbd_ObjSims(p, i);
+ if ( Gia_ObjIsXor(pObj) )
+ Abc_TtXor( pSims,
+ Sbd_ObjSims(p, Gia_ObjFaninId0(pObj, i)),
+ Sbd_ObjSims(p, Gia_ObjFaninId1(pObj, i)),
+ nWords,
+ Gia_ObjFaninC0(pObj) ^ Gia_ObjFaninC1(pObj) );
+ else
+ Abc_TtAndCompl( pSims,
+ Sbd_ObjSims(p, Gia_ObjFaninId0(pObj, i)), Gia_ObjFaninC0(pObj),
+ Sbd_ObjSims(p, Gia_ObjFaninId1(pObj, i)), Gia_ObjFaninC1(pObj),
+ nWords );
+ // hash sim info
+ fCompl = (int)(pSims[0] & 1);
+ if ( fCompl ) Abc_TtNot( pSims, nWords );
+ Vec_IntWriteEntry( vMap, i, Vec_MemHashInsert(vStore, pSims) );
+ if ( fCompl ) Abc_TtNot( pSims, nWords );
+ }
+ Gia_ManForEachCo( p, pObj, i )
+ {
+ word * pSims = Sbd_ObjSims(p, Gia_ObjId(p, pObj));
+ Abc_TtCopy( pSims, Sbd_ObjSims(p, Gia_ObjFaninId0p(p, pObj)), nWords, Gia_ObjFaninC0(pObj) );
+// printf( "%d ", Abc_TtCountOnesVec(pSims, nWords) );
+ assert( Gia_ObjPhase(pObj) == (int)(pSims[0] & 1) );
+ }
+// printf( "\n" );
+ Vec_MemHashFree( vStore );
+ Vec_MemFree( vStore );
+ printf( "Objects = %6d. Unique = %6d.\n", Gia_ManAndNum(p), Vec_IntCountUnique(vMap) );
+ if ( pvMap )
+ *pvMap = vMap;
+ else
+ Vec_IntFree( vMap );
+}
+void Sbd_GiaSimTest( Gia_Man_t * pGia )
+{
+ Gia_ManSetPhase( pGia );
+
+ // allocate simulation info
+ pGia->iPatsPi = 32;
+ pGia->vSims = Vec_WrdStart( Gia_ManObjNum(pGia) * pGia->iPatsPi );
+ pGia->vSimsPi = Vec_WrdStart( Gia_ManObjNum(pGia) * pGia->iPatsPi );
+
+ Gia_ManRandom( 1 );
+
+ Sbd_GiaSimRound( pGia, 0, NULL );
+ Sbd_GiaSimRound( pGia, 0, NULL );
+ Sbd_GiaSimRound( pGia, 0, NULL );
+
+ printf( "\n" );
+ Sbd_GiaSimRound( pGia, 1, NULL );
+ printf( "\n" );
+ Sbd_GiaSimRound( pGia, 1, NULL );
+ printf( "\n" );
+ Sbd_GiaSimRound( pGia, 1, NULL );
+
+ Vec_WrdFreeP( &pGia->vSims );
+ Vec_WrdFreeP( &pGia->vSimsPi );
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/opt/sbd/sbdWin.c b/src/opt/sbd/sbdWin.c
new file mode 100644
index 00000000..d722f456
--- /dev/null
+++ b/src/opt/sbd/sbdWin.c
@@ -0,0 +1,283 @@
+/**CFile****************************************************************
+
+ FileName [sbd.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [SAT-based optimization using internal don't-cares.]
+
+ Synopsis []
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: sbd.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "sbdInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Constructs SAT solver for the window.]
+
+ Description [The window for the pivot node (Pivot) is represented as
+ a DFS ordered array of objects (vWinObjs) whose indexed in the array
+ (which will be used as SAT variables) are given in array vObj2Var.
+ The TFO nodes are listed as the last ones in vWinObjs. The root nodes
+ are labeled with Abc_LitIsCompl() in vTfo and also given in vRoots.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, Vec_Int_t * vMirrors, int Pivot, Vec_Int_t * vWinObjs, Vec_Int_t * vObj2Var, Vec_Int_t * vTfo, Vec_Int_t * vRoots )
+{
+ Gia_Obj_t * pObj;
+ int i, iLit = 1, iObj, Fan0, Fan1, Lit0m, Lit1m, Node, fCompl0, fCompl1, RetValue;
+ int TfoStart = Vec_IntSize(vWinObjs) - Vec_IntSize(vTfo);
+ int PivotVar = Vec_IntEntry(vObj2Var, Pivot);
+ //Vec_IntPrint( vWinObjs );
+ //Vec_IntPrint( vTfo );
+ //Vec_IntPrint( vRoots );
+ // create SAT solver
+ if ( pSat == NULL )
+ pSat = sat_solver_new();
+ else
+ sat_solver_restart( pSat );
+ sat_solver_setnvars( pSat, Vec_IntSize(vWinObjs) + Vec_IntSize(vTfo) + Vec_IntSize(vRoots) + 32 );
+ // create constant 0 clause
+ sat_solver_addclause( pSat, &iLit, &iLit + 1 );
+ // add clauses for all nodes
+ Vec_IntForEachEntryStart( vWinObjs, iObj, i, 1 )
+ {
+ pObj = Gia_ManObj( p, iObj );
+ if ( Gia_ObjIsCi(pObj) )
+ continue;
+ assert( Gia_ObjIsAnd(pObj) );
+ assert( Vec_IntEntry( vMirrors, iObj ) < 0 );
+ Node = Vec_IntEntry( vObj2Var, iObj );
+ Lit0m = Vec_IntEntry( vMirrors, Gia_ObjFaninId0(pObj, iObj) );
+ Lit1m = Vec_IntEntry( vMirrors, Gia_ObjFaninId1(pObj, iObj) );
+ Fan0 = Lit0m >= 0 ? Abc_Lit2Var(Lit0m) : Gia_ObjFaninId0(pObj, iObj);
+ Fan1 = Lit1m >= 0 ? Abc_Lit2Var(Lit1m) : Gia_ObjFaninId1(pObj, iObj);
+ Fan0 = Vec_IntEntry( vObj2Var, Fan0 );
+ Fan1 = Vec_IntEntry( vObj2Var, Fan1 );
+ fCompl0 = Gia_ObjFaninC0(pObj) ^ (Lit0m >= 0 && Abc_LitIsCompl(Lit0m));
+ fCompl1 = Gia_ObjFaninC1(pObj) ^ (Lit1m >= 0 && Abc_LitIsCompl(Lit1m));
+ if ( Gia_ObjIsXor(pObj) )
+ sat_solver_add_xor( pSat, Node, Fan0, Fan1, fCompl0 ^ fCompl1 );
+ else
+ sat_solver_add_and( pSat, Node, Fan0, Fan1, fCompl0, fCompl1, 0 );
+ }
+ // add second clauses for the TFO
+ Vec_IntForEachEntryStart( vWinObjs, iObj, i, TfoStart )
+ {
+ pObj = Gia_ManObj( p, iObj );
+ assert( Gia_ObjIsAnd(pObj) );
+ assert( Vec_IntEntry( vMirrors, iObj ) < 0 );
+ Node = Vec_IntEntry( vObj2Var, iObj ) + Vec_IntSize(vTfo);
+ Lit0m = Vec_IntEntry( vMirrors, Gia_ObjFaninId0(pObj, iObj) );
+ Lit1m = Vec_IntEntry( vMirrors, Gia_ObjFaninId1(pObj, iObj) );
+ Fan0 = Lit0m >= 0 ? Abc_Lit2Var(Lit0m) : Gia_ObjFaninId0(pObj, iObj);
+ Fan1 = Lit1m >= 0 ? Abc_Lit2Var(Lit1m) : Gia_ObjFaninId1(pObj, iObj);
+ Fan0 = Vec_IntEntry( vObj2Var, Fan0 );
+ Fan1 = Vec_IntEntry( vObj2Var, Fan1 );
+ Fan0 = Fan0 < TfoStart ? Fan0 : Fan0 + Vec_IntSize(vTfo);
+ Fan1 = Fan1 < TfoStart ? Fan1 : Fan1 + Vec_IntSize(vTfo);
+ fCompl0 = Gia_ObjFaninC0(pObj) ^ (Fan0 == PivotVar) ^ (Lit0m >= 0 && Abc_LitIsCompl(Lit0m));
+ fCompl1 = Gia_ObjFaninC1(pObj) ^ (Fan1 == PivotVar) ^ (Lit1m >= 0 && Abc_LitIsCompl(Lit1m));
+ if ( Gia_ObjIsXor(pObj) )
+ sat_solver_add_xor( pSat, Node, Fan0, Fan1, fCompl0 ^ fCompl1 );
+ else
+ sat_solver_add_and( pSat, Node, Fan0, Fan1, fCompl0, fCompl1, 0 );
+ }
+ if ( Vec_IntSize(vRoots) > 0 )
+ {
+ // create XOR clauses for the roots
+ int nVars = Vec_IntSize(vWinObjs) + Vec_IntSize(vTfo);
+ Vec_Int_t * vFaninVars = Vec_IntAlloc( Vec_IntSize(vRoots) );
+ Vec_IntForEachEntry( vRoots, iObj, i )
+ {
+ assert( Vec_IntEntry( vMirrors, iObj ) < 0 );
+ Node = Vec_IntEntry( vObj2Var, iObj );
+ Vec_IntPush( vFaninVars, Abc_Var2Lit(nVars, 0) );
+ sat_solver_add_xor( pSat, Node, Node + Vec_IntSize(vTfo), nVars++, 0 );
+ }
+ // make OR clause for the last nRoots variables
+ RetValue = sat_solver_addclause( pSat, Vec_IntArray(vFaninVars), Vec_IntLimit(vFaninVars) );
+ Vec_IntFree( vFaninVars );
+ if ( RetValue == 0 )
+ {
+ sat_solver_delete( pSat );
+ return NULL;
+ }
+ assert( sat_solver_nvars(pSat) == nVars + 32 );
+ }
+ // finalize
+ RetValue = sat_solver_simplify( pSat );
+ if ( RetValue == 0 )
+ {
+ sat_solver_delete( pSat );
+ return NULL;
+ }
+ return pSat;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Solves one SAT problem.]
+
+ Description [Computes node function for PivotVar with fanins in vDivVars
+ using don't-care represented in the SAT solver. Uses array vValues to
+ return the values of the first Vec_IntSize(vValues) SAT variables in case
+ the implementation of the node with the given fanins does not exist.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+word Sbd_ManSolve( sat_solver * pSat, int PivotVar, int FreeVar, Vec_Int_t * vDivVars, Vec_Int_t * vValues, Vec_Int_t * vTemp )
+{
+ int nBTLimit = 0;
+ word uCube, uTruth = 0;
+ int status, i, iVar, nFinal, * pFinal, pLits[2], nIter = 0;
+ assert( FreeVar < sat_solver_nvars(pSat) );
+ pLits[0] = Abc_Var2Lit( PivotVar, 0 ); // F = 1
+ pLits[1] = Abc_Var2Lit( FreeVar, 0 ); // iNewLit
+ while ( 1 )
+ {
+ // find onset minterm
+ status = sat_solver_solve( pSat, pLits, pLits + 2, nBTLimit, 0, 0, 0 );
+ if ( status == l_Undef )
+ return SBD_SAT_UNDEC;
+ if ( status == l_False )
+ return uTruth;
+ assert( status == l_True );
+ // remember variable values
+ for ( i = 0; i < Vec_IntSize(vValues); i++ )
+ Vec_IntWriteEntry( vValues, i, 2*sat_solver_var_value(pSat, i) );
+ // collect divisor literals
+ Vec_IntClear( vTemp );
+ Vec_IntPush( vTemp, Abc_LitNot(pLits[0]) ); // F = 0
+ Vec_IntForEachEntry( vDivVars, iVar, i )
+ Vec_IntPush( vTemp, sat_solver_var_literal(pSat, iVar) );
+ // check against offset
+ status = sat_solver_solve( pSat, Vec_IntArray(vTemp), Vec_IntArray(vTemp) + Vec_IntSize(vTemp), nBTLimit, 0, 0, 0 );
+ if ( status == l_Undef )
+ return SBD_SAT_UNDEC;
+ if ( status == l_True )
+ break;
+ assert( status == l_False );
+ // compute cube and add clause
+ nFinal = sat_solver_final( pSat, &pFinal );
+ uCube = ~(word)0;
+ Vec_IntClear( vTemp );
+ Vec_IntPush( vTemp, Abc_LitNot(pLits[1]) ); // NOT(iNewLit)
+ for ( i = 0; i < nFinal; i++ )
+ {
+ if ( pFinal[i] == pLits[0] )
+ continue;
+ Vec_IntPush( vTemp, pFinal[i] );
+ iVar = Vec_IntFind( vDivVars, Abc_Lit2Var(pFinal[i]) ); assert( iVar >= 0 );
+ uCube &= Abc_LitIsCompl(pFinal[i]) ? s_Truths6[iVar] : ~s_Truths6[iVar];
+ }
+ uTruth |= uCube;
+ status = sat_solver_addclause( pSat, Vec_IntArray(vTemp), Vec_IntArray(vTemp) + Vec_IntSize(vTemp) );
+ assert( status );
+ nIter++;
+ }
+ assert( status == l_True );
+ // store the counter-example
+ for ( i = 0; i < Vec_IntSize(vValues); i++ )
+ Vec_IntAddToEntry( vValues, i, sat_solver_var_value(pSat, i) );
+
+ for ( i = 0; i < Vec_IntSize(vValues); i++ )
+ Vec_IntAddToEntry( vValues, i, 0xC );
+/*
+ // reduce the counter example
+ for ( n = 0; n < 2; n++ )
+ {
+ Vec_IntClear( vTemp );
+ Vec_IntPush( vTemp, Abc_Var2Lit(PivotVar, n) ); // n = 0 => F = 1 (expanding offset against onset)
+ for ( i = 0; i < Vec_IntSize(vValues); i++ )
+ Vec_IntPush( vTemp, Abc_Var2Lit(i, !((Vec_IntEntry(vValues, i) >> n) & 1)) );
+ status = sat_solver_solve( pSat, Vec_IntArray(vTemp), Vec_IntArray(vTemp) + Vec_IntSize(vTemp), nBTLimit, 0, 0, 0 );
+ assert( status == l_False );
+ // compute cube and add clause
+ nFinal = sat_solver_final( pSat, &pFinal );
+ for ( i = 0; i < nFinal; i++ )
+ if ( Abc_Lit2Var(pFinal[i]) != PivotVar )
+ Vec_IntAddToEntry( vValues, Abc_Lit2Var(pFinal[i]), 1 << (n+2) );
+ }
+*/
+ return SBD_SAT_SAT;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns a bunch of positive/negative random care minterms.]
+
+ Description [Returns 0/1 if the functions is const 0/1.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static void sat_solver_random_polarity(sat_solver* s)
+{
+ int i, k;
+ for ( i = 0; i < s->size; i += 64 )
+ {
+ word Polar = Gia_ManRandomW(0);
+ for ( k = 0; k < 64 && (i << 6) + k < s->size; k++ )
+ s->polarity[(i << 6) + k] = Abc_TtGetBit(&Polar, k);
+ }
+}
+int Sbd_ManCollectConstants( sat_solver * pSat, int nCareMints[2], int PivotVar, word * pVarSims[], Vec_Int_t * vInds )
+{
+ int nBTLimit = 0;
+ int i, Ind;
+ assert( Vec_IntSize(vInds) == nCareMints[0] + nCareMints[1] );
+ Vec_IntForEachEntry( vInds, Ind, i )
+ {
+ int fOffSet = (int)(i < nCareMints[0]);
+ int status, k, iLit = Abc_Var2Lit( PivotVar, fOffSet );
+ sat_solver_random_polarity( pSat );
+ status = sat_solver_solve( pSat, &iLit, &iLit + 1, nBTLimit, 0, 0, 0 );
+ if ( status == l_Undef )
+ return -2;
+ if ( status == l_False )
+ return fOffSet;
+ for ( k = 0; k <= PivotVar; k++ )
+ if ( Abc_TtGetBit(pVarSims[k], Ind) != sat_solver_var_value(pSat, k) )
+ Abc_TtXorBit(pVarSims[k], Ind);
+ }
+ return -1;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
generated by cgit v1.2.3 (git 2.25.1) at 2024-09-14 02:37:32 +0000