summaryrefslogtreecommitdiffstats
path: root/src/temp
diff options
context:
space:
mode:
Diffstat (limited to 'src/temp')
-rw-r--r--src/temp/ivy/ivy.h30
-rw-r--r--src/temp/ivy/ivyBalance.c6
-rw-r--r--src/temp/ivy/ivyFastMap.c536
-rw-r--r--src/temp/ivy/ivyFraig.c1445
-rw-r--r--src/temp/ivy/ivyMan.c27
-rw-r--r--src/temp/ivy/ivyObj.c8
-rw-r--r--src/temp/ivy/ivyShow.c20
-rw-r--r--src/temp/ivy/satSolver.c1194
-rw-r--r--src/temp/ivy/satSolver.h141
-rw-r--r--src/temp/ivy/satUtil.c161
-rw-r--r--src/temp/ivy/satVec.h83
-rw-r--r--src/temp/player/playerToAbc.c3
12 files changed, 3619 insertions, 35 deletions
diff --git a/src/temp/ivy/ivy.h b/src/temp/ivy/ivy.h
index 864d5e8c..5b684244 100644
--- a/src/temp/ivy/ivy.h
+++ b/src/temp/ivy/ivy.h
@@ -43,6 +43,7 @@ extern "C" {
typedef struct Ivy_Man_t_ Ivy_Man_t;
typedef struct Ivy_Obj_t_ Ivy_Obj_t;
typedef int Ivy_Edge_t;
+typedef struct Ivy_FraigParams_t_ Ivy_FraigParams_t;
// object types
typedef enum {
@@ -70,13 +71,14 @@ struct Ivy_Obj_t_ // 24 bytes (32-bit) or 32 bytes (64-bit) // 10 words - 16
{
int Id; // integer ID
int TravId; // traversal ID
- unsigned Type : 4; // object type
- unsigned fPhase : 1; // value under 000...0 pattern
- unsigned fMarkA : 1; // multipurpose mask
- unsigned fMarkB : 1; // multipurpose mask
- unsigned fExFan : 1; // set to 1 if last fanout added is EXOR
- unsigned Init : 2; // latch initial value
- unsigned Level : 22; // logic level
+ unsigned Type : 4; // object type
+ unsigned fMarkA : 1; // multipurpose mask
+ unsigned fMarkB : 1; // multipurpose mask
+ unsigned fExFan : 1; // set to 1 if last fanout added is EXOR
+ unsigned fPhase : 1; // value under 000...0 pattern
+ unsigned fFailTfo : 1; // the TFO of the failed node
+ unsigned Init : 2; // latch initial value
+ unsigned Level : 21; // logic level
int nRefs; // reference counter
Ivy_Obj_t * pFanin0; // fanin
Ivy_Obj_t * pFanin1; // fanin
@@ -124,6 +126,12 @@ struct Ivy_Man_t_
int time2;
};
+struct Ivy_FraigParams_t_
+{
+ int nSimWords; // the number of words in the simulation info
+ double SimSatur; // the ratio of refined classes when saturation is reached
+};
+
#define IVY_CUT_LIMIT 256
#define IVY_CUT_INPUT 6
@@ -249,6 +257,8 @@ static inline Ivy_Obj_t * Ivy_ObjChild0Equiv( Ivy_Obj_t * pObj ) { assert( !Ivy
static inline Ivy_Obj_t * Ivy_ObjChild1Equiv( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return Ivy_ObjFanin1(pObj)? Ivy_NotCond(Ivy_ObjFanin1(pObj)->pEquiv, Ivy_ObjFaninC1(pObj)) : NULL; }
static inline int Ivy_ObjLevel( Ivy_Obj_t * pObj ) { return pObj->Level; }
static inline int Ivy_ObjLevelNew( Ivy_Obj_t * pObj ) { return 1 + Ivy_ObjIsExor(pObj) + IVY_MAX(Ivy_ObjFanin0(pObj)->Level, Ivy_ObjFanin1(pObj)->Level); }
+static inline int Ivy_ObjFaninPhase( Ivy_Obj_t * pObj ) { return Ivy_IsComplement(pObj)? !Ivy_Regular(pObj)->fPhase : pObj->fPhase; }
+
static inline void Ivy_ObjClean( Ivy_Obj_t * pObj )
{
int IdSaved = pObj->Id;
@@ -430,6 +440,9 @@ extern void Ivy_FastMapPerform( Ivy_Man_t * pAig, int nLimit );
extern void Ivy_FastMapStop( Ivy_Man_t * pAig );
extern void Ivy_FastMapReadSupp( Ivy_Man_t * pAig, Ivy_Obj_t * pObj, Vec_Int_t * vLeaves );
extern void Ivy_FastMapReverseLevel( Ivy_Man_t * pAig );
+/*=== ivyFraig.c ==========================================================*/
+extern Ivy_Man_t * Ivy_FraigPerform( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams );
+extern void Ivy_FraigParamsDefault( Ivy_FraigParams_t * pParams );
/*=== ivyHaig.c ==========================================================*/
extern void Ivy_ManHaigStart( Ivy_Man_t * p, int fVerbose );
extern void Ivy_ManHaigTrasfer( Ivy_Man_t * p, Ivy_Man_t * pNew );
@@ -442,6 +455,7 @@ extern void Ivy_ManHaigSimulate( Ivy_Man_t * p );
extern int Ivy_TruthIsop( unsigned * puTruth, int nVars, Vec_Int_t * vCover, int fTryBoth );
/*=== ivyMan.c ==========================================================*/
extern Ivy_Man_t * Ivy_ManStart();
+extern Ivy_Man_t * Ivy_ManStartFrom( Ivy_Man_t * p );
extern Ivy_Man_t * Ivy_ManDup( Ivy_Man_t * p );
extern void Ivy_ManStop( Ivy_Man_t * p );
extern int Ivy_ManCleanup( Ivy_Man_t * p );
@@ -487,7 +501,7 @@ extern int Ivy_ManRewritePre( Ivy_Man_t * p, int fUpdateLevel, int f
/*=== ivySeq.c =========================================================*/
extern int Ivy_ManRewriteSeq( Ivy_Man_t * p, int fUseZeroCost, int fVerbose );
/*=== ivyShow.c =========================================================*/
-extern void Ivy_ManShow( Ivy_Man_t * pMan, int fHaig );
+extern void Ivy_ManShow( Ivy_Man_t * pMan, int fHaig, Vec_Ptr_t * vBold );
/*=== ivyTable.c ========================================================*/
extern Ivy_Obj_t * Ivy_TableLookup( Ivy_Man_t * p, Ivy_Obj_t * pObj );
extern void Ivy_TableInsert( Ivy_Man_t * p, Ivy_Obj_t * pObj );
diff --git a/src/temp/ivy/ivyBalance.c b/src/temp/ivy/ivyBalance.c
index 3e8bd6d2..5627039a 100644
--- a/src/temp/ivy/ivyBalance.c
+++ b/src/temp/ivy/ivyBalance.c
@@ -17,7 +17,7 @@
Revision [$Id: ivyBalance.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
***********************************************************************/
-
+
#include "ivy.h"
////////////////////////////////////////////////////////////////////////
@@ -73,7 +73,9 @@ Ivy_Man_t * Ivy_ManBalance( Ivy_Man_t * p, int fUpdateLevel )
}
Vec_VecFree( vStore );
if ( i = Ivy_ManCleanup( pNew ) )
- printf( "Cleanup after balancing removed %d dangling nodes.\n", i );
+ {
+// printf( "Cleanup after balancing removed %d dangling nodes.\n", i );
+ }
// check the resulting AIG
if ( !Ivy_ManCheck(pNew) )
printf( "Ivy_ManBalance(): The check has failed.\n" );
diff --git a/src/temp/ivy/ivyFastMap.c b/src/temp/ivy/ivyFastMap.c
index 1d74fd13..39c632c7 100644
--- a/src/temp/ivy/ivyFastMap.c
+++ b/src/temp/ivy/ivyFastMap.c
@@ -68,13 +68,16 @@ static int Ivy_FastMapPrint( Ivy_Man_t * pAig, int Time );
static int Ivy_FastMapDelay( Ivy_Man_t * pAig );
static int Ivy_FastMapArea( Ivy_Man_t * pAig );
static void Ivy_FastMapNode( Ivy_Man_t * pAig, Ivy_Obj_t * pObj, int nLimit );
+static void Ivy_FastMapNodeArea( Ivy_Man_t * pAig, Ivy_Obj_t * pObj, int nLimit );
static int Ivy_FastMapMerge( Ivy_Supp_t * pSupp0, Ivy_Supp_t * pSupp1, Ivy_Supp_t * pSupp, int nLimit );
-static void Ivy_FastMapRequired( Ivy_Man_t * pAig, int Delay );
+static void Ivy_FastMapRequired( Ivy_Man_t * pAig, int Delay, int fSetInter );
static void Ivy_FastMapRecover( Ivy_Man_t * pAig, int nLimit );
static int Ivy_FastMapNodeDelay( Ivy_Man_t * pAig, Ivy_Obj_t * pObj );
static int Ivy_FastMapNodeAreaRefed( Ivy_Man_t * pAig, Ivy_Obj_t * pObj );
static int Ivy_FastMapNodeAreaDerefed( Ivy_Man_t * pAig, Ivy_Obj_t * pObj );
static void Ivy_FastMapNodeRecover( Ivy_Man_t * pAig, Ivy_Obj_t * pObj, int nLimit, Vec_Ptr_t * vFront, Vec_Ptr_t * vFrontOld );
+static int Ivy_FastMapNodeRef( Ivy_Man_t * pAig, Ivy_Obj_t * pObj );
+static int Ivy_FastMapNodeDeref( Ivy_Man_t * pAig, Ivy_Obj_t * pObj );
extern int s_MappingTime;
@@ -108,6 +111,7 @@ void Ivy_FastMapPerform( Ivy_Man_t * pAig, int nLimit )
pMan->nObjs = Ivy_ManObjIdMax(pAig) + 1;
pMan->nSize = sizeof(Ivy_Supp_t) + nLimit * sizeof(int);
pMan->pMem = (char *)malloc( pMan->nObjs * pMan->nSize );
+ memset( pMan->pMem, 0, pMan->nObjs * pMan->nSize );
pMan->vLuts = Vec_VecAlloc( 100 );
pAig->pData = pMan;
clk = clock();
@@ -122,28 +126,43 @@ clk = clock();
printf( "Delay oriented mapping: " );
Delay = Ivy_FastMapPrint( pAig, clock() - clk );
- // perform area recovery
-clk = clock();
- Ivy_FastMapRequired( pAig, Delay );
-// PRT( "Required time computation", clock() - clk );
+// 2-1-2 (doing 2-1-2-1-2 improves 0.5%)
+clk = clock();
+ Ivy_FastMapRequired( pAig, Delay, 0 );
// remap the nodes
Ivy_FastMapRecover( pAig, nLimit );
- printf( "Area recovery : " );
+ printf( "Area recovery 2 : " );
Delay = Ivy_FastMapPrint( pAig, clock() - clk );
- // perform area recovery
clk = clock();
- Ivy_FastMapRequired( pAig, Delay );
-// PRT( "Required time computation", clock() - clk );
+ Ivy_FastMapRequired( pAig, Delay, 0 );
+ // iterate through all nodes in the topological order
+ Ivy_ManForEachNode( pAig, pObj, i )
+ Ivy_FastMapNodeArea( pAig, pObj, nLimit );
+ printf( "Area recovery 1 : " );
+ Delay = Ivy_FastMapPrint( pAig, clock() - clk );
+clk = clock();
+ Ivy_FastMapRequired( pAig, Delay, 0 );
// remap the nodes
Ivy_FastMapRecover( pAig, nLimit );
- printf( "Area recovery : " );
+ printf( "Area recovery 2 : " );
Delay = Ivy_FastMapPrint( pAig, clock() - clk );
+
s_MappingTime = clock() - clkTotal;
s_MappingMem = pMan->nObjs * pMan->nSize;
+/*
+ {
+ Vec_Ptr_t * vNodes;
+ vNodes = Vec_PtrAlloc( 100 );
+ Vec_VecForEachEntry( pMan->vLuts, pObj, i, k )
+ Vec_PtrPush( vNodes, pObj );
+ Ivy_ManShow( pAig, 0, vNodes );
+ Vec_PtrFree( vNodes );
+ }
+*/
}
/**Function*************************************************************
@@ -283,9 +302,261 @@ int Ivy_FastMapArea( Ivy_Man_t * pAig )
SeeAlso []
***********************************************************************/
+static inline Ivy_ObjIsNodeInt1( Ivy_Obj_t * pObj )
+{
+ return Ivy_ObjIsNode(pObj) && Ivy_ObjRefs(pObj) == 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs fast mapping for one node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline Ivy_ObjIsNodeInt2( Ivy_Obj_t * pObj )
+{
+ return Ivy_ObjIsNode(pObj) && Ivy_ObjRefs(pObj) <= 2;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs fast mapping for one node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Vec_IntSelectSort( int * pArray, int nSize )
+{
+ int temp, i, j, best_i;
+ for ( i = 0; i < nSize-1; i++ )
+ {
+ best_i = i;
+ for ( j = i+1; j < nSize; j++ )
+ if ( pArray[j] < pArray[best_i] )
+ best_i = j;
+ temp = pArray[i];
+ pArray[i] = pArray[best_i];
+ pArray[best_i] = temp;
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs fast mapping for one node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Vec_IntRemoveDup( int * pArray, int nSize )
+{
+ int i, k;
+ if ( nSize < 2 )
+ return nSize;
+ for ( i = k = 1; i < nSize; i++ )
+ if ( pArray[i] != pArray[i-1] )
+ pArray[k++] = pArray[i];
+ return k;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs fast mapping for one node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_FastMapNodeArea2( Ivy_Man_t * pAig, Ivy_Obj_t * pObj, int nLimit )
+{
+ static int Store[32], StoreSize;
+ static char Supp0[16], Supp1[16];
+ static Ivy_Supp_t * pTemp0 = (Ivy_Supp_t *)Supp0;
+ static Ivy_Supp_t * pTemp1 = (Ivy_Supp_t *)Supp1;
+ Ivy_Obj_t * pFanin0, * pFanin1;
+ Ivy_Supp_t * pSupp0, * pSupp1, * pSupp;
+ int RetValue, DelayOld;
+ assert( nLimit <= 32 );
+ assert( Ivy_ObjIsNode(pObj) );
+ // get the fanins
+ pFanin0 = Ivy_ObjFanin0(pObj);
+ pFanin1 = Ivy_ObjFanin1(pObj);
+ // get the supports
+ pSupp0 = Ivy_ObjSupp( pAig, pFanin0 );
+ pSupp1 = Ivy_ObjSupp( pAig, pFanin1 );
+ pSupp = Ivy_ObjSupp( pAig, pObj );
+ assert( pSupp->fMark == 0 );
+ // get the old delay of the node
+ DelayOld = Ivy_FastMapNodeDelay(pAig, pObj);
+ assert( DelayOld <= pSupp->DelayR );
+ // copy the current cut
+ memcpy( Store, pSupp->pArray, sizeof(int) * pSupp->nSize );
+ StoreSize = pSupp->nSize;
+ // get the fanin support
+ if ( Ivy_ObjRefs(pFanin0) > 1 && pSupp0->Delay < pSupp->DelayR )
+ {
+ pSupp0 = pTemp0;
+ pSupp0->nSize = 1;
+ pSupp0->pArray[0] = Ivy_ObjFaninId0(pObj);
+ }
+ // get the fanin support
+ if ( Ivy_ObjRefs(pFanin1) > 1 && pSupp1->Delay < pSupp->DelayR )
+ {
+ pSupp1 = pTemp1;
+ pSupp1->nSize = 1;
+ pSupp1->pArray[0] = Ivy_ObjFaninId1(pObj);
+ }
+ // merge the cuts
+ if ( pSupp0->nSize < pSupp1->nSize )
+ RetValue = Ivy_FastMapMerge( pSupp1, pSupp0, pSupp, nLimit );
+ else
+ RetValue = Ivy_FastMapMerge( pSupp0, pSupp1, pSupp, nLimit );
+ if ( !RetValue )
+ {
+ pSupp->nSize = 2;
+ pSupp->pArray[0] = Ivy_ObjFaninId0(pObj);
+ pSupp->pArray[1] = Ivy_ObjFaninId1(pObj);
+ }
+ // check the resulting delay
+ pSupp->Delay = Ivy_FastMapNodeDelay(pAig, pObj);
+ if ( pSupp->Delay > pSupp->DelayR )
+ {
+ pSupp->nSize = StoreSize;
+ memcpy( pSupp->pArray, Store, sizeof(int) * pSupp->nSize );
+ pSupp->Delay = DelayOld;
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs fast mapping for one node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_FastMapNodeArea( Ivy_Man_t * pAig, Ivy_Obj_t * pObj, int nLimit )
+{
+ static int Store[32], StoreSize;
+ static char Supp0[16], Supp1[16];
+ static Ivy_Supp_t * pTemp0 = (Ivy_Supp_t *)Supp0;
+ static Ivy_Supp_t * pTemp1 = (Ivy_Supp_t *)Supp1;
+ Ivy_Obj_t * pFanin0, * pFanin1;
+ Ivy_Supp_t * pSupp0, * pSupp1, * pSupp;
+ int RetValue, DelayOld, RefsOld;
+ int AreaBef, AreaAft;
+ assert( nLimit <= 32 );
+ assert( Ivy_ObjIsNode(pObj) );
+ // get the fanins
+ pFanin0 = Ivy_ObjFanin0(pObj);
+ pFanin1 = Ivy_ObjFanin1(pObj);
+ // get the supports
+ pSupp0 = Ivy_ObjSupp( pAig, pFanin0 );
+ pSupp1 = Ivy_ObjSupp( pAig, pFanin1 );
+ pSupp = Ivy_ObjSupp( pAig, pObj );
+ assert( pSupp->fMark == 0 );
+
+ // get the area
+ if ( pSupp->nRefs == 0 )
+ AreaBef = Ivy_FastMapNodeAreaDerefed( pAig, pObj );
+ else
+ AreaBef = Ivy_FastMapNodeAreaRefed( pAig, pObj );
+// if ( AreaBef == 1 )
+// return;
+
+ // deref the cut if the node is refed
+ if ( pSupp->nRefs != 0 )
+ Ivy_FastMapNodeDeref( pAig, pObj );
+
+ // get the old delay of the node
+ DelayOld = Ivy_FastMapNodeDelay(pAig, pObj);
+ assert( DelayOld <= pSupp->DelayR );
+ // copy the current cut
+ memcpy( Store, pSupp->pArray, sizeof(int) * pSupp->nSize );
+ StoreSize = pSupp->nSize;
+ // get the fanin support
+ if ( Ivy_ObjRefs(pFanin0) > 2 && pSupp0->Delay < pSupp->DelayR )
+// if ( pSupp0->nRefs > 0 && pSupp0->Delay < pSupp->DelayR ) // this leads to 2% worse results
+ {
+ pSupp0 = pTemp0;
+ pSupp0->nSize = 1;
+ pSupp0->pArray[0] = Ivy_ObjFaninId0(pObj);
+ }
+ // get the fanin support
+ if ( Ivy_ObjRefs(pFanin1) > 2 && pSupp1->Delay < pSupp->DelayR )
+// if ( pSupp1->nRefs > 0 && pSupp1->Delay < pSupp->DelayR )
+ {
+ pSupp1 = pTemp1;
+ pSupp1->nSize = 1;
+ pSupp1->pArray[0] = Ivy_ObjFaninId1(pObj);
+ }
+ // merge the cuts
+ if ( pSupp0->nSize < pSupp1->nSize )
+ RetValue = Ivy_FastMapMerge( pSupp1, pSupp0, pSupp, nLimit );
+ else
+ RetValue = Ivy_FastMapMerge( pSupp0, pSupp1, pSupp, nLimit );
+ if ( !RetValue )
+ {
+ pSupp->nSize = 2;
+ pSupp->pArray[0] = Ivy_ObjFaninId0(pObj);
+ pSupp->pArray[1] = Ivy_ObjFaninId1(pObj);
+ }
+
+ // check the resulting delay
+ pSupp->Delay = Ivy_FastMapNodeDelay(pAig, pObj);
+
+ RefsOld = pSupp->nRefs; pSupp->nRefs = 0;
+ AreaAft = Ivy_FastMapNodeAreaDerefed( pAig, pObj );
+ pSupp->nRefs = RefsOld;
+
+ if ( AreaAft > AreaBef || pSupp->Delay > pSupp->DelayR )
+// if ( pSupp->Delay > pSupp->DelayR )
+ {
+ pSupp->nSize = StoreSize;
+ memcpy( pSupp->pArray, Store, sizeof(int) * pSupp->nSize );
+ pSupp->Delay = DelayOld;
+// printf( "-" );
+ }
+// else
+// printf( "+" );
+
+ if ( pSupp->nRefs != 0 )
+ Ivy_FastMapNodeRef( pAig, pObj );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs fast mapping for one node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
void Ivy_FastMapNode( Ivy_Man_t * pAig, Ivy_Obj_t * pObj, int nLimit )
{
Ivy_Supp_t * pSupp0, * pSupp1, * pSupp;
+ int fFaninParam = 2;
int RetValue;
assert( Ivy_ObjIsNode(pObj) );
// get the supports
@@ -316,9 +587,123 @@ void Ivy_FastMapNode( Ivy_Man_t * pAig, Ivy_Obj_t * pObj, int nLimit )
if ( !RetValue )
{
pSupp->Delay++;
- pSupp->nSize = 2;
- pSupp->pArray[0] = Ivy_ObjFaninId0(pObj);
- pSupp->pArray[1] = Ivy_ObjFaninId1(pObj);
+ if ( fFaninParam == 2 )
+ {
+ pSupp->nSize = 2;
+ pSupp->pArray[0] = Ivy_ObjFaninId0(pObj);
+ pSupp->pArray[1] = Ivy_ObjFaninId1(pObj);
+ }
+ else if ( fFaninParam == 3 )
+ {
+ Ivy_Obj_t * pFanin0, * pFanin1, * pFaninA, * pFaninB;
+ pFanin0 = Ivy_ObjFanin0(pObj);
+ pFanin1 = Ivy_ObjFanin1(pObj);
+ pSupp->nSize = 0;
+ // process the first fanin
+ if ( Ivy_ObjIsNodeInt1(pFanin0) )
+ {
+ pFaninA = Ivy_ObjFanin0(pFanin0);
+ pFaninB = Ivy_ObjFanin1(pFanin0);
+ if ( Ivy_ObjIsNodeInt1(pFaninA) && Ivy_ObjIsNodeInt1(pFaninB) )
+ pSupp->pArray[pSupp->nSize++] = Ivy_ObjId(pFanin0);
+ else
+ {
+ pSupp->pArray[pSupp->nSize++] = Ivy_ObjId(pFaninA);
+ pSupp->pArray[pSupp->nSize++] = Ivy_ObjId(pFaninB);
+ }
+ }
+ else
+ pSupp->pArray[pSupp->nSize++] = Ivy_ObjId(pFanin0);
+ // process the second fanin
+ if ( Ivy_ObjIsNodeInt1(pFanin1) )
+ {
+ pFaninA = Ivy_ObjFanin0(pFanin1);
+ pFaninB = Ivy_ObjFanin1(pFanin1);
+ if ( Ivy_ObjIsNodeInt1(pFaninA) && Ivy_ObjIsNodeInt1(pFaninB) )
+ pSupp->pArray[pSupp->nSize++] = Ivy_ObjId(pFanin1);
+ else
+ {
+ pSupp->pArray[pSupp->nSize++] = Ivy_ObjId(pFaninA);
+ pSupp->pArray[pSupp->nSize++] = Ivy_ObjId(pFaninB);
+ }
+ }
+ else
+ pSupp->pArray[pSupp->nSize++] = Ivy_ObjId(pFanin1);
+ // sort the fanins
+ Vec_IntSelectSort( pSupp->pArray, pSupp->nSize );
+ pSupp->nSize = Vec_IntRemoveDup( pSupp->pArray, pSupp->nSize );
+ assert( pSupp->pArray[0] < pSupp->pArray[1] );
+ }
+ else if ( fFaninParam == 4 )
+ {
+ Ivy_Obj_t * pFanin0, * pFanin1, * pFaninA, * pFaninB;
+ pFanin0 = Ivy_ObjFanin0(pObj);
+ pFanin1 = Ivy_ObjFanin1(pObj);
+ pSupp->nSize = 0;
+ // consider the case when exactly one of them is internal
+ if ( Ivy_ObjIsNodeInt1(pFanin0) ^ Ivy_ObjIsNodeInt1(pFanin1) )
+ {
+ pSupp0 = Ivy_ObjSupp( pAig, Ivy_ObjFanin0(pObj) );
+ pSupp1 = Ivy_ObjSupp( pAig, Ivy_ObjFanin1(pObj) );
+ if ( Ivy_ObjIsNodeInt1(pFanin0) && pSupp0->nSize < nLimit )
+ {
+ pSupp->Delay = IVY_MAX( pSupp0->Delay, pSupp1->Delay + 1 );
+ pSupp1 = Ivy_ObjSupp( pAig, Ivy_ManConst1(pAig) );
+ pSupp1->pArray[0] = Ivy_ObjId(pFanin1);
+ // merge the cuts
+ RetValue = Ivy_FastMapMerge( pSupp0, pSupp1, pSupp, nLimit );
+ assert( RetValue );
+ assert( pSupp->nSize > 1 );
+ return;
+ }
+ if ( Ivy_ObjIsNodeInt1(pFanin1) && pSupp1->nSize < nLimit )
+ {
+ pSupp->Delay = IVY_MAX( pSupp1->Delay, pSupp0->Delay + 1 );
+ pSupp0 = Ivy_ObjSupp( pAig, Ivy_ManConst1(pAig) );
+ pSupp0->pArray[0] = Ivy_ObjId(pFanin0);
+ // merge the cuts
+ RetValue = Ivy_FastMapMerge( pSupp1, pSupp0, pSupp, nLimit );
+ assert( RetValue );
+ assert( pSupp->nSize > 1 );
+ return;
+ }
+ }
+ // process the first fanin
+ if ( Ivy_ObjIsNodeInt1(pFanin0) )
+ {
+ pFaninA = Ivy_ObjFanin0(pFanin0);
+ pFaninB = Ivy_ObjFanin1(pFanin0);
+ if ( Ivy_ObjIsNodeInt1(pFaninA) && Ivy_ObjIsNodeInt1(pFaninB) )
+ pSupp->pArray[pSupp->nSize++] = Ivy_ObjId(pFanin0);
+ else
+ {
+ pSupp->pArray[pSupp->nSize++] = Ivy_ObjId(pFaninA);
+ pSupp->pArray[pSupp->nSize++] = Ivy_ObjId(pFaninB);
+ }
+ }
+ else
+ pSupp->pArray[pSupp->nSize++] = Ivy_ObjId(pFanin0);
+ // process the second fanin
+ if ( Ivy_ObjIsNodeInt1(pFanin1) )
+ {
+ pFaninA = Ivy_ObjFanin0(pFanin1);
+ pFaninB = Ivy_ObjFanin1(pFanin1);
+ if ( Ivy_ObjIsNodeInt1(pFaninA) && Ivy_ObjIsNodeInt1(pFaninB) )
+ pSupp->pArray[pSupp->nSize++] = Ivy_ObjId(pFanin1);
+ else
+ {
+ pSupp->pArray[pSupp->nSize++] = Ivy_ObjId(pFaninA);
+ pSupp->pArray[pSupp->nSize++] = Ivy_ObjId(pFaninB);
+ }
+ }
+ else
+ pSupp->pArray[pSupp->nSize++] = Ivy_ObjId(pFanin1);
+ // sort the fanins
+ Vec_IntSelectSort( pSupp->pArray, pSupp->nSize );
+ pSupp->nSize = Vec_IntRemoveDup( pSupp->pArray, pSupp->nSize );
+ assert( pSupp->pArray[0] < pSupp->pArray[1] );
+ assert( pSupp->nSize > 1 );
+ }
}
assert( pSupp->Delay > 0 );
}
@@ -431,6 +816,29 @@ void Ivy_FastMapReadSupp( Ivy_Man_t * pAig, Ivy_Obj_t * pObj, Vec_Int_t * vLeave
/**Function*************************************************************
+ Synopsis [Sets the required times of the intermediate nodes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_FastMapRequired_rec( Ivy_Man_t * pAig, Ivy_Obj_t * pObj, Ivy_Obj_t * pRoot, int DelayR )
+{
+ Ivy_Supp_t * pSupp;
+ pSupp = Ivy_ObjSupp( pAig, pObj );
+ if ( pObj != pRoot && (pSupp->nRefs > 0 || Ivy_ObjIsCi(pObj)) )
+ return;
+ Ivy_FastMapRequired_rec( pAig, Ivy_ObjFanin0(pObj), pRoot, DelayR );
+ Ivy_FastMapRequired_rec( pAig, Ivy_ObjFanin1(pObj), pRoot, DelayR );
+// assert( pObj == pRoot || pSupp->DelayR == IVY_INFINITY );
+ pSupp->DelayR = DelayR;
+}
+
+/**Function*************************************************************
+
Synopsis [Computes the required times for each node.]
Description [Sets reference counters for each node.]
@@ -440,7 +848,7 @@ void Ivy_FastMapReadSupp( Ivy_Man_t * pAig, Ivy_Obj_t * pObj, Vec_Int_t * vLeave
SeeAlso []
***********************************************************************/
-void Ivy_FastMapRequired( Ivy_Man_t * pAig, int Delay )
+void Ivy_FastMapRequired( Ivy_Man_t * pAig, int Delay, int fSetInter )
{
Vec_Vec_t * vLuts;
Vec_Ptr_t * vNodes;
@@ -491,6 +899,23 @@ void Ivy_FastMapRequired( Ivy_Man_t * pAig, int Delay )
}
printf( "\n" );
*/
+
+ if ( fSetInter )
+ {
+ // set the required times of the intermediate nodes
+ Vec_VecForEachLevelReverse( vLuts, vNodes, i )
+ Vec_PtrForEachEntry( vNodes, pObj, k )
+ {
+ pSupp = Ivy_ObjSupp( pAig, pObj );
+ Ivy_FastMapRequired_rec( pAig, pObj, pObj, pSupp->DelayR );
+ }
+ // make sure that all required times are assigned
+ Ivy_ManForEachNode( pAig, pObj, i )
+ {
+ pSupp = Ivy_ObjSupp( pAig, pObj );
+ assert( pSupp->DelayR < IVY_INFINITY );
+ }
+ }
}
/**Function*************************************************************
@@ -688,7 +1113,7 @@ int Ivy_FastMapCutCost( Ivy_Man_t * pAig, Vec_Ptr_t * vFront )
Vec_PtrForEachEntry( vFront, pFanin, i )
{
pSuppF = Ivy_ObjSupp( pAig, pFanin );
- if ( pSuppF->nRefs == 1 )
+ if ( pSuppF->nRefs == 0 )
Counter++;
}
return Counter;
@@ -754,17 +1179,17 @@ int Ivy_FastMapNodeFaninCost( Ivy_Man_t * pAig, Ivy_Obj_t * pObj )
assert( Ivy_ObjIsNode(pObj) );
// check if the node has external refs
pSuppF = Ivy_ObjSupp( pAig, pObj );
- if ( pSuppF->nRefs == 1 )
+ if ( pSuppF->nRefs == 0 )
Counter--;
// increment the number of fanins without external refs
pFanin = Ivy_ObjFanin0(pObj);
pSuppF = Ivy_ObjSupp( pAig, pFanin );
- if ( !Ivy_ObjIsTravIdCurrent(pAig, pFanin) && pSuppF->nRefs == 1 )
+ if ( !Ivy_ObjIsTravIdCurrent(pAig, pFanin) && pSuppF->nRefs == 0 )
Counter++;
// increment the number of fanins without external refs
pFanin = Ivy_ObjFanin1(pObj);
pSuppF = Ivy_ObjSupp( pAig, pFanin );
- if ( !Ivy_ObjIsTravIdCurrent(pAig, pFanin) && pSuppF->nRefs == 1 )
+ if ( !Ivy_ObjIsTravIdCurrent(pAig, pFanin) && pSuppF->nRefs == 0 )
Counter++;
return Counter;
}
@@ -1055,13 +1480,79 @@ void Ivy_FastMapNodeRecover( Ivy_Man_t * pAig, Ivy_Obj_t * pObj, int nLimit, Vec
Ivy_Supp_t * pSupp;
int CostBef, CostAft;
int AreaBef, AreaAft;
+ int DelayOld;
pSupp = Ivy_ObjSupp( pAig, pObj );
+ DelayOld = pSupp->Delay = Ivy_FastMapNodeDelay( pAig, pObj );
+ assert( pSupp->Delay <= pSupp->DelayR );
if ( pSupp->nRefs == 0 )
return;
// get the area
AreaBef = Ivy_FastMapNodeAreaRefed( pAig, pObj );
+// if ( AreaBef == 1 )
+// return;
+ if ( pObj->Id == 102 )
+ {
+ int x = 0;
+ }
+ // the cut is non-trivial
+ Ivy_FastMapNodePrepare( pAig, pObj, nLimit, vFront, vFrontOld );
+ // iteratively modify the cut
+ Ivy_FastMapNodeDeref( pAig, pObj );
+ CostBef = Ivy_FastMapCutCost( pAig, vFront );
+ Ivy_FastMapNodeFaninCompact( pAig, pObj, nLimit, vFront );
+ CostAft = Ivy_FastMapCutCost( pAig, vFront );
+ Ivy_FastMapNodeRef( pAig, pObj );
+ assert( CostBef >= CostAft );
+ // update the node
+ Ivy_FastMapNodeUpdate( pAig, pObj, vFront );
+ pSupp->Delay = Ivy_FastMapNodeDelay( pAig, pObj );
+ // get the new area
+ AreaAft = Ivy_FastMapNodeAreaRefed( pAig, pObj );
+ if ( AreaAft > AreaBef || pSupp->Delay > pSupp->DelayR )
+ {
+ Ivy_FastMapNodeUpdate( pAig, pObj, vFrontOld );
+ AreaAft = Ivy_FastMapNodeAreaRefed( pAig, pObj );
+ assert( AreaAft == AreaBef );
+ pSupp->Delay = DelayOld;
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs area recovery for each node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_FastMapNodeRecover4( Ivy_Man_t * pAig, Ivy_Obj_t * pObj, int nLimit, Vec_Ptr_t * vFront, Vec_Ptr_t * vFrontOld )
+{
+ Ivy_Supp_t * pSupp;
+ int CostBef, CostAft;
+ int AreaBef, AreaAft;
+ int DelayOld;
+ pSupp = Ivy_ObjSupp( pAig, pObj );
+ DelayOld = pSupp->Delay = Ivy_FastMapNodeDelay( pAig, pObj );
+ assert( pSupp->Delay <= pSupp->DelayR );
+// if ( pSupp->nRefs == 0 )
+// return;
+// AreaBef = Ivy_FastMapNodeAreaRefed( pAig, pObj );
+ // get the area
+ if ( pSupp->nRefs == 0 )
+ AreaBef = Ivy_FastMapNodeAreaDerefed( pAig, pObj );
+ else
+ AreaBef = Ivy_FastMapNodeAreaRefed( pAig, pObj );
if ( AreaBef == 1 )
return;
+
+ if ( pSupp->nRefs == 0 )
+ {
+ pSupp->nRefs = 1000000;
+ Ivy_FastMapNodeRef( pAig, pObj );
+ }
// the cut is non-trivial
Ivy_FastMapNodePrepare( pAig, pObj, nLimit, vFront, vFrontOld );
// iteratively modify the cut
@@ -1071,13 +1562,20 @@ void Ivy_FastMapNodeRecover( Ivy_Man_t * pAig, Ivy_Obj_t * pObj, int nLimit, Vec
assert( CostBef >= CostAft );
// update the node
Ivy_FastMapNodeUpdate( pAig, pObj, vFront );
+ pSupp->Delay = Ivy_FastMapNodeDelay( pAig, pObj );
// get the new area
AreaAft = Ivy_FastMapNodeAreaRefed( pAig, pObj );
- if ( AreaAft > AreaBef )
+ if ( AreaAft > AreaBef || pSupp->Delay > pSupp->DelayR )
{
Ivy_FastMapNodeUpdate( pAig, pObj, vFrontOld );
AreaAft = Ivy_FastMapNodeAreaRefed( pAig, pObj );
assert( AreaAft == AreaBef );
+ pSupp->Delay = DelayOld;
+ }
+ if ( pSupp->nRefs == 1000000 )
+ {
+ pSupp->nRefs = 0;
+ Ivy_FastMapNodeDeref( pAig, pObj );
}
}
diff --git a/src/temp/ivy/ivyFraig.c b/src/temp/ivy/ivyFraig.c
new file mode 100644
index 00000000..a3a3b33a
--- /dev/null
+++ b/src/temp/ivy/ivyFraig.c
@@ -0,0 +1,1445 @@
+/**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 "ivy.h"
+#include "satSolver.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Ivy_Fraig_t_ Ivy_Fraig_t;
+struct Ivy_Fraig_t_
+{
+ // general info
+ Ivy_FraigParams_t * pParams; // various parameters
+ // AIG manager
+ Ivy_Man_t * pManAig; // the starting AIG manager
+ Ivy_Man_t * pManFraig; // the final AIG manager
+ // simulation information
+ int nWords; // the number of words
+ unsigned * pWords; // the simulation info
+ // counter example storage
+ int nPatWords; // the number of words in the counter example
+ unsigned * pPatWords; // the counter example
+ // equivalence classes
+ int nClasses; // the number of equivalence classes
+ Ivy_Obj_t * pClassesHead; // the linked list of classes
+ Ivy_Obj_t * pClassesTail; // the linked list of classes
+ // equivalence checking
+ sat_solver * pSat; // SAT solver
+ int nSatVars; // the number of variables currently used
+ // statistics
+ int nSimRounds;
+ int nClassesZero;
+ int nClassesBeg;
+ int nClassesEnd;
+ int nSatCalls;
+ int nSatCallsSat;
+ int nSatCallsUnsat;
+ int nSatProof;
+ int nSatFails;
+ int nSatFailsReal;
+ // runtime
+ int timeSim;
+ int timeTrav;
+ int timeSat;
+ int timeRef;
+ int timeTotal;
+};
+
+static inline unsigned * Ivy_ObjSim( Ivy_Obj_t * pObj ) { return (unsigned *)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, unsigned * 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) )
+#define Ivy_FraigForEachClassNodeSafe( pClass, pEnt, pEnt2 ) \
+ for ( pEnt = pClass, \
+ pEnt2 = pEnt? Ivy_ObjClassNodeNext(pEnt): NULL; \
+ pEnt; \
+ pEnt = pEnt2, \
+ pEnt2 = pEnt? Ivy_ObjClassNodeNext(pEnt): NULL )
+// iterate through nodes in the hash table
+#define Ivy_FraigForEachBinNode( pBin, pEnt ) \
+ for ( pEnt = pBin; \
+ pEnt; \
+ pEnt = Ivy_ObjNodeHashNext(pEnt) )
+#define Ivy_FraigForEachBinNodeSafe( pBin, pEnt, pEnt2 ) \
+ for ( pEnt = pBin, \
+ pEnt2 = pEnt? Ivy_ObjNodeHashNext(pEnt): NULL; \
+ pEnt; \
+ pEnt = pEnt2, \
+ pEnt2 = pEnt? Ivy_ObjNodeHashNext(pEnt): NULL )
+
+static Ivy_Fraig_t * Ivy_FraigStart( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams );
+static void Ivy_FraigPrint( Ivy_Fraig_t * p );
+static void Ivy_FraigStop( Ivy_Fraig_t * p );
+static void Ivy_FraigSimulate( Ivy_Fraig_t * p );
+static void Ivy_FraigSweep( Ivy_Fraig_t * p );
+static Ivy_Obj_t * Ivy_FraigAnd( Ivy_Fraig_t * p, Ivy_Obj_t * pObjOld );
+static int Ivy_FraigNodesAreEquiv( Ivy_Fraig_t * p, Ivy_Obj_t * pObj0, Ivy_Obj_t * pObj1, int nBTLimit );
+static void Ivy_FraigNodeAddToSolver( Ivy_Fraig_t * p, Ivy_Obj_t * pObj0, Ivy_Obj_t * pObj1 );
+static int Ivy_FraigMarkConeSetActivity_rec( Ivy_Fraig_t * p, Ivy_Obj_t * pObj, int * pTravIds, int TravId, double * pFactors, int LevelMax );
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Performs fraiging of the initial AIG.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Ivy_Man_t * Ivy_FraigPerform( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams )
+{
+ Ivy_Fraig_t * p;
+ Ivy_Man_t * pManAigNew;
+ int clk;
+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 [Performs fraiging of the initial AIG.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_FraigParamsDefault( Ivy_FraigParams_t * pParams )
+{
+ memset( pParams, 0, sizeof(Ivy_FraigParams_t) );
+ pParams->nSimWords = 32;
+ pParams->SimSatur = 0.005;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Starts the fraiging manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Ivy_Fraig_t * Ivy_FraigStart( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams )
+{
+ Ivy_Fraig_t * p;
+ Ivy_Obj_t * pObj;
+ int i, k;
+ // 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_Fraig_t, 1 );
+ memset( p, 0, sizeof(Ivy_Fraig_t) );
+ p->pParams = pParams;
+ p->pManAig = pManAig;
+ p->pManFraig = Ivy_ManStartFrom( pManAig );
+ // allocate simulation info
+ p->nWords = pParams->nSimWords;
+ p->pWords = ALLOC( unsigned, Ivy_ManObjNum(pManAig) * p->nWords );
+ k = 0;
+ Ivy_ManForEachObj( pManAig, pObj, i )
+ Ivy_ObjSetSim( pObj, p->pWords + p->nWords * k++ );
+ assert( k == Ivy_ManObjNum(pManAig) );
+ // allocate storage for sim pattern
+ p->nPatWords = Ivy_BitWordNum( Ivy_ManPiNum(pManAig) );
+ p->pPatWords = ALLOC( unsigned, p->nPatWords );
+ // set random number generator
+ srand( 0xABCABC );
+ return p;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Stops the fraiging manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_FraigPrint( Ivy_Fraig_t * p )
+{
+ double nMemory;
+ nMemory = (double)Ivy_ManObjNum(p->pManAig)*p->nWords*sizeof(unsigned)/(1<<20);
+ printf( "SimWords = %d. Rounds = %d. Mem = %0.2f Mb. ", p->nWords, p->nSimRounds, nMemory );
+ printf( "Classes: Beg = %d. End = %d.\n", p->nClassesBeg, p->nClassesEnd );
+ printf( "Proof = %d. Counter-example = %d. Fail = %d. FailReal = %d. Zero = %d.\n",
+ p->nSatProof, p->nSatCallsSat, p->nSatFails, p->nSatFailsReal, p->nClassesZero );
+ printf( "Nodes: Final = %d. Total = %d. Mux = %d. (Exor = %d.) SatVars = %d.\n",
+ Ivy_ManNodeNum(p->pManFraig), 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( "Class refining ", p->timeRef );
+ PRT( "TOTAL RUNTIME ", p->timeTotal );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Stops the fraiging manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_FraigStop( Ivy_Fraig_t * p )
+{
+ Ivy_FraigPrint( p );
+ if ( p->pSat ) sat_solver_delete( p->pSat );
+ free( p->pPatWords );
+ free( p->pWords );
+ free( p );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Simulates one node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_NodeAssignRandom( Ivy_Fraig_t * p, Ivy_Obj_t * pObj )
+{
+ unsigned * pSims;
+ int i;
+ pSims = Ivy_ObjSim(pObj);
+ for ( i = 0; i < p->nWords; i++ )
+ pSims[i] = Ivy_ObjRandomSim();
+}
+
+/**Function*************************************************************
+
+ Synopsis [Simulates one node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_NodeAssignConst( Ivy_Fraig_t * p, Ivy_Obj_t * pObj, int fConst1 )
+{
+ unsigned * pSims;
+ int i;
+ pSims = Ivy_ObjSim(pObj);
+ for ( i = 0; i < p->nWords; i++ )
+ pSims[i] = fConst1? ~(unsigned)0 : 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns 1 if simulation info is composed of all zeros.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ivy_NodeHasZeroSim( Ivy_Fraig_t * p, Ivy_Obj_t * pObj )
+{
+ unsigned * pSims;
+ int i;
+ pSims = Ivy_ObjSim(pObj);
+ for ( i = 0; i < p->nWords; i++ )
+ if ( pSims[i] )
+ return 0;
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns 1 if simulation infos are equal.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ivy_NodeCompareSims( Ivy_Fraig_t * p, Ivy_Obj_t * pObj0, Ivy_Obj_t * pObj1 )
+{
+ unsigned * pSims0, * pSims1;
+ int i;
+ pSims0 = Ivy_ObjSim(pObj0);
+ pSims1 = Ivy_ObjSim(pObj1);
+ for ( i = 0; i < p->nWords; i++ )
+ if ( pSims0[i] != pSims1[i] )
+ return 0;
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Simulates one node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_NodeSimulate( Ivy_Fraig_t * p, Ivy_Obj_t * pObj )
+{
+ unsigned * 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->nWords; i++ )
+ pSims[i] = (pSims0[i] | pSims1[i]);
+ else
+ for ( i = 0; i < p->nWords; i++ )
+ pSims[i] = ~(pSims0[i] | pSims1[i]);
+ }
+ else if ( fCompl0 && !fCompl1 )
+ {
+ if ( fCompl )
+ for ( i = 0; i < p->nWords; i++ )
+ pSims[i] = (pSims0[i] | ~pSims1[i]);
+ else
+ for ( i = 0; i < p->nWords; i++ )
+ pSims[i] = (~pSims0[i] & pSims1[i]);
+ }
+ else if ( !fCompl0 && fCompl1 )
+ {
+ if ( fCompl )
+ for ( i = 0; i < p->nWords; i++ )
+ pSims[i] = (~pSims0[i] | pSims1[i]);
+ else
+ for ( i = 0; i < p->nWords; i++ )
+ pSims[i] = (pSims0[i] & ~pSims1[i]);
+ }
+ else // if ( !fCompl0 && !fCompl1 )
+ {
+ if ( fCompl )
+ for ( i = 0; i < p->nWords; i++ )
+ pSims[i] = ~(pSims0[i] & pSims1[i]);
+ else
+ for ( i = 0; i < p->nWords; i++ )
+ pSims[i] = (pSims0[i] & pSims1[i]);
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes hash value using simulation info.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+unsigned Ivy_NodeHash( Ivy_Fraig_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
+ };
+ unsigned uHash, * pSims;
+ int i;
+ assert( p->nWords <= 128 );
+ uHash = 0;
+ pSims = Ivy_ObjSim(pObj);
+ for ( i = 0; i < p->nWords; i++ )
+ uHash ^= pSims[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_Fraig_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_FraigAssignRandom( Ivy_Fraig_t * p )
+{
+ Ivy_Obj_t * pObj;
+ int i;
+ Ivy_ManForEachPi( p->pManAig, pObj, i )
+ Ivy_NodeAssignRandom( p, pObj );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Simulates AIG manager.]
+
+ Description [Assumes that the PI simulation info is attached.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_FraigAssignDist1( Ivy_Fraig_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->nWords * 32 - 1 );
+ for ( i = 0; i < Limit; i++ )
+ Ivy_InfoXorBit( Ivy_ObjSim( Ivy_ManPi(p->pManAig,i) ), i+1 );
+/*
+ for ( i = 0; i < Limit; i++ )
+ Extra_PrintBinary( stdout, Ivy_ObjSim( Ivy_ManPi(p->pManAig,i) ), 30 ), printf( "\n" );
+*/
+}
+
+/**Function*************************************************************
+
+ Synopsis [Adds new nodes 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 new nodes to the equivalence class.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_FraigAddClass( Ivy_Fraig_t * p, Ivy_Obj_t * pClass )
+{
+ if ( p->pClassesHead == NULL )
+ {
+ p->pClassesHead = pClass;
+ p->pClassesTail = pClass;
+ Ivy_ObjSetEquivListPrev( pClass, NULL );
+ Ivy_ObjSetEquivListNext( pClass, NULL );
+ }
+ else
+ {
+ Ivy_ObjSetEquivListNext( p->pClassesTail, pClass );
+ Ivy_ObjSetEquivListPrev( pClass, p->pClassesTail );
+ Ivy_ObjSetEquivListNext( pClass, NULL );
+ p->pClassesTail = pClass;
+ }
+ p->nClasses++;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Updates the list of classes after base class has split.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_FraigInsertClass( Ivy_Fraig_t * p, 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 ( p->pClassesTail == pBase )
+ p->pClassesTail = pClass;
+ p->nClasses++;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Updates the list of classes after base class has split.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_FraigRemoveClass( Ivy_Fraig_t * p, Ivy_Obj_t * pClass )
+{
+ if ( p->pClassesHead == pClass )
+ p->pClassesHead = Ivy_ObjEquivListNext(pClass);
+ if ( p->pClassesTail == pClass )
+ p->pClassesTail = 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 );
+ p->nClasses--;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Creates initial simulation classes.]
+
+ Description [Assumes that simulation info is assigned.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_FraigCreateClasses( Ivy_Fraig_t * p )
+{
+ Ivy_Obj_t ** pTable;
+ Ivy_Obj_t * pObj, * pConst1, * pBin, * pEntry, * pEntry2;
+ 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->pClassesHead == NULL );
+ if ( Ivy_ObjClassNodeNext(pConst1) )
+ {
+ Ivy_FraigAddClass( p, pConst1 );
+ Ivy_ObjSetClassNodeLast( pConst1, NULL );
+ }
+ for ( i = 0; i < nTableSize; i++ )
+ Ivy_FraigForEachBinNodeSafe( pTable[i], pEntry, pEntry2 )
+ if ( Ivy_ObjClassNodeNext(pEntry) )
+ {
+ Ivy_FraigAddClass( p, pEntry );
+ Ivy_ObjSetClassNodeLast( pEntry, NULL );
+ }
+ else
+ Ivy_ObjSetNodeHashNext( pEntry, NULL );
+ // 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_Fraig_t * p, Ivy_Obj_t * pClass )
+{
+ Ivy_Obj_t * pClassNew, * pListOld, * pListNew, * pNode;
+ // check if there is refinement
+ pListOld = pClass;
+ Ivy_FraigForEachClassNode( Ivy_ObjClassNodeNext(pClass), pClassNew )
+ {
+ if ( !Ivy_NodeCompareSims(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, pClass, pClassNew );
+ // if the old class is trivial, remove it
+ if ( Ivy_ObjClassNodeNext(pClass) == NULL )
+ Ivy_FraigRemoveClass( p, pClass );
+ // if the new class is trivial, remove it; otherwise, try to refine it
+ if ( Ivy_ObjClassNodeNext(pClassNew) == NULL )
+ Ivy_FraigRemoveClass( p, pClassNew );
+ else
+ Ivy_FraigRefineClass_rec( p, pClassNew );
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Refines the classes after simulation.]
+
+ Description [Assumes that simulation info is assigned. Returns the
+ number of classes refined.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ivy_FraigRefineClasses( Ivy_Fraig_t * p )
+{
+ Ivy_Obj_t * pClass, * pClass2;
+ int clk, RetValue = 0;
+clk = clock();
+ Ivy_FraigForEachEquivClassSafe( p->pClassesHead, pClass, pClass2 )
+ RetValue += Ivy_FraigRefineClass_rec( p, pClass );
+p->timeRef += clock() - clk;
+ return RetValue;
+}
+
+/**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 [Stops the fraiging manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ivy_FraigCountClasses( Ivy_Fraig_t * p )
+{
+ Ivy_Obj_t * pClass;
+ int Counter = 0;
+ Ivy_FraigForEachEquivClass( p->pClassesHead, pClass )
+ Counter++;
+ return Counter;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Stops the fraiging manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_FraigPrintSimClasses( Ivy_Fraig_t * p )
+{
+ Ivy_Obj_t * pClass;
+ Ivy_FraigForEachEquivClass( p->pClassesHead, pClass )
+ {
+// Ivy_FraigPrintClass( pClass );
+ printf( "%d ", Ivy_FraigCountClassNodes( pClass ) );
+ }
+// printf( "\n" );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Stops the fraiging manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_FraigSimulate( Ivy_Fraig_t * p )
+{
+ int nChanges, nClasses;
+ Ivy_FraigAssignRandom( p );
+ Ivy_FraigSimulateOne( p );
+ Ivy_FraigCreateClasses( p );
+//printf( "Starting classes = %5d.\n", p->nClasses );
+ do {
+ Ivy_FraigAssignRandom( p );
+ Ivy_FraigSimulateOne( p );
+ nClasses = p->nClasses;
+ nChanges = Ivy_FraigRefineClasses( p );
+//printf( "Refined classes = %5d. Changes = %4d.\n", p->nClasses, nChanges );
+ } while ( (double)nChanges / nClasses > p->pParams->SimSatur );
+// Ivy_FraigPrintSimClasses( p );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Stops the fraiging manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_FraigResimulate( Ivy_Fraig_t * p )
+{
+ int nChanges;
+ Ivy_FraigAssignDist1( p, p->pPatWords );
+ Ivy_FraigSimulateOne( p );
+ nChanges = Ivy_FraigRefineClasses( p );
+ assert( nChanges >= 1 );
+//printf( "Refined classes! = %5d. Changes = %4d.\n", p->nClasses, nChanges );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Performs fraiging for the internal nodes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_FraigSweep( Ivy_Fraig_t * p )
+{
+ Ivy_Obj_t * pObj;
+ int i;
+p->nClassesZero = Ivy_ObjIsConst1(p->pClassesHead) ? Ivy_FraigCountClassNodes(p->pClassesHead) : 0;
+p->nClassesBeg = Ivy_FraigCountClasses(p);
+ // duplicate internal nodes
+ Ivy_ManForEachNode( p->pManAig, pObj, i )
+ pObj->pEquiv = Ivy_FraigAnd( p, pObj );
+p->nClassesEnd = Ivy_FraigCountClasses(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 );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs fraiging for one node.]
+
+ Description [Returns the fraiged node.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Ivy_Obj_t * Ivy_FraigAnd( Ivy_Fraig_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
+ {
+ 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;
+ // they are different (the counter-example is in p->pPatWords)
+ RetValue = Ivy_FraigNodesAreEquiv( p, Ivy_Regular(pObjReprNew), Ivy_Regular(pObjNew), 1000 );
+ if ( RetValue == 1 ) // proved equivalent
+ 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 [Copy pattern from the solver into the internal storage.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_FraigSavePattern( Ivy_Fraig_t * p )
+{
+ Ivy_Obj_t * pObj;
+ int i;
+ memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
+ Ivy_ManForEachPi( p->pManFraig, pObj, i )
+ if ( p->pSat->model.ptr[Ivy_ObjSatNum(pObj)] == l_True )
+ Ivy_InfoSetBit( p->pPatWords, i );
+/*
+ // print sat variables
+ for ( i = 0; i < p->nSatVars; i++ )
+ printf( "%d=%d ", i, p->pSat->model.ptr[i] );
+ printf( "\n" );
+*/
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs fraiging for one node.]
+
+ Description [Returns the fraiged node.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ivy_FraigNodesAreEquiv( Ivy_Fraig_t * p, Ivy_Obj_t * pOld, Ivy_Obj_t * pNew, int nBTLimit )
+{
+ int pLits[4], RetValue, RetValue1, clk, Counter;
+
+// printf( "Trying to prove nodes %d and %d\n", pOld->Id, pNew->Id );
+
+ // 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
+ if ( nBTLimit > 0 && (pOld->fFailTfo || pNew->fFailTfo) )
+ {
+ p->nSatFails++;
+ if ( nBTLimit <= 10 )
+ return -1;
+ nBTLimit = (int)sqrt(nBTLimit);
+ }
+ 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
+clk = clock();
+ Ivy_ManIncrementTravId( p->pManFraig );
+ Counter = Ivy_FraigMarkConeSetActivity_rec( p, pOld, NULL, 0, NULL, 0 );
+ Counter += Ivy_FraigMarkConeSetActivity_rec( p, pNew, NULL, 0, NULL, 0 );
+// printf( "%d ", Counter );
+p->timeTrav += clock() - clk;
+
+
+ // 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 );
+p->timeSat += clock() - clk;
+ if ( RetValue1 == l_False )
+ {
+ 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 )
+ {
+ Ivy_FraigSavePattern( p );
+ p->nSatCallsSat++;
+ return 0;
+ }
+ else // if ( RetValue1 == l_Undef )
+ {
+ // 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 );
+p->timeSat += clock() - clk;
+ if ( RetValue1 == l_False )
+ {
+ 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 )
+ {
+ Ivy_FraigSavePattern( p );
+ p->nSatCallsSat++;
+ return 0;
+ }
+ else // if ( RetValue1 == l_Undef )
+ {
+ // mark the node as the failed node
+ pOld->fFailTfo = 1;
+ 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_Fraig_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_Fraig_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 [Collects the supergate.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_FraigObjAddToFrontier( Ivy_Fraig_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 [Addes clauses to the solver.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_FraigNodeAddToSolver( Ivy_Fraig_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;
+ // quit if CNF is ready
+ if ( Ivy_ObjFaninVec(pOld) && Ivy_ObjFaninVec(pNew) )
+ return;
+ // start the frontier
+ vFrontier = Vec_PtrAlloc( 100 );
+ Ivy_FraigObjAddToFrontier( p, pOld, vFrontier );
+ 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 [Performs fraiging for one node.]
+
+ Description [Returns the fraiged node.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ivy_FraigMarkConeSetActivity_rec( Ivy_Fraig_t * p, Ivy_Obj_t * pObj, int * pTravIds, int TravId, double * pFactors, int LevelMax )
+{
+ Vec_Ptr_t * vFanins;
+ Ivy_Obj_t * pFanin;
+ int i, Counter;
+ assert( !Ivy_IsComplement(pObj) );
+ if ( Ivy_ObjIsConst1(pObj) )
+ return 0;
+ assert( Ivy_ObjSatNum(pObj) );
+// if ( pTravIds[Ivy_ObjSatNum(pObj)] == TravId )
+// return;
+// pTravIds[Ivy_ObjSatNum(pObj)] = TravId;
+// pFactors[Ivy_ObjSatNum(pObj)] = pow( 0.97, LevelMax - pObj->Level );
+ if ( Ivy_ObjIsTravIdCurrent(p->pManFraig, pObj) )
+ return 0;
+ Ivy_ObjSetTravIdCurrent(p->pManFraig, pObj);
+ if ( Ivy_ObjIsPi(pObj) )
+ return 0;
+
+ vFanins = Ivy_ObjFaninVec( pObj );
+ Counter = 1;
+ Vec_PtrForEachEntry( vFanins, pFanin, i )
+ Counter += Ivy_FraigMarkConeSetActivity_rec( p, Ivy_Regular(pFanin), pTravIds, TravId, pFactors, LevelMax );
+ return Counter;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/temp/ivy/ivyMan.c b/src/temp/ivy/ivyMan.c
index 786949e7..c6ad75e8 100644
--- a/src/temp/ivy/ivyMan.c
+++ b/src/temp/ivy/ivyMan.c
@@ -58,7 +58,7 @@ Ivy_Man_t * Ivy_ManStart()
Ivy_ManStartMemory( p );
// create the constant node
p->pConst1 = Ivy_ManFetchMemory( p );
-// p->pConst1->fPhase = 1;
+ p->pConst1->fPhase = 1;
Vec_PtrPush( p->vObjs, p->pConst1 );
p->nCreated = 1;
// start the table
@@ -79,6 +79,31 @@ Ivy_Man_t * Ivy_ManStart()
SeeAlso []
***********************************************************************/
+Ivy_Man_t * Ivy_ManStartFrom( Ivy_Man_t * p )
+{
+ Ivy_Man_t * pNew;
+ Ivy_Obj_t * pObj;
+ int i;
+ // create the new manager
+ pNew = Ivy_ManStart();
+ // create the PIs
+ Ivy_ManConst1(p)->pEquiv = Ivy_ManConst1(pNew);
+ Ivy_ManForEachPi( p, pObj, i )
+ pObj->pEquiv = Ivy_ObjCreatePi(pNew);
+ return pNew;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Duplicates the AIG manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
Ivy_Man_t * Ivy_ManDup( Ivy_Man_t * p )
{
Vec_Int_t * vNodes, * vLatches;
diff --git a/src/temp/ivy/ivyObj.c b/src/temp/ivy/ivyObj.c
index 36af3920..d9887c5b 100644
--- a/src/temp/ivy/ivyObj.c
+++ b/src/temp/ivy/ivyObj.c
@@ -96,6 +96,14 @@ Ivy_Obj_t * Ivy_ObjCreate( Ivy_Man_t * p, Ivy_Obj_t * pGhost )
pObj->Level = Ivy_ObjFanin0(pObj)->Level;
else if ( !Ivy_ObjIsPi(pObj) )
assert( 0 );
+ // create phase
+ if ( Ivy_ObjIsNode(pObj) )
+ pObj->fPhase = Ivy_ObjFaninPhase(Ivy_ObjChild0(pObj)) & Ivy_ObjFaninPhase(Ivy_ObjChild1(pObj));
+ else if ( Ivy_ObjIsOneFanin(pObj) )
+ pObj->fPhase = Ivy_ObjFaninPhase(Ivy_ObjChild0(pObj));
+ // set the fail TFO flag
+ if ( Ivy_ObjIsNode(pObj) )
+ pObj->fFailTfo = Ivy_ObjFanin0(pObj)->fFailTfo | Ivy_ObjFanin1(pObj)->fFailTfo;
// mark the fanins in a special way if the node is EXOR
if ( Ivy_ObjIsExor(pObj) )
{
diff --git a/src/temp/ivy/ivyShow.c b/src/temp/ivy/ivyShow.c
index 3105081e..cd726e43 100644
--- a/src/temp/ivy/ivyShow.c
+++ b/src/temp/ivy/ivyShow.c
@@ -24,7 +24,7 @@
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
-static void Ivy_WriteDotAig( Ivy_Man_t * pMan, char * pFileName, int fHaig );
+static void Ivy_WriteDotAig( Ivy_Man_t * pMan, char * pFileName, int fHaig, Vec_Ptr_t * vBold );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
@@ -41,7 +41,7 @@ static void Ivy_WriteDotAig( Ivy_Man_t * pMan, char * pFileName, int fHaig );
SeeAlso []
***********************************************************************/
-void Ivy_ManShow( Ivy_Man_t * pMan, int fHaig )
+void Ivy_ManShow( Ivy_Man_t * pMan, int fHaig, Vec_Ptr_t * vBold )
{
extern void Abc_ShowFile( char * FileNameDot );
static Counter = 0;
@@ -58,7 +58,7 @@ void Ivy_ManShow( Ivy_Man_t * pMan, int fHaig )
}
fclose( pFile );
// generate the file
- Ivy_WriteDotAig( pMan, FileNameDot, fHaig );
+ Ivy_WriteDotAig( pMan, FileNameDot, fHaig, vBold );
// visualize the file
Abc_ShowFile( FileNameDot );
}
@@ -75,7 +75,7 @@ void Ivy_ManShow( Ivy_Man_t * pMan, int fHaig )
SeeAlso []
***********************************************************************/
-void Ivy_WriteDotAig( Ivy_Man_t * pMan, char * pFileName, int fHaig )
+void Ivy_WriteDotAig( Ivy_Man_t * pMan, char * pFileName, int fHaig, Vec_Ptr_t * vBold )
{
FILE * pFile;
Ivy_Obj_t * pNode, * pTemp, * pPrev;
@@ -92,6 +92,11 @@ void Ivy_WriteDotAig( Ivy_Man_t * pMan, char * pFileName, int fHaig )
return;
}
+ // mark the nodes
+ if ( vBold )
+ Vec_PtrForEachEntry( vBold, pNode, i )
+ pNode->fMarkB = 1;
+
// compute levels
LevelMax = 1 + Ivy_ManSetLevels( pMan, fHaig );
@@ -218,6 +223,8 @@ void Ivy_WriteDotAig( Ivy_Man_t * pMan, char * pFileName, int fHaig )
fprintf( pFile, " Node%d [label = \"%d(%d%s)\"", pNode->Id, pNode->Id,
Ivy_Regular(pNode->pEquiv)->Id, Ivy_IsComplement(pNode->pEquiv)? "\'":"" );
fprintf( pFile, ", shape = ellipse" );
+ if ( vBold && pNode->fMarkB )
+ fprintf( pFile, ", style = filled" );
fprintf( pFile, "];\n" );
}
fprintf( pFile, "}" );
@@ -316,6 +323,11 @@ void Ivy_WriteDotAig( Ivy_Man_t * pMan, char * pFileName, int fHaig )
fprintf( pFile, "\n" );
fprintf( pFile, "\n" );
fclose( pFile );
+
+ // unmark nodes
+ if ( vBold )
+ Vec_PtrForEachEntry( vBold, pNode, i )
+ pNode->fMarkB = 0;
}
diff --git a/src/temp/ivy/satSolver.c b/src/temp/ivy/satSolver.c
new file mode 100644
index 00000000..b8248df8
--- /dev/null
+++ b/src/temp/ivy/satSolver.c
@@ -0,0 +1,1194 @@
+/**************************************************************************************************
+MiniSat -- Copyright (c) 2005, Niklas Sorensson
+http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/
+
+Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
+associated documentation files (the "Software"), to deal in the Software without restriction,
+including without limitation the rights to use, copy, modify, merge, publish, distribute,
+sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all copies or
+substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
+NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
+DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
+OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+**************************************************************************************************/
+// Modified to compile with MS Visual Studio 6.0 by Alan Mishchenko
+
+#include <stdio.h>
+#include <assert.h>
+#include <string.h>
+#include <math.h>
+
+#include "satSolver.h"
+
+//=================================================================================================
+// Debug:
+
+//#define VERBOSEDEBUG
+
+// For derivation output (verbosity level 2)
+#define L_IND "%-*d"
+#define L_ind sat_solver_dlevel(s)*3+3,sat_solver_dlevel(s)
+#define L_LIT "%sx%d"
+#define L_lit(p) lit_sign(p)?"~":"", (lit_var(p))
+
+// Just like 'assert()' but expression will be evaluated in the release version as well.
+static inline void check(int expr) { assert(expr); }
+
+static void printlits(lit* begin, lit* end)
+{
+ int i;
+ for (i = 0; i < end - begin; i++)
+ printf(L_LIT" ",L_lit(begin[i]));
+}
+
+//=================================================================================================
+// Random numbers:
+
+
+// Returns a random float 0 <= x < 1. Seed must never be 0.
+static inline double drand(double* seed) {
+ int q;
+ *seed *= 1389796;
+ q = (int)(*seed / 2147483647);
+ *seed -= (double)q * 2147483647;
+ return *seed / 2147483647; }
+
+
+// Returns a random integer 0 <= x < size. Seed must never be 0.
+static inline int irand(double* seed, int size) {
+ return (int)(drand(seed) * size); }
+
+
+//=================================================================================================
+// Predeclarations:
+
+static void sat_solver_sort(void** array, int size, int(*comp)(const void *, const void *));
+
+//=================================================================================================
+// Clause datatype + minor functions:
+
+struct clause_t
+{
+ int size_learnt;
+ lit lits[0];
+};
+
+static inline int clause_size (clause* c) { return c->size_learnt >> 1; }
+static inline lit* clause_begin (clause* c) { return c->lits; }
+static inline int clause_learnt (clause* c) { return c->size_learnt & 1; }
+static inline float clause_activity (clause* c) { return *((float*)&c->lits[c->size_learnt>>1]); }
+static inline void clause_setactivity(clause* c, float a) { *((float*)&c->lits[c->size_learnt>>1]) = a; }
+
+//=================================================================================================
+// Encode literals in clause pointers:
+
+static clause* clause_from_lit (lit l) { return (clause*)((unsigned long)l + (unsigned long)l + 1); }
+static bool clause_is_lit (clause* c) { return ((unsigned long)c & 1); }
+static lit clause_read_lit (clause* c) { return (lit)((unsigned long)c >> 1); }
+
+//=================================================================================================
+// Simple helpers:
+
+static inline int sat_solver_dlevel(sat_solver* s) { return veci_size(&s->trail_lim); }
+static inline vecp* sat_solver_read_wlist(sat_solver* s, lit l) { return &s->wlists[l]; }
+static inline void vecp_remove(vecp* v, void* e)
+{
+ void** ws = vecp_begin(v);
+ int j = 0;
+ for (; ws[j] != e ; j++);
+ assert(j < vecp_size(v));
+ for (; j < vecp_size(v)-1; j++) ws[j] = ws[j+1];
+ vecp_resize(v,vecp_size(v)-1);
+}
+
+//=================================================================================================
+// Variable order functions:
+
+static inline void order_update(sat_solver* s, int v) // updateorder
+{
+ int* orderpos = s->orderpos;
+ double* activity = s->activity;
+ int* heap = veci_begin(&s->order);
+ int i = orderpos[v];
+ int x = heap[i];
+ int parent = (i - 1) / 2;
+
+ assert(s->orderpos[v] != -1);
+
+ while (i != 0 && activity[x] > activity[heap[parent]]){
+ heap[i] = heap[parent];
+ orderpos[heap[i]] = i;
+ i = parent;
+ parent = (i - 1) / 2;
+ }
+ heap[i] = x;
+ orderpos[x] = i;
+}
+
+static inline void order_assigned(sat_solver* s, int v)
+{
+}
+
+static inline void order_unassigned(sat_solver* s, int v) // undoorder
+{
+ int* orderpos = s->orderpos;
+ if (orderpos[v] == -1){
+ orderpos[v] = veci_size(&s->order);
+ veci_push(&s->order,v);
+ order_update(s,v);
+ }
+}
+
+static int order_select(sat_solver* s, float random_var_freq) // selectvar
+{
+ int* heap;
+ double* activity;
+ int* orderpos;
+
+ lbool* values = s->assigns;
+
+ // Random decision:
+ if (drand(&s->random_seed) < random_var_freq){
+ int next = irand(&s->random_seed,s->size);
+ assert(next >= 0 && next < s->size);
+ if (values[next] == l_Undef)
+ return next;
+ }
+
+ // Activity based decision:
+
+ heap = veci_begin(&s->order);
+ activity = s->activity;
+ orderpos = s->orderpos;
+
+
+ while (veci_size(&s->order) > 0){
+ int next = heap[0];
+ int size = veci_size(&s->order)-1;
+ int x = heap[size];
+
+ veci_resize(&s->order,size);
+
+ orderpos[next] = -1;
+
+ if (size > 0){
+ double act = activity[x];
+
+ int i = 0;
+ int child = 1;
+
+
+ while (child < size){
+ if (child+1 < size && activity[heap[child]] < activity[heap[child+1]])
+ child++;
+
+ assert(child < size);
+
+ if (act >= activity[heap[child]])
+ break;
+
+ heap[i] = heap[child];
+ orderpos[heap[i]] = i;
+ i = child;
+ child = 2 * child + 1;
+ }
+ heap[i] = x;
+ orderpos[heap[i]] = i;
+ }
+
+ if (values[next] == l_Undef)
+ return next;
+ }
+
+ return var_Undef;
+}
+
+//=================================================================================================
+// Activity functions:
+
+static inline void act_var_rescale(sat_solver* s) {
+ double* activity = s->activity;
+ int i;
+ for (i = 0; i < s->size; i++)
+ activity[i] *= 1e-100;
+ s->var_inc *= 1e-100;
+}
+
+static inline void act_var_bump(sat_solver* s, int v) {
+ double* activity = s->activity;
+ if ((activity[v] += s->var_inc) > 1e100)
+ act_var_rescale(s);
+
+ //printf("bump %d %f\n", v-1, activity[v]);
+
+ if (s->orderpos[v] != -1)
+ order_update(s,v);
+
+}
+
+static inline void act_var_decay(sat_solver* s) { s->var_inc *= s->var_decay; }
+
+static inline void act_clause_rescale(sat_solver* s) {
+ clause** cs = (clause**)vecp_begin(&s->learnts);
+ int i;
+ for (i = 0; i < vecp_size(&s->learnts); i++){
+ float a = clause_activity(cs[i]);
+ clause_setactivity(cs[i], a * (float)1e-20);
+ }
+ s->cla_inc *= (float)1e-20;
+}
+
+
+static inline void act_clause_bump(sat_solver* s, clause *c) {
+ float a = clause_activity(c) + s->cla_inc;
+ clause_setactivity(c,a);
+ if (a > 1e20) act_clause_rescale(s);
+}
+
+static inline void act_clause_decay(sat_solver* s) { s->cla_inc *= s->cla_decay; }
+
+
+//=================================================================================================
+// Clause functions:
+
+/* pre: size > 1 && no variable occurs twice
+ */
+static clause* clause_new(sat_solver* s, lit* begin, lit* end, int learnt)
+{
+ int size;
+ clause* c;
+ int i;
+
+ assert(end - begin > 1);
+ assert(learnt >= 0 && learnt < 2);
+ size = end - begin;
+ c = (clause*)malloc(sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float));
+ c->size_learnt = (size << 1) | learnt;
+ assert(((unsigned int)c & 1) == 0);
+
+ for (i = 0; i < size; i++)
+ c->lits[i] = begin[i];
+
+ if (learnt)
+ *((float*)&c->lits[size]) = 0.0;
+
+ assert(begin[0] >= 0);
+ assert(begin[0] < s->size*2);
+ assert(begin[1] >= 0);
+ assert(begin[1] < s->size*2);
+
+ assert(lit_neg(begin[0]) < s->size*2);
+ assert(lit_neg(begin[1]) < s->size*2);
+
+ //vecp_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(void*)c);
+ //vecp_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(void*)c);
+
+ vecp_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(void*)(size > 2 ? c : clause_from_lit(begin[1])));
+ vecp_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(void*)(size > 2 ? c : clause_from_lit(begin[0])));
+
+ return c;
+}
+
+
+static void clause_remove(sat_solver* s, clause* c)
+{
+ lit* lits = clause_begin(c);
+ assert(lit_neg(lits[0]) < s->size*2);
+ assert(lit_neg(lits[1]) < s->size*2);
+
+ //vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[0])),(void*)c);
+ //vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[1])),(void*)c);
+
+ assert(lits[0] < s->size*2);
+ vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[0])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[1])));
+ vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[1])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[0])));
+
+ if (clause_learnt(c)){
+ s->stats.learnts--;
+ s->stats.learnts_literals -= clause_size(c);
+ }else{
+ s->stats.clauses--;
+ s->stats.clauses_literals -= clause_size(c);
+ }
+
+ free(c);
+}
+
+
+static lbool clause_simplify(sat_solver* s, clause* c)
+{
+ lit* lits = clause_begin(c);
+ lbool* values = s->assigns;
+ int i;
+
+ assert(sat_solver_dlevel(s) == 0);
+
+ for (i = 0; i < clause_size(c); i++){
+ lbool sig = !lit_sign(lits[i]); sig += sig - 1;
+ if (values[lit_var(lits[i])] == sig)
+ return l_True;
+ }
+ return l_False;
+}
+
+//=================================================================================================
+// Minor (solver) functions:
+
+void sat_solver_setnvars(sat_solver* s,int n)
+{
+ int var;
+
+ if (s->cap < n){
+
+ while (s->cap < n) s->cap = s->cap*2+1;
+
+ s->wlists = (vecp*) realloc(s->wlists, sizeof(vecp)*s->cap*2);
+ s->activity = (double*) realloc(s->activity, sizeof(double)*s->cap);
+ s->assigns = (lbool*) realloc(s->assigns, sizeof(lbool)*s->cap);
+ s->orderpos = (int*) realloc(s->orderpos, sizeof(int)*s->cap);
+ s->reasons = (clause**)realloc(s->reasons, sizeof(clause*)*s->cap);
+ s->levels = (int*) realloc(s->levels, sizeof(int)*s->cap);
+ s->tags = (lbool*) realloc(s->tags, sizeof(lbool)*s->cap);
+ s->trail = (lit*) realloc(s->trail, sizeof(lit)*s->cap);
+ }
+
+ for (var = s->size; var < n; var++){
+ vecp_new(&s->wlists[2*var]);
+ vecp_new(&s->wlists[2*var+1]);
+ s->activity [var] = 0;
+ s->assigns [var] = l_Undef;
+ s->orderpos [var] = veci_size(&s->order);
+ s->reasons [var] = (clause*)0;
+ s->levels [var] = 0;
+ s->tags [var] = l_Undef;
+
+ /* does not hold because variables enqueued at top level will not be reinserted in the heap
+ assert(veci_size(&s->order) == var);
+ */
+ veci_push(&s->order,var);
+ order_update(s, var);
+ }
+
+ s->size = n > s->size ? n : s->size;
+}
+
+
+static inline bool enqueue(sat_solver* s, lit l, clause* from)
+{
+ lbool* values = s->assigns;
+ int v = lit_var(l);
+ lbool val = values[v];
+#ifdef VERBOSEDEBUG
+ printf(L_IND"enqueue("L_LIT")\n", L_ind, L_lit(l));
+#endif
+
+ lbool sig = !lit_sign(l); sig += sig - 1;
+ if (val != l_Undef){
+ return val == sig;
+ }else{
+ // New fact -- store it.
+#ifdef VERBOSEDEBUG
+ printf(L_IND"bind("L_LIT")\n", L_ind, L_lit(l));
+#endif
+ int* levels = s->levels;
+ clause** reasons = s->reasons;
+
+ values [v] = sig;
+ levels [v] = sat_solver_dlevel(s);
+ reasons[v] = from;
+ s->trail[s->qtail++] = l;
+
+ order_assigned(s, v);
+ return true;
+ }
+}
+
+
+static inline void assume(sat_solver* s, lit l){
+ assert(s->qtail == s->qhead);
+ assert(s->assigns[lit_var(l)] == l_Undef);
+#ifdef VERBOSEDEBUG
+ printf(L_IND"assume("L_LIT")\n", L_ind, L_lit(l));
+#endif
+ veci_push(&s->trail_lim,s->qtail);
+ enqueue(s,l,(clause*)0);
+}
+
+
+static inline void sat_solver_canceluntil(sat_solver* s, int level) {
+ lit* trail;
+ lbool* values;
+ clause** reasons;
+ int bound;
+ int c;
+
+ if (sat_solver_dlevel(s) <= level)
+ return;
+
+ trail = s->trail;
+ values = s->assigns;
+ reasons = s->reasons;
+ bound = (veci_begin(&s->trail_lim))[level];
+
+ for (c = s->qtail-1; c >= bound; c--) {
+ int x = lit_var(trail[c]);
+ values [x] = l_Undef;
+ reasons[x] = (clause*)0;
+ }
+
+ for (c = s->qhead-1; c >= bound; c--)
+ order_unassigned(s,lit_var(trail[c]));
+
+ s->qhead = s->qtail = bound;
+ veci_resize(&s->trail_lim,level);
+}
+
+static void sat_solver_record(sat_solver* s, veci* cls)
+{
+ lit* begin = veci_begin(cls);
+ lit* end = begin + veci_size(cls);
+ clause* c = (veci_size(cls) > 1) ? clause_new(s,begin,end,1) : (clause*)0;
+ enqueue(s,*begin,c);
+
+ assert(veci_size(cls) > 0);
+
+ if (c != 0) {
+ vecp_push(&s->learnts,c);
+ act_clause_bump(s,c);
+ s->stats.learnts++;
+ s->stats.learnts_literals += veci_size(cls);
+ }
+}
+
+
+static double sat_solver_progress(sat_solver* s)
+{
+ lbool* values = s->assigns;
+ int* levels = s->levels;
+ int i;
+
+ double progress = 0;
+ double F = 1.0 / s->size;
+ for (i = 0; i < s->size; i++)
+ if (values[i] != l_Undef)
+ progress += pow(F, levels[i]);
+ return progress / s->size;
+}
+
+//=================================================================================================
+// Major methods:
+
+static bool sat_solver_lit_removable(sat_solver* s, lit l, int minl)
+{
+ lbool* tags = s->tags;
+ clause** reasons = s->reasons;
+ int* levels = s->levels;
+ int top = veci_size(&s->tagged);
+
+ assert(lit_var(l) >= 0 && lit_var(l) < s->size);
+ assert(reasons[lit_var(l)] != 0);
+ veci_resize(&s->stack,0);
+ veci_push(&s->stack,lit_var(l));
+
+ while (veci_size(&s->stack) > 0){
+ clause* c;
+ int v = veci_begin(&s->stack)[veci_size(&s->stack)-1];
+ assert(v >= 0 && v < s->size);
+ veci_resize(&s->stack,veci_size(&s->stack)-1);
+ assert(reasons[v] != 0);
+ c = reasons[v];
+
+ if (clause_is_lit(c)){
+ int v = lit_var(clause_read_lit(c));
+ if (tags[v] == l_Undef && levels[v] != 0){
+ if (reasons[v] != 0 && ((1 << (levels[v] & 31)) & minl)){
+ veci_push(&s->stack,v);
+ tags[v] = l_True;
+ veci_push(&s->tagged,v);
+ }else{
+ int* tagged = veci_begin(&s->tagged);
+ int j;
+ for (j = top; j < veci_size(&s->tagged); j++)
+ tags[tagged[j]] = l_Undef;
+ veci_resize(&s->tagged,top);
+ return false;
+ }
+ }
+ }else{
+ lit* lits = clause_begin(c);
+ int i, j;
+
+ for (i = 1; i < clause_size(c); i++){
+ int v = lit_var(lits[i]);
+ if (tags[v] == l_Undef && levels[v] != 0){
+ if (reasons[v] != 0 && ((1 << (levels[v] & 31)) & minl)){
+
+ veci_push(&s->stack,lit_var(lits[i]));
+ tags[v] = l_True;
+ veci_push(&s->tagged,v);
+ }else{
+ int* tagged = veci_begin(&s->tagged);
+ for (j = top; j < veci_size(&s->tagged); j++)
+ tags[tagged[j]] = l_Undef;
+ veci_resize(&s->tagged,top);
+ return false;
+ }
+ }
+ }
+ }
+ }
+
+ return true;
+}
+
+static void sat_solver_analyze(sat_solver* s, clause* c, veci* learnt)
+{
+ lit* trail = s->trail;
+ lbool* tags = s->tags;
+ clause** reasons = s->reasons;
+ int* levels = s->levels;
+ int cnt = 0;
+ lit p = lit_Undef;
+ int ind = s->qtail-1;
+ lit* lits;
+ int i, j, minl;
+ int* tagged;
+
+ veci_push(learnt,lit_Undef);
+
+ do{
+ assert(c != 0);
+
+ if (clause_is_lit(c)){
+ lit q = clause_read_lit(c);
+ assert(lit_var(q) >= 0 && lit_var(q) < s->size);
+ if (tags[lit_var(q)] == l_Undef && levels[lit_var(q)] > 0){
+ tags[lit_var(q)] = l_True;
+ veci_push(&s->tagged,lit_var(q));
+ act_var_bump(s,lit_var(q));
+ if (levels[lit_var(q)] == sat_solver_dlevel(s))
+ cnt++;
+ else
+ veci_push(learnt,q);
+ }
+ }else{
+
+ if (clause_learnt(c))
+ act_clause_bump(s,c);
+
+ lits = clause_begin(c);
+ //printlits(lits,lits+clause_size(c)); printf("\n");
+ for (j = (p == lit_Undef ? 0 : 1); j < clause_size(c); j++){
+ lit q = lits[j];
+ assert(lit_var(q) >= 0 && lit_var(q) < s->size);
+ if (tags[lit_var(q)] == l_Undef && levels[lit_var(q)] > 0){
+ tags[lit_var(q)] = l_True;
+ veci_push(&s->tagged,lit_var(q));
+ act_var_bump(s,lit_var(q));
+ if (levels[lit_var(q)] == sat_solver_dlevel(s))
+ cnt++;
+ else
+ veci_push(learnt,q);
+ }
+ }
+ }
+
+ while (tags[lit_var(trail[ind--])] == l_Undef);
+
+ p = trail[ind+1];
+ c = reasons[lit_var(p)];
+ cnt--;
+
+ }while (cnt > 0);
+
+ *veci_begin(learnt) = lit_neg(p);
+
+ lits = veci_begin(learnt);
+ minl = 0;
+ for (i = 1; i < veci_size(learnt); i++){
+ int lev = levels[lit_var(lits[i])];
+ minl |= 1 << (lev & 31);
+ }
+
+ // simplify (full)
+ for (i = j = 1; i < veci_size(learnt); i++){
+ if (reasons[lit_var(lits[i])] == 0 || !sat_solver_lit_removable(s,lits[i],minl))
+ lits[j++] = lits[i];
+ }
+
+ // update size of learnt + statistics
+ s->stats.max_literals += veci_size(learnt);
+ veci_resize(learnt,j);
+ s->stats.tot_literals += j;
+
+ // clear tags
+ tagged = veci_begin(&s->tagged);
+ for (i = 0; i < veci_size(&s->tagged); i++)
+ tags[tagged[i]] = l_Undef;
+ veci_resize(&s->tagged,0);
+
+#ifdef DEBUG
+ for (i = 0; i < s->size; i++)
+ assert(tags[i] == l_Undef);
+#endif
+
+#ifdef VERBOSEDEBUG
+ printf(L_IND"Learnt {", L_ind);
+ for (i = 0; i < veci_size(learnt); i++) printf(" "L_LIT, L_lit(lits[i]));
+#endif
+ if (veci_size(learnt) > 1){
+ int max_i = 1;
+ int max = levels[lit_var(lits[1])];
+ lit tmp;
+
+ for (i = 2; i < veci_size(learnt); i++)
+ if (levels[lit_var(lits[i])] > max){
+ max = levels[lit_var(lits[i])];
+ max_i = i;
+ }
+
+ tmp = lits[1];
+ lits[1] = lits[max_i];
+ lits[max_i] = tmp;
+ }
+#ifdef VERBOSEDEBUG
+ {
+ int lev = veci_size(learnt) > 1 ? levels[lit_var(lits[1])] : 0;
+ printf(" } at level %d\n", lev);
+ }
+#endif
+}
+
+
+clause* sat_solver_propagate(sat_solver* s)
+{
+ lbool* values = s->assigns;
+ clause* confl = (clause*)0;
+ lit* lits;
+
+ //printf("sat_solver_propagate\n");
+ while (confl == 0 && s->qtail - s->qhead > 0){
+ lit p = s->trail[s->qhead++];
+ vecp* ws = sat_solver_read_wlist(s,p);
+ clause **begin = (clause**)vecp_begin(ws);
+ clause **end = begin + vecp_size(ws);
+ clause **i, **j;
+
+ s->stats.propagations++;
+ s->simpdb_props--;
+
+ //printf("checking lit %d: "L_LIT"\n", veci_size(ws), L_lit(p));
+ for (i = j = begin; i < end; ){
+ if (clause_is_lit(*i)){
+ *j++ = *i;
+ if (!enqueue(s,clause_read_lit(*i),clause_from_lit(p))){
+ confl = s->binary;
+ (clause_begin(confl))[1] = lit_neg(p);
+ (clause_begin(confl))[0] = clause_read_lit(*i++);
+
+ // Copy the remaining watches:
+ while (i < end)
+ *j++ = *i++;
+ }
+ }else{
+ lit false_lit;
+ lbool sig;
+
+ lits = clause_begin(*i);
+
+ // Make sure the false literal is data[1]:
+ false_lit = lit_neg(p);
+ if (lits[0] == false_lit){
+ lits[0] = lits[1];
+ lits[1] = false_lit;
+ }
+ assert(lits[1] == false_lit);
+ //printf("checking clause: "); printlits(lits, lits+clause_size(*i)); printf("\n");
+
+ // If 0th watch is true, then clause is already satisfied.
+ sig = !lit_sign(lits[0]); sig += sig - 1;
+ if (values[lit_var(lits[0])] == sig){
+ *j++ = *i;
+ }else{
+ // Look for new watch:
+ lit* stop = lits + clause_size(*i);
+ lit* k;
+ for (k = lits + 2; k < stop; k++){
+ lbool sig = lit_sign(*k); sig += sig - 1;
+ if (values[lit_var(*k)] != sig){
+ lits[1] = *k;
+ *k = false_lit;
+ vecp_push(sat_solver_read_wlist(s,lit_neg(lits[1])),*i);
+ goto next; }
+ }
+
+ *j++ = *i;
+ // Clause is unit under assignment:
+ if (!enqueue(s,lits[0], *i)){
+ confl = *i++;
+ // Copy the remaining watches:
+ while (i < end)
+ *j++ = *i++;
+ }
+ }
+ }
+ next:
+ i++;
+ }
+
+ s->stats.inspects += j - (clause**)vecp_begin(ws);
+ vecp_resize(ws,j - (clause**)vecp_begin(ws));
+ }
+
+ return confl;
+}
+
+static inline int clause_cmp (const void* x, const void* y) {
+ return clause_size((clause*)x) > 2 && (clause_size((clause*)y) == 2 || clause_activity((clause*)x) < clause_activity((clause*)y)) ? -1 : 1; }
+
+void sat_solver_reducedb(sat_solver* s)
+{
+ int i, j;
+ double extra_lim = s->cla_inc / vecp_size(&s->learnts); // Remove any clause below this activity
+ clause** learnts = (clause**)vecp_begin(&s->learnts);
+ clause** reasons = s->reasons;
+
+ sat_solver_sort(vecp_begin(&s->learnts), vecp_size(&s->learnts), &clause_cmp);
+
+ for (i = j = 0; i < vecp_size(&s->learnts) / 2; i++){
+ if (clause_size(learnts[i]) > 2 && reasons[lit_var(*clause_begin(learnts[i]))] != learnts[i])
+ clause_remove(s,learnts[i]);
+ else
+ learnts[j++] = learnts[i];
+ }
+ for (; i < vecp_size(&s->learnts); i++){
+ if (clause_size(learnts[i]) > 2 && reasons[lit_var(*clause_begin(learnts[i]))] != learnts[i] && clause_activity(learnts[i]) < extra_lim)
+ clause_remove(s,learnts[i]);
+ else
+ learnts[j++] = learnts[i];
+ }
+
+ //printf("reducedb deleted %d\n", vecp_size(&s->learnts) - j);
+
+
+ vecp_resize(&s->learnts,j);
+}
+
+static lbool sat_solver_search(sat_solver* s, int nof_conflicts, int nof_learnts)
+{
+ int* levels = s->levels;
+ double var_decay = 0.95;
+ double clause_decay = 0.999;
+ double random_var_freq = 0.02;
+
+ int conflictC = 0;
+ veci learnt_clause;
+
+ assert(s->root_level == sat_solver_dlevel(s));
+
+ s->stats.starts++;
+ s->var_decay = (float)(1 / var_decay );
+ s->cla_decay = (float)(1 / clause_decay);
+ veci_resize(&s->model,0);
+ veci_new(&learnt_clause);
+
+ for (;;){
+ clause* confl = sat_solver_propagate(s);
+ if (confl != 0){
+ // CONFLICT
+ int blevel;
+
+#ifdef VERBOSEDEBUG
+ printf(L_IND"**CONFLICT**\n", L_ind);
+#endif
+ s->stats.conflicts++; conflictC++;
+ if (sat_solver_dlevel(s) == s->root_level){
+ veci_delete(&learnt_clause);
+ return l_False;
+ }
+
+ veci_resize(&learnt_clause,0);
+ sat_solver_analyze(s, confl, &learnt_clause);
+ blevel = veci_size(&learnt_clause) > 1 ? levels[lit_var(veci_begin(&learnt_clause)[1])] : s->root_level;
+ blevel = s->root_level > blevel ? s->root_level : blevel;
+ sat_solver_canceluntil(s,blevel);
+ sat_solver_record(s,&learnt_clause);
+ act_var_decay(s);
+ act_clause_decay(s);
+
+ }else{
+ // NO CONFLICT
+ int next;
+
+ if (nof_conflicts >= 0 && conflictC >= nof_conflicts){
+ // Reached bound on number of conflicts:
+ s->progress_estimate = sat_solver_progress(s);
+ sat_solver_canceluntil(s,s->root_level);
+ veci_delete(&learnt_clause);
+ return l_Undef; }
+
+ if (sat_solver_dlevel(s) == 0)
+ // Simplify the set of problem clauses:
+ sat_solver_simplify(s);
+
+ if (nof_learnts >= 0 && vecp_size(&s->learnts) - s->qtail >= nof_learnts)
+ // Reduce the set of learnt clauses:
+ sat_solver_reducedb(s);
+
+ // New variable decision:
+ s->stats.decisions++;
+ next = order_select(s,(float)random_var_freq);
+
+ if (next == var_Undef){
+ // Model found:
+ lbool* values = s->assigns;
+ int i;
+ veci_resize(&s->model, 0);
+ for (i = 0; i < s->size; i++)
+ veci_push(&s->model,(int)values[i]);
+ sat_solver_canceluntil(s,s->root_level);
+ veci_delete(&learnt_clause);
+
+ /*
+ veci apa; veci_new(&apa);
+ for (i = 0; i < s->size; i++)
+ veci_push(&apa,(int)(s->model.ptr[i] == l_True ? toLit(i) : lit_neg(toLit(i))));
+ printf("model: "); printlits((lit*)apa.ptr, (lit*)apa.ptr + veci_size(&apa)); printf("\n");
+ veci_delete(&apa);
+ */
+
+ return l_True;
+ }
+
+ assume(s,lit_neg(toLit(next)));
+ }
+ }
+
+ return l_Undef; // cannot happen
+}
+
+//=================================================================================================
+// External solver functions:
+
+sat_solver* sat_solver_new(void)
+{
+ sat_solver* s = (sat_solver*)malloc(sizeof(sat_solver));
+ memset( s, 0, sizeof(sat_solver) );
+
+ // initialize vectors
+ vecp_new(&s->clauses);
+ vecp_new(&s->learnts);
+ veci_new(&s->order);
+ veci_new(&s->trail_lim);
+ veci_new(&s->tagged);
+ veci_new(&s->stack);
+ veci_new(&s->model);
+
+ // initialize arrays
+ s->wlists = 0;
+ s->activity = 0;
+ s->assigns = 0;
+ s->orderpos = 0;
+ s->reasons = 0;
+ s->levels = 0;
+ s->tags = 0;
+ s->trail = 0;
+
+
+ // initialize other vars
+ s->size = 0;
+ s->cap = 0;
+ s->qhead = 0;
+ s->qtail = 0;
+ s->cla_inc = 1;
+ s->cla_decay = 1;
+ s->var_inc = 1;
+ s->var_decay = 1;
+ s->root_level = 0;
+ s->simpdb_assigns = 0;
+ s->simpdb_props = 0;
+ s->random_seed = 91648253;
+ s->progress_estimate = 0;
+ s->binary = (clause*)malloc(sizeof(clause) + sizeof(lit)*2);
+ s->binary->size_learnt = (2 << 1);
+ s->verbosity = 0;
+
+ s->stats.starts = 0;
+ s->stats.decisions = 0;
+ s->stats.propagations = 0;
+ s->stats.inspects = 0;
+ s->stats.conflicts = 0;
+ s->stats.clauses = 0;
+ s->stats.clauses_literals = 0;
+ s->stats.learnts = 0;
+ s->stats.learnts_literals = 0;
+ s->stats.max_literals = 0;
+ s->stats.tot_literals = 0;
+
+ return s;
+}
+
+
+void sat_solver_delete(sat_solver* s)
+{
+ int i;
+ for (i = 0; i < vecp_size(&s->clauses); i++)
+ free(vecp_begin(&s->clauses)[i]);
+
+ for (i = 0; i < vecp_size(&s->learnts); i++)
+ free(vecp_begin(&s->learnts)[i]);
+
+ // delete vectors
+ vecp_delete(&s->clauses);
+ vecp_delete(&s->learnts);
+ veci_delete(&s->order);
+ veci_delete(&s->trail_lim);
+ veci_delete(&s->tagged);
+ veci_delete(&s->stack);
+ veci_delete(&s->model);
+ free(s->binary);
+
+ // delete arrays
+ if (s->wlists != 0){
+ int i;
+ for (i = 0; i < s->size*2; i++)
+ vecp_delete(&s->wlists[i]);
+
+ // if one is different from null, all are
+ free(s->wlists);
+ free(s->activity );
+ free(s->assigns );
+ free(s->orderpos );
+ free(s->reasons );
+ free(s->levels );
+ free(s->trail );
+ free(s->tags );
+ }
+
+ free(s);
+}
+
+
+bool sat_solver_addclause(sat_solver* s, lit* begin, lit* end)
+{
+ lit *i,*j;
+ int maxvar;
+ lbool* values;
+ lit last;
+
+ if (begin == end) return false;
+
+ //printlits(begin,end); printf("\n");
+ // insertion sort
+ maxvar = lit_var(*begin);
+ for (i = begin + 1; i < end; i++){
+ lit l = *i;
+ maxvar = lit_var(l) > maxvar ? lit_var(l) : maxvar;
+ for (j = i; j > begin && *(j-1) > l; j--)
+ *j = *(j-1);
+ *j = l;
+ }
+ sat_solver_setnvars(s,maxvar+1);
+
+ //printlits(begin,end); printf("\n");
+ values = s->assigns;
+
+ // delete duplicates
+ last = lit_Undef;
+ for (i = j = begin; i < end; i++){
+ //printf("lit: "L_LIT", value = %d\n", L_lit(*i), (lit_sign(*i) ? -values[lit_var(*i)] : values[lit_var(*i)]));
+ lbool sig = !lit_sign(*i); sig += sig - 1;
+ if (*i == lit_neg(last) || sig == values[lit_var(*i)])
+ return true; // tautology
+ else if (*i != last && values[lit_var(*i)] == l_Undef)
+ last = *j++ = *i;
+ }
+
+ //printf("final: "); printlits(begin,j); printf("\n");
+
+ if (j == begin) // empty clause
+ return false;
+ else if (j - begin == 1) // unit clause
+ return enqueue(s,*begin,(clause*)0);
+
+ // create new clause
+ vecp_push(&s->clauses,clause_new(s,begin,j,0));
+
+
+ s->stats.clauses++;
+ s->stats.clauses_literals += j - begin;
+
+ return true;
+}
+
+
+bool sat_solver_simplify(sat_solver* s)
+{
+ clause** reasons;
+ int type;
+
+ assert(sat_solver_dlevel(s) == 0);
+
+ if (sat_solver_propagate(s) != 0)
+ return false;
+
+ if (s->qhead == s->simpdb_assigns || s->simpdb_props > 0)
+ return true;
+
+ reasons = s->reasons;
+ for (type = 0; type < 2; type++){
+ vecp* cs = type ? &s->learnts : &s->clauses;
+ clause** cls = (clause**)vecp_begin(cs);
+
+ int i, j;
+ for (j = i = 0; i < vecp_size(cs); i++){
+ if (reasons[lit_var(*clause_begin(cls[i]))] != cls[i] &&
+ clause_simplify(s,cls[i]) == l_True)
+ clause_remove(s,cls[i]);
+ else
+ cls[j++] = cls[i];
+ }
+ vecp_resize(cs,j);
+ }
+
+ s->simpdb_assigns = s->qhead;
+ // (shouldn't depend on 'stats' really, but it will do for now)
+ s->simpdb_props = (int)(s->stats.clauses_literals + s->stats.learnts_literals);
+
+ return true;
+}
+
+
+int sat_solver_solve(sat_solver* s, lit* begin, lit* end)
+{
+ double nof_conflicts = 100;
+ double nof_learnts = sat_solver_nclauses(s) / 3;
+ lbool status = l_Undef;
+ lbool* values = s->assigns;
+ lit* i;
+
+ //printf("solve: "); printlits(begin, end); printf("\n");
+ for (i = begin; i < end; i++){
+ switch (lit_sign(*i) ? -values[lit_var(*i)] : values[lit_var(*i)]){
+ case 1: /* l_True: */
+ break;
+ case 0: /* l_Undef */
+ assume(s, *i);
+ if (sat_solver_propagate(s) == NULL)
+ break;
+ // falltrough
+ case -1: /* l_False */
+ sat_solver_canceluntil(s, 0);
+ return l_False;
+ }
+ }
+
+ s->root_level = sat_solver_dlevel(s);
+
+ if (s->verbosity >= 1){
+ printf("==================================[MINISAT]===================================\n");
+ printf("| Conflicts | ORIGINAL | LEARNT | Progress |\n");
+ printf("| | Clauses Literals | Limit Clauses Literals Lit/Cl | |\n");
+ printf("==============================================================================\n");
+ }
+
+ while (status == l_Undef){
+ double Ratio = (s->stats.learnts == 0)? 0.0 :
+ s->stats.learnts_literals / (double)s->stats.learnts;
+
+ if (s->verbosity >= 1){
+ printf("| %9.0f | %7.0f %8.0f | %7.0f %7.0f %8.0f %7.1f | %6.3f %% |\n",
+ (double)s->stats.conflicts,
+ (double)s->stats.clauses,
+ (double)s->stats.clauses_literals,
+ (double)nof_learnts,
+ (double)s->stats.learnts,
+ (double)s->stats.learnts_literals,
+ Ratio,
+ s->progress_estimate*100);
+ fflush(stdout);
+ }
+ status = sat_solver_search(s,(int)nof_conflicts, (int)nof_learnts);
+ nof_conflicts *= 1.5;
+ nof_learnts *= 1.1;
+ }
+ if (s->verbosity >= 1)
+ printf("==============================================================================\n");
+
+ sat_solver_canceluntil(s,0);
+ return status;
+}
+
+
+int sat_solver_nvars(sat_solver* s)
+{
+ return s->size;
+}
+
+
+int sat_solver_nclauses(sat_solver* s)
+{
+ return vecp_size(&s->clauses);
+}
+
+
+int sat_solver_nconflicts(sat_solver* s)
+{
+ return (int)s->stats.conflicts;
+}
+
+//=================================================================================================
+// Sorting functions (sigh):
+
+static inline void selectionsort(void** array, int size, int(*comp)(const void *, const void *))
+{
+ int i, j, best_i;
+ void* tmp;
+
+ for (i = 0; i < size-1; i++){
+ best_i = i;
+ for (j = i+1; j < size; j++){
+ if (comp(array[j], array[best_i]) < 0)
+ best_i = j;
+ }
+ tmp = array[i]; array[i] = array[best_i]; array[best_i] = tmp;
+ }
+}
+
+
+static void sortrnd(void** array, int size, int(*comp)(const void *, const void *), double* seed)
+{
+ if (size <= 15)
+ selectionsort(array, size, comp);
+
+ else{
+ void* pivot = array[irand(seed, size)];
+ void* tmp;
+ int i = -1;
+ int j = size;
+
+ for(;;){
+ do i++; while(comp(array[i], pivot)<0);
+ do j--; while(comp(pivot, array[j])<0);
+
+ if (i >= j) break;
+
+ tmp = array[i]; array[i] = array[j]; array[j] = tmp;
+ }
+
+ sortrnd(array , i , comp, seed);
+ sortrnd(&array[i], size-i, comp, seed);
+ }
+}
+
+void sat_solver_sort(void** array, int size, int(*comp)(const void *, const void *))
+{
+ double seed = 91648253;
+ sortrnd(array,size,comp,&seed);
+}
diff --git a/src/temp/ivy/satSolver.h b/src/temp/ivy/satSolver.h
new file mode 100644
index 00000000..401a28e7
--- /dev/null
+++ b/src/temp/ivy/satSolver.h
@@ -0,0 +1,141 @@
+/**************************************************************************************************
+MiniSat -- Copyright (c) 2005, Niklas Sorensson
+http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/
+
+Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
+associated documentation files (the "Software"), to deal in the Software without restriction,
+including without limitation the rights to use, copy, modify, merge, publish, distribute,
+sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all copies or
+substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
+NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
+DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
+OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+**************************************************************************************************/
+// Modified to compile with MS Visual Studio 6.0 by Alan Mishchenko
+
+#ifndef satSolver_h
+#define satSolver_h
+
+#ifdef _WIN32
+#define inline __inline // compatible with MS VS 6.0
+#endif
+
+#include "satVec.h"
+
+//=================================================================================================
+// Simple types:
+
+// does not work for c++
+typedef int bool;
+static const bool true = 1;
+static const bool false = 0;
+
+typedef int lit;
+typedef char lbool;
+
+#ifdef _WIN32
+typedef signed __int64 sint64; // compatible with MS VS 6.0
+#else
+typedef long long sint64;
+#endif
+
+static const int var_Undef = -1;
+static const lit lit_Undef = -2;
+
+static const lbool l_Undef = 0;
+static const lbool l_True = 1;
+static const lbool l_False = -1;
+
+static inline lit toLit (int v) { return v + v; }
+static inline lit toLitCond(int v, int c) { return v + v + (c != 0); }
+static inline lit lit_neg (lit l) { return l ^ 1; }
+static inline int lit_var (lit l) { return l >> 1; }
+static inline int lit_sign (lit l) { return l & 1; }
+
+
+//=================================================================================================
+// Public interface:
+
+struct sat_solver_t;
+typedef struct sat_solver_t sat_solver;
+
+extern sat_solver* sat_solver_new(void);
+extern void sat_solver_delete(sat_solver* s);
+
+extern bool sat_solver_addclause(sat_solver* s, lit* begin, lit* end);
+extern bool sat_solver_simplify(sat_solver* s);
+extern int sat_solver_solve(sat_solver* s, lit* begin, lit* end);
+
+extern int sat_solver_nvars(sat_solver* s);
+extern int sat_solver_nclauses(sat_solver* s);
+extern int sat_solver_nconflicts(sat_solver* s);
+
+extern void sat_solver_setnvars(sat_solver* s,int n);
+
+struct stats_t
+{
+ sint64 starts, decisions, propagations, inspects, conflicts;
+ sint64 clauses, clauses_literals, learnts, learnts_literals, max_literals, tot_literals;
+};
+typedef struct stats_t stats;
+
+extern void Sat_SolverWriteDimacs( sat_solver * p, char * pFileName, lit* assumptionsBegin, lit* assumptionsEnd, int incrementVars );
+extern void Sat_SolverPrintStats( FILE * pFile, sat_solver * p );
+
+//=================================================================================================
+// Solver representation:
+
+struct clause_t;
+typedef struct clause_t clause;
+
+struct sat_solver_t
+{
+ int size; // nof variables
+ int cap; // size of varmaps
+ int qhead; // Head index of queue.
+ int qtail; // Tail index of queue.
+
+ // clauses
+ vecp clauses; // List of problem constraints. (contains: clause*)
+ vecp learnts; // List of learnt clauses. (contains: clause*)
+
+ // activities
+ double var_inc; // Amount to bump next variable with.
+ double var_decay; // INVERSE decay factor for variable activity: stores 1/decay.
+ float cla_inc; // Amount to bump next clause with.
+ float cla_decay; // INVERSE decay factor for clause activity: stores 1/decay.
+
+ vecp* wlists; //
+ double* activity; // A heuristic measurement of the activity of a variable.
+ lbool* assigns; // Current values of variables.
+ int* orderpos; // Index in variable order.
+ clause** reasons; //
+ int* levels; //
+ lit* trail;
+
+ clause* binary; // A temporary binary clause
+ lbool* tags; //
+ veci tagged; // (contains: var)
+ veci stack; // (contains: var)
+
+ veci order; // Variable order. (heap) (contains: var)
+ veci trail_lim; // Separator indices for different decision levels in 'trail'. (contains: int)
+ veci model; // If problem is solved, this vector contains the model (contains: lbool).
+
+ int root_level; // Level of first proper decision.
+ int simpdb_assigns;// Number of top-level assignments at last 'simplifyDB()'.
+ int simpdb_props; // Number of propagations before next 'simplifyDB()'.
+ double random_seed;
+ double progress_estimate;
+ int verbosity; // Verbosity level. 0=silent, 1=some progress report, 2=everything
+
+ stats stats;
+};
+
+#endif
diff --git a/src/temp/ivy/satUtil.c b/src/temp/ivy/satUtil.c
new file mode 100644
index 00000000..f2b78fe6
--- /dev/null
+++ b/src/temp/ivy/satUtil.c
@@ -0,0 +1,161 @@
+/**CFile****************************************************************
+
+ FileName [satUtil.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [C-language MiniSat solver.]
+
+ Synopsis [Additional SAT solver procedures.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: satUtil.c,v 1.4 2005/09/16 22:55:03 casem Exp $]
+
+***********************************************************************/
+
+#include <stdio.h>
+#include <assert.h>
+#include "satSolver.h"
+#include "extra.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+struct clause_t
+{
+ int size_learnt;
+ lit lits[0];
+};
+
+static inline int clause_size( clause* c ) { return c->size_learnt >> 1; }
+static inline lit* clause_begin( clause* c ) { return c->lits; }
+
+static void Sat_SolverClauseWriteDimacs( FILE * pFile, clause * pC, bool fIncrement );
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Write the clauses in the solver into a file in DIMACS format.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Sat_SolverWriteDimacs( sat_solver * p, char * pFileName, lit* assumptionsBegin, lit* assumptionsEnd, int incrementVars )
+{
+ FILE * pFile;
+ void ** pClauses;
+ int nClauses, i;
+
+ // count the number of clauses
+ nClauses = p->clauses.size + p->learnts.size;
+ for ( i = 0; i < p->size; i++ )
+ if ( p->levels[i] == 0 && p->assigns[i] != l_Undef )
+ nClauses++;
+
+ // start the file
+ pFile = fopen( pFileName, "wb" );
+ if ( pFile == NULL )
+ {
+ printf( "Sat_SolverWriteDimacs(): Cannot open the ouput file.\n" );
+ return;
+ }
+ fprintf( pFile, "c CNF generated by ABC on %s\n", Extra_TimeStamp() );
+ fprintf( pFile, "p cnf %d %d\n", p->size, nClauses );
+
+ // write the original clauses
+ nClauses = p->clauses.size;
+ pClauses = p->clauses.ptr;
+ for ( i = 0; i < nClauses; i++ )
+ Sat_SolverClauseWriteDimacs( pFile, pClauses[i], incrementVars );
+
+ // write the learned clauses
+ nClauses = p->learnts.size;
+ pClauses = p->learnts.ptr;
+ for ( i = 0; i < nClauses; i++ )
+ Sat_SolverClauseWriteDimacs( pFile, pClauses[i], incrementVars );
+
+ // write zero-level assertions
+ for ( i = 0; i < p->size; i++ )
+ if ( p->levels[i] == 0 && p->assigns[i] != l_Undef )
+ fprintf( pFile, "%s%d%s\n",
+ (p->assigns[i] == l_False)? "-": "",
+ i + (int)(incrementVars>0),
+ (incrementVars) ? " 0" : "");
+
+ // write the assumptions
+ if (assumptionsBegin) {
+ for (; assumptionsBegin != assumptionsEnd; assumptionsBegin++) {
+ fprintf( pFile, "%s%d%s\n",
+ lit_sign(*assumptionsBegin)? "-": "",
+ lit_var(*assumptionsBegin) + (int)(incrementVars>0),
+ (incrementVars) ? " 0" : "");
+ }
+ }
+
+ fprintf( pFile, "\n" );
+ fclose( pFile );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Writes the given clause in a file in DIMACS format.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Sat_SolverClauseWriteDimacs( FILE * pFile, clause * pC, bool fIncrement )
+{
+ lit * pLits = clause_begin(pC);
+ int nLits = clause_size(pC);
+ int i;
+
+ for ( i = 0; i < nLits; i++ )
+ fprintf( pFile, "%s%d ", (lit_sign(pLits[i])? "-": ""), lit_var(pLits[i]) + (int)(fIncrement>0) );
+ if ( fIncrement )
+ fprintf( pFile, "0" );
+ fprintf( pFile, "\n" );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Writes the given clause in a file in DIMACS format.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Sat_SolverPrintStats( FILE * pFile, sat_solver * p )
+{
+ printf( "starts : %d\n", (int)p->stats.starts );
+ printf( "conflicts : %d\n", (int)p->stats.conflicts );
+ printf( "decisions : %d\n", (int)p->stats.decisions );
+ printf( "propagations : %d\n", (int)p->stats.propagations );
+ printf( "inspects : %d\n", (int)p->stats.inspects );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/temp/ivy/satVec.h b/src/temp/ivy/satVec.h
new file mode 100644
index 00000000..ffa9c431
--- /dev/null
+++ b/src/temp/ivy/satVec.h
@@ -0,0 +1,83 @@
+/**************************************************************************************************
+MiniSat -- Copyright (c) 2005, Niklas Sorensson
+http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/
+
+Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
+associated documentation files (the "Software"), to deal in the Software without restriction,
+including without limitation the rights to use, copy, modify, merge, publish, distribute,
+sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all copies or
+substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
+NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
+DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
+OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+**************************************************************************************************/
+// Modified to compile with MS Visual Studio 6.0 by Alan Mishchenko
+
+#ifndef satVec_h
+#define satVec_h
+
+#include <stdlib.h>
+
+// vector of 32-bit intergers (added for 64-bit portability)
+struct veci_t {
+ int size;
+ int cap;
+ int* ptr;
+};
+typedef struct veci_t veci;
+
+static inline void veci_new (veci* v) {
+ v->size = 0;
+ v->cap = 4;
+ v->ptr = (int*)malloc(sizeof(int)*v->cap);
+}
+
+static inline void veci_delete (veci* v) { free(v->ptr); }
+static inline int* veci_begin (veci* v) { return v->ptr; }
+static inline int veci_size (veci* v) { return v->size; }
+static inline void veci_resize (veci* v, int k) { v->size = k; } // only safe to shrink !!
+static inline void veci_push (veci* v, int e)
+{
+ if (v->size == v->cap) {
+ int newsize = v->cap * 2+1;
+ v->ptr = (int*)realloc(v->ptr,sizeof(int)*newsize);
+ v->cap = newsize; }
+ v->ptr[v->size++] = e;
+}
+
+
+// vector of 32- or 64-bit pointers
+struct vecp_t {
+ int size;
+ int cap;
+ void** ptr;
+};
+typedef struct vecp_t vecp;
+
+static inline void vecp_new (vecp* v) {
+ v->size = 0;
+ v->cap = 4;
+ v->ptr = (void**)malloc(sizeof(void*)*v->cap);
+}
+
+static inline void vecp_delete (vecp* v) { free(v->ptr); }
+static inline void** vecp_begin (vecp* v) { return v->ptr; }
+static inline int vecp_size (vecp* v) { return v->size; }
+static inline void vecp_resize (vecp* v, int k) { v->size = k; } // only safe to shrink !!
+static inline void vecp_push (vecp* v, void* e)
+{
+ if (v->size == v->cap) {
+ int newsize = v->cap * 2+1;
+ v->ptr = (void**)realloc(v->ptr,sizeof(void*)*newsize);
+ v->cap = newsize; }
+ v->ptr[v->size++] = e;
+}
+
+
+#endif
diff --git a/src/temp/player/playerToAbc.c b/src/temp/player/playerToAbc.c
index e06eca28..7c6ab114 100644
--- a/src/temp/player/playerToAbc.c
+++ b/src/temp/player/playerToAbc.c
@@ -91,6 +91,7 @@ void * Abc_NtkPlayer( void * pNtk, int nLutMax, int nPlaMax, int RankCost, int f
Ivy_FastMapPerform( pMan, nLutMax );
// convert from the extended AIG manager into an SOP network
pNtkNew = Ivy_ManToAbc( pNtk, pMan, NULL, fFastMode );
+// pNtkNew = NULL;
Ivy_FastMapStop( pMan );
}
else
@@ -104,7 +105,7 @@ void * Abc_NtkPlayer( void * pNtk, int nLutMax, int nPlaMax, int RankCost, int f
}
Ivy_ManStop( pMan );
// chech the resulting network
- if ( !Abc_NtkCheck( pNtkNew ) )
+ if ( pNtkNew && !Abc_NtkCheck( pNtkNew ) )
{
printf( "Abc_NtkPlayer: The network check has failed.\n" );
Abc_NtkDelete( pNtkNew );
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-04 14:44:41 +0000