diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index d06867617..a86c4848b 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -540,6 +540,7 @@ static int Abc_CommandAbc9PoPart ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandAbc9GroupProve ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9MultiProve ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9SplitProve ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9SplitSat ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Bmc ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9SBmc ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9ChainBmc ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -1300,6 +1301,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "ABC9", "&gprove", Abc_CommandAbc9GroupProve, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&mprove", Abc_CommandAbc9MultiProve, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&splitprove", Abc_CommandAbc9SplitProve, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&splitsat", Abc_CommandAbc9SplitSat, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&bmc", Abc_CommandAbc9Bmc, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&bmcs", Abc_CommandAbc9SBmc, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&chainbmc", Abc_CommandAbc9ChainBmc, 0 ); @@ -46082,6 +46084,159 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandAbc9SplitSat( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern void Cnf_SplitSat( char * pFileName, int iVarBeg, int iVarEnd, int nLits, int Value, int TimeOut, int nProcs, int nIters, int Seed, int fVerbose ); + int c, iVarBeg = 0, iVarEnd = ABC_INFINITY, nLits = 10, Value = 2, TimeOut = 5, nProcs = 1, nIters = 1, Seed = 0, fVerbose = 0; char * pFileName = NULL; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "BENVTPISvh" ) ) != EOF ) + { + switch ( c ) + { + case 'B': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-B\" should be followed by a positive integer.\n" ); + goto usage; + } + iVarBeg = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( iVarBeg < 0 ) + goto usage; + break; + case 'E': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-E\" should be followed by a positive integer.\n" ); + goto usage; + } + iVarEnd = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( iVarEnd < 0 ) + goto usage; + break; + case 'N': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-N\" should be followed by a positive integer.\n" ); + goto usage; + } + nLits = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nLits < 0 ) + goto usage; + break; + case 'V': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-V\" should be followed by a positive integer.\n" ); + goto usage; + } + Value = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( Value < 0 || Value > 2 ) + goto usage; + break; + case 'T': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-T\" should be followed by a positive integer.\n" ); + goto usage; + } + TimeOut = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( TimeOut < 0 ) + goto usage; + break; + case 'P': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-P\" should be followed by a positive integer.\n" ); + goto usage; + } + nProcs = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nProcs <= 0 ) + goto usage; + break; + case 'I': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" ); + goto usage; + } + nIters = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nIters < 0 ) + goto usage; + break; + case 'S': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" ); + goto usage; + } + Seed = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( Seed < 0 ) + goto usage; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + // get the file name + if ( argc != globalUtilOptind + 1 ) + { + Abc_Print( -1, "Abc_CommandAbc9SplitSat(): CNF file names should be given on the command line.\n" ); + return 1; + } + { + FILE * pFile; + pFileName = argv[globalUtilOptind]; + pFile = fopen( pFileName, "r" ); + if ( pFile == NULL ) + { + Abc_Print( -1, "Cannot open file \"%s\" with the input test patterns.\n", pFileName ); + return 0; + } + fclose( pFile ); + } + Cnf_SplitSat( pFileName, iVarBeg, iVarEnd, nLits, Value, TimeOut, nProcs, nIters, Seed, fVerbose ); + return 0; + +usage: + Abc_Print( -2, "usage: &splitsat [-BENVTPIS num] [-vh]\n" ); + Abc_Print( -2, "\t solves CNF-based SAT problem by randomized case-splitting\n" ); + Abc_Print( -2, "\t-B num : the first CNF variable to use for splitting [default = %d]\n", iVarBeg ); + Abc_Print( -2, "\t-E num : the last CNF variable to use for splitting [default = %d]\n", iVarEnd ); + Abc_Print( -2, "\t-N num : the number of CNF variables to use for splitting [default = %d]\n", nLits ); + Abc_Print( -2, "\t-V num : the variable values to use (0, 1, or 2 for \"any\") [default = %d]\n", Value ); + Abc_Print( -2, "\t-T num : the runtime limit in seconds per subproblem [default = %d]\n", TimeOut ); + Abc_Print( -2, "\t-P num : the number of concurrent processes [default = %d]\n", nProcs ); + Abc_Print( -2, "\t-I num : the max number of iterations (0 = infinity) [default = %d]\n", nIters ); + Abc_Print( -2, "\t-S num : the random seed used to generate cofactors [default = %d]\n", Seed ); + Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + return 1; +} + /**Function************************************************************* Synopsis [] diff --git a/src/sat/cnf/cnf.h b/src/sat/cnf/cnf.h index f79c67798..1fbf58049 100644 --- a/src/sat/cnf/cnf.h +++ b/src/sat/cnf/cnf.h @@ -155,6 +155,7 @@ extern Vec_Int_t * Cnf_DataCollectPiSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p extern Cnf_Dat_t * Cnf_DataAlloc( Aig_Man_t * pAig, int nVars, int nClauses, int nLiterals ); extern Cnf_Dat_t * Cnf_DataDup( Cnf_Dat_t * p ); extern Cnf_Dat_t * Cnf_DataDupCof( Cnf_Dat_t * p, int Lit ); +extern Cnf_Dat_t * Cnf_DataDupCofArray( Cnf_Dat_t * p, Vec_Int_t * vLits ); extern void Cnf_DataFree( Cnf_Dat_t * p ); extern void Cnf_DataLift( Cnf_Dat_t * p, int nVarsPlus ); extern void Cnf_DataCollectFlipLits( Cnf_Dat_t * p, int iFlipVar, Vec_Int_t * vFlips ); diff --git a/src/sat/cnf/cnfMan.c b/src/sat/cnf/cnfMan.c index 518a066be..16a4cf219 100644 --- a/src/sat/cnf/cnfMan.c +++ b/src/sat/cnf/cnfMan.c @@ -175,6 +175,23 @@ Cnf_Dat_t * Cnf_DataDupCof( Cnf_Dat_t * p, int Lit ) assert( pCnf->pClauses[p->nClauses+1] == pCnf->pClauses[0] + p->nLiterals+1 ); return pCnf; } +Cnf_Dat_t * Cnf_DataDupCofArray( Cnf_Dat_t * p, Vec_Int_t * vLits ) +{ + Cnf_Dat_t * pCnf; + int i, iLit; + pCnf = Cnf_DataAlloc( p->pMan, p->nVars, p->nClauses+Vec_IntSize(vLits), p->nLiterals+Vec_IntSize(vLits) ); + memcpy( pCnf->pClauses[0], p->pClauses[0], sizeof(int) * p->nLiterals ); + if ( pCnf->pVarNums ) + memcpy( pCnf->pVarNums, p->pVarNums, sizeof(int) * Aig_ManObjNumMax(p->pMan) ); + for ( i = 1; i < p->nClauses; i++ ) + pCnf->pClauses[i] = pCnf->pClauses[0] + (p->pClauses[i] - p->pClauses[0]); + Vec_IntForEachEntry( vLits, iLit, i ) { + pCnf->pClauses[p->nClauses+i] = pCnf->pClauses[0] + p->nLiterals+i; + pCnf->pClauses[p->nClauses+i][0] = iLit; + } + assert( pCnf->pClauses[p->nClauses+Vec_IntSize(vLits)] == pCnf->pClauses[0] + p->nLiterals+Vec_IntSize(vLits) ); + return pCnf; +} /**Function************************************************************* diff --git a/src/sat/cnf/cnfUtil.c b/src/sat/cnf/cnfUtil.c index d15e83665..9d1bb9722 100644 --- a/src/sat/cnf/cnfUtil.c +++ b/src/sat/cnf/cnfUtil.c @@ -9,7 +9,7 @@ Synopsis [] Author [Alan Mishchenko] - + Affiliation [UC Berkeley] Date [Ver. 1.0. Started - April 28, 2007.] @@ -23,55 +23,249 @@ ABC_NAMESPACE_IMPL_START +#ifdef ABC_USE_PTHREADS + +#ifdef _WIN32 +#include "../lib/pthread.h" +#else +#include +#include +#endif + +#endif //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +extern Vec_Int_t *Exa4_ManParse(char *pFileName); + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* - Synopsis [Computes area, references, and nodes used in the mapping.] + Synopsis [Solving problems using one core.] Description [] - + SideEffects [] SeeAlso [] ***********************************************************************/ -int Aig_ManScanMapping_rec( Cnf_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vMapped ) +Vec_Int_t *Cnf_RunSolverOnce(int Id, int Rand, int TimeOut, int fVerbose) { - Aig_Obj_t * pLeaf; - Dar_Cut_t * pCutBest; - int aArea, i; - if ( pObj->nRefs++ || Aig_ObjIsCi(pObj) || Aig_ObjIsConst1(pObj) ) + int fVerboseSolver = 0; + Vec_Int_t *vRes = NULL; + abctime clkTotal = Abc_Clock(); + char FileNameIn[100], FileNameOut[100]; + sprintf(FileNameIn, "%02d.cnf", Id); + sprintf(FileNameOut, "%02d.txt", Id); +#ifdef _WIN32 + char *pKissat = "kissat.exe"; +#else + char *pKissat = "kissat"; +#endif + char Command[1000], *pCommand = (char *)&Command; + if (TimeOut) + sprintf(pCommand, "%s --seed=%d --time=%d %s %s > %s", pKissat, Rand, TimeOut, fVerboseSolver ? "" : "-q", FileNameIn, FileNameOut); + else + sprintf(pCommand, "%s --seed=%d %s %s > %s", pKissat, Rand, fVerboseSolver ? "" : "-q", FileNameIn, FileNameOut); + //printf( "Thread command: %s\n", pCommand); + if (system(pCommand) == -1) { + fprintf(stdout, "Command \"%s\" did not succeed.\n", pCommand); return 0; - assert( Aig_ObjIsAnd(pObj) ); - // collect the node first to derive pre-order - if ( vMapped ) - Vec_PtrPush( vMapped, pObj ); - // visit the transitive fanin of the selected cut - if ( pObj->fMarkB ) + } + vRes = Exa4_ManParse(FileNameOut); // FileNameOut is removed here + if (fVerbose) { + double SolvingTime = ((double)(Abc_Clock() - clkTotal))/((double)CLOCKS_PER_SEC); + if (vRes) + printf("Problem %2d has a solution. ", Id); + else if (vRes == NULL && (TimeOut == 0 || SolvingTime < (double)TimeOut)) + printf("Problem %2d has no solution. ", Id); + else if (vRes == NULL) + printf("Problem %2d has no solution or timed out after %d sec. ", Id, TimeOut); + Abc_PrintTime(1, "Solving time", Abc_Clock() - clkTotal ); + } + else if (vRes) { + printf("Problem %2d has a solution. ", Id); + Abc_PrintTime(1, "Solving time", Abc_Clock() - clkTotal ); + printf("(Currently waiting for %d sec for other threads to finish.)\n", TimeOut); + } + return vRes; +} +Vec_Int_t * Cnf_RunSolverArray(int nProcs, int TimeOut, int fVerbose) +{ + Vec_Int_t *vRes = NULL; int i; + for ( i = 0; i < nProcs; i++ ) + if ((vRes = Cnf_RunSolverOnce(i, 0, TimeOut, fVerbose))) + break; + return vRes; +} + +/**Function************************************************************* + + Synopsis [Solving problems using many cores.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +#ifndef ABC_USE_PTHREADS + +Vec_Int_t *Cnf_RunSolver(int nProcs, int TimeOut, int fVerbose) +{ + return Cnf_RunSolverArray(nProcs, TimeOut, fVerbose); +} + +#else // pthreads are used + +#define PAR_THR_MAX 100 +typedef struct Cnf_ThData_t_ +{ + Vec_Int_t *vRes; + int Index; + int Rand; + int nTimeOut; + int fWorking; + int fVerbose; +} Cnf_ThData_t; + +void *Cnf_WorkerThread(void *pArg) +{ + Cnf_ThData_t *pThData = (Cnf_ThData_t *)pArg; + volatile int *pPlace = &pThData->fWorking; + while (1) { - Vec_Ptr_t * vSuper = Vec_PtrAlloc( 100 ); - Aig_ObjCollectSuper( pObj, vSuper ); + while (*pPlace == 0) + ; + assert(pThData->fWorking); + if (pThData->Index == -1) + { + pthread_exit(NULL); + assert(0); + return NULL; + } + pThData->vRes = Cnf_RunSolverOnce(pThData->Index, pThData->Rand, pThData->nTimeOut, pThData->fVerbose); + pThData->fWorking = 0; + } + assert(0); + return NULL; +} + +Vec_Int_t *Cnf_RunSolver(int nProcs, int TimeOut, int fVerbose) +{ + Vec_Int_t *vRes = NULL; + Cnf_ThData_t ThData[PAR_THR_MAX]; + pthread_t WorkerThread[PAR_THR_MAX]; + int i, k, status; + if (fVerbose) + printf("Running concurrent solving with %d processes.\n", nProcs); + fflush(stdout); + if (nProcs < 2) + return Cnf_RunSolverArray(nProcs, TimeOut, fVerbose); + // subtract manager thread + // nProcs--; + assert(nProcs >= 1 && nProcs <= PAR_THR_MAX); + // start threads + for (i = 0; i < nProcs; i++) + { + ThData[i].vRes = NULL; + ThData[i].Index = -1; + ThData[i].Rand = Abc_Random(0) % 0x1000000; + ThData[i].nTimeOut = TimeOut; + ThData[i].fWorking = 0; + ThData[i].fVerbose = fVerbose; + status = pthread_create(WorkerThread + i, NULL, Cnf_WorkerThread, (void *)(ThData + i)); + assert(status == 0); + } + // look at the threads + for (k = 0; k < nProcs;) + { + for (i = 0; i < nProcs; i++) + { + if (ThData[i].fWorking) + continue; + if (ThData[i].vRes) + { + k = nProcs; + break; + } + ThData[i].Index = k++; + ThData[i].fWorking = 1; + break; + } + } + // wait till threads finish + for (i = 0; i < nProcs; i++) + if (ThData[i].fWorking) + i = -1; + // stop threads + for (i = 0; i < nProcs; i++) + { + assert(!ThData[i].fWorking); + if (ThData[i].vRes && vRes == NULL) + { + vRes = ThData[i].vRes; + ThData[i].vRes = NULL; + } + Vec_IntFreeP(&ThData[i].vRes); + // stop + ThData[i].Index = -1; + ThData[i].fWorking = 1; + } + return vRes; +} + +#endif // pthreads are used + + + +/**Function************************************************************* + + Synopsis [Computes area, references, and nodes used in the mapping.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_ManScanMapping_rec(Cnf_Man_t *p, Aig_Obj_t *pObj, Vec_Ptr_t *vMapped) +{ + Aig_Obj_t *pLeaf; + Dar_Cut_t *pCutBest; + int aArea, i; + if (pObj->nRefs++ || Aig_ObjIsCi(pObj) || Aig_ObjIsConst1(pObj)) + return 0; + assert(Aig_ObjIsAnd(pObj)); + // collect the node first to derive pre-order + if (vMapped) + Vec_PtrPush(vMapped, pObj); + // visit the transitive fanin of the selected cut + if (pObj->fMarkB) + { + Vec_Ptr_t *vSuper = Vec_PtrAlloc(100); + Aig_ObjCollectSuper(pObj, vSuper); aArea = Vec_PtrSize(vSuper) + 1; - Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pLeaf, i ) - aArea += Aig_ManScanMapping_rec( p, Aig_Regular(pLeaf), vMapped ); - Vec_PtrFree( vSuper ); + Vec_PtrForEachEntry(Aig_Obj_t *, vSuper, pLeaf, i) + aArea += Aig_ManScanMapping_rec(p, Aig_Regular(pLeaf), vMapped); + Vec_PtrFree(vSuper); //////////////////////////// pObj->fMarkB = 1; } else { - pCutBest = Dar_ObjBestCut( pObj ); - aArea = Cnf_CutSopCost( p, pCutBest ); - Dar_CutForEachLeaf( p->pManAig, pCutBest, pLeaf, i ) - aArea += Aig_ManScanMapping_rec( p, pLeaf, vMapped ); + pCutBest = Dar_ObjBestCut(pObj); + aArea = Cnf_CutSopCost(p, pCutBest); + Dar_CutForEachLeaf(p->pManAig, pCutBest, pLeaf, i) + aArea += Aig_ManScanMapping_rec(p, pLeaf, vMapped); } return aArea; } @@ -81,28 +275,28 @@ int Aig_ManScanMapping_rec( Cnf_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vMapped Synopsis [Computes area, references, and nodes used in the mapping.] Description [Collects the nodes in reverse topological order.] - + SideEffects [] SeeAlso [] ***********************************************************************/ -Vec_Ptr_t * Aig_ManScanMapping( Cnf_Man_t * p, int fCollect ) +Vec_Ptr_t *Aig_ManScanMapping(Cnf_Man_t *p, int fCollect) { - Vec_Ptr_t * vMapped = NULL; - Aig_Obj_t * pObj; + Vec_Ptr_t *vMapped = NULL; + Aig_Obj_t *pObj; int i; // clean all references - Aig_ManForEachObj( p->pManAig, pObj, i ) + Aig_ManForEachObj(p->pManAig, pObj, i) pObj->nRefs = 0; // allocate the array - if ( fCollect ) - vMapped = Vec_PtrAlloc( 1000 ); + if (fCollect) + vMapped = Vec_PtrAlloc(1000); // collect nodes reachable from POs in the DFS order through the best cuts p->aArea = 0; - Aig_ManForEachCo( p->pManAig, pObj, i ) - p->aArea += Aig_ManScanMapping_rec( p, Aig_ObjFanin0(pObj), vMapped ); -// printf( "Variables = %6d. Clauses = %8d.\n", vMapped? Vec_PtrSize(vMapped) + Aig_ManCiNum(p->pManAig) + 1 : 0, p->aArea + 2 ); + Aig_ManForEachCo(p->pManAig, pObj, i) + p->aArea += Aig_ManScanMapping_rec(p, Aig_ObjFanin0(pObj), vMapped); + // printf( "Variables = %6d. Clauses = %8d.\n", vMapped? Vec_PtrSize(vMapped) + Aig_ManCiNum(p->pManAig) + 1 : 0, p->aArea + 2 ); return vMapped; } @@ -111,48 +305,48 @@ Vec_Ptr_t * Aig_ManScanMapping( Cnf_Man_t * p, int fCollect ) Synopsis [Computes area, references, and nodes used in the mapping.] Description [] - + SideEffects [] SeeAlso [] ***********************************************************************/ -int Cnf_ManScanMapping_rec( Cnf_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vMapped, int fPreorder ) +int Cnf_ManScanMapping_rec(Cnf_Man_t *p, Aig_Obj_t *pObj, Vec_Ptr_t *vMapped, int fPreorder) { - Aig_Obj_t * pLeaf; - Cnf_Cut_t * pCutBest; + Aig_Obj_t *pLeaf; + Cnf_Cut_t *pCutBest; int aArea, i; - if ( pObj->nRefs++ || Aig_ObjIsCi(pObj) || Aig_ObjIsConst1(pObj) ) + if (pObj->nRefs++ || Aig_ObjIsCi(pObj) || Aig_ObjIsConst1(pObj)) return 0; - assert( Aig_ObjIsAnd(pObj) ); - assert( pObj->pData != NULL ); + assert(Aig_ObjIsAnd(pObj)); + assert(pObj->pData != NULL); // add the node to the mapping - if ( vMapped && fPreorder ) - Vec_PtrPush( vMapped, pObj ); + if (vMapped && fPreorder) + Vec_PtrPush(vMapped, pObj); // visit the transitive fanin of the selected cut - if ( pObj->fMarkB ) + if (pObj->fMarkB) { - Vec_Ptr_t * vSuper = Vec_PtrAlloc( 100 ); - Aig_ObjCollectSuper( pObj, vSuper ); + Vec_Ptr_t *vSuper = Vec_PtrAlloc(100); + Aig_ObjCollectSuper(pObj, vSuper); aArea = Vec_PtrSize(vSuper) + 1; - Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pLeaf, i ) - aArea += Cnf_ManScanMapping_rec( p, Aig_Regular(pLeaf), vMapped, fPreorder ); - Vec_PtrFree( vSuper ); + Vec_PtrForEachEntry(Aig_Obj_t *, vSuper, pLeaf, i) + aArea += Cnf_ManScanMapping_rec(p, Aig_Regular(pLeaf), vMapped, fPreorder); + Vec_PtrFree(vSuper); //////////////////////////// pObj->fMarkB = 1; } else { pCutBest = (Cnf_Cut_t *)pObj->pData; -// assert( pCutBest->nFanins > 0 ); - assert( pCutBest->Cost < 127 ); + // assert( pCutBest->nFanins > 0 ); + assert(pCutBest->Cost < 127); aArea = pCutBest->Cost; - Cnf_CutForEachLeaf( p->pManAig, pCutBest, pLeaf, i ) - aArea += Cnf_ManScanMapping_rec( p, pLeaf, vMapped, fPreorder ); + Cnf_CutForEachLeaf(p->pManAig, pCutBest, pLeaf, i) + aArea += Cnf_ManScanMapping_rec(p, pLeaf, vMapped, fPreorder); } // add the node to the mapping - if ( vMapped && !fPreorder ) - Vec_PtrPush( vMapped, pObj ); + if (vMapped && !fPreorder) + Vec_PtrPush(vMapped, pObj); return aArea; } @@ -161,28 +355,28 @@ int Cnf_ManScanMapping_rec( Cnf_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vMapped Synopsis [Computes area, references, and nodes used in the mapping.] Description [Collects the nodes in reverse topological order.] - + SideEffects [] SeeAlso [] ***********************************************************************/ -Vec_Ptr_t * Cnf_ManScanMapping( Cnf_Man_t * p, int fCollect, int fPreorder ) +Vec_Ptr_t *Cnf_ManScanMapping(Cnf_Man_t *p, int fCollect, int fPreorder) { - Vec_Ptr_t * vMapped = NULL; - Aig_Obj_t * pObj; + Vec_Ptr_t *vMapped = NULL; + Aig_Obj_t *pObj; int i; // clean all references - Aig_ManForEachObj( p->pManAig, pObj, i ) + Aig_ManForEachObj(p->pManAig, pObj, i) pObj->nRefs = 0; // allocate the array - if ( fCollect ) - vMapped = Vec_PtrAlloc( 1000 ); + if (fCollect) + vMapped = Vec_PtrAlloc(1000); // collect nodes reachable from POs in the DFS order through the best cuts p->aArea = 0; - Aig_ManForEachCo( p->pManAig, pObj, i ) - p->aArea += Cnf_ManScanMapping_rec( p, Aig_ObjFanin0(pObj), vMapped, fPreorder ); -// printf( "Variables = %6d. Clauses = %8d.\n", vMapped? Vec_PtrSize(vMapped) + Aig_ManCiNum(p->pManAig) + 1 : 0, p->aArea + 2 ); + Aig_ManForEachCo(p->pManAig, pObj, i) + p->aArea += Cnf_ManScanMapping_rec(p, Aig_ObjFanin0(pObj), vMapped, fPreorder); + // printf( "Variables = %6d. Clauses = %8d.\n", vMapped? Vec_PtrSize(vMapped) + Aig_ManCiNum(p->pManAig) + 1 : 0, p->aArea + 2 ); return vMapped; } @@ -191,20 +385,20 @@ Vec_Ptr_t * Cnf_ManScanMapping( Cnf_Man_t * p, int fCollect, int fPreorder ) Synopsis [Returns the array of CI IDs.] Description [] - + SideEffects [] SeeAlso [] ***********************************************************************/ -Vec_Int_t * Cnf_DataCollectCiSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p ) +Vec_Int_t *Cnf_DataCollectCiSatNums(Cnf_Dat_t *pCnf, Aig_Man_t *p) { - Vec_Int_t * vCiIds; - Aig_Obj_t * pObj; + Vec_Int_t *vCiIds; + Aig_Obj_t *pObj; int i; - vCiIds = Vec_IntAlloc( Aig_ManCiNum(p) ); - Aig_ManForEachCi( p, pObj, i ) - Vec_IntPush( vCiIds, pCnf->pVarNums[pObj->Id] ); + vCiIds = Vec_IntAlloc(Aig_ManCiNum(p)); + Aig_ManForEachCi(p, pObj, i) + Vec_IntPush(vCiIds, pCnf->pVarNums[pObj->Id]); return vCiIds; } @@ -213,20 +407,20 @@ Vec_Int_t * Cnf_DataCollectCiSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p ) Synopsis [Returns the array of CI IDs.] Description [] - + SideEffects [] SeeAlso [] ***********************************************************************/ -Vec_Int_t * Cnf_DataCollectCoSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p ) +Vec_Int_t *Cnf_DataCollectCoSatNums(Cnf_Dat_t *pCnf, Aig_Man_t *p) { - Vec_Int_t * vCoIds; - Aig_Obj_t * pObj; + Vec_Int_t *vCoIds; + Aig_Obj_t *pObj; int i; - vCoIds = Vec_IntAlloc( Aig_ManCoNum(p) ); - Aig_ManForEachCo( p, pObj, i ) - Vec_IntPush( vCoIds, pCnf->pVarNums[pObj->Id] ); + vCoIds = Vec_IntAlloc(Aig_ManCoNum(p)); + Aig_ManForEachCo(p, pObj, i) + Vec_IntPush(vCoIds, pCnf->pVarNums[pObj->Id]); return vCoIds; } @@ -235,58 +429,58 @@ Vec_Int_t * Cnf_DataCollectCoSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p ) Synopsis [] Description [] - + SideEffects [] SeeAlso [] ***********************************************************************/ -unsigned char * Cnf_DataDeriveLitPolarities( Cnf_Dat_t * p ) +unsigned char *Cnf_DataDeriveLitPolarities(Cnf_Dat_t *p) { - int i, c, iClaBeg, iClaEnd, * pLit; - unsigned * pPols0 = ABC_CALLOC( unsigned, Aig_ManObjNumMax(p->pMan) ); - unsigned * pPols1 = ABC_CALLOC( unsigned, Aig_ManObjNumMax(p->pMan) ); - unsigned char * pPres = ABC_CALLOC( unsigned char, p->nClauses ); - for ( i = 0; i < Aig_ManObjNumMax(p->pMan); i++ ) + int i, c, iClaBeg, iClaEnd, *pLit; + unsigned *pPols0 = ABC_CALLOC(unsigned, Aig_ManObjNumMax(p->pMan)); + unsigned *pPols1 = ABC_CALLOC(unsigned, Aig_ManObjNumMax(p->pMan)); + unsigned char *pPres = ABC_CALLOC(unsigned char, p->nClauses); + for (i = 0; i < Aig_ManObjNumMax(p->pMan); i++) { - if ( p->pObj2Count[i] == 0 ) + if (p->pObj2Count[i] == 0) continue; iClaBeg = p->pObj2Clause[i]; iClaEnd = p->pObj2Clause[i] + p->pObj2Count[i]; // go through the negative polarity clauses - for ( c = iClaBeg; c < iClaEnd; c++ ) - for ( pLit = p->pClauses[c]+1; pLit < p->pClauses[c+1]; pLit++ ) - if ( Abc_LitIsCompl(p->pClauses[c][0]) ) - pPols0[Abc_Lit2Var(*pLit)] |= (unsigned)(2 - Abc_LitIsCompl(*pLit)); // taking the opposite (!) -- not the case + for (c = iClaBeg; c < iClaEnd; c++) + for (pLit = p->pClauses[c] + 1; pLit < p->pClauses[c + 1]; pLit++) + if (Abc_LitIsCompl(p->pClauses[c][0])) + pPols0[Abc_Lit2Var(*pLit)] |= (unsigned)(2 - Abc_LitIsCompl(*pLit)); // taking the opposite (!) -- not the case else - pPols1[Abc_Lit2Var(*pLit)] |= (unsigned)(2 - Abc_LitIsCompl(*pLit)); // taking the opposite (!) -- not the case + pPols1[Abc_Lit2Var(*pLit)] |= (unsigned)(2 - Abc_LitIsCompl(*pLit)); // taking the opposite (!) -- not the case // record these clauses - for ( c = iClaBeg; c < iClaEnd; c++ ) - for ( pLit = p->pClauses[c]+1; pLit < p->pClauses[c+1]; pLit++ ) - if ( Abc_LitIsCompl(p->pClauses[c][0]) ) - pPres[c] = (unsigned char)( (unsigned)pPres[c] | (pPols0[Abc_Lit2Var(*pLit)] << (2*(pLit-p->pClauses[c]-1))) ); + for (c = iClaBeg; c < iClaEnd; c++) + for (pLit = p->pClauses[c] + 1; pLit < p->pClauses[c + 1]; pLit++) + if (Abc_LitIsCompl(p->pClauses[c][0])) + pPres[c] = (unsigned char)((unsigned)pPres[c] | (pPols0[Abc_Lit2Var(*pLit)] << (2 * (pLit - p->pClauses[c] - 1)))); else - pPres[c] = (unsigned char)( (unsigned)pPres[c] | (pPols1[Abc_Lit2Var(*pLit)] << (2*(pLit-p->pClauses[c]-1))) ); + pPres[c] = (unsigned char)((unsigned)pPres[c] | (pPols1[Abc_Lit2Var(*pLit)] << (2 * (pLit - p->pClauses[c] - 1)))); // clean negative polarity - for ( c = iClaBeg; c < iClaEnd; c++ ) - for ( pLit = p->pClauses[c]+1; pLit < p->pClauses[c+1]; pLit++ ) + for (c = iClaBeg; c < iClaEnd; c++) + for (pLit = p->pClauses[c] + 1; pLit < p->pClauses[c + 1]; pLit++) pPols0[Abc_Lit2Var(*pLit)] = pPols1[Abc_Lit2Var(*pLit)] = 0; } - ABC_FREE( pPols0 ); - ABC_FREE( pPols1 ); -/* -// for ( c = 0; c < p->nClauses; c++ ) - for ( c = 0; c < 100; c++ ) - { - printf( "Clause %6d : ", c ); - for ( i = 0; i < 4; i++ ) - printf( "%d ", ((unsigned)pPres[c] >> (2*i)) & 3 ); - printf( " " ); - for ( pLit = p->pClauses[c]; pLit < p->pClauses[c+1]; pLit++ ) - printf( "%6d ", *pLit ); - printf( "\n" ); - } -*/ + ABC_FREE(pPols0); + ABC_FREE(pPols1); + /* + // for ( c = 0; c < p->nClauses; c++ ) + for ( c = 0; c < 100; c++ ) + { + printf( "Clause %6d : ", c ); + for ( i = 0; i < 4; i++ ) + printf( "%d ", ((unsigned)pPres[c] >> (2*i)) & 3 ); + printf( " " ); + for ( pLit = p->pClauses[c]; pLit < p->pClauses[c+1]; pLit++ ) + printf( "%6d ", *pLit ); + printf( "\n" ); + } + */ return pPres; } @@ -295,96 +489,96 @@ unsigned char * Cnf_DataDeriveLitPolarities( Cnf_Dat_t * p ) Synopsis [] Description [] - + SideEffects [] SeeAlso [] ***********************************************************************/ -Cnf_Dat_t * Cnf_DataReadFromFile( char * pFileName ) +Cnf_Dat_t *Cnf_DataReadFromFile(char *pFileName) { int MaxLine = 1000000; int Var, Lit, nVars = -1, nClas = -1, i, Entry, iLine = 0; - Cnf_Dat_t * pCnf = NULL; - Vec_Int_t * vClas = NULL; - Vec_Int_t * vLits = NULL; - char * pBuffer, * pToken; - FILE * pFile = fopen( pFileName, "rb" ); - if ( pFile == NULL ) + Cnf_Dat_t *pCnf = NULL; + Vec_Int_t *vClas = NULL; + Vec_Int_t *vLits = NULL; + char *pBuffer, *pToken; + FILE *pFile = fopen(pFileName, "rb"); + if (pFile == NULL) { - printf( "Cannot open file \"%s\" for writing.\n", pFileName ); + printf("Cannot open file \"%s\" for writing.\n", pFileName); return NULL; } - pBuffer = ABC_ALLOC( char, MaxLine ); - while ( fgets(pBuffer, MaxLine, pFile) != NULL ) + pBuffer = ABC_ALLOC(char, MaxLine); + while (fgets(pBuffer, MaxLine, pFile) != NULL) { iLine++; - if ( pBuffer[0] == 'c' ) + if (pBuffer[0] == 'c') continue; - if ( pBuffer[0] == 'p' ) + if (pBuffer[0] == 'p') { - pToken = strtok( pBuffer+1, " \t" ); - if ( strcmp(pToken, "cnf") ) + pToken = strtok(pBuffer + 1, " \t"); + if (strcmp(pToken, "cnf")) { - printf( "Incorrect input file.\n" ); + printf("Incorrect input file.\n"); goto finish; } - pToken = strtok( NULL, " \t" ); - nVars = atoi( pToken ); - pToken = strtok( NULL, " \t" ); - nClas = atoi( pToken ); - if ( nVars <= 0 || nClas <= 0 ) + pToken = strtok(NULL, " \t"); + nVars = atoi(pToken); + pToken = strtok(NULL, " \t"); + nClas = atoi(pToken); + if (nVars <= 0 || nClas <= 0) { - printf( "Incorrect parameters.\n" ); + printf("Incorrect parameters.\n"); goto finish; } // temp storage - vClas = Vec_IntAlloc( nClas+1 ); - vLits = Vec_IntAlloc( nClas*8 ); + vClas = Vec_IntAlloc(nClas + 1); + vLits = Vec_IntAlloc(nClas * 8); continue; } - pToken = strtok( pBuffer, " \t\r\n" ); - if ( pToken == NULL ) + pToken = strtok(pBuffer, " \t\r\n"); + if (pToken == NULL) continue; - Vec_IntPush( vClas, Vec_IntSize(vLits) ); - while ( pToken ) + Vec_IntPush(vClas, Vec_IntSize(vLits)); + while (pToken) { - Var = atoi( pToken ); - if ( Var == 0 ) + Var = atoi(pToken); + if (Var == 0) break; - Lit = (Var > 0) ? Abc_Var2Lit(Var-1, 0) : Abc_Var2Lit(-Var-1, 1); - if ( Lit >= 2*nVars ) + Lit = (Var > 0) ? Abc_Var2Lit(Var - 1, 0) : Abc_Var2Lit(-Var - 1, 1); + if (Lit >= 2 * nVars) { - printf( "Literal %d is out-of-bound for %d variables.\n", Lit, nVars ); + printf("Literal %d is out-of-bound for %d variables.\n", Lit, nVars); goto finish; } - Vec_IntPush( vLits, Lit ); - pToken = strtok( NULL, " \t\r\n" ); + Vec_IntPush(vLits, Lit); + pToken = strtok(NULL, " \t\r\n"); } - if ( Var != 0 ) + if (Var != 0) { - printf( "There is no zero-terminator in line %d.\n", iLine ); + printf("There is no zero-terminator in line %d.\n", iLine); goto finish; } } // finalize - if ( Vec_IntSize(vClas) != nClas ) - printf( "Warning! The number of clauses (%d) is different from declaration (%d).\n", Vec_IntSize(vClas), nClas ); - Vec_IntPush( vClas, Vec_IntSize(vLits) ); + if (Vec_IntSize(vClas) != nClas) + printf("Warning! The number of clauses (%d) is different from declaration (%d).\n", Vec_IntSize(vClas), nClas); + Vec_IntPush(vClas, Vec_IntSize(vLits)); // create - pCnf = ABC_CALLOC( Cnf_Dat_t, 1 ); - pCnf->nVars = nVars; - pCnf->nClauses = Vec_IntSize(vClas)-1; + pCnf = ABC_CALLOC(Cnf_Dat_t, 1); + pCnf->nVars = nVars; + pCnf->nClauses = Vec_IntSize(vClas) - 1; pCnf->nLiterals = Vec_IntSize(vLits); - pCnf->pClauses = ABC_ALLOC( int *, Vec_IntSize(vClas) ); + pCnf->pClauses = ABC_ALLOC(int *, Vec_IntSize(vClas)); pCnf->pClauses[0] = Vec_IntReleaseArray(vLits); - Vec_IntForEachEntry( vClas, Entry, i ) + Vec_IntForEachEntry(vClas, Entry, i) pCnf->pClauses[i] = pCnf->pClauses[0] + Entry; finish: - fclose( pFile ); - Vec_IntFreeP( &vClas ); - Vec_IntFreeP( &vLits ); - ABC_FREE( pBuffer ); + fclose(pFile); + Vec_IntFreeP(&vClas); + Vec_IntFreeP(&vLits); + ABC_FREE(pBuffer); return pCnf; } @@ -393,79 +587,79 @@ finish: Synopsis [] Description [] - + SideEffects [] SeeAlso [] ***********************************************************************/ -int Cnf_DataSolveFromFile( char * pFileName, int nConfLimit, int nLearnedStart, int nLearnedDelta, int nLearnedPerce, int fVerbose, int fShowPattern, int ** ppModel, int nPis ) +int Cnf_DataSolveFromFile(char *pFileName, int nConfLimit, int nLearnedStart, int nLearnedDelta, int nLearnedPerce, int fVerbose, int fShowPattern, int **ppModel, int nPis) { abctime clk = Abc_Clock(); - Cnf_Dat_t * pCnf = Cnf_DataReadFromFile( pFileName ); - sat_solver * pSat; + Cnf_Dat_t *pCnf = Cnf_DataReadFromFile(pFileName); + sat_solver *pSat; int i, status, RetValue = -1; - if ( pCnf == NULL ) + if (pCnf == NULL) return -1; - if ( fVerbose ) + if (fVerbose) { - printf( "CNF stats: Vars = %6d. Clauses = %7d. Literals = %8d. ", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals ); - Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); + printf("CNF stats: Vars = %6d. Clauses = %7d. Literals = %8d. ", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals); + Abc_PrintTime(1, "Time", Abc_Clock() - clk); } // convert into SAT solver - pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); - if ( pSat == NULL ) + pSat = (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0); + if (pSat == NULL) { - printf( "The problem is trivially UNSAT.\n" ); - Cnf_DataFree( pCnf ); + printf("The problem is trivially UNSAT.\n"); + Cnf_DataFree(pCnf); return 1; } - if ( nLearnedStart ) + if (nLearnedStart) pSat->nLearntStart = pSat->nLearntMax = nLearnedStart; - if ( nLearnedDelta ) + if (nLearnedDelta) pSat->nLearntDelta = nLearnedDelta; - if ( nLearnedPerce ) + if (nLearnedPerce) pSat->nLearntRatio = nLearnedPerce; - if ( fVerbose ) + if (fVerbose) pSat->fVerbose = fVerbose; -//sat_solver_start_cardinality( pSat, 100 ); + // sat_solver_start_cardinality( pSat, 100 ); // solve the miter - status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfLimit, 0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); - if ( status == l_Undef ) + status = sat_solver_solve(pSat, NULL, NULL, (ABC_INT64_T)nConfLimit, 0, (ABC_INT64_T)0, (ABC_INT64_T)0); + if (status == l_Undef) RetValue = -1; - else if ( status == l_True ) + else if (status == l_True) RetValue = 0; - else if ( status == l_False ) + else if (status == l_False) RetValue = 1; else - assert( 0 ); - if ( fVerbose ) - Sat_SolverPrintStats( stdout, pSat ); - if ( RetValue == -1 ) - Abc_Print( 1, "UNDECIDED " ); - else if ( RetValue == 0 ) - Abc_Print( 1, "SATISFIABLE " ); + assert(0); + if (fVerbose) + Sat_SolverPrintStats(stdout, pSat); + if (RetValue == -1) + Abc_Print(1, "UNDECIDED "); + else if (RetValue == 0) + Abc_Print(1, "SATISFIABLE "); else - Abc_Print( 1, "UNSATISFIABLE " ); - //Abc_Print( -1, "\n" ); - Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); + Abc_Print(1, "UNSATISFIABLE "); + // Abc_Print( -1, "\n" ); + Abc_PrintTime(1, "Time", Abc_Clock() - clk); // derive SAT assignment - if ( RetValue == 0 && nPis > 0 ) + if (RetValue == 0 && nPis > 0) { - *ppModel = ABC_ALLOC( int, nPis ); - for ( i = 0; i < nPis; i++ ) - (*ppModel)[i] = sat_solver_var_value( pSat, pCnf->nVars - nPis + i ); + *ppModel = ABC_ALLOC(int, nPis); + for (i = 0; i < nPis; i++) + (*ppModel)[i] = sat_solver_var_value(pSat, pCnf->nVars - nPis + i); } - if ( RetValue == 0 && fShowPattern ) + if (RetValue == 0 && fShowPattern) { - for ( i = 0; i < pCnf->nVars; i++ ) - printf( "%d", sat_solver_var_value(pSat,i) ); - printf( "\n" ); + for (i = 0; i < pCnf->nVars; i++) + printf("%d", sat_solver_var_value(pSat, i)); + printf("\n"); } - Cnf_DataFree( pCnf ); - sat_solver_delete( pSat ); + Cnf_DataFree(pCnf); + sat_solver_delete(pSat); return RetValue; } @@ -474,47 +668,127 @@ int Cnf_DataSolveFromFile( char * pFileName, int nConfLimit, int nLearnedStart, Synopsis [] Description [] - + SideEffects [] SeeAlso [] ***********************************************************************/ -int Cnf_DataBestVar( Cnf_Dat_t * p, int * pSkip ) +int Cnf_DataBestVar(Cnf_Dat_t *p, int *pSkip) { - int * pNums = ABC_CALLOC( int, p->nVars ); - int i, * pLit, NumMax = -1, iVarMax = -1; - for ( i = 0; i < p->nClauses; i++ ) - for ( pLit = p->pClauses[i]; pLit < p->pClauses[i+1]; pLit++ ) + int *pNums = ABC_CALLOC(int, p->nVars); + int i, *pLit, NumMax = -1, iVarMax = -1; + for (i = 0; i < p->nClauses; i++) + for (pLit = p->pClauses[i]; pLit < p->pClauses[i + 1]; pLit++) pNums[Abc_Lit2Var(*pLit)]++; - for ( i = 0; i < p->nVars; i++ ) - if ( (!pSkip || !pSkip[i]) && NumMax < pNums[i] ) + for (i = 0; i < p->nVars; i++) + if ((!pSkip || !pSkip[i]) && NumMax < pNums[i]) NumMax = pNums[i], iVarMax = i; - ABC_FREE( pNums ); + ABC_FREE(pNums); return iVarMax; } void Cnf_Experiment1() { - Cnf_Dat_t * pTemp, * p = Cnf_DataReadFromFile( "../166b.cnf" ); int i; - int * pSkip = ABC_CALLOC( int, p->nVars ); - for ( i = 0; i < 100; i++ ) + Cnf_Dat_t *pTemp, *p = Cnf_DataReadFromFile("../166b.cnf"); + int i, *pSkip = ABC_CALLOC(int, p->nVars); + for (i = 0; i < 100; i++) { - int iVar = Cnf_DataBestVar( p, pSkip ); - char FileName[100]; sprintf( FileName, "cnf/%03d.cnf", i ); - Cnf_DataWriteIntoFile( p, FileName, 0, NULL, NULL ); - printf( "Dumped file \"%s\".\n", FileName ); - p = Cnf_DataDupCof( pTemp = p, Abc_Var2Lit(iVar, 0) ); - Cnf_DataFree( pTemp ); + int iVar = Cnf_DataBestVar(p, pSkip); + char FileName[100]; + sprintf(FileName, "cnf/%03d.cnf", i); + Cnf_DataWriteIntoFile(p, FileName, 0, NULL, NULL); + printf("Dumped file \"%s\".\n", FileName); + p = Cnf_DataDupCof(pTemp = p, Abc_Var2Lit(iVar, 0)); + Cnf_DataFree(pTemp); pSkip[iVar] = 1; } - Cnf_DataFree( p ); - ABC_FREE( pSkip ); + Cnf_DataFree(p); + ABC_FREE(pSkip); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t *Cnf_GenRandLits(int iVarBeg, int iVarEnd, int nLits, int Value, int Rand, int fVerbose) +{ + Vec_Int_t *vLits = Vec_IntAlloc(nLits); + assert(iVarBeg < iVarEnd && nLits < iVarEnd - iVarBeg); + while (Vec_IntSize(vLits) < nLits) + { + int iVar = iVarBeg + (Abc_Random(0) ^ Rand) % (iVarEnd - iVarBeg); + assert(iVar >= iVarBeg && iVar < iVarEnd); + if (Vec_IntFind(vLits, Abc_Var2Lit(iVar, 0)) == -1 && Vec_IntFind(vLits, Abc_Var2Lit(iVar, 1)) == -1) + { + if (Value == 0) + Vec_IntPush(vLits, Abc_Var2Lit(iVar, 1)); + else if (Value == 1) + Vec_IntPush(vLits, Abc_Var2Lit(iVar, 0)); + else + Vec_IntPush(vLits, Abc_Var2Lit(iVar, Abc_Random(0) & 1)); + } + } + Vec_IntSort(vLits, 0); + if ( fVerbose ) + Vec_IntPrint(vLits); + fflush(stdout); + return vLits; +} +void Cnf_SplitCnfFile(char * pFileName, int nParts, int iVarBeg, int iVarEnd, int nLits, int Value, int Rand, int fVerbose) +{ + Cnf_Dat_t *p = Cnf_DataReadFromFile(pFileName); int k; + if (iVarEnd == ABC_INFINITY) + iVarEnd = p->nVars; + for (k = 0; k < nParts; k++) + { + Vec_Int_t *vLits = Cnf_GenRandLits(iVarBeg, iVarEnd, nLits, Value, Rand, fVerbose); + Cnf_Dat_t *pCnf = Cnf_DataDupCofArray(p, vLits); + char FileName[100]; sprintf(FileName, "%02d.cnf", k); + Cnf_DataWriteIntoFile(pCnf, FileName, 0, NULL, NULL); + Cnf_DataFree(pCnf); + Vec_IntFree(vLits); + } + Cnf_DataFree(p); +} +void Cnf_SplitCnfCleanup(int nParts) +{ + char FileName[100]; int k; + for (k = 0; k < nParts; k++) { + sprintf(FileName, "%02d.cnf", k); + unlink(FileName); + } +} +void Cnf_SplitSat(char *pFileName, int iVarBeg, int iVarEnd, int nLits, int Value, int TimeOut, int nProcs, int nIters, int Seed, int fVerbose) +{ + abctime clk = Abc_Clock(); + Vec_Int_t *vSol = NULL; + int i, Rand = 0; + if ( nIters == 0 ) + nIters = ABC_INFINITY; + Abc_Random(1); + for ( i = 0; i < Seed; i++ ) + Abc_Random(0); + Rand = Abc_Random(0); + for (i = 0; i < nIters && !vSol; i++) + { + Cnf_SplitCnfFile(pFileName, nProcs, iVarBeg, iVarEnd, nLits, Value, Rand, fVerbose); + vSol = Cnf_RunSolver(nProcs, TimeOut, fVerbose); + Cnf_SplitCnfCleanup(nProcs); + } + printf("%solution is found. ", vSol ? "S" : "No s"); + Abc_PrintTime(0, "Total time", Abc_Clock() - clk); + Vec_IntFreeP(&vSol); } //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// - ABC_NAMESPACE_IMPL_END -