luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Experiments with SAT-based simulation.

This commit is contained in:
Alan Mishchenko 2018-01-25 00:09:27 -08:00
parent 066e8d1b17
commit e4cd0d60f1
8 changed files with 60 additions and 19 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
src/aig/gia/gia.h
View File

@ -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 );

45
src/aig/gia/giaCSat.c
View File

@ -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,12 @@ 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;
@ -943,8 +952,6 @@ int Cbs_ManSolve( Cbs_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pObj2 )
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 ( pObj2 )
Cbs_ManAssign( p, pObj2, 0, NULL, NULL );
if ( !Cbs_ManSolve_rec(p, 0) && !Cbs_ManCheckLimits(p) )
Cbs_ManSaveModel( p, p->vModel );
else
@ -956,7 +963,31 @@ 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;
}
int Cbs_ManSolve2( Cbs_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pObj2 )
{
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 ( pObj2 )
Cbs_ManAssign( p, pObj2, 0, NULL, NULL );
if ( !Cbs_ManSolve_rec(p, 0) && !Cbs_ManCheckLimits(p) )
Cbs_ManSaveModelAll( 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;
}
@ -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 );

4
src/aig/gia/giaSim.c
View File

@ -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 );
}

2
src/base/abci/abc.c
View File

@ -13050,7 +13050,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
// Cba_PrsReadBlifTest();
}
// Abc_NtkComputePaths( Abc_FrameReadNtk(pAbc) );
// Maj_ManExactSynthesisTest();
// Psl_FileTest();
return 0;
usage:
Abc_Print( -2, "usage: test [-CKDNM] [-aovwh] <file_name>\n" );

19
src/proof/cec/cecSat.c
View File

@ -278,26 +278,28 @@ void Cec2_AddClausesSuper( Gia_Man_t * p, Gia_Obj_t * pNode, Vec_Ptr_t * vSuper,
SeeAlso []
***********************************************************************/
void Cec2_CollectSuper_rec( Gia_Obj_t * pObj, Vec_Ptr_t * vSuper, int fFirst, int fUseMuxes )
void Cec2_CollectSuper_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Ptr_t * vSuper, int fFirst, int fUseMuxes )
{
//printf( "v%d ", Gia_ObjValue(pObj) );
// if the new node is complemented or a PI, another gate begins
if ( Gia_IsComplement(pObj) || Gia_ObjIsCi(pObj) ||
(!fFirst && Gia_ObjValue(pObj) > 1) ||
// (!fFirst && Gia_ObjValue(pObj) > 1) ||
(!fFirst && (p->pRefs ? Gia_ObjRefNum(p, pObj) : Gia_ObjValue(pObj)) > 1) ||
(fUseMuxes && pObj->fMark0) )
{
Vec_PtrPushUnique( vSuper, pObj );
return;
}
// go through the branches
Cec2_CollectSuper_rec( Gia_ObjChild0(pObj), vSuper, 0, fUseMuxes );
Cec2_CollectSuper_rec( Gia_ObjChild1(pObj), vSuper, 0, fUseMuxes );
Cec2_CollectSuper_rec( p, Gia_ObjChild0(pObj), vSuper, 0, fUseMuxes );
Cec2_CollectSuper_rec( p, Gia_ObjChild1(pObj), vSuper, 0, fUseMuxes );
}
void Cec2_CollectSuper( Gia_Obj_t * pObj, int fUseMuxes, Vec_Ptr_t * vSuper )
void Cec2_CollectSuper( Gia_Man_t * p, Gia_Obj_t * pObj, int fUseMuxes, Vec_Ptr_t * vSuper )
{
assert( !Gia_IsComplement(pObj) );
assert( !Gia_ObjIsCi(pObj) );
Vec_PtrClear( vSuper );
Cec2_CollectSuper_rec( pObj, vSuper, 1, fUseMuxes );
Cec2_CollectSuper_rec( p, pObj, vSuper, 1, fUseMuxes );
}
void Cec2_ObjAddToFrontier( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Ptr_t * vFrontier, satoko_t * pSat )
{
@ -360,10 +362,11 @@ int Gia_ObjGetCnfVar( Gia_Man_t * pGia, int iObj, Vec_Ptr_t * vFrontier, Vec_Ptr
}
else
{
Cec2_CollectSuper( pNode, fUseMuxes, vFanins );
Cec2_CollectSuper( pGia, pNode, fUseMuxes, vFanins );
Vec_PtrForEachEntry( Gia_Obj_t *, vFanins, pFanin, k )
Cec2_ObjAddToFrontier( pGia, Gia_Regular(pFanin), vFrontier, pSat );
Cec2_AddClausesSuper( pGia, pNode, vFanins, pSat );
Cec2_AddClausesSuper( pGia, pNode, vFanins, pSat );
//printf( "%d ", Vec_PtrSize(vFanins) );
}
assert( Vec_PtrSize(vFanins) > 1 );
}

1
src/sat/satoko/satoko.h
View File

@ -76,6 +76,7 @@ struct satoko_stats {
long n_decisions;
long n_propagations;
long n_propagations_all;
long n_inspects;
long n_conflicts;
long n_conflicts_all;

1
src/sat/satoko/solver.c
View File

@ -620,6 +620,7 @@ unsigned solver_propagate(solver_t *s)
watch_list_shrink(ws, j - watch_list_array(ws));
}
s->stats.n_propagations += n_propagations;
s->stats.n_propagations_all += n_propagations;
s->n_props_simplify -= n_propagations;
return conf_cref;
}

4
src/sat/satoko/solver_api.c
View File

@ -45,9 +45,11 @@ static inline int clause_is_satisfied(solver_t *s, struct clause *clause)
static inline void solver_clean_stats(solver_t *s)
{
int n_conflicts_all = s->stats.n_conflicts_all;
long n_conflicts_all = s->stats.n_conflicts_all;
long n_propagations_all = s->stats.n_propagations_all;
memset(&(s->stats), 0, sizeof(struct satoko_stats));
s->stats.n_conflicts_all = n_conflicts_all;
s->stats.n_propagations_all = n_propagations_all;
}
static inline void print_opts(solver_t *s)