summaryrefslogtreecommitdiffstats
path: root/src/aig
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2007-07-03 08:01:00 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2007-07-03 08:01:00 -0700
commita8db621dc96768cf2cf543be905d534579847020 (patch)
treec5c11558d1adf35b474cebd78d89b2e5ae1bc1bc /src/aig
parentd6804597a397379f826810a736ccbe99bf56c497 (diff)
downloadabc-a8db621dc96768cf2cf543be905d534579847020.tar.gz
abc-a8db621dc96768cf2cf543be905d534579847020.tar.bz2
abc-a8db621dc96768cf2cf543be905d534579847020.zip
Version abc70703
Diffstat (limited to 'src/aig')
-rw-r--r--src/aig/cnf/cnf.h148
-rw-r--r--src/aig/cnf/cnfCore.c101
-rw-r--r--src/aig/cnf/cnfCut.c371
-rw-r--r--src/aig/cnf/cnfData.c (renamed from src/aig/dar/darData2.c)11
-rw-r--r--src/aig/cnf/cnfMan.c173
-rw-r--r--src/aig/cnf/cnfMap.c271
-rw-r--r--src/aig/cnf/cnfPost.c225
-rw-r--r--src/aig/cnf/cnfUtil.c157
-rw-r--r--src/aig/cnf/cnfWrite.c337
-rw-r--r--src/aig/cnf/cnf_.c48
-rw-r--r--src/aig/cnf/module.make8
-rw-r--r--src/aig/dar/dar.h25
-rw-r--r--src/aig/dar/darCnf.c679
-rw-r--r--src/aig/dar/darCore.c5
-rw-r--r--src/aig/dar/darCut.c32
-rw-r--r--src/aig/dar/darLib.c12
-rw-r--r--src/aig/dar/darMan.c72
-rw-r--r--src/aig/fra/fra.h196
-rw-r--r--src/aig/fra/fraAnd.c138
-rw-r--r--src/aig/fra/fraClass.c394
-rw-r--r--src/aig/fra/fraCnf.c285
-rw-r--r--src/aig/fra/fraCore.c64
-rw-r--r--src/aig/fra/fraMan.c188
-rw-r--r--src/aig/fra/fraSat.c328
-rw-r--r--src/aig/fra/fraSim.c599
-rw-r--r--src/aig/fra/fra_.c48
-rw-r--r--src/aig/fra/ivyFraig.c2750
-rw-r--r--src/aig/fra/module.make7
28 files changed, 6953 insertions, 719 deletions
diff --git a/src/aig/cnf/cnf.h b/src/aig/cnf/cnf.h
new file mode 100644
index 00000000..8c27b62d
--- /dev/null
+++ b/src/aig/cnf/cnf.h
@@ -0,0 +1,148 @@
+/**CFile****************************************************************
+
+ FileName [cnf.h]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [DAG-aware AIG rewriting.]
+
+ Synopsis [External declarations.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - April 28, 2007.]
+
+ Revision [$Id: cnf.h,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#ifndef __CNF_H__
+#define __CNF_H__
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+////////////////////////////////////////////////////////////////////////
+/// INCLUDES ///
+////////////////////////////////////////////////////////////////////////
+
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include <assert.h>
+#include <time.h>
+
+#include "vec.h"
+#include "dar.h"
+
+////////////////////////////////////////////////////////////////////////
+/// PARAMETERS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// BASIC TYPES ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Cnf_Man_t_ Cnf_Man_t;
+typedef struct Cnf_Dat_t_ Cnf_Dat_t;
+typedef struct Cnf_Cut_t_ Cnf_Cut_t;
+
+// the CNF asserting outputs of AIG to be 1
+struct Cnf_Dat_t_
+{
+ Dar_Man_t * pMan; // the AIG manager, for which CNF is computed
+ int nVars; // the number of variables
+ int nLiterals; // the number of CNF literals
+ int nClauses; // the number of CNF clauses
+ int ** pClauses; // the CNF clauses
+ int * pVarNums; // the number of CNF variable for each node ID (-1 if unused)
+};
+
+// the cut used to represent node in the AIG
+struct Cnf_Cut_t_
+{
+ char nFanins; // the number of leaves
+ char Cost; // the cost of this cut
+ short nWords; // the number of words in truth table
+ Vec_Int_t * vIsop[2]; // neg/pos ISOPs
+ int pFanins[0]; // the fanins (followed by the truth table)
+};
+
+// the CNF computation manager
+struct Cnf_Man_t_
+{
+ Dar_Man_t * pManAig; // the underlying AIG manager
+ char * pSopSizes; // sizes of SOPs for 4-variable functions
+ char ** pSops; // the SOPs for 4-variable functions
+ int aArea; // the area of the mapping
+ Dar_MmFlex_t * pMemCuts; // memory manager for cuts
+ int nMergeLimit; // the limit on the size of merged cut
+ unsigned * pTruths[4]; // temporary truth tables
+ Vec_Int_t * vMemory; // memory for intermediate ISOP representation
+};
+
+static inline int Cnf_CutLeaveNum( Cnf_Cut_t * pCut ) { return pCut->nFanins; }
+static inline int * Cnf_CutLeaves( Cnf_Cut_t * pCut ) { return pCut->pFanins; }
+static inline unsigned * Cnf_CutTruth( Cnf_Cut_t * pCut ) { return (unsigned *)(pCut->pFanins + pCut->nFanins); }
+
+static inline Cnf_Cut_t * Cnf_ObjBestCut( Dar_Obj_t * pObj ) { return pObj->pData; }
+static inline void Cnf_ObjSetBestCut( Dar_Obj_t * pObj, Cnf_Cut_t * pCut ) { pObj->pData = pCut; }
+
+////////////////////////////////////////////////////////////////////////
+/// MACRO DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// ITERATORS ///
+////////////////////////////////////////////////////////////////////////
+
+// iterator over leaves of the cut
+#define Cnf_CutForEachLeaf( p, pCut, pLeaf, i ) \
+ for ( i = 0; (i < (int)(pCut)->nFanins) && ((pLeaf) = Dar_ManObj(p, (pCut)->pFanins[i])); i++ )
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== cnfCore.c ========================================================*/
+extern Cnf_Dat_t * Cnf_Derive( Cnf_Man_t * p, Dar_Man_t * pAig );
+/*=== cnfCut.c ========================================================*/
+extern Cnf_Cut_t * Cnf_CutCreate( Cnf_Man_t * p, Dar_Obj_t * pObj );
+extern void Cnf_CutPrint( Cnf_Cut_t * pCut );
+extern void Cnf_CutFree( Cnf_Cut_t * pCut );
+extern void Cnf_CutUpdateRefs( Cnf_Man_t * p, Cnf_Cut_t * pCut, Cnf_Cut_t * pCutFan, Cnf_Cut_t * pCutRes );
+extern Cnf_Cut_t * Cnf_CutCompose( Cnf_Man_t * p, Cnf_Cut_t * pCut, Cnf_Cut_t * pCutFan, int iFan );
+/*=== cnfData.c ========================================================*/
+extern void Cnf_ReadMsops( char ** ppSopSizes, char *** ppSops );
+/*=== cnfMan.c ========================================================*/
+extern Cnf_Man_t * Cnf_ManStart();
+extern void Cnf_ManStop( Cnf_Man_t * p );
+extern void Cnf_DataFree( Cnf_Dat_t * p );
+extern void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName );
+void * Cnf_DataWriteIntoSolver( Cnf_Dat_t * p );
+/*=== cnfMap.c ========================================================*/
+extern int Cnf_ManMapForCnf( Cnf_Man_t * p );
+/*=== cnfPost.c ========================================================*/
+extern void Cnf_ManTransferCuts( Cnf_Man_t * p );
+extern void Cnf_ManFreeCuts( Cnf_Man_t * p );
+extern void Cnf_ManPostprocess( Cnf_Man_t * p );
+/*=== cnfUtil.c ========================================================*/
+extern Vec_Ptr_t * Dar_ManScanMapping( Cnf_Man_t * p, int fCollect );
+extern Vec_Ptr_t * Cnf_ManScanMapping( Cnf_Man_t * p, int fCollect );
+/*=== cnfWrite.c ========================================================*/
+extern void Cnf_SopConvertToVector( char * pSop, int nCubes, Vec_Int_t * vCover );
+extern Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped );
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/aig/cnf/cnfCore.c b/src/aig/cnf/cnfCore.c
new file mode 100644
index 00000000..b09f0bdc
--- /dev/null
+++ b/src/aig/cnf/cnfCore.c
@@ -0,0 +1,101 @@
+/**CFile****************************************************************
+
+ FileName [cnfCore.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [AIG-to-CNF conversion.]
+
+ Synopsis []
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - April 28, 2007.]
+
+ Revision [$Id: cnfCore.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "cnf.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Cnf_Dat_t * Cnf_Derive( Cnf_Man_t * p, Dar_Man_t * pAig )
+{
+ Cnf_Dat_t * pCnf = NULL;
+ Vec_Ptr_t * vMapped;
+ int nIters = 2;
+ int clk;
+
+ // connect the managers
+ pAig->pManCnf = p;
+ p->pManAig = pAig;
+
+ // generate cuts for all nodes, assign cost, and find best cuts
+clk = clock();
+ Dar_ManComputeCuts( pAig );
+PRT( "Cuts", clock() - clk );
+/*
+ // iteratively improve area flow
+ for ( i = 0; i < nIters; i++ )
+ {
+clk = clock();
+ Cnf_ManScanMapping( p, 0 );
+ Cnf_ManMapForCnf( p );
+PRT( "iter ", clock() - clk );
+ }
+*/
+ // write the file
+ vMapped = Dar_ManScanMapping( p, 1 );
+ Vec_PtrFree( vMapped );
+
+clk = clock();
+ Cnf_ManTransferCuts( p );
+
+ Cnf_ManPostprocess( p );
+ Cnf_ManScanMapping( p, 0 );
+/*
+ Cnf_ManPostprocess( p );
+ Cnf_ManScanMapping( p, 0 );
+ Cnf_ManPostprocess( p );
+ Cnf_ManScanMapping( p, 0 );
+*/
+PRT( "Ext ", clock() - clk );
+
+/*
+ vMapped = Cnf_ManScanMapping( p, 1 );
+ pCnf = Cnf_ManWriteCnf( p, vMapped );
+ Vec_PtrFree( vMapped );
+
+ // clean up
+ Cnf_ManFreeCuts( p );
+ Dar_ManCutsFree( pAig );
+ return pCnf;
+*/
+ return NULL;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/cnf/cnfCut.c b/src/aig/cnf/cnfCut.c
new file mode 100644
index 00000000..feeef1f2
--- /dev/null
+++ b/src/aig/cnf/cnfCut.c
@@ -0,0 +1,371 @@
+/**CFile****************************************************************
+
+ FileName [cnfCut.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [AIG-to-CNF conversion.]
+
+ Synopsis []
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - April 28, 2007.]
+
+ Revision [$Id: cnfCut.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "cnf.h"
+#include "kit.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Allocates cut of the given size.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Cnf_Cut_t * Cnf_CutAlloc( Cnf_Man_t * p, int nLeaves )
+{
+ Cnf_Cut_t * pCut;
+ int nSize = sizeof(Cnf_Cut_t) + sizeof(int) * nLeaves + sizeof(unsigned) * Dar_TruthWordNum(nLeaves);
+ pCut = (Cnf_Cut_t *)Dar_MmFlexEntryFetch( p->pMemCuts, nSize );
+ pCut->nFanins = nLeaves;
+ pCut->nWords = Dar_TruthWordNum(nLeaves);
+ pCut->vIsop[0] = pCut->vIsop[1] = NULL;
+ return pCut;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Deallocates cut.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Cnf_CutFree( Cnf_Cut_t * pCut )
+{
+ if ( pCut->vIsop[0] )
+ Vec_IntFree( pCut->vIsop[0] );
+ if ( pCut->vIsop[1] )
+ Vec_IntFree( pCut->vIsop[1] );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Creates cut for the given node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Cnf_Cut_t * Cnf_CutCreate( Cnf_Man_t * p, Dar_Obj_t * pObj )
+{
+ Dar_Cut_t * pCutBest;
+ Cnf_Cut_t * pCut;
+ unsigned * pTruth;
+ assert( Dar_ObjIsNode(pObj) );
+ pCutBest = Dar_ObjBestCut( pObj );
+ assert( pCutBest != NULL );
+ assert( pCutBest->nLeaves <= 4 );
+ pCut = Cnf_CutAlloc( p, pCutBest->nLeaves );
+ memcpy( pCut->pFanins, pCutBest->pLeaves, sizeof(int) * pCutBest->nLeaves );
+ pTruth = Cnf_CutTruth(pCut);
+ *pTruth = (pCutBest->uTruth << 16) | pCutBest->uTruth;
+ pCut->Cost = p->pSopSizes[0xFFFF & *pTruth] + p->pSopSizes[0xFFFF & ~*pTruth];
+ return pCut;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Deallocates cut.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Cnf_CutPrint( Cnf_Cut_t * pCut )
+{
+ int i;
+ printf( "{" );
+ for ( i = 0; i < pCut->nFanins; i++ )
+ printf( "%d ", pCut->pFanins[i] );
+ printf( " } " );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Allocates cut of the given size.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Cnf_CutDeref( Cnf_Man_t * p, Cnf_Cut_t * pCut )
+{
+ Dar_Obj_t * pObj;
+ int i;
+ Cnf_CutForEachLeaf( p->pManAig, pCut, pObj, i )
+ {
+ assert( pObj->nRefs > 0 );
+ pObj->nRefs--;
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Allocates cut of the given size.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Cnf_CutRef( Cnf_Man_t * p, Cnf_Cut_t * pCut )
+{
+ Dar_Obj_t * pObj;
+ int i;
+ Cnf_CutForEachLeaf( p->pManAig, pCut, pObj, i )
+ {
+ pObj->nRefs++;
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Allocates cut of the given size.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Cnf_CutUpdateRefs( Cnf_Man_t * p, Cnf_Cut_t * pCut, Cnf_Cut_t * pCutFan, Cnf_Cut_t * pCutRes )
+{
+ Cnf_CutDeref( p, pCut );
+ Cnf_CutDeref( p, pCutFan );
+ Cnf_CutRef( p, pCutRes );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Merges two arrays of integers.]
+
+ Description [Returns the number of items.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Cnf_CutMergeLeaves( Cnf_Cut_t * pCut, Cnf_Cut_t * pCutFan, int * pFanins )
+{
+ int i, k, nFanins = 0;
+ for ( i = k = 0; i < pCut->nFanins && k < pCutFan->nFanins; )
+ {
+ if ( pCut->pFanins[i] == pCutFan->pFanins[k] )
+ pFanins[nFanins++] = pCut->pFanins[i], i++, k++;
+ else if ( pCut->pFanins[i] < pCutFan->pFanins[k] )
+ pFanins[nFanins++] = pCut->pFanins[i], i++;
+ else
+ pFanins[nFanins++] = pCutFan->pFanins[k], k++;
+ }
+ for ( ; i < pCut->nFanins; i++ )
+ pFanins[nFanins++] = pCut->pFanins[i];
+ for ( ; k < pCutFan->nFanins; k++ )
+ pFanins[nFanins++] = pCutFan->pFanins[k];
+ return nFanins;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes the stretching phase of the cut w.r.t. the merged cut.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline unsigned Cnf_TruthPhase( Cnf_Cut_t * pCut, Cnf_Cut_t * pCut1 )
+{
+ unsigned uPhase = 0;
+ int i, k;
+ for ( i = k = 0; i < pCut->nFanins; i++ )
+ {
+ if ( k == pCut1->nFanins )
+ break;
+ if ( pCut->pFanins[i] < pCut1->pFanins[k] )
+ continue;
+ assert( pCut->pFanins[i] == pCut1->pFanins[k] );
+ uPhase |= (1 << i);
+ k++;
+ }
+ return uPhase;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Removes the fanin variable.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Cnf_CutRemoveIthVar( Cnf_Cut_t * pCut, int iVar, int iFan )
+{
+ int i;
+ assert( pCut->pFanins[iVar] == iFan );
+ pCut->nFanins--;
+ for ( i = iVar; i < pCut->nFanins; i++ )
+ pCut->pFanins[i] = pCut->pFanins[i+1];
+}
+
+/**Function*************************************************************
+
+ Synopsis [Inserts the fanin variable.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Cnf_CutInsertIthVar( Cnf_Cut_t * pCut, int iVar, int iFan )
+{
+ int i;
+ for ( i = pCut->nFanins; i > iVar; i-- )
+ pCut->pFanins[i] = pCut->pFanins[i-1];
+ pCut->pFanins[iVar] = iFan;
+ pCut->nFanins++;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Merges two cuts.]
+
+ Description [Returns NULL of the cuts cannot be merged.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Cnf_Cut_t * Cnf_CutCompose( Cnf_Man_t * p, Cnf_Cut_t * pCut, Cnf_Cut_t * pCutFan, int iFan )
+{
+ Cnf_Cut_t * pCutRes;
+ static int pFanins[32];
+ unsigned * pTruth, * pTruthFan, * pTruthRes;
+ unsigned * pTop = p->pTruths[0], * pFan = p->pTruths[2], * pTemp = p->pTruths[3];
+ unsigned uPhase, uPhaseFan;
+ int i, iVar, nFanins, RetValue;
+
+ // make sure the second cut is the fanin of the first
+ for ( iVar = 0; iVar < pCut->nFanins; iVar++ )
+ if ( pCut->pFanins[iVar] == iFan )
+ break;
+ assert( iVar < pCut->nFanins );
+ // remove this variable
+ Cnf_CutRemoveIthVar( pCut, iVar, iFan );
+ // merge leaves of the cuts
+ nFanins = Cnf_CutMergeLeaves( pCut, pCutFan, pFanins );
+ if ( nFanins+1 > p->nMergeLimit )
+ {
+ Cnf_CutInsertIthVar( pCut, iVar, iFan );
+ return NULL;
+ }
+ // create new cut
+ pCutRes = Cnf_CutAlloc( p, nFanins );
+ memcpy( pCutRes->pFanins, pFanins, sizeof(int) * nFanins );
+ assert( pCutRes->nFanins <= pCut->nFanins + pCutFan->nFanins );
+
+ // derive its truth table
+ // get the truth tables in the composition space
+ pTruth = Cnf_CutTruth(pCut);
+ pTruthFan = Cnf_CutTruth(pCutFan);
+ pTruthRes = Cnf_CutTruth(pCutRes);
+ for ( i = 0; i < 2*pCutRes->nWords; i++ )
+ pTop[i] = pTruth[i % pCut->nWords];
+ for ( i = 0; i < pCutRes->nWords; i++ )
+ pFan[i] = pTruthFan[i % pCutFan->nWords];
+ // move the variable to the end
+ uPhase = Kit_BitMask( pCutRes->nFanins+1 ) & ~(1 << iVar);
+ Kit_TruthShrink( pTemp, pTop, pCutRes->nFanins, pCutRes->nFanins+1, uPhase, 1 );
+ // compute the phases
+ uPhase = Cnf_TruthPhase( pCutRes, pCut ) | (1 << pCutRes->nFanins);
+ uPhaseFan = Cnf_TruthPhase( pCutRes, pCutFan );
+ // permute truth-tables to the common support
+ Kit_TruthStretch( pTemp, pTop, pCut->nFanins+1, pCutRes->nFanins+1, uPhase, 1 );
+ Kit_TruthStretch( pTemp, pFan, pCutFan->nFanins, pCutRes->nFanins, uPhaseFan, 1 );
+ // perform Boolean operation
+ Kit_TruthMux( pTruthRes, pTop, pTop+pCutRes->nWords, pFan, pCutRes->nFanins );
+ // return the cut to its original condition
+ Cnf_CutInsertIthVar( pCut, iVar, iFan );
+ // consider the simple case
+ if ( pCutRes->nFanins < 5 )
+ {
+ pCutRes->Cost = p->pSopSizes[0xFFFF & *pTruthRes] + p->pSopSizes[0xFFFF & ~*pTruthRes];
+ return pCutRes;
+ }
+
+ // derive ISOP for positive phase
+ RetValue = Kit_TruthIsop( pTruthRes, pCutRes->nFanins, p->vMemory, 0 );
+ pCutRes->vIsop[1] = (RetValue == -1)? NULL : Vec_IntDup( p->vMemory );
+ // derive ISOP for negative phase
+ Kit_TruthNot( pTruthRes, pTruthRes, pCutRes->nFanins );
+ RetValue = Kit_TruthIsop( pTruthRes, pCutRes->nFanins, p->vMemory, 0 );
+ pCutRes->vIsop[0] = (RetValue == -1)? NULL : Vec_IntDup( p->vMemory );
+ Kit_TruthNot( pTruthRes, pTruthRes, pCutRes->nFanins );
+
+ // compute the cut cost
+ if ( pCutRes->vIsop[0] == NULL || pCutRes->vIsop[1] == NULL )
+ pCutRes->Cost = 127;
+ else if ( Vec_IntSize(pCutRes->vIsop[0]) + Vec_IntSize(pCutRes->vIsop[1]) > 127 )
+ pCutRes->Cost = 127;
+ else
+ pCutRes->Cost = Vec_IntSize(pCutRes->vIsop[0]) + Vec_IntSize(pCutRes->vIsop[1]);
+ return pCutRes;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/dar/darData2.c b/src/aig/cnf/cnfData.c
index 81607ee9..57ce9392 100644
--- a/src/aig/dar/darData2.c
+++ b/src/aig/cnf/cnfData.c
@@ -1,10 +1,10 @@
/**CFile****************************************************************
- FileName [dar_.c]
+ FileName [cnfData.c]
SystemName [ABC: Logic synthesis and verification system.]
- PackageName [DAG-aware AIG rewriting.]
+ PackageName [AIG-to-CNF conversion.]
Synopsis []
@@ -14,11 +14,11 @@
Date [Ver. 1.0. Started - April 28, 2007.]
- Revision [$Id: dar_.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+ Revision [$Id: cnfData.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
***********************************************************************/
-#include "dar.h"
+#include "cnf.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
@@ -4531,7 +4531,7 @@ NULL
SeeAlso []
***********************************************************************/
-void Dar_LibReadMsops( char ** ppSopSizes, char *** ppSops )
+void Cnf_ReadMsops( char ** ppSopSizes, char *** ppSops )
{
unsigned uMasks[4][2] = {
{ 0x5555, 0xAAAA },
@@ -4566,6 +4566,7 @@ void Dar_LibReadMsops( char ** ppSopSizes, char *** ppSops )
// set pointers and compute SOP sizes
pSopSizes = ALLOC( char, 65536 );
pSops = ALLOC( char *, 65536 );
+ pSopSizes[0] = 0;
pSops[0] = NULL;
pPrev = pMemory;
for ( k = 0, i = 1; i < 65536; k++ )
diff --git a/src/aig/cnf/cnfMan.c b/src/aig/cnf/cnfMan.c
new file mode 100644
index 00000000..d1d1fc21
--- /dev/null
+++ b/src/aig/cnf/cnfMan.c
@@ -0,0 +1,173 @@
+/**CFile****************************************************************
+
+ FileName [cnfMan.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [AIG-to-CNF conversion.]
+
+ Synopsis []
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - April 28, 2007.]
+
+ Revision [$Id: cnfMan.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "cnf.h"
+#include "satSolver.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+static inline int Cnf_Lit2Var( int Lit ) { return (Lit & 1)? -(Lit >> 1)-1 : (Lit >> 1)+1; }
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Starts the fraiging manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Cnf_Man_t * Cnf_ManStart()
+{
+ Cnf_Man_t * p;
+ int i;
+ // allocate the manager
+ p = ALLOC( Cnf_Man_t, 1 );
+ memset( p, 0, sizeof(Cnf_Man_t) );
+ // derive internal data structures
+ Cnf_ReadMsops( &p->pSopSizes, &p->pSops );
+ // allocate memory manager for cuts
+ p->pMemCuts = Dar_MmFlexStart();
+ p->nMergeLimit = 10;
+ // allocate temporary truth tables
+ p->pTruths[0] = ALLOC( unsigned, 4 * Dar_TruthWordNum(p->nMergeLimit) );
+ for ( i = 1; i < 4; i++ )
+ p->pTruths[i] = p->pTruths[i-1] + Dar_TruthWordNum(p->nMergeLimit);
+ p->vMemory = Vec_IntAlloc( 1 << 18 );
+ return p;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Stops the fraiging manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Cnf_ManStop( Cnf_Man_t * p )
+{
+ Vec_IntFree( p->vMemory );
+ free( p->pTruths[0] );
+ Dar_MmFlexStop( p->pMemCuts, 0 );
+ free( p->pSopSizes );
+ free( p->pSops[1] );
+ free( p->pSops );
+ free( p );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Cnf_DataFree( Cnf_Dat_t * p )
+{
+ if ( p == NULL )
+ return;
+ free( p->pClauses[0] );
+ free( p->pClauses );
+ free( p->pVarNums );
+ free( p );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Writes CNF into a file.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName )
+{
+ FILE * pFile;
+ int * pLit, * pStop, i;
+ pFile = fopen( pFileName, "w" );
+ if ( pFile == NULL )
+ {
+ printf( "Cnf_WriteIntoFile(): Output file cannot be opened.\n" );
+ return;
+ }
+ fprintf( pFile, "c Result of efficient AIG-to-CNF conversion using package CNF\n" );
+ fprintf( pFile, "p %d %d\n", p->nVars, p->nClauses );
+ for ( i = 0; i < p->nClauses; i++ )
+ {
+ for ( pLit = p->pClauses[i], pStop = p->pClauses[i+1]; pLit < pStop; pLit++ )
+ fprintf( pFile, "%d ", Cnf_Lit2Var(*pLit) );
+ fprintf( pFile, "0\n" );
+ }
+ fprintf( pFile, "\n" );
+ fclose( pFile );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Writes CNF into a file.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void * Cnf_DataWriteIntoSolver( Cnf_Dat_t * p )
+{
+ sat_solver * pSat;
+ int i;
+ pSat = sat_solver_new();
+ sat_solver_setnvars( pSat, p->nVars );
+ for ( i = 0; i < p->nClauses; i++ )
+ {
+ if ( !sat_solver_addclause( pSat, p->pClauses[i], p->pClauses[i+1] ) )
+ {
+ sat_solver_delete( pSat );
+ return NULL;
+ }
+ }
+ return pSat;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/cnf/cnfMap.c b/src/aig/cnf/cnfMap.c
new file mode 100644
index 00000000..09be7701
--- /dev/null
+++ b/src/aig/cnf/cnfMap.c
@@ -0,0 +1,271 @@
+/**CFile****************************************************************
+
+ FileName [cnfMap.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [AIG-to-CNF conversion.]
+
+ Synopsis []
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - April 28, 2007.]
+
+ Revision [$Id: cnfMap.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "cnf.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Computes area of the first level.]
+
+ Description [The cut need to be derefed.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Dar_CutDeref( Dar_Man_t * p, Dar_Cut_t * pCut )
+{
+ Dar_Obj_t * pLeaf;
+ int i;
+ Dar_CutForEachLeaf( p, pCut, pLeaf, i )
+ {
+ assert( pLeaf->nRefs > 0 );
+ if ( --pLeaf->nRefs > 0 || !Dar_ObjIsAnd(pLeaf) )
+ continue;
+ Dar_CutDeref( p, Dar_ObjBestCut(pLeaf) );
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes area of the first level.]
+
+ Description [The cut need to be derefed.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Dar_CutRef( Dar_Man_t * p, Dar_Cut_t * pCut )
+{
+ Dar_Obj_t * pLeaf;
+ int i, Area = pCut->Cost;
+ Dar_CutForEachLeaf( p, pCut, pLeaf, i )
+ {
+ assert( pLeaf->nRefs >= 0 );
+ if ( pLeaf->nRefs++ > 0 || !Dar_ObjIsAnd(pLeaf) )
+ continue;
+ Area += Dar_CutRef( p, Dar_ObjBestCut(pLeaf) );
+ }
+ return Area;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes exact area of the cut.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Cnf_CutArea( Dar_Man_t * p, Dar_Cut_t * pCut )
+{
+ int Area;
+ Area = Dar_CutRef( p, pCut );
+ Dar_CutDeref( p, pCut );
+ return Area;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns 1 if the second cut is better.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Cnf_CutCompare( Dar_Cut_t * pC0, Dar_Cut_t * pC1 )
+{
+ if ( pC0->Area < pC1->Area - 0.0001 )
+ return -1;
+ if ( pC0->Area > pC1->Area + 0.0001 ) // smaller area flow is better
+ return 1;
+// if ( pC0->NoRefs < pC1->NoRefs )
+// return -1;
+// if ( pC0->NoRefs > pC1->NoRefs ) // fewer non-referenced fanins is better
+// return 1;
+// if ( pC0->FanRefs / pC0->nLeaves > pC1->FanRefs / pC1->nLeaves )
+// return -1;
+// if ( pC0->FanRefs / pC0->nLeaves < pC1->FanRefs / pC1->nLeaves )
+// return 1; // larger average fanin ref-counter is better
+// return 0;
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns the cut with the smallest area flow.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Dar_Cut_t * Cnf_ObjFindBestCut( Dar_Obj_t * pObj )
+{
+ Dar_Cut_t * pCut, * pCutBest;
+ int i;
+ pCutBest = NULL;
+ Dar_ObjForEachCut( pObj, pCut, i )
+ if ( pCutBest == NULL || Cnf_CutCompare(pCutBest, pCut) == 1 )
+ pCutBest = pCut;
+ return pCutBest;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes area flow of the cut.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Cnf_CutAssignAreaFlow( Cnf_Man_t * p, Dar_Cut_t * pCut )
+{
+ Dar_Obj_t * pLeaf;
+ int i;
+ pCut->Cost = p->pSopSizes[pCut->uTruth] + p->pSopSizes[0xFFFF & ~pCut->uTruth];
+ pCut->Area = (float)pCut->Cost;
+ pCut->NoRefs = 0;
+ pCut->FanRefs = 0;
+ Dar_CutForEachLeaf( p->pManAig, pCut, pLeaf, i )
+ {
+ if ( !Dar_ObjIsNode(pLeaf) )
+ continue;
+ if ( pLeaf->nRefs == 0 )
+ {
+ pCut->Area += Dar_ObjBestCut(pLeaf)->Area;
+ pCut->NoRefs++;
+ }
+ else
+ {
+ pCut->Area += Dar_ObjBestCut(pLeaf)->Area / pLeaf->nRefs;
+ if ( pCut->FanRefs + pLeaf->nRefs > 15 )
+ pCut->FanRefs = 15;
+ else
+ pCut->FanRefs += pLeaf->nRefs;
+ }
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes area flow of the cut.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Cnf_CutAssignArea( Cnf_Man_t * p, Dar_Cut_t * pCut )
+{
+ Dar_Obj_t * pLeaf;
+ int i;
+ pCut->Area = (float)pCut->Cost;
+ pCut->NoRefs = 0;
+ pCut->FanRefs = 0;
+ Dar_CutForEachLeaf( p->pManAig, pCut, pLeaf, i )
+ {
+ if ( !Dar_ObjIsNode(pLeaf) )
+ continue;
+ if ( pLeaf->nRefs == 0 )
+ {
+ pCut->Area += Dar_ObjBestCut(pLeaf)->Cost;
+ pCut->NoRefs++;
+ }
+ else
+ {
+ if ( pCut->FanRefs + pLeaf->nRefs > 15 )
+ pCut->FanRefs = 15;
+ else
+ pCut->FanRefs += pLeaf->nRefs;
+ }
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs one round of "area recovery" using exact local area.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Cnf_ManMapForCnf( Cnf_Man_t * p )
+{
+ Dar_Obj_t * pObj;
+ Dar_Cut_t * pCut, * pCutBest;
+ int i, k;
+ // visit the nodes in the topological order and update their best cuts
+ Dar_ManForEachNode( p->pManAig, pObj, i )
+ {
+ // find the old best cut
+ pCutBest = Dar_ObjBestCut(pObj);
+ Dar_ObjClearBestCut(pCutBest);
+ // if the node is used, dereference its cut
+ if ( pObj->nRefs )
+ Dar_CutDeref( p->pManAig, pCutBest );
+
+ // evaluate the cuts of this node
+ Dar_ObjForEachCut( pObj, pCut, k )
+// Cnf_CutAssignAreaFlow( p, pCut );
+ pCut->Area = (float)Cnf_CutArea( p->pManAig, pCut );
+
+ // find the new best cut
+ pCutBest = Cnf_ObjFindBestCut(pObj);
+ Dar_ObjSetBestCut( pCutBest );
+ // if the node is used, reference its cut
+ if ( pObj->nRefs )
+ Dar_CutRef( p->pManAig, pCutBest );
+ }
+ return 1;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/cnf/cnfPost.c b/src/aig/cnf/cnfPost.c
new file mode 100644
index 00000000..2f6a6424
--- /dev/null
+++ b/src/aig/cnf/cnfPost.c
@@ -0,0 +1,225 @@
+/**CFile****************************************************************
+
+ FileName [cnfPost.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [AIG-to-CNF conversion.]
+
+ Synopsis []
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - April 28, 2007.]
+
+ Revision [$Id: cnfPost.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "cnf.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Cnf_ManPostprocess_old( Cnf_Man_t * p )
+{
+ extern int Dar_ManLargeCutEval( Dar_Man_t * p, Dar_Obj_t * pRoot, Dar_Cut_t * pCutR, Dar_Cut_t * pCutL, int Leaf );
+ int nNew, Gain, nGain = 0, nVars = 0;
+
+ Dar_Obj_t * pObj, * pFan;
+ Dar_Cut_t * pCutBest, * pCut;
+ int i, k;//, a, b, Counter;
+ Dar_ManForEachObj( p->pManAig, pObj, i )
+ {
+ if ( !Dar_ObjIsNode(pObj) )
+ continue;
+ if ( pObj->nRefs == 0 )
+ continue;
+ pCutBest = Dar_ObjBestCut(pObj);
+ Dar_CutForEachLeaf( p->pManAig, pCutBest, pFan, k )
+ {
+ if ( !Dar_ObjIsNode(pFan) )
+ continue;
+ assert( pFan->nRefs != 0 );
+ if ( pFan->nRefs != 1 )
+ continue;
+ pCut = Dar_ObjBestCut(pFan);
+/*
+ // find how many common variable they have
+ Counter = 0;
+ for ( a = 0; a < (int)pCut->nLeaves; a++ )
+ {
+ for ( b = 0; b < (int)pCutBest->nLeaves; b++ )
+ if ( pCut->pLeaves[a] == pCutBest->pLeaves[b] )
+ break;
+ if ( b == (int)pCutBest->nLeaves )
+ continue;
+ Counter++;
+ }
+ printf( "%d ", Counter );
+*/
+ // find the new truth table after collapsing these two cuts
+ nNew = Dar_ManLargeCutEval( p->pManAig, pObj, pCutBest, pCut, pFan->Id );
+// printf( "%d+%d=%d:%d(%d) ", pCutBest->Cost, pCut->Cost,
+// pCutBest->Cost+pCut->Cost, nNew, pCutBest->Cost+pCut->Cost-nNew );
+
+ Gain = pCutBest->Cost+pCut->Cost-nNew;
+ if ( Gain > 0 )
+ {
+ nGain += Gain;
+ nVars++;
+ }
+ }
+ }
+ printf( "Total gain = %d. Vars = %d.\n", nGain, nVars );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Transfers cuts of the mapped nodes into internal representation.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Cnf_ManTransferCuts( Cnf_Man_t * p )
+{
+ Dar_Obj_t * pObj;
+ int i;
+ Dar_MmFlexRestart( p->pMemCuts );
+ Dar_ManForEachObj( p->pManAig, pObj, i )
+ {
+ if ( Dar_ObjIsNode(pObj) && pObj->nRefs > 0 )
+ pObj->pData = Cnf_CutCreate( p, pObj );
+ else
+ pObj->pData = NULL;
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Transfers cuts of the mapped nodes into internal representation.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Cnf_ManFreeCuts( Cnf_Man_t * p )
+{
+ Dar_Obj_t * pObj;
+ int i;
+ Dar_ManForEachObj( p->pManAig, pObj, i )
+ if ( pObj->pData )
+ {
+ Cnf_CutFree( pObj->pData );
+ pObj->pData = NULL;
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Cnf_ManPostprocess( Cnf_Man_t * p )
+{
+ Cnf_Cut_t * pCut, * pCutFan, * pCutRes;
+ Dar_Obj_t * pObj, * pFan;
+ int Order[16], Costs[16];
+ int i, k, fChanges;
+ Dar_ManForEachNode( p->pManAig, pObj, i )
+ {
+ if ( pObj->nRefs == 0 )
+ continue;
+ pCut = Cnf_ObjBestCut(pObj);
+
+ // sort fanins according to their size
+ Cnf_CutForEachLeaf( p->pManAig, pCut, pFan, k )
+ {
+ Order[k] = k;
+ Costs[k] = Dar_ObjIsNode(pFan)? Cnf_ObjBestCut(pFan)->Cost : 0;
+ }
+ // sort the cuts by Weight
+ do {
+ int Temp;
+ fChanges = 0;
+ for ( k = 0; k < pCut->nFanins - 1; k++ )
+ {
+ if ( Costs[Order[k]] <= Costs[Order[k+1]] )
+ continue;
+ Temp = Order[k];
+ Order[k] = Order[k+1];
+ Order[k+1] = Temp;
+ fChanges = 1;
+ }
+ } while ( fChanges );
+
+
+// Cnf_CutForEachLeaf( p->pManAig, pCut, pFan, k )
+ for ( k = 0; (k < (int)(pCut)->nFanins) && ((pFan) = Dar_ManObj(p->pManAig, (pCut)->pFanins[Order[k]])); k++ )
+ {
+ if ( !Dar_ObjIsNode(pFan) )
+ continue;
+ assert( pFan->nRefs != 0 );
+ if ( pFan->nRefs != 1 )
+ continue;
+ pCutFan = Cnf_ObjBestCut(pFan);
+ // try composing these two cuts
+// Cnf_CutPrint( pCut );
+ pCutRes = Cnf_CutCompose( p, pCut, pCutFan, pFan->Id );
+// Cnf_CutPrint( pCut );
+// printf( "\n" );
+ // check if the cost if reduced
+ if ( pCutRes == NULL || pCutRes->Cost == 127 || pCutRes->Cost > pCut->Cost + pCutFan->Cost )
+ {
+ if ( pCutRes )
+ Cnf_CutFree( pCutRes );
+ continue;
+ }
+ // update the cut
+ Cnf_ObjSetBestCut( pObj, pCutRes );
+ Cnf_ObjSetBestCut( pFan, NULL );
+ Cnf_CutUpdateRefs( p, pCut, pCutFan, pCutRes );
+ assert( pFan->nRefs == 0 );
+ Cnf_CutFree( pCut );
+ Cnf_CutFree( pCutFan );
+ break;
+ }
+ }
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/cnf/cnfUtil.c b/src/aig/cnf/cnfUtil.c
new file mode 100644
index 00000000..249f43fb
--- /dev/null
+++ b/src/aig/cnf/cnfUtil.c
@@ -0,0 +1,157 @@
+/**CFile****************************************************************
+
+ FileName [cnfUtil.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [AIG-to-CNF conversion.]
+
+ Synopsis []
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - April 28, 2007.]
+
+ Revision [$Id: cnfUtil.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "cnf.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Computes area, references, and nodes used in the mapping.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Dar_ManScanMapping_rec( Cnf_Man_t * p, Dar_Obj_t * pObj, Vec_Ptr_t * vMapped )
+{
+ Dar_Obj_t * pLeaf;
+ Dar_Cut_t * pCutBest;
+ int aArea, i;
+ if ( pObj->nRefs++ || Dar_ObjIsPi(pObj) || Dar_ObjIsConst1(pObj) )
+ return 0;
+ assert( Dar_ObjIsAnd(pObj) );
+ // collect the node first to derive pre-order
+ if ( vMapped )
+ Vec_PtrPush( vMapped, pObj );
+ // visit the transitive fanin of the selected cut
+ pCutBest = Dar_ObjBestCut(pObj);
+ aArea = pCutBest->Cost;
+ Dar_CutForEachLeaf( p->pManAig, pCutBest, pLeaf, i )
+ aArea += Dar_ManScanMapping_rec( p, pLeaf, vMapped );
+ return aArea;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes area, references, and nodes used in the mapping.]
+
+ Description [Collects the nodes in reverse topological order.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Ptr_t * Dar_ManScanMapping( Cnf_Man_t * p, int fCollect )
+{
+ Vec_Ptr_t * vMapped = NULL;
+ Dar_Obj_t * pObj;
+ int i;
+ // clean all references
+ Dar_ManForEachObj( p->pManAig, pObj, i )
+ pObj->nRefs = 0;
+ // allocate the array
+ if ( fCollect )
+ vMapped = Vec_PtrAlloc( 1000 );
+ // collect nodes reachable from POs in the DFS order through the best cuts
+ p->aArea = 0;
+ Dar_ManForEachPo( p->pManAig, pObj, i )
+ p->aArea += Dar_ManScanMapping_rec( p, Dar_ObjFanin0(pObj), vMapped );
+ printf( "Variables = %6d. Clauses = %8d.\n", vMapped? Vec_PtrSize(vMapped) : 0, p->aArea );
+ return vMapped;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes area, references, and nodes used in the mapping.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Cnf_ManScanMapping_rec( Cnf_Man_t * p, Dar_Obj_t * pObj, Vec_Ptr_t * vMapped )
+{
+ Dar_Obj_t * pLeaf;
+ Cnf_Cut_t * pCutBest;
+ int aArea, i;
+ if ( pObj->nRefs++ || Dar_ObjIsPi(pObj) || Dar_ObjIsConst1(pObj) )
+ return 0;
+ assert( Dar_ObjIsAnd(pObj) );
+ assert( pObj->pData != NULL );
+ // visit the transitive fanin of the selected cut
+ pCutBest = pObj->pData;
+ assert( pCutBest->Cost < 127 );
+ aArea = pCutBest->Cost;
+ Cnf_CutForEachLeaf( p->pManAig, pCutBest, pLeaf, i )
+ aArea += Cnf_ManScanMapping_rec( p, pLeaf, vMapped );
+ // collect the node first to derive pre-order
+ if ( vMapped )
+ Vec_PtrPush( vMapped, pObj );
+ return aArea;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes area, references, and nodes used in the mapping.]
+
+ Description [Collects the nodes in reverse topological order.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Ptr_t * Cnf_ManScanMapping( Cnf_Man_t * p, int fCollect )
+{
+ Vec_Ptr_t * vMapped = NULL;
+ Dar_Obj_t * pObj;
+ int i;
+ // clean all references
+ Dar_ManForEachObj( p->pManAig, pObj, i )
+ pObj->nRefs = 0;
+ // allocate the array
+ if ( fCollect )
+ vMapped = Vec_PtrAlloc( 1000 );
+ // collect nodes reachable from POs in the DFS order through the best cuts
+ p->aArea = 0;
+ Dar_ManForEachPo( p->pManAig, pObj, i )
+ p->aArea += Cnf_ManScanMapping_rec( p, Dar_ObjFanin0(pObj), vMapped );
+ printf( "Variables = %6d. Clauses = %8d.\n", vMapped? Vec_PtrSize(vMapped) : 0, p->aArea );
+ return vMapped;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/cnf/cnfWrite.c b/src/aig/cnf/cnfWrite.c
new file mode 100644
index 00000000..2637d115
--- /dev/null
+++ b/src/aig/cnf/cnfWrite.c
@@ -0,0 +1,337 @@
+/**CFile****************************************************************
+
+ FileName [cnfWrite.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [AIG-to-CNF conversion.]
+
+ Synopsis []
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - April 28, 2007.]
+
+ Revision [$Id: cnfWrite.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "cnf.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Writes the cover into the array.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Cnf_SopConvertToVector( char * pSop, int nCubes, Vec_Int_t * vCover )
+{
+ int Lits[4], Cube, iCube, i, b;
+ Vec_IntClear( vCover );
+ for ( i = 0; i < nCubes; i++ )
+ {
+ Cube = pSop[i];
+ for ( b = 0; b < 4; b++ )
+ {
+ if ( Cube % 3 == 0 )
+ Lits[b] = 1;
+ else if ( Cube % 3 == 1 )
+ Lits[b] = 2;
+ else
+ Lits[b] = 0;
+ Cube = Cube / 3;
+ }
+ iCube = 0;
+ for ( b = 0; b < 4; b++ )
+ iCube = (iCube << 2) | Lits[b];
+ Vec_IntPush( vCover, iCube );
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns the number of literals in the SOP.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Cnf_SopCountLiterals( char * pSop, int nCubes )
+{
+ int nLits = 0, Cube, i, b;
+ for ( i = 0; i < nCubes; i++ )
+ {
+ Cube = pSop[i];
+ for ( b = 0; b < 4; b++ )
+ {
+ if ( Cube % 3 != 2 )
+ nLits++;
+ Cube = Cube / 3;
+ }
+ }
+ return nLits;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns the number of literals in the SOP.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Cnf_IsopCountLiterals( Vec_Int_t * vIsop, int nVars )
+{
+ int nLits = 0, Cube, i, b;
+ Vec_IntForEachEntry( vIsop, Cube, i )
+ {
+ for ( b = 0; b < nVars; b++ )
+ {
+ if ( (Cube & 3) == 1 || (Cube & 3) == 2 )
+ nLits++;
+ Cube >>= 2;
+ }
+ }
+ return nLits;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Writes the cube and returns the number of literals in it.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Cnf_SopWriteCube( char Cube, int * pVars, int fCompl, int * pLiterals )
+{
+ int nLits = 4, b;
+ for ( b = 0; b < 4; b++ )
+ {
+ if ( Cube % 3 == 0 )
+ *pLiterals++ = 2 * pVars[b] + !fCompl;
+ else if ( Cube % 3 == 1 )
+ *pLiterals++ = 2 * pVars[b] + fCompl;
+ else
+ nLits--;
+ Cube = Cube / 3;
+ }
+ return nLits;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Writes the cube and returns the number of literals in it.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Cnf_IsopWriteCube( int Cube, int nVars, int * pVars, int fCompl, int * pLiterals )
+{
+ int nLits = nVars, b;
+ for ( b = 0; b < nVars; b++ )
+ {
+ if ( (Cube & 3) == 1 )
+ *pLiterals++ = 2 * pVars[b] + !fCompl;
+ else if ( (Cube & 3) == 2 )
+ *pLiterals++ = 2 * pVars[b] + fCompl;
+ else
+ nLits--;
+ Cube >>= 2;
+ }
+ return nLits;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped )
+{
+ Dar_Obj_t * pObj;
+ Cnf_Dat_t * pCnf;
+ Cnf_Cut_t * pCut;
+ int OutVar, pVars[32], * pLits, ** pClas;
+ unsigned uTruth;
+ int i, k, nLiterals, nClauses, nCubes, Cube, Number;
+
+ // count the number of literals and clauses
+ nLiterals = 1 + Dar_ManPoNum( p->pManAig );
+ nClauses = 1 + Dar_ManPoNum( p->pManAig );
+ Vec_PtrForEachEntry( vMapped, pObj, i )
+ {
+ assert( Dar_ObjIsNode(pObj) );
+ pCut = Cnf_ObjBestCut( pObj );
+
+ // positive polarity of the cut
+ if ( pCut->nFanins < 5 )
+ {
+ uTruth = 0xFFFF & *Cnf_CutTruth(pCut);
+ nLiterals += Cnf_SopCountLiterals( p->pSops[uTruth], p->pSopSizes[uTruth] ) + p->pSopSizes[uTruth];
+ assert( p->pSopSizes[uTruth] >= 0 );
+ nClauses += p->pSopSizes[uTruth];
+ }
+ else
+ {
+ nLiterals += Cnf_IsopCountLiterals( pCut->vIsop[1], pCut->nFanins ) + Vec_IntSize(pCut->vIsop[1]);
+ nClauses += Vec_IntSize(pCut->vIsop[1]);
+ }
+ // negative polarity of the cut
+ if ( pCut->nFanins < 5 )
+ {
+ uTruth = 0xFFFF & ~*Cnf_CutTruth(pCut);
+ nLiterals += Cnf_SopCountLiterals( p->pSops[uTruth], p->pSopSizes[uTruth] ) + p->pSopSizes[uTruth];
+ assert( p->pSopSizes[uTruth] >= 0 );
+ nClauses += p->pSopSizes[uTruth];
+ }
+ else
+ {
+ nLiterals += Cnf_IsopCountLiterals( pCut->vIsop[0], pCut->nFanins ) + Vec_IntSize(pCut->vIsop[0]);
+ nClauses += Vec_IntSize(pCut->vIsop[0]);
+ }
+//printf( "%d ", nClauses-(1 + Dar_ManPoNum( p->pManAig )) );
+ }
+//printf( "\n" );
+
+ // allocate CNF
+ pCnf = ALLOC( Cnf_Dat_t, 1 );
+ memset( pCnf, 0, sizeof(Cnf_Dat_t) );
+ pCnf->nLiterals = nLiterals;
+ pCnf->nClauses = nClauses;
+ pCnf->pClauses = ALLOC( int *, nClauses + 1 );
+ pCnf->pClauses[0] = ALLOC( int, nLiterals );
+ pCnf->pClauses[nClauses] = pCnf->pClauses[0] + nLiterals;
+
+ // set variable numbers
+ Number = 0;
+ pCnf->pVarNums = ALLOC( int, 1+Dar_ManObjIdMax(p->pManAig) );
+ memset( pCnf->pVarNums, 0xff, sizeof(int) * (1+Dar_ManObjIdMax(p->pManAig)) );
+ Vec_PtrForEachEntry( vMapped, pObj, i )
+ pCnf->pVarNums[pObj->Id] = Number++;
+ Dar_ManForEachPi( p->pManAig, pObj, i )
+ pCnf->pVarNums[pObj->Id] = Number++;
+ pCnf->pVarNums[Dar_ManConst1(p->pManAig)->Id] = Number++;
+ pCnf->nVars = Number;
+
+ // assign the clauses
+ pLits = pCnf->pClauses[0];
+ pClas = pCnf->pClauses;
+ Vec_PtrForEachEntry( vMapped, pObj, i )
+ {
+ pCut = Cnf_ObjBestCut( pObj );
+
+ // save variables of this cut
+ OutVar = pCnf->pVarNums[ pObj->Id ];
+ for ( k = 0; k < (int)pCut->nFanins; k++ )
+ {
+ pVars[k] = pCnf->pVarNums[ pCut->pFanins[k] ];
+ assert( pVars[k] <= Dar_ManObjIdMax(p->pManAig) );
+ }
+
+ // positive polarity of the cut
+ if ( pCut->nFanins < 5 )
+ {
+ uTruth = 0xFFFF & *Cnf_CutTruth(pCut);
+ nCubes = p->pSopSizes[uTruth];
+ for ( k = 0; k < nCubes; k++ )
+ {
+ *pClas++ = pLits;
+ *pLits++ = 2 * OutVar + 1;
+ pLits += Cnf_SopWriteCube( p->pSops[uTruth][k], pVars, 0, pLits );
+ }
+ }
+ else
+ {
+ Vec_IntForEachEntry( pCut->vIsop[1], Cube, k )
+ {
+ *pClas++ = pLits;
+ *pLits++ = 2 * OutVar + 1;
+ pLits += Cnf_IsopWriteCube( Cube, pCut->nFanins, pVars, 0, pLits );
+ }
+ }
+
+ // negative polarity of the cut
+ if ( pCut->nFanins < 5 )
+ {
+ uTruth = 0xFFFF & ~*Cnf_CutTruth(pCut);
+ nCubes = p->pSopSizes[uTruth];
+ for ( k = 0; k < nCubes; k++ )
+ {
+ *pClas++ = pLits;
+ *pLits++ = 2 * OutVar;
+ pLits += Cnf_SopWriteCube( p->pSops[uTruth][k], pVars, 1, pLits );
+ }
+ }
+ else
+ {
+ Vec_IntForEachEntry( pCut->vIsop[0], Cube, k )
+ {
+ *pClas++ = pLits;
+ *pLits++ = 2 * OutVar;
+ pLits += Cnf_IsopWriteCube( Cube, pCut->nFanins, pVars, 1, pLits );
+ }
+ }
+//printf( "%d ", pClas-pCnf->pClauses );
+ }
+
+ // write the constant literal
+ OutVar = pCnf->pVarNums[ Dar_ManConst1(p->pManAig)->Id ];
+ assert( OutVar <= Dar_ManObjIdMax(p->pManAig) );
+ *pClas++ = pLits;
+ *pLits++ = 2 * OutVar;
+
+ // write the output literals
+ Dar_ManForEachPo( p->pManAig, pObj, i )
+ {
+ OutVar = pCnf->pVarNums[ Dar_ObjFanin0(pObj)->Id ];
+ *pClas++ = pLits;
+ *pLits++ = 2 * OutVar + Dar_ObjFaninC0(pObj);
+ }
+
+ // verify that the correct number of literals and clauses was written
+ assert( pLits - pCnf->pClauses[0] == nLiterals );
+ assert( pClas - pCnf->pClauses == nClauses );
+ return pCnf;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/cnf/cnf_.c b/src/aig/cnf/cnf_.c
new file mode 100644
index 00000000..7c9ca499
--- /dev/null
+++ b/src/aig/cnf/cnf_.c
@@ -0,0 +1,48 @@
+/**CFile****************************************************************
+
+ FileName [cnf_.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [AIG-to-CNF conversion.]
+
+ Synopsis []
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - April 28, 2007.]
+
+ Revision [$Id: cnf_.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "cnf.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/cnf/module.make b/src/aig/cnf/module.make
new file mode 100644
index 00000000..dbcaeba4
--- /dev/null
+++ b/src/aig/cnf/module.make
@@ -0,0 +1,8 @@
+SRC += src/aig/cnf/cnfCore.c \
+ src/aig/cnf/cnfCut.c \
+ src/aig/cnf/cnfData.c \
+ src/aig/cnf/cnfMan.c \
+ src/aig/cnf/cnfMap.c \
+ src/aig/cnf/cnfPost.c \
+ src/aig/cnf/cnfUtil.c \
+ src/aig/cnf/cnfWrite.c
diff --git a/src/aig/dar/dar.h b/src/aig/dar/dar.h
index f71470cf..9744da88 100644
--- a/src/aig/dar/dar.h
+++ b/src/aig/dar/dar.h
@@ -84,10 +84,11 @@ struct Dar_Cut_t_ // 8 words
{
unsigned uSign;
unsigned uTruth : 16; // the truth table of the cut function
- unsigned Cost : 6; // the cost of the cut in terms of CNF clauses
+ unsigned Cost : 5; // the cost of the cut in terms of CNF clauses
unsigned FanRefs : 4; // the average number of fanin references
unsigned NoRefs : 3; // the average number of fanin references
unsigned nLeaves : 3; // the number of leaves
+ unsigned fBest : 1; // marks the best cut
int pLeaves[4]; // the array of leaves
// unsigned char pIndices[4];
float Area; // the area flow or exact area of the cut
@@ -139,6 +140,7 @@ struct Dar_Man_t_
int nNodesInit; // the original number of nodes
Vec_Ptr_t * vLeavesBest; // the best set of leaves
int OutBest; // the best output (in the library)
+ int OutNumBest; // the best number of the output
int GainBest; // the best gain
int LevelBest; // the level of node with the best gain
int ClassBest; // the equivalence class of the best replacement
@@ -146,6 +148,7 @@ struct Dar_Man_t_
int ClassTimes[222];// the runtimes for each class
int ClassGains[222];// the gains for each class
int ClassSubgs[222];// the graphs for each class
+ int nCutMemUsed; // memory used for cuts
// various data members
Dar_MmFixed_t * pMemObjs; // memory manager for objects
Dar_MmFlex_t * pMemCuts; // memory manager for cuts
@@ -155,9 +158,7 @@ struct Dar_Man_t_
int nTravIds; // the current traversal ID
int fCatchExor; // enables EXOR nodes
// CNF mapping
- char * pSopSizes; // sizes of SOPs for 4-variable functions
- char ** pSops; // the SOPs for 4-variable functions
- int aArea; // the area of the mapping
+ void * pManCnf; // CNF conversion manager
// rewriting statistics
int nCutsBad;
int nCutsGood;
@@ -274,8 +275,16 @@ static inline int Dar_ObjFanoutC( Dar_Obj_t * pObj, Dar_Obj_t * pFanout
if ( Dar_ObjFanin1(pFanout) == pObj ) return Dar_ObjFaninC1(pObj);
assert(0); return -1;
}
-static inline Dar_Cut_t * Dar_ObjBestCut( Dar_Obj_t * pObj ) { return (Dar_Cut_t *)pObj->pNext; }
-static inline void Dar_ObjSetBestCut( Dar_Obj_t * pObj, Dar_Cut_t * pCut ) { pObj->pNext = (Dar_Obj_t *)pCut; }
+static inline Dar_Cut_t * Dar_ObjBestCut( Dar_Obj_t * pObj )
+{
+ Dar_Cut_t * pCut; int i;
+ for ( pCut = pObj->pData, i = 0; i < (int)pObj->nCuts; i++, pCut++ )
+ if ( pCut->fBest )
+ return pCut;
+ return NULL;
+}
+static inline void Dar_ObjSetBestCut( Dar_Cut_t * pCut ) { assert( !pCut->fBest ); pCut->fBest = 1; }
+static inline void Dar_ObjClearBestCut( Dar_Cut_t * pCut ) { assert( pCut->fBest ); pCut->fBest = 0; }
// create the ghost of the new node
static inline Dar_Obj_t * Dar_ObjCreateGhost( Dar_Man_t * p, Dar_Obj_t * p0, Dar_Obj_t * p1, Dar_Type_t Type )
@@ -333,6 +342,9 @@ static inline void Dar_ManRecycleMemory( Dar_Man_t * p, Dar_Obj_t * pEntry )
// iterator over all objects, including those currently not used
#define Dar_ManForEachObj( p, pObj, i ) \
Vec_PtrForEachEntry( p->vObjs, pObj, i ) if ( (pObj) == NULL ) {} else
+// iterator over all nodes
+#define Dar_ManForEachNode( p, pObj, i ) \
+ Vec_PtrForEachEntry( p->vObjs, pObj, i ) if ( (pObj) == NULL || !Dar_ObjIsNode(pObj) ) {} else
// iterator over all cuts of the node
#define Dar_ObjForEachCut( pObj, pCut, i ) \
for ( pCut = pObj->pData, i = 0; i < (int)pObj->nCuts; i++, pCut++ ) if ( i==0 ) {} else
@@ -383,6 +395,7 @@ extern void Dar_LibEval( Dar_Man_t * p, Dar_Obj_t * pRoot, Dar_Cut_t
extern Dar_Obj_t * Dar_LibBuildBest( Dar_Man_t * p );
/*=== darMan.c ==========================================================*/
extern Dar_Man_t * Dar_ManStart();
+extern Dar_Man_t * Dar_ManStartFrom( Dar_Man_t * p );
extern Dar_Man_t * Dar_ManDup( Dar_Man_t * p );
extern void Dar_ManStop( Dar_Man_t * p );
extern int Dar_ManCleanup( Dar_Man_t * p );
diff --git a/src/aig/dar/darCnf.c b/src/aig/dar/darCnf.c
deleted file mode 100644
index fd58b875..00000000
--- a/src/aig/dar/darCnf.c
+++ /dev/null
@@ -1,679 +0,0 @@
-/**CFile****************************************************************
-
- FileName [darCnf.c]
-
- SystemName [ABC: Logic synthesis and verification system.]
-
- PackageName [DAG-aware AIG rewriting.]
-
- Synopsis []
-
- Author [Alan Mishchenko]
-
- Affiliation [UC Berkeley]
-
- Date [Ver. 1.0. Started - April 28, 2007.]
-
- Revision [$Id: darCnf.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "dar.h"
-
-////////////////////////////////////////////////////////////////////////
-/// DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
- Synopsis [Dereferences the cut.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-static inline void Dar_CurDeref2( Dar_Man_t * p, Dar_Cut_t * pCut )
-{
- Dar_Obj_t * pLeaf;
- int i;
- Dar_CutForEachLeaf( p, pCut, pLeaf, i )
- {
- assert( pLeaf->nRefs > 0 );
- pLeaf->nRefs--;
- }
-}
-
-/**Function*************************************************************
-
- Synopsis [References the cut.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-static inline void Dar_CurRef2( Dar_Man_t * p, Dar_Cut_t * pCut )
-{
- Dar_Obj_t * pLeaf;
- int i;
- Dar_CutForEachLeaf( p, pCut, pLeaf, i )
- pLeaf->nRefs++;
-}
-
-/**Function*************************************************************
-
- Synopsis [Computes area of the first level.]
-
- Description [The cut need to be derefed.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Dar_CutDeref( Dar_Man_t * p, Dar_Cut_t * pCut )
-{
- Dar_Obj_t * pLeaf;
- int i;
- Dar_CutForEachLeaf( p, pCut, pLeaf, i )
- {
- assert( pLeaf->nRefs > 0 );
- if ( --pLeaf->nRefs > 0 || !Dar_ObjIsAnd(pLeaf) )
- continue;
- Dar_CutDeref( p, Dar_ObjBestCut(pLeaf) );
- }
-}
-
-/**Function*************************************************************
-
- Synopsis [Computes area of the first level.]
-
- Description [The cut need to be derefed.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Dar_CutRef( Dar_Man_t * p, Dar_Cut_t * pCut )
-{
- Dar_Obj_t * pLeaf;
- int i, Area = pCut->Cost;
- Dar_CutForEachLeaf( p, pCut, pLeaf, i )
- {
- assert( pLeaf->nRefs >= 0 );
- if ( pLeaf->nRefs++ > 0 || !Dar_ObjIsAnd(pLeaf) )
- continue;
- Area += Dar_CutRef( p, Dar_ObjBestCut(pLeaf) );
- }
- return Area;
-}
-
-/**Function*************************************************************
-
- Synopsis [Computes exact area of the cut.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Dar_CutArea( Dar_Man_t * p, Dar_Cut_t * pCut )
-{
- int Area = Dar_CutRef( p, pCut );
- Dar_CutDeref( p, pCut );
- return Area;
-}
-
-
-/**Function*************************************************************
-
- Synopsis [Returns 1 if the second cut is better.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-static inline int Dar_CutCompare( Dar_Cut_t * pC0, Dar_Cut_t * pC1 )
-{
- if ( pC0->Area < pC1->Area - 0.0001 )
- return -1;
- if ( pC0->Area > pC1->Area + 0.0001 ) // smaller area flow is better
- return 1;
-/*
- if ( pC0->NoRefs < pC1->NoRefs )
- return -1;
- if ( pC0->NoRefs > pC1->NoRefs ) // fewer non-referenced fanins is better
- return 1;
-*/
-// if ( pC0->FanRefs / pC0->nLeaves > pC1->FanRefs / pC1->nLeaves )
-// return -1;
-
-// if ( pC0->FanRefs / pC0->nLeaves < pC1->FanRefs / pC1->nLeaves )
- return 1; // larger average fanin ref-counter is better
-// return 0;
-}
-
-/**Function*************************************************************
-
- Synopsis [Returns the cut with the smallest area flow.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Dar_Cut_t * Dar_ObjFindBestCut( Dar_Obj_t * pObj )
-{
- Dar_Cut_t * pCut, * pCutBest;
- int i;
- pCutBest = NULL;
- Dar_ObjForEachCut( pObj, pCut, i )
- if ( pCutBest == NULL || Dar_CutCompare(pCutBest, pCut) == 1 )
- pCutBest = pCut;
- return pCutBest;
-}
-
-/**Function*************************************************************
-
- Synopsis [Computes area flow of the cut.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Dar_CutAssignAreaFlow( Dar_Man_t * p, Dar_Cut_t * pCut )
-{
- Dar_Obj_t * pLeaf;
- int i;
- pCut->Area = (float)pCut->Cost;
- pCut->NoRefs = 0;
- pCut->FanRefs = 0;
- Dar_CutForEachLeaf( p, pCut, pLeaf, i )
- {
- if ( !Dar_ObjIsNode(pLeaf) )
- continue;
- if ( pLeaf->nRefs == 0 )
- {
- pCut->Area += Dar_ObjBestCut(pLeaf)->Area;
-// pCut->NoRefs++;
- }
- else
- {
- pCut->Area += Dar_ObjBestCut(pLeaf)->Area / pLeaf->nRefs;
-// if ( pCut->FanRefs + pLeaf->nRefs > 15 )
-// pCut->FanRefs = 15;
-// else
-// pCut->FanRefs += pLeaf->nRefs;
- }
- }
-}
-
-/**Function*************************************************************
-
- Synopsis [Computes area flow of the cut.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Dar_CutAssignArea( Dar_Man_t * p, Dar_Cut_t * pCut )
-{
- Dar_Obj_t * pLeaf;
- int i;
- pCut->Area = (float)pCut->Cost;
- pCut->NoRefs = 0;
- pCut->FanRefs = 0;
- Dar_CutForEachLeaf( p, pCut, pLeaf, i )
- {
- if ( !Dar_ObjIsNode(pLeaf) )
- continue;
- if ( pLeaf->nRefs == 0 )
- {
- pCut->Area += Dar_ObjBestCut(pLeaf)->Cost;
- pCut->NoRefs++;
- }
- else
- {
- if ( pCut->FanRefs + pLeaf->nRefs > 15 )
- pCut->FanRefs = 15;
- else
- pCut->FanRefs += pLeaf->nRefs;
- }
- }
-}
-
-
-/**Function*************************************************************
-
- Synopsis [Computes area, references, and nodes used in the mapping.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Dar_ManScanMapping_rec( Dar_Man_t * p, Dar_Obj_t * pObj, Vec_Ptr_t * vMapped )
-{
- Dar_Obj_t * pLeaf;
- Dar_Cut_t * pCutBest;
- int aArea, i;
- if ( pObj->nRefs++ || Dar_ObjIsPi(pObj) || Dar_ObjIsConst1(pObj) )
- return 0;
- assert( Dar_ObjIsAnd(pObj) );
- // collect the node first to derive pre-order
- if ( vMapped )
- {
-// printf( "%d ", Dar_ObjBestCut(pObj)->Cost );
- Vec_PtrPush( vMapped, pObj );
- }
- // visit the transitive fanin of the selected cut
- pCutBest = Dar_ObjBestCut(pObj);
- aArea = pCutBest->Cost;
- Dar_CutForEachLeaf( p, pCutBest, pLeaf, i )
- aArea += Dar_ManScanMapping_rec( p, pLeaf, vMapped );
- return aArea;
-}
-
-/**Function*************************************************************
-
- Synopsis [Computes area, references, and nodes used in the mapping.]
-
- Description [Collects the nodes in reverse topological order in array
- p->vMapping.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Vec_Ptr_t * Dar_ManScanMapping( Dar_Man_t * p, int fCollect )
-{
- Vec_Ptr_t * vMapped = NULL;
- Dar_Obj_t * pObj;
- int i;
- // clean all references
- Dar_ManForEachObj( p, pObj, i )
- pObj->nRefs = 0;
- // allocate the array
- if ( fCollect )
- vMapped = Vec_PtrAlloc( 1000 );
- // collect nodes reachable from POs in the DFS order through the best cuts
- p->aArea = 0;
- Dar_ManForEachPo( p, pObj, i )
- p->aArea += Dar_ManScanMapping_rec( p, Dar_ObjFanin0(pObj), vMapped );
- printf( "Variables = %d. Clauses = %6d.\n", vMapped? Vec_PtrSize(vMapped) : 0, p->aArea );
- return vMapped;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Dar_ManMapForCnf( Dar_Man_t * p )
-{
- Dar_Obj_t * pObj;
- Dar_Cut_t * pCut;
- int i, k;
- // visit the nodes in the topological order and update their best cuts
- Dar_ManForEachObj( p, pObj, i )
- {
- if ( !Dar_ObjIsNode(pObj) )
- continue;
-// if ( pObj->nRefs )
-// continue;
-
- // if the node is used, dereference its cut
- if ( pObj->nRefs )
- Dar_CutDeref( p, Dar_ObjBestCut(pObj) );
- // evaluate the cuts of this node
- Dar_ObjForEachCut( pObj, pCut, k )
-// Dar_CutAssignArea( p, pCut );
-// Dar_CutAssignAreaFlow( p, pCut );
- pCut->Area = (float)Dar_CutArea( p, pCut );
- // find a new good cut
- Dar_ObjSetBestCut( pObj, Dar_ObjFindBestCut(pObj) );
- // if the node is used, reference its cut
- if ( pObj->nRefs )
- Dar_CutRef( p, Dar_ObjBestCut(pObj) );
- }
- return 1;
-}
-
-/**Function*************************************************************
-
- Synopsis [Returns the number of literals in the SOP.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Dar_SopCountLiterals( char * pSop, int nCubes )
-{
- int nLits = 0, Cube, i, b;
- for ( i = 0; i < nCubes; i++ )
- {
- Cube = pSop[i];
- for ( b = 3; b >= 0; b-- )
- {
- if ( Cube % 3 != 2 )
- nLits++;
- Cube = Cube / 3;
- }
- }
- return nLits;
-}
-
-/**Function*************************************************************
-
- Synopsis [Writes the cube and returns the number of literals in it.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Dar_SopWriteCube( char Cube, int * pVars, int fCompl, int * pLiterals )
-{
- int nLits = 4, b;
- for ( b = 3; b >= 0; b-- )
- {
- if ( Cube % 3 == 0 )
- *pLiterals++ = 2 * pVars[b] + 1 ^ fCompl;
- else if ( Cube % 3 == 1 )
- *pLiterals++ = 2 * pVars[b] + fCompl;
- else
- nLits--;
- Cube = Cube / 3;
- }
- return nLits;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Dar_Cnf_t * Dar_ManWriteCnf( Dar_Man_t * p, Vec_Ptr_t * vMapped )
-{
- Dar_Cnf_t * pCnf;
- Dar_Obj_t * pObj;
- Dar_Cut_t * pCut;
- int OutVar, pVars[4], * pLits, ** pClas;
- unsigned uTruth;
- int i, k, nLiterals, nClauses, nCubes, Number;
-
- // count the number of literals and clauses
- nLiterals = 1 + Dar_ManPoNum( p );
- nClauses = 1 + Dar_ManPoNum( p );
- Vec_PtrForEachEntry( vMapped, pObj, i )
- {
- assert( Dar_ObjIsNode(pObj) );
- pCut = Dar_ObjBestCut( pObj );
- // positive polarity of the cut
- uTruth = pCut->uTruth;
- nLiterals += Dar_SopCountLiterals( p->pSops[uTruth], p->pSopSizes[uTruth] ) + p->pSopSizes[uTruth];
- nClauses += p->pSopSizes[uTruth];
- // negative polarity of the cut
- uTruth = 0xFFFF & ~pCut->uTruth;
- nLiterals += Dar_SopCountLiterals( p->pSops[uTruth], p->pSopSizes[uTruth] ) + p->pSopSizes[uTruth];
- nClauses += p->pSopSizes[uTruth];
- }
-
- // allocate CNF
- pCnf = ALLOC( Dar_Cnf_t, 1 );
- memset( pCnf, 0, sizeof(Dar_Cnf_t) );
- pCnf->nLiterals = nLiterals;
- pCnf->nClauses = nClauses;
- pCnf->pClauses = ALLOC( int *, nClauses );
- pCnf->pClauses[0] = ALLOC( int, nLiterals );
- pCnf->pVarNums = ALLOC( int, 1+Dar_ManObjIdMax(p) );
-
- // set variable numbers
- Number = 0;
- memset( pCnf->pVarNums, 0xff, sizeof(int) * (1+Dar_ManObjIdMax(p)) );
- Vec_PtrForEachEntry( vMapped, pObj, i )
- pCnf->pVarNums[pObj->Id] = Number++;
- Dar_ManForEachPi( p, pObj, i )
- pCnf->pVarNums[pObj->Id] = Number++;
- pCnf->pVarNums[Dar_ManConst1(p)->Id] = Number++;
-
- // assign the clauses
- pLits = pCnf->pClauses[0];
- pClas = pCnf->pClauses;
- Vec_PtrForEachEntry( vMapped, pObj, i )
- {
- pCut = Dar_ObjBestCut( pObj );
- // write variables of this cut
- OutVar = pCnf->pVarNums[ pObj->Id ];
- for ( k = 0; k < (int)pCut->nLeaves; k++ )
- {
- pVars[k] = pCnf->pVarNums[ pCut->pLeaves[k] ];
- assert( pVars[k] <= Dar_ManObjIdMax(p) );
- }
-
- // positive polarity of the cut
- uTruth = pCut->uTruth;
- nCubes = p->pSopSizes[uTruth];
- // write the cubes
- for ( k = 0; k < nCubes; k++ )
- {
- *pClas++ = pLits;
- *pLits++ = 2 * pVars[OutVar] + 1;
- pLits += Dar_SopWriteCube( p->pSops[uTruth][k], pVars, 0, pLits );
- }
-
- // negative polarity of the cut
- uTruth = 0xFFFF & ~pCut->uTruth;
- nCubes = p->pSopSizes[uTruth];
- // write the cubes
- for ( k = 0; k < nCubes; k++ )
- {
- *pClas++ = pLits;
- *pLits++ = 2 * pVars[OutVar];
- pLits += Dar_SopWriteCube( p->pSops[uTruth][k], pVars, 1, pLits );
- }
- }
-
- // write the output literals
- Dar_ManForEachPo( p, pObj, i )
- {
- OutVar = pCnf->pVarNums[ Dar_ObjFanin0(pObj)->Id ];
- *pClas++ = pLits;
- *pLits++ = 2 * pVars[OutVar] + Dar_ObjFaninC0(pObj);
- }
- // write the constant literal
- OutVar = pCnf->pVarNums[ Dar_ManConst1(p)->Id ];
- assert( OutVar <= Dar_ManObjIdMax(p) );
- *pClas++ = pLits;
- *pLits++ = 2 * pVars[OutVar];
-
- // verify that the correct number of literals and clauses was written
- assert( pLits - pCnf->pClauses[0] == nLiterals );
- assert( pClas - pCnf->pClauses == nClauses );
- return pCnf;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Dar_CnfFree( Dar_Cnf_t * pCnf )
-{
- if ( pCnf == NULL )
- return;
- free( pCnf->pClauses[0] );
- free( pCnf->pClauses );
- free( pCnf->pVarNums );
- free( pCnf );
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Dar_ManExploreMapping( Dar_Man_t * p )
-{
- extern int Dar_ManLargeCutEval( Dar_Man_t * p, Dar_Obj_t * pRoot, Dar_Cut_t * pCutR, Dar_Cut_t * pCutL, int Leaf );
- int nNew, Gain, nGain = 0, nVars = 0;
-
- Dar_Obj_t * pObj, * pLeaf;
- Dar_Cut_t * pCutBest, * pCut;
- int i, k, a, b, Counter;
- Dar_ManForEachObj( p, pObj, i )
- {
- if ( !Dar_ObjIsNode(pObj) )
- continue;
- if ( pObj->nRefs == 0 )
- continue;
- pCutBest = Dar_ObjBestCut(pObj);
- Dar_CutForEachLeaf( p, pCutBest, pLeaf, k )
- {
- if ( !Dar_ObjIsNode(pLeaf) )
- continue;
- assert( pLeaf->nRefs != 0 );
- if ( pLeaf->nRefs != 1 )
- continue;
- pCut = Dar_ObjBestCut(pLeaf);
-/*
- // find how many common variable they have
- Counter = 0;
- for ( a = 0; a < (int)pCut->nLeaves; a++ )
- {
- for ( b = 0; b < (int)pCutBest->nLeaves; b++ )
- if ( pCut->pLeaves[a] == pCutBest->pLeaves[b] )
- break;
- if ( b == (int)pCutBest->nLeaves )
- continue;
- Counter++;
- }
- printf( "%d ", Counter );
-*/
- // find the new truth table after collapsing these two cuts
- nNew = Dar_ManLargeCutEval( p, pObj, pCutBest, pCut, pLeaf->Id );
-// printf( "%d+%d=%d:%d(%d) ", pCutBest->Cost, pCut->Cost,
-// pCutBest->Cost+pCut->Cost, nNew, pCutBest->Cost+pCut->Cost-nNew );
-
- Gain = pCutBest->Cost+pCut->Cost-nNew;
- if ( Gain > 0 )
- {
- nGain += Gain;
- nVars++;
- }
- }
- }
- printf( "Total gain = %d. Vars = %d.\n", nGain, nVars );
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Dar_Cnf_t * Dar_ManDeriveCnf( Dar_Man_t * p )
-{
- Dar_Cnf_t * pCnf = NULL;
- Vec_Ptr_t * vMapped;
- int i, nIters = 2;
- int clk;
-
- // derive SOPs for all 4-variable functions
-clk = clock();
- Dar_LibReadMsops( &p->pSopSizes, &p->pSops );
-PRT( "setup", clock() - clk );
-
- // generate cuts for all nodes, assign cost, and find best cuts
- // (used pObj->pNext for storing the best cut of the node!)
-clk = clock();
- Dar_ManComputeCuts( p );
-PRT( "cuts ", clock() - clk );
-
- // iteratively improve area flow
- for ( i = 0; i < nIters; i++ )
- {
-clk = clock();
- Dar_ManScanMapping( p, 0 );
- Dar_ManMapForCnf( p );
-PRT( "iter ", clock() - clk );
- }
-
- // write the file
- vMapped = Dar_ManScanMapping( p, 1 );
-clk = clock();
- Dar_ManExploreMapping( p );
-PRT( "exten", clock() - clk );
-// pCnf = Dar_ManWriteCnf( p, vMapped );
- Vec_PtrFree( vMapped );
-
- // clean up
- Dar_ManCutsFree( p );
- return pCnf;
-}
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/aig/dar/darCore.c b/src/aig/dar/darCore.c
index 820b0002..147cd38f 100644
--- a/src/aig/dar/darCore.c
+++ b/src/aig/dar/darCore.c
@@ -106,11 +106,15 @@ p->timeCuts += clock() - clk;
// count gains of this class
p->ClassGains[p->ClassBest] += nNodeBefore - nNodeAfter;
+// if ( p->ClassBest == 29 )
+// printf( "%d ", p->OutNumBest );
+
}
p->timeTotal = clock() - clkStart;
p->timeOther = p->timeTotal - p->timeCuts - p->timeEval;
Extra_ProgressBarStop( pProgress );
+ p->nCutMemUsed = Dar_MmFlexReadMemUsage(p->pMemCuts)/(1<<20);
Dar_ManCutsFree( p );
// put the nodes into the DFS order and reassign their IDs
// Dar_NtkReassignIds( p );
@@ -161,7 +165,6 @@ int Dar_ManComputeCuts( Dar_Man_t * p )
Dar_ManNodeNum(p), nCutsTotal, nCutsMax, (float)nCutsTotal/Dar_ManNodeNum(p),
p->nCutsFiltered, p->nCutsFiltered+nCutsTotal+Dar_ManNodeNum(p)+Dar_ManPiNum(p) );
PRT( "Time", clock() - clkStart );
-
// free the cuts
// Dar_ManCutsFree( p );
return 1;
diff --git a/src/aig/dar/darCut.c b/src/aig/dar/darCut.c
index 51b0bb10..48f4dc6c 100644
--- a/src/aig/dar/darCut.c
+++ b/src/aig/dar/darCut.c
@@ -65,7 +65,7 @@ static inline int Dar_CutCheckDominance( Dar_Cut_t * pDom, Dar_Cut_t * pCut )
SeeAlso []
***********************************************************************/
-int Dar_CutFilter( Dar_Man_t * p, Dar_Cut_t * pCut )
+static inline int Dar_CutFilter( Dar_Man_t * p, Dar_Cut_t * pCut )
{
Dar_Cut_t * pTemp;
int i, k;
@@ -213,7 +213,7 @@ static inline int Dar_CutMergeOrdered( Dar_Cut_t * pC, Dar_Cut_t * pC0, Dar_Cut_
SeeAlso []
***********************************************************************/
-int Dar_CutMerge( Dar_Cut_t * pCut, Dar_Cut_t * pCut0, Dar_Cut_t * pCut1 )
+static inline int Dar_CutMerge( Dar_Cut_t * pCut, Dar_Cut_t * pCut0, Dar_Cut_t * pCut1 )
{
// merge the nodes
if ( pCut0->nLeaves <= pCut1->nLeaves )
@@ -347,7 +347,7 @@ static inline unsigned Dar_CutTruthShrink( unsigned uTruth, int nVars, unsigned
SeeAlso []
***********************************************************************/
-unsigned Dar_CutTruth( Dar_Cut_t * pCut, Dar_Cut_t * pCut0, Dar_Cut_t * pCut1, int fCompl0, int fCompl1 )
+static inline unsigned Dar_CutTruth( Dar_Cut_t * pCut, Dar_Cut_t * pCut0, Dar_Cut_t * pCut1, int fCompl0, int fCompl1 )
{
unsigned uTruth0 = fCompl0 ? ~pCut0->uTruth : pCut0->uTruth;
unsigned uTruth1 = fCompl1 ? ~pCut1->uTruth : pCut1->uTruth;
@@ -367,7 +367,7 @@ unsigned Dar_CutTruth( Dar_Cut_t * pCut, Dar_Cut_t * pCut0, Dar_Cut_t * pCut1, i
SeeAlso []
***********************************************************************/
-int Dar_CutSuppMinimize( Dar_Cut_t * pCut )
+static inline int Dar_CutSuppMinimize( Dar_Cut_t * pCut )
{
unsigned uMasks[4][2] = {
{ 0x5555, 0xAAAA },
@@ -420,7 +420,7 @@ void Dar_ObjSetupTrivial( Dar_Obj_t * pObj )
{
Dar_Cut_t * pCut;
pCut = pObj->pData;
- pCut->Cost = 0;
+ memset( pCut, 0, sizeof(Dar_Cut_t) );
pCut->nLeaves = 1;
pCut->pLeaves[0] = pObj->Id;
// pCut->pIndices[0] = 0;
@@ -464,10 +464,7 @@ void Dar_ManSetupPis( Dar_Man_t * p )
***********************************************************************/
void Dar_ManCutsFree( Dar_Man_t * p )
{
- Dar_Obj_t * pObj;
- int i;
- Dar_ManForEachObj( p, pObj, i )
- pObj->pData = NULL;
+// Dar_ManCleanData( p );
Dar_MmFlexStop( p->pMemCuts, 0 );
p->pMemCuts = NULL;
}
@@ -519,11 +516,11 @@ Dar_Cut_t * Dar_ObjComputeCuts( Dar_Man_t * p, Dar_Obj_t * pObj )
continue;
}
- // CNF mapping: assign the cut cost if needed
- if ( p->pSopSizes )
+ // CNF mapping: assign the cut cost
+ if ( p->pManCnf )
{
- pCut->Cost = p->pSopSizes[pCut->uTruth] + p->pSopSizes[0xFFFF & ~pCut->uTruth];
- Dar_CutAssignAreaFlow( p, pCut );
+ extern void Cnf_CutAssignAreaFlow( void * pManCnf, Dar_Cut_t * pCut );
+ Cnf_CutAssignAreaFlow( p->pManCnf, pCut );
}
// increment the number of cuts
@@ -538,9 +535,12 @@ Dar_Cut_t * Dar_ObjComputeCuts( Dar_Man_t * p, Dar_Obj_t * pObj )
for ( i = 0; i < p->nCutsUsed; i++ )
*++pCut = *(p->pBaseCuts[i]);
- // CNF mapping: assign the best cut if needed
- if ( p->pSopSizes )
- Dar_ObjSetBestCut( pObj, Dar_ObjFindBestCut(pObj) );
+ // CNF mapping: assign the best cut
+ if ( p->pManCnf )
+ {
+ extern Dar_Cut_t * Cnf_ObjFindBestCut( Dar_Obj_t * pObj );
+ Dar_ObjSetBestCut( Cnf_ObjFindBestCut(pObj) );
+ }
return pObj->pData;
}
diff --git a/src/aig/dar/darLib.c b/src/aig/dar/darLib.c
index c92324f6..89ce2f0b 100644
--- a/src/aig/dar/darLib.c
+++ b/src/aig/dar/darLib.c
@@ -273,6 +273,7 @@ void Dar_LibSetup( Dar_Lib_t * p, Vec_Int_t * vOuts )
for ( k = 0; k < p->nSubgr[i]; k++ )
Dar_LibSetup_rec( p, Dar_LibObj(p, p->pSubgr[i][k]), i );
nNodesTotal += p->nNodes[i];
+//printf( "Class %3d : Subgraphs = %4d. Nodes = %5d.\n", i, p->nSubgr[i], p->nNodes[i] );
}
assert( nNodesTotal == p->pNodesTotal );
// prepare the number of the PI nodes
@@ -604,6 +605,8 @@ void Dar_LibEval( Dar_Man_t * p, Dar_Obj_t * pRoot, Dar_Cut_t * pCut, int Requir
int i, k, Class, nNodesSaved, nNodesAdded, nNodesGained, clk;
if ( pCut->nLeaves != 4 )
return;
+// if ( s_DarLib->nSubgr[ s_DarLib->pMap[pCut->uTruth] ] > 100 )
+// return;
clk = clock();
/*
for ( k = 0; k < 4; k++ )
@@ -643,10 +646,11 @@ void Dar_LibEval( Dar_Man_t * p, Dar_Obj_t * pRoot, Dar_Cut_t * pCut, int Requir
Vec_PtrClear( p->vLeavesBest );
for ( k = 0; k < 4; k++ )
Vec_PtrPush( p->vLeavesBest, s_DarLib->pDatas[k].pFunc );
- p->OutBest = s_DarLib->pSubgr[Class][i];
- p->LevelBest = s_DarLib->pDatas[pObj->Num].Level;
- p->GainBest = nNodesGained;
- p->ClassBest = Class;
+ p->OutBest = s_DarLib->pSubgr[Class][i];
+ p->OutNumBest = i;
+ p->LevelBest = s_DarLib->pDatas[pObj->Num].Level;
+ p->GainBest = nNodesGained;
+ p->ClassBest = Class;
}
clk = clock() - clk;
p->ClassTimes[Class] += clk;
diff --git a/src/aig/dar/darMan.c b/src/aig/dar/darMan.c
index da66043e..25b15e9c 100644
--- a/src/aig/dar/darMan.c
+++ b/src/aig/dar/darMan.c
@@ -79,6 +79,68 @@ Dar_Man_t * Dar_ManStart( int nNodesMax )
/**Function*************************************************************
+ Synopsis [Duplicates the AIG manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Dar_Man_t * Dar_ManStartFrom( Dar_Man_t * p )
+{
+ Dar_Man_t * pNew;
+ Dar_Obj_t * pObj;
+ int i;
+ // create the new manager
+ pNew = Dar_ManStart();
+ // create the PIs
+ Dar_ManConst1(p)->pData = Dar_ManConst1(pNew);
+ Dar_ManForEachPi( p, pObj, i )
+ pObj->pData = Dar_ObjCreatePi(pNew);
+ return pNew;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Duplicates the AIG manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Dar_Man_t * Dar_ManDup( Dar_Man_t * p )
+{
+ Dar_Man_t * pNew;
+ Dar_Obj_t * pObj;
+ int i;
+ // create the new manager
+ pNew = Dar_ManStart();
+ // create the PIs
+ Dar_ManConst1(p)->pData = Dar_ManConst1(pNew);
+ Dar_ManForEachPi( p, pObj, i )
+ pObj->pData = Dar_ObjCreatePi(pNew);
+ // duplicate internal nodes
+ Dar_ManForEachObj( p, pObj, i )
+ if ( Dar_ObjIsBuf(pObj) )
+ pObj->pData = Dar_ObjChild0Copy(pObj);
+ else if ( Dar_ObjIsNode(pObj) )
+ pObj->pData = Dar_And( pNew, Dar_ObjChild0Copy(pObj), Dar_ObjChild1Copy(pObj) );
+ // add the POs
+ Dar_ManForEachPo( p, pObj, i )
+ Dar_ObjCreatePo( pNew, Dar_ObjChild0Copy(pObj) );
+ // check the resulting network
+ if ( !Dar_ManCheck(pNew) )
+ printf( "Dar_ManDup(): The check has failed.\n" );
+ return pNew;
+}
+
+/**Function*************************************************************
+
Synopsis [Stops the AIG manager.]
Description []
@@ -107,13 +169,6 @@ void Dar_ManStop( Dar_Man_t * p )
if ( p->vRequired ) Vec_IntFree( p->vRequired );
if ( p->vLeavesBest ) Vec_PtrFree( p->vLeavesBest );
free( p->pTable );
- // free CNF mapping data
- if ( p->pSopSizes )
- {
- free( p->pSopSizes );
- free( p->pSops[1] );
- free( p->pSops );
- }
free( p );
}
@@ -185,7 +240,8 @@ void Dar_ManPrintStats( Dar_Man_t * p )
void Dar_ManPrintRuntime( Dar_Man_t * p )
{
int i, Gain;
- printf( "Good cuts = %d. Bad cuts = %d.\n", p->nCutsGood, p->nCutsBad );
+ printf( "Good cuts = %d. Bad cuts = %d. Cut mem = %d Mb\n",
+ p->nCutsGood, p->nCutsBad, p->nCutMemUsed );
PRT( "Cuts ", p->timeCuts );
PRT( "Eval ", p->timeEval );
PRT( "Other ", p->timeOther );
diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h
new file mode 100644
index 00000000..41d8692d
--- /dev/null
+++ b/src/aig/fra/fra.h
@@ -0,0 +1,196 @@
+/**CFile****************************************************************
+
+ FileName [fra.h]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [[New FRAIG package.]
+
+ Synopsis [External declarations.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 30, 2007.]
+
+ Revision [$Id: fra.h,v 1.00 2007/06/30 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#ifndef __FRA_H__
+#define __FRA_H__
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+////////////////////////////////////////////////////////////////////////
+/// INCLUDES ///
+////////////////////////////////////////////////////////////////////////
+
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include <assert.h>
+#include <time.h>
+
+#include "vec.h"
+#include "dar.h"
+#include "satSolver.h"
+
+////////////////////////////////////////////////////////////////////////
+/// PARAMETERS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// BASIC TYPES ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Fra_Par_t_ Fra_Par_t;
+typedef struct Fra_Man_t_ Fra_Man_t;
+
+// FRAIG parameters
+struct Fra_Par_t_
+{
+ int nSimWords; // the number of words in the simulation info
+ double dSimSatur; // the ratio of refined classes when saturation is reached
+ int fPatScores; // enables simulation pattern scoring
+ int MaxScore; // max score after which resimulation is used
+ double dActConeRatio; // the ratio of cone to be bumped
+ double dActConeBumpMax; // the largest bump in activity
+ int fSpeculate; // use speculative reduction
+ int fProve; // prove the miter outputs
+ int fVerbose; // verbose output
+ int fDoSparse; // skip sparse functions
+ int nBTLimitNode; // conflict limit at a node
+ int nBTLimitMiter; // conflict limit at an output
+};
+
+// FRAIG manager
+struct Fra_Man_t_
+{
+ // high-level data
+ Fra_Par_t * pPars; // parameters governing fraiging
+ // AIG managers
+ Dar_Man_t * pManAig; // the starting AIG manager
+ Dar_Man_t * pManFraig; // the final AIG manager
+ // simulation info
+ unsigned * pSimWords; // memory for simulation information
+ int nSimWords; // the number of simulation words
+ // counter example storage
+ int nPatWords; // the number of words in the counter example
+ unsigned * pPatWords; // the counter example
+ int * pPatScores; // the scores of each pattern
+ // equivalence classes
+ Vec_Ptr_t * vClasses; // equivalence classes
+ Vec_Ptr_t * vClasses1; // equivalence class of Const1 node
+ Vec_Ptr_t * vClassesTemp; // temporary storage for new classes
+ Dar_Obj_t ** pMemClasses; // memory allocated for equivalence classes
+ Dar_Obj_t ** pMemClassesFree; // memory allocated for equivalence classes to be used
+ Vec_Ptr_t * vClassOld; // old equivalence class after splitting
+ Vec_Ptr_t * vClassNew; // new equivalence class(es) after splitting
+ int nPairs; // the number of pairs of nodes
+ // equivalence checking
+ sat_solver * pSat; // SAT solver
+ int nSatVars; // the number of variables currently used
+ Vec_Ptr_t * vPiVars; // the PIs of the cone used
+ sint64 nBTLimitGlobal; // resource limit
+ sint64 nInsLimitGlobal; // resource limit
+ // various data members
+ Dar_Obj_t ** pMemFraig; // memory allocated for points to the fraig nodes
+ Dar_Obj_t ** pMemRepr; // memory allocated for points to the node representatives
+ Vec_Ptr_t ** pMemFanins; // the arrays of fanins
+ int * pMemSatNums; // the array of SAT numbers
+ int nSizeAlloc; // allocated size of the arrays
+ // statistics
+ int nSimRounds;
+ int nNodesMiter;
+ int nClassesZero;
+ int nClassesBeg;
+ int nClassesEnd;
+ int nPairsBeg;
+ int nPairsEnd;
+ int nSatCalls;
+ int nSatCallsSat;
+ int nSatCallsUnsat;
+ int nSatProof;
+ int nSatFails;
+ int nSatFailsReal;
+ // runtime
+ int timeSim;
+ int timeTrav;
+ int timeSat;
+ int timeSatUnsat;
+ int timeSatSat;
+ int timeSatFail;
+ int timeRef;
+ int timeTotal;
+ int time1;
+ int time2;
+};
+
+////////////////////////////////////////////////////////////////////////
+/// MACRO DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+static inline unsigned * Fra_ObjSim( Dar_Obj_t * pObj ) { return ((Fra_Man_t *)pObj->pData)->pSimWords + ((Fra_Man_t *)pObj->pData)->nSimWords * pObj->Id; }
+static inline unsigned Fra_ObjRandomSim() { return (rand() << 24) ^ (rand() << 12) ^ rand(); }
+
+static inline Dar_Obj_t * Fra_ObjFraig( Dar_Obj_t * pObj ) { return ((Fra_Man_t *)pObj->pData)->pMemFraig[pObj->Id]; }
+static inline Dar_Obj_t * Fra_ObjRepr( Dar_Obj_t * pObj ) { return ((Fra_Man_t *)pObj->pData)->pMemRepr[pObj->Id]; }
+static inline Vec_Ptr_t * Fra_ObjFaninVec( Dar_Obj_t * pObj ) { return ((Fra_Man_t *)pObj->pData)->pMemFanins[pObj->Id]; }
+static inline int Fra_ObjSatNum( Dar_Obj_t * pObj ) { return ((Fra_Man_t *)pObj->pData)->pMemSatNums[pObj->Id]; }
+
+static inline Dar_Obj_t * Fra_ObjChild0Fra( Dar_Obj_t * pObj ) { assert( !Dar_IsComplement(pObj) ); return Dar_ObjFanin0(pObj)? Dar_NotCond(Fra_ObjFraig(Dar_ObjFanin0(pObj)), Dar_ObjFaninC0(pObj)) : NULL; }
+static inline Dar_Obj_t * Fra_ObjChild1Fra( Dar_Obj_t * pObj ) { assert( !Dar_IsComplement(pObj) ); return Dar_ObjFanin1(pObj)? Dar_NotCond(Fra_ObjFraig(Dar_ObjFanin1(pObj)), Dar_ObjFaninC1(pObj)) : NULL; }
+
+static inline void Fra_ObjSetFraig( Dar_Obj_t * pObj, Dar_Obj_t * pNode ) { ((Fra_Man_t *)pObj->pData)->pMemFraig[pObj->Id] = pNode; }
+static inline void Fra_ObjSetRepr( Dar_Obj_t * pObj, Dar_Obj_t * pNode ) { ((Fra_Man_t *)pObj->pData)->pMemRepr[pObj->Id] = pNode; }
+static inline void Fra_ObjSetFaninVec( Dar_Obj_t * pObj, Vec_Ptr_t * vFanins ) { ((Fra_Man_t *)pObj->pData)->pMemFanins[pObj->Id] = vFanins; }
+static inline void Fra_ObjSetSatNum( Dar_Obj_t * pObj, int Num ) { ((Fra_Man_t *)pObj->pData)->pMemSatNums[pObj->Id] = Num; }
+
+////////////////////////////////////////////////////////////////////////
+/// ITERATORS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== fraAnd.c ========================================================*/
+extern void Fra_Sweep( Fra_Man_t * p );
+/*=== fraClass.c ========================================================*/
+extern void Fra_CreateClasses( Fra_Man_t * p );
+extern int Fra_RefineClasses( Fra_Man_t * p );
+extern int Fra_RefineClasses1( Fra_Man_t * p );
+/*=== fraCnf.c ========================================================*/
+extern void Fra_NodeAddToSolver( Fra_Man_t * p, Dar_Obj_t * pOld, Dar_Obj_t * pNew );
+/*=== fraCore.c ========================================================*/
+extern Dar_Man_t * Fra_Perform( Dar_Man_t * pManAig, Fra_Par_t * pParams );
+/*=== fraMan.c ========================================================*/
+extern void Fra_ParamsDefault( Fra_Par_t * pParams );
+extern Fra_Man_t * Fra_ManStart( Dar_Man_t * pManAig, Fra_Par_t * pParams );
+extern void Fra_ManStop( Fra_Man_t * p );
+extern void Fra_ManPrint( Fra_Man_t * p );
+/*=== fraSat.c ========================================================*/
+extern int Fra_NodesAreEquiv( Fra_Man_t * p, Dar_Obj_t * pOld, Dar_Obj_t * pNew );
+extern int Fra_NodeIsConst( Fra_Man_t * p, Dar_Obj_t * pNew );
+/*=== fraSim.c ========================================================*/
+extern int Fra_NodeHasZeroSim( Fra_Man_t * p, Dar_Obj_t * pObj );
+extern int Fra_NodeCompareSims( Fra_Man_t * p, Dar_Obj_t * pObj0, Dar_Obj_t * pObj1 );
+extern void Fra_SavePattern( Fra_Man_t * p );
+extern void Fra_Simulate( Fra_Man_t * p );
+extern void Fra_Resimulate( Fra_Man_t * p );
+extern int Fra_CheckOutputSims( Fra_Man_t * p );
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/aig/fra/fraAnd.c b/src/aig/fra/fraAnd.c
new file mode 100644
index 00000000..333ef1b1
--- /dev/null
+++ b/src/aig/fra/fraAnd.c
@@ -0,0 +1,138 @@
+/**CFile****************************************************************
+
+ FileName [fraAnd.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Fraig FRAIG package.]
+
+ Synopsis []
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 30, 2007.]
+
+ Revision [$Id: fraAnd.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "fra.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+
+/**Function*************************************************************
+
+ Synopsis [Performs fraiging for one node.]
+
+ Description [Returns the fraiged node.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Dar_Obj_t * Fra_And( Fra_Man_t * p, Dar_Obj_t * pObjOld )
+{
+ Dar_Obj_t * pObjOldRepr, * pObjFraig, * pFanin0Fraig, * pFanin1Fraig, * pObjOldReprFraig;
+ int RetValue;
+ assert( !Dar_IsComplement(pObjOld) );
+ assert( Dar_ObjIsNode(pObjOld) );
+ // get the fraiged fanins
+ pFanin0Fraig = Fra_ObjChild0Fra(pObjOld);
+ pFanin1Fraig = Fra_ObjChild1Fra(pObjOld);
+ // get the fraiged node
+ pObjFraig = Dar_And( p->pManFraig, pFanin0Fraig, pFanin1Fraig );
+ // get representative of this class
+ pObjOldRepr = Fra_ObjRepr(pObjOld);
+ if ( pObjOldRepr == NULL || // this is a unique node
+ (!p->pPars->fDoSparse && pObjOldRepr == Dar_ManConst1(p->pManAig)) ) // this is a sparse node
+ {
+ assert( Dar_Regular(pFanin0Fraig) != Dar_Regular(pFanin1Fraig) );
+ assert( pObjFraig != Dar_Regular(pFanin0Fraig) );
+ assert( pObjFraig != Dar_Regular(pFanin1Fraig) );
+ return pObjFraig;
+ }
+ // get the fraiged representative
+ pObjOldReprFraig = Fra_ObjFraig(pObjOldRepr);
+ // if the fraiged nodes are the same, return
+ if ( Dar_Regular(pObjFraig) == Dar_Regular(pObjOldReprFraig) )
+ return pObjFraig;
+ assert( Dar_Regular(pObjFraig) != Dar_ManConst1(p->pManFraig) );
+ // if they are proved different, the c-ex will be in p->pPatWords
+ RetValue = Fra_NodesAreEquiv( p, Dar_Regular(pObjOldReprFraig), Dar_Regular(pObjFraig) );
+ if ( RetValue == 1 ) // proved equivalent
+ {
+ pObjOld->fMarkA = 1;
+ return Dar_NotCond( pObjOldReprFraig, pObjOld->fPhase ^ pObjOldRepr->fPhase );
+ }
+ if ( RetValue == -1 ) // failed
+ {
+ if ( !p->pPars->fSpeculate )
+ return pObjFraig;
+ // substitute the node
+ pObjOld->fMarkB = 1;
+ return Dar_NotCond( pObjOldReprFraig, pObjOld->fPhase ^ pObjOldRepr->fPhase );
+ }
+ // simulate the counter-example and return the Fraig node
+ Fra_Resimulate( p );
+ return pObjFraig;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs fraiging for the internal nodes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Fra_Sweep( Fra_Man_t * p )
+{
+ Dar_Obj_t * pObj, * pObjNew;
+ int i, k = 0;
+p->nClassesZero = Vec_PtrSize(p->vClasses1);
+p->nClassesBeg = Vec_PtrSize(p->vClasses);
+ // duplicate internal nodes
+// p->pProgress = Extra_ProgressBarStart( stdout, Dar_ManNodeNum(p->pManAig) );
+ Dar_ManForEachNode( p->pManAig, pObj, i )
+ {
+// Extra_ProgressBarUpdate( p->pProgress, k++, NULL );
+ // default to simple strashing if simulation detected a counter-example for a PO
+ if ( p->pManFraig->pData )
+ pObjNew = Dar_And( p->pManFraig, Fra_ObjChild0Fra(pObj), Fra_ObjChild1Fra(pObj) );
+ else
+ pObjNew = Fra_And( p, pObj ); // pObjNew can be complemented
+ assert( Fra_ObjFraig(pObj) != NULL );
+ Fra_ObjSetFraig( pObj, pObjNew );
+ }
+// Extra_ProgressBarStop( p->pProgress );
+p->nClassesEnd = Vec_PtrSize(p->vClasses);
+ // try to prove the outputs of the miter
+ p->nNodesMiter = Dar_ManNodeNum(p->pManFraig);
+// Fra_MiterStatus( p->pManFraig );
+// if ( p->pPars->fProve && p->pManFraig->pData == NULL )
+// Fra_MiterProve( p );
+ // add the POs
+ Dar_ManForEachPo( p->pManAig, pObj, i )
+ Dar_ObjCreatePo( p->pManFraig, Fra_ObjChild0Fra(pObj) );
+ // remove dangling nodes
+ Dar_ManCleanup( p->pManFraig );
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/fra/fraClass.c b/src/aig/fra/fraClass.c
new file mode 100644
index 00000000..1f2fc165
--- /dev/null
+++ b/src/aig/fra/fraClass.c
@@ -0,0 +1,394 @@
+/**CFile****************************************************************
+
+ FileName [fraClass.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [New FRAIG package.]
+
+ Synopsis []
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 30, 2007.]
+
+ Revision [$Id: fraClass.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "fra.h"
+
+/*
+ The candidate equivalence classes are stored as a vector of pointers
+ to the array of pointers to the nodes in each class.
+ The first node of the class is its representative node.
+ The representative has the smallest topological order among the class nodes.
+ The classes are ordered according to the topological order of their representatives.
+ The array of pointers to the class nodes is terminated with a NULL pointer.
+ To enable dynamic addition of new classes (during class refinement),
+ each array has at least as many NULLs in the end, as there are nodes in the class.
+*/
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Count the number of pairs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Fra_CountPairsClasses( Fra_Man_t * p )
+{
+ Dar_Obj_t ** pClass;
+ int i, nNodes, nPairs = 0;
+ Vec_PtrForEachEntry( p->vClasses, pClass, i )
+ {
+ for ( nNodes = 0; pClass[nNodes]; nNodes++ )
+ {
+ if ( nNodes > DAR_INFINITY )
+ {
+ printf( "Error in equivalence classes.\n" );
+ break;
+ }
+ }
+ nPairs += (nNodes - 1) * (nNodes - 2) / 2;
+ }
+ return nPairs;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes hash value using simulation info.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+unsigned Fra_NodeHash( Fra_Man_t * p, Dar_Obj_t * pObj )
+{
+ static int s_FPrimes[128] = {
+ 1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459,
+ 1499, 1559, 1607, 1657, 1709, 1759, 1823, 1877, 1933, 1997,
+ 2039, 2089, 2141, 2213, 2269, 2311, 2371, 2411, 2467, 2543,
+ 2609, 2663, 2699, 2741, 2797, 2851, 2909, 2969, 3037, 3089,
+ 3169, 3221, 3299, 3331, 3389, 3461, 3517, 3557, 3613, 3671,
+ 3719, 3779, 3847, 3907, 3943, 4013, 4073, 4129, 4201, 4243,
+ 4289, 4363, 4441, 4493, 4549, 4621, 4663, 4729, 4793, 4871,
+ 4933, 4973, 5021, 5087, 5153, 5227, 5281, 5351, 5417, 5471,
+ 5519, 5573, 5651, 5693, 5749, 5821, 5861, 5923, 6011, 6073,
+ 6131, 6199, 6257, 6301, 6353, 6397, 6481, 6563, 6619, 6689,
+ 6737, 6803, 6863, 6917, 6977, 7027, 7109, 7187, 7237, 7309,
+ 7393, 7477, 7523, 7561, 7607, 7681, 7727, 7817, 7877, 7933,
+ 8011, 8039, 8059, 8081, 8093, 8111, 8123, 8147
+ };
+ unsigned * pSims;
+ unsigned uHash;
+ int i;
+ assert( p->nSimWords <= 128 );
+ uHash = 0;
+ pSims = Fra_ObjSim(pObj);
+ for ( i = 0; i < p->nSimWords; i++ )
+ uHash ^= pSims[i] * s_FPrimes[i];
+ return uHash;
+}
+
+/**Function********************************************************************
+
+ Synopsis [Returns the next prime &gt;= p.]
+
+ Description [Copied from CUDD, for stand-aloneness.]
+
+ SideEffects [None]
+
+ SeeAlso []
+
+******************************************************************************/
+unsigned int Cudd_PrimeFra( unsigned int p )
+{
+ int i,pn;
+
+ p--;
+ do {
+ p++;
+ if (p&1) {
+ pn = 1;
+ i = 3;
+ while ((unsigned) (i * i) <= p) {
+ if (p % i == 0) {
+ pn = 0;
+ break;
+ }
+ i += 2;
+ }
+ } else {
+ pn = 0;
+ }
+ } while (!pn);
+ return(p);
+
+} /* end of Cudd_Prime */
+
+
+/**Function*************************************************************
+
+ Synopsis [Creates initial simulation classes.]
+
+ Description [Assumes that simulation info is assigned.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Fra_CreateClasses( Fra_Man_t * p )
+{
+ Dar_Obj_t ** pTable;
+ Dar_Obj_t * pObj;
+ int i, k, k2, nTableSize, nEntries, iEntry;
+ // allocate the table
+ nTableSize = Cudd_PrimeFra( Dar_ManNodeNum(p->pManAig) );
+ pTable = ALLOC( Dar_Obj_t *, nTableSize );
+ memset( pTable, 0, sizeof(Dar_Obj_t *) * nTableSize );
+ // collect nodes into the table
+ Vec_PtrClear( p->vClasses1 );
+ Dar_ManForEachObj( p->pManAig, pObj, i )
+ {
+ if ( !Dar_ObjIsPi(pObj) && !Dar_ObjIsNode(pObj) )
+ continue;
+ // hash the node by its simulation info
+ iEntry = Fra_NodeHash( p, pObj ) % nTableSize;
+ // check if the node belongs to the class of constant 1
+ if ( iEntry == 0 && Fra_NodeHasZeroSim( p, pObj ) )
+ {
+ Vec_PtrPush( p->vClasses1, pObj );
+ continue;
+ }
+ // add the node to the table
+ pObj->pData = pTable[iEntry];
+ pTable[iEntry] = pObj;
+ }
+ // count the total number of nodes in the non-trivial classes
+ nEntries = 0;
+ for ( i = 0; i < nTableSize; i++ )
+ if ( pTable[i] && pTable[i]->pData )
+ {
+ k = 0;
+ for ( pObj = pTable[i]; pObj; pObj = pObj->pData )
+ k++;
+ nEntries += 2*k;
+ }
+ // allocate room for classes
+ p->pMemClasses = ALLOC( Dar_Obj_t *, nEntries + 2*Vec_PtrSize(p->vClasses1) );
+ p->pMemClassesFree = p->pMemClasses + nEntries;
+ // copy the entries into storage
+ Vec_PtrClear( p->vClasses );
+ nEntries = 0;
+ for ( i = 0; i < nTableSize; i++ )
+ if ( pTable[i] && pTable[i]->pData )
+ {
+ k = 0;
+ for ( pObj = pTable[i]; pObj; pObj = pObj->pData )
+ k++;
+ // write entries in the topological order
+ k2 = k;
+ for ( pObj = pTable[i]; pObj; pObj = pObj->pData )
+ {
+ k2--;
+ p->pMemClasses[nEntries+k2] = pObj;
+ p->pMemClasses[nEntries+k+k2] = NULL;
+ }
+ assert( k2 == 0 );
+ Vec_PtrPush( p->vClasses, p->pMemClasses + nEntries );
+ nEntries += 2*k;
+ }
+ free( pTable );
+ // now it is time to refine the classes
+ Fra_RefineClasses( p );
+ // set the pointer to the manager
+ Dar_ManForEachObj( p->pManAig, pObj, i )
+ pObj->pData = p->pManAig;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Refines one class using simulation info.]
+
+ Description [Returns the new class if refinement happened.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Dar_Obj_t ** Fra_RefineClassOne( Fra_Man_t * p, Dar_Obj_t ** pClass )
+{
+ Dar_Obj_t * pObj;
+ int i;
+ assert( pClass[1] != NULL );
+ // check if the class is going to be refined
+ for ( pObj = pClass[1]; pObj; pObj++ )
+ if ( !Fra_NodeCompareSims(p, pClass[0], pObj) )
+ break;
+ if ( pObj == NULL )
+ return NULL;
+ // split the class
+ Vec_PtrClear( p->vClassOld );
+ Vec_PtrClear( p->vClassNew );
+ Vec_PtrPush( p->vClassOld, pClass[0] );
+ for ( pObj = pClass[1]; pObj; pObj++ )
+ if ( Fra_NodeCompareSims(p, pClass[0], pObj) )
+ Vec_PtrPush( p->vClassOld, pObj );
+ else
+ Vec_PtrPush( p->vClassNew, pObj );
+ // put the nodes back into the class memory
+ Vec_PtrForEachEntry( p->vClassOld, pObj, i )
+ {
+ pClass[i] = pObj;
+ pClass[Vec_PtrSize(p->vClassOld)+i] = NULL;
+ }
+ pClass += 2*Vec_PtrSize(p->vClassOld);
+ // put the new nodes into the class memory
+ Vec_PtrForEachEntry( p->vClassNew, pObj, i )
+ {
+ pClass[i] = pObj;
+ pClass[Vec_PtrSize(p->vClassNew)+i] = NULL;
+ }
+ return pClass;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Iteratively refines the classes after simulation.]
+
+ Description [Returns the number of refinements performed.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Fra_RefineClassLastIter( Fra_Man_t * p, Vec_Ptr_t * vClasses )
+{
+ Dar_Obj_t ** pClass, ** pClass2;
+ int nRefis;
+ pClass = Vec_PtrEntryLast( vClasses );
+ for ( nRefis = 0; pClass2 = Fra_RefineClassOne( p, pClass ); nRefis++ )
+ {
+ // if the original class is trivial, remove it
+ if ( pClass[1] == NULL )
+ Vec_PtrPop( vClasses );
+ // if the new class is trivial, stop
+ if ( pClass2[1] == NULL )
+ break;
+ // othewise, add the class and continue
+ Vec_PtrPush( vClasses, pClass2 );
+ pClass = pClass2;
+ }
+ return nRefis;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Refines the classes after simulation.]
+
+ Description [Assumes that simulation info is assigned. Returns the
+ number of classes refined.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Fra_RefineClasses( Fra_Man_t * p )
+{
+ Vec_Ptr_t * vTemp;
+ Dar_Obj_t ** pClass;
+ int clk, i, nRefis = 0;
+ // check if some outputs already became non-constant
+ // this is a special case when computation can be stopped!!!
+ if ( p->pPars->fProve )
+ Fra_CheckOutputSims( p );
+ if ( p->pManFraig->pData )
+ return 0;
+ // refine the classes
+clk = clock();
+ Vec_PtrClear( p->vClassesTemp );
+ Vec_PtrForEachEntry( p->vClasses, pClass, i )
+ {
+ // add the class to the new array
+ Vec_PtrPush( p->vClassesTemp, pClass );
+ // refine the class interatively
+ nRefis += Fra_RefineClassLastIter( p, p->vClassesTemp );
+ }
+ // exchange the class representation
+ vTemp = p->vClassesTemp;
+ p->vClassesTemp = p->vClasses;
+ p->vClasses = vTemp;
+p->timeRef += clock() - clk;
+ return nRefis;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Refines constant 1 equivalence class.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Fra_RefineClasses1( Fra_Man_t * p )
+{
+ Dar_Obj_t * pObj, ** pClass;
+ int i, k;
+ // collect all the nodes to be refined
+ Vec_PtrClear( p->vClassNew );
+ k = 0;
+ Vec_PtrForEachEntry( p->vClasses1, pObj, i )
+ {
+ if ( Fra_NodeHasZeroSim( p, pObj ) )
+ Vec_PtrWriteEntry( p->vClasses1, k++, pObj );
+ else
+ Vec_PtrPush( p->vClassNew, pObj );
+ }
+ Vec_PtrShrink( p->vClasses1, k );
+ if ( Vec_PtrSize(p->vClassNew) == 0 )
+ return 0;
+ if ( Vec_PtrSize(p->vClassNew) == 1 )
+ return 1;
+ // create a new class composed of these nodes
+ pClass = p->pMemClassesFree;
+ p->pMemClassesFree += 2 * Vec_PtrSize(p->vClassNew);
+ Vec_PtrForEachEntry( p->vClassNew, pObj, i )
+ {
+ pClass[i] = pObj;
+ pClass[Vec_PtrSize(p->vClassNew)+i] = NULL;
+ }
+ Vec_PtrPush( p->vClasses, pClass );
+ // iteratively refine this class
+ return 1 + Fra_RefineClassLastIter( p, p->vClasses );
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/fra/fraCnf.c b/src/aig/fra/fraCnf.c
new file mode 100644
index 00000000..18a5ceb6
--- /dev/null
+++ b/src/aig/fra/fraCnf.c
@@ -0,0 +1,285 @@
+/**CFile****************************************************************
+
+ FileName [fraCnf.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [New FRAIG package.]
+
+ Synopsis []
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 30, 2007.]
+
+ Revision [$Id: fraCnf.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "fra.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+
+/**Function*************************************************************
+
+ Synopsis [Addes clauses to the solver.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Fra_AddClausesMux( Fra_Man_t * p, Dar_Obj_t * pNode )
+{
+ Dar_Obj_t * pNodeI, * pNodeT, * pNodeE;
+ int pLits[4], RetValue, VarF, VarI, VarT, VarE, fCompT, fCompE;
+
+ assert( !Dar_IsComplement( pNode ) );
+ assert( Dar_ObjIsMuxType( pNode ) );
+ // get nodes (I = if, T = then, E = else)
+ pNodeI = Dar_ObjRecognizeMux( pNode, &pNodeT, &pNodeE );
+ // get the variable numbers
+ VarF = Fra_ObjSatNum(pNode);
+ VarI = Fra_ObjSatNum(pNodeI);
+ VarT = Fra_ObjSatNum(Dar_Regular(pNodeT));
+ VarE = Fra_ObjSatNum(Dar_Regular(pNodeE));
+ // get the complementation flags
+ fCompT = Dar_IsComplement(pNodeT);
+ fCompE = Dar_IsComplement(pNodeE);
+
+ // f = ITE(i, t, e)
+
+ // i' + t' + f
+ // i' + t + f'
+ // i + e' + f
+ // i + e + f'
+
+ // create four clauses
+ pLits[0] = toLitCond(VarI, 1);
+ pLits[1] = toLitCond(VarT, 1^fCompT);
+ pLits[2] = toLitCond(VarF, 0);
+ RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
+ assert( RetValue );
+ pLits[0] = toLitCond(VarI, 1);
+ pLits[1] = toLitCond(VarT, 0^fCompT);
+ pLits[2] = toLitCond(VarF, 1);
+ RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
+ assert( RetValue );
+ pLits[0] = toLitCond(VarI, 0);
+ pLits[1] = toLitCond(VarE, 1^fCompE);
+ pLits[2] = toLitCond(VarF, 0);
+ RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
+ assert( RetValue );
+ pLits[0] = toLitCond(VarI, 0);
+ pLits[1] = toLitCond(VarE, 0^fCompE);
+ pLits[2] = toLitCond(VarF, 1);
+ RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
+ assert( RetValue );
+
+ // two additional clauses
+ // t' & e' -> f'
+ // t & e -> f
+
+ // t + e + f'
+ // t' + e' + f
+
+ if ( VarT == VarE )
+ {
+// assert( fCompT == !fCompE );
+ return;
+ }
+
+ pLits[0] = toLitCond(VarT, 0^fCompT);
+ pLits[1] = toLitCond(VarE, 0^fCompE);
+ pLits[2] = toLitCond(VarF, 1);
+ RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
+ assert( RetValue );
+ pLits[0] = toLitCond(VarT, 1^fCompT);
+ pLits[1] = toLitCond(VarE, 1^fCompE);
+ pLits[2] = toLitCond(VarF, 0);
+ RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
+ assert( RetValue );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Addes clauses to the solver.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Fra_AddClausesSuper( Fra_Man_t * p, Dar_Obj_t * pNode, Vec_Ptr_t * vSuper )
+{
+ Dar_Obj_t * pFanin;
+ int * pLits, nLits, RetValue, i;
+ assert( !Dar_IsComplement(pNode) );
+ assert( Dar_ObjIsNode( pNode ) );
+ // create storage for literals
+ nLits = Vec_PtrSize(vSuper) + 1;
+ pLits = ALLOC( int, nLits );
+ // suppose AND-gate is A & B = C
+ // add !A => !C or A + !C
+ Vec_PtrForEachEntry( vSuper, pFanin, i )
+ {
+ pLits[0] = toLitCond(Fra_ObjSatNum(Dar_Regular(pFanin)), Dar_IsComplement(pFanin));
+ pLits[1] = toLitCond(Fra_ObjSatNum(pNode), 1);
+ RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
+ assert( RetValue );
+ }
+ // add A & B => C or !A + !B + C
+ Vec_PtrForEachEntry( vSuper, pFanin, i )
+ pLits[i] = toLitCond(Fra_ObjSatNum(Dar_Regular(pFanin)), !Dar_IsComplement(pFanin));
+ pLits[nLits-1] = toLitCond(Fra_ObjSatNum(pNode), 0);
+ RetValue = sat_solver_addclause( p->pSat, pLits, pLits + nLits );
+ assert( RetValue );
+ free( pLits );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Collects the supergate.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Fra_CollectSuper_rec( Dar_Obj_t * pObj, Vec_Ptr_t * vSuper, int fFirst, int fUseMuxes )
+{
+ // if the new node is complemented or a PI, another gate begins
+ if ( Dar_IsComplement(pObj) || Dar_ObjIsPi(pObj) || (!fFirst && Dar_ObjRefs(pObj) > 1) ||
+ (fUseMuxes && Dar_ObjIsMuxType(pObj)) )
+ {
+ Vec_PtrPushUnique( vSuper, pObj );
+ return;
+ }
+ // go through the branches
+ Fra_CollectSuper_rec( Dar_ObjChild0(pObj), vSuper, 0, fUseMuxes );
+ Fra_CollectSuper_rec( Dar_ObjChild1(pObj), vSuper, 0, fUseMuxes );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Collects the supergate.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Ptr_t * Fra_CollectSuper( Dar_Obj_t * pObj, int fUseMuxes )
+{
+ Vec_Ptr_t * vSuper;
+ assert( !Dar_IsComplement(pObj) );
+ assert( !Dar_ObjIsPi(pObj) );
+ vSuper = Vec_PtrAlloc( 4 );
+ Fra_CollectSuper_rec( pObj, vSuper, 1, fUseMuxes );
+ return vSuper;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Updates the solver clause database.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Fra_ObjAddToFrontier( Fra_Man_t * p, Dar_Obj_t * pObj, Vec_Ptr_t * vFrontier )
+{
+ assert( !Dar_IsComplement(pObj) );
+ if ( Fra_ObjSatNum(pObj) )
+ return;
+ assert( Fra_ObjSatNum(pObj) == 0 );
+ assert( Fra_ObjFaninVec(pObj) == NULL );
+ if ( Dar_ObjIsConst1(pObj) )
+ return;
+//printf( "Assigning node %d number %d\n", pObj->Id, p->nSatVars );
+ Fra_ObjSetSatNum( pObj, p->nSatVars++ );
+ if ( Dar_ObjIsNode(pObj) )
+ Vec_PtrPush( vFrontier, pObj );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Updates the solver clause database.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Fra_NodeAddToSolver( Fra_Man_t * p, Dar_Obj_t * pOld, Dar_Obj_t * pNew )
+{
+ Vec_Ptr_t * vFrontier, * vFanins;
+ Dar_Obj_t * pNode, * pFanin;
+ int i, k, fUseMuxes = 1;
+ assert( pOld || pNew );
+ // quit if CNF is ready
+ if ( (!pOld || Fra_ObjFaninVec(pOld)) && (!pNew || Fra_ObjFaninVec(pNew)) )
+ return;
+ // start the frontier
+ vFrontier = Vec_PtrAlloc( 100 );
+ if ( pOld ) Fra_ObjAddToFrontier( p, pOld, vFrontier );
+ if ( pNew ) Fra_ObjAddToFrontier( p, pNew, vFrontier );
+ // explore nodes in the frontier
+ Vec_PtrForEachEntry( vFrontier, pNode, i )
+ {
+ // create the supergate
+ assert( Fra_ObjSatNum(pNode) );
+ assert( Fra_ObjFaninVec(pNode) == NULL );
+ if ( fUseMuxes && Dar_ObjIsMuxType(pNode) )
+ {
+ vFanins = Vec_PtrAlloc( 4 );
+ Vec_PtrPushUnique( vFanins, Dar_ObjFanin0( Dar_ObjFanin0(pNode) ) );
+ Vec_PtrPushUnique( vFanins, Dar_ObjFanin0( Dar_ObjFanin1(pNode) ) );
+ Vec_PtrPushUnique( vFanins, Dar_ObjFanin1( Dar_ObjFanin0(pNode) ) );
+ Vec_PtrPushUnique( vFanins, Dar_ObjFanin1( Dar_ObjFanin1(pNode) ) );
+ Vec_PtrForEachEntry( vFanins, pFanin, k )
+ Fra_ObjAddToFrontier( p, Dar_Regular(pFanin), vFrontier );
+ Fra_AddClausesMux( p, pNode );
+ }
+ else
+ {
+ vFanins = Fra_CollectSuper( pNode, fUseMuxes );
+ Vec_PtrForEachEntry( vFanins, pFanin, k )
+ Fra_ObjAddToFrontier( p, Dar_Regular(pFanin), vFrontier );
+ Fra_AddClausesSuper( p, pNode, vFanins );
+ }
+ assert( Vec_PtrSize(vFanins) > 1 );
+ Fra_ObjSetFaninVec( pNode, vFanins );
+ }
+ Vec_PtrFree( vFrontier );
+}
+
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/fra/fraCore.c b/src/aig/fra/fraCore.c
new file mode 100644
index 00000000..7fdd1b83
--- /dev/null
+++ b/src/aig/fra/fraCore.c
@@ -0,0 +1,64 @@
+/**CFile****************************************************************
+
+ FileName [fraCore.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [New FRAIG package.]
+
+ Synopsis []
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 30, 2007.]
+
+ Revision [$Id: fraCore.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "fra.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Performs fraiging of the AIG.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Dar_Man_t * Fra_Perform( Dar_Man_t * pManAig, Fra_Par_t * pPars )
+{
+ Fra_Man_t * p;
+ Dar_Man_t * pManAigNew;
+ int clk;
+ if ( Dar_ManNodeNum(pManAig) == 0 )
+ return Dar_ManDup(pManAig);
+clk = clock();
+ assert( Dar_ManLatchNum(pManAig) == 0 );
+ p = Fra_ManStart( pManAig, pPars );
+ Fra_Simulate( p );
+ Fra_Sweep( p );
+ pManAigNew = p->pManFraig;
+p->timeTotal = clock() - clk;
+ Fra_ManStop( p );
+ return pManAigNew;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/fra/fraMan.c b/src/aig/fra/fraMan.c
new file mode 100644
index 00000000..cccd1d75
--- /dev/null
+++ b/src/aig/fra/fraMan.c
@@ -0,0 +1,188 @@
+/**CFile****************************************************************
+
+ FileName [fraMan.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [New FRAIG package.]
+
+ Synopsis [Starts the FRAIG manager.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 30, 2007.]
+
+ Revision [$Id: fraMan.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "fra.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Sets the default solving parameters.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Fra_ParamsDefault( Fra_Par_t * pPars )
+{
+ memset( pPars, 0, sizeof(Fra_Par_t) );
+ pPars->nSimWords = 32; // the number of words in the simulation info
+ pPars->dSimSatur = 0.005; // the ratio of refined classes when saturation is reached
+ pPars->fPatScores = 0; // enables simulation pattern scoring
+ pPars->MaxScore = 25; // max score after which resimulation is used
+ pPars->fDoSparse = 1; // skips sparse functions
+// pPars->dActConeRatio = 0.05; // the ratio of cone to be bumped
+// pPars->dActConeBumpMax = 5.0; // the largest bump of activity
+ pPars->dActConeRatio = 0.3; // the ratio of cone to be bumped
+ pPars->dActConeBumpMax = 10.0; // the largest bump of activity
+ pPars->nBTLimitNode = 100; // conflict limit at a node
+ pPars->nBTLimitMiter = 500000; // conflict limit at an output
+}
+
+/**Function*************************************************************
+
+ Synopsis [Starts the fraiging manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Fra_Man_t * Fra_ManStart( Dar_Man_t * pManAig, Fra_Par_t * pPars )
+{
+ Fra_Man_t * p;
+ Dar_Obj_t * pObj;
+ int i;
+ // allocate the fraiging manager
+ p = ALLOC( Fra_Man_t, 1 );
+ memset( p, 0, sizeof(Fra_Man_t) );
+ p->pPars = pPars;
+ p->pManAig = pManAig;
+ p->pManFraig = Dar_ManStartFrom( pManAig );
+ assert( Dar_ManPiNum(p->pManAig) == Dar_ManPiNum(p->pManFraig) );
+ // allocate simulation info
+ p->nSimWords = pPars->nSimWords;
+ p->pSimWords = ALLOC( unsigned, (Dar_ManObjIdMax(pManAig) + 1) * p->nSimWords );
+ // clean simulation info of the constant node
+ memset( p->pSimWords, 0, p->nSimWords * sizeof(unsigned) );
+ // allocate storage for sim pattern
+ p->nPatWords = Dar_BitWordNum( Dar_ManPiNum(pManAig) );
+ p->pPatWords = ALLOC( unsigned, p->nPatWords );
+ p->pPatScores = ALLOC( int, 32 * p->nSimWords );
+ p->vPiVars = Vec_PtrAlloc( 100 );
+ p->vClasses = Vec_PtrAlloc( 100 );
+ // allocate other members
+ p->nSizeAlloc = Dar_ManObjIdMax(pManAig) + 1;
+ p->pMemFraig = ALLOC( Dar_Obj_t *, p->nSizeAlloc );
+ memset( p->pMemFraig, 0, p->nSizeAlloc * sizeof(Dar_Obj_t *) );
+ p->pMemRepr = ALLOC( Dar_Obj_t *, p->nSizeAlloc );
+ memset( p->pMemRepr, 0, p->nSizeAlloc * sizeof(Dar_Obj_t *) );
+ p->pMemFanins = ALLOC( Vec_Ptr_t *, p->nSizeAlloc );
+ memset( p->pMemFanins, 0, p->nSizeAlloc * sizeof(Vec_Ptr_t *) );
+ p->pMemSatNums = ALLOC( int, p->nSizeAlloc );
+ memset( p->pMemSatNums, 0xff, p->nSizeAlloc * sizeof(int) );
+ // set the pointers to the available fraig nodes
+ Fra_ObjSetFraig( Dar_ManConst1(p->pManAig), Dar_ManConst1(p->pManFraig) );
+ Dar_ManForEachPi( p->pManAig, pObj, i )
+ Fra_ObjSetFraig( pObj, Dar_ManPi(p->pManFraig, i) );
+ // set the pointers to the manager
+ Dar_ManForEachObj( p->pManFraig, pObj, i )
+ pObj->pData = p->pManFraig;
+ // set random number generator
+ srand( 0xABCABC );
+ return p;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Stops the fraiging manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Fra_ManStop( Fra_Man_t * p )
+{
+ int i;
+ for ( i = 0; i < p->nSizeAlloc; i++ )
+ if ( p->pMemFanins[i] )
+ Vec_PtrFree( p->pMemFanins[i] );
+ if ( p->pPars->fVerbose )
+ Fra_ManPrint( p );
+ if ( p->vClassesTemp ) Vec_PtrFree( p->vClassesTemp );
+ if ( p->vClassNew ) Vec_PtrFree( p->vClassNew );
+ if ( p->vClassOld ) Vec_PtrFree( p->vClassOld );
+ if ( p->vClasses1 ) Vec_PtrFree( p->vClasses1 );
+ if ( p->vClasses ) Vec_PtrFree( p->vClasses );
+ if ( p->vPiVars ) Vec_PtrFree( p->vPiVars );
+ if ( p->pSat ) sat_solver_delete( p->pSat );
+ FREE( p->pMemSatNums );
+ FREE( p->pMemFanins );
+ FREE( p->pMemRepr );
+ FREE( p->pMemFraig );
+ FREE( p->pMemClasses );
+ FREE( p->pPatScores );
+ FREE( p->pPatWords );
+ FREE( p->pSimWords );
+ free( p );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Prints stats for the fraiging manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Fra_ManPrint( Fra_Man_t * p )
+{
+ double nMemory = 1.0*Dar_ManObjIdMax(p->pManAig)*((p->nSimWords+2)*sizeof(unsigned)+6*sizeof(void*))/(1<<20);
+ printf( "SimWords = %d. Rounds = %d. Mem = %0.2f Mb. ", p->nSimWords, p->nSimRounds, nMemory );
+ printf( "Classes: Beg = %d. End = %d.\n", p->nClassesBeg, p->nClassesEnd );
+ printf( "Limits: BTNode = %d. BTMiter = %d.\n", p->pPars->nBTLimitNode, p->pPars->nBTLimitMiter );
+ printf( "Proof = %d. Counter-example = %d. Fail = %d. FailReal = %d. Zero = %d.\n",
+ p->nSatProof, p->nSatCallsSat, p->nSatFails, p->nSatFailsReal, p->nClassesZero );
+ printf( "Final = %d. Miter = %d. Total = %d. Mux = %d. (Exor = %d.) SatVars = %d.\n",
+ Dar_ManNodeNum(p->pManFraig), p->nNodesMiter, Dar_ManNodeNum(p->pManAig), 0, 0, p->nSatVars );
+ if ( p->pSat ) Sat_SolverPrintStats( stdout, p->pSat );
+ PRT( "AIG simulation ", p->timeSim );
+ PRT( "AIG traversal ", p->timeTrav );
+ PRT( "SAT solving ", p->timeSat );
+ PRT( " Unsat ", p->timeSatUnsat );
+ PRT( " Sat ", p->timeSatSat );
+ PRT( " Fail ", p->timeSatFail );
+ PRT( "Class refining ", p->timeRef );
+ PRT( "TOTAL RUNTIME ", p->timeTotal );
+ if ( p->time1 ) { PRT( "time1 ", p->time1 ); }
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/fra/fraSat.c b/src/aig/fra/fraSat.c
new file mode 100644
index 00000000..1c72c807
--- /dev/null
+++ b/src/aig/fra/fraSat.c
@@ -0,0 +1,328 @@
+/**CFile****************************************************************
+
+ FileName [fraSat.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [New FRAIG package.]
+
+ Synopsis []
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 30, 2007.]
+
+ Revision [$Id: fraSat.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "fra.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+static int Fra_SetActivityFactors( Fra_Man_t * p, Dar_Obj_t * pOld, Dar_Obj_t * pNew );
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Runs equivalence test for the two nodes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Fra_NodesAreEquiv( Fra_Man_t * p, Dar_Obj_t * pOld, Dar_Obj_t * pNew )
+{
+ int pLits[4], RetValue, RetValue1, nBTLimit, clk, clk2 = clock();
+
+ // make sure the nodes are not complemented
+ assert( !Dar_IsComplement(pNew) );
+ assert( !Dar_IsComplement(pOld) );
+ assert( pNew != pOld );
+
+ // if at least one of the nodes is a failed node, perform adjustments:
+ // if the backtrack limit is small, simply skip this node
+ // if the backtrack limit is > 10, take the quare root of the limit
+ nBTLimit = p->pPars->nBTLimitNode;
+/*
+ if ( nBTLimit > 0 && (pOld->fFailTfo || pNew->fFailTfo) )
+ {
+ p->nSatFails++;
+ // fail immediately
+// return -1;
+ if ( nBTLimit <= 10 )
+ return -1;
+ nBTLimit = (int)pow(nBTLimit, 0.7);
+ }
+*/
+ p->nSatCalls++;
+
+ // make sure the solver is allocated and has enough variables
+ if ( p->pSat == NULL )
+ {
+ p->pSat = sat_solver_new();
+ p->nSatVars = 1;
+ sat_solver_setnvars( p->pSat, 1000 );
+ }
+
+ // if the nodes do not have SAT variables, allocate them
+ Fra_NodeAddToSolver( p, pOld, pNew );
+
+ // prepare variable activity
+ Fra_SetActivityFactors( p, pOld, pNew );
+
+ // solve under assumptions
+ // A = 1; B = 0 OR A = 1; B = 1
+clk = clock();
+ pLits[0] = toLitCond( Fra_ObjSatNum(pOld), 0 );
+ pLits[1] = toLitCond( Fra_ObjSatNum(pNew), pOld->fPhase == pNew->fPhase );
+//Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 );
+ RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2,
+ (sint64)nBTLimit, (sint64)0,
+ p->nBTLimitGlobal, p->nInsLimitGlobal );
+p->timeSat += clock() - clk;
+ if ( RetValue1 == l_False )
+ {
+p->timeSatUnsat += clock() - clk;
+ pLits[0] = lit_neg( pLits[0] );
+ pLits[1] = lit_neg( pLits[1] );
+ RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
+ assert( RetValue );
+ // continue solving the other implication
+ p->nSatCallsUnsat++;
+ }
+ else if ( RetValue1 == l_True )
+ {
+p->timeSatSat += clock() - clk;
+ Fra_SavePattern( p );
+ p->nSatCallsSat++;
+ return 0;
+ }
+ else // if ( RetValue1 == l_Undef )
+ {
+p->timeSatFail += clock() - clk;
+ // mark the node as the failed node
+// if ( pOld != p->pManFraig->pConst1 )
+// pOld->fFailTfo = 1;
+// pNew->fFailTfo = 1;
+ p->nSatFailsReal++;
+ return -1;
+ }
+
+ // if the old node was constant 0, we already know the answer
+ if ( pOld == p->pManFraig->pConst1 )
+ {
+ p->nSatProof++;
+ return 1;
+ }
+
+ // solve under assumptions
+ // A = 0; B = 1 OR A = 0; B = 0
+clk = clock();
+ pLits[0] = toLitCond( Fra_ObjSatNum(pOld), 1 );
+ pLits[1] = toLitCond( Fra_ObjSatNum(pNew), pOld->fPhase ^ pNew->fPhase );
+ RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2,
+ (sint64)nBTLimit, (sint64)0,
+ p->nBTLimitGlobal, p->nInsLimitGlobal );
+p->timeSat += clock() - clk;
+ if ( RetValue1 == l_False )
+ {
+p->timeSatUnsat += clock() - clk;
+ pLits[0] = lit_neg( pLits[0] );
+ pLits[1] = lit_neg( pLits[1] );
+ RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
+ assert( RetValue );
+ p->nSatCallsUnsat++;
+ }
+ else if ( RetValue1 == l_True )
+ {
+p->timeSatSat += clock() - clk;
+ Fra_SavePattern( p );
+ p->nSatCallsSat++;
+ return 0;
+ }
+ else // if ( RetValue1 == l_Undef )
+ {
+p->timeSatFail += clock() - clk;
+ // mark the node as the failed node
+// pOld->fFailTfo = 1;
+// pNew->fFailTfo = 1;
+ p->nSatFailsReal++;
+ return -1;
+ }
+/*
+ // check BDD proof
+ {
+ int RetVal;
+ PRT( "Sat", clock() - clk2 );
+ clk2 = clock();
+ RetVal = Fra_NodesAreEquivBdd( pOld, pNew );
+// printf( "%d ", RetVal );
+ assert( RetVal );
+ PRT( "Bdd", clock() - clk2 );
+ printf( "\n" );
+ }
+*/
+ // return SAT proof
+ p->nSatProof++;
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Runs equivalence test for one node.]
+
+ Description [Returns the fraiged node.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Fra_NodeIsConst( Fra_Man_t * p, Dar_Obj_t * pNew )
+{
+ int pLits[2], RetValue1, RetValue, clk;
+
+ // make sure the nodes are not complemented
+ assert( !Dar_IsComplement(pNew) );
+ assert( pNew != p->pManFraig->pConst1 );
+ p->nSatCalls++;
+
+ // make sure the solver is allocated and has enough variables
+ if ( p->pSat == NULL )
+ {
+ p->pSat = sat_solver_new();
+ p->nSatVars = 1;
+ sat_solver_setnvars( p->pSat, 1000 );
+ }
+
+ // if the nodes do not have SAT variables, allocate them
+ Fra_NodeAddToSolver( p, NULL, pNew );
+
+ // prepare variable activity
+ Fra_SetActivityFactors( p, NULL, pNew );
+
+ // solve under assumptions
+clk = clock();
+ pLits[0] = toLitCond( Fra_ObjSatNum(pNew), pNew->fPhase );
+ RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 1,
+ (sint64)p->pPars->nBTLimitMiter, (sint64)0,
+ p->nBTLimitGlobal, p->nInsLimitGlobal );
+p->timeSat += clock() - clk;
+ if ( RetValue1 == l_False )
+ {
+p->timeSatUnsat += clock() - clk;
+ pLits[0] = lit_neg( pLits[0] );
+ RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 1 );
+ assert( RetValue );
+ // continue solving the other implication
+ p->nSatCallsUnsat++;
+ }
+ else if ( RetValue1 == l_True )
+ {
+p->timeSatSat += clock() - clk;
+ if ( p->pPatWords )
+ Fra_SavePattern( p );
+ p->nSatCallsSat++;
+ return 0;
+ }
+ else // if ( RetValue1 == l_Undef )
+ {
+p->timeSatFail += clock() - clk;
+ // mark the node as the failed node
+// pNew->fFailTfo = 1;
+ p->nSatFailsReal++;
+ return -1;
+ }
+
+ // return SAT proof
+ p->nSatProof++;
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Sets variable activities in the cone.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Fra_SetActivityFactors_rec( Fra_Man_t * p, Dar_Obj_t * pObj, int LevelMin, int LevelMax )
+{
+ Vec_Ptr_t * vFanins;
+ Dar_Obj_t * pFanin;
+ int i, Counter = 0;
+ assert( !Dar_IsComplement(pObj) );
+ assert( Fra_ObjSatNum(pObj) );
+ // skip visited variables
+ if ( Dar_ObjIsTravIdCurrent(p->pManFraig, pObj) )
+ return 0;
+ Dar_ObjSetTravIdCurrent(p->pManFraig, pObj);
+ // add the PI to the list
+ if ( pObj->Level <= (unsigned)LevelMin || Dar_ObjIsPi(pObj) )
+ return 0;
+ // set the factor of this variable
+ // (LevelMax-LevelMin) / (pObj->Level-LevelMin) = p->pPars->dActConeBumpMax / ThisBump
+ p->pSat->factors[Fra_ObjSatNum(pObj)] = p->pPars->dActConeBumpMax * (pObj->Level - LevelMin)/(LevelMax - LevelMin);
+ veci_push(&p->pSat->act_vars, Fra_ObjSatNum(pObj));
+ // explore the fanins
+ vFanins = Fra_ObjFaninVec( pObj );
+ Vec_PtrForEachEntry( vFanins, pFanin, i )
+ Counter += Fra_SetActivityFactors_rec( p, Dar_Regular(pFanin), LevelMin, LevelMax );
+ return 1 + Counter;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Sets variable activities in the cone.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Fra_SetActivityFactors( Fra_Man_t * p, Dar_Obj_t * pOld, Dar_Obj_t * pNew )
+{
+ int clk, LevelMin, LevelMax;
+ assert( pOld || pNew );
+clk = clock();
+ // reset the active variables
+ veci_resize(&p->pSat->act_vars, 0);
+ // prepare for traversal
+ Dar_ManIncrementTravId( p->pManFraig );
+ // determine the min and max level to visit
+ assert( p->pPars->dActConeRatio > 0 && p->pPars->dActConeRatio < 1 );
+ LevelMax = DAR_MAX( (pNew ? pNew->Level : 0), (pOld ? pOld->Level : 0) );
+ LevelMin = (int)(LevelMax * (1.0 - p->pPars->dActConeRatio));
+ // traverse
+ if ( pOld && !Dar_ObjIsConst1(pOld) )
+ Fra_SetActivityFactors_rec( p, pOld, LevelMin, LevelMax );
+ if ( pNew && !Dar_ObjIsConst1(pNew) )
+ Fra_SetActivityFactors_rec( p, pNew, LevelMin, LevelMax );
+//Fra_PrintActivity( p );
+p->timeTrav += clock() - clk;
+ return 1;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/fra/fraSim.c b/src/aig/fra/fraSim.c
new file mode 100644
index 00000000..e8b88159
--- /dev/null
+++ b/src/aig/fra/fraSim.c
@@ -0,0 +1,599 @@
+/**CFile****************************************************************
+
+ FileName [fraSim.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [New FRAIG package.]
+
+ Synopsis []
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 30, 2007.]
+
+ Revision [$Id: fraSim.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "fra.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Assigns random patterns to the PI node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Fra_NodeAssignRandom( Fra_Man_t * p, Dar_Obj_t * pObj )
+{
+ unsigned * pSims;
+ int i;
+ assert( Dar_ObjIsPi(pObj) );
+ pSims = Fra_ObjSim(pObj);
+ for ( i = 0; i < p->nSimWords; i++ )
+ pSims[i] = Fra_ObjRandomSim();
+}
+
+/**Function*************************************************************
+
+ Synopsis [Assigns constant patterns to the PI node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Fra_NodeAssignConst( Fra_Man_t * p, Dar_Obj_t * pObj, int fConst1 )
+{
+ unsigned * pSims;
+ int i;
+ assert( Dar_ObjIsPi(pObj) );
+ pSims = Fra_ObjSim(pObj);
+ for ( i = 0; i < p->nSimWords; i++ )
+ pSims[i] = fConst1? ~(unsigned)0 : 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Assings random simulation info for the PIs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Fra_AssignRandom( Fra_Man_t * p )
+{
+ Dar_Obj_t * pObj;
+ int i;
+ Dar_ManForEachPi( p->pManAig, pObj, i )
+ Fra_NodeAssignRandom( p, pObj );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Assings distance-1 simulation info for the PIs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Fra_AssignDist1( Fra_Man_t * p, unsigned * pPat )
+{
+ Dar_Obj_t * pObj;
+ int i, Limit;
+ Dar_ManForEachPi( p->pManAig, pObj, i )
+ Fra_NodeAssignConst( p, pObj, Dar_InfoHasBit(pPat, i) );
+ Limit = DAR_MIN( Dar_ManPiNum(p->pManAig), p->nSimWords * 32 - 1 );
+ for ( i = 0; i < Limit; i++ )
+ Dar_InfoXorBit( Fra_ObjSim( Dar_ManPi(p->pManAig,i) ), i+1 );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns 1 if simulation info is composed of all zeros.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Fra_NodeHasZeroSim( Fra_Man_t * p, Dar_Obj_t * pObj )
+{
+ unsigned * pSims;
+ int i;
+ pSims = Fra_ObjSim(pObj);
+ for ( i = 0; i < p->nSimWords; i++ )
+ if ( pSims[i] )
+ return 0;
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns 1 if simulation info is composed of all zeros.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Fra_NodeComplementSim( Fra_Man_t * p, Dar_Obj_t * pObj )
+{
+ unsigned * pSims;
+ int i;
+ pSims = Fra_ObjSim(pObj);
+ for ( i = 0; i < p->nSimWords; i++ )
+ pSims[i] = ~pSims[i];
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns 1 if simulation infos are equal.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Fra_NodeCompareSims( Fra_Man_t * p, Dar_Obj_t * pObj0, Dar_Obj_t * pObj1 )
+{
+ unsigned * pSims0, * pSims1;
+ int i;
+ pSims0 = Fra_ObjSim(pObj0);
+ pSims1 = Fra_ObjSim(pObj1);
+ for ( i = 0; i < p->nSimWords; i++ )
+ if ( pSims0[i] != pSims1[i] )
+ return 0;
+ return 1;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Simulates one node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Fra_NodeSimulate( Fra_Man_t * p, Dar_Obj_t * pObj )
+{
+ unsigned * pSims, * pSims0, * pSims1;
+ int fCompl, fCompl0, fCompl1, i;
+ assert( !Dar_IsComplement(pObj) );
+ assert( Dar_ObjIsNode(pObj) );
+ // get hold of the simulation information
+ pSims = Fra_ObjSim(pObj);
+ pSims0 = Fra_ObjSim(Dar_ObjFanin0(pObj));
+ pSims1 = Fra_ObjSim(Dar_ObjFanin1(pObj));
+ // get complemented attributes of the children using their random info
+ fCompl = pObj->fPhase;
+ fCompl0 = Dar_ObjFaninPhase(Dar_ObjChild0(pObj));
+ fCompl1 = Dar_ObjFaninPhase(Dar_ObjChild1(pObj));
+ // simulate
+ if ( fCompl0 && fCompl1 )
+ {
+ if ( fCompl )
+ for ( i = 0; i < p->nSimWords; i++ )
+ pSims[i] = (pSims0[i] | pSims1[i]);
+ else
+ for ( i = 0; i < p->nSimWords; i++ )
+ pSims[i] = ~(pSims0[i] | pSims1[i]);
+ }
+ else if ( fCompl0 && !fCompl1 )
+ {
+ if ( fCompl )
+ for ( i = 0; i < p->nSimWords; i++ )
+ pSims[i] = (pSims0[i] | ~pSims1[i]);
+ else
+ for ( i = 0; i < p->nSimWords; i++ )
+ pSims[i] = (~pSims0[i] & pSims1[i]);
+ }
+ else if ( !fCompl0 && fCompl1 )
+ {
+ if ( fCompl )
+ for ( i = 0; i < p->nSimWords; i++ )
+ pSims[i] = (~pSims0[i] | pSims1[i]);
+ else
+ for ( i = 0; i < p->nSimWords; i++ )
+ pSims[i] = (pSims0[i] & ~pSims1[i]);
+ }
+ else // if ( !fCompl0 && !fCompl1 )
+ {
+ if ( fCompl )
+ for ( i = 0; i < p->nSimWords; i++ )
+ pSims[i] = ~(pSims0[i] & pSims1[i]);
+ else
+ for ( i = 0; i < p->nSimWords; i++ )
+ pSims[i] = (pSims0[i] & pSims1[i]);
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Generated const 0 pattern.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Fra_SavePattern0( Fra_Man_t * p )
+{
+ memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
+}
+
+/**Function*************************************************************
+
+ Synopsis [[Generated const 1 pattern.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Fra_SavePattern1( Fra_Man_t * p )
+{
+ memset( p->pPatWords, 0xff, sizeof(unsigned) * p->nPatWords );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Copy pattern from the solver into the internal storage.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Fra_SavePattern( Fra_Man_t * p )
+{
+ Dar_Obj_t * pObj;
+ int i;
+ memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
+ Dar_ManForEachPi( p->pManFraig, pObj, i )
+// Vec_PtrForEachEntry( p->vPiVars, pObj, i )
+ if ( p->pSat->model.ptr[Fra_ObjSatNum(pObj)] == l_True )
+ Dar_InfoSetBit( p->pPatWords, i );
+// Ivy_InfoSetBit( p->pPatWords, pObj->Id - 1 );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Cleans pattern scores.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Fra_CleanPatScores( Fra_Man_t * p )
+{
+ int i, nLimit = p->nSimWords * 32;
+ for ( i = 0; i < nLimit; i++ )
+ p->pPatScores[i] = 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Adds to pattern scores.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Fra_AddToPatScores( Fra_Man_t * p, Dar_Obj_t * pClass, Dar_Obj_t * pClassNew )
+{
+ unsigned * pSims0, * pSims1;
+ unsigned uDiff;
+ int i, w;
+ // get hold of the simulation information
+ pSims0 = Fra_ObjSim(pClass);
+ pSims1 = Fra_ObjSim(pClassNew);
+ // iterate through the differences and record the score
+ for ( w = 0; w < p->nSimWords; w++ )
+ {
+ uDiff = pSims0[w] ^ pSims1[w];
+ if ( uDiff == 0 )
+ continue;
+ for ( i = 0; i < 32; i++ )
+ if ( uDiff & ( 1 << i ) )
+ p->pPatScores[w*32+i]++;
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Selects the best pattern.]
+
+ Description [Returns 1 if such pattern is found.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Fra_SelectBestPat( Fra_Man_t * p )
+{
+ unsigned * pSims;
+ Dar_Obj_t * pObj;
+ int i, nLimit = p->nSimWords * 32, MaxScore = 0, BestPat = -1;
+ for ( i = 1; i < nLimit; i++ )
+ {
+ if ( MaxScore < p->pPatScores[i] )
+ {
+ MaxScore = p->pPatScores[i];
+ BestPat = i;
+ }
+ }
+ if ( MaxScore == 0 )
+ return 0;
+// if ( MaxScore > p->pPars->MaxScore )
+// printf( "Max score is %3d. ", MaxScore );
+ // copy the best pattern into the selected pattern
+ memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
+ Dar_ManForEachPi( p->pManAig, pObj, i )
+ {
+ pSims = Fra_ObjSim(pObj);
+ if ( Dar_InfoHasBit(pSims, BestPat) )
+ Dar_InfoSetBit(p->pPatWords, i);
+ }
+ return MaxScore;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Simulates AIG manager.]
+
+ Description [Assumes that the PI simulation info is attached.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Fra_SimulateOne( Fra_Man_t * p )
+{
+ Dar_Obj_t * pObj;
+ int i, clk;
+clk = clock();
+ Dar_ManForEachNode( p->pManAig, pObj, i )
+ {
+ Fra_NodeSimulate( p, pObj );
+/*
+ if ( Dar_ObjFraig(pObj) == NULL )
+ printf( "%3d --- -- %d : ", pObj->Id, pObj->fPhase );
+ else
+ printf( "%3d %3d %2d %d : ", pObj->Id, Dar_Regular(Dar_ObjFraig(pObj))->Id, Dar_ObjSatNum(Dar_Regular(Dar_ObjFraig(pObj))), pObj->fPhase );
+ Extra_PrintBinary( stdout, Fra_ObjSim(pObj), 30 );
+ printf( "\n" );
+*/
+ }
+p->timeSim += clock() - clk;
+p->nSimRounds++;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Resimulates fraiging manager after finding a counter-example.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Fra_Resimulate( Fra_Man_t * p )
+{
+ int nChanges;
+ Fra_AssignDist1( p, p->pPatWords );
+ Fra_SimulateOne( p );
+ if ( p->pPars->fPatScores )
+ Fra_CleanPatScores( p );
+ nChanges = Fra_RefineClasses( p );
+ nChanges += Fra_RefineClasses1( p );
+ if ( p->pManFraig->pData )
+ return;
+ if ( nChanges < 1 )
+ printf( "Error: A counter-example did not refine classes!\n" );
+ assert( nChanges >= 1 );
+//printf( "Refined classes! = %5d. Changes = %4d.\n", p->lClasses.nItems, nChanges );
+
+ if ( !p->pPars->fPatScores )
+ return;
+
+ // perform additional simulation using dist1 patterns derived from successful patterns
+ while ( Fra_SelectBestPat(p) > p->pPars->MaxScore )
+ {
+ Fra_AssignDist1( p, p->pPatWords );
+ Fra_SimulateOne( p );
+ Fra_CleanPatScores( p );
+ nChanges = Fra_RefineClasses( p );
+ nChanges += Fra_RefineClasses1( p );
+ if ( p->pManFraig->pData )
+ return;
+//printf( "Refined class!!! = %5d. Changes = %4d. Pairs = %6d.\n", p->lClasses.nItems, nChanges, Fra_CountPairsClasses(p) );
+ if ( nChanges == 0 )
+ break;
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs simulation of the manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Fra_Simulate( Fra_Man_t * p )
+{
+ int nChanges, nClasses;
+ // start the classes
+ Fra_AssignRandom( p );
+ Fra_SimulateOne( p );
+ Fra_CreateClasses( p );
+//printf( "Starting classes = %5d. Pairs = %6d.\n", p->lClasses.nItems, Fra_CountPairsClasses(p) );
+ // refine classes by walking 0/1 patterns
+ Fra_SavePattern0( p );
+ Fra_AssignDist1( p, p->pPatWords );
+ Fra_SimulateOne( p );
+ nChanges = Fra_RefineClasses( p );
+ nChanges += Fra_RefineClasses1( p );
+ if ( p->pManFraig )
+ return;
+//printf( "Refined classes = %5d. Changes = %4d. Pairs = %6d.\n", p->lClasses.nItems, nChanges, Fra_CountPairsClasses(p) );
+ Fra_SavePattern1( p );
+ Fra_AssignDist1( p, p->pPatWords );
+ Fra_SimulateOne( p );
+ nChanges = Fra_RefineClasses( p );
+ nChanges += Fra_RefineClasses1( p );
+ if ( p->pManFraig )
+ return;
+//printf( "Refined classes = %5d. Changes = %4d. Pairs = %6d.\n", p->lClasses.nItems, nChanges, Fra_CountPairsClasses(p) );
+ // refine classes by random simulation
+ do {
+ Fra_AssignRandom( p );
+ Fra_SimulateOne( p );
+ nClasses = Vec_PtrSize(p->vClasses);
+ nChanges = Fra_RefineClasses( p );
+ nChanges += Fra_RefineClasses1( p );
+ if ( p->pManFraig )
+ return;
+//printf( "Refined classes = %5d. Changes = %4d. Pairs = %6d.\n", p->lClasses.nItems, nChanges, Fra_CountPairsClasses(p) );
+ } while ( (double)nChanges / nClasses > p->pPars->dSimSatur );
+// Fra_PrintSimClasses( p );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Creates the counter-example from the successful pattern.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Fra_CheckOutputSimsSavePattern( Fra_Man_t * p, Dar_Obj_t * pObj )
+{
+ unsigned * pSims;
+ int i, k, BestPat, * pModel;
+ // find the word of the pattern
+ pSims = Fra_ObjSim(pObj);
+ for ( i = 0; i < p->nSimWords; i++ )
+ if ( pSims[i] )
+ break;
+ assert( i < p->nSimWords );
+ // find the bit of the pattern
+ for ( k = 0; k < 32; k++ )
+ if ( pSims[i] & (1 << k) )
+ break;
+ assert( k < 32 );
+ // determine the best pattern
+ BestPat = i * 32 + k;
+ // fill in the counter-example data
+ pModel = ALLOC( int, Dar_ManPiNum(p->pManFraig) );
+ Dar_ManForEachPi( p->pManAig, pObj, i )
+ {
+ pModel[i] = Dar_InfoHasBit(Fra_ObjSim(pObj), BestPat);
+// printf( "%d", pModel[i] );
+ }
+// printf( "\n" );
+ // set the model
+ assert( p->pManFraig->pData == NULL );
+ p->pManFraig->pData = pModel;
+ return;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns 1 if the one of the output is already non-constant 0.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Fra_CheckOutputSims( Fra_Man_t * p )
+{
+ Dar_Obj_t * pObj;
+ int i;
+ // make sure the reference simulation pattern does not detect the bug
+ pObj = Dar_ManPo( p->pManAig, 0 );
+ assert( Dar_ObjFanin0(pObj)->fPhase == (unsigned)Dar_ObjFaninC0(pObj) ); // Dar_ObjFaninPhase(Dar_ObjChild0(pObj)) == 0
+ Dar_ManForEachPo( p->pManAig, pObj, i )
+ {
+ // complement simulation info
+// if ( Dar_ObjFanin0(pObj)->fPhase ^ Dar_ObjFaninC0(pObj) ) // Dar_ObjFaninPhase(Dar_ObjChild0(pObj))
+// Fra_NodeComplementSim( p, Dar_ObjFanin0(pObj) );
+ // check
+ if ( !Fra_NodeHasZeroSim( p, Dar_ObjFanin0(pObj) ) )
+ {
+ // create the counter-example from this pattern
+ Fra_CheckOutputSimsSavePattern( p, Dar_ObjFanin0(pObj) );
+ return 1;
+ }
+ // complement simulation info
+// if ( Dar_ObjFanin0(pObj)->fPhase ^ Dar_ObjFaninC0(pObj) )
+// Fra_NodeComplementSim( p, Dar_ObjFanin0(pObj) );
+ }
+ return 0;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/fra/fra_.c b/src/aig/fra/fra_.c
new file mode 100644
index 00000000..2b601587
--- /dev/null
+++ b/src/aig/fra/fra_.c
@@ -0,0 +1,48 @@
+/**CFile****************************************************************
+
+ FileName [fra_.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [New FRAIG package.]
+
+ Synopsis []
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 30, 2007.]
+
+ Revision [$Id: fra_.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "fra.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/fra/ivyFraig.c b/src/aig/fra/ivyFraig.c
new file mode 100644
index 00000000..e9a65881
--- /dev/null
+++ b/src/aig/fra/ivyFraig.c
@@ -0,0 +1,2750 @@
+/**CFile****************************************************************
+
+ FileName [ivyFraig.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [And-Inverter Graph package.]
+
+ Synopsis [Functional reduction of AIGs]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - May 11, 2006.]
+
+ Revision [$Id: ivyFraig.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "satSolver.h"
+#include "extra.h"
+#include "ivy.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Ivy_FraigMan_t_ Ivy_FraigMan_t;
+typedef struct Ivy_FraigSim_t_ Ivy_FraigSim_t;
+typedef struct Ivy_FraigList_t_ Ivy_FraigList_t;
+
+struct Ivy_FraigList_t_
+{
+ Ivy_Obj_t * pHead;
+ Ivy_Obj_t * pTail;
+ int nItems;
+};
+
+struct Ivy_FraigSim_t_
+{
+ int Type;
+ Ivy_FraigSim_t * pNext;
+ Ivy_FraigSim_t * pFanin0;
+ Ivy_FraigSim_t * pFanin1;
+ unsigned pData[0];
+};
+
+struct Ivy_FraigMan_t_
+{
+ // general info
+ Ivy_FraigParams_t * pParams; // various parameters
+ // temporary backtrack limits because "sint64" cannot be defined in Ivy_FraigParams_t ...
+ sint64 nBTLimitGlobal; // global limit on the number of backtracks
+ sint64 nInsLimitGlobal;// global limit on the number of clause inspects
+ // AIG manager
+ Ivy_Man_t * pManAig; // the starting AIG manager
+ Ivy_Man_t * pManFraig; // the final AIG manager
+ // simulation information
+ int nSimWords; // the number of words
+ char * pSimWords; // the simulation info
+ Ivy_FraigSim_t * pSimStart; // the list of simulation info for internal nodes
+ // counter example storage
+ int nPatWords; // the number of words in the counter example
+ unsigned * pPatWords; // the counter example
+ int * pPatScores; // the scores of each pattern
+ // equivalence classes
+ Ivy_FraigList_t lClasses; // equivalence classes
+ Ivy_FraigList_t lCand; // candidatates
+ int nPairs; // the number of pairs of nodes
+ // equivalence checking
+ sat_solver * pSat; // SAT solver
+ int nSatVars; // the number of variables currently used
+ Vec_Ptr_t * vPiVars; // the PIs of the cone used
+ // other
+ ProgressBar * pProgress;
+ // statistics
+ int nSimRounds;
+ int nNodesMiter;
+ int nClassesZero;
+ int nClassesBeg;
+ int nClassesEnd;
+ int nPairsBeg;
+ int nPairsEnd;
+ int nSatCalls;
+ int nSatCallsSat;
+ int nSatCallsUnsat;
+ int nSatProof;
+ int nSatFails;
+ int nSatFailsReal;
+ // runtime
+ int timeSim;
+ int timeTrav;
+ int timeSat;
+ int timeSatUnsat;
+ int timeSatSat;
+ int timeSatFail;
+ int timeRef;
+ int timeTotal;
+ int time1;
+ int time2;
+};
+
+typedef struct Prove_ParamsStruct_t_ Prove_Params_t;
+struct Prove_ParamsStruct_t_
+{
+ // general parameters
+ int fUseFraiging; // enables fraiging
+ int fUseRewriting; // enables rewriting
+ int fUseBdds; // enables BDD construction when other methods fail
+ int fVerbose; // prints verbose stats
+ // iterations
+ int nItersMax; // the number of iterations
+ // mitering
+ int nMiteringLimitStart; // starting mitering limit
+ float nMiteringLimitMulti; // multiplicative coefficient to increase the limit in each iteration
+ // rewriting
+ int nRewritingLimitStart; // the number of rewriting iterations
+ float nRewritingLimitMulti; // multiplicative coefficient to increase the limit in each iteration
+ // fraiging
+ int nFraigingLimitStart; // starting backtrack(conflict) limit
+ float nFraigingLimitMulti; // multiplicative coefficient to increase the limit in each iteration
+ // last-gasp BDD construction
+ int nBddSizeLimit; // the number of BDD nodes when construction is aborted
+ int fBddReorder; // enables dynamic BDD variable reordering
+ // last-gasp mitering
+ int nMiteringLimitLast; // final mitering limit
+ // global SAT solver limits
+ sint64 nTotalBacktrackLimit; // global limit on the number of backtracks
+ sint64 nTotalInspectLimit; // global limit on the number of clause inspects
+ // global resources applied
+ sint64 nTotalBacktracksMade; // the total number of backtracks made
+ sint64 nTotalInspectsMade; // the total number of inspects made
+};
+
+static inline Ivy_FraigSim_t * Ivy_ObjSim( Ivy_Obj_t * pObj ) { return (Ivy_FraigSim_t *)pObj->pFanout; }
+static inline Ivy_Obj_t * Ivy_ObjClassNodeLast( Ivy_Obj_t * pObj ) { return pObj->pNextFan0; }
+static inline Ivy_Obj_t * Ivy_ObjClassNodeRepr( Ivy_Obj_t * pObj ) { return pObj->pNextFan0; }
+static inline Ivy_Obj_t * Ivy_ObjClassNodeNext( Ivy_Obj_t * pObj ) { return pObj->pNextFan1; }
+static inline Ivy_Obj_t * Ivy_ObjNodeHashNext( Ivy_Obj_t * pObj ) { return pObj->pPrevFan0; }
+static inline Ivy_Obj_t * Ivy_ObjEquivListNext( Ivy_Obj_t * pObj ) { return pObj->pPrevFan0; }
+static inline Ivy_Obj_t * Ivy_ObjEquivListPrev( Ivy_Obj_t * pObj ) { return pObj->pPrevFan1; }
+static inline Ivy_Obj_t * Ivy_ObjFraig( Ivy_Obj_t * pObj ) { return pObj->pEquiv; }
+static inline int Ivy_ObjSatNum( Ivy_Obj_t * pObj ) { return (int)pObj->pNextFan0; }
+static inline Vec_Ptr_t * Ivy_ObjFaninVec( Ivy_Obj_t * pObj ) { return (Vec_Ptr_t *)pObj->pNextFan1; }
+
+static inline void Ivy_ObjSetSim( Ivy_Obj_t * pObj, Ivy_FraigSim_t * pSim ) { pObj->pFanout = (Ivy_Obj_t *)pSim; }
+static inline void Ivy_ObjSetClassNodeLast( Ivy_Obj_t * pObj, Ivy_Obj_t * pLast ) { pObj->pNextFan0 = pLast; }
+static inline void Ivy_ObjSetClassNodeRepr( Ivy_Obj_t * pObj, Ivy_Obj_t * pRepr ) { pObj->pNextFan0 = pRepr; }
+static inline void Ivy_ObjSetClassNodeNext( Ivy_Obj_t * pObj, Ivy_Obj_t * pNext ) { pObj->pNextFan1 = pNext; }
+static inline void Ivy_ObjSetNodeHashNext( Ivy_Obj_t * pObj, Ivy_Obj_t * pNext ) { pObj->pPrevFan0 = pNext; }
+static inline void Ivy_ObjSetEquivListNext( Ivy_Obj_t * pObj, Ivy_Obj_t * pNext ) { pObj->pPrevFan0 = pNext; }
+static inline void Ivy_ObjSetEquivListPrev( Ivy_Obj_t * pObj, Ivy_Obj_t * pPrev ) { pObj->pPrevFan1 = pPrev; }
+static inline void Ivy_ObjSetFraig( Ivy_Obj_t * pObj, Ivy_Obj_t * pNode ) { pObj->pEquiv = pNode; }
+static inline void Ivy_ObjSetSatNum( Ivy_Obj_t * pObj, int Num ) { pObj->pNextFan0 = (Ivy_Obj_t *)Num; }
+static inline void Ivy_ObjSetFaninVec( Ivy_Obj_t * pObj, Vec_Ptr_t * vFanins ) { pObj->pNextFan1 = (Ivy_Obj_t *)vFanins; }
+
+static inline unsigned Ivy_ObjRandomSim() { return (rand() << 24) ^ (rand() << 12) ^ rand(); }
+
+// iterate through equivalence classes
+#define Ivy_FraigForEachEquivClass( pList, pEnt ) \
+ for ( pEnt = pList; \
+ pEnt; \
+ pEnt = Ivy_ObjEquivListNext(pEnt) )
+#define Ivy_FraigForEachEquivClassSafe( pList, pEnt, pEnt2 ) \
+ for ( pEnt = pList, \
+ pEnt2 = pEnt? Ivy_ObjEquivListNext(pEnt): NULL; \
+ pEnt; \
+ pEnt = pEnt2, \
+ pEnt2 = pEnt? Ivy_ObjEquivListNext(pEnt): NULL )
+// iterate through nodes in one class
+#define Ivy_FraigForEachClassNode( pClass, pEnt ) \
+ for ( pEnt = pClass; \
+ pEnt; \
+ pEnt = Ivy_ObjClassNodeNext(pEnt) )
+// iterate through nodes in the hash table
+#define Ivy_FraigForEachBinNode( pBin, pEnt ) \
+ for ( pEnt = pBin; \
+ pEnt; \
+ pEnt = Ivy_ObjNodeHashNext(pEnt) )
+
+static Ivy_FraigMan_t * Ivy_FraigStart( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams );
+static Ivy_FraigMan_t * Ivy_FraigStartSimple( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams );
+static Ivy_Man_t * Ivy_FraigPerform_int( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams, sint64 nBTLimitGlobal, sint64 nInsLimitGlobal, sint64 * pnSatConfs, sint64 * pnSatInspects );
+static void Ivy_FraigPrint( Ivy_FraigMan_t * p );
+static void Ivy_FraigStop( Ivy_FraigMan_t * p );
+static void Ivy_FraigSimulate( Ivy_FraigMan_t * p );
+static void Ivy_FraigSweep( Ivy_FraigMan_t * p );
+static Ivy_Obj_t * Ivy_FraigAnd( Ivy_FraigMan_t * p, Ivy_Obj_t * pObjOld );
+static int Ivy_FraigNodesAreEquiv( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj0, Ivy_Obj_t * pObj1 );
+static int Ivy_FraigNodeIsConst( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj );
+static void Ivy_FraigNodeAddToSolver( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj0, Ivy_Obj_t * pObj1 );
+static int Ivy_FraigSetActivityFactors( Ivy_FraigMan_t * p, Ivy_Obj_t * pOld, Ivy_Obj_t * pNew );
+static void Ivy_FraigAddToPatScores( Ivy_FraigMan_t * p, Ivy_Obj_t * pClass, Ivy_Obj_t * pClassNew );
+static int Ivy_FraigMiterStatus( Ivy_Man_t * pMan );
+static void Ivy_FraigMiterProve( Ivy_FraigMan_t * p );
+static void Ivy_FraigMiterPrint( Ivy_Man_t * pNtk, char * pString, int clk, int fVerbose );
+static int * Ivy_FraigCreateModel( Ivy_FraigMan_t * p );
+
+static int Ivy_FraigNodesAreEquivBdd( Ivy_Obj_t * pObj1, Ivy_Obj_t * pObj2 );
+
+static sint64 s_nBTLimitGlobal = 0;
+static sint64 s_nInsLimitGlobal = 0;
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Sets the default solving parameters.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_FraigParamsDefault( Ivy_FraigParams_t * pParams )
+{
+ memset( pParams, 0, sizeof(Ivy_FraigParams_t) );
+ pParams->nSimWords = 32; // the number of words in the simulation info
+ pParams->dSimSatur = 0.005; // the ratio of refined classes when saturation is reached
+ pParams->fPatScores = 0; // enables simulation pattern scoring
+ pParams->MaxScore = 25; // max score after which resimulation is used
+ pParams->fDoSparse = 1; // skips sparse functions
+// pParams->dActConeRatio = 0.05; // the ratio of cone to be bumped
+// pParams->dActConeBumpMax = 5.0; // the largest bump of activity
+ pParams->dActConeRatio = 0.3; // the ratio of cone to be bumped
+ pParams->dActConeBumpMax = 10.0; // the largest bump of activity
+
+ pParams->nBTLimitNode = 100; // conflict limit at a node
+ pParams->nBTLimitMiter = 500000; // conflict limit at an output
+// pParams->nBTLimitGlobal = 0; // conflict limit global
+// pParams->nInsLimitGlobal = 0; // inspection limit global
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs combinational equivalence checking for the miter.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ivy_FraigProve( Ivy_Man_t ** ppManAig, void * pPars )
+{
+ Prove_Params_t * pParams = pPars;
+ Ivy_FraigParams_t Params, * pIvyParams = &Params;
+ Ivy_Man_t * pManAig, * pManTemp;
+ int RetValue, nIter, clk, timeStart = clock();//, Counter;
+ sint64 nSatConfs, nSatInspects;
+
+ // start the network and parameters
+ pManAig = *ppManAig;
+ Ivy_FraigParamsDefault( pIvyParams );
+ pIvyParams->fVerbose = pParams->fVerbose;
+ pIvyParams->fProve = 1;
+
+ if ( pParams->fVerbose )
+ {
+ printf( "RESOURCE LIMITS: Iterations = %d. Rewriting = %s. Fraiging = %s.\n",
+ pParams->nItersMax, pParams->fUseRewriting? "yes":"no", pParams->fUseFraiging? "yes":"no" );
+ printf( "Mitering = %d (%3.1f). Rewriting = %d (%3.1f). Fraiging = %d (%3.1f).\n",
+ pParams->nMiteringLimitStart, pParams->nMiteringLimitMulti,
+ pParams->nRewritingLimitStart, pParams->nRewritingLimitMulti,
+ pParams->nFraigingLimitStart, pParams->nFraigingLimitMulti );
+ printf( "Mitering last = %d.\n",
+ pParams->nMiteringLimitLast );
+ }
+
+ // if SAT only, solve without iteration
+ if ( !pParams->fUseRewriting && !pParams->fUseFraiging )
+ {
+ clk = clock();
+ pIvyParams->nBTLimitMiter = pParams->nMiteringLimitLast / Ivy_ManPoNum(pManAig);
+ pManAig = Ivy_FraigMiter( pManTemp = pManAig, pIvyParams ); Ivy_ManStop( pManTemp );
+ RetValue = Ivy_FraigMiterStatus( pManAig );
+ Ivy_FraigMiterPrint( pManAig, "SAT solving", clk, pParams->fVerbose );
+ *ppManAig = pManAig;
+ return RetValue;
+ }
+
+ if ( Ivy_ManNodeNum(pManAig) < 500 )
+ {
+ // run the first mitering
+ clk = clock();
+ pIvyParams->nBTLimitMiter = pParams->nMiteringLimitStart / Ivy_ManPoNum(pManAig);
+ pManAig = Ivy_FraigMiter( pManTemp = pManAig, pIvyParams ); Ivy_ManStop( pManTemp );
+ RetValue = Ivy_FraigMiterStatus( pManAig );
+ Ivy_FraigMiterPrint( pManAig, "SAT solving", clk, pParams->fVerbose );
+ if ( RetValue >= 0 )
+ {
+ *ppManAig = pManAig;
+ return RetValue;
+ }
+ }
+
+ // check the current resource limits
+ RetValue = -1;
+ for ( nIter = 0; nIter < pParams->nItersMax; nIter++ )
+ {
+ if ( pParams->fVerbose )
+ {
+ printf( "ITERATION %2d : Confs = %6d. FraigBTL = %3d. \n", nIter+1,
+ (int)(pParams->nMiteringLimitStart * pow(pParams->nMiteringLimitMulti,nIter)),
+ (int)(pParams->nFraigingLimitStart * pow(pParams->nFraigingLimitMulti,nIter)) );
+ fflush( stdout );
+ }
+
+ // try rewriting
+ if ( pParams->fUseRewriting )
+ { // bug in Ivy_NodeFindCutsAll() when leaves are identical!
+/*
+ clk = clock();
+ Counter = (int)(pParams->nRewritingLimitStart * pow(pParams->nRewritingLimitMulti,nIter));
+ pManAig = Ivy_ManRwsat( pManAig, 0 );
+ RetValue = Ivy_FraigMiterStatus( pManAig );
+ Ivy_FraigMiterPrint( pManAig, "Rewriting ", clk, pParams->fVerbose );
+*/
+ }
+ if ( RetValue >= 0 )
+ break;
+
+ // try fraiging followed by mitering
+ if ( pParams->fUseFraiging )
+ {
+ clk = clock();
+ pIvyParams->nBTLimitNode = (int)(pParams->nFraigingLimitStart * pow(pParams->nFraigingLimitMulti,nIter));
+ pIvyParams->nBTLimitMiter = (int)(pParams->nMiteringLimitStart * pow(pParams->nMiteringLimitMulti,nIter)) / Ivy_ManPoNum(pManAig);
+ pManAig = Ivy_FraigPerform_int( pManTemp = pManAig, pIvyParams, pParams->nTotalBacktrackLimit, pParams->nTotalInspectLimit, &nSatConfs, &nSatInspects ); Ivy_ManStop( pManTemp );
+ RetValue = Ivy_FraigMiterStatus( pManAig );
+ Ivy_FraigMiterPrint( pManAig, "Fraiging ", clk, pParams->fVerbose );
+ }
+ if ( RetValue >= 0 )
+ break;
+
+ // add to the number of backtracks and inspects
+ pParams->nTotalBacktracksMade += nSatConfs;
+ pParams->nTotalInspectsMade += nSatInspects;
+ // check if global resource limit is reached
+ if ( (pParams->nTotalBacktrackLimit && pParams->nTotalBacktracksMade >= pParams->nTotalBacktrackLimit) ||
+ (pParams->nTotalInspectLimit && pParams->nTotalInspectsMade >= pParams->nTotalInspectLimit) )
+ {
+ printf( "Reached global limit on conflicts/inspects. Quitting.\n" );
+ *ppManAig = pManAig;
+ return -1;
+ }
+ }
+
+ if ( RetValue < 0 )
+ {
+ if ( pParams->fVerbose )
+ {
+ printf( "Attempting SAT with conflict limit %d ...\n", pParams->nMiteringLimitLast );
+ fflush( stdout );
+ }
+ clk = clock();
+ pIvyParams->nBTLimitMiter = pParams->nMiteringLimitLast / Ivy_ManPoNum(pManAig);
+ if ( pParams->nTotalBacktrackLimit )
+ s_nBTLimitGlobal = pParams->nTotalBacktrackLimit - pParams->nTotalBacktracksMade;
+ if ( pParams->nTotalInspectLimit )
+ s_nInsLimitGlobal = pParams->nTotalInspectLimit - pParams->nTotalInspectsMade;
+ pManAig = Ivy_FraigMiter( pManTemp = pManAig, pIvyParams ); Ivy_ManStop( pManTemp );
+ s_nBTLimitGlobal = 0;
+ s_nInsLimitGlobal = 0;
+ RetValue = Ivy_FraigMiterStatus( pManAig );
+ Ivy_FraigMiterPrint( pManAig, "SAT solving", clk, pParams->fVerbose );
+ // make sure that the sover never returns "undecided" when infinite resource limits are set
+ if( RetValue == -1 && pParams->nTotalInspectLimit == 0 &&
+ pParams->nTotalBacktrackLimit == 0 )
+ {
+ extern void Prove_ParamsPrint( Prove_Params_t * pParams );
+ Prove_ParamsPrint( pParams );
+ printf("ERROR: ABC has returned \"undecided\" in spite of no limits...\n");
+ exit(1);
+ }
+ }
+
+ // assign the model if it was proved by rewriting (const 1 miter)
+ if ( RetValue == 0 && pManAig->pData == NULL )
+ {
+ pManAig->pData = ALLOC( int, Ivy_ManPiNum(pManAig) );
+ memset( pManAig->pData, 0, sizeof(int) * Ivy_ManPiNum(pManAig) );
+ }
+ *ppManAig = pManAig;
+ return RetValue;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs fraiging of the AIG.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Ivy_Man_t * Ivy_FraigPerform_int( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams, sint64 nBTLimitGlobal, sint64 nInsLimitGlobal, sint64 * pnSatConfs, sint64 * pnSatInspects )
+{
+ Ivy_FraigMan_t * p;
+ Ivy_Man_t * pManAigNew;
+ int clk;
+ if ( Ivy_ManNodeNum(pManAig) == 0 )
+ return Ivy_ManDup(pManAig);
+clk = clock();
+ assert( Ivy_ManLatchNum(pManAig) == 0 );
+ p = Ivy_FraigStart( pManAig, pParams );
+ // set global limits
+ p->nBTLimitGlobal = nBTLimitGlobal;
+ p->nInsLimitGlobal = nInsLimitGlobal;
+
+ Ivy_FraigSimulate( p );
+ Ivy_FraigSweep( p );
+ pManAigNew = p->pManFraig;
+p->timeTotal = clock() - clk;
+ if ( pnSatConfs )
+ *pnSatConfs = p->pSat? p->pSat->stats.conflicts : 0;
+ if ( pnSatInspects )
+ *pnSatInspects = p->pSat? p->pSat->stats.inspects : 0;
+ Ivy_FraigStop( p );
+ return pManAigNew;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs fraiging of the AIG.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Ivy_Man_t * Ivy_FraigPerform( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams )
+{
+ Ivy_FraigMan_t * p;
+ Ivy_Man_t * pManAigNew;
+ int clk;
+ if ( Ivy_ManNodeNum(pManAig) == 0 )
+ return Ivy_ManDup(pManAig);
+clk = clock();
+ assert( Ivy_ManLatchNum(pManAig) == 0 );
+ p = Ivy_FraigStart( pManAig, pParams );
+ Ivy_FraigSimulate( p );
+ Ivy_FraigSweep( p );
+ pManAigNew = p->pManFraig;
+p->timeTotal = clock() - clk;
+ Ivy_FraigStop( p );
+ return pManAigNew;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Applies brute-force SAT to the miter.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Ivy_Man_t * Ivy_FraigMiter( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams )
+{
+ Ivy_FraigMan_t * p;
+ Ivy_Man_t * pManAigNew;
+ Ivy_Obj_t * pObj;
+ int i, clk;
+clk = clock();
+ assert( Ivy_ManLatchNum(pManAig) == 0 );
+ p = Ivy_FraigStartSimple( pManAig, pParams );
+ // set global limits
+ p->nBTLimitGlobal = s_nBTLimitGlobal;
+ p->nInsLimitGlobal = s_nInsLimitGlobal;
+ // duplicate internal nodes
+ Ivy_ManForEachNode( p->pManAig, pObj, i )
+ pObj->pEquiv = Ivy_And( p->pManFraig, Ivy_ObjChild0Equiv(pObj), Ivy_ObjChild1Equiv(pObj) );
+ // try to prove each output of the miter
+ Ivy_FraigMiterProve( p );
+ // add the POs
+ Ivy_ManForEachPo( p->pManAig, pObj, i )
+ Ivy_ObjCreatePo( p->pManFraig, Ivy_ObjChild0Equiv(pObj) );
+ // clean the new manager
+ Ivy_ManForEachObj( p->pManFraig, pObj, i )
+ {
+ if ( Ivy_ObjFaninVec(pObj) )
+ Vec_PtrFree( Ivy_ObjFaninVec(pObj) );
+ pObj->pNextFan0 = pObj->pNextFan1 = NULL;
+ }
+ // remove dangling nodes
+ Ivy_ManCleanup( p->pManFraig );
+ pManAigNew = p->pManFraig;
+p->timeTotal = clock() - clk;
+
+//printf( "Final nodes = %6d. ", Ivy_ManNodeNum(pManAigNew) );
+//PRT( "Time", p->timeTotal );
+ Ivy_FraigStop( p );
+ return pManAigNew;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Starts the fraiging manager without simulation info.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Ivy_FraigMan_t * Ivy_FraigStartSimple( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams )
+{
+ Ivy_FraigMan_t * p;
+ // allocat the fraiging manager
+ p = ALLOC( Ivy_FraigMan_t, 1 );
+ memset( p, 0, sizeof(Ivy_FraigMan_t) );
+ p->pParams = pParams;
+ p->pManAig = pManAig;
+ p->pManFraig = Ivy_ManStartFrom( pManAig );
+ p->vPiVars = Vec_PtrAlloc( 100 );
+ return p;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Starts the fraiging manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Ivy_FraigMan_t * Ivy_FraigStart( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams )
+{
+ Ivy_FraigMan_t * p;
+ Ivy_FraigSim_t * pSims;
+ Ivy_Obj_t * pObj;
+ int i, k, EntrySize;
+ // clean the fanout representation
+ Ivy_ManForEachObj( pManAig, pObj, i )
+// pObj->pEquiv = pObj->pFanout = pObj->pNextFan0 = pObj->pNextFan1 = pObj->pPrevFan0 = pObj->pPrevFan1 = NULL;
+ assert( !pObj->pEquiv && !pObj->pFanout );
+ // allocat the fraiging manager
+ p = ALLOC( Ivy_FraigMan_t, 1 );
+ memset( p, 0, sizeof(Ivy_FraigMan_t) );
+ p->pParams = pParams;
+ p->pManAig = pManAig;
+ p->pManFraig = Ivy_ManStartFrom( pManAig );
+ // allocate simulation info
+ p->nSimWords = pParams->nSimWords;
+// p->pSimWords = ALLOC( unsigned, Ivy_ManObjNum(pManAig) * p->nSimWords );
+ EntrySize = sizeof(Ivy_FraigSim_t) + sizeof(unsigned) * p->nSimWords;
+ p->pSimWords = (char *)malloc( Ivy_ManObjNum(pManAig) * EntrySize );
+ memset( p->pSimWords, 0, EntrySize );
+ k = 0;
+ Ivy_ManForEachObj( pManAig, pObj, i )
+ {
+ pSims = (Ivy_FraigSim_t *)(p->pSimWords + EntrySize * k++);
+ pSims->pNext = NULL;
+ if ( Ivy_ObjIsNode(pObj) )
+ {
+ if ( p->pSimStart == NULL )
+ p->pSimStart = pSims;
+ else
+ ((Ivy_FraigSim_t *)(p->pSimWords + EntrySize * (k-2)))->pNext = pSims;
+ pSims->pFanin0 = Ivy_ObjSim( Ivy_ObjFanin0(pObj) );
+ pSims->pFanin1 = Ivy_ObjSim( Ivy_ObjFanin1(pObj) );
+ pSims->Type = (Ivy_ObjFaninPhase(Ivy_ObjChild0(pObj)) << 2) | (Ivy_ObjFaninPhase(Ivy_ObjChild1(pObj)) << 1) | pObj->fPhase;
+ }
+ else
+ {
+ pSims->pFanin0 = NULL;
+ pSims->pFanin1 = NULL;
+ pSims->Type = 0;
+ }
+ Ivy_ObjSetSim( pObj, pSims );
+ }
+ assert( k == Ivy_ManObjNum(pManAig) );
+ // allocate storage for sim pattern
+ p->nPatWords = Ivy_BitWordNum( Ivy_ManPiNum(pManAig) );
+ p->pPatWords = ALLOC( unsigned, p->nPatWords );
+ p->pPatScores = ALLOC( int, 32 * p->nSimWords );
+ p->vPiVars = Vec_PtrAlloc( 100 );
+ // set random number generator
+ srand( 0xABCABC );
+ return p;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Stops the fraiging manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_FraigStop( Ivy_FraigMan_t * p )
+{
+ if ( p->pParams->fVerbose )
+ Ivy_FraigPrint( p );
+ if ( p->vPiVars ) Vec_PtrFree( p->vPiVars );
+ if ( p->pSat ) sat_solver_delete( p->pSat );
+ FREE( p->pPatScores );
+ FREE( p->pPatWords );
+ FREE( p->pSimWords );
+ free( p );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Prints stats for the fraiging manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_FraigPrint( Ivy_FraigMan_t * p )
+{
+ double nMemory;
+ nMemory = (double)Ivy_ManObjNum(p->pManAig)*p->nSimWords*sizeof(unsigned)/(1<<20);
+ printf( "SimWords = %d. Rounds = %d. Mem = %0.2f Mb. ", p->nSimWords, p->nSimRounds, nMemory );
+ printf( "Classes: Beg = %d. End = %d.\n", p->nClassesBeg, p->nClassesEnd );
+ printf( "Limits: BTNode = %d. BTMiter = %d.\n", p->pParams->nBTLimitNode, p->pParams->nBTLimitMiter );
+ printf( "Proof = %d. Counter-example = %d. Fail = %d. FailReal = %d. Zero = %d.\n",
+ p->nSatProof, p->nSatCallsSat, p->nSatFails, p->nSatFailsReal, p->nClassesZero );
+ printf( "Final = %d. Miter = %d. Total = %d. Mux = %d. (Exor = %d.) SatVars = %d.\n",
+ Ivy_ManNodeNum(p->pManFraig), p->nNodesMiter, Ivy_ManNodeNum(p->pManAig), 0, 0, p->nSatVars );
+ if ( p->pSat ) Sat_SolverPrintStats( stdout, p->pSat );
+ PRT( "AIG simulation ", p->timeSim );
+ PRT( "AIG traversal ", p->timeTrav );
+ PRT( "SAT solving ", p->timeSat );
+ PRT( " Unsat ", p->timeSatUnsat );
+ PRT( " Sat ", p->timeSatSat );
+ PRT( " Fail ", p->timeSatFail );
+ PRT( "Class refining ", p->timeRef );
+ PRT( "TOTAL RUNTIME ", p->timeTotal );
+ if ( p->time1 ) { PRT( "time1 ", p->time1 ); }
+}
+
+
+
+/**Function*************************************************************
+
+ Synopsis [Assigns random patterns to the PI node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_NodeAssignRandom( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj )
+{
+ Ivy_FraigSim_t * pSims;
+ int i;
+ assert( Ivy_ObjIsPi(pObj) );
+ pSims = Ivy_ObjSim(pObj);
+ for ( i = 0; i < p->nSimWords; i++ )
+ pSims->pData[i] = Ivy_ObjRandomSim();
+}
+
+/**Function*************************************************************
+
+ Synopsis [Assigns constant patterns to the PI node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_NodeAssignConst( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj, int fConst1 )
+{
+ Ivy_FraigSim_t * pSims;
+ int i;
+ assert( Ivy_ObjIsPi(pObj) );
+ pSims = Ivy_ObjSim(pObj);
+ for ( i = 0; i < p->nSimWords; i++ )
+ pSims->pData[i] = fConst1? ~(unsigned)0 : 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Assings random simulation info for the PIs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_FraigAssignRandom( Ivy_FraigMan_t * p )
+{
+ Ivy_Obj_t * pObj;
+ int i;
+ Ivy_ManForEachPi( p->pManAig, pObj, i )
+ Ivy_NodeAssignRandom( p, pObj );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Assings distance-1 simulation info for the PIs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_FraigAssignDist1( Ivy_FraigMan_t * p, unsigned * pPat )
+{
+ Ivy_Obj_t * pObj;
+ int i, Limit;
+ Ivy_ManForEachPi( p->pManAig, pObj, i )
+ Ivy_NodeAssignConst( p, pObj, Ivy_InfoHasBit(pPat, i) );
+ Limit = IVY_MIN( Ivy_ManPiNum(p->pManAig), p->nSimWords * 32 - 1 );
+ for ( i = 0; i < Limit; i++ )
+ Ivy_InfoXorBit( Ivy_ObjSim( Ivy_ManPi(p->pManAig,i) )->pData, i+1 );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns 1 if simulation info is composed of all zeros.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ivy_NodeHasZeroSim( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj )
+{
+ Ivy_FraigSim_t * pSims;
+ int i;
+ pSims = Ivy_ObjSim(pObj);
+ for ( i = 0; i < p->nSimWords; i++ )
+ if ( pSims->pData[i] )
+ return 0;
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns 1 if simulation info is composed of all zeros.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_NodeComplementSim( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj )
+{
+ Ivy_FraigSim_t * pSims;
+ int i;
+ pSims = Ivy_ObjSim(pObj);
+ for ( i = 0; i < p->nSimWords; i++ )
+ pSims->pData[i] = ~pSims->pData[i];
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns 1 if simulation infos are equal.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ivy_NodeCompareSims( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj0, Ivy_Obj_t * pObj1 )
+{
+ Ivy_FraigSim_t * pSims0, * pSims1;
+ int i;
+ pSims0 = Ivy_ObjSim(pObj0);
+ pSims1 = Ivy_ObjSim(pObj1);
+ for ( i = 0; i < p->nSimWords; i++ )
+ if ( pSims0->pData[i] != pSims1->pData[i] )
+ return 0;
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Simulates one node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_NodeSimulateSim( Ivy_FraigMan_t * p, Ivy_FraigSim_t * pSims )
+{
+ unsigned * pData, * pData0, * pData1;
+ int i;
+ pData = pSims->pData;
+ pData0 = pSims->pFanin0->pData;
+ pData1 = pSims->pFanin1->pData;
+ switch( pSims->Type )
+ {
+ case 0:
+ for ( i = 0; i < p->nSimWords; i++ )
+ pData[i] = (pData0[i] & pData1[i]);
+ break;
+ case 1:
+ for ( i = 0; i < p->nSimWords; i++ )
+ pData[i] = ~(pData0[i] & pData1[i]);
+ break;
+ case 2:
+ for ( i = 0; i < p->nSimWords; i++ )
+ pData[i] = (pData0[i] & ~pData1[i]);
+ break;
+ case 3:
+ for ( i = 0; i < p->nSimWords; i++ )
+ pData[i] = (~pData0[i] | pData1[i]);
+ break;
+ case 4:
+ for ( i = 0; i < p->nSimWords; i++ )
+ pData[i] = (~pData0[i] & pData1[i]);
+ break;
+ case 5:
+ for ( i = 0; i < p->nSimWords; i++ )
+ pData[i] = (pData0[i] | ~pData1[i]);
+ break;
+ case 6:
+ for ( i = 0; i < p->nSimWords; i++ )
+ pData[i] = ~(pData0[i] | pData1[i]);
+ break;
+ case 7:
+ for ( i = 0; i < p->nSimWords; i++ )
+ pData[i] = (pData0[i] | pData1[i]);
+ break;
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Simulates one node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_NodeSimulate( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj )
+{
+ Ivy_FraigSim_t * pSims, * pSims0, * pSims1;
+ int fCompl, fCompl0, fCompl1, i;
+ assert( !Ivy_IsComplement(pObj) );
+ // get hold of the simulation information
+ pSims = Ivy_ObjSim(pObj);
+ pSims0 = Ivy_ObjSim(Ivy_ObjFanin0(pObj));
+ pSims1 = Ivy_ObjSim(Ivy_ObjFanin1(pObj));
+ // get complemented attributes of the children using their random info
+ fCompl = pObj->fPhase;
+ fCompl0 = Ivy_ObjFaninPhase(Ivy_ObjChild0(pObj));
+ fCompl1 = Ivy_ObjFaninPhase(Ivy_ObjChild1(pObj));
+ // simulate
+ if ( fCompl0 && fCompl1 )
+ {
+ if ( fCompl )
+ for ( i = 0; i < p->nSimWords; i++ )
+ pSims->pData[i] = (pSims0->pData[i] | pSims1->pData[i]);
+ else
+ for ( i = 0; i < p->nSimWords; i++ )
+ pSims->pData[i] = ~(pSims0->pData[i] | pSims1->pData[i]);
+ }
+ else if ( fCompl0 && !fCompl1 )
+ {
+ if ( fCompl )
+ for ( i = 0; i < p->nSimWords; i++ )
+ pSims->pData[i] = (pSims0->pData[i] | ~pSims1->pData[i]);
+ else
+ for ( i = 0; i < p->nSimWords; i++ )
+ pSims->pData[i] = (~pSims0->pData[i] & pSims1->pData[i]);
+ }
+ else if ( !fCompl0 && fCompl1 )
+ {
+ if ( fCompl )
+ for ( i = 0; i < p->nSimWords; i++ )
+ pSims->pData[i] = (~pSims0->pData[i] | pSims1->pData[i]);
+ else
+ for ( i = 0; i < p->nSimWords; i++ )
+ pSims->pData[i] = (pSims0->pData[i] & ~pSims1->pData[i]);
+ }
+ else // if ( !fCompl0 && !fCompl1 )
+ {
+ if ( fCompl )
+ for ( i = 0; i < p->nSimWords; i++ )
+ pSims->pData[i] = ~(pSims0->pData[i] & pSims1->pData[i]);
+ else
+ for ( i = 0; i < p->nSimWords; i++ )
+ pSims->pData[i] = (pSims0->pData[i] & pSims1->pData[i]);
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes hash value using simulation info.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+unsigned Ivy_NodeHash( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj )
+{
+ static int s_FPrimes[128] = {
+ 1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459,
+ 1499, 1559, 1607, 1657, 1709, 1759, 1823, 1877, 1933, 1997,
+ 2039, 2089, 2141, 2213, 2269, 2311, 2371, 2411, 2467, 2543,
+ 2609, 2663, 2699, 2741, 2797, 2851, 2909, 2969, 3037, 3089,
+ 3169, 3221, 3299, 3331, 3389, 3461, 3517, 3557, 3613, 3671,
+ 3719, 3779, 3847, 3907, 3943, 4013, 4073, 4129, 4201, 4243,
+ 4289, 4363, 4441, 4493, 4549, 4621, 4663, 4729, 4793, 4871,
+ 4933, 4973, 5021, 5087, 5153, 5227, 5281, 5351, 5417, 5471,
+ 5519, 5573, 5651, 5693, 5749, 5821, 5861, 5923, 6011, 6073,
+ 6131, 6199, 6257, 6301, 6353, 6397, 6481, 6563, 6619, 6689,
+ 6737, 6803, 6863, 6917, 6977, 7027, 7109, 7187, 7237, 7309,
+ 7393, 7477, 7523, 7561, 7607, 7681, 7727, 7817, 7877, 7933,
+ 8011, 8039, 8059, 8081, 8093, 8111, 8123, 8147
+ };
+ Ivy_FraigSim_t * pSims;
+ unsigned uHash;
+ int i;
+ assert( p->nSimWords <= 128 );
+ uHash = 0;
+ pSims = Ivy_ObjSim(pObj);
+ for ( i = 0; i < p->nSimWords; i++ )
+ uHash ^= pSims->pData[i] * s_FPrimes[i];
+ return uHash;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Simulates AIG manager.]
+
+ Description [Assumes that the PI simulation info is attached.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_FraigSimulateOne( Ivy_FraigMan_t * p )
+{
+ Ivy_Obj_t * pObj;
+ int i, clk;
+clk = clock();
+ Ivy_ManForEachNode( p->pManAig, pObj, i )
+ {
+ Ivy_NodeSimulate( p, pObj );
+/*
+ if ( Ivy_ObjFraig(pObj) == NULL )
+ printf( "%3d --- -- %d : ", pObj->Id, pObj->fPhase );
+ else
+ printf( "%3d %3d %2d %d : ", pObj->Id, Ivy_Regular(Ivy_ObjFraig(pObj))->Id, Ivy_ObjSatNum(Ivy_Regular(Ivy_ObjFraig(pObj))), pObj->fPhase );
+ Extra_PrintBinary( stdout, Ivy_ObjSim(pObj), 30 );
+ printf( "\n" );
+*/
+ }
+p->timeSim += clock() - clk;
+p->nSimRounds++;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Simulates AIG manager.]
+
+ Description [Assumes that the PI simulation info is attached.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_FraigSimulateOneSim( Ivy_FraigMan_t * p )
+{
+ Ivy_FraigSim_t * pSims;
+ int clk;
+clk = clock();
+ for ( pSims = p->pSimStart; pSims; pSims = pSims->pNext )
+ Ivy_NodeSimulateSim( p, pSims );
+p->timeSim += clock() - clk;
+p->nSimRounds++;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Adds one node to the equivalence class.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_NodeAddToClass( Ivy_Obj_t * pClass, Ivy_Obj_t * pObj )
+{
+ if ( Ivy_ObjClassNodeNext(pClass) == NULL )
+ Ivy_ObjSetClassNodeNext( pClass, pObj );
+ else
+ Ivy_ObjSetClassNodeNext( Ivy_ObjClassNodeLast(pClass), pObj );
+ Ivy_ObjSetClassNodeLast( pClass, pObj );
+ Ivy_ObjSetClassNodeRepr( pObj, pClass );
+ Ivy_ObjSetClassNodeNext( pObj, NULL );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Adds equivalence class to the list of classes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_FraigAddClass( Ivy_FraigList_t * pList, Ivy_Obj_t * pClass )
+{
+ if ( pList->pHead == NULL )
+ {
+ pList->pHead = pClass;
+ pList->pTail = pClass;
+ Ivy_ObjSetEquivListPrev( pClass, NULL );
+ Ivy_ObjSetEquivListNext( pClass, NULL );
+ }
+ else
+ {
+ Ivy_ObjSetEquivListNext( pList->pTail, pClass );
+ Ivy_ObjSetEquivListPrev( pClass, pList->pTail );
+ Ivy_ObjSetEquivListNext( pClass, NULL );
+ pList->pTail = pClass;
+ }
+ pList->nItems++;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Updates the list of classes after base class has split.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_FraigInsertClass( Ivy_FraigList_t * pList, Ivy_Obj_t * pBase, Ivy_Obj_t * pClass )
+{
+ Ivy_ObjSetEquivListPrev( pClass, pBase );
+ Ivy_ObjSetEquivListNext( pClass, Ivy_ObjEquivListNext(pBase) );
+ if ( Ivy_ObjEquivListNext(pBase) )
+ Ivy_ObjSetEquivListPrev( Ivy_ObjEquivListNext(pBase), pClass );
+ Ivy_ObjSetEquivListNext( pBase, pClass );
+ if ( pList->pTail == pBase )
+ pList->pTail = pClass;
+ pList->nItems++;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Removes equivalence class from the list of classes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_FraigRemoveClass( Ivy_FraigList_t * pList, Ivy_Obj_t * pClass )
+{
+ if ( pList->pHead == pClass )
+ pList->pHead = Ivy_ObjEquivListNext(pClass);
+ if ( pList->pTail == pClass )
+ pList->pTail = Ivy_ObjEquivListPrev(pClass);
+ if ( Ivy_ObjEquivListPrev(pClass) )
+ Ivy_ObjSetEquivListNext( Ivy_ObjEquivListPrev(pClass), Ivy_ObjEquivListNext(pClass) );
+ if ( Ivy_ObjEquivListNext(pClass) )
+ Ivy_ObjSetEquivListPrev( Ivy_ObjEquivListNext(pClass), Ivy_ObjEquivListPrev(pClass) );
+ Ivy_ObjSetEquivListNext( pClass, NULL );
+ Ivy_ObjSetEquivListPrev( pClass, NULL );
+ pClass->fMarkA = 0;
+ pList->nItems--;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Count the number of pairs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ivy_FraigCountPairsClasses( Ivy_FraigMan_t * p )
+{
+ Ivy_Obj_t * pClass, * pNode;
+ int nPairs = 0, nNodes;
+ return nPairs;
+
+ Ivy_FraigForEachEquivClass( p->lClasses.pHead, pClass )
+ {
+ nNodes = 0;
+ Ivy_FraigForEachClassNode( pClass, pNode )
+ nNodes++;
+ nPairs += nNodes * (nNodes - 1) / 2;
+ }
+ return nPairs;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Creates initial simulation classes.]
+
+ Description [Assumes that simulation info is assigned.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_FraigCreateClasses( Ivy_FraigMan_t * p )
+{
+ Ivy_Obj_t ** pTable;
+ Ivy_Obj_t * pObj, * pConst1, * pBin, * pEntry;
+ int i, nTableSize;
+ unsigned Hash;
+ pConst1 = Ivy_ManConst1(p->pManAig);
+ // allocate the table
+ nTableSize = Ivy_ManObjNum(p->pManAig) / 2 + 13;
+ pTable = ALLOC( Ivy_Obj_t *, nTableSize );
+ memset( pTable, 0, sizeof(Ivy_Obj_t *) * nTableSize );
+ // collect nodes into the table
+ Ivy_ManForEachObj( p->pManAig, pObj, i )
+ {
+ if ( !Ivy_ObjIsPi(pObj) && !Ivy_ObjIsNode(pObj) )
+ continue;
+ Hash = Ivy_NodeHash( p, pObj );
+ if ( Hash == 0 && Ivy_NodeHasZeroSim( p, pObj ) )
+ {
+ Ivy_NodeAddToClass( pConst1, pObj );
+ continue;
+ }
+ // add the node to the table
+ pBin = pTable[Hash % nTableSize];
+ Ivy_FraigForEachBinNode( pBin, pEntry )
+ if ( Ivy_NodeCompareSims( p, pEntry, pObj ) )
+ {
+ Ivy_NodeAddToClass( pEntry, pObj );
+ break;
+ }
+ // check if the entry was added
+ if ( pEntry )
+ continue;
+ Ivy_ObjSetNodeHashNext( pObj, pBin );
+ pTable[Hash % nTableSize] = pObj;
+ }
+ // collect non-trivial classes
+ assert( p->lClasses.pHead == NULL );
+ Ivy_ManForEachObj( p->pManAig, pObj, i )
+ {
+ if ( !Ivy_ObjIsConst1(pObj) && !Ivy_ObjIsPi(pObj) && !Ivy_ObjIsNode(pObj) )
+ continue;
+ Ivy_ObjSetNodeHashNext( pObj, NULL );
+ if ( Ivy_ObjClassNodeRepr(pObj) == NULL )
+ {
+ assert( Ivy_ObjClassNodeNext(pObj) == NULL );
+ continue;
+ }
+ // recognize the head of the class
+ if ( Ivy_ObjClassNodeNext( Ivy_ObjClassNodeRepr(pObj) ) != NULL )
+ continue;
+ // clean the class representative and add it to the list
+ Ivy_ObjSetClassNodeRepr( pObj, NULL );
+ Ivy_FraigAddClass( &p->lClasses, pObj );
+ }
+ // free the table
+ free( pTable );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Recursively refines the class after simulation.]
+
+ Description [Returns 1 if the class has changed.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ivy_FraigRefineClass_rec( Ivy_FraigMan_t * p, Ivy_Obj_t * pClass )
+{
+ Ivy_Obj_t * pClassNew, * pListOld, * pListNew, * pNode;
+ int RetValue = 0;
+ // check if there is refinement
+ pListOld = pClass;
+ Ivy_FraigForEachClassNode( Ivy_ObjClassNodeNext(pClass), pClassNew )
+ {
+ if ( !Ivy_NodeCompareSims(p, pClass, pClassNew) )
+ {
+ if ( p->pParams->fPatScores )
+ Ivy_FraigAddToPatScores( p, pClass, pClassNew );
+ break;
+ }
+ pListOld = pClassNew;
+ }
+ if ( pClassNew == NULL )
+ return 0;
+ // set representative of the new class
+ Ivy_ObjSetClassNodeRepr( pClassNew, NULL );
+ // start the new list
+ pListNew = pClassNew;
+ // go through the remaining nodes and sort them into two groups:
+ // (1) matches of the old node; (2) non-matches of the old node
+ Ivy_FraigForEachClassNode( Ivy_ObjClassNodeNext(pClassNew), pNode )
+ if ( Ivy_NodeCompareSims( p, pClass, pNode ) )
+ {
+ Ivy_ObjSetClassNodeNext( pListOld, pNode );
+ pListOld = pNode;
+ }
+ else
+ {
+ Ivy_ObjSetClassNodeNext( pListNew, pNode );
+ Ivy_ObjSetClassNodeRepr( pNode, pClassNew );
+ pListNew = pNode;
+ }
+ // finish both lists
+ Ivy_ObjSetClassNodeNext( pListNew, NULL );
+ Ivy_ObjSetClassNodeNext( pListOld, NULL );
+ // update the list of classes
+ Ivy_FraigInsertClass( &p->lClasses, pClass, pClassNew );
+ // if the old class is trivial, remove it
+ if ( Ivy_ObjClassNodeNext(pClass) == NULL )
+ Ivy_FraigRemoveClass( &p->lClasses, pClass );
+ // if the new class is trivial, remove it; otherwise, try to refine it
+ if ( Ivy_ObjClassNodeNext(pClassNew) == NULL )
+ Ivy_FraigRemoveClass( &p->lClasses, pClassNew );
+ else
+ RetValue = Ivy_FraigRefineClass_rec( p, pClassNew );
+ return RetValue + 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Creates the counter-example from the successful pattern.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_FraigCheckOutputSimsSavePattern( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj )
+{
+ Ivy_FraigSim_t * pSims;
+ int i, k, BestPat, * pModel;
+ // find the word of the pattern
+ pSims = Ivy_ObjSim(pObj);
+ for ( i = 0; i < p->nSimWords; i++ )
+ if ( pSims->pData[i] )
+ break;
+ assert( i < p->nSimWords );
+ // find the bit of the pattern
+ for ( k = 0; k < 32; k++ )
+ if ( pSims->pData[i] & (1 << k) )
+ break;
+ assert( k < 32 );
+ // determine the best pattern
+ BestPat = i * 32 + k;
+ // fill in the counter-example data
+ pModel = ALLOC( int, Ivy_ManPiNum(p->pManFraig) );
+ Ivy_ManForEachPi( p->pManAig, pObj, i )
+ {
+ pModel[i] = Ivy_InfoHasBit(Ivy_ObjSim(pObj)->pData, BestPat);
+// printf( "%d", pModel[i] );
+ }
+// printf( "\n" );
+ // set the model
+ assert( p->pManFraig->pData == NULL );
+ p->pManFraig->pData = pModel;
+ return;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns 1 if the one of the output is already non-constant 0.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ivy_FraigCheckOutputSims( Ivy_FraigMan_t * p )
+{
+ Ivy_Obj_t * pObj;
+ int i;
+ // make sure the reference simulation pattern does not detect the bug
+ pObj = Ivy_ManPo( p->pManAig, 0 );
+ assert( Ivy_ObjFanin0(pObj)->fPhase == (unsigned)Ivy_ObjFaninC0(pObj) ); // Ivy_ObjFaninPhase(Ivy_ObjChild0(pObj)) == 0
+ Ivy_ManForEachPo( p->pManAig, pObj, i )
+ {
+ // complement simulation info
+// if ( Ivy_ObjFanin0(pObj)->fPhase ^ Ivy_ObjFaninC0(pObj) ) // Ivy_ObjFaninPhase(Ivy_ObjChild0(pObj))
+// Ivy_NodeComplementSim( p, Ivy_ObjFanin0(pObj) );
+ // check
+ if ( !Ivy_NodeHasZeroSim( p, Ivy_ObjFanin0(pObj) ) )
+ {
+ // create the counter-example from this pattern
+ Ivy_FraigCheckOutputSimsSavePattern( p, Ivy_ObjFanin0(pObj) );
+ return 1;
+ }
+ // complement simulation info
+// if ( Ivy_ObjFanin0(pObj)->fPhase ^ Ivy_ObjFaninC0(pObj) )
+// Ivy_NodeComplementSim( p, Ivy_ObjFanin0(pObj) );
+ }
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Refines the classes after simulation.]
+
+ Description [Assumes that simulation info is assigned. Returns the
+ number of classes refined.]
+
+ SideEffects [Large equivalence class of constant 0 may cause problems.]
+
+ SeeAlso []
+
+***********************************************************************/
+int Ivy_FraigRefineClasses( Ivy_FraigMan_t * p )
+{
+ Ivy_Obj_t * pClass, * pClass2;
+ int clk, RetValue, Counter = 0;
+ // check if some outputs already became non-constant
+ // this is a special case when computation can be stopped!!!
+ if ( p->pParams->fProve )
+ Ivy_FraigCheckOutputSims( p );
+ if ( p->pManFraig->pData )
+ return 0;
+ // refine the classed
+clk = clock();
+ Ivy_FraigForEachEquivClassSafe( p->lClasses.pHead, pClass, pClass2 )
+ {
+ if ( pClass->fMarkA )
+ continue;
+ RetValue = Ivy_FraigRefineClass_rec( p, pClass );
+ Counter += ( RetValue > 0 );
+//if ( Ivy_ObjIsConst1(pClass) )
+//printf( "%d ", RetValue );
+//if ( Ivy_ObjIsConst1(pClass) )
+// p->time1 += clock() - clk;
+ }
+p->timeRef += clock() - clk;
+ return Counter;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Print the class.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_FraigPrintClass( Ivy_Obj_t * pClass )
+{
+ Ivy_Obj_t * pObj;
+ printf( "Class {" );
+ Ivy_FraigForEachClassNode( pClass, pObj )
+ printf( " %d(%d)%c", pObj->Id, pObj->Level, pObj->fPhase? '+' : '-' );
+ printf( " }\n" );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Count the number of elements in the class.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ivy_FraigCountClassNodes( Ivy_Obj_t * pClass )
+{
+ Ivy_Obj_t * pObj;
+ int Counter = 0;
+ Ivy_FraigForEachClassNode( pClass, pObj )
+ Counter++;
+ return Counter;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Prints simulation classes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_FraigPrintSimClasses( Ivy_FraigMan_t * p )
+{
+ Ivy_Obj_t * pClass;
+ Ivy_FraigForEachEquivClass( p->lClasses.pHead, pClass )
+ {
+// Ivy_FraigPrintClass( pClass );
+ printf( "%d ", Ivy_FraigCountClassNodes( pClass ) );
+ }
+// printf( "\n" );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Generated const 0 pattern.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_FraigSavePattern0( Ivy_FraigMan_t * p )
+{
+ memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
+}
+
+/**Function*************************************************************
+
+ Synopsis [[Generated const 1 pattern.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_FraigSavePattern1( Ivy_FraigMan_t * p )
+{
+ memset( p->pPatWords, 0xff, sizeof(unsigned) * p->nPatWords );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Generates the counter-example satisfying the miter.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int * Ivy_FraigCreateModel( Ivy_FraigMan_t * p )
+{
+ int * pModel;
+ Ivy_Obj_t * pObj;
+ int i;
+ pModel = ALLOC( int, Ivy_ManPiNum(p->pManFraig) );
+ Ivy_ManForEachPi( p->pManFraig, pObj, i )
+ pModel[i] = ( p->pSat->model.ptr[Ivy_ObjSatNum(pObj)] == l_True );
+ return pModel;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Copy pattern from the solver into the internal storage.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_FraigSavePattern( Ivy_FraigMan_t * p )
+{
+ Ivy_Obj_t * pObj;
+ int i;
+ memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
+ Ivy_ManForEachPi( p->pManFraig, pObj, i )
+// Vec_PtrForEachEntry( p->vPiVars, pObj, i )
+ if ( p->pSat->model.ptr[Ivy_ObjSatNum(pObj)] == l_True )
+ Ivy_InfoSetBit( p->pPatWords, i );
+// Ivy_InfoSetBit( p->pPatWords, pObj->Id - 1 );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Copy pattern from the solver into the internal storage.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_FraigSavePattern2( Ivy_FraigMan_t * p )
+{
+ Ivy_Obj_t * pObj;
+ int i;
+ memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
+// Ivy_ManForEachPi( p->pManFraig, pObj, i )
+ Vec_PtrForEachEntry( p->vPiVars, pObj, i )
+ if ( p->pSat->model.ptr[Ivy_ObjSatNum(pObj)] == l_True )
+// Ivy_InfoSetBit( p->pPatWords, i );
+ Ivy_InfoSetBit( p->pPatWords, pObj->Id - 1 );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Copy pattern from the solver into the internal storage.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_FraigSavePattern3( Ivy_FraigMan_t * p )
+{
+ Ivy_Obj_t * pObj;
+ int i;
+ for ( i = 0; i < p->nPatWords; i++ )
+ p->pPatWords[i] = Ivy_ObjRandomSim();
+ Vec_PtrForEachEntry( p->vPiVars, pObj, i )
+ if ( Ivy_InfoHasBit( p->pPatWords, pObj->Id - 1 ) ^ (p->pSat->model.ptr[Ivy_ObjSatNum(pObj)] == l_True) )
+ Ivy_InfoXorBit( p->pPatWords, pObj->Id - 1 );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Performs simulation of the manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_FraigSimulate( Ivy_FraigMan_t * p )
+{
+ int nChanges, nClasses;
+ // start the classes
+ Ivy_FraigAssignRandom( p );
+ Ivy_FraigSimulateOne( p );
+ Ivy_FraigCreateClasses( p );
+//printf( "Starting classes = %5d. Pairs = %6d.\n", p->lClasses.nItems, Ivy_FraigCountPairsClasses(p) );
+ // refine classes by walking 0/1 patterns
+ Ivy_FraigSavePattern0( p );
+ Ivy_FraigAssignDist1( p, p->pPatWords );
+ Ivy_FraigSimulateOne( p );
+ nChanges = Ivy_FraigRefineClasses( p );
+ if ( p->pManFraig->pData )
+ return;
+//printf( "Refined classes = %5d. Changes = %4d. Pairs = %6d.\n", p->lClasses.nItems, nChanges, Ivy_FraigCountPairsClasses(p) );
+ Ivy_FraigSavePattern1( p );
+ Ivy_FraigAssignDist1( p, p->pPatWords );
+ Ivy_FraigSimulateOne( p );
+ nChanges = Ivy_FraigRefineClasses( p );
+ if ( p->pManFraig->pData )
+ return;
+//printf( "Refined classes = %5d. Changes = %4d. Pairs = %6d.\n", p->lClasses.nItems, nChanges, Ivy_FraigCountPairsClasses(p) );
+ // refine classes by random simulation
+ do {
+ Ivy_FraigAssignRandom( p );
+ Ivy_FraigSimulateOne( p );
+ nClasses = p->lClasses.nItems;
+ nChanges = Ivy_FraigRefineClasses( p );
+ if ( p->pManFraig->pData )
+ return;
+//printf( "Refined classes = %5d. Changes = %4d. Pairs = %6d.\n", p->lClasses.nItems, nChanges, Ivy_FraigCountPairsClasses(p) );
+ } while ( (double)nChanges / nClasses > p->pParams->dSimSatur );
+// Ivy_FraigPrintSimClasses( p );
+}
+
+
+
+/**Function*************************************************************
+
+ Synopsis [Cleans pattern scores.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_FraigCleanPatScores( Ivy_FraigMan_t * p )
+{
+ int i, nLimit = p->nSimWords * 32;
+ for ( i = 0; i < nLimit; i++ )
+ p->pPatScores[i] = 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Adds to pattern scores.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_FraigAddToPatScores( Ivy_FraigMan_t * p, Ivy_Obj_t * pClass, Ivy_Obj_t * pClassNew )
+{
+ Ivy_FraigSim_t * pSims0, * pSims1;
+ unsigned uDiff;
+ int i, w;
+ // get hold of the simulation information
+ pSims0 = Ivy_ObjSim(pClass);
+ pSims1 = Ivy_ObjSim(pClassNew);
+ // iterate through the differences and record the score
+ for ( w = 0; w < p->nSimWords; w++ )
+ {
+ uDiff = pSims0->pData[w] ^ pSims1->pData[w];
+ if ( uDiff == 0 )
+ continue;
+ for ( i = 0; i < 32; i++ )
+ if ( uDiff & ( 1 << i ) )
+ p->pPatScores[w*32+i]++;
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Selects the best pattern.]
+
+ Description [Returns 1 if such pattern is found.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ivy_FraigSelectBestPat( Ivy_FraigMan_t * p )
+{
+ Ivy_FraigSim_t * pSims;
+ Ivy_Obj_t * pObj;
+ int i, nLimit = p->nSimWords * 32, MaxScore = 0, BestPat = -1;
+ for ( i = 1; i < nLimit; i++ )
+ {
+ if ( MaxScore < p->pPatScores[i] )
+ {
+ MaxScore = p->pPatScores[i];
+ BestPat = i;
+ }
+ }
+ if ( MaxScore == 0 )
+ return 0;
+// if ( MaxScore > p->pParams->MaxScore )
+// printf( "Max score is %3d. ", MaxScore );
+ // copy the best pattern into the selected pattern
+ memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
+ Ivy_ManForEachPi( p->pManAig, pObj, i )
+ {
+ pSims = Ivy_ObjSim(pObj);
+ if ( Ivy_InfoHasBit(pSims->pData, BestPat) )
+ Ivy_InfoSetBit(p->pPatWords, i);
+ }
+ return MaxScore;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Resimulates fraiging manager after finding a counter-example.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_FraigResimulate( Ivy_FraigMan_t * p )
+{
+ int nChanges;
+ Ivy_FraigAssignDist1( p, p->pPatWords );
+ Ivy_FraigSimulateOne( p );
+ if ( p->pParams->fPatScores )
+ Ivy_FraigCleanPatScores( p );
+ nChanges = Ivy_FraigRefineClasses( p );
+ if ( p->pManFraig->pData )
+ return;
+ if ( nChanges < 1 )
+ printf( "Error: A counter-example did not refine classes!\n" );
+ assert( nChanges >= 1 );
+//printf( "Refined classes! = %5d. Changes = %4d.\n", p->lClasses.nItems, nChanges );
+
+ if ( !p->pParams->fPatScores )
+ return;
+
+ // perform additional simulation using dist1 patterns derived from successful patterns
+ while ( Ivy_FraigSelectBestPat(p) > p->pParams->MaxScore )
+ {
+ Ivy_FraigAssignDist1( p, p->pPatWords );
+ Ivy_FraigSimulateOne( p );
+ Ivy_FraigCleanPatScores( p );
+ nChanges = Ivy_FraigRefineClasses( p );
+ if ( p->pManFraig->pData )
+ return;
+//printf( "Refined class!!! = %5d. Changes = %4d. Pairs = %6d.\n", p->lClasses.nItems, nChanges, Ivy_FraigCountPairsClasses(p) );
+ if ( nChanges == 0 )
+ break;
+ }
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Prints the status of the miter.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_FraigMiterPrint( Ivy_Man_t * pNtk, char * pString, int clk, int fVerbose )
+{
+ if ( !fVerbose )
+ return;
+ printf( "Nodes = %7d. Levels = %4d. ", Ivy_ManNodeNum(pNtk), Ivy_ManLevels(pNtk) );
+ PRT( pString, clock() - clk );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Reports the status of the miter.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ivy_FraigMiterStatus( Ivy_Man_t * pMan )
+{
+ Ivy_Obj_t * pObj, * pObjNew;
+ int i, CountConst0 = 0, CountNonConst0 = 0, CountUndecided = 0;
+ if ( pMan->pData )
+ return 0;
+ Ivy_ManForEachPo( pMan, pObj, i )
+ {
+ pObjNew = Ivy_ObjChild0(pObj);
+ // check if the output is constant 1
+ if ( pObjNew == pMan->pConst1 )
+ {
+ CountNonConst0++;
+ continue;
+ }
+ // check if the output is constant 0
+ if ( pObjNew == Ivy_Not(pMan->pConst1) )
+ {
+ CountConst0++;
+ continue;
+ }
+ // check if the output can be constant 0
+ if ( Ivy_Regular(pObjNew)->fPhase != (unsigned)Ivy_IsComplement(pObjNew) )
+ {
+ CountNonConst0++;
+ continue;
+ }
+ CountUndecided++;
+ }
+/*
+ if ( p->pParams->fVerbose )
+ {
+ printf( "Miter has %d outputs. ", Ivy_ManPoNum(p->pManAig) );
+ printf( "Const0 = %d. ", CountConst0 );
+ printf( "NonConst0 = %d. ", CountNonConst0 );
+ printf( "Undecided = %d. ", CountUndecided );
+ printf( "\n" );
+ }
+*/
+ if ( CountNonConst0 )
+ return 0;
+ if ( CountUndecided )
+ return -1;
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Tries to prove each output of the miter until encountering a sat output.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_FraigMiterProve( Ivy_FraigMan_t * p )
+{
+ Ivy_Obj_t * pObj, * pObjNew;
+ int i, RetValue, clk = clock();
+ int fVerbose = 0;
+ Ivy_ManForEachPo( p->pManAig, pObj, i )
+ {
+ if ( i && fVerbose )
+ {
+ PRT( "Time", clock() -clk );
+ }
+ pObjNew = Ivy_ObjChild0Equiv(pObj);
+ // check if the output is constant 1
+ if ( pObjNew == p->pManFraig->pConst1 )
+ {
+ if ( fVerbose )
+ printf( "Output %2d (out of %2d) is constant 1. ", i, Ivy_ManPoNum(p->pManAig) );
+ // assing constant 0 model
+ p->pManFraig->pData = ALLOC( int, Ivy_ManPiNum(p->pManFraig) );
+ memset( p->pManFraig->pData, 0, sizeof(int) * Ivy_ManPiNum(p->pManFraig) );
+ break;
+ }
+ // check if the output is constant 0
+ if ( pObjNew == Ivy_Not(p->pManFraig->pConst1) )
+ {
+ if ( fVerbose )
+ printf( "Output %2d (out of %2d) is already constant 0. ", i, Ivy_ManPoNum(p->pManAig) );
+ continue;
+ }
+ // check if the output can be constant 0
+ if ( Ivy_Regular(pObjNew)->fPhase != (unsigned)Ivy_IsComplement(pObjNew) )
+ {
+ if ( fVerbose )
+ printf( "Output %2d (out of %2d) cannot be constant 0. ", i, Ivy_ManPoNum(p->pManAig) );
+ // assing constant 0 model
+ p->pManFraig->pData = ALLOC( int, Ivy_ManPiNum(p->pManFraig) );
+ memset( p->pManFraig->pData, 0, sizeof(int) * Ivy_ManPiNum(p->pManFraig) );
+ break;
+ }
+/*
+ // check the representative of this node
+ pRepr = Ivy_ObjClassNodeRepr(Ivy_ObjFanin0(pObj));
+ if ( Ivy_Regular(pRepr) != p->pManAig->pConst1 )
+ printf( "Representative is not constant 1.\n" );
+ else
+ printf( "Representative is constant 1.\n" );
+*/
+ // try to prove the output constant 0
+ RetValue = Ivy_FraigNodeIsConst( p, Ivy_Regular(pObjNew) );
+ if ( RetValue == 1 ) // proved equivalent
+ {
+ if ( fVerbose )
+ printf( "Output %2d (out of %2d) was proved constant 0. ", i, Ivy_ManPoNum(p->pManAig) );
+ // set the constant miter
+ Ivy_ObjFanin0(pObj)->pEquiv = Ivy_NotCond( p->pManFraig->pConst1, !Ivy_ObjFaninC0(pObj) );
+ continue;
+ }
+ if ( RetValue == -1 ) // failed
+ {
+ if ( fVerbose )
+ printf( "Output %2d (out of %2d) has timed out at %d backtracks. ", i, Ivy_ManPoNum(p->pManAig), p->pParams->nBTLimitMiter );
+ continue;
+ }
+ // proved satisfiable
+ if ( fVerbose )
+ printf( "Output %2d (out of %2d) was proved NOT a constant 0. ", i, Ivy_ManPoNum(p->pManAig) );
+ // create the model
+ p->pManFraig->pData = Ivy_FraigCreateModel(p);
+ break;
+ }
+ if ( fVerbose )
+ {
+ PRT( "Time", clock() -clk );
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs fraiging for the internal nodes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_FraigSweep( Ivy_FraigMan_t * p )
+{
+ Ivy_Obj_t * pObj;//, * pTemp;
+ int i, k = 0;
+p->nClassesZero = p->lClasses.pHead? (Ivy_ObjIsConst1(p->lClasses.pHead) ? Ivy_FraigCountClassNodes(p->lClasses.pHead) : 0) : 0;
+p->nClassesBeg = p->lClasses.nItems;
+ // duplicate internal nodes
+ p->pProgress = Extra_ProgressBarStart( stdout, Ivy_ManNodeNum(p->pManAig) );
+ Ivy_ManForEachNode( p->pManAig, pObj, i )
+ {
+ Extra_ProgressBarUpdate( p->pProgress, k++, NULL );
+ // default to simple strashing if simulation detected a counter-example for a PO
+ if ( p->pManFraig->pData )
+ pObj->pEquiv = Ivy_And( p->pManFraig, Ivy_ObjChild0Equiv(pObj), Ivy_ObjChild1Equiv(pObj) );
+ else
+ pObj->pEquiv = Ivy_FraigAnd( p, pObj );
+ assert( pObj->pEquiv != NULL );
+// pTemp = Ivy_Regular(pObj->pEquiv);
+// assert( Ivy_Regular(pObj->pEquiv)->Type );
+ }
+ Extra_ProgressBarStop( p->pProgress );
+p->nClassesEnd = p->lClasses.nItems;
+ // try to prove the outputs of the miter
+ p->nNodesMiter = Ivy_ManNodeNum(p->pManFraig);
+// Ivy_FraigMiterStatus( p->pManFraig );
+ if ( p->pParams->fProve && p->pManFraig->pData == NULL )
+ Ivy_FraigMiterProve( p );
+ // add the POs
+ Ivy_ManForEachPo( p->pManAig, pObj, i )
+ Ivy_ObjCreatePo( p->pManFraig, Ivy_ObjChild0Equiv(pObj) );
+ // clean the old manager
+ Ivy_ManForEachObj( p->pManAig, pObj, i )
+ pObj->pFanout = pObj->pNextFan0 = pObj->pNextFan1 = pObj->pPrevFan0 = pObj->pPrevFan1 = NULL;
+ // clean the new manager
+ Ivy_ManForEachObj( p->pManFraig, pObj, i )
+ {
+ if ( Ivy_ObjFaninVec(pObj) )
+ Vec_PtrFree( Ivy_ObjFaninVec(pObj) );
+ pObj->pNextFan0 = pObj->pNextFan1 = NULL;
+ }
+ // remove dangling nodes
+ Ivy_ManCleanup( p->pManFraig );
+ // clean up the class marks
+ Ivy_FraigForEachEquivClass( p->lClasses.pHead, pObj )
+ pObj->fMarkA = 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs fraiging for one node.]
+
+ Description [Returns the fraiged node.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Ivy_Obj_t * Ivy_FraigAnd( Ivy_FraigMan_t * p, Ivy_Obj_t * pObjOld )
+{
+ Ivy_Obj_t * pObjNew, * pFanin0New, * pFanin1New, * pObjReprNew;
+ int RetValue;
+ // get the fraiged fanins
+ pFanin0New = Ivy_ObjChild0Equiv(pObjOld);
+ pFanin1New = Ivy_ObjChild1Equiv(pObjOld);
+ // get the candidate fraig node
+ pObjNew = Ivy_And( p->pManFraig, pFanin0New, pFanin1New );
+ // get representative of this class
+ if ( Ivy_ObjClassNodeRepr(pObjOld) == NULL || // this is a unique node
+ (!p->pParams->fDoSparse && Ivy_ObjClassNodeRepr(pObjOld) == p->pManAig->pConst1) ) // this is a sparse node
+ {
+ assert( Ivy_Regular(pFanin0New) != Ivy_Regular(pFanin1New) );
+ assert( pObjNew != Ivy_Regular(pFanin0New) );
+ assert( pObjNew != Ivy_Regular(pFanin1New) );
+ return pObjNew;
+ }
+ // get the fraiged representative
+ pObjReprNew = Ivy_ObjFraig(Ivy_ObjClassNodeRepr(pObjOld));
+ // if the fraiged nodes are the same return
+ if ( Ivy_Regular(pObjNew) == Ivy_Regular(pObjReprNew) )
+ return pObjNew;
+ assert( Ivy_Regular(pObjNew) != Ivy_ManConst1(p->pManFraig) );
+ // they are different (the counter-example is in p->pPatWords)
+ RetValue = Ivy_FraigNodesAreEquiv( p, Ivy_Regular(pObjReprNew), Ivy_Regular(pObjNew) );
+ if ( RetValue == 1 ) // proved equivalent
+ {
+ // mark the class as proved
+ if ( Ivy_ObjClassNodeNext(pObjOld) == NULL )
+ Ivy_ObjClassNodeRepr(pObjOld)->fMarkA = 1;
+ return Ivy_NotCond( pObjReprNew, pObjOld->fPhase ^ Ivy_ObjClassNodeRepr(pObjOld)->fPhase );
+ }
+ if ( RetValue == -1 ) // failed
+ return pObjNew;
+ // simulate the counter-example and return the new node
+ Ivy_FraigResimulate( p );
+ return pObjNew;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Prints variable activity.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_FraigPrintActivity( Ivy_FraigMan_t * p )
+{
+ int i;
+ for ( i = 0; i < p->nSatVars; i++ )
+ printf( "%d %.3f ", i, p->pSat->activity[i] );
+ printf( "\n" );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Runs equivalence test for the two nodes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ivy_FraigNodesAreEquiv( Ivy_FraigMan_t * p, Ivy_Obj_t * pOld, Ivy_Obj_t * pNew )
+{
+ int pLits[4], RetValue, RetValue1, nBTLimit, clk, clk2 = clock();
+
+ // make sure the nodes are not complemented
+ assert( !Ivy_IsComplement(pNew) );
+ assert( !Ivy_IsComplement(pOld) );
+ assert( pNew != pOld );
+
+ // if at least one of the nodes is a failed node, perform adjustments:
+ // if the backtrack limit is small, simply skip this node
+ // if the backtrack limit is > 10, take the quare root of the limit
+ nBTLimit = p->pParams->nBTLimitNode;
+ if ( nBTLimit > 0 && (pOld->fFailTfo || pNew->fFailTfo) )
+ {
+ p->nSatFails++;
+ // fail immediately
+// return -1;
+ if ( nBTLimit <= 10 )
+ return -1;
+ nBTLimit = (int)pow(nBTLimit, 0.7);
+ }
+ p->nSatCalls++;
+
+ // make sure the solver is allocated and has enough variables
+ if ( p->pSat == NULL )
+ {
+ p->pSat = sat_solver_new();
+ p->nSatVars = 1;
+ sat_solver_setnvars( p->pSat, 1000 );
+ }
+
+ // if the nodes do not have SAT variables, allocate them
+ Ivy_FraigNodeAddToSolver( p, pOld, pNew );
+
+ // prepare variable activity
+ Ivy_FraigSetActivityFactors( p, pOld, pNew );
+
+ // solve under assumptions
+ // A = 1; B = 0 OR A = 1; B = 1
+clk = clock();
+ pLits[0] = toLitCond( Ivy_ObjSatNum(pOld), 0 );
+ pLits[1] = toLitCond( Ivy_ObjSatNum(pNew), pOld->fPhase == pNew->fPhase );
+//Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 );
+ RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2,
+ (sint64)nBTLimit, (sint64)0,
+ p->nBTLimitGlobal, p->nInsLimitGlobal );
+p->timeSat += clock() - clk;
+ if ( RetValue1 == l_False )
+ {
+p->timeSatUnsat += clock() - clk;
+ pLits[0] = lit_neg( pLits[0] );
+ pLits[1] = lit_neg( pLits[1] );
+ RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
+ assert( RetValue );
+ // continue solving the other implication
+ p->nSatCallsUnsat++;
+ }
+ else if ( RetValue1 == l_True )
+ {
+p->timeSatSat += clock() - clk;
+ Ivy_FraigSavePattern( p );
+ p->nSatCallsSat++;
+ return 0;
+ }
+ else // if ( RetValue1 == l_Undef )
+ {
+p->timeSatFail += clock() - clk;
+ // mark the node as the failed node
+ if ( pOld != p->pManFraig->pConst1 )
+ pOld->fFailTfo = 1;
+ pNew->fFailTfo = 1;
+ p->nSatFailsReal++;
+ return -1;
+ }
+
+ // if the old node was constant 0, we already know the answer
+ if ( pOld == p->pManFraig->pConst1 )
+ {
+ p->nSatProof++;
+ return 1;
+ }
+
+ // solve under assumptions
+ // A = 0; B = 1 OR A = 0; B = 0
+clk = clock();
+ pLits[0] = toLitCond( Ivy_ObjSatNum(pOld), 1 );
+ pLits[1] = toLitCond( Ivy_ObjSatNum(pNew), pOld->fPhase ^ pNew->fPhase );
+ RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2,
+ (sint64)nBTLimit, (sint64)0,
+ p->nBTLimitGlobal, p->nInsLimitGlobal );
+p->timeSat += clock() - clk;
+ if ( RetValue1 == l_False )
+ {
+p->timeSatUnsat += clock() - clk;
+ pLits[0] = lit_neg( pLits[0] );
+ pLits[1] = lit_neg( pLits[1] );
+ RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
+ assert( RetValue );
+ p->nSatCallsUnsat++;
+ }
+ else if ( RetValue1 == l_True )
+ {
+p->timeSatSat += clock() - clk;
+ Ivy_FraigSavePattern( p );
+ p->nSatCallsSat++;
+ return 0;
+ }
+ else // if ( RetValue1 == l_Undef )
+ {
+p->timeSatFail += clock() - clk;
+ // mark the node as the failed node
+ pOld->fFailTfo = 1;
+ pNew->fFailTfo = 1;
+ p->nSatFailsReal++;
+ return -1;
+ }
+/*
+ // check BDD proof
+ {
+ int RetVal;
+ PRT( "Sat", clock() - clk2 );
+ clk2 = clock();
+ RetVal = Ivy_FraigNodesAreEquivBdd( pOld, pNew );
+// printf( "%d ", RetVal );
+ assert( RetVal );
+ PRT( "Bdd", clock() - clk2 );
+ printf( "\n" );
+ }
+*/
+ // return SAT proof
+ p->nSatProof++;
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Runs equivalence test for one node.]
+
+ Description [Returns the fraiged node.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ivy_FraigNodeIsConst( Ivy_FraigMan_t * p, Ivy_Obj_t * pNew )
+{
+ int pLits[2], RetValue1, RetValue, clk;
+
+ // make sure the nodes are not complemented
+ assert( !Ivy_IsComplement(pNew) );
+ assert( pNew != p->pManFraig->pConst1 );
+ p->nSatCalls++;
+
+ // make sure the solver is allocated and has enough variables
+ if ( p->pSat == NULL )
+ {
+ p->pSat = sat_solver_new();
+ p->nSatVars = 1;
+ sat_solver_setnvars( p->pSat, 1000 );
+ }
+
+ // if the nodes do not have SAT variables, allocate them
+ Ivy_FraigNodeAddToSolver( p, NULL, pNew );
+
+ // prepare variable activity
+ Ivy_FraigSetActivityFactors( p, NULL, pNew );
+
+ // solve under assumptions
+clk = clock();
+ pLits[0] = toLitCond( Ivy_ObjSatNum(pNew), pNew->fPhase );
+ RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 1,
+ (sint64)p->pParams->nBTLimitMiter, (sint64)0,
+ p->nBTLimitGlobal, p->nInsLimitGlobal );
+p->timeSat += clock() - clk;
+ if ( RetValue1 == l_False )
+ {
+p->timeSatUnsat += clock() - clk;
+ pLits[0] = lit_neg( pLits[0] );
+ RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 1 );
+ assert( RetValue );
+ // continue solving the other implication
+ p->nSatCallsUnsat++;
+ }
+ else if ( RetValue1 == l_True )
+ {
+p->timeSatSat += clock() - clk;
+ if ( p->pPatWords )
+ Ivy_FraigSavePattern( p );
+ p->nSatCallsSat++;
+ return 0;
+ }
+ else // if ( RetValue1 == l_Undef )
+ {
+p->timeSatFail += clock() - clk;
+ // mark the node as the failed node
+ pNew->fFailTfo = 1;
+ p->nSatFailsReal++;
+ return -1;
+ }
+
+ // return SAT proof
+ p->nSatProof++;
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Addes clauses to the solver.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_FraigAddClausesMux( Ivy_FraigMan_t * p, Ivy_Obj_t * pNode )
+{
+ Ivy_Obj_t * pNodeI, * pNodeT, * pNodeE;
+ int pLits[4], RetValue, VarF, VarI, VarT, VarE, fCompT, fCompE;
+
+ assert( !Ivy_IsComplement( pNode ) );
+ assert( Ivy_ObjIsMuxType( pNode ) );
+ // get nodes (I = if, T = then, E = else)
+ pNodeI = Ivy_ObjRecognizeMux( pNode, &pNodeT, &pNodeE );
+ // get the variable numbers
+ VarF = Ivy_ObjSatNum(pNode);
+ VarI = Ivy_ObjSatNum(pNodeI);
+ VarT = Ivy_ObjSatNum(Ivy_Regular(pNodeT));
+ VarE = Ivy_ObjSatNum(Ivy_Regular(pNodeE));
+ // get the complementation flags
+ fCompT = Ivy_IsComplement(pNodeT);
+ fCompE = Ivy_IsComplement(pNodeE);
+
+ // f = ITE(i, t, e)
+
+ // i' + t' + f
+ // i' + t + f'
+ // i + e' + f
+ // i + e + f'
+
+ // create four clauses
+ pLits[0] = toLitCond(VarI, 1);
+ pLits[1] = toLitCond(VarT, 1^fCompT);
+ pLits[2] = toLitCond(VarF, 0);
+ RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
+ assert( RetValue );
+ pLits[0] = toLitCond(VarI, 1);
+ pLits[1] = toLitCond(VarT, 0^fCompT);
+ pLits[2] = toLitCond(VarF, 1);
+ RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
+ assert( RetValue );
+ pLits[0] = toLitCond(VarI, 0);
+ pLits[1] = toLitCond(VarE, 1^fCompE);
+ pLits[2] = toLitCond(VarF, 0);
+ RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
+ assert( RetValue );
+ pLits[0] = toLitCond(VarI, 0);
+ pLits[1] = toLitCond(VarE, 0^fCompE);
+ pLits[2] = toLitCond(VarF, 1);
+ RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
+ assert( RetValue );
+
+ // two additional clauses
+ // t' & e' -> f'
+ // t & e -> f
+
+ // t + e + f'
+ // t' + e' + f
+
+ if ( VarT == VarE )
+ {
+// assert( fCompT == !fCompE );
+ return;
+ }
+
+ pLits[0] = toLitCond(VarT, 0^fCompT);
+ pLits[1] = toLitCond(VarE, 0^fCompE);
+ pLits[2] = toLitCond(VarF, 1);
+ RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
+ assert( RetValue );
+ pLits[0] = toLitCond(VarT, 1^fCompT);
+ pLits[1] = toLitCond(VarE, 1^fCompE);
+ pLits[2] = toLitCond(VarF, 0);
+ RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
+ assert( RetValue );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Addes clauses to the solver.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_FraigAddClausesSuper( Ivy_FraigMan_t * p, Ivy_Obj_t * pNode, Vec_Ptr_t * vSuper )
+{
+ Ivy_Obj_t * pFanin;
+ int * pLits, nLits, RetValue, i;
+ assert( !Ivy_IsComplement(pNode) );
+ assert( Ivy_ObjIsNode( pNode ) );
+ // create storage for literals
+ nLits = Vec_PtrSize(vSuper) + 1;
+ pLits = ALLOC( int, nLits );
+ // suppose AND-gate is A & B = C
+ // add !A => !C or A + !C
+ Vec_PtrForEachEntry( vSuper, pFanin, i )
+ {
+ pLits[0] = toLitCond(Ivy_ObjSatNum(Ivy_Regular(pFanin)), Ivy_IsComplement(pFanin));
+ pLits[1] = toLitCond(Ivy_ObjSatNum(pNode), 1);
+ RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
+ assert( RetValue );
+ }
+ // add A & B => C or !A + !B + C
+ Vec_PtrForEachEntry( vSuper, pFanin, i )
+ pLits[i] = toLitCond(Ivy_ObjSatNum(Ivy_Regular(pFanin)), !Ivy_IsComplement(pFanin));
+ pLits[nLits-1] = toLitCond(Ivy_ObjSatNum(pNode), 0);
+ RetValue = sat_solver_addclause( p->pSat, pLits, pLits + nLits );
+ assert( RetValue );
+ free( pLits );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Collects the supergate.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_FraigCollectSuper_rec( Ivy_Obj_t * pObj, Vec_Ptr_t * vSuper, int fFirst, int fUseMuxes )
+{
+ // if the new node is complemented or a PI, another gate begins
+ if ( Ivy_IsComplement(pObj) || Ivy_ObjIsPi(pObj) || (!fFirst && Ivy_ObjRefs(pObj) > 1) ||
+ (fUseMuxes && Ivy_ObjIsMuxType(pObj)) )
+ {
+ Vec_PtrPushUnique( vSuper, pObj );
+ return;
+ }
+ // go through the branches
+ Ivy_FraigCollectSuper_rec( Ivy_ObjChild0(pObj), vSuper, 0, fUseMuxes );
+ Ivy_FraigCollectSuper_rec( Ivy_ObjChild1(pObj), vSuper, 0, fUseMuxes );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Collects the supergate.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Ptr_t * Ivy_FraigCollectSuper( Ivy_Obj_t * pObj, int fUseMuxes )
+{
+ Vec_Ptr_t * vSuper;
+ assert( !Ivy_IsComplement(pObj) );
+ assert( !Ivy_ObjIsPi(pObj) );
+ vSuper = Vec_PtrAlloc( 4 );
+ Ivy_FraigCollectSuper_rec( pObj, vSuper, 1, fUseMuxes );
+ return vSuper;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Updates the solver clause database.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_FraigObjAddToFrontier( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj, Vec_Ptr_t * vFrontier )
+{
+ assert( !Ivy_IsComplement(pObj) );
+ if ( Ivy_ObjSatNum(pObj) )
+ return;
+ assert( Ivy_ObjSatNum(pObj) == 0 );
+ assert( Ivy_ObjFaninVec(pObj) == NULL );
+ if ( Ivy_ObjIsConst1(pObj) )
+ return;
+//printf( "Assigning node %d number %d\n", pObj->Id, p->nSatVars );
+ Ivy_ObjSetSatNum( pObj, p->nSatVars++ );
+ if ( Ivy_ObjIsNode(pObj) )
+ Vec_PtrPush( vFrontier, pObj );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Updates the solver clause database.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_FraigNodeAddToSolver( Ivy_FraigMan_t * p, Ivy_Obj_t * pOld, Ivy_Obj_t * pNew )
+{
+ Vec_Ptr_t * vFrontier, * vFanins;
+ Ivy_Obj_t * pNode, * pFanin;
+ int i, k, fUseMuxes = 1;
+ assert( pOld || pNew );
+ // quit if CNF is ready
+ if ( (!pOld || Ivy_ObjFaninVec(pOld)) && (!pNew || Ivy_ObjFaninVec(pNew)) )
+ return;
+ // start the frontier
+ vFrontier = Vec_PtrAlloc( 100 );
+ if ( pOld ) Ivy_FraigObjAddToFrontier( p, pOld, vFrontier );
+ if ( pNew ) Ivy_FraigObjAddToFrontier( p, pNew, vFrontier );
+ // explore nodes in the frontier
+ Vec_PtrForEachEntry( vFrontier, pNode, i )
+ {
+ // create the supergate
+ assert( Ivy_ObjSatNum(pNode) );
+ assert( Ivy_ObjFaninVec(pNode) == NULL );
+ if ( fUseMuxes && Ivy_ObjIsMuxType(pNode) )
+ {
+ vFanins = Vec_PtrAlloc( 4 );
+ Vec_PtrPushUnique( vFanins, Ivy_ObjFanin0( Ivy_ObjFanin0(pNode) ) );
+ Vec_PtrPushUnique( vFanins, Ivy_ObjFanin0( Ivy_ObjFanin1(pNode) ) );
+ Vec_PtrPushUnique( vFanins, Ivy_ObjFanin1( Ivy_ObjFanin0(pNode) ) );
+ Vec_PtrPushUnique( vFanins, Ivy_ObjFanin1( Ivy_ObjFanin1(pNode) ) );
+ Vec_PtrForEachEntry( vFanins, pFanin, k )
+ Ivy_FraigObjAddToFrontier( p, Ivy_Regular(pFanin), vFrontier );
+ Ivy_FraigAddClausesMux( p, pNode );
+ }
+ else
+ {
+ vFanins = Ivy_FraigCollectSuper( pNode, fUseMuxes );
+ Vec_PtrForEachEntry( vFanins, pFanin, k )
+ Ivy_FraigObjAddToFrontier( p, Ivy_Regular(pFanin), vFrontier );
+ Ivy_FraigAddClausesSuper( p, pNode, vFanins );
+ }
+ assert( Vec_PtrSize(vFanins) > 1 );
+ Ivy_ObjSetFaninVec( pNode, vFanins );
+ }
+ Vec_PtrFree( vFrontier );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Sets variable activities in the cone.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ivy_FraigSetActivityFactors_rec( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj, int LevelMin, int LevelMax )
+{
+ Vec_Ptr_t * vFanins;
+ Ivy_Obj_t * pFanin;
+ int i, Counter = 0;
+ assert( !Ivy_IsComplement(pObj) );
+ assert( Ivy_ObjSatNum(pObj) );
+ // skip visited variables
+ if ( Ivy_ObjIsTravIdCurrent(p->pManFraig, pObj) )
+ return 0;
+ Ivy_ObjSetTravIdCurrent(p->pManFraig, pObj);
+ // add the PI to the list
+ if ( pObj->Level <= (unsigned)LevelMin || Ivy_ObjIsPi(pObj) )
+ return 0;
+ // set the factor of this variable
+ // (LevelMax-LevelMin) / (pObj->Level-LevelMin) = p->pParams->dActConeBumpMax / ThisBump
+ p->pSat->factors[Ivy_ObjSatNum(pObj)] = p->pParams->dActConeBumpMax * (pObj->Level - LevelMin)/(LevelMax - LevelMin);
+ veci_push(&p->pSat->act_vars, Ivy_ObjSatNum(pObj));
+ // explore the fanins
+ vFanins = Ivy_ObjFaninVec( pObj );
+ Vec_PtrForEachEntry( vFanins, pFanin, i )
+ Counter += Ivy_FraigSetActivityFactors_rec( p, Ivy_Regular(pFanin), LevelMin, LevelMax );
+ return 1 + Counter;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Sets variable activities in the cone.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ivy_FraigSetActivityFactors( Ivy_FraigMan_t * p, Ivy_Obj_t * pOld, Ivy_Obj_t * pNew )
+{
+ int clk, LevelMin, LevelMax;
+ assert( pOld || pNew );
+clk = clock();
+ // reset the active variables
+ veci_resize(&p->pSat->act_vars, 0);
+ // prepare for traversal
+ Ivy_ManIncrementTravId( p->pManFraig );
+ // determine the min and max level to visit
+ assert( p->pParams->dActConeRatio > 0 && p->pParams->dActConeRatio < 1 );
+ LevelMax = IVY_MAX( (pNew ? pNew->Level : 0), (pOld ? pOld->Level : 0) );
+ LevelMin = (int)(LevelMax * (1.0 - p->pParams->dActConeRatio));
+ // traverse
+ if ( pOld && !Ivy_ObjIsConst1(pOld) )
+ Ivy_FraigSetActivityFactors_rec( p, pOld, LevelMin, LevelMax );
+ if ( pNew && !Ivy_ObjIsConst1(pNew) )
+ Ivy_FraigSetActivityFactors_rec( p, pNew, LevelMin, LevelMax );
+//Ivy_FraigPrintActivity( p );
+p->timeTrav += clock() - clk;
+ return 1;
+}
+
+
+
+#include "cuddInt.h"
+
+/**Function*************************************************************
+
+ Synopsis [Checks equivalence using BDDs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+DdNode * Ivy_FraigNodesAreEquivBdd_int( DdManager * dd, DdNode * bFunc, Vec_Ptr_t * vFront, int Level )
+{
+ DdNode ** pFuncs;
+ DdNode * bFuncNew;
+ Vec_Ptr_t * vTemp;
+ Ivy_Obj_t * pObj, * pFanin;
+ int i, NewSize;
+ // create new frontier
+ vTemp = Vec_PtrAlloc( 100 );
+ Vec_PtrForEachEntry( vFront, pObj, i )
+ {
+ if ( (int)pObj->Level != Level )
+ {
+ pObj->fMarkB = 1;
+ pObj->TravId = Vec_PtrSize(vTemp);
+ Vec_PtrPush( vTemp, pObj );
+ continue;
+ }
+
+ pFanin = Ivy_ObjFanin0(pObj);
+ if ( pFanin->fMarkB == 0 )
+ {
+ pFanin->fMarkB = 1;
+ pFanin->TravId = Vec_PtrSize(vTemp);
+ Vec_PtrPush( vTemp, pFanin );
+ }
+
+ pFanin = Ivy_ObjFanin1(pObj);
+ if ( pFanin->fMarkB == 0 )
+ {
+ pFanin->fMarkB = 1;
+ pFanin->TravId = Vec_PtrSize(vTemp);
+ Vec_PtrPush( vTemp, pFanin );
+ }
+ }
+ // collect the permutation
+ NewSize = IVY_MAX(dd->size, Vec_PtrSize(vTemp));
+ pFuncs = ALLOC( DdNode *, NewSize );
+ Vec_PtrForEachEntry( vFront, pObj, i )
+ {
+ if ( (int)pObj->Level != Level )
+ pFuncs[i] = Cudd_bddIthVar( dd, pObj->TravId );
+ else
+ pFuncs[i] = Cudd_bddAnd( dd,
+ Cudd_NotCond( Cudd_bddIthVar(dd, Ivy_ObjFanin0(pObj)->TravId), Ivy_ObjFaninC0(pObj) ),
+ Cudd_NotCond( Cudd_bddIthVar(dd, Ivy_ObjFanin1(pObj)->TravId), Ivy_ObjFaninC1(pObj) ) );
+ Cudd_Ref( pFuncs[i] );
+ }
+ // add the remaining vars
+ assert( NewSize == dd->size );
+ for ( i = Vec_PtrSize(vFront); i < dd->size; i++ )
+ {
+ pFuncs[i] = Cudd_bddIthVar( dd, i );
+ Cudd_Ref( pFuncs[i] );
+ }
+
+ // create new
+ bFuncNew = Cudd_bddVectorCompose( dd, bFunc, pFuncs ); Cudd_Ref( bFuncNew );
+ // clean trav Id
+ Vec_PtrForEachEntry( vTemp, pObj, i )
+ {
+ pObj->fMarkB = 0;
+ pObj->TravId = 0;
+ }
+ // deref
+ for ( i = 0; i < dd->size; i++ )
+ Cudd_RecursiveDeref( dd, pFuncs[i] );
+ free( pFuncs );
+
+ free( vFront->pArray );
+ *vFront = *vTemp;
+
+ vTemp->nCap = vTemp->nSize = 0;
+ vTemp->pArray = NULL;
+ Vec_PtrFree( vTemp );
+
+ Cudd_Deref( bFuncNew );
+ return bFuncNew;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Checks equivalence using BDDs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ivy_FraigNodesAreEquivBdd( Ivy_Obj_t * pObj1, Ivy_Obj_t * pObj2 )
+{
+ static DdManager * dd = NULL;
+ DdNode * bFunc, * bTemp;
+ Vec_Ptr_t * vFront;
+ Ivy_Obj_t * pObj;
+ int i, RetValue, Iter, Level;
+ // start the manager
+ if ( dd == NULL )
+ dd = Cudd_Init( 50, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
+ // create front
+ vFront = Vec_PtrAlloc( 100 );
+ Vec_PtrPush( vFront, pObj1 );
+ Vec_PtrPush( vFront, pObj2 );
+ // get the function
+ bFunc = Cudd_bddXor( dd, Cudd_bddIthVar(dd,0), Cudd_bddIthVar(dd,1) ); Cudd_Ref( bFunc );
+ bFunc = Cudd_NotCond( bFunc, pObj1->fPhase != pObj2->fPhase );
+ // try running BDDs
+ for ( Iter = 0; ; Iter++ )
+ {
+ // find max level
+ Level = 0;
+ Vec_PtrForEachEntry( vFront, pObj, i )
+ if ( Level < (int)pObj->Level )
+ Level = (int)pObj->Level;
+ if ( Level == 0 )
+ break;
+ bFunc = Ivy_FraigNodesAreEquivBdd_int( dd, bTemp = bFunc, vFront, Level ); Cudd_Ref( bFunc );
+ Cudd_RecursiveDeref( dd, bTemp );
+ if ( bFunc == Cudd_ReadLogicZero(dd) ) // proved
+ {printf( "%d", Iter ); break;}
+ if ( Cudd_DagSize(bFunc) > 1000 )
+ {printf( "b" ); break;}
+ if ( dd->size > 120 )
+ {printf( "s" ); break;}
+ if ( Iter > 50 )
+ {printf( "i" ); break;}
+ }
+ if ( bFunc == Cudd_ReadLogicZero(dd) ) // unsat
+ RetValue = 1;
+ else if ( Level == 0 ) // sat
+ RetValue = 0;
+ else
+ RetValue = -1; // spaceout/timeout
+ Cudd_RecursiveDeref( dd, bFunc );
+ Vec_PtrFree( vFront );
+ return RetValue;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/fra/module.make b/src/aig/fra/module.make
new file mode 100644
index 00000000..934fbdac
--- /dev/null
+++ b/src/aig/fra/module.make
@@ -0,0 +1,7 @@
+SRC += src/aig/fra/fraAnd.c \
+ src/aig/fra/fraClass.c \
+ src/aig/fra/fraCnf.c \
+ src/aig/fra/fraCore.c \
+ src/aig/fra/fraMan.c \
+ src/aig/fra/fraSat.c \
+ src/aig/fra/fraSim.c