diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/base/abc/abc.h | 2 | ||||
-rw-r--r-- | src/base/abci/abc.c | 189 | ||||
-rw-r--r-- | src/base/abci/abcIvy.c | 61 | ||||
-rw-r--r-- | src/base/abci/abcStrash.c | 13 | ||||
-rw-r--r-- | src/sat/asat/solver.c | 7 | ||||
-rw-r--r-- | src/sat/asat/solver.h | 2 | ||||
-rw-r--r-- | src/sat/fraig/fraigSat.c | 14 | ||||
-rw-r--r-- | src/temp/ivy/ivy.h | 15 | ||||
-rw-r--r-- | src/temp/ivy/ivyFraig.c | 1209 | ||||
-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 | 93 | ||||
-rw-r--r-- | src/temp/ivy/satSolver.h | 15 |
13 files changed, 1998 insertions, 227 deletions
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h index c4dbb52f..b619e8b9 100644 --- a/src/base/abc/abc.h +++ b/src/base/abc/abc.h @@ -601,8 +601,8 @@ extern Abc_Obj_t * Abc_NtkDupBox( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pBox, extern Abc_Obj_t * Abc_NtkCloneObj( Abc_Obj_t * pNode ); extern Abc_Obj_t * Abc_NtkFindNode( Abc_Ntk_t * pNtk, char * pName ); extern Abc_Obj_t * Abc_NtkFindNet( Abc_Ntk_t * pNtk, char * pName ); -extern Abc_Obj_t * Abc_NtkFindTerm( Abc_Ntk_t * pNtk, char * pName ); extern Abc_Obj_t * Abc_NtkFindCi( Abc_Ntk_t * pNtk, char * pName ); +extern Abc_Obj_t * Abc_NtkFindCo( Abc_Ntk_t * pNtk, char * pName ); extern Abc_Obj_t * Abc_NtkFindOrCreateNet( Abc_Ntk_t * pNtk, char * pName ); extern Abc_Obj_t * Abc_NodeCreateConst0( Abc_Ntk_t * pNtk ); extern Abc_Obj_t * Abc_NodeCreateConst1( Abc_Ntk_t * pNtk ); diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index b0ccae3a..2427146c 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -97,7 +97,9 @@ static int Abc_CommandICut ( Abc_Frame_t * pAbc, int argc, char ** arg static int Abc_CommandIRewrite ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandIRewriteSeq ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandIResyn ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandISat ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandIFraig ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandIProve ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandHaig ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandMini ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -224,7 +226,9 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "New AIG", "irw", Abc_CommandIRewrite, 1 ); Cmd_CommandAdd( pAbc, "New AIG", "irws", Abc_CommandIRewriteSeq, 1 ); Cmd_CommandAdd( pAbc, "New AIG", "iresyn", Abc_CommandIResyn, 1 ); + Cmd_CommandAdd( pAbc, "New AIG", "isat", Abc_CommandISat, 1 ); Cmd_CommandAdd( pAbc, "New AIG", "ifraig", Abc_CommandIFraig, 1 ); + Cmd_CommandAdd( pAbc, "New AIG", "iprove", Abc_CommandIProve, 1 ); Cmd_CommandAdd( pAbc, "New AIG", "haig", Abc_CommandHaig, 1 ); Cmd_CommandAdd( pAbc, "New AIG", "mini", Abc_CommandMini, 1 ); @@ -3354,7 +3358,8 @@ int Abc_CommandAppend( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } Abc_NtkDelete( pNtk2 ); - + // sweep dangling logic + Abc_AigCleanup( pNtk->pManFunc ); // replace the current network // Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); return 0; @@ -5441,26 +5446,126 @@ usage: SeeAlso [] ***********************************************************************/ +int Abc_CommandISat( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk, * pNtkRes; + int c, fUpdateLevel, fVerbose; + int nConfLimit; + + extern Abc_Ntk_t * Abc_NtkIvySat( Abc_Ntk_t * pNtk, int nConfLimit, int fVerbose ); + + pNtk = Abc_FrameReadNtk(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + nConfLimit = 100000; + fUpdateLevel = 1; + fVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "Clzvh" ) ) != EOF ) + { + switch ( c ) + { + case 'C': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" ); + goto usage; + } + nConfLimit = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nConfLimit < 0 ) + goto usage; + break; + case 'l': + fUpdateLevel ^= 1; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pNtk == NULL ) + { + fprintf( pErr, "Empty network.\n" ); + return 1; + } + if ( Abc_NtkIsSeq(pNtk) ) + { + fprintf( pErr, "Only works for non-sequential networks.\n" ); + return 1; + } + + pNtkRes = Abc_NtkIvySat( pNtk, nConfLimit, fVerbose ); + if ( pNtkRes == NULL ) + { + fprintf( pErr, "Command has failed.\n" ); + return 0; + } + // replace the current network + Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); + return 0; + +usage: + fprintf( pErr, "usage: isat [-C num] [-vh]\n" ); + fprintf( pErr, "\t tries to prove the miter constant 0\n" ); + fprintf( pErr, "\t-C num : limit on the number of conflicts [default = %d]\n", nConfLimit ); +// fprintf( pErr, "\t-l : toggle preserving the number of levels [default = %s]\n", fUpdateLevel? "yes": "no" ); + fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" ); + fprintf( pErr, "\t-h : print the command usage\n"); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ int Abc_CommandIFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; Abc_Ntk_t * pNtk, * pNtkRes; int c, fUpdateLevel, fVerbose; + int nConfLimit; - extern Abc_Ntk_t * Abc_NtkIvyFraig( Abc_Ntk_t * pNtk ); + extern Abc_Ntk_t * Abc_NtkIvyFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fVerbose ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); // set defaults + nConfLimit = 100; fUpdateLevel = 1; fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "lzvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "Clzvh" ) ) != EOF ) { switch ( c ) { + case 'C': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" ); + goto usage; + } + nConfLimit = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nConfLimit < 0 ) + goto usage; + break; case 'l': fUpdateLevel ^= 1; break; @@ -5484,7 +5589,7 @@ int Abc_CommandIFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } - pNtkRes = Abc_NtkIvyFraig( pNtk ); + pNtkRes = Abc_NtkIvyFraig( pNtk, nConfLimit, fVerbose ); if ( pNtkRes == NULL ) { fprintf( pErr, "Command has failed.\n" ); @@ -5495,8 +5600,82 @@ int Abc_CommandIFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: ifraig [-h]\n" ); + fprintf( pErr, "usage: ifraig [-C num] [-vh]\n" ); fprintf( pErr, "\t performs fraiging using a new method\n" ); + fprintf( pErr, "\t-C num : limit on the number of conflicts [default = %d]\n", nConfLimit ); +// fprintf( pErr, "\t-l : toggle preserving the number of levels [default = %s]\n", fUpdateLevel? "yes": "no" ); + fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" ); + fprintf( pErr, "\t-h : print the command usage\n"); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandIProve( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk, * pNtkRes; + int c, fUpdateLevel, fVerbose; + + extern Abc_Ntk_t * Abc_NtkIvyProve( Abc_Ntk_t * pNtk ); + + pNtk = Abc_FrameReadNtk(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + fUpdateLevel = 1; + fVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "lzvh" ) ) != EOF ) + { + switch ( c ) + { + case 'l': + fUpdateLevel ^= 1; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pNtk == NULL ) + { + fprintf( pErr, "Empty network.\n" ); + return 1; + } + if ( Abc_NtkIsSeq(pNtk) ) + { + fprintf( pErr, "Only works for non-sequential networks.\n" ); + return 1; + } + + pNtkRes = Abc_NtkIvyProve( pNtk ); + if ( pNtkRes == NULL ) + { + fprintf( pErr, "Command has failed.\n" ); + return 0; + } + // replace the current network + Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); + return 0; + +usage: + fprintf( pErr, "usage: iprove [-h]\n" ); + fprintf( pErr, "\t performs CEC using a new method\n" ); // fprintf( pErr, "\t-l : toggle preserving the number of levels [default = %s]\n", fUpdateLevel? "yes": "no" ); // fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); diff --git a/src/base/abci/abcIvy.c b/src/base/abci/abcIvy.c index 3a5333f4..320c76dd 100644 --- a/src/base/abci/abcIvy.c +++ b/src/base/abci/abcIvy.c @@ -338,7 +338,7 @@ Abc_Ntk_t * Abc_NtkIvyResyn( Abc_Ntk_t * pNtk, int fUpdateLevel, int fVerbose ) SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkIvyFraig( Abc_Ntk_t * pNtk ) +Abc_Ntk_t * Abc_NtkIvySat( Abc_Ntk_t * pNtk, int nConfLimit, int fVerbose ) { Ivy_FraigParams_t Params, * pParams = &Params; Abc_Ntk_t * pNtkAig; @@ -347,6 +347,38 @@ Abc_Ntk_t * Abc_NtkIvyFraig( Abc_Ntk_t * pNtk ) if ( pMan == NULL ) return NULL; Ivy_FraigParamsDefault( pParams ); + pParams->nBTLimitMiter = nConfLimit; + pParams->fVerbose = fVerbose; +// pMan = Ivy_FraigPerform( pTemp = pMan, pParams ); + pMan = Ivy_FraigMiter( pTemp = pMan, pParams ); + Ivy_ManStop( pTemp ); + pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 0, 0 ); + Ivy_ManStop( pMan ); + return pNtkAig; +} + +/**Function************************************************************* + + Synopsis [Gives the current ABC network to AIG manager for processing.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkIvyFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fVerbose ) +{ + Ivy_FraigParams_t Params, * pParams = &Params; + Abc_Ntk_t * pNtkAig; + Ivy_Man_t * pMan, * pTemp; + pMan = Abc_NtkIvyBefore( pNtk, 0, 0 ); + if ( pMan == NULL ) + return NULL; + Ivy_FraigParamsDefault( pParams ); + pParams->nBTLimitNode = nConfLimit; + pParams->fVerbose = fVerbose; pMan = Ivy_FraigPerform( pTemp = pMan, pParams ); Ivy_ManStop( pTemp ); pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 0, 0 ); @@ -365,6 +397,33 @@ Abc_Ntk_t * Abc_NtkIvyFraig( Abc_Ntk_t * pNtk ) SeeAlso [] ***********************************************************************/ +Abc_Ntk_t * Abc_NtkIvyProve( Abc_Ntk_t * pNtk ) +{ + Ivy_FraigParams_t Params, * pParams = &Params; + Abc_Ntk_t * pNtkAig; + Ivy_Man_t * pMan, * pTemp; + pMan = Abc_NtkIvyBefore( pNtk, 0, 0 ); + if ( pMan == NULL ) + return NULL; + Ivy_FraigParamsDefault( pParams ); + pMan = Ivy_FraigProve( pTemp = pMan, pParams ); + Ivy_ManStop( pTemp ); + pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 0, 0 ); + Ivy_ManStop( pMan ); + return pNtkAig; +} + +/**Function************************************************************* + + Synopsis [Gives the current ABC network to AIG manager for processing.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ Abc_Ntk_t * Abc_NtkIvy( Abc_Ntk_t * pNtk ) { // Abc_Ntk_t * pNtkAig; diff --git a/src/base/abci/abcStrash.c b/src/base/abci/abcStrash.c index a130c11f..e8dc9793 100644 --- a/src/base/abci/abcStrash.c +++ b/src/base/abci/abcStrash.c @@ -135,9 +135,8 @@ Abc_Ntk_t * Abc_NtkStrash( Abc_Ntk_t * pNtk, bool fAllNodes, bool fCleanup ) Synopsis [Appends the second network to the first.] Description [Modifies the first network by adding the logic of the second. - Performs structural hashing while appending the networks. Does not add - the COs of the second. Does not change the second network. Returns 0 - if the appending failed, 1 otherise.] + Performs structural hashing while appending the networks. Does not change + the second network. Returns 0 if the appending failed, 1 otherise.] SideEffects [] @@ -159,11 +158,15 @@ int Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fAddPos ) // check that the networks have the same PIs // reorder PIs of pNtk2 according to pNtk1 if ( !Abc_NtkCompareSignals( pNtk1, pNtk2, 1, 1 ) ) - return 0; + printf( "Abc_NtkAppend(): The union of the network PIs is computed (warning).\n" ); // perform strashing Abc_NtkCleanCopy( pNtk2 ); Abc_NtkForEachCi( pNtk2, pObj, i ) - pObj->pCopy = Abc_NtkCi(pNtk1, i); + { + pObj->pCopy = Abc_NtkFindCi(pNtk1, Abc_ObjName(pObj)); + if ( pObj->pCopy == NULL ) + pObj->pCopy = Abc_NtkDupObj(pNtk1, pObj, 1); + } // add pNtk2 to pNtk1 while strashing if ( Abc_NtkIsLogic(pNtk2) ) Abc_NtkStrashPerform( pNtk2, pNtk1, 1 ); diff --git a/src/sat/asat/solver.c b/src/sat/asat/solver.c index 34b4d233..6f8fe037 100644 --- a/src/sat/asat/solver.c +++ b/src/sat/asat/solver.c @@ -853,9 +853,16 @@ static lbool solver_search(solver* s, int nof_conflicts, int nof_learnts) // reset the activities if ( s->factors ) + { + s->var_inc = 1.0; for ( i = 0; i < s->size; i++ ) + { s->activity[i] = (double)s->factors[i]; +// if ( s->orderpos[i] != -1 ) +// order_update(s, i ); + } // s->activity[i] = 1.0; + } for (;;){ clause* confl = solver_propagate(s); diff --git a/src/sat/asat/solver.h b/src/sat/asat/solver.h index 7a5e5be6..bd6e8569 100644 --- a/src/sat/asat/solver.h +++ b/src/sat/asat/solver.h @@ -76,7 +76,7 @@ extern void solver_delete(solver* s); extern bool solver_addclause(solver* s, lit* begin, lit* end); extern bool solver_simplify(solver* s); -extern int solver_solve(solver* s, lit* begin, lit* end, sint64 nConfLimit, sint64 nInsLimit ); +extern int solver_solve(solver* s, lit* begin, lit* end, sint64 nConfLimit, sint64 nInsLimit); extern int * solver_get_model( solver * p, int * pVars, int nVars ); extern int solver_nvars(solver* s); diff --git a/src/sat/fraig/fraigSat.c b/src/sat/fraig/fraigSat.c index af0f13ce..53057fc3 100644 --- a/src/sat/fraig/fraigSat.c +++ b/src/sat/fraig/fraigSat.c @@ -300,6 +300,7 @@ int Fraig_NodeIsEquivalent( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * { int RetValue, RetValue1, i, fComp, clk; int fVerbose = 0; + int fSwitch = 0; // make sure the nodes are not complemented assert( !Fraig_IsComplement(pNew) ); @@ -318,6 +319,7 @@ int Fraig_NodeIsEquivalent( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * if ( nBTLimit <= 10 ) return 0; nBTLimit = (int)sqrt(nBTLimit); +// fSwitch = 1; } p->nSatCalls++; @@ -417,6 +419,8 @@ PRT( "time", clock() - clk ); // if ( pOld->fFailTfo || pNew->fFailTfo ) // printf( "*" ); // printf( "s(%d)", pNew->Level ); + if ( fSwitch ) + printf( "s(%d)", pNew->Level ); p->nSatCounter++; return 0; } @@ -433,6 +437,8 @@ p->time3 += clock() - clk; pOld->fFailTfo = 1; pNew->fFailTfo = 1; // p->nSatFails++; + if ( fSwitch ) + printf( "T(%d)", pNew->Level ); p->nSatFailsReal++; return 0; } @@ -491,6 +497,8 @@ PRT( "time", clock() - clk ); // if ( pOld->fFailTfo || pNew->fFailTfo ) // printf( "*" ); // printf( "s(%d)", pNew->Level ); + if ( fSwitch ) + printf( "s(%d)", pNew->Level ); return 0; } else // if ( RetValue1 == MSAT_UNKNOWN ) @@ -500,6 +508,8 @@ p->time3 += clock() - clk; // if ( pOld->fFailTfo || pNew->fFailTfo ) // printf( "*" ); // printf( "T(%d)", pNew->Level ); + if ( fSwitch ) + printf( "T(%d)", pNew->Level ); // mark the node as the failed node pOld->fFailTfo = 1; @@ -515,6 +525,10 @@ p->time3 += clock() - clk; // if ( pOld->fFailTfo || pNew->fFailTfo ) // printf( "*" ); // printf( "u(%d)", pNew->Level ); + + if ( fSwitch ) + printf( "u(%d)", pNew->Level ); + return 1; } diff --git a/src/temp/ivy/ivy.h b/src/temp/ivy/ivy.h index 5b684244..d9c17d80 100644 --- a/src/temp/ivy/ivy.h +++ b/src/temp/ivy/ivy.h @@ -128,8 +128,17 @@ 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 + int nSimWords; // the number of words in the simulation info + double SimSatur; // the ratio of refined classes when saturation is reached + int fPatScores; // enables simulation pattern scoring + int MaxScore; // max score after which resimulation is used + int fVerbose; // verbose output + int nBTLimitNode; // conflict limit at a node + int nBTLimitMiter; // conflict limit at an output + int nBTLimitGlobal; // conflict limit global + int nInsLimitNode; // inspection limit at a node + int nInsLimitMiter; // inspection limit at an output + int nInsLimitGlobal; // inspection limit global }; @@ -441,7 +450,9 @@ 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 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 void Ivy_FraigParamsDefault( Ivy_FraigParams_t * pParams ); /*=== ivyHaig.c ==========================================================*/ extern void Ivy_ManHaigStart( Ivy_Man_t * p, int fVerbose ); diff --git a/src/temp/ivy/ivyFraig.c b/src/temp/ivy/ivyFraig.c index a3a3b33a..88c726c7 100644 --- a/src/temp/ivy/ivyFraig.c +++ b/src/temp/ivy/ivyFraig.c @@ -20,13 +20,33 @@ #include "ivy.h" #include "satSolver.h" +#include "extra.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -typedef struct Ivy_Fraig_t_ Ivy_Fraig_t; -struct Ivy_Fraig_t_ +typedef struct Ivy_FraigMan_t_ Ivy_FraigMan_t; +typedef struct Ivy_FraigSim_t_ Ivy_FraigSim_t; +typedef struct Ivy_FraigList_t_ Ivy_FraigList_t; + +struct Ivy_FraigList_t_ +{ + Ivy_Obj_t * pHead; + Ivy_Obj_t * pTail; + int nItems; +}; + +struct Ivy_FraigSim_t_ +{ + int Type; + Ivy_FraigSim_t * pNext; + Ivy_FraigSim_t * pFanin0; + Ivy_FraigSim_t * pFanin1; + unsigned pData[0]; +}; + +struct Ivy_FraigMan_t_ { // general info Ivy_FraigParams_t * pParams; // various parameters @@ -34,23 +54,31 @@ struct Ivy_Fraig_t_ Ivy_Man_t * pManAig; // the starting AIG manager Ivy_Man_t * pManFraig; // the final AIG manager // simulation information - int nWords; // the number of words - unsigned * pWords; // the simulation info + int nSimWords; // the number of words + char * pSimWords; // the simulation info + Ivy_FraigSim_t * pSimStart; // the list of simulation info for internal nodes // counter example storage int nPatWords; // the number of words in the counter example unsigned * pPatWords; // the counter example + int * pPatScores; // the scores of each pattern // equivalence classes - int nClasses; // the number of equivalence classes - Ivy_Obj_t * pClassesHead; // the linked list of classes - Ivy_Obj_t * pClassesTail; // the linked list of classes + Ivy_FraigList_t lClasses; // equivalence classes + Ivy_FraigList_t lCand; // candidatates + int nPairs; // the number of pairs of nodes // equivalence checking sat_solver * pSat; // SAT solver int nSatVars; // the number of variables currently used + Vec_Ptr_t * vPiVars; // the PIs of the cone used + // other + ProgressBar * pProgress; // statistics int nSimRounds; + int nNodesMiter; int nClassesZero; int nClassesBeg; int nClassesEnd; + int nPairsBeg; + int nPairsEnd; int nSatCalls; int nSatCallsSat; int nSatCallsUnsat; @@ -61,11 +89,16 @@ struct Ivy_Fraig_t_ int timeSim; int timeTrav; int timeSat; + int timeSatUnsat; + int timeSatSat; + int timeSatFail; int timeRef; int timeTotal; + int time1; + int time2; }; -static inline unsigned * Ivy_ObjSim( Ivy_Obj_t * pObj ) { return (unsigned *)pObj->pFanout; } +static inline Ivy_FraigSim_t * Ivy_ObjSim( Ivy_Obj_t * pObj ) { return (Ivy_FraigSim_t *)pObj->pFanout; } static inline Ivy_Obj_t * Ivy_ObjClassNodeLast( Ivy_Obj_t * pObj ) { return pObj->pNextFan0; } static inline Ivy_Obj_t * Ivy_ObjClassNodeRepr( Ivy_Obj_t * pObj ) { return pObj->pNextFan0; } static inline Ivy_Obj_t * Ivy_ObjClassNodeNext( Ivy_Obj_t * pObj ) { return pObj->pNextFan1; } @@ -76,7 +109,7 @@ static inline Ivy_Obj_t * Ivy_ObjFraig( Ivy_Obj_t * pObj ) static inline int Ivy_ObjSatNum( Ivy_Obj_t * pObj ) { return (int)pObj->pNextFan0; } static inline Vec_Ptr_t * Ivy_ObjFaninVec( Ivy_Obj_t * pObj ) { return (Vec_Ptr_t *)pObj->pNextFan1; } -static inline void Ivy_ObjSetSim( Ivy_Obj_t * pObj, unsigned * pSim ) { pObj->pFanout = (Ivy_Obj_t *)pSim; } +static inline void Ivy_ObjSetSim( Ivy_Obj_t * pObj, Ivy_FraigSim_t * pSim ) { pObj->pFanout = (Ivy_Obj_t *)pSim; } static inline void Ivy_ObjSetClassNodeLast( Ivy_Obj_t * pObj, Ivy_Obj_t * pLast ) { pObj->pNextFan0 = pLast; } static inline void Ivy_ObjSetClassNodeRepr( Ivy_Obj_t * pObj, Ivy_Obj_t * pRepr ) { pObj->pNextFan0 = pRepr; } static inline void Ivy_ObjSetClassNodeNext( Ivy_Obj_t * pObj, Ivy_Obj_t * pNext ) { pObj->pNextFan1 = pNext; } @@ -105,33 +138,26 @@ static inline unsigned Ivy_ObjRandomSim() { return (ran for ( pEnt = pClass; \ pEnt; \ pEnt = Ivy_ObjClassNodeNext(pEnt) ) -#define Ivy_FraigForEachClassNodeSafe( pClass, pEnt, pEnt2 ) \ - for ( pEnt = pClass, \ - pEnt2 = pEnt? Ivy_ObjClassNodeNext(pEnt): NULL; \ - pEnt; \ - pEnt = pEnt2, \ - pEnt2 = pEnt? Ivy_ObjClassNodeNext(pEnt): NULL ) // iterate through nodes in the hash table #define Ivy_FraigForEachBinNode( pBin, pEnt ) \ for ( pEnt = pBin; \ pEnt; \ pEnt = Ivy_ObjNodeHashNext(pEnt) ) -#define Ivy_FraigForEachBinNodeSafe( pBin, pEnt, pEnt2 ) \ - for ( pEnt = pBin, \ - pEnt2 = pEnt? Ivy_ObjNodeHashNext(pEnt): NULL; \ - pEnt; \ - pEnt = pEnt2, \ - pEnt2 = pEnt? Ivy_ObjNodeHashNext(pEnt): NULL ) - -static Ivy_Fraig_t * Ivy_FraigStart( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams ); -static void Ivy_FraigPrint( Ivy_Fraig_t * p ); -static void Ivy_FraigStop( Ivy_Fraig_t * p ); -static void Ivy_FraigSimulate( Ivy_Fraig_t * p ); -static void Ivy_FraigSweep( Ivy_Fraig_t * p ); -static Ivy_Obj_t * Ivy_FraigAnd( Ivy_Fraig_t * p, Ivy_Obj_t * pObjOld ); -static int Ivy_FraigNodesAreEquiv( Ivy_Fraig_t * p, Ivy_Obj_t * pObj0, Ivy_Obj_t * pObj1, int nBTLimit ); -static void Ivy_FraigNodeAddToSolver( Ivy_Fraig_t * p, Ivy_Obj_t * pObj0, Ivy_Obj_t * pObj1 ); -static int Ivy_FraigMarkConeSetActivity_rec( Ivy_Fraig_t * p, Ivy_Obj_t * pObj, int * pTravIds, int TravId, double * pFactors, int LevelMax ); + +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 void Ivy_FraigPrint( Ivy_FraigMan_t * p ); +static void Ivy_FraigStop( Ivy_FraigMan_t * p ); +static void Ivy_FraigSimulate( Ivy_FraigMan_t * p ); +static void Ivy_FraigSweep( Ivy_FraigMan_t * p ); +static Ivy_Obj_t * Ivy_FraigAnd( Ivy_FraigMan_t * p, Ivy_Obj_t * pObjOld ); +static int Ivy_FraigNodesAreEquiv( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj0, Ivy_Obj_t * pObj1 ); +static int Ivy_FraigNodeIsConst( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj ); +static void Ivy_FraigNodeAddToSolver( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj0, Ivy_Obj_t * pObj1 ); +static int Ivy_FraigMarkConeSetActivity( 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 void Ivy_FraigMiterProve( Ivy_FraigMan_t * p ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -148,9 +174,36 @@ static int Ivy_FraigMarkConeSetActivity_rec( Ivy_Fraig_t * p, Ivy_Obj_ SeeAlso [] ***********************************************************************/ +Ivy_Man_t * Ivy_FraigProve( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams ) +{ + Ivy_FraigMan_t * p; + Ivy_Man_t * pManAigNew; + int clk; +clk = clock(); + assert( Ivy_ManLatchNum(pManAig) == 0 ); + p = Ivy_FraigStart( pManAig, pParams ); + Ivy_FraigSimulate( p ); + Ivy_FraigSweep( p ); + pManAigNew = p->pManFraig; +p->timeTotal = clock() - clk; + Ivy_FraigStop( p ); + return pManAigNew; +} + +/**Function************************************************************* + + Synopsis [Performs fraiging of the initial AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ Ivy_Man_t * Ivy_FraigPerform( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams ) { - Ivy_Fraig_t * p; + Ivy_FraigMan_t * p; Ivy_Man_t * pManAigNew; int clk; clk = clock(); @@ -175,11 +228,62 @@ p->timeTotal = clock() - clk; SeeAlso [] ***********************************************************************/ +Ivy_Man_t * Ivy_FraigMiter( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams ) +{ + Ivy_FraigMan_t * p; + Ivy_Man_t * pManAigNew; + Ivy_Obj_t * pObj; + int i, clk; +clk = clock(); + assert( Ivy_ManLatchNum(pManAig) == 0 ); + p = Ivy_FraigStartSimple( pManAig, pParams ); + // duplicate internal nodes + Ivy_ManForEachNode( p->pManAig, pObj, i ) + pObj->pEquiv = Ivy_And( p->pManFraig, Ivy_ObjChild0Equiv(pObj), Ivy_ObjChild1Equiv(pObj) ); + // try to prove each output of the miter + Ivy_FraigMiterProve( p ); + // add the POs + Ivy_ManForEachPo( p->pManAig, pObj, i ) + Ivy_ObjCreatePo( p->pManFraig, Ivy_ObjChild0Equiv(pObj) ); + // clean the new manager + Ivy_ManForEachObj( p->pManFraig, pObj, i ) + { + if ( Ivy_ObjFaninVec(pObj) ) + Vec_PtrFree( Ivy_ObjFaninVec(pObj) ); + pObj->pNextFan0 = pObj->pNextFan1 = NULL; + } + // remove dangling nodes + Ivy_ManCleanup( p->pManFraig ); + pManAigNew = p->pManFraig; +p->timeTotal = clock() - clk; + 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->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************************************************************* @@ -193,31 +297,81 @@ void Ivy_FraigParamsDefault( Ivy_FraigParams_t * pParams ) SeeAlso [] ***********************************************************************/ -Ivy_Fraig_t * Ivy_FraigStart( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams ) +Ivy_FraigMan_t * Ivy_FraigStartSimple( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams ) { - Ivy_Fraig_t * p; + Ivy_FraigMan_t * p; + // allocat the fraiging manager + p = ALLOC( Ivy_FraigMan_t, 1 ); + memset( p, 0, sizeof(Ivy_FraigMan_t) ); + p->pParams = pParams; + p->pManAig = pManAig; + p->pManFraig = Ivy_ManStartFrom( pManAig ); + p->vPiVars = Vec_PtrAlloc( 100 ); + return p; +} + +/**Function************************************************************* + + Synopsis [Starts the fraiging manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_FraigMan_t * Ivy_FraigStart( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams ) +{ + Ivy_FraigMan_t * p; + Ivy_FraigSim_t * pSims; Ivy_Obj_t * pObj; - int i, k; + int i, k, EntrySize; // clean the fanout representation Ivy_ManForEachObj( pManAig, pObj, i ) // pObj->pEquiv = pObj->pFanout = pObj->pNextFan0 = pObj->pNextFan1 = pObj->pPrevFan0 = pObj->pPrevFan1 = NULL; assert( !pObj->pEquiv && !pObj->pFanout ); // allocat the fraiging manager - p = ALLOC( Ivy_Fraig_t, 1 ); - memset( p, 0, sizeof(Ivy_Fraig_t) ); + p = ALLOC( Ivy_FraigMan_t, 1 ); + memset( p, 0, sizeof(Ivy_FraigMan_t) ); p->pParams = pParams; p->pManAig = pManAig; p->pManFraig = Ivy_ManStartFrom( pManAig ); // allocate simulation info - p->nWords = pParams->nSimWords; - p->pWords = ALLOC( unsigned, Ivy_ManObjNum(pManAig) * p->nWords ); + p->nSimWords = pParams->nSimWords; +// p->pSimWords = ALLOC( unsigned, Ivy_ManObjNum(pManAig) * p->nSimWords ); + EntrySize = sizeof(Ivy_FraigSim_t) + sizeof(unsigned) * p->nSimWords; + p->pSimWords = (char *)malloc( Ivy_ManObjNum(pManAig) * EntrySize ); + memset( p->pSimWords, 0, EntrySize ); k = 0; Ivy_ManForEachObj( pManAig, pObj, i ) - Ivy_ObjSetSim( pObj, p->pWords + p->nWords * k++ ); + { + pSims = (Ivy_FraigSim_t *)(p->pSimWords + EntrySize * k++); + pSims->pNext = NULL; + if ( Ivy_ObjIsNode(pObj) ) + { + if ( p->pSimStart == NULL ) + p->pSimStart = pSims; + else + ((Ivy_FraigSim_t *)(p->pSimWords + EntrySize * (k-2)))->pNext = pSims; + pSims->pFanin0 = Ivy_ObjSim( Ivy_ObjFanin0(pObj) ); + pSims->pFanin1 = Ivy_ObjSim( Ivy_ObjFanin1(pObj) ); + pSims->Type = (Ivy_ObjFaninPhase(Ivy_ObjChild0(pObj)) << 2) | (Ivy_ObjFaninPhase(Ivy_ObjChild1(pObj)) << 1) | pObj->fPhase; + } + else + { + pSims->pFanin0 = NULL; + pSims->pFanin1 = NULL; + pSims->Type = 0; + } + Ivy_ObjSetSim( pObj, pSims ); + } assert( k == Ivy_ManObjNum(pManAig) ); // allocate storage for sim pattern p->nPatWords = Ivy_BitWordNum( Ivy_ManPiNum(pManAig) ); p->pPatWords = ALLOC( unsigned, p->nPatWords ); + p->pPatScores = ALLOC( int, 32 * p->nSimWords ); + p->vPiVars = Vec_PtrAlloc( 100 ); // set random number generator srand( 0xABCABC ); return p; @@ -234,22 +388,27 @@ Ivy_Fraig_t * Ivy_FraigStart( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams ) SeeAlso [] ***********************************************************************/ -void Ivy_FraigPrint( Ivy_Fraig_t * p ) +void Ivy_FraigPrint( Ivy_FraigMan_t * p ) { double nMemory; - nMemory = (double)Ivy_ManObjNum(p->pManAig)*p->nWords*sizeof(unsigned)/(1<<20); - printf( "SimWords = %d. Rounds = %d. Mem = %0.2f Mb. ", p->nWords, p->nSimRounds, nMemory ); + nMemory = (double)Ivy_ManObjNum(p->pManAig)*p->nSimWords*sizeof(unsigned)/(1<<20); + printf( "SimWords = %d. Rounds = %d. Mem = %0.2f Mb. ", p->nSimWords, p->nSimRounds, nMemory ); printf( "Classes: Beg = %d. End = %d.\n", p->nClassesBeg, p->nClassesEnd ); + printf( "Limits: BTNode = %d. BTMiter = %d.\n", p->pParams->nBTLimitNode, p->pParams->nBTLimitMiter ); printf( "Proof = %d. Counter-example = %d. Fail = %d. FailReal = %d. Zero = %d.\n", p->nSatProof, p->nSatCallsSat, p->nSatFails, p->nSatFailsReal, p->nClassesZero ); - printf( "Nodes: Final = %d. Total = %d. Mux = %d. (Exor = %d.) SatVars = %d.\n", - Ivy_ManNodeNum(p->pManFraig), Ivy_ManNodeNum(p->pManAig), 0, 0, p->nSatVars ); + printf( "Final = %d. Miter = %d. Total = %d. Mux = %d. (Exor = %d.) SatVars = %d.\n", + Ivy_ManNodeNum(p->pManFraig), p->nNodesMiter, Ivy_ManNodeNum(p->pManAig), 0, 0, p->nSatVars ); if ( p->pSat ) Sat_SolverPrintStats( stdout, p->pSat ); PRT( "AIG simulation ", p->timeSim ); PRT( "AIG traversal ", p->timeTrav ); PRT( "SAT solving ", p->timeSat ); + PRT( " Unsat ", p->timeSatUnsat ); + PRT( " Sat ", p->timeSatSat ); + PRT( " Fail ", p->timeSatFail ); PRT( "Class refining ", p->timeRef ); PRT( "TOTAL RUNTIME ", p->timeTotal ); + PRT( "time1 ", p->time1 ); } /**Function************************************************************* @@ -263,15 +422,19 @@ void Ivy_FraigPrint( Ivy_Fraig_t * p ) SeeAlso [] ***********************************************************************/ -void Ivy_FraigStop( Ivy_Fraig_t * p ) +void Ivy_FraigStop( Ivy_FraigMan_t * p ) { - Ivy_FraigPrint( 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->pPatWords ); - free( p->pWords ); + FREE( p->pPatScores ); + FREE( p->pPatWords ); + FREE( p->pSimWords ); free( p ); } + /**Function************************************************************* Synopsis [Simulates one node.] @@ -283,13 +446,13 @@ void Ivy_FraigStop( Ivy_Fraig_t * p ) SeeAlso [] ***********************************************************************/ -void Ivy_NodeAssignRandom( Ivy_Fraig_t * p, Ivy_Obj_t * pObj ) +void Ivy_NodeAssignRandom( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj ) { - unsigned * pSims; + Ivy_FraigSim_t * pSims; int i; pSims = Ivy_ObjSim(pObj); - for ( i = 0; i < p->nWords; i++ ) - pSims[i] = Ivy_ObjRandomSim(); + for ( i = 0; i < p->nSimWords; i++ ) + pSims->pData[i] = Ivy_ObjRandomSim(); } /**Function************************************************************* @@ -303,13 +466,13 @@ void Ivy_NodeAssignRandom( Ivy_Fraig_t * p, Ivy_Obj_t * pObj ) SeeAlso [] ***********************************************************************/ -void Ivy_NodeAssignConst( Ivy_Fraig_t * p, Ivy_Obj_t * pObj, int fConst1 ) +void Ivy_NodeAssignConst( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj, int fConst1 ) { - unsigned * pSims; + Ivy_FraigSim_t * pSims; int i; pSims = Ivy_ObjSim(pObj); - for ( i = 0; i < p->nWords; i++ ) - pSims[i] = fConst1? ~(unsigned)0 : 0; + for ( i = 0; i < p->nSimWords; i++ ) + pSims->pData[i] = fConst1? ~(unsigned)0 : 0; } /**Function************************************************************* @@ -323,13 +486,13 @@ void Ivy_NodeAssignConst( Ivy_Fraig_t * p, Ivy_Obj_t * pObj, int fConst1 ) SeeAlso [] ***********************************************************************/ -int Ivy_NodeHasZeroSim( Ivy_Fraig_t * p, Ivy_Obj_t * pObj ) +int Ivy_NodeHasZeroSim( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj ) { - unsigned * pSims; + Ivy_FraigSim_t * pSims; int i; pSims = Ivy_ObjSim(pObj); - for ( i = 0; i < p->nWords; i++ ) - if ( pSims[i] ) + for ( i = 0; i < p->nSimWords; i++ ) + if ( pSims->pData[i] ) return 0; return 1; } @@ -345,14 +508,14 @@ int Ivy_NodeHasZeroSim( Ivy_Fraig_t * p, Ivy_Obj_t * pObj ) SeeAlso [] ***********************************************************************/ -int Ivy_NodeCompareSims( Ivy_Fraig_t * p, Ivy_Obj_t * pObj0, Ivy_Obj_t * pObj1 ) +int Ivy_NodeCompareSims( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj0, Ivy_Obj_t * pObj1 ) { - unsigned * pSims0, * pSims1; + Ivy_FraigSim_t * pSims0, * pSims1; int i; pSims0 = Ivy_ObjSim(pObj0); pSims1 = Ivy_ObjSim(pObj1); - for ( i = 0; i < p->nWords; i++ ) - if ( pSims0[i] != pSims1[i] ) + for ( i = 0; i < p->nSimWords; i++ ) + if ( pSims0->pData[i] != pSims1->pData[i] ) return 0; return 1; } @@ -368,9 +531,64 @@ int Ivy_NodeCompareSims( Ivy_Fraig_t * p, Ivy_Obj_t * pObj0, Ivy_Obj_t * pObj1 ) SeeAlso [] ***********************************************************************/ -void Ivy_NodeSimulate( Ivy_Fraig_t * p, Ivy_Obj_t * pObj ) +void Ivy_NodeSimulateSim( Ivy_FraigMan_t * p, Ivy_FraigSim_t * pSims ) { - unsigned * pSims, * pSims0, * pSims1; + unsigned * pData, * pData0, * pData1; + int i; + pData = pSims->pData; + pData0 = pSims->pFanin0->pData; + pData1 = pSims->pFanin1->pData; + switch( pSims->Type ) + { + case 0: + for ( i = 0; i < p->nSimWords; i++ ) + pData[i] = (pData0[i] & pData1[i]); + break; + case 1: + for ( i = 0; i < p->nSimWords; i++ ) + pData[i] = ~(pData0[i] & pData1[i]); + break; + case 2: + for ( i = 0; i < p->nSimWords; i++ ) + pData[i] = (pData0[i] & ~pData1[i]); + break; + case 3: + for ( i = 0; i < p->nSimWords; i++ ) + pData[i] = (~pData0[i] | pData1[i]); + break; + case 4: + for ( i = 0; i < p->nSimWords; i++ ) + pData[i] = (~pData0[i] & pData1[i]); + break; + case 5: + for ( i = 0; i < p->nSimWords; i++ ) + pData[i] = (pData0[i] | ~pData1[i]); + break; + case 6: + for ( i = 0; i < p->nSimWords; i++ ) + pData[i] = ~(pData0[i] | pData1[i]); + break; + case 7: + for ( i = 0; i < p->nSimWords; i++ ) + pData[i] = (pData0[i] | pData1[i]); + break; + } +} + +/**Function************************************************************* + + Synopsis [Simulates one node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_NodeSimulate( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj ) +{ + Ivy_FraigSim_t * pSims, * pSims0, * pSims1; int fCompl, fCompl0, fCompl1, i; assert( !Ivy_IsComplement(pObj) ); // get hold of the simulation information @@ -385,38 +603,38 @@ void Ivy_NodeSimulate( Ivy_Fraig_t * p, Ivy_Obj_t * pObj ) if ( fCompl0 && fCompl1 ) { if ( fCompl ) - for ( i = 0; i < p->nWords; i++ ) - pSims[i] = (pSims0[i] | pSims1[i]); + for ( i = 0; i < p->nSimWords; i++ ) + pSims->pData[i] = (pSims0->pData[i] | pSims1->pData[i]); else - for ( i = 0; i < p->nWords; i++ ) - pSims[i] = ~(pSims0[i] | pSims1[i]); + for ( i = 0; i < p->nSimWords; i++ ) + pSims->pData[i] = ~(pSims0->pData[i] | pSims1->pData[i]); } else if ( fCompl0 && !fCompl1 ) { if ( fCompl ) - for ( i = 0; i < p->nWords; i++ ) - pSims[i] = (pSims0[i] | ~pSims1[i]); + for ( i = 0; i < p->nSimWords; i++ ) + pSims->pData[i] = (pSims0->pData[i] | ~pSims1->pData[i]); else - for ( i = 0; i < p->nWords; i++ ) - pSims[i] = (~pSims0[i] & pSims1[i]); + for ( i = 0; i < p->nSimWords; i++ ) + pSims->pData[i] = (~pSims0->pData[i] & pSims1->pData[i]); } else if ( !fCompl0 && fCompl1 ) { if ( fCompl ) - for ( i = 0; i < p->nWords; i++ ) - pSims[i] = (~pSims0[i] | pSims1[i]); + for ( i = 0; i < p->nSimWords; i++ ) + pSims->pData[i] = (~pSims0->pData[i] | pSims1->pData[i]); else - for ( i = 0; i < p->nWords; i++ ) - pSims[i] = (pSims0[i] & ~pSims1[i]); + for ( i = 0; i < p->nSimWords; i++ ) + pSims->pData[i] = (pSims0->pData[i] & ~pSims1->pData[i]); } else // if ( !fCompl0 && !fCompl1 ) { if ( fCompl ) - for ( i = 0; i < p->nWords; i++ ) - pSims[i] = ~(pSims0[i] & pSims1[i]); + for ( i = 0; i < p->nSimWords; i++ ) + pSims->pData[i] = ~(pSims0->pData[i] & pSims1->pData[i]); else - for ( i = 0; i < p->nWords; i++ ) - pSims[i] = (pSims0[i] & pSims1[i]); + for ( i = 0; i < p->nSimWords; i++ ) + pSims->pData[i] = (pSims0->pData[i] & pSims1->pData[i]); } } @@ -431,7 +649,7 @@ void Ivy_NodeSimulate( Ivy_Fraig_t * p, Ivy_Obj_t * pObj ) SeeAlso [] ***********************************************************************/ -unsigned Ivy_NodeHash( Ivy_Fraig_t * p, Ivy_Obj_t * pObj ) +unsigned Ivy_NodeHash( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj ) { static int s_FPrimes[128] = { 1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459, @@ -448,13 +666,14 @@ unsigned Ivy_NodeHash( Ivy_Fraig_t * p, Ivy_Obj_t * pObj ) 7393, 7477, 7523, 7561, 7607, 7681, 7727, 7817, 7877, 7933, 8011, 8039, 8059, 8081, 8093, 8111, 8123, 8147 }; - unsigned uHash, * pSims; + Ivy_FraigSim_t * pSims; + unsigned uHash; int i; - assert( p->nWords <= 128 ); + assert( p->nSimWords <= 128 ); uHash = 0; pSims = Ivy_ObjSim(pObj); - for ( i = 0; i < p->nWords; i++ ) - uHash ^= pSims[i] * s_FPrimes[i]; + for ( i = 0; i < p->nSimWords; i++ ) + uHash ^= pSims->pData[i] * s_FPrimes[i]; return uHash; } @@ -469,7 +688,7 @@ unsigned Ivy_NodeHash( Ivy_Fraig_t * p, Ivy_Obj_t * pObj ) SeeAlso [] ***********************************************************************/ -void Ivy_FraigSimulateOne( Ivy_Fraig_t * p ) +void Ivy_FraigSimulateOne( Ivy_FraigMan_t * p ) { Ivy_Obj_t * pObj; int i, clk; @@ -501,7 +720,29 @@ p->nSimRounds++; SeeAlso [] ***********************************************************************/ -void Ivy_FraigAssignRandom( Ivy_Fraig_t * p ) +void Ivy_FraigSimulateOneSim( Ivy_FraigMan_t * p ) +{ + Ivy_FraigSim_t * pSims; + int clk; +clk = clock(); + for ( pSims = p->pSimStart; pSims; pSims = pSims->pNext ) + Ivy_NodeSimulateSim( p, pSims ); +p->timeSim += clock() - clk; +p->nSimRounds++; +} + +/**Function************************************************************* + + Synopsis [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; @@ -520,15 +761,15 @@ void Ivy_FraigAssignRandom( Ivy_Fraig_t * p ) SeeAlso [] ***********************************************************************/ -void Ivy_FraigAssignDist1( Ivy_Fraig_t * p, unsigned * pPat ) +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->nWords * 32 - 1 ); + 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) ), i+1 ); + 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" ); @@ -568,23 +809,23 @@ void Ivy_NodeAddToClass( Ivy_Obj_t * pClass, Ivy_Obj_t * pObj ) SeeAlso [] ***********************************************************************/ -void Ivy_FraigAddClass( Ivy_Fraig_t * p, Ivy_Obj_t * pClass ) +void Ivy_FraigAddClass( Ivy_FraigList_t * pList, Ivy_Obj_t * pClass ) { - if ( p->pClassesHead == NULL ) + if ( pList->pHead == NULL ) { - p->pClassesHead = pClass; - p->pClassesTail = pClass; + pList->pHead = pClass; + pList->pTail = pClass; Ivy_ObjSetEquivListPrev( pClass, NULL ); Ivy_ObjSetEquivListNext( pClass, NULL ); } else { - Ivy_ObjSetEquivListNext( p->pClassesTail, pClass ); - Ivy_ObjSetEquivListPrev( pClass, p->pClassesTail ); + Ivy_ObjSetEquivListNext( pList->pTail, pClass ); + Ivy_ObjSetEquivListPrev( pClass, pList->pTail ); Ivy_ObjSetEquivListNext( pClass, NULL ); - p->pClassesTail = pClass; + pList->pTail = pClass; } - p->nClasses++; + pList->nItems++; } /**Function************************************************************* @@ -598,16 +839,16 @@ void Ivy_FraigAddClass( Ivy_Fraig_t * p, Ivy_Obj_t * pClass ) SeeAlso [] ***********************************************************************/ -void Ivy_FraigInsertClass( Ivy_Fraig_t * p, Ivy_Obj_t * pBase, Ivy_Obj_t * pClass ) +void Ivy_FraigInsertClass( Ivy_FraigList_t * pList, Ivy_Obj_t * pBase, Ivy_Obj_t * pClass ) { Ivy_ObjSetEquivListPrev( pClass, pBase ); Ivy_ObjSetEquivListNext( pClass, Ivy_ObjEquivListNext(pBase) ); if ( Ivy_ObjEquivListNext(pBase) ) Ivy_ObjSetEquivListPrev( Ivy_ObjEquivListNext(pBase), pClass ); Ivy_ObjSetEquivListNext( pBase, pClass ); - if ( p->pClassesTail == pBase ) - p->pClassesTail = pClass; - p->nClasses++; + if ( pList->pTail == pBase ) + pList->pTail = pClass; + pList->nItems++; } /**Function************************************************************* @@ -621,19 +862,47 @@ void Ivy_FraigInsertClass( Ivy_Fraig_t * p, Ivy_Obj_t * pBase, Ivy_Obj_t * pClas SeeAlso [] ***********************************************************************/ -void Ivy_FraigRemoveClass( Ivy_Fraig_t * p, Ivy_Obj_t * pClass ) +void Ivy_FraigRemoveClass( Ivy_FraigList_t * pList, Ivy_Obj_t * pClass ) { - if ( p->pClassesHead == pClass ) - p->pClassesHead = Ivy_ObjEquivListNext(pClass); - if ( p->pClassesTail == pClass ) - p->pClassesTail = Ivy_ObjEquivListPrev(pClass); + if ( pList->pHead == pClass ) + pList->pHead = Ivy_ObjEquivListNext(pClass); + if ( pList->pTail == pClass ) + pList->pTail = Ivy_ObjEquivListPrev(pClass); if ( Ivy_ObjEquivListPrev(pClass) ) Ivy_ObjSetEquivListNext( Ivy_ObjEquivListPrev(pClass), Ivy_ObjEquivListNext(pClass) ); if ( Ivy_ObjEquivListNext(pClass) ) Ivy_ObjSetEquivListPrev( Ivy_ObjEquivListNext(pClass), Ivy_ObjEquivListPrev(pClass) ); Ivy_ObjSetEquivListNext( pClass, NULL ); Ivy_ObjSetEquivListPrev( pClass, NULL ); - p->nClasses--; + pClass->fMarkA = 0; + pList->nItems--; +} + +/**Function************************************************************* + + Synopsis [Count the number of pairs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ivy_FraigCountPairsClasses( Ivy_FraigMan_t * p ) +{ + Ivy_Obj_t * pClass, * pNode; + int nPairs = 0, nNodes; + return nPairs; + + Ivy_FraigForEachEquivClass( p->lClasses.pHead, pClass ) + { + nNodes = 0; + Ivy_FraigForEachClassNode( pClass, pNode ) + nNodes++; + nPairs += nNodes * (nNodes - 1) / 2; + } + return nPairs; } /**Function************************************************************* @@ -647,10 +916,10 @@ void Ivy_FraigRemoveClass( Ivy_Fraig_t * p, Ivy_Obj_t * pClass ) SeeAlso [] ***********************************************************************/ -void Ivy_FraigCreateClasses( Ivy_Fraig_t * p ) +void Ivy_FraigCreateClasses( Ivy_FraigMan_t * p ) { Ivy_Obj_t ** pTable; - Ivy_Obj_t * pObj, * pConst1, * pBin, * pEntry, * pEntry2; + Ivy_Obj_t * pObj, * pConst1, * pBin, * pEntry; int i, nTableSize; unsigned Hash; pConst1 = Ivy_ManConst1(p->pManAig); @@ -684,21 +953,24 @@ void Ivy_FraigCreateClasses( Ivy_Fraig_t * p ) pTable[Hash % nTableSize] = pObj; } // collect non-trivial classes - assert( p->pClassesHead == NULL ); - if ( Ivy_ObjClassNodeNext(pConst1) ) + assert( p->lClasses.pHead == NULL ); + Ivy_ManForEachObj( p->pManAig, pObj, i ) { - Ivy_FraigAddClass( p, pConst1 ); - Ivy_ObjSetClassNodeLast( pConst1, NULL ); + if ( !Ivy_ObjIsConst1(pObj) && !Ivy_ObjIsPi(pObj) && !Ivy_ObjIsNode(pObj) ) + continue; + Ivy_ObjSetNodeHashNext( pObj, NULL ); + if ( Ivy_ObjClassNodeRepr(pObj) == NULL ) + { + assert( Ivy_ObjClassNodeNext(pObj) == NULL ); + continue; + } + // recognize the head of the class + if ( Ivy_ObjClassNodeNext( Ivy_ObjClassNodeRepr(pObj) ) != NULL ) + continue; + // clean the class representative and add it to the list + Ivy_ObjSetClassNodeRepr( pObj, NULL ); + Ivy_FraigAddClass( &p->lClasses, pObj ); } - for ( i = 0; i < nTableSize; i++ ) - Ivy_FraigForEachBinNodeSafe( pTable[i], pEntry, pEntry2 ) - if ( Ivy_ObjClassNodeNext(pEntry) ) - { - Ivy_FraigAddClass( p, pEntry ); - Ivy_ObjSetClassNodeLast( pEntry, NULL ); - } - else - Ivy_ObjSetNodeHashNext( pEntry, NULL ); // free the table free( pTable ); } @@ -714,15 +986,20 @@ void Ivy_FraigCreateClasses( Ivy_Fraig_t * p ) SeeAlso [] ***********************************************************************/ -int Ivy_FraigRefineClass_rec( Ivy_Fraig_t * p, Ivy_Obj_t * pClass ) +int Ivy_FraigRefineClass_rec( Ivy_FraigMan_t * p, Ivy_Obj_t * pClass ) { Ivy_Obj_t * pClassNew, * pListOld, * pListNew, * pNode; + int RetValue = 0; // check if there is refinement pListOld = pClass; Ivy_FraigForEachClassNode( Ivy_ObjClassNodeNext(pClass), pClassNew ) { if ( !Ivy_NodeCompareSims(p, pClass, pClassNew) ) + { + if ( p->pParams->fPatScores ) + Ivy_FraigAddToPatScores( p, pClass, pClassNew ); break; + } pListOld = pClassNew; } if ( pClassNew == NULL ) @@ -749,16 +1026,16 @@ int Ivy_FraigRefineClass_rec( Ivy_Fraig_t * p, Ivy_Obj_t * pClass ) Ivy_ObjSetClassNodeNext( pListNew, NULL ); Ivy_ObjSetClassNodeNext( pListOld, NULL ); // update the list of classes - Ivy_FraigInsertClass( p, pClass, pClassNew ); + Ivy_FraigInsertClass( &p->lClasses, pClass, pClassNew ); // if the old class is trivial, remove it if ( Ivy_ObjClassNodeNext(pClass) == NULL ) - Ivy_FraigRemoveClass( p, pClass ); + Ivy_FraigRemoveClass( &p->lClasses, pClass ); // if the new class is trivial, remove it; otherwise, try to refine it if ( Ivy_ObjClassNodeNext(pClassNew) == NULL ) - Ivy_FraigRemoveClass( p, pClassNew ); + Ivy_FraigRemoveClass( &p->lClasses, pClassNew ); else - Ivy_FraigRefineClass_rec( p, pClassNew ); - return 1; + RetValue = Ivy_FraigRefineClass_rec( p, pClassNew ); + return RetValue + 1; } /**Function************************************************************* @@ -773,15 +1050,24 @@ int Ivy_FraigRefineClass_rec( Ivy_Fraig_t * p, Ivy_Obj_t * pClass ) SeeAlso [] ***********************************************************************/ -int Ivy_FraigRefineClasses( Ivy_Fraig_t * p ) +int Ivy_FraigRefineClasses( Ivy_FraigMan_t * p ) { Ivy_Obj_t * pClass, * pClass2; - int clk, RetValue = 0; + int clk, RetValue, Counter = 0; clk = clock(); - Ivy_FraigForEachEquivClassSafe( p->pClassesHead, pClass, pClass2 ) - RetValue += Ivy_FraigRefineClass_rec( p, pClass ); + Ivy_FraigForEachEquivClassSafe( p->lClasses.pHead, pClass, pClass2 ) + { + if ( pClass->fMarkA ) + continue; + RetValue = Ivy_FraigRefineClass_rec( p, pClass ); + Counter += ( RetValue > 0 ); +//if ( Ivy_ObjIsConst1(pClass) ) +//printf( "%d ", RetValue ); +if ( Ivy_ObjIsConst1(pClass) ) + p->time1 += clock() - clk; + } p->timeRef += clock() - clk; - return RetValue; + return Counter; } /**Function************************************************************* @@ -835,18 +1121,20 @@ int Ivy_FraigCountClassNodes( Ivy_Obj_t * pClass ) SeeAlso [] ***********************************************************************/ -int Ivy_FraigCountClasses( Ivy_Fraig_t * p ) +void Ivy_FraigPrintSimClasses( Ivy_FraigMan_t * p ) { Ivy_Obj_t * pClass; - int Counter = 0; - Ivy_FraigForEachEquivClass( p->pClassesHead, pClass ) - Counter++; - return Counter; + Ivy_FraigForEachEquivClass( p->lClasses.pHead, pClass ) + { +// Ivy_FraigPrintClass( pClass ); + printf( "%d ", Ivy_FraigCountClassNodes( pClass ) ); + } +// printf( "\n" ); } /**Function************************************************************* - Synopsis [Stops the fraiging manager.] + Synopsis [Copy pattern from the solver into the internal storage.] Description [] @@ -855,20 +1143,119 @@ int Ivy_FraigCountClasses( Ivy_Fraig_t * p ) SeeAlso [] ***********************************************************************/ -void Ivy_FraigPrintSimClasses( Ivy_Fraig_t * p ) +void Ivy_FraigSavePattern0( Ivy_FraigMan_t * p ) { - Ivy_Obj_t * pClass; - Ivy_FraigForEachEquivClass( p->pClassesHead, pClass ) - { -// Ivy_FraigPrintClass( pClass ); - printf( "%d ", Ivy_FraigCountClassNodes( pClass ) ); - } -// printf( "\n" ); + memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords ); +} + +/**Function************************************************************* + + Synopsis [Copy pattern from the solver into the internal storage.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_FraigSavePattern1( Ivy_FraigMan_t * p ) +{ + memset( p->pPatWords, 0xff, sizeof(unsigned) * p->nPatWords ); +} + +/**Function************************************************************* + + Synopsis [Copy pattern from the solver into the internal storage.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_FraigSavePattern( Ivy_FraigMan_t * p ) +{ + Ivy_Obj_t * pObj; + int i; + memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords ); + Ivy_ManForEachPi( p->pManFraig, pObj, i ) +// Vec_PtrForEachEntry( p->vPiVars, pObj, i ) + if ( p->pSat->model.ptr[Ivy_ObjSatNum(pObj)] == l_True ) + Ivy_InfoSetBit( p->pPatWords, i ); +// Ivy_InfoSetBit( p->pPatWords, pObj->Id - 1 ); +} + +/**Function************************************************************* + + Synopsis [Copy pattern from the solver into the internal storage.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_FraigSavePattern2( Ivy_FraigMan_t * p ) +{ + Ivy_Obj_t * pObj; + int i; + memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords ); +// Ivy_ManForEachPi( p->pManFraig, pObj, i ) + Vec_PtrForEachEntry( p->vPiVars, pObj, i ) + if ( p->pSat->model.ptr[Ivy_ObjSatNum(pObj)] == l_True ) +// Ivy_InfoSetBit( p->pPatWords, i ); + Ivy_InfoSetBit( p->pPatWords, pObj->Id - 1 ); +} + +/**Function************************************************************* + + Synopsis [Copy pattern from the solver into the internal storage.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_FraigSavePattern3( Ivy_FraigMan_t * p ) +{ + Ivy_Obj_t * pObj; + int i; + for ( i = 0; i < p->nPatWords; i++ ) + p->pPatWords[i] = Ivy_ObjRandomSim(); + Vec_PtrForEachEntry( p->vPiVars, pObj, i ) + if ( Ivy_InfoHasBit( p->pPatWords, pObj->Id - 1 ) ^ (p->pSat->model.ptr[Ivy_ObjSatNum(pObj)] == l_True) ) + Ivy_InfoXorBit( p->pPatWords, pObj->Id - 1 ); } /**Function************************************************************* + Synopsis [Returns 1 if the one of the output is already non-constant 0.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ivy_FraigCheckOutputSims( Ivy_FraigMan_t * p ) +{ + Ivy_Obj_t * pObj; + int i; + Ivy_ManForEachPo( p->pManAig, pObj, i ) + if ( !Ivy_NodeHasZeroSim( p, Ivy_ObjFanin0(pObj) ) ) + return 1; + return 0; +} + +/**Function************************************************************* + Synopsis [Stops the fraiging manager.] Description [] @@ -878,21 +1265,127 @@ void Ivy_FraigPrintSimClasses( Ivy_Fraig_t * p ) SeeAlso [] ***********************************************************************/ -void Ivy_FraigSimulate( Ivy_Fraig_t * p ) +void Ivy_FraigSimulate( Ivy_FraigMan_t * p ) { int nChanges, nClasses; + // start the classes Ivy_FraigAssignRandom( p ); Ivy_FraigSimulateOne( p ); Ivy_FraigCreateClasses( p ); -//printf( "Starting classes = %5d.\n", p->nClasses ); +//printf( "Starting classes = %5d. Pairs = %6d.\n", p->lClasses.nItems, Ivy_FraigCountPairsClasses(p) ); + // refine classes by walking 0/1 patterns + Ivy_FraigSavePattern0( p ); + Ivy_FraigAssignDist1( p, p->pPatWords ); + Ivy_FraigSimulateOne( p ); + nChanges = Ivy_FraigRefineClasses( p ); +//printf( "Refined classes = %5d. Changes = %4d. Pairs = %6d.\n", p->lClasses.nItems, nChanges, Ivy_FraigCountPairsClasses(p) ); + Ivy_FraigSavePattern1( p ); + Ivy_FraigAssignDist1( p, p->pPatWords ); + Ivy_FraigSimulateOne( p ); + nChanges = Ivy_FraigRefineClasses( p ); +//printf( "Refined classes = %5d. Changes = %4d. Pairs = %6d.\n", p->lClasses.nItems, nChanges, Ivy_FraigCountPairsClasses(p) ); + // refine classes by random simulation do { Ivy_FraigAssignRandom( p ); Ivy_FraigSimulateOne( p ); - nClasses = p->nClasses; + nClasses = p->lClasses.nItems; nChanges = Ivy_FraigRefineClasses( p ); -//printf( "Refined classes = %5d. Changes = %4d.\n", p->nClasses, nChanges ); +//printf( "Refined classes = %5d. Changes = %4d. Pairs = %6d.\n", p->lClasses.nItems, nChanges, Ivy_FraigCountPairsClasses(p) ); } while ( (double)nChanges / nClasses > p->pParams->SimSatur ); // 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" ); +} + + + +/**Function************************************************************* + + Synopsis [Cleans pattern scores.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_FraigCleanPatScores( Ivy_FraigMan_t * p ) +{ + int i, nLimit = p->nSimWords * 32; + for ( i = 0; i < nLimit; i++ ) + p->pPatScores[i] = 0; +} + +/**Function************************************************************* + + Synopsis [Adds to pattern scores.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_FraigAddToPatScores( Ivy_FraigMan_t * p, Ivy_Obj_t * pClass, Ivy_Obj_t * pClassNew ) +{ + Ivy_FraigSim_t * pSims0, * pSims1; + unsigned uDiff; + int i, w; + // get hold of the simulation information + pSims0 = Ivy_ObjSim(pClass); + pSims1 = Ivy_ObjSim(pClassNew); + // iterate through the differences and record the score + for ( w = 0; w < p->nSimWords; w++ ) + { + uDiff = pSims0->pData[w] ^ pSims1->pData[w]; + if ( uDiff == 0 ) + continue; + for ( i = 0; i < 32; i++ ) + if ( uDiff & ( 1 << i ) ) + p->pPatScores[w*32+i]++; + } +} + +/**Function************************************************************* + + Synopsis [Selects the best pattern.] + + Description [Returns 1 if such pattern is found.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ivy_FraigSelectBestPat( Ivy_FraigMan_t * p ) +{ + Ivy_FraigSim_t * pSims; + Ivy_Obj_t * pObj; + int i, nLimit = p->nSimWords * 32, MaxScore = 0, BestPat = -1; + for ( i = 1; i < nLimit; i++ ) + { + if ( MaxScore < p->pPatScores[i] ) + { + MaxScore = p->pPatScores[i]; + BestPat = i; + } + } + if ( MaxScore == 0 ) + return 0; +// if ( MaxScore > p->pParams->MaxScore ) +// printf( "Max score is %3d. ", MaxScore ); + // copy the best pattern into the selected pattern + memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords ); + Ivy_ManForEachPi( p->pManAig, pObj, i ) + { + pSims = Ivy_ObjSim(pObj); + if ( Ivy_InfoHasBit(pSims->pData, BestPat) ) + Ivy_InfoSetBit(p->pPatWords, i); + } + return MaxScore; } /**Function************************************************************* @@ -906,19 +1399,158 @@ void Ivy_FraigSimulate( Ivy_Fraig_t * p ) SeeAlso [] ***********************************************************************/ -void Ivy_FraigResimulate( Ivy_Fraig_t * p ) +void Ivy_FraigResimulate( Ivy_FraigMan_t * p ) { int nChanges; Ivy_FraigAssignDist1( p, p->pPatWords ); Ivy_FraigSimulateOne( p ); + if ( p->pParams->fPatScores ) + Ivy_FraigCleanPatScores( p ); nChanges = Ivy_FraigRefineClasses( p ); + if ( nChanges < 1 ) + printf( "Error: A counter-example did not refine classes!\n" ); assert( nChanges >= 1 ); -//printf( "Refined classes! = %5d. Changes = %4d.\n", p->nClasses, nChanges ); +//printf( "Refined classes! = %5d. Changes = %4d.\n", p->lClasses.nItems, nChanges ); + + if ( !p->pParams->fPatScores ) + return; + + // perform additional simulation using dist1 patterns derived from successful patterns + while ( Ivy_FraigSelectBestPat(p) > p->pParams->MaxScore ) + { + Ivy_FraigAssignDist1( p, p->pPatWords ); + Ivy_FraigSimulateOne( p ); + Ivy_FraigCleanPatScores( p ); + nChanges = Ivy_FraigRefineClasses( p ); +//printf( "Refined class!!! = %5d. Changes = %4d. Pairs = %6d.\n", p->lClasses.nItems, nChanges, Ivy_FraigCountPairsClasses(p) ); + if ( nChanges == 0 ) + break; + } } /**Function************************************************************* + Synopsis [Reports the status of the miter.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ivy_FraigMiterStatus( Ivy_FraigMan_t * p ) +{ + Ivy_Obj_t * pObj, * pObjNew; + int i, CountConst0 = 0, CountNonConst0 = 0, CountUndecided = 0; + Ivy_ManForEachPo( p->pManAig, pObj, i ) + { + pObjNew = Ivy_ObjChild0Equiv(pObj); + // check if the output is constant 1 + if ( pObjNew == p->pManFraig->pConst1 ) + { + CountNonConst0++; + continue; + } + // check if the output is constant 0 + if ( pObjNew == Ivy_Not(p->pManFraig->pConst1) ) + { + CountConst0++; + continue; + } + // check if the output can be constant 0 + if ( Ivy_Regular(pObjNew)->fPhase != (unsigned)Ivy_IsComplement(pObjNew) ) + { + CountNonConst0++; + continue; + } + CountUndecided++; + } + if ( p->pParams->fVerbose ) + { + printf( "Miter has %d outputs. ", Ivy_ManPoNum(p->pManAig) ); + printf( "Const0 = %d. ", CountConst0 ); + printf( "NonConst0 = %d. ", CountNonConst0 ); + printf( "Undecided = %d. ", CountUndecided ); + printf( "\n" ); + } + return 1; +} + +/**Function************************************************************* + + Synopsis [Works on the miter.] + + Description [Tries to prove each output until encountering a sat output.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_FraigMiterProve( Ivy_FraigMan_t * p ) +{ + Ivy_Obj_t * pObj, * pObjNew; + int i, RetValue, clk = clock(); + int fVerbose = p->pParams->fVerbose; + Ivy_ManForEachPo( p->pManAig, pObj, i ) + { + if ( i && fVerbose ) + { + PRT( "Time", clock() -clk ); + } + pObjNew = Ivy_ObjChild0Equiv(pObj); + // check if the output is constant 1 + if ( pObjNew == p->pManFraig->pConst1 ) + { + if ( fVerbose ) + printf( "Output %2d (out of %2d) is constant 1. ", i, Ivy_ManPoNum(p->pManAig) ); + break; + } + // check if the output is constant 0 + if ( pObjNew == Ivy_Not(p->pManFraig->pConst1) ) + { + if ( fVerbose ) + printf( "Output %2d (out of %2d) is already constant 0. ", i, Ivy_ManPoNum(p->pManAig) ); + continue; + } + // check if the output can be constant 0 + if ( Ivy_Regular(pObjNew)->fPhase != (unsigned)Ivy_IsComplement(pObjNew) ) + { + if ( fVerbose ) + printf( "Output %2d (out of %2d) cannot be constant 0. ", i, Ivy_ManPoNum(p->pManAig) ); + break; + } + // try to prove the output constant 0 + RetValue = Ivy_FraigNodeIsConst( p, Ivy_Regular(pObjNew) ); + if ( RetValue == 1 ) // proved equivalent + { + if ( fVerbose ) + printf( "Output %2d (out of %2d) was proved constant 0. ", i, Ivy_ManPoNum(p->pManAig) ); + // set the constant miter + Ivy_ObjFanin0(pObj)->pEquiv = Ivy_NotCond( p->pManFraig->pConst1, !Ivy_IsComplement(pObj) ); + continue; + } + if ( RetValue == -1 ) // failed + { + if ( fVerbose ) + printf( "Output %2d (out of %2d) has timed out at %d backtracks. ", i, Ivy_ManPoNum(p->pManAig), p->pParams->nBTLimitMiter ); + continue; + } + // proved satisfiable + if ( fVerbose ) + printf( "Output %2d (out of %2d) was proved NOT a constant 0. ", i, Ivy_ManPoNum(p->pManAig) ); + break; + } + if ( fVerbose ) + { + PRT( "Time", clock() -clk ); + } +} + +/**Function************************************************************* + Synopsis [Performs fraiging for the internal nodes.] Description [] @@ -928,16 +1560,25 @@ void Ivy_FraigResimulate( Ivy_Fraig_t * p ) SeeAlso [] ***********************************************************************/ -void Ivy_FraigSweep( Ivy_Fraig_t * p ) +void Ivy_FraigSweep( Ivy_FraigMan_t * p ) { Ivy_Obj_t * pObj; - int i; -p->nClassesZero = Ivy_ObjIsConst1(p->pClassesHead) ? Ivy_FraigCountClassNodes(p->pClassesHead) : 0; -p->nClassesBeg = Ivy_FraigCountClasses(p); + int i, k = 0; +p->nClassesZero = Ivy_ObjIsConst1(p->lClasses.pHead) ? Ivy_FraigCountClassNodes(p->lClasses.pHead) : 0; +p->nClassesBeg = p->lClasses.nItems; // duplicate internal nodes + p->pProgress = Extra_ProgressBarStart( stdout, Ivy_ManNodeNum(p->pManAig) ); Ivy_ManForEachNode( p->pManAig, pObj, i ) + { + Extra_ProgressBarUpdate( p->pProgress, k++, NULL ); pObj->pEquiv = Ivy_FraigAnd( p, pObj ); -p->nClassesEnd = Ivy_FraigCountClasses(p); + } + Extra_ProgressBarStop( p->pProgress ); +p->nClassesEnd = p->lClasses.nItems; + // try to prove the outputs of the miter + p->nNodesMiter = Ivy_ManNodeNum(p->pManFraig); + Ivy_FraigMiterStatus( p ); + Ivy_FraigMiterProve( p ); // add the POs Ivy_ManForEachPo( p->pManAig, pObj, i ) Ivy_ObjCreatePo( p->pManFraig, Ivy_ObjChild0Equiv(pObj) ); @@ -953,6 +1594,9 @@ p->nClassesEnd = Ivy_FraigCountClasses(p); } // remove dangling nodes Ivy_ManCleanup( p->pManFraig ); + // clean up the class marks + Ivy_FraigForEachEquivClass( p->lClasses.pHead, pObj ) + pObj->fMarkA = 0; } /**Function************************************************************* @@ -966,7 +1610,7 @@ p->nClassesEnd = Ivy_FraigCountClasses(p); SeeAlso [] ***********************************************************************/ -Ivy_Obj_t * Ivy_FraigAnd( Ivy_Fraig_t * p, Ivy_Obj_t * pObjOld ) +Ivy_Obj_t * Ivy_FraigAnd( Ivy_FraigMan_t * p, Ivy_Obj_t * pObjOld ) { Ivy_Obj_t * pObjNew, * pFanin0New, * pFanin1New, * pObjReprNew; int RetValue; @@ -988,10 +1632,16 @@ Ivy_Obj_t * Ivy_FraigAnd( Ivy_Fraig_t * p, Ivy_Obj_t * pObjOld ) // if the fraiged nodes are the same return if ( Ivy_Regular(pObjNew) == Ivy_Regular(pObjReprNew) ) return pObjNew; + assert( Ivy_Regular(pObjNew) != Ivy_ManConst1(p->pManFraig) ); // they are different (the counter-example is in p->pPatWords) - RetValue = Ivy_FraigNodesAreEquiv( p, Ivy_Regular(pObjReprNew), Ivy_Regular(pObjNew), 1000 ); + RetValue = Ivy_FraigNodesAreEquiv( p, Ivy_Regular(pObjReprNew), Ivy_Regular(pObjNew) ); if ( RetValue == 1 ) // proved equivalent + { + // mark the class as proved + if ( Ivy_ObjClassNodeNext(pObjOld) == NULL ) + Ivy_ObjClassNodeRepr(pObjOld)->fMarkA = 1; return Ivy_NotCond( pObjReprNew, pObjOld->fPhase ^ Ivy_ObjClassNodeRepr(pObjOld)->fPhase ); + } if ( RetValue == -1 ) // failed return pObjNew; // simulate the counter-example and return the new node @@ -1001,29 +1651,25 @@ Ivy_Obj_t * Ivy_FraigAnd( Ivy_Fraig_t * p, Ivy_Obj_t * pObjOld ) /**Function************************************************************* - Synopsis [Copy pattern from the solver into the internal storage.] + Synopsis [Performs fraiging for one node.] - Description [] + Description [Returns the fraiged node.] SideEffects [] SeeAlso [] ***********************************************************************/ -void Ivy_FraigSavePattern( Ivy_Fraig_t * p ) +void Ivy_FraigCleanActivity( Ivy_FraigMan_t * p ) { - Ivy_Obj_t * pObj; + double * pActivity; int i; - memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords ); - Ivy_ManForEachPi( p->pManFraig, pObj, i ) - if ( p->pSat->model.ptr[Ivy_ObjSatNum(pObj)] == l_True ) - Ivy_InfoSetBit( p->pPatWords, i ); -/* - // print sat variables + pActivity = sat_solver_activity(p->pSat); for ( i = 0; i < p->nSatVars; i++ ) - printf( "%d=%d ", i, p->pSat->model.ptr[i] ); - printf( "\n" ); -*/ + { + pActivity[i] = 0.0; + sat_solver_order_update( p->pSat, i ); + } } /**Function************************************************************* @@ -1037,11 +1683,30 @@ void Ivy_FraigSavePattern( Ivy_Fraig_t * p ) SeeAlso [] ***********************************************************************/ -int Ivy_FraigNodesAreEquiv( Ivy_Fraig_t * p, Ivy_Obj_t * pOld, Ivy_Obj_t * pNew, int nBTLimit ) +void Ivy_FraigPrintActivity( Ivy_FraigMan_t * p ) { - int pLits[4], RetValue, RetValue1, clk, Counter; + double * pActivity; + int i; + pActivity = sat_solver_activity(p->pSat); + for ( i = 0; i < p->nSatVars; i++ ) + printf( "%d %.3f ", i, pActivity[i] ); + printf( "\n" ); +} + +/**Function************************************************************* + + Synopsis [Performs fraiging for one node.] + + Description [Returns the fraiged node.] + + SideEffects [] -// printf( "Trying to prove nodes %d and %d\n", pOld->Id, pNew->Id ); + SeeAlso [] + +***********************************************************************/ +int Ivy_FraigNodesAreEquiv( Ivy_FraigMan_t * p, Ivy_Obj_t * pOld, Ivy_Obj_t * pNew ) +{ + int pLits[4], RetValue, RetValue1, nBTLimit, clk; // make sure the nodes are not complemented assert( !Ivy_IsComplement(pNew) ); @@ -1051,9 +1716,13 @@ int Ivy_FraigNodesAreEquiv( Ivy_Fraig_t * p, Ivy_Obj_t * pOld, Ivy_Obj_t * pNew, // if at least one of the nodes is a failed node, perform adjustments: // if the backtrack limit is small, simply skip this node // if the backtrack limit is > 10, take the quare root of the limit + nBTLimit = p->pParams->nBTLimitNode; if ( nBTLimit > 0 && (pOld->fFailTfo || pNew->fFailTfo) ) { p->nSatFails++; + // fail immediately + return -1; + if ( nBTLimit <= 10 ) return -1; nBTLimit = (int)sqrt(nBTLimit); @@ -1071,25 +1740,19 @@ int Ivy_FraigNodesAreEquiv( Ivy_Fraig_t * p, Ivy_Obj_t * pOld, Ivy_Obj_t * pNew, // if the nodes do not have SAT variables, allocate them Ivy_FraigNodeAddToSolver( p, pOld, pNew ); - // prepare variable activity -clk = clock(); - Ivy_ManIncrementTravId( p->pManFraig ); - Counter = Ivy_FraigMarkConeSetActivity_rec( p, pOld, NULL, 0, NULL, 0 ); - Counter += Ivy_FraigMarkConeSetActivity_rec( p, pNew, NULL, 0, NULL, 0 ); -// printf( "%d ", Counter ); -p->timeTrav += clock() - clk; - - // solve under assumptions // A = 1; B = 0 OR A = 1; B = 1 clk = clock(); pLits[0] = toLitCond( Ivy_ObjSatNum(pOld), 0 ); pLits[1] = toLitCond( Ivy_ObjSatNum(pNew), pOld->fPhase == pNew->fPhase ); //Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 ); - RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2 ); + RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2, + nBTLimit, p->pParams->nInsLimitNode, + p->pParams->nBTLimitGlobal, p->pParams->nInsLimitGlobal ); p->timeSat += clock() - clk; if ( RetValue1 == l_False ) { +p->timeSatUnsat += clock() - clk; pLits[0] = lit_neg( pLits[0] ); pLits[1] = lit_neg( pLits[1] ); RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 ); @@ -1099,12 +1762,14 @@ p->timeSat += clock() - clk; } else if ( RetValue1 == l_True ) { +p->timeSatSat += clock() - clk; Ivy_FraigSavePattern( p ); p->nSatCallsSat++; return 0; } else // if ( RetValue1 == l_Undef ) { +p->timeSatFail += clock() - clk; // mark the node as the failed node if ( pOld != p->pManFraig->pConst1 ) pOld->fFailTfo = 1; @@ -1125,10 +1790,13 @@ p->timeSat += clock() - clk; clk = clock(); pLits[0] = toLitCond( Ivy_ObjSatNum(pOld), 1 ); pLits[1] = toLitCond( Ivy_ObjSatNum(pNew), pOld->fPhase ^ pNew->fPhase ); - RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2 ); + RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2, + nBTLimit, p->pParams->nInsLimitNode, + p->pParams->nBTLimitGlobal, p->pParams->nInsLimitGlobal ); p->timeSat += clock() - clk; if ( RetValue1 == l_False ) { +p->timeSatUnsat += clock() - clk; pLits[0] = lit_neg( pLits[0] ); pLits[1] = lit_neg( pLits[1] ); RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 ); @@ -1137,12 +1805,14 @@ p->timeSat += clock() - clk; } else if ( RetValue1 == l_True ) { +p->timeSatSat += clock() - clk; Ivy_FraigSavePattern( p ); p->nSatCallsSat++; return 0; } else // if ( RetValue1 == l_Undef ) { +p->timeSatFail += clock() - clk; // mark the node as the failed node pOld->fFailTfo = 1; pNew->fFailTfo = 1; @@ -1157,6 +1827,77 @@ p->timeSat += clock() - clk; /**Function************************************************************* + Synopsis [Performs fraiging for one node.] + + Description [Returns the fraiged node.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ivy_FraigNodeIsConst( Ivy_FraigMan_t * p, Ivy_Obj_t * pNew ) +{ + int pLits[2], RetValue1, RetValue, clk; + + // make sure the nodes are not complemented + assert( !Ivy_IsComplement(pNew) ); + assert( pNew != p->pManFraig->pConst1 ); + p->nSatCalls++; + + // make sure the solver is allocated and has enough variables + if ( p->pSat == NULL ) + { + p->pSat = sat_solver_new(); + p->nSatVars = 1; + sat_solver_setnvars( p->pSat, 1000 ); + } + + // if the nodes do not have SAT variables, allocate them + Ivy_FraigNodeAddToSolver( p, NULL, pNew ); + + // prepare variable activity + Ivy_FraigMarkConeSetActivity( p, NULL, pNew ); + + // solve under assumptions +clk = clock(); + pLits[0] = toLitCond( Ivy_ObjSatNum(pNew), pNew->fPhase ); + RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 1, + p->pParams->nBTLimitMiter, p->pParams->nInsLimitMiter, + p->pParams->nBTLimitGlobal, p->pParams->nInsLimitGlobal ); +p->timeSat += clock() - clk; + if ( RetValue1 == l_False ) + { +p->timeSatUnsat += clock() - clk; + pLits[0] = lit_neg( pLits[0] ); + RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 1 ); + assert( RetValue ); + // continue solving the other implication + p->nSatCallsUnsat++; + } + else if ( RetValue1 == l_True ) + { +p->timeSatSat += clock() - clk; + Ivy_FraigSavePattern( p ); + p->nSatCallsSat++; + return 0; + } + else // if ( RetValue1 == l_Undef ) + { +p->timeSatFail += clock() - clk; + // mark the node as the failed node + pNew->fFailTfo = 1; + p->nSatFailsReal++; + return -1; + } + + // return SAT proof + p->nSatProof++; + return 1; +} + +/**Function************************************************************* + Synopsis [Addes clauses to the solver.] Description [] @@ -1166,7 +1907,7 @@ p->timeSat += clock() - clk; SeeAlso [] ***********************************************************************/ -void Ivy_FraigAddClausesMux( Ivy_Fraig_t * p, Ivy_Obj_t * pNode ) +void Ivy_FraigAddClausesMux( Ivy_FraigMan_t * p, Ivy_Obj_t * pNode ) { Ivy_Obj_t * pNodeI, * pNodeT, * pNodeE; int pLits[4], RetValue, VarF, VarI, VarT, VarE, fCompT, fCompE; @@ -1249,7 +1990,7 @@ void Ivy_FraigAddClausesMux( Ivy_Fraig_t * p, Ivy_Obj_t * pNode ) SeeAlso [] ***********************************************************************/ -void Ivy_FraigAddClausesSuper( Ivy_Fraig_t * p, Ivy_Obj_t * pNode, Vec_Ptr_t * vSuper ) +void Ivy_FraigAddClausesSuper( Ivy_FraigMan_t * p, Ivy_Obj_t * pNode, Vec_Ptr_t * vSuper ) { Ivy_Obj_t * pFanin; int * pLits, nLits, RetValue, i; @@ -1333,7 +2074,7 @@ Vec_Ptr_t * Ivy_FraigCollectSuper( Ivy_Obj_t * pObj, int fUseMuxes ) SeeAlso [] ***********************************************************************/ -void Ivy_FraigObjAddToFrontier( Ivy_Fraig_t * p, Ivy_Obj_t * pObj, Vec_Ptr_t * vFrontier ) +void Ivy_FraigObjAddToFrontier( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj, Vec_Ptr_t * vFrontier ) { assert( !Ivy_IsComplement(pObj) ); if ( Ivy_ObjSatNum(pObj) ) @@ -1359,18 +2100,19 @@ void Ivy_FraigObjAddToFrontier( Ivy_Fraig_t * p, Ivy_Obj_t * pObj, Vec_Ptr_t * v SeeAlso [] ***********************************************************************/ -void Ivy_FraigNodeAddToSolver( Ivy_Fraig_t * p, Ivy_Obj_t * pOld, Ivy_Obj_t * pNew ) -{ +void Ivy_FraigNodeAddToSolver( Ivy_FraigMan_t * p, Ivy_Obj_t * pOld, Ivy_Obj_t * pNew ) +{ Vec_Ptr_t * vFrontier, * vFanins; Ivy_Obj_t * pNode, * pFanin; int i, k, fUseMuxes = 1; + assert( pOld || pNew ); // quit if CNF is ready - if ( Ivy_ObjFaninVec(pOld) && Ivy_ObjFaninVec(pNew) ) + if ( (!pOld || Ivy_ObjFaninVec(pOld)) && (!pNew || Ivy_ObjFaninVec(pNew)) ) return; // start the frontier vFrontier = Vec_PtrAlloc( 100 ); - Ivy_FraigObjAddToFrontier( p, pOld, vFrontier ); - Ivy_FraigObjAddToFrontier( p, pNew, vFrontier ); + if ( pOld ) Ivy_FraigObjAddToFrontier( p, pOld, vFrontier ); + if ( pNew ) Ivy_FraigObjAddToFrontier( p, pNew, vFrontier ); // explore nodes in the frontier Vec_PtrForEachEntry( vFrontier, pNode, i ) { @@ -1412,7 +2154,7 @@ void Ivy_FraigNodeAddToSolver( Ivy_Fraig_t * p, Ivy_Obj_t * pOld, Ivy_Obj_t * pN SeeAlso [] ***********************************************************************/ -int Ivy_FraigMarkConeSetActivity_rec( Ivy_Fraig_t * p, Ivy_Obj_t * pObj, int * pTravIds, int TravId, double * pFactors, int LevelMax ) +int Ivy_FraigMarkConeSetActivity_rec( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj, double * pActivity, int LevelMax, Vec_Ptr_t * vPiVars ) { Vec_Ptr_t * vFanins; Ivy_Obj_t * pFanin; @@ -1421,21 +2163,74 @@ int Ivy_FraigMarkConeSetActivity_rec( Ivy_Fraig_t * p, Ivy_Obj_t * pObj, int * p if ( Ivy_ObjIsConst1(pObj) ) return 0; assert( Ivy_ObjSatNum(pObj) ); -// if ( pTravIds[Ivy_ObjSatNum(pObj)] == TravId ) -// return; -// pTravIds[Ivy_ObjSatNum(pObj)] = TravId; -// pFactors[Ivy_ObjSatNum(pObj)] = pow( 0.97, LevelMax - pObj->Level ); if ( Ivy_ObjIsTravIdCurrent(p->pManFraig, pObj) ) return 0; Ivy_ObjSetTravIdCurrent(p->pManFraig, pObj); + + // 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 ); return 0; + } + // explore the fanins vFanins = Ivy_ObjFaninVec( pObj ); Counter = 1; Vec_PtrForEachEntry( vFanins, pFanin, i ) - Counter += Ivy_FraigMarkConeSetActivity_rec( p, Ivy_Regular(pFanin), pTravIds, TravId, pFactors, LevelMax ); + 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; +} + +/**Function************************************************************* + + Synopsis [Performs fraiging for one node.] + + Description [Returns the fraiged node.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ivy_FraigMarkConeSetActivity( Ivy_FraigMan_t * p, Ivy_Obj_t * pOld, Ivy_Obj_t * pNew ) +{ + int clk, LevelMax, Counter; + assert( pOld || pNew ); +clk = clock(); + Vec_PtrClear( p->vPiVars ); + 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 ); +//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/satMem.c b/src/temp/ivy/satMem.c new file mode 100644 index 00000000..bb234f66 --- /dev/null +++ b/src/temp/ivy/satMem.c @@ -0,0 +1,527 @@ +/**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 new file mode 100644 index 00000000..5c5ddd9c --- /dev/null +++ b/src/temp/ivy/satMem.h @@ -0,0 +1,78 @@ +/**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 index b8248df8..38e73c7d 100644 --- a/src/temp/ivy/satSolver.c +++ b/src/temp/ivy/satSolver.c @@ -26,6 +26,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "satSolver.h" +//#define ASAT_USE_SYSTEM_MEMORY_MANAGEMENT + //================================================================================================= // Debug: @@ -142,6 +144,7 @@ static inline void order_unassigned(sat_solver* s, int v) // undoorder orderpos[v] = veci_size(&s->order); veci_push(&s->order,v); order_update(s,v); +//printf( "+%d ", v ); } } @@ -202,6 +205,7 @@ static int order_select(sat_solver* s, float random_var_freq) // selectvar orderpos[heap[i]] = i; } +//printf( "-%d ", next ); if (values[next] == l_Undef) return next; } @@ -209,6 +213,21 @@ static int order_select(sat_solver* s, float random_var_freq) // selectvar 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: @@ -232,6 +251,18 @@ static inline void act_var_bump(sat_solver* s, int 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) { @@ -253,6 +284,7 @@ static inline void act_clause_bump(sat_solver* s, clause *c) { 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: @@ -268,7 +300,13 @@ static clause* clause_new(sat_solver* s, lit* begin, lit* end, int learnt) assert(end - begin > 1); assert(learnt >= 0 && learnt < 2); size = end - begin; - c = (clause*)malloc(sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float)); +// 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); @@ -317,7 +355,11 @@ static void clause_remove(sat_solver* s, clause* c) 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 } @@ -833,6 +875,16 @@ static lbool sat_solver_search(sat_solver* s, int nof_conflicts, int nof_learnts 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); @@ -931,18 +983,27 @@ sat_solver* sat_solver_new(void) 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); @@ -1065,14 +1126,26 @@ bool sat_solver_simplify(sat_solver* s) } -int sat_solver_solve(sat_solver* s, lit* begin, lit* end) +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)]){ @@ -1117,6 +1190,18 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end) 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"); diff --git a/src/temp/ivy/satSolver.h b/src/temp/ivy/satSolver.h index 401a28e7..a7ace8ed 100644 --- a/src/temp/ivy/satSolver.h +++ b/src/temp/ivy/satSolver.h @@ -27,6 +27,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #endif #include "satVec.h" +#include "satMem.h" //================================================================================================= // Simple types: @@ -70,7 +71,7 @@ extern void sat_solver_delete(sat_solver* s); extern bool sat_solver_addclause(sat_solver* s, lit* begin, lit* end); extern bool sat_solver_simplify(sat_solver* s); -extern int sat_solver_solve(sat_solver* s, lit* begin, lit* end); +extern int sat_solver_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); @@ -78,6 +79,13 @@ 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; @@ -136,6 +144,11 @@ struct sat_solver_t 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 |