diff options
38 files changed, 2374 insertions, 114 deletions
@@ -1166,6 +1166,10 @@ SOURCE=.\src\sat\asat\jfront.c # End Source File # Begin Source File +SOURCE=.\src\sat\asat\satTrace.c +# End Source File +# Begin Source File + SOURCE=.\src\sat\asat\solver.c # End Source File # Begin Source File @@ -1345,6 +1349,18 @@ SOURCE=.\src\sat\bsat\satUtil.c SOURCE=.\src\sat\bsat\satVec.h # End Source File # End Group +# Begin Group "proof" + +# PROP Default_Filter "" +# Begin Source File + +SOURCE=.\src\sat\proof\pr.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\proof\pr.h +# End Source File +# End Group # End Group # Begin Group "opt" @@ -1,7 +1,7 @@ # global parameters set check # checks intermediate networks #set checkfio # prints warnings when fanins/fanouts are duplicated -#set checkread # checks new networks after reading from file +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 progressbar # display the progress bar diff --git a/src/aig/ivy/ivyCut.c b/src/aig/ivy/ivyCut.c index d918c96c..e257d8a6 100644 --- a/src/aig/ivy/ivyCut.c +++ b/src/aig/ivy/ivyCut.c @@ -930,6 +930,8 @@ Ivy_Store_t * Ivy_NodeFindCutsAll( Ivy_Man_t * p, Ivy_Obj_t * pObj, int nLeaves */ iLeaf0 = Ivy_ObjId( Ivy_ObjRealFanin(Ivy_ObjFanin0(pLeaf)) ); iLeaf1 = Ivy_ObjId( Ivy_ObjRealFanin(Ivy_ObjFanin1(pLeaf)) ); +// if ( iLeaf0 == iLeaf1 ) // strange situation observed on Jan 18, 2007 +// continue; if ( !Ivy_NodeCutPrescreen( pCut, iLeaf0, iLeaf1 ) ) continue; if ( iLeaf0 > iLeaf1 ) diff --git a/src/aig/ivy/ivyFraig.c b/src/aig/ivy/ivyFraig.c index ce21c269..e9a65881 100644 --- a/src/aig/ivy/ivyFraig.c +++ b/src/aig/ivy/ivyFraig.c @@ -252,7 +252,7 @@ int Ivy_FraigProve( Ivy_Man_t ** ppManAig, void * pPars ) Prove_Params_t * pParams = pPars; Ivy_FraigParams_t Params, * pIvyParams = &Params; Ivy_Man_t * pManAig, * pManTemp; - int RetValue, nIter, Counter, clk, timeStart = clock(); + int RetValue, nIter, clk, timeStart = clock();//, Counter; sint64 nSatConfs, nSatInspects; // start the network and parameters @@ -314,12 +314,14 @@ int Ivy_FraigProve( Ivy_Man_t ** ppManAig, void * pPars ) // try rewriting if ( pParams->fUseRewriting ) - { + { // bug in Ivy_NodeFindCutsAll() when leaves are identical! +/* clk = clock(); Counter = (int)(pParams->nRewritingLimitStart * pow(pParams->nRewritingLimitMulti,nIter)); pManAig = Ivy_ManRwsat( pManAig, 0 ); RetValue = Ivy_FraigMiterStatus( pManAig ); Ivy_FraigMiterPrint( pManAig, "Rewriting ", clk, pParams->fVerbose ); +*/ } if ( RetValue >= 0 ) break; @@ -368,6 +370,15 @@ int Ivy_FraigProve( Ivy_Man_t ** ppManAig, void * pPars ) s_nInsLimitGlobal = 0; RetValue = Ivy_FraigMiterStatus( pManAig ); Ivy_FraigMiterPrint( pManAig, "SAT solving", clk, pParams->fVerbose ); + // make sure that the sover never returns "undecided" when infinite resource limits are set + if( RetValue == -1 && pParams->nTotalInspectLimit == 0 && + pParams->nTotalBacktrackLimit == 0 ) + { + extern void Prove_ParamsPrint( Prove_Params_t * pParams ); + Prove_ParamsPrint( pParams ); + printf("ERROR: ABC has returned \"undecided\" in spite of no limits...\n"); + exit(1); + } } // assign the model if it was proved by rewriting (const 1 miter) diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h index 5774afbc..849a888a 100644 --- a/src/base/abc/abc.h +++ b/src/base/abc/abc.h @@ -570,9 +570,9 @@ extern void Abc_NtkFraigStoreClean(); /*=== abcFunc.c ==========================================================*/ extern int Abc_NtkSopToBdd( Abc_Ntk_t * pNtk ); extern DdNode * Abc_ConvertSopToBdd( DdManager * dd, char * pSop ); -extern char * Abc_ConvertBddToSop( Extra_MmFlex_t * pMan, DdManager * dd, DdNode * bFuncOn, DdNode * bFuncOnDc, int nFanins, Vec_Str_t * vCube, int fMode ); +extern char * Abc_ConvertBddToSop( Extra_MmFlex_t * pMan, DdManager * dd, DdNode * bFuncOn, DdNode * bFuncOnDc, int nFanins, int fAllPrimes, Vec_Str_t * vCube, int fMode ); extern int Abc_NtkBddToSop( Abc_Ntk_t * pNtk, int fDirect ); -extern void Abc_NodeBddToCnf( Abc_Obj_t * pNode, Extra_MmFlex_t * pMmMan, Vec_Str_t * vCube, char ** ppSop0, char ** ppSop1 ); +extern void Abc_NodeBddToCnf( Abc_Obj_t * pNode, Extra_MmFlex_t * pMmMan, Vec_Str_t * vCube, int fAllPrimes, char ** ppSop0, char ** ppSop1 ); extern int Abc_CountZddCubes( DdManager * dd, DdNode * zCover ); extern void Abc_NtkLogicMakeDirectSops( Abc_Ntk_t * pNtk ); extern int Abc_NtkSopToAig( Abc_Ntk_t * pNtk ); @@ -726,7 +726,7 @@ extern int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, i extern int Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUpdateLevel, int fUseZeros, int fVerbose, int fVeryVerbose ); /*=== abcSat.c ==========================================================*/ extern int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fJFront, int fVerbose, sint64 * pNumConfs, sint64 * pNumInspects ); -extern solver * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk, int fJFront ); +extern solver * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk, int fJFront, int fAllPrimes ); /*=== abcSop.c ==========================================================*/ extern char * Abc_SopRegister( Extra_MmFlex_t * pMan, char * pName ); extern char * Abc_SopStart( Extra_MmFlex_t * pMan, int nCubes, int nVars ); diff --git a/src/base/abc/abcFunc.c b/src/base/abc/abcFunc.c index 59f736e5..421a64cf 100644 --- a/src/base/abc/abcFunc.c +++ b/src/base/abc/abcFunc.c @@ -184,7 +184,7 @@ void Abc_NtkLogicMakeDirectSops( Abc_Ntk_t * pNtk ) if ( Abc_SopIsComplement(pNode->pData) ) { bFunc = Abc_ConvertSopToBdd( dd, pNode->pData ); Cudd_Ref( bFunc ); - pNode->pData = Abc_ConvertBddToSop( pNtk->pManFunc, dd, bFunc, bFunc, Abc_ObjFaninNum(pNode), vCube, 1 ); + pNode->pData = Abc_ConvertBddToSop( pNtk->pManFunc, dd, bFunc, bFunc, Abc_ObjFaninNum(pNode), 0, vCube, 1 ); Cudd_RecursiveDeref( dd, bFunc ); assert( !Abc_SopIsComplement(pNode->pData) ); } @@ -233,7 +233,7 @@ int Abc_NtkBddToSop( Abc_Ntk_t * pNtk, int fDirect ) { assert( pNode->pData ); bFunc = pNode->pData; - pNode->pNext = (Abc_Obj_t *)Abc_ConvertBddToSop( pManNew, dd, bFunc, bFunc, Abc_ObjFaninNum(pNode), vCube, fMode ); + pNode->pNext = (Abc_Obj_t *)Abc_ConvertBddToSop( pManNew, dd, bFunc, bFunc, Abc_ObjFaninNum(pNode), 0, vCube, fMode ); if ( pNode->pNext == NULL ) { Extra_MmFlexStop( pManNew ); @@ -273,7 +273,7 @@ int Abc_NtkBddToSop( Abc_Ntk_t * pNtk, int fDirect ) SeeAlso [] ***********************************************************************/ -char * Abc_ConvertBddToSop( Extra_MmFlex_t * pMan, DdManager * dd, DdNode * bFuncOn, DdNode * bFuncOnDc, int nFanins, Vec_Str_t * vCube, int fMode ) +char * Abc_ConvertBddToSop( Extra_MmFlex_t * pMan, DdManager * dd, DdNode * bFuncOn, DdNode * bFuncOnDc, int nFanins, int fAllPrimes, Vec_Str_t * vCube, int fMode ) { int fVerify = 0; char * pSop; @@ -301,6 +301,7 @@ char * Abc_ConvertBddToSop( Extra_MmFlex_t * pMan, DdManager * dd, DdNode * bFun if ( fMode == -1 ) { // try both phases + assert( fAllPrimes == 0 ); // get the ZDD of the negative polarity bCover = Cudd_zddIsop( dd, Cudd_Not(bFuncOnDc), Cudd_Not(bFuncOn), &zCover0 ); @@ -335,20 +336,36 @@ char * Abc_ConvertBddToSop( Extra_MmFlex_t * pMan, DdManager * dd, DdNode * bFun else if ( fMode == 0 ) { // get the ZDD of the negative polarity - bCover = Cudd_zddIsop( dd, Cudd_Not(bFuncOnDc), Cudd_Not(bFuncOn), &zCover ); - Cudd_Ref( zCover ); - Cudd_Ref( bCover ); - Cudd_RecursiveDeref( dd, bCover ); + if ( fAllPrimes ) + { + zCover = Extra_zddPrimes( dd, Cudd_Not(bFuncOnDc) ); + Cudd_Ref( zCover ); + } + else + { + bCover = Cudd_zddIsop( dd, Cudd_Not(bFuncOnDc), Cudd_Not(bFuncOn), &zCover ); + Cudd_Ref( zCover ); + Cudd_Ref( bCover ); + Cudd_RecursiveDeref( dd, bCover ); + } nCubes = Abc_CountZddCubes( dd, zCover ); fPhase = 0; } else if ( fMode == 1 ) { // get the ZDD of the positive polarity - bCover = Cudd_zddIsop( dd, bFuncOn, bFuncOnDc, &zCover ); - Cudd_Ref( zCover ); - Cudd_Ref( bCover ); - Cudd_RecursiveDeref( dd, bCover ); + if ( fAllPrimes ) + { + zCover = Extra_zddPrimes( dd, bFuncOnDc ); + Cudd_Ref( zCover ); + } + else + { + bCover = Cudd_zddIsop( dd, bFuncOn, bFuncOnDc, &zCover ); + Cudd_Ref( zCover ); + Cudd_Ref( bCover ); + Cudd_RecursiveDeref( dd, bCover ); + } nCubes = Abc_CountZddCubes( dd, zCover ); fPhase = 1; } @@ -462,11 +479,11 @@ int Abc_ConvertZddToSop( DdManager * dd, DdNode * zCover, char * pSop, int nFani SeeAlso [] ***********************************************************************/ -void Abc_NodeBddToCnf( Abc_Obj_t * pNode, Extra_MmFlex_t * pMmMan, Vec_Str_t * vCube, char ** ppSop0, char ** ppSop1 ) +void Abc_NodeBddToCnf( Abc_Obj_t * pNode, Extra_MmFlex_t * pMmMan, Vec_Str_t * vCube, int fAllPrimes, char ** ppSop0, char ** ppSop1 ) { assert( Abc_NtkIsBddLogic(pNode->pNtk) ); - *ppSop0 = Abc_ConvertBddToSop( pMmMan, pNode->pNtk->pManFunc, pNode->pData, pNode->pData, Abc_ObjFaninNum(pNode), vCube, 0 ); - *ppSop1 = Abc_ConvertBddToSop( pMmMan, pNode->pNtk->pManFunc, pNode->pData, pNode->pData, Abc_ObjFaninNum(pNode), vCube, 1 ); + *ppSop0 = Abc_ConvertBddToSop( pMmMan, pNode->pNtk->pManFunc, pNode->pData, pNode->pData, Abc_ObjFaninNum(pNode), fAllPrimes, vCube, 0 ); + *ppSop1 = Abc_ConvertBddToSop( pMmMan, pNode->pNtk->pManFunc, pNode->pData, pNode->pData, Abc_ObjFaninNum(pNode), fAllPrimes, vCube, 1 ); } diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index ff63bbd9..f6c180da 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -72,6 +72,7 @@ static int Abc_CommandComb ( 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_CommandAndPos ( 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 ); @@ -207,6 +208,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", "andpos", Abc_CommandAndPos, 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 ); @@ -2038,25 +2040,30 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv ) FILE * pOut, * pErr; Abc_Ntk_t * pNtk, * pNtkRes; int nLutSize, nCutsMax, c; + int nFlowIters, nAreaIters; int fArea; int fUseBdds; int fUseSops; + int fUseCnfs; int fVerbose; - extern Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nLutSize, int nCutsMax, int fArea, int fUseBdds, int fUseSops, int fVerbose ); + extern Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nLutSize, int nCutsMax, int nFlowIters, int nAreaIters, int fArea, int fUseBdds, int fUseSops, int fUseCnfs, int fVerbose ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); // set defaults - nLutSize = 8; - nCutsMax = 5; - fArea = 0; - fUseBdds = 0; - fUseSops = 0; - fVerbose = 0; + nLutSize = 8; + nCutsMax = 5; + nFlowIters = 1; + nAreaIters = 1; + fArea = 0; + fUseBdds = 0; + fUseSops = 0; + fUseCnfs = 0; + fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "KCabsvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "KCFAabscvh" ) ) != EOF ) { switch ( c ) { @@ -2082,6 +2089,28 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( nCutsMax < 0 ) goto usage; break; + case 'F': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-F\" should be followed by a positive integer.\n" ); + goto usage; + } + nFlowIters = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nFlowIters < 0 ) + goto usage; + break; + case 'A': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-A\" should be followed by a positive integer.\n" ); + goto usage; + } + nAreaIters = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nAreaIters < 0 ) + goto usage; + break; case 'a': fArea ^= 1; break; @@ -2091,6 +2120,9 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv ) case 's': fUseSops ^= 1; break; + case 'c': + fUseCnfs ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -2101,9 +2133,9 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv ) } } - if ( fUseBdds && fUseSops ) + if ( fUseBdds && fUseSops || fUseBdds && fUseCnfs || fUseSops && fUseCnfs ) { - fprintf( pErr, "Cannot optimize both BDDs and SOPs at the same time.\n" ); + fprintf( pErr, "Cannot optimize two parameters at the same time.\n" ); return 1; } @@ -2131,7 +2163,7 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv ) } // get the new network - pNtkRes = Abc_NtkRenode( pNtk, nLutSize, nCutsMax, fArea, fUseBdds, fUseSops, fVerbose ); + pNtkRes = Abc_NtkRenode( pNtk, nLutSize, nCutsMax, nFlowIters, nAreaIters, fArea, fUseBdds, fUseSops, fUseCnfs, fVerbose ); if ( pNtkRes == NULL ) { fprintf( pErr, "Renoding has failed.\n" ); @@ -2142,13 +2174,16 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: renode [-K num] [-C num] [-sbav]\n" ); + fprintf( pErr, "usage: renode [-K num] [-C num] [-F num] [-A num] [-sbcav]\n" ); fprintf( pErr, "\t transforms the AIG into a logic network with larger nodes\n" ); fprintf( pErr, "\t while minimizing the number of FF literals of the node SOPs\n" ); fprintf( pErr, "\t-K num : the max cut size for renoding (2 < num < %d) [default = %d]\n", IF_MAX_FUNC_LUTSIZE+1, nLutSize ); fprintf( pErr, "\t-C num : the max number of cuts used at a node (1 < num < 2^12) [default = %d]\n", nCutsMax ); + fprintf( pErr, "\t-F num : the number of area flow recovery iterations (num >= 0) [default = %d]\n", nFlowIters ); + fprintf( pErr, "\t-A num : the number of exact area recovery iterations (num >= 0) [default = %d]\n", nAreaIters ); fprintf( pErr, "\t-s : toggles minimizing SOP cubes instead of FF lits [default = %s]\n", fUseSops? "yes": "no" ); fprintf( pErr, "\t-b : toggles minimizing BDD nodes instead of FF lits [default = %s]\n", fUseBdds? "yes": "no" ); + fprintf( pErr, "\t-c : toggles minimizing CNF clauses instead of FF lits [default = %s]\n", fUseCnfs? "yes": "no" ); fprintf( pErr, "\t-a : toggles area-oriented mapping [default = %s]\n", fArea? "yes": "no" ); fprintf( pErr, "\t-v : print verbose information [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); @@ -3450,7 +3485,7 @@ int Abc_CommandOrPos( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Ntk_t * pNtk;//, * pNtkRes; int fComb; int c; - extern int Abc_NtkOrPos( Abc_Ntk_t * pNtk ); + extern int Abc_NtkCombinePos( Abc_Ntk_t * pNtk, int fAnd ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); @@ -3489,7 +3524,7 @@ int Abc_CommandOrPos( Abc_Frame_t * pAbc, int argc, char ** argv ) } // get the new network - if ( !Abc_NtkOrPos( pNtk ) ) + if ( !Abc_NtkCombinePos( pNtk, 0 ) ) { fprintf( pErr, "ORing the POs has failed.\n" ); return 1; @@ -3517,6 +3552,79 @@ usage: SeeAlso [] ***********************************************************************/ +int Abc_CommandAndPos( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk;//, * pNtkRes; + int fComb; + int c; + extern int Abc_NtkCombinePos( Abc_Ntk_t * pNtk, int fAnd ); + + 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; + } + } + + if ( !Abc_NtkIsStrash(pNtk) ) + { + fprintf( pErr, "The network is not strashed.\n" ); + return 1; + } + + if ( Abc_NtkPoNum(pNtk) == 1 ) + { + fprintf( pErr, "The network already has one PO.\n" ); + return 1; + } + + if ( Abc_NtkLatchNum(pNtk) ) + { + fprintf( pErr, "The miter has latches. ORing is not performed.\n" ); + return 1; + } + + // get the new network + if ( !Abc_NtkCombinePos( pNtk, 1 ) ) + { + fprintf( pErr, "ANDing the POs has failed.\n" ); + return 1; + } + // replace the current network +// Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); + return 0; + +usage: + fprintf( pErr, "usage: andpos [-h]\n" ); + fprintf( pErr, "\t creates single-output miter by ANDing the POs 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"); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ int Abc_CommandAppend( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; @@ -5286,6 +5394,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) // extern Abc_Ntk_t * Abc_NtkNewAig( Abc_Ntk_t * pNtk ); // extern Abc_Ntk_t * Abc_NtkIvy( Abc_Ntk_t * pNtk ); extern void Abc_NtkMaxFlowTest( Abc_Ntk_t * pNtk ); + extern int Pr_ManProofTest( char * pFileName ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); @@ -5379,7 +5488,8 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) // replace the current network Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); */ - Abc_NtkMaxFlowTest( pNtk ); +// Abc_NtkMaxFlowTest( pNtk ); + Pr_ManProofTest( "trace.cnf" ); return 0; usage: @@ -7524,6 +7634,8 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv ) // user-controlable paramters pPars->nLutSize = 4; pPars->nCutsMax = 8; + pPars->nFlowIters = 1; + pPars->nAreaIters = 2; pPars->DelayTarget = -1; pPars->fPreprocess = 1; pPars->fArea = 0; @@ -7542,7 +7654,7 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv ) pPars->pFuncCost = NULL; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "KCDpaflrstvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "KCFADpaflrstvh" ) ) != EOF ) { switch ( c ) { @@ -7570,6 +7682,28 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pPars->nCutsMax < 0 ) goto usage; break; + case 'F': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-F\" should be followed by a positive integer.\n" ); + goto usage; + } + pPars->nFlowIters = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nFlowIters < 0 ) + goto usage; + break; + case 'A': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-A\" should be followed by a positive integer.\n" ); + goto usage; + } + pPars->nAreaIters = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nAreaIters < 0 ) + goto usage; + break; case 'D': if ( globalUtilOptind >= argc ) { @@ -7705,10 +7839,12 @@ usage: sprintf( LutSize, "library" ); else sprintf( LutSize, "%d", pPars->nLutSize ); - fprintf( pErr, "usage: if [-K num] [-C num] [-D float] [-pafrsvh]\n" ); + fprintf( pErr, "usage: if [-K num] [-C num] [-F num] [-A num] [-D float] [-pafrsvh]\n" ); fprintf( pErr, "\t performs FPGA technology mapping of the network\n" ); fprintf( pErr, "\t-K num : the number of LUT inputs (2 < num < %d) [default = %s]\n", IF_MAX_LUTSIZE+1, LutSize ); fprintf( pErr, "\t-C num : the max number of cuts to use (1 < num < 2^12) [default = %d]\n", pPars->nCutsMax ); + fprintf( pErr, "\t-F num : the number of area flow recovery iterations (num >= 0) [default = %d]\n", pPars->nFlowIters ); + fprintf( pErr, "\t-A num : the number of exact area recovery iterations (num >= 0) [default = %d]\n", pPars->nAreaIters ); fprintf( pErr, "\t-D float : sets the delay constraint for the mapping [default = %s]\n", Buffer ); fprintf( pErr, "\t-p : toggles preprocessing using several starting points [default = %s]\n", pPars->fPreprocess? "yes": "no" ); fprintf( pErr, "\t-a : toggles area-oriented mapping [default = %s]\n", pPars->fArea? "yes": "no" ); @@ -9143,11 +9279,9 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv ) } else { - Abc_Ntk_t * pTemp; - pTemp = Abc_NtkStrash( pNtk, 0, 0 ); - RetValue = Abc_NtkMiterSat( pTemp, (sint64)nConfLimit, (sint64)nInsLimit, fJFront, fVerbose, NULL, NULL ); - pNtk->pModel = pTemp->pModel; pTemp->pModel = NULL; - Abc_NtkDelete( pTemp ); + assert( Abc_NtkIsLogic(pNtk) ); + Abc_NtkLogicToBdd( pNtk ); + RetValue = Abc_NtkMiterSat( pNtk, (sint64)nConfLimit, (sint64)nInsLimit, fJFront, fVerbose, NULL, NULL ); } // verify that the pattern is correct diff --git a/src/base/abci/abcIf.c b/src/base/abci/abcIf.c index 871bf148..887f6cc9 100644 --- a/src/base/abci/abcIf.c +++ b/src/base/abci/abcIf.c @@ -31,6 +31,8 @@ static Abc_Ntk_t * Abc_NtkFromIf( If_Man_t * pIfMan, Abc_Ntk_t * pNtk ); static Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t * pIfObj, Vec_Int_t * vCover ); static Hop_Obj_t * Abc_NodeIfToHop( Hop_Man_t * pHopMan, If_Man_t * pIfMan, If_Obj_t * pIfObj ); static Vec_Ptr_t * Abc_NtkFindGoodOrder( Abc_Ntk_t * pNtk ); + +extern void Abc_NtkBddReorder( Abc_Ntk_t * pNtk, int fVerbose ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -122,6 +124,11 @@ If_Man_t * Abc_NtkToIf( Abc_Ntk_t * pNtk, If_Par_t * pPars ) // start the mapping manager and set its parameters pIfMan = If_ManStart( pPars ); + // print warning about excessive memory usage + if ( 1.0 * Abc_NtkObjNum(pNtk) * pIfMan->nEntrySize / (1<<30) > 0.5 ) + printf( "Warning: The mapper is about to allocate %.1f Gb for to represent %d cuts per node.\n", + 1.0 * Abc_NtkObjNum(pNtk) * pIfMan->nEntrySize / (1<<30), pPars->nCutsMax ); + // create PIs and remember them in the old nodes Abc_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)If_ManConst1( pIfMan ); Abc_NtkForEachCi( pNtk, pNode, i ) @@ -177,7 +184,7 @@ Abc_Ntk_t * Abc_NtkFromIf( If_Man_t * pIfMan, Abc_Ntk_t * pNtk ) Vec_Int_t * vCover; int i, nDupGates; // create the new network - if ( pIfMan->pPars->fUseBdds ) + if ( pIfMan->pPars->fUseBdds || pIfMan->pPars->fUseCnfs ) pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_BDD ); else if ( pIfMan->pPars->fUseSops ) pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_SOP ); @@ -206,6 +213,11 @@ Abc_Ntk_t * Abc_NtkFromIf( If_Man_t * pIfMan, Abc_Ntk_t * pNtk ) pNodeNew = (Abc_Obj_t *)If_ObjCopy( If_ManConst1(pIfMan) ); if ( Abc_ObjFanoutNum(pNodeNew) == 0 ) Abc_NtkDeleteObj( pNodeNew ); + // minimize the node + if ( pIfMan->pPars->fUseCnfs || pIfMan->pPars->fUseBdds ) + Abc_NtkSweep( pNtkNew, 0 ); + if ( pIfMan->pPars->fUseBdds ) + Abc_NtkBddReorder( pNtkNew, 0 ); // decouple the PO driver nodes to reduce the number of levels nDupGates = Abc_NtkLogicMakeSimpleCos( pNtkNew, 1 ); // if ( nDupGates && If_ManReadVerbose(pIfMan) ) @@ -239,28 +251,28 @@ Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t // create a new node pNodeNew = Abc_NtkCreateNode( pNtkNew ); pCutBest = If_ObjCutBest( pIfObj ); - If_CutForEachLeaf( pIfMan, pCutBest, pIfLeaf, i ) - Abc_ObjAddFanin( pNodeNew, Abc_NodeFromIf_rec(pNtkNew, pIfMan, pIfLeaf, vCover) ); + if ( pIfMan->pPars->fUseCnfs ) + { + If_CutForEachLeafReverse( pIfMan, pCutBest, pIfLeaf, i ) + Abc_ObjAddFanin( pNodeNew, Abc_NodeFromIf_rec(pNtkNew, pIfMan, pIfLeaf, vCover) ); + } + else + { + If_CutForEachLeaf( pIfMan, pCutBest, pIfLeaf, i ) + Abc_ObjAddFanin( pNodeNew, Abc_NodeFromIf_rec(pNtkNew, pIfMan, pIfLeaf, vCover) ); + } // derive the function of this node if ( pIfMan->pPars->fTruth ) { if ( pIfMan->pPars->fUseBdds ) { - extern void Abc_NodeBddReorder( void * p, Abc_Obj_t * pNode ); // transform truth table into the BDD pNodeNew->pData = Kit_TruthToBdd( pNtkNew->pManFunc, If_CutTruth(pCutBest), If_CutLeaveNum(pCutBest), 0 ); Cudd_Ref(pNodeNew->pData); - if ( pNodeNew->pData == Cudd_ReadLogicZero(pNtkNew->pManFunc) || pNodeNew->pData == Cudd_ReadOne(pNtkNew->pManFunc) ) - { - // replace the node by a constant node - pNodeNew = pNodeNew->pData == Cudd_ReadOne(pNtkNew->pManFunc) ? Abc_NtkCreateNodeConst1(pNtkNew) : Abc_NtkCreateNodeConst0(pNtkNew); - } - else - { - // make sure the node is minimum base - Abc_NodeMinimumBase( pNodeNew ); - // reorder the fanins to minimize the BDD size - Abc_NodeBddReorder( pIfMan->pPars->pReoMan, pNodeNew ); - } + } + else if ( pIfMan->pPars->fUseCnfs ) + { + // transform truth table into the BDD + pNodeNew->pData = Kit_TruthToBdd( pNtkNew->pManFunc, If_CutTruth(pCutBest), If_CutLeaveNum(pCutBest), 1 ); Cudd_Ref(pNodeNew->pData); } else if ( pIfMan->pPars->fUseSops ) { diff --git a/src/base/abci/abcMiter.c b/src/base/abci/abcMiter.c index ddbbf671..15a81723 100644 --- a/src/base/abci/abcMiter.c +++ b/src/base/abci/abcMiter.c @@ -1039,7 +1039,7 @@ int Abc_NtkDemiter( Abc_Ntk_t * pNtk ) /**Function************************************************************* - Synopsis [ORs the outputs.] + Synopsis [Computes OR or AND of the POs.] Description [] @@ -1048,16 +1048,23 @@ int Abc_NtkDemiter( Abc_Ntk_t * pNtk ) SeeAlso [] ***********************************************************************/ -int Abc_NtkOrPos( Abc_Ntk_t * pNtk ) +int Abc_NtkCombinePos( Abc_Ntk_t * pNtk, int fAnd ) { Abc_Obj_t * pNode, * pMiter; int i; assert( Abc_NtkIsStrash(pNtk) ); assert( Abc_NtkLatchNum(pNtk) == 0 ); - // OR the POs - pMiter = Abc_ObjNot( Abc_AigConst1(pNtk) ); + // start the result + if ( fAnd ) + pMiter = Abc_AigConst1(pNtk); + else + pMiter = Abc_ObjNot( Abc_AigConst1(pNtk) ); + // perform operations on the POs Abc_NtkForEachPo( pNtk, pNode, i ) - pMiter = Abc_AigOr( pNtk->pManFunc, pMiter, Abc_ObjChild0(pNode) ); + if ( fAnd ) + pMiter = Abc_AigAnd( pNtk->pManFunc, pMiter, Abc_ObjChild0(pNode) ); + else + pMiter = Abc_AigOr( pNtk->pManFunc, pMiter, Abc_ObjChild0(pNode) ); // remove the POs and their names for ( i = Abc_NtkPoNum(pNtk) - 1; i >= 0; i-- ) Abc_NtkDeleteObj( Abc_NtkPo(pNtk, i) ); diff --git a/src/base/abci/abcRefactor.c b/src/base/abci/abcRefactor.c index 0328d8d3..834e33aa 100644 --- a/src/base/abci/abcRefactor.c +++ b/src/base/abci/abcRefactor.c @@ -233,7 +233,7 @@ p->timeDcs += clock() - clk; // get the SOP of the cut clk = clock(); - pSop = Abc_ConvertBddToSop( NULL, p->dd, bNodeFunc, bNodeFunc, vFanins->nSize, p->vCube, -1 ); + pSop = Abc_ConvertBddToSop( NULL, p->dd, bNodeFunc, bNodeFunc, vFanins->nSize, 0, p->vCube, -1 ); p->timeSop += clock() - clk; // get the factored form diff --git a/src/base/abci/abcRenode.c b/src/base/abci/abcRenode.c index 462d9da3..af3f55cf 100644 --- a/src/base/abci/abcRenode.c +++ b/src/base/abci/abcRenode.c @@ -29,6 +29,7 @@ static int Abc_NtkRenodeEvalBdd( If_Cut_t * pCut ); static int Abc_NtkRenodeEvalSop( If_Cut_t * pCut ); +static int Abc_NtkRenodeEvalCnf( If_Cut_t * pCut ); static int Abc_NtkRenodeEvalAig( If_Cut_t * pCut ); static reo_man * s_pReo = NULL; @@ -50,7 +51,7 @@ static Vec_Int_t * s_vMemory = NULL; SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nFaninMax, int nCubeMax, int fArea, int fUseBdds, int fUseSops, int fVerbose ) +Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nFaninMax, int nCubeMax, int nFlowIters, int nAreaIters, int fArea, int fUseBdds, int fUseSops, int fUseCnfs, int fVerbose ) { extern Abc_Ntk_t * Abc_NtkIf( Abc_Ntk_t * pNtk, If_Par_t * pPars ); If_Par_t Pars, * pPars = &Pars; @@ -64,6 +65,8 @@ Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nFaninMax, int nCubeMax, int fA // user-controlable paramters pPars->nLutSize = nFaninMax; pPars->nCutsMax = nCubeMax; + pPars->nFlowIters = nFlowIters; + pPars->nAreaIters = nAreaIters; pPars->DelayTarget = -1; pPars->fPreprocess = 1; pPars->fArea = fArea; @@ -81,10 +84,16 @@ Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nFaninMax, int nCubeMax, int fA pPars->pTimesArr = NULL; pPars->fUseBdds = fUseBdds; pPars->fUseSops = fUseSops; + pPars->fUseCnfs = fUseCnfs; if ( fUseBdds ) pPars->pFuncCost = Abc_NtkRenodeEvalBdd; else if ( fUseSops ) pPars->pFuncCost = Abc_NtkRenodeEvalSop; + else if ( fUseCnfs ) + { + pPars->fArea = 1; + pPars->pFuncCost = Abc_NtkRenodeEvalCnf; + } else pPars->pFuncCost = Abc_NtkRenodeEvalAig; @@ -176,6 +185,39 @@ int Abc_NtkRenodeEvalSop( If_Cut_t * pCut ) /**Function************************************************************* + Synopsis [Computes the cost based on two ISOPs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkRenodeEvalCnf( If_Cut_t * pCut ) +{ + int i, RetValue, nClauses; + for ( i = 0; i < If_CutLeaveNum(pCut); i++ ) + pCut->pPerm[i] = 1; + // compute ISOP for the positive phase + RetValue = Kit_TruthIsop( If_CutTruth(pCut), If_CutLeaveNum(pCut), s_vMemory, 0 ); + if ( RetValue == -1 ) + return ABC_INFINITY; + assert( RetValue == 0 || RetValue == 1 ); + nClauses = Vec_IntSize( s_vMemory ); + // compute ISOP for the negative phase + Kit_TruthNot( If_CutTruth(pCut), If_CutTruth(pCut), If_CutLeaveNum(pCut) ); + RetValue = Kit_TruthIsop( If_CutTruth(pCut), If_CutLeaveNum(pCut), s_vMemory, 0 ); + Kit_TruthNot( If_CutTruth(pCut), If_CutTruth(pCut), If_CutLeaveNum(pCut) ); + if ( RetValue == -1 ) + return ABC_INFINITY; + assert( RetValue == 0 || RetValue == 1 ); + nClauses += Vec_IntSize( s_vMemory ); + return nClauses; +} + +/**Function************************************************************* + Synopsis [Computes the cost based on the factored form.] Description [] diff --git a/src/base/abci/abcSat.c b/src/base/abci/abcSat.c index 55498288..cf67db6d 100644 --- a/src/base/abci/abcSat.c +++ b/src/base/abci/abcSat.c @@ -24,6 +24,7 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +static solver * Abc_NtkMiterSatCreateLogic( Abc_Ntk_t * pNtk, int fAllPrimes ); extern Vec_Int_t * Abc_NtkGetCiSatVarNums( Abc_Ntk_t * pNtk ); static nMuxes; @@ -53,7 +54,6 @@ int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int if ( pNumInspects ) *pNumInspects = 0; - assert( Abc_NtkIsStrash(pNtk) ); assert( Abc_NtkLatchNum(pNtk) == 0 ); // if ( Abc_NtkPoNum(pNtk) > 1 ) @@ -61,7 +61,7 @@ int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int // load clauses into the solver clk = clock(); - pSat = Abc_NtkMiterSatCreate( pNtk, fJFront ); + pSat = Abc_NtkMiterSatCreate( pNtk, fJFront, 0 ); if ( pSat == NULL ) return 1; // printf( "Created SAT problem with %d variable and %d clauses. ", solver_nvars(pSat), solver_nclauses(pSat) ); @@ -121,6 +121,9 @@ int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int if ( pNumInspects ) *pNumInspects = (int)pSat->solver_stats.inspects; +Sat_SolverTraceWrite( pSat, NULL, NULL, 0 ); +Sat_SolverTraceStop( pSat ); + solver_delete( pSat ); return RetValue; } @@ -660,14 +663,17 @@ Quits : SeeAlso [] ***********************************************************************/ -solver * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk, int fJFront ) +solver * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk, int fJFront, int fAllPrimes ) { solver * pSat; Abc_Obj_t * pNode; int RetValue, i, clk = clock(); - nMuxes = 0; + assert( Abc_NtkIsStrash(pNtk) || Abc_NtkIsBddLogic(pNtk) ); + if ( Abc_NtkIsBddLogic(pNtk) ) + return Abc_NtkMiterSatCreateLogic(pNtk, fAllPrimes); + nMuxes = 0; pSat = solver_new(); RetValue = Abc_NtkMiterSatCreateInt( pSat, pNtk, fJFront ); Abc_NtkForEachObj( pNtk, pNode, i ) @@ -684,6 +690,242 @@ solver * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk, int fJFront ) } + + +/**Function************************************************************* + + Synopsis [Adds clauses for the internal node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NodeAddClauses( solver * pSat, char * pSop0, char * pSop1, Abc_Obj_t * pNode, Vec_Int_t * vVars ) +{ + Abc_Obj_t * pFanin; + int i, c, nFanins; + int RetValue; + char * pCube; + + nFanins = Abc_ObjFaninNum( pNode ); + assert( nFanins == Abc_SopGetVarNum( pSop0 ) ); + +// if ( nFanins == 0 ) + if ( Cudd_Regular(pNode->pData) == Cudd_ReadOne(pNode->pNtk->pManFunc) ) + { + vVars->nSize = 0; +// if ( Abc_SopIsConst1(pSop1) ) + if ( !Cudd_IsComplement(pNode->pData) ) + Vec_IntPush( vVars, toLit(pNode->Id) ); + else + Vec_IntPush( vVars, neg(toLit(pNode->Id)) ); + RetValue = solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ); + if ( !RetValue ) + { + printf( "The CNF is trivially UNSAT.\n" ); + return 0; + } + return 1; + } + + // add clauses for the negative phase + for ( c = 0; ; c++ ) + { + // get the cube + pCube = pSop0 + c * (nFanins + 3); + if ( *pCube == 0 ) + break; + // add the clause + vVars->nSize = 0; + Abc_ObjForEachFanin( pNode, pFanin, i ) + { + if ( pCube[i] == '0' ) + Vec_IntPush( vVars, toLit(pFanin->Id) ); + else if ( pCube[i] == '1' ) + Vec_IntPush( vVars, neg(toLit(pFanin->Id)) ); + } + Vec_IntPush( vVars, neg(toLit(pNode->Id)) ); + RetValue = solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ); + if ( !RetValue ) + { + printf( "The CNF is trivially UNSAT.\n" ); + return 0; + } + } + + // add clauses for the positive phase + for ( c = 0; ; c++ ) + { + // get the cube + pCube = pSop1 + c * (nFanins + 3); + if ( *pCube == 0 ) + break; + // add the clause + vVars->nSize = 0; + Abc_ObjForEachFanin( pNode, pFanin, i ) + { + if ( pCube[i] == '0' ) + Vec_IntPush( vVars, toLit(pFanin->Id) ); + else if ( pCube[i] == '1' ) + Vec_IntPush( vVars, neg(toLit(pFanin->Id)) ); + } + Vec_IntPush( vVars, toLit(pNode->Id) ); + RetValue = solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ); + if ( !RetValue ) + { + printf( "The CNF is trivially UNSAT.\n" ); + return 0; + } + } + return 1; +} + +/**Function************************************************************* + + Synopsis [Adds clauses for the PO node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NodeAddClausesTop( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars ) +{ + Abc_Obj_t * pFanin; + int RetValue; + + pFanin = Abc_ObjFanin0(pNode); + if ( Abc_ObjFaninC0(pNode) ) + { + vVars->nSize = 0; + Vec_IntPush( vVars, toLit(pFanin->Id) ); + Vec_IntPush( vVars, toLit(pNode->Id) ); + RetValue = solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ); + if ( !RetValue ) + { + printf( "The CNF is trivially UNSAT.\n" ); + return 0; + } + + vVars->nSize = 0; + Vec_IntPush( vVars, neg(toLit(pFanin->Id)) ); + Vec_IntPush( vVars, neg(toLit(pNode->Id)) ); + RetValue = solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ); + if ( !RetValue ) + { + printf( "The CNF is trivially UNSAT.\n" ); + return 0; + } + } + else + { + vVars->nSize = 0; + Vec_IntPush( vVars, neg(toLit(pFanin->Id)) ); + Vec_IntPush( vVars, toLit(pNode->Id) ); + RetValue = solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ); + if ( !RetValue ) + { + printf( "The CNF is trivially UNSAT.\n" ); + return 0; + } + + vVars->nSize = 0; + Vec_IntPush( vVars, toLit(pFanin->Id) ); + Vec_IntPush( vVars, neg(toLit(pNode->Id)) ); + RetValue = solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ); + if ( !RetValue ) + { + printf( "The CNF is trivially UNSAT.\n" ); + return 0; + } + } + + vVars->nSize = 0; + Vec_IntPush( vVars, toLit(pNode->Id) ); + RetValue = solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ); + if ( !RetValue ) + { + printf( "The CNF is trivially UNSAT.\n" ); + return 0; + } + return 1; +} + +/**Function************************************************************* + + Synopsis [Sets up the SAT solver.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +solver * Abc_NtkMiterSatCreateLogic( Abc_Ntk_t * pNtk, int fAllPrimes ) +{ + solver * pSat; + Extra_MmFlex_t * pMmFlex; + Abc_Obj_t * pNode; + Vec_Str_t * vCube; + Vec_Int_t * vVars; + char * pSop0, * pSop1; + int i; + + assert( Abc_NtkIsBddLogic(pNtk) ); + + // transfer the IDs to the copy field + Abc_NtkForEachPi( pNtk, pNode, i ) + pNode->pCopy = (void *)pNode->Id; + + // start the data structures + pSat = solver_new(); + pMmFlex = Extra_MmFlexStart(); + vCube = Vec_StrAlloc( 100 ); + vVars = Vec_IntAlloc( 100 ); + +Sat_SolverTraceStart( pSat, "trace.cnf" ); + + // add clauses for each internal nodes + Abc_NtkForEachNode( pNtk, pNode, i ) + { + // derive SOPs for both phases of the node + Abc_NodeBddToCnf( pNode, pMmFlex, vCube, fAllPrimes, &pSop0, &pSop1 ); + // add the clauses to the solver + if ( !Abc_NodeAddClauses( pSat, pSop0, pSop1, pNode, vVars ) ) + { + solver_delete( pSat ); + pSat = NULL; + goto finish; + } + } + // add clauses for each PO + Abc_NtkForEachPo( pNtk, pNode, i ) + { + if ( !Abc_NodeAddClausesTop( pSat, pNode, vVars ) ) + { + solver_delete( pSat ); + pSat = NULL; + goto finish; + } + } + +finish: + // delete + Vec_StrFree( vCube ); + Vec_IntFree( vVars ); + Extra_MmFlexStop( pMmFlex ); + return pSat; +} + + + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abci/abcStrash.c b/src/base/abci/abcStrash.c index 9af6dc00..b6aecef9 100644 --- a/src/base/abci/abcStrash.c +++ b/src/base/abci/abcStrash.c @@ -49,7 +49,7 @@ Abc_Ntk_t * Abc_NtkRestrash( Abc_Ntk_t * pNtk, bool fCleanup ) extern int timeRetime; Abc_Ntk_t * pNtkAig; Abc_Obj_t * pObj; - int i, nNodes, RetValue; + int i, nNodes;//, RetValue; assert( Abc_NtkIsStrash(pNtk) ); //timeRetime = clock(); // print warning about choice nodes @@ -79,8 +79,8 @@ Abc_Ntk_t * Abc_NtkRestrash( Abc_Ntk_t * pNtk, bool fCleanup ) return NULL; } //timeRetime = clock() - timeRetime; - if ( RetValue = Abc_NtkRemoveSelfFeedLatches(pNtkAig) ) - printf( "Modified %d self-feeding latches. The result will not verify.\n", RetValue ); +// if ( RetValue = Abc_NtkRemoveSelfFeedLatches(pNtkAig) ) +// printf( "Modified %d self-feeding latches. The result will not verify.\n", RetValue ); return pNtkAig; } diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c index ec0ba8ca..f3a069f4 100644 --- a/src/base/abci/abcVerify.c +++ b/src/base/abci/abcVerify.c @@ -417,6 +417,12 @@ int * Abc_NtkVerifySimulatePattern( Abc_Ntk_t * pNtk, int * pModel ) pNtk = Abc_NtkStrash(pNtk, 0, 0); fStrashed = 1; } +/* + printf( "Counter example: " ); + Abc_NtkForEachCi( pNtk, pNode, i ) + printf( " %d", pModel[i] ); + printf( "\n" ); +*/ // increment the trav ID Abc_NtkIncrementTravId( pNtk ); // set the CI values diff --git a/src/base/io/io.c b/src/base/io/io.c index f50faa11..8d5b8ad6 100644 --- a/src/base/io/io.c +++ b/src/base/io/io.c @@ -1212,12 +1212,17 @@ int IoCommandWriteCnf( Abc_Frame_t * pAbc, int argc, char **argv ) { char * pFileName; int c; + int fAllPrimes; + fAllPrimes = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "ph" ) ) != EOF ) { switch ( c ) { + case 'p': + fAllPrimes ^= 1; + break; case 'h': goto usage; default: @@ -1228,13 +1233,23 @@ int IoCommandWriteCnf( Abc_Frame_t * pAbc, int argc, char **argv ) goto usage; // get the output file name pFileName = argv[globalUtilOptind]; + // check if the feature will be used + if ( Abc_NtkIsStrash(pAbc->pNtkCur) && fAllPrimes ) + { + fAllPrimes = 0; + printf( "Warning: Selected option to write all primes has no effect when deriving CNF from AIG.\n" ); + } // call the corresponding file writer - Io_Write( pAbc->pNtkCur, pFileName, IO_FILE_CNF ); + if ( fAllPrimes ) + Io_WriteCnf( pAbc->pNtkCur, pFileName, 1 ); + else + Io_Write( pAbc->pNtkCur, pFileName, IO_FILE_CNF ); return 0; usage: - fprintf( pAbc->Err, "usage: write_cnf [-h] <file>\n" ); + fprintf( pAbc->Err, "usage: write_cnf [-ph] <file>\n" ); fprintf( pAbc->Err, "\t write the miter cone into a CNF file\n" ); + fprintf( pAbc->Err, "\t-p : toggle using all primes to enhance implicativity [default = %s]\n", fAllPrimes? "yes" : "no" ); fprintf( pAbc->Err, "\t-h : print the help massage\n" ); fprintf( pAbc->Err, "\tfile : the name of the file to write\n" ); return 1; diff --git a/src/base/io/io.h b/src/base/io/io.h index 55339790..78bc4563 100644 --- a/src/base/io/io.h +++ b/src/base/io/io.h @@ -100,7 +100,7 @@ extern void Io_WriteBlifMvNetlist( Abc_Ntk_t * pNtk, char * FileNa /*=== abcWriteBench.c =========================================================*/ extern int Io_WriteBench( Abc_Ntk_t * pNtk, char * FileName ); /*=== abcWriteCnf.c ===========================================================*/ -extern int Io_WriteCnf( Abc_Ntk_t * pNtk, char * FileName ); +extern int Io_WriteCnf( Abc_Ntk_t * pNtk, char * FileName, int fAllPrimes ); /*=== abcWriteDot.c ===========================================================*/ extern void Io_WriteDot( Abc_Ntk_t * pNtk, char * FileName ); extern void Io_WriteDotNtk( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesShow, char * pFileName, int fGateNames, int fUseReverse ); diff --git a/src/base/io/ioUtil.c b/src/base/io/ioUtil.c index ba390a2f..ed197ab4 100644 --- a/src/base/io/ioUtil.c +++ b/src/base/io/ioUtil.c @@ -220,7 +220,7 @@ void Io_Write( Abc_Ntk_t * pNtk, char * pFileName, Io_FileType_t FileType ) // write non-netlist types if ( FileType == IO_FILE_CNF ) { - Io_WriteCnf( pNtk, pFileName ); + Io_WriteCnf( pNtk, pFileName, 0 ); return; } if ( FileType == IO_FILE_DOT ) diff --git a/src/base/io/ioWriteCnf.c b/src/base/io/ioWriteCnf.c index 24612566..f12a1297 100644 --- a/src/base/io/ioWriteCnf.c +++ b/src/base/io/ioWriteCnf.c @@ -41,14 +41,13 @@ static Abc_Ntk_t * s_pNtk = NULL; SeeAlso [] ***********************************************************************/ -int Io_WriteCnf( Abc_Ntk_t * pNtk, char * pFileName ) +int Io_WriteCnf( Abc_Ntk_t * pNtk, char * pFileName, int fAllPrimes ) { solver * pSat; - if ( !Abc_NtkIsStrash(pNtk) ) - { - fprintf( stdout, "Io_WriteCnf(): Currently can only process AIGs.\n" ); - return 0; - } + if ( Abc_NtkIsStrash(pNtk) ) + printf( "Io_WriteCnf() warning: Generating CNF by applying heuristic AIG to CNF conversion.\n" ); + else + printf( "Io_WriteCnf() warning: Generating CNF by convering logic nodes into CNF clauses.\n" ); if ( Abc_NtkPoNum(pNtk) != 1 ) { fprintf( stdout, "Io_WriteCnf(): Currently can only process the miter (the network with one PO).\n" ); @@ -64,8 +63,11 @@ int Io_WriteCnf( Abc_Ntk_t * pNtk, char * pFileName ) fprintf( stdout, "The network has no logic nodes. No CNF file is generaled.\n" ); return 0; } + // convert to logic BDD network + if ( Abc_NtkIsLogic(pNtk) ) + Abc_NtkLogicToBdd( pNtk ); // create solver with clauses - pSat = Abc_NtkMiterSatCreate( pNtk, 0 ); + pSat = Abc_NtkMiterSatCreate( pNtk, 0, fAllPrimes ); if ( pSat == NULL ) { fprintf( stdout, "The problem is trivially UNSAT. No CNF file is generated.\n" ); diff --git a/src/base/seq/seqAigCore.c b/src/base/seq/seqAigCore.c index 21215af6..42fa14a2 100644 --- a/src/base/seq/seqAigCore.c +++ b/src/base/seq/seqAigCore.c @@ -352,7 +352,7 @@ int Seq_NtkImplementRetimingBackward( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMoves, int printf( "The number of ANDs in the AIG = %5d.\n", Abc_NtkNodeNum(pNtkMiter) ); // transform the miter into a logic network for efficient CNF construction -// pNtkCnf = Abc_NtkRenode( pNtkMiter, 0, 100, 1, 0, 0 ); +// pNtkCnf = Abc_Ntk_Renode( pNtkMiter, 0, 100, 1, 0, 0 ); // Abc_NtkDelete( pNtkMiter ); pNtkCnf = pNtkMiter; diff --git a/src/map/if/if.h b/src/map/if/if.h index 80678cbf..81d4007c 100644 --- a/src/map/if/if.h +++ b/src/map/if/if.h @@ -45,6 +45,8 @@ extern "C" { #define IF_MAX_LUTSIZE 32 // the largest possible number of LUT inputs when funtionality of the LUTs are computed #define IF_MAX_FUNC_LUTSIZE 15 +// a very large number +#define IF_INFINITY 100000000 // object types typedef enum { @@ -75,6 +77,8 @@ struct If_Par_t_ // user-controlable paramters int nLutSize; // the LUT size int nCutsMax; // the max number of cuts + int nFlowIters; // the number of iterations of area recovery + int nAreaIters; // the number of iterations of area recovery float DelayTarget; // delay target int fPreprocess; // preprossing int fArea; // area-oriented mapping @@ -88,6 +92,7 @@ struct If_Par_t_ int fUsePerm; // use permutation (delay info) int fUseBdds; // sets local BDDs at the nodes int fUseSops; // sets local SOPs at the nodes + int fUseCnfs; // sets local CNFs at the nodes int nLatches; // the number of latches in seq mapping int fLiftLeaves; // shift the leaves for seq mapping If_Lib_t * pLutLib; // the LUT library @@ -276,6 +281,8 @@ static inline float If_CutLutArea( If_Man_t * p, If_Cut_t * pCut ) { r // iterator over the leaves of the cut #define If_CutForEachLeaf( p, pCut, pLeaf, i ) \ for ( i = 0; (i < (int)(pCut)->nLeaves) && ((pLeaf) = If_ManObj(p, (pCut)->pLeaves[i])); i++ ) +#define If_CutForEachLeafReverse( p, pCut, pLeaf, i ) \ + for ( i = (int)(pCut)->nLeaves - 1; (i >= 0) && ((pLeaf) = If_ManObj(p, (pCut)->pLeaves[i])); i-- ) //#define If_CutForEachLeaf( p, pCut, pLeaf, i ) \ // for ( i = 0; (i < (int)(pCut)->nLeaves) && ((pLeaf) = If_ManObj(p, p->pPars->fLiftLeaves? (pCut)->pLeaves[i] >> 8 : (pCut)->pLeaves[i])); i++ ) // iterator over the leaves of the sequential cut diff --git a/src/map/if/ifCore.c b/src/map/if/ifCore.c index 38983832..be2c7e33 100644 --- a/src/map/if/ifCore.c +++ b/src/map/if/ifCore.c @@ -42,8 +42,6 @@ int If_ManPerformMapping( If_Man_t * p ) { If_Obj_t * pObj; - int nItersFlow = 1; - int nItersArea = 2; int clkTotal = clock(); int RetValue, i; @@ -74,14 +72,14 @@ int If_ManPerformMapping( If_Man_t * p ) if ( p->pPars->fExpRed && !p->pPars->fTruth ) If_ManImproveMapping( p ); // area flow oriented mapping - for ( i = 0; i < nItersFlow; i++ ) + for ( i = 0; i < p->pPars->nFlowIters; i++ ) { If_ManPerformMappingRound( p, p->pPars->nCutsMax, 1, 1, "Flow" ); if ( p->pPars->fExpRed && !p->pPars->fTruth ) If_ManImproveMapping( p ); } // area oriented mapping - for ( i = 0; i < nItersArea; i++ ) + for ( i = 0; i < p->pPars->nAreaIters; i++ ) { If_ManPerformMappingRound( p, p->pPars->nCutsMax, 2, 1, "Area" ); if ( p->pPars->fExpRed && !p->pPars->fTruth ) diff --git a/src/map/if/ifCut.c b/src/map/if/ifCut.c index 8c092b99..f0663f7f 100644 --- a/src/map/if/ifCut.c +++ b/src/map/if/ifCut.c @@ -473,7 +473,7 @@ float If_CutAverageRefs( If_Man_t * p, If_Cut_t * pCut ) SideEffects [] SeeAlso [] - + ***********************************************************************/ float If_CutDeref( If_Man_t * p, If_Cut_t * pCut, int nLevels ) { diff --git a/src/map/if/ifMap.c b/src/map/if/ifMap.c index 569f200b..2d04d780 100644 --- a/src/map/if/ifMap.c +++ b/src/map/if/ifMap.c @@ -86,7 +86,7 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode ) pObj->EstRefs = (float)((2.0 * pObj->EstRefs + pObj->nRefs) / 3.0); } if ( Mode && pObj->nRefs > 0 ) - If_CutDeref( p, If_ObjCutBest(pObj), 100 ); + If_CutDeref( p, If_ObjCutBest(pObj), IF_INFINITY ); // save the best cut as one of the candidate cuts p->nCuts = 0; @@ -97,7 +97,7 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode ) pCut = If_ObjCutBest(pObj); pCut->Delay = If_CutDelay( p, pCut ); assert( pCut->Delay <= pObj->Required + p->fEpsilon ); - pCut->Area = (Mode == 2)? If_CutAreaDerefed( p, pCut, 100 ) : If_CutFlow( p, pCut ); + pCut->Area = (Mode == 2)? If_CutAreaDerefed( p, pCut, IF_INFINITY ) : If_CutFlow( p, pCut ); // save the best cut from the previous iteration If_CutCopy( p->ppCuts[p->nCuts++], pCut ); p->nCutsMerged++; @@ -135,7 +135,7 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode ) if ( Mode && pCut->Delay > pObj->Required + p->fEpsilon ) continue; // compute area of the cut (this area may depend on the application specific cost) - pCut->Area = (Mode == 2)? If_CutAreaDerefed( p, pCut, 100 ) : If_CutFlow( p, pCut ); + pCut->Area = (Mode == 2)? If_CutAreaDerefed( p, pCut, IF_INFINITY ) : If_CutFlow( p, pCut ); pCut->AveRefs = (Mode == 0)? (float)0.0 : If_CutAverageRefs( p, pCut ); // make sure the cut is the last one (after filtering it may not be so) assert( pCut == p->ppCuts[iCut] ); @@ -160,7 +160,7 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode ) assert( p->pPars->fSeqMap || If_ObjCutBest(pObj)->nLeaves > 1 ); // ref the selected cut if ( Mode && pObj->nRefs > 0 ) - If_CutRef( p, If_ObjCutBest(pObj), 100 ); + If_CutRef( p, If_ObjCutBest(pObj), IF_INFINITY ); } /**Function************************************************************* @@ -182,7 +182,7 @@ void If_ObjPerformMappingChoice( If_Man_t * p, If_Obj_t * pObj, int Mode ) assert( pObj->pEquiv != NULL ); // prepare if ( Mode && pObj->nRefs > 0 ) - If_CutDeref( p, If_ObjCutBest(pObj), 100 ); + If_CutDeref( p, If_ObjCutBest(pObj), IF_INFINITY ); // prepare room for the next cut p->nCuts = 0; iCut = p->nCuts; @@ -207,7 +207,7 @@ void If_ObjPerformMappingChoice( If_Man_t * p, If_Obj_t * pObj, int Mode ) // set the phase attribute pCut->fCompl ^= (pObj->fPhase ^ pTemp->fPhase); // compute area of the cut (this area may depend on the application specific cost) - pCut->Area = (Mode == 2)? If_CutAreaDerefed( p, pCut, 100 ) : If_CutFlow( p, pCut ); + pCut->Area = (Mode == 2)? If_CutAreaDerefed( p, pCut, IF_INFINITY ) : If_CutFlow( p, pCut ); pCut->AveRefs = (Mode == 0)? (float)0.0 : If_CutAverageRefs( p, pCut ); // make sure the cut is the last one (after filtering it may not be so) assert( pCut == p->ppCuts[iCut] ); @@ -237,7 +237,7 @@ void If_ObjPerformMappingChoice( If_Man_t * p, If_Obj_t * pObj, int Mode ) assert( p->pPars->fSeqMap || If_ObjCutBest(pObj)->nLeaves > 1 ); // ref the selected cut if ( Mode && pObj->nRefs > 0 ) - If_CutRef( p, If_ObjCutBest(pObj), 100 ); + If_CutRef( p, If_ObjCutBest(pObj), IF_INFINITY ); } /**Function************************************************************* diff --git a/src/map/if/ifReduce.c b/src/map/if/ifReduce.c index 2e2a6d81..26989b8c 100644 --- a/src/map/if/ifReduce.c +++ b/src/map/if/ifReduce.c @@ -156,17 +156,17 @@ void If_ManImproveNodeExpand( If_Man_t * p, If_Obj_t * pObj, int nLimit, Vec_Ptr // get the delay DelayOld = pCut->Delay; // get the area - AreaBef = If_CutAreaRefed( p, pCut, 100000 ); + AreaBef = If_CutAreaRefed( p, pCut, IF_INFINITY ); // if ( AreaBef == 1 ) // return; // the cut is non-trivial If_ManImproveNodePrepare( p, pObj, nLimit, vFront, vFrontOld, vVisited ); // iteratively modify the cut - If_CutDeref( p, pCut, 100000 ); + If_CutDeref( p, pCut, IF_INFINITY ); CostBef = If_ManImproveCutCost( p, vFront ); If_ManImproveNodeFaninCompact( p, pObj, nLimit, vFront, vVisited ); CostAft = If_ManImproveCutCost( p, vFront ); - If_CutRef( p, pCut, 100000 ); + If_CutRef( p, pCut, IF_INFINITY ); assert( CostBef >= CostAft ); // clean up Vec_PtrForEachEntry( vVisited, pFanin, i ) @@ -175,11 +175,11 @@ void If_ManImproveNodeExpand( If_Man_t * p, If_Obj_t * pObj, int nLimit, Vec_Ptr If_ManImproveNodeUpdate( p, pObj, vFront ); pCut->Delay = If_CutDelay( p, pCut ); // get the new area - AreaAft = If_CutAreaRefed( p, pCut, 100000 ); + AreaAft = If_CutAreaRefed( p, pCut, IF_INFINITY ); if ( AreaAft > AreaBef || pCut->Delay > pObj->Required + p->fEpsilon ) { If_ManImproveNodeUpdate( p, pObj, vFrontOld ); - AreaAft = If_CutAreaRefed( p, pCut, 100000 ); + AreaAft = If_CutAreaRefed( p, pCut, IF_INFINITY ); assert( AreaAft == AreaBef ); pCut->Delay = DelayOld; } @@ -257,13 +257,13 @@ void If_ManImproveNodeUpdate( If_Man_t * p, If_Obj_t * pObj, Vec_Ptr_t * vFront int i; pCut = If_ObjCutBest(pObj); // deref node's cut - If_CutDeref( p, pCut, 10000 ); + If_CutDeref( p, pCut, IF_INFINITY ); // update the node's cut pCut->nLeaves = Vec_PtrSize(vFront); Vec_PtrForEachEntry( vFront, pFanin, i ) pCut->pLeaves[i] = pFanin->Id; // ref the new cut - If_CutRef( p, pCut, 10000 ); + If_CutRef( p, pCut, IF_INFINITY ); } @@ -506,9 +506,9 @@ void If_ManImproveNodeReduce( If_Man_t * p, If_Obj_t * pObj, int nLimit ) // deref the cut if the node is refed if ( pObj->nRefs > 0 ) - If_CutDeref( p, pCut, 100000 ); + If_CutDeref( p, pCut, IF_INFINITY ); // get the area - AreaBef = If_CutAreaDerefed( p, pCut, 100000 ); + AreaBef = If_CutAreaDerefed( p, pCut, IF_INFINITY ); // get the fanin support if ( pFanin0->nRefs > 2 && pCut0->Delay < pObj->Required + p->fEpsilon ) // if ( pSupp0->nRefs > 0 && pSupp0->Delay < pSupp->DelayR ) // this leads to 2% worse results @@ -534,7 +534,7 @@ void If_ManImproveNodeReduce( If_Man_t * p, If_Obj_t * pObj, int nLimit ) if ( RetValue ) { pCutR->Delay = If_CutDelay( p, pCutR ); - AreaAft = If_CutAreaDerefed( p, pCutR, 100000 ); + AreaAft = If_CutAreaDerefed( p, pCutR, IF_INFINITY ); // update the best cut if ( AreaAft < AreaBef - p->fEpsilon && pCutR->Delay < pObj->Required + p->fEpsilon ) If_CutCopy( pCut, pCutR ); @@ -543,7 +543,7 @@ void If_ManImproveNodeReduce( If_Man_t * p, If_Obj_t * pObj, int nLimit ) pCut->Delay = If_CutDelay( p, pCut ); // ref the cut if the node is refed if ( pObj->nRefs > 0 ) - If_CutRef( p, pCut, 100000 ); + If_CutRef( p, pCut, IF_INFINITY ); } /**Function************************************************************* diff --git a/src/map/mio/mioFunc.c b/src/map/mio/mioFunc.c index 78c98fbe..21a078f9 100644 --- a/src/map/mio/mioFunc.c +++ b/src/map/mio/mioFunc.c @@ -213,7 +213,7 @@ int Mio_GateParseFormula( Mio_Gate_t * pGate ) Cudd_Ref( pGate->bFunc ); // derive the cover (SOP) - pGate->pSop = Abc_ConvertBddToSop( pGate->pLib->pMmFlex, dd, pGate->bFunc, pGate->bFunc, nPins, pGate->pLib->vCube, -1 ); + pGate->pSop = Abc_ConvertBddToSop( pGate->pLib->pMmFlex, dd, pGate->bFunc, pGate->bFunc, nPins, 0, pGate->pLib->vCube, -1 ); return 0; } diff --git a/src/misc/extra/extra.h b/src/misc/extra/extra.h index 45686afb..9dd494eb 100644 --- a/src/misc/extra/extra.h +++ b/src/misc/extra/extra.h @@ -169,6 +169,7 @@ extern int Extra_bddIsVar( DdNode * bFunc ); extern DdNode * Extra_bddCreateAnd( DdManager * dd, int nVars ); extern DdNode * Extra_bddCreateOr( DdManager * dd, int nVars ); extern DdNode * Extra_bddCreateExor( DdManager * dd, int nVars ); +extern DdNode * Extra_zddPrimes( DdManager * dd, DdNode * F ); /*=== extraBddKmap.c ================================================================*/ diff --git a/src/misc/extra/extraBddMisc.c b/src/misc/extra/extraBddMisc.c index 1c720061..6d27b8cc 100644 --- a/src/misc/extra/extraBddMisc.c +++ b/src/misc/extra/extraBddMisc.c @@ -55,6 +55,8 @@ static DdNode * extraTransferPermute( DdManager * ddS, DdManager * ddD, DdNode * static void ddSupportStep(DdNode *f, int *support); static void ddClearFlag(DdNode *f); +static DdNode* extraZddPrimes( DdManager *dd, DdNode* F ); + /**AutomaticEnd***************************************************************/ /*---------------------------------------------------------------------------*/ @@ -890,6 +892,30 @@ DdNode * Extra_bddCreateExor( DdManager * dd, int nVars ) return bFunc; } +/**Function******************************************************************** + + Synopsis [Computes the set of primes as a ZDD.] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +DdNode * Extra_zddPrimes( DdManager * dd, DdNode * F ) +{ + DdNode *res; + do { + dd->reordered = 0; + res = extraZddPrimes(dd, F); + if ( dd->reordered == 1 ) + printf("\nReordering in Extra_zddPrimes()\n"); + } while (dd->reordered == 1); + return(res); + +} /* end of Extra_zddPrimes */ + /*---------------------------------------------------------------------------*/ /* Definition of internal functions */ @@ -1246,6 +1272,201 @@ ddClearFlag( } /* end of ddClearFlag */ +/**Function******************************************************************** + + Synopsis [Composed three subcovers into one ZDD.] + + Description [] + + SideEffects [None] + + SeeAlso [] + +******************************************************************************/ +DdNode * +extraComposeCover( + DdManager* dd, /* the manager */ + DdNode* zC0, /* the pointer to the negative var cofactor */ + DdNode* zC1, /* the pointer to the positive var cofactor */ + DdNode* zC2, /* the pointer to the cofactor without var */ + int TopVar) /* the index of the positive ZDD var */ +{ + DdNode * zRes, * zTemp; + /* compose with-neg-var and without-var using the neg ZDD var */ + zTemp = cuddZddGetNode( dd, 2*TopVar + 1, zC0, zC2 ); + if ( zTemp == NULL ) + { + Cudd_RecursiveDerefZdd(dd, zC0); + Cudd_RecursiveDerefZdd(dd, zC1); + Cudd_RecursiveDerefZdd(dd, zC2); + return NULL; + } + cuddRef( zTemp ); + cuddDeref( zC0 ); + cuddDeref( zC2 ); + + /* compose with-pos-var and previous result using the pos ZDD var */ + zRes = cuddZddGetNode( dd, 2*TopVar, zC1, zTemp ); + if ( zRes == NULL ) + { + Cudd_RecursiveDerefZdd(dd, zC1); + Cudd_RecursiveDerefZdd(dd, zTemp); + return NULL; + } + cuddDeref( zC1 ); + cuddDeref( zTemp ); + return zRes; +} /* extraComposeCover */ + +/**Function******************************************************************** + + Synopsis [Performs the recursive step of prime computation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +DdNode* extraZddPrimes( DdManager *dd, DdNode* F ) +{ + DdNode *zRes; + + if ( F == Cudd_Not( dd->one ) ) + return dd->zero; + if ( F == dd->one ) + return dd->one; + + /* check cache */ + zRes = cuddCacheLookup1Zdd(dd, extraZddPrimes, F); + if (zRes) + return(zRes); + { + /* temporary variables */ + DdNode *bF01, *zP0, *zP1; + /* three components of the prime set */ + DdNode *zResE, *zResP, *zResN; + int fIsComp = Cudd_IsComplement( F ); + + /* find cofactors of F */ + DdNode * bF0 = Cudd_NotCond( Cudd_E( F ), fIsComp ); + DdNode * bF1 = Cudd_NotCond( Cudd_T( F ), fIsComp ); + + /* find the intersection of cofactors */ + bF01 = cuddBddAndRecur( dd, bF0, bF1 ); + if ( bF01 == NULL ) return NULL; + cuddRef( bF01 ); + + /* solve the problems for cofactors */ + zP0 = extraZddPrimes( dd, bF0 ); + if ( zP0 == NULL ) + { + Cudd_RecursiveDeref( dd, bF01 ); + return NULL; + } + cuddRef( zP0 ); + + zP1 = extraZddPrimes( dd, bF1 ); + if ( zP1 == NULL ) + { + Cudd_RecursiveDeref( dd, bF01 ); + Cudd_RecursiveDerefZdd( dd, zP0 ); + return NULL; + } + cuddRef( zP1 ); + + /* check for local unateness */ + if ( bF01 == bF0 ) /* unate increasing */ + { + /* intersection is useless */ + cuddDeref( bF01 ); + /* the primes of intersection are the primes of F0 */ + zResE = zP0; + /* there are no primes with negative var */ + zResN = dd->zero; + cuddRef( zResN ); + /* primes with positive var are primes of F1 that are not primes of F01 */ + zResP = cuddZddDiff( dd, zP1, zP0 ); + if ( zResP == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zResE ); + Cudd_RecursiveDerefZdd( dd, zResN ); + Cudd_RecursiveDerefZdd( dd, zP1 ); + return NULL; + } + cuddRef( zResP ); + Cudd_RecursiveDerefZdd( dd, zP1 ); + } + else if ( bF01 == bF1 ) /* unate decreasing */ + { + /* intersection is useless */ + cuddDeref( bF01 ); + /* the primes of intersection are the primes of F1 */ + zResE = zP1; + /* there are no primes with positive var */ + zResP = dd->zero; + cuddRef( zResP ); + /* primes with negative var are primes of F0 that are not primes of F01 */ + zResN = cuddZddDiff( dd, zP0, zP1 ); + if ( zResN == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zResE ); + Cudd_RecursiveDerefZdd( dd, zResP ); + Cudd_RecursiveDerefZdd( dd, zP0 ); + return NULL; + } + cuddRef( zResN ); + Cudd_RecursiveDerefZdd( dd, zP0 ); + } + else /* not unate */ + { + /* primes without the top var are primes of F10 */ + zResE = extraZddPrimes( dd, bF01 ); + if ( zResE == NULL ) + { + Cudd_RecursiveDerefZdd( dd, bF01 ); + Cudd_RecursiveDerefZdd( dd, zP0 ); + Cudd_RecursiveDerefZdd( dd, zP1 ); + return NULL; + } + cuddRef( zResE ); + Cudd_RecursiveDeref( dd, bF01 ); + + /* primes with the negative top var are those of P0 that are not in F10 */ + zResN = cuddZddDiff( dd, zP0, zResE ); + if ( zResN == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zResE ); + Cudd_RecursiveDerefZdd( dd, zP0 ); + Cudd_RecursiveDerefZdd( dd, zP1 ); + return NULL; + } + cuddRef( zResN ); + Cudd_RecursiveDerefZdd( dd, zP0 ); + + /* primes with the positive top var are those of P1 that are not in F10 */ + zResP = cuddZddDiff( dd, zP1, zResE ); + if ( zResP == NULL ) + { + Cudd_RecursiveDerefZdd( dd, zResE ); + Cudd_RecursiveDerefZdd( dd, zResN ); + Cudd_RecursiveDerefZdd( dd, zP1 ); + return NULL; + } + cuddRef( zResP ); + Cudd_RecursiveDerefZdd( dd, zP1 ); + } + + zRes = extraComposeCover( dd, zResN, zResP, zResE, Cudd_Regular(F)->index ); + if ( zRes == NULL ) return NULL; + + /* insert the result into cache */ + cuddCacheInsert1(dd, extraZddPrimes, F, zRes); + return zRes; + } +} /* end of extraZddPrimes */ + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/opt/kit/kitFactor.c b/src/opt/kit/kitFactor.c index cbac918d..4ef3fd94 100644 --- a/src/opt/kit/kitFactor.c +++ b/src/opt/kit/kitFactor.c @@ -64,7 +64,7 @@ Kit_Graph_t * Kit_SopFactor( Vec_Int_t * vCover, int fCompl, int nVars, Vec_Int_ // check for trivial functions if ( Vec_IntSize(vCover) == 0 ) return Kit_GraphCreateConst0(); - if ( Vec_IntSize(vCover) == 1 && Vec_IntEntry(vCover, 0) == (int)Kit_CubeMask(nVars) ) + if ( Vec_IntSize(vCover) == 1 && Vec_IntEntry(vCover, 0) == 0 ) //(int)Kit_CubeMask(2 * nVars) ) return Kit_GraphCreateConst1(); // prepare memory manager diff --git a/src/opt/kit/kitIsop.c b/src/opt/kit/kitIsop.c index d54932ee..cc61a6bd 100644 --- a/src/opt/kit/kitIsop.c +++ b/src/opt/kit/kitIsop.c @@ -72,6 +72,7 @@ int Kit_TruthIsop( unsigned * puTruth, int nVars, Vec_Int_t * vMemory, int fTryB assert( Extra_TruthIsEqual( puTruth, pResult, nVars ) ); if ( pcRes->nCubes == 0 || (pcRes->nCubes == 1 && pcRes->pCubes[0] == 0) ) { + vMemory->pArray[0] = 0; Vec_IntShrink( vMemory, pcRes->nCubes ); return 0; } diff --git a/src/opt/res/resDivs.c b/src/opt/res/resDivs.c index 42ec8955..0739b81b 100644 --- a/src/opt/res/resDivs.c +++ b/src/opt/res/resDivs.c @@ -25,8 +25,6 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -static int Res_WinVisitMffc( Res_Win_t * p ); - //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// diff --git a/src/sat/asat/satTrace.c b/src/sat/asat/satTrace.c new file mode 100644 index 00000000..3318933a --- /dev/null +++ b/src/sat/asat/satTrace.c @@ -0,0 +1,112 @@ +/**CFile**************************************************************** + + FileName [satTrace.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [C-language MiniSat solver.] + + Synopsis [Records the trace of SAT solving in the CNF form.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: satTrace.c,v 1.4 2005/09/16 22:55:03 casem Exp $] + +***********************************************************************/ + +#include <stdio.h> +#include <assert.h> +#include "solver.h" + +/* + The trace of SAT solving contains the original clause of the problem + along with the learned clauses derived during SAT solving. + The first line of the resulting file contains 3 numbers instead of 2: + c <num_vars> <num_all_clauses> <num_root_clauses> +*/ + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static inline int lit_var (lit l) { return l >> 1; } +static inline int lit_sign (lit l) { return l & 1; } +static inline int lit_print(lit l) { return lit_sign(l)? -lit_var(l)-1 : lit_var(l)+1; } + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Start the trace recording.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sat_SolverTraceStart( solver * pSat, char * pName ) +{ + assert( pSat->pFile == NULL ); + pSat->pFile = fopen( pName, "w" ); + fprintf( pSat->pFile, " \n" ); + pSat->nClauses = 0; + pSat->nRoots = 0; +} + +/**Function************************************************************* + + Synopsis [Stops the trace recording.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sat_SolverTraceStop( solver * pSat ) +{ + if ( pSat->pFile == NULL ) + return; + rewind( pSat->pFile ); + fprintf( pSat->pFile, "p %d %d %d", solver_nvars(pSat), pSat->nClauses, pSat->nRoots ); + fclose( pSat->pFile ); + pSat->pFile = NULL; +} + + +/**Function************************************************************* + + Synopsis [Writes one clause into the trace file.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sat_SolverTraceWrite( solver * pSat, int * pBeg, int * pEnd, int fRoot ) +{ + if ( pSat->pFile == NULL ) + return; + pSat->nClauses++; + pSat->nRoots += fRoot; + for ( ; pBeg < pEnd ; pBeg++ ) + fprintf( pSat->pFile, " %d", lit_print(*pBeg) ); + fprintf( pSat->pFile, " 0\n" ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/sat/asat/solver.c b/src/sat/asat/solver.c index 6f8fe037..b9851a54 100644 --- a/src/sat/asat/solver.c +++ b/src/sat/asat/solver.c @@ -20,6 +20,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA // Modified to compile with MS Visual Studio 6.0 by Alan Mishchenko #include <stdio.h> +#include <string.h> #include <assert.h> #include <math.h> #include <time.h> @@ -505,6 +506,8 @@ static void solver_record(solver* s, veci* cls) clause* c = (veci_size(cls) > 1) ? clause_new(s,begin,end,1) : (clause*)0; enqueue(s,*begin,c); +Sat_SolverTraceWrite( s, begin, end, 0 ); + assert(veci_size(cls) > 0); if (c != 0) { @@ -948,6 +951,7 @@ static lbool solver_search(solver* s, int nof_conflicts, int nof_learnts) solver* solver_new(void) { solver* s = (solver*)malloc(sizeof(solver)); + memset( s, 0, sizeof(solver) ); // initialize vectors vec_new(&s->clauses); @@ -1100,7 +1104,10 @@ bool solver_addclause(solver* s, lit* begin, lit* end) if (j == begin) // empty clause return 0; - else if (j - begin == 1) // unit clause + +Sat_SolverTraceWrite( s, begin, end, 1 ); + + if (j - begin == 1) // unit clause return enqueue(s,*begin,(clause*)0); // create new clause diff --git a/src/sat/asat/solver.h b/src/sat/asat/solver.h index bd6e8569..83066f41 100644 --- a/src/sat/asat/solver.h +++ b/src/sat/asat/solver.h @@ -91,6 +91,11 @@ extern void Asat_SatPrintStats( FILE * pFile, solver * p ); extern void Asat_SolverSetPrefVars( solver * s, int * pPrefVars, int nPrefVars ); extern void Asat_SolverSetFactors( solver * s, float * pFactors ); +// trace recording +extern void Sat_SolverTraceStart( solver * pSat, char * pName ); +extern void Sat_SolverTraceStop( solver * pSat ); +extern void Sat_SolverTraceWrite( solver * pSat, int * pBeg, int * pEnd, int fRoot ); + // J-frontier support extern Asat_JMan_t * Asat_JManStart( solver * pSat, void * vCircuit ); extern void Asat_JManStop( solver * pSat ); @@ -170,6 +175,11 @@ struct solver_t int timeTotal; int timeSelect; int timeUpdate; + + // trace recording + FILE * pFile; + int nClauses; + int nRoots; }; #ifdef __cplusplus diff --git a/src/sat/csat/csat_apis.c b/src/sat/csat/csat_apis.c index c212fce7..e45b1b81 100644 --- a/src/sat/csat/csat_apis.c +++ b/src/sat/csat/csat_apis.c @@ -90,7 +90,7 @@ ABC_Manager ABC_InitManager() // set default parameters for CEC Prove_ParamsSetDefault( &mng->Params ); // set infinite resource limit for the final mitering - mng->Params.nMiteringLimitLast = ABC_INFINITY; +// mng->Params.nMiteringLimitLast = ABC_INFINITY; return mng; } diff --git a/src/sat/fraig/fraigMan.c b/src/sat/fraig/fraigMan.c index 4e12dfe4..7fd937d5 100644 --- a/src/sat/fraig/fraigMan.c +++ b/src/sat/fraig/fraigMan.c @@ -74,6 +74,39 @@ void Prove_ParamsSetDefault( Prove_Params_t * pParams ) /**Function************************************************************* + Synopsis [Prints out the current values of CEC engine parameters.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Prove_ParamsPrint( Prove_Params_t * pParams ) +{ + printf( "CEC enging parameters:\n" ); + printf( "Fraiging enabled: %s\n", pParams->fUseFraiging? "yes":"no" ); + printf( "Rewriting enabled: %s\n", pParams->fUseRewriting? "yes":"no" ); + printf( "BDD construction enabled: %s\n", pParams->fUseBdds? "yes":"no" ); + printf( "Verbose output enabled: %s\n", pParams->fVerbose? "yes":"no" ); + printf( "Solver iterations: %d\n", pParams->nItersMax ); + printf( "Starting mitering limit: %d\n", pParams->nMiteringLimitStart ); + printf( "Multiplicative coeficient for mitering: %.2f\n", pParams->nMiteringLimitMulti ); + printf( "Starting number of rewriting iterations: %d\n", pParams->nRewritingLimitStart ); + printf( "Multiplicative coeficient for rewriting: %.2f\n", pParams->nRewritingLimitMulti ); + printf( "Starting number of conflicts in fraiging: %d\n", pParams->nFraigingLimitMulti ); + printf( "Multiplicative coeficient for fraiging: %.2f\n", pParams->nRewritingLimitMulti ); + printf( "BDD size limit for bailing out: %.2f\n", pParams->nBddSizeLimit ); + printf( "BDD reordering enabled: %s\n", pParams->fBddReorder? "yes":"no" ); + printf( "Last-gasp mitering limit: %d\n", pParams->nMiteringLimitLast ); + printf( "Total conflict limit: %d\n", pParams->nTotalBacktrackLimit ); + printf( "Total inspection limit: %d\n", pParams->nTotalInspectLimit ); + printf( "Parameter dump complete.\n" ); +} + +/**Function************************************************************* + Synopsis [Sets the default parameters of the package.] Description [This set of parameters is tuned for equivalence checking.] diff --git a/src/sat/proof/pr.c b/src/sat/proof/pr.c new file mode 100644 index 00000000..4e8a3522 --- /dev/null +++ b/src/sat/proof/pr.c @@ -0,0 +1,1235 @@ +/**CFile**************************************************************** + + FileName [pr.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Proof recording.] + + Synopsis [Core procedures of the package.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: pr.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include <stdio.h> +#include <stdlib.h> +#include <string.h> +#include <assert.h> +#include <time.h> +#include "vec.h" +#include "pr.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +typedef unsigned lit; + +typedef struct Pr_Cls_t_ Pr_Cls_t; +struct Pr_Cls_t_ +{ + unsigned uTruth; // interpolant + void * pProof; // the proof node +// void * pAntis; // the anticedents + Pr_Cls_t * pNext; // the next clause + Pr_Cls_t * pNext0; // the next 0-watch + Pr_Cls_t * pNext1; // the next 0-watch + int Id; // the clause ID + unsigned fA : 1; // belongs to A + unsigned fRoot : 1; // original clause + unsigned fVisit : 1; // visited clause + unsigned nLits : 24; // the number of literals + lit pLits[0]; // literals of this clause +}; + +struct Pr_Man_t_ +{ + // general data + int fProofWrite; // writes the proof file + int fProofVerif; // verifies the proof + int nVars; // the number of variables + int nVarsAB; // the number of global variables + int nRoots; // the number of root clauses + int nClauses; // the number of all clauses + int nClausesA; // the number of clauses of A + Pr_Cls_t * pHead; // the head clause + Pr_Cls_t * pTail; // the tail clause + Pr_Cls_t * pLearnt; // the tail clause + Pr_Cls_t * pEmpty; // the empty clause + // internal BCP + int nRootSize; // the number of root level assignments + int nTrailSize; // the number of assignments made + lit * pTrail; // chronological order of assignments (size nVars) + lit * pAssigns; // assignments by variable (size nVars) + char * pSeens; // temporary mark (size nVars) + char * pVarTypes; // variable type (size nVars) [1=A, 0=B, <0=AB] + Pr_Cls_t ** pReasons; // reasons for each assignment (size nVars) + Pr_Cls_t ** pWatches; // watched clauses for each literal (size 2*nVars) + int nVarsAlloc; // the allocated size of arrays + // proof recording + void * pManProof; // proof manager + int Counter; // counter of resolved clauses + // memory management + int nChunkSize; // the number of bytes in a chunk + int nChunkUsed; // the number of bytes used in the last chunk + char * pChunkLast; // the last memory chunk + // internal verification + lit * pResLits; // the literals of the resolvent + int nResLits; // the number of literals of the resolvent + int nResLitsAlloc;// the number of literals of the resolvent + // runtime stats + int timeBcp; + int timeTrace; + int timeRead; + int timeTotal; +}; + +#ifndef PRT +#define PRT(a,t) printf("%s = ", (a)); printf("%6.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC)) +#endif + +// variable assignments +static const lit LIT_UNDEF = 0xffffffff; + +// variable/literal conversions (taken from MiniSat) +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; } +static inline int lit_print(lit l) { return lit_sign(l)? -lit_var(l)-1 : lit_var(l)+1; } +static inline lit lit_read (int s) { return s > 0 ? toLit(s-1) : lit_neg(toLit(-s-1)); } +static inline int lit_check(lit l, int n) { return l >= 0 && lit_var(l) < n; } + +// iterators through the clauses +#define Pr_ManForEachClause( p, pCls ) for( pCls = p->pHead; pCls; pCls = pCls->pNext ) +#define Pr_ManForEachClauseRoot( p, pCls ) for( pCls = p->pHead; pCls != p->pLearnt; pCls = pCls->pNext ) +#define Pr_ManForEachClauseLearnt( p, pCls ) for( pCls = p->pLearnt; pCls; pCls = pCls->pNext ) + +// static procedures +static char * Pr_ManMemoryFetch( Pr_Man_t * p, int nBytes ); +static void Pr_ManMemoryStop( Pr_Man_t * p ); +static void Pr_ManResize( Pr_Man_t * p, int nVarsNew ); + +// exported procedures +extern Pr_Man_t * Pr_ManAlloc( int nVarsAlloc ); +extern void Pr_ManFree( Pr_Man_t * p ); +extern int Pr_ManAddClause( Pr_Man_t * p, lit * pBeg, lit * pEnd, int fRoot, int fClauseA ); +extern int Pr_ManProofWrite( Pr_Man_t * p ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Allocate proof manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Pr_Man_t * Pr_ManAlloc( int nVarsAlloc ) +{ + Pr_Man_t * p; + // allocate the manager + p = (Pr_Man_t *)malloc( sizeof(Pr_Man_t) ); + memset( p, 0, sizeof(Pr_Man_t) ); + // allocate internal arrays + Pr_ManResize( p, nVarsAlloc? nVarsAlloc : 256 ); + // set the starting number of variables + p->nVars = 0; + // memory management + p->nChunkSize = (1<<18); // use 256K chunks + // verification + p->nResLitsAlloc = (1<<16); + p->pResLits = malloc( sizeof(lit) * p->nResLitsAlloc ); + // parameters + p->fProofWrite = 0; + p->fProofVerif = 0; + return p; +} + +/**Function************************************************************* + + Synopsis [Resize proof manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Pr_ManResize( Pr_Man_t * p, int nVarsNew ) +{ + // check if resizing is needed + if ( p->nVarsAlloc < nVarsNew ) + { + int nVarsAllocOld = p->nVarsAlloc; + // find the new size + if ( p->nVarsAlloc == 0 ) + p->nVarsAlloc = 1; + while ( p->nVarsAlloc < nVarsNew ) + p->nVarsAlloc *= 2; + // resize the arrays + p->pTrail = (lit *) realloc( p->pTrail, sizeof(lit) * p->nVarsAlloc ); + p->pAssigns = (lit *) realloc( p->pAssigns, sizeof(lit) * p->nVarsAlloc ); + p->pSeens = (char *) realloc( p->pSeens, sizeof(char) * p->nVarsAlloc ); + p->pVarTypes = (char *) realloc( p->pVarTypes, sizeof(char) * p->nVarsAlloc ); + p->pReasons = (Pr_Cls_t **)realloc( p->pReasons, sizeof(Pr_Cls_t *) * p->nVarsAlloc ); + p->pWatches = (Pr_Cls_t **)realloc( p->pWatches, sizeof(Pr_Cls_t *) * p->nVarsAlloc*2 ); + // clean the free space + memset( p->pAssigns + nVarsAllocOld, 0xff, sizeof(lit) * (p->nVarsAlloc - nVarsAllocOld) ); + memset( p->pSeens + nVarsAllocOld, 0, sizeof(char) * (p->nVarsAlloc - nVarsAllocOld) ); + memset( p->pVarTypes + nVarsAllocOld, 0, sizeof(char) * (p->nVarsAlloc - nVarsAllocOld) ); + memset( p->pReasons + nVarsAllocOld, 0, sizeof(Pr_Cls_t *) * (p->nVarsAlloc - nVarsAllocOld) ); + memset( p->pWatches + nVarsAllocOld, 0, sizeof(Pr_Cls_t *) * (p->nVarsAlloc - nVarsAllocOld)*2 ); + } + // adjust the number of variables + if ( p->nVars < nVarsNew ) + p->nVars = nVarsNew; +} + +/**Function************************************************************* + + Synopsis [Deallocate proof manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Pr_ManFree( Pr_Man_t * p ) +{ + printf( "Runtime stats:\n" ); +PRT( "Reading ", p->timeRead ); +PRT( "BCP ", p->timeBcp ); +PRT( "Trace ", p->timeTrace ); +PRT( "TOTAL ", p->timeTotal ); + + Pr_ManMemoryStop( p ); + free( p->pTrail ); + free( p->pAssigns ); + free( p->pSeens ); + free( p->pVarTypes ); + free( p->pReasons ); + free( p->pWatches ); + free( p->pResLits ); + free( p ); +} + +/**Function************************************************************* + + Synopsis [Adds one clause to the watcher list.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Pr_ManWatchClause( Pr_Man_t * p, Pr_Cls_t * pClause, lit Lit ) +{ + assert( lit_check(Lit, p->nVars) ); + if ( pClause->pLits[0] == Lit ) + pClause->pNext0 = p->pWatches[lit_neg(Lit)]; + else + { + assert( pClause->pLits[1] == Lit ); + pClause->pNext1 = p->pWatches[lit_neg(Lit)]; + } + p->pWatches[lit_neg(Lit)] = pClause; +} + +/**Function************************************************************* + + Synopsis [Adds one clause to the manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Pr_ManAddClause( Pr_Man_t * p, lit * pBeg, lit * pEnd, int fRoot, int fClauseA ) +{ + Pr_Cls_t * pClause; + lit Lit, * i, * j; + int nSize, VarMax; + + // process the literals + if ( pBeg < pEnd ) + { + // insertion sort + VarMax = lit_var( *pBeg ); + for ( i = pBeg + 1; i < pEnd; i++ ) + { + Lit = *i; + VarMax = lit_var(Lit) > VarMax ? lit_var(Lit) : VarMax; + for ( j = i; j > pBeg && *(j-1) > Lit; j-- ) + *j = *(j-1); + *j = Lit; + } + // make sure there is no duplicated variables + for ( i = pBeg + 1; i < pEnd; i++ ) + assert( lit_var(*(i-1)) != lit_var(*i) ); + // resize the manager + Pr_ManResize( p, VarMax+1 ); + } + + // get memory for the clause + nSize = sizeof(Pr_Cls_t) + sizeof(lit) * (pEnd - pBeg); + pClause = (Pr_Cls_t *)Pr_ManMemoryFetch( p, nSize ); + memset( pClause, 0, sizeof(Pr_Cls_t) ); + + // assign the clause + assert( !fClauseA || fRoot ); // clause of A is always a root clause + p->nRoots += fRoot; + p->nClausesA += fClauseA; + pClause->Id = p->nClauses++; + pClause->fA = fClauseA; + pClause->fRoot = fRoot; + pClause->nLits = pEnd - pBeg; + memcpy( pClause->pLits, pBeg, sizeof(lit) * (pEnd - pBeg) ); + + // add the clause to the list + if ( p->pHead == NULL ) + p->pHead = pClause; + if ( p->pTail == NULL ) + p->pTail = pClause; + else + { + p->pTail->pNext = pClause; + p->pTail = pClause; + } + + // mark the first learnt clause + if ( p->pLearnt == NULL && !pClause->fRoot ) + p->pLearnt = pClause; + + // add the empty clause + if ( pClause->nLits == 0 ) + { + if ( p->pEmpty ) + printf( "More than one empty clause!\n" ); + p->pEmpty = pClause; + } + + // create watcher lists for the root clauses + if ( fRoot && pClause->nLits > 1 ) + { + Pr_ManWatchClause( p, pClause, pClause->pLits[0] ); + Pr_ManWatchClause( p, pClause, pClause->pLits[1] ); + } + return 1; +} + +/**Function************************************************************* + + Synopsis [Fetches memory.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +char * Pr_ManMemoryFetch( Pr_Man_t * p, int nBytes ) +{ + char * pMem; + if ( p->pChunkLast == NULL || nBytes > p->nChunkSize - p->nChunkUsed ) + { + pMem = (char *)malloc( p->nChunkSize ); + *(char **)pMem = p->pChunkLast; + p->pChunkLast = pMem; + p->nChunkUsed = sizeof(char *); + } + pMem = p->pChunkLast + p->nChunkUsed; + p->nChunkUsed += nBytes; + return pMem; +} + +/**Function************************************************************* + + Synopsis [Frees memory manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Pr_ManMemoryStop( Pr_Man_t * p ) +{ + char * pMem, * pNext; + if ( p->pChunkLast == NULL ) + return; + for ( pMem = p->pChunkLast; pNext = *(char **)pMem; pMem = pNext ) + free( pMem ); + free( pMem ); +} + +/**Function************************************************************* + + Synopsis [Records the proof.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Extra_PrintBinary_( FILE * pFile, unsigned Sign[], int nBits ) +{ + int Remainder, nWords; + int w, i; + + Remainder = (nBits%(sizeof(unsigned)*8)); + nWords = (nBits/(sizeof(unsigned)*8)) + (Remainder>0); + + for ( w = nWords-1; w >= 0; w-- ) + for ( i = ((w == nWords-1 && Remainder)? Remainder-1: 31); i >= 0; i-- ) + fprintf( pFile, "%c", '0' + (int)((Sign[w] & (1<<i)) > 0) ); +} + +/**Function************************************************************* + + Synopsis [Prints the interpolant for one clause.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Pr_ManPrintInterOne( Pr_Man_t * p, Pr_Cls_t * pClause ) +{ + printf( "Clause %2d : ", pClause->Id ); + Extra_PrintBinary_( stdout, &pClause->uTruth, (1 << p->nVarsAB) ); + printf( "\n" ); +} + + + +/**Function************************************************************* + + Synopsis [Records implication.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Pr_ManEnqueue( Pr_Man_t * p, lit Lit, Pr_Cls_t * pReason ) +{ + int Var = lit_var(Lit); + if ( p->pAssigns[Var] != LIT_UNDEF ) + return p->pAssigns[Var] == Lit; + p->pAssigns[Var] = Lit; + p->pReasons[Var] = pReason; + p->pTrail[p->nTrailSize++] = Lit; +//printf( "assigning var %d value %d\n", Var, !lit_sign(Lit) ); + return 1; +} + +/**Function************************************************************* + + Synopsis [Records implication.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Pr_ManCancelUntil( Pr_Man_t * p, int Level ) +{ + lit Lit; + int i, Var; + for ( i = p->nTrailSize - 1; i >= Level; i-- ) + { + Lit = p->pTrail[i]; + Var = lit_var( Lit ); + p->pReasons[Var] = NULL; + p->pAssigns[Var] = LIT_UNDEF; +//printf( "cancelling var %d\n", Var ); + } + p->nTrailSize = Level; +} + +/**Function************************************************************* + + Synopsis [Propagate one assignment.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Pr_Cls_t * Pr_ManPropagateOne( Pr_Man_t * p, lit Lit ) +{ + Pr_Cls_t ** ppPrev, * pCur, * pTemp; + lit LitF = lit_neg(Lit); + int i; + // iterate through the literals + ppPrev = p->pWatches + Lit; + for ( pCur = p->pWatches[Lit]; pCur; pCur = *ppPrev ) + { + // make sure the false literal is in the second literal of the clause + if ( pCur->pLits[0] == LitF ) + { + pCur->pLits[0] = pCur->pLits[1]; + pCur->pLits[1] = LitF; + pTemp = pCur->pNext0; + pCur->pNext0 = pCur->pNext1; + pCur->pNext1 = pTemp; + } + assert( pCur->pLits[1] == LitF ); + + // if the first literal is true, the clause is satisfied + if ( pCur->pLits[0] == p->pAssigns[lit_var(pCur->pLits[0])] ) + { + ppPrev = &pCur->pNext1; + continue; + } + + // look for a new literal to watch + for ( i = 2; i < (int)pCur->nLits; i++ ) + { + // skip the case when the literal is false + if ( lit_neg(pCur->pLits[i]) == p->pAssigns[lit_var(pCur->pLits[i])] ) + continue; + // the literal is either true or unassigned - watch it + pCur->pLits[1] = pCur->pLits[i]; + pCur->pLits[i] = LitF; + // remove this clause from the watch list of Lit + *ppPrev = pCur->pNext1; + // add this clause to the watch list of pCur->pLits[i] (now it is pCur->pLits[1]) + Pr_ManWatchClause( p, pCur, pCur->pLits[1] ); + break; + } + if ( i < (int)pCur->nLits ) // found new watch + continue; + + // clause is unit - enqueue new implication + if ( Pr_ManEnqueue(p, pCur->pLits[0], pCur) ) + { + ppPrev = &pCur->pNext1; + continue; + } + + // conflict detected - return the conflict clause + return pCur; + } + return NULL; +} + +/**Function************************************************************* + + Synopsis [Propagate the current assignments.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Pr_Cls_t * Pr_ManPropagate( Pr_Man_t * p, int Start ) +{ + Pr_Cls_t * pClause; + int i; + int clk = clock(); + for ( i = Start; i < p->nTrailSize; i++ ) + { + pClause = Pr_ManPropagateOne( p, p->pTrail[i] ); + if ( pClause ) + { +p->timeBcp += clock() - clk; + return pClause; + } + } +p->timeBcp += clock() - clk; + return NULL; +} + + +/**Function************************************************************* + + Synopsis [Prints the clause.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Pr_ManPrintClause( Pr_Cls_t * pClause ) +{ + int i; + printf( "Clause ID = %d. Proof = %d. {", pClause->Id, (int)pClause->pProof ); + for ( i = 0; i < (int)pClause->nLits; i++ ) + printf( " %d", pClause->pLits[i] ); + printf( " }\n" ); +} + +/**Function************************************************************* + + Synopsis [Prints the resolvent.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Pr_ManPrintResolvent( lit * pResLits, int nResLits ) +{ + int i; + printf( "Resolvent: {" ); + for ( i = 0; i < nResLits; i++ ) + printf( " %d", pResLits[i] ); + printf( " }\n" ); +} + +/**Function************************************************************* + + Synopsis [Writes one root clause into a file.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Pr_ManProofWriteOne( Pr_Man_t * p, Pr_Cls_t * pClause ) +{ + pClause->pProof = (void *)++p->Counter; + + if ( p->fProofWrite ) + { + int v; + fprintf( p->pManProof, "%d", (int)pClause->pProof ); + for ( v = 0; v < (int)pClause->nLits; v++ ) + fprintf( p->pManProof, " %d", lit_print(pClause->pLits[v]) ); + fprintf( p->pManProof, " 0 0\n" ); + } +} + +/**Function************************************************************* + + Synopsis [Traces the proof for one clause.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Pr_ManProofTraceOne( Pr_Man_t * p, Pr_Cls_t * pConflict, Pr_Cls_t * pFinal ) +{ + Pr_Cls_t * pReason; + int i, v, Var, PrevId; + int fPrint = 0; + int clk = clock(); + + // collect resolvent literals + if ( p->fProofVerif ) + { + assert( (int)pConflict->nLits <= p->nResLitsAlloc ); + memcpy( p->pResLits, pConflict->pLits, sizeof(lit) * pConflict->nLits ); + p->nResLits = pConflict->nLits; + } + + // mark all the variables in the conflict as seen + for ( v = 0; v < (int)pConflict->nLits; v++ ) + p->pSeens[lit_var(pConflict->pLits[v])] = 1; + + // start the anticedents +// pFinal->pAntis = Vec_PtrAlloc( 32 ); +// Vec_PtrPush( pFinal->pAntis, pConflict ); + + if ( p->nClausesA ) + pFinal->uTruth = pConflict->uTruth; + + // follow the trail backwards + PrevId = (int)pConflict->pProof; + for ( i = p->nTrailSize - 1; i >= 0; i-- ) + { + // skip literals that are not involved + Var = lit_var(p->pTrail[i]); + if ( !p->pSeens[Var] ) + continue; + + // skip literals of the resulting clause + pReason = p->pReasons[Var]; + if ( pReason == NULL ) + continue; + assert( p->pTrail[i] == pReason->pLits[0] ); + + // record the reason clause + assert( pReason->pProof > 0 ); + p->Counter++; + if ( p->fProofWrite ) + fprintf( p->pManProof, "%d * %d %d 0\n", p->Counter, PrevId, (int)pReason->pProof ); + PrevId = p->Counter; + + if ( p->nClausesA ) + { + if ( p->pVarTypes[Var] == 1 ) // var of A + pFinal->uTruth |= pReason->uTruth; + else + pFinal->uTruth &= pReason->uTruth; + } + + // resolve the temporary resolvent with the reason clause + if ( p->fProofVerif ) + { + int v1, v2; + if ( fPrint ) + Pr_ManPrintResolvent( p->pResLits, p->nResLits ); + // check that the var is present in the resolvent + for ( v1 = 0; v1 < p->nResLits; v1++ ) + if ( lit_var(p->pResLits[v1]) == Var ) + break; + if ( v1 == p->nResLits ) + printf( "Recording clause %d: Cannot find variable %d in the temporary resolvent.\n", pFinal->Id, Var ); + if ( p->pResLits[v1] != lit_neg(pReason->pLits[0]) ) + printf( "Recording clause %d: The resolved variable %d is in the wrong polarity.\n", pFinal->Id, Var ); + // remove this variable from the resolvent + assert( lit_var(p->pResLits[v1]) == Var ); + p->nResLits--; + for ( ; v1 < p->nResLits; v1++ ) + p->pResLits[v1] = p->pResLits[v1+1]; + // add variables of the reason clause + for ( v2 = 1; v2 < (int)pReason->nLits; v2++ ) + { + for ( v1 = 0; v1 < p->nResLits; v1++ ) + if ( lit_var(p->pResLits[v1]) == lit_var(pReason->pLits[v2]) ) + break; + // if it is a new variable, add it to the resolvent + if ( v1 == p->nResLits ) + { + if ( p->nResLits == p->nResLitsAlloc ) + printf( "Recording clause %d: Ran out of space for intermediate resolvent.\n, pFinal->Id" ); + p->pResLits[ p->nResLits++ ] = pReason->pLits[v2]; + continue; + } + // if the variable is the same, the literal should be the same too + if ( p->pResLits[v1] == pReason->pLits[v2] ) + continue; + // the literal is different + printf( "Recording clause %d: Trying to resolve the clause with more than one opposite literal.\n", pFinal->Id ); + } + } + + // add the variables to seen + for ( v = 1; v < (int)pReason->nLits; v++ ) + p->pSeens[lit_var(pReason->pLits[v])] = 1; + +// Vec_PtrPush( pFinal->pAntis, pReason ); + } + + // unmark all seen variables + for ( i = p->nTrailSize - 1; i >= 0; i-- ) + p->pSeens[lit_var(p->pTrail[i])] = 0; + + // use the resulting clause to check the correctness of resolution + if ( p->fProofVerif ) + { + int v1, v2; + if ( fPrint ) + Pr_ManPrintResolvent( p->pResLits, p->nResLits ); + for ( v1 = 0; v1 < p->nResLits; v1++ ) + { + for ( v2 = 0; v2 < (int)pFinal->nLits; v2++ ) + if ( pFinal->pLits[v2] == p->pResLits[v1] ) + break; + if ( v2 < (int)pFinal->nLits ) + continue; + break; + } + if ( v1 < p->nResLits ) + { + printf( "Recording clause %d: The final resolvent is wrong.\n", pFinal->Id ); + Pr_ManPrintClause( pConflict ); + Pr_ManPrintResolvent( p->pResLits, p->nResLits ); + Pr_ManPrintClause( pFinal ); + } + } +p->timeTrace += clock() - clk; + + // return the proof pointer + if ( p->nClausesA ) + { + Pr_ManPrintInterOne( p, pFinal ); + } + return p->Counter; +} + +/**Function************************************************************* + + Synopsis [Records the proof for one clause.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Pr_ManProofRecordOne( Pr_Man_t * p, Pr_Cls_t * pClause ) +{ + Pr_Cls_t * pConflict; + int i; + + // empty clause never ends up there + assert( pClause->nLits > 0 ); + if ( pClause->nLits == 0 ) + printf( "Error: Empty clause is attempted.\n" ); + + // add assumptions to the trail + assert( !pClause->fRoot ); + assert( p->nTrailSize == p->nRootSize ); + for ( i = 0; i < (int)pClause->nLits; i++ ) + if ( !Pr_ManEnqueue( p, lit_neg(pClause->pLits[i]), NULL ) ) + { + assert( 0 ); // impossible + return 0; + } + + // propagate the assumptions + pConflict = Pr_ManPropagate( p, p->nRootSize ); + if ( pConflict == NULL ) + { + assert( 0 ); // cannot prove + return 0; + } + + // construct the proof + pClause->pProof = (void *)Pr_ManProofTraceOne( p, pConflict, pClause ); + + // undo to the root level + Pr_ManCancelUntil( p, p->nRootSize ); + + // add large clauses to the watched lists + if ( pClause->nLits > 1 ) + { + Pr_ManWatchClause( p, pClause, pClause->pLits[0] ); + Pr_ManWatchClause( p, pClause, pClause->pLits[1] ); + return 1; + } + assert( pClause->nLits == 1 ); + + // if the clause proved is unit, add it and propagate + if ( !Pr_ManEnqueue( p, pClause->pLits[0], pClause ) ) + { + assert( 0 ); // impossible + return 0; + } + + // propagate the assumption + pConflict = Pr_ManPropagate( p, p->nRootSize ); + if ( pConflict ) + { + // construct the proof + p->pEmpty->pProof = (void *)Pr_ManProofTraceOne( p, pConflict, p->pEmpty ); + printf( "Found last conflict after adding unit clause number %d!\n", pClause->Id ); + return 0; + } + + // update the root level + p->nRootSize = p->nTrailSize; + return 1; +} + +/**Function************************************************************* + + Synopsis [Propagate the root clauses.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Pr_ManProcessRoots( Pr_Man_t * p ) +{ + Pr_Cls_t * pClause; + int Counter; + + // make sure the root clauses are preceeding the learnt clauses + Counter = 0; + Pr_ManForEachClause( p, pClause ) + { + assert( (int)pClause->fA == (Counter < (int)p->nClausesA) ); + assert( (int)pClause->fRoot == (Counter < (int)p->nRoots) ); + Counter++; + } + assert( p->nClauses == Counter ); + + // make sure the last clause if empty + assert( p->pTail->nLits == 0 ); + + // go through the root unit clauses + p->nTrailSize = 0; + Pr_ManForEachClauseRoot( p, pClause ) + { + // empty clause and large clauses + if ( pClause->nLits != 1 ) + continue; + // unit clause + assert( lit_check(pClause->pLits[0], p->nVars) ); + if ( !Pr_ManEnqueue( p, pClause->pLits[0], pClause ) ) + { + // detected root level conflict + printf( "Pr_ManProcessRoots(): Detected a root-level conflict\n" ); + assert( 0 ); + return 0; + } + } + + // propagate the root unit clauses + pClause = Pr_ManPropagate( p, 0 ); + if ( pClause ) + { + // detected root level conflict + printf( "Pr_ManProcessRoots(): Detected a root-level conflict\n" ); + assert( 0 ); + return 0; + } + + // set the root level + p->nRootSize = p->nTrailSize; + return 1; +} + +/**Function************************************************************* + + Synopsis [Records the proof.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Pr_ManPrepareInter( Pr_Man_t * p ) +{ + unsigned uTruths[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 }; + Pr_Cls_t * pClause; + int Var, v; + + // mark the variable encountered in the clauses of A + Pr_ManForEachClauseRoot( p, pClause ) + { + if ( !pClause->fA ) + break; + for ( v = 0; v < (int)pClause->nLits; v++ ) + p->pVarTypes[lit_var(pClause->pLits[v])] = 1; + } + + // check variables that appear in clauses of B + p->nVarsAB = 0; + Pr_ManForEachClauseRoot( p, pClause ) + { + if ( pClause->fA ) + continue; + for ( v = 0; v < (int)pClause->nLits; v++ ) + { + Var = lit_var(pClause->pLits[v]); + if ( p->pVarTypes[Var] == 1 ) // var of A + { + // change it into a global variable + p->nVarsAB++; + p->pVarTypes[Var] = -1; + } + } + } + + // order global variables + p->nVarsAB = 0; + for ( v = 0; v < p->nVars; v++ ) + if ( p->pVarTypes[v] == -1 ) + p->pVarTypes[v] -= p->nVarsAB++; +printf( "There are %d global variables.\n", p->nVarsAB ); + + // set interpolants for root clauses + Pr_ManForEachClauseRoot( p, pClause ) + { + if ( !pClause->fA ) // clause of B + { + pClause->uTruth = ~0; + Pr_ManPrintInterOne( p, pClause ); + continue; + } + // clause of A + pClause->uTruth = 0; + for ( v = 0; v < (int)pClause->nLits; v++ ) + { + Var = lit_var(pClause->pLits[v]); + if ( p->pVarTypes[Var] < 0 ) // global var + { + if ( lit_sign(pClause->pLits[v]) ) // negative var + pClause->uTruth |= ~uTruths[ -p->pVarTypes[Var]-1 ]; + else + pClause->uTruth |= uTruths[ -p->pVarTypes[Var]-1 ]; + } + } + Pr_ManPrintInterOne( p, pClause ); + } +} + +/**Function************************************************************* + + Synopsis [Records the proof.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Pr_ManProofWrite( Pr_Man_t * p ) +{ + Pr_Cls_t * pClause; + int RetValue = 1; + + // propagate root level assignments + Pr_ManProcessRoots( p ); + + // prepare the interpolant computation + if ( p->nClausesA ) + Pr_ManPrepareInter( p ); + + // construct proof for each clause + // start the proof + if ( p->fProofWrite ) + p->pManProof = fopen( "proof.cnf_", "w" ); + p->Counter = 0; + + // write the root clauses + Pr_ManForEachClauseRoot( p, pClause ) + Pr_ManProofWriteOne( p, pClause ); + + // consider each learned clause + Pr_ManForEachClauseLearnt( p, pClause ) + { + if ( !Pr_ManProofRecordOne( p, pClause ) ) + { + RetValue = 0; + break; + } + } + + if ( p->nClausesA ) + { + printf( "Interpolant: " ); + } + + + // stop the proof + if ( p->fProofWrite ) + { + fclose( p->pManProof ); + p->pManProof = NULL; + } + return RetValue; +} + +/**Function************************************************************* + + Synopsis [Reads clauses from file.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Pr_Man_t * Pr_ManProofRead( char * pFileName ) +{ + Pr_Man_t * p = NULL; + char * pCur, * pBuffer = NULL; + int * pArray = NULL; + FILE * pFile; + int RetValue, Counter, nNumbers, Temp; + int nClauses, nClausesA, nRoots, nVars; + + // open the file + pFile = fopen( pFileName, "r" ); + if ( pFile == NULL ) + { + printf( "Count not open input file \"%s\".\n", pFileName ); + return NULL; + } + + // read the file + pBuffer = (char *)malloc( (1<<16) ); + for ( Counter = 0; fgets( pBuffer, (1<<16), pFile ); ) + { + if ( pBuffer[0] == 'c' ) + continue; + if ( pBuffer[0] == 'p' ) + { + assert( p == NULL ); + nClausesA = 0; + RetValue = sscanf( pBuffer + 1, "%d %d %d %d", &nVars, &nClauses, &nRoots, &nClausesA ); + if ( RetValue != 3 && RetValue != 4 ) + { + printf( "Wrong input file format.\n" ); + } + p = Pr_ManAlloc( nVars ); + pArray = (int *)malloc( sizeof(int) * (nVars + 10) ); + continue; + } + // skip empty lines + for ( pCur = pBuffer; *pCur; pCur++ ) + if ( !(*pCur == ' ' || *pCur == '\t' || *pCur == '\r' || *pCur == '\n') ) + break; + if ( *pCur == 0 ) + continue; + // scan the numbers from file + nNumbers = 0; + pCur = pBuffer; + while ( *pCur ) + { + // skip spaces + for ( ; *pCur && *pCur == ' '; pCur++ ); + // read next number + Temp = 0; + sscanf( pCur, "%d", &Temp ); + if ( Temp == 0 ) + break; + pArray[ nNumbers++ ] = lit_read( Temp ); + // skip non-spaces + for ( ; *pCur && *pCur != ' '; pCur++ ); + } + // add the clause + if ( !Pr_ManAddClause( p, pArray, pArray + nNumbers, Counter < nRoots, Counter < nClausesA ) ) + { + printf( "Bad clause number %d.\n", Counter ); + return NULL; + } + // count the clauses + Counter++; + } + // check the number of clauses + if ( Counter != nClauses ) + printf( "Expected %d clauses but read %d.\n", nClauses, Counter ); + + // finish + if ( pArray ) free( pArray ); + if ( pBuffer ) free( pBuffer ); + fclose( pFile ); + return p; +} + +/**Function************************************************************* + + Synopsis [Records the proof.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +/* +int Pr_ManProofCount_rec( Pr_Cls_t * pClause ) +{ + Pr_Cls_t * pNext; + int i, Counter; + if ( pClause->fRoot ) + return 0; + if ( pClause->fVisit ) + return 0; + pClause->fVisit = 1; + // count the number of visited clauses + Counter = 1; + Vec_PtrForEachEntry( pClause->pAntis, pNext, i ) + Counter += Pr_ManProofCount_rec( pNext ); + return Counter; +} +*/ + +/**Function************************************************************* + + Synopsis [Records the proof.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Pr_ManProofTest( char * pFileName ) +{ + Pr_Man_t * p; + int clk, clkTotal = clock(); + +clk = clock(); + p = Pr_ManProofRead( pFileName ); +p->timeRead = clock() - clk; + if ( p == NULL ) + return 0; + + Pr_ManProofWrite( p ); + + // print stats +/* + nUsed = Pr_ManProofCount_rec( p->pEmpty ); + printf( "Roots = %d. Learned = %d. Total = %d. Steps = %d. Ave = %.2f. Used = %d. Ratio = %.2f. \n", + p->nRoots, p->nClauses-p->nRoots, p->nClauses, p->Counter, + 1.0*(p->Counter-p->nRoots)/(p->nClauses-p->nRoots), + nUsed, 1.0*nUsed/(p->nClauses-p->nRoots) ); +*/ + printf( "Vars = %d. Roots = %d. Learned = %d. Resolution steps = %d. Ave = %.2f.\n", + p->nVars, p->nRoots, p->nClauses-p->nRoots, p->Counter, + 1.0*(p->Counter-p->nRoots)/(p->nClauses-p->nRoots) ); + +p->timeTotal = clock() - clkTotal; + Pr_ManFree( p ); + return 1; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/sat/proof/pr.h b/src/sat/proof/pr.h new file mode 100644 index 00000000..1e71a2d3 --- /dev/null +++ b/src/sat/proof/pr.h @@ -0,0 +1,65 @@ +/**CFile**************************************************************** + + FileName [pr.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Proof recording.] + + Synopsis [External declarations.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: pr.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef __PR_H__ +#define __PR_H__ + +#ifdef __cplusplus +extern "C" { +#endif + +#ifdef _WIN32 +#define inline __inline // compatible with MS VS 6.0 +#endif + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// BASIC TYPES /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Pr_Man_t_ Pr_Man_t; + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +/*=== pr.c ==========================================================*/ + +#ifdef __cplusplus +} +#endif + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + diff --git a/src/sat/proof/stats.txt b/src/sat/proof/stats.txt new file mode 100644 index 00000000..470b1630 --- /dev/null +++ b/src/sat/proof/stats.txt @@ -0,0 +1,66 @@ +UC Berkeley, ABC 1.01 (compiled Jan 20 2007 16:47:34) +abc.rc: No such file or directory +Loaded "abc.rc" from the parent directory. +abc 01> test +Found last conflict after adding unit clause number 10229! +Roots = 7184. Learned = 3047. Total = 10231. Steps = 196361. Ave = 62.09. Used = 2224. Ratio = 0.73. +Runtime stats: +Reading = 0.03 sec +BCP = 0.32 sec +Trace = 0.06 sec +TOTAL = 0.43 sec +abc 01> test +Found last conflict after adding unit clause number 7676! +Roots = 6605. Learned = 1073. Total = 7678. Steps = 52402. Ave = 42.68. Used = 1011. Ratio = 0.94. +Runtime stats: +Reading = 0.01 sec +BCP = 0.02 sec +Trace = 0.02 sec +TOTAL = 0.06 sec +abc 01> test +Found last conflict after adding unit clause number 37868! +Roots = 15443. Learned = 22427. Total = 37870. Steps = 2365472. Ave = 104.79. Used = 19763. Ratio = 0.88. +Runtime stats: +Reading = 0.20 sec +BCP = 14.67 sec +Trace = 0.56 sec +TOTAL = 15.74 sec +abc 01> + + +abc 05> wb ibm_bmc/len25u_renc.blif +abc 05> ps +(no name) : i/o = 348/ 1 lat = 0 nd = 3648 bdd = 15522 lev = 246 +abc 05> sat -v +==================================[MINISAT]=================================== +| Conflicts | ORIGINAL | LEARNT | Progress | +| | Clauses Literals | Limit Clauses Literals Lit/Cl | | +============================================================================== +| 0 | 17413 54996 | 5804 0 0 0.0 | 0.000 % | +| 100 | 17413 54996 | 6384 100 606 6.1 | 0.417 % | +| 250 | 17413 54996 | 7023 250 1586 6.3 | 0.417 % | +| 476 | 17413 54996 | 7725 476 3288 6.9 | 0.417 % | +| 813 | 17413 54996 | 8498 813 7586 9.3 | 0.417 % | +| 1319 | 17403 54970 | 9347 1318 14848 11.3 | 0.442 % | +| 2078 | 17403 54970 | 10282 2076 40186 19.4 | 0.466 % | +| 3217 | 17397 54948 | 11310 3208 99402 31.0 | 0.466 % | +| 4926 | 17392 54930 | 12441 4911 131848 26.8 | 0.491 % | +| 7489 | 17392 54930 | 13686 7474 204217 27.3 | 0.491 % | +| 11336 | 17357 54829 | 15054 11310 332863 29.4 | 0.638 % | +| 17103 | 17346 54794 | 16559 9130 203029 22.2 | 0.687 % | +| 25752 | 17288 54606 | 18215 9083 176982 19.5 | 0.834 % | +| 38727 | 17266 54536 | 20037 12674 278949 22.0 | 0.883 % | +| 58188 | 17240 54453 | 22041 11905 255255 21.4 | 0.957 % | +============================================================================== +Start = 15. Conf = 79435. Dec = 130967. Prop = 24083434. Insp = 136774586. +Total runtime = 18.66 sec. Var select = 0.00 sec. Var update = 0.00 sec. +UNSATISFIABLE Time = 18.69 sec +abc 05> +abc 05> test +Found last conflict after adding unit clause number 96902! +Roots = 17469. Learned = 79435. Total = 96904. Steps = 9700042. Ave = 121.89. Used = 57072. Ratio = 0.72. +Runtime stats: +Reading = 1.26 sec +BCP = 204.99 sec +Trace = 2.85 sec +TOTAL = 209.85 sec
\ No newline at end of file |