diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/base/abc/abcAig.c | 45 | ||||
-rw-r--r-- | src/base/abci/abc.c | 49 | ||||
-rw-r--r-- | src/base/abci/abcSat.c | 497 | ||||
-rw-r--r-- | src/base/abci/abcVerify.c | 6 | ||||
-rw-r--r-- | src/opt/xyz/xyz.h | 2 | ||||
-rw-r--r-- | src/opt/xyz/xyzCore.c | 348 | ||||
-rw-r--r-- | src/opt/xyz/xyzInt.h | 77 | ||||
-rw-r--r-- | src/opt/xyz/xyzMinEsop.c | 38 | ||||
-rw-r--r-- | src/opt/xyz/xyzMinMan.c | 1 | ||||
-rw-r--r-- | src/opt/xyz/xyzMinSop.c | 346 | ||||
-rw-r--r-- | src/opt/xyz/xyzMinUtil.c | 56 | ||||
-rw-r--r-- | src/opt/xyz/xyzTest.c | 370 | ||||
-rw-r--r-- | src/sat/asat/solver.h | 5 | ||||
-rw-r--r-- | src/sat/fraig/fraigCanon.c | 4 | ||||
-rw-r--r-- | src/sat/fraig/fraigSat.c | 22 | ||||
-rw-r--r-- | src/sat/msat/msat.h | 1 | ||||
-rw-r--r-- | src/sat/msat/msatClause.c | 5 | ||||
-rw-r--r-- | src/sat/msat/msatInt.h | 1 | ||||
-rw-r--r-- | src/sat/msat/msatSolverApi.c | 1 | ||||
-rw-r--r-- | src/sat/msat/msatSolverCore.c | 20 |
20 files changed, 1784 insertions, 110 deletions
diff --git a/src/base/abc/abcAig.c b/src/base/abc/abcAig.c index 53ad88c2..167e7552 100644 --- a/src/base/abc/abcAig.c +++ b/src/base/abc/abcAig.c @@ -572,7 +572,28 @@ Abc_Obj_t * Abc_AigXor( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 ) return Abc_AigOr( pMan, Abc_AigAnd(pMan, p0, Abc_ObjNot(p1)), Abc_AigAnd(pMan, p1, Abc_ObjNot(p0)) ); } + +/**Function************************************************************* + + Synopsis [Implements the miter.] + + Description [] + + SideEffects [] + SeeAlso [] + +***********************************************************************/ +Abc_Obj_t * Abc_AigMiter_rec( Abc_Aig_t * pMan, Abc_Obj_t ** ppObjs, int nObjs ) +{ + Abc_Obj_t * pObj1, * pObj2; + if ( nObjs == 1 ) + return ppObjs[0]; + pObj1 = Abc_AigMiter_rec( pMan, ppObjs, nObjs/2 ); + pObj2 = Abc_AigMiter_rec( pMan, ppObjs + nObjs/2, nObjs - nObjs/2 ); + return Abc_AigOr( pMan, pObj1, pObj2 ); +} + /**Function************************************************************* Synopsis [Implements the miter.] @@ -586,6 +607,30 @@ Abc_Obj_t * Abc_AigXor( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 ) ***********************************************************************/ Abc_Obj_t * Abc_AigMiter( Abc_Aig_t * pMan, Vec_Ptr_t * vPairs ) { + int i; + if ( vPairs->nSize == 0 ) + return Abc_ObjNot( Abc_NtkConst1(pMan->pNtkAig) ); + assert( vPairs->nSize % 2 == 0 ); + // go through the cubes of the node's SOP + for ( i = 0; i < vPairs->nSize; i += 2 ) + vPairs->pArray[i/2] = Abc_AigXor( pMan, vPairs->pArray[i], vPairs->pArray[i+1] ); + vPairs->nSize = vPairs->nSize/2; + return Abc_AigMiter_rec( pMan, (Abc_Obj_t **)vPairs->pArray, vPairs->nSize ); +} + +/**Function************************************************************* + + Synopsis [Implements the miter.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Obj_t * Abc_AigMiter2( Abc_Aig_t * pMan, Vec_Ptr_t * vPairs ) +{ Abc_Obj_t * pMiter, * pXor; int i; assert( vPairs->nSize % 2 == 0 ); diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 71b76cf6..70cd2e6c 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -2868,6 +2868,13 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( stdout, "Currently can only solve the miter for combinational circuits.\n" ); return 0; } + if ( Abc_NtkIsSeq(pNtk) ) + { + fprintf( stdout, "This command cannot be applied to the sequential AIG.\n" ); + return 0; + } + +/* if ( !Abc_NtkIsLogic(pNtk) ) { fprintf( stdout, "This command can only be applied to logic network (run \"renode -c\").\n" ); @@ -2877,19 +2884,35 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_NtkUnmap(pNtk); if ( Abc_NtkIsSopLogic(pNtk) ) Abc_NtkSopToBdd(pNtk); - - RetValue = Abc_NtkMiterSat( pNtk, nSeconds, fVerbose ); - if ( RetValue == -1 ) - printf( "The miter is UNDECIDED (SAT solver timed out).\n" ); - else if ( RetValue == 0 ) - printf( "The miter is SATISFIABLE.\n" ); +*/ + if ( Abc_NtkIsStrash(pNtk) ) + { + RetValue = Abc_NtkMiterSat2( pNtk, nSeconds, fVerbose ); + if ( RetValue == -1 ) + printf( "The miter is UNDECIDED (SAT solver timed out).\n" ); + else if ( RetValue == 0 ) + printf( "The miter is SATISFIABLE.\n" ); + else + printf( "The miter is UNSATISFIABLE.\n" ); + } else - printf( "The miter is UNSATISFIABLE.\n" ); + { + Abc_Ntk_t * pTemp; + pTemp = Abc_NtkStrash( pNtk, 0, 0 ); + RetValue = Abc_NtkMiterSat2( pTemp, nSeconds, fVerbose ); + if ( RetValue == -1 ) + printf( "The miter is UNDECIDED (SAT solver timed out).\n" ); + else if ( RetValue == 0 ) + printf( "The miter is SATISFIABLE.\n" ); + else + printf( "The miter is UNSATISFIABLE.\n" ); + Abc_NtkDelete( pTemp ); + } return 0; usage: fprintf( pErr, "usage: sat [-T num] [-vh]\n" ); - fprintf( pErr, "\t solves the miter\n" ); + fprintf( pErr, "\t solves the combinational miter\n" ); fprintf( pErr, "\t-T num : approximate runtime limit in seconds [default = %d]\n", nSeconds ); fprintf( pErr, "\t-v : prints verbose information [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); @@ -3722,11 +3745,11 @@ int Abc_CommandXyz( Abc_Frame_t * pAbc, int argc, char ** argv ) } // run the command - pNtkRes = Abc_NtkXyz( pNtk, nFaninMax, 0, 0, fUseInvs, fVerbose ); + pNtkRes = Abc_NtkXyz( pNtk, nFaninMax, 1, 0, fUseInvs, fVerbose ); if ( pNtkRes == NULL ) { fprintf( pErr, "Command has failed.\n" ); - return 1; + return 0; } // replace the current network Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); @@ -3788,9 +3811,9 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } -// Abc_NtkDeriveEsops( pNtk ); -// Abc_NtkXyz( pNtk, 128, 0, 0, 0 ); - printf( "This command is currently not used.\n" ); + Abc_NtkTestEsop( pNtk ); +// Abc_NtkTestSop( pNtk ); +// printf( "This command is currently not used.\n" ); /* // run the command diff --git a/src/base/abci/abcSat.c b/src/base/abci/abcSat.c index 4a65659c..8c8636c5 100644 --- a/src/base/abci/abcSat.c +++ b/src/base/abci/abcSat.c @@ -27,6 +27,10 @@ static int Abc_NodeAddClauses( solver * pSat, char * pSop0, char * pSop1, Abc_Obj_t * pNode, Vec_Int_t * vVars ); static int Abc_NodeAddClausesTop( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars ); +static solver * Abc_NtkMiterSatCreate2( Abc_Ntk_t * pNtk ); + +static nMuxes; + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -129,7 +133,7 @@ solver * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk ) Vec_Str_t * vCube; Vec_Int_t * vVars; char * pSop0, * pSop1; - int i; + int i, clk = clock(); assert( Abc_NtkIsBddLogic(pNtk) ); @@ -159,6 +163,8 @@ solver * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk ) } // Asat_SolverWriteDimacs( pSat, "test.cnf", NULL, NULL, 0 ); + PRT( "Creating solver", clock() - clk ); + // delete Vec_StrFree( vCube ); Vec_IntFree( vVars ); @@ -291,6 +297,495 @@ int Abc_NodeAddClausesTop( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars ) } + + + + + + + + + +/**Function************************************************************* + + Synopsis [Attempts to solve the miter using an internal SAT solver.] + + Description [Returns -1 if timed out; 0 if SAT; 1 if UNSAT.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkMiterSat2( Abc_Ntk_t * pNtk, int nSeconds, int fVerbose ) +{ + solver * pSat; + lbool status; + int RetValue, clk; + + assert( Abc_NtkIsStrash(pNtk) ); + assert( Abc_NtkLatchNum(pNtk) == 0 ); + + if ( Abc_NtkPoNum(pNtk) > 1 ) + fprintf( stdout, "Warning: The miter has %d outputs. SAT will try to prove all of them.\n", Abc_NtkPoNum(pNtk) ); + + // load clauses into the solver + clk = clock(); + pSat = Abc_NtkMiterSatCreate2( pNtk ); + if ( pSat == NULL ) + return 1; +// printf( "Created SAT problem with %d variable and %d clauses. ", solver_nvars(pSat), solver_nclauses(pSat) ); +// PRT( "Time", clock() - clk ); + + // simplify the problem + clk = clock(); + status = solver_simplify(pSat); +// printf( "Simplified the problem to %d variables and %d clauses. ", solver_nvars(pSat), solver_nclauses(pSat) ); +// PRT( "Time", clock() - clk ); + if ( status == 0 ) + { + solver_delete( pSat ); +// printf( "The problem is UNSATISFIABLE after simplification.\n" ); + return 1; + } + + // solve the miter + clk = clock(); + if ( fVerbose ) + pSat->verbosity = 1; + status = solver_solve( pSat, NULL, NULL, nSeconds ); + if ( status == l_Undef ) + { +// printf( "The problem timed out.\n" ); + RetValue = -1; + } + else if ( status == l_True ) + { +// printf( "The problem is SATISFIABLE.\n" ); + RetValue = 0; + } + else if ( status == l_False ) + { +// printf( "The problem is UNSATISFIABLE.\n" ); + RetValue = 1; + } + else + assert( 0 ); + PRT( "SAT solver time", clock() - clk ); + + // if the problem is SAT, get the counterexample + if ( status == l_True ) + { + Vec_Int_t * vCiIds = Abc_NtkGetCiIds( pNtk ); + pNtk->pModel = solver_get_model( pSat, vCiIds->pArray, vCiIds->nSize ); + Vec_IntFree( vCiIds ); + } + // free the solver + solver_delete( pSat ); + return RetValue; +} + + + + +/**Function************************************************************* + + Synopsis [Adds trivial clause.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkClauseTriv( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars ) +{ +//printf( "Adding triv %d. %d\n", Abc_ObjRegular(pNode)->Id, (int)pSat->solver_stats.clauses ); + vVars->nSize = 0; + Vec_IntPush( vVars, toLitCond( (int)Abc_ObjRegular(pNode)->pCopy, Abc_ObjIsComplement(pNode) ) ); +// Vec_IntPush( vVars, toLitCond( (int)Abc_ObjRegular(pNode)->Id, Abc_ObjIsComplement(pNode) ) ); + return solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ); +} + +/**Function************************************************************* + + Synopsis [Adds trivial clause.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkClauseAnd( solver * pSat, Abc_Obj_t * pNode, Vec_Ptr_t * vSuper, Vec_Int_t * vVars ) +{ + int fComp1, Var, Var1, i; +//printf( "Adding AND %d. (%d) %d\n", pNode->Id, vSuper->nSize+1, (int)pSat->solver_stats.clauses ); + + assert( !Abc_ObjIsComplement( pNode ) ); + assert( Abc_ObjIsNode( pNode ) ); + +// nVars = solver_nvars(pSat); + Var = (int)pNode->pCopy; +// Var = pNode->Id; + +// assert( Var < nVars ); + for ( i = 0; i < vSuper->nSize; i++ ) + { + // get the predecessor nodes + // get the complemented attributes of the nodes + fComp1 = Abc_ObjIsComplement(vSuper->pArray[i]); + // determine the variable numbers + Var1 = (int)Abc_ObjRegular(vSuper->pArray[i])->pCopy; +// Var1 = (int)Abc_ObjRegular(vSuper->pArray[i])->Id; + + // check that the variables are in the SAT manager +// assert( Var1 < nVars ); + + // suppose the AND-gate is A * B = C + // add !A => !C or A + !C + // fprintf( pFile, "%d %d 0%c", Var1, -Var, 10 ); + vVars->nSize = 0; + Vec_IntPush( vVars, toLitCond(Var1, fComp1) ); + Vec_IntPush( vVars, toLitCond(Var, 1 ) ); + if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) ) + return 0; + } + + // add A & B => C or !A + !B + C +// fprintf( pFile, "%d %d %d 0%c", -Var1, -Var2, Var, 10 ); + vVars->nSize = 0; + for ( i = 0; i < vSuper->nSize; i++ ) + { + // get the predecessor nodes + // get the complemented attributes of the nodes + fComp1 = Abc_ObjIsComplement(vSuper->pArray[i]); + // determine the variable numbers + Var1 = (int)Abc_ObjRegular(vSuper->pArray[i])->pCopy; +// Var1 = (int)Abc_ObjRegular(vSuper->pArray[i])->Id; + // add this variable to the array + Vec_IntPush( vVars, toLitCond(Var1, !fComp1) ); + } + Vec_IntPush( vVars, toLitCond(Var, 0) ); + return solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ); +} + +/**Function************************************************************* + + Synopsis [Adds trivial clause.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkClauseMux( solver * pSat, Abc_Obj_t * pNode, Abc_Obj_t * pNodeC, Abc_Obj_t * pNodeT, Abc_Obj_t * pNodeE, Vec_Int_t * vVars ) +{ + int VarF, VarI, VarT, VarE, fCompT, fCompE; +//printf( "Adding mux %d. %d\n", pNode->Id, (int)pSat->solver_stats.clauses ); + + assert( !Abc_ObjIsComplement( pNode ) ); + assert( Abc_NodeIsMuxType( pNode ) ); + // get the variable numbers + VarF = (int)pNode->pCopy; + VarI = (int)pNodeC->pCopy; + VarT = (int)Abc_ObjRegular(pNodeT)->pCopy; + VarE = (int)Abc_ObjRegular(pNodeE)->pCopy; +// VarF = (int)pNode->Id; +// VarI = (int)pNodeC->Id; +// VarT = (int)Abc_ObjRegular(pNodeT)->Id; +// VarE = (int)Abc_ObjRegular(pNodeE)->Id; + + // get the complementation flags + fCompT = Abc_ObjIsComplement(pNodeT); + fCompE = Abc_ObjIsComplement(pNodeE); + + // f = ITE(i, t, e) + // i' + t' + f + // i' + t + f' + // i + e' + f + // i + e + f' + // create four clauses + vVars->nSize = 0; + Vec_IntPush( vVars, toLitCond(VarI, 1) ); + Vec_IntPush( vVars, toLitCond(VarT, 1^fCompT) ); + Vec_IntPush( vVars, toLitCond(VarF, 0) ); + if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) ) + return 0; + vVars->nSize = 0; + Vec_IntPush( vVars, toLitCond(VarI, 1) ); + Vec_IntPush( vVars, toLitCond(VarT, 0^fCompT) ); + Vec_IntPush( vVars, toLitCond(VarF, 1) ); + if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) ) + return 0; + vVars->nSize = 0; + Vec_IntPush( vVars, toLitCond(VarI, 0) ); + Vec_IntPush( vVars, toLitCond(VarE, 1^fCompE) ); + Vec_IntPush( vVars, toLitCond(VarF, 0) ); + if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) ) + return 0; + vVars->nSize = 0; + Vec_IntPush( vVars, toLitCond(VarI, 0) ); + Vec_IntPush( vVars, toLitCond(VarE, 0^fCompE) ); + Vec_IntPush( vVars, toLitCond(VarF, 1) ); + if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) ) + return 0; + + if ( VarT == VarE ) + { + assert( fCompT == !fCompE ); + return 1; + } + + // two additional clauses + // t' & e' -> f' t + e + f' + // t & e -> f t' + e' + f + vVars->nSize = 0; + Vec_IntPush( vVars, toLitCond(VarT, 0^fCompT) ); + Vec_IntPush( vVars, toLitCond(VarE, 0^fCompE) ); + Vec_IntPush( vVars, toLitCond(VarF, 1) ); + if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) ) + return 0; + vVars->nSize = 0; + Vec_IntPush( vVars, toLitCond(VarT, 1^fCompT) ); + Vec_IntPush( vVars, toLitCond(VarE, 1^fCompE) ); + Vec_IntPush( vVars, toLitCond(VarF, 0) ); + return solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ); +} + +/**Function************************************************************* + + Synopsis [Returns the array of nodes to be combined into one multi-input AND-gate.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkCollectSupergate_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vSuper, int fFirst, int fStopAtMux ) +{ + int RetValue1, RetValue2, i; + // check if the node is visited + if ( Abc_ObjRegular(pNode)->fMarkB ) + { + // check if the node occurs in the same polarity + for ( i = 0; i < vSuper->nSize; i++ ) + if ( vSuper->pArray[i] == pNode ) + return 1; + // check if the node is present in the opposite polarity + for ( i = 0; i < vSuper->nSize; i++ ) + if ( vSuper->pArray[i] == Abc_ObjNot(pNode) ) + return -1; + assert( 0 ); + return 0; + } + // if the new node is complemented or a PI, another gate begins + if ( !fFirst ) + if ( Abc_ObjIsComplement(pNode) || !Abc_ObjIsNode(pNode) || Abc_ObjFanoutNum(pNode) > 1 || fStopAtMux && Abc_NodeIsMuxType(pNode) ) + { + Vec_PtrPush( vSuper, pNode ); + Abc_ObjRegular(pNode)->fMarkB = 1; + return 0; + } + assert( !Abc_ObjIsComplement(pNode) ); + assert( Abc_ObjIsNode(pNode) ); + // go through the branches + RetValue1 = Abc_NtkCollectSupergate_rec( Abc_ObjChild0(pNode), vSuper, 0, fStopAtMux ); + RetValue2 = Abc_NtkCollectSupergate_rec( Abc_ObjChild1(pNode), vSuper, 0, fStopAtMux ); + if ( RetValue1 == -1 || RetValue2 == -1 ) + return -1; + // return 1 if at least one branch has a duplicate + return RetValue1 || RetValue2; +} + +/**Function************************************************************* + + Synopsis [Returns the array of nodes to be combined into one multi-input AND-gate.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkCollectSupergate( Abc_Obj_t * pNode, int fStopAtMux, Vec_Ptr_t * vNodes ) +{ + int RetValue, i; + assert( !Abc_ObjIsComplement(pNode) ); + // collect the nodes in the implication supergate + Vec_PtrClear( vNodes ); + RetValue = Abc_NtkCollectSupergate_rec( pNode, vNodes, 1, fStopAtMux ); + assert( vNodes->nSize > 1 ); + // unmark the visited nodes + for ( i = 0; i < vNodes->nSize; i++ ) + Abc_ObjRegular((Abc_Obj_t *)vNodes->pArray[i])->fMarkB = 0; + // if we found the node and its complement in the same implication supergate, + // return empty set of nodes (meaning that we should use constant-0 node) + if ( RetValue == -1 ) + vNodes->nSize = 0; +} + + +/**Function************************************************************* + + Synopsis [Sets up the SAT solver.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkMiterSatCreate2Int( solver * pSat, Abc_Ntk_t * pNtk ) +{ + Abc_Obj_t * pNode, * pFanin, * pNodeC, * pNodeT, * pNodeE; + Vec_Ptr_t * vNodes, * vSuper; + Vec_Int_t * vVars; + int i, k, fUseMuxes = 1; + + assert( Abc_NtkIsStrash(pNtk) ); + + // start the data structures + vNodes = Vec_PtrAlloc( 1000 ); // the nodes corresponding to vars in the solver + vSuper = Vec_PtrAlloc( 100 ); // the nodes belonging to the given implication supergate + vVars = Vec_IntAlloc( 100 ); // the temporary array for variables in the clause + + // add the clause for the constant node + pNode = Abc_NtkConst1(pNtk); + pNode->fMarkA = 1; + pNode->pCopy = (Abc_Obj_t *)vNodes->nSize; + Vec_PtrPush( vNodes, pNode ); + Abc_NtkClauseTriv( pSat, pNode, vVars ); + + // collect the nodes that need clauses and top-level assignments + Abc_NtkForEachCo( pNtk, pNode, i ) + { + // get the fanin + pFanin = Abc_ObjFanin0(pNode); + // create the node's variable + if ( pFanin->fMarkA == 0 ) + { + pFanin->fMarkA = 1; + pFanin->pCopy = (Abc_Obj_t *)vNodes->nSize; + Vec_PtrPush( vNodes, pFanin ); + } + // add the trivial clause + if ( !Abc_NtkClauseTriv( pSat, Abc_ObjChild0(pNode), vVars ) ) + return 0; + } + + // add the clauses + Vec_PtrForEachEntry( vNodes, pNode, i ) + { + assert( !Abc_ObjIsComplement(pNode) ); + if ( !Abc_NodeIsAigAnd(pNode) ) + continue; +//printf( "%d ", pNode->Id ); + + // add the clauses + if ( fUseMuxes && Abc_NodeIsMuxType(pNode) ) + { + nMuxes++; + + pNodeC = Abc_NodeRecognizeMux( pNode, &pNodeT, &pNodeE ); + Vec_PtrClear( vSuper ); + Vec_PtrPush( vSuper, pNodeC ); + Vec_PtrPush( vSuper, pNodeT ); + Vec_PtrPush( vSuper, pNodeE ); + // add the fanin nodes to explore + Vec_PtrForEachEntry( vSuper, pFanin, k ) + { + pFanin = Abc_ObjRegular(pFanin); + if ( pFanin->fMarkA == 0 ) + { + pFanin->fMarkA = 1; + pFanin->pCopy = (Abc_Obj_t *)vNodes->nSize; + Vec_PtrPush( vNodes, pFanin ); + } + } + // add the clauses + if ( !Abc_NtkClauseMux( pSat, pNode, pNodeC, pNodeT, pNodeE, vVars ) ) + return 0; + } + else + { + // get the supergate + Abc_NtkCollectSupergate( pNode, fUseMuxes, vSuper ); + // add the fanin nodes to explore + Vec_PtrForEachEntry( vSuper, pFanin, k ) + { + pFanin = Abc_ObjRegular(pFanin); + if ( pFanin->fMarkA == 0 ) + { + pFanin->fMarkA = 1; + pFanin->pCopy = (Abc_Obj_t *)vNodes->nSize; + Vec_PtrPush( vNodes, pFanin ); + } + } + // add the clauses + if ( vSuper->nSize == 0 ) + { + if ( !Abc_NtkClauseTriv( pSat, Abc_ObjNot(pNode), vVars ) ) + return 0; + } + else + { + if ( !Abc_NtkClauseAnd( pSat, pNode, vSuper, vVars ) ) + return 0; + } + } + } + + // delete + Vec_IntFree( vVars ); + Vec_PtrFree( vNodes ); + Vec_PtrFree( vSuper ); + return 1; +} + +/**Function************************************************************* + + Synopsis [Sets up the SAT solver.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +solver * Abc_NtkMiterSatCreate2( Abc_Ntk_t * pNtk ) +{ + solver * pSat; + Abc_Obj_t * pNode; + int RetValue, i, clk = clock(); + + nMuxes = 0; + + pSat = solver_new(); + RetValue = Abc_NtkMiterSatCreate2Int( pSat, pNtk ); + Abc_NtkForEachObj( pNtk, pNode, i ) + pNode->fMarkA = 0; + Asat_SolverWriteDimacs( pSat, "temp_sat.cnf", NULL, NULL, 1 ); + if ( RetValue == 0 ) + { + solver_delete(pSat); + return NULL; + } + printf( "The number of MUXes detected = %d (%5.2f %% of logic). ", nMuxes, 300.0*nMuxes/Abc_NtkNodeNum(pNtk) ); + PRT( "Creating solver", clock() - clk ); + return pSat; +} + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c index 070c871d..b30a6452 100644 --- a/src/base/abci/abcVerify.c +++ b/src/base/abci/abcVerify.c @@ -148,6 +148,9 @@ void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fV Fraig_ParamsSetDefault( &Params ); Params.fVerbose = fVerbose; Params.nSeconds = nSeconds; + Params.fFuncRed = 0; + Params.nPatsRand = 0; + Params.nPatsDyna = 0; pMan = Abc_NtkToFraig( pMiter, &Params, 0, 0 ); Fraig_ManProveMiter( pMan ); @@ -325,6 +328,9 @@ void Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nF Fraig_ParamsSetDefault( &Params ); Params.fVerbose = fVerbose; Params.nSeconds = nSeconds; + Params.fFuncRed = 0; + Params.nPatsRand = 0; + Params.nPatsDyna = 0; pMan = Abc_NtkToFraig( pFrames, &Params, 0, 0 ); Fraig_ManProveMiter( pMan ); diff --git a/src/opt/xyz/xyz.h b/src/opt/xyz/xyz.h index f18686ff..ea488068 100644 --- a/src/opt/xyz/xyz.h +++ b/src/opt/xyz/xyz.h @@ -46,6 +46,8 @@ struct Xyz_Man_t_ Vec_Ptr_t * vObjStrs; // object structures void * pMemory; // memory for the internal data strctures Min_Man_t * pManMin; // the cub manager + int fUseEsop; // enables ESOPs + int fUseSop; // enables SOPs // arrays to map local variables Vec_Int_t * vComTo0; // mapping of common variables into first fanin Vec_Int_t * vComTo1; // mapping of common variables into second fanin diff --git a/src/opt/xyz/xyzCore.c b/src/opt/xyz/xyzCore.c index a48f749e..e5089788 100644 --- a/src/opt/xyz/xyzCore.c +++ b/src/opt/xyz/xyzCore.c @@ -27,13 +27,19 @@ static void Abc_NtkXyzCovers( Xyz_Man_t * p, Abc_Ntk_t * pNtk, bool fVerbose ); static int Abc_NtkXyzCoversOne( Xyz_Man_t * p, Abc_Ntk_t * pNtk, bool fVerbose ); static void Abc_NtkXyzCovers_rec( Xyz_Man_t * p, Abc_Obj_t * pObj, Vec_Ptr_t * vBoundary ); - +/* static int Abc_NodeXyzPropagateEsop( Xyz_Man_t * p, Abc_Obj_t * pObj, Abc_Obj_t * pObj0, Abc_Obj_t * pObj1 ); static int Abc_NodeXyzPropagateSop( Xyz_Man_t * p, Abc_Obj_t * pObj, Abc_Obj_t * pObj0, Abc_Obj_t * pObj1 ); static int Abc_NodeXyzUnionEsop( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp ); static int Abc_NodeXyzUnionSop( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp ); static int Abc_NodeXyzProductEsop( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp ); static int Abc_NodeXyzProductSop( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp ); +*/ + +static int Abc_NodeXyzPropagate( Xyz_Man_t * p, Abc_Obj_t * pObj ); +static Min_Cube_t * Abc_NodeXyzProduct( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int fEsop, int nSupp ); +static Min_Cube_t * Abc_NodeXyzSum( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int fEsop, int nSupp ); + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -59,6 +65,8 @@ Abc_Ntk_t * Abc_NtkXyz( Abc_Ntk_t * pNtk, int nFaninMax, bool fUseEsop, bool fUs // create the manager p = Xyz_ManAlloc( pNtk, nFaninMax ); + p->fUseEsop = fUseEsop; + p->fUseSop = 1;//fUseSop; pNtk->pManCut = p; // perform mapping @@ -69,6 +77,8 @@ Abc_Ntk_t * Abc_NtkXyz( Abc_Ntk_t * pNtk, int nFaninMax, bool fUseEsop, bool fUs pNtkNew = Abc_NtkXyzDeriveClean( p, pNtk ); else pNtkNew = Abc_NtkXyzDerive( p, pNtk ); +// pNtkNew = NULL; + Xyz_ManFree( p ); pNtk->pManCut = NULL; @@ -164,7 +174,10 @@ int Abc_NtkXyzCoversOne( Xyz_Man_t * p, Abc_Ntk_t * pNtk, bool fVerbose ) } // traverse the cone starting from this node - Abc_NtkXyzCovers_rec( p, pObj, vBoundary ); + if ( Abc_ObjGetSupp(pObj) == NULL ) + Abc_NtkXyzCovers_rec( p, pObj, vBoundary ); + + // count the number of solved cones if ( Abc_ObjGetSupp(pObj) == NULL ) fStop = 0; else @@ -225,7 +238,7 @@ void Abc_NtkXyzCovers_rec( Xyz_Man_t * p, Abc_Obj_t * pObj, Vec_Ptr_t * vBoundar { Abc_Obj_t * pObj0, * pObj1; // return if the support is already computed - if ( pObj->fMarkB || pObj->fMarkA || Abc_ObjGetSupp(pObj) ) + if ( pObj->fMarkB || pObj->fMarkA )//|| Abc_ObjGetSupp(pObj) ) // why do we need Supp check here??? return; // mark as visited pObj->fMarkB = 1; @@ -236,9 +249,9 @@ void Abc_NtkXyzCovers_rec( Xyz_Man_t * p, Abc_Obj_t * pObj, Vec_Ptr_t * vBoundar Abc_NtkXyzCovers_rec( p, pObj0, vBoundary ); Abc_NtkXyzCovers_rec( p, pObj1, vBoundary ); // skip the node that spaced out - if ( !pObj0->fMarkA && !Abc_ObjGetSupp(pObj0) || // fanin is not ready - !pObj1->fMarkA && !Abc_ObjGetSupp(pObj1) || // fanin is not ready - !Abc_NodeXyzPropagateEsop(p, pObj, pObj0, pObj1) ) // node's support or covers cannot be computed + if ( !pObj0->fMarkA && !Abc_ObjGetSupp(pObj0) || // fanin is not ready + !pObj1->fMarkA && !Abc_ObjGetSupp(pObj1) || // fanin is not ready + !Abc_NodeXyzPropagate( p, pObj ) ) // node's support or covers cannot be computed { // save the nodes of the future boundary if ( !pObj0->fMarkA && Abc_ObjGetSupp(pObj0) ) @@ -331,6 +344,321 @@ Vec_Int_t * Abc_NodeXyzSupport( Xyz_Man_t * p, Vec_Int_t * vSupp0, Vec_Int_t * v /**Function************************************************************* + Synopsis [Propagates all types of covers.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NodeXyzPropagate( Xyz_Man_t * p, Abc_Obj_t * pObj ) +{ + Min_Cube_t * pCoverP = NULL, * pCoverN = NULL, * pCoverX = NULL; + Min_Cube_t * pCov0, * pCov1, * pCover0, * pCover1; + Vec_Int_t * vSupp, * vSupp0, * vSupp1; + Abc_Obj_t * pObj0, * pObj1; + int fCompl0, fCompl1; + + pObj0 = Abc_ObjFanin0( pObj ); + pObj1 = Abc_ObjFanin1( pObj ); + + if ( pObj0->fMarkA ) Vec_IntWriteEntry( p->vTriv0, 0, pObj0->Id ); + if ( pObj1->fMarkA ) Vec_IntWriteEntry( p->vTriv1, 0, pObj1->Id ); + + // get the resulting support + vSupp0 = pObj0->fMarkA? p->vTriv0 : Abc_ObjGetSupp(pObj0); + vSupp1 = pObj1->fMarkA? p->vTriv1 : Abc_ObjGetSupp(pObj1); + vSupp = Abc_NodeXyzSupport( p, vSupp0, vSupp1 ); + + // quit if support if too large + if ( vSupp->nSize > p->nFaninMax ) + { + Vec_IntFree( vSupp ); + return 0; + } + + // get the complemented attributes + fCompl0 = Abc_ObjFaninC0( pObj ); + fCompl1 = Abc_ObjFaninC1( pObj ); + + // propagate ESOP + if ( p->fUseEsop ) + { + // get the covers + pCov0 = pObj0->fMarkA? p->pManMin->pTriv0[0] : Abc_ObjGetCover2(pObj0); + pCov1 = pObj1->fMarkA? p->pManMin->pTriv1[0] : Abc_ObjGetCover2(pObj1); + if ( pCov0 && pCov1 ) + { + // complement the first if needed + if ( !fCompl0 ) + pCover0 = pCov0; + else if ( pCov0 && pCov0->nLits == 0 ) // topmost one is the tautology cube + pCover0 = pCov0->pNext; + else + pCover0 = p->pManMin->pOne0, p->pManMin->pOne0->pNext = pCov0; + + // complement the second if needed + if ( !fCompl1 ) + pCover1 = pCov1; + else if ( pCov1 && pCov1->nLits == 0 ) // topmost one is the tautology cube + pCover1 = pCov1->pNext; + else + pCover1 = p->pManMin->pOne1, p->pManMin->pOne1->pNext = pCov1; + + // derive the new cover + pCoverX = Abc_NodeXyzProduct( p, pCover0, pCover1, 1, vSupp->nSize ); + } + } + // propagate SOPs + if ( p->fUseSop ) + { + // get the covers for the direct polarity + pCover0 = pObj0->fMarkA? p->pManMin->pTriv0[fCompl0] : Abc_ObjGetCover(pObj0, fCompl0); + pCover1 = pObj1->fMarkA? p->pManMin->pTriv1[fCompl1] : Abc_ObjGetCover(pObj1, fCompl1); + // derive the new cover + if ( pCover0 && pCover1 ) + pCoverP = Abc_NodeXyzProduct( p, pCover0, pCover1, 0, vSupp->nSize ); + + // get the covers for the inverse polarity + pCover0 = pObj0->fMarkA? p->pManMin->pTriv0[!fCompl0] : Abc_ObjGetCover(pObj0, !fCompl0); + pCover1 = pObj1->fMarkA? p->pManMin->pTriv1[!fCompl1] : Abc_ObjGetCover(pObj1, !fCompl1); + // derive the new cover + if ( pCover0 && pCover1 ) + pCoverN = Abc_NodeXyzSum( p, pCover0, pCover1, 0, vSupp->nSize ); + } + + // if none of the covers can be computed quit + if ( !pCoverX && !pCoverP && !pCoverN ) + { + Vec_IntFree( vSupp ); + return 0; + } + + // set the covers + assert( Abc_ObjGetSupp(pObj) == NULL ); + Abc_ObjSetSupp( pObj, vSupp ); + Abc_ObjSetCover( pObj, pCoverP, 0 ); + Abc_ObjSetCover( pObj, pCoverN, 1 ); + Abc_ObjSetCover2( pObj, pCoverX ); +//printf( "%3d : %4d %4d %4d\n", pObj->Id, Min_CoverCountCubes(pCoverP), Min_CoverCountCubes(pCoverN), Min_CoverCountCubes(pCoverX) ); + + // count statistics + p->nSupps++; + p->nSuppsMax = ABC_MAX( p->nSuppsMax, p->nSupps ); + return 1; +} + + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Min_Cube_t * Abc_NodeXyzProduct( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int fEsop, int nSupp ) +{ + Min_Cube_t * pCube, * pCube0, * pCube1; + Min_Cube_t * pCover; + int i, Val0, Val1; + assert( pCover0 && pCover1 ); + + // clean storage + Min_ManClean( p->pManMin, nSupp ); + // go through the cube pairs + Min_CoverForEachCube( pCover0, pCube0 ) + Min_CoverForEachCube( pCover1, pCube1 ) + { + // go through the support variables of the cubes + for ( i = 0; i < p->vPairs0->nSize; i++ ) + { + Val0 = Min_CubeGetVar( pCube0, p->vPairs0->pArray[i] ); + Val1 = Min_CubeGetVar( pCube1, p->vPairs1->pArray[i] ); + if ( (Val0 & Val1) == 0 ) + break; + } + // check disjointness + if ( i < p->vPairs0->nSize ) + continue; + + if ( p->pManMin->nCubes > p->nCubesMax ) + { + pCover = Min_CoverCollect( p->pManMin, nSupp ); +//Min_CoverWriteFile( pCover, "large", 1 ); + Min_CoverRecycle( p->pManMin, pCover ); + return NULL; + } + + // create the product cube + pCube = Min_CubeAlloc( p->pManMin ); + + // add the literals + pCube->nLits = 0; + for ( i = 0; i < nSupp; i++ ) + { + if ( p->vComTo0->pArray[i] == -1 ) + Val0 = 3; + else + Val0 = Min_CubeGetVar( pCube0, p->vComTo0->pArray[i] ); + + if ( p->vComTo1->pArray[i] == -1 ) + Val1 = 3; + else + Val1 = Min_CubeGetVar( pCube1, p->vComTo1->pArray[i] ); + + if ( (Val0 & Val1) == 3 ) + continue; + + Min_CubeXorVar( pCube, i, (Val0 & Val1) ^ 3 ); + pCube->nLits++; + } + // add the cube to storage + if ( fEsop ) + Min_EsopAddCube( p->pManMin, pCube ); + else + Min_SopAddCube( p->pManMin, pCube ); + } + + // minimize the cover + if ( fEsop ) + Min_EsopMinimize( p->pManMin ); + else + Min_SopMinimize( p->pManMin ); + pCover = Min_CoverCollect( p->pManMin, nSupp ); + + // quit if the cover is too large + if ( Min_CoverCountCubes(pCover) > p->nFaninMax ) + { +/* +Min_CoverWriteFile( pCover, "large", 1 ); + Min_CoverExpand( p->pManMin, pCover ); + Min_EsopMinimize( p->pManMin ); + Min_EsopMinimize( p->pManMin ); + Min_EsopMinimize( p->pManMin ); + Min_EsopMinimize( p->pManMin ); + Min_EsopMinimize( p->pManMin ); + Min_EsopMinimize( p->pManMin ); + Min_EsopMinimize( p->pManMin ); + Min_EsopMinimize( p->pManMin ); + Min_EsopMinimize( p->pManMin ); + pCover = Min_CoverCollect( p->pManMin, nSupp ); +*/ + Min_CoverRecycle( p->pManMin, pCover ); + return NULL; + } + return pCover; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Min_Cube_t * Abc_NodeXyzSum( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int fEsop, int nSupp ) +{ + Min_Cube_t * pCube, * pCube0, * pCube1; + Min_Cube_t * pCover; + int i, Val0, Val1; + assert( pCover0 && pCover1 ); + + // clean storage + Min_ManClean( p->pManMin, nSupp ); + Min_CoverForEachCube( pCover0, pCube0 ) + { + // create the cube + pCube = Min_CubeAlloc( p->pManMin ); + pCube->nLits = 0; + for ( i = 0; i < p->vComTo0->nSize; i++ ) + { + if ( p->vComTo0->pArray[i] == -1 ) + continue; + Val0 = Min_CubeGetVar( pCube0, p->vComTo0->pArray[i] ); + if ( Val0 == 3 ) + continue; + Min_CubeXorVar( pCube, i, Val0 ^ 3 ); + pCube->nLits++; + } + if ( p->pManMin->nCubes > p->nCubesMax ) + { + pCover = Min_CoverCollect( p->pManMin, nSupp ); + Min_CoverRecycle( p->pManMin, pCover ); + return NULL; + } + // add the cube to storage + if ( fEsop ) + Min_EsopAddCube( p->pManMin, pCube ); + else + Min_SopAddCube( p->pManMin, pCube ); + } + Min_CoverForEachCube( pCover1, pCube1 ) + { + // create the cube + pCube = Min_CubeAlloc( p->pManMin ); + pCube->nLits = 0; + for ( i = 0; i < p->vComTo1->nSize; i++ ) + { + if ( p->vComTo1->pArray[i] == -1 ) + continue; + Val1 = Min_CubeGetVar( pCube1, p->vComTo1->pArray[i] ); + if ( Val1 == 3 ) + continue; + Min_CubeXorVar( pCube, i, Val1 ^ 3 ); + pCube->nLits++; + } + if ( p->pManMin->nCubes > p->nCubesMax ) + { + pCover = Min_CoverCollect( p->pManMin, nSupp ); + Min_CoverRecycle( p->pManMin, pCover ); + return NULL; + } + // add the cube to storage + if ( fEsop ) + Min_EsopAddCube( p->pManMin, pCube ); + else + Min_SopAddCube( p->pManMin, pCube ); + } + + // minimize the cover + if ( fEsop ) + Min_EsopMinimize( p->pManMin ); + else + Min_SopMinimize( p->pManMin ); + pCover = Min_CoverCollect( p->pManMin, nSupp ); + + // quit if the cover is too large + if ( Min_CoverCountCubes(pCover) > p->nFaninMax ) + { + Min_CoverRecycle( p->pManMin, pCover ); + return NULL; + } + return pCover; +} + + + + + + + +#if 0 + + + +/**Function************************************************************* + Synopsis [] Description [] @@ -581,7 +909,7 @@ int Abc_NodeXyzProductEsop( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pC pCube->nLits++; } // add the cube to storage - while ( Min_EsopAddCube( p->pManMin, pCube ) ); + Min_EsopAddCube( p->pManMin, pCube ); } return 1; } @@ -642,7 +970,7 @@ int Abc_NodeXyzUnionEsop( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCov if ( p->pManMin->nCubes >= p->nCubesMax ) return 0; // add the cube to storage - while ( Min_EsopAddCube( p->pManMin, pCube ) ); + Min_EsopAddCube( p->pManMin, pCube ); } } if ( pCover1 ) @@ -665,7 +993,7 @@ int Abc_NodeXyzUnionEsop( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCov if ( p->pManMin->nCubes >= p->nCubesMax ) return 0; // add the cube to storage - while ( Min_EsopAddCube( p->pManMin, pCube ) ); + Min_EsopAddCube( p->pManMin, pCube ); } } return 1; @@ -688,7 +1016,7 @@ int Abc_NodeXyzUnionSop( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCove } - +#endif //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/opt/xyz/xyzInt.h b/src/opt/xyz/xyzInt.h index 22950bfd..656612aa 100644 --- a/src/opt/xyz/xyzInt.h +++ b/src/opt/xyz/xyzInt.h @@ -81,10 +81,10 @@ static inline void Min_CubeXorVar( Min_Cube_t * p, int Var, int Value ) { p->uDa /*=== xyzMinEsop.c ==========================================================*/ extern void Min_EsopMinimize( Min_Man_t * p ); -extern int Min_EsopAddCube( Min_Man_t * p, Min_Cube_t * pCube ); +extern void Min_EsopAddCube( Min_Man_t * p, Min_Cube_t * pCube ); /*=== xyzMinSop.c ==========================================================*/ extern void Min_SopMinimize( Min_Man_t * p ); -extern int Min_SopAddCube( Min_Man_t * p, Min_Cube_t * pCube ); +extern void Min_SopAddCube( Min_Man_t * p, Min_Cube_t * pCube ); /*=== xyzMinMan.c ==========================================================*/ extern Min_Man_t * Min_ManAlloc( int nVars ); extern void Min_ManClean( Min_Man_t * p, int nSupp ); @@ -92,8 +92,10 @@ extern void Min_ManFree( Min_Man_t * p ); /*=== xyzMinUtil.c ==========================================================*/ extern void Min_CubeWrite( FILE * pFile, Min_Cube_t * pCube ); extern void Min_CoverWrite( FILE * pFile, Min_Cube_t * pCover ); +extern void Min_CoverWriteStore( FILE * pFile, Min_Man_t * p ); extern void Min_CoverWriteFile( Min_Cube_t * pCover, char * pName, int fEsop ); extern void Min_CoverCheck( Min_Man_t * p ); +extern int Min_CubeCheck( Min_Cube_t * pCube ); extern Min_Cube_t * Min_CoverCollect( Min_Man_t * p, int nSuppSize ); extern void Min_CoverExpand( Min_Man_t * p, Min_Cube_t * pCover ); extern int Min_CoverSuppVarNum( Min_Man_t * p, Min_Cube_t * pCover ); @@ -161,6 +163,7 @@ static inline Min_Cube_t * Min_CubeDup( Min_Man_t * p, Min_Cube_t * pCopy ) Min_Cube_t * pCube; pCube = Min_CubeAlloc( p ); memcpy( pCube->uData, pCopy->uData, sizeof(unsigned) * p->nWords ); + pCube->nLits = pCopy->nLits; return pCube; } @@ -538,6 +541,24 @@ static inline void Min_CubesTransform( Min_Cube_t * pCube, Min_Cube_t * pDist, M } } +/**Function************************************************************* + + Synopsis [Transforms the cube into the result of distance-1 merging.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Min_CubesTransformOr( Min_Cube_t * pCube, Min_Cube_t * pDist ) +{ + int w; + for ( w = 0; w < (int)pCube->nWords; w++ ) + pCube->uData[w] |= pDist->uData[w]; +} + /**Function************************************************************* @@ -579,7 +600,7 @@ static inline void Min_CoverExpandRemoveEqual( Min_Man_t * p, Min_Cube_t * pCove /**Function************************************************************* - Synopsis [Check if the cube is equal or dist1 or contained.] + Synopsis [Returns 1 if the given cube is contained in one of the cubes of the cover.] Description [] @@ -588,42 +609,32 @@ static inline void Min_CoverExpandRemoveEqual( Min_Man_t * p, Min_Cube_t * pCove SeeAlso [] ***********************************************************************/ -static inline int Min_CubeIsEqualOrSubsumed( Min_Man_t * p, Min_Cube_t * pNew ) +static inline int Min_CoverContainsCube( Min_Man_t * p, Min_Cube_t * pCube ) { - Min_Cube_t * pCube; + Min_Cube_t * pThis; int i; - // check identity - Min_CoverForEachCube( p->ppStore[pNew->nLits], pCube ) - if ( Min_CubesAreEqual( pCube, pNew ) ) +/* + // this cube cannot be equal to any cube + Min_CoverForEachCube( p->ppStore[pCube->nLits], pThis ) + { + if ( Min_CubesAreEqual( pCube, pThis ) ) + { + Min_CubeWrite( stdout, pCube ); + assert( 0 ); + } + } +*/ + // try to find a containing cube + for ( i = 0; i <= (int)pCube->nLits; i++ ) + Min_CoverForEachCube( p->ppStore[i], pThis ) + { + // skip the bubble + if ( pThis != p->pBubble && Min_CubeIsContained( pThis, pCube ) ) return 1; - // check containment - for ( i = 0; i < (int)pNew->nLits; i++ ) - Min_CoverForEachCube( p->ppStore[i], pCube ) - if ( Min_CubeIsContained( pCube, pNew ) ) - return 1; + } return 0; } -/**Function************************************************************* - - Synopsis [Check if the cube is equal or dist1 or contained.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline Min_Cube_t * Min_CubeHasDistanceOne( Min_Man_t * p, Min_Cube_t * pNew ) -{ - Min_Cube_t * pCube; - Min_CoverForEachCube( p->ppStore[pNew->nLits], pCube ) - if ( Min_CubesDistOne( pCube, pNew, NULL ) ) - return pCube; - return NULL; -} - //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/opt/xyz/xyzMinEsop.c b/src/opt/xyz/xyzMinEsop.c index 114e28a6..839e2410 100644 --- a/src/opt/xyz/xyzMinEsop.c +++ b/src/opt/xyz/xyzMinEsop.c @@ -62,7 +62,11 @@ void Min_EsopMinimize( Min_Man_t * p ) Synopsis [Performs one round of rewriting using distance 2 cubes.] - Description [] + Description [The weakness of this procedure is that it tries each cube + with only one distance-2 cube. If this pair does not lead to improvement + the cube is inserted into the cover anyhow, and we try another pair. + A possible improvement would be to try this cube with all distance-2 + cubes, until an improvement is found, or until all such cubes are tried.] SideEffects [] @@ -162,8 +166,8 @@ void Min_EsopRewrite( Min_Man_t * p ) // add the cubes nCubesOld = p->nCubes; - while ( Min_EsopAddCube( p, pCube ) ); - while ( Min_EsopAddCube( p, pThis ) ); + Min_EsopAddCube( p, pCube ); + Min_EsopAddCube( p, pThis ); // check if the cubes were absorbed if ( p->nCubes < nCubesOld + 2 ) continue; @@ -191,8 +195,8 @@ void Min_EsopRewrite( Min_Man_t * p ) pThis->nLits += (v11 != 3); // add them anyhow - while ( Min_EsopAddCube( p, pCube ) ); - while ( Min_EsopAddCube( p, pThis ) ); + Min_EsopAddCube( p, pCube ); + Min_EsopAddCube( p, pThis ); } // printf( "Pairs = %d ", nPairs ); } @@ -201,8 +205,8 @@ void Min_EsopRewrite( Min_Man_t * p ) Synopsis [Adds the cube to storage.] - Description [If the distance one cube is found, returns the transformed - cube. If there is no distance one, adds the given cube to storage. + Description [Returns 0 if the cube is added or removed. Returns 1 + if the cube is glued with some other cube and has to be added again. Do not forget to clean the storage!] SideEffects [] @@ -210,7 +214,7 @@ void Min_EsopRewrite( Min_Man_t * p ) SeeAlso [] ***********************************************************************/ -int Min_EsopAddCube( Min_Man_t * p, Min_Cube_t * pCube ) +int Min_EsopAddCubeInt( Min_Man_t * p, Min_Cube_t * pCube ) { Min_Cube_t * pThis, ** ppPrev; // try to find the identical cube @@ -270,6 +274,24 @@ int Min_EsopAddCube( Min_Man_t * p, Min_Cube_t * pCube ) return 0; } +/**Function************************************************************* + + Synopsis [Adds the cube to storage.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Min_EsopAddCube( Min_Man_t * p, Min_Cube_t * pCube ) +{ + assert( pCube != p->pBubble ); + assert( (int)pCube->nLits == Min_CubeCountLits(pCube) ); + while ( Min_EsopAddCubeInt( p, pCube ) ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/opt/xyz/xyzMinMan.c b/src/opt/xyz/xyzMinMan.c index 423564c1..20314698 100644 --- a/src/opt/xyz/xyzMinMan.c +++ b/src/opt/xyz/xyzMinMan.c @@ -62,6 +62,7 @@ Min_Man_t * Min_ManAlloc( int nVars ) pMan->pTriv0[1] = Min_CubeAllocVar( pMan, 0, 1 ); pMan->pTriv1[0] = Min_CubeAllocVar( pMan, 0, 0 ); pMan->pTriv1[1] = Min_CubeAllocVar( pMan, 0, 1 ); + Min_ManClean( pMan, nVars ); return pMan; } diff --git a/src/opt/xyz/xyzMinSop.c b/src/opt/xyz/xyzMinSop.c index 1c5951fe..a5d57c66 100644 --- a/src/opt/xyz/xyzMinSop.c +++ b/src/opt/xyz/xyzMinSop.c @@ -52,10 +52,11 @@ void Min_SopMinimize( Min_Man_t * p ) nCubesOld = p->nCubes; Min_SopRewrite( p ); nIter++; +// printf( "%d:%d->%d ", nIter, nCubesInit, p->nCubes ); } while ( 100.0*(nCubesOld - p->nCubes)/nCubesOld > 3.0 ); +// printf( "\n" ); -// printf( "%d:%d->%d ", nIter, nCubesInit, p->nCubes ); } /**Function************************************************************* @@ -74,8 +75,17 @@ void Min_SopRewrite( Min_Man_t * p ) Min_Cube_t * pCube, ** ppPrev; Min_Cube_t * pThis, ** ppPrevT; Min_Cube_t * pTemp; - int v00, v01, v10, v11, Var0, Var1, Index; + int v00, v01, v10, v11, Var0, Var1, Index, fCont0, fCont1, nCubesOld; int nPairs = 0; +/* + { + Min_Cube_t * pCover; + pCover = Min_CoverCollect( p, p->nVars ); +printf( "\n\n" ); +Min_CoverWrite( stdout, pCover ); + Min_CoverExpand( p, pCover ); + } +*/ // insert the bubble before the first cube p->pBubble->pNext = p->ppStore[0]; @@ -127,7 +137,11 @@ void Min_SopRewrite( Min_Man_t * p ) continue; } nPairs++; - +/* +printf( "\n" ); +Min_CubeWrite( stdout, pCube ); +Min_CubeWrite( stdout, pThis ); +*/ // remove the cubes, insert the bubble instead of pCube *ppPrevT = pThis->pNext; *ppPrev = p->pBubble; @@ -135,6 +149,8 @@ void Min_SopRewrite( Min_Man_t * p ) p->pBubble->nLits = pCube->nLits; p->nCubes -= 2; + assert( pCube != p->pBubble && pThis != p->pBubble ); + // save the dist2 parameters v00 = Min_CubeGetVar( pCube, Var0 ); @@ -145,22 +161,83 @@ void Min_SopRewrite( Min_Man_t * p ) assert( v00 != 3 || v01 != 3 ); assert( v10 != 3 || v11 != 3 ); - // skip the case when rewriting is impossible +//printf( "\n" ); +//Min_CubeWrite( stdout, pCube ); +//Min_CubeWrite( stdout, pThis ); + +//printf( "\n" ); +//Min_CubeWrite( stdout, pCube ); +//Min_CubeWrite( stdout, pThis ); + + // consider the case when both cubes have non-empty literals if ( v00 != 3 && v01 != 3 && v10 != 3 && v11 != 3 ) + { + assert( v00 == (v10 ^ 3) ); + assert( v01 == (v11 ^ 3) ); + // create the temporary cube equal to the first corner + Min_CubeXorVar( pCube, Var0, 3 ); + // check if this cube is contained + fCont0 = Min_CoverContainsCube( p, pCube ); + // create the temporary cube equal to the first corner + Min_CubeXorVar( pCube, Var0, 3 ); + Min_CubeXorVar( pCube, Var1, 3 ); +//printf( "\n" ); +//Min_CubeWrite( stdout, pCube ); +//Min_CubeWrite( stdout, pThis ); + // check if this cube is contained + fCont1 = Min_CoverContainsCube( p, pCube ); + // undo the change + Min_CubeXorVar( pCube, Var1, 3 ); + + // check if the cubes can be overwritten + if ( fCont0 && fCont1 ) + { + // one of the cubes can be recycled, the other expanded and added + Min_CubeRecycle( p, pThis ); + // remove the literals + Min_CubeXorVar( pCube, Var0, v00 ^ 3 ); + Min_CubeXorVar( pCube, Var1, v01 ^ 3 ); + pCube->nLits -= 2; + Min_SopAddCube( p, pCube ); + } + else if ( fCont0 ) + { + // expand both cubes and add them + Min_CubeXorVar( pCube, Var0, v00 ^ 3 ); + pCube->nLits--; + Min_SopAddCube( p, pCube ); + Min_CubeXorVar( pThis, Var1, v11 ^ 3 ); + pThis->nLits--; + Min_SopAddCube( p, pThis ); + } + else if ( fCont1 ) + { + // expand both cubes and add them + Min_CubeXorVar( pCube, Var1, v01 ^ 3 ); + pCube->nLits--; + Min_SopAddCube( p, pCube ); + Min_CubeXorVar( pThis, Var0, v10 ^ 3 ); + pThis->nLits--; + Min_SopAddCube( p, pThis ); + } + else + { + Min_SopAddCube( p, pCube ); + Min_SopAddCube( p, pThis ); + } + // otherwise, no change is possible continue; + } // if one of them does not have DC lit, move it if ( v00 != 3 && v01 != 3 ) { + assert( v10 == 3 || v11 == 3 ); pTemp = pCube; pCube = pThis; pThis = pTemp; Index = v00; v00 = v10; v10 = Index; Index = v01; v01 = v11; v11 = Index; } -//printf( "\n" ); -//Min_CubeWrite( stdout, pCube ); -//Min_CubeWrite( stdout, pThis ); - // make sure the first cube has first var DC if ( v00 != 3 ) { @@ -174,13 +251,93 @@ void Min_SopRewrite( Min_Man_t * p ) if ( v00 == 3 && v11 == 3 ) { assert( v01 != 3 && v10 != 3 ); - // try two reduced cubes - + // try the remaining minterm + // create the temporary cube equal to the first corner + Min_CubeXorVar( pCube, Var0, v10 ); + Min_CubeXorVar( pCube, Var1, 3 ); + pCube->nLits++; + // check if this cube is contained + fCont0 = Min_CoverContainsCube( p, pCube ); + // undo the cube transformations + Min_CubeXorVar( pCube, Var0, v10 ); + Min_CubeXorVar( pCube, Var1, 3 ); + pCube->nLits--; + // check the case when both are covered + if ( fCont0 ) + { + // one of the cubes can be recycled, the other expanded and added + Min_CubeRecycle( p, pThis ); + // remove the literals + Min_CubeXorVar( pCube, Var1, v01 ^ 3 ); + pCube->nLits--; + Min_SopAddCube( p, pCube ); + } + else + { + // try two reduced cubes + Min_CubeXorVar( pCube, Var0, v10 ); + pCube->nLits++; + // remember the cubes + nCubesOld = p->nCubes; + Min_SopAddCube( p, pCube ); + // check if the cube is absorbed + if ( p->nCubes < nCubesOld + 1 ) + { // absorbed - add the second cube + Min_SopAddCube( p, pThis ); + } + else + { // remove this cube, and try another one + assert( pCube == p->ppStore[pCube->nLits] ); + p->ppStore[pCube->nLits] = pCube->pNext; + p->nCubes--; + + // return the cube to the previous state + Min_CubeXorVar( pCube, Var0, v10 ); + pCube->nLits--; + + // generate another reduced cube + Min_CubeXorVar( pThis, Var1, v01 ); + pThis->nLits++; + + // add both cubes + Min_SopAddCube( p, pCube ); + Min_SopAddCube( p, pThis ); + } + } } else // the first cube has DC lit { assert( v01 != 3 && v10 != 3 && v11 != 3 ); - // try reduced and expanded cube + // try the remaining minterm + // create the temporary cube equal to the minterm + Min_CubeXorVar( pThis, Var0, 3 ); + // check if this cube is contained + fCont0 = Min_CoverContainsCube( p, pThis ); + // undo the cube transformations + Min_CubeXorVar( pThis, Var0, 3 ); + // check the case when both are covered + if ( fCont0 ) + { + // one of the cubes can be recycled, the other expanded and added + Min_CubeRecycle( p, pThis ); + // remove the literals + Min_CubeXorVar( pCube, Var1, v01 ^ 3 ); + pCube->nLits--; + Min_SopAddCube( p, pCube ); + } + else + { + // try reshaping the cubes + // reduce the first cube + Min_CubeXorVar( pCube, Var0, v10 ); + pCube->nLits++; + // expand the second cube + Min_CubeXorVar( pThis, Var1, v11 ^ 3 ); + pThis->nLits--; + // add both cubes + Min_SopAddCube( p, pCube ); + Min_SopAddCube( p, pThis ); + } } } // printf( "Pairs = %d ", nPairs ); @@ -188,26 +345,80 @@ void Min_SopRewrite( Min_Man_t * p ) /**Function************************************************************* - Synopsis [] + Synopsis [Adds cube to the SOP cover stored in the manager.] - Description [] + Description [Returns 0 if the cube is added or removed. Returns 1 + if the cube is glued with some other cube and has to be added again.] SideEffects [] SeeAlso [] ***********************************************************************/ -int Min_SopAddCube( Min_Man_t * p, Min_Cube_t * pCube ) +int Min_SopAddCubeInt( Min_Man_t * p, Min_Cube_t * pCube ) { - return 1; -} - + Min_Cube_t * pThis, * pThis2, ** ppPrev; + int i; + // try to find the identical cube + Min_CoverForEachCube( p->ppStore[pCube->nLits], pThis ) + { + if ( Min_CubesAreEqual( pCube, pThis ) ) + { + Min_CubeRecycle( p, pCube ); + return 0; + } + } + // try to find a containing cube + for ( i = 0; i < (int)pCube->nLits; i++ ) + Min_CoverForEachCube( p->ppStore[i], pThis ) + { + if ( pThis != p->pBubble && Min_CubeIsContained( pThis, pCube ) ) + { + Min_CubeRecycle( p, pCube ); + return 0; + } + } + // try to find distance one in the same bin + Min_CoverForEachCubePrev( p->ppStore[pCube->nLits], pThis, ppPrev ) + { + if ( Min_CubesDistOne( pCube, pThis, NULL ) ) + { + *ppPrev = pThis->pNext; + Min_CubesTransformOr( pCube, pThis ); + pCube->nLits--; + Min_CubeRecycle( p, pThis ); + p->nCubes--; + return 1; + } + } + // clean the other cubes using this one + for ( i = pCube->nLits + 1; i <= (int)pCube->nVars; i++ ) + { + ppPrev = &p->ppStore[i]; + Min_CoverForEachCubeSafe( p->ppStore[i], pThis, pThis2 ) + { + if ( pThis != p->pBubble && Min_CubeIsContained( pCube, pThis ) ) + { + *ppPrev = pThis->pNext; + Min_CubeRecycle( p, pThis ); + p->nCubes--; + } + else + ppPrev = &pThis->pNext; + } + } + // add the cube + pCube->pNext = p->ppStore[pCube->nLits]; + p->ppStore[pCube->nLits] = pCube; + p->nCubes++; + return 0; +} /**Function************************************************************* - Synopsis [] + Synopsis [Adds the cube to storage.] Description [] @@ -216,27 +427,18 @@ int Min_SopAddCube( Min_Man_t * p, Min_Cube_t * pCube ) SeeAlso [] ***********************************************************************/ -void Min_SopDist1Merge( Min_Man_t * p ) +void Min_SopAddCube( Min_Man_t * p, Min_Cube_t * pCube ) { - Min_Cube_t * pCube, * pCube2, * pCubeNew; - int i; - for ( i = p->nVars; i >= 0; i-- ) - { - Min_CoverForEachCube( p->ppStore[i], pCube ) - Min_CoverForEachCube( pCube->pNext, pCube2 ) - { - assert( pCube->nLits == pCube2->nLits ); - if ( !Min_CubesDistOne( pCube, pCube2, NULL ) ) - continue; - pCubeNew = Min_CubesXor( p, pCube, pCube2 ); - assert( pCubeNew->nLits == pCube->nLits - 1 ); - pCubeNew->pNext = p->ppStore[pCubeNew->nLits]; - p->ppStore[pCubeNew->nLits] = pCubeNew; - p->nCubes++; - } - } + assert( Min_CubeCheck( pCube ) ); + assert( pCube != p->pBubble ); + assert( (int)pCube->nLits == Min_CubeCountLits(pCube) ); + while ( Min_SopAddCubeInt( p, pCube ) ); } + + + + /**Function************************************************************* Synopsis [] @@ -286,6 +488,38 @@ void Min_SopContain( Min_Man_t * p ) SeeAlso [] ***********************************************************************/ +void Min_SopDist1Merge( Min_Man_t * p ) +{ + Min_Cube_t * pCube, * pCube2, * pCubeNew; + int i; + for ( i = p->nVars; i >= 0; i-- ) + { + Min_CoverForEachCube( p->ppStore[i], pCube ) + Min_CoverForEachCube( pCube->pNext, pCube2 ) + { + assert( pCube->nLits == pCube2->nLits ); + if ( !Min_CubesDistOne( pCube, pCube2, NULL ) ) + continue; + pCubeNew = Min_CubesXor( p, pCube, pCube2 ); + assert( pCubeNew->nLits == pCube->nLits - 1 ); + pCubeNew->pNext = p->ppStore[pCubeNew->nLits]; + p->ppStore[pCubeNew->nLits] = pCubeNew; + p->nCubes++; + } + } +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ Min_Cube_t * Min_SopComplement( Min_Man_t * p, Min_Cube_t * pSharp ) { Vec_Int_t * vVars; @@ -334,6 +568,46 @@ Min_Cube_t * Min_SopComplement( Min_Man_t * p, Min_Cube_t * pSharp ) return Min_CoverCollect( p, p->nVars ); } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Min_SopCheck( Min_Man_t * p ) +{ + Min_Cube_t * pCube, * pThis; + int i; + + pCube = Min_CubeAlloc( p ); + Min_CubeXorBit( pCube, 2*0+1 ); + Min_CubeXorBit( pCube, 2*1+1 ); + Min_CubeXorBit( pCube, 2*2+0 ); + Min_CubeXorBit( pCube, 2*3+0 ); + Min_CubeXorBit( pCube, 2*4+0 ); + Min_CubeXorBit( pCube, 2*5+1 ); + Min_CubeXorBit( pCube, 2*6+1 ); + pCube->nLits = 7; + +// Min_CubeWrite( stdout, pCube ); + + // check that the cubes contain it + for ( i = 0; i <= p->nVars; i++ ) + Min_CoverForEachCube( p->ppStore[i], pThis ) + if ( pThis != p->pBubble && Min_CubeIsContained( pThis, pCube ) ) + { + Min_CubeRecycle( p, pCube ); + return 1; + } + Min_CubeRecycle( p, pCube ); + return 0; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/opt/xyz/xyzMinUtil.c b/src/opt/xyz/xyzMinUtil.c index 0aebb815..9ec5f83f 100644 --- a/src/opt/xyz/xyzMinUtil.c +++ b/src/opt/xyz/xyzMinUtil.c @@ -92,13 +92,44 @@ void Min_CoverWrite( FILE * pFile, Min_Cube_t * pCover ) SeeAlso [] ***********************************************************************/ +void Min_CoverWriteStore( FILE * pFile, Min_Man_t * p ) +{ + Min_Cube_t * pCube; + int i; + for ( i = 0; i <= p->nVars; i++ ) + { + Min_CoverForEachCube( p->ppStore[i], pCube ) + { + printf( "%2d : ", i ); + if ( pCube == p->pBubble ) + { + printf( "Bubble\n" ); + continue; + } + Min_CubeWrite( pFile, pCube ); + } + } + printf( "\n" ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ void Min_CoverWriteFile( Min_Cube_t * pCover, char * pName, int fEsop ) { char Buffer[1000]; Min_Cube_t * pCube; FILE * pFile; int i; - sprintf( Buffer, "%s.esop", pName ); + sprintf( Buffer, "%s.%s", pName, fEsop? "esop" : "pla" ); for ( i = strlen(Buffer) - 1; i >= 0; i-- ) if ( Buffer[i] == '<' || Buffer[i] == '>' ) Buffer[i] = '_'; @@ -116,7 +147,7 @@ void Min_CoverWriteFile( Min_Cube_t * pCover, char * pName, int fEsop ) /**Function************************************************************* - Synopsis [Performs one round of rewriting using distance 2 cubes.] + Synopsis [] Description [] @@ -137,6 +168,26 @@ void Min_CoverCheck( Min_Man_t * p ) /**Function************************************************************* + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Min_CubeCheck( Min_Cube_t * pCube ) +{ + int i; + for ( i = 0; i < (int)pCube->nVars; i++ ) + if ( Min_CubeGetVar( pCube, i ) == 0 ) + return 0; + return 1; +} + +/**Function************************************************************* + Synopsis [Converts the cover from the sorted structure.] Description [] @@ -158,6 +209,7 @@ Min_Cube_t * Min_CoverCollect( Min_Man_t * p, int nSuppSize ) assert( i == (int)pCube->nLits ); *ppTail = pCube; ppTail = &pCube->pNext; + assert( pCube->uData[0] ); // not a bubble } } *ppTail = NULL; diff --git a/src/opt/xyz/xyzTest.c b/src/opt/xyz/xyzTest.c index 6c0a63f3..38580790 100644 --- a/src/opt/xyz/xyzTest.c +++ b/src/opt/xyz/xyzTest.c @@ -39,11 +39,377 @@ SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkXyzTestSop( Abc_Ntk_t * pNtk ) +Min_Cube_t * Abc_NodeDeriveCoverPro( Min_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1 ) { - return NULL; + Min_Cube_t * pCover; + Min_Cube_t * pCube0, * pCube1, * pCube; + if ( pCover0 == NULL || pCover1 == NULL ) + return NULL; + // clean storage + Min_ManClean( p, p->nVars ); + // go through the cube pairs + Min_CoverForEachCube( pCover0, pCube0 ) + Min_CoverForEachCube( pCover1, pCube1 ) + { + if ( Min_CubesDisjoint( pCube0, pCube1 ) ) + continue; + pCube = Min_CubesProduct( p, pCube0, pCube1 ); + // add the cube to storage + Min_SopAddCube( p, pCube ); + } + Min_SopMinimize( p ); + pCover = Min_CoverCollect( p, p->nVars ); + assert( p->nCubes == Min_CoverCountCubes(pCover) ); + return pCover; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Min_Cube_t * Abc_NodeDeriveCoverSum( Min_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1 ) +{ + Min_Cube_t * pCover; + Min_Cube_t * pThis, * pCube; + if ( pCover0 == NULL || pCover1 == NULL ) + return NULL; + // clean storage + Min_ManClean( p, p->nVars ); + // add the cubes to storage + Min_CoverForEachCube( pCover0, pThis ) + { + pCube = Min_CubeDup( p, pThis ); + Min_SopAddCube( p, pCube ); + } + Min_CoverForEachCube( pCover1, pThis ) + { + pCube = Min_CubeDup( p, pThis ); + Min_SopAddCube( p, pCube ); + } + Min_SopMinimize( p ); + pCover = Min_CoverCollect( p, p->nVars ); + assert( p->nCubes == Min_CoverCountCubes(pCover) ); + return pCover; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NodeDeriveSops( Min_Man_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t * vSupp, Vec_Ptr_t * vNodes ) +{ + Min_Cube_t * pCov0[2], * pCov1[2]; + Min_Cube_t * pCoverP, * pCoverN; + Abc_Obj_t * pObj; + int i, nCubes, fCompl0, fCompl1; + + // set elementary vars + Vec_PtrForEachEntry( vSupp, pObj, i ) + { + pObj->pCopy = (Abc_Obj_t *)Min_CubeAllocVar( p, i, 0 ); + pObj->pNext = (Abc_Obj_t *)Min_CubeAllocVar( p, i, 1 ); + } + + // get the cover for each node in the array + Vec_PtrForEachEntry( vNodes, pObj, i ) + { + // get the complements + fCompl0 = Abc_ObjFaninC0(pObj); + fCompl1 = Abc_ObjFaninC1(pObj); + // get the covers + pCov0[0] = (Min_Cube_t *)Abc_ObjFanin0(pObj)->pCopy; + pCov0[1] = (Min_Cube_t *)Abc_ObjFanin0(pObj)->pNext; + pCov1[0] = (Min_Cube_t *)Abc_ObjFanin1(pObj)->pCopy; + pCov1[1] = (Min_Cube_t *)Abc_ObjFanin1(pObj)->pNext; + // compute the covers + pCoverP = Abc_NodeDeriveCoverPro( p, pCov0[ fCompl0], pCov1[ fCompl1] ); + pCoverN = Abc_NodeDeriveCoverSum( p, pCov0[!fCompl0], pCov1[!fCompl1] ); + // set the covers + pObj->pCopy = (Abc_Obj_t *)pCoverP; + pObj->pNext = (Abc_Obj_t *)pCoverN; + } + + nCubes = ABC_MIN( Min_CoverCountCubes(pCoverN), Min_CoverCountCubes(pCoverP) ); + +/* +printf( "\n\n" ); +Min_CoverWrite( stdout, pCoverP ); +printf( "\n\n" ); +Min_CoverWrite( stdout, pCoverN ); +*/ + +// printf( "\n" ); +// Min_CoverWrite( stdout, pCoverP ); + +// Min_CoverExpand( p, pCoverP ); +// Min_SopMinimize( p ); +// pCoverP = Min_CoverCollect( p, p->nVars ); + +// printf( "\n" ); +// Min_CoverWrite( stdout, pCoverP ); + +// nCubes = Min_CoverCountCubes(pCoverP); + + // clean the copy fields + Vec_PtrForEachEntry( vNodes, pObj, i ) + pObj->pCopy = pObj->pNext = NULL; + Vec_PtrForEachEntry( vSupp, pObj, i ) + pObj->pCopy = pObj->pNext = NULL; + +// Min_CoverWriteFile( pCoverP, Abc_ObjName(pRoot), 0 ); +// printf( "\n" ); +// Min_CoverWrite( stdout, pCoverP ); + +// printf( "\n" ); +// Min_CoverWrite( stdout, pCoverP ); +// printf( "\n" ); +// Min_CoverWrite( stdout, pCoverN ); + return nCubes; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkTestSop( Abc_Ntk_t * pNtk ) +{ + Min_Man_t * p; + Vec_Ptr_t * vSupp, * vNodes; + Abc_Obj_t * pObj; + int i, nCubes; + assert( Abc_NtkIsStrash(pNtk) ); + + Abc_NtkCleanCopy(pNtk); + Abc_NtkCleanNext(pNtk); + Abc_NtkForEachCo( pNtk, pObj, i ) + { + if ( !Abc_NodeIsAigAnd(Abc_ObjFanin0(pObj)) ) + { + printf( "%-20s : Trivial.\n", Abc_ObjName(pObj) ); + continue; + } + + vSupp = Abc_NtkNodeSupport( pNtk, &pObj, 1 ); + vNodes = Abc_NtkDfsNodes( pNtk, &pObj, 1 ); + + printf( "%20s : Cone = %5d. Supp = %5d. ", + Abc_ObjName(pObj), vNodes->nSize, vSupp->nSize ); +// if ( vSupp->nSize <= 128 ) + { + p = Min_ManAlloc( vSupp->nSize ); + nCubes = Abc_NodeDeriveSops( p, pObj, vSupp, vNodes ); + printf( "Cubes = %5d. ", nCubes ); + Min_ManFree( p ); + } + printf( "\n" ); + + + Vec_PtrFree( vNodes ); + Vec_PtrFree( vSupp ); + } +} + + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Min_Cube_t * Abc_NodeDeriveCover( Min_Man_t * p, Min_Cube_t * pCov0, Min_Cube_t * pCov1, int fComp0, int fComp1 ) +{ + Min_Cube_t * pCover0, * pCover1, * pCover; + Min_Cube_t * pCube0, * pCube1, * pCube; + + // complement the first if needed + if ( !fComp0 ) + pCover0 = pCov0; + else if ( pCov0 && pCov0->nLits == 0 ) // topmost one is the tautology cube + pCover0 = pCov0->pNext; + else + pCover0 = p->pOne0, p->pOne0->pNext = pCov0; + + // complement the second if needed + if ( !fComp1 ) + pCover1 = pCov1; + else if ( pCov1 && pCov1->nLits == 0 ) // topmost one is the tautology cube + pCover1 = pCov1->pNext; + else + pCover1 = p->pOne1, p->pOne1->pNext = pCov1; + + if ( pCover0 == NULL || pCover1 == NULL ) + return NULL; + + // clean storage + Min_ManClean( p, p->nVars ); + // go through the cube pairs + Min_CoverForEachCube( pCover0, pCube0 ) + Min_CoverForEachCube( pCover1, pCube1 ) + { + if ( Min_CubesDisjoint( pCube0, pCube1 ) ) + continue; + pCube = Min_CubesProduct( p, pCube0, pCube1 ); + // add the cube to storage + Min_EsopAddCube( p, pCube ); + } + + if ( p->nCubes > 10 ) + { +// printf( "(%d,", p->nCubes ); + Min_EsopMinimize( p ); +// printf( "%d) ", p->nCubes ); + } + + pCover = Min_CoverCollect( p, p->nVars ); + assert( p->nCubes == Min_CoverCountCubes(pCover) ); + +// if ( p->nCubes > 1000 ) +// printf( "%d ", p->nCubes ); + return pCover; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NodeDeriveEsops( Min_Man_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t * vSupp, Vec_Ptr_t * vNodes ) +{ + Min_Cube_t * pCover, * pCube; + Abc_Obj_t * pObj; + int i; + + // set elementary vars + Vec_PtrForEachEntry( vSupp, pObj, i ) + pObj->pCopy = (Abc_Obj_t *)Min_CubeAllocVar( p, i, 0 ); + + // get the cover for each node in the array + Vec_PtrForEachEntry( vNodes, pObj, i ) + { + pCover = Abc_NodeDeriveCover( p, + (Min_Cube_t *)Abc_ObjFanin0(pObj)->pCopy, + (Min_Cube_t *)Abc_ObjFanin1(pObj)->pCopy, + Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) ); + pObj->pCopy = (Abc_Obj_t *)pCover; + if ( p->nCubes > 3000 ) + return -1; + } + + // add complement if needed + if ( Abc_ObjFaninC0(pRoot) ) + { + if ( pCover && pCover->nLits == 0 ) // topmost one is the tautology cube + { + pCube = pCover; + pCover = pCover->pNext; + Min_CubeRecycle( p, pCube ); + p->nCubes--; + } + else + { + pCube = Min_CubeAlloc( p ); + pCube->pNext = pCover; + p->nCubes++; + } + } +/* + Min_CoverExpand( p, pCover ); + Min_EsopMinimize( p ); + pCover = Min_CoverCollect( p, p->nVars ); +*/ + // clean the copy fields + Vec_PtrForEachEntry( vNodes, pObj, i ) + pObj->pCopy = NULL; + Vec_PtrForEachEntry( vSupp, pObj, i ) + pObj->pCopy = NULL; + +// Min_CoverWriteFile( pCover, Abc_ObjName(pRoot), 1 ); +// Min_CoverWrite( stdout, pCover ); + return p->nCubes; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkTestEsop( Abc_Ntk_t * pNtk ) +{ + Min_Man_t * p; + Vec_Ptr_t * vSupp, * vNodes; + Abc_Obj_t * pObj; + int i, nCubes; + assert( Abc_NtkIsStrash(pNtk) ); + + Abc_NtkCleanCopy(pNtk); + Abc_NtkForEachCo( pNtk, pObj, i ) + { + if ( !Abc_NodeIsAigAnd(Abc_ObjFanin0(pObj)) ) + { + printf( "%-20s : Trivial.\n", Abc_ObjName(pObj) ); + continue; + } + + vSupp = Abc_NtkNodeSupport( pNtk, &pObj, 1 ); + vNodes = Abc_NtkDfsNodes( pNtk, &pObj, 1 ); + + printf( "%20s : Cone = %5d. Supp = %5d. ", + Abc_ObjName(pObj), vNodes->nSize, vSupp->nSize ); +// if ( vSupp->nSize <= 128 ) + { + p = Min_ManAlloc( vSupp->nSize ); + nCubes = Abc_NodeDeriveEsops( p, pObj, vSupp, vNodes ); + printf( "Cubes = %5d. ", nCubes ); + Min_ManFree( p ); + } + printf( "\n" ); + + + Vec_PtrFree( vNodes ); + Vec_PtrFree( vSupp ); + } +} + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/sat/asat/solver.h b/src/sat/asat/solver.h index b82601c4..9618603c 100644 --- a/src/sat/asat/solver.h +++ b/src/sat/asat/solver.h @@ -52,8 +52,9 @@ static const lbool l_Undef = 0; static const lbool l_True = 1; static const lbool l_False = -1; -static inline lit neg (lit l) { return l ^ 1; } -static inline lit toLit (int v) { return v + v; } +static inline lit neg (lit l) { return l ^ 1; } +static inline lit toLit (int v) { return v + v; } +static inline lit toLitCond (int v, int c) { return v + v + (int)(c != 0); } //================================================================================================= // Public interface: diff --git a/src/sat/fraig/fraigCanon.c b/src/sat/fraig/fraigCanon.c index 97da413d..fab01368 100644 --- a/src/sat/fraig/fraigCanon.c +++ b/src/sat/fraig/fraigCanon.c @@ -68,7 +68,7 @@ Fraig_Node_t * Fraig_NodeAndCanon( Fraig_Man_t * pMan, Fraig_Node_t * p1, Fraig_ return p1; return Fraig_Not(pMan->pConst1); } - +/* // check for less trivial cases if ( Fraig_IsComplement(p1) ) { @@ -125,7 +125,7 @@ Fraig_Node_t * Fraig_NodeAndCanon( Fraig_Man_t * pMan, Fraig_Node_t * p1, Fraig_ return Fraig_Not(pMan->pConst1); } } - +*/ // perform level-one structural hashing if ( Fraig_HashTableLookupS( pMan, p1, p2, &pNodeNew ) ) // the node with these children is found { diff --git a/src/sat/fraig/fraigSat.c b/src/sat/fraig/fraigSat.c index bc60e4e9..13f6b50b 100644 --- a/src/sat/fraig/fraigSat.c +++ b/src/sat/fraig/fraigSat.c @@ -41,6 +41,8 @@ extern void * Msat_ClauseVecReadEntry( void * p, int i ); // The best way seems to be fanins followed by fanouts. Slight changes to this order // leads to big degradation in quality. +static int nMuxes; + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -105,7 +107,7 @@ void Fraig_ManProveMiter( Fraig_Man_t * p ) } if ( p->fVerboseP ) { - PRT( "Final miter proof time", clock() - clk ); +// PRT( "Final miter proof time", clock() - clk ); } } @@ -195,6 +197,8 @@ int Fraig_NodeIsEquivalent( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * } */ + nMuxes = 0; + // get the logic cone clk = clock(); @@ -202,6 +206,9 @@ clk = clock(); // Fraig_PrepareCones( p, pOld, pNew ); p->timeTrav += clock() - clk; +// printf( "The number of MUXes detected = %d (%5.2f %% of logic). ", nMuxes, 300.0*nMuxes/(p->vNodes->nSize - p->vInputs->nSize) ); +// PRT( "Time", clock() - clk ); + if ( fVerbose ) printf( "%d(%d) - ", Fraig_CountPis(p,p->vVarsInt), Msat_IntVecReadSize(p->vVarsInt) ); @@ -226,6 +233,8 @@ clk = clock(); RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit, nTimeLimit ); p->timeSat += clock() - clk; +Msat_SolverWriteDimacs( p->pSat, "temp_fraig.cnf" ); + if ( RetValue1 == MSAT_FALSE ) { //p->time1 += clock() - clk; @@ -284,6 +293,7 @@ p->time3 += clock() - clk; clk = clock(); RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit, nTimeLimit ); p->timeSat += clock() - clk; + if ( RetValue1 == MSAT_FALSE ) { //p->time1 += clock() - clk; @@ -552,6 +562,7 @@ void Fraig_PrepareCones( Fraig_Man_t * pMan, Fraig_Node_t * pOld, Fraig_Node_t * Fraig_PrepareCones_rec( pMan, pNew ); Fraig_PrepareCones_rec( pMan, pOld ); + /* nVars = Msat_IntVecReadSize( pMan->vVarsInt ); pVars = Msat_IntVecReadArray( pMan->vVarsInt ); @@ -715,6 +726,8 @@ void Fraig_OrderVariables( Fraig_Man_t * pMan, Fraig_Node_t * pOld, Fraig_Node_t Fraig_NodeVecPushUnique( pNode->vFanins, Fraig_Regular(Fraig_Regular(pNode->p2)->p2) ); Fraig_SupergateAddClausesMux( pMan, pNode ); // Fraig_DetectFanoutFreeConeMux( pMan, pNode ); + + nMuxes++; } else { @@ -1057,6 +1070,12 @@ void Fraig_SupergateAddClausesMux( Fraig_Man_t * p, Fraig_Node_t * pNode ) // t + e + f' // t' + e' + f + if ( VarT == VarE ) + { +// assert( fCompT == !fCompE ); + return; + } + Msat_IntVecClear( p->vProj ); Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarT, 0^fCompT) ); Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarE, 0^fCompE) ); @@ -1069,6 +1088,7 @@ void Fraig_SupergateAddClausesMux( Fraig_Man_t * p, Fraig_Node_t * pNode ) Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarF, 0) ); RetValue = Msat_SolverAddClause( p->pSat, p->vProj ); assert( RetValue ); + } diff --git a/src/sat/msat/msat.h b/src/sat/msat/msat.h index 37e0bbeb..40028784 100644 --- a/src/sat/msat/msat.h +++ b/src/sat/msat/msat.h @@ -87,6 +87,7 @@ extern void Msat_SolverPrintClauses( Msat_Solver_t * p ); extern void Msat_SolverWriteDimacs( Msat_Solver_t * p, char * pFileName ); // access to the solver internal data extern int Msat_SolverReadVarNum( Msat_Solver_t * p ); +extern int Msat_SolverReadClauseNum( Msat_Solver_t * p ); extern int Msat_SolverReadVarAllocNum( Msat_Solver_t * p ); extern int * Msat_SolverReadAssignsArray( Msat_Solver_t * p ); extern int * Msat_SolverReadModelArray( Msat_Solver_t * p ); diff --git a/src/sat/msat/msatClause.c b/src/sat/msat/msatClause.c index f944ed81..62b9ecad 100644 --- a/src/sat/msat/msatClause.c +++ b/src/sat/msat/msatClause.c @@ -82,6 +82,10 @@ bool Msat_ClauseCreate( Msat_Solver_t * p, Msat_IntVec_t * vLits, bool fLearned, // nSeenId - 1 stands for negative // nSeenId stands for positive // Remove false literals + + // there is a bug here!!!! + // when the same var in opposite polarities is given, it drops one polarity!!! + for ( i = j = 0; i < nLits; i++ ) { // get the corresponding variable Var = MSAT_LIT2VAR(pLits[i]); @@ -190,6 +194,7 @@ bool Msat_ClauseCreate( Msat_Solver_t * p, Msat_IntVec_t * vLits, bool fLearned, { Msat_SolverVarBumpActivity( p, pLits[i] ); // Msat_SolverVarBumpActivity( p, pLits[i] ); + p->pFreq[ MSAT_LIT2VAR(pLits[i]) ]++; } } diff --git a/src/sat/msat/msatInt.h b/src/sat/msat/msatInt.h index ef2375a7..3dfe2109 100644 --- a/src/sat/msat/msatInt.h +++ b/src/sat/msat/msatInt.h @@ -151,6 +151,7 @@ struct Msat_Solver_t_ int nSeenId; // the id of current seeing Msat_IntVec_t * vReason; // the temporary array of literals Msat_IntVec_t * vTemp; // the temporary array of literals + int * pFreq; // the number of times each var participated in conflicts // the memory manager Msat_MmStep_t * pMem; diff --git a/src/sat/msat/msatSolverApi.c b/src/sat/msat/msatSolverApi.c index dd3a5a43..4a721487 100644 --- a/src/sat/msat/msatSolverApi.c +++ b/src/sat/msat/msatSolverApi.c @@ -42,6 +42,7 @@ static void Msat_SolverSetupTruthTables( unsigned uTruths[][2] ); ***********************************************************************/ int Msat_SolverReadVarNum( Msat_Solver_t * p ) { return p->nVars; } +int Msat_SolverReadClauseNum( Msat_Solver_t * p ) { return p->nClauses; } int Msat_SolverReadVarAllocNum( Msat_Solver_t * p ) { return p->nVarsAlloc;} int Msat_SolverReadDecisionLevel( Msat_Solver_t * p ) { return Msat_IntVecReadSize(p->vTrailLim); } int * Msat_SolverReadDecisionLevelArray( Msat_Solver_t * p ) { return p->pLevel; } diff --git a/src/sat/msat/msatSolverCore.c b/src/sat/msat/msatSolverCore.c index ed228b33..5f13694b 100644 --- a/src/sat/msat/msatSolverCore.c +++ b/src/sat/msat/msatSolverCore.c @@ -140,6 +140,9 @@ bool Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * vAssumps, int nBackTra int64 nConflictsOld = p->Stats.nConflicts; int64 nDecisionsOld = p->Stats.nDecisions; + p->pFreq = ALLOC( int, p->nVarsAlloc ); + memset( p->pFreq, 0, sizeof(int) * p->nVarsAlloc ); + if ( vAssumps ) { int * pAssumps, nAssumps, i; @@ -181,6 +184,23 @@ bool Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * vAssumps, int nBackTra } Msat_SolverCancelUntil( p, 0 ); p->nBackTracks = (int)p->Stats.nConflicts - p->nBackTracks; +/* + PRT( "True solver runtime", clock() - timeStart ); + // print the statistics + { + int i, Counter = 0; + for ( i = 0; i < p->nVars; i++ ) + if ( p->pFreq[i] > 0 ) + { + printf( "%d ", p->pFreq[i] ); + Counter++; + } + if ( Counter ) + printf( "\n" ); + printf( "Total = %d. Used = %d. Decisions = %d. Imps = %d. Conflicts = %d. ", p->nVars, Counter, (int)p->Stats.nDecisions, (int)p->Stats.nPropagations, (int)p->Stats.nConflicts ); + PRT( "Time", clock() - timeStart ); + } +*/ return Status; } |