| /**CFile**************************************************************** | |
| FileName [cecSolve.c] | |
| SystemName [ABC: Logic synthesis and verification system.] | |
| PackageName [Combinational equivalence checking.] | |
| Synopsis [Performs one round of SAT solving.] | |
| Author [Alan Mishchenko] | |
| Affiliation [UC Berkeley] | |
| Date [Ver. 1.0. Started - June 20, 2005.] | |
| Revision [$Id: cecSolve.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] | |
| ***********************************************************************/ | |
| #include "cecInt.h" | |
| ABC_NAMESPACE_IMPL_START | |
| //////////////////////////////////////////////////////////////////////// | |
| /// DECLARATIONS /// | |
| //////////////////////////////////////////////////////////////////////// | |
| static inline int Cec_ObjSatNum( Cec_ManSat_t * p, Gia_Obj_t * pObj ) { return p->pSatVars[Gia_ObjId(p->pAig,pObj)]; } | |
| static inline void Cec_ObjSetSatNum( Cec_ManSat_t * p, Gia_Obj_t * pObj, int Num ) { p->pSatVars[Gia_ObjId(p->pAig,pObj)] = Num; } | |
| //////////////////////////////////////////////////////////////////////// | |
| /// FUNCTION DEFINITIONS /// | |
| //////////////////////////////////////////////////////////////////////// | |
| /**Function************************************************************* | |
| Synopsis [Returns value of the SAT variable.] | |
| Description [] | |
| SideEffects [] | |
| SeeAlso [] | |
| ***********************************************************************/ | |
| int Cec_ObjSatVarValue( Cec_ManSat_t * p, Gia_Obj_t * pObj ) | |
| { | |
| return sat_solver_var_value( p->pSat, Cec_ObjSatNum(p, pObj) ); | |
| } | |
| /**Function************************************************************* | |
| Synopsis [Addes clauses to the solver.] | |
| Description [] | |
| SideEffects [] | |
| SeeAlso [] | |
| ***********************************************************************/ | |
| void Cec_AddClausesMux( Cec_ManSat_t * p, Gia_Obj_t * pNode ) | |
| { | |
| Gia_Obj_t * pNodeI, * pNodeT, * pNodeE; | |
| int pLits[4], RetValue, VarF, VarI, VarT, VarE, fCompT, fCompE; | |
| assert( !Gia_IsComplement( pNode ) ); | |
| assert( Gia_ObjIsMuxType( pNode ) ); | |
| // get nodes (I = if, T = then, E = else) | |
| pNodeI = Gia_ObjRecognizeMux( pNode, &pNodeT, &pNodeE ); | |
| // get the variable numbers | |
| VarF = Cec_ObjSatNum(p,pNode); | |
| VarI = Cec_ObjSatNum(p,pNodeI); | |
| VarT = Cec_ObjSatNum(p,Gia_Regular(pNodeT)); | |
| VarE = Cec_ObjSatNum(p,Gia_Regular(pNodeE)); | |
| // get the complementation flags | |
| fCompT = Gia_IsComplement(pNodeT); | |
| fCompE = Gia_IsComplement(pNodeE); | |
| // f = ITE(i, t, e) | |
| // i' + t' + f | |
| // i' + t + f' | |
| // i + e' + f | |
| // i + e + f' | |
| // create four clauses | |
| pLits[0] = toLitCond(VarI, 1); | |
| pLits[1] = toLitCond(VarT, 1^fCompT); | |
| pLits[2] = toLitCond(VarF, 0); | |
| if ( p->pPars->fPolarFlip ) | |
| { | |
| if ( pNodeI->fPhase ) pLits[0] = lit_neg( pLits[0] ); | |
| if ( Gia_Regular(pNodeT)->fPhase ) pLits[1] = lit_neg( pLits[1] ); | |
| if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] ); | |
| } | |
| RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 ); | |
| assert( RetValue ); | |
| pLits[0] = toLitCond(VarI, 1); | |
| pLits[1] = toLitCond(VarT, 0^fCompT); | |
| pLits[2] = toLitCond(VarF, 1); | |
| if ( p->pPars->fPolarFlip ) | |
| { | |
| if ( pNodeI->fPhase ) pLits[0] = lit_neg( pLits[0] ); | |
| if ( Gia_Regular(pNodeT)->fPhase ) pLits[1] = lit_neg( pLits[1] ); | |
| if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] ); | |
| } | |
| RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 ); | |
| assert( RetValue ); | |
| pLits[0] = toLitCond(VarI, 0); | |
| pLits[1] = toLitCond(VarE, 1^fCompE); | |
| pLits[2] = toLitCond(VarF, 0); | |
| if ( p->pPars->fPolarFlip ) | |
| { | |
| if ( pNodeI->fPhase ) pLits[0] = lit_neg( pLits[0] ); | |
| if ( Gia_Regular(pNodeE)->fPhase ) pLits[1] = lit_neg( pLits[1] ); | |
| if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] ); | |
| } | |
| RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 ); | |
| assert( RetValue ); | |
| pLits[0] = toLitCond(VarI, 0); | |
| pLits[1] = toLitCond(VarE, 0^fCompE); | |
| pLits[2] = toLitCond(VarF, 1); | |
| if ( p->pPars->fPolarFlip ) | |
| { | |
| if ( pNodeI->fPhase ) pLits[0] = lit_neg( pLits[0] ); | |
| if ( Gia_Regular(pNodeE)->fPhase ) pLits[1] = lit_neg( pLits[1] ); | |
| if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] ); | |
| } | |
| RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 ); | |
| assert( RetValue ); | |
| // two additional clauses | |
| // t' & e' -> f' | |
| // t & e -> f | |
| // t + e + f' | |
| // t' + e' + f | |
| if ( VarT == VarE ) | |
| { | |
| // assert( fCompT == !fCompE ); | |
| return; | |
| } | |
| pLits[0] = toLitCond(VarT, 0^fCompT); | |
| pLits[1] = toLitCond(VarE, 0^fCompE); | |
| pLits[2] = toLitCond(VarF, 1); | |
| if ( p->pPars->fPolarFlip ) | |
| { | |
| if ( Gia_Regular(pNodeT)->fPhase ) pLits[0] = lit_neg( pLits[0] ); | |
| if ( Gia_Regular(pNodeE)->fPhase ) pLits[1] = lit_neg( pLits[1] ); | |
| if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] ); | |
| } | |
| RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 ); | |
| assert( RetValue ); | |
| pLits[0] = toLitCond(VarT, 1^fCompT); | |
| pLits[1] = toLitCond(VarE, 1^fCompE); | |
| pLits[2] = toLitCond(VarF, 0); | |
| if ( p->pPars->fPolarFlip ) | |
| { | |
| if ( Gia_Regular(pNodeT)->fPhase ) pLits[0] = lit_neg( pLits[0] ); | |
| if ( Gia_Regular(pNodeE)->fPhase ) pLits[1] = lit_neg( pLits[1] ); | |
| if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] ); | |
| } | |
| RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 ); | |
| assert( RetValue ); | |
| } | |
| /**Function************************************************************* | |
| Synopsis [Addes clauses to the solver.] | |
| Description [] | |
| SideEffects [] | |
| SeeAlso [] | |
| ***********************************************************************/ | |
| void Cec_AddClausesSuper( Cec_ManSat_t * p, Gia_Obj_t * pNode, Vec_Ptr_t * vSuper ) | |
| { | |
| Gia_Obj_t * pFanin; | |
| int * pLits, nLits, RetValue, i; | |
| assert( !Gia_IsComplement(pNode) ); | |
| assert( Gia_ObjIsAnd( pNode ) ); | |
| // create storage for literals | |
| nLits = Vec_PtrSize(vSuper) + 1; | |
| pLits = ABC_ALLOC( int, nLits ); | |
| // suppose AND-gate is A & B = C | |
| // add !A => !C or A + !C | |
| Vec_PtrForEachEntry( Gia_Obj_t *, vSuper, pFanin, i ) | |
| { | |
| pLits[0] = toLitCond(Cec_ObjSatNum(p,Gia_Regular(pFanin)), Gia_IsComplement(pFanin)); | |
| pLits[1] = toLitCond(Cec_ObjSatNum(p,pNode), 1); | |
| if ( p->pPars->fPolarFlip ) | |
| { | |
| if ( Gia_Regular(pFanin)->fPhase ) pLits[0] = lit_neg( pLits[0] ); | |
| if ( pNode->fPhase ) pLits[1] = lit_neg( pLits[1] ); | |
| } | |
| RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 ); | |
| assert( RetValue ); | |
| } | |
| // add A & B => C or !A + !B + C | |
| Vec_PtrForEachEntry( Gia_Obj_t *, vSuper, pFanin, i ) | |
| { | |
| pLits[i] = toLitCond(Cec_ObjSatNum(p,Gia_Regular(pFanin)), !Gia_IsComplement(pFanin)); | |
| if ( p->pPars->fPolarFlip ) | |
| { | |
| if ( Gia_Regular(pFanin)->fPhase ) pLits[i] = lit_neg( pLits[i] ); | |
| } | |
| } | |
| pLits[nLits-1] = toLitCond(Cec_ObjSatNum(p,pNode), 0); | |
| if ( p->pPars->fPolarFlip ) | |
| { | |
| if ( pNode->fPhase ) pLits[nLits-1] = lit_neg( pLits[nLits-1] ); | |
| } | |
| RetValue = sat_solver_addclause( p->pSat, pLits, pLits + nLits ); | |
| assert( RetValue ); | |
| ABC_FREE( pLits ); | |
| } | |
| /**Function************************************************************* | |
| Synopsis [Collects the supergate.] | |
| Description [] | |
| SideEffects [] | |
| SeeAlso [] | |
| ***********************************************************************/ | |
| void Cec_CollectSuper_rec( Gia_Obj_t * pObj, Vec_Ptr_t * vSuper, int fFirst, int fUseMuxes ) | |
| { | |
| // if the new node is complemented or a PI, another gate begins | |
| if ( Gia_IsComplement(pObj) || Gia_ObjIsCi(pObj) || | |
| (!fFirst && Gia_ObjValue(pObj) > 1) || | |
| (fUseMuxes && Gia_ObjIsMuxType(pObj)) ) | |
| { | |
| Vec_PtrPushUnique( vSuper, pObj ); | |
| return; | |
| } | |
| // go through the branches | |
| Cec_CollectSuper_rec( Gia_ObjChild0(pObj), vSuper, 0, fUseMuxes ); | |
| Cec_CollectSuper_rec( Gia_ObjChild1(pObj), vSuper, 0, fUseMuxes ); | |
| } | |
| /**Function************************************************************* | |
| Synopsis [Collects the supergate.] | |
| Description [] | |
| SideEffects [] | |
| SeeAlso [] | |
| ***********************************************************************/ | |
| void Cec_CollectSuper( Gia_Obj_t * pObj, int fUseMuxes, Vec_Ptr_t * vSuper ) | |
| { | |
| assert( !Gia_IsComplement(pObj) ); | |
| assert( !Gia_ObjIsCi(pObj) ); | |
| Vec_PtrClear( vSuper ); | |
| Cec_CollectSuper_rec( pObj, vSuper, 1, fUseMuxes ); | |
| } | |
| /**Function************************************************************* | |
| Synopsis [Updates the solver clause database.] | |
| Description [] | |
| SideEffects [] | |
| SeeAlso [] | |
| ***********************************************************************/ | |
| void Cec_ObjAddToFrontier( Cec_ManSat_t * p, Gia_Obj_t * pObj, Vec_Ptr_t * vFrontier ) | |
| { | |
| assert( !Gia_IsComplement(pObj) ); | |
| if ( Cec_ObjSatNum(p,pObj) ) | |
| return; | |
| assert( Cec_ObjSatNum(p,pObj) == 0 ); | |
| if ( Gia_ObjIsConst0(pObj) ) | |
| return; | |
| Vec_PtrPush( p->vUsedNodes, pObj ); | |
| Cec_ObjSetSatNum( p, pObj, p->nSatVars++ ); | |
| if ( Gia_ObjIsAnd(pObj) ) | |
| Vec_PtrPush( vFrontier, pObj ); | |
| } | |
| /**Function************************************************************* | |
| Synopsis [Updates the solver clause database.] | |
| Description [] | |
| SideEffects [] | |
| SeeAlso [] | |
| ***********************************************************************/ | |
| void Cec_CnfNodeAddToSolver( Cec_ManSat_t * p, Gia_Obj_t * pObj ) | |
| { | |
| Vec_Ptr_t * vFrontier; | |
| Gia_Obj_t * pNode, * pFanin; | |
| int i, k, fUseMuxes = 1; | |
| // quit if CNF is ready | |
| if ( Cec_ObjSatNum(p,pObj) ) | |
| return; | |
| if ( Gia_ObjIsCi(pObj) ) | |
| { | |
| Vec_PtrPush( p->vUsedNodes, pObj ); | |
| Cec_ObjSetSatNum( p, pObj, p->nSatVars++ ); | |
| sat_solver_setnvars( p->pSat, p->nSatVars ); | |
| return; | |
| } | |
| assert( Gia_ObjIsAnd(pObj) ); | |
| // start the frontier | |
| vFrontier = Vec_PtrAlloc( 100 ); | |
| Cec_ObjAddToFrontier( p, pObj, vFrontier ); | |
| // explore nodes in the frontier | |
| Vec_PtrForEachEntry( Gia_Obj_t *, vFrontier, pNode, i ) | |
| { | |
| // create the supergate | |
| assert( Cec_ObjSatNum(p,pNode) ); | |
| if ( fUseMuxes && Gia_ObjIsMuxType(pNode) ) | |
| { | |
| Vec_PtrClear( p->vFanins ); | |
| Vec_PtrPushUnique( p->vFanins, Gia_ObjFanin0( Gia_ObjFanin0(pNode) ) ); | |
| Vec_PtrPushUnique( p->vFanins, Gia_ObjFanin0( Gia_ObjFanin1(pNode) ) ); | |
| Vec_PtrPushUnique( p->vFanins, Gia_ObjFanin1( Gia_ObjFanin0(pNode) ) ); | |
| Vec_PtrPushUnique( p->vFanins, Gia_ObjFanin1( Gia_ObjFanin1(pNode) ) ); | |
| Vec_PtrForEachEntry( Gia_Obj_t *, p->vFanins, pFanin, k ) | |
| Cec_ObjAddToFrontier( p, Gia_Regular(pFanin), vFrontier ); | |
| Cec_AddClausesMux( p, pNode ); | |
| } | |
| else | |
| { | |
| Cec_CollectSuper( pNode, fUseMuxes, p->vFanins ); | |
| Vec_PtrForEachEntry( Gia_Obj_t *, p->vFanins, pFanin, k ) | |
| Cec_ObjAddToFrontier( p, Gia_Regular(pFanin), vFrontier ); | |
| Cec_AddClausesSuper( p, pNode, p->vFanins ); | |
| } | |
| assert( Vec_PtrSize(p->vFanins) > 1 ); | |
| } | |
| Vec_PtrFree( vFrontier ); | |
| } | |
| /**Function************************************************************* | |
| Synopsis [Recycles the SAT solver.] | |
| Description [] | |
| SideEffects [] | |
| SeeAlso [] | |
| ***********************************************************************/ | |
| void Cec_ManSatSolverRecycle( Cec_ManSat_t * p ) | |
| { | |
| int Lit; | |
| if ( p->pSat ) | |
| { | |
| Gia_Obj_t * pObj; | |
| int i; | |
| Vec_PtrForEachEntry( Gia_Obj_t *, p->vUsedNodes, pObj, i ) | |
| Cec_ObjSetSatNum( p, pObj, 0 ); | |
| Vec_PtrClear( p->vUsedNodes ); | |
| // memset( p->pSatVars, 0, sizeof(int) * Gia_ManObjNumMax(p->pAigTotal) ); | |
| sat_solver_delete( p->pSat ); | |
| } | |
| p->pSat = sat_solver_new(); | |
| sat_solver_setnvars( p->pSat, 1000 ); | |
| p->pSat->factors = ABC_CALLOC( double, p->pSat->cap ); | |
| // var 0 is not used | |
| // var 1 is reserved for const0 node - add the clause | |
| p->nSatVars = 1; | |
| // p->nSatVars = 0; | |
| Lit = toLitCond( p->nSatVars, 1 ); | |
| // if ( p->pPars->fPolarFlip ) // no need to normalize const0 node (bug fix by SS on 9/17/2012) | |
| // Lit = lit_neg( Lit ); | |
| sat_solver_addclause( p->pSat, &Lit, &Lit + 1 ); | |
| Cec_ObjSetSatNum( p, Gia_ManConst0(p->pAig), p->nSatVars++ ); | |
| p->nRecycles++; | |
| p->nCallsSince = 0; | |
| } | |
| /**Function************************************************************* | |
| Synopsis [Sets variable activities in the cone.] | |
| Description [] | |
| SideEffects [] | |
| SeeAlso [] | |
| ***********************************************************************/ | |
| void Cec_SetActivityFactors_rec( Cec_ManSat_t * p, Gia_Obj_t * pObj, int LevelMin, int LevelMax ) | |
| { | |
| float dActConeBumpMax = 20.0; | |
| int iVar; | |
| // skip visited variables | |
| if ( Gia_ObjIsTravIdCurrent(p->pAig, pObj) ) | |
| return; | |
| Gia_ObjSetTravIdCurrent(p->pAig, pObj); | |
| // add the PI to the list | |
| if ( Gia_ObjLevel(p->pAig, pObj) <= LevelMin || Gia_ObjIsCi(pObj) ) | |
| return; | |
| // set the factor of this variable | |
| // (LevelMax-LevelMin) / (pObj->Level-LevelMin) = p->pPars->dActConeBumpMax / ThisBump | |
| if ( (iVar = Cec_ObjSatNum(p,pObj)) ) | |
| { | |
| p->pSat->factors[iVar] = dActConeBumpMax * (Gia_ObjLevel(p->pAig, pObj) - LevelMin)/(LevelMax - LevelMin); | |
| veci_push(&p->pSat->act_vars, iVar); | |
| } | |
| // explore the fanins | |
| Cec_SetActivityFactors_rec( p, Gia_ObjFanin0(pObj), LevelMin, LevelMax ); | |
| Cec_SetActivityFactors_rec( p, Gia_ObjFanin1(pObj), LevelMin, LevelMax ); | |
| } | |
| /**Function************************************************************* | |
| Synopsis [Sets variable activities in the cone.] | |
| Description [] | |
| SideEffects [] | |
| SeeAlso [] | |
| ***********************************************************************/ | |
| int Cec_SetActivityFactors( Cec_ManSat_t * p, Gia_Obj_t * pObj ) | |
| { | |
| float dActConeRatio = 0.5; | |
| int LevelMin, LevelMax; | |
| // reset the active variables | |
| veci_resize(&p->pSat->act_vars, 0); | |
| // prepare for traversal | |
| Gia_ManIncrementTravId( p->pAig ); | |
| // determine the min and max level to visit | |
| assert( dActConeRatio > 0 && dActConeRatio < 1 ); | |
| LevelMax = Gia_ObjLevel(p->pAig,pObj); | |
| LevelMin = (int)(LevelMax * (1.0 - dActConeRatio)); | |
| // traverse | |
| Cec_SetActivityFactors_rec( p, pObj, LevelMin, LevelMax ); | |
| //Cec_PrintActivity( p ); | |
| return 1; | |
| } | |
| /**Function************************************************************* | |
| Synopsis [Runs equivalence test for the two nodes.] | |
| Description [] | |
| SideEffects [] | |
| SeeAlso [] | |
| ***********************************************************************/ | |
| int Cec_ManSatCheckNode( Cec_ManSat_t * p, Gia_Obj_t * pObj ) | |
| { | |
| Gia_Obj_t * pObjR = Gia_Regular(pObj); | |
| int nBTLimit = p->pPars->nBTLimit; | |
| int Lit, RetValue, status, nConflicts; | |
| abctime clk, clk2; | |
| if ( pObj == Gia_ManConst0(p->pAig) ) | |
| return 1; | |
| if ( pObj == Gia_ManConst1(p->pAig) ) | |
| { | |
| assert( 0 ); | |
| return 0; | |
| } | |
| p->nCallsSince++; // experiment with this!!! | |
| p->nSatTotal++; | |
| // check if SAT solver needs recycling | |
| if ( p->pSat == NULL || | |
| (p->pPars->nSatVarMax && | |
| p->nSatVars > p->pPars->nSatVarMax && | |
| p->nCallsSince > p->pPars->nCallsRecycle) ) | |
| Cec_ManSatSolverRecycle( p ); | |
| // if the nodes do not have SAT variables, allocate them | |
| clk2 = Abc_Clock(); | |
| Cec_CnfNodeAddToSolver( p, pObjR ); | |
| //ABC_PRT( "cnf", Abc_Clock() - clk2 ); | |
| //Abc_Print( 1, "%d \n", p->pSat->size ); | |
| clk2 = Abc_Clock(); | |
| // Cec_SetActivityFactors( p, pObjR ); | |
| //ABC_PRT( "act", Abc_Clock() - clk2 ); | |
| // propage unit clauses | |
| if ( p->pSat->qtail != p->pSat->qhead ) | |
| { | |
| status = sat_solver_simplify(p->pSat); | |
| assert( status != 0 ); | |
| assert( p->pSat->qtail == p->pSat->qhead ); | |
| } | |
| // solve under assumptions | |
| // A = 1; B = 0 OR A = 1; B = 1 | |
| Lit = toLitCond( Cec_ObjSatNum(p,pObjR), Gia_IsComplement(pObj) ); | |
| if ( p->pPars->fPolarFlip ) | |
| { | |
| if ( pObjR->fPhase ) Lit = lit_neg( Lit ); | |
| } | |
| //Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 ); | |
| clk = Abc_Clock(); | |
| nConflicts = p->pSat->stats.conflicts; | |
| clk2 = Abc_Clock(); | |
| RetValue = sat_solver_solve( p->pSat, &Lit, &Lit + 1, | |
| (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); | |
| //ABC_PRT( "sat", Abc_Clock() - clk2 ); | |
| if ( RetValue == l_False ) | |
| { | |
| p->timeSatUnsat += Abc_Clock() - clk; | |
| Lit = lit_neg( Lit ); | |
| RetValue = sat_solver_addclause( p->pSat, &Lit, &Lit + 1 ); | |
| assert( RetValue ); | |
| p->nSatUnsat++; | |
| p->nConfUnsat += p->pSat->stats.conflicts - nConflicts; | |
| //Abc_Print( 1, "UNSAT after %d conflicts\n", p->pSat->stats.conflicts - nConflicts ); | |
| return 1; | |
| } | |
| else if ( RetValue == l_True ) | |
| { | |
| p->timeSatSat += Abc_Clock() - clk; | |
| p->nSatSat++; | |
| p->nConfSat += p->pSat->stats.conflicts - nConflicts; | |
| //Abc_Print( 1, "SAT after %d conflicts\n", p->pSat->stats.conflicts - nConflicts ); | |
| return 0; | |
| } | |
| else // if ( RetValue == l_Undef ) | |
| { | |
| p->timeSatUndec += Abc_Clock() - clk; | |
| p->nSatUndec++; | |
| p->nConfUndec += p->pSat->stats.conflicts - nConflicts; | |
| //Abc_Print( 1, "UNDEC after %d conflicts\n", p->pSat->stats.conflicts - nConflicts ); | |
| return -1; | |
| } | |
| } | |
| /**Function************************************************************* | |
| Synopsis [Runs equivalence test for the two nodes.] | |
| Description [] | |
| SideEffects [] | |
| SeeAlso [] | |
| ***********************************************************************/ | |
| int Cec_ManSatCheckNodeTwo( Cec_ManSat_t * p, Gia_Obj_t * pObj1, Gia_Obj_t * pObj2 ) | |
| { | |
| Gia_Obj_t * pObjR1 = Gia_Regular(pObj1); | |
| Gia_Obj_t * pObjR2 = Gia_Regular(pObj2); | |
| int nBTLimit = p->pPars->nBTLimit; | |
| int Lits[2], RetValue, status, nConflicts; | |
| abctime clk, clk2; | |
| if ( pObj1 == Gia_ManConst0(p->pAig) || pObj2 == Gia_ManConst0(p->pAig) || pObj1 == Gia_Not(pObj2) ) | |
| return 1; | |
| if ( pObj1 == Gia_ManConst1(p->pAig) && (pObj2 == NULL || pObj2 == Gia_ManConst1(p->pAig)) ) | |
| { | |
| assert( 0 ); | |
| return 0; | |
| } | |
| p->nCallsSince++; // experiment with this!!! | |
| p->nSatTotal++; | |
| // check if SAT solver needs recycling | |
| if ( p->pSat == NULL || | |
| (p->pPars->nSatVarMax && | |
| p->nSatVars > p->pPars->nSatVarMax && | |
| p->nCallsSince > p->pPars->nCallsRecycle) ) | |
| Cec_ManSatSolverRecycle( p ); | |
| // if the nodes do not have SAT variables, allocate them | |
| clk2 = Abc_Clock(); | |
| Cec_CnfNodeAddToSolver( p, pObjR1 ); | |
| Cec_CnfNodeAddToSolver( p, pObjR2 ); | |
| //ABC_PRT( "cnf", Abc_Clock() - clk2 ); | |
| //Abc_Print( 1, "%d \n", p->pSat->size ); | |
| clk2 = Abc_Clock(); | |
| // Cec_SetActivityFactors( p, pObjR1 ); | |
| // Cec_SetActivityFactors( p, pObjR2 ); | |
| //ABC_PRT( "act", Abc_Clock() - clk2 ); | |
| // propage unit clauses | |
| if ( p->pSat->qtail != p->pSat->qhead ) | |
| { | |
| status = sat_solver_simplify(p->pSat); | |
| assert( status != 0 ); | |
| assert( p->pSat->qtail == p->pSat->qhead ); | |
| } | |
| // solve under assumptions | |
| // A = 1; B = 0 OR A = 1; B = 1 | |
| Lits[0] = toLitCond( Cec_ObjSatNum(p,pObjR1), Gia_IsComplement(pObj1) ); | |
| Lits[1] = toLitCond( Cec_ObjSatNum(p,pObjR2), Gia_IsComplement(pObj2) ); | |
| if ( p->pPars->fPolarFlip ) | |
| { | |
| if ( pObjR1->fPhase ) Lits[0] = lit_neg( Lits[0] ); | |
| if ( pObjR2->fPhase ) Lits[1] = lit_neg( Lits[1] ); | |
| } | |
| //Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 ); | |
| clk = Abc_Clock(); | |
| nConflicts = p->pSat->stats.conflicts; | |
| clk2 = Abc_Clock(); | |
| RetValue = sat_solver_solve( p->pSat, Lits, Lits + 2, | |
| (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); | |
| //ABC_PRT( "sat", Abc_Clock() - clk2 ); | |
| if ( RetValue == l_False ) | |
| { | |
| p->timeSatUnsat += Abc_Clock() - clk; | |
| Lits[0] = lit_neg( Lits[0] ); | |
| Lits[1] = lit_neg( Lits[1] ); | |
| RetValue = sat_solver_addclause( p->pSat, Lits, Lits + 2 ); | |
| assert( RetValue ); | |
| p->nSatUnsat++; | |
| p->nConfUnsat += p->pSat->stats.conflicts - nConflicts; | |
| //Abc_Print( 1, "UNSAT after %d conflicts\n", p->pSat->stats.conflicts - nConflicts ); | |
| return 1; | |
| } | |
| else if ( RetValue == l_True ) | |
| { | |
| p->timeSatSat += Abc_Clock() - clk; | |
| p->nSatSat++; | |
| p->nConfSat += p->pSat->stats.conflicts - nConflicts; | |
| //Abc_Print( 1, "SAT after %d conflicts\n", p->pSat->stats.conflicts - nConflicts ); | |
| return 0; | |
| } | |
| else // if ( RetValue == l_Undef ) | |
| { | |
| p->timeSatUndec += Abc_Clock() - clk; | |
| p->nSatUndec++; | |
| p->nConfUndec += p->pSat->stats.conflicts - nConflicts; | |
| //Abc_Print( 1, "UNDEC after %d conflicts\n", p->pSat->stats.conflicts - nConflicts ); | |
| return -1; | |
| } | |
| } | |
| /**Function************************************************************* | |
| Synopsis [Performs one round of solving for the POs of the AIG.] | |
| Description [Labels the nodes that have been proved (pObj->fMark1) | |
| and returns the set of satisfying assignments.] | |
| SideEffects [] | |
| SeeAlso [] | |
| ***********************************************************************/ | |
| void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_Int_t * vIdsOrig, Vec_Int_t * vMiterPairs, Vec_Int_t * vEquivPairs ) | |
| { | |
| Bar_Progress_t * pProgress = NULL; | |
| Cec_ManSat_t * p; | |
| Gia_Obj_t * pObj; | |
| int i, status; | |
| abctime clk = Abc_Clock(), clk2; | |
| // reset the manager | |
| if ( pPat ) | |
| { | |
| pPat->iStart = Vec_StrSize(pPat->vStorage); | |
| pPat->nPats = 0; | |
| pPat->nPatLits = 0; | |
| pPat->nPatLitsMin = 0; | |
| } | |
| Gia_ManSetPhase( pAig ); | |
| Gia_ManLevelNum( pAig ); | |
| Gia_ManIncrementTravId( pAig ); | |
| p = Cec_ManSatCreate( pAig, pPars ); | |
| pProgress = Bar_ProgressStart( stdout, Gia_ManPoNum(pAig) ); | |
| Gia_ManForEachCo( pAig, pObj, i ) | |
| { | |
| if ( Gia_ObjIsConst0(Gia_ObjFanin0(pObj)) ) | |
| { | |
| pObj->fMark0 = 0; | |
| pObj->fMark1 = 1; | |
| continue; | |
| } | |
| Bar_ProgressUpdate( pProgress, i, "SAT..." ); | |
| clk2 = Abc_Clock(); | |
| status = Cec_ManSatCheckNode( p, Gia_ObjChild0(pObj) ); | |
| pObj->fMark0 = (status == 0); | |
| pObj->fMark1 = (status == 1); | |
| if ( status == 1 && vIdsOrig ) | |
| { | |
| int iObj1 = Vec_IntEntry(vMiterPairs, 2*i); | |
| int iObj2 = Vec_IntEntry(vMiterPairs, 2*i+1); | |
| int OrigId1 = Vec_IntEntry(vIdsOrig, iObj1); | |
| int OrigId2 = Vec_IntEntry(vIdsOrig, iObj2); | |
| assert( OrigId1 >= 0 && OrigId2 >= 0 ); | |
| Vec_IntPushTwo( vEquivPairs, OrigId1, OrigId2 ); | |
| } | |
| /* | |
| if ( status == -1 ) | |
| { | |
| Gia_Man_t * pTemp = Gia_ManDupDfsCone( pAig, pObj ); | |
| Gia_AigerWrite( pTemp, "gia_hard.aig", 0, 0 ); | |
| Gia_ManStop( pTemp ); | |
| Abc_Print( 1, "Dumping hard cone into file \"%s\".\n", "gia_hard.aig" ); | |
| } | |
| */ | |
| if ( status != 0 ) | |
| continue; | |
| // save the pattern | |
| if ( pPat ) | |
| { | |
| abctime clk3 = Abc_Clock(); | |
| Cec_ManPatSavePattern( pPat, p, pObj ); | |
| pPat->timeTotalSave += Abc_Clock() - clk3; | |
| } | |
| // quit if one of them is solved | |
| if ( pPars->fCheckMiter ) | |
| break; | |
| } | |
| p->timeTotal = Abc_Clock() - clk; | |
| Bar_ProgressStop( pProgress ); | |
| if ( pPars->fVerbose ) | |
| Cec_ManSatPrintStats( p ); | |
| Cec_ManSatStop( p ); | |
| } | |
| /**Function************************************************************* | |
| Synopsis [Performs one round of solving for the POs of the AIG.] | |
| Description [Labels the nodes that have been proved (pObj->fMark1) | |
| and returns the set of satisfying assignments.] | |
| SideEffects [] | |
| SeeAlso [] | |
| ***********************************************************************/ | |
| int Cec_ManSatSolveExractPattern( Vec_Int_t * vCexStore, int iStart, Vec_Int_t * vPat ) | |
| { | |
| int k, nSize; | |
| Vec_IntClear( vPat ); | |
| // skip the output number | |
| iStart++; | |
| // get the number of items | |
| nSize = Vec_IntEntry( vCexStore, iStart++ ); | |
| if ( nSize <= 0 ) | |
| return iStart; | |
| // extract pattern | |
| for ( k = 0; k < nSize; k++ ) | |
| Vec_IntPush( vPat, Vec_IntEntry( vCexStore, iStart++ ) ); | |
| return iStart; | |
| } | |
| void Cec_ManSatSolveCSat( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars ) | |
| { | |
| Vec_Str_t * vStatus; | |
| Vec_Int_t * vPat = Vec_IntAlloc( 1000 ); | |
| Vec_Int_t * vCexStore = Cbs_ManSolveMiterNc( pAig, pPars->nBTLimit, &vStatus, 0 ); | |
| Gia_Obj_t * pObj; | |
| int i, status, iStart = 0; | |
| assert( Vec_StrSize(vStatus) == Gia_ManCoNum(pAig) ); | |
| // reset the manager | |
| if ( pPat ) | |
| { | |
| pPat->iStart = Vec_StrSize(pPat->vStorage); | |
| pPat->nPats = 0; | |
| pPat->nPatLits = 0; | |
| pPat->nPatLitsMin = 0; | |
| } | |
| Gia_ManForEachCo( pAig, pObj, i ) | |
| { | |
| status = (int)Vec_StrEntry(vStatus, i); | |
| pObj->fMark0 = (status == 0); | |
| pObj->fMark1 = (status == 1); | |
| if ( Vec_IntSize(vCexStore) > 0 && status != 1 ) | |
| iStart = Cec_ManSatSolveExractPattern( vCexStore, iStart, vPat ); | |
| if ( status != 0 ) | |
| continue; | |
| // save the pattern | |
| if ( pPat && Vec_IntSize(vPat) > 0 ) | |
| { | |
| abctime clk3 = Abc_Clock(); | |
| Cec_ManPatSavePatternCSat( pPat, vPat ); | |
| pPat->timeTotalSave += Abc_Clock() - clk3; | |
| } | |
| // quit if one of them is solved | |
| if ( pPars->fCheckMiter ) | |
| break; | |
| } | |
| assert( iStart == Vec_IntSize(vCexStore) ); | |
| Vec_IntFree( vPat ); | |
| Vec_StrFree( vStatus ); | |
| Vec_IntFree( vCexStore ); | |
| } | |
| /**Function************************************************************* | |
| Synopsis [Returns the pattern stored.] | |
| Description [] | |
| SideEffects [] | |
| SeeAlso [] | |
| ***********************************************************************/ | |
| Vec_Int_t * Cec_ManSatReadCex( Cec_ManSat_t * pSat ) | |
| { | |
| return pSat->vCex; | |
| } | |
| /**Function************************************************************* | |
| Synopsis [Save values in the cone of influence.] | |
| Description [] | |
| SideEffects [] | |
| SeeAlso [] | |
| ***********************************************************************/ | |
| void Cec_ManSatSolveSeq_rec( Cec_ManSat_t * pSat, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Ptr_t * vInfo, int iPat, int nRegs ) | |
| { | |
| if ( Gia_ObjIsTravIdCurrent(p, pObj) ) | |
| return; | |
| Gia_ObjSetTravIdCurrent(p, pObj); | |
| if ( Gia_ObjIsCi(pObj) ) | |
| { | |
| unsigned * pInfo = (unsigned *)Vec_PtrEntry( vInfo, nRegs + Gia_ObjCioId(pObj) ); | |
| if ( Cec_ObjSatVarValue( pSat, pObj ) != Abc_InfoHasBit( pInfo, iPat ) ) | |
| Abc_InfoXorBit( pInfo, iPat ); | |
| pSat->nCexLits++; | |
| // Vec_IntPush( pSat->vCex, Abc_Var2Lit( Gia_ObjCioId(pObj), !Cec_ObjSatVarValue(pSat, pObj) ) ); | |
| return; | |
| } | |
| assert( Gia_ObjIsAnd(pObj) ); | |
| Cec_ManSatSolveSeq_rec( pSat, p, Gia_ObjFanin0(pObj), vInfo, iPat, nRegs ); | |
| Cec_ManSatSolveSeq_rec( pSat, p, Gia_ObjFanin1(pObj), vInfo, iPat, nRegs ); | |
| } | |
| /**Function************************************************************* | |
| Synopsis [Performs one round of solving for the POs of the AIG.] | |
| Description [Labels the nodes that have been proved (pObj->fMark1) | |
| and returns the set of satisfying assignments.] | |
| SideEffects [] | |
| SeeAlso [] | |
| ***********************************************************************/ | |
| Vec_Str_t * Cec_ManSatSolveSeq( Vec_Ptr_t * vPatts, Gia_Man_t * pAig, Cec_ParSat_t * pPars, int nRegs, int * pnPats ) | |
| { | |
| Bar_Progress_t * pProgress = NULL; | |
| Vec_Str_t * vStatus; | |
| Cec_ManSat_t * p; | |
| Gia_Obj_t * pObj; | |
| int iPat = 0, nPatsInit, nPats; | |
| int i, status; | |
| abctime clk = Abc_Clock(); | |
| nPatsInit = nPats = 32 * Vec_PtrReadWordsSimInfo(vPatts); | |
| Gia_ManSetPhase( pAig ); | |
| Gia_ManLevelNum( pAig ); | |
| Gia_ManIncrementTravId( pAig ); | |
| p = Cec_ManSatCreate( pAig, pPars ); | |
| vStatus = Vec_StrAlloc( Gia_ManPoNum(pAig) ); | |
| pProgress = Bar_ProgressStart( stdout, Gia_ManPoNum(pAig) ); | |
| Gia_ManForEachCo( pAig, pObj, i ) | |
| { | |
| Bar_ProgressUpdate( pProgress, i, "SAT..." ); | |
| if ( Gia_ObjIsConst0(Gia_ObjFanin0(pObj)) ) | |
| { | |
| if ( Gia_ObjFaninC0(pObj) ) | |
| { | |
| // Abc_Print( 1, "Constant 1 output of SRM!!!\n" ); | |
| Vec_StrPush( vStatus, 0 ); | |
| } | |
| else | |
| { | |
| // Abc_Print( 1, "Constant 0 output of SRM!!!\n" ); | |
| Vec_StrPush( vStatus, 1 ); | |
| } | |
| continue; | |
| } | |
| status = Cec_ManSatCheckNode( p, Gia_ObjChild0(pObj) ); | |
| //Abc_Print( 1, "output %d status = %d\n", i, status ); | |
| Vec_StrPush( vStatus, (char)status ); | |
| if ( status != 0 ) | |
| continue; | |
| // resize storage | |
| if ( iPat == nPats ) | |
| { | |
| int nWords = Vec_PtrReadWordsSimInfo(vPatts); | |
| Vec_PtrReallocSimInfo( vPatts ); | |
| Vec_PtrCleanSimInfo( vPatts, nWords, 2*nWords ); | |
| nPats = 32 * Vec_PtrReadWordsSimInfo(vPatts); | |
| } | |
| if ( iPat % nPatsInit == 0 ) | |
| iPat++; | |
| // save the pattern | |
| Gia_ManIncrementTravId( pAig ); | |
| // Vec_IntClear( p->vCex ); | |
| Cec_ManSatSolveSeq_rec( p, pAig, Gia_ObjFanin0(pObj), vPatts, iPat++, nRegs ); | |
| // Gia_SatVerifyPattern( pAig, pObj, p->vCex, p->vVisits ); | |
| // Cec_ManSatAddToStore( p->vCexStore, p->vCex ); | |
| // if ( iPat == nPats ) | |
| // break; | |
| // quit if one of them is solved | |
| // if ( pPars->fFirstStop ) | |
| // break; | |
| // if ( iPat == 32 * 15 * 16 - 1 ) | |
| // break; | |
| } | |
| p->timeTotal = Abc_Clock() - clk; | |
| Bar_ProgressStop( pProgress ); | |
| if ( pPars->fVerbose ) | |
| Cec_ManSatPrintStats( p ); | |
| // Abc_Print( 1, "Total number of cex literals = %d. (Ave = %d)\n", p->nCexLits, p->nCexLits/p->nSatSat ); | |
| Cec_ManSatStop( p ); | |
| if ( pnPats ) | |
| *pnPats = iPat-1; | |
| return vStatus; | |
| } | |
| /**Function************************************************************* | |
| Synopsis [Save values in the cone of influence.] | |
| Description [] | |
| SideEffects [] | |
| SeeAlso [] | |
| ***********************************************************************/ | |
| void Cec_ManSatAddToStore( Vec_Int_t * vCexStore, Vec_Int_t * vCex, int Out ) | |
| { | |
| int i, Entry; | |
| Vec_IntPush( vCexStore, Out ); | |
| if ( vCex == NULL ) // timeout | |
| { | |
| Vec_IntPush( vCexStore, -1 ); | |
| return; | |
| } | |
| // write the counter-example | |
| Vec_IntPush( vCexStore, Vec_IntSize(vCex) ); | |
| Vec_IntForEachEntry( vCex, Entry, i ) | |
| Vec_IntPush( vCexStore, Entry ); | |
| } | |
| /**Function************************************************************* | |
| Synopsis [Save values in the cone of influence.] | |
| Description [] | |
| SideEffects [] | |
| SeeAlso [] | |
| ***********************************************************************/ | |
| void Cec_ManSatSolveMiter_rec( Cec_ManSat_t * pSat, Gia_Man_t * p, Gia_Obj_t * pObj ) | |
| { | |
| if ( Gia_ObjIsTravIdCurrent(p, pObj) ) | |
| return; | |
| Gia_ObjSetTravIdCurrent(p, pObj); | |
| if ( Gia_ObjIsCi(pObj) ) | |
| { | |
| pSat->nCexLits++; | |
| Vec_IntPush( pSat->vCex, Abc_Var2Lit( Gia_ObjCioId(pObj), !Cec_ObjSatVarValue(pSat, pObj) ) ); | |
| return; | |
| } | |
| assert( Gia_ObjIsAnd(pObj) ); | |
| Cec_ManSatSolveMiter_rec( pSat, p, Gia_ObjFanin0(pObj) ); | |
| Cec_ManSatSolveMiter_rec( pSat, p, Gia_ObjFanin1(pObj) ); | |
| } | |
| /**Function************************************************************* | |
| Synopsis [Save patterns.] | |
| Description [] | |
| SideEffects [] | |
| SeeAlso [] | |
| ***********************************************************************/ | |
| void Cec_ManSavePattern( Cec_ManSat_t * p, Gia_Obj_t * pObj1, Gia_Obj_t * pObj2 ) | |
| { | |
| Vec_IntClear( p->vCex ); | |
| Gia_ManIncrementTravId( p->pAig ); | |
| Cec_ManSatSolveMiter_rec( p, p->pAig, Gia_Regular(pObj1) ); | |
| if ( pObj2 ) | |
| Cec_ManSatSolveMiter_rec( p, p->pAig, Gia_Regular(pObj2) ); | |
| } | |
| /**Function************************************************************* | |
| Synopsis [Performs one round of solving for the POs of the AIG.] | |
| Description [Labels the nodes that have been proved (pObj->fMark1) | |
| and returns the set of satisfying assignments.] | |
| SideEffects [] | |
| SeeAlso [] | |
| ***********************************************************************/ | |
| Vec_Int_t * Cec_ManSatSolveMiter( Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_Str_t ** pvStatus ) | |
| { | |
| Bar_Progress_t * pProgress = NULL; | |
| Vec_Int_t * vCexStore; | |
| Vec_Str_t * vStatus; | |
| Cec_ManSat_t * p; | |
| Gia_Obj_t * pObj; | |
| int i, status; | |
| abctime clk = Abc_Clock(); | |
| // prepare AIG | |
| Gia_ManSetPhase( pAig ); | |
| Gia_ManLevelNum( pAig ); | |
| Gia_ManIncrementTravId( pAig ); | |
| // create resulting data-structures | |
| vStatus = Vec_StrAlloc( Gia_ManPoNum(pAig) ); | |
| vCexStore = Vec_IntAlloc( 10000 ); | |
| // perform solving | |
| p = Cec_ManSatCreate( pAig, pPars ); | |
| pProgress = Bar_ProgressStart( stdout, Gia_ManPoNum(pAig) ); | |
| Gia_ManForEachCo( pAig, pObj, i ) | |
| { | |
| Vec_IntClear( p->vCex ); | |
| Bar_ProgressUpdate( pProgress, i, "SAT..." ); | |
| if ( Gia_ObjIsConst0(Gia_ObjFanin0(pObj)) ) | |
| { | |
| if ( Gia_ObjFaninC0(pObj) ) | |
| { | |
| // Abc_Print( 1, "Constant 1 output of SRM!!!\n" ); | |
| Cec_ManSatAddToStore( vCexStore, p->vCex, i ); // trivial counter-example | |
| Vec_StrPush( vStatus, 0 ); | |
| } | |
| else | |
| { | |
| // Abc_Print( 1, "Constant 0 output of SRM!!!\n" ); | |
| Vec_StrPush( vStatus, 1 ); | |
| } | |
| continue; | |
| } | |
| status = Cec_ManSatCheckNode( p, Gia_ObjChild0(pObj) ); | |
| Vec_StrPush( vStatus, (char)status ); | |
| if ( status == -1 ) | |
| { | |
| Cec_ManSatAddToStore( vCexStore, NULL, i ); // timeout | |
| continue; | |
| } | |
| if ( status == 1 ) | |
| continue; | |
| assert( status == 0 ); | |
| // save the pattern | |
| // Gia_ManIncrementTravId( pAig ); | |
| // Cec_ManSatSolveMiter_rec( p, pAig, Gia_ObjFanin0(pObj) ); | |
| Cec_ManSavePattern( p, Gia_ObjFanin0(pObj), NULL ); | |
| // Gia_SatVerifyPattern( pAig, pObj, p->vCex, p->vVisits ); | |
| Cec_ManSatAddToStore( vCexStore, p->vCex, i ); | |
| } | |
| p->timeTotal = Abc_Clock() - clk; | |
| Bar_ProgressStop( pProgress ); | |
| // if ( pPars->fVerbose ) | |
| // Cec_ManSatPrintStats( p ); | |
| Cec_ManSatStop( p ); | |
| *pvStatus = vStatus; | |
| return vCexStore; | |
| } | |
| //////////////////////////////////////////////////////////////////////// | |
| /// END OF FILE /// | |
| //////////////////////////////////////////////////////////////////////// | |
| ABC_NAMESPACE_IMPL_END | |