diff options
Diffstat (limited to 'src/temp/ivy')
| -rw-r--r-- | src/temp/ivy/ivy.h | 13 | ||||
| -rw-r--r-- | src/temp/ivy/ivyFastMap.c | 41 | ||||
| -rw-r--r-- | src/temp/ivy/ivyFraig.c | 626 | ||||
| -rw-r--r-- | src/temp/ivy/ivyMan.c | 104 | ||||
| -rw-r--r-- | src/temp/ivy/ivyResyn.c | 50 | ||||
| -rw-r--r-- | src/temp/ivy/module.make | 4 | ||||
| -rw-r--r-- | src/temp/ivy/satMem.c | 527 | ||||
| -rw-r--r-- | src/temp/ivy/satMem.h | 78 | ||||
| -rw-r--r-- | src/temp/ivy/satSolver.c | 1279 | ||||
| -rw-r--r-- | src/temp/ivy/satSolver.h | 154 | ||||
| -rw-r--r-- | src/temp/ivy/satUtil.c | 161 | ||||
| -rw-r--r-- | src/temp/ivy/satVec.h | 83 |
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 |