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

Experiments with SAT sweeping.

This commit is contained in:
Alan Mishchenko 2017-04-11 21:06:42 -07:00
parent 0d53eece0a
commit 79584f5e20
3 changed files with 79 additions and 24 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

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

52
src/proof/cec/cecSynth.c
View File

@ -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 ///
////////////////////////////////////////////////////////////////////////

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

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