Skip to content

A
abc
Commit c4b64ed8 by Alan Mishchenko
Options

User-controlable SAT sweeper.

parent 59bc3cb9
Showing with 139 additions and 77 deletions
src/aig/gia/gia.h
...@@ -476,9 +476,11 @@ static inline int Gia_ManAppendAnd( Gia_Man_t * p, int iLit0, int iLit1 ) ...@@ -476,9 +476,11 @@ static inline int Gia_ManAppendAnd( Gia_Man_t * p, int iLit0, int iLit1 )
} }
if ( p->fSweeper ) if ( p->fSweeper )
{ {
Gia_ObjFanin0(pObj)->fMark0 = Gia_ObjFanin1(pObj)->fMark0 = 1; Gia_Obj_t * pFan0 = Gia_ObjFanin0(pObj);
pObj->fPhase = (Gia_ObjPhase(Gia_ObjFanin0(pObj)) ^ Gia_ObjFaninC0(pObj)) & Gia_Obj_t * pFan1 = Gia_ObjFanin1(pObj);
(Gia_ObjPhase(Gia_ObjFanin1(pObj)) ^ Gia_ObjFaninC1(pObj)); if ( pFan0->fMark0 ) pFan0->fMark1 = 1; else pFan0->fMark0 = 1;
if ( pFan1->fMark0 ) pFan1->fMark1 = 1; else pFan1->fMark0 = 1;
pObj->fPhase = (Gia_ObjPhase(pFan0) ^ Gia_ObjFaninC0(pObj)) & (Gia_ObjPhase(pFan1) ^ Gia_ObjFaninC1(pObj));
} }
return Gia_ObjId( p, pObj ) << 1; return Gia_ObjId( p, pObj ) << 1;
} }
......
src/aig/gia/giaSweeper.c
...@@ -87,20 +87,9 @@ struct Swp_Man_t_ ...@@ -87,20 +87,9 @@ struct Swp_Man_t_
clock_t timeSatUndec; clock_t timeSatUndec;
}; };
static inline int Swp_ManObj2Lit( Gia_Man_t * p, int Id ) static inline int Swp_ManObj2Lit( Swp_Man_t * p, int Id ) { return Vec_IntGetEntry( p->vId2Lit, Id ); }
{ static inline int Swp_ManLit2Lit( Swp_Man_t * p, int Lit ) { return Abc_Lit2LitL( Vec_IntArray(p->vId2Lit), Lit ); }
return Vec_IntGetEntry( ((Swp_Man_t *)p->pData)->vId2Lit, Id ); static inline void Swp_ManSetObj2Lit( Swp_Man_t * p, int Id, int Lit ) { Vec_IntSetEntry( p->vId2Lit, Id, Lit ); }
}
static inline void Swp_ManSetObj2Lit( Gia_Man_t * p, int Id, int Lit )
{
Vec_IntSetEntry( ((Swp_Man_t *)p->pData)->vId2Lit, Id, Lit );
}
static inline int Swp_ManLit2Lit( Gia_Man_t * p, int Lit )
{
return Abc_Lit2LitL( Vec_IntArray(((Swp_Man_t *)p->pData)->vId2Lit), Lit );
}
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS /// /// FUNCTION DEFINITIONS ///
...@@ -120,6 +109,7 @@ static inline int Swp_ManLit2Lit( Gia_Man_t * p, int Lit ) ...@@ -120,6 +109,7 @@ static inline int Swp_ManLit2Lit( Gia_Man_t * p, int Lit )
static inline Swp_Man_t * Swp_ManStart( Gia_Man_t * pGia ) static inline Swp_Man_t * Swp_ManStart( Gia_Man_t * pGia )
{ {
Swp_Man_t * p; Swp_Man_t * p;
int Lit;
p = ABC_CALLOC( Swp_Man_t, 1 ); p = ABC_CALLOC( Swp_Man_t, 1 );
p->pGia = pGia; p->pGia = pGia;
p->nConfMax = 1000; p->nConfMax = 1000;
...@@ -133,7 +123,8 @@ static inline Swp_Man_t * Swp_ManStart( Gia_Man_t * pGia ) ...@@ -133,7 +123,8 @@ static inline Swp_Man_t * Swp_ManStart( Gia_Man_t * pGia )
p->vCexSwp = Vec_IntAlloc( 100 ); p->vCexSwp = Vec_IntAlloc( 100 );
p->pSat = sat_solver_new(); p->pSat = sat_solver_new();
p->nSatVars = 1; p->nSatVars = 1;
Swp_ManSetObj2Lit( pGia, 0, Abc_Var2Lit(p->nSatVars++, 0) ); Swp_ManSetObj2Lit( p, 0, (Lit = Abc_Var2Lit(p->nSatVars++, 1)) );
sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
pGia->pData = p; pGia->pData = p;
return p; return p;
} }
...@@ -189,6 +180,8 @@ void Gia_SweeperSetRuntimeLimit( Gia_Man_t * p, int nSeconds ) ...@@ -189,6 +180,8 @@ void Gia_SweeperSetRuntimeLimit( Gia_Man_t * p, int nSeconds )
{ {
Swp_Man_t * pSwp = (Swp_Man_t *)p->pData; Swp_Man_t * pSwp = (Swp_Man_t *)p->pData;
pSwp->nTimeOut = nSeconds; pSwp->nTimeOut = nSeconds;
if ( nSeconds )
sat_solver_set_runtime_limit( pSwp->pSat, nSeconds * CLOCKS_PER_SEC + clock() );
} }
Vec_Int_t * Gia_SweeperGetCex( Gia_Man_t * p ) Vec_Int_t * Gia_SweeperGetCex( Gia_Man_t * p )
{ {
...@@ -214,7 +207,7 @@ int Gia_SweeperProbeCreate( Gia_Man_t * p, int iLit ) ...@@ -214,7 +207,7 @@ int Gia_SweeperProbeCreate( Gia_Man_t * p, int iLit )
int ProbeId = Vec_IntSize(pSwp->vProbes); int ProbeId = Vec_IntSize(pSwp->vProbes);
Vec_IntPush( pSwp->vProbes, iLit ); Vec_IntPush( pSwp->vProbes, iLit );
Vec_IntPush( pSwp->vProbRefs, 1 ); Vec_IntPush( pSwp->vProbRefs, 1 );
Vec_IntSetEntryFull( pSwp->vLit2Prob, iLit, ProbeId ); Vec_IntSetEntryFull( pSwp->vLit2Prob, iLit, ProbeId ); // consider hash table in the future
return ProbeId; return ProbeId;
} }
// if probe with this literal (iLit) exists, this procedure increments its reference counter and returns it. // if probe with this literal (iLit) exists, this procedure increments its reference counter and returns it.
...@@ -222,7 +215,7 @@ int Gia_SweeperProbeCreate( Gia_Man_t * p, int iLit ) ...@@ -222,7 +215,7 @@ int Gia_SweeperProbeCreate( Gia_Man_t * p, int iLit )
int Gia_SweeperProbeFind( Gia_Man_t * p, int iLit ) int Gia_SweeperProbeFind( Gia_Man_t * p, int iLit )
{ {
Swp_Man_t * pSwp = (Swp_Man_t *)p->pData; Swp_Man_t * pSwp = (Swp_Man_t *)p->pData;
if ( iLit >= Vec_IntSize(pSwp->vLit2Prob) || Vec_IntEntry(pSwp->vLit2Prob, iLit) >= 0 ) if ( iLit < Vec_IntSize(pSwp->vLit2Prob) && Vec_IntEntry(pSwp->vLit2Prob, iLit) >= 0 )
return Vec_IntEntry(pSwp->vLit2Prob, iLit); return Vec_IntEntry(pSwp->vLit2Prob, iLit);
return Gia_SweeperProbeCreate( p, iLit ); return Gia_SweeperProbeCreate( p, iLit );
} }
...@@ -231,11 +224,12 @@ void Gia_SweeperProbeDeref( Gia_Man_t * p, int ProbeId ) ...@@ -231,11 +224,12 @@ void Gia_SweeperProbeDeref( Gia_Man_t * p, int ProbeId )
{ {
Swp_Man_t * pSwp = (Swp_Man_t *)p->pData; Swp_Man_t * pSwp = (Swp_Man_t *)p->pData;
assert( Vec_IntEntry(pSwp->vProbRefs, ProbeId) > 0 ); assert( Vec_IntEntry(pSwp->vProbRefs, ProbeId) > 0 );
Vec_IntAddToEntry( pSwp->vProbRefs, ProbeId, -1 ); if ( Vec_IntAddToEntry( pSwp->vProbRefs, ProbeId, -1 ) == 0 )
if ( Vec_IntEntry(pSwp->vProbRefs, ProbeId) == 0 )
{ {
int iLit = Gia_SweeperProbeLit( p, ProbeId ); int iLit = Gia_SweeperProbeLit( p, ProbeId );
Vec_IntWriteEntry( pSwp->vLit2Prob, iLit, -1 ); Vec_IntWriteEntry( pSwp->vLit2Prob, iLit, -1 );
Vec_IntWriteEntry( pSwp->vProbes, ProbeId, 0 );
// TODO: recycle probe ID
} }
} }
// returns literal associated with the probe // returns literal associated with the probe
...@@ -269,11 +263,6 @@ int Gia_SweeperCondPop( Gia_Man_t * p ) ...@@ -269,11 +263,6 @@ int Gia_SweeperCondPop( Gia_Man_t * p )
Vec_IntPop( pSwp->vCondLits ); Vec_IntPop( pSwp->vCondLits );
return ProbId; return ProbId;
} }
// returns 1 if the set of conditions is UNSAT (0 if SAT; -1 if undecided)
int Gia_SweeperCondCheckUnsat( Gia_Man_t * p )
{
return 0;
}
/**Function************************************************************* /**Function*************************************************************
...@@ -299,7 +288,7 @@ static void Gia_ManExtract_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vOb ...@@ -299,7 +288,7 @@ static void Gia_ManExtract_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vOb
} }
Gia_Man_t * Gia_SweeperExtractUserLogic( Gia_Man_t * p, Vec_Int_t * vProbeIds, Vec_Ptr_t * vOutNames ) Gia_Man_t * Gia_SweeperExtractUserLogic( Gia_Man_t * p, Vec_Int_t * vProbeIds, Vec_Ptr_t * vOutNames )
{ {
Gia_Man_t * pNew; Gia_Man_t * pNew, * pTemp;
Gia_Obj_t * pObj; Gia_Obj_t * pObj;
Vec_Int_t * vObjIds; Vec_Int_t * vObjIds;
int i, ProbeId; int i, ProbeId;
...@@ -319,13 +308,19 @@ Gia_Man_t * Gia_SweeperExtractUserLogic( Gia_Man_t * p, Vec_Int_t * vProbeIds, V ...@@ -319,13 +308,19 @@ Gia_Man_t * Gia_SweeperExtractUserLogic( Gia_Man_t * p, Vec_Int_t * vProbeIds, V
Gia_ManForEachPi( p, pObj, i ) Gia_ManForEachPi( p, pObj, i )
pObj->Value = Gia_ManAppendCi(pNew); pObj->Value = Gia_ManAppendCi(pNew);
Gia_ManForEachObjVec( vObjIds, p, pObj, i ) Gia_ManForEachObjVec( vObjIds, p, pObj, i )
pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
Vec_IntFree( vObjIds ); Vec_IntFree( vObjIds );
Vec_IntForEachEntry( vProbeIds, ProbeId, i ) Vec_IntForEachEntry( vProbeIds, ProbeId, i )
{ {
pObj = Gia_Lit2Obj( p, Gia_SweeperProbeLit(p, ProbeId) ); pObj = Gia_Lit2Obj( p, Gia_SweeperProbeLit(p, ProbeId) );
Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(Gia_Regular(pObj)) ^ Gia_IsComplement(pObj) ); Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(Gia_Regular(pObj)) ^ Gia_IsComplement(pObj) );
} }
// duplicated if needed
if ( Gia_ManHasDangling(pNew) )
{
pNew = Gia_ManCleanup( pTemp = pNew );
Gia_ManStop( pTemp );
}
// copy names if present // copy names if present
if ( p->vNamesIn ) if ( p->vNamesIn )
pNew->vNamesIn = Vec_PtrDup( p->vNamesIn ); pNew->vNamesIn = Vec_PtrDup( p->vNamesIn );
...@@ -346,9 +341,8 @@ Gia_Man_t * Gia_SweeperExtractUserLogic( Gia_Man_t * p, Vec_Int_t * vProbeIds, V ...@@ -346,9 +341,8 @@ Gia_Man_t * Gia_SweeperExtractUserLogic( Gia_Man_t * p, Vec_Int_t * vProbeIds, V
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
static void Gia_ManAddClausesMux( Gia_Man_t * pGia, Gia_Obj_t * pNode ) static void Gia_ManAddClausesMux( Swp_Man_t * p, Gia_Obj_t * pNode )
{ {
Swp_Man_t * p = (Swp_Man_t *)pGia->pData;
Gia_Obj_t * pNodeI, * pNodeT, * pNodeE; Gia_Obj_t * pNodeI, * pNodeT, * pNodeE;
int pLits[4], LitF, LitI, LitT, LitE, RetValue; int pLits[4], LitF, LitI, LitT, LitE, RetValue;
assert( !Gia_IsComplement( pNode ) ); assert( !Gia_IsComplement( pNode ) );
...@@ -356,10 +350,10 @@ static void Gia_ManAddClausesMux( Gia_Man_t * pGia, Gia_Obj_t * pNode ) ...@@ -356,10 +350,10 @@ static void Gia_ManAddClausesMux( Gia_Man_t * pGia, Gia_Obj_t * pNode )
// get nodes (I = if, T = then, E = else) // get nodes (I = if, T = then, E = else)
pNodeI = Gia_ObjRecognizeMux( pNode, &pNodeT, &pNodeE ); pNodeI = Gia_ObjRecognizeMux( pNode, &pNodeT, &pNodeE );
// get the Litiable numbers // get the Litiable numbers
LitF = Swp_ManLit2Lit( pGia, Gia_Obj2Lit(pGia,pNode) ); LitF = Swp_ManLit2Lit( p, Gia_Obj2Lit(p->pGia,pNode) );
LitI = Swp_ManLit2Lit( pGia, Gia_Obj2Lit(pGia,pNodeI) ); LitI = Swp_ManLit2Lit( p, Gia_Obj2Lit(p->pGia,pNodeI) );
LitT = Swp_ManLit2Lit( pGia, Gia_Obj2Lit(pGia,pNodeT) ); LitT = Swp_ManLit2Lit( p, Gia_Obj2Lit(p->pGia,pNodeT) );
LitE = Swp_ManLit2Lit( pGia, Gia_Obj2Lit(pGia,pNodeE) ); LitE = Swp_ManLit2Lit( p, Gia_Obj2Lit(p->pGia,pNodeE) );
// f = ITE(i, t, e) // f = ITE(i, t, e)
...@@ -426,22 +420,23 @@ static void Gia_ManAddClausesMux( Gia_Man_t * pGia, Gia_Obj_t * pNode ) ...@@ -426,22 +420,23 @@ static void Gia_ManAddClausesMux( Gia_Man_t * pGia, Gia_Obj_t * pNode )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
static void Gia_ManAddClausesSuper( Gia_Man_t * pGia, Gia_Obj_t * pNode, Vec_Int_t * vSuper ) static void Gia_ManAddClausesSuper( Swp_Man_t * p, Gia_Obj_t * pNode, Vec_Int_t * vSuper )
{ {
Swp_Man_t * p = (Swp_Man_t *)pGia->pData;
int i, RetValue, Lit, LitNode, pLits[2]; int i, RetValue, Lit, LitNode, pLits[2];
assert( !Gia_IsComplement(pNode) ); assert( !Gia_IsComplement(pNode) );
assert( Gia_ObjIsAnd( pNode ) ); assert( Gia_ObjIsAnd( pNode ) );
// suppose AND-gate is A & B = C // suppose AND-gate is A & B = C
// add !A => !C or A + !C // add !A => !C or A + !C
LitNode = Swp_ManObj2Lit( pGia, Gia_ObjId(pGia, pNode) ); // add !B => !C or B + !C
LitNode = Swp_ManLit2Lit( p, Gia_Obj2Lit(p->pGia,pNode) );
Vec_IntForEachEntry( vSuper, Lit, i ) Vec_IntForEachEntry( vSuper, Lit, i )
{ {
pLits[0] = Abc_LitNot( LitNode ); pLits[0] = Swp_ManLit2Lit( p, Lit );
pLits[1] = Swp_ManLit2Lit( pGia, Lit ); pLits[1] = Abc_LitNot( LitNode );
Vec_IntWriteEntry( vSuper, i, Abc_LitNot(pLits[1]) );
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 ); RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
assert( RetValue ); assert( RetValue );
// update literals
Vec_IntWriteEntry( vSuper, i, Abc_LitNot(pLits[0]) );
} }
// add A & B => C or !A + !B + C // add A & B => C or !A + !B + C
Vec_IntPush( vSuper, LitNode ); Vec_IntPush( vSuper, LitNode );
...@@ -465,7 +460,7 @@ static void Gia_ManAddClausesSuper( Gia_Man_t * pGia, Gia_Obj_t * pNode, Vec_Int ...@@ -465,7 +460,7 @@ static void Gia_ManAddClausesSuper( Gia_Man_t * pGia, Gia_Obj_t * pNode, Vec_Int
static void Gia_ManCollectSuper_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSuper ) static void Gia_ManCollectSuper_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSuper )
{ {
// stop at complements, shared, PIs, and MUXes // stop at complements, shared, PIs, and MUXes
if ( Gia_IsComplement(pObj) || pObj->fMark0 || Gia_ObjIsCi(pObj) || Gia_ObjIsMuxType(pObj) ) if ( Gia_IsComplement(pObj) || pObj->fMark1 || Gia_ObjIsCi(pObj) || Gia_ObjIsMuxType(pObj) )
{ {
Vec_IntPushUnique( vSuper, Gia_ObjId(p, pObj) ); Vec_IntPushUnique( vSuper, Gia_ObjId(p, pObj) );
return; return;
...@@ -493,65 +488,83 @@ static void Gia_ManCollectSuper( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vS ...@@ -493,65 +488,83 @@ static void Gia_ManCollectSuper( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vS
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
static void Gia_ManObjAddToFrontier( Gia_Man_t * pGia, int Id, Vec_Int_t * vFront ) static void Gia_ManObjAddToFrontier( Swp_Man_t * p, int Id, Vec_Int_t * vFront )
{ {
Swp_Man_t * p = (Swp_Man_t *)pGia->pData;
Gia_Obj_t * pObj; Gia_Obj_t * pObj;
if ( Id == 0 ) if ( Id == 0 || Swp_ManObj2Lit(p, Id) )
return; return;
if ( Swp_ManObj2Lit(pGia, Id) ) pObj = Gia_ManObj( p->pGia, Id );
return; Swp_ManSetObj2Lit( p, Id, Abc_Var2Lit(p->nSatVars++, pObj->fPhase) );
pObj = Gia_ManObj( pGia, Id );
Swp_ManSetObj2Lit( pGia, Id, Abc_Var2Lit(p->nSatVars++, pObj->fPhase) );
sat_solver_setnvars( p->pSat, p->nSatVars + 100 ); sat_solver_setnvars( p->pSat, p->nSatVars + 100 );
if ( Gia_ObjIsAnd(pObj) ) if ( Gia_ObjIsAnd(pObj) )
Vec_IntPush( vFront, Id ); Vec_IntPush( vFront, Id );
} }
static void Gia_ManCnfNodeAddToSolver( Gia_Man_t * p, int NodeId ) static void Gia_ManCnfNodeAddToSolver( Swp_Man_t * p, int NodeId )
{ {
Vec_Int_t * vFront, * vFanins;
Gia_Obj_t * pNode; Gia_Obj_t * pNode;
int i, k, Id; int i, k, Id;
// quit if CNF is ready // quit if CNF is ready
if ( NodeId == 0 ) if ( NodeId == 0 || Swp_ManObj2Lit(p, NodeId) )
return;
if ( Swp_ManObj2Lit(p, NodeId) )
return; return;
// start the frontier // start the frontier
vFront = ((Swp_Man_t *)p->pData)->vFront; Vec_IntClear( p->vFront );
Vec_IntClear( vFront ); Gia_ManObjAddToFrontier( p, NodeId, p->vFront );
Gia_ManObjAddToFrontier( p, NodeId, vFront );
// explore nodes in the frontier // explore nodes in the frontier
Gia_ManForEachObjVec( vFront, p, pNode, i ) Gia_ManForEachObjVec( p->vFront, p->pGia, pNode, i )
{ {
vFanins = ((Swp_Man_t *)p->pData)->vFanins;
// create the supergate // create the supergate
assert( Swp_ManObj2Lit(p,Gia_ObjId(p, pNode)) ); assert( Swp_ManObj2Lit(p, Gia_ObjId(p->pGia, pNode)) );
if ( Gia_ObjIsMuxType(pNode) ) if ( Gia_ObjIsMuxType(pNode) )
{ {
Vec_IntClear( vFanins ); Vec_IntClear( p->vFanins );
Vec_IntPushUnique( vFanins, Gia_ObjFaninId0p( p, Gia_ObjFanin0(pNode) ) ); Vec_IntPushUnique( p->vFanins, Gia_ObjFaninId0p( p->pGia, Gia_ObjFanin0(pNode) ) );
Vec_IntPushUnique( vFanins, Gia_ObjFaninId0p( p, Gia_ObjFanin1(pNode) ) ); Vec_IntPushUnique( p->vFanins, Gia_ObjFaninId0p( p->pGia, Gia_ObjFanin1(pNode) ) );
Vec_IntPushUnique( vFanins, Gia_ObjFaninId1p( p, Gia_ObjFanin0(pNode) ) ); Vec_IntPushUnique( p->vFanins, Gia_ObjFaninId1p( p->pGia, Gia_ObjFanin0(pNode) ) );
Vec_IntPushUnique( vFanins, Gia_ObjFaninId1p( p, Gia_ObjFanin1(pNode) ) ); Vec_IntPushUnique( p->vFanins, Gia_ObjFaninId1p( p->pGia, Gia_ObjFanin1(pNode) ) );
Vec_IntForEachEntry( vFanins, Id, k ) Vec_IntForEachEntry( p->vFanins, Id, k )
Gia_ManObjAddToFrontier( p, Id, vFront ); Gia_ManObjAddToFrontier( p, Id, p->vFront );
Gia_ManAddClausesMux( p, pNode ); Gia_ManAddClausesMux( p, pNode );
} }
else else
{ {
Gia_ManCollectSuper( p, pNode, vFanins ); Gia_ManCollectSuper( p->pGia, pNode, p->vFanins );
Vec_IntForEachEntry( vFanins, Id, k ) Vec_IntForEachEntry( p->vFanins, Id, k )
Gia_ManObjAddToFrontier( p, Id, vFront ); Gia_ManObjAddToFrontier( p, Id, p->vFront );
Gia_ManAddClausesSuper( p, pNode, vFanins ); Gia_ManAddClausesSuper( p, pNode, p->vFanins );
} }
assert( Vec_IntSize(vFanins) > 1 ); assert( Vec_IntSize(p->vFanins) > 1 );
} }
} }
/**Function************************************************************* /**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static Vec_Int_t * Gia_ManGetCex( Gia_Man_t * pGia, Vec_Int_t * vId2Lit, sat_solver * pSat, Vec_Int_t * vCex )
{
Gia_Obj_t * pObj;
int i, LitSat, Value;
Vec_IntClear( vCex );
Gia_ManForEachPi( pGia, pObj, i )
{
LitSat = Vec_IntEntry( vId2Lit, Gia_ObjId(pGia, pObj) );
assert( LitSat > 0 );
Value = sat_solver_var_value(pSat, Abc_Lit2Var(LitSat)) ^ Abc_LitIsCompl(LitSat);
Vec_IntPush( vCex, Value );
}
return vCex;
}
/**Function*************************************************************
Synopsis [Runs equivalence test for probes.] Synopsis [Runs equivalence test for probes.]
Description [] Description []
...@@ -576,10 +589,11 @@ int Gia_SweeperCheckEquiv( Gia_Man_t * pGia, int Probe1, int Probe2 ) ...@@ -576,10 +589,11 @@ int Gia_SweeperCheckEquiv( Gia_Man_t * pGia, int Probe1, int Probe2 )
// if the literals are identical, the probes are equivalent // if the literals are identical, the probes are equivalent
if ( iLitOld == iLitNew ) if ( iLitOld == iLitNew )
return 1; return 1;
// if the literals are opposites, the probes are // if the literals are opposites, the probes are not equivalent
if ( Abc_LitRegular(iLitOld) == Abc_LitRegular(iLitNew) ) if ( Abc_LitRegular(iLitOld) == Abc_LitRegular(iLitNew) )
{ {
Vec_IntFill( p->vCexSwp, Gia_ManPiNum(pGia), 0 ); Vec_IntFill( p->vCexSwp, Gia_ManPiNum(pGia), 0 );
p->vCexUser = p->vCexSwp;
return 0; return 0;
} }
// order the literals // order the literals
...@@ -588,13 +602,13 @@ int Gia_SweeperCheckEquiv( Gia_Man_t * pGia, int Probe1, int Probe2 ) ...@@ -588,13 +602,13 @@ int Gia_SweeperCheckEquiv( Gia_Man_t * pGia, int Probe1, int Probe2 )
assert( iLitOld > iLitNew ); assert( iLitOld > iLitNew );
// if the nodes do not have SAT variables, allocate them // if the nodes do not have SAT variables, allocate them
Gia_ManCnfNodeAddToSolver( pGia, Abc_Lit2Var(iLitOld) ); Gia_ManCnfNodeAddToSolver( p, Abc_Lit2Var(iLitOld) );
Gia_ManCnfNodeAddToSolver( pGia, Abc_Lit2Var(iLitNew) ); Gia_ManCnfNodeAddToSolver( p, Abc_Lit2Var(iLitNew) );
sat_solver_compress( p->pSat ); sat_solver_compress( p->pSat );
// set the SAT literals // set the SAT literals
pLitsSat[0] = Swp_ManLit2Lit( pGia, iLitOld ); pLitsSat[0] = Swp_ManLit2Lit( p, iLitOld );
pLitsSat[1] = Swp_ManLit2Lit( pGia, iLitNew ); pLitsSat[1] = Swp_ManLit2Lit( p, iLitNew );
// solve under assumptions // solve under assumptions
// A = 1; B = 0 OR A = 1; B = 1 // A = 1; B = 0 OR A = 1; B = 1
...@@ -619,6 +633,7 @@ p->timeSatUnsat += clock() - clk; ...@@ -619,6 +633,7 @@ p->timeSatUnsat += clock() - clk;
} }
else if ( RetValue1 == l_True ) else if ( RetValue1 == l_True )
{ {
p->vCexUser = Gia_ManGetCex( p->pGia, p->vId2Lit, p->pSat, p->vCexSwp );
p->timeSatSat += clock() - clk; p->timeSatSat += clock() - clk;
p->nSatCallsSat++; p->nSatCallsSat++;
return 0; return 0;
...@@ -660,6 +675,7 @@ p->timeSatUnsat += clock() - clk; ...@@ -660,6 +675,7 @@ p->timeSatUnsat += clock() - clk;
} }
else if ( RetValue1 == l_True ) else if ( RetValue1 == l_True )
{ {
p->vCexUser = Gia_ManGetCex( p->pGia, p->vId2Lit, p->pSat, p->vCexSwp );
p->timeSatSat += clock() - clk; p->timeSatSat += clock() - clk;
p->nSatCallsSat++; p->nSatCallsSat++;
return 0; return 0;
...@@ -675,7 +691,51 @@ p->timeSatUndec += clock() - clk; ...@@ -675,7 +691,51 @@ p->timeSatUndec += clock() - clk;
return 1; return 1;
} }
/**Function*************************************************************
Synopsis [Returns 1 if the set of conditions is UNSAT (0 if SAT; -1 if undecided).]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_SweeperCondCheckUnsat( Gia_Man_t * pGia )
{
Swp_Man_t * p = (Swp_Man_t *)pGia->pData;
int RetValue;
clock_t clk;
p->nSatCalls++;
assert( p->pSat != NULL );
p->vCexUser = NULL;
clk = clock();
RetValue = sat_solver_solve( p->pSat, Vec_IntArray(p->vCondLits), Vec_IntArray(p->vCondLits) + Vec_IntSize(p->vCondLits),
(ABC_INT64_T)p->nConfMax, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
p->timeSat += clock() - clk;
if ( RetValue == l_False )
{
assert( Vec_IntSize(p->vCondLits) > 0 );
p->timeSatUnsat += clock() - clk;
p->nSatCallsUnsat++;
return 1;
}
else if ( RetValue == l_True )
{
p->vCexUser = Gia_ManGetCex( p->pGia, p->vId2Lit, p->pSat, p->vCexSwp );
p->timeSatSat += clock() - clk;
p->nSatCallsSat++;
return 0;
}
else // if ( RetValue1 == l_Undef )
{
p->timeSatUndec += clock() - clk;
p->nSatFails++;
return -1;
}
}
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// END OF FILE /// /// END OF FILE ///
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment