From e4cd0d60f1d2ecf8563c22b51519f3da0125d3be Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 25 Jan 2018 00:09:27 -0800 Subject: Experiments with SAT-based simulation. --- src/aig/gia/gia.h | 3 ++- src/aig/gia/giaCSat.c | 43 +++++++++++++++++++++++++++++++++++++------ src/aig/gia/giaSim.c | 4 +++- 3 files changed, 42 insertions(+), 8 deletions(-) (limited to 'src/aig/gia') diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index fcdb3941..20648b39 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -1219,7 +1219,8 @@ extern Vec_Int_t * Cbs_ManSolveMiter( Gia_Man_t * pGia, int nConfs, Vec_ typedef struct Cbs_Man_t_ Cbs_Man_t; extern Cbs_Man_t * Cbs_ManAlloc( Gia_Man_t * pGia ); extern void Cbs_ManStop( Cbs_Man_t * p ); -extern int Cbs_ManSolve( Cbs_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pObj2 ); +extern int Cbs_ManSolve( Cbs_Man_t * p, Gia_Obj_t * pObj ); +extern int Cbs_ManSolve2( Cbs_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pObj2 ); extern Vec_Int_t * Cbs_ManSolveMiterNc( Gia_Man_t * pGia, int nConfs, Vec_Str_t ** pvStatus, int fVerbose ); extern void Cbs_ManSetConflictNum( Cbs_Man_t * p, int Num ); extern Vec_Int_t * Cbs_ReadModel( Cbs_Man_t * p ); diff --git a/src/aig/gia/giaCSat.c b/src/aig/gia/giaCSat.c index 31f32e30..baf1b418 100644 --- a/src/aig/gia/giaCSat.c +++ b/src/aig/gia/giaCSat.c @@ -246,6 +246,15 @@ static inline void Cbs_ManSaveModel( Cbs_Man_t * p, Vec_Int_t * vCex ) // Vec_IntPush( vCex, Abc_Var2Lit(Gia_ObjId(p->pAig,pVar), !Cbs_VarValue(pVar)) ); Vec_IntPush( vCex, Abc_Var2Lit(Gia_ObjCioId(pVar), !Cbs_VarValue(pVar)) ); } +static inline void Cbs_ManSaveModelAll( Cbs_Man_t * p, Vec_Int_t * vCex ) +{ + Gia_Obj_t * pVar; + int i; + Vec_IntClear( vCex ); + p->pProp.iHead = 0; + Cbs_QueForEachEntry( p->pProp, pVar, i ) + Vec_IntPush( vCex, Abc_Var2Lit(Gia_ObjId(p->pAig,pVar), !Cbs_VarValue(pVar)) ); +} /**Function************************************************************* @@ -929,12 +938,35 @@ int Cbs_ManSolve_rec( Cbs_Man_t * p, int Level ) Returns 1 if unsatisfiable, 0 if satisfiable, and -1 if undecided. The node may be complemented. ] - SideEffects [] + SideEffects [The two procedures differ in the CEX format.] SeeAlso [] ***********************************************************************/ -int Cbs_ManSolve( Cbs_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pObj2 ) +int Cbs_ManSolve( Cbs_Man_t * p, Gia_Obj_t * pObj ) +{ + int RetValue = 0; + s_Counter = 0; + assert( !p->pProp.iHead && !p->pProp.iTail ); + assert( !p->pJust.iHead && !p->pJust.iTail ); + assert( p->pClauses.iHead == 1 && p->pClauses.iTail == 1 ); + p->Pars.nBTThis = p->Pars.nJustThis = p->Pars.nBTThisNc = 0; + Cbs_ManAssign( p, pObj, 0, NULL, NULL ); + if ( !Cbs_ManSolve_rec(p, 0) && !Cbs_ManCheckLimits(p) ) + Cbs_ManSaveModel( p, p->vModel ); + else + RetValue = 1; + Cbs_ManCancelUntil( p, 0 ); + p->pJust.iHead = p->pJust.iTail = 0; + p->pClauses.iHead = p->pClauses.iTail = 1; + p->Pars.nBTTotal += p->Pars.nBTThis; + p->Pars.nJustTotal = Abc_MaxInt( p->Pars.nJustTotal, p->Pars.nJustThis ); + if ( Cbs_ManCheckLimits( p ) ) + RetValue = -1; +// printf( "%d ", s_Counter ); + return RetValue; +} +int Cbs_ManSolve2( Cbs_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pObj2 ) { int RetValue = 0; s_Counter = 0; @@ -946,7 +978,7 @@ int Cbs_ManSolve( Cbs_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pObj2 ) if ( pObj2 ) Cbs_ManAssign( p, pObj2, 0, NULL, NULL ); if ( !Cbs_ManSolve_rec(p, 0) && !Cbs_ManCheckLimits(p) ) - Cbs_ManSaveModel( p, p->vModel ); + Cbs_ManSaveModelAll( p, p->vModel ); else RetValue = 1; Cbs_ManCancelUntil( p, 0 ); @@ -956,7 +988,6 @@ int Cbs_ManSolve( Cbs_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pObj2 ) p->Pars.nJustTotal = Abc_MaxInt( p->Pars.nJustTotal, p->Pars.nJustThis ); if ( Cbs_ManCheckLimits( p ) ) RetValue = -1; - // printf( "%d ", s_Counter ); return RetValue; } @@ -1052,14 +1083,14 @@ Vec_Int_t * Cbs_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvSt clk = Abc_Clock(); p->Pars.fUseHighest = 1; p->Pars.fUseLowest = 0; - status = Cbs_ManSolve( p, Gia_ObjChild0(pRoot), NULL ); + status = Cbs_ManSolve( p, Gia_ObjChild0(pRoot) ); // printf( "\n" ); /* if ( status == -1 ) { p->Pars.fUseHighest = 0; p->Pars.fUseLowest = 1; - status = Cbs_ManSolve( p, Gia_ObjChild0(pRoot), NULL ); + status = Cbs_ManSolve( p, Gia_ObjChild0(pRoot) ); } */ Vec_StrPush( vStatus, (char)status ); diff --git a/src/aig/gia/giaSim.c b/src/aig/gia/giaSim.c index 228f6fb4..88e94156 100644 --- a/src/aig/gia/giaSim.c +++ b/src/aig/gia/giaSim.c @@ -1182,7 +1182,7 @@ void Gia_ManIncrSimSet( Gia_Man_t * p, Vec_Int_t * vObjLits ) if ( Gia_ObjIsAnd(Gia_ManObj(p, Abc_Lit2Var(iLit))) ) continue; //assert( Vec_IntEntry(p->vTimeStamps, Abc_Lit2Var(iLit)) == p->iTimeStamp-1 ); - //Vec_IntWriteEntry(p->vTimeStamps, Abc_Lit2Var(iLit), p->iTimeStamp); + Vec_IntWriteEntry(p->vTimeStamps, Abc_Lit2Var(iLit), p->iTimeStamp); if ( Abc_TtGetBit(pSims, p->iPatsPi) == Abc_LitIsCompl(iLit) ) Abc_TtXorBit(pSims, p->iPatsPi); } @@ -1208,6 +1208,7 @@ int Gia_ManIncrSimCheckOver( Gia_Man_t * p, int iLit0, int iLit1 ) Gia_ManIncrSimUpdate( p ); Gia_ManIncrSimCone_rec( p, Abc_Lit2Var(iLit0) ); Gia_ManIncrSimCone_rec( p, Abc_Lit2Var(iLit1) ); +// return 0; // disable return Gia_ManBuiltInSimCheckOver( p, iLit0, iLit1 ); } int Gia_ManIncrSimCheckEqual( Gia_Man_t * p, int iLit0, int iLit1 ) @@ -1216,6 +1217,7 @@ int Gia_ManIncrSimCheckEqual( Gia_Man_t * p, int iLit0, int iLit1 ) Gia_ManIncrSimUpdate( p ); Gia_ManIncrSimCone_rec( p, Abc_Lit2Var(iLit0) ); Gia_ManIncrSimCone_rec( p, Abc_Lit2Var(iLit1) ); +// return 1; // disable return Gia_ManBuiltInSimCheckEqual( p, iLit0, iLit1 ); } -- cgit v1.2.3