diff options
38 files changed, 5351 insertions, 73 deletions
@@ -1006,7 +1006,7 @@ SOURCE=.\src\sat\msat\msatMem.c # End Source File # Begin Source File -SOURCE=.\src\sat\msat\msatOrderJ.c +SOURCE=.\src\sat\msat\msatOrderH.c # End Source File # Begin Source File @@ -1762,6 +1762,10 @@ SOURCE=.\src\misc\vec\vec.h # End Source File # Begin Source File +SOURCE=.\src\misc\vec\vecFlt.h +# End Source File +# Begin Source File + SOURCE=.\src\misc\vec\vecInt.h # End Source File # Begin Source File @@ -2054,6 +2058,10 @@ SOURCE=.\src\temp\ivy\ivyFastMap.c # End Source File # Begin Source File +SOURCE=.\src\temp\ivy\ivyFraig.c +# End Source File +# Begin Source File + SOURCE=.\src\temp\ivy\ivyHaig.c # End Source File # Begin Source File @@ -2104,6 +2112,22 @@ SOURCE=.\src\temp\ivy\ivyTable.c SOURCE=.\src\temp\ivy\ivyUtil.c # End Source File +# Begin Source File + +SOURCE=.\src\temp\ivy\satSolver.c +# End Source File +# Begin Source File + +SOURCE=.\src\temp\ivy\satSolver.h +# End Source File +# Begin Source File + +SOURCE=.\src\temp\ivy\satUtil.c +# End Source File +# Begin Source File + +SOURCE=.\src\temp\ivy\satVec.h +# End Source File # End Group # Begin Group "player" @@ -2,8 +2,8 @@ #set check # checks intermediate networks #set checkfio # prints warnings when fanins/fanouts are duplicated #set checkread # checks new networks after reading from file -set backup # saves backup networks retrived by "undo" and "recall" -set savesteps 1 # sets the maximum number of backup networks to save +#set backup # saves backup networks retrived by "undo" and "recall" +#set savesteps 1 # sets the maximum number of backup networks to save set progressbar # display the progress bar # program names for internal calls @@ -99,6 +99,8 @@ alias src_rws "st; rw -l; rs -K 6 -N 2 -l; rwz -l; rs -K 9 -N 2 -l; rwz -l; alias compress2rs "b -l; rs -K 6 -l; rw -l; rs -K 6 -N 2 -l; rf -l; rs -K 8 -l; b -l; rs -K 8 -N 2 -l; rw -l; rs -K 10 -l; rwz -l; rs -K 10 -N 2 -l; b -l; rs -K 12 -l; rfz -l; rs -K 12 -N 2 -l; rwz -l; b -l" # temporaries -alias test "rvl th/lib.v; rvv th/t2.v" +#alias test "rvl th/lib.v; rvv th/t2.v" +alias test "so c/pure_sat/test.c" + diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h index a921081b..c4dbb52f 100644 --- a/src/base/abc/abc.h +++ b/src/base/abc/abc.h @@ -516,7 +516,7 @@ extern bool Abc_NtkCheck( Abc_Ntk_t * pNtk ); extern bool Abc_NtkCheckRead( Abc_Ntk_t * pNtk ); extern bool Abc_NtkDoCheck( Abc_Ntk_t * pNtk ); extern bool Abc_NtkCheckObj( Abc_Ntk_t * pNtk, Abc_Obj_t * pObj ); -extern bool Abc_NtkCompareSignals( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb ); +extern bool Abc_NtkCompareSignals( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fOnlyPis, int fComb ); /*=== abcCollapse.c ==========================================================*/ extern Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, int fReorder, int fVerbose ); /*=== abcCut.c ==========================================================*/ @@ -589,7 +589,6 @@ extern Abc_Ntk_t * Abc_NtkMiterQuantify( Abc_Ntk_t * pNtk, int In, int fE extern Abc_Ntk_t * Abc_NtkMiterQuantifyPis( Abc_Ntk_t * pNtk ); extern int Abc_NtkMiterIsConstant( Abc_Ntk_t * pMiter ); extern void Abc_NtkMiterReport( Abc_Ntk_t * pMiter ); -extern int Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 ); extern Abc_Ntk_t * Abc_NtkFrames( Abc_Ntk_t * pNtk, int nFrames, int fInitial ); /*=== abcObj.c ==========================================================*/ extern Abc_Obj_t * Abc_ObjAlloc( Abc_Ntk_t * pNtk, Abc_ObjType_t Type ); @@ -743,7 +742,7 @@ extern char * Abc_SopFromTruthHex( char * pTruth ); /*=== abcStrash.c ==========================================================*/ extern Abc_Ntk_t * Abc_NtkStrash( Abc_Ntk_t * pNtk, bool fAllNodes, bool fCleanup ); extern Abc_Obj_t * Abc_NodeStrash( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode ); -extern int Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 ); +extern int Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fAddPos ); extern Abc_Ntk_t * Abc_NtkTopmost( Abc_Ntk_t * pNtk, int nLevels ); /*=== abcSweep.c ==========================================================*/ extern int Abc_NtkSweep( Abc_Ntk_t * pNtk, int fVerbose ); diff --git a/src/base/abc/abcCheck.c b/src/base/abc/abcCheck.c index 0156b331..118ea291 100644 --- a/src/base/abc/abcCheck.c +++ b/src/base/abc/abcCheck.c @@ -709,16 +709,19 @@ bool Abc_NtkCompareBoxes( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb ) SeeAlso [] ***********************************************************************/ -bool Abc_NtkCompareSignals( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb ) +bool Abc_NtkCompareSignals( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fOnlyPis, int fComb ) { Abc_NtkOrderObjsByName( pNtk1, fComb ); Abc_NtkOrderObjsByName( pNtk2, fComb ); - if ( !Abc_NtkCompareBoxes( pNtk1, pNtk2, fComb ) ) - return 0; if ( !Abc_NtkComparePis( pNtk1, pNtk2, fComb ) ) return 0; - if ( !Abc_NtkComparePos( pNtk1, pNtk2, fComb ) ) - return 0; + if ( !fOnlyPis ) + { + if ( !Abc_NtkCompareBoxes( pNtk1, pNtk2, fComb ) ) + return 0; + if ( !Abc_NtkComparePos( pNtk1, pNtk2, fComb ) ) + return 0; + } return 1; } diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 4154fe53..b0ccae3a 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -71,6 +71,7 @@ static int Abc_CommandLogic ( Abc_Frame_t * pAbc, int argc, char ** arg static int Abc_CommandMiter ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandDemiter ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandOrPos ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAppend ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandFrames ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandSop ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandBdd ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -96,6 +97,7 @@ 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_CommandIFraig ( 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 ); @@ -196,6 +198,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Various", "miter", Abc_CommandMiter, 1 ); Cmd_CommandAdd( pAbc, "Various", "demiter", Abc_CommandDemiter, 1 ); Cmd_CommandAdd( pAbc, "Various", "orpos", Abc_CommandOrPos, 1 ); + Cmd_CommandAdd( pAbc, "Various", "append", Abc_CommandAppend, 1 ); Cmd_CommandAdd( pAbc, "Various", "frames", Abc_CommandFrames, 1 ); Cmd_CommandAdd( pAbc, "Various", "sop", Abc_CommandSop, 0 ); Cmd_CommandAdd( pAbc, "Various", "bdd", Abc_CommandBdd, 0 ); @@ -221,6 +224,7 @@ 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", "ifraig", Abc_CommandIFraig, 1 ); Cmd_CommandAdd( pAbc, "New AIG", "haig", Abc_CommandHaig, 1 ); Cmd_CommandAdd( pAbc, "New AIG", "mini", Abc_CommandMini, 1 ); @@ -3276,6 +3280,105 @@ usage: SeeAlso [] ***********************************************************************/ +int Abc_CommandAppend( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr, * pFile; + Abc_Ntk_t * pNtk, * pNtk2; + char * FileName; + int fComb; + int c; + + pNtk = Abc_FrameReadNtk(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "ch" ) ) != EOF ) + { + switch ( c ) + { + case 'c': + fComb ^= 1; + break; + default: + goto usage; + } + } + + // get the second network + if ( argc != globalUtilOptind + 1 ) + { + fprintf( pErr, "The network to append is not given.\n" ); + return 1; + } + + if ( !Abc_NtkIsStrash(pNtk) ) + { + fprintf( pErr, "The base network should be strashed for the appending to work.\n" ); + return 1; + } + + // get the input file name + FileName = argv[globalUtilOptind]; + if ( (pFile = fopen( FileName, "r" )) == NULL ) + { + fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName ); + if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".eqn", ".bench" ) ) + fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName ); + fprintf( pAbc->Err, "\n" ); + return 1; + } + fclose( pFile ); + + // read the second network + pNtk2 = Io_Read( FileName, 1 ); + if ( pNtk2 == NULL ) + { + fprintf( pAbc->Err, "Reading network from file has failed.\n" ); + return 1; + } + + // check if the second network is combinational + if ( Abc_NtkLatchNum(pNtk2) ) + { + fprintf( pErr, "The second network has latches. Appending does not work for such networks.\n" ); + return 1; + } + + // get the new network + if ( !Abc_NtkAppend( pNtk, pNtk2, 1 ) ) + { + Abc_NtkDelete( pNtk2 ); + fprintf( pErr, "Appending the networks failed.\n" ); + return 1; + } + Abc_NtkDelete( pNtk2 ); + + // replace the current network +// Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); + return 0; + +usage: + fprintf( pErr, "usage: append [-h] <file>\n" ); + fprintf( pErr, "\t appends a combinational network on top of the current network\n" ); +// fprintf( pErr, "\t-c : computes combinational miter (latches as POs) [default = %s]\n", fComb? "yes": "no" ); + fprintf( pErr, "\t-h : print the command usage\n"); + fprintf( pErr, "\t<file> : file name with the second network\n"); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ int Abc_CommandFrames( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; @@ -4810,13 +4913,13 @@ int Abc_CommandXyz( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "Only works for strashed networks.\n" ); return 1; } - +/* if ( nLutMax < 2 || nLutMax > 12 || nPlaMax < 8 || nPlaMax > 128 ) { fprintf( pErr, "Incorrect LUT/PLA parameters.\n" ); return 1; } - +*/ // run the command // pNtkRes = Abc_NtkXyz( pNtk, nPlaMax, 1, 0, fInvs, fVerbose ); pNtkRes = Abc_NtkPlayer( pNtk, nLutMax, nPlaMax, RankCost, fFastMode, fRewriting, fSynthesis, fVerbose ); @@ -5338,6 +5441,79 @@ usage: SeeAlso [] ***********************************************************************/ +int Abc_CommandIFraig( 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_NtkIvyFraig( 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_NtkIvyFraig( 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: ifraig [-h]\n" ); + fprintf( pErr, "\t performs fraiging 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"); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ int Abc_CommandHaig( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; diff --git a/src/base/abci/abcFpga.c b/src/base/abci/abcFpga.c index e5286487..80238b48 100644 --- a/src/base/abci/abcFpga.c +++ b/src/base/abci/abcFpga.c @@ -209,7 +209,8 @@ Abc_Ntk_t * Abc_NtkFromFpga( Fpga_Man_t * pMan, Abc_Ntk_t * pNtk ) Abc_NtkForEachCi( pNtk, pNode, i ) Fpga_NodeSetData0( Fpga_ManReadInputs(pMan)[i], (char *)pNode->pCopy ); // set the constant node - Fpga_NodeSetData0( Fpga_ManReadConst1(pMan), (char *)Abc_NodeCreateConst1(pNtkNew) ); +// if ( Fpga_NodeReadRefs(Fpga_ManReadConst1(pMan)) > 0 ) + Fpga_NodeSetData0( Fpga_ManReadConst1(pMan), (char *)Abc_NodeCreateConst1(pNtkNew) ); // process the nodes in topological order pProgress = Extra_ProgressBarStart( stdout, Abc_NtkCoNum(pNtk) ); Abc_NtkForEachCo( pNtk, pNode, i ) @@ -222,6 +223,10 @@ Abc_Ntk_t * Abc_NtkFromFpga( Fpga_Man_t * pMan, Abc_Ntk_t * pNtk ) Extra_ProgressBarStop( pProgress ); // finalize the new network Abc_NtkFinalize( pNtk, pNtkNew ); + // remove the constant node if not used + pNodeNew = (Abc_Obj_t *)Fpga_NodeReadData0(Fpga_ManReadConst1(pMan)); + if ( Abc_ObjFanoutNum(pNodeNew) == 0 ) + Abc_NtkDeleteObj( pNodeNew ); // decouple the PO driver nodes to reduce the number of levels nDupGates = Abc_NtkLogicMakeSimpleCos( pNtkNew, 1 ); // if ( nDupGates && Fpga_ManReadVerbose(pMan) ) diff --git a/src/base/abci/abcFraig.c b/src/base/abci/abcFraig.c index 778c8284..a4c44883 100644 --- a/src/base/abci/abcFraig.c +++ b/src/base/abci/abcFraig.c @@ -679,7 +679,7 @@ int Abc_NtkFraigStore( Abc_Ntk_t * pNtk ) { // add the new network to storage nAndsOld = Abc_NtkNodeNum( pStore ); - if ( !Abc_NtkAppend( pStore, pNtk ) ) + if ( !Abc_NtkAppend( pStore, pNtk, 0 ) ) { printf( "The current network cannot be appended to the stored network.\n" ); return 0; diff --git a/src/base/abci/abcIvy.c b/src/base/abci/abcIvy.c index 9793a4e2..3a5333f4 100644 --- a/src/base/abci/abcIvy.c +++ b/src/base/abci/abcIvy.c @@ -288,6 +288,31 @@ Abc_Ntk_t * Abc_NtkIvyRewriteSeq( Abc_Ntk_t * pNtk, int fUseZeroCost, int fVerbo SeeAlso [] ***********************************************************************/ +Abc_Ntk_t * Abc_NtkIvyResyn0( Abc_Ntk_t * pNtk, int fUpdateLevel, int fVerbose ) +{ + Abc_Ntk_t * pNtkAig; + Ivy_Man_t * pMan, * pTemp; + pMan = Abc_NtkIvyBefore( pNtk, 0, 0 ); + if ( pMan == NULL ) + return NULL; + pMan = Ivy_ManResyn0( pTemp = pMan, fUpdateLevel, fVerbose ); + 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_NtkIvyResyn( Abc_Ntk_t * pNtk, int fUpdateLevel, int fVerbose ) { Abc_Ntk_t * pNtkAig; @@ -313,6 +338,33 @@ Abc_Ntk_t * Abc_NtkIvyResyn( Abc_Ntk_t * pNtk, int fUpdateLevel, int fVerbose ) SeeAlso [] ***********************************************************************/ +Abc_Ntk_t * Abc_NtkIvyFraig( 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_FraigPerform( 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; @@ -538,12 +590,12 @@ Abc_Ntk_t * Abc_NtkFromAigSeq( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan, int fHaig if ( fHaig && pNode->pEquiv && Ivy_ObjRefs(pNode) > 0 ) { pFaninNew = Abc_EdgeToNode( pNtk, pNode->TravId ); - pFaninNew->fPhase = 0; +// pFaninNew->fPhase = 0; assert( !Ivy_IsComplement(pNode->pEquiv) ); for ( pTemp = pNode->pEquiv; pTemp != pNode; pTemp = Ivy_Regular(pTemp->pEquiv) ) { pFaninNew1 = Abc_EdgeToNode( pNtk, pTemp->TravId ); - pFaninNew1->fPhase = Ivy_IsComplement( pTemp->pEquiv ); +// pFaninNew1->fPhase = Ivy_IsComplement( pTemp->pEquiv ); pFaninNew->pData = pFaninNew1; pFaninNew = pFaninNew1; } diff --git a/src/base/abci/abcMiter.c b/src/base/abci/abcMiter.c index 64f414aa..0ee1e804 100644 --- a/src/base/abci/abcMiter.c +++ b/src/base/abci/abcMiter.c @@ -57,7 +57,7 @@ Abc_Ntk_t * Abc_NtkMiter( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb ) assert( Abc_NtkHasOnlyLatchBoxes(pNtk1) ); assert( Abc_NtkHasOnlyLatchBoxes(pNtk2) ); // check that the networks have the same PIs/POs/latches - if ( !Abc_NtkCompareSignals( pNtk1, pNtk2, fComb ) ) + if ( !Abc_NtkCompareSignals( pNtk1, pNtk2, 0, fComb ) ) return NULL; // make sure the circuits are strashed fRemove1 = (!Abc_NtkIsStrash(pNtk1)) && (pNtk1 = Abc_NtkStrash(pNtk1, 0, 0)); diff --git a/src/base/abci/abcProve.c b/src/base/abci/abcProve.c index 85a58c32..f3c1a825 100644 --- a/src/base/abci/abcProve.c +++ b/src/base/abci/abcProve.c @@ -122,8 +122,24 @@ int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, void * pPars ) { clk = clock(); Counter = (int)(pParams->nRewritingLimitStart * pow(pParams->nRewritingLimitMulti,nIter)); +// Counter = 1; while ( 1 ) { +/* + extern Abc_Ntk_t * Abc_NtkIvyResyn( Abc_Ntk_t * pNtk, int fUpdateLevel, int fVerbose ); + pNtk = Abc_NtkIvyResyn( pNtkTemp = pNtk, 0, 0 ); Abc_NtkDelete( pNtkTemp ); + if ( (RetValue = Abc_NtkMiterIsConstant(pNtk)) >= 0 ) + break; + if ( --Counter == 0 ) + break; +*/ +/* + Abc_NtkRewrite( pNtk, 0, 0, 0 ); + if ( (RetValue = Abc_NtkMiterIsConstant(pNtk)) >= 0 ) + break; + if ( --Counter == 0 ) + break; +*/ Abc_NtkRewrite( pNtk, 0, 0, 0 ); if ( (RetValue = Abc_NtkMiterIsConstant(pNtk)) >= 0 ) break; diff --git a/src/base/abci/abcSat.c b/src/base/abci/abcSat.c index 02bfca17..3e0d6ba0 100644 --- a/src/base/abci/abcSat.c +++ b/src/base/abci/abcSat.c @@ -429,7 +429,7 @@ int Abc_NtkMiterSatCreateInt( solver * pSat, Abc_Ntk_t * pNtk, int fJFront ) { Abc_Obj_t * pNode, * pFanin, * pNodeC, * pNodeT, * pNodeE; Vec_Ptr_t * vNodes, * vSuper; -// Vec_Int_t * vLevels; + Vec_Flt_t * vFactors; Vec_Int_t * vVars, * vFanio; Vec_Vec_t * vCircuit; int i, k, fUseMuxes = 1; @@ -588,6 +588,23 @@ int Abc_NtkMiterSatCreateInt( solver * pSat, Abc_Ntk_t * pNtk, int fJFront ) // Asat_JManStop( pSat ); // PRT( "Total", clock() - clk1 ); } + + Abc_NtkStartReverseLevels( pNtk ); + vFactors = Vec_FltStart( solver_nvars(pSat) ); + Abc_NtkForEachNode( pNtk, pNode, i ) + if ( pNode->fMarkA ) + Vec_FltWriteEntry( vFactors, (int)pNode->pCopy, (float)pow(0.97, Abc_NodeReadReverseLevel(pNode)) ); + Abc_NtkForEachCi( pNtk, pNode, i ) + if ( pNode->fMarkA ) + Vec_FltWriteEntry( vFactors, (int)pNode->pCopy, (float)pow(0.97, nLevelsMax+1) ); + // set the PI levels +// Abc_NtkForEachObj( pNtk, pNode, i ) +// if ( pNode->fMarkA ) +// printf( "(%d) %.3f ", Abc_NodeReadReverseLevel(pNode), Vec_FltEntry(vFactors, (int)pNode->pCopy) ); +// printf( "\n" ); + Asat_SolverSetFactors( pSat, Vec_FltReleaseArray(vFactors) ); + Vec_FltFree( vFactors ); + /* // create factors vLevels = Vec_IntStart( Vec_PtrSize(vNodes) ); // the reverse levels of the nodes diff --git a/src/base/abci/abcStrash.c b/src/base/abci/abcStrash.c index d00be668..a130c11f 100644 --- a/src/base/abci/abcStrash.c +++ b/src/base/abci/abcStrash.c @@ -144,7 +144,7 @@ Abc_Ntk_t * Abc_NtkStrash( Abc_Ntk_t * pNtk, bool fAllNodes, bool fCleanup ) SeeAlso [] ***********************************************************************/ -int Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 ) +int Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fAddPos ) { Abc_Obj_t * pObj; int i; @@ -158,7 +158,7 @@ int Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 ) } // check that the networks have the same PIs // reorder PIs of pNtk2 according to pNtk1 - if ( !Abc_NtkCompareSignals( pNtk1, pNtk2, 1 ) ) + if ( !Abc_NtkCompareSignals( pNtk1, pNtk2, 1, 1 ) ) return 0; // perform strashing Abc_NtkCleanCopy( pNtk2 ); @@ -170,6 +170,16 @@ int Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 ) else Abc_NtkForEachNode( pNtk2, pObj, i ) pObj->pCopy = Abc_AigAnd( pNtk1->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) ); + // add the COs of the second network + if ( fAddPos ) + { + Abc_NtkForEachPo( pNtk2, pObj, i ) + { + Abc_NtkDupObj( pNtk1, pObj, 0 ); + Abc_ObjAddFanin( pObj->pCopy, Abc_ObjChild0Copy(pObj) ); + Abc_ObjAssignName( pObj->pCopy, Abc_ObjName(pObj->pCopy), NULL ); + } + } // make sure that everything is okay if ( !Abc_NtkCheck( pNtk1 ) ) { diff --git a/src/map/fpga/fpga.h b/src/map/fpga/fpga.h index df4a9189..3ecdb44f 100644 --- a/src/map/fpga/fpga.h +++ b/src/map/fpga/fpga.h @@ -105,6 +105,7 @@ extern int Fpga_LibReadLutMax( Fpga_LutLib_t * pLib ); extern char * Fpga_NodeReadData0( Fpga_Node_t * p ); extern Fpga_Node_t * Fpga_NodeReadData1( Fpga_Node_t * p ); +extern int Fpga_NodeReadRefs( Fpga_Node_t * p ); extern int Fpga_NodeReadNum( Fpga_Node_t * p ); extern int Fpga_NodeReadLevel( Fpga_Node_t * p ); extern Fpga_Cut_t * Fpga_NodeReadCuts( Fpga_Node_t * p ); diff --git a/src/map/fpga/fpgaCreate.c b/src/map/fpga/fpgaCreate.c index 41bea4d0..479a4bdc 100644 --- a/src/map/fpga/fpgaCreate.c +++ b/src/map/fpga/fpgaCreate.c @@ -97,6 +97,7 @@ int Fpga_LibReadLutMax( Fpga_LutLib_t * pLib ) { return pLib->LutMa ***********************************************************************/ char * Fpga_NodeReadData0( Fpga_Node_t * p ) { return p->pData0; } Fpga_Node_t * Fpga_NodeReadData1( Fpga_Node_t * p ) { return p->pLevel; } +int Fpga_NodeReadRefs( Fpga_Node_t * p ) { return p->nRefs; } int Fpga_NodeReadNum( Fpga_Node_t * p ) { return p->Num; } int Fpga_NodeReadLevel( Fpga_Node_t * p ) { return Fpga_Regular(p)->Level; } Fpga_Cut_t * Fpga_NodeReadCuts( Fpga_Node_t * p ) { return p->pCuts; } diff --git a/src/sat/asat/added.c b/src/sat/asat/added.c index 100b823b..222693ad 100644 --- a/src/sat/asat/added.c +++ b/src/sat/asat/added.c @@ -220,7 +220,7 @@ void Asat_SolverSetPrefVars(solver * s, int * pPrefVars, int nPrefVars) SeeAlso [] ***********************************************************************/ -void Asat_SolverSetFactors(solver * s, int * pFactors) +void Asat_SolverSetFactors(solver * s, float * pFactors) { assert( s->factors == NULL ); s->factors = pFactors; diff --git a/src/sat/asat/solver.c b/src/sat/asat/solver.c index f2642c38..34b4d233 100644 --- a/src/sat/asat/solver.c +++ b/src/sat/asat/solver.c @@ -253,12 +253,11 @@ static inline void act_var_rescale(solver* s) { static inline void act_var_bump(solver* s, int v) { double* activity = s->activity; - if ((activity[v] += s->var_inc) > 1e100) -// if ((activity[v] += s->var_inc*s->factors[v]/100000000) > 1e100) + activity[v] += s->var_inc; +// activity[v] += s->var_inc * s->factors[v]; + if (activity[v] > 1e100) act_var_rescale(s); - //printf("bump %d %f\n", v-1, activity[v]); - if ( s->pJMan == NULL && s->orderpos[v] != -1 ) order_update(s,v); @@ -842,6 +841,7 @@ static lbool solver_search(solver* s, int nof_conflicts, int nof_learnts) int conflictC = 0; veci learnt_clause; + int i; assert(s->root_level == solver_dlevel(s)); @@ -851,6 +851,12 @@ static lbool solver_search(solver* s, int nof_conflicts, int nof_learnts) veci_resize(&s->model,0); veci_new(&learnt_clause); + // reset the activities + if ( s->factors ) + for ( i = 0; i < s->size; i++ ) + s->activity[i] = (double)s->factors[i]; +// s->activity[i] = 1.0; + for (;;){ clause* confl = solver_propagate(s); if (confl != 0){ diff --git a/src/sat/asat/solver.h b/src/sat/asat/solver.h index 7edfb537..7a5e5be6 100644 --- a/src/sat/asat/solver.h +++ b/src/sat/asat/solver.h @@ -89,7 +89,7 @@ extern void Asat_SolverWriteDimacs( solver * pSat, char * pFileName, int incrementVars); extern void Asat_SatPrintStats( FILE * pFile, solver * p ); extern void Asat_SolverSetPrefVars( solver * s, int * pPrefVars, int nPrefVars ); -extern void Asat_SolverSetFactors( solver * s, int * pFactors ); +extern void Asat_SolverSetFactors( solver * s, float * pFactors ); // J-frontier support extern Asat_JMan_t * Asat_JManStart( solver * pSat, void * vCircuit ); @@ -128,7 +128,7 @@ struct solver_t vec* wlists; // double* activity; // A heuristic measurement of the activity of a variable. - int * factors; // the factor of variable activity + float * factors; // the factor of variable activity lbool* assigns; // Current values of variables. int* orderpos; // Index in variable order. clause** reasons; // diff --git a/src/sat/asat_fixed/satSolver.c b/src/sat/asat_fixed/satSolver.c new file mode 100644 index 00000000..d3b99c9d --- /dev/null +++ b/src/sat/asat_fixed/satSolver.c @@ -0,0 +1,1191 @@ +/************************************************************************************************** +MiniSat -- Copyright (c) 2005, Niklas Sorensson +http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/ + +Permission is hereby granted, free of charge, to any person obtaining a copy of this software and +associated documentation files (the "Software"), to deal in the Software without restriction, +including without limitation the rights to use, copy, modify, merge, publish, distribute, +sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all copies or +substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT +NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, +DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT +OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +**************************************************************************************************/ +// Modified to compile with MS Visual Studio 6.0 by Alan Mishchenko + +#include <stdio.h> +#include <assert.h> +#include <math.h> + +#include "solver.h" + +//================================================================================================= +// Debug: + +//#define VERBOSEDEBUG + +// For derivation output (verbosity level 2) +#define L_IND "%-*d" +#define L_ind solver_dlevel(s)*3+3,solver_dlevel(s) +#define L_LIT "%sx%d" +#define L_lit(p) lit_sign(p)?"~":"", (lit_var(p)) + +// Just like 'assert()' but expression will be evaluated in the release version as well. +static inline void check(int expr) { assert(expr); } + +static void printlits(lit* begin, lit* end) +{ + int i; + for (i = 0; i < end - begin; i++) + printf(L_LIT" ",L_lit(begin[i])); +} + +//================================================================================================= +// Random numbers: + + +// Returns a random float 0 <= x < 1. Seed must never be 0. +static inline double drand(double* seed) { + int q; + *seed *= 1389796; + q = (int)(*seed / 2147483647); + *seed -= (double)q * 2147483647; + return *seed / 2147483647; } + + +// Returns a random integer 0 <= x < size. Seed must never be 0. +static inline int irand(double* seed, int size) { + return (int)(drand(seed) * size); } + + +//================================================================================================= +// Predeclarations: + +void sort(void** array, int size, int(*comp)(const void *, const void *)); + +//================================================================================================= +// Clause datatype + minor functions: + +struct clause_t +{ + int size_learnt; + lit lits[0]; +}; + +static inline int clause_size (clause* c) { return c->size_learnt >> 1; } +static inline lit* clause_begin (clause* c) { return c->lits; } +static inline int clause_learnt (clause* c) { return c->size_learnt & 1; } +static inline float clause_activity (clause* c) { return *((float*)&c->lits[c->size_learnt>>1]); } +static inline void clause_setactivity(clause* c, float a) { *((float*)&c->lits[c->size_learnt>>1]) = a; } + +//================================================================================================= +// Encode literals in clause pointers: + +clause* clause_from_lit (lit l) { return (clause*)((unsigned long)l + (unsigned long)l + 1); } +bool clause_is_lit (clause* c) { return ((unsigned long)c & 1); } +lit clause_read_lit (clause* c) { return (lit)((unsigned long)c >> 1); } + +//================================================================================================= +// Simple helpers: + +static inline int solver_dlevel(solver* s) { return veci_size(&s->trail_lim); } +static inline vecp* solver_read_wlist (solver* s, lit l){ return &s->wlists[l]; } +static inline void vecp_remove(vecp* v, void* e) +{ + void** ws = vecp_begin(v); + int j = 0; + + for (; ws[j] != e ; j++); + assert(j < vecp_size(v)); + for (; j < vecp_size(v)-1; j++) ws[j] = ws[j+1]; + vecp_resize(v,vecp_size(v)-1); +} + +//================================================================================================= +// Variable order functions: + +static inline void order_update(solver* s, int v) // updateorder +{ + int* orderpos = s->orderpos; + double* activity = s->activity; + int* heap = veci_begin(&s->order); + int i = orderpos[v]; + int x = heap[i]; + int parent = (i - 1) / 2; + + assert(s->orderpos[v] != -1); + + while (i != 0 && activity[x] > activity[heap[parent]]){ + heap[i] = heap[parent]; + orderpos[heap[i]] = i; + i = parent; + parent = (i - 1) / 2; + } + heap[i] = x; + orderpos[x] = i; +} + +static inline void order_assigned(solver* s, int v) +{ +} + +static inline void order_unassigned(solver* s, int v) // undoorder +{ + int* orderpos = s->orderpos; + if (orderpos[v] == -1){ + orderpos[v] = veci_size(&s->order); + veci_push(&s->order,v); + order_update(s,v); + } +} + +static int order_select(solver* s, float random_var_freq) // selectvar +{ + int* heap; + double* activity; + int* orderpos; + + lbool* values = s->assigns; + + // Random decision: + if (drand(&s->random_seed) < random_var_freq){ + int next = irand(&s->random_seed,s->size); + assert(next >= 0 && next < s->size); + if (values[next] == l_Undef) + return next; + } + + // Activity based decision: + + heap = veci_begin(&s->order); + activity = s->activity; + orderpos = s->orderpos; + + + while (veci_size(&s->order) > 0){ + int next = heap[0]; + int size = veci_size(&s->order)-1; + int x = heap[size]; + + veci_resize(&s->order,size); + + orderpos[next] = -1; + + if (size > 0){ + double act = activity[x]; + + int i = 0; + int child = 1; + + + while (child < size){ + if (child+1 < size && activity[heap[child]] < activity[heap[child+1]]) + child++; + + assert(child < size); + + if (act >= activity[heap[child]]) + break; + + heap[i] = heap[child]; + orderpos[heap[i]] = i; + i = child; + child = 2 * child + 1; + } + heap[i] = x; + orderpos[heap[i]] = i; + } + + if (values[next] == l_Undef) + return next; + } + + return var_Undef; +} + +//================================================================================================= +// Activity functions: + +static inline void act_var_rescale(solver* s) { + double* activity = s->activity; + int i; + for (i = 0; i < s->size; i++) + activity[i] *= 1e-100; + s->var_inc *= 1e-100; +} + +static inline void act_var_bump(solver* s, int v) { + double* activity = s->activity; + if ((activity[v] += s->var_inc) > 1e100) + act_var_rescale(s); + + //printf("bump %d %f\n", v-1, activity[v]); + + if (s->orderpos[v] != -1) + order_update(s,v); + +} + +static inline void act_var_decay(solver* s) { s->var_inc *= s->var_decay; } + +static inline void act_clause_rescale(solver* s) { + clause** cs = (clause**)vecp_begin(&s->learnts); + int i; + for (i = 0; i < vecp_size(&s->learnts); i++){ + float a = clause_activity(cs[i]); + clause_setactivity(cs[i], a * (float)1e-20); + } + s->cla_inc *= (float)1e-20; +} + + +static inline void act_clause_bump(solver* s, clause *c) { + float a = clause_activity(c) + s->cla_inc; + clause_setactivity(c,a); + if (a > 1e20) act_clause_rescale(s); +} + +static inline void act_clause_decay(solver* s) { s->cla_inc *= s->cla_decay; } + + +//================================================================================================= +// Clause functions: + +/* pre: size > 1 && no variable occurs twice + */ +static clause* clause_new(solver* s, lit* begin, lit* end, int learnt) +{ + int size; + clause* c; + int i; + + assert(end - begin > 1); + assert(learnt >= 0 && learnt < 2); + size = end - begin; + c = (clause*)malloc(sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float)); + c->size_learnt = (size << 1) | learnt; + assert(((unsigned int)c & 1) == 0); + + for (i = 0; i < size; i++) + c->lits[i] = begin[i]; + + if (learnt) + *((float*)&c->lits[size]) = 0.0; + + assert(begin[0] >= 0); + assert(begin[0] < s->size*2); + assert(begin[1] >= 0); + assert(begin[1] < s->size*2); + + assert(lit_neg(begin[0]) < s->size*2); + assert(lit_neg(begin[1]) < s->size*2); + + //vecp_push(solver_read_wlist(s,lit_neg(begin[0])),(void*)c); + //vecp_push(solver_read_wlist(s,lit_neg(begin[1])),(void*)c); + + vecp_push(solver_read_wlist(s,lit_neg(begin[0])),(void*)(size > 2 ? c : clause_from_lit(begin[1]))); + vecp_push(solver_read_wlist(s,lit_neg(begin[1])),(void*)(size > 2 ? c : clause_from_lit(begin[0]))); + + return c; +} + + +static void clause_remove(solver* s, clause* c) +{ + lit* lits = clause_begin(c); + assert(lit_neg(lits[0]) < s->size*2); + assert(lit_neg(lits[1]) < s->size*2); + + //vecp_remove(solver_read_wlist(s,lit_neg(lits[0])),(void*)c); + //vecp_remove(solver_read_wlist(s,lit_neg(lits[1])),(void*)c); + + assert(lits[0] < s->size*2); + vecp_remove(solver_read_wlist(s,lit_neg(lits[0])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[1]))); + vecp_remove(solver_read_wlist(s,lit_neg(lits[1])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[0]))); + + if (clause_learnt(c)){ + s->stats.learnts--; + s->stats.learnts_literals -= clause_size(c); + }else{ + s->stats.clauses--; + s->stats.clauses_literals -= clause_size(c); + } + + free(c); +} + + +static lbool clause_simplify(solver* s, clause* c) +{ + lit* lits = clause_begin(c); + lbool* values = s->assigns; + int i; + + assert(solver_dlevel(s) == 0); + + for (i = 0; i < clause_size(c); i++){ + lbool sig = !lit_sign(lits[i]); sig += sig - 1; + if (values[lit_var(lits[i])] == sig) + return l_True; + } + return l_False; +} + +//================================================================================================= +// Minor (solver) functions: + +void solver_setnvars(solver* s,int n) +{ + int var; + + if (s->cap < n){ + + while (s->cap < n) s->cap = s->cap*2+1; + + s->wlists = (vecp*) realloc(s->wlists, sizeof(vecp)*s->cap*2); + s->activity = (double*) realloc(s->activity, sizeof(double)*s->cap); + s->assigns = (lbool*) realloc(s->assigns, sizeof(lbool)*s->cap); + s->orderpos = (int*) realloc(s->orderpos, sizeof(int)*s->cap); + s->reasons = (clause**)realloc(s->reasons, sizeof(clause*)*s->cap); + s->levels = (int*) realloc(s->levels, sizeof(int)*s->cap); + s->tags = (lbool*) realloc(s->tags, sizeof(lbool)*s->cap); + s->trail = (lit*) realloc(s->trail, sizeof(lit)*s->cap); + } + + for (var = s->size; var < n; var++){ + vecp_new(&s->wlists[2*var]); + vecp_new(&s->wlists[2*var+1]); + s->activity [var] = 0; + s->assigns [var] = l_Undef; + s->orderpos [var] = veci_size(&s->order); + s->reasons [var] = (clause*)0; + s->levels [var] = 0; + s->tags [var] = l_Undef; + + /* does not hold because variables enqueued at top level will not be reinserted in the heap + assert(veci_size(&s->order) == var); + */ + veci_push(&s->order,var); + order_update(s, var); + } + + s->size = n > s->size ? n : s->size; +} + + +static inline bool enqueue(solver* s, lit l, clause* from) +{ + lbool* values = s->assigns; + int v = lit_var(l); + lbool val = values[v]; +#ifdef VERBOSEDEBUG + printf(L_IND"enqueue("L_LIT")\n", L_ind, L_lit(l)); +#endif + + lbool sig = !lit_sign(l); sig += sig - 1; + if (val != l_Undef){ + return val == sig; + }else{ + // New fact -- store it. +#ifdef VERBOSEDEBUG + printf(L_IND"bind("L_LIT")\n", L_ind, L_lit(l)); +#endif + int* levels = s->levels; + clause** reasons = s->reasons; + + values [v] = sig; + levels [v] = solver_dlevel(s); + reasons[v] = from; + s->trail[s->qtail++] = l; + + order_assigned(s, v); + return true; + } +} + + +static inline void assume(solver* s, lit l){ + assert(s->qtail == s->qhead); + assert(s->assigns[lit_var(l)] == l_Undef); +#ifdef VERBOSEDEBUG + printf(L_IND"assume("L_LIT")\n", L_ind, L_lit(l)); +#endif + veci_push(&s->trail_lim,s->qtail); + enqueue(s,l,(clause*)0); +} + + +static inline void solver_canceluntil(solver* s, int level) { + lit* trail; + lbool* values; + clause** reasons; + int bound; + int c; + + if (solver_dlevel(s) <= level) + return; + + trail = s->trail; + values = s->assigns; + reasons = s->reasons; + bound = (veci_begin(&s->trail_lim))[level]; + + for (c = s->qtail-1; c >= bound; c--) { + int x = lit_var(trail[c]); + values [x] = l_Undef; + reasons[x] = (clause*)0; + } + + for (c = s->qhead-1; c >= bound; c--) + order_unassigned(s,lit_var(trail[c])); + + s->qhead = s->qtail = bound; + veci_resize(&s->trail_lim,level); +} + +static void solver_record(solver* s, veci* cls) +{ + lit* begin = veci_begin(cls); + lit* end = begin + veci_size(cls); + clause* c = (veci_size(cls) > 1) ? clause_new(s,begin,end,1) : (clause*)0; + enqueue(s,*begin,c); + + assert(veci_size(cls) > 0); + + if (c != 0) { + vecp_push(&s->learnts,c); + act_clause_bump(s,c); + s->stats.learnts++; + s->stats.learnts_literals += veci_size(cls); + } +} + + +static double solver_progress(solver* s) +{ + lbool* values = s->assigns; + int* levels = s->levels; + int i; + + double progress = 0; + double F = 1.0 / s->size; + for (i = 0; i < s->size; i++) + if (values[i] != l_Undef) + progress += pow(F, levels[i]); + return progress / s->size; +} + +//================================================================================================= +// Major methods: + +static bool solver_lit_removable(solver* s, lit l, int minl) +{ + lbool* tags = s->tags; + clause** reasons = s->reasons; + int* levels = s->levels; + int top = veci_size(&s->tagged); + + assert(lit_var(l) >= 0 && lit_var(l) < s->size); + assert(reasons[lit_var(l)] != 0); + veci_resize(&s->stack,0); + veci_push(&s->stack,lit_var(l)); + + while (veci_size(&s->stack) > 0){ + clause* c; + int v = veci_begin(&s->stack)[veci_size(&s->stack)-1]; + assert(v >= 0 && v < s->size); + veci_resize(&s->stack,veci_size(&s->stack)-1); + assert(reasons[v] != 0); + c = reasons[v]; + + if (clause_is_lit(c)){ + int v = lit_var(clause_read_lit(c)); + if (tags[v] == l_Undef && levels[v] != 0){ + if (reasons[v] != 0 && ((1 << (levels[v] & 31)) & minl)){ + veci_push(&s->stack,v); + tags[v] = l_True; + veci_push(&s->tagged,v); + }else{ + int* tagged = veci_begin(&s->tagged); + int j; + for (j = top; j < veci_size(&s->tagged); j++) + tags[tagged[j]] = l_Undef; + veci_resize(&s->tagged,top); + return false; + } + } + }else{ + lit* lits = clause_begin(c); + int i, j; + + for (i = 1; i < clause_size(c); i++){ + int v = lit_var(lits[i]); + if (tags[v] == l_Undef && levels[v] != 0){ + if (reasons[v] != 0 && ((1 << (levels[v] & 31)) & minl)){ + + veci_push(&s->stack,lit_var(lits[i])); + tags[v] = l_True; + veci_push(&s->tagged,v); + }else{ + int* tagged = veci_begin(&s->tagged); + for (j = top; j < veci_size(&s->tagged); j++) + tags[tagged[j]] = l_Undef; + veci_resize(&s->tagged,top); + return false; + } + } + } + } + } + + return true; +} + +static void solver_analyze(solver* s, clause* c, veci* learnt) +{ + lit* trail = s->trail; + lbool* tags = s->tags; + clause** reasons = s->reasons; + int* levels = s->levels; + int cnt = 0; + lit p = lit_Undef; + int ind = s->qtail-1; + lit* lits; + int i, j, minl; + int* tagged; + + veci_push(learnt,lit_Undef); + + do{ + assert(c != 0); + + if (clause_is_lit(c)){ + lit q = clause_read_lit(c); + assert(lit_var(q) >= 0 && lit_var(q) < s->size); + if (tags[lit_var(q)] == l_Undef && levels[lit_var(q)] > 0){ + tags[lit_var(q)] = l_True; + veci_push(&s->tagged,lit_var(q)); + act_var_bump(s,lit_var(q)); + if (levels[lit_var(q)] == solver_dlevel(s)) + cnt++; + else + veci_push(learnt,q); + } + }else{ + + if (clause_learnt(c)) + act_clause_bump(s,c); + + lits = clause_begin(c); + //printlits(lits,lits+clause_size(c)); printf("\n"); + for (j = (p == lit_Undef ? 0 : 1); j < clause_size(c); j++){ + lit q = lits[j]; + assert(lit_var(q) >= 0 && lit_var(q) < s->size); + if (tags[lit_var(q)] == l_Undef && levels[lit_var(q)] > 0){ + tags[lit_var(q)] = l_True; + veci_push(&s->tagged,lit_var(q)); + act_var_bump(s,lit_var(q)); + if (levels[lit_var(q)] == solver_dlevel(s)) + cnt++; + else + veci_push(learnt,q); + } + } + } + + while (tags[lit_var(trail[ind--])] == l_Undef); + + p = trail[ind+1]; + c = reasons[lit_var(p)]; + cnt--; + + }while (cnt > 0); + + *veci_begin(learnt) = lit_neg(p); + + lits = veci_begin(learnt); + minl = 0; + for (i = 1; i < veci_size(learnt); i++){ + int lev = levels[lit_var(lits[i])]; + minl |= 1 << (lev & 31); + } + + // simplify (full) + for (i = j = 1; i < veci_size(learnt); i++){ + if (reasons[lit_var(lits[i])] == 0 || !solver_lit_removable(s,lits[i],minl)) + lits[j++] = lits[i]; + } + + // update size of learnt + statistics + s->stats.max_literals += veci_size(learnt); + veci_resize(learnt,j); + s->stats.tot_literals += j; + + // clear tags + tagged = veci_begin(&s->tagged); + for (i = 0; i < veci_size(&s->tagged); i++) + tags[tagged[i]] = l_Undef; + veci_resize(&s->tagged,0); + +#ifdef DEBUG + for (i = 0; i < s->size; i++) + assert(tags[i] == l_Undef); +#endif + +#ifdef VERBOSEDEBUG + printf(L_IND"Learnt {", L_ind); + for (i = 0; i < veci_size(learnt); i++) printf(" "L_LIT, L_lit(lits[i])); +#endif + if (veci_size(learnt) > 1){ + int max_i = 1; + int max = levels[lit_var(lits[1])]; + lit tmp; + + for (i = 2; i < veci_size(learnt); i++) + if (levels[lit_var(lits[i])] > max){ + max = levels[lit_var(lits[i])]; + max_i = i; + } + + tmp = lits[1]; + lits[1] = lits[max_i]; + lits[max_i] = tmp; + } +#ifdef VERBOSEDEBUG + { + int lev = veci_size(learnt) > 1 ? levels[lit_var(lits[1])] : 0; + printf(" } at level %d\n", lev); + } +#endif +} + + +clause* solver_propagate(solver* s) +{ + lbool* values = s->assigns; + clause* confl = (clause*)0; + lit* lits; + + //printf("solver_propagate\n"); + while (confl == 0 && s->qtail - s->qhead > 0){ + lit p = s->trail[s->qhead++]; + vecp* ws = solver_read_wlist(s,p); + clause **begin = (clause**)vecp_begin(ws); + clause **end = begin + vecp_size(ws); + clause **i, **j; + + s->stats.propagations++; + s->simpdb_props--; + + //printf("checking lit %d: "L_LIT"\n", veci_size(ws), L_lit(p)); + for (i = j = begin; i < end; ){ + if (clause_is_lit(*i)){ + *j++ = *i; + if (!enqueue(s,clause_read_lit(*i),clause_from_lit(p))){ + confl = s->binary; + (clause_begin(confl))[1] = lit_neg(p); + (clause_begin(confl))[0] = clause_read_lit(*i++); + + // Copy the remaining watches: + while (i < end) + *j++ = *i++; + } + }else{ + lit false_lit; + lbool sig; + + lits = clause_begin(*i); + + // Make sure the false literal is data[1]: + false_lit = lit_neg(p); + if (lits[0] == false_lit){ + lits[0] = lits[1]; + lits[1] = false_lit; + } + assert(lits[1] == false_lit); + //printf("checking clause: "); printlits(lits, lits+clause_size(*i)); printf("\n"); + + // If 0th watch is true, then clause is already satisfied. + sig = !lit_sign(lits[0]); sig += sig - 1; + if (values[lit_var(lits[0])] == sig){ + *j++ = *i; + }else{ + // Look for new watch: + lit* stop = lits + clause_size(*i); + lit* k; + for (k = lits + 2; k < stop; k++){ + lbool sig = lit_sign(*k); sig += sig - 1; + if (values[lit_var(*k)] != sig){ + lits[1] = *k; + *k = false_lit; + vecp_push(solver_read_wlist(s,lit_neg(lits[1])),*i); + goto next; } + } + + *j++ = *i; + // Clause is unit under assignment: + if (!enqueue(s,lits[0], *i)){ + confl = *i++; + // Copy the remaining watches: + while (i < end) + *j++ = *i++; + } + } + } + next: + i++; + } + + s->stats.inspects += j - (clause**)vecp_begin(ws); + vecp_resize(ws,j - (clause**)vecp_begin(ws)); + } + + return confl; +} + +static inline int clause_cmp (const void* x, const void* y) { + return clause_size((clause*)x) > 2 && (clause_size((clause*)y) == 2 || clause_activity((clause*)x) < clause_activity((clause*)y)) ? -1 : 1; } + +void solver_reducedb(solver* s) +{ + int i, j; + double extra_lim = s->cla_inc / vecp_size(&s->learnts); // Remove any clause below this activity + clause** learnts = (clause**)vecp_begin(&s->learnts); + clause** reasons = s->reasons; + + sort(vecp_begin(&s->learnts), vecp_size(&s->learnts), &clause_cmp); + + for (i = j = 0; i < vecp_size(&s->learnts) / 2; i++){ + if (clause_size(learnts[i]) > 2 && reasons[lit_var(*clause_begin(learnts[i]))] != learnts[i]) + clause_remove(s,learnts[i]); + else + learnts[j++] = learnts[i]; + } + for (; i < vecp_size(&s->learnts); i++){ + if (clause_size(learnts[i]) > 2 && reasons[lit_var(*clause_begin(learnts[i]))] != learnts[i] && clause_activity(learnts[i]) < extra_lim) + clause_remove(s,learnts[i]); + else + learnts[j++] = learnts[i]; + } + + //printf("reducedb deleted %d\n", vecp_size(&s->learnts) - j); + + + vecp_resize(&s->learnts,j); +} + +static lbool solver_search(solver* s, int nof_conflicts, int nof_learnts) +{ + int* levels = s->levels; + double var_decay = 0.95; + double clause_decay = 0.999; + double random_var_freq = 0.02; + + int conflictC = 0; + veci learnt_clause; + + assert(s->root_level == solver_dlevel(s)); + + s->stats.starts++; + s->var_decay = (float)(1 / var_decay ); + s->cla_decay = (float)(1 / clause_decay); + veci_resize(&s->model,0); + veci_new(&learnt_clause); + + for (;;){ + clause* confl = solver_propagate(s); + if (confl != 0){ + // CONFLICT + int blevel; + +#ifdef VERBOSEDEBUG + printf(L_IND"**CONFLICT**\n", L_ind); +#endif + s->stats.conflicts++; conflictC++; + if (solver_dlevel(s) == s->root_level){ + veci_delete(&learnt_clause); + return l_False; + } + + veci_resize(&learnt_clause,0); + solver_analyze(s, confl, &learnt_clause); + blevel = veci_size(&learnt_clause) > 1 ? levels[lit_var(veci_begin(&learnt_clause)[1])] : s->root_level; + blevel = s->root_level > blevel ? s->root_level : blevel; + solver_canceluntil(s,blevel); + solver_record(s,&learnt_clause); + act_var_decay(s); + act_clause_decay(s); + + }else{ + // NO CONFLICT + int next; + + if (nof_conflicts >= 0 && conflictC >= nof_conflicts){ + // Reached bound on number of conflicts: + s->progress_estimate = solver_progress(s); + solver_canceluntil(s,s->root_level); + veci_delete(&learnt_clause); + return l_Undef; } + + if (solver_dlevel(s) == 0) + // Simplify the set of problem clauses: + solver_simplify(s); + + if (nof_learnts >= 0 && vecp_size(&s->learnts) - s->qtail >= nof_learnts) + // Reduce the set of learnt clauses: + solver_reducedb(s); + + // New variable decision: + s->stats.decisions++; + next = order_select(s,(float)random_var_freq); + + if (next == var_Undef){ + // Model found: + lbool* values = s->assigns; + int i; + for (i = 0; i < s->size; i++) veci_push(&s->model,(int)values[i]); + solver_canceluntil(s,s->root_level); + veci_delete(&learnt_clause); + + /* + veci apa; veci_new(&apa); + for (i = 0; i < s->size; i++) + veci_push(&apa,(int)(s->model.ptr[i] == l_True ? toLit(i) : lit_neg(toLit(i)))); + printf("model: "); printlits((lit*)apa.ptr, (lit*)apa.ptr + veci_size(&apa)); printf("\n"); + veci_delete(&apa); + */ + + return l_True; + } + + assume(s,lit_neg(toLit(next))); + } + } + + return l_Undef; // cannot happen +} + +//================================================================================================= +// External solver functions: + +solver* solver_new(void) +{ + solver* s = (solver*)malloc(sizeof(solver)); + + // initialize vectors + vecp_new(&s->clauses); + vecp_new(&s->learnts); + veci_new(&s->order); + veci_new(&s->trail_lim); + veci_new(&s->tagged); + veci_new(&s->stack); + veci_new(&s->model); + + // initialize arrays + s->wlists = 0; + s->activity = 0; + s->assigns = 0; + s->orderpos = 0; + s->reasons = 0; + s->levels = 0; + s->tags = 0; + s->trail = 0; + + + // initialize other vars + s->size = 0; + s->cap = 0; + s->qhead = 0; + s->qtail = 0; + s->cla_inc = 1; + s->cla_decay = 1; + s->var_inc = 1; + s->var_decay = 1; + s->root_level = 0; + s->simpdb_assigns = 0; + s->simpdb_props = 0; + s->random_seed = 91648253; + s->progress_estimate = 0; + s->binary = (clause*)malloc(sizeof(clause) + sizeof(lit)*2); + s->binary->size_learnt = (2 << 1); + s->verbosity = 0; + + s->stats.starts = 0; + s->stats.decisions = 0; + s->stats.propagations = 0; + s->stats.inspects = 0; + s->stats.conflicts = 0; + s->stats.clauses = 0; + s->stats.clauses_literals = 0; + s->stats.learnts = 0; + s->stats.learnts_literals = 0; + s->stats.max_literals = 0; + s->stats.tot_literals = 0; + + return s; +} + + +void solver_delete(solver* s) +{ + int i; + for (i = 0; i < vecp_size(&s->clauses); i++) + free(vecp_begin(&s->clauses)[i]); + + for (i = 0; i < vecp_size(&s->learnts); i++) + free(vecp_begin(&s->learnts)[i]); + + // delete vectors + vecp_delete(&s->clauses); + vecp_delete(&s->learnts); + veci_delete(&s->order); + veci_delete(&s->trail_lim); + veci_delete(&s->tagged); + veci_delete(&s->stack); + veci_delete(&s->model); + free(s->binary); + + // delete arrays + if (s->wlists != 0){ + int i; + for (i = 0; i < s->size*2; i++) + vecp_delete(&s->wlists[i]); + + // if one is different from null, all are + free(s->wlists); + free(s->activity ); + free(s->assigns ); + free(s->orderpos ); + free(s->reasons ); + free(s->levels ); + free(s->trail ); + free(s->tags ); + } + + free(s); +} + + +bool solver_addclause(solver* s, lit* begin, lit* end) +{ + lit *i,*j; + int maxvar; + lbool* values; + lit last; + + if (begin == end) return false; + + //printlits(begin,end); printf("\n"); + // insertion sort + maxvar = lit_var(*begin); + for (i = begin + 1; i < end; i++){ + lit l = *i; + maxvar = lit_var(l) > maxvar ? lit_var(l) : maxvar; + for (j = i; j > begin && *(j-1) > l; j--) + *j = *(j-1); + *j = l; + } + solver_setnvars(s,maxvar+1); + + //printlits(begin,end); printf("\n"); + values = s->assigns; + + // delete duplicates + last = lit_Undef; + for (i = j = begin; i < end; i++){ + //printf("lit: "L_LIT", value = %d\n", L_lit(*i), (lit_sign(*i) ? -values[lit_var(*i)] : values[lit_var(*i)])); + lbool sig = !lit_sign(*i); sig += sig - 1; + if (*i == lit_neg(last) || sig == values[lit_var(*i)]) + return true; // tautology + else if (*i != last && values[lit_var(*i)] == l_Undef) + last = *j++ = *i; + } + + //printf("final: "); printlits(begin,j); printf("\n"); + + if (j == begin) // empty clause + return false; + else if (j - begin == 1) // unit clause + return enqueue(s,*begin,(clause*)0); + + // create new clause + vecp_push(&s->clauses,clause_new(s,begin,j,0)); + + + s->stats.clauses++; + s->stats.clauses_literals += j - begin; + + return true; +} + + +bool solver_simplify(solver* s) +{ + clause** reasons; + int type; + + assert(solver_dlevel(s) == 0); + + if (solver_propagate(s) != 0) + return false; + + if (s->qhead == s->simpdb_assigns || s->simpdb_props > 0) + return true; + + reasons = s->reasons; + for (type = 0; type < 2; type++){ + vecp* cs = type ? &s->learnts : &s->clauses; + clause** cls = (clause**)vecp_begin(cs); + + int i, j; + for (j = i = 0; i < vecp_size(cs); i++){ + if (reasons[lit_var(*clause_begin(cls[i]))] != cls[i] && + clause_simplify(s,cls[i]) == l_True) + clause_remove(s,cls[i]); + else + cls[j++] = cls[i]; + } + vecp_resize(cs,j); + } + + s->simpdb_assigns = s->qhead; + // (shouldn't depend on 'stats' really, but it will do for now) + s->simpdb_props = (int)(s->stats.clauses_literals + s->stats.learnts_literals); + + return true; +} + + +bool solver_solve(solver* s, lit* begin, lit* end) +{ + double nof_conflicts = 100; + double nof_learnts = solver_nclauses(s) / 3; + lbool status = l_Undef; + lbool* values = s->assigns; + lit* i; + + //printf("solve: "); printlits(begin, end); printf("\n"); + for (i = begin; i < end; i++){ + switch (lit_sign(*i) ? -values[lit_var(*i)] : values[lit_var(*i)]){ + case 1: /* l_True: */ + break; + case 0: /* l_Undef */ + assume(s, *i); + if (solver_propagate(s) == NULL) + break; + // falltrough + case -1: /* l_False */ + solver_canceluntil(s, 0); + return false; + } + } + + s->root_level = solver_dlevel(s); + + if (s->verbosity >= 1){ + printf("==================================[MINISAT]===================================\n"); + printf("| Conflicts | ORIGINAL | LEARNT | Progress |\n"); + printf("| | Clauses Literals | Limit Clauses Literals Lit/Cl | |\n"); + printf("==============================================================================\n"); + } + + while (status == l_Undef){ + double Ratio = (s->stats.learnts == 0)? 0.0 : + s->stats.learnts_literals / (double)s->stats.learnts; + + if (s->verbosity >= 1){ + printf("| %9.0f | %7.0f %8.0f | %7.0f %7.0f %8.0f %7.1f | %6.3f %% |\n", + (double)s->stats.conflicts, + (double)s->stats.clauses, + (double)s->stats.clauses_literals, + (double)nof_learnts, + (double)s->stats.learnts, + (double)s->stats.learnts_literals, + Ratio, + s->progress_estimate*100); + fflush(stdout); + } + status = solver_search(s,(int)nof_conflicts, (int)nof_learnts); + nof_conflicts *= 1.5; + nof_learnts *= 1.1; + } + if (s->verbosity >= 1) + printf("==============================================================================\n"); + + solver_canceluntil(s,0); + return status != l_False; +} + + +int solver_nvars(solver* s) +{ + return s->size; +} + + +int solver_nclauses(solver* s) +{ + return vecp_size(&s->clauses); +} + + +int solver_nconflicts(solver* s) +{ + return (int)s->stats.conflicts; +} + +//================================================================================================= +// Sorting functions (sigh): + +static inline void selectionsort(void** array, int size, int(*comp)(const void *, const void *)) +{ + int i, j, best_i; + void* tmp; + + for (i = 0; i < size-1; i++){ + best_i = i; + for (j = i+1; j < size; j++){ + if (comp(array[j], array[best_i]) < 0) + best_i = j; + } + tmp = array[i]; array[i] = array[best_i]; array[best_i] = tmp; + } +} + + +static void sortrnd(void** array, int size, int(*comp)(const void *, const void *), double* seed) +{ + if (size <= 15) + selectionsort(array, size, comp); + + else{ + void* pivot = array[irand(seed, size)]; + void* tmp; + int i = -1; + int j = size; + + for(;;){ + do i++; while(comp(array[i], pivot)<0); + do j--; while(comp(pivot, array[j])<0); + + if (i >= j) break; + + tmp = array[i]; array[i] = array[j]; array[j] = tmp; + } + + sortrnd(array , i , comp, seed); + sortrnd(&array[i], size-i, comp, seed); + } +} + +void sort(void** array, int size, int(*comp)(const void *, const void *)) +{ + double seed = 91648253; + sortrnd(array,size,comp,&seed); +} diff --git a/src/sat/asat_fixed/satSolver.h b/src/sat/asat_fixed/satSolver.h new file mode 100644 index 00000000..c9ce0219 --- /dev/null +++ b/src/sat/asat_fixed/satSolver.h @@ -0,0 +1,137 @@ +/************************************************************************************************** +MiniSat -- Copyright (c) 2005, Niklas Sorensson +http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/ + +Permission is hereby granted, free of charge, to any person obtaining a copy of this software and +associated documentation files (the "Software"), to deal in the Software without restriction, +including without limitation the rights to use, copy, modify, merge, publish, distribute, +sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all copies or +substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT +NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, +DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT +OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +**************************************************************************************************/ +// Modified to compile with MS Visual Studio 6.0 by Alan Mishchenko + +#ifndef solver_h +#define solver_h + +#ifdef _WIN32 +#define inline __inline // compatible with MS VS 6.0 +#endif + +#include "vec.h" + +//================================================================================================= +// Simple types: + +// does not work for c++ +typedef int bool; +static const bool true = 1; +static const bool false = 0; + +typedef int lit; +typedef char lbool; + +#ifdef _WIN32 +typedef signed __int64 uint64; // compatible with MS VS 6.0 +#else +typedef unsigned long long uint64; +#endif + +static const int var_Undef = -1; +static const lit lit_Undef = -2; + +static const lbool l_Undef = 0; +static const lbool l_True = 1; +static const lbool l_False = -1; + +static inline lit toLit (int v) { return v + v; } +static inline lit lit_neg (lit l) { return l ^ 1; } +static inline int lit_var (lit l) { return l >> 1; } +static inline int lit_sign(lit l) { return (l & 1); } + + +//================================================================================================= +// Public interface: + +struct solver_t; +typedef struct solver_t solver; + +extern solver* solver_new(void); +extern void solver_delete(solver* s); + +extern bool solver_addclause(solver* s, lit* begin, lit* end); +extern bool solver_simplify(solver* s); +extern bool solver_solve(solver* s, lit* begin, lit* end); + +extern int solver_nvars(solver* s); +extern int solver_nclauses(solver* s); +extern int solver_nconflicts(solver* s); + +extern void solver_setnvars(solver* s,int n); + +struct stats_t +{ + uint64 starts, decisions, propagations, inspects, conflicts; + uint64 clauses, clauses_literals, learnts, learnts_literals, max_literals, tot_literals; +}; +typedef struct stats_t stats; + +//================================================================================================= +// Solver representation: + +struct clause_t; +typedef struct clause_t clause; + +struct solver_t +{ + int size; // nof variables + int cap; // size of varmaps + int qhead; // Head index of queue. + int qtail; // Tail index of queue. + + // clauses + vecp clauses; // List of problem constraints. (contains: clause*) + vecp learnts; // List of learnt clauses. (contains: clause*) + + // activities + double var_inc; // Amount to bump next variable with. + double var_decay; // INVERSE decay factor for variable activity: stores 1/decay. + float cla_inc; // Amount to bump next clause with. + float cla_decay; // INVERSE decay factor for clause activity: stores 1/decay. + + vecp* wlists; // + double* activity; // A heuristic measurement of the activity of a variable. + lbool* assigns; // Current values of variables. + int* orderpos; // Index in variable order. + clause** reasons; // + int* levels; // + lit* trail; + + clause* binary; // A temporary binary clause + lbool* tags; // + veci tagged; // (contains: var) + veci stack; // (contains: var) + + veci order; // Variable order. (heap) (contains: var) + veci trail_lim; // Separator indices for different decision levels in 'trail'. (contains: int) + veci model; // If problem is solved, this vector contains the model (contains: lbool). + + int root_level; // Level of first proper decision. + int simpdb_assigns;// Number of top-level assignments at last 'simplifyDB()'. + int simpdb_props; // Number of propagations before next 'simplifyDB()'. + double random_seed; + double progress_estimate; + int verbosity; // Verbosity level. 0=silent, 1=some progress report, 2=everything + + stats stats; +}; + +#endif diff --git a/src/sat/fraig/fraigFeed.c b/src/sat/fraig/fraigFeed.c index 18b8bfcb..8a3cc6c7 100644 --- a/src/sat/fraig/fraigFeed.c +++ b/src/sat/fraig/fraigFeed.c @@ -463,6 +463,10 @@ Fraig_NodeVec_t * Fraig_FeedBackCoveringStart( Fraig_Man_t * p ) Fraig_NodeVecPush( p->vCones, pEntD ); if ( p->vCones->nSize == 1 ) continue; + //////////////////////////////// bug fix by alanmi, September 14, 2006 + if ( p->vCones->nSize > 20 ) + continue; + //////////////////////////////// for ( k = 0; k < p->vCones->nSize; k++ ) for ( m = k+1; m < p->vCones->nSize; m++ ) diff --git a/src/sat/fraig/fraigSat.c b/src/sat/fraig/fraigSat.c index 1a56cf0e..af0f13ce 100644 --- a/src/sat/fraig/fraigSat.c +++ b/src/sat/fraig/fraigSat.c @@ -34,6 +34,7 @@ static void Fraig_SupergateAddClausesExor( Fraig_Man_t * pMan, Fraig_Node_t * pN static void Fraig_SupergateAddClausesMux( Fraig_Man_t * pMan, Fraig_Node_t * pNode ); //static void Fraig_DetectFanoutFreeCone( Fraig_Man_t * pMan, Fraig_Node_t * pNode ); static void Fraig_DetectFanoutFreeConeMux( Fraig_Man_t * pMan, Fraig_Node_t * pNode ); +static void Fraig_SetActivity( Fraig_Man_t * pMan, Fraig_Node_t * pOld, Fraig_Node_t * pNew ); extern void * Msat_ClauseVecReadEntry( void * p, int i ); @@ -355,6 +356,9 @@ if ( fVerbose ) printf( "%d(%d) - ", Fraig_CountPis(p,p->vVarsInt), Msat_IntVecReadSize(p->vVarsInt) ); + // prepare variable activity + Fraig_SetActivity( p, pOld, pNew ); + // get the complemented attribute fComp = Fraig_NodeComparePhase( pOld, pNew ); //Msat_SolverPrintClauses( p->pSat ); @@ -1396,6 +1400,40 @@ printf( "%d(%d)", vFanins->nSize, nCubes ); } + +/**Function************************************************************* + + Synopsis [Collect variables using their proximity from the nodes.] + + Description [This procedure creates a variable order based on collecting + first the nodes that are the closest to the given two target nodes.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_SetActivity( Fraig_Man_t * pMan, Fraig_Node_t * pOld, Fraig_Node_t * pNew ) +{ + Fraig_Node_t * pNode; + int i, Number, MaxLevel; + float * pFactors = Msat_SolverReadFactors(pMan->pSat); + if ( pFactors == NULL ) + return; + MaxLevel = FRAIG_MAX( pOld->Level, pNew->Level ); + // create the variable order + for ( i = 0; i < Msat_IntVecReadSize(pMan->vVarsInt); i++ ) + { + // get the new node on the frontier + Number = Msat_IntVecReadEntry(pMan->vVarsInt, i); + pNode = pMan->vNodes->pArray[Number]; + pFactors[pNode->Num] = (float)pow( 0.97, MaxLevel - pNode->Level ); +// if ( pNode->Num % 50 == 0 ) +// printf( "(%d) %.2f ", MaxLevel - pNode->Level, pFactors[pNode->Num] ); + } +// printf( "\n" ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/sat/msat/msat.h b/src/sat/msat/msat.h index 1d9c0005..53353ba6 100644 --- a/src/sat/msat/msat.h +++ b/src/sat/msat/msat.h @@ -104,6 +104,7 @@ extern void Msat_SolverSetVarTypeA( Msat_Solver_t * p, int Var ); extern void Msat_SolverSetVarMap( Msat_Solver_t * p, Msat_IntVec_t * vVarMap ); extern void Msat_SolverMarkLastClauseTypeA( Msat_Solver_t * p ); extern void Msat_SolverMarkClausesStart( Msat_Solver_t * p ); +extern float * Msat_SolverReadFactors( Msat_Solver_t * p ); // returns the solution after incremental solving extern int Msat_SolverReadSolutions( Msat_Solver_t * p ); extern int * Msat_SolverReadSolutionsArray( Msat_Solver_t * p ); diff --git a/src/sat/msat/msatActivity.c b/src/sat/msat/msatActivity.c index 23925669..1cd795bd 100644 --- a/src/sat/msat/msatActivity.c +++ b/src/sat/msat/msatActivity.c @@ -45,8 +45,9 @@ void Msat_SolverVarBumpActivity( Msat_Solver_t * p, Msat_Lit_t Lit ) if ( p->dVarDecay < 0 ) // (negative decay means static variable order -- don't bump) return; Var = MSAT_LIT2VAR(Lit); - if ( (p->pdActivity[Var] += p->dVarInc) > 1e100 ) -// if ( (p->pdActivity[Var] += p->dVarInc * (1.0 + 0.005*p->pActLevels[Var])) > 1e100 ) + p->pdActivity[Var] += p->dVarInc; +// p->pdActivity[Var] += p->dVarInc * p->pFactors[Var]; + if ( p->pdActivity[Var] > 1e100 ) Msat_SolverVarRescaleActivity( p ); Msat_OrderUpdate( p->pOrder, Var ); } diff --git a/src/sat/msat/msatInt.h b/src/sat/msat/msatInt.h index 7845ec0b..03903abe 100644 --- a/src/sat/msat/msatInt.h +++ b/src/sat/msat/msatInt.h @@ -119,7 +119,7 @@ struct Msat_Solver_t_ double dClaDecay; // INVERSE decay factor for clause activity: stores 1/decay. double * pdActivity; // A heuristic measurement of the activity of a variable. - int * pActLevels; // the levels of the variables + float * pFactors; // the multiplicative factors of variable activity double dVarInc; // Amount to bump next variable with. double dVarDecay; // INVERSE decay factor for variable activity: stores 1/decay. Use negative value for static variable order. Msat_Order_t * pOrder; // Keeps track of the decision variable order. diff --git a/src/sat/msat/msatSolverApi.c b/src/sat/msat/msatSolverApi.c index 9317dcac..ee3507a6 100644 --- a/src/sat/msat/msatSolverApi.c +++ b/src/sat/msat/msatSolverApi.c @@ -64,6 +64,7 @@ void Msat_SolverClausesIncrementL( Msat_Solver_t * p ) { void Msat_SolverClausesDecrementL( Msat_Solver_t * p ) { p->nClausesAllocL--; } void Msat_SolverMarkLastClauseTypeA( Msat_Solver_t * p ) { Msat_ClauseSetTypeA( Msat_ClauseVecReadEntry( p->vClauses, Msat_ClauseVecReadSize(p->vClauses)-1 ), 1 ); } void Msat_SolverMarkClausesStart( Msat_Solver_t * p ) { p->nClausesStart = Msat_ClauseVecReadSize(p->vClauses); } +float * Msat_SolverReadFactors( Msat_Solver_t * p ) { return p->pFactors; } /**Function************************************************************* @@ -174,11 +175,11 @@ Msat_Solver_t * Msat_SolverAlloc( int nVarsAlloc, p->dVarDecay = dVarDecay; p->pdActivity = ALLOC( double, p->nVarsAlloc ); - p->pActLevels = ALLOC( int, p->nVarsAlloc ); + p->pFactors = ALLOC( float, p->nVarsAlloc ); for ( i = 0; i < p->nVarsAlloc; i++ ) { - p->pdActivity[i] = 0; - p->pActLevels[i] = 0; + p->pdActivity[i] = 0.0; + p->pFactors[i] = 1.0; } p->pAssigns = ALLOC( int, p->nVarsAlloc ); @@ -243,9 +244,12 @@ void Msat_SolverResize( Msat_Solver_t * p, int nVarsAlloc ) p->nVarsAlloc = nVarsAlloc; p->pdActivity = REALLOC( double, p->pdActivity, p->nVarsAlloc ); - p->pActLevels = REALLOC( int, p->pActLevels, p->nVarsAlloc ); + p->pFactors = REALLOC( float, p->pFactors, p->nVarsAlloc ); for ( i = nVarsAllocOld; i < p->nVarsAlloc; i++ ) - p->pdActivity[i] = 0; + { + p->pdActivity[i] = 0.0; + p->pFactors[i] = 1.0; + } p->pAssigns = REALLOC( int, p->pAssigns, p->nVarsAlloc ); p->pModel = REALLOC( int, p->pModel, p->nVarsAlloc ); @@ -399,7 +403,7 @@ void Msat_SolverFree( Msat_Solver_t * p ) Msat_ClauseVecFree( p->vLearned ); FREE( p->pdActivity ); - FREE( p->pActLevels ); + FREE( p->pFactors ); Msat_OrderFree( p->pOrder ); for ( i = 0; i < 2 * p->nVarsAlloc; i++ ) diff --git a/src/sat/msat/msatSolverSearch.c b/src/sat/msat/msatSolverSearch.c index 4b73d6b3..11a6540c 100644 --- a/src/sat/msat/msatSolverSearch.c +++ b/src/sat/msat/msatSolverSearch.c @@ -534,12 +534,18 @@ Msat_Type_t Msat_SolverSearch( Msat_Solver_t * p, int nConfLimit, int nLearnedLi Msat_Clause_t * pConf; Msat_Var_t Var; int nLevelBack, nConfs, nAssigns, Value; + int i; assert( Msat_SolverReadDecisionLevel(p) == p->nLevelRoot ); p->Stats.nStarts++; p->dVarDecay = 1 / pPars->dVarDecay; p->dClaDecay = 1 / pPars->dClaDecay; + // reset the activities + for ( i = 0; i < p->nVars; i++ ) + p->pdActivity[i] = (double)p->pFactors[i]; +// p->pdActivity[i] = 0.0; + nConfs = 0; while ( 1 ) { diff --git a/src/temp/ivy/ivy.h b/src/temp/ivy/ivy.h index 864d5e8c..5b684244 100644 --- a/src/temp/ivy/ivy.h +++ b/src/temp/ivy/ivy.h @@ -43,6 +43,7 @@ extern "C" { typedef struct Ivy_Man_t_ Ivy_Man_t; typedef struct Ivy_Obj_t_ Ivy_Obj_t; typedef int Ivy_Edge_t; +typedef struct Ivy_FraigParams_t_ Ivy_FraigParams_t; // object types typedef enum { @@ -70,13 +71,14 @@ struct Ivy_Obj_t_ // 24 bytes (32-bit) or 32 bytes (64-bit) // 10 words - 16 { int Id; // integer ID int TravId; // traversal ID - unsigned Type : 4; // object type - unsigned fPhase : 1; // value under 000...0 pattern - unsigned fMarkA : 1; // multipurpose mask - unsigned fMarkB : 1; // multipurpose mask - unsigned fExFan : 1; // set to 1 if last fanout added is EXOR - unsigned Init : 2; // latch initial value - unsigned Level : 22; // logic level + unsigned Type : 4; // object type + unsigned fMarkA : 1; // multipurpose mask + unsigned fMarkB : 1; // multipurpose mask + unsigned fExFan : 1; // set to 1 if last fanout added is EXOR + unsigned fPhase : 1; // value under 000...0 pattern + unsigned fFailTfo : 1; // the TFO of the failed node + unsigned Init : 2; // latch initial value + unsigned Level : 21; // logic level int nRefs; // reference counter Ivy_Obj_t * pFanin0; // fanin Ivy_Obj_t * pFanin1; // fanin @@ -124,6 +126,12 @@ struct Ivy_Man_t_ int time2; }; +struct Ivy_FraigParams_t_ +{ + int nSimWords; // the number of words in the simulation info + double SimSatur; // the ratio of refined classes when saturation is reached +}; + #define IVY_CUT_LIMIT 256 #define IVY_CUT_INPUT 6 @@ -249,6 +257,8 @@ static inline Ivy_Obj_t * Ivy_ObjChild0Equiv( Ivy_Obj_t * pObj ) { assert( !Ivy static inline Ivy_Obj_t * Ivy_ObjChild1Equiv( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return Ivy_ObjFanin1(pObj)? Ivy_NotCond(Ivy_ObjFanin1(pObj)->pEquiv, Ivy_ObjFaninC1(pObj)) : NULL; } static inline int Ivy_ObjLevel( Ivy_Obj_t * pObj ) { return pObj->Level; } static inline int Ivy_ObjLevelNew( Ivy_Obj_t * pObj ) { return 1 + Ivy_ObjIsExor(pObj) + IVY_MAX(Ivy_ObjFanin0(pObj)->Level, Ivy_ObjFanin1(pObj)->Level); } +static inline int Ivy_ObjFaninPhase( Ivy_Obj_t * pObj ) { return Ivy_IsComplement(pObj)? !Ivy_Regular(pObj)->fPhase : pObj->fPhase; } + static inline void Ivy_ObjClean( Ivy_Obj_t * pObj ) { int IdSaved = pObj->Id; @@ -430,6 +440,9 @@ extern void Ivy_FastMapPerform( Ivy_Man_t * pAig, int nLimit ); extern void Ivy_FastMapStop( Ivy_Man_t * pAig ); extern void Ivy_FastMapReadSupp( Ivy_Man_t * pAig, Ivy_Obj_t * pObj, Vec_Int_t * vLeaves ); extern void Ivy_FastMapReverseLevel( Ivy_Man_t * pAig ); +/*=== ivyFraig.c ==========================================================*/ +extern Ivy_Man_t * Ivy_FraigPerform( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams ); +extern void Ivy_FraigParamsDefault( Ivy_FraigParams_t * pParams ); /*=== ivyHaig.c ==========================================================*/ extern void Ivy_ManHaigStart( Ivy_Man_t * p, int fVerbose ); extern void Ivy_ManHaigTrasfer( Ivy_Man_t * p, Ivy_Man_t * pNew ); @@ -442,6 +455,7 @@ extern void Ivy_ManHaigSimulate( Ivy_Man_t * p ); extern int Ivy_TruthIsop( unsigned * puTruth, int nVars, Vec_Int_t * vCover, int fTryBoth ); /*=== ivyMan.c ==========================================================*/ extern Ivy_Man_t * Ivy_ManStart(); +extern Ivy_Man_t * Ivy_ManStartFrom( Ivy_Man_t * p ); extern Ivy_Man_t * Ivy_ManDup( Ivy_Man_t * p ); extern void Ivy_ManStop( Ivy_Man_t * p ); extern int Ivy_ManCleanup( Ivy_Man_t * p ); @@ -487,7 +501,7 @@ extern int Ivy_ManRewritePre( Ivy_Man_t * p, int fUpdateLevel, int f /*=== ivySeq.c =========================================================*/ extern int Ivy_ManRewriteSeq( Ivy_Man_t * p, int fUseZeroCost, int fVerbose ); /*=== ivyShow.c =========================================================*/ -extern void Ivy_ManShow( Ivy_Man_t * pMan, int fHaig ); +extern void Ivy_ManShow( Ivy_Man_t * pMan, int fHaig, Vec_Ptr_t * vBold ); /*=== ivyTable.c ========================================================*/ extern Ivy_Obj_t * Ivy_TableLookup( Ivy_Man_t * p, Ivy_Obj_t * pObj ); extern void Ivy_TableInsert( Ivy_Man_t * p, Ivy_Obj_t * pObj ); diff --git a/src/temp/ivy/ivyBalance.c b/src/temp/ivy/ivyBalance.c index 3e8bd6d2..5627039a 100644 --- a/src/temp/ivy/ivyBalance.c +++ b/src/temp/ivy/ivyBalance.c @@ -17,7 +17,7 @@ Revision [$Id: ivyBalance.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $] ***********************************************************************/ - + #include "ivy.h" //////////////////////////////////////////////////////////////////////// @@ -73,7 +73,9 @@ Ivy_Man_t * Ivy_ManBalance( Ivy_Man_t * p, int fUpdateLevel ) } Vec_VecFree( vStore ); if ( i = Ivy_ManCleanup( pNew ) ) - printf( "Cleanup after balancing removed %d dangling nodes.\n", i ); + { +// printf( "Cleanup after balancing removed %d dangling nodes.\n", i ); + } // check the resulting AIG if ( !Ivy_ManCheck(pNew) ) printf( "Ivy_ManBalance(): The check has failed.\n" ); diff --git a/src/temp/ivy/ivyFastMap.c b/src/temp/ivy/ivyFastMap.c index 1d74fd13..39c632c7 100644 --- a/src/temp/ivy/ivyFastMap.c +++ b/src/temp/ivy/ivyFastMap.c @@ -68,13 +68,16 @@ static int Ivy_FastMapPrint( Ivy_Man_t * pAig, int Time ); static int Ivy_FastMapDelay( Ivy_Man_t * pAig ); static int Ivy_FastMapArea( Ivy_Man_t * pAig ); static void Ivy_FastMapNode( Ivy_Man_t * pAig, Ivy_Obj_t * pObj, int nLimit ); +static void Ivy_FastMapNodeArea( Ivy_Man_t * pAig, Ivy_Obj_t * pObj, int nLimit ); static int Ivy_FastMapMerge( Ivy_Supp_t * pSupp0, Ivy_Supp_t * pSupp1, Ivy_Supp_t * pSupp, int nLimit ); -static void Ivy_FastMapRequired( Ivy_Man_t * pAig, int Delay ); +static void Ivy_FastMapRequired( Ivy_Man_t * pAig, int Delay, int fSetInter ); static void Ivy_FastMapRecover( Ivy_Man_t * pAig, int nLimit ); static int Ivy_FastMapNodeDelay( Ivy_Man_t * pAig, Ivy_Obj_t * pObj ); static int Ivy_FastMapNodeAreaRefed( Ivy_Man_t * pAig, Ivy_Obj_t * pObj ); static int Ivy_FastMapNodeAreaDerefed( Ivy_Man_t * pAig, Ivy_Obj_t * pObj ); static void Ivy_FastMapNodeRecover( Ivy_Man_t * pAig, Ivy_Obj_t * pObj, int nLimit, Vec_Ptr_t * vFront, Vec_Ptr_t * vFrontOld ); +static int Ivy_FastMapNodeRef( Ivy_Man_t * pAig, Ivy_Obj_t * pObj ); +static int Ivy_FastMapNodeDeref( Ivy_Man_t * pAig, Ivy_Obj_t * pObj ); extern int s_MappingTime; @@ -108,6 +111,7 @@ void Ivy_FastMapPerform( Ivy_Man_t * pAig, int nLimit ) pMan->nObjs = Ivy_ManObjIdMax(pAig) + 1; pMan->nSize = sizeof(Ivy_Supp_t) + nLimit * sizeof(int); pMan->pMem = (char *)malloc( pMan->nObjs * pMan->nSize ); + memset( pMan->pMem, 0, pMan->nObjs * pMan->nSize ); pMan->vLuts = Vec_VecAlloc( 100 ); pAig->pData = pMan; clk = clock(); @@ -122,28 +126,43 @@ clk = clock(); printf( "Delay oriented mapping: " ); Delay = Ivy_FastMapPrint( pAig, clock() - clk ); - // perform area recovery -clk = clock(); - Ivy_FastMapRequired( pAig, Delay ); -// PRT( "Required time computation", clock() - clk ); +// 2-1-2 (doing 2-1-2-1-2 improves 0.5%) +clk = clock(); + Ivy_FastMapRequired( pAig, Delay, 0 ); // remap the nodes Ivy_FastMapRecover( pAig, nLimit ); - printf( "Area recovery : " ); + printf( "Area recovery 2 : " ); Delay = Ivy_FastMapPrint( pAig, clock() - clk ); - // perform area recovery clk = clock(); - Ivy_FastMapRequired( pAig, Delay ); -// PRT( "Required time computation", clock() - clk ); + Ivy_FastMapRequired( pAig, Delay, 0 ); + // iterate through all nodes in the topological order + Ivy_ManForEachNode( pAig, pObj, i ) + Ivy_FastMapNodeArea( pAig, pObj, nLimit ); + printf( "Area recovery 1 : " ); + Delay = Ivy_FastMapPrint( pAig, clock() - clk ); +clk = clock(); + Ivy_FastMapRequired( pAig, Delay, 0 ); // remap the nodes Ivy_FastMapRecover( pAig, nLimit ); - printf( "Area recovery : " ); + printf( "Area recovery 2 : " ); Delay = Ivy_FastMapPrint( pAig, clock() - clk ); + s_MappingTime = clock() - clkTotal; s_MappingMem = pMan->nObjs * pMan->nSize; +/* + { + Vec_Ptr_t * vNodes; + vNodes = Vec_PtrAlloc( 100 ); + Vec_VecForEachEntry( pMan->vLuts, pObj, i, k ) + Vec_PtrPush( vNodes, pObj ); + Ivy_ManShow( pAig, 0, vNodes ); + Vec_PtrFree( vNodes ); + } +*/ } /**Function************************************************************* @@ -283,9 +302,261 @@ int Ivy_FastMapArea( Ivy_Man_t * pAig ) SeeAlso [] ***********************************************************************/ +static inline Ivy_ObjIsNodeInt1( Ivy_Obj_t * pObj ) +{ + return Ivy_ObjIsNode(pObj) && Ivy_ObjRefs(pObj) == 1; +} + +/**Function************************************************************* + + Synopsis [Performs fast mapping for one node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Ivy_ObjIsNodeInt2( Ivy_Obj_t * pObj ) +{ + return Ivy_ObjIsNode(pObj) && Ivy_ObjRefs(pObj) <= 2; +} + +/**Function************************************************************* + + Synopsis [Performs fast mapping for one node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Vec_IntSelectSort( int * pArray, int nSize ) +{ + int temp, i, j, best_i; + for ( i = 0; i < nSize-1; i++ ) + { + best_i = i; + for ( j = i+1; j < nSize; j++ ) + if ( pArray[j] < pArray[best_i] ) + best_i = j; + temp = pArray[i]; + pArray[i] = pArray[best_i]; + pArray[best_i] = temp; + } +} + +/**Function************************************************************* + + Synopsis [Performs fast mapping for one node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Vec_IntRemoveDup( int * pArray, int nSize ) +{ + int i, k; + if ( nSize < 2 ) + return nSize; + for ( i = k = 1; i < nSize; i++ ) + if ( pArray[i] != pArray[i-1] ) + pArray[k++] = pArray[i]; + return k; +} + +/**Function************************************************************* + + Synopsis [Performs fast mapping for one node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_FastMapNodeArea2( Ivy_Man_t * pAig, Ivy_Obj_t * pObj, int nLimit ) +{ + static int Store[32], StoreSize; + static char Supp0[16], Supp1[16]; + static Ivy_Supp_t * pTemp0 = (Ivy_Supp_t *)Supp0; + static Ivy_Supp_t * pTemp1 = (Ivy_Supp_t *)Supp1; + Ivy_Obj_t * pFanin0, * pFanin1; + Ivy_Supp_t * pSupp0, * pSupp1, * pSupp; + int RetValue, DelayOld; + assert( nLimit <= 32 ); + assert( Ivy_ObjIsNode(pObj) ); + // get the fanins + pFanin0 = Ivy_ObjFanin0(pObj); + pFanin1 = Ivy_ObjFanin1(pObj); + // get the supports + pSupp0 = Ivy_ObjSupp( pAig, pFanin0 ); + pSupp1 = Ivy_ObjSupp( pAig, pFanin1 ); + pSupp = Ivy_ObjSupp( pAig, pObj ); + assert( pSupp->fMark == 0 ); + // get the old delay of the node + DelayOld = Ivy_FastMapNodeDelay(pAig, pObj); + assert( DelayOld <= pSupp->DelayR ); + // copy the current cut + memcpy( Store, pSupp->pArray, sizeof(int) * pSupp->nSize ); + StoreSize = pSupp->nSize; + // get the fanin support + if ( Ivy_ObjRefs(pFanin0) > 1 && pSupp0->Delay < pSupp->DelayR ) + { + pSupp0 = pTemp0; + pSupp0->nSize = 1; + pSupp0->pArray[0] = Ivy_ObjFaninId0(pObj); + } + // get the fanin support + if ( Ivy_ObjRefs(pFanin1) > 1 && pSupp1->Delay < pSupp->DelayR ) + { + pSupp1 = pTemp1; + pSupp1->nSize = 1; + pSupp1->pArray[0] = Ivy_ObjFaninId1(pObj); + } + // merge the cuts + if ( pSupp0->nSize < pSupp1->nSize ) + RetValue = Ivy_FastMapMerge( pSupp1, pSupp0, pSupp, nLimit ); + else + RetValue = Ivy_FastMapMerge( pSupp0, pSupp1, pSupp, nLimit ); + if ( !RetValue ) + { + pSupp->nSize = 2; + pSupp->pArray[0] = Ivy_ObjFaninId0(pObj); + pSupp->pArray[1] = Ivy_ObjFaninId1(pObj); + } + // check the resulting delay + pSupp->Delay = Ivy_FastMapNodeDelay(pAig, pObj); + if ( pSupp->Delay > pSupp->DelayR ) + { + pSupp->nSize = StoreSize; + memcpy( pSupp->pArray, Store, sizeof(int) * pSupp->nSize ); + pSupp->Delay = DelayOld; + } +} + +/**Function************************************************************* + + Synopsis [Performs fast mapping for one node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_FastMapNodeArea( Ivy_Man_t * pAig, Ivy_Obj_t * pObj, int nLimit ) +{ + static int Store[32], StoreSize; + static char Supp0[16], Supp1[16]; + static Ivy_Supp_t * pTemp0 = (Ivy_Supp_t *)Supp0; + static Ivy_Supp_t * pTemp1 = (Ivy_Supp_t *)Supp1; + Ivy_Obj_t * pFanin0, * pFanin1; + Ivy_Supp_t * pSupp0, * pSupp1, * pSupp; + int RetValue, DelayOld, RefsOld; + int AreaBef, AreaAft; + assert( nLimit <= 32 ); + assert( Ivy_ObjIsNode(pObj) ); + // get the fanins + pFanin0 = Ivy_ObjFanin0(pObj); + pFanin1 = Ivy_ObjFanin1(pObj); + // get the supports + pSupp0 = Ivy_ObjSupp( pAig, pFanin0 ); + pSupp1 = Ivy_ObjSupp( pAig, pFanin1 ); + pSupp = Ivy_ObjSupp( pAig, pObj ); + assert( pSupp->fMark == 0 ); + + // get the area + if ( pSupp->nRefs == 0 ) + AreaBef = Ivy_FastMapNodeAreaDerefed( pAig, pObj ); + else + AreaBef = Ivy_FastMapNodeAreaRefed( pAig, pObj ); +// if ( AreaBef == 1 ) +// return; + + // deref the cut if the node is refed + if ( pSupp->nRefs != 0 ) + Ivy_FastMapNodeDeref( pAig, pObj ); + + // get the old delay of the node + DelayOld = Ivy_FastMapNodeDelay(pAig, pObj); + assert( DelayOld <= pSupp->DelayR ); + // copy the current cut + memcpy( Store, pSupp->pArray, sizeof(int) * pSupp->nSize ); + StoreSize = pSupp->nSize; + // get the fanin support + if ( Ivy_ObjRefs(pFanin0) > 2 && pSupp0->Delay < pSupp->DelayR ) +// if ( pSupp0->nRefs > 0 && pSupp0->Delay < pSupp->DelayR ) // this leads to 2% worse results + { + pSupp0 = pTemp0; + pSupp0->nSize = 1; + pSupp0->pArray[0] = Ivy_ObjFaninId0(pObj); + } + // get the fanin support + if ( Ivy_ObjRefs(pFanin1) > 2 && pSupp1->Delay < pSupp->DelayR ) +// if ( pSupp1->nRefs > 0 && pSupp1->Delay < pSupp->DelayR ) + { + pSupp1 = pTemp1; + pSupp1->nSize = 1; + pSupp1->pArray[0] = Ivy_ObjFaninId1(pObj); + } + // merge the cuts + if ( pSupp0->nSize < pSupp1->nSize ) + RetValue = Ivy_FastMapMerge( pSupp1, pSupp0, pSupp, nLimit ); + else + RetValue = Ivy_FastMapMerge( pSupp0, pSupp1, pSupp, nLimit ); + if ( !RetValue ) + { + pSupp->nSize = 2; + pSupp->pArray[0] = Ivy_ObjFaninId0(pObj); + pSupp->pArray[1] = Ivy_ObjFaninId1(pObj); + } + + // check the resulting delay + pSupp->Delay = Ivy_FastMapNodeDelay(pAig, pObj); + + RefsOld = pSupp->nRefs; pSupp->nRefs = 0; + AreaAft = Ivy_FastMapNodeAreaDerefed( pAig, pObj ); + pSupp->nRefs = RefsOld; + + if ( AreaAft > AreaBef || pSupp->Delay > pSupp->DelayR ) +// if ( pSupp->Delay > pSupp->DelayR ) + { + pSupp->nSize = StoreSize; + memcpy( pSupp->pArray, Store, sizeof(int) * pSupp->nSize ); + pSupp->Delay = DelayOld; +// printf( "-" ); + } +// else +// printf( "+" ); + + if ( pSupp->nRefs != 0 ) + Ivy_FastMapNodeRef( pAig, pObj ); +} + +/**Function************************************************************* + + Synopsis [Performs fast mapping for one node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ void Ivy_FastMapNode( Ivy_Man_t * pAig, Ivy_Obj_t * pObj, int nLimit ) { Ivy_Supp_t * pSupp0, * pSupp1, * pSupp; + int fFaninParam = 2; int RetValue; assert( Ivy_ObjIsNode(pObj) ); // get the supports @@ -316,9 +587,123 @@ void Ivy_FastMapNode( Ivy_Man_t * pAig, Ivy_Obj_t * pObj, int nLimit ) if ( !RetValue ) { pSupp->Delay++; - pSupp->nSize = 2; - pSupp->pArray[0] = Ivy_ObjFaninId0(pObj); - pSupp->pArray[1] = Ivy_ObjFaninId1(pObj); + if ( fFaninParam == 2 ) + { + pSupp->nSize = 2; + pSupp->pArray[0] = Ivy_ObjFaninId0(pObj); + pSupp->pArray[1] = Ivy_ObjFaninId1(pObj); + } + else if ( fFaninParam == 3 ) + { + Ivy_Obj_t * pFanin0, * pFanin1, * pFaninA, * pFaninB; + pFanin0 = Ivy_ObjFanin0(pObj); + pFanin1 = Ivy_ObjFanin1(pObj); + pSupp->nSize = 0; + // process the first fanin + if ( Ivy_ObjIsNodeInt1(pFanin0) ) + { + pFaninA = Ivy_ObjFanin0(pFanin0); + pFaninB = Ivy_ObjFanin1(pFanin0); + if ( Ivy_ObjIsNodeInt1(pFaninA) && Ivy_ObjIsNodeInt1(pFaninB) ) + pSupp->pArray[pSupp->nSize++] = Ivy_ObjId(pFanin0); + else + { + pSupp->pArray[pSupp->nSize++] = Ivy_ObjId(pFaninA); + pSupp->pArray[pSupp->nSize++] = Ivy_ObjId(pFaninB); + } + } + else + pSupp->pArray[pSupp->nSize++] = Ivy_ObjId(pFanin0); + // process the second fanin + if ( Ivy_ObjIsNodeInt1(pFanin1) ) + { + pFaninA = Ivy_ObjFanin0(pFanin1); + pFaninB = Ivy_ObjFanin1(pFanin1); + if ( Ivy_ObjIsNodeInt1(pFaninA) && Ivy_ObjIsNodeInt1(pFaninB) ) + pSupp->pArray[pSupp->nSize++] = Ivy_ObjId(pFanin1); + else + { + pSupp->pArray[pSupp->nSize++] = Ivy_ObjId(pFaninA); + pSupp->pArray[pSupp->nSize++] = Ivy_ObjId(pFaninB); + } + } + else + pSupp->pArray[pSupp->nSize++] = Ivy_ObjId(pFanin1); + // sort the fanins + Vec_IntSelectSort( pSupp->pArray, pSupp->nSize ); + pSupp->nSize = Vec_IntRemoveDup( pSupp->pArray, pSupp->nSize ); + assert( pSupp->pArray[0] < pSupp->pArray[1] ); + } + else if ( fFaninParam == 4 ) + { + Ivy_Obj_t * pFanin0, * pFanin1, * pFaninA, * pFaninB; + pFanin0 = Ivy_ObjFanin0(pObj); + pFanin1 = Ivy_ObjFanin1(pObj); + pSupp->nSize = 0; + // consider the case when exactly one of them is internal + if ( Ivy_ObjIsNodeInt1(pFanin0) ^ Ivy_ObjIsNodeInt1(pFanin1) ) + { + pSupp0 = Ivy_ObjSupp( pAig, Ivy_ObjFanin0(pObj) ); + pSupp1 = Ivy_ObjSupp( pAig, Ivy_ObjFanin1(pObj) ); + if ( Ivy_ObjIsNodeInt1(pFanin0) && pSupp0->nSize < nLimit ) + { + pSupp->Delay = IVY_MAX( pSupp0->Delay, pSupp1->Delay + 1 ); + pSupp1 = Ivy_ObjSupp( pAig, Ivy_ManConst1(pAig) ); + pSupp1->pArray[0] = Ivy_ObjId(pFanin1); + // merge the cuts + RetValue = Ivy_FastMapMerge( pSupp0, pSupp1, pSupp, nLimit ); + assert( RetValue ); + assert( pSupp->nSize > 1 ); + return; + } + if ( Ivy_ObjIsNodeInt1(pFanin1) && pSupp1->nSize < nLimit ) + { + pSupp->Delay = IVY_MAX( pSupp1->Delay, pSupp0->Delay + 1 ); + pSupp0 = Ivy_ObjSupp( pAig, Ivy_ManConst1(pAig) ); + pSupp0->pArray[0] = Ivy_ObjId(pFanin0); + // merge the cuts + RetValue = Ivy_FastMapMerge( pSupp1, pSupp0, pSupp, nLimit ); + assert( RetValue ); + assert( pSupp->nSize > 1 ); + return; + } + } + // process the first fanin + if ( Ivy_ObjIsNodeInt1(pFanin0) ) + { + pFaninA = Ivy_ObjFanin0(pFanin0); + pFaninB = Ivy_ObjFanin1(pFanin0); + if ( Ivy_ObjIsNodeInt1(pFaninA) && Ivy_ObjIsNodeInt1(pFaninB) ) + pSupp->pArray[pSupp->nSize++] = Ivy_ObjId(pFanin0); + else + { + pSupp->pArray[pSupp->nSize++] = Ivy_ObjId(pFaninA); + pSupp->pArray[pSupp->nSize++] = Ivy_ObjId(pFaninB); + } + } + else + pSupp->pArray[pSupp->nSize++] = Ivy_ObjId(pFanin0); + // process the second fanin + if ( Ivy_ObjIsNodeInt1(pFanin1) ) + { + pFaninA = Ivy_ObjFanin0(pFanin1); + pFaninB = Ivy_ObjFanin1(pFanin1); + if ( Ivy_ObjIsNodeInt1(pFaninA) && Ivy_ObjIsNodeInt1(pFaninB) ) + pSupp->pArray[pSupp->nSize++] = Ivy_ObjId(pFanin1); + else + { + pSupp->pArray[pSupp->nSize++] = Ivy_ObjId(pFaninA); + pSupp->pArray[pSupp->nSize++] = Ivy_ObjId(pFaninB); + } + } + else + pSupp->pArray[pSupp->nSize++] = Ivy_ObjId(pFanin1); + // sort the fanins + Vec_IntSelectSort( pSupp->pArray, pSupp->nSize ); + pSupp->nSize = Vec_IntRemoveDup( pSupp->pArray, pSupp->nSize ); + assert( pSupp->pArray[0] < pSupp->pArray[1] ); + assert( pSupp->nSize > 1 ); + } } assert( pSupp->Delay > 0 ); } @@ -431,6 +816,29 @@ void Ivy_FastMapReadSupp( Ivy_Man_t * pAig, Ivy_Obj_t * pObj, Vec_Int_t * vLeave /**Function************************************************************* + Synopsis [Sets the required times of the intermediate nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_FastMapRequired_rec( Ivy_Man_t * pAig, Ivy_Obj_t * pObj, Ivy_Obj_t * pRoot, int DelayR ) +{ + Ivy_Supp_t * pSupp; + pSupp = Ivy_ObjSupp( pAig, pObj ); + if ( pObj != pRoot && (pSupp->nRefs > 0 || Ivy_ObjIsCi(pObj)) ) + return; + Ivy_FastMapRequired_rec( pAig, Ivy_ObjFanin0(pObj), pRoot, DelayR ); + Ivy_FastMapRequired_rec( pAig, Ivy_ObjFanin1(pObj), pRoot, DelayR ); +// assert( pObj == pRoot || pSupp->DelayR == IVY_INFINITY ); + pSupp->DelayR = DelayR; +} + +/**Function************************************************************* + Synopsis [Computes the required times for each node.] Description [Sets reference counters for each node.] @@ -440,7 +848,7 @@ void Ivy_FastMapReadSupp( Ivy_Man_t * pAig, Ivy_Obj_t * pObj, Vec_Int_t * vLeave SeeAlso [] ***********************************************************************/ -void Ivy_FastMapRequired( Ivy_Man_t * pAig, int Delay ) +void Ivy_FastMapRequired( Ivy_Man_t * pAig, int Delay, int fSetInter ) { Vec_Vec_t * vLuts; Vec_Ptr_t * vNodes; @@ -491,6 +899,23 @@ void Ivy_FastMapRequired( Ivy_Man_t * pAig, int Delay ) } printf( "\n" ); */ + + if ( fSetInter ) + { + // set the required times of the intermediate nodes + Vec_VecForEachLevelReverse( vLuts, vNodes, i ) + Vec_PtrForEachEntry( vNodes, pObj, k ) + { + pSupp = Ivy_ObjSupp( pAig, pObj ); + Ivy_FastMapRequired_rec( pAig, pObj, pObj, pSupp->DelayR ); + } + // make sure that all required times are assigned + Ivy_ManForEachNode( pAig, pObj, i ) + { + pSupp = Ivy_ObjSupp( pAig, pObj ); + assert( pSupp->DelayR < IVY_INFINITY ); + } + } } /**Function************************************************************* @@ -688,7 +1113,7 @@ int Ivy_FastMapCutCost( Ivy_Man_t * pAig, Vec_Ptr_t * vFront ) Vec_PtrForEachEntry( vFront, pFanin, i ) { pSuppF = Ivy_ObjSupp( pAig, pFanin ); - if ( pSuppF->nRefs == 1 ) + if ( pSuppF->nRefs == 0 ) Counter++; } return Counter; @@ -754,17 +1179,17 @@ int Ivy_FastMapNodeFaninCost( Ivy_Man_t * pAig, Ivy_Obj_t * pObj ) assert( Ivy_ObjIsNode(pObj) ); // check if the node has external refs pSuppF = Ivy_ObjSupp( pAig, pObj ); - if ( pSuppF->nRefs == 1 ) + if ( pSuppF->nRefs == 0 ) Counter--; // increment the number of fanins without external refs pFanin = Ivy_ObjFanin0(pObj); pSuppF = Ivy_ObjSupp( pAig, pFanin ); - if ( !Ivy_ObjIsTravIdCurrent(pAig, pFanin) && pSuppF->nRefs == 1 ) + if ( !Ivy_ObjIsTravIdCurrent(pAig, pFanin) && pSuppF->nRefs == 0 ) Counter++; // increment the number of fanins without external refs pFanin = Ivy_ObjFanin1(pObj); pSuppF = Ivy_ObjSupp( pAig, pFanin ); - if ( !Ivy_ObjIsTravIdCurrent(pAig, pFanin) && pSuppF->nRefs == 1 ) + if ( !Ivy_ObjIsTravIdCurrent(pAig, pFanin) && pSuppF->nRefs == 0 ) Counter++; return Counter; } @@ -1055,13 +1480,79 @@ void Ivy_FastMapNodeRecover( Ivy_Man_t * pAig, Ivy_Obj_t * pObj, int nLimit, Vec Ivy_Supp_t * pSupp; int CostBef, CostAft; int AreaBef, AreaAft; + int DelayOld; pSupp = Ivy_ObjSupp( pAig, pObj ); + DelayOld = pSupp->Delay = Ivy_FastMapNodeDelay( pAig, pObj ); + assert( pSupp->Delay <= pSupp->DelayR ); if ( pSupp->nRefs == 0 ) return; // get the area AreaBef = Ivy_FastMapNodeAreaRefed( pAig, pObj ); +// if ( AreaBef == 1 ) +// return; + if ( pObj->Id == 102 ) + { + int x = 0; + } + // the cut is non-trivial + Ivy_FastMapNodePrepare( pAig, pObj, nLimit, vFront, vFrontOld ); + // iteratively modify the cut + Ivy_FastMapNodeDeref( pAig, pObj ); + CostBef = Ivy_FastMapCutCost( pAig, vFront ); + Ivy_FastMapNodeFaninCompact( pAig, pObj, nLimit, vFront ); + CostAft = Ivy_FastMapCutCost( pAig, vFront ); + Ivy_FastMapNodeRef( pAig, pObj ); + assert( CostBef >= CostAft ); + // update the node + Ivy_FastMapNodeUpdate( pAig, pObj, vFront ); + pSupp->Delay = Ivy_FastMapNodeDelay( pAig, pObj ); + // get the new area + AreaAft = Ivy_FastMapNodeAreaRefed( pAig, pObj ); + if ( AreaAft > AreaBef || pSupp->Delay > pSupp->DelayR ) + { + Ivy_FastMapNodeUpdate( pAig, pObj, vFrontOld ); + AreaAft = Ivy_FastMapNodeAreaRefed( pAig, pObj ); + assert( AreaAft == AreaBef ); + pSupp->Delay = DelayOld; + } +} + +/**Function************************************************************* + + Synopsis [Performs area recovery for each node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_FastMapNodeRecover4( Ivy_Man_t * pAig, Ivy_Obj_t * pObj, int nLimit, Vec_Ptr_t * vFront, Vec_Ptr_t * vFrontOld ) +{ + Ivy_Supp_t * pSupp; + int CostBef, CostAft; + int AreaBef, AreaAft; + int DelayOld; + pSupp = Ivy_ObjSupp( pAig, pObj ); + DelayOld = pSupp->Delay = Ivy_FastMapNodeDelay( pAig, pObj ); + assert( pSupp->Delay <= pSupp->DelayR ); +// if ( pSupp->nRefs == 0 ) +// return; +// AreaBef = Ivy_FastMapNodeAreaRefed( pAig, pObj ); + // get the area + if ( pSupp->nRefs == 0 ) + AreaBef = Ivy_FastMapNodeAreaDerefed( pAig, pObj ); + else + AreaBef = Ivy_FastMapNodeAreaRefed( pAig, pObj ); if ( AreaBef == 1 ) return; + + if ( pSupp->nRefs == 0 ) + { + pSupp->nRefs = 1000000; + Ivy_FastMapNodeRef( pAig, pObj ); + } // the cut is non-trivial Ivy_FastMapNodePrepare( pAig, pObj, nLimit, vFront, vFrontOld ); // iteratively modify the cut @@ -1071,13 +1562,20 @@ void Ivy_FastMapNodeRecover( Ivy_Man_t * pAig, Ivy_Obj_t * pObj, int nLimit, Vec assert( CostBef >= CostAft ); // update the node Ivy_FastMapNodeUpdate( pAig, pObj, vFront ); + pSupp->Delay = Ivy_FastMapNodeDelay( pAig, pObj ); // get the new area AreaAft = Ivy_FastMapNodeAreaRefed( pAig, pObj ); - if ( AreaAft > AreaBef ) + if ( AreaAft > AreaBef || pSupp->Delay > pSupp->DelayR ) { Ivy_FastMapNodeUpdate( pAig, pObj, vFrontOld ); AreaAft = Ivy_FastMapNodeAreaRefed( pAig, pObj ); assert( AreaAft == AreaBef ); + pSupp->Delay = DelayOld; + } + if ( pSupp->nRefs == 1000000 ) + { + pSupp->nRefs = 0; + Ivy_FastMapNodeDeref( pAig, pObj ); } } diff --git a/src/temp/ivy/ivyFraig.c b/src/temp/ivy/ivyFraig.c new file mode 100644 index 00000000..a3a3b33a --- /dev/null +++ b/src/temp/ivy/ivyFraig.c @@ -0,0 +1,1445 @@ +/**CFile**************************************************************** + + FileName [ivyFraig.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [And-Inverter Graph package.] + + Synopsis [Functional reduction of AIGs] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - May 11, 2006.] + + Revision [$Id: ivyFraig.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "ivy.h" +#include "satSolver.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Ivy_Fraig_t_ Ivy_Fraig_t; +struct Ivy_Fraig_t_ +{ + // general info + Ivy_FraigParams_t * pParams; // various parameters + // AIG manager + Ivy_Man_t * pManAig; // the starting AIG manager + Ivy_Man_t * pManFraig; // the final AIG manager + // simulation information + int nWords; // the number of words + unsigned * pWords; // the simulation info + // counter example storage + int nPatWords; // the number of words in the counter example + unsigned * pPatWords; // the counter example + // equivalence classes + int nClasses; // the number of equivalence classes + Ivy_Obj_t * pClassesHead; // the linked list of classes + Ivy_Obj_t * pClassesTail; // the linked list of classes + // equivalence checking + sat_solver * pSat; // SAT solver + int nSatVars; // the number of variables currently used + // statistics + int nSimRounds; + int nClassesZero; + int nClassesBeg; + int nClassesEnd; + int nSatCalls; + int nSatCallsSat; + int nSatCallsUnsat; + int nSatProof; + int nSatFails; + int nSatFailsReal; + // runtime + int timeSim; + int timeTrav; + int timeSat; + int timeRef; + int timeTotal; +}; + +static inline unsigned * Ivy_ObjSim( Ivy_Obj_t * pObj ) { return (unsigned *)pObj->pFanout; } +static inline Ivy_Obj_t * Ivy_ObjClassNodeLast( Ivy_Obj_t * pObj ) { return pObj->pNextFan0; } +static inline Ivy_Obj_t * Ivy_ObjClassNodeRepr( Ivy_Obj_t * pObj ) { return pObj->pNextFan0; } +static inline Ivy_Obj_t * Ivy_ObjClassNodeNext( Ivy_Obj_t * pObj ) { return pObj->pNextFan1; } +static inline Ivy_Obj_t * Ivy_ObjNodeHashNext( Ivy_Obj_t * pObj ) { return pObj->pPrevFan0; } +static inline Ivy_Obj_t * Ivy_ObjEquivListNext( Ivy_Obj_t * pObj ) { return pObj->pPrevFan0; } +static inline Ivy_Obj_t * Ivy_ObjEquivListPrev( Ivy_Obj_t * pObj ) { return pObj->pPrevFan1; } +static inline Ivy_Obj_t * Ivy_ObjFraig( Ivy_Obj_t * pObj ) { return pObj->pEquiv; } +static inline int Ivy_ObjSatNum( Ivy_Obj_t * pObj ) { return (int)pObj->pNextFan0; } +static inline Vec_Ptr_t * Ivy_ObjFaninVec( Ivy_Obj_t * pObj ) { return (Vec_Ptr_t *)pObj->pNextFan1; } + +static inline void Ivy_ObjSetSim( Ivy_Obj_t * pObj, unsigned * pSim ) { pObj->pFanout = (Ivy_Obj_t *)pSim; } +static inline void Ivy_ObjSetClassNodeLast( Ivy_Obj_t * pObj, Ivy_Obj_t * pLast ) { pObj->pNextFan0 = pLast; } +static inline void Ivy_ObjSetClassNodeRepr( Ivy_Obj_t * pObj, Ivy_Obj_t * pRepr ) { pObj->pNextFan0 = pRepr; } +static inline void Ivy_ObjSetClassNodeNext( Ivy_Obj_t * pObj, Ivy_Obj_t * pNext ) { pObj->pNextFan1 = pNext; } +static inline void Ivy_ObjSetNodeHashNext( Ivy_Obj_t * pObj, Ivy_Obj_t * pNext ) { pObj->pPrevFan0 = pNext; } +static inline void Ivy_ObjSetEquivListNext( Ivy_Obj_t * pObj, Ivy_Obj_t * pNext ) { pObj->pPrevFan0 = pNext; } +static inline void Ivy_ObjSetEquivListPrev( Ivy_Obj_t * pObj, Ivy_Obj_t * pPrev ) { pObj->pPrevFan1 = pPrev; } +static inline void Ivy_ObjSetFraig( Ivy_Obj_t * pObj, Ivy_Obj_t * pNode ) { pObj->pEquiv = pNode; } +static inline void Ivy_ObjSetSatNum( Ivy_Obj_t * pObj, int Num ) { pObj->pNextFan0 = (Ivy_Obj_t *)Num; } +static inline void Ivy_ObjSetFaninVec( Ivy_Obj_t * pObj, Vec_Ptr_t * vFanins ) { pObj->pNextFan1 = (Ivy_Obj_t *)vFanins; } + +static inline unsigned Ivy_ObjRandomSim() { return (rand() << 24) ^ (rand() << 12) ^ rand(); } + +// iterate through equivalence classes +#define Ivy_FraigForEachEquivClass( pList, pEnt ) \ + for ( pEnt = pList; \ + pEnt; \ + pEnt = Ivy_ObjEquivListNext(pEnt) ) +#define Ivy_FraigForEachEquivClassSafe( pList, pEnt, pEnt2 ) \ + for ( pEnt = pList, \ + pEnt2 = pEnt? Ivy_ObjEquivListNext(pEnt): NULL; \ + pEnt; \ + pEnt = pEnt2, \ + pEnt2 = pEnt? Ivy_ObjEquivListNext(pEnt): NULL ) +// iterate through nodes in one class +#define Ivy_FraigForEachClassNode( pClass, pEnt ) \ + for ( pEnt = pClass; \ + pEnt; \ + pEnt = Ivy_ObjClassNodeNext(pEnt) ) +#define Ivy_FraigForEachClassNodeSafe( pClass, pEnt, pEnt2 ) \ + for ( pEnt = pClass, \ + pEnt2 = pEnt? Ivy_ObjClassNodeNext(pEnt): NULL; \ + pEnt; \ + pEnt = pEnt2, \ + pEnt2 = pEnt? Ivy_ObjClassNodeNext(pEnt): NULL ) +// iterate through nodes in the hash table +#define Ivy_FraigForEachBinNode( pBin, pEnt ) \ + for ( pEnt = pBin; \ + pEnt; \ + pEnt = Ivy_ObjNodeHashNext(pEnt) ) +#define Ivy_FraigForEachBinNodeSafe( pBin, pEnt, pEnt2 ) \ + for ( pEnt = pBin, \ + pEnt2 = pEnt? Ivy_ObjNodeHashNext(pEnt): NULL; \ + pEnt; \ + pEnt = pEnt2, \ + pEnt2 = pEnt? Ivy_ObjNodeHashNext(pEnt): NULL ) + +static Ivy_Fraig_t * Ivy_FraigStart( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams ); +static void Ivy_FraigPrint( Ivy_Fraig_t * p ); +static void Ivy_FraigStop( Ivy_Fraig_t * p ); +static void Ivy_FraigSimulate( Ivy_Fraig_t * p ); +static void Ivy_FraigSweep( Ivy_Fraig_t * p ); +static Ivy_Obj_t * Ivy_FraigAnd( Ivy_Fraig_t * p, Ivy_Obj_t * pObjOld ); +static int Ivy_FraigNodesAreEquiv( Ivy_Fraig_t * p, Ivy_Obj_t * pObj0, Ivy_Obj_t * pObj1, int nBTLimit ); +static void Ivy_FraigNodeAddToSolver( Ivy_Fraig_t * p, Ivy_Obj_t * pObj0, Ivy_Obj_t * pObj1 ); +static int Ivy_FraigMarkConeSetActivity_rec( Ivy_Fraig_t * p, Ivy_Obj_t * pObj, int * pTravIds, int TravId, double * pFactors, int LevelMax ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Performs fraiging of the initial AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Man_t * Ivy_FraigPerform( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams ) +{ + Ivy_Fraig_t * p; + Ivy_Man_t * pManAigNew; + int clk; +clk = clock(); + assert( Ivy_ManLatchNum(pManAig) == 0 ); + p = Ivy_FraigStart( pManAig, pParams ); + Ivy_FraigSimulate( p ); + Ivy_FraigSweep( p ); + pManAigNew = p->pManFraig; +p->timeTotal = clock() - clk; + Ivy_FraigStop( p ); + return pManAigNew; +} + +/**Function************************************************************* + + Synopsis [Performs fraiging of the initial AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_FraigParamsDefault( Ivy_FraigParams_t * pParams ) +{ + memset( pParams, 0, sizeof(Ivy_FraigParams_t) ); + pParams->nSimWords = 32; + pParams->SimSatur = 0.005; +} + +/**Function************************************************************* + + Synopsis [Starts the fraiging manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Fraig_t * Ivy_FraigStart( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams ) +{ + Ivy_Fraig_t * p; + Ivy_Obj_t * pObj; + int i, k; + // clean the fanout representation + Ivy_ManForEachObj( pManAig, pObj, i ) +// pObj->pEquiv = pObj->pFanout = pObj->pNextFan0 = pObj->pNextFan1 = pObj->pPrevFan0 = pObj->pPrevFan1 = NULL; + assert( !pObj->pEquiv && !pObj->pFanout ); + // allocat the fraiging manager + p = ALLOC( Ivy_Fraig_t, 1 ); + memset( p, 0, sizeof(Ivy_Fraig_t) ); + p->pParams = pParams; + p->pManAig = pManAig; + p->pManFraig = Ivy_ManStartFrom( pManAig ); + // allocate simulation info + p->nWords = pParams->nSimWords; + p->pWords = ALLOC( unsigned, Ivy_ManObjNum(pManAig) * p->nWords ); + k = 0; + Ivy_ManForEachObj( pManAig, pObj, i ) + Ivy_ObjSetSim( pObj, p->pWords + p->nWords * k++ ); + assert( k == Ivy_ManObjNum(pManAig) ); + // allocate storage for sim pattern + p->nPatWords = Ivy_BitWordNum( Ivy_ManPiNum(pManAig) ); + p->pPatWords = ALLOC( unsigned, p->nPatWords ); + // set random number generator + srand( 0xABCABC ); + return p; +} + +/**Function************************************************************* + + Synopsis [Stops the fraiging manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_FraigPrint( Ivy_Fraig_t * p ) +{ + double nMemory; + nMemory = (double)Ivy_ManObjNum(p->pManAig)*p->nWords*sizeof(unsigned)/(1<<20); + printf( "SimWords = %d. Rounds = %d. Mem = %0.2f Mb. ", p->nWords, p->nSimRounds, nMemory ); + printf( "Classes: Beg = %d. End = %d.\n", p->nClassesBeg, p->nClassesEnd ); + printf( "Proof = %d. Counter-example = %d. Fail = %d. FailReal = %d. Zero = %d.\n", + p->nSatProof, p->nSatCallsSat, p->nSatFails, p->nSatFailsReal, p->nClassesZero ); + printf( "Nodes: Final = %d. Total = %d. Mux = %d. (Exor = %d.) SatVars = %d.\n", + Ivy_ManNodeNum(p->pManFraig), Ivy_ManNodeNum(p->pManAig), 0, 0, p->nSatVars ); + if ( p->pSat ) Sat_SolverPrintStats( stdout, p->pSat ); + PRT( "AIG simulation ", p->timeSim ); + PRT( "AIG traversal ", p->timeTrav ); + PRT( "SAT solving ", p->timeSat ); + PRT( "Class refining ", p->timeRef ); + PRT( "TOTAL RUNTIME ", p->timeTotal ); +} + +/**Function************************************************************* + + Synopsis [Stops the fraiging manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_FraigStop( Ivy_Fraig_t * p ) +{ + Ivy_FraigPrint( p ); + if ( p->pSat ) sat_solver_delete( p->pSat ); + free( p->pPatWords ); + free( p->pWords ); + free( p ); +} + +/**Function************************************************************* + + Synopsis [Simulates one node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_NodeAssignRandom( Ivy_Fraig_t * p, Ivy_Obj_t * pObj ) +{ + unsigned * pSims; + int i; + pSims = Ivy_ObjSim(pObj); + for ( i = 0; i < p->nWords; i++ ) + pSims[i] = Ivy_ObjRandomSim(); +} + +/**Function************************************************************* + + Synopsis [Simulates one node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_NodeAssignConst( Ivy_Fraig_t * p, Ivy_Obj_t * pObj, int fConst1 ) +{ + unsigned * pSims; + int i; + pSims = Ivy_ObjSim(pObj); + for ( i = 0; i < p->nWords; i++ ) + pSims[i] = fConst1? ~(unsigned)0 : 0; +} + +/**Function************************************************************* + + Synopsis [Returns 1 if simulation info is composed of all zeros.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ivy_NodeHasZeroSim( Ivy_Fraig_t * p, Ivy_Obj_t * pObj ) +{ + unsigned * pSims; + int i; + pSims = Ivy_ObjSim(pObj); + for ( i = 0; i < p->nWords; i++ ) + if ( pSims[i] ) + return 0; + return 1; +} + +/**Function************************************************************* + + Synopsis [Returns 1 if simulation infos are equal.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ivy_NodeCompareSims( Ivy_Fraig_t * p, Ivy_Obj_t * pObj0, Ivy_Obj_t * pObj1 ) +{ + unsigned * pSims0, * pSims1; + int i; + pSims0 = Ivy_ObjSim(pObj0); + pSims1 = Ivy_ObjSim(pObj1); + for ( i = 0; i < p->nWords; i++ ) + if ( pSims0[i] != pSims1[i] ) + return 0; + return 1; +} + +/**Function************************************************************* + + Synopsis [Simulates one node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_NodeSimulate( Ivy_Fraig_t * p, Ivy_Obj_t * pObj ) +{ + unsigned * pSims, * pSims0, * pSims1; + int fCompl, fCompl0, fCompl1, i; + assert( !Ivy_IsComplement(pObj) ); + // get hold of the simulation information + pSims = Ivy_ObjSim(pObj); + pSims0 = Ivy_ObjSim(Ivy_ObjFanin0(pObj)); + pSims1 = Ivy_ObjSim(Ivy_ObjFanin1(pObj)); + // get complemented attributes of the children using their random info + fCompl = pObj->fPhase; + fCompl0 = Ivy_ObjFaninPhase(Ivy_ObjChild0(pObj)); + fCompl1 = Ivy_ObjFaninPhase(Ivy_ObjChild1(pObj)); + // simulate + if ( fCompl0 && fCompl1 ) + { + if ( fCompl ) + for ( i = 0; i < p->nWords; i++ ) + pSims[i] = (pSims0[i] | pSims1[i]); + else + for ( i = 0; i < p->nWords; i++ ) + pSims[i] = ~(pSims0[i] | pSims1[i]); + } + else if ( fCompl0 && !fCompl1 ) + { + if ( fCompl ) + for ( i = 0; i < p->nWords; i++ ) + pSims[i] = (pSims0[i] | ~pSims1[i]); + else + for ( i = 0; i < p->nWords; i++ ) + pSims[i] = (~pSims0[i] & pSims1[i]); + } + else if ( !fCompl0 && fCompl1 ) + { + if ( fCompl ) + for ( i = 0; i < p->nWords; i++ ) + pSims[i] = (~pSims0[i] | pSims1[i]); + else + for ( i = 0; i < p->nWords; i++ ) + pSims[i] = (pSims0[i] & ~pSims1[i]); + } + else // if ( !fCompl0 && !fCompl1 ) + { + if ( fCompl ) + for ( i = 0; i < p->nWords; i++ ) + pSims[i] = ~(pSims0[i] & pSims1[i]); + else + for ( i = 0; i < p->nWords; i++ ) + pSims[i] = (pSims0[i] & pSims1[i]); + } +} + +/**Function************************************************************* + + Synopsis [Computes hash value using simulation info.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +unsigned Ivy_NodeHash( Ivy_Fraig_t * p, Ivy_Obj_t * pObj ) +{ + static int s_FPrimes[128] = { + 1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459, + 1499, 1559, 1607, 1657, 1709, 1759, 1823, 1877, 1933, 1997, + 2039, 2089, 2141, 2213, 2269, 2311, 2371, 2411, 2467, 2543, + 2609, 2663, 2699, 2741, 2797, 2851, 2909, 2969, 3037, 3089, + 3169, 3221, 3299, 3331, 3389, 3461, 3517, 3557, 3613, 3671, + 3719, 3779, 3847, 3907, 3943, 4013, 4073, 4129, 4201, 4243, + 4289, 4363, 4441, 4493, 4549, 4621, 4663, 4729, 4793, 4871, + 4933, 4973, 5021, 5087, 5153, 5227, 5281, 5351, 5417, 5471, + 5519, 5573, 5651, 5693, 5749, 5821, 5861, 5923, 6011, 6073, + 6131, 6199, 6257, 6301, 6353, 6397, 6481, 6563, 6619, 6689, + 6737, 6803, 6863, 6917, 6977, 7027, 7109, 7187, 7237, 7309, + 7393, 7477, 7523, 7561, 7607, 7681, 7727, 7817, 7877, 7933, + 8011, 8039, 8059, 8081, 8093, 8111, 8123, 8147 + }; + unsigned uHash, * pSims; + int i; + assert( p->nWords <= 128 ); + uHash = 0; + pSims = Ivy_ObjSim(pObj); + for ( i = 0; i < p->nWords; i++ ) + uHash ^= pSims[i] * s_FPrimes[i]; + return uHash; +} + +/**Function************************************************************* + + Synopsis [Simulates AIG manager.] + + Description [Assumes that the PI simulation info is attached.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_FraigSimulateOne( Ivy_Fraig_t * p ) +{ + Ivy_Obj_t * pObj; + int i, clk; +clk = clock(); + Ivy_ManForEachNode( p->pManAig, pObj, i ) + { + Ivy_NodeSimulate( p, pObj ); +/* + if ( Ivy_ObjFraig(pObj) == NULL ) + printf( "%3d --- -- %d : ", pObj->Id, pObj->fPhase ); + else + printf( "%3d %3d %2d %d : ", pObj->Id, Ivy_Regular(Ivy_ObjFraig(pObj))->Id, Ivy_ObjSatNum(Ivy_Regular(Ivy_ObjFraig(pObj))), pObj->fPhase ); + Extra_PrintBinary( stdout, Ivy_ObjSim(pObj), 30 ); + printf( "\n" ); +*/ + } +p->timeSim += clock() - clk; +p->nSimRounds++; +} + +/**Function************************************************************* + + Synopsis [Simulates AIG manager.] + + Description [Assumes that the PI simulation info is attached.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_FraigAssignRandom( Ivy_Fraig_t * p ) +{ + Ivy_Obj_t * pObj; + int i; + Ivy_ManForEachPi( p->pManAig, pObj, i ) + Ivy_NodeAssignRandom( p, pObj ); +} + +/**Function************************************************************* + + Synopsis [Simulates AIG manager.] + + Description [Assumes that the PI simulation info is attached.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_FraigAssignDist1( Ivy_Fraig_t * p, unsigned * pPat ) +{ + Ivy_Obj_t * pObj; + int i, Limit; + Ivy_ManForEachPi( p->pManAig, pObj, i ) + Ivy_NodeAssignConst( p, pObj, Ivy_InfoHasBit(pPat, i) ); + Limit = IVY_MIN( Ivy_ManPiNum(p->pManAig), p->nWords * 32 - 1 ); + for ( i = 0; i < Limit; i++ ) + Ivy_InfoXorBit( Ivy_ObjSim( Ivy_ManPi(p->pManAig,i) ), i+1 ); +/* + for ( i = 0; i < Limit; i++ ) + Extra_PrintBinary( stdout, Ivy_ObjSim( Ivy_ManPi(p->pManAig,i) ), 30 ), printf( "\n" ); +*/ +} + +/**Function************************************************************* + + Synopsis [Adds new nodes to the equivalence class.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_NodeAddToClass( Ivy_Obj_t * pClass, Ivy_Obj_t * pObj ) +{ + if ( Ivy_ObjClassNodeNext(pClass) == NULL ) + Ivy_ObjSetClassNodeNext( pClass, pObj ); + else + Ivy_ObjSetClassNodeNext( Ivy_ObjClassNodeLast(pClass), pObj ); + Ivy_ObjSetClassNodeLast( pClass, pObj ); + Ivy_ObjSetClassNodeRepr( pObj, pClass ); + Ivy_ObjSetClassNodeNext( pObj, NULL ); +} + +/**Function************************************************************* + + Synopsis [Adds new nodes to the equivalence class.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_FraigAddClass( Ivy_Fraig_t * p, Ivy_Obj_t * pClass ) +{ + if ( p->pClassesHead == NULL ) + { + p->pClassesHead = pClass; + p->pClassesTail = pClass; + Ivy_ObjSetEquivListPrev( pClass, NULL ); + Ivy_ObjSetEquivListNext( pClass, NULL ); + } + else + { + Ivy_ObjSetEquivListNext( p->pClassesTail, pClass ); + Ivy_ObjSetEquivListPrev( pClass, p->pClassesTail ); + Ivy_ObjSetEquivListNext( pClass, NULL ); + p->pClassesTail = pClass; + } + p->nClasses++; +} + +/**Function************************************************************* + + Synopsis [Updates the list of classes after base class has split.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_FraigInsertClass( Ivy_Fraig_t * p, Ivy_Obj_t * pBase, Ivy_Obj_t * pClass ) +{ + Ivy_ObjSetEquivListPrev( pClass, pBase ); + Ivy_ObjSetEquivListNext( pClass, Ivy_ObjEquivListNext(pBase) ); + if ( Ivy_ObjEquivListNext(pBase) ) + Ivy_ObjSetEquivListPrev( Ivy_ObjEquivListNext(pBase), pClass ); + Ivy_ObjSetEquivListNext( pBase, pClass ); + if ( p->pClassesTail == pBase ) + p->pClassesTail = pClass; + p->nClasses++; +} + +/**Function************************************************************* + + Synopsis [Updates the list of classes after base class has split.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_FraigRemoveClass( Ivy_Fraig_t * p, Ivy_Obj_t * pClass ) +{ + if ( p->pClassesHead == pClass ) + p->pClassesHead = Ivy_ObjEquivListNext(pClass); + if ( p->pClassesTail == pClass ) + p->pClassesTail = Ivy_ObjEquivListPrev(pClass); + if ( Ivy_ObjEquivListPrev(pClass) ) + Ivy_ObjSetEquivListNext( Ivy_ObjEquivListPrev(pClass), Ivy_ObjEquivListNext(pClass) ); + if ( Ivy_ObjEquivListNext(pClass) ) + Ivy_ObjSetEquivListPrev( Ivy_ObjEquivListNext(pClass), Ivy_ObjEquivListPrev(pClass) ); + Ivy_ObjSetEquivListNext( pClass, NULL ); + Ivy_ObjSetEquivListPrev( pClass, NULL ); + p->nClasses--; +} + +/**Function************************************************************* + + Synopsis [Creates initial simulation classes.] + + Description [Assumes that simulation info is assigned.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_FraigCreateClasses( Ivy_Fraig_t * p ) +{ + Ivy_Obj_t ** pTable; + Ivy_Obj_t * pObj, * pConst1, * pBin, * pEntry, * pEntry2; + int i, nTableSize; + unsigned Hash; + pConst1 = Ivy_ManConst1(p->pManAig); + // allocate the table + nTableSize = Ivy_ManObjNum(p->pManAig) / 2 + 13; + pTable = ALLOC( Ivy_Obj_t *, nTableSize ); + memset( pTable, 0, sizeof(Ivy_Obj_t *) * nTableSize ); + // collect nodes into the table + Ivy_ManForEachObj( p->pManAig, pObj, i ) + { + if ( !Ivy_ObjIsPi(pObj) && !Ivy_ObjIsNode(pObj) ) + continue; + Hash = Ivy_NodeHash( p, pObj ); + if ( Hash == 0 && Ivy_NodeHasZeroSim( p, pObj ) ) + { + Ivy_NodeAddToClass( pConst1, pObj ); + continue; + } + // add the node to the table + pBin = pTable[Hash % nTableSize]; + Ivy_FraigForEachBinNode( pBin, pEntry ) + if ( Ivy_NodeCompareSims( p, pEntry, pObj ) ) + { + Ivy_NodeAddToClass( pEntry, pObj ); + break; + } + // check if the entry was added + if ( pEntry ) + continue; + Ivy_ObjSetNodeHashNext( pObj, pBin ); + pTable[Hash % nTableSize] = pObj; + } + // collect non-trivial classes + assert( p->pClassesHead == NULL ); + if ( Ivy_ObjClassNodeNext(pConst1) ) + { + Ivy_FraigAddClass( p, pConst1 ); + Ivy_ObjSetClassNodeLast( pConst1, NULL ); + } + for ( i = 0; i < nTableSize; i++ ) + Ivy_FraigForEachBinNodeSafe( pTable[i], pEntry, pEntry2 ) + if ( Ivy_ObjClassNodeNext(pEntry) ) + { + Ivy_FraigAddClass( p, pEntry ); + Ivy_ObjSetClassNodeLast( pEntry, NULL ); + } + else + Ivy_ObjSetNodeHashNext( pEntry, NULL ); + // free the table + free( pTable ); +} + +/**Function************************************************************* + + Synopsis [Recursively refines the class after simulation.] + + Description [Returns 1 if the class has changed.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ivy_FraigRefineClass_rec( Ivy_Fraig_t * p, Ivy_Obj_t * pClass ) +{ + Ivy_Obj_t * pClassNew, * pListOld, * pListNew, * pNode; + // check if there is refinement + pListOld = pClass; + Ivy_FraigForEachClassNode( Ivy_ObjClassNodeNext(pClass), pClassNew ) + { + if ( !Ivy_NodeCompareSims(p, pClass, pClassNew) ) + break; + pListOld = pClassNew; + } + if ( pClassNew == NULL ) + return 0; + // set representative of the new class + Ivy_ObjSetClassNodeRepr( pClassNew, NULL ); + // start the new list + pListNew = pClassNew; + // go through the remaining nodes and sort them into two groups: + // (1) matches of the old node; (2) non-matches of the old node + Ivy_FraigForEachClassNode( Ivy_ObjClassNodeNext(pClassNew), pNode ) + if ( Ivy_NodeCompareSims( p, pClass, pNode ) ) + { + Ivy_ObjSetClassNodeNext( pListOld, pNode ); + pListOld = pNode; + } + else + { + Ivy_ObjSetClassNodeNext( pListNew, pNode ); + Ivy_ObjSetClassNodeRepr( pNode, pClassNew ); + pListNew = pNode; + } + // finish both lists + Ivy_ObjSetClassNodeNext( pListNew, NULL ); + Ivy_ObjSetClassNodeNext( pListOld, NULL ); + // update the list of classes + Ivy_FraigInsertClass( p, pClass, pClassNew ); + // if the old class is trivial, remove it + if ( Ivy_ObjClassNodeNext(pClass) == NULL ) + Ivy_FraigRemoveClass( p, pClass ); + // if the new class is trivial, remove it; otherwise, try to refine it + if ( Ivy_ObjClassNodeNext(pClassNew) == NULL ) + Ivy_FraigRemoveClass( p, pClassNew ); + else + Ivy_FraigRefineClass_rec( p, pClassNew ); + return 1; +} + +/**Function************************************************************* + + Synopsis [Refines the classes after simulation.] + + Description [Assumes that simulation info is assigned. Returns the + number of classes refined.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ivy_FraigRefineClasses( Ivy_Fraig_t * p ) +{ + Ivy_Obj_t * pClass, * pClass2; + int clk, RetValue = 0; +clk = clock(); + Ivy_FraigForEachEquivClassSafe( p->pClassesHead, pClass, pClass2 ) + RetValue += Ivy_FraigRefineClass_rec( p, pClass ); +p->timeRef += clock() - clk; + return RetValue; +} + +/**Function************************************************************* + + Synopsis [Print the class.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_FraigPrintClass( Ivy_Obj_t * pClass ) +{ + Ivy_Obj_t * pObj; + printf( "Class {" ); + Ivy_FraigForEachClassNode( pClass, pObj ) + printf( " %d(%d)%c", pObj->Id, pObj->Level, pObj->fPhase? '+' : '-' ); + printf( " }\n" ); +} + +/**Function************************************************************* + + Synopsis [Count the number of elements in the class.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ivy_FraigCountClassNodes( Ivy_Obj_t * pClass ) +{ + Ivy_Obj_t * pObj; + int Counter = 0; + Ivy_FraigForEachClassNode( pClass, pObj ) + Counter++; + return Counter; +} + +/**Function************************************************************* + + Synopsis [Stops the fraiging manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ivy_FraigCountClasses( Ivy_Fraig_t * p ) +{ + Ivy_Obj_t * pClass; + int Counter = 0; + Ivy_FraigForEachEquivClass( p->pClassesHead, pClass ) + Counter++; + return Counter; +} + +/**Function************************************************************* + + Synopsis [Stops the fraiging manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_FraigPrintSimClasses( Ivy_Fraig_t * p ) +{ + Ivy_Obj_t * pClass; + Ivy_FraigForEachEquivClass( p->pClassesHead, pClass ) + { +// Ivy_FraigPrintClass( pClass ); + printf( "%d ", Ivy_FraigCountClassNodes( pClass ) ); + } +// printf( "\n" ); +} + + +/**Function************************************************************* + + Synopsis [Stops the fraiging manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_FraigSimulate( Ivy_Fraig_t * p ) +{ + int nChanges, nClasses; + Ivy_FraigAssignRandom( p ); + Ivy_FraigSimulateOne( p ); + Ivy_FraigCreateClasses( p ); +//printf( "Starting classes = %5d.\n", p->nClasses ); + do { + Ivy_FraigAssignRandom( p ); + Ivy_FraigSimulateOne( p ); + nClasses = p->nClasses; + nChanges = Ivy_FraigRefineClasses( p ); +//printf( "Refined classes = %5d. Changes = %4d.\n", p->nClasses, nChanges ); + } while ( (double)nChanges / nClasses > p->pParams->SimSatur ); +// Ivy_FraigPrintSimClasses( p ); +} + +/**Function************************************************************* + + Synopsis [Stops the fraiging manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_FraigResimulate( Ivy_Fraig_t * p ) +{ + int nChanges; + Ivy_FraigAssignDist1( p, p->pPatWords ); + Ivy_FraigSimulateOne( p ); + nChanges = Ivy_FraigRefineClasses( p ); + assert( nChanges >= 1 ); +//printf( "Refined classes! = %5d. Changes = %4d.\n", p->nClasses, nChanges ); +} + + +/**Function************************************************************* + + Synopsis [Performs fraiging for the internal nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_FraigSweep( Ivy_Fraig_t * p ) +{ + Ivy_Obj_t * pObj; + int i; +p->nClassesZero = Ivy_ObjIsConst1(p->pClassesHead) ? Ivy_FraigCountClassNodes(p->pClassesHead) : 0; +p->nClassesBeg = Ivy_FraigCountClasses(p); + // duplicate internal nodes + Ivy_ManForEachNode( p->pManAig, pObj, i ) + pObj->pEquiv = Ivy_FraigAnd( p, pObj ); +p->nClassesEnd = Ivy_FraigCountClasses(p); + // add the POs + Ivy_ManForEachPo( p->pManAig, pObj, i ) + Ivy_ObjCreatePo( p->pManFraig, Ivy_ObjChild0Equiv(pObj) ); + // clean the old manager + Ivy_ManForEachObj( p->pManAig, pObj, i ) + pObj->pFanout = pObj->pNextFan0 = pObj->pNextFan1 = pObj->pPrevFan0 = pObj->pPrevFan1 = NULL; + // clean the new manager + Ivy_ManForEachObj( p->pManFraig, pObj, i ) + { + if ( Ivy_ObjFaninVec(pObj) ) + Vec_PtrFree( Ivy_ObjFaninVec(pObj) ); + pObj->pNextFan0 = pObj->pNextFan1 = NULL; + } + // remove dangling nodes + Ivy_ManCleanup( p->pManFraig ); +} + +/**Function************************************************************* + + Synopsis [Performs fraiging for one node.] + + Description [Returns the fraiged node.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Obj_t * Ivy_FraigAnd( Ivy_Fraig_t * p, Ivy_Obj_t * pObjOld ) +{ + Ivy_Obj_t * pObjNew, * pFanin0New, * pFanin1New, * pObjReprNew; + int RetValue; + // get the fraiged fanins + pFanin0New = Ivy_ObjChild0Equiv(pObjOld); + pFanin1New = Ivy_ObjChild1Equiv(pObjOld); + // get the candidate fraig node + pObjNew = Ivy_And( p->pManFraig, pFanin0New, pFanin1New ); + // get representative of this class + if ( Ivy_ObjClassNodeRepr(pObjOld) == NULL ) // this is a unique node + { + assert( Ivy_Regular(pFanin0New) != Ivy_Regular(pFanin1New) ); + assert( pObjNew != Ivy_Regular(pFanin0New) ); + assert( pObjNew != Ivy_Regular(pFanin1New) ); + return pObjNew; + } + // get the fraiged representative + pObjReprNew = Ivy_ObjFraig(Ivy_ObjClassNodeRepr(pObjOld)); + // if the fraiged nodes are the same return + if ( Ivy_Regular(pObjNew) == Ivy_Regular(pObjReprNew) ) + return pObjNew; + // they are different (the counter-example is in p->pPatWords) + RetValue = Ivy_FraigNodesAreEquiv( p, Ivy_Regular(pObjReprNew), Ivy_Regular(pObjNew), 1000 ); + if ( RetValue == 1 ) // proved equivalent + return Ivy_NotCond( pObjReprNew, pObjOld->fPhase ^ Ivy_ObjClassNodeRepr(pObjOld)->fPhase ); + if ( RetValue == -1 ) // failed + return pObjNew; + // simulate the counter-example and return the new node + Ivy_FraigResimulate( p ); + return pObjNew; +} + +/**Function************************************************************* + + Synopsis [Copy pattern from the solver into the internal storage.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_FraigSavePattern( Ivy_Fraig_t * p ) +{ + Ivy_Obj_t * pObj; + int i; + memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords ); + Ivy_ManForEachPi( p->pManFraig, pObj, i ) + if ( p->pSat->model.ptr[Ivy_ObjSatNum(pObj)] == l_True ) + Ivy_InfoSetBit( p->pPatWords, i ); +/* + // print sat variables + for ( i = 0; i < p->nSatVars; i++ ) + printf( "%d=%d ", i, p->pSat->model.ptr[i] ); + printf( "\n" ); +*/ +} + +/**Function************************************************************* + + Synopsis [Performs fraiging for one node.] + + Description [Returns the fraiged node.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ivy_FraigNodesAreEquiv( Ivy_Fraig_t * p, Ivy_Obj_t * pOld, Ivy_Obj_t * pNew, int nBTLimit ) +{ + int pLits[4], RetValue, RetValue1, clk, Counter; + +// printf( "Trying to prove nodes %d and %d\n", pOld->Id, pNew->Id ); + + // make sure the nodes are not complemented + assert( !Ivy_IsComplement(pNew) ); + assert( !Ivy_IsComplement(pOld) ); + assert( pNew != pOld ); + + // if at least one of the nodes is a failed node, perform adjustments: + // if the backtrack limit is small, simply skip this node + // if the backtrack limit is > 10, take the quare root of the limit + if ( nBTLimit > 0 && (pOld->fFailTfo || pNew->fFailTfo) ) + { + p->nSatFails++; + if ( nBTLimit <= 10 ) + return -1; + nBTLimit = (int)sqrt(nBTLimit); + } + p->nSatCalls++; + + // make sure the solver is allocated and has enough variables + if ( p->pSat == NULL ) + { + p->pSat = sat_solver_new(); + p->nSatVars = 1; + sat_solver_setnvars( p->pSat, 1000 ); + } + + // if the nodes do not have SAT variables, allocate them + Ivy_FraigNodeAddToSolver( p, pOld, pNew ); + + // prepare variable activity +clk = clock(); + Ivy_ManIncrementTravId( p->pManFraig ); + Counter = Ivy_FraigMarkConeSetActivity_rec( p, pOld, NULL, 0, NULL, 0 ); + Counter += Ivy_FraigMarkConeSetActivity_rec( p, pNew, NULL, 0, NULL, 0 ); +// printf( "%d ", Counter ); +p->timeTrav += clock() - clk; + + + // solve under assumptions + // A = 1; B = 0 OR A = 1; B = 1 +clk = clock(); + pLits[0] = toLitCond( Ivy_ObjSatNum(pOld), 0 ); + pLits[1] = toLitCond( Ivy_ObjSatNum(pNew), pOld->fPhase == pNew->fPhase ); +//Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 ); + RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2 ); +p->timeSat += clock() - clk; + if ( RetValue1 == l_False ) + { + pLits[0] = lit_neg( pLits[0] ); + pLits[1] = lit_neg( pLits[1] ); + RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 ); + assert( RetValue ); + // continue solving the other implication + p->nSatCallsUnsat++; + } + else if ( RetValue1 == l_True ) + { + Ivy_FraigSavePattern( p ); + p->nSatCallsSat++; + return 0; + } + else // if ( RetValue1 == l_Undef ) + { + // mark the node as the failed node + if ( pOld != p->pManFraig->pConst1 ) + pOld->fFailTfo = 1; + pNew->fFailTfo = 1; + p->nSatFailsReal++; + return -1; + } + + // if the old node was constant 0, we already know the answer + if ( pOld == p->pManFraig->pConst1 ) + { + p->nSatProof++; + return 1; + } + + // solve under assumptions + // A = 0; B = 1 OR A = 0; B = 0 +clk = clock(); + pLits[0] = toLitCond( Ivy_ObjSatNum(pOld), 1 ); + pLits[1] = toLitCond( Ivy_ObjSatNum(pNew), pOld->fPhase ^ pNew->fPhase ); + RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2 ); +p->timeSat += clock() - clk; + if ( RetValue1 == l_False ) + { + pLits[0] = lit_neg( pLits[0] ); + pLits[1] = lit_neg( pLits[1] ); + RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 ); + assert( RetValue ); + p->nSatCallsUnsat++; + } + else if ( RetValue1 == l_True ) + { + Ivy_FraigSavePattern( p ); + p->nSatCallsSat++; + return 0; + } + else // if ( RetValue1 == l_Undef ) + { + // mark the node as the failed node + pOld->fFailTfo = 1; + pNew->fFailTfo = 1; + p->nSatFailsReal++; + return -1; + } + + // return SAT proof + p->nSatProof++; + return 1; +} + +/**Function************************************************************* + + Synopsis [Addes clauses to the solver.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_FraigAddClausesMux( Ivy_Fraig_t * p, Ivy_Obj_t * pNode ) +{ + Ivy_Obj_t * pNodeI, * pNodeT, * pNodeE; + int pLits[4], RetValue, VarF, VarI, VarT, VarE, fCompT, fCompE; + + assert( !Ivy_IsComplement( pNode ) ); + assert( Ivy_ObjIsMuxType( pNode ) ); + // get nodes (I = if, T = then, E = else) + pNodeI = Ivy_ObjRecognizeMux( pNode, &pNodeT, &pNodeE ); + // get the variable numbers + VarF = Ivy_ObjSatNum(pNode); + VarI = Ivy_ObjSatNum(pNodeI); + VarT = Ivy_ObjSatNum(Ivy_Regular(pNodeT)); + VarE = Ivy_ObjSatNum(Ivy_Regular(pNodeE)); + // get the complementation flags + fCompT = Ivy_IsComplement(pNodeT); + fCompE = Ivy_IsComplement(pNodeE); + + // f = ITE(i, t, e) + + // i' + t' + f + // i' + t + f' + // i + e' + f + // i + e + f' + + // create four clauses + pLits[0] = toLitCond(VarI, 1); + pLits[1] = toLitCond(VarT, 1^fCompT); + pLits[2] = toLitCond(VarF, 0); + RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 ); + assert( RetValue ); + pLits[0] = toLitCond(VarI, 1); + pLits[1] = toLitCond(VarT, 0^fCompT); + pLits[2] = toLitCond(VarF, 1); + RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 ); + assert( RetValue ); + pLits[0] = toLitCond(VarI, 0); + pLits[1] = toLitCond(VarE, 1^fCompE); + pLits[2] = toLitCond(VarF, 0); + RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 ); + assert( RetValue ); + pLits[0] = toLitCond(VarI, 0); + pLits[1] = toLitCond(VarE, 0^fCompE); + pLits[2] = toLitCond(VarF, 1); + RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 ); + assert( RetValue ); + + // two additional clauses + // t' & e' -> f' + // t & e -> f + + // t + e + f' + // t' + e' + f + + if ( VarT == VarE ) + { +// assert( fCompT == !fCompE ); + return; + } + + pLits[0] = toLitCond(VarT, 0^fCompT); + pLits[1] = toLitCond(VarE, 0^fCompE); + pLits[2] = toLitCond(VarF, 1); + RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 ); + assert( RetValue ); + pLits[0] = toLitCond(VarT, 1^fCompT); + pLits[1] = toLitCond(VarE, 1^fCompE); + pLits[2] = toLitCond(VarF, 0); + RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 ); + assert( RetValue ); +} + +/**Function************************************************************* + + Synopsis [Addes clauses to the solver.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_FraigAddClausesSuper( Ivy_Fraig_t * p, Ivy_Obj_t * pNode, Vec_Ptr_t * vSuper ) +{ + Ivy_Obj_t * pFanin; + int * pLits, nLits, RetValue, i; + assert( !Ivy_IsComplement(pNode) ); + assert( Ivy_ObjIsNode( pNode ) ); + // create storage for literals + nLits = Vec_PtrSize(vSuper) + 1; + pLits = ALLOC( int, nLits ); + // suppose AND-gate is A & B = C + // add !A => !C or A + !C + Vec_PtrForEachEntry( vSuper, pFanin, i ) + { + pLits[0] = toLitCond(Ivy_ObjSatNum(Ivy_Regular(pFanin)), Ivy_IsComplement(pFanin)); + pLits[1] = toLitCond(Ivy_ObjSatNum(pNode), 1); + RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 ); + assert( RetValue ); + } + // add A & B => C or !A + !B + C + Vec_PtrForEachEntry( vSuper, pFanin, i ) + pLits[i] = toLitCond(Ivy_ObjSatNum(Ivy_Regular(pFanin)), !Ivy_IsComplement(pFanin)); + pLits[nLits-1] = toLitCond(Ivy_ObjSatNum(pNode), 0); + RetValue = sat_solver_addclause( p->pSat, pLits, pLits + nLits ); + assert( RetValue ); + free( pLits ); +} + +/**Function************************************************************* + + Synopsis [Collects the supergate.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_FraigCollectSuper_rec( Ivy_Obj_t * pObj, Vec_Ptr_t * vSuper, int fFirst, int fUseMuxes ) +{ + // if the new node is complemented or a PI, another gate begins + if ( Ivy_IsComplement(pObj) || Ivy_ObjIsPi(pObj) || (!fFirst && Ivy_ObjRefs(pObj) > 1) || + (fUseMuxes && Ivy_ObjIsMuxType(pObj)) ) + { + Vec_PtrPushUnique( vSuper, pObj ); + return; + } + // go through the branches + Ivy_FraigCollectSuper_rec( Ivy_ObjChild0(pObj), vSuper, 0, fUseMuxes ); + Ivy_FraigCollectSuper_rec( Ivy_ObjChild1(pObj), vSuper, 0, fUseMuxes ); +} + +/**Function************************************************************* + + Synopsis [Collects the supergate.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Ivy_FraigCollectSuper( Ivy_Obj_t * pObj, int fUseMuxes ) +{ + Vec_Ptr_t * vSuper; + assert( !Ivy_IsComplement(pObj) ); + assert( !Ivy_ObjIsPi(pObj) ); + vSuper = Vec_PtrAlloc( 4 ); + Ivy_FraigCollectSuper_rec( pObj, vSuper, 1, fUseMuxes ); + return vSuper; +} + +/**Function************************************************************* + + Synopsis [Collects the supergate.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_FraigObjAddToFrontier( Ivy_Fraig_t * p, Ivy_Obj_t * pObj, Vec_Ptr_t * vFrontier ) +{ + assert( !Ivy_IsComplement(pObj) ); + if ( Ivy_ObjSatNum(pObj) ) + return; + assert( Ivy_ObjSatNum(pObj) == 0 ); + assert( Ivy_ObjFaninVec(pObj) == NULL ); + if ( Ivy_ObjIsConst1(pObj) ) + return; +//printf( "Assigning node %d number %d\n", pObj->Id, p->nSatVars ); + Ivy_ObjSetSatNum( pObj, p->nSatVars++ ); + if ( Ivy_ObjIsNode(pObj) ) + Vec_PtrPush( vFrontier, pObj ); +} + +/**Function************************************************************* + + Synopsis [Addes clauses to the solver.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_FraigNodeAddToSolver( Ivy_Fraig_t * p, Ivy_Obj_t * pOld, Ivy_Obj_t * pNew ) +{ + Vec_Ptr_t * vFrontier, * vFanins; + Ivy_Obj_t * pNode, * pFanin; + int i, k, fUseMuxes = 1; + // quit if CNF is ready + if ( Ivy_ObjFaninVec(pOld) && Ivy_ObjFaninVec(pNew) ) + return; + // start the frontier + vFrontier = Vec_PtrAlloc( 100 ); + Ivy_FraigObjAddToFrontier( p, pOld, vFrontier ); + Ivy_FraigObjAddToFrontier( p, pNew, vFrontier ); + // explore nodes in the frontier + Vec_PtrForEachEntry( vFrontier, pNode, i ) + { + // create the supergate + assert( Ivy_ObjSatNum(pNode) ); + assert( Ivy_ObjFaninVec(pNode) == NULL ); + if ( fUseMuxes && Ivy_ObjIsMuxType(pNode) ) + { + vFanins = Vec_PtrAlloc( 4 ); + Vec_PtrPushUnique( vFanins, Ivy_ObjFanin0( Ivy_ObjFanin0(pNode) ) ); + Vec_PtrPushUnique( vFanins, Ivy_ObjFanin0( Ivy_ObjFanin1(pNode) ) ); + Vec_PtrPushUnique( vFanins, Ivy_ObjFanin1( Ivy_ObjFanin0(pNode) ) ); + Vec_PtrPushUnique( vFanins, Ivy_ObjFanin1( Ivy_ObjFanin1(pNode) ) ); + Vec_PtrForEachEntry( vFanins, pFanin, k ) + Ivy_FraigObjAddToFrontier( p, Ivy_Regular(pFanin), vFrontier ); + Ivy_FraigAddClausesMux( p, pNode ); + } + else + { + vFanins = Ivy_FraigCollectSuper( pNode, fUseMuxes ); + Vec_PtrForEachEntry( vFanins, pFanin, k ) + Ivy_FraigObjAddToFrontier( p, Ivy_Regular(pFanin), vFrontier ); + Ivy_FraigAddClausesSuper( p, pNode, vFanins ); + } + assert( Vec_PtrSize(vFanins) > 1 ); + Ivy_ObjSetFaninVec( pNode, vFanins ); + } + Vec_PtrFree( vFrontier ); +} + +/**Function************************************************************* + + Synopsis [Performs fraiging for one node.] + + Description [Returns the fraiged node.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ivy_FraigMarkConeSetActivity_rec( Ivy_Fraig_t * p, Ivy_Obj_t * pObj, int * pTravIds, int TravId, double * pFactors, int LevelMax ) +{ + Vec_Ptr_t * vFanins; + Ivy_Obj_t * pFanin; + int i, Counter; + assert( !Ivy_IsComplement(pObj) ); + if ( Ivy_ObjIsConst1(pObj) ) + return 0; + assert( Ivy_ObjSatNum(pObj) ); +// if ( pTravIds[Ivy_ObjSatNum(pObj)] == TravId ) +// return; +// pTravIds[Ivy_ObjSatNum(pObj)] = TravId; +// pFactors[Ivy_ObjSatNum(pObj)] = pow( 0.97, LevelMax - pObj->Level ); + if ( Ivy_ObjIsTravIdCurrent(p->pManFraig, pObj) ) + return 0; + Ivy_ObjSetTravIdCurrent(p->pManFraig, pObj); + if ( Ivy_ObjIsPi(pObj) ) + return 0; + + vFanins = Ivy_ObjFaninVec( pObj ); + Counter = 1; + Vec_PtrForEachEntry( vFanins, pFanin, i ) + Counter += Ivy_FraigMarkConeSetActivity_rec( p, Ivy_Regular(pFanin), pTravIds, TravId, pFactors, LevelMax ); + return Counter; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/temp/ivy/ivyMan.c b/src/temp/ivy/ivyMan.c index 786949e7..c6ad75e8 100644 --- a/src/temp/ivy/ivyMan.c +++ b/src/temp/ivy/ivyMan.c @@ -58,7 +58,7 @@ Ivy_Man_t * Ivy_ManStart() Ivy_ManStartMemory( p ); // create the constant node p->pConst1 = Ivy_ManFetchMemory( p ); -// p->pConst1->fPhase = 1; + p->pConst1->fPhase = 1; Vec_PtrPush( p->vObjs, p->pConst1 ); p->nCreated = 1; // start the table @@ -79,6 +79,31 @@ Ivy_Man_t * Ivy_ManStart() SeeAlso [] ***********************************************************************/ +Ivy_Man_t * Ivy_ManStartFrom( Ivy_Man_t * p ) +{ + Ivy_Man_t * pNew; + Ivy_Obj_t * pObj; + int i; + // create the new manager + pNew = Ivy_ManStart(); + // create the PIs + Ivy_ManConst1(p)->pEquiv = Ivy_ManConst1(pNew); + Ivy_ManForEachPi( p, pObj, i ) + pObj->pEquiv = Ivy_ObjCreatePi(pNew); + return pNew; +} + +/**Function************************************************************* + + Synopsis [Duplicates the AIG manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ Ivy_Man_t * Ivy_ManDup( Ivy_Man_t * p ) { Vec_Int_t * vNodes, * vLatches; diff --git a/src/temp/ivy/ivyObj.c b/src/temp/ivy/ivyObj.c index 36af3920..d9887c5b 100644 --- a/src/temp/ivy/ivyObj.c +++ b/src/temp/ivy/ivyObj.c @@ -96,6 +96,14 @@ Ivy_Obj_t * Ivy_ObjCreate( Ivy_Man_t * p, Ivy_Obj_t * pGhost ) pObj->Level = Ivy_ObjFanin0(pObj)->Level; else if ( !Ivy_ObjIsPi(pObj) ) assert( 0 ); + // create phase + if ( Ivy_ObjIsNode(pObj) ) + pObj->fPhase = Ivy_ObjFaninPhase(Ivy_ObjChild0(pObj)) & Ivy_ObjFaninPhase(Ivy_ObjChild1(pObj)); + else if ( Ivy_ObjIsOneFanin(pObj) ) + pObj->fPhase = Ivy_ObjFaninPhase(Ivy_ObjChild0(pObj)); + // set the fail TFO flag + if ( Ivy_ObjIsNode(pObj) ) + pObj->fFailTfo = Ivy_ObjFanin0(pObj)->fFailTfo | Ivy_ObjFanin1(pObj)->fFailTfo; // mark the fanins in a special way if the node is EXOR if ( Ivy_ObjIsExor(pObj) ) { diff --git a/src/temp/ivy/ivyShow.c b/src/temp/ivy/ivyShow.c index 3105081e..cd726e43 100644 --- a/src/temp/ivy/ivyShow.c +++ b/src/temp/ivy/ivyShow.c @@ -24,7 +24,7 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -static void Ivy_WriteDotAig( Ivy_Man_t * pMan, char * pFileName, int fHaig ); +static void Ivy_WriteDotAig( Ivy_Man_t * pMan, char * pFileName, int fHaig, Vec_Ptr_t * vBold ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -41,7 +41,7 @@ static void Ivy_WriteDotAig( Ivy_Man_t * pMan, char * pFileName, int fHaig ); SeeAlso [] ***********************************************************************/ -void Ivy_ManShow( Ivy_Man_t * pMan, int fHaig ) +void Ivy_ManShow( Ivy_Man_t * pMan, int fHaig, Vec_Ptr_t * vBold ) { extern void Abc_ShowFile( char * FileNameDot ); static Counter = 0; @@ -58,7 +58,7 @@ void Ivy_ManShow( Ivy_Man_t * pMan, int fHaig ) } fclose( pFile ); // generate the file - Ivy_WriteDotAig( pMan, FileNameDot, fHaig ); + Ivy_WriteDotAig( pMan, FileNameDot, fHaig, vBold ); // visualize the file Abc_ShowFile( FileNameDot ); } @@ -75,7 +75,7 @@ void Ivy_ManShow( Ivy_Man_t * pMan, int fHaig ) SeeAlso [] ***********************************************************************/ -void Ivy_WriteDotAig( Ivy_Man_t * pMan, char * pFileName, int fHaig ) +void Ivy_WriteDotAig( Ivy_Man_t * pMan, char * pFileName, int fHaig, Vec_Ptr_t * vBold ) { FILE * pFile; Ivy_Obj_t * pNode, * pTemp, * pPrev; @@ -92,6 +92,11 @@ void Ivy_WriteDotAig( Ivy_Man_t * pMan, char * pFileName, int fHaig ) return; } + // mark the nodes + if ( vBold ) + Vec_PtrForEachEntry( vBold, pNode, i ) + pNode->fMarkB = 1; + // compute levels LevelMax = 1 + Ivy_ManSetLevels( pMan, fHaig ); @@ -218,6 +223,8 @@ void Ivy_WriteDotAig( Ivy_Man_t * pMan, char * pFileName, int fHaig ) fprintf( pFile, " Node%d [label = \"%d(%d%s)\"", pNode->Id, pNode->Id, Ivy_Regular(pNode->pEquiv)->Id, Ivy_IsComplement(pNode->pEquiv)? "\'":"" ); fprintf( pFile, ", shape = ellipse" ); + if ( vBold && pNode->fMarkB ) + fprintf( pFile, ", style = filled" ); fprintf( pFile, "];\n" ); } fprintf( pFile, "}" ); @@ -316,6 +323,11 @@ void Ivy_WriteDotAig( Ivy_Man_t * pMan, char * pFileName, int fHaig ) fprintf( pFile, "\n" ); fprintf( pFile, "\n" ); fclose( pFile ); + + // unmark nodes + if ( vBold ) + Vec_PtrForEachEntry( vBold, pNode, i ) + pNode->fMarkB = 0; } diff --git a/src/temp/ivy/satSolver.c b/src/temp/ivy/satSolver.c new file mode 100644 index 00000000..b8248df8 --- /dev/null +++ b/src/temp/ivy/satSolver.c @@ -0,0 +1,1194 @@ +/************************************************************************************************** +MiniSat -- Copyright (c) 2005, Niklas Sorensson +http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/ + +Permission is hereby granted, free of charge, to any person obtaining a copy of this software and +associated documentation files (the "Software"), to deal in the Software without restriction, +including without limitation the rights to use, copy, modify, merge, publish, distribute, +sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all copies or +substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT +NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, +DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT +OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +**************************************************************************************************/ +// Modified to compile with MS Visual Studio 6.0 by Alan Mishchenko + +#include <stdio.h> +#include <assert.h> +#include <string.h> +#include <math.h> + +#include "satSolver.h" + +//================================================================================================= +// Debug: + +//#define VERBOSEDEBUG + +// For derivation output (verbosity level 2) +#define L_IND "%-*d" +#define L_ind sat_solver_dlevel(s)*3+3,sat_solver_dlevel(s) +#define L_LIT "%sx%d" +#define L_lit(p) lit_sign(p)?"~":"", (lit_var(p)) + +// Just like 'assert()' but expression will be evaluated in the release version as well. +static inline void check(int expr) { assert(expr); } + +static void printlits(lit* begin, lit* end) +{ + int i; + for (i = 0; i < end - begin; i++) + printf(L_LIT" ",L_lit(begin[i])); +} + +//================================================================================================= +// Random numbers: + + +// Returns a random float 0 <= x < 1. Seed must never be 0. +static inline double drand(double* seed) { + int q; + *seed *= 1389796; + q = (int)(*seed / 2147483647); + *seed -= (double)q * 2147483647; + return *seed / 2147483647; } + + +// Returns a random integer 0 <= x < size. Seed must never be 0. +static inline int irand(double* seed, int size) { + return (int)(drand(seed) * size); } + + +//================================================================================================= +// Predeclarations: + +static void sat_solver_sort(void** array, int size, int(*comp)(const void *, const void *)); + +//================================================================================================= +// Clause datatype + minor functions: + +struct clause_t +{ + int size_learnt; + lit lits[0]; +}; + +static inline int clause_size (clause* c) { return c->size_learnt >> 1; } +static inline lit* clause_begin (clause* c) { return c->lits; } +static inline int clause_learnt (clause* c) { return c->size_learnt & 1; } +static inline float clause_activity (clause* c) { return *((float*)&c->lits[c->size_learnt>>1]); } +static inline void clause_setactivity(clause* c, float a) { *((float*)&c->lits[c->size_learnt>>1]) = a; } + +//================================================================================================= +// Encode literals in clause pointers: + +static clause* clause_from_lit (lit l) { return (clause*)((unsigned long)l + (unsigned long)l + 1); } +static bool clause_is_lit (clause* c) { return ((unsigned long)c & 1); } +static lit clause_read_lit (clause* c) { return (lit)((unsigned long)c >> 1); } + +//================================================================================================= +// Simple helpers: + +static inline int sat_solver_dlevel(sat_solver* s) { return veci_size(&s->trail_lim); } +static inline vecp* sat_solver_read_wlist(sat_solver* s, lit l) { return &s->wlists[l]; } +static inline void vecp_remove(vecp* v, void* e) +{ + void** ws = vecp_begin(v); + int j = 0; + for (; ws[j] != e ; j++); + assert(j < vecp_size(v)); + for (; j < vecp_size(v)-1; j++) ws[j] = ws[j+1]; + vecp_resize(v,vecp_size(v)-1); +} + +//================================================================================================= +// Variable order functions: + +static inline void order_update(sat_solver* s, int v) // updateorder +{ + int* orderpos = s->orderpos; + double* activity = s->activity; + int* heap = veci_begin(&s->order); + int i = orderpos[v]; + int x = heap[i]; + int parent = (i - 1) / 2; + + assert(s->orderpos[v] != -1); + + while (i != 0 && activity[x] > activity[heap[parent]]){ + heap[i] = heap[parent]; + orderpos[heap[i]] = i; + i = parent; + parent = (i - 1) / 2; + } + heap[i] = x; + orderpos[x] = i; +} + +static inline void order_assigned(sat_solver* s, int v) +{ +} + +static inline void order_unassigned(sat_solver* s, int v) // undoorder +{ + int* orderpos = s->orderpos; + if (orderpos[v] == -1){ + orderpos[v] = veci_size(&s->order); + veci_push(&s->order,v); + order_update(s,v); + } +} + +static int order_select(sat_solver* s, float random_var_freq) // selectvar +{ + int* heap; + double* activity; + int* orderpos; + + lbool* values = s->assigns; + + // Random decision: + if (drand(&s->random_seed) < random_var_freq){ + int next = irand(&s->random_seed,s->size); + assert(next >= 0 && next < s->size); + if (values[next] == l_Undef) + return next; + } + + // Activity based decision: + + heap = veci_begin(&s->order); + activity = s->activity; + orderpos = s->orderpos; + + + while (veci_size(&s->order) > 0){ + int next = heap[0]; + int size = veci_size(&s->order)-1; + int x = heap[size]; + + veci_resize(&s->order,size); + + orderpos[next] = -1; + + if (size > 0){ + double act = activity[x]; + + int i = 0; + int child = 1; + + + while (child < size){ + if (child+1 < size && activity[heap[child]] < activity[heap[child+1]]) + child++; + + assert(child < size); + + if (act >= activity[heap[child]]) + break; + + heap[i] = heap[child]; + orderpos[heap[i]] = i; + i = child; + child = 2 * child + 1; + } + heap[i] = x; + orderpos[heap[i]] = i; + } + + if (values[next] == l_Undef) + return next; + } + + return var_Undef; +} + +//================================================================================================= +// Activity functions: + +static inline void act_var_rescale(sat_solver* s) { + double* activity = s->activity; + int i; + for (i = 0; i < s->size; i++) + activity[i] *= 1e-100; + s->var_inc *= 1e-100; +} + +static inline void act_var_bump(sat_solver* s, int v) { + double* activity = s->activity; + if ((activity[v] += s->var_inc) > 1e100) + act_var_rescale(s); + + //printf("bump %d %f\n", v-1, activity[v]); + + if (s->orderpos[v] != -1) + order_update(s,v); + +} + +static inline void act_var_decay(sat_solver* s) { s->var_inc *= s->var_decay; } + +static inline void act_clause_rescale(sat_solver* s) { + clause** cs = (clause**)vecp_begin(&s->learnts); + int i; + for (i = 0; i < vecp_size(&s->learnts); i++){ + float a = clause_activity(cs[i]); + clause_setactivity(cs[i], a * (float)1e-20); + } + s->cla_inc *= (float)1e-20; +} + + +static inline void act_clause_bump(sat_solver* s, clause *c) { + float a = clause_activity(c) + s->cla_inc; + clause_setactivity(c,a); + if (a > 1e20) act_clause_rescale(s); +} + +static inline void act_clause_decay(sat_solver* s) { s->cla_inc *= s->cla_decay; } + + +//================================================================================================= +// Clause functions: + +/* pre: size > 1 && no variable occurs twice + */ +static clause* clause_new(sat_solver* s, lit* begin, lit* end, int learnt) +{ + int size; + clause* c; + int i; + + assert(end - begin > 1); + assert(learnt >= 0 && learnt < 2); + size = end - begin; + c = (clause*)malloc(sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float)); + c->size_learnt = (size << 1) | learnt; + assert(((unsigned int)c & 1) == 0); + + for (i = 0; i < size; i++) + c->lits[i] = begin[i]; + + if (learnt) + *((float*)&c->lits[size]) = 0.0; + + assert(begin[0] >= 0); + assert(begin[0] < s->size*2); + assert(begin[1] >= 0); + assert(begin[1] < s->size*2); + + assert(lit_neg(begin[0]) < s->size*2); + assert(lit_neg(begin[1]) < s->size*2); + + //vecp_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(void*)c); + //vecp_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(void*)c); + + vecp_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(void*)(size > 2 ? c : clause_from_lit(begin[1]))); + vecp_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(void*)(size > 2 ? c : clause_from_lit(begin[0]))); + + return c; +} + + +static void clause_remove(sat_solver* s, clause* c) +{ + lit* lits = clause_begin(c); + assert(lit_neg(lits[0]) < s->size*2); + assert(lit_neg(lits[1]) < s->size*2); + + //vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[0])),(void*)c); + //vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[1])),(void*)c); + + assert(lits[0] < s->size*2); + vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[0])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[1]))); + vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[1])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[0]))); + + if (clause_learnt(c)){ + s->stats.learnts--; + s->stats.learnts_literals -= clause_size(c); + }else{ + s->stats.clauses--; + s->stats.clauses_literals -= clause_size(c); + } + + free(c); +} + + +static lbool clause_simplify(sat_solver* s, clause* c) +{ + lit* lits = clause_begin(c); + lbool* values = s->assigns; + int i; + + assert(sat_solver_dlevel(s) == 0); + + for (i = 0; i < clause_size(c); i++){ + lbool sig = !lit_sign(lits[i]); sig += sig - 1; + if (values[lit_var(lits[i])] == sig) + return l_True; + } + return l_False; +} + +//================================================================================================= +// Minor (solver) functions: + +void sat_solver_setnvars(sat_solver* s,int n) +{ + int var; + + if (s->cap < n){ + + while (s->cap < n) s->cap = s->cap*2+1; + + s->wlists = (vecp*) realloc(s->wlists, sizeof(vecp)*s->cap*2); + s->activity = (double*) realloc(s->activity, sizeof(double)*s->cap); + s->assigns = (lbool*) realloc(s->assigns, sizeof(lbool)*s->cap); + s->orderpos = (int*) realloc(s->orderpos, sizeof(int)*s->cap); + s->reasons = (clause**)realloc(s->reasons, sizeof(clause*)*s->cap); + s->levels = (int*) realloc(s->levels, sizeof(int)*s->cap); + s->tags = (lbool*) realloc(s->tags, sizeof(lbool)*s->cap); + s->trail = (lit*) realloc(s->trail, sizeof(lit)*s->cap); + } + + for (var = s->size; var < n; var++){ + vecp_new(&s->wlists[2*var]); + vecp_new(&s->wlists[2*var+1]); + s->activity [var] = 0; + s->assigns [var] = l_Undef; + s->orderpos [var] = veci_size(&s->order); + s->reasons [var] = (clause*)0; + s->levels [var] = 0; + s->tags [var] = l_Undef; + + /* does not hold because variables enqueued at top level will not be reinserted in the heap + assert(veci_size(&s->order) == var); + */ + veci_push(&s->order,var); + order_update(s, var); + } + + s->size = n > s->size ? n : s->size; +} + + +static inline bool enqueue(sat_solver* s, lit l, clause* from) +{ + lbool* values = s->assigns; + int v = lit_var(l); + lbool val = values[v]; +#ifdef VERBOSEDEBUG + printf(L_IND"enqueue("L_LIT")\n", L_ind, L_lit(l)); +#endif + + lbool sig = !lit_sign(l); sig += sig - 1; + if (val != l_Undef){ + return val == sig; + }else{ + // New fact -- store it. +#ifdef VERBOSEDEBUG + printf(L_IND"bind("L_LIT")\n", L_ind, L_lit(l)); +#endif + int* levels = s->levels; + clause** reasons = s->reasons; + + values [v] = sig; + levels [v] = sat_solver_dlevel(s); + reasons[v] = from; + s->trail[s->qtail++] = l; + + order_assigned(s, v); + return true; + } +} + + +static inline void assume(sat_solver* s, lit l){ + assert(s->qtail == s->qhead); + assert(s->assigns[lit_var(l)] == l_Undef); +#ifdef VERBOSEDEBUG + printf(L_IND"assume("L_LIT")\n", L_ind, L_lit(l)); +#endif + veci_push(&s->trail_lim,s->qtail); + enqueue(s,l,(clause*)0); +} + + +static inline void sat_solver_canceluntil(sat_solver* s, int level) { + lit* trail; + lbool* values; + clause** reasons; + int bound; + int c; + + if (sat_solver_dlevel(s) <= level) + return; + + trail = s->trail; + values = s->assigns; + reasons = s->reasons; + bound = (veci_begin(&s->trail_lim))[level]; + + for (c = s->qtail-1; c >= bound; c--) { + int x = lit_var(trail[c]); + values [x] = l_Undef; + reasons[x] = (clause*)0; + } + + for (c = s->qhead-1; c >= bound; c--) + order_unassigned(s,lit_var(trail[c])); + + s->qhead = s->qtail = bound; + veci_resize(&s->trail_lim,level); +} + +static void sat_solver_record(sat_solver* s, veci* cls) +{ + lit* begin = veci_begin(cls); + lit* end = begin + veci_size(cls); + clause* c = (veci_size(cls) > 1) ? clause_new(s,begin,end,1) : (clause*)0; + enqueue(s,*begin,c); + + assert(veci_size(cls) > 0); + + if (c != 0) { + vecp_push(&s->learnts,c); + act_clause_bump(s,c); + s->stats.learnts++; + s->stats.learnts_literals += veci_size(cls); + } +} + + +static double sat_solver_progress(sat_solver* s) +{ + lbool* values = s->assigns; + int* levels = s->levels; + int i; + + double progress = 0; + double F = 1.0 / s->size; + for (i = 0; i < s->size; i++) + if (values[i] != l_Undef) + progress += pow(F, levels[i]); + return progress / s->size; +} + +//================================================================================================= +// Major methods: + +static bool sat_solver_lit_removable(sat_solver* s, lit l, int minl) +{ + lbool* tags = s->tags; + clause** reasons = s->reasons; + int* levels = s->levels; + int top = veci_size(&s->tagged); + + assert(lit_var(l) >= 0 && lit_var(l) < s->size); + assert(reasons[lit_var(l)] != 0); + veci_resize(&s->stack,0); + veci_push(&s->stack,lit_var(l)); + + while (veci_size(&s->stack) > 0){ + clause* c; + int v = veci_begin(&s->stack)[veci_size(&s->stack)-1]; + assert(v >= 0 && v < s->size); + veci_resize(&s->stack,veci_size(&s->stack)-1); + assert(reasons[v] != 0); + c = reasons[v]; + + if (clause_is_lit(c)){ + int v = lit_var(clause_read_lit(c)); + if (tags[v] == l_Undef && levels[v] != 0){ + if (reasons[v] != 0 && ((1 << (levels[v] & 31)) & minl)){ + veci_push(&s->stack,v); + tags[v] = l_True; + veci_push(&s->tagged,v); + }else{ + int* tagged = veci_begin(&s->tagged); + int j; + for (j = top; j < veci_size(&s->tagged); j++) + tags[tagged[j]] = l_Undef; + veci_resize(&s->tagged,top); + return false; + } + } + }else{ + lit* lits = clause_begin(c); + int i, j; + + for (i = 1; i < clause_size(c); i++){ + int v = lit_var(lits[i]); + if (tags[v] == l_Undef && levels[v] != 0){ + if (reasons[v] != 0 && ((1 << (levels[v] & 31)) & minl)){ + + veci_push(&s->stack,lit_var(lits[i])); + tags[v] = l_True; + veci_push(&s->tagged,v); + }else{ + int* tagged = veci_begin(&s->tagged); + for (j = top; j < veci_size(&s->tagged); j++) + tags[tagged[j]] = l_Undef; + veci_resize(&s->tagged,top); + return false; + } + } + } + } + } + + return true; +} + +static void sat_solver_analyze(sat_solver* s, clause* c, veci* learnt) +{ + lit* trail = s->trail; + lbool* tags = s->tags; + clause** reasons = s->reasons; + int* levels = s->levels; + int cnt = 0; + lit p = lit_Undef; + int ind = s->qtail-1; + lit* lits; + int i, j, minl; + int* tagged; + + veci_push(learnt,lit_Undef); + + do{ + assert(c != 0); + + if (clause_is_lit(c)){ + lit q = clause_read_lit(c); + assert(lit_var(q) >= 0 && lit_var(q) < s->size); + if (tags[lit_var(q)] == l_Undef && levels[lit_var(q)] > 0){ + tags[lit_var(q)] = l_True; + veci_push(&s->tagged,lit_var(q)); + act_var_bump(s,lit_var(q)); + if (levels[lit_var(q)] == sat_solver_dlevel(s)) + cnt++; + else + veci_push(learnt,q); + } + }else{ + + if (clause_learnt(c)) + act_clause_bump(s,c); + + lits = clause_begin(c); + //printlits(lits,lits+clause_size(c)); printf("\n"); + for (j = (p == lit_Undef ? 0 : 1); j < clause_size(c); j++){ + lit q = lits[j]; + assert(lit_var(q) >= 0 && lit_var(q) < s->size); + if (tags[lit_var(q)] == l_Undef && levels[lit_var(q)] > 0){ + tags[lit_var(q)] = l_True; + veci_push(&s->tagged,lit_var(q)); + act_var_bump(s,lit_var(q)); + if (levels[lit_var(q)] == sat_solver_dlevel(s)) + cnt++; + else + veci_push(learnt,q); + } + } + } + + while (tags[lit_var(trail[ind--])] == l_Undef); + + p = trail[ind+1]; + c = reasons[lit_var(p)]; + cnt--; + + }while (cnt > 0); + + *veci_begin(learnt) = lit_neg(p); + + lits = veci_begin(learnt); + minl = 0; + for (i = 1; i < veci_size(learnt); i++){ + int lev = levels[lit_var(lits[i])]; + minl |= 1 << (lev & 31); + } + + // simplify (full) + for (i = j = 1; i < veci_size(learnt); i++){ + if (reasons[lit_var(lits[i])] == 0 || !sat_solver_lit_removable(s,lits[i],minl)) + lits[j++] = lits[i]; + } + + // update size of learnt + statistics + s->stats.max_literals += veci_size(learnt); + veci_resize(learnt,j); + s->stats.tot_literals += j; + + // clear tags + tagged = veci_begin(&s->tagged); + for (i = 0; i < veci_size(&s->tagged); i++) + tags[tagged[i]] = l_Undef; + veci_resize(&s->tagged,0); + +#ifdef DEBUG + for (i = 0; i < s->size; i++) + assert(tags[i] == l_Undef); +#endif + +#ifdef VERBOSEDEBUG + printf(L_IND"Learnt {", L_ind); + for (i = 0; i < veci_size(learnt); i++) printf(" "L_LIT, L_lit(lits[i])); +#endif + if (veci_size(learnt) > 1){ + int max_i = 1; + int max = levels[lit_var(lits[1])]; + lit tmp; + + for (i = 2; i < veci_size(learnt); i++) + if (levels[lit_var(lits[i])] > max){ + max = levels[lit_var(lits[i])]; + max_i = i; + } + + tmp = lits[1]; + lits[1] = lits[max_i]; + lits[max_i] = tmp; + } +#ifdef VERBOSEDEBUG + { + int lev = veci_size(learnt) > 1 ? levels[lit_var(lits[1])] : 0; + printf(" } at level %d\n", lev); + } +#endif +} + + +clause* sat_solver_propagate(sat_solver* s) +{ + lbool* values = s->assigns; + clause* confl = (clause*)0; + lit* lits; + + //printf("sat_solver_propagate\n"); + while (confl == 0 && s->qtail - s->qhead > 0){ + lit p = s->trail[s->qhead++]; + vecp* ws = sat_solver_read_wlist(s,p); + clause **begin = (clause**)vecp_begin(ws); + clause **end = begin + vecp_size(ws); + clause **i, **j; + + s->stats.propagations++; + s->simpdb_props--; + + //printf("checking lit %d: "L_LIT"\n", veci_size(ws), L_lit(p)); + for (i = j = begin; i < end; ){ + if (clause_is_lit(*i)){ + *j++ = *i; + if (!enqueue(s,clause_read_lit(*i),clause_from_lit(p))){ + confl = s->binary; + (clause_begin(confl))[1] = lit_neg(p); + (clause_begin(confl))[0] = clause_read_lit(*i++); + + // Copy the remaining watches: + while (i < end) + *j++ = *i++; + } + }else{ + lit false_lit; + lbool sig; + + lits = clause_begin(*i); + + // Make sure the false literal is data[1]: + false_lit = lit_neg(p); + if (lits[0] == false_lit){ + lits[0] = lits[1]; + lits[1] = false_lit; + } + assert(lits[1] == false_lit); + //printf("checking clause: "); printlits(lits, lits+clause_size(*i)); printf("\n"); + + // If 0th watch is true, then clause is already satisfied. + sig = !lit_sign(lits[0]); sig += sig - 1; + if (values[lit_var(lits[0])] == sig){ + *j++ = *i; + }else{ + // Look for new watch: + lit* stop = lits + clause_size(*i); + lit* k; + for (k = lits + 2; k < stop; k++){ + lbool sig = lit_sign(*k); sig += sig - 1; + if (values[lit_var(*k)] != sig){ + lits[1] = *k; + *k = false_lit; + vecp_push(sat_solver_read_wlist(s,lit_neg(lits[1])),*i); + goto next; } + } + + *j++ = *i; + // Clause is unit under assignment: + if (!enqueue(s,lits[0], *i)){ + confl = *i++; + // Copy the remaining watches: + while (i < end) + *j++ = *i++; + } + } + } + next: + i++; + } + + s->stats.inspects += j - (clause**)vecp_begin(ws); + vecp_resize(ws,j - (clause**)vecp_begin(ws)); + } + + return confl; +} + +static inline int clause_cmp (const void* x, const void* y) { + return clause_size((clause*)x) > 2 && (clause_size((clause*)y) == 2 || clause_activity((clause*)x) < clause_activity((clause*)y)) ? -1 : 1; } + +void sat_solver_reducedb(sat_solver* s) +{ + int i, j; + double extra_lim = s->cla_inc / vecp_size(&s->learnts); // Remove any clause below this activity + clause** learnts = (clause**)vecp_begin(&s->learnts); + clause** reasons = s->reasons; + + sat_solver_sort(vecp_begin(&s->learnts), vecp_size(&s->learnts), &clause_cmp); + + for (i = j = 0; i < vecp_size(&s->learnts) / 2; i++){ + if (clause_size(learnts[i]) > 2 && reasons[lit_var(*clause_begin(learnts[i]))] != learnts[i]) + clause_remove(s,learnts[i]); + else + learnts[j++] = learnts[i]; + } + for (; i < vecp_size(&s->learnts); i++){ + if (clause_size(learnts[i]) > 2 && reasons[lit_var(*clause_begin(learnts[i]))] != learnts[i] && clause_activity(learnts[i]) < extra_lim) + clause_remove(s,learnts[i]); + else + learnts[j++] = learnts[i]; + } + + //printf("reducedb deleted %d\n", vecp_size(&s->learnts) - j); + + + vecp_resize(&s->learnts,j); +} + +static lbool sat_solver_search(sat_solver* s, int nof_conflicts, int nof_learnts) +{ + int* levels = s->levels; + double var_decay = 0.95; + double clause_decay = 0.999; + double random_var_freq = 0.02; + + int conflictC = 0; + veci learnt_clause; + + assert(s->root_level == sat_solver_dlevel(s)); + + s->stats.starts++; + s->var_decay = (float)(1 / var_decay ); + s->cla_decay = (float)(1 / clause_decay); + veci_resize(&s->model,0); + veci_new(&learnt_clause); + + for (;;){ + clause* confl = sat_solver_propagate(s); + if (confl != 0){ + // CONFLICT + int blevel; + +#ifdef VERBOSEDEBUG + printf(L_IND"**CONFLICT**\n", L_ind); +#endif + s->stats.conflicts++; conflictC++; + if (sat_solver_dlevel(s) == s->root_level){ + veci_delete(&learnt_clause); + return l_False; + } + + veci_resize(&learnt_clause,0); + sat_solver_analyze(s, confl, &learnt_clause); + blevel = veci_size(&learnt_clause) > 1 ? levels[lit_var(veci_begin(&learnt_clause)[1])] : s->root_level; + blevel = s->root_level > blevel ? s->root_level : blevel; + sat_solver_canceluntil(s,blevel); + sat_solver_record(s,&learnt_clause); + act_var_decay(s); + act_clause_decay(s); + + }else{ + // NO CONFLICT + int next; + + if (nof_conflicts >= 0 && conflictC >= nof_conflicts){ + // Reached bound on number of conflicts: + s->progress_estimate = sat_solver_progress(s); + sat_solver_canceluntil(s,s->root_level); + veci_delete(&learnt_clause); + return l_Undef; } + + if (sat_solver_dlevel(s) == 0) + // Simplify the set of problem clauses: + sat_solver_simplify(s); + + if (nof_learnts >= 0 && vecp_size(&s->learnts) - s->qtail >= nof_learnts) + // Reduce the set of learnt clauses: + sat_solver_reducedb(s); + + // New variable decision: + s->stats.decisions++; + next = order_select(s,(float)random_var_freq); + + if (next == var_Undef){ + // Model found: + lbool* values = s->assigns; + int i; + veci_resize(&s->model, 0); + for (i = 0; i < s->size; i++) + veci_push(&s->model,(int)values[i]); + sat_solver_canceluntil(s,s->root_level); + veci_delete(&learnt_clause); + + /* + veci apa; veci_new(&apa); + for (i = 0; i < s->size; i++) + veci_push(&apa,(int)(s->model.ptr[i] == l_True ? toLit(i) : lit_neg(toLit(i)))); + printf("model: "); printlits((lit*)apa.ptr, (lit*)apa.ptr + veci_size(&apa)); printf("\n"); + veci_delete(&apa); + */ + + return l_True; + } + + assume(s,lit_neg(toLit(next))); + } + } + + return l_Undef; // cannot happen +} + +//================================================================================================= +// External solver functions: + +sat_solver* sat_solver_new(void) +{ + sat_solver* s = (sat_solver*)malloc(sizeof(sat_solver)); + memset( s, 0, sizeof(sat_solver) ); + + // initialize vectors + vecp_new(&s->clauses); + vecp_new(&s->learnts); + veci_new(&s->order); + veci_new(&s->trail_lim); + veci_new(&s->tagged); + veci_new(&s->stack); + veci_new(&s->model); + + // initialize arrays + s->wlists = 0; + s->activity = 0; + s->assigns = 0; + s->orderpos = 0; + s->reasons = 0; + s->levels = 0; + s->tags = 0; + s->trail = 0; + + + // initialize other vars + s->size = 0; + s->cap = 0; + s->qhead = 0; + s->qtail = 0; + s->cla_inc = 1; + s->cla_decay = 1; + s->var_inc = 1; + s->var_decay = 1; + s->root_level = 0; + s->simpdb_assigns = 0; + s->simpdb_props = 0; + s->random_seed = 91648253; + s->progress_estimate = 0; + s->binary = (clause*)malloc(sizeof(clause) + sizeof(lit)*2); + s->binary->size_learnt = (2 << 1); + s->verbosity = 0; + + s->stats.starts = 0; + s->stats.decisions = 0; + s->stats.propagations = 0; + s->stats.inspects = 0; + s->stats.conflicts = 0; + s->stats.clauses = 0; + s->stats.clauses_literals = 0; + s->stats.learnts = 0; + s->stats.learnts_literals = 0; + s->stats.max_literals = 0; + s->stats.tot_literals = 0; + + return s; +} + + +void sat_solver_delete(sat_solver* s) +{ + int i; + for (i = 0; i < vecp_size(&s->clauses); i++) + free(vecp_begin(&s->clauses)[i]); + + for (i = 0; i < vecp_size(&s->learnts); i++) + free(vecp_begin(&s->learnts)[i]); + + // delete vectors + vecp_delete(&s->clauses); + vecp_delete(&s->learnts); + veci_delete(&s->order); + veci_delete(&s->trail_lim); + veci_delete(&s->tagged); + veci_delete(&s->stack); + veci_delete(&s->model); + free(s->binary); + + // delete arrays + if (s->wlists != 0){ + int i; + for (i = 0; i < s->size*2; i++) + vecp_delete(&s->wlists[i]); + + // if one is different from null, all are + free(s->wlists); + free(s->activity ); + free(s->assigns ); + free(s->orderpos ); + free(s->reasons ); + free(s->levels ); + free(s->trail ); + free(s->tags ); + } + + free(s); +} + + +bool sat_solver_addclause(sat_solver* s, lit* begin, lit* end) +{ + lit *i,*j; + int maxvar; + lbool* values; + lit last; + + if (begin == end) return false; + + //printlits(begin,end); printf("\n"); + // insertion sort + maxvar = lit_var(*begin); + for (i = begin + 1; i < end; i++){ + lit l = *i; + maxvar = lit_var(l) > maxvar ? lit_var(l) : maxvar; + for (j = i; j > begin && *(j-1) > l; j--) + *j = *(j-1); + *j = l; + } + sat_solver_setnvars(s,maxvar+1); + + //printlits(begin,end); printf("\n"); + values = s->assigns; + + // delete duplicates + last = lit_Undef; + for (i = j = begin; i < end; i++){ + //printf("lit: "L_LIT", value = %d\n", L_lit(*i), (lit_sign(*i) ? -values[lit_var(*i)] : values[lit_var(*i)])); + lbool sig = !lit_sign(*i); sig += sig - 1; + if (*i == lit_neg(last) || sig == values[lit_var(*i)]) + return true; // tautology + else if (*i != last && values[lit_var(*i)] == l_Undef) + last = *j++ = *i; + } + + //printf("final: "); printlits(begin,j); printf("\n"); + + if (j == begin) // empty clause + return false; + else if (j - begin == 1) // unit clause + return enqueue(s,*begin,(clause*)0); + + // create new clause + vecp_push(&s->clauses,clause_new(s,begin,j,0)); + + + s->stats.clauses++; + s->stats.clauses_literals += j - begin; + + return true; +} + + +bool sat_solver_simplify(sat_solver* s) +{ + clause** reasons; + int type; + + assert(sat_solver_dlevel(s) == 0); + + if (sat_solver_propagate(s) != 0) + return false; + + if (s->qhead == s->simpdb_assigns || s->simpdb_props > 0) + return true; + + reasons = s->reasons; + for (type = 0; type < 2; type++){ + vecp* cs = type ? &s->learnts : &s->clauses; + clause** cls = (clause**)vecp_begin(cs); + + int i, j; + for (j = i = 0; i < vecp_size(cs); i++){ + if (reasons[lit_var(*clause_begin(cls[i]))] != cls[i] && + clause_simplify(s,cls[i]) == l_True) + clause_remove(s,cls[i]); + else + cls[j++] = cls[i]; + } + vecp_resize(cs,j); + } + + s->simpdb_assigns = s->qhead; + // (shouldn't depend on 'stats' really, but it will do for now) + s->simpdb_props = (int)(s->stats.clauses_literals + s->stats.learnts_literals); + + return true; +} + + +int sat_solver_solve(sat_solver* s, lit* begin, lit* end) +{ + double nof_conflicts = 100; + double nof_learnts = sat_solver_nclauses(s) / 3; + lbool status = l_Undef; + lbool* values = s->assigns; + lit* i; + + //printf("solve: "); printlits(begin, end); printf("\n"); + for (i = begin; i < end; i++){ + switch (lit_sign(*i) ? -values[lit_var(*i)] : values[lit_var(*i)]){ + case 1: /* l_True: */ + break; + case 0: /* l_Undef */ + assume(s, *i); + if (sat_solver_propagate(s) == NULL) + break; + // falltrough + case -1: /* l_False */ + sat_solver_canceluntil(s, 0); + return l_False; + } + } + + s->root_level = sat_solver_dlevel(s); + + if (s->verbosity >= 1){ + printf("==================================[MINISAT]===================================\n"); + printf("| Conflicts | ORIGINAL | LEARNT | Progress |\n"); + printf("| | Clauses Literals | Limit Clauses Literals Lit/Cl | |\n"); + printf("==============================================================================\n"); + } + + while (status == l_Undef){ + double Ratio = (s->stats.learnts == 0)? 0.0 : + s->stats.learnts_literals / (double)s->stats.learnts; + + if (s->verbosity >= 1){ + printf("| %9.0f | %7.0f %8.0f | %7.0f %7.0f %8.0f %7.1f | %6.3f %% |\n", + (double)s->stats.conflicts, + (double)s->stats.clauses, + (double)s->stats.clauses_literals, + (double)nof_learnts, + (double)s->stats.learnts, + (double)s->stats.learnts_literals, + Ratio, + s->progress_estimate*100); + fflush(stdout); + } + status = sat_solver_search(s,(int)nof_conflicts, (int)nof_learnts); + nof_conflicts *= 1.5; + nof_learnts *= 1.1; + } + if (s->verbosity >= 1) + printf("==============================================================================\n"); + + sat_solver_canceluntil(s,0); + return status; +} + + +int sat_solver_nvars(sat_solver* s) +{ + return s->size; +} + + +int sat_solver_nclauses(sat_solver* s) +{ + return vecp_size(&s->clauses); +} + + +int sat_solver_nconflicts(sat_solver* s) +{ + return (int)s->stats.conflicts; +} + +//================================================================================================= +// Sorting functions (sigh): + +static inline void selectionsort(void** array, int size, int(*comp)(const void *, const void *)) +{ + int i, j, best_i; + void* tmp; + + for (i = 0; i < size-1; i++){ + best_i = i; + for (j = i+1; j < size; j++){ + if (comp(array[j], array[best_i]) < 0) + best_i = j; + } + tmp = array[i]; array[i] = array[best_i]; array[best_i] = tmp; + } +} + + +static void sortrnd(void** array, int size, int(*comp)(const void *, const void *), double* seed) +{ + if (size <= 15) + selectionsort(array, size, comp); + + else{ + void* pivot = array[irand(seed, size)]; + void* tmp; + int i = -1; + int j = size; + + for(;;){ + do i++; while(comp(array[i], pivot)<0); + do j--; while(comp(pivot, array[j])<0); + + if (i >= j) break; + + tmp = array[i]; array[i] = array[j]; array[j] = tmp; + } + + sortrnd(array , i , comp, seed); + sortrnd(&array[i], size-i, comp, seed); + } +} + +void sat_solver_sort(void** array, int size, int(*comp)(const void *, const void *)) +{ + double seed = 91648253; + sortrnd(array,size,comp,&seed); +} diff --git a/src/temp/ivy/satSolver.h b/src/temp/ivy/satSolver.h new file mode 100644 index 00000000..401a28e7 --- /dev/null +++ b/src/temp/ivy/satSolver.h @@ -0,0 +1,141 @@ +/************************************************************************************************** +MiniSat -- Copyright (c) 2005, Niklas Sorensson +http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/ + +Permission is hereby granted, free of charge, to any person obtaining a copy of this software and +associated documentation files (the "Software"), to deal in the Software without restriction, +including without limitation the rights to use, copy, modify, merge, publish, distribute, +sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all copies or +substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT +NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, +DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT +OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +**************************************************************************************************/ +// Modified to compile with MS Visual Studio 6.0 by Alan Mishchenko + +#ifndef satSolver_h +#define satSolver_h + +#ifdef _WIN32 +#define inline __inline // compatible with MS VS 6.0 +#endif + +#include "satVec.h" + +//================================================================================================= +// Simple types: + +// does not work for c++ +typedef int bool; +static const bool true = 1; +static const bool false = 0; + +typedef int lit; +typedef char lbool; + +#ifdef _WIN32 +typedef signed __int64 sint64; // compatible with MS VS 6.0 +#else +typedef long long sint64; +#endif + +static const int var_Undef = -1; +static const lit lit_Undef = -2; + +static const lbool l_Undef = 0; +static const lbool l_True = 1; +static const lbool l_False = -1; + +static inline lit toLit (int v) { return v + v; } +static inline lit toLitCond(int v, int c) { return v + v + (c != 0); } +static inline lit lit_neg (lit l) { return l ^ 1; } +static inline int lit_var (lit l) { return l >> 1; } +static inline int lit_sign (lit l) { return l & 1; } + + +//================================================================================================= +// Public interface: + +struct sat_solver_t; +typedef struct sat_solver_t sat_solver; + +extern sat_solver* sat_solver_new(void); +extern void sat_solver_delete(sat_solver* s); + +extern bool sat_solver_addclause(sat_solver* s, lit* begin, lit* end); +extern bool sat_solver_simplify(sat_solver* s); +extern int sat_solver_solve(sat_solver* s, lit* begin, lit* end); + +extern int sat_solver_nvars(sat_solver* s); +extern int sat_solver_nclauses(sat_solver* s); +extern int sat_solver_nconflicts(sat_solver* s); + +extern void sat_solver_setnvars(sat_solver* s,int n); + +struct stats_t +{ + sint64 starts, decisions, propagations, inspects, conflicts; + sint64 clauses, clauses_literals, learnts, learnts_literals, max_literals, tot_literals; +}; +typedef struct stats_t stats; + +extern void Sat_SolverWriteDimacs( sat_solver * p, char * pFileName, lit* assumptionsBegin, lit* assumptionsEnd, int incrementVars ); +extern void Sat_SolverPrintStats( FILE * pFile, sat_solver * p ); + +//================================================================================================= +// Solver representation: + +struct clause_t; +typedef struct clause_t clause; + +struct sat_solver_t +{ + int size; // nof variables + int cap; // size of varmaps + int qhead; // Head index of queue. + int qtail; // Tail index of queue. + + // clauses + vecp clauses; // List of problem constraints. (contains: clause*) + vecp learnts; // List of learnt clauses. (contains: clause*) + + // activities + double var_inc; // Amount to bump next variable with. + double var_decay; // INVERSE decay factor for variable activity: stores 1/decay. + float cla_inc; // Amount to bump next clause with. + float cla_decay; // INVERSE decay factor for clause activity: stores 1/decay. + + vecp* wlists; // + double* activity; // A heuristic measurement of the activity of a variable. + lbool* assigns; // Current values of variables. + int* orderpos; // Index in variable order. + clause** reasons; // + int* levels; // + lit* trail; + + clause* binary; // A temporary binary clause + lbool* tags; // + veci tagged; // (contains: var) + veci stack; // (contains: var) + + veci order; // Variable order. (heap) (contains: var) + veci trail_lim; // Separator indices for different decision levels in 'trail'. (contains: int) + veci model; // If problem is solved, this vector contains the model (contains: lbool). + + int root_level; // Level of first proper decision. + int simpdb_assigns;// Number of top-level assignments at last 'simplifyDB()'. + int simpdb_props; // Number of propagations before next 'simplifyDB()'. + double random_seed; + double progress_estimate; + int verbosity; // Verbosity level. 0=silent, 1=some progress report, 2=everything + + stats stats; +}; + +#endif diff --git a/src/temp/ivy/satUtil.c b/src/temp/ivy/satUtil.c new file mode 100644 index 00000000..f2b78fe6 --- /dev/null +++ b/src/temp/ivy/satUtil.c @@ -0,0 +1,161 @@ +/**CFile**************************************************************** + + FileName [satUtil.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [C-language MiniSat solver.] + + Synopsis [Additional SAT solver procedures.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: satUtil.c,v 1.4 2005/09/16 22:55:03 casem Exp $] + +***********************************************************************/ + +#include <stdio.h> +#include <assert.h> +#include "satSolver.h" +#include "extra.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +struct clause_t +{ + int size_learnt; + lit lits[0]; +}; + +static inline int clause_size( clause* c ) { return c->size_learnt >> 1; } +static inline lit* clause_begin( clause* c ) { return c->lits; } + +static void Sat_SolverClauseWriteDimacs( FILE * pFile, clause * pC, bool fIncrement ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Write the clauses in the solver into a file in DIMACS format.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sat_SolverWriteDimacs( sat_solver * p, char * pFileName, lit* assumptionsBegin, lit* assumptionsEnd, int incrementVars ) +{ + FILE * pFile; + void ** pClauses; + int nClauses, i; + + // count the number of clauses + nClauses = p->clauses.size + p->learnts.size; + for ( i = 0; i < p->size; i++ ) + if ( p->levels[i] == 0 && p->assigns[i] != l_Undef ) + nClauses++; + + // start the file + pFile = fopen( pFileName, "wb" ); + if ( pFile == NULL ) + { + printf( "Sat_SolverWriteDimacs(): Cannot open the ouput file.\n" ); + return; + } + fprintf( pFile, "c CNF generated by ABC on %s\n", Extra_TimeStamp() ); + fprintf( pFile, "p cnf %d %d\n", p->size, nClauses ); + + // write the original clauses + nClauses = p->clauses.size; + pClauses = p->clauses.ptr; + for ( i = 0; i < nClauses; i++ ) + Sat_SolverClauseWriteDimacs( pFile, pClauses[i], incrementVars ); + + // write the learned clauses + nClauses = p->learnts.size; + pClauses = p->learnts.ptr; + for ( i = 0; i < nClauses; i++ ) + Sat_SolverClauseWriteDimacs( pFile, pClauses[i], incrementVars ); + + // write zero-level assertions + for ( i = 0; i < p->size; i++ ) + if ( p->levels[i] == 0 && p->assigns[i] != l_Undef ) + fprintf( pFile, "%s%d%s\n", + (p->assigns[i] == l_False)? "-": "", + i + (int)(incrementVars>0), + (incrementVars) ? " 0" : ""); + + // write the assumptions + if (assumptionsBegin) { + for (; assumptionsBegin != assumptionsEnd; assumptionsBegin++) { + fprintf( pFile, "%s%d%s\n", + lit_sign(*assumptionsBegin)? "-": "", + lit_var(*assumptionsBegin) + (int)(incrementVars>0), + (incrementVars) ? " 0" : ""); + } + } + + fprintf( pFile, "\n" ); + fclose( pFile ); +} + +/**Function************************************************************* + + Synopsis [Writes the given clause in a file in DIMACS format.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sat_SolverClauseWriteDimacs( FILE * pFile, clause * pC, bool fIncrement ) +{ + lit * pLits = clause_begin(pC); + int nLits = clause_size(pC); + int i; + + for ( i = 0; i < nLits; i++ ) + fprintf( pFile, "%s%d ", (lit_sign(pLits[i])? "-": ""), lit_var(pLits[i]) + (int)(fIncrement>0) ); + if ( fIncrement ) + fprintf( pFile, "0" ); + fprintf( pFile, "\n" ); +} + +/**Function************************************************************* + + Synopsis [Writes the given clause in a file in DIMACS format.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sat_SolverPrintStats( FILE * pFile, sat_solver * p ) +{ + printf( "starts : %d\n", (int)p->stats.starts ); + printf( "conflicts : %d\n", (int)p->stats.conflicts ); + printf( "decisions : %d\n", (int)p->stats.decisions ); + printf( "propagations : %d\n", (int)p->stats.propagations ); + printf( "inspects : %d\n", (int)p->stats.inspects ); +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/temp/ivy/satVec.h b/src/temp/ivy/satVec.h new file mode 100644 index 00000000..ffa9c431 --- /dev/null +++ b/src/temp/ivy/satVec.h @@ -0,0 +1,83 @@ +/************************************************************************************************** +MiniSat -- Copyright (c) 2005, Niklas Sorensson +http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/ + +Permission is hereby granted, free of charge, to any person obtaining a copy of this software and +associated documentation files (the "Software"), to deal in the Software without restriction, +including without limitation the rights to use, copy, modify, merge, publish, distribute, +sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all copies or +substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT +NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, +DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT +OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +**************************************************************************************************/ +// Modified to compile with MS Visual Studio 6.0 by Alan Mishchenko + +#ifndef satVec_h +#define satVec_h + +#include <stdlib.h> + +// vector of 32-bit intergers (added for 64-bit portability) +struct veci_t { + int size; + int cap; + int* ptr; +}; +typedef struct veci_t veci; + +static inline void veci_new (veci* v) { + v->size = 0; + v->cap = 4; + v->ptr = (int*)malloc(sizeof(int)*v->cap); +} + +static inline void veci_delete (veci* v) { free(v->ptr); } +static inline int* veci_begin (veci* v) { return v->ptr; } +static inline int veci_size (veci* v) { return v->size; } +static inline void veci_resize (veci* v, int k) { v->size = k; } // only safe to shrink !! +static inline void veci_push (veci* v, int e) +{ + if (v->size == v->cap) { + int newsize = v->cap * 2+1; + v->ptr = (int*)realloc(v->ptr,sizeof(int)*newsize); + v->cap = newsize; } + v->ptr[v->size++] = e; +} + + +// vector of 32- or 64-bit pointers +struct vecp_t { + int size; + int cap; + void** ptr; +}; +typedef struct vecp_t vecp; + +static inline void vecp_new (vecp* v) { + v->size = 0; + v->cap = 4; + v->ptr = (void**)malloc(sizeof(void*)*v->cap); +} + +static inline void vecp_delete (vecp* v) { free(v->ptr); } +static inline void** vecp_begin (vecp* v) { return v->ptr; } +static inline int vecp_size (vecp* v) { return v->size; } +static inline void vecp_resize (vecp* v, int k) { v->size = k; } // only safe to shrink !! +static inline void vecp_push (vecp* v, void* e) +{ + if (v->size == v->cap) { + int newsize = v->cap * 2+1; + v->ptr = (void**)realloc(v->ptr,sizeof(void*)*newsize); + v->cap = newsize; } + v->ptr[v->size++] = e; +} + + +#endif diff --git a/src/temp/player/playerToAbc.c b/src/temp/player/playerToAbc.c index e06eca28..7c6ab114 100644 --- a/src/temp/player/playerToAbc.c +++ b/src/temp/player/playerToAbc.c @@ -91,6 +91,7 @@ void * Abc_NtkPlayer( void * pNtk, int nLutMax, int nPlaMax, int RankCost, int f Ivy_FastMapPerform( pMan, nLutMax ); // convert from the extended AIG manager into an SOP network pNtkNew = Ivy_ManToAbc( pNtk, pMan, NULL, fFastMode ); +// pNtkNew = NULL; Ivy_FastMapStop( pMan ); } else @@ -104,7 +105,7 @@ void * Abc_NtkPlayer( void * pNtk, int nLutMax, int nPlaMax, int RankCost, int f } Ivy_ManStop( pMan ); // chech the resulting network - if ( !Abc_NtkCheck( pNtkNew ) ) + if ( pNtkNew && !Abc_NtkCheck( pNtkNew ) ) { printf( "Abc_NtkPlayer: The network check has failed.\n" ); Abc_NtkDelete( pNtkNew ); |