summaryrefslogtreecommitdiffstats
path: root/src/aig
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig')
-rw-r--r--src/aig/aig/aig.h54
-rw-r--r--src/aig/aig/aigCuts.c669
-rw-r--r--src/aig/cnf/cnfCore.c2
-rw-r--r--src/aig/dar/dar.h2
-rw-r--r--src/aig/dar/darCore.c49
-rw-r--r--src/aig/dar/darCut.c41
-rw-r--r--src/aig/dar/darInt.h1
-rw-r--r--src/aig/fra/fraClaus.c498
8 files changed, 1245 insertions, 71 deletions
diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index e871373a..5bff39f7 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -137,6 +137,7 @@ struct Aig_Man_t_
void (*pImpFunc) (void*, void*); // implication checking precedure
void * pImpData; // implication checking data
void * pManTime; // the timing manager
+ void * pManCuts;
Vec_Ptr_t * vMapped;
Vec_Int_t * vFlopNums;
void * pSeqModel;
@@ -146,6 +147,56 @@ struct Aig_Man_t_
int time2;
};
+// cut computation
+typedef struct Aig_ManCut_t_ Aig_ManCut_t;
+typedef struct Aig_Cut_t_ Aig_Cut_t;
+
+// the cut used to represent node in the AIG
+struct Aig_Cut_t_
+{
+ Aig_Cut_t * pNext; // the next cut in the table
+ int Cost; // the cost of the cut
+ unsigned uSign; // cut signature
+ int iNode; // the node, for which it is the cut
+ short nCutSize; // the number of bytes in the cut
+ char nLeafMax; // the maximum number of fanins
+ char nFanins; // the current number of fanins
+ int pFanins[0]; // the fanins (followed by the truth table)
+};
+
+// the CNF computation manager
+struct Aig_ManCut_t_
+{
+ // AIG manager
+ Aig_Man_t * pAig; // the input AIG manager
+ Aig_Cut_t ** pCuts; // the cuts for each node in the output manager
+ // parameters
+ int nCutsMax; // the max number of cuts at the node
+ int nLeafMax; // the max number of leaves of a cut
+ int fTruth; // enables truth table computation
+ int fVerbose; // enables verbose output
+ // internal variables
+ int nCutSize; // the number of bytes needed to store one cut
+ int nTruthWords; // the number of truth table words
+ Aig_MmFixed_t * pMemCuts; // memory manager for cuts
+ unsigned * puTemp[4]; // used for the truth table computation
+};
+
+static inline Aig_Cut_t * Aig_ObjCuts( Aig_ManCut_t * p, Aig_Obj_t * pObj ) { return p->pCuts[pObj->Id]; }
+static inline void Aig_ObjSetCuts( Aig_ManCut_t * p, Aig_Obj_t * pObj, Aig_Cut_t * pCuts ) { p->pCuts[pObj->Id] = pCuts; }
+
+static inline int Aig_CutLeaveNum( Aig_Cut_t * pCut ) { return pCut->nFanins; }
+static inline int * Aig_CutLeaves( Aig_Cut_t * pCut ) { return pCut->pFanins; }
+static inline unsigned * Aig_CutTruth( Aig_Cut_t * pCut ) { return (unsigned *)(pCut->pFanins + pCut->nLeafMax); }
+static inline Aig_Cut_t * Aig_CutNext( Aig_Cut_t * pCut ) { return (Aig_Cut_t *)(((char *)pCut) + pCut->nCutSize); }
+
+// iterator over cuts of the node
+#define Aig_ObjForEachCut( p, pObj, pCut, i ) \
+ for ( i = 0, pCut = Aig_ObjCuts(p, pObj); i < p->nCutsMax; i++, pCut = Aig_CutNext(pCut) )
+// iterator over leaves of the cut
+#define Aig_CutForEachLeaf( p, pCut, pLeaf, i ) \
+ for ( i = 0; (i < (int)(pCut)->nFanins) && ((pLeaf) = Aig_ManObj(p, (pCut)->pFanins[i])); i++ )
+
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
@@ -386,6 +437,9 @@ static inline int Aig_ObjFanoutNext( Aig_Man_t * p, int iFan ) { assert(iF
extern int Aig_ManCheck( Aig_Man_t * p );
extern void Aig_ManCheckMarkA( Aig_Man_t * p );
extern void Aig_ManCheckPhase( Aig_Man_t * p );
+/*=== aigCuts.c ========================================================*/
+extern Aig_ManCut_t * Aig_ComputeCuts( Aig_Man_t * pAig, int nCutsMax, int nLeafMax, int fTruth, int fVerbose );
+extern void Aig_ManCutStop( Aig_ManCut_t * p );
/*=== aigDfs.c ==========================================================*/
extern Vec_Ptr_t * Aig_ManDfs( Aig_Man_t * p );
extern Vec_Ptr_t * Aig_ManDfsPio( Aig_Man_t * p );
diff --git a/src/aig/aig/aigCuts.c b/src/aig/aig/aigCuts.c
new file mode 100644
index 00000000..494d0d5b
--- /dev/null
+++ b/src/aig/aig/aigCuts.c
@@ -0,0 +1,669 @@
+/**CFile****************************************************************
+
+ FileName [aigCuts.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [AIG package.]
+
+ Synopsis [Computation of K-feasible priority cuts.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - April 28, 2007.]
+
+ Revision [$Id: aigCuts.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.h"
+#include "kit.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Starts the cut sweeping manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_ManCut_t * Aig_ManCutStart( Aig_Man_t * pMan, int nCutsMax, int nLeafMax, int fTruth, int fVerbose )
+{
+ Aig_ManCut_t * p;
+ assert( nCutsMax >= 2 );
+ assert( nLeafMax <= 16 );
+ // allocate the fraiging manager
+ p = ALLOC( Aig_ManCut_t, 1 );
+ memset( p, 0, sizeof(Aig_ManCut_t) );
+ p->nCutsMax = nCutsMax;
+ p->nLeafMax = nLeafMax;
+ p->fTruth = fTruth;
+ p->fVerbose = fVerbose;
+ p->pAig = pMan;
+ // allocate room for cuts and equivalent nodes
+ p->pCuts = ALLOC( Aig_Cut_t *, Aig_ManObjNumMax(pMan) );
+ memset( p->pCuts, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(pMan) );
+ // allocate memory manager
+ p->nTruthWords = Aig_TruthWordNum(nLeafMax);
+ p->nCutSize = sizeof(Aig_Cut_t) + sizeof(int) * nLeafMax + fTruth * sizeof(unsigned) * p->nTruthWords;
+ p->pMemCuts = Aig_MmFixedStart( p->nCutSize * p->nCutsMax, 512 );
+ // room for temporary truth tables
+ if ( fTruth )
+ {
+ p->puTemp[0] = ALLOC( unsigned, 4 * p->nTruthWords );
+ p->puTemp[1] = p->puTemp[0] + p->nTruthWords;
+ p->puTemp[2] = p->puTemp[1] + p->nTruthWords;
+ p->puTemp[3] = p->puTemp[2] + p->nTruthWords;
+ }
+ return p;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Stops the fraiging manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Aig_ManCutStop( Aig_ManCut_t * p )
+{
+ Aig_MmFixedStop( p->pMemCuts, 0 );
+ FREE( p->puTemp[0] );
+ free( p->pCuts );
+ free( p );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Prints one cut.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Aig_CutPrint( Aig_Cut_t * pCut )
+{
+ int i;
+ printf( "{" );
+ for ( i = 0; i < pCut->nFanins; i++ )
+ printf( " %d", pCut->pFanins[i] );
+ printf( " }\n" );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Prints one cut.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Aig_ObjCutPrint( Aig_ManCut_t * p, Aig_Obj_t * pObj )
+{
+ Aig_Cut_t * pCut;
+ int i;
+ printf( "Cuts for node %d:\n", pObj->Id );
+ Aig_ObjForEachCut( p, pObj, pCut, i )
+ if ( pCut->nFanins )
+ Aig_CutPrint( pCut );
+// printf( "\n" );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes the total number of cuts.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Aig_ManCutCount( Aig_ManCut_t * p, int * pnCutsK )
+{
+ Aig_Cut_t * pCut;
+ Aig_Obj_t * pObj;
+ int i, k, nCuts = 0, nCutsK = 0;
+ Aig_ManForEachNode( p->pAig, pObj, i )
+ Aig_ObjForEachCut( p, pObj, pCut, k )
+ {
+ if ( pCut->nFanins == 0 )
+ continue;
+ nCuts++;
+ if ( pCut->nFanins == p->nLeafMax )
+ nCutsK++;
+ }
+ if ( pnCutsK )
+ *pnCutsK = nCutsK;
+ return nCuts;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Compute the cost of the cut.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Aig_CutFindCost( Aig_ManCut_t * p, Aig_Cut_t * pCut )
+{
+ Aig_Obj_t * pLeaf;
+ int i, Cost = 0;
+ assert( pCut->nFanins > 0 );
+ Aig_CutForEachLeaf( p->pAig, pCut, pLeaf, i )
+ Cost += pLeaf->nRefs;
+ return Cost * 1000 / pCut->nFanins;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Compute the cost of the cut.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline float Aig_CutFindCost2( Aig_ManCut_t * p, Aig_Cut_t * pCut )
+{
+ Aig_Obj_t * pLeaf;
+ float Cost = 0.0;
+ int i;
+ assert( pCut->nFanins > 0 );
+ Aig_CutForEachLeaf( p->pAig, pCut, pLeaf, i )
+ Cost += (float)1.0/pLeaf->nRefs;
+ return 1/Cost;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns the next free cut to use.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline Aig_Cut_t * Aig_CutFindFree( Aig_ManCut_t * p, Aig_Obj_t * pObj )
+{
+ Aig_Cut_t * pCut, * pCutMax;
+ int i;
+ pCutMax = NULL;
+ Aig_ObjForEachCut( p, pObj, pCut, i )
+ {
+ if ( pCut->nFanins == 0 )
+ return pCut;
+ if ( pCutMax == NULL || pCutMax->Cost < pCut->Cost )
+ pCutMax = pCut;
+ }
+ assert( pCutMax != NULL );
+ pCutMax->nFanins = 0;
+ return pCutMax;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes the stretching phase of the cut w.r.t. the merged cut.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline unsigned Aig_CutTruthPhase( Aig_Cut_t * pCut, Aig_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 [Performs truth table computation.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+unsigned * Aig_CutComputeTruth( Aig_ManCut_t * p, Aig_Cut_t * pCut, Aig_Cut_t * pCut0, Aig_Cut_t * pCut1, int fCompl0, int fCompl1 )
+{
+ // permute the first table
+ if ( fCompl0 )
+ Kit_TruthNot( p->puTemp[0], Aig_CutTruth(pCut0), p->nLeafMax );
+ else
+ Kit_TruthCopy( p->puTemp[0], Aig_CutTruth(pCut0), p->nLeafMax );
+ Kit_TruthStretch( p->puTemp[2], p->puTemp[0], pCut0->nFanins, p->nLeafMax, Aig_CutTruthPhase(pCut, pCut0), 0 );
+ // permute the second table
+ if ( fCompl1 )
+ Kit_TruthNot( p->puTemp[1], Aig_CutTruth(pCut1), p->nLeafMax );
+ else
+ Kit_TruthCopy( p->puTemp[1], Aig_CutTruth(pCut1), p->nLeafMax );
+ Kit_TruthStretch( p->puTemp[3], p->puTemp[1], pCut1->nFanins, p->nLeafMax, Aig_CutTruthPhase(pCut, pCut1), 0 );
+ // produce the resulting table
+ Kit_TruthAnd( Aig_CutTruth(pCut), p->puTemp[2], p->puTemp[3], p->nLeafMax );
+// assert( pCut->nFanins >= Kit_TruthSupportSize( Aig_CutTruth(pCut), p->nLeafMax ) );
+ return Aig_CutTruth(pCut);
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs support minimization for the truth table.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Aig_CutSupportMinimize( Aig_ManCut_t * p, Aig_Cut_t * pCut )
+{
+ unsigned * pTruth;
+ int uSupp, nFansNew, i, k;
+ // get truth table
+ pTruth = Aig_CutTruth( pCut );
+ // get support
+ uSupp = Kit_TruthSupport( pTruth, p->nLeafMax );
+ // get the new support size
+ nFansNew = Kit_WordCountOnes( uSupp );
+ // check if there are redundant variables
+ if ( nFansNew == pCut->nFanins )
+ return nFansNew;
+ assert( nFansNew < pCut->nFanins );
+ // minimize support
+ Kit_TruthShrink( p->puTemp[0], pTruth, nFansNew, p->nLeafMax, uSupp, 1 );
+ for ( i = k = 0; i < pCut->nFanins; i++ )
+ if ( uSupp & (1 << i) )
+ pCut->pFanins[k++] = pCut->pFanins[i];
+ assert( k == nFansNew );
+ pCut->nFanins = nFansNew;
+// assert( nFansNew == Kit_TruthSupportSize( pTruth, p->nLeafMax ) );
+//Extra_PrintBinary( stdout, pTruth, (1<<p->nLeafMax) ); printf( "\n" );
+ return nFansNew;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns 1 if pDom is contained in pCut.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Aig_CutCheckDominance( Aig_Cut_t * pDom, Aig_Cut_t * pCut )
+{
+ int i, k;
+ for ( i = 0; i < (int)pDom->nFanins; i++ )
+ {
+ for ( k = 0; k < (int)pCut->nFanins; k++ )
+ if ( pDom->pFanins[i] == pCut->pFanins[k] )
+ break;
+ if ( k == (int)pCut->nFanins ) // node i in pDom is not contained in pCut
+ return 0;
+ }
+ // every node in pDom is contained in pCut
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns 1 if the cut is contained.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Aig_CutFilter( Aig_ManCut_t * p, Aig_Obj_t * pObj, Aig_Cut_t * pCut )
+{
+ Aig_Cut_t * pTemp;
+ int i;
+ // go through the cuts of the node
+ Aig_ObjForEachCut( p, pObj, pTemp, i )
+ {
+ if ( pTemp->nFanins < 2 )
+ continue;
+ if ( pTemp == pCut )
+ continue;
+ if ( pTemp->nFanins > pCut->nFanins )
+ {
+ // skip the non-contained cuts
+ if ( (pTemp->uSign & pCut->uSign) != pCut->uSign )
+ continue;
+ // check containment seriously
+ if ( Aig_CutCheckDominance( pCut, pTemp ) )
+ {
+ // remove contained cut
+ pTemp->nFanins = 0;
+ }
+ }
+ else
+ {
+ // skip the non-contained cuts
+ if ( (pTemp->uSign & pCut->uSign) != pTemp->uSign )
+ continue;
+ // check containment seriously
+ if ( Aig_CutCheckDominance( pTemp, pCut ) )
+ {
+ // remove the given
+ pCut->nFanins = 0;
+ return 1;
+ }
+ }
+ }
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Merges two cuts.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Aig_CutMergeOrdered( Aig_ManCut_t * p, Aig_Cut_t * pC0, Aig_Cut_t * pC1, Aig_Cut_t * pC )
+{
+ int i, k, c;
+ assert( pC0->nFanins >= pC1->nFanins );
+ // the case of the largest cut sizes
+ if ( pC0->nFanins == p->nLeafMax && pC1->nFanins == p->nLeafMax )
+ {
+ for ( i = 0; i < pC0->nFanins; i++ )
+ if ( pC0->pFanins[i] != pC1->pFanins[i] )
+ return 0;
+ for ( i = 0; i < pC0->nFanins; i++ )
+ pC->pFanins[i] = pC0->pFanins[i];
+ pC->nFanins = pC0->nFanins;
+ return 1;
+ }
+ // the case when one of the cuts is the largest
+ if ( pC0->nFanins == p->nLeafMax )
+ {
+ for ( i = 0; i < pC1->nFanins; i++ )
+ {
+ for ( k = pC0->nFanins - 1; k >= 0; k-- )
+ if ( pC0->pFanins[k] == pC1->pFanins[i] )
+ break;
+ if ( k == -1 ) // did not find
+ return 0;
+ }
+ for ( i = 0; i < pC0->nFanins; i++ )
+ pC->pFanins[i] = pC0->pFanins[i];
+ pC->nFanins = pC0->nFanins;
+ return 1;
+ }
+
+ // compare two cuts with different numbers
+ i = k = 0;
+ for ( c = 0; c < p->nLeafMax; c++ )
+ {
+ if ( k == pC1->nFanins )
+ {
+ if ( i == pC0->nFanins )
+ {
+ pC->nFanins = c;
+ return 1;
+ }
+ pC->pFanins[c] = pC0->pFanins[i++];
+ continue;
+ }
+ if ( i == pC0->nFanins )
+ {
+ if ( k == pC1->nFanins )
+ {
+ pC->nFanins = c;
+ return 1;
+ }
+ pC->pFanins[c] = pC1->pFanins[k++];
+ continue;
+ }
+ if ( pC0->pFanins[i] < pC1->pFanins[k] )
+ {
+ pC->pFanins[c] = pC0->pFanins[i++];
+ continue;
+ }
+ if ( pC0->pFanins[i] > pC1->pFanins[k] )
+ {
+ pC->pFanins[c] = pC1->pFanins[k++];
+ continue;
+ }
+ pC->pFanins[c] = pC0->pFanins[i++];
+ k++;
+ }
+ if ( i < pC0->nFanins || k < pC1->nFanins )
+ return 0;
+ pC->nFanins = c;
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Prepares the object for FPGA mapping.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Aig_CutMerge( Aig_ManCut_t * p, Aig_Cut_t * pCut0, Aig_Cut_t * pCut1, Aig_Cut_t * pCut )
+{
+ assert( p->nLeafMax > 0 );
+ // merge the nodes
+ if ( pCut0->nFanins < pCut1->nFanins )
+ {
+ if ( !Aig_CutMergeOrdered( p, pCut1, pCut0, pCut ) )
+ return 0;
+ }
+ else
+ {
+ if ( !Aig_CutMergeOrdered( p, pCut0, pCut1, pCut ) )
+ return 0;
+ }
+ pCut->uSign = pCut0->uSign | pCut1->uSign;
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Cut_t * Aig_ObjPrepareCuts( Aig_ManCut_t * p, Aig_Obj_t * pObj, int fTriv )
+{
+ Aig_Cut_t * pCutSet, * pCut;
+ int i;
+ // create the cutset of the node
+ pCutSet = (Aig_Cut_t *)Aig_MmFixedEntryFetch( p->pMemCuts );
+ Aig_ObjSetCuts( p, pObj, pCutSet );
+ Aig_ObjForEachCut( p, pObj, pCut, i )
+ {
+ pCut->nFanins = 0;
+ pCut->iNode = pObj->Id;
+ pCut->nCutSize = p->nCutSize;
+ pCut->nLeafMax = p->nLeafMax;
+ }
+ // add unit cut if needed
+ if ( fTriv )
+ {
+ pCut = pCutSet;
+ pCut->Cost = 0;
+ pCut->iNode = pObj->Id;
+ pCut->nFanins = 1;
+ pCut->pFanins[0] = pObj->Id;
+ pCut->uSign = Aig_ObjCutSign( pObj->Id );
+ if ( p->fTruth )
+ memset( Aig_CutTruth(pCut), 0xAA, sizeof(unsigned) * p->nTruthWords );
+ }
+ return pCutSet;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Derives cuts for one node and sweeps this node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Aig_ObjComputeCuts( Aig_ManCut_t * p, Aig_Obj_t * pObj, int fTriv )
+{
+ Aig_Cut_t * pCut0, * pCut1, * pCut, * pCutSet;
+ Aig_Obj_t * pFanin0 = Aig_ObjFanin0(pObj);
+ Aig_Obj_t * pFanin1 = Aig_ObjFanin1(pObj);
+ int i, k;
+ // the node is not processed yet
+ assert( Aig_ObjIsNode(pObj) );
+ assert( Aig_ObjCuts(p, pObj) == NULL );
+ // set up the first cut
+ pCutSet = Aig_ObjPrepareCuts( p, pObj, fTriv );
+ // compute pair-wise cut combinations while checking table
+ Aig_ObjForEachCut( p, pFanin0, pCut0, i )
+ if ( pCut0->nFanins > 0 )
+ Aig_ObjForEachCut( p, pFanin1, pCut1, k )
+ if ( pCut1->nFanins > 0 )
+ {
+ // make sure K-feasible cut exists
+ if ( Kit_WordCountOnes(pCut0->uSign | pCut1->uSign) > p->nLeafMax )
+ continue;
+ // get the next cut of this node
+ pCut = Aig_CutFindFree( p, pObj );
+ // assemble the new cut
+ if ( !Aig_CutMerge( p, pCut0, pCut1, pCut ) )
+ {
+ assert( pCut->nFanins == 0 );
+ continue;
+ }
+ // check containment
+ if ( Aig_CutFilter( p, pObj, pCut ) )
+ {
+ assert( pCut->nFanins == 0 );
+ continue;
+ }
+ // create its truth table
+ if ( p->fTruth )
+ Aig_CutComputeTruth( p, pCut, pCut0, pCut1, Aig_ObjFaninC0(pObj), Aig_ObjFaninC1(pObj) );
+ // assign the cost
+ pCut->Cost = Aig_CutFindCost( p, pCut );
+ assert( pCut->nFanins > 0 );
+ assert( pCut->Cost > 0 );
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes the cuts for all nodes in the static AIG.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_ManCut_t * Aig_ComputeCuts( Aig_Man_t * pAig, int nCutsMax, int nLeafMax, int fTruth, int fVerbose )
+{
+ Aig_ManCut_t * p;
+ Aig_Obj_t * pObj;
+ int i, clk = clock();
+ assert( pAig->pManCuts == NULL );
+ // start the manager
+ p = Aig_ManCutStart( pAig, nCutsMax, nLeafMax, fTruth, fVerbose );
+ // set elementary cuts at the PIs
+ Aig_ManForEachPi( pAig, pObj, i )
+ Aig_ObjPrepareCuts( p, pObj, 1 );
+ // process the nodes
+ Aig_ManForEachNode( pAig, pObj, i )
+ Aig_ObjComputeCuts( p, pObj, 1 );
+ // print stats
+ if ( fVerbose )
+ {
+ int nCuts, nCutsK;
+ nCuts = Aig_ManCutCount( p, &nCutsK );
+ printf( "Nodes = %6d. Total cuts = %6d. %d-input cuts = %6d.\n",
+ Aig_ManObjNum(pAig), nCuts, nLeafMax, nCutsK );
+ printf( "Cut size = %2d. Truth size = %2d. Total mem = %5.2f Mb ",
+ p->nCutSize, 4*p->nTruthWords, 1.0*Aig_MmFixedReadMemUsage(p->pMemCuts)/(1<<20) );
+ PRT( "Runtime", clock() - clk );
+/*
+ Aig_ManForEachNode( pAig, pObj, i )
+ if ( i % 300 == 0 )
+ Aig_ObjCutPrint( p, pObj );
+*/
+ }
+ // remember the cut manager
+ pAig->pManCuts = p;
+ return p;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/cnf/cnfCore.c b/src/aig/cnf/cnfCore.c
index 06731451..e1d62de0 100644
--- a/src/aig/cnf/cnfCore.c
+++ b/src/aig/cnf/cnfCore.c
@@ -57,7 +57,7 @@ Cnf_Dat_t * Cnf_Derive( Aig_Man_t * pAig, int nOutputs )
// generate cuts for all nodes, assign cost, and find best cuts
clk = clock();
- pMemCuts = Dar_ManComputeCuts( pAig, 10 );
+ pMemCuts = Dar_ManComputeCuts( pAig, 10, 0 );
p->timeCuts = clock() - clk;
// find the mapping
diff --git a/src/aig/dar/dar.h b/src/aig/dar/dar.h
index 2a4fcaf3..72e7d3d1 100644
--- a/src/aig/dar/dar.h
+++ b/src/aig/dar/dar.h
@@ -83,7 +83,7 @@ extern Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel );
/*=== darCore.c ========================================================*/
extern void Dar_ManDefaultRwrParams( Dar_RwrPar_t * pPars );
extern int Dar_ManRewrite( Aig_Man_t * pAig, Dar_RwrPar_t * pPars );
-extern Aig_MmFixed_t * Dar_ManComputeCuts( Aig_Man_t * pAig, int nCutsMax );
+extern Aig_MmFixed_t * Dar_ManComputeCuts( Aig_Man_t * pAig, int nCutsMax, int fVerbose );
/*=== darRefact.c ========================================================*/
extern void Dar_ManDefaultRefParams( Dar_RefPar_t * pPars );
extern int Dar_ManRefactor( Aig_Man_t * pAig, Dar_RefPar_t * pPars );
diff --git a/src/aig/dar/darCore.c b/src/aig/dar/darCore.c
index f4041dd1..141d9b79 100644
--- a/src/aig/dar/darCore.c
+++ b/src/aig/dar/darCore.c
@@ -195,6 +195,34 @@ p->timeOther = p->timeTotal - p->timeCuts - p->timeEval;
/**Function*************************************************************
+ Synopsis [Computes the total number of cuts.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Dar_ManCutCount( Aig_Man_t * pAig, int * pnCutsK )
+{
+ Dar_Cut_t * pCut;
+ Aig_Obj_t * pObj;
+ int i, k, nCuts = 0, nCutsK = 0;
+ Aig_ManForEachNode( pAig, pObj, i )
+ Dar_ObjForEachCut( pObj, pCut, k )
+ {
+ nCuts++;
+ if ( pCut->nLeaves == 4 )
+ nCutsK++;
+ }
+ if ( pnCutsK )
+ *pnCutsK = nCutsK;
+ return nCuts;
+}
+
+/**Function*************************************************************
+
Synopsis []
Description []
@@ -204,13 +232,13 @@ p->timeOther = p->timeTotal - p->timeCuts - p->timeEval;
SeeAlso []
***********************************************************************/
-Aig_MmFixed_t * Dar_ManComputeCuts( Aig_Man_t * pAig, int nCutsMax )
+Aig_MmFixed_t * Dar_ManComputeCuts( Aig_Man_t * pAig, int nCutsMax, int fVerbose )
{
Dar_Man_t * p;
Dar_RwrPar_t Pars, * pPars = &Pars;
Aig_Obj_t * pObj;
Aig_MmFixed_t * pMemCuts;
- int i, nNodes;
+ int i, nNodes, clk = clock();
// remove dangling nodes
if ( (nNodes = Aig_ManCleanup( pAig )) )
{
@@ -226,6 +254,23 @@ Aig_MmFixed_t * Dar_ManComputeCuts( Aig_Man_t * pAig, int nCutsMax )
// compute cuts for each nodes in the topological order
Aig_ManForEachNode( pAig, pObj, i )
Dar_ObjComputeCuts( p, pObj );
+ // print verbose stats
+ if ( fVerbose )
+ {
+// Aig_Obj_t * pObj;
+ int nCuts, nCutsK;//, i;
+ nCuts = Dar_ManCutCount( pAig, &nCutsK );
+ printf( "Nodes = %6d. Total cuts = %6d. 4-input cuts = %6d.\n",
+ Aig_ManObjNum(pAig), nCuts, nCutsK );
+ printf( "Cut size = %2d. Truth size = %2d. Total mem = %5.2f Mb ",
+ sizeof(Dar_Cut_t), 4, 1.0*Aig_MmFixedReadMemUsage(p->pMemCuts)/(1<<20) );
+ PRT( "Runtime", clock() - clk );
+/*
+ Aig_ManForEachNode( pAig, pObj, i )
+ if ( i % 300 == 0 )
+ Dar_ObjCutPrint( pAig, pObj );
+*/
+ }
// free the cuts
pMemCuts = p->pMemCuts;
p->pMemCuts = NULL;
diff --git a/src/aig/dar/darCut.c b/src/aig/dar/darCut.c
index b0aff095..79e4dcc4 100644
--- a/src/aig/dar/darCut.c
+++ b/src/aig/dar/darCut.c
@@ -30,6 +30,47 @@
/**Function*************************************************************
+ Synopsis [Prints one cut.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Dar_CutPrint( Dar_Cut_t * pCut )
+{
+ unsigned i;
+ printf( "{" );
+ for ( i = 0; i < pCut->nLeaves; i++ )
+ printf( " %d", pCut->pLeaves[i] );
+ printf( " }\n" );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Prints one cut.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Dar_ObjCutPrint( Aig_Man_t * p, Aig_Obj_t * pObj )
+{
+ Dar_Cut_t * pCut;
+ int i;
+ printf( "Cuts for node %d:\n", pObj->Id );
+ Dar_ObjForEachCut( pObj, pCut, i )
+ Dar_CutPrint( pCut );
+// printf( "\n" );
+}
+
+/**Function*************************************************************
+
Synopsis [Returns the number of 1s in the machine word.]
Description []
diff --git a/src/aig/dar/darInt.h b/src/aig/dar/darInt.h
index 4da793f5..afa3bd07 100644
--- a/src/aig/dar/darInt.h
+++ b/src/aig/dar/darInt.h
@@ -134,6 +134,7 @@ extern void Dar_ManCutsStart( Dar_Man_t * p );
extern void Dar_ManCutsFree( Dar_Man_t * p );
extern Dar_Cut_t * Dar_ObjComputeCuts_rec( Dar_Man_t * p, Aig_Obj_t * pObj );
extern Dar_Cut_t * Dar_ObjComputeCuts( Dar_Man_t * p, Aig_Obj_t * pObj );
+extern void Dar_ObjCutPrint( Aig_Man_t * p, Aig_Obj_t * pObj );
/*=== darData.c ===========================================================*/
extern Vec_Int_t * Dar_LibReadNodes();
extern Vec_Int_t * Dar_LibReadOuts();
diff --git a/src/aig/fra/fraClaus.c b/src/aig/fra/fraClaus.c
index e3ac9aa3..7e8d7dd1 100644
--- a/src/aig/fra/fraClaus.c
+++ b/src/aig/fra/fraClaus.c
@@ -33,6 +33,11 @@ struct Clu_Man_t_
int nFrames; // the K of the K-step induction
int nPref; // the number of timeframes to skip
int nClausesMax; // the max number of 4-clauses to consider
+ int nLutSize; // the max cut size
+ int nLevels; // the number of levels for cut computation
+ int nCutsMax; // the maximum number of cuts to compute at a node
+ int nBatches; // the number of clause batches to use
+ int fStepUp; // increase cut size for each batch
int fVerbose;
int fVeryVerbose;
// internal parameters
@@ -40,18 +45,25 @@ struct Clu_Man_t_
int nSimWordsPref; // the number of simulation words in the prefix
int nSimFrames; // the number of frames to simulate
int nBTLimit; // the largest number of backtracks (0 = infinite)
- // the network
+ // the network
Aig_Man_t * pAig;
// SAT solvers
sat_solver * pSatMain;
sat_solver * pSatBmc;
// CNF for the test solver
Cnf_Dat_t * pCnf;
+ int fFail;
+ int fFiltering;
+ int fNothingNew;
// clauses
Vec_Int_t * vLits;
Vec_Int_t * vClauses;
Vec_Int_t * vCosts;
int nClauses;
+ // clauses proven
+ Vec_Int_t * vLitsProven;
+ Vec_Int_t * vClausesProven;
+ int nClausesProven;
// counter-examples
Vec_Ptr_t * vCexes;
int nCexes;
@@ -184,7 +196,7 @@ void transpose32a( unsigned a[32] )
int Fra_ClausProcessClausesCut( Clu_Man_t * p, Fra_Sml_t * pSimMan, Dar_Cut_t * pCut, int * pScores )
{
unsigned Matrix[32];
- unsigned * pSims[4], uWord;
+ unsigned * pSims[16], uWord;
int nSeries, i, k, j;
int nWordsForSim = pSimMan->nWordsTotal - p->nSimWordsPref;
// compute parameters
@@ -229,7 +241,7 @@ int Fra_ClausProcessClausesCut( Clu_Man_t * p, Fra_Sml_t * pSimMan, Dar_Cut_t *
***********************************************************************/
int Fra_ClausProcessClausesCut2( Clu_Man_t * p, Fra_Sml_t * pSimMan, Dar_Cut_t * pCut, int * pScores )
{
- unsigned * pSims[4], uWord;
+ unsigned * pSims[16], uWord;
int iMint, i, k, b;
int nWordsForSim = pSimMan->nWordsTotal - p->nSimWordsPref;
// compute parameters
@@ -258,6 +270,43 @@ int Fra_ClausProcessClausesCut2( Clu_Man_t * p, Fra_Sml_t * pSimMan, Dar_Cut_t *
return (int)uWord;
}
+/**Function*************************************************************
+
+ Synopsis [Return the number of combinations appearing in the cut.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Fra_ClausProcessClausesCut3( Clu_Man_t * p, Fra_Sml_t * pSimMan, Aig_Cut_t * pCut, int * pScores )
+{
+ unsigned * pSims[16];
+ int iMint, i, k, b, nMints;
+ int nWordsForSim = pSimMan->nWordsTotal - p->nSimWordsPref;
+ // compute parameters
+ assert( pCut->nFanins > 1 && pCut->nFanins < 17 );
+ assert( nWordsForSim % 8 == 0 );
+ // get parameters
+ for ( i = 0; i < (int)pCut->nFanins; i++ )
+ pSims[i] = Fra_ObjSim( pSimMan, pCut->pFanins[i] ) + p->nSimWordsPref;
+ // add combinational patterns
+ nMints = (1 << pCut->nFanins);
+ memset( pScores, 0, sizeof(int) * nMints );
+ // go through the simulation patterns
+ for ( i = 0; i < nWordsForSim; i++ )
+ for ( k = 0; k < 32; k++ )
+ {
+ iMint = 0;
+ for ( b = 0; b < (int)pCut->nFanins; b++ )
+ if ( pSims[b][i] & (1 << k) )
+ iMint |= (1 << b);
+ pScores[iMint]++;
+ }
+}
+
/**Function*************************************************************
@@ -280,6 +329,8 @@ int Fra_ClausSelectClauses( Clu_Man_t * p )
memset( pCostCount, 0, sizeof(int) * CostMax );
Vec_IntForEachEntry( p->vCosts, Cost, i )
{
+ if ( Cost == -1 )
+ continue;
assert( Cost < CostMax );
pCostCount[ Cost ]++;
}
@@ -334,6 +385,26 @@ void Fra_ClausRecordClause( Clu_Man_t * p, Dar_Cut_t * pCut, int iMint, int Cost
/**Function*************************************************************
+ Synopsis [Processes the clauses.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Fra_ClausRecordClause2( Clu_Man_t * p, Aig_Cut_t * pCut, int iMint, int Cost )
+{
+ int i;
+ for ( i = 0; i < (int)pCut->nFanins; i++ )
+ Vec_IntPush( p->vLits, toLitCond( p->pCnf->pVarNums[pCut->pFanins[i]], (iMint&(1<<i)) ) );
+ Vec_IntPush( p->vClauses, Vec_IntSize(p->vLits) );
+ Vec_IntPush( p->vCosts, Cost );
+}
+
+/**Function*************************************************************
+
Synopsis [Returns 1 if simulation info is composed of all zeros.]
Description []
@@ -485,6 +556,7 @@ int Fra_ClausCollectLatchClauses( Clu_Man_t * p, Fra_Sml_t * pSeq )
int Fra_ClausProcessClauses( Clu_Man_t * p, int fRefs )
{
Aig_MmFixed_t * pMemCuts;
+// Aig_ManCut_t * pManCut;
Fra_Sml_t * pComb, * pSeq;
Aig_Obj_t * pObj;
Dar_Cut_t * pCut;
@@ -519,7 +591,8 @@ PRT( "Lat-cla", clock() - clk );
// generate cuts for all nodes, assign cost, and find best cuts
clk = clock();
- pMemCuts = Dar_ManComputeCuts( p->pAig, 10 );
+ pMemCuts = Dar_ManComputeCuts( p->pAig, 10, 1 );
+// pManCut = Aig_ComputeCuts( p->pAig, 10, 4, 0, 1 );
if ( p->fVerbose )
{
PRT( "Cuts ", clock() - clk );
@@ -572,6 +645,7 @@ clk = clock();
}
Fra_SmlStop( pComb );
Aig_MmFixedStop( pMemCuts, 0 );
+// Aig_ManCutStop( pManCut );
if ( p->fVerbose )
{
PRT( "Infocmb", clock() - clk );
@@ -590,6 +664,174 @@ PRT( "Infocmb", clock() - clk );
/**Function*************************************************************
+ Synopsis [Processes the clauses.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Fra_ClausProcessClauses2( Clu_Man_t * p, int fRefs )
+{
+// Aig_MmFixed_t * pMemCuts;
+ Aig_ManCut_t * pManCut;
+ Fra_Sml_t * pComb, * pSeq;
+ Aig_Obj_t * pObj;
+ Aig_Cut_t * pCut;
+ int i, k, j, clk, nCuts = 0;
+ int ScoresSeq[1<<12], ScoresComb[1<<12];
+ assert( p->nLutSize < 13 );
+
+ // simulate the AIG
+clk = clock();
+ srand( 0xAABBAABB );
+ pSeq = Fra_SmlSimulateSeq( p->pAig, 0, p->nPref + p->nSimFrames, p->nSimWords/p->nSimFrames );
+ if ( pSeq->fNonConstOut )
+ {
+ printf( "Property failed after sequential simulation!\n" );
+ Fra_SmlStop( pSeq );
+ return 0;
+ }
+if ( p->fVerbose )
+{
+PRT( "Sim-seq", clock() - clk );
+}
+
+ // perform combinational simulation
+clk = clock();
+ srand( 0xAABBAABB );
+ pComb = Fra_SmlSimulateComb( p->pAig, p->nSimWords + p->nSimWordsPref );
+if ( p->fVerbose )
+{
+PRT( "Sim-cmb", clock() - clk );
+}
+
+
+clk = clock();
+ if ( fRefs )
+ {
+ Fra_ClausCollectLatchClauses( p, pSeq );
+if ( p->fVerbose )
+{
+PRT( "Lat-cla", clock() - clk );
+}
+ }
+
+
+ // generate cuts for all nodes, assign cost, and find best cuts
+clk = clock();
+// pMemCuts = Dar_ManComputeCuts( p->pAig, 10, 1 );
+ pManCut = Aig_ComputeCuts( p->pAig, p->nCutsMax, p->nLutSize, 0, p->fVerbose );
+if ( p->fVerbose )
+{
+PRT( "Cuts ", clock() - clk );
+}
+
+ // collect combinational info for each cut
+clk = clock();
+ Aig_ManForEachNode( p->pAig, pObj, i )
+ {
+ if ( pObj->Level > (unsigned)p->nLevels )
+ continue;
+ Aig_ObjForEachCut( pManCut, pObj, pCut, k )
+ if ( pCut->nFanins > 1 )
+ {
+ nCuts++;
+ Fra_ClausProcessClausesCut3( p, pSeq, pCut, ScoresSeq );
+ Fra_ClausProcessClausesCut3( p, pComb, pCut, ScoresComb );
+ // write the clauses
+ for ( j = 0; j < (1<<pCut->nFanins); j++ )
+ if ( ScoresComb[j] != 0 && ScoresSeq[j] == 0 )
+ Fra_ClausRecordClause2( p, pCut, j, ScoresComb[j] );
+
+ }
+ }
+ Fra_SmlStop( pSeq );
+ Fra_SmlStop( pComb );
+// Aig_MmFixedStop( pMemCuts, 0 );
+ Aig_ManCutStop( pManCut );
+ p->pAig->pManCuts = NULL;
+if ( p->fVerbose )
+{
+PRT( "Infosim", clock() - clk );
+}
+
+ if ( p->fVerbose )
+ printf( "Node = %5d. Non-triv cuts = %7d. Clauses = %6d. Clause per cut = %6.2f.\n",
+ Aig_ManNodeNum(p->pAig), nCuts, Vec_IntSize(p->vClauses), 1.0*Vec_IntSize(p->vClauses)/nCuts );
+
+ // filter out clauses that are contained in the already proven clauses
+ assert( p->nClauses == 0 );
+ p->nClauses = Vec_IntSize( p->vClauses );
+ if ( Vec_IntSize( p->vClausesProven ) > 0 )
+ {
+ int RetValue, k, Beg, End, * pStart;
+ // reset the solver
+ if ( p->pSatMain ) sat_solver_delete( p->pSatMain );
+ p->pSatMain = Cnf_DataWriteIntoSolver( p->pCnf, 1, 0 );
+ if ( p->pSatMain == NULL )
+ {
+ printf( "Error: Main solver is unsat.\n" );
+ return -1;
+ }
+
+ // add the proven clauses
+ Beg = 0;
+ pStart = Vec_IntArray(p->vLitsProven);
+ Vec_IntForEachEntry( p->vClausesProven, End, i )
+ {
+ assert( End - Beg <= p->nLutSize );
+ // add the clause to all timeframes
+ RetValue = sat_solver_addclause( p->pSatMain, pStart + Beg, pStart + End );
+ if ( RetValue == 0 )
+ {
+ printf( "Error: Solver is UNSAT after adding assumption clauses.\n" );
+ return -1;
+ }
+ Beg = End;
+ }
+ assert( End == Vec_IntSize(p->vLitsProven) );
+
+ // check the clauses
+ Beg = 0;
+ pStart = Vec_IntArray(p->vLits);
+ Vec_IntForEachEntry( p->vClauses, End, i )
+ {
+ assert( Vec_IntEntry( p->vCosts, i ) >= 0 );
+ assert( End - Beg <= p->nLutSize );
+ // check the clause
+ for ( k = Beg; k < End; k++ )
+ pStart[k] = lit_neg( pStart[k] );
+ RetValue = sat_solver_solve( p->pSatMain, pStart + Beg, pStart + End, (sint64)p->nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+ for ( k = Beg; k < End; k++ )
+ pStart[k] = lit_neg( pStart[k] );
+ // the clause holds
+ if ( RetValue == l_False )
+ {
+ Vec_IntWriteEntry( p->vCosts, i, -1 );
+ p->nClauses--;
+ }
+ Beg = End;
+ }
+ assert( End == Vec_IntSize(p->vLits) );
+ if ( p->fVerbose )
+ printf( "Already proved clauses filtered out %d candidate clauses (out of %d).\n",
+ Vec_IntSize(p->vClauses) - p->nClauses, Vec_IntSize(p->vClauses) );
+ }
+
+ p->fFiltering = 0;
+ if ( p->nClauses > p->nClausesMax )
+ {
+ Fra_ClausSelectClauses( p );
+ p->fFiltering = 1;
+ }
+ return 1;
+}
+
+/**Function*************************************************************
+
Synopsis [Converts AIG into the SAT solver.]
Description []
@@ -630,7 +872,7 @@ int Fra_ClausBmcClauses( Clu_Man_t * p )
continue;
}
assert( Vec_IntEntry( p->vCosts, i ) > 0 );
- assert( End - Beg < 5 );
+ assert( End - Beg <= p->nLutSize );
for ( k = Beg; k < End; k++ )
pStart[k] = lit_neg( pStart[k] );
@@ -760,7 +1002,7 @@ void Fra_ClausSimInfoRecord( Clu_Man_t * p, int * pModel )
***********************************************************************/
int Fra_ClausSimInfoCheck( Clu_Man_t * p, int * pLits, int nLits )
{
- unsigned * pSims[4], uWord;
+ unsigned * pSims[16], uWord;
int nWords, iVar, i, w;
for ( i = 0; i < nLits; i++ )
{
@@ -803,7 +1045,8 @@ int Fra_ClausSimInfoCheck( Clu_Man_t * p, int * pLits, int nLits )
int Fra_ClausInductiveClauses( Clu_Man_t * p )
{
// Aig_Obj_t * pObjLi, * pObjLo;
- int * pStart, nLitsTot, RetValue, Beg, End, Counter, i, k, f, fFail = 0, fFlag;//, Lits[2];
+ int * pStart, nLitsTot, RetValue, Beg, End, Counter, i, k, f, fFlag;//, Lits[2];
+ p->fFail = 0;
// reset the solver
if ( p->pSatMain ) sat_solver_delete( p->pSatMain );
@@ -839,6 +1082,54 @@ int Fra_ClausInductiveClauses( Clu_Man_t * p )
}
}
*/
+
+
+ // add the proven clauses
+ nLitsTot = 2 * p->pCnf->nVars;
+ pStart = Vec_IntArray(p->vLitsProven);
+ for ( f = 0; f < p->nFrames; f++ )
+ {
+ Beg = 0;
+ Vec_IntForEachEntry( p->vClausesProven, End, i )
+ {
+ assert( End - Beg <= p->nLutSize );
+ // add the clause to all timeframes
+ RetValue = sat_solver_addclause( p->pSatMain, pStart + Beg, pStart + End );
+ if ( RetValue == 0 )
+ {
+ printf( "Error: Solver is UNSAT after adding assumption clauses.\n" );
+ return -1;
+ }
+ Beg = End;
+ }
+ // increment literals
+ for ( i = 0; i < Vec_IntSize(p->vLitsProven); i++ )
+ p->vLitsProven->pArray[i] += nLitsTot;
+ }
+ // return clauses back to normal
+ nLitsTot = (p->nFrames) * nLitsTot;
+ for ( i = 0; i < Vec_IntSize(p->vLitsProven); i++ )
+ p->vLitsProven->pArray[i] -= nLitsTot;
+
+/*
+ // add the proven clauses
+ nLitsTot = 2 * p->pCnf->nVars;
+ pStart = Vec_IntArray(p->vLitsProven);
+ Beg = 0;
+ Vec_IntForEachEntry( p->vClausesProven, End, i )
+ {
+ assert( End - Beg <= p->nLutSize );
+ // add the clause to all timeframes
+ RetValue = sat_solver_addclause( p->pSatMain, pStart + Beg, pStart + End );
+ if ( RetValue == 0 )
+ {
+ printf( "Error: Solver is UNSAT after adding assumption clauses.\n" );
+ return -1;
+ }
+ Beg = End;
+ }
+*/
+
// add the clauses
nLitsTot = 2 * p->pCnf->nVars;
pStart = Vec_IntArray(p->vLits);
@@ -853,7 +1144,7 @@ int Fra_ClausInductiveClauses( Clu_Man_t * p )
continue;
}
assert( Vec_IntEntry( p->vCosts, i ) > 0 );
- assert( End - Beg < 5 );
+ assert( End - Beg <= p->nLutSize );
// add the clause to all timeframes
RetValue = sat_solver_addclause( p->pSatMain, pStart + Beg, pStart + End );
if ( RetValue == 0 )
@@ -887,7 +1178,7 @@ int Fra_ClausInductiveClauses( Clu_Man_t * p )
if ( p->fVerbose )
printf( " Property fails. " );
// return -2;
- fFail = 1;
+ p->fFail = 1;
}
/*
@@ -930,7 +1221,7 @@ int Fra_ClausInductiveClauses( Clu_Man_t * p )
continue;
}
assert( Vec_IntEntry( p->vCosts, i ) > 0 );
- assert( End - Beg < 5 );
+ assert( End - Beg <= p->nLutSize );
if ( Fra_ClausSimInfoCheck(p, pStart + Beg, End - Beg) )
{
@@ -996,8 +1287,8 @@ int Fra_ClausInductiveClauses( Clu_Man_t * p )
for ( i = 0; i < Vec_IntSize(p->vLits); i++ )
p->vLits->pArray[i] -= nLitsTot;
- if ( fFail )
- return -2;
+// if ( fFail )
+// return -2;
return Counter;
}
@@ -1014,7 +1305,7 @@ int Fra_ClausInductiveClauses( Clu_Man_t * p )
SeeAlso []
***********************************************************************/
-Clu_Man_t * Fra_ClausAlloc( Aig_Man_t * pAig, int nFrames, int nPref, int nClausesMax, int fVerbose, int fVeryVerbose )
+Clu_Man_t * Fra_ClausAlloc( Aig_Man_t * pAig, int nFrames, int nPref, int nClausesMax, int nLutSize, int nLevels, int nCutsMax, int nBatches, int fStepUp, int fVerbose, int fVeryVerbose )
{
Clu_Man_t * p;
p = ALLOC( Clu_Man_t, 1 );
@@ -1023,6 +1314,11 @@ Clu_Man_t * Fra_ClausAlloc( Aig_Man_t * pAig, int nFrames, int nPref, int nClaus
p->nFrames = nFrames;
p->nPref = nPref;
p->nClausesMax = nClausesMax;
+ p->nLutSize = nLutSize;
+ p->nLevels = nLevels;
+ p->nCutsMax = nCutsMax;
+ p->nBatches = nBatches;
+ p->fStepUp = fStepUp;
p->fVerbose = fVerbose;
p->fVeryVerbose = fVeryVerbose;
p->nSimWords = 512;//1024;//64;
@@ -1033,6 +1329,9 @@ Clu_Man_t * Fra_ClausAlloc( Aig_Man_t * pAig, int nFrames, int nPref, int nClaus
p->vClauses = Vec_IntAlloc( 1<<12 );
p->vCosts = Vec_IntAlloc( 1<<12 );
+ p->vLitsProven = Vec_IntAlloc( 1<<14 );
+ p->vClausesProven= Vec_IntAlloc( 1<<12 );
+
p->nCexesAlloc = 1024;
p->vCexes = Vec_PtrAllocSimInfo( Aig_ManObjNumMax(p->pAig)+1, p->nCexesAlloc/32 );
Vec_PtrCleanSimInfo( p->vCexes, 0, p->nCexesAlloc/32 );
@@ -1055,6 +1354,8 @@ void Fra_ClausFree( Clu_Man_t * p )
if ( p->vCexes ) Vec_PtrFree( p->vCexes );
if ( p->vLits ) Vec_IntFree( p->vLits );
if ( p->vClauses ) Vec_IntFree( p->vClauses );
+ if ( p->vLitsProven ) Vec_IntFree( p->vLitsProven );
+ if ( p->vClausesProven ) Vec_IntFree( p->vClausesProven );
if ( p->vCosts ) Vec_IntFree( p->vCosts );
if ( p->pCnf ) Cnf_DataFree( p->pCnf );
if ( p->pSatMain ) sat_solver_delete( p->pSatMain );
@@ -1062,6 +1363,51 @@ void Fra_ClausFree( Clu_Man_t * p )
free( p );
}
+
+/**Function*************************************************************
+
+ Synopsis [Converts AIG into the SAT solver.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Fra_ClausAddToStorage( Clu_Man_t * p )
+{
+ int * pStart;
+ int Beg, End, Counter, i, k;
+ Beg = 0;
+ Counter = 0;
+ pStart = Vec_IntArray( p->vLits );
+ Vec_IntForEachEntry( p->vClauses, End, i )
+ {
+ if ( Vec_IntEntry( p->vCosts, i ) == -1 )
+ {
+ Beg = End;
+ continue;
+ }
+ assert( Vec_IntEntry( p->vCosts, i ) > 0 );
+ assert( End - Beg <= p->nLutSize );
+ for ( k = Beg; k < End; k++ )
+ Vec_IntPush( p->vLitsProven, pStart[k] );
+ Vec_IntPush( p->vClausesProven, Vec_IntSize(p->vLitsProven) );
+ Beg = End;
+ Counter++;
+ }
+ if ( p->fVerbose )
+ printf( "Added to storage %d proved clauses\n", Counter );
+
+ Vec_IntClear( p->vClauses );
+ Vec_IntClear( p->vLits );
+ Vec_IntClear( p->vCosts );
+ p->nClauses = 0;
+
+ p->fNothingNew = (int)(Counter == 0);
+}
+
/**Function*************************************************************
Synopsis [Converts AIG into the SAT solver.]
@@ -1073,16 +1419,16 @@ void Fra_ClausFree( Clu_Man_t * p )
SeeAlso []
***********************************************************************/
-int Fra_Claus( Aig_Man_t * pAig, int nFrames, int nPref, int nClausesMax, int fBmc, int fRefs, int fVerbose, int fVeryVerbose )
+int Fra_Claus( Aig_Man_t * pAig, int nFrames, int nPref, int nClausesMax, int nLutSize, int nLevels, int nCutsMax, int nBatches, int fStepUp, int fBmc, int fRefs, int fVerbose, int fVeryVerbose )
{
Clu_Man_t * p;
int clk, clkTotal = clock();
- int Iter, Counter, nPrefOld;
+ int b, Iter, Counter, nPrefOld;
assert( Aig_ManPoNum(pAig) - Aig_ManRegNum(pAig) == 1 );
// create the manager
- p = Fra_ClausAlloc( pAig, nFrames, nPref, nClausesMax, fVerbose, fVeryVerbose );
+ p = Fra_ClausAlloc( pAig, nFrames, nPref, nClausesMax, nLutSize, nLevels, nCutsMax, nBatches, fStepUp, fVerbose, fVeryVerbose );
clk = clock();
// derive CNF
@@ -1123,67 +1469,85 @@ clk = clock();
Fra_ClausFree( p );
return 1;
}
- // try solving without additional clauses
- if ( Fra_ClausRunSat( p ) )
+
+
+ for ( b = 0; b < p->nBatches; b++ )
{
- printf( "Problem is inductive without strengthening.\n" );
- Fra_ClausFree( p );
- return 1;
- }
-if ( fVerbose )
-{
-PRT( "SAT-ind", clock() - clk );
-}
+// if ( fVerbose )
+ printf( "*** BATCH %d: ", b+1 );
+ if ( b && (!p->fFiltering || p->fNothingNew || p->fStepUp) )
+ p->nLutSize++;
+ printf( "Using %d-cuts.\n", p->nLutSize );
+
+ // try solving without additional clauses
+ if ( Fra_ClausRunSat( p ) )
+ {
+ printf( "Problem is inductive without strengthening.\n" );
+ Fra_ClausFree( p );
+ return 1;
+ }
+ if ( fVerbose )
+ {
+ PRT( "SAT-ind", clock() - clk );
+ }
- // collect the candidate inductive clauses using 4-cuts
-clk = clock();
- nPrefOld = p->nPref; p->nPref = 0; p->nSimWordsPref = 0;
- Fra_ClausProcessClauses( p, fRefs );
- p->nPref = nPrefOld;
- p->nSimWordsPref = p->nPref*p->nSimWords/p->nSimFrames;
+ // collect the candidate inductive clauses using 4-cuts
+ clk = clock();
+ nPrefOld = p->nPref; p->nPref = 0; p->nSimWordsPref = 0;
+ // Fra_ClausProcessClauses( p, fRefs );
+ Fra_ClausProcessClauses2( p, fRefs );
+ p->nPref = nPrefOld;
+ p->nSimWordsPref = p->nPref*p->nSimWords/p->nSimFrames;
-//PRT( "Clauses", clock() - clk );
+ //PRT( "Clauses", clock() - clk );
- // check clauses using BMC
- if ( fBmc )
- {
-clk = clock();
- Counter = Fra_ClausBmcClauses( p );
- p->nClauses -= Counter;
-if ( fVerbose )
-{
- printf( "BMC disproved %d clauses.\n", Counter );
-PRT( "Cla-bmc", clock() - clk );
-}
- }
+ // check clauses using BMC
+ if ( fBmc )
+ {
+ clk = clock();
+ Counter = Fra_ClausBmcClauses( p );
+ p->nClauses -= Counter;
+ if ( fVerbose )
+ {
+ printf( "BMC disproved %d clauses.\n", Counter );
+ PRT( "Cla-bmc", clock() - clk );
+ }
+ }
- // prove clauses inductively
-clk = clock();
- Counter = 1;
- for ( Iter = 0; Counter > 0; Iter++ )
- {
- if ( fVerbose )
- printf( "Iter %3d : Begin = %5d. ", Iter, p->nClauses );
- Counter = Fra_ClausInductiveClauses( p );
- if ( Counter > 0 )
- p->nClauses -= Counter;
- if ( fVerbose )
+ // prove clauses inductively
+ clk = clock();
+ Counter = 1;
+ for ( Iter = 0; Counter > 0; Iter++ )
{
- printf( "End = %5d. Exs = %5d. ", p->nClauses, p->nCexes );
-// printf( "\n" );
- PRT( "Time", clock() - clk );
+ if ( fVerbose )
+ printf( "Iter %3d : Begin = %5d. ", Iter, p->nClauses );
+ Counter = Fra_ClausInductiveClauses( p );
+ if ( Counter > 0 )
+ p->nClauses -= Counter;
+ if ( fVerbose )
+ {
+ printf( "End = %5d. Exs = %5d. ", p->nClauses, p->nCexes );
+ // printf( "\n" );
+ PRT( "Time", clock() - clk );
+ }
+ clk = clock();
}
- clk = clock();
+ if ( Counter == -1 )
+ printf( "Fra_Claus(): Internal error. " );
+ else if ( p->fFail )
+ printf( "Property FAILS during refinement. " );
+ else
+ printf( "Property HOLDS inductively after strengthening. " );
+ PRT( "Time ", clock() - clkTotal );
+
+ if ( !p->fFail )
+ break;
+
+ // add proved clauses to storage
+ Fra_ClausAddToStorage( p );
}
- if ( Counter == -1 )
- printf( "Fra_Claus(): Internal error. " );
- else if ( Counter == -2 )
- printf( "Property FAILS during refinement. " );
- else
- printf( "Property HOLDS inductively after strengthening. " );
- PRT( "Time ", clock() - clkTotal );
// clean the manager
Fra_ClausFree( p );
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-04 00:46:46 +0000