Commit 40bfe2fb authored by Alan Mishchenko's avatar Alan Mishchenko

Experiments with SAT sweeping.

parent 0b89fd38
......@@ -5415,6 +5415,10 @@ SOURCE=.\src\proof\cec\cecSatG.c
# End Source File
# Begin Source File
SOURCE=.\src\proof\cec\cecSatG2.c
# End Source File
# Begin Source File
SOURCE=.\src\proof\cec\cecSeq.c
# End Source File
# Begin Source File
......
......@@ -1069,9 +1069,11 @@ static inline void Gia_ClassUndoPair( Gia_Man_t * p, int i ) { a
#define Gia_ManForEachClassReverse( p, i ) \
for ( i = Gia_ManObjNum(p) - 1; i > 0; i-- ) if ( !Gia_ObjIsHead(p, i) ) {} else
#define Gia_ClassForEachObj( p, i, iObj ) \
for ( assert(Gia_ObjIsHead(p, i)), iObj = i; iObj > 0; iObj = Gia_ObjNext(p, iObj) )
for ( assert(Gia_ObjIsHead(p, i) && i), iObj = i; iObj > 0; iObj = Gia_ObjNext(p, iObj) )
#define Gia_ClassForEachObj1( p, i, iObj ) \
for ( assert(Gia_ObjIsHead(p, i)), iObj = Gia_ObjNext(p, i); iObj > 0; iObj = Gia_ObjNext(p, iObj) )
#define Gia_ClassForEachObjStart( p, i, iObj, Start ) \
for ( assert(Gia_ObjIsHead(p, i)), iObj = Gia_ObjNext(p, Start); iObj > 0; iObj = Gia_ObjNext(p, iObj) )
static inline int Gia_ObjFoffsetId( Gia_Man_t * p, int Id ) { return Vec_IntEntry( p->vFanout, Id ); }
......
......@@ -480,8 +480,10 @@ void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem )
}
CounterX -= Gia_ManCoNum(p);
nLits = Gia_ManCiNum(p) + Gia_ManAndNum(p) - Counter - CounterX;
Abc_Print( 1, "cst =%8d cls =%7d lit =%8d unused =%8d proof =%6d mem =%5.2f MB\n",
Counter0, Counter, nLits, CounterX, Proved, (Mem == 0.0) ? 8.0*Gia_ManObjNum(p)/(1<<20) : Mem );
// Abc_Print( 1, "cst =%8d cls =%7d lit =%8d unused =%8d proof =%6d mem =%5.2f MB\n",
// Counter0, Counter, nLits, CounterX, Proved, (Mem == 0.0) ? 8.0*Gia_ManObjNum(p)/(1<<20) : Mem );
Abc_Print( 1, "cst =%8d cls =%7d lit =%8d unused =%8d proof =%6d\n",
Counter0, Counter, nLits, CounterX, Proved );
assert( Gia_ManEquivCheckLits( p, nLits ) );
if ( fVerbose )
{
......
......@@ -36286,14 +36286,15 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern Gia_Man_t * Cec2_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars );
extern Gia_Man_t * Cec3_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars );
extern Gia_Man_t * Cec4_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars );
Cec_ParFra_t ParsFra, * pPars = &ParsFra;
Gia_Man_t * pTemp;
int c, fUseAlgo = 0, fUseAlgoG = 0;
int c, fUseAlgo = 0, fUseAlgoG = 0, fUseAlgoG2 = 0;
Cec_ManFraSetDefaultParams( pPars );
pPars->fSatSweeping = 1;
pPars->nItersMax = 1000000;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "WRILDCrmdckngwvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "WRILDCrmdckngxwvh" ) ) != EOF )
{
switch ( c )
{
......@@ -36384,6 +36385,9 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'g':
fUseAlgoG ^= 1;
break;
case 'x':
fUseAlgoG2 ^= 1;
break;
case 'w':
pPars->fVeryVerbose ^= 1;
break;
......@@ -36403,6 +36407,8 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
pTemp = Cec2_ManSimulateTest( pAbc->pGia, pPars );
else if ( fUseAlgoG )
pTemp = Cec3_ManSimulateTest( pAbc->pGia, pPars );
else if ( fUseAlgoG2 )
pTemp = Cec4_ManSimulateTest( pAbc->pGia, pPars );
else
pTemp = Cec_ManSatSweeping( pAbc->pGia, pPars, 0 );
Abc_FrameUpdateGia( pAbc, pTemp );
......@@ -348,6 +348,8 @@ Gia_Man_t * Cec_ManSatSweeping( Gia_Man_t * pAig, Cec_ParFra_t * pPars, int fSil
Cec_ManPat_t * pPat;
int i, fTimeOut = 0, nMatches = 0;
abctime clk, clk2, clkTotal = Abc_Clock();
if ( pPars->fVerbose )
printf( "Simulating %d words for %d rounds. SAT solving with %d conflicts.\n", pPars->nWords, pPars->nRounds, pPars->nBTLimit );
// duplicate AIG and transfer equivalence classes
Gia_ManRandom( 1 );
......@@ -519,6 +521,9 @@ p->timeSat += Abc_Clock() - clk;
}
}
finalize:
if ( pPars->fVerbose )
printf( "Performed %d SAT calls: P = %d D = %d F = %d\n",
p->nAllProvedS + p->nAllDisprovedS + p->nAllFailedS, p->nAllProvedS, p->nAllDisprovedS, p->nAllFailedS );
if ( p->pPars->fVerbose && p->pAig )
{
Abc_Print( 1, "NBeg = %d. NEnd = %d. (Gain = %6.2f %%). RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n",
......
......@@ -153,6 +153,9 @@ struct Cec_ManFra_t_
int nAllProved; // total number of proved nodes
int nAllDisproved; // total number of disproved nodes
int nAllFailed; // total number of failed nodes
int nAllProvedS; // total number of proved nodes
int nAllDisprovedS; // total number of disproved nodes
int nAllFailedS; // total number of failed nodes
// runtime stats
abctime timeSim; // unsat
abctime timePat; // unsat
......
/**CFile****************************************************************
FileName [cecSatG2.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Combinational equivalence checking.]
Synopsis [Detection of structural isomorphism.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: cecSatG2.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "aig/gia/gia.h"
#include "misc/util/utilTruth.h"
#include "sat/glucose/AbcGlucose.h"
#include "cec.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
// sweeping manager
typedef struct Cec4_Par_t_ Cec4_Par_t;
struct Cec4_Par_t_
{
int nSimWords; // simulation words
int nSimRounds; // simulation rounds
int nItersMax; // max number of iterations
int nConfLimit; // SAT solver conflict limit
int nSatVarMax; // the max number of SAT variables
int nCallsRecycle; // calls to perform before recycling SAT solver
int fIsMiter; // this is a miter
int fUseCones; // use logic cones
int fVeryVerbose; // verbose stats
int fVerbose; // verbose stats
};
// SAT solving manager
typedef struct Cec4_Man_t_ Cec4_Man_t;
struct Cec4_Man_t_
{
Cec4_Par_t * pPars; // parameters
Gia_Man_t * pAig; // user's AIG
Gia_Man_t * pNew; // internal AIG
// SAT solving
bmcg_sat_solver* pSat; // SAT solver
Vec_Ptr_t * vFrontier; // CNF construction
Vec_Ptr_t * vFanins; // CNF construction
Vec_Wrd_t * vSims; // CI simulation info
Vec_Int_t * vCexMin; // minimized CEX
Vec_Int_t * vClassUpdates; // updated equiv classes
Vec_Int_t * vCexStamps; // time stamps
int iLastConst; // last const node proved
// statistics
int nPatterns;
int nSatSat;
int nSatUnsat;
int nSatUndec;
int nCallsSince;
int nSimulates;
int nRecycles;
int nConflicts[2][3];
abctime timeSatSat0;
abctime timeSatUnsat0;
abctime timeSatSat;
abctime timeSatUnsat;
abctime timeSatUndec;
abctime timeSim;
abctime timeRefine;
abctime timeResimGlo;
abctime timeResimLoc;
abctime timeStart;
};
static inline int Cec4_ObjSatId( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_ObjCopy2Array(p, Gia_ObjId(p, pObj)); }
static inline int Cec4_ObjSetSatId( Gia_Man_t * p, Gia_Obj_t * pObj, int Num ) { assert(Cec4_ObjSatId(p, pObj) == -1); Gia_ObjSetCopy2Array(p, Gia_ObjId(p, pObj), Num); Vec_IntPush(&p->vSuppVars, Gia_ObjId(p, pObj)); if ( Gia_ObjIsCi(pObj) ) Vec_IntPushTwo(&p->vCopiesTwo, Gia_ObjId(p, pObj), Num); return Num; }
static inline void Cec4_ObjCleanSatId( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert(Cec4_ObjSatId(p, pObj) != -1); Gia_ObjSetCopy2Array(p, Gia_ObjId(p, pObj), -1); }
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Sets parameter defaults.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cec4_SetDefaultParams( Cec4_Par_t * p )
{
memset( p, 0, sizeof(Cec4_Par_t) );
p->nSimWords = 4; // simulation words
p->nSimRounds = 250; // simulation rounds
p->nItersMax = 10; // max number of iterations
p->nConfLimit = 1000; // conflict limit at a node
p->nSatVarMax = 1000; // the max number of SAT variables before recycling SAT solver
p->nCallsRecycle = 200; // calls to perform before recycling SAT solver
p->fIsMiter = 0; // this is a miter
p->fUseCones = 0; // use logic cones
p->fVeryVerbose = 0; // verbose stats
p->fVerbose = 0; // verbose stats
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Cec4_Man_t * Cec4_ManCreate( Gia_Man_t * pAig, Cec4_Par_t * pPars )
{
Cec4_Man_t * p;
Gia_Obj_t * pObj; int i;
//assert( Gia_ManRegNum(pAig) == 0 );
p = ABC_CALLOC( Cec4_Man_t, 1 );
memset( p, 0, sizeof(Cec4_Man_t) );
p->timeStart = Abc_Clock();
p->pPars = pPars;
p->pAig = pAig;
pAig->pData = p->pSat; // point AIG manager to the solver
// create new manager
p->pNew = Gia_ManStart( Gia_ManObjNum(pAig) );
Gia_ManFillValue( pAig );
Gia_ManConst0(pAig)->Value = 0;
Gia_ManForEachCi( pAig, pObj, i )
pObj->Value = Gia_ManAppendCi( p->pNew );
Gia_ManHashAlloc( p->pNew );
Vec_IntFill( &p->pNew->vCopies2, Gia_ManObjNum(pAig), -1 );
// SAT solving
p->pSat = bmcg_sat_solver_start();
p->vFrontier = Vec_PtrAlloc( 1000 );
p->vFanins = Vec_PtrAlloc( 100 );
p->vCexMin = Vec_IntAlloc( 100 );
p->vClassUpdates = Vec_IntAlloc( 100 );
p->vCexStamps = Vec_IntStart( Gia_ManObjNum(pAig) );
return p;
}
void Cec4_ManDestroy( Cec4_Man_t * p )
{
if ( p->pPars->fVerbose )
{
abctime timeTotal = Abc_Clock() - p->timeStart;
abctime timeSat = p->timeSatSat0 + p->timeSatSat + p->timeSatUnsat0 + p->timeSatUnsat + p->timeSatUndec;
abctime timeOther = timeTotal - timeSat - p->timeSim - p->timeRefine - p->timeResimLoc;// - p->timeResimGlo;
ABC_PRTP( "SAT solving ", timeSat, timeTotal );
ABC_PRTP( " sat(easy) ", p->timeSatSat0, timeTotal );
ABC_PRTP( " sat ", p->timeSatSat, timeTotal );
ABC_PRTP( " unsat(easy)", p->timeSatUnsat0, timeTotal );
ABC_PRTP( " unsat ", p->timeSatUnsat, timeTotal );
ABC_PRTP( " fail ", p->timeSatUndec, timeTotal );
ABC_PRTP( "Simulation ", p->timeSim, timeTotal );
ABC_PRTP( "Refinement ", p->timeRefine, timeTotal );
ABC_PRTP( "Resim global ", p->timeResimGlo, timeTotal );
ABC_PRTP( "Resim local ", p->timeResimLoc, timeTotal );
ABC_PRTP( "Other ", timeOther, timeTotal );
ABC_PRTP( "TOTAL ", timeTotal, timeTotal );
fflush( stdout );
}
Vec_WrdFreeP( &p->pAig->vSims );
Gia_ManCleanMark01( p->pAig );
bmcg_sat_solver_stop( p->pSat );
Gia_ManStopP( &p->pNew );
Vec_PtrFreeP( &p->vFrontier );
Vec_PtrFreeP( &p->vFanins );
Vec_IntFreeP( &p->vCexMin );
Vec_IntFreeP( &p->vClassUpdates );
Vec_IntFreeP( &p->vCexStamps );
ABC_FREE( p );
}
/**Function*************************************************************
Synopsis [Adds clauses to the solver.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cec4_AddClausesMux( Gia_Man_t * p, Gia_Obj_t * pNode, bmcg_sat_solver * pSat )
{
int fPolarFlip = 0;
Gia_Obj_t * pNodeI, * pNodeT, * pNodeE;
int pLits[4], RetValue, VarF, VarI, VarT, VarE, fCompT, fCompE;
assert( !Gia_IsComplement( pNode ) );
assert( pNode->fMark0 );
// get nodes (I = if, T = then, E = else)
pNodeI = Gia_ObjRecognizeMux( pNode, &pNodeT, &pNodeE );
// get the variable numbers
VarF = Cec4_ObjSatId(p, pNode);
VarI = Cec4_ObjSatId(p, pNodeI);
VarT = Cec4_ObjSatId(p, Gia_Regular(pNodeT));
VarE = Cec4_ObjSatId(p, Gia_Regular(pNodeE));
// get the complementation flags
fCompT = Gia_IsComplement(pNodeT);
fCompE = Gia_IsComplement(pNodeE);
// f = ITE(i, t, e)
// i' + t' + f
// i' + t + f'
// i + e' + f
// i + e + f'
// create four clauses
pLits[0] = Abc_Var2Lit(VarI, 1);
pLits[1] = Abc_Var2Lit(VarT, 1^fCompT);
pLits[2] = Abc_Var2Lit(VarF, 0);
if ( fPolarFlip )
{
if ( pNodeI->fPhase ) pLits[0] = Abc_LitNot( pLits[0] );
if ( Gia_Regular(pNodeT)->fPhase ) pLits[1] = Abc_LitNot( pLits[1] );
if ( pNode->fPhase ) pLits[2] = Abc_LitNot( pLits[2] );
}
RetValue = bmcg_sat_solver_addclause( pSat, pLits, 3 );
assert( RetValue );
pLits[0] = Abc_Var2Lit(VarI, 1);
pLits[1] = Abc_Var2Lit(VarT, 0^fCompT);
pLits[2] = Abc_Var2Lit(VarF, 1);
if ( fPolarFlip )
{
if ( pNodeI->fPhase ) pLits[0] = Abc_LitNot( pLits[0] );
if ( Gia_Regular(pNodeT)->fPhase ) pLits[1] = Abc_LitNot( pLits[1] );
if ( pNode->fPhase ) pLits[2] = Abc_LitNot( pLits[2] );
}
RetValue = bmcg_sat_solver_addclause( pSat, pLits, 3 );
assert( RetValue );
pLits[0] = Abc_Var2Lit(VarI, 0);
pLits[1] = Abc_Var2Lit(VarE, 1^fCompE);
pLits[2] = Abc_Var2Lit(VarF, 0);
if ( fPolarFlip )
{
if ( pNodeI->fPhase ) pLits[0] = Abc_LitNot( pLits[0] );
if ( Gia_Regular(pNodeE)->fPhase ) pLits[1] = Abc_LitNot( pLits[1] );
if ( pNode->fPhase ) pLits[2] = Abc_LitNot( pLits[2] );
}
RetValue = bmcg_sat_solver_addclause( pSat, pLits, 3 );
assert( RetValue );
pLits[0] = Abc_Var2Lit(VarI, 0);
pLits[1] = Abc_Var2Lit(VarE, 0^fCompE);
pLits[2] = Abc_Var2Lit(VarF, 1);
if ( fPolarFlip )
{
if ( pNodeI->fPhase ) pLits[0] = Abc_LitNot( pLits[0] );
if ( Gia_Regular(pNodeE)->fPhase ) pLits[1] = Abc_LitNot( pLits[1] );
if ( pNode->fPhase ) pLits[2] = Abc_LitNot( pLits[2] );
}
RetValue = bmcg_sat_solver_addclause( pSat, pLits, 3 );
assert( RetValue );
// two additional clauses
// t' & e' -> f'
// t & e -> f
// t + e + f'
// t' + e' + f
if ( VarT == VarE )
{
// assert( fCompT == !fCompE );
return;
}
pLits[0] = Abc_Var2Lit(VarT, 0^fCompT);
pLits[1] = Abc_Var2Lit(VarE, 0^fCompE);
pLits[2] = Abc_Var2Lit(VarF, 1);
if ( fPolarFlip )
{
if ( Gia_Regular(pNodeT)->fPhase ) pLits[0] = Abc_LitNot( pLits[0] );
if ( Gia_Regular(pNodeE)->fPhase ) pLits[1] = Abc_LitNot( pLits[1] );
if ( pNode->fPhase ) pLits[2] = Abc_LitNot( pLits[2] );
}
RetValue = bmcg_sat_solver_addclause( pSat, pLits, 3 );
assert( RetValue );
pLits[0] = Abc_Var2Lit(VarT, 1^fCompT);
pLits[1] = Abc_Var2Lit(VarE, 1^fCompE);
pLits[2] = Abc_Var2Lit(VarF, 0);
if ( fPolarFlip )
{
if ( Gia_Regular(pNodeT)->fPhase ) pLits[0] = Abc_LitNot( pLits[0] );
if ( Gia_Regular(pNodeE)->fPhase ) pLits[1] = Abc_LitNot( pLits[1] );
if ( pNode->fPhase ) pLits[2] = Abc_LitNot( pLits[2] );
}
RetValue = bmcg_sat_solver_addclause( pSat, pLits, 3 );
assert( RetValue );
}
void Cec4_AddClausesSuper( Gia_Man_t * p, Gia_Obj_t * pNode, Vec_Ptr_t * vSuper, bmcg_sat_solver * pSat )
{
int fPolarFlip = 0;
Gia_Obj_t * pFanin;
int * pLits, nLits, RetValue, i;
assert( !Gia_IsComplement(pNode) );
assert( Gia_ObjIsAnd( pNode ) );
// create storage for literals
nLits = Vec_PtrSize(vSuper) + 1;
pLits = ABC_ALLOC( int, nLits );
// suppose AND-gate is A & B = C
// add !A => !C or A + !C
Vec_PtrForEachEntry( Gia_Obj_t *, vSuper, pFanin, i )
{
pLits[0] = Abc_Var2Lit(Cec4_ObjSatId(p, Gia_Regular(pFanin)), Gia_IsComplement(pFanin));
pLits[1] = Abc_Var2Lit(Cec4_ObjSatId(p, pNode), 1);
if ( fPolarFlip )
{
if ( Gia_Regular(pFanin)->fPhase ) pLits[0] = Abc_LitNot( pLits[0] );
if ( pNode->fPhase ) pLits[1] = Abc_LitNot( pLits[1] );
}
RetValue = bmcg_sat_solver_addclause( pSat, pLits, 2 );
assert( RetValue );
}
// add A & B => C or !A + !B + C
Vec_PtrForEachEntry( Gia_Obj_t *, vSuper, pFanin, i )
{
pLits[i] = Abc_Var2Lit(Cec4_ObjSatId(p, Gia_Regular(pFanin)), !Gia_IsComplement(pFanin));
if ( fPolarFlip )
{
if ( Gia_Regular(pFanin)->fPhase ) pLits[i] = Abc_LitNot( pLits[i] );
}
}
pLits[nLits-1] = Abc_Var2Lit(Cec4_ObjSatId(p, pNode), 0);
if ( fPolarFlip )
{
if ( pNode->fPhase ) pLits[nLits-1] = Abc_LitNot( pLits[nLits-1] );
}
RetValue = bmcg_sat_solver_addclause( pSat, pLits, nLits );
assert( RetValue );
ABC_FREE( pLits );
}
/**Function*************************************************************
Synopsis [Adds clauses and returns CNF variable of the node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cec4_CollectSuper_rec( Gia_Obj_t * pObj, Vec_Ptr_t * vSuper, int fFirst, int fUseMuxes )
{
// if the new node is complemented or a PI, another gate begins
if ( Gia_IsComplement(pObj) || Gia_ObjIsCi(pObj) ||
(!fFirst && Gia_ObjValue(pObj) > 1) ||
(fUseMuxes && pObj->fMark0) )
{
Vec_PtrPushUnique( vSuper, pObj );
return;
}
// go through the branches
Cec4_CollectSuper_rec( Gia_ObjChild0(pObj), vSuper, 0, fUseMuxes );
Cec4_CollectSuper_rec( Gia_ObjChild1(pObj), vSuper, 0, fUseMuxes );
}
void Cec4_CollectSuper( Gia_Obj_t * pObj, int fUseMuxes, Vec_Ptr_t * vSuper )
{
assert( !Gia_IsComplement(pObj) );
assert( !Gia_ObjIsCi(pObj) );
Vec_PtrClear( vSuper );
Cec4_CollectSuper_rec( pObj, vSuper, 1, fUseMuxes );
}
void Cec4_ObjAddToFrontier( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Ptr_t * vFrontier, bmcg_sat_solver * pSat )
{
assert( !Gia_IsComplement(pObj) );
assert( !Gia_ObjIsConst0(pObj) );
if ( Cec4_ObjSatId(p, pObj) >= 0 )
return;
assert( Cec4_ObjSatId(p, pObj) == -1 );
Cec4_ObjSetSatId( p, pObj, bmcg_sat_solver_addvar(pSat) );
if ( Gia_ObjIsAnd(pObj) )
Vec_PtrPush( vFrontier, pObj );
}
int Cec4_ObjGetCnfVar( Cec4_Man_t * p, int iObj )
{
int fUseAnd2 = 1; // enable simple CNF
int fUseMuxes = 1; // enable MUXes when using complex CNF
Gia_Obj_t * pNode, * pFanin;
Gia_Obj_t * pObj = Gia_ManObj(p->pNew, iObj);
int i, k;
// quit if CNF is ready
if ( Cec4_ObjSatId(p->pNew,pObj) >= 0 )
return Cec4_ObjSatId(p->pNew,pObj);
assert( iObj > 0 );
if ( Gia_ObjIsCi(pObj) )
return Cec4_ObjSetSatId( p->pNew, pObj, bmcg_sat_solver_addvar(p->pSat) );
assert( Gia_ObjIsAnd(pObj) );
if ( fUseAnd2 )
{
Cec4_ObjGetCnfVar( p, Gia_ObjFaninId0(pObj, iObj) );
Cec4_ObjGetCnfVar( p, Gia_ObjFaninId1(pObj, iObj) );
Vec_PtrClear( p->vFanins );
Vec_PtrPush( p->vFanins, Gia_ObjChild0(pObj) );
Vec_PtrPush( p->vFanins, Gia_ObjChild1(pObj) );
Cec4_ObjSetSatId( p->pNew, pObj, bmcg_sat_solver_addvar(p->pSat) );
Cec4_AddClausesSuper( p->pNew, pObj, p->vFanins, p->pSat );
return Cec4_ObjSatId( p->pNew, pObj );
}
// start the frontier
Vec_PtrClear( p->vFrontier );
Cec4_ObjAddToFrontier( p->pNew, pObj, p->vFrontier, p->pSat );
// explore nodes in the frontier
Vec_PtrForEachEntry( Gia_Obj_t *, p->vFrontier, pNode, i )
{
// create the supergate
assert( Cec4_ObjSatId(p->pNew,pNode) >= 0 );
if ( fUseMuxes && pNode->fMark0 )
{
Vec_PtrClear( p->vFanins );
Vec_PtrPushUnique( p->vFanins, Gia_ObjFanin0( Gia_ObjFanin0(pNode) ) );
Vec_PtrPushUnique( p->vFanins, Gia_ObjFanin0( Gia_ObjFanin1(pNode) ) );
Vec_PtrPushUnique( p->vFanins, Gia_ObjFanin1( Gia_ObjFanin0(pNode) ) );
Vec_PtrPushUnique( p->vFanins, Gia_ObjFanin1( Gia_ObjFanin1(pNode) ) );
Vec_PtrForEachEntry( Gia_Obj_t *, p->vFanins, pFanin, k )
Cec4_ObjAddToFrontier( p->pNew, Gia_Regular(pFanin), p->vFrontier, p->pSat );
Cec4_AddClausesMux( p->pNew, pNode, p->pSat );
}
else
{
Cec4_CollectSuper( pNode, fUseMuxes, p->vFanins );
Vec_PtrForEachEntry( Gia_Obj_t *, p->vFanins, pFanin, k )
Cec4_ObjAddToFrontier( p->pNew, Gia_Regular(pFanin), p->vFrontier, p->pSat );
Cec4_AddClausesSuper( p->pNew, pNode, p->vFanins, p->pSat );
}
assert( Vec_PtrSize(p->vFanins) > 1 );
}
return Cec4_ObjSatId(p->pNew,pObj);
}
/**Function*************************************************************
Synopsis [Internal simulation APIs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline word * Cec4_ObjSim( Gia_Man_t * p, int iObj )
{
return Vec_WrdEntryP( p->vSims, p->nSimWords * iObj );
}
static inline void Cec4_ObjSimSetInputBit( Gia_Man_t * p, int iObj, int Bit )
{
word * pSim = Cec4_ObjSim( p, iObj );
if ( Abc_InfoHasBit( (unsigned*)pSim, p->iPatsPi ) != Bit )
Abc_InfoXorBit( (unsigned*)pSim, p->iPatsPi );
}
static inline void Cec4_ObjSimRo( Gia_Man_t * p, int iObj )
{
int w;
word * pSimRo = Cec4_ObjSim( p, iObj );
word * pSimRi = Cec4_ObjSim( p, Gia_ObjRoToRiId(p, iObj) );
for ( w = 0; w < p->nSimWords; w++ )
pSimRo[w] = pSimRi[w];
}
static inline void Cec4_ObjSimCo( Gia_Man_t * p, int iObj )
{
int w;
Gia_Obj_t * pObj = Gia_ManObj( p, iObj );
word * pSimCo = Cec4_ObjSim( p, iObj );
word * pSimDri = Cec4_ObjSim( p, Gia_ObjFaninId0(pObj, iObj) );
if ( Gia_ObjFaninC0(pObj) )
for ( w = 0; w < p->nSimWords; w++ )
pSimCo[w] = ~pSimDri[w];
else
for ( w = 0; w < p->nSimWords; w++ )
pSimCo[w] = pSimDri[w];
}
static inline void Cec4_ObjSimAnd( Gia_Man_t * p, int iObj )
{
int w;
Gia_Obj_t * pObj = Gia_ManObj( p, iObj );
word * pSim = Cec4_ObjSim( p, iObj );
word * pSim0 = Cec4_ObjSim( p, Gia_ObjFaninId0(pObj, iObj) );
word * pSim1 = Cec4_ObjSim( p, Gia_ObjFaninId1(pObj, iObj) );
if ( Gia_ObjFaninC0(pObj) && Gia_ObjFaninC1(pObj) )
for ( w = 0; w < p->nSimWords; w++ )
pSim[w] = ~pSim0[w] & ~pSim1[w];
else if ( Gia_ObjFaninC0(pObj) && !Gia_ObjFaninC1(pObj) )
for ( w = 0; w < p->nSimWords; w++ )
pSim[w] = ~pSim0[w] & pSim1[w];
else if ( !Gia_ObjFaninC0(pObj) && Gia_ObjFaninC1(pObj) )
for ( w = 0; w < p->nSimWords; w++ )
pSim[w] = pSim0[w] & ~pSim1[w];
else
for ( w = 0; w < p->nSimWords; w++ )
pSim[w] = pSim0[w] & pSim1[w];
}
static inline int Cec4_ObjSimEqual( Gia_Man_t * p, int iObj0, int iObj1 )
{
int w;
word * pSim0 = Cec4_ObjSim( p, iObj0 );
word * pSim1 = Cec4_ObjSim( p, iObj1 );
if ( (pSim0[0] & 1) == (pSim1[0] & 1) )
{
for ( w = 0; w < p->nSimWords; w++ )
if ( pSim0[w] != pSim1[w] )
return 0;
return 1;
}
else
{
for ( w = 0; w < p->nSimWords; w++ )
if ( pSim0[w] != ~pSim1[w] )
return 0;
return 1;
}
}
static inline void Cec4_ObjSimCi( Gia_Man_t * p, int iObj )
{
int w;
word * pSim = Cec4_ObjSim( p, iObj );
for ( w = 0; w < p->nSimWords; w++ )
pSim[w] = Gia_ManRandomW( 0 );
pSim[0] <<= 1;
}
static inline void Cec4_ObjClearSimCi( Gia_Man_t * p, int iObj )
{
int w;
word * pSim = Cec4_ObjSim( p, iObj );
for ( w = 0; w < p->nSimWords; w++ )
pSim[w] = 0;
}
void Cec4_ManSimulateCis( Gia_Man_t * p )
{
int i, Id;
Gia_ManForEachCiId( p, Id, i )
Cec4_ObjSimCi( p, Id );
p->iPatsPi = 0;
}
void Cec4_ManClearCis( Gia_Man_t * p )
{
int i, Id;
Gia_ManForEachCiId( p, Id, i )
Cec4_ObjClearSimCi( p, Id );
p->iPatsPi = 0;
}
Abc_Cex_t * Cec4_ManDeriveCex( Gia_Man_t * p, int iOut, int iPat )
{
Abc_Cex_t * pCex;
int i, Id;
pCex = Abc_CexAlloc( 0, Gia_ManCiNum(p), 1 );
pCex->iPo = iOut;
if ( iPat == -1 )
return pCex;
Gia_ManForEachCiId( p, Id, i )
if ( Abc_InfoHasBit((unsigned *)Cec4_ObjSim(p, Id), iPat) )
Abc_InfoSetBit( pCex->pData, i );
return pCex;
}
int Cec4_ManSimulateCos( Gia_Man_t * p )
{
int i, Id;
// check outputs and generate CEX if they fail
Gia_ManForEachCoId( p, Id, i )
{
Cec4_ObjSimCo( p, Id );
if ( Cec4_ObjSimEqual(p, Id, 0) )
continue;
p->pCexSeq = Cec4_ManDeriveCex( p, i, Abc_TtFindFirstBit2(Cec4_ObjSim(p, Id), p->nSimWords) );
return 0;
}
return 1;
}
void Cec4_ManSimulate( Gia_Man_t * p, Cec4_Man_t * pMan, int fRefine )
{
extern void Cec4_ManSimClassRefineOne( Gia_Man_t * p, int