diff options
-rw-r--r-- | src/proof/cec/cecSat.c | 49 | ||||
-rw-r--r-- | src/proof/cec/cecSynth.c | 52 | ||||
-rw-r--r-- | src/sat/satoko/solver.c | 2 |
3 files changed, 79 insertions, 24 deletions
diff --git a/src/proof/cec/cecSat.c b/src/proof/cec/cecSat.c index 025668d3..fc53d503 100644 --- a/src/proof/cec/cecSat.c +++ b/src/proof/cec/cecSat.c @@ -61,6 +61,7 @@ struct Cec2_Man_t_ Vec_Int_t * vObjSatPairs; // nodes Vec_Int_t * vCexTriples; // nodes // statistics + int nPatterns; int nSatSat; int nSatUnsat; int nSatUndec; @@ -100,7 +101,7 @@ void Cec2_SetDefaultParams( Cec2_Par_t * p ) p->nItersMax = 10; // max number of iterations p->nConfLimit = 1000; // conflict limit at a node p->fIsMiter = 0; // this is a miter - p->fUseCones = 0; // use logic cones + p->fUseCones = 0; // use logic cones p->fVeryVerbose = 0; // verbose stats p->fVerbose = 0; // verbose stats } @@ -487,18 +488,18 @@ void Cec2_ManSaveCis( Gia_Man_t * p ) Gia_ManForEachCiId( p, Id, i ) Vec_WrdPush( p->vSimsPi, Cec2_ObjSim(p, Id)[w] ); } -void Cec2_ManSimulate( Gia_Man_t * p, Vec_Int_t * vTriples, Cec2_Man_t * pMan ) +int Cec2_ManSimulate( Gia_Man_t * p, Vec_Int_t * vTriples, Cec2_Man_t * pMan ) { extern void Cec2_ManSimClassRefineOne( Gia_Man_t * p, int iRepr ); abctime clk = Abc_Clock(); Gia_Obj_t * pObj; - int i, iRepr, iObj, Entry; + int i, iRepr, iObj, Entry, Count = 0; //Cec2_ManSaveCis( p ); Gia_ManForEachAnd( p, pObj, i ) Cec2_ObjSimAnd( p, i ); pMan->timeSim += Abc_Clock() - clk; if ( p->pReprs == NULL ) - return; + return 0; if ( vTriples ) { Vec_IntForEachEntryTriple( vTriples, iRepr, iObj, Entry, i ) @@ -508,13 +509,17 @@ void Cec2_ManSimulate( Gia_Man_t * p, Vec_Int_t * vTriples, Cec2_Man_t * pMan ) int iPat = Abc_Lit2Var(Entry); int fPhase = Abc_LitIsCompl(Entry); if ( (fPhase ^ Abc_InfoHasBit((unsigned *)pSim0, iPat)) == Abc_InfoHasBit((unsigned *)pSim1, iPat) ) - printf( "ERROR: Pattern %d did not disprove pair %d and %d.\n", iPat, iRepr, iObj ); + { + //printf( "ERROR: Pattern %d did not disprove pair %d and %d.\n", iPat, iRepr, iObj ); + Count++; + } } } clk = Abc_Clock(); Gia_ManForEachClass0( p, i ) Cec2_ManSimClassRefineOne( p, i ); pMan->timeRefine += Abc_Clock() - clk; + return Count; } void Cec2_ManSimAlloc( Gia_Man_t * p, int nWords ) { @@ -677,6 +682,7 @@ Cec2_Man_t * Cec2_ManCreate( Gia_Man_t * pAig, Cec2_Par_t * pPars ) p->vSatVars = Vec_IntAlloc( 100 ); p->vObjSatPairs = Vec_IntAlloc( 100 ); p->vCexTriples = Vec_IntAlloc( 100 ); + p->pSat->opts.conf_limit = pPars->nConfLimit; // remember pointer to the solver in the AIG manager pAig->pData = p->pSat; return p; @@ -849,12 +855,13 @@ int Cec2_ManSweepNode( Cec2_Man_t * p, int iObj ) if ( status == SATOKO_SAT ) { p->nSatSat++; + p->nPatterns++; p->pAig->iPatsPi = (p->pAig->iPatsPi == 64 * p->pAig->nSimWords - 1) ? 1 : p->pAig->iPatsPi + 1; assert( p->pAig->iPatsPi > 0 && p->pAig->iPatsPi < 64 * p->pAig->nSimWords ); Vec_IntForEachEntryDouble( p->vObjSatPairs, IdAig, IdSat, i ) Cec2_ObjSimSetInputBit( p->pAig, IdAig, var_polarity(p->pSat, IdSat) == LIT_TRUE ); - RetValue = 0; p->timeSatSat += Abc_Clock() - clk; + RetValue = 0; } else if ( status == SATOKO_UNSAT ) { @@ -862,14 +869,15 @@ int Cec2_ManSweepNode( Cec2_Man_t * p, int iObj ) pObj->Value = Abc_LitNotCond( pRepr->Value, fCompl ); Gia_ObjSetProved( p->pAig, iObj ); p->timeSatUnsat += Abc_Clock() - clk; + RetValue = 1; } else { p->nSatUndec++; assert( status == SATOKO_UNDEC ); Gia_ObjSetFailed( p->pAig, iObj ); - assert( 0 ); p->timeSatUndec += Abc_Clock() - clk; + RetValue = 2; } if ( p->pPars->fUseCones ) return RetValue; @@ -895,6 +903,7 @@ int Cec2_ManPerformSweeping( Gia_Man_t * p, Cec2_Par_t * pPars, Gia_Man_t ** ppN int i, Iter, fDisproved = 1; // check if any output trivially fails under all-0 pattern + Gia_ManRandomW( 1 ); Gia_ManSetPhase( p ); if ( pPars->fIsMiter ) { @@ -902,7 +911,7 @@ int Cec2_ManPerformSweeping( Gia_Man_t * p, Cec2_Par_t * pPars, Gia_Man_t ** ppN if ( pObj->fPhase ) { p->pCexSeq = Cec2_ManDeriveCex( p, i, -1 ); - return 0; + goto finalize; } } @@ -911,7 +920,7 @@ int Cec2_ManPerformSweeping( Gia_Man_t * p, Cec2_Par_t * pPars, Gia_Man_t ** ppN Cec2_ManSimulateCis( p ); Cec2_ManSimulate( p, NULL, pMan ); if ( pPars->fIsMiter && !Cec2_ManSimulateCos(p) ) // cex detected - return 0; + goto finalize; Cec2_ManCreateClasses( p, pMan ); Cec2_ManPrintStats( p, pPars, pMan ); @@ -921,7 +930,7 @@ int Cec2_ManPerformSweeping( Gia_Man_t * p, Cec2_Par_t * pPars, Gia_Man_t ** ppN Cec2_ManSimulateCis( p ); Cec2_ManSimulate( p, NULL, pMan ); if ( pPars->fIsMiter && !Cec2_ManSimulateCos(p) ) // cex detected - return 0; + goto finalize; Cec2_ManPrintStats( p, pPars, pMan ); } // perform sweeping @@ -929,14 +938,12 @@ int Cec2_ManPerformSweeping( Gia_Man_t * p, Cec2_Par_t * pPars, Gia_Man_t ** ppN for ( Iter = 0; fDisproved && Iter < pPars->nItersMax; Iter++ ) { fDisproved = 0; + pMan->nPatterns = 0; Cec2_ManSimulateCis( p ); Vec_IntClear( pMan->vCexTriples ); Gia_ManForEachAnd( p, pObj, i ) { - pObj->fMark1 = Gia_ObjFanin0(pObj)->fMark1 || Gia_ObjFanin1(pObj)->fMark1; - if ( pObj->fMark1 ) // skip nodes in the TFO of a disproved one - continue; - if ( ~pObj->Value ) // skip swept nodes + if ( ~pObj->Value || Gia_ObjFailed(p, i) ) // skip swept nodes and failed nodes continue; if ( !~Gia_ObjFanin0(pObj)->Value || !~Gia_ObjFanin1(pObj)->Value ) // skip fanouts of non-swept nodes continue; @@ -952,7 +959,7 @@ int Cec2_ManPerformSweeping( Gia_Man_t * p, Cec2_Par_t * pPars, Gia_Man_t ** ppN } assert( Vec_IntSize(&pMan->pNew->vCopies) == Gia_ManObjNum(pMan->pNew) ); pRepr = Gia_ObjReprObj( p, i ); - if ( pRepr == NULL || pRepr->fMark1 || !~pRepr->Value ) + if ( pRepr == NULL || !~pRepr->Value ) continue; if ( Abc_Lit2Var(pObj->Value) == Abc_Lit2Var(pRepr->Value) ) { @@ -964,18 +971,13 @@ int Cec2_ManPerformSweeping( Gia_Man_t * p, Cec2_Par_t * pPars, Gia_Man_t ** ppN continue; pObj->Value = ~0; Vec_IntPushThree( pMan->vCexTriples, Gia_ObjId(p, pRepr), i, Abc_Var2Lit(p->iPatsPi, pObj->fPhase ^ pRepr->fPhase) ); - // mark nodes as disproved fDisproved = 1; - //if ( Iter > 5 ) - continue; - if ( Gia_ObjIsAnd(pRepr) ) - pRepr->fMark1 = 1; - pObj->fMark1 = 1; } if ( fDisproved ) { - //printf( "The number of pattern = %d.\n", p->iPatsPi ); - Cec2_ManSimulate( p, pMan->vCexTriples, pMan ); + int Fails = Cec2_ManSimulate( p, pMan->vCexTriples, pMan ); + if ( Fails && pPars->fVerbose ) + printf( "Failed to resimulate %d times with pattern = %d (total = %d).\n", Fails, pMan->nPatterns, pPars->nSimWords * 64 ); if ( pPars->fIsMiter && !Cec2_ManSimulateCos(p) ) // cex detected break; } @@ -993,6 +995,7 @@ int Cec2_ManPerformSweeping( Gia_Man_t * p, Cec2_Par_t * pPars, Gia_Man_t ** ppN (*ppNew)->pName = Abc_UtilStrsav( p->pName ); (*ppNew)->pSpec = Abc_UtilStrsav( p->pSpec ); } +finalize: Cec2_ManDestroy( pMan ); //Gia_ManEquivPrintClasses( p, 1, 0 ); return p->pCexSeq ? 0 : 1; diff --git a/src/proof/cec/cecSynth.c b/src/proof/cec/cecSynth.c index c00723bc..6e5fd221 100644 --- a/src/proof/cec/cecSynth.c +++ b/src/proof/cec/cecSynth.c @@ -372,6 +372,58 @@ int Cec_SequentialSynthesisPart( Gia_Man_t * p, Cec_ParSeq_t * pPars ) return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Gia_ManTestOnePair_rec( sat_solver * pSat, Gia_Man_t * p, int iObj, Vec_Int_t * vSatVar ) +{ + Gia_Obj_t * pObj; + int iVar, iVar0, iVar1; + if ( Vec_IntEntry(vSatVar, iObj) >= 0 ) + return Vec_IntEntry(vSatVar, iObj); + iVar = sat_solver_addvar(pSat); + Vec_IntWriteEntry( vSatVar, iObj, iVar ); + pObj = Gia_ManObj( p, iObj ); + if ( Gia_ObjIsAnd(pObj) ) + { + iVar0 = Gia_ManTestOnePair_rec( pSat, p, Gia_ObjFaninId0(pObj, iObj), vSatVar ); + iVar1 = Gia_ManTestOnePair_rec( pSat, p, Gia_ObjFaninId1(pObj, iObj), vSatVar ); + sat_solver_add_and( pSat, iVar, iVar0, iVar1, Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj), 0 ); + } + return iVar; +} +int Gia_ManTestOnePair( Gia_Man_t * p, int iObj1, int iObj2, int fPhase ) +{ + int Lits[2] = {1}, status; + sat_solver * pSat = sat_solver_new(); + Vec_Int_t * vSatVar = Vec_IntStartFull( Gia_ManObjNum(p) ); + Vec_IntWriteEntry( vSatVar, 0, sat_solver_addvar(pSat) ); + sat_solver_addclause( pSat, Lits, Lits + 1 ); + Gia_ManTestOnePair_rec( pSat, p, iObj1, vSatVar ); + Gia_ManTestOnePair_rec( pSat, p, iObj2, vSatVar ); + Lits[0] = Abc_Var2Lit( Vec_IntEntry(vSatVar, iObj1), 1 ); + Lits[1] = Abc_Var2Lit( Vec_IntEntry(vSatVar, iObj2), fPhase ); + status = sat_solver_solve( pSat, Lits, Lits + 2, 0, 0, 0, 0 ); + if ( status == l_False ) + { + Lits[0] = Abc_LitNot( Lits[0] ); + Lits[1] = Abc_LitNot( Lits[1] ); + status = sat_solver_solve( pSat, Lits, Lits + 2, 0, 0, 0, 0 ); + } + Vec_IntFree( vSatVar ); + sat_solver_delete( pSat ); + return status; +} + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/sat/satoko/solver.c b/src/sat/satoko/solver.c index 368ece2f..a72e39f7 100644 --- a/src/sat/satoko/solver.c +++ b/src/sat/satoko/solver.c @@ -639,7 +639,7 @@ char solver_search(solver_t *s) /* No conflict */ unsigned next_lit; - if (solver_rst(s)) { + if (solver_rst(s) || solver_check_limits(s) == 0) { b_queue_clean(s->bq_lbd); solver_cancel_until(s, 0); return SATOKO_UNDEC; |