summaryrefslogtreecommitdiffstats
path: root/src/temp/ivy
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2006-10-07 08:01:00 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2006-10-07 08:01:00 -0700
commit73bb7932f7edad95086d67a795444537c438309e (patch)
tree43ce6255913e15ecb3f4f8a41ac531d6679ddcf1 /src/temp/ivy
parent0da555cb481696efd78d9c5dc6293b6a95d1ffd5 (diff)
downloadabc-73bb7932f7edad95086d67a795444537c438309e.tar.gz
abc-73bb7932f7edad95086d67a795444537c438309e.tar.bz2
abc-73bb7932f7edad95086d67a795444537c438309e.zip
Version abc61007
Diffstat (limited to 'src/temp/ivy')
-rw-r--r--src/temp/ivy/ivy.h13
-rw-r--r--src/temp/ivy/ivyFastMap.c41
-rw-r--r--src/temp/ivy/ivyFraig.c626
-rw-r--r--src/temp/ivy/ivyMan.c104
-rw-r--r--src/temp/ivy/ivyResyn.c50
-rw-r--r--src/temp/ivy/module.make4
-rw-r--r--src/temp/ivy/satMem.c527
-rw-r--r--src/temp/ivy/satMem.h78
-rw-r--r--src/temp/ivy/satSolver.c1279
-rw-r--r--src/temp/ivy/satSolver.h154
-rw-r--r--src/temp/ivy/satUtil.c161
-rw-r--r--src/temp/ivy/satVec.h83
12 files changed, 603 insertions, 2517 deletions
diff --git a/src/temp/ivy/ivy.h b/src/temp/ivy/ivy.h
index d9c17d80..e7c9bc2e 100644
--- a/src/temp/ivy/ivy.h
+++ b/src/temp/ivy/ivy.h
@@ -129,9 +129,12 @@ struct Ivy_Man_t_
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
+ double dSimSatur; // the ratio of refined classes when saturation is reached
int fPatScores; // enables simulation pattern scoring
int MaxScore; // max score after which resimulation is used
+ double dActConeRatio; // the ratio of cone to be bumped
+ double dActConeBumpMax; // the largest bump in activity
+ int fProve; // prove the miter outputs
int fVerbose; // verbose output
int nBTLimitNode; // conflict limit at a node
int nBTLimitMiter; // conflict limit at an output
@@ -445,14 +448,14 @@ extern void Ivy_ObjCollectFanouts( Ivy_Man_t * p, Ivy_Obj_t * pObj, V
extern Ivy_Obj_t * Ivy_ObjReadFirstFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj );
extern int Ivy_ObjFanoutNum( Ivy_Man_t * p, Ivy_Obj_t * pObj );
/*=== ivyFastMap.c =============================================================*/
-extern void Ivy_FastMapPerform( Ivy_Man_t * pAig, int nLimit );
+extern void Ivy_FastMapPerform( Ivy_Man_t * pAig, int nLimit, int fRecovery, int fVerbose );
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_FraigMiter( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams );
+extern int Ivy_FraigProve( Ivy_Man_t ** ppManAig, void * pPars );
extern Ivy_Man_t * Ivy_FraigPerform( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams );
-extern Ivy_Man_t * Ivy_FraigProve( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams );
+extern Ivy_Man_t * Ivy_FraigMiter( 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 );
@@ -505,6 +508,7 @@ extern Ivy_Obj_t * Ivy_Latch( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Init_t In
/*=== ivyResyn.c =========================================================*/
extern Ivy_Man_t * Ivy_ManResyn0( Ivy_Man_t * p, int fUpdateLevel, int fVerbose );
extern Ivy_Man_t * Ivy_ManResyn( Ivy_Man_t * p, int fUpdateLevel, int fVerbose );
+extern Ivy_Man_t * Ivy_ManRwsat( Ivy_Man_t * pMan, int fVerbose );
/*=== ivyRewrite.c =========================================================*/
extern int Ivy_ManSeqRewrite( Ivy_Man_t * p, int fUpdateLevel, int fUseZeroCost );
extern int Ivy_ManRewriteAlg( Ivy_Man_t * p, int fUpdateLevel, int fUseZeroCost );
@@ -524,6 +528,7 @@ extern void Ivy_TableProfile( Ivy_Man_t * p );
extern void Ivy_ManIncrementTravId( Ivy_Man_t * p );
extern void Ivy_ManCleanTravId( Ivy_Man_t * p );
extern unsigned * Ivy_ManCutTruth( Ivy_Man_t * p, Ivy_Obj_t * pRoot, Vec_Int_t * vLeaves, Vec_Int_t * vNodes, Vec_Int_t * vTruth );
+extern void Ivy_ManCollectCut( Ivy_Man_t * p, Ivy_Obj_t * pRoot, Vec_Int_t * vLeaves, Vec_Int_t * vNodes );
extern Vec_Int_t * Ivy_ManLatches( Ivy_Man_t * p );
extern int Ivy_ManLevels( Ivy_Man_t * p );
extern void Ivy_ManResetLevels( Ivy_Man_t * p );
diff --git a/src/temp/ivy/ivyFastMap.c b/src/temp/ivy/ivyFastMap.c
index 39c632c7..c4a043f2 100644
--- a/src/temp/ivy/ivyFastMap.c
+++ b/src/temp/ivy/ivyFastMap.c
@@ -64,7 +64,7 @@ static inline Ivy_Supp_t * Ivy_ObjSuppStart( Ivy_Man_t * pAig, Ivy_Obj_t * pObj
return pSupp;
}
-static int Ivy_FastMapPrint( Ivy_Man_t * pAig, int Time );
+static void Ivy_FastMapPrint( Ivy_Man_t * pAig, int Delay, int Area, int Time, char * pStr );
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 );
@@ -99,11 +99,11 @@ extern int s_MappingMem;
SeeAlso []
***********************************************************************/
-void Ivy_FastMapPerform( Ivy_Man_t * pAig, int nLimit )
+void Ivy_FastMapPerform( Ivy_Man_t * pAig, int nLimit, int fRecovery, int fVerbose )
{
Ivy_SuppMan_t * pMan;
Ivy_Obj_t * pObj;
- int i, Delay, clk, clkTotal = clock();
+ int i, Delay, Area, clk, clkTotal = clock();
// start the memory for supports
pMan = ALLOC( Ivy_SuppMan_t, 1 );
memset( pMan, 0, sizeof(Ivy_SuppMan_t) );
@@ -123,32 +123,43 @@ clk = clock();
Ivy_ManForEachNode( pAig, pObj, i )
Ivy_FastMapNode( pAig, pObj, nLimit );
// find the best arrival time and area
- printf( "Delay oriented mapping: " );
- Delay = Ivy_FastMapPrint( pAig, clock() - clk );
+ Delay = Ivy_FastMapDelay( pAig );
+ Area = Ivy_FastMapArea(pAig);
+ if ( fVerbose )
+ Ivy_FastMapPrint( pAig, Delay, Area, clock() - clk, "Delay oriented mapping: " );
// 2-1-2 (doing 2-1-2-1-2 improves 0.5%)
+ if ( fRecovery )
+ {
clk = clock();
Ivy_FastMapRequired( pAig, Delay, 0 );
// remap the nodes
Ivy_FastMapRecover( pAig, nLimit );
- printf( "Area recovery 2 : " );
- Delay = Ivy_FastMapPrint( pAig, clock() - clk );
+ Delay = Ivy_FastMapDelay( pAig );
+ Area = Ivy_FastMapArea(pAig);
+ if ( fVerbose )
+ Ivy_FastMapPrint( pAig, Delay, Area, clock() - clk, "Area recovery 2 : " );
clk = clock();
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 );
+ Delay = Ivy_FastMapDelay( pAig );
+ Area = Ivy_FastMapArea(pAig);
+ if ( fVerbose )
+ Ivy_FastMapPrint( pAig, Delay, Area, clock() - clk, "Area recovery 1 : " );
clk = clock();
Ivy_FastMapRequired( pAig, Delay, 0 );
// remap the nodes
Ivy_FastMapRecover( pAig, nLimit );
- printf( "Area recovery 2 : " );
- Delay = Ivy_FastMapPrint( pAig, clock() - clk );
+ Delay = Ivy_FastMapDelay( pAig );
+ Area = Ivy_FastMapArea(pAig);
+ if ( fVerbose )
+ Ivy_FastMapPrint( pAig, Delay, Area, clock() - clk, "Area recovery 2 : " );
+ }
s_MappingTime = clock() - clkTotal;
@@ -196,14 +207,10 @@ void Ivy_FastMapStop( Ivy_Man_t * pAig )
SeeAlso []
***********************************************************************/
-int Ivy_FastMapPrint( Ivy_Man_t * pAig, int Time )
+void Ivy_FastMapPrint( Ivy_Man_t * pAig, int Delay, int Area, int Time, char * pStr )
{
- int Delay, Area;
- Delay = Ivy_FastMapDelay( pAig );
- Area = Ivy_FastMapArea( pAig );
- printf( "Delay = %3d. Area = %6d. ", Delay, Area );
+ printf( "%s : Delay = %3d. Area = %6d. ", pStr, Delay, Area );
PRT( "Time", Time );
- return Delay;
}
/**Function*************************************************************
diff --git a/src/temp/ivy/ivyFraig.c b/src/temp/ivy/ivyFraig.c
index 88c726c7..9c729b23 100644
--- a/src/temp/ivy/ivyFraig.c
+++ b/src/temp/ivy/ivyFraig.c
@@ -98,6 +98,38 @@ struct Ivy_FraigMan_t_
int time2;
};
+typedef struct Prove_ParamsStruct_t_ Prove_Params_t;
+struct Prove_ParamsStruct_t_
+{
+ // general parameters
+ int fUseFraiging; // enables fraiging
+ int fUseRewriting; // enables rewriting
+ int fUseBdds; // enables BDD construction when other methods fail
+ int fVerbose; // prints verbose stats
+ // iterations
+ int nItersMax; // the number of iterations
+ // mitering
+ int nMiteringLimitStart; // starting mitering limit
+ float nMiteringLimitMulti; // multiplicative coefficient to increase the limit in each iteration
+ // rewriting
+ int nRewritingLimitStart; // the number of rewriting iterations
+ float nRewritingLimitMulti; // multiplicative coefficient to increase the limit in each iteration
+ // fraiging
+ int nFraigingLimitStart; // starting backtrack(conflict) limit
+ float nFraigingLimitMulti; // multiplicative coefficient to increase the limit in each iteration
+ // last-gasp BDD construction
+ int nBddSizeLimit; // the number of BDD nodes when construction is aborted
+ int fBddReorder; // enables dynamic BDD variable reordering
+ // last-gasp mitering
+ int nMiteringLimitLast; // final mitering limit
+ // global SAT solver limits
+ sint64 nTotalBacktrackLimit; // global limit on the number of backtracks
+ sint64 nTotalInspectLimit; // global limit on the number of clause inspects
+ // global resources applied
+ sint64 nTotalBacktracksMade; // the total number of backtracks made
+ sint64 nTotalInspectsMade; // the total number of inspects made
+};
+
static inline Ivy_FraigSim_t * Ivy_ObjSim( Ivy_Obj_t * pObj ) { return (Ivy_FraigSim_t *)pObj->pFanout; }
static inline Ivy_Obj_t * Ivy_ObjClassNodeLast( Ivy_Obj_t * pObj ) { return pObj->pNextFan0; }
static inline Ivy_Obj_t * Ivy_ObjClassNodeRepr( Ivy_Obj_t * pObj ) { return pObj->pNextFan0; }
@@ -146,6 +178,7 @@ static inline unsigned Ivy_ObjRandomSim() { return (ran
static Ivy_FraigMan_t * Ivy_FraigStart( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams );
static Ivy_FraigMan_t * Ivy_FraigStartSimple( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams );
+static Ivy_Man_t * Ivy_FraigPerform_int( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams, sint64 * pnSatConfs, sint64 * pnSatInspects );
static void Ivy_FraigPrint( Ivy_FraigMan_t * p );
static void Ivy_FraigStop( Ivy_FraigMan_t * p );
static void Ivy_FraigSimulate( Ivy_FraigMan_t * p );
@@ -154,10 +187,12 @@ static Ivy_Obj_t * Ivy_FraigAnd( Ivy_FraigMan_t * p, Ivy_Obj_t * pObjOld );
static int Ivy_FraigNodesAreEquiv( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj0, Ivy_Obj_t * pObj1 );
static int Ivy_FraigNodeIsConst( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj );
static void Ivy_FraigNodeAddToSolver( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj0, Ivy_Obj_t * pObj1 );
-static int Ivy_FraigMarkConeSetActivity( Ivy_FraigMan_t * p, Ivy_Obj_t * pOld, Ivy_Obj_t * pNew );
+static int Ivy_FraigSetActivityFactors( Ivy_FraigMan_t * p, Ivy_Obj_t * pOld, Ivy_Obj_t * pNew );
static void Ivy_FraigAddToPatScores( Ivy_FraigMan_t * p, Ivy_Obj_t * pClass, Ivy_Obj_t * pClassNew );
-static int Ivy_FraigMiterStatus( Ivy_FraigMan_t * p );
+static int Ivy_FraigMiterStatus( Ivy_Man_t * pMan );
static void Ivy_FraigMiterProve( Ivy_FraigMan_t * p );
+static void Ivy_FraigMiterPrint( Ivy_Man_t * pNtk, char * pString, int clk, int fVerbose );
+static int * Ivy_FraigCreateModel( Ivy_FraigMan_t * p );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
@@ -165,7 +200,7 @@ static void Ivy_FraigMiterProve( Ivy_FraigMan_t * p );
/**Function*************************************************************
- Synopsis [Performs fraiging of the initial AIG.]
+ Synopsis [Sets the default solving parameters.]
Description []
@@ -174,11 +209,184 @@ static void Ivy_FraigMiterProve( Ivy_FraigMan_t * p );
SeeAlso []
***********************************************************************/
-Ivy_Man_t * Ivy_FraigProve( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams )
+void Ivy_FraigParamsDefault( Ivy_FraigParams_t * pParams )
{
+ memset( pParams, 0, sizeof(Ivy_FraigParams_t) );
+ pParams->nSimWords = 32; // the number of words in the simulation info
+ pParams->dSimSatur = 0.005; // the ratio of refined classes when saturation is reached
+ pParams->fPatScores = 0; // enables simulation pattern scoring
+ pParams->MaxScore = 25; // max score after which resimulation is used
+// pParams->dActConeRatio = 0.05; // the ratio of cone to be bumped
+// pParams->dActConeBumpMax = 5.0; // the largest bump of activity
+ pParams->dActConeRatio = 0.3; // the ratio of cone to be bumped
+ pParams->dActConeBumpMax = 10.0; // the largest bump of activity
+
+ pParams->nBTLimitNode = 100; // conflict limit at a node
+ pParams->nBTLimitMiter = 500000; // conflict limit at an output
+ pParams->nBTLimitGlobal = 0; // conflict limit global
+ pParams->nInsLimitNode = 0; // inspection limit at a node
+ pParams->nInsLimitMiter = 0; // inspection limit at an output
+ pParams->nInsLimitGlobal = 0; // inspection limit global
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs combinational equivalence checking for the miter.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ivy_FraigProve( Ivy_Man_t ** ppManAig, void * pPars )
+{
+ Prove_Params_t * pParams = pPars;
+ Ivy_FraigParams_t Params, * pIvyParams = &Params;
+ Ivy_Man_t * pManAig, * pManTemp;
+ int RetValue, nIter, Counter, clk, timeStart = clock();
+ sint64 nSatConfs, nSatInspects, nInspectLimit;
+
+ // start the network and parameters
+ pManAig = *ppManAig;
+ Ivy_FraigParamsDefault( pIvyParams );
+ pIvyParams->fVerbose = pParams->fVerbose;
+ pIvyParams->fProve = 1;
+
+ if ( pParams->fVerbose )
+ {
+ printf( "RESOURCE LIMITS: Iterations = %d. Rewriting = %s. Fraiging = %s.\n",
+ pParams->nItersMax, pParams->fUseRewriting? "yes":"no", pParams->fUseFraiging? "yes":"no" );
+ printf( "Mitering = %d (%3.1f). Rewriting = %d (%3.1f). Fraiging = %d (%3.1f).\n",
+ pParams->nMiteringLimitStart, pParams->nMiteringLimitMulti,
+ pParams->nRewritingLimitStart, pParams->nRewritingLimitMulti,
+ pParams->nFraigingLimitStart, pParams->nFraigingLimitMulti );
+ printf( "Mitering last = %d.\n",
+ pParams->nMiteringLimitLast );
+ }
+
+ // if SAT only, solve without iteration
+ if ( !pParams->fUseRewriting && !pParams->fUseFraiging )
+ {
+ clk = clock();
+ pIvyParams->nBTLimitMiter = pParams->nMiteringLimitLast / Ivy_ManPoNum(pManAig);
+ pManAig = Ivy_FraigMiter( pManTemp = pManAig, pIvyParams ); Ivy_ManStop( pManTemp );
+ RetValue = Ivy_FraigMiterStatus( pManAig );
+ Ivy_FraigMiterPrint( pManAig, "SAT solving", clk, pParams->fVerbose );
+ *ppManAig = pManAig;
+ return RetValue;
+ }
+
+ if ( Ivy_ManNodeNum(pManAig) < 500 )
+ {
+ // run the first mitering
+ clk = clock();
+ pIvyParams->nBTLimitMiter = pParams->nMiteringLimitStart / Ivy_ManPoNum(pManAig);
+ pManAig = Ivy_FraigMiter( pManTemp = pManAig, pIvyParams ); Ivy_ManStop( pManTemp );
+ RetValue = Ivy_FraigMiterStatus( pManAig );
+ Ivy_FraigMiterPrint( pManAig, "SAT solving", clk, pParams->fVerbose );
+ if ( RetValue >= 0 )
+ {
+ *ppManAig = pManAig;
+ return RetValue;
+ }
+ }
+
+ // check the current resource limits
+ RetValue = -1;
+ for ( nIter = 0; nIter < pParams->nItersMax; nIter++ )
+ {
+ if ( pParams->fVerbose )
+ {
+ printf( "ITERATION %2d : Confs = %6d. FraigBTL = %3d. \n", nIter+1,
+ (int)(pParams->nMiteringLimitStart * pow(pParams->nMiteringLimitMulti,nIter)),
+ (int)(pParams->nFraigingLimitStart * pow(pParams->nFraigingLimitMulti,nIter)) );
+ fflush( stdout );
+ }
+
+ // try rewriting
+ if ( pParams->fUseRewriting )
+ {
+ clk = clock();
+ Counter = (int)(pParams->nRewritingLimitStart * pow(pParams->nRewritingLimitMulti,nIter));
+ pManAig = Ivy_ManRwsat( pManAig, 0 );
+ RetValue = Ivy_FraigMiterStatus( pManAig );
+ Ivy_FraigMiterPrint( pManAig, "Rewriting ", clk, pParams->fVerbose );
+ }
+ if ( RetValue >= 0 )
+ break;
+
+ // try fraiging followed by mitering
+ if ( pParams->fUseFraiging )
+ {
+ clk = clock();
+ nInspectLimit = pParams->nTotalInspectLimit? pParams->nTotalInspectLimit - pParams->nTotalInspectsMade : 0;
+ pIvyParams->nBTLimitNode = (int)(pParams->nFraigingLimitStart * pow(pParams->nFraigingLimitMulti,nIter));
+ pIvyParams->nBTLimitMiter = (int)(pParams->nMiteringLimitStart * pow(pParams->nMiteringLimitMulti,nIter)) / Ivy_ManPoNum(pManAig);
+ pManAig = Ivy_FraigPerform_int( pManTemp = pManAig, pIvyParams, &nSatConfs, &nSatInspects ); Ivy_ManStop( pManTemp );
+ RetValue = Ivy_FraigMiterStatus( pManAig );
+ Ivy_FraigMiterPrint( pManAig, "Fraiging ", clk, pParams->fVerbose );
+ }
+ if ( RetValue >= 0 )
+ break;
+
+ // add to the number of backtracks and inspects
+ pParams->nTotalBacktracksMade += nSatConfs;
+ pParams->nTotalInspectsMade += nSatInspects;
+ // check if global resource limit is reached
+ if ( (pParams->nTotalBacktrackLimit && pParams->nTotalBacktracksMade >= pParams->nTotalBacktrackLimit) ||
+ (pParams->nTotalInspectLimit && pParams->nTotalInspectsMade >= pParams->nTotalInspectLimit) )
+ {
+ printf( "Reached global limit on conflicts/inspects. Quitting.\n" );
+ *ppManAig = pManAig;
+ return -1;
+ }
+ }
+
+ if ( RetValue < 0 )
+ {
+ if ( pParams->fVerbose )
+ {
+ printf( "Attempting SAT with conflict limit %d ...\n", pParams->nMiteringLimitLast );
+ fflush( stdout );
+ }
+ clk = clock();
+ nInspectLimit = pParams->nTotalInspectLimit? pParams->nTotalInspectLimit - pParams->nTotalInspectsMade : 0;
+ pIvyParams->nBTLimitMiter = pParams->nMiteringLimitLast / Ivy_ManPoNum(pManAig);
+ pManAig = Ivy_FraigMiter( pManTemp = pManAig, pIvyParams ); Ivy_ManStop( pManTemp );
+ RetValue = Ivy_FraigMiterStatus( pManAig );
+ Ivy_FraigMiterPrint( pManAig, "SAT solving", clk, pParams->fVerbose );
+ }
+
+ // assign the model if it was proved by rewriting (const 1 miter)
+ if ( RetValue == 0 && pManAig->pData == NULL )
+ {
+ pManAig->pData = ALLOC( int, Ivy_ManPiNum(pManAig) );
+ memset( pManAig->pData, 0, sizeof(int) * Ivy_ManPiNum(pManAig) );
+ }
+ *ppManAig = pManAig;
+ return RetValue;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs fraiging of the AIG.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Ivy_Man_t * Ivy_FraigPerform_int( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams, sint64 * pnSatConfs, sint64 * pnSatInspects )
+{
Ivy_FraigMan_t * p;
Ivy_Man_t * pManAigNew;
int clk;
+ if ( Ivy_ManNodeNum(pManAig) == 0 )
+ return Ivy_ManDup(pManAig);
clk = clock();
assert( Ivy_ManLatchNum(pManAig) == 0 );
p = Ivy_FraigStart( pManAig, pParams );
@@ -186,13 +394,17 @@ clk = clock();
Ivy_FraigSweep( p );
pManAigNew = p->pManFraig;
p->timeTotal = clock() - clk;
+ if ( pnSatConfs )
+ *pnSatConfs = p->pSat? p->pSat->stats.conflicts : 0;
+ if ( pnSatInspects )
+ *pnSatInspects = p->pSat? p->pSat->stats.inspects : 0;
Ivy_FraigStop( p );
return pManAigNew;
}
/**Function*************************************************************
- Synopsis [Performs fraiging of the initial AIG.]
+ Synopsis [Performs fraiging of the AIG.]
Description []
@@ -206,6 +418,8 @@ Ivy_Man_t * Ivy_FraigPerform( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams )
Ivy_FraigMan_t * p;
Ivy_Man_t * pManAigNew;
int clk;
+ if ( Ivy_ManNodeNum(pManAig) == 0 )
+ return Ivy_ManDup(pManAig);
clk = clock();
assert( Ivy_ManLatchNum(pManAig) == 0 );
p = Ivy_FraigStart( pManAig, pParams );
@@ -219,7 +433,7 @@ p->timeTotal = clock() - clk;
/**Function*************************************************************
- Synopsis [Performs fraiging of the initial AIG.]
+ Synopsis [Applies brute-force SAT to the miter.]
Description []
@@ -256,39 +470,16 @@ clk = clock();
Ivy_ManCleanup( p->pManFraig );
pManAigNew = p->pManFraig;
p->timeTotal = clock() - clk;
+
+//printf( "Final nodes = %6d. ", Ivy_ManNodeNum(pManAigNew) );
+//PRT( "Time", p->timeTotal );
Ivy_FraigStop( p );
return pManAigNew;
}
/**Function*************************************************************
- Synopsis [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;
- pParams->fPatScores = 0;
- pParams->MaxScore = 25;
- pParams->nBTLimitNode = 100; // conflict limit at a node
- pParams->nBTLimitMiter = 500000; // conflict limit at an output
- pParams->nBTLimitGlobal = 0; // conflict limit global
- pParams->nInsLimitNode = 0; // inspection limit at a node
- pParams->nInsLimitMiter = 0; // inspection limit at an output
- pParams->nInsLimitGlobal = 0; // inspection limit global
-}
-
-/**Function*************************************************************
-
- Synopsis [Starts the fraiging manager.]
+ Synopsis [Starts the fraiging manager without simulation info.]
Description []
@@ -388,6 +579,29 @@ Ivy_FraigMan_t * Ivy_FraigStart( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParam
SeeAlso []
***********************************************************************/
+void Ivy_FraigStop( Ivy_FraigMan_t * p )
+{
+ if ( p->pParams->fVerbose )
+ Ivy_FraigPrint( p );
+ if ( p->vPiVars ) Vec_PtrFree( p->vPiVars );
+ if ( p->pSat ) sat_solver_delete( p->pSat );
+ FREE( p->pPatScores );
+ FREE( p->pPatWords );
+ FREE( p->pSimWords );
+ free( p );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Prints stats for the fraiging manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
void Ivy_FraigPrint( Ivy_FraigMan_t * p )
{
double nMemory;
@@ -408,12 +622,14 @@ void Ivy_FraigPrint( Ivy_FraigMan_t * p )
PRT( " Fail ", p->timeSatFail );
PRT( "Class refining ", p->timeRef );
PRT( "TOTAL RUNTIME ", p->timeTotal );
- PRT( "time1 ", p->time1 );
+ if ( p->time1 ) { PRT( "time1 ", p->time1 ); }
}
+
+
/**Function*************************************************************
- Synopsis [Stops the fraiging manager.]
+ Synopsis [Assigns random patterns to the PI node.]
Description []
@@ -422,22 +638,19 @@ void Ivy_FraigPrint( Ivy_FraigMan_t * p )
SeeAlso []
***********************************************************************/
-void Ivy_FraigStop( Ivy_FraigMan_t * p )
+void Ivy_NodeAssignRandom( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj )
{
- if ( p->pParams->fVerbose )
- Ivy_FraigPrint( p );
- if ( p->vPiVars ) Vec_PtrFree( p->vPiVars );
- if ( p->pSat ) sat_solver_delete( p->pSat );
- FREE( p->pPatScores );
- FREE( p->pPatWords );
- FREE( p->pSimWords );
- free( p );
+ Ivy_FraigSim_t * pSims;
+ int i;
+ assert( Ivy_ObjIsPi(pObj) );
+ pSims = Ivy_ObjSim(pObj);
+ for ( i = 0; i < p->nSimWords; i++ )
+ pSims->pData[i] = Ivy_ObjRandomSim();
}
-
/**Function*************************************************************
- Synopsis [Simulates one node.]
+ Synopsis [Assigns constant patterns to the PI node.]
Description []
@@ -446,18 +659,19 @@ void Ivy_FraigStop( Ivy_FraigMan_t * p )
SeeAlso []
***********************************************************************/
-void Ivy_NodeAssignRandom( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj )
+void Ivy_NodeAssignConst( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj, int fConst1 )
{
Ivy_FraigSim_t * pSims;
int i;
+ assert( Ivy_ObjIsPi(pObj) );
pSims = Ivy_ObjSim(pObj);
for ( i = 0; i < p->nSimWords; i++ )
- pSims->pData[i] = Ivy_ObjRandomSim();
+ pSims->pData[i] = fConst1? ~(unsigned)0 : 0;
}
/**Function*************************************************************
- Synopsis [Simulates one node.]
+ Synopsis [Assings random simulation info for the PIs.]
Description []
@@ -466,13 +680,34 @@ void Ivy_NodeAssignRandom( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj )
SeeAlso []
***********************************************************************/
-void Ivy_NodeAssignConst( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj, int fConst1 )
+void Ivy_FraigAssignRandom( Ivy_FraigMan_t * p )
{
- Ivy_FraigSim_t * pSims;
+ Ivy_Obj_t * pObj;
int i;
- pSims = Ivy_ObjSim(pObj);
- for ( i = 0; i < p->nSimWords; i++ )
- pSims->pData[i] = fConst1? ~(unsigned)0 : 0;
+ Ivy_ManForEachPi( p->pManAig, pObj, i )
+ Ivy_NodeAssignRandom( p, pObj );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Assings distance-1 simulation info for the PIs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_FraigAssignDist1( Ivy_FraigMan_t * p, unsigned * pPat )
+{
+ Ivy_Obj_t * pObj;
+ int i, Limit;
+ Ivy_ManForEachPi( p->pManAig, pObj, i )
+ Ivy_NodeAssignConst( p, pObj, Ivy_InfoHasBit(pPat, i) );
+ Limit = IVY_MIN( Ivy_ManPiNum(p->pManAig), p->nSimWords * 32 - 1 );
+ for ( i = 0; i < Limit; i++ )
+ Ivy_InfoXorBit( Ivy_ObjSim( Ivy_ManPi(p->pManAig,i) )->pData, i+1 );
}
/**Function*************************************************************
@@ -733,52 +968,7 @@ p->nSimRounds++;
/**Function*************************************************************
- Synopsis [Simulates AIG manager.]
-
- Description [Assumes that the PI simulation info is attached.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Ivy_FraigAssignRandom( Ivy_FraigMan_t * p )
-{
- Ivy_Obj_t * pObj;
- int i;
- Ivy_ManForEachPi( p->pManAig, pObj, i )
- Ivy_NodeAssignRandom( p, pObj );
-}
-
-/**Function*************************************************************
-
- Synopsis [Simulates AIG manager.]
-
- Description [Assumes that the PI simulation info is attached.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Ivy_FraigAssignDist1( Ivy_FraigMan_t * p, unsigned * pPat )
-{
- Ivy_Obj_t * pObj;
- int i, Limit;
- Ivy_ManForEachPi( p->pManAig, pObj, i )
- Ivy_NodeAssignConst( p, pObj, Ivy_InfoHasBit(pPat, i) );
- Limit = IVY_MIN( Ivy_ManPiNum(p->pManAig), p->nSimWords * 32 - 1 );
- for ( i = 0; i < Limit; i++ )
- Ivy_InfoXorBit( Ivy_ObjSim( Ivy_ManPi(p->pManAig,i) )->pData, i+1 );
-/*
- 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.]
+ Synopsis [Adds one node to the equivalence class.]
Description []
@@ -800,7 +990,7 @@ void Ivy_NodeAddToClass( Ivy_Obj_t * pClass, Ivy_Obj_t * pObj )
/**Function*************************************************************
- Synopsis [Adds new nodes to the equivalence class.]
+ Synopsis [Adds equivalence class to the list of classes.]
Description []
@@ -853,7 +1043,7 @@ void Ivy_FraigInsertClass( Ivy_FraigList_t * pList, Ivy_Obj_t * pBase, Ivy_Obj_t
/**Function*************************************************************
- Synopsis [Updates the list of classes after base class has split.]
+ Synopsis [Removes equivalence class from the list of classes.]
Description []
@@ -1045,7 +1235,7 @@ int Ivy_FraigRefineClass_rec( Ivy_FraigMan_t * p, Ivy_Obj_t * pClass )
Description [Assumes that simulation info is assigned. Returns the
number of classes refined.]
- SideEffects []
+ SideEffects [Large equivalence class of constant 0 may cause problems.]
SeeAlso []
@@ -1063,8 +1253,8 @@ clk = clock();
Counter += ( RetValue > 0 );
//if ( Ivy_ObjIsConst1(pClass) )
//printf( "%d ", RetValue );
-if ( Ivy_ObjIsConst1(pClass) )
- p->time1 += clock() - clk;
+//if ( Ivy_ObjIsConst1(pClass) )
+// p->time1 += clock() - clk;
}
p->timeRef += clock() - clk;
return Counter;
@@ -1112,7 +1302,7 @@ int Ivy_FraigCountClassNodes( Ivy_Obj_t * pClass )
/**Function*************************************************************
- Synopsis [Stops the fraiging manager.]
+ Synopsis [Prints simulation classes.]
Description []
@@ -1134,7 +1324,7 @@ void Ivy_FraigPrintSimClasses( Ivy_FraigMan_t * p )
/**Function*************************************************************
- Synopsis [Copy pattern from the solver into the internal storage.]
+ Synopsis [Generated const 0 pattern.]
Description []
@@ -1150,7 +1340,7 @@ void Ivy_FraigSavePattern0( Ivy_FraigMan_t * p )
/**Function*************************************************************
- Synopsis [Copy pattern from the solver into the internal storage.]
+ Synopsis [[Generated const 1 pattern.]
Description []
@@ -1166,6 +1356,28 @@ void Ivy_FraigSavePattern1( Ivy_FraigMan_t * p )
/**Function*************************************************************
+ Synopsis [Generates the counter-example satisfying the miter.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int * Ivy_FraigCreateModel( Ivy_FraigMan_t * p )
+{
+ int * pModel;
+ Ivy_Obj_t * pObj;
+ int i;
+ pModel = ALLOC( int, Ivy_ManPiNum(p->pManFraig) );
+ Ivy_ManForEachPi( p->pManFraig, pObj, i )
+ pModel[i] = ( p->pSat->model.ptr[Ivy_ObjSatNum(pObj)] == l_True );
+ return pModel;
+}
+
+/**Function*************************************************************
+
Synopsis [Copy pattern from the solver into the internal storage.]
Description []
@@ -1256,7 +1468,7 @@ int Ivy_FraigCheckOutputSims( Ivy_FraigMan_t * p )
/**Function*************************************************************
- Synopsis [Stops the fraiging manager.]
+ Synopsis [Performs simulation of the manager.]
Description []
@@ -1291,11 +1503,12 @@ void Ivy_FraigSimulate( Ivy_FraigMan_t * p )
nClasses = p->lClasses.nItems;
nChanges = Ivy_FraigRefineClasses( p );
//printf( "Refined classes = %5d. Changes = %4d. Pairs = %6d.\n", p->lClasses.nItems, nChanges, Ivy_FraigCountPairsClasses(p) );
- } while ( (double)nChanges / nClasses > p->pParams->SimSatur );
+ } while ( (double)nChanges / nClasses > p->pParams->dSimSatur );
// Ivy_FraigPrintSimClasses( p );
+
// check if some outputs already became non-constant
- if ( Ivy_FraigCheckOutputSims(p) )
- printf( "Special case: One of the POs is already non-const zero.\n" );
+// if ( Ivy_FraigCheckOutputSims(p) )
+// printf( "Special case: One of the POs is already non-const zero.\n" );
}
@@ -1390,7 +1603,7 @@ int Ivy_FraigSelectBestPat( Ivy_FraigMan_t * p )
/**Function*************************************************************
- Synopsis [Stops the fraiging manager.]
+ Synopsis [Resimulates fraiging manager after finding a counter-example.]
Description []
@@ -1431,6 +1644,25 @@ void Ivy_FraigResimulate( Ivy_FraigMan_t * p )
/**Function*************************************************************
+ Synopsis [Prints the status of the miter.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_FraigMiterPrint( Ivy_Man_t * pNtk, char * pString, int clk, int fVerbose )
+{
+ if ( !fVerbose )
+ return;
+ printf( "Nodes = %7d. Levels = %4d. ", Ivy_ManNodeNum(pNtk), Ivy_ManLevels(pNtk) );
+ PRT( pString, clock() - clk );
+}
+
+/**Function*************************************************************
+
Synopsis [Reports the status of the miter.]
Description []
@@ -1440,21 +1672,23 @@ void Ivy_FraigResimulate( Ivy_FraigMan_t * p )
SeeAlso []
***********************************************************************/
-int Ivy_FraigMiterStatus( Ivy_FraigMan_t * p )
+int Ivy_FraigMiterStatus( Ivy_Man_t * pMan )
{
Ivy_Obj_t * pObj, * pObjNew;
int i, CountConst0 = 0, CountNonConst0 = 0, CountUndecided = 0;
- Ivy_ManForEachPo( p->pManAig, pObj, i )
+ if ( pMan->pData )
+ return 0;
+ Ivy_ManForEachPo( pMan, pObj, i )
{
- pObjNew = Ivy_ObjChild0Equiv(pObj);
+ pObjNew = Ivy_ObjChild0(pObj);
// check if the output is constant 1
- if ( pObjNew == p->pManFraig->pConst1 )
+ if ( pObjNew == pMan->pConst1 )
{
CountNonConst0++;
continue;
}
// check if the output is constant 0
- if ( pObjNew == Ivy_Not(p->pManFraig->pConst1) )
+ if ( pObjNew == Ivy_Not(pMan->pConst1) )
{
CountConst0++;
continue;
@@ -1467,6 +1701,7 @@ int Ivy_FraigMiterStatus( Ivy_FraigMan_t * p )
}
CountUndecided++;
}
+/*
if ( p->pParams->fVerbose )
{
printf( "Miter has %d outputs. ", Ivy_ManPoNum(p->pManAig) );
@@ -1475,14 +1710,19 @@ int Ivy_FraigMiterStatus( Ivy_FraigMan_t * p )
printf( "Undecided = %d. ", CountUndecided );
printf( "\n" );
}
+*/
+ if ( CountNonConst0 )
+ return 0;
+ if ( CountUndecided )
+ return -1;
return 1;
}
/**Function*************************************************************
- Synopsis [Works on the miter.]
+ Synopsis [Tries to prove each output of the miter until encountering a sat output.]
- Description [Tries to prove each output until encountering a sat output.]
+ Description []
SideEffects []
@@ -1493,7 +1733,7 @@ void Ivy_FraigMiterProve( Ivy_FraigMan_t * p )
{
Ivy_Obj_t * pObj, * pObjNew;
int i, RetValue, clk = clock();
- int fVerbose = p->pParams->fVerbose;
+ int fVerbose = 0;
Ivy_ManForEachPo( p->pManAig, pObj, i )
{
if ( i && fVerbose )
@@ -1520,6 +1760,9 @@ void Ivy_FraigMiterProve( Ivy_FraigMan_t * p )
{
if ( fVerbose )
printf( "Output %2d (out of %2d) cannot be constant 0. ", i, Ivy_ManPoNum(p->pManAig) );
+ // assing constant 0 model
+ p->pManFraig->pData = ALLOC( int, Ivy_ManPiNum(p->pManFraig) );
+ memset( p->pManFraig->pData, 0, sizeof(int) * Ivy_ManPiNum(p->pManFraig) );
break;
}
// try to prove the output constant 0
@@ -1529,7 +1772,7 @@ void Ivy_FraigMiterProve( Ivy_FraigMan_t * p )
if ( fVerbose )
printf( "Output %2d (out of %2d) was proved constant 0. ", i, Ivy_ManPoNum(p->pManAig) );
// set the constant miter
- Ivy_ObjFanin0(pObj)->pEquiv = Ivy_NotCond( p->pManFraig->pConst1, !Ivy_IsComplement(pObj) );
+ Ivy_ObjFanin0(pObj)->pEquiv = Ivy_NotCond( p->pManFraig->pConst1, !Ivy_ObjFaninC0(pObj) );
continue;
}
if ( RetValue == -1 ) // failed
@@ -1541,6 +1784,8 @@ void Ivy_FraigMiterProve( Ivy_FraigMan_t * p )
// proved satisfiable
if ( fVerbose )
printf( "Output %2d (out of %2d) was proved NOT a constant 0. ", i, Ivy_ManPoNum(p->pManAig) );
+ // create the model
+ p->pManFraig->pData = Ivy_FraigCreateModel(p);
break;
}
if ( fVerbose )
@@ -1564,7 +1809,7 @@ void Ivy_FraigSweep( Ivy_FraigMan_t * p )
{
Ivy_Obj_t * pObj;
int i, k = 0;
-p->nClassesZero = Ivy_ObjIsConst1(p->lClasses.pHead) ? Ivy_FraigCountClassNodes(p->lClasses.pHead) : 0;
+p->nClassesZero = p->lClasses.pHead? (Ivy_ObjIsConst1(p->lClasses.pHead) ? Ivy_FraigCountClassNodes(p->lClasses.pHead) : 0) : 0;
p->nClassesBeg = p->lClasses.nItems;
// duplicate internal nodes
p->pProgress = Extra_ProgressBarStart( stdout, Ivy_ManNodeNum(p->pManAig) );
@@ -1577,8 +1822,9 @@ p->nClassesBeg = p->lClasses.nItems;
p->nClassesEnd = p->lClasses.nItems;
// try to prove the outputs of the miter
p->nNodesMiter = Ivy_ManNodeNum(p->pManFraig);
- Ivy_FraigMiterStatus( p );
- Ivy_FraigMiterProve( p );
+// Ivy_FraigMiterStatus( p->pManFraig );
+ if ( p->pParams->fProve )
+ Ivy_FraigMiterProve( p );
// add the POs
Ivy_ManForEachPo( p->pManAig, pObj, i )
Ivy_ObjCreatePo( p->pManFraig, Ivy_ObjChild0Equiv(pObj) );
@@ -1651,32 +1897,9 @@ Ivy_Obj_t * Ivy_FraigAnd( Ivy_FraigMan_t * p, Ivy_Obj_t * pObjOld )
/**Function*************************************************************
- Synopsis [Performs fraiging for one node.]
+ Synopsis [Prints variable activity.]
- Description [Returns the fraiged node.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Ivy_FraigCleanActivity( Ivy_FraigMan_t * p )
-{
- double * pActivity;
- int i;
- pActivity = sat_solver_activity(p->pSat);
- for ( i = 0; i < p->nSatVars; i++ )
- {
- pActivity[i] = 0.0;
- sat_solver_order_update( p->pSat, i );
- }
-}
-
-/**Function*************************************************************
-
- Synopsis [Performs fraiging for one node.]
-
- Description [Returns the fraiged node.]
+ Description []
SideEffects []
@@ -1685,19 +1908,17 @@ void Ivy_FraigCleanActivity( Ivy_FraigMan_t * p )
***********************************************************************/
void Ivy_FraigPrintActivity( Ivy_FraigMan_t * p )
{
- double * pActivity;
int i;
- pActivity = sat_solver_activity(p->pSat);
for ( i = 0; i < p->nSatVars; i++ )
- printf( "%d %.3f ", i, pActivity[i] );
+ printf( "%d %.3f ", i, p->pSat->activity[i] );
printf( "\n" );
}
/**Function*************************************************************
- Synopsis [Performs fraiging for one node.]
+ Synopsis [Runs equivalence test for the two nodes.]
- Description [Returns the fraiged node.]
+ Description []
SideEffects []
@@ -1721,11 +1942,10 @@ int Ivy_FraigNodesAreEquiv( Ivy_FraigMan_t * p, Ivy_Obj_t * pOld, Ivy_Obj_t * pN
{
p->nSatFails++;
// fail immediately
- return -1;
-
+// return -1;
if ( nBTLimit <= 10 )
return -1;
- nBTLimit = (int)sqrt(nBTLimit);
+ nBTLimit = (int)pow(nBTLimit, 0.7);
}
p->nSatCalls++;
@@ -1740,6 +1960,9 @@ int Ivy_FraigNodesAreEquiv( Ivy_FraigMan_t * p, Ivy_Obj_t * pOld, Ivy_Obj_t * pN
// if the nodes do not have SAT variables, allocate them
Ivy_FraigNodeAddToSolver( p, pOld, pNew );
+ // prepare variable activity
+ Ivy_FraigSetActivityFactors( p, pOld, pNew );
+
// solve under assumptions
// A = 1; B = 0 OR A = 1; B = 1
clk = clock();
@@ -1827,7 +2050,7 @@ p->timeSatFail += clock() - clk;
/**Function*************************************************************
- Synopsis [Performs fraiging for one node.]
+ Synopsis [Runs equivalence test for one node.]
Description [Returns the fraiged node.]
@@ -1857,7 +2080,7 @@ int Ivy_FraigNodeIsConst( Ivy_FraigMan_t * p, Ivy_Obj_t * pNew )
Ivy_FraigNodeAddToSolver( p, NULL, pNew );
// prepare variable activity
- Ivy_FraigMarkConeSetActivity( p, NULL, pNew );
+ Ivy_FraigSetActivityFactors( p, NULL, pNew );
// solve under assumptions
clk = clock();
@@ -1878,7 +2101,8 @@ p->timeSatUnsat += clock() - clk;
else if ( RetValue1 == l_True )
{
p->timeSatSat += clock() - clk;
- Ivy_FraigSavePattern( p );
+ if ( p->pPatWords )
+ Ivy_FraigSavePattern( p );
p->nSatCallsSat++;
return 0;
}
@@ -2065,7 +2289,7 @@ Vec_Ptr_t * Ivy_FraigCollectSuper( Ivy_Obj_t * pObj, int fUseMuxes )
/**Function*************************************************************
- Synopsis [Collects the supergate.]
+ Synopsis [Updates the solver clause database.]
Description []
@@ -2091,7 +2315,7 @@ void Ivy_FraigObjAddToFrontier( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj, Vec_Ptr_t
/**Function*************************************************************
- Synopsis [Addes clauses to the solver.]
+ Synopsis [Updates the solver clause database.]
Description []
@@ -2145,90 +2369,70 @@ void Ivy_FraigNodeAddToSolver( Ivy_FraigMan_t * p, Ivy_Obj_t * pOld, Ivy_Obj_t *
/**Function*************************************************************
- Synopsis [Performs fraiging for one node.]
+ Synopsis [Sets variable activities in the cone.]
- Description [Returns the fraiged node.]
+ Description []
SideEffects []
SeeAlso []
***********************************************************************/
-int Ivy_FraigMarkConeSetActivity_rec( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj, double * pActivity, int LevelMax, Vec_Ptr_t * vPiVars )
+int Ivy_FraigSetActivityFactors_rec( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj, int LevelMin, int LevelMax )
{
Vec_Ptr_t * vFanins;
Ivy_Obj_t * pFanin;
- int i, Counter;
+ int i, Counter = 0;
assert( !Ivy_IsComplement(pObj) );
- if ( Ivy_ObjIsConst1(pObj) )
- return 0;
assert( Ivy_ObjSatNum(pObj) );
+ // skip visited variables
if ( Ivy_ObjIsTravIdCurrent(p->pManFraig, pObj) )
return 0;
Ivy_ObjSetTravIdCurrent(p->pManFraig, pObj);
-
- // add this variable to the decision
- assert( Ivy_ObjSatNum(pObj) > 0 );
-// pActivity[Ivy_ObjSatNum(pObj)] = 3.0 * pow( 0.97, LevelMax - pObj->Level );
-// sat_solver_order_unassigned( p->pSat, Ivy_ObjSatNum(pObj) );
-
-// pActivity[Ivy_ObjSatNum(pObj)] += 3.0 * pObj->Level / LevelMax;
-// sat_solver_order_update( p->pSat, Ivy_ObjSatNum(pObj) );
-
- if ( LevelMax > 150 && (int)pObj->Level > LevelMax - 100 )
- sat_solver_act_var_bump_factor( p->pSat, Ivy_ObjSatNum(pObj), 1.0 + 10.0 * (pObj->Level - (LevelMax - 100)) / 100 );
-
// add the PI to the list
- if ( Ivy_ObjIsPi(pObj) )
- {
- Vec_PtrPush( vPiVars, pObj );
+ if ( pObj->Level <= (unsigned)LevelMin || Ivy_ObjIsPi(pObj) )
return 0;
- }
-
+ // set the factor of this variable
+ // (LevelMax-LevelMin) / (pObj->Level-LevelMin) = p->pParams->dActConeBumpMax / ThisBump
+ p->pSat->factors[Ivy_ObjSatNum(pObj)] = p->pParams->dActConeBumpMax * (pObj->Level - LevelMin)/(LevelMax - LevelMin);
+ veci_push(&p->pSat->act_vars, Ivy_ObjSatNum(pObj));
// explore the fanins
vFanins = Ivy_ObjFaninVec( pObj );
- Counter = 1;
Vec_PtrForEachEntry( vFanins, pFanin, i )
- Counter += Ivy_FraigMarkConeSetActivity_rec( p, Ivy_Regular(pFanin), pActivity, LevelMax, vPiVars );
- return Counter;
-
-// Counter = Ivy_FraigMarkConeSetActivity_rec( p, Ivy_ObjFanin0(pObj), pActivity, LevelMax, vPiVars );
-// Counter += Ivy_FraigMarkConeSetActivity_rec( p, Ivy_ObjFanin1(pObj), pActivity, LevelMax, vPiVars );
-// return Counter;
+ Counter += Ivy_FraigSetActivityFactors_rec( p, Ivy_Regular(pFanin), LevelMin, LevelMax );
+ return 1 + Counter;
}
/**Function*************************************************************
- Synopsis [Performs fraiging for one node.]
+ Synopsis [Sets variable activities in the cone.]
- Description [Returns the fraiged node.]
+ Description []
SideEffects []
SeeAlso []
***********************************************************************/
-int Ivy_FraigMarkConeSetActivity( Ivy_FraigMan_t * p, Ivy_Obj_t * pOld, Ivy_Obj_t * pNew )
+int Ivy_FraigSetActivityFactors( Ivy_FraigMan_t * p, Ivy_Obj_t * pOld, Ivy_Obj_t * pNew )
{
- int clk, LevelMax, Counter;
+ int clk, LevelMin, LevelMax;
assert( pOld || pNew );
clk = clock();
- Vec_PtrClear( p->vPiVars );
+ // reset the active variables
+ veci_resize(&p->pSat->act_vars, 0);
+ // prepare for traversal
Ivy_ManIncrementTravId( p->pManFraig );
-// Ivy_FraigCleanActivity( p );
-// sat_solver_order_clean( p->pSat );
-//printf( "\n" );
-//printf( "Adding\n" );
- LevelMax = IVY_MAX( pNew ? pNew->Level : 0, pOld ? pOld->Level : 0 );
- Counter = 0;
- if ( pOld )
- Counter += Ivy_FraigMarkConeSetActivity_rec( p, pOld, sat_solver_activity(p->pSat), LevelMax, p->vPiVars );
- if ( pNew )
- Counter += Ivy_FraigMarkConeSetActivity_rec( p, pNew, sat_solver_activity(p->pSat), LevelMax, p->vPiVars );
+ // determine the min and max level to visit
+ assert( p->pParams->dActConeRatio > 0 && p->pParams->dActConeRatio < 1 );
+ LevelMax = IVY_MAX( (pNew ? pNew->Level : 0), (pOld ? pOld->Level : 0) );
+ LevelMin = (int)(LevelMax * (1.0 - p->pParams->dActConeRatio));
+ // traverse
+ if ( pOld && !Ivy_ObjIsConst1(pOld) )
+ Ivy_FraigSetActivityFactors_rec( p, pOld, LevelMin, LevelMax );
+ if ( pNew && !Ivy_ObjIsConst1(pNew) )
+ Ivy_FraigSetActivityFactors_rec( p, pNew, LevelMin, LevelMax );
//Ivy_FraigPrintActivity( p );
-//printf( "\n" );
-//printf( "Solving\n" );
-// printf( "%d ", Vec_PtrSize(p->vPiVars) );
p->timeTrav += clock() - clk;
return 1;
}
diff --git a/src/temp/ivy/ivyMan.c b/src/temp/ivy/ivyMan.c
index c6ad75e8..e2689580 100644
--- a/src/temp/ivy/ivyMan.c
+++ b/src/temp/ivy/ivyMan.c
@@ -123,7 +123,10 @@ Ivy_Man_t * Ivy_ManDup( Ivy_Man_t * p )
pObj->pEquiv = Ivy_ObjCreatePi(pNew);
// duplicate internal nodes
Ivy_ManForEachNodeVec( p, vNodes, pObj, i )
- pObj->pEquiv = Ivy_And( pNew, Ivy_ObjChild0Equiv(pObj), Ivy_ObjChild1Equiv(pObj) );
+ if ( Ivy_ObjIsBuf(pObj) )
+ pObj->pEquiv = Ivy_ObjChild0Equiv(pObj);
+ else
+ pObj->pEquiv = Ivy_And( pNew, Ivy_ObjChild0Equiv(pObj), Ivy_ObjChild1Equiv(pObj) );
// add the POs
Ivy_ManForEachPo( p, pObj, i )
Ivy_ObjCreatePo( pNew, Ivy_ObjChild0Equiv(pObj) );
@@ -181,9 +184,9 @@ void Ivy_ManStop( Ivy_Man_t * p )
/**Function*************************************************************
- Synopsis [Returns the number of dangling nodes removed.]
+ Synopsis [Removes nodes without fanout.]
- Description []
+ Description [Returns the number of dangling nodes removed.]
SideEffects []
@@ -199,11 +202,97 @@ int Ivy_ManCleanup( Ivy_Man_t * p )
if ( Ivy_ObjIsNode(pNode) || Ivy_ObjIsLatch(pNode) || Ivy_ObjIsBuf(pNode) )
if ( Ivy_ObjRefs(pNode) == 0 )
Ivy_ObjDelete_rec( p, pNode, 1 );
+//printf( "Cleanup removed %d nodes.\n", nNodesOld - Ivy_ManNodeNum(p) );
return nNodesOld - Ivy_ManNodeNum(p);
}
/**Function*************************************************************
+ Synopsis [Marks nodes reachable from the given one.]
+
+ Description [Returns the number of dangling nodes removed.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_ManCleanupSeq_rec( Ivy_Obj_t * pObj )
+{
+ if ( Ivy_ObjIsMarkA(pObj) )
+ return;
+ Ivy_ObjSetMarkA(pObj);
+ if ( pObj->pFanin0 != NULL )
+ Ivy_ManCleanupSeq_rec( Ivy_ObjFanin0(pObj) );
+ if ( pObj->pFanin1 != NULL )
+ Ivy_ManCleanupSeq_rec( Ivy_ObjFanin1(pObj) );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Removes logic that does not feed into POs.]
+
+ Description [Returns the number of dangling nodes removed.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ivy_ManCleanupSeq( Ivy_Man_t * p )
+{
+ Vec_Ptr_t * vNodes;
+ Ivy_Obj_t * pObj;
+ int i, RetValue;
+ // mark the constant and PIs
+ Ivy_ObjSetMarkA( Ivy_ManConst1(p) );
+ Ivy_ManForEachPi( p, pObj, i )
+ Ivy_ObjSetMarkA( pObj );
+ // mark nodes visited from POs
+ Ivy_ManForEachPo( p, pObj, i )
+ Ivy_ManCleanupSeq_rec( pObj );
+ // collect unmarked nodes
+ vNodes = Vec_PtrAlloc( 100 );
+ Ivy_ManForEachObj( p, pObj, i )
+ {
+ if ( Ivy_ObjIsMarkA(pObj) )
+ Ivy_ObjClearMarkA(pObj);
+ else
+ Vec_PtrPush( vNodes, pObj );
+ }
+ if ( Vec_PtrSize(vNodes) == 0 )
+ {
+ Vec_PtrFree( vNodes );
+//printf( "Sequential sweep cleaned out %d nodes.\n", 0 );
+ return 0;
+ }
+ // disconnect the marked objects
+ Vec_PtrForEachEntry( vNodes, pObj, i )
+ Ivy_ObjDisconnect( p, pObj );
+ // remove the dangling objects
+ Vec_PtrForEachEntry( vNodes, pObj, i )
+ {
+ assert( Ivy_ObjIsNode(pObj) || Ivy_ObjIsLatch(pObj) || Ivy_ObjIsBuf(pObj) );
+ assert( Ivy_ObjRefs(pObj) == 0 );
+ // update node counters of the manager
+ p->nObjs[pObj->Type]--;
+ p->nDeleted++;
+ // delete buffer from the array of buffers
+ if ( p->fFanout && Ivy_ObjIsBuf(pObj) )
+ Vec_PtrRemove( p->vBufs, pObj );
+ // free the node
+ Vec_PtrWriteEntry( p->vObjs, pObj->Id, NULL );
+ Ivy_ManRecycleMemory( p, pObj );
+ }
+ // return the number of nodes freed
+ RetValue = Vec_PtrSize(vNodes);
+ Vec_PtrFree( vNodes );
+//printf( "Sequential sweep cleaned out %d nodes.\n", RetValue );
+ return RetValue;
+}
+
+/**Function*************************************************************
+
Synopsis [Returns the number of dangling nodes removed.]
Description []
@@ -216,13 +305,21 @@ int Ivy_ManCleanup( Ivy_Man_t * p )
int Ivy_ManPropagateBuffers( Ivy_Man_t * p, int fUpdateLevel )
{
Ivy_Obj_t * pNode;
+ int LimitFactor = 20;
int nSteps;
for ( nSteps = 0; Vec_PtrSize(p->vBufs) > 0; nSteps++ )
{
pNode = Vec_PtrEntryLast(p->vBufs);
while ( Ivy_ObjIsBuf(pNode) )
pNode = Ivy_ObjReadFirstFanout( p, pNode );
+//printf( "Propagating buffer %d with input %d and output %d\n", Ivy_ObjFaninId0(pNode), Ivy_ObjFaninId0(Ivy_ObjFanin0(pNode)), pNode->Id );
+//printf( "Latch num %d\n", Ivy_ManLatchNum(p) );
Ivy_NodeFixBufferFanins( p, pNode, fUpdateLevel );
+ if ( nSteps > Ivy_ManNodeNum(p) * LimitFactor )
+ {
+ printf( "This circuit cannot be forward retimed completely. Structural hashing is not finished after %d forward latch moves.\n", Ivy_ManNodeNum(p) * LimitFactor );
+ break;
+ }
}
// printf( "Number of steps = %d\n", nSteps );
return nSteps;
@@ -307,6 +404,7 @@ void Ivy_ManMakeSeq( Ivy_Man_t * p, int nLatches, int * pInits )
p->nDeleted -= 2 * nLatches;
// remove dangling nodes
Ivy_ManCleanup(p);
+ Ivy_ManCleanupSeq(p);
/*
// check for dangling nodes
Ivy_ManForEachObj( p, pObj, i )
diff --git a/src/temp/ivy/ivyResyn.c b/src/temp/ivy/ivyResyn.c
index b2e4a4dd..f42d7464 100644
--- a/src/temp/ivy/ivyResyn.c
+++ b/src/temp/ivy/ivyResyn.c
@@ -138,6 +138,56 @@ if ( fVerbose ) Ivy_ManPrintStats( pMan );
return pMan;
}
+/**Function*************************************************************
+
+ Synopsis [Performs several passes of rewriting on the AIG.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Ivy_Man_t * Ivy_ManRwsat( Ivy_Man_t * pMan, int fVerbose )
+{
+ int clk;
+ Ivy_Man_t * pTemp;
+
+if ( fVerbose ) { printf( "Original:\n" ); }
+if ( fVerbose ) Ivy_ManPrintStats( pMan );
+
+clk = clock();
+ Ivy_ManRewritePre( pMan, 0, 0, 0 );
+if ( fVerbose ) { printf( "\n" ); }
+if ( fVerbose ) { PRT( "Rewrite", clock() - clk ); }
+if ( fVerbose ) Ivy_ManPrintStats( pMan );
+
+clk = clock();
+ pMan = Ivy_ManBalance( pTemp = pMan, 0 );
+// pMan = Ivy_ManDup( pTemp = pMan );
+ Ivy_ManStop( pTemp );
+if ( fVerbose ) { printf( "\n" ); }
+if ( fVerbose ) { PRT( "Balance", clock() - clk ); }
+if ( fVerbose ) Ivy_ManPrintStats( pMan );
+
+/*
+clk = clock();
+ Ivy_ManRewritePre( pMan, 0, 0, 0 );
+if ( fVerbose ) { printf( "\n" ); }
+if ( fVerbose ) { PRT( "Rewrite", clock() - clk ); }
+if ( fVerbose ) Ivy_ManPrintStats( pMan );
+
+clk = clock();
+ pMan = Ivy_ManBalance( pTemp = pMan, 0 );
+ Ivy_ManStop( pTemp );
+if ( fVerbose ) { printf( "\n" ); }
+if ( fVerbose ) { PRT( "Balance", clock() - clk ); }
+if ( fVerbose ) Ivy_ManPrintStats( pMan );
+*/
+ return pMan;
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
diff --git a/src/temp/ivy/module.make b/src/temp/ivy/module.make
index 05409745..f5f34f27 100644
--- a/src/temp/ivy/module.make
+++ b/src/temp/ivy/module.make
@@ -2,10 +2,13 @@ SRC += src/temp/ivy/ivyBalance.c \
src/temp/ivy/ivyCanon.c \
src/temp/ivy/ivyCheck.c \
src/temp/ivy/ivyCut.c \
+ src/temp/ivy/ivyCutTrav.c \
src/temp/ivy/ivyDfs.c \
src/temp/ivy/ivyDsd.c \
src/temp/ivy/ivyFanout.c \
src/temp/ivy/ivyFastMap.c \
+ src/temp/ivy/ivyFraig.c \
+ src/temp/ivy/ivyHaig.c \
src/temp/ivy/ivyIsop.c \
src/temp/ivy/ivyMan.c \
src/temp/ivy/ivyMem.c \
@@ -15,5 +18,6 @@ SRC += src/temp/ivy/ivyBalance.c \
src/temp/ivy/ivyResyn.c \
src/temp/ivy/ivyRwr.c \
src/temp/ivy/ivySeq.c \
+ src/temp/ivy/ivyShow.c \
src/temp/ivy/ivyTable.c \
src/temp/ivy/ivyUtil.c
diff --git a/src/temp/ivy/satMem.c b/src/temp/ivy/satMem.c
deleted file mode 100644
index bb234f66..00000000
--- a/src/temp/ivy/satMem.c
+++ /dev/null
@@ -1,527 +0,0 @@
-/**CFile****************************************************************
-
- FileName [satMem.c]
-
- PackageName [SAT solver.]
-
- Synopsis [Memory management.]
-
- Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>]
-
- Affiliation [UC Berkeley]
-
- Date [Ver. 1.0. Started - January 1, 2004.]
-
- Revision [$Id: satMem.c,v 1.0 2004/01/01 1:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "satMem.h"
-#include "extra.h"
-
-////////////////////////////////////////////////////////////////////////
-/// DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-struct Sat_MmFixed_t_
-{
- // information about individual entries
- int nEntrySize; // the size of one entry
- int nEntriesAlloc; // the total number of entries allocated
- int nEntriesUsed; // the number of entries in use
- int nEntriesMax; // the max number of entries in use
- char * pEntriesFree; // the linked list of free entries
-
- // this is where the memory is stored
- int nChunkSize; // the size of one chunk
- int nChunksAlloc; // the maximum number of memory chunks
- int nChunks; // the current number of memory chunks
- char ** pChunks; // the allocated memory
-
- // statistics
- int nMemoryUsed; // memory used in the allocated entries
- int nMemoryAlloc; // memory allocated
-};
-
-struct Sat_MmFlex_t_
-{
- // information about individual entries
- int nEntriesUsed; // the number of entries allocated
- char * pCurrent; // the current pointer to free memory
- char * pEnd; // the first entry outside the free memory
-
- // this is where the memory is stored
- int nChunkSize; // the size of one chunk
- int nChunksAlloc; // the maximum number of memory chunks
- int nChunks; // the current number of memory chunks
- char ** pChunks; // the allocated memory
-
- // statistics
- int nMemoryUsed; // memory used in the allocated entries
- int nMemoryAlloc; // memory allocated
-};
-
-struct Sat_MmStep_t_
-{
- int nMems; // the number of fixed memory managers employed
- Sat_MmFixed_t ** pMems; // memory managers: 2^1 words, 2^2 words, etc
- int nMapSize; // the size of the memory array
- Sat_MmFixed_t ** pMap; // maps the number of bytes into its memory manager
-};
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
- Synopsis [Allocates memory pieces of fixed size.]
-
- Description [The size of the chunk is computed as the minimum of
- 1024 entries and 64K. Can only work with entry size at least 4 byte long.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Sat_MmFixed_t * Sat_MmFixedStart( int nEntrySize )
-{
- Sat_MmFixed_t * p;
-
- p = ALLOC( Sat_MmFixed_t, 1 );
- memset( p, 0, sizeof(Sat_MmFixed_t) );
-
- p->nEntrySize = nEntrySize;
- p->nEntriesAlloc = 0;
- p->nEntriesUsed = 0;
- p->pEntriesFree = NULL;
-
- if ( nEntrySize * (1 << 10) < (1<<16) )
- p->nChunkSize = (1 << 10);
- else
- p->nChunkSize = (1<<16) / nEntrySize;
- if ( p->nChunkSize < 8 )
- p->nChunkSize = 8;
-
- p->nChunksAlloc = 64;
- p->nChunks = 0;
- p->pChunks = ALLOC( char *, p->nChunksAlloc );
-
- p->nMemoryUsed = 0;
- p->nMemoryAlloc = 0;
- return p;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Sat_MmFixedStop( Sat_MmFixed_t * p, int fVerbose )
-{
- int i;
- if ( p == NULL )
- return;
- if ( fVerbose )
- {
- printf( "Fixed memory manager: Entry = %5d. Chunk = %5d. Chunks used = %5d.\n",
- p->nEntrySize, p->nChunkSize, p->nChunks );
- printf( " Entries used = %8d. Entries peak = %8d. Memory used = %8d. Memory alloc = %8d.\n",
- p->nEntriesUsed, p->nEntriesMax, p->nEntrySize * p->nEntriesUsed, p->nMemoryAlloc );
- }
- for ( i = 0; i < p->nChunks; i++ )
- free( p->pChunks[i] );
- free( p->pChunks );
- free( p );
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-char * Sat_MmFixedEntryFetch( Sat_MmFixed_t * p )
-{
- char * pTemp;
- int i;
-
- // check if there are still free entries
- if ( p->nEntriesUsed == p->nEntriesAlloc )
- { // need to allocate more entries
- assert( p->pEntriesFree == NULL );
- if ( p->nChunks == p->nChunksAlloc )
- {
- p->nChunksAlloc *= 2;
- p->pChunks = REALLOC( char *, p->pChunks, p->nChunksAlloc );
- }
- p->pEntriesFree = ALLOC( char, p->nEntrySize * p->nChunkSize );
- p->nMemoryAlloc += p->nEntrySize * p->nChunkSize;
- // transform these entries into a linked list
- pTemp = p->pEntriesFree;
- for ( i = 1; i < p->nChunkSize; i++ )
- {
- *((char **)pTemp) = pTemp + p->nEntrySize;
- pTemp += p->nEntrySize;
- }
- // set the last link
- *((char **)pTemp) = NULL;
- // add the chunk to the chunk storage
- p->pChunks[ p->nChunks++ ] = p->pEntriesFree;
- // add to the number of entries allocated
- p->nEntriesAlloc += p->nChunkSize;
- }
- // incrememt the counter of used entries
- p->nEntriesUsed++;
- if ( p->nEntriesMax < p->nEntriesUsed )
- p->nEntriesMax = p->nEntriesUsed;
- // return the first entry in the free entry list
- pTemp = p->pEntriesFree;
- p->pEntriesFree = *((char **)pTemp);
- return pTemp;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Sat_MmFixedEntryRecycle( Sat_MmFixed_t * p, char * pEntry )
-{
- // decrement the counter of used entries
- p->nEntriesUsed--;
- // add the entry to the linked list of free entries
- *((char **)pEntry) = p->pEntriesFree;
- p->pEntriesFree = pEntry;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description [Relocates all the memory except the first chunk.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Sat_MmFixedRestart( Sat_MmFixed_t * p )
-{
- int i;
- char * pTemp;
-
- // deallocate all chunks except the first one
- for ( i = 1; i < p->nChunks; i++ )
- free( p->pChunks[i] );
- p->nChunks = 1;
- // transform these entries into a linked list
- pTemp = p->pChunks[0];
- for ( i = 1; i < p->nChunkSize; i++ )
- {
- *((char **)pTemp) = pTemp + p->nEntrySize;
- pTemp += p->nEntrySize;
- }
- // set the last link
- *((char **)pTemp) = NULL;
- // set the free entry list
- p->pEntriesFree = p->pChunks[0];
- // set the correct statistics
- p->nMemoryAlloc = p->nEntrySize * p->nChunkSize;
- p->nMemoryUsed = 0;
- p->nEntriesAlloc = p->nChunkSize;
- p->nEntriesUsed = 0;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Sat_MmFixedReadMemUsage( Sat_MmFixed_t * p )
-{
- return p->nMemoryAlloc;
-}
-
-
-
-/**Function*************************************************************
-
- Synopsis [Allocates entries of flexible size.]
-
- Description [Can only work with entry size at least 4 byte long.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Sat_MmFlex_t * Sat_MmFlexStart()
-{
- Sat_MmFlex_t * p;
-
- p = ALLOC( Sat_MmFlex_t, 1 );
- memset( p, 0, sizeof(Sat_MmFlex_t) );
-
- p->nEntriesUsed = 0;
- p->pCurrent = NULL;
- p->pEnd = NULL;
-
- p->nChunkSize = (1 << 12);
- p->nChunksAlloc = 64;
- p->nChunks = 0;
- p->pChunks = ALLOC( char *, p->nChunksAlloc );
-
- p->nMemoryUsed = 0;
- p->nMemoryAlloc = 0;
- return p;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Sat_MmFlexStop( Sat_MmFlex_t * p, int fVerbose )
-{
- int i;
- if ( p == NULL )
- return;
- if ( fVerbose )
- {
- printf( "Flexible memory manager: Chunk size = %d. Chunks used = %d.\n",
- p->nChunkSize, p->nChunks );
- printf( " Entries used = %d. Memory used = %d. Memory alloc = %d.\n",
- p->nEntriesUsed, p->nMemoryUsed, p->nMemoryAlloc );
- }
- for ( i = 0; i < p->nChunks; i++ )
- free( p->pChunks[i] );
- free( p->pChunks );
- free( p );
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-char * Sat_MmFlexEntryFetch( Sat_MmFlex_t * p, int nBytes )
-{
- char * pTemp;
- // check if there are still free entries
- if ( p->pCurrent == NULL || p->pCurrent + nBytes > p->pEnd )
- { // need to allocate more entries
- if ( p->nChunks == p->nChunksAlloc )
- {
- p->nChunksAlloc *= 2;
- p->pChunks = REALLOC( char *, p->pChunks, p->nChunksAlloc );
- }
- if ( nBytes > p->nChunkSize )
- {
- // resize the chunk size if more memory is requested than it can give
- // (ideally, this should never happen)
- p->nChunkSize = 2 * nBytes;
- }
- p->pCurrent = ALLOC( char, p->nChunkSize );
- p->pEnd = p->pCurrent + p->nChunkSize;
- p->nMemoryAlloc += p->nChunkSize;
- // add the chunk to the chunk storage
- p->pChunks[ p->nChunks++ ] = p->pCurrent;
- }
- assert( p->pCurrent + nBytes <= p->pEnd );
- // increment the counter of used entries
- p->nEntriesUsed++;
- // keep track of the memory used
- p->nMemoryUsed += nBytes;
- // return the next entry
- pTemp = p->pCurrent;
- p->pCurrent += nBytes;
- return pTemp;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Sat_MmFlexReadMemUsage( Sat_MmFlex_t * p )
-{
- return p->nMemoryAlloc;
-}
-
-
-
-
-
-/**Function*************************************************************
-
- Synopsis [Starts the hierarchical memory manager.]
-
- Description [This manager can allocate entries of any size.
- Iternally they are mapped into the entries with the number of bytes
- equal to the power of 2. The smallest entry size is 8 bytes. The
- next one is 16 bytes etc. So, if the user requests 6 bytes, he gets
- 8 byte entry. If we asks for 25 bytes, he gets 32 byte entry etc.
- The input parameters "nSteps" says how many fixed memory managers
- are employed internally. Calling this procedure with nSteps equal
- to 10 results in 10 hierarchically arranged internal memory managers,
- which can allocate up to 4096 (1Kb) entries. Requests for larger
- entries are handed over to malloc() and then free()ed.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Sat_MmStep_t * Sat_MmStepStart( int nSteps )
-{
- Sat_MmStep_t * p;
- int i, k;
- p = ALLOC( Sat_MmStep_t, 1 );
- p->nMems = nSteps;
- // start the fixed memory managers
- p->pMems = ALLOC( Sat_MmFixed_t *, p->nMems );
- for ( i = 0; i < p->nMems; i++ )
- p->pMems[i] = Sat_MmFixedStart( (8<<i) );
- // set up the mapping of the required memory size into the corresponding manager
- p->nMapSize = (4<<p->nMems);
- p->pMap = ALLOC( Sat_MmFixed_t *, p->nMapSize+1 );
- p->pMap[0] = NULL;
- for ( k = 1; k <= 4; k++ )
- p->pMap[k] = p->pMems[0];
- for ( i = 0; i < p->nMems; i++ )
- for ( k = (4<<i)+1; k <= (8<<i); k++ )
- p->pMap[k] = p->pMems[i];
-//for ( i = 1; i < 100; i ++ )
-//printf( "%10d: size = %10d\n", i, p->pMap[i]->nEntrySize );
- return p;
-}
-
-/**Function*************************************************************
-
- Synopsis [Stops the memory manager.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Sat_MmStepStop( Sat_MmStep_t * p, int fVerbose )
-{
- int i;
- for ( i = 0; i < p->nMems; i++ )
- Sat_MmFixedStop( p->pMems[i], fVerbose );
- free( p->pMems );
- free( p->pMap );
- free( p );
-}
-
-/**Function*************************************************************
-
- Synopsis [Creates the entry.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-char * Sat_MmStepEntryFetch( Sat_MmStep_t * p, int nBytes )
-{
- if ( nBytes == 0 )
- return NULL;
- if ( nBytes > p->nMapSize )
- {
-// printf( "Allocating %d bytes.\n", nBytes );
- return ALLOC( char, nBytes );
- }
- return Sat_MmFixedEntryFetch( p->pMap[nBytes] );
-}
-
-
-/**Function*************************************************************
-
- Synopsis [Recycles the entry.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Sat_MmStepEntryRecycle( Sat_MmStep_t * p, char * pEntry, int nBytes )
-{
- if ( nBytes == 0 )
- return;
- if ( nBytes > p->nMapSize )
- {
- free( pEntry );
- return;
- }
- Sat_MmFixedEntryRecycle( p->pMap[nBytes], pEntry );
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Sat_MmStepReadMemUsage( Sat_MmStep_t * p )
-{
- int i, nMemTotal = 0;
- for ( i = 0; i < p->nMems; i++ )
- nMemTotal += p->pMems[i]->nMemoryAlloc;
- return nMemTotal;
-}
diff --git a/src/temp/ivy/satMem.h b/src/temp/ivy/satMem.h
deleted file mode 100644
index 5c5ddd9c..00000000
--- a/src/temp/ivy/satMem.h
+++ /dev/null
@@ -1,78 +0,0 @@
-/**CFile****************************************************************
-
- FileName [satMem.h]
-
- PackageName [SAT solver.]
-
- Synopsis [Memory management.]
-
- Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>]
-
- Affiliation [UC Berkeley]
-
- Date [Ver. 1.0. Started - January 1, 2004.]
-
- Revision [$Id: satMem.h,v 1.0 2004/01/01 1:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#ifndef __SAT_MEM_H__
-#define __SAT_MEM_H__
-
-////////////////////////////////////////////////////////////////////////
-/// INCLUDES ///
-////////////////////////////////////////////////////////////////////////
-
-//#include "leaks.h"
-#include <stdio.h>
-#include <stdlib.h>
-
-////////////////////////////////////////////////////////////////////////
-/// PARAMETERS ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-/// STRUCTURE DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-typedef struct Sat_MmFixed_t_ Sat_MmFixed_t;
-typedef struct Sat_MmFlex_t_ Sat_MmFlex_t;
-typedef struct Sat_MmStep_t_ Sat_MmStep_t;
-
-////////////////////////////////////////////////////////////////////////
-/// GLOBAL VARIABLES ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-/// MACRO DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-// fixed-size-block memory manager
-extern Sat_MmFixed_t * Sat_MmFixedStart( int nEntrySize );
-extern void Sat_MmFixedStop( Sat_MmFixed_t * p, int fVerbose );
-extern char * Sat_MmFixedEntryFetch( Sat_MmFixed_t * p );
-extern void Sat_MmFixedEntryRecycle( Sat_MmFixed_t * p, char * pEntry );
-extern void Sat_MmFixedRestart( Sat_MmFixed_t * p );
-extern int Sat_MmFixedReadMemUsage( Sat_MmFixed_t * p );
-// flexible-size-block memory manager
-extern Sat_MmFlex_t * Sat_MmFlexStart();
-extern void Sat_MmFlexStop( Sat_MmFlex_t * p, int fVerbose );
-extern char * Sat_MmFlexEntryFetch( Sat_MmFlex_t * p, int nBytes );
-extern int Sat_MmFlexReadMemUsage( Sat_MmFlex_t * p );
-// hierarchical memory manager
-extern Sat_MmStep_t * Sat_MmStepStart( int nSteps );
-extern void Sat_MmStepStop( Sat_MmStep_t * p, int fVerbose );
-extern char * Sat_MmStepEntryFetch( Sat_MmStep_t * p, int nBytes );
-extern void Sat_MmStepEntryRecycle( Sat_MmStep_t * p, char * pEntry, int nBytes );
-extern int Sat_MmStepReadMemUsage( Sat_MmStep_t * p );
-
-#endif
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
diff --git a/src/temp/ivy/satSolver.c b/src/temp/ivy/satSolver.c
deleted file mode 100644
index 38e73c7d..00000000
--- a/src/temp/ivy/satSolver.c
+++ /dev/null
@@ -1,1279 +0,0 @@
-/**************************************************************************************************
-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"
-
-//#define ASAT_USE_SYSTEM_MEMORY_MANAGEMENT
-
-//=================================================================================================
-// 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);
-//printf( "+%d ", 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;
- }
-
-//printf( "-%d ", next );
- if (values[next] == l_Undef)
- return next;
- }
-
- return var_Undef;
-}
-
-void sat_solver_order_clean(sat_solver* s) // removes all variables from the queue
-{
- while ( order_select(s, 0.0) != var_Undef );
-}
-
-void sat_solver_order_unassigned(sat_solver* s, int v) // undoorder
-{
- order_unassigned(s, v);
-}
-
-void sat_solver_order_update(sat_solver* s, int v) // updateorder
-{
- order_update(s, v);
-}
-
-//=================================================================================================
-// 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);
-
-}
-
-void sat_solver_act_var_bump_factor(sat_solver* s, int v, double factor) {
- double* activity = s->activity;
- if ((activity[v] += s->var_inc * factor) > 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; }
-
-double* sat_solver_activity(sat_solver* s) { return s->activity; }
-
-//=================================================================================================
-// 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));
-#ifdef ASAT_USE_SYSTEM_MEMORY_MANAGEMENT
- c = (clause*)malloc(sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float));
-#else
- c = (clause*)Sat_MmStepEntryFetch( s->pMem, sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float) );
-#endif
-
- 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);
- }
-
-#ifdef ASAT_USE_SYSTEM_MEMORY_MANAGEMENT
- free(c);
-#else
- Sat_MmStepEntryRecycle( s->pMem, (char *)c, sizeof(clause) + sizeof(lit) * clause_size(c) + clause_learnt(c) * sizeof(float) );
-#endif
-}
-
-
-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 ( s->nConfLimit && s->stats.conflicts > s->nConfLimit ||
- s->nInsLimit && s->stats.inspects > s->nInsLimit )
- {
- // 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;
-
-#ifdef ASAT_USE_SYSTEM_MEMORY_MANAGEMENT
- s->pMem = NULL;
-#else
- s->pMem = Sat_MmStepStart( 10 );
-#endif
- return s;
-}
-
-
-void sat_solver_delete(sat_solver* s)
-{
-
-#ifdef ASAT_USE_SYSTEM_MEMORY_MANAGEMENT
- 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]);
-#else
- Sat_MmStepStop( s->pMem, 0 );
-#endif
-
- // 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, sint64 nConfLimit, sint64 nInsLimit, sint64 nConfLimitGlobal, sint64 nInsLimitGlobal)
-{
- double nof_conflicts = 100;
- double nof_learnts = sat_solver_nclauses(s) / 3;
- lbool status = l_Undef;
- lbool* values = s->assigns;
- lit* i;
-
- // set the external limits
- s->nConfLimit = 0;
- s->nInsLimit = 0;
- if ( nConfLimit )
- s->nConfLimit = s->stats.conflicts + nConfLimit;
- if ( nInsLimit )
- s->nInsLimit = s->stats.inspects + nInsLimit;
- if ( nConfLimitGlobal && s->nConfLimit > nConfLimitGlobal )
- s->nConfLimit = nConfLimitGlobal;
- if ( nInsLimitGlobal && s->nInsLimit > nInsLimitGlobal )
- s->nInsLimit = nInsLimitGlobal;
-
- //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;
-
- // quit the loop if reached an external limit
- if ( s->nConfLimit && s->stats.conflicts > s->nConfLimit )
- {
-// printf( "Reached the limit on the number of conflicts (%d).\n", s->nConfLimit );
- break;
- }
- if ( s->nInsLimit && s->stats.inspects > s->nInsLimit )
- {
-// printf( "Reached the limit on the number of implications (%d).\n", s->nInsLimit );
- break;
- }
- }
- 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
deleted file mode 100644
index a7ace8ed..00000000
--- a/src/temp/ivy/satSolver.h
+++ /dev/null
@@ -1,154 +0,0 @@
-/**************************************************************************************************
-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"
-#include "satMem.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, sint64 nConfLimit, sint64 nInsLimit, sint64 nConfLimitGlobal, sint64 nInsLimitGlobal);
-
-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);
-
-extern void sat_solver_order_clean(sat_solver* s);
-extern void sat_solver_order_unassigned(sat_solver* s, int v);
-extern void sat_solver_order_update(sat_solver* s, int v);
-
-extern double* sat_solver_activity(sat_solver* s);
-extern void sat_solver_act_var_bump_factor(sat_solver* s, int v, double factor);
-
-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;
-
- sint64 nConfLimit; // external limit on the number of conflicts
- sint64 nInsLimit; // external limit on the number of implications
-
- Sat_MmStep_t * pMem;
-};
-
-#endif
diff --git a/src/temp/ivy/satUtil.c b/src/temp/ivy/satUtil.c
deleted file mode 100644
index f2b78fe6..00000000
--- a/src/temp/ivy/satUtil.c
+++ /dev/null
@@ -1,161 +0,0 @@
-/**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
deleted file mode 100644
index ffa9c431..00000000
--- a/src/temp/ivy/satVec.h
+++ /dev/null
@@ -1,83 +0,0 @@
-/**************************************************************************************************
-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
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-11 02:02:42 +0000