summaryrefslogtreecommitdiffstats
path: root/src/proof
diff options
context:
space:
mode:
Diffstat (limited to 'src/proof')
-rw-r--r--src/proof/abs/absVta.c4
-rw-r--r--src/proof/acec/acecFadds.c30
-rw-r--r--src/proof/cec/cec.h8
-rw-r--r--src/proof/cec/cecCec.c6
-rw-r--r--src/proof/cec/cecChoice.c25
-rw-r--r--src/proof/cec/cecClass.c33
-rw-r--r--src/proof/cec/cecCore.c32
-rw-r--r--src/proof/cec/cecCorr.c2
-rw-r--r--src/proof/cec/cecInt.h11
-rw-r--r--src/proof/cec/cecMan.c1
-rw-r--r--src/proof/cec/cecSatG2.c1921
-rw-r--r--src/proof/cec/cecSim.c360
-rw-r--r--src/proof/cec/cecSolve.c7
-rw-r--r--src/proof/cec/cecSolveG.c641
-rw-r--r--src/proof/cec/cecSweep.c3
-rw-r--r--src/proof/cec/module.make3
-rw-r--r--src/proof/dch/dch.h1
-rw-r--r--src/proof/dch/dchCore.c4
-rw-r--r--src/proof/dch/dchSimSat.c4
-rw-r--r--src/proof/fra/fraSec.c24
-rw-r--r--src/proof/int/int.h2
-rw-r--r--src/proof/pdr/pdrCore.c4
-rw-r--r--src/proof/pdr/pdrIncr.c4
-rw-r--r--src/proof/pdr/pdrInv.c6
24 files changed, 3089 insertions, 47 deletions
diff --git a/src/proof/abs/absVta.c b/src/proof/abs/absVta.c
index 597e4b72..b6001d3f 100644
--- a/src/proof/abs/absVta.c
+++ b/src/proof/abs/absVta.c
@@ -705,8 +705,8 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
// objects with equal distance should receive priority based on number
// those objects whose prototypes have been added in other timeframes
// should have higher priority than the current object
- Vec_PtrSort( vTermsUsed, (int (*)(void))Vta_ManComputeDepthIncrease );
- Vec_PtrSort( vTermsUnused, (int (*)(void))Vta_ManComputeDepthIncrease );
+ Vec_PtrSort( vTermsUsed, (int (*)(const void *, const void *))Vta_ManComputeDepthIncrease );
+ Vec_PtrSort( vTermsUnused, (int (*)(const void *, const void *))Vta_ManComputeDepthIncrease );
if ( Vec_PtrSize(vTermsUsed) > 1 )
{
pThis0 = (Vta_Obj_t *)Vec_PtrEntry(vTermsUsed, 0);
diff --git a/src/proof/acec/acecFadds.c b/src/proof/acec/acecFadds.c
index d55eefe2..a2bdcfbe 100644
--- a/src/proof/acec/acecFadds.c
+++ b/src/proof/acec/acecFadds.c
@@ -314,16 +314,21 @@ void Dtc_ManCutMerge( Gia_Man_t * p, int iObj, int * pList0, int * pList1, Vec_I
if ( Type == 0 )
continue;
vTemp = Type == 1 ? vCutsXor : vCutsMaj;
- if ( fVerbose )
- printf( "%d = %s(", iObj, Type == 1 ? "XOR" : "MAJ" );
- for ( c = 1; c <= pCut[0]; c++ )
+ if ( 0 && Type == 2 )
{
+ fVerbose = 1;
+ if ( fVerbose )
+ printf( "%d = %s(", iObj, Type == 1 ? "XOR" : "MAJ" );
+ for ( c = 1; c <= pCut[0]; c++ )
+ {
+ if ( fVerbose )
+ printf( " %d", pCut[c] );
+ Vec_IntPush( vTemp, pCut[c] );
+ }
if ( fVerbose )
- printf( " %d", pCut[c] );
- Vec_IntPush( vTemp, pCut[c] );
+ printf( " )\n" );
+ fVerbose = 0;
}
- if ( fVerbose )
- printf( " )\n" );
Vec_IntPush( vTemp, iObj );
}
}
@@ -450,6 +455,16 @@ Vec_Int_t * Gia_ManDetectFullAdders( Gia_Man_t * p, int fVerbose, Vec_Int_t ** p
Vec_IntFree( vCutsMaj );
return vFadds;
}
+void Gia_ManDetectFullAdders2( Gia_Man_t * p, int fVerbose )
+{
+ Vec_Int_t * vCutsXor2, * vCutsXor, * vCutsMaj;
+ Dtc_ManComputeCuts( p, &vCutsXor2, &vCutsXor, &vCutsMaj, fVerbose );
+ if ( fVerbose )
+ printf( "XOR3 cuts = %d. MAJ cuts = %d.\n", Vec_IntSize(vCutsXor)/4, Vec_IntSize(vCutsMaj)/4 );
+ Vec_IntFree( vCutsXor2 );
+ Vec_IntFree( vCutsXor );
+ Vec_IntFree( vCutsMaj );
+}
/**Function*************************************************************
@@ -1238,6 +1253,7 @@ Gia_Man_t * Gia_ManDupWithArtificialBoxes( Gia_Man_t * p, int DelayC, int nPathM
return pNew;
}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/proof/cec/cec.h b/src/proof/cec/cec.h
index 757d9fd3..7c101570 100644
--- a/src/proof/cec/cec.h
+++ b/src/proof/cec/cec.h
@@ -43,6 +43,7 @@ ABC_NAMESPACE_HEADER_START
typedef struct Cec_ParSat_t_ Cec_ParSat_t;
struct Cec_ParSat_t_
{
+ int SolverType; // SAT solver type
int nBTLimit; // conflict limit at a node
int nSatVarMax; // the max number of SAT variables
int nCallsRecycle; // calls to perform before recycling SAT solver
@@ -95,13 +96,18 @@ struct Cec_ParSmf_t_
typedef struct Cec_ParFra_t_ Cec_ParFra_t;
struct Cec_ParFra_t_
{
+ int jType; // solver type
int nWords; // the number of simulation words
int nRounds; // the number of simulation rounds
int nItersMax; // the maximum number of iterations of SAT sweeping
int nBTLimit; // conflict limit at a node
+ int nBTLimitPo; // conflict limit at an output
int TimeLimit; // the runtime limit in seconds
int nLevelMax; // restriction on the level nodes to be swept
int nDepthMax; // the depth in terms of steps of speculative reduction
+ int nCallsRecycle; // calls to perform before recycling SAT solver
+ int nSatVarMax; // the max number of SAT variables
+ int nGenIters; // pattern generation iterations
int fRewriting; // enables AIG rewriting
int fCheckMiter; // the circuit is the miter
// int fFirstStop; // stop on the first sat output
@@ -215,7 +221,7 @@ extern void Cec_ManCecSetDefaultParams( Cec_ParCec_t * p );
extern void Cec_ManCorSetDefaultParams( Cec_ParCor_t * p );
extern void Cec_ManChcSetDefaultParams( Cec_ParChc_t * p );
extern Gia_Man_t * Cec_ManSatSweeping( Gia_Man_t * pAig, Cec_ParFra_t * pPars, int fSilent );
-extern Gia_Man_t * Cec_ManSatSolving( Gia_Man_t * pAig, Cec_ParSat_t * pPars );
+extern Gia_Man_t * Cec_ManSatSolving( Gia_Man_t * pAig, Cec_ParSat_t * pPars, int f0Proved );
extern void Cec_ManSimulation( Gia_Man_t * pAig, Cec_ParSim_t * pPars );
/*=== cecSeq.c ==========================================================*/
extern int Cec_ManSeqResimulateCounter( Gia_Man_t * pAig, Cec_ParSim_t * pPars, Abc_Cex_t * pCex );
diff --git a/src/proof/cec/cecCec.c b/src/proof/cec/cecCec.c
index ee45aa6c..cfa07ff8 100644
--- a/src/proof/cec/cecCec.c
+++ b/src/proof/cec/cecCec.c
@@ -349,12 +349,18 @@ int Cec_ManVerify( Gia_Man_t * pInit, Cec_ParCec_t * pPars )
Gia_ManStop( p );
return RetValue;
}
+ if ( pInit->vSimsPi )
+ {
+ p->vSimsPi = Vec_WrdDup(pInit->vSimsPi);
+ p->nSimWords = pInit->nSimWords;
+ }
// sweep for equivalences
Cec_ManFraSetDefaultParams( pParsFra );
pParsFra->nItersMax = 1000;
pParsFra->nBTLimit = pPars->nBTLimit;
pParsFra->TimeLimit = pPars->TimeLimit;
pParsFra->fVerbose = pPars->fVerbose;
+ pParsFra->fVeryVerbose = pPars->fVeryVerbose;
pParsFra->fCheckMiter = 1;
pParsFra->fDualOut = 1;
pNew = Cec_ManSatSweeping( p, pParsFra, pPars->fSilent );
diff --git a/src/proof/cec/cecChoice.c b/src/proof/cec/cecChoice.c
index 49025630..db0059fd 100644
--- a/src/proof/cec/cecChoice.c
+++ b/src/proof/cec/cecChoice.c
@@ -256,7 +256,7 @@ int Cec_ManChoiceComputation_int( Gia_Man_t * pAig, Cec_ParChc_t * pPars )
// found counter-examples to speculation
clk2 = Abc_Clock();
if ( pPars->fUseCSat )
- vCexStore = Cbs_ManSolveMiterNc( pSrm, pPars->nBTLimit, &vStatus, 0 );
+ vCexStore = Cbs_ManSolveMiterNc( pSrm, pPars->nBTLimit, &vStatus, 0, 0 );
else
vCexStore = Cec_ManSatSolveMiter( pSrm, pParsSat, &vStatus );
Gia_ManStop( pSrm );
@@ -401,6 +401,29 @@ Aig_Man_t * Cec_ComputeChoices( Gia_Man_t * pGia, Dch_Pars_t * pPars )
return pAig;
}
+/**Function*************************************************************
+
+ Synopsis [Performs computation of AIGs with choices.]
+
+ Description [Takes several AIGs and performs choicing.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Cec_ComputeChoicesNew( Gia_Man_t * pGia, int nConfs, int fVerbose )
+{
+ extern void Cec4_ManSimulateTest2( Gia_Man_t * p, int nConfs, int fVerbose );
+ Aig_Man_t * pAig;
+ Cec4_ManSimulateTest2( pGia, nConfs, fVerbose );
+ pGia = Gia_ManEquivToChoices( pGia, 3 );
+ Gia_ManSetRegNum( pGia, Gia_ManRegNum(pGia) );
+ pAig = Gia_ManToAig( pGia, 1 );
+ Gia_ManStop( pGia );
+ return pAig;
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/proof/cec/cecClass.c b/src/proof/cec/cecClass.c
index 2d820c39..be88b9be 100644
--- a/src/proof/cec/cecClass.c
+++ b/src/proof/cec/cecClass.c
@@ -878,19 +878,34 @@ int Cec_ManSimClassesPrepare( Cec_ManSim_t * p, int LevelMax )
if ( pObj->Value )
Gia_ObjSetRepr( p->pAig, Gia_ObjId(p->pAig, pObj), 0 );
// perform simulation
- p->nWords = 1;
- do {
+ if ( p->pAig->nSimWords )
+ {
+ p->nWords = 2*p->pAig->nSimWords;
+ assert( Vec_WrdSize(p->pAig->vSimsPi) == Gia_ManCiNum(p->pAig) * p->pAig->nSimWords );
+ //Cec_ManSimCreateInfo( p, p->vCiSimInfo, p->vCoSimInfo );
+ for ( i = 0; i < Gia_ManCiNum(p->pAig); i++ )
+ memmove( Vec_PtrEntry(p->vCiSimInfo, i), Vec_WrdEntryP(p->pAig->vSimsPi, i*p->pAig->nSimWords), sizeof(word)*p->pAig->nSimWords );
+ if ( Cec_ManSimSimulateRound( p, p->vCiSimInfo, p->vCoSimInfo ) )
+ return 1;
if ( p->pPars->fVerbose )
Gia_ManEquivPrintClasses( p->pAig, 0, Cec_MemUsage(p) );
- for ( i = 0; i < 4; i++ )
- {
- Cec_ManSimCreateInfo( p, p->vCiSimInfo, p->vCoSimInfo );
- if ( Cec_ManSimSimulateRound( p, p->vCiSimInfo, p->vCoSimInfo ) )
- return 1;
+ }
+ else
+ {
+ p->nWords = 1;
+ do {
+ if ( p->pPars->fVerbose )
+ Gia_ManEquivPrintClasses( p->pAig, 0, Cec_MemUsage(p) );
+ for ( i = 0; i < 4; i++ )
+ {
+ Cec_ManSimCreateInfo( p, p->vCiSimInfo, p->vCoSimInfo );
+ if ( Cec_ManSimSimulateRound( p, p->vCiSimInfo, p->vCoSimInfo ) )
+ return 1;
+ }
+ p->nWords = 2 * p->nWords + 1;
}
- p->nWords = 2 * p->nWords + 1;
+ while ( p->nWords <= p->pPars->nWords );
}
- while ( p->nWords <= p->pPars->nWords );
return 0;
}
diff --git a/src/proof/cec/cecCore.c b/src/proof/cec/cecCore.c
index b9529658..f94bd27f 100644
--- a/src/proof/cec/cecCore.c
+++ b/src/proof/cec/cecCore.c
@@ -45,6 +45,7 @@ ABC_NAMESPACE_IMPL_START
void Cec_ManSatSetDefaultParams( Cec_ParSat_t * p )
{
memset( p, 0, sizeof(Cec_ParSat_t) );
+ p->SolverType = -1; // SAT solver type
p->nBTLimit = 100; // conflict limit at a node
p->nSatVarMax = 2000; // the max number of SAT variables
p->nCallsRecycle = 200; // calls to perform before recycling SAT solver
@@ -232,14 +233,17 @@ void Cec_ManChcSetDefaultParams( Cec_ParChc_t * p )
SeeAlso []
***********************************************************************/
-Gia_Man_t * Cec_ManSatSolving( Gia_Man_t * pAig, Cec_ParSat_t * pPars )
+Gia_Man_t * Cec_ManSatSolving( Gia_Man_t * pAig, Cec_ParSat_t * pPars, int f0Proved )
{
Gia_Man_t * pNew;
Cec_ManPat_t * pPat;
pPat = Cec_ManPatStart();
- Cec_ManSatSolve( pPat, pAig, pPars, NULL, NULL, NULL );
+ if ( pPars->SolverType == -1 )
+ Cec_ManSatSolve( pPat, pAig, pPars, NULL, NULL, NULL, f0Proved );
+ else
+ CecG_ManSatSolve( pPat, pAig, pPars, f0Proved );
// pNew = Gia_ManDupDfsSkip( pAig );
- pNew = Gia_ManDup( pAig );
+ pNew = Gia_ManCleanup( pAig );
Cec_ManPatStop( pPat );
pNew->vSeqModelVec = pAig->vSeqModelVec;
pAig->vSeqModelVec = NULL;
@@ -348,6 +352,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 );
@@ -360,6 +366,11 @@ Gia_Man_t * Cec_ManSatSweeping( Gia_Man_t * pAig, Cec_ParFra_t * pPars, int fSil
Vec_IntFreeP( &pAig->vIdsEquiv );
pAig->vIdsEquiv = Vec_IntAlloc( 1000 );
}
+ if ( pAig->vSimsPi )
+ {
+ pIni->vSimsPi = Vec_WrdDup(pAig->vSimsPi);
+ pIni->nSimWords = pAig->nSimWords;
+ }
// prepare the managers
// SAT sweeping
@@ -368,25 +379,25 @@ Gia_Man_t * Cec_ManSatSweeping( Gia_Man_t * pAig, Cec_ParFra_t * pPars, int fSil
pPars->fColorDiff = 1;
// simulation
Cec_ManSimSetDefaultParams( pParsSim );
- pParsSim->nWords = pPars->nWords;
+ pParsSim->nWords = Abc_MaxInt(2*pAig->nSimWords, pPars->nWords);
pParsSim->nFrames = pPars->nRounds;
pParsSim->fCheckMiter = pPars->fCheckMiter;
pParsSim->fDualOut = pPars->fDualOut;
pParsSim->fVerbose = pPars->fVerbose;
- pSim = Cec_ManSimStart( p->pAig, pParsSim );
+ pSim = Cec_ManSimStart( pIni, pParsSim );
// SAT solving
Cec_ManSatSetDefaultParams( pParsSat );
pParsSat->nBTLimit = pPars->nBTLimit;
pParsSat->fVerbose = pPars->fVeryVerbose;
// simulation patterns
pPat = Cec_ManPatStart();
- pPat->fVerbose = pPars->fVeryVerbose;
+ //pPat->fVerbose = pPars->fVeryVerbose;
// start equivalence classes
clk = Abc_Clock();
if ( p->pAig->pReprs == NULL )
{
- if ( Cec_ManSimClassesPrepare(pSim, -1) || Cec_ManSimClassesRefine(pSim) )
+ if ( Cec_ManSimClassesPrepare(pSim, -1) || (!p->pAig->nSimWords && Cec_ManSimClassesRefine(pSim)) )
{
Gia_ManStop( p->pAig );
p->pAig = NULL;
@@ -438,7 +449,7 @@ clk = Abc_Clock();
if ( pPars->fRunCSat )
Cec_ManSatSolveCSat( pPat, pSrm, pParsSat );
else
- Cec_ManSatSolve( pPat, pSrm, pParsSat, p->pAig->vIdsOrig, p->vXorNodes, pAig->vIdsEquiv );
+ Cec_ManSatSolve( pPat, pSrm, pParsSat, p->pAig->vIdsOrig, p->vXorNodes, pAig->vIdsEquiv, 0 );
p->timeSat += Abc_Clock() - clk;
if ( Cec_ManFraClassesUpdate( p, pSim, pPat, pSrm ) )
{
@@ -514,6 +525,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",
@@ -543,6 +557,8 @@ finalize:
Cec_ManSimStop( pSim );
Cec_ManPatStop( pPat );
Cec_ManFraStop( p );
+ if ( pTemp ) ABC_FREE( pTemp->pReprs );
+ if ( pTemp ) ABC_FREE( pTemp->pNexts );
return pTemp;
}
diff --git a/src/proof/cec/cecCorr.c b/src/proof/cec/cecCorr.c
index 8f708910..ce7e0885 100644
--- a/src/proof/cec/cecCorr.c
+++ b/src/proof/cec/cecCorr.c
@@ -996,7 +996,7 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
// found counter-examples to speculation
clk2 = Abc_Clock();
if ( pPars->fUseCSat )
- vCexStore = Cbs_ManSolveMiterNc( pSrm, pPars->nBTLimit, &vStatus, 0 );
+ vCexStore = Cbs_ManSolveMiterNc( pSrm, pPars->nBTLimit, &vStatus, 0, 0 );
else
vCexStore = Cec_ManSatSolveMiter( pSrm, pParsSat, &vStatus );
Gia_ManStop( pSrm );
diff --git a/src/proof/cec/cecInt.h b/src/proof/cec/cecInt.h
index d93e5e86..f78e5f25 100644
--- a/src/proof/cec/cecInt.h
+++ b/src/proof/cec/cecInt.h
@@ -27,6 +27,7 @@
////////////////////////////////////////////////////////////////////////
#include "sat/bsat/satSolver.h"
+#include "sat/glucose2/AbcGlucose2.h"
#include "misc/bar/bar.h"
#include "aig/gia/gia.h"
#include "cec.h"
@@ -80,7 +81,8 @@ struct Cec_ManSat_t_
Gia_Man_t * pAig; // the AIG whose outputs are considered
Vec_Int_t * vStatus; // status for each output
// SAT solving
- sat_solver * pSat; // recyclable SAT solver
+ sat_solver * pSat; // recyclable SAT solver (MiniSAT)
+ bmcg2_sat_solver*pSat2; // recyclable SAT solver (Glucose)
int nSatVars; // the counter of SAT variables
int * pSatVars; // mapping of each node into its SAT var
Vec_Ptr_t * vUsedNodes; // nodes whose SAT vars are assigned
@@ -153,6 +155,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
@@ -201,7 +206,7 @@ extern int Cec_ManCountNonConstOutputs( Gia_Man_t * pAig );
extern int Cec_ManCheckNonTrivialCands( Gia_Man_t * pAig );
/*=== cecSolve.c ============================================================*/
extern int Cec_ObjSatVarValue( Cec_ManSat_t * p, Gia_Obj_t * pObj );
-extern void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_Int_t * vIdsOrig, Vec_Int_t * vMiterPairs, Vec_Int_t * vEquivPairs );
+extern void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_Int_t * vIdsOrig, Vec_Int_t * vMiterPairs, Vec_Int_t * vEquivPairs, int f0Proved );
extern void Cec_ManSatSolveCSat( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars );
extern Vec_Str_t * Cec_ManSatSolveSeq( Vec_Ptr_t * vPatts, Gia_Man_t * pAig, Cec_ParSat_t * pPars, int nRegs, int * pnPats );
extern Vec_Int_t * Cec_ManSatSolveMiter( Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_Str_t ** pvStatus );
@@ -209,6 +214,8 @@ extern int Cec_ManSatCheckNode( Cec_ManSat_t * p, Gia_Obj_t * p
extern int Cec_ManSatCheckNodeTwo( Cec_ManSat_t * p, Gia_Obj_t * pObj1, Gia_Obj_t * pObj2 );
extern void Cec_ManSavePattern( Cec_ManSat_t * p, Gia_Obj_t * pObj1, Gia_Obj_t * pObj2 );
extern Vec_Int_t * Cec_ManSatReadCex( Cec_ManSat_t * p );
+/*=== cecSolveG.c ============================================================*/
+extern void CecG_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars, int f0Proved );
/*=== ceFraeep.c ============================================================*/
extern Gia_Man_t * Cec_ManFraSpecReduction( Cec_ManFra_t * p );
extern int Cec_ManFraClassesUpdate( Cec_ManFra_t * p, Cec_ManSim_t * pSim, Cec_ManPat_t * pPat, Gia_Man_t * pNew );
diff --git a/src/proof/cec/cecMan.c b/src/proof/cec/cecMan.c
index 1d32b99e..c636a00d 100644
--- a/src/proof/cec/cecMan.c
+++ b/src/proof/cec/cecMan.c
@@ -73,6 +73,7 @@ Cec_ManSat_t * Cec_ManSatCreate( Gia_Man_t * pAig, Cec_ParSat_t * pPars )
***********************************************************************/
void Cec_ManSatPrintStats( Cec_ManSat_t * p )
{
+ printf( "SAT solver statistics:\n" );
Abc_Print( 1, "CO = %8d ", Gia_ManCoNum(p->pAig) );
Abc_Print( 1, "AND = %8d ", Gia_ManAndNum(p->pAig) );
Abc_Print( 1, "Conf = %5d ", p->pPars->nBTLimit );
diff --git a/src/proof/cec/cecSatG2.c b/src/proof/cec/cecSatG2.c
new file mode 100644
index 00000000..ce299c66
--- /dev/null
+++ b/src/proof/cec/cecSatG2.c
@@ -0,0 +1,1921 @@
+/**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 "cec.h"
+
+#define USE_GLUCOSE2
+
+#ifdef USE_GLUCOSE2
+
+#include "sat/glucose2/AbcGlucose2.h"
+
+#define sat_solver bmcg2_sat_solver
+#define sat_solver_start bmcg2_sat_solver_start
+#define sat_solver_stop bmcg2_sat_solver_stop
+#define sat_solver_addclause bmcg2_sat_solver_addclause
+#define sat_solver_add_and bmcg2_sat_solver_add_and
+#define sat_solver_add_xor bmcg2_sat_solver_add_xor
+#define sat_solver_addvar bmcg2_sat_solver_addvar
+#define sat_solver_read_cex_varvalue bmcg2_sat_solver_read_cex_varvalue
+#define sat_solver_reset bmcg2_sat_solver_reset
+#define sat_solver_set_conflict_budget bmcg2_sat_solver_set_conflict_budget
+#define sat_solver_conflictnum bmcg2_sat_solver_conflictnum
+#define sat_solver_solve bmcg2_sat_solver_solve
+#define sat_solver_read_cex_varvalue bmcg2_sat_solver_read_cex_varvalue
+#define sat_solver_read_cex bmcg2_sat_solver_read_cex
+#define sat_solver_jftr bmcg2_sat_solver_jftr
+#define sat_solver_set_jftr bmcg2_sat_solver_set_jftr
+#define sat_solver_set_var_fanin_lit bmcg2_sat_solver_set_var_fanin_lit
+#define sat_solver_start_new_round bmcg2_sat_solver_start_new_round
+#define sat_solver_mark_cone bmcg2_sat_solver_mark_cone
+
+#else
+
+#include "sat/glucose/AbcGlucose.h"
+
+#define sat_solver bmcg_sat_solver
+#define sat_solver_start bmcg_sat_solver_start
+#define sat_solver_stop bmcg_sat_solver_stop
+#define sat_solver_addclause bmcg_sat_solver_addclause
+#define sat_solver_add_and bmcg_sat_solver_add_and
+#define sat_solver_add_xor bmcg_sat_solver_add_xor
+#define sat_solver_addvar bmcg_sat_solver_addvar
+#define sat_solver_read_cex_varvalue bmcg_sat_solver_read_cex_varvalue
+#define sat_solver_reset bmcg_sat_solver_reset
+#define sat_solver_set_conflict_budget bmcg_sat_solver_set_conflict_budget
+#define sat_solver_conflictnum bmcg_sat_solver_conflictnum
+#define sat_solver_solve bmcg_sat_solver_solve
+#define sat_solver_read_cex_varvalue bmcg_sat_solver_read_cex_varvalue
+#define sat_solver_read_cex bmcg_sat_solver_read_cex
+#define sat_solver_jftr bmcg_sat_solver_jftr
+#define sat_solver_set_jftr bmcg_sat_solver_set_jftr
+#define sat_solver_set_var_fanin_lit bmcg_sat_solver_set_var_fanin_lit
+#define sat_solver_start_new_round bmcg_sat_solver_start_new_round
+#define sat_solver_mark_cone bmcg_sat_solver_mark_cone
+
+#endif
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+// SAT solving manager
+typedef struct Cec4_Man_t_ Cec4_Man_t;
+struct Cec4_Man_t_
+{
+ Cec_ParFra_t * pPars; // parameters
+ Gia_Man_t * pAig; // user's AIG
+ Gia_Man_t * pNew; // internal AIG
+ // SAT solving
+ sat_solver * pSat; // SAT solver
+ Vec_Ptr_t * vFrontier; // CNF construction
+ Vec_Ptr_t * vFanins; // CNF construction
+ Vec_Int_t * vCexMin; // minimized CEX
+ Vec_Int_t * vClassUpdates; // updated equiv classes
+ Vec_Int_t * vCexStamps; // time stamps
+ Vec_Int_t * vCands;
+ Vec_Int_t * vVisit;
+ Vec_Int_t * vPat;
+ Vec_Int_t * vDisprPairs;
+ Vec_Bit_t * vFails;
+ Vec_Bit_t * vCoDrivers;
+ int iPosRead; // candidate reading position
+ int iPosWrite; // candidate writing position
+ int iLastConst; // last const node proved
+ // refinement
+ Vec_Int_t * vRefClasses;
+ Vec_Int_t * vRefNodes;
+ Vec_Int_t * vRefBins;
+ int * pTable;
+ int nTableSize;
+ // statistics
+ int nItersSim;
+ int nItersSat;
+ int nAndNodes;
+ int nPatterns;
+ int nSatSat;
+ int nSatUnsat;
+ int nSatUndec;
+ int nCallsSince;
+ int nSimulates;
+ int nRecycles;
+ int nConflicts[2][3];
+ int nGates[2];
+ int nFaster[2];
+ abctime timeCnf;
+ abctime timeGenPats;
+ 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); assert(Vec_IntSize(&p->vVarMap) == Num); Vec_IntPush(&p->vVarMap, Gia_ObjId(p, pObj)); 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 []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Wrd_t * Cec4_EvalCombine( Vec_Int_t * vPats, int nPats, int nInputs, int nWords )
+{
+ //Vec_Wrd_t * vSimsPi = Vec_WrdStart( nInputs * nWords );
+ Vec_Wrd_t * vSimsPi = Vec_WrdStartRandom( nInputs * nWords );
+ int i, k, iLit, iPat = 0; word * pSim;
+ for ( i = 0; i < Vec_IntSize(vPats); i += Vec_IntEntry(vPats, i), iPat++ )
+ for ( k = 1; k < Vec_IntEntry(vPats, i)-1; k++ )
+ if ( (iLit = Vec_IntEntry(vPats, i+k)) )
+ {
+ assert( Abc_Lit2Var(iLit) > 0 && Abc_Lit2Var(iLit) <= nInputs );
+ pSim = Vec_WrdEntryP( vSimsPi, (Abc_Lit2Var(iLit)-1)*nWords );
+ if ( Abc_InfoHasBit( (unsigned*)pSim, iPat ) != Abc_LitIsCompl(iLit) )
+ Abc_InfoXorBit( (unsigned*)pSim, iPat );
+ }
+ assert( iPat == nPats );
+ return vSimsPi;
+}
+void Cec4_EvalPatterns( Gia_Man_t * p, Vec_Int_t * vPats, int nPats )
+{
+ int nWords = Abc_Bit6WordNum(nPats);
+ Vec_Wrd_t * vSimsPi = Cec4_EvalCombine( vPats, nPats, Gia_ManCiNum(p), nWords );
+ Vec_Wrd_t * vSimsPo = Gia_ManSimPatSimOut( p, vSimsPi, 1 );
+ int i, Count = 0, nErrors = 0;
+ for ( i = 0; i < Gia_ManCoNum(p); i++ )
+ {
+ int CountThis = Abc_TtCountOnesVec( Vec_WrdEntryP(vSimsPo, i*nWords), nWords );
+ if ( CountThis == 0 )
+ continue;
+ printf( "%d ", CountThis );
+ nErrors += CountThis;
+ Count++;
+ }
+ printf( "\nDetected %d error POs with %d errors (average %.2f).\n", Count, nErrors, 1.0*nErrors/Abc_MaxInt(1, Count) );
+ Vec_WrdFree( vSimsPi );
+ Vec_WrdFree( vSimsPo );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Default parameter settings.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Cec4_ManSetParams( Cec_ParFra_t * pPars )
+{
+ memset( pPars, 0, sizeof(Cec_ParFra_t) );
+ pPars->jType = 2; // solver type
+ pPars->fSatSweeping = 1; // conflict limit at a node
+ pPars->nWords = 4; // simulation words
+ pPars->nRounds = 10; // simulation rounds
+ pPars->nItersMax = 2000; // this is a miter
+ pPars->nBTLimit = 1000000; // use logic cones
+ pPars->nBTLimitPo = 0; // use logic outputs
+ pPars->nSatVarMax = 1000; // the max number of SAT variables before recycling SAT solver
+ pPars->nCallsRecycle = 500; // calls to perform before recycling SAT solver
+ pPars->nGenIters = 100; // pattern generation iterations
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Cec4_Man_t * Cec4_ManCreate( Gia_Man_t * pAig, Cec_ParFra_t * pPars )
+{
+ Cec4_Man_t * p = ABC_CALLOC( Cec4_Man_t, 1 );
+ memset( p, 0, sizeof(Cec4_Man_t) );
+ p->timeStart = Abc_Clock();
+ p->pPars = pPars;
+ p->pAig = pAig;
+ p->pSat = sat_solver_start();
+ sat_solver_set_jftr( p->pSat, pPars->jType );
+ 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) );
+ p->vCands = Vec_IntAlloc( 100 );
+ p->vVisit = Vec_IntAlloc( 100 );
+ p->vPat = Vec_IntAlloc( 100 );
+ p->vDisprPairs = Vec_IntAlloc( 100 );
+ p->vFails = Vec_BitStart( Gia_ManObjNum(pAig) );
+ //pAig->pData = p->pSat; // point AIG manager to the solver
+ //Vec_IntFreeP( &p->pAig->vPats );
+ //p->pAig->vPats = Vec_IntAlloc( 1000 );
+ if ( pPars->nBTLimitPo )
+ {
+ int i, Driver;
+ p->vCoDrivers = Vec_BitStart( Gia_ManObjNum(pAig) );
+ Gia_ManForEachCoDriverId( pAig, Driver, i )
+ Vec_BitWriteEntry( p->vCoDrivers, Driver, 1 );
+ }
+ 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->timeGenPats;// - 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( "Generate CNF ", p->timeCnf, timeTotal );
+ ABC_PRTP( "Generate pats", p->timeGenPats, 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 );
+ }
+ //printf( "Recorded %d patterns with %d literals (average %.2f).\n",
+ // p->pAig->nBitPats, Vec_IntSize(p->pAig->vPats) - 2*p->pAig->nBitPats, 1.0*Vec_IntSize(p->pAig->vPats)/Abc_MaxInt(1, p->pAig->nBitPats)-2 );
+ //Cec4_EvalPatterns( p->pAig, p->pAig->vPats, p->pAig->nBitPats );
+ //Vec_IntFreeP( &p->pAig->vPats );
+ Vec_WrdFreeP( &p->pAig->vSims );
+ Vec_WrdFreeP( &p->pAig->vSimsPi );
+ Gia_ManCleanMark01( p->pAig );
+ 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 );
+ Vec_IntFreeP( &p->vCands );
+ Vec_IntFreeP( &p->vVisit );
+ Vec_IntFreeP( &p->vPat );
+ Vec_IntFreeP( &p->vDisprPairs );
+ Vec_BitFreeP( &p->vFails );
+ Vec_BitFreeP( &p->vCoDrivers );
+ Vec_IntFreeP( &p->vRefClasses );
+ Vec_IntFreeP( &p->vRefNodes );
+ Vec_IntFreeP( &p->vRefBins );
+ ABC_FREE( p->pTable );
+ ABC_FREE( p );
+}
+Gia_Man_t * Cec4_ManStartNew( Gia_Man_t * pAig )
+{
+ Gia_Obj_t * pObj; int i;
+ Gia_Man_t * pNew = Gia_ManStart( Gia_ManObjNum(pAig) );
+ pNew->pName = Abc_UtilStrsav( pAig->pName );
+ pNew->pSpec = Abc_UtilStrsav( pAig->pSpec );
+ if ( pAig->pMuxes )
+ pNew->pMuxes = ABC_CALLOC( unsigned, pNew->nObjsAlloc );
+ Gia_ManFillValue( pAig );
+ Gia_ManConst0(pAig)->Value = 0;
+ Gia_ManForEachCi( pAig, pObj, i )
+ pObj->Value = Gia_ManAppendCi( pNew );
+ Gia_ManHashAlloc( pNew );
+ Vec_IntFill( &pNew->vCopies2, Gia_ManObjNum(pAig), -1 );
+ Gia_ManSetRegNum( pNew, Gia_ManRegNum(pAig) );
+ return pNew;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Adds clauses to the solver.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Cec4_AddClausesMux( Gia_Man_t * p, Gia_Obj_t * pNode, 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 = 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 = 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 = 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 = 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 = 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 = sat_solver_addclause( pSat, pLits, 3 );
+ assert( RetValue );
+}
+void Cec4_AddClausesSuper( Gia_Man_t * p, Gia_Obj_t * pNode, Vec_Ptr_t * vSuper, 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 = 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 = 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, 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, sat_solver_addvar(pSat) );
+ if ( Gia_ObjIsAnd(pObj) )
+ Vec_PtrPush( vFrontier, pObj );
+}
+int Cec4_ObjGetCnfVar( Cec4_Man_t * p, int iObj )
+{
+ int fUseSimple = 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, sat_solver_addvar(p->pSat) );
+ assert( Gia_ObjIsAnd(pObj) );
+ if ( fUseSimple )
+ {
+ Gia_Obj_t * pFan0, * pFan1;
+ //if ( Gia_ObjRecognizeExor(pObj, &pFan0, &pFan1) )
+ // printf( "%d", (Gia_IsComplement(pFan1) << 1) + Gia_IsComplement(pFan0) );
+ if ( p->pNew->pMuxes == NULL && Gia_ObjRecognizeExor(pObj, &pFan0, &pFan1) && Gia_IsComplement(pFan0) == Gia_IsComplement(pFan1) )
+ {
+ int iVar0 = Cec4_ObjGetCnfVar( p, Gia_ObjId(p->pNew, Gia_Regular(pFan0)) );
+ int iVar1 = Cec4_ObjGetCnfVar( p, Gia_ObjId(p->pNew, Gia_Regular(pFan1)) );
+ int iVar = Cec4_ObjSetSatId( p->pNew, pObj, sat_solver_addvar(p->pSat) );
+ if ( p->pPars->jType < 2 )
+ sat_solver_add_xor( p->pSat, iVar, iVar0, iVar1, 0 );
+ if ( p->pPars->jType > 0 )
+ {
+ int Lit0 = Abc_Var2Lit( iVar0, 0 );
+ int Lit1 = Abc_Var2Lit( iVar1, 0 );
+ if ( Lit0 < Lit1 )
+ Lit1 ^= Lit0, Lit0 ^= Lit1, Lit1 ^= Lit0;
+ assert( Lit0 > Lit1 );
+ sat_solver_set_var_fanin_lit( p->pSat, iVar, Lit0, Lit1 );
+ p->nGates[1]++;
+ }
+ }
+ else
+ {
+ int iVar0 = Cec4_ObjGetCnfVar( p, Gia_ObjFaninId0(pObj, iObj) );
+ int iVar1 = Cec4_ObjGetCnfVar( p, Gia_ObjFaninId1(pObj, iObj) );
+ int iVar = Cec4_ObjSetSatId( p->pNew, pObj, sat_solver_addvar(p->pSat) );
+ if ( p->pPars->jType < 2 )
+ {
+ if ( Gia_ObjIsXor(pObj) )
+ sat_solver_add_xor( p->pSat, iVar, iVar0, iVar1, Gia_ObjFaninC0(pObj) ^ Gia_ObjFaninC1(pObj) );
+ else
+ sat_solver_add_and( p->pSat, iVar, iVar0, iVar1, Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj), 0 );
+ }
+ if ( p->pPars->jType > 0 )
+ {
+ int Lit0 = Abc_Var2Lit( iVar0, Gia_ObjFaninC0(pObj) );
+ int Lit1 = Abc_Var2Lit( iVar1, Gia_ObjFaninC1(pObj) );
+ if ( (Lit0 > Lit1) ^ Gia_ObjIsXor(pObj) )
+ Lit1 ^= Lit0, Lit0 ^= Lit1, Lit1 ^= Lit0;
+ sat_solver_set_var_fanin_lit( p->pSat, iVar, Lit0, Lit1 );
+ p->nGates[Gia_ObjIsXor(pObj)]++;
+ }
+ }
+ return Cec4_ObjSatId( p->pNew, pObj );
+ }
+ assert( !Gia_ObjIsXor(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 [Refinement of equivalence classes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline word * Cec4_ObjSim( Gia_Man_t * p, int iObj )
+{
+ return Vec_WrdEntryP( p->vSims, p->nSimWords * iObj );
+}
+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;
+ }
+}
+int Cec4_ManSimHashKey( word * pSim, int nSims, int nTableSize )
+{
+ static int s_Primes[16] = {
+ 1291, 1699, 1999, 2357, 2953, 3313, 3907, 4177,
+ 4831, 5147, 5647, 6343, 6899, 7103, 7873, 8147 };
+ unsigned uHash = 0, * pSimU = (unsigned *)pSim;
+ int i, nSimsU = 2 * nSims;
+ if ( pSimU[0] & 1 )
+ for ( i = 0; i < nSimsU; i++ )
+ uHash ^= ~pSimU[i] * s_Primes[i & 0xf];
+ else
+ for ( i = 0; i < nSimsU; i++ )
+ uHash ^= pSimU[i] * s_Primes[i & 0xf];
+ return (int)(uHash % nTableSize);
+
+}
+void Cec4_RefineOneClassIter( Gia_Man_t * p, int iRepr )
+{
+ int iObj, iPrev = iRepr, iPrev2, iRepr2;
+ assert( Gia_ObjRepr(p, iRepr) == GIA_VOID );
+ assert( Gia_ObjNext(p, iRepr) > 0 );
+ Gia_ClassForEachObj1( p, iRepr, iRepr2 )
+ if ( Cec4_ObjSimEqual(p, iRepr, iRepr2) )
+ iPrev = iRepr2;
+ else
+ break;
+ if ( iRepr2 <= 0 ) // no refinement
+ return;
+ // relink remaining nodes of the class
+ // nodes that are equal to iRepr, remain in the class of iRepr
+ // nodes that are not equal to iRepr, move to the class of iRepr2
+ Gia_ObjSetRepr( p, iRepr2, GIA_VOID );
+ iPrev2 = iRepr2;
+ for ( iObj = Gia_ObjNext(p, iRepr2); iObj > 0; iObj = Gia_ObjNext(p, iObj) )
+ {
+ if ( Cec4_ObjSimEqual(p, iRepr, iObj) ) // remains with iRepr
+ {
+ Gia_ObjSetNext( p, iPrev, iObj );
+ iPrev = iObj;
+ }
+ else // moves to iRepr2
+ {
+ Gia_ObjSetRepr( p, iObj, iRepr2 );
+ Gia_ObjSetNext( p, iPrev2, iObj );
+ iPrev2 = iObj;
+ }
+ }
+ Gia_ObjSetNext( p, iPrev, -1 );
+ Gia_ObjSetNext( p, iPrev2, -1 );
+ // refine incrementally
+ if ( Gia_ObjNext(p, iRepr2) > 0 )
+ Cec4_RefineOneClassIter( p, iRepr2 );
+}
+void Cec4_RefineOneClass( Gia_Man_t * p, Cec4_Man_t * pMan, Vec_Int_t * vNodes )
+{
+ int k, iObj, Bin;
+ Vec_IntClear( pMan->vRefBins );
+ Vec_IntForEachEntryReverse( vNodes, iObj, k )
+ {
+ int Key = Cec4_ManSimHashKey( Cec4_ObjSim(p, iObj), p->nSimWords, pMan->nTableSize );
+ assert( Key >= 0 && Key < pMan->nTableSize );
+ if ( pMan->pTable[Key] == -1 )
+ Vec_IntPush( pMan->vRefBins, Key );
+ p->pNexts[iObj] = pMan->pTable[Key];
+ pMan->pTable[Key] = iObj;
+ }
+ Vec_IntForEachEntry( pMan->vRefBins, Bin, k )
+ {
+ int iRepr = pMan->pTable[Bin];
+ pMan->pTable[Bin] = -1;
+ assert( p->pReprs[iRepr].iRepr == GIA_VOID );
+ assert( p->pNexts[iRepr] != 0 );
+ if ( p->pNexts[iRepr] == -1 )
+ continue;
+ for ( iObj = p->pNexts[iRepr]; iObj > 0; iObj = p->pNexts[iObj] )
+ p->pReprs[iObj].iRepr = iRepr;
+ Cec4_RefineOneClassIter( p, iRepr );
+ }
+ Vec_IntClear( pMan->vRefBins );
+}
+void Cec4_RefineClasses( Gia_Man_t * p, Cec4_Man_t * pMan, Vec_Int_t * vClasses )
+{
+ if ( Vec_IntSize(pMan->vRefClasses) == 0 )
+ return;
+ if ( Vec_IntSize(pMan->vRefNodes) > 0 )
+ Cec4_RefineOneClass( p, pMan, pMan->vRefNodes );
+ else
+ {
+ int i, k, iObj, iRepr;
+ Vec_IntForEachEntry( pMan->vRefClasses, iRepr, i )
+ {
+ assert( p->pReprs[iRepr].fColorA );
+ p->pReprs[iRepr].fColorA = 0;
+ Vec_IntClear( pMan->vRefNodes );
+ Vec_IntPush( pMan->vRefNodes, iRepr );
+ Gia_ClassForEachObj1( p, iRepr, k )
+ Vec_IntPush( pMan->vRefNodes, k );
+ Vec_IntForEachEntry( pMan->vRefNodes, iObj, k )
+ {
+ p->pReprs[iObj].iRepr = GIA_VOID;
+ p->pNexts[iObj] = -1;
+ }
+ Cec4_RefineOneClass( p, pMan, pMan->vRefNodes );
+ }
+ }
+ Vec_IntClear( pMan->vRefClasses );
+ Vec_IntClear( pMan->vRefNodes );
+}
+void Cec4_RefineInit( Gia_Man_t * p, Cec4_Man_t * pMan )
+{
+ Gia_Obj_t * pObj; int i;
+ ABC_FREE( p->pReprs );
+ ABC_FREE( p->pNexts );
+ p->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p) );
+ p->pNexts = ABC_FALLOC( int, Gia_ManObjNum(p) );
+ pMan->nTableSize = Abc_PrimeCudd( Gia_ManObjNum(p) );
+ pMan->pTable = ABC_FALLOC( int, pMan->nTableSize );
+ pMan->vRefNodes = Vec_IntAlloc( Gia_ManObjNum(p) );
+ Gia_ManForEachObj( p, pObj, i )
+ {
+ p->pReprs[i].iRepr = GIA_VOID;
+ if ( !Gia_ObjIsCo(pObj) && (!pMan->pPars->nLevelMax || Gia_ObjLevel(p, pObj) <= pMan->pPars->nLevelMax) )
+ Vec_IntPush( pMan->vRefNodes, i );
+ }
+ pMan->vRefBins = Vec_IntAlloc( Gia_ManObjNum(p)/2 );
+ pMan->vRefClasses = Vec_IntAlloc( Gia_ManObjNum(p)/2 );
+ Vec_IntPush( pMan->vRefClasses, 0 );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Internal simulation APIs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+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 int Cec4_ObjSimGetInputBit( Gia_Man_t * p, int iObj )
+{
+ word * pSim = Cec4_ObjSim( p, iObj );
+ return Abc_InfoHasBit( (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 void Cec4_ObjSimXor( 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
+ for ( w = 0; w < p->nSimWords; w++ )
+ pSim[w] = pSim0[w] ^ pSim1[w];
+}
+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 )
+{
+ abctime clk = Abc_Clock();
+ Gia_Obj_t * pObj; int i;
+ pMan->nSimulates++;
+ if ( pMan->pTable == NULL )
+ Cec4_RefineInit( p, pMan );
+ else
+ assert( Vec_IntSize(pMan->vRefClasses) == 0 );
+ Gia_ManForEachAnd( p, pObj, i )
+ {
+ int iRepr = Gia_ObjRepr( p, i );
+ if ( Gia_ObjIsXor(pObj) )
+ Cec4_ObjSimXor( p, i );
+ else
+ Cec4_ObjSimAnd( p, i );
+ if ( iRepr == GIA_VOID || p->pReprs[iRepr].fColorA || Cec4_ObjSimEqual(p, iRepr, i) )
+ continue;
+ p->pReprs[iRepr].fColorA = 1;
+ Vec_IntPush( pMan->vRefClasses, iRepr );
+ }
+ pMan->timeSim += Abc_Clock() - clk;
+ clk = Abc_Clock();
+ Cec4_RefineClasses( p, pMan, pMan->vRefClasses );
+ pMan->timeRefine += Abc_Clock() - clk;
+}
+void Cec4_ManSimulate_rec( Gia_Man_t * p, Cec4_Man_t * pMan, int iObj )
+{
+ Gia_Obj_t * pObj;
+ if ( !iObj || Vec_IntEntry(pMan->vCexStamps, iObj) == p->iPatsPi )
+ return;
+ Vec_IntWriteEntry( pMan->vCexStamps, iObj, p->iPatsPi );
+ pObj = Gia_ManObj(p, iObj);
+ if ( Gia_ObjIsCi(pObj) )
+ return;
+ assert( Gia_ObjIsAnd(pObj) );
+ Cec4_ManSimulate_rec( p, pMan, Gia_ObjFaninId0(pObj, iObj) );
+ Cec4_ManSimulate_rec( p, pMan, Gia_ObjFaninId1(pObj, iObj) );
+ if ( Gia_ObjIsXor(pObj) )
+ Cec4_ObjSimXor( p, iObj );
+ else
+ Cec4_ObjSimAnd( p, iObj );
+}
+void Cec4_ManSimAlloc( Gia_Man_t * p, int nWords )
+{
+ Vec_WrdFreeP( &p->vSims );
+ Vec_WrdFreeP( &p->vSimsPi );
+ p->vSims = Vec_WrdStart( Gia_ManObjNum(p) * nWords );
+ p->vSimsPi = Vec_WrdStart( (Gia_ManCiNum(p) + 1) * nWords );
+ p->nSimWords = nWords;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Creating initial equivalence classes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Cec4_ManPrintTfiConeStats( Gia_Man_t * p )
+{
+ Vec_Int_t * vRoots = Vec_IntAlloc( 100 );
+ Vec_Int_t * vNodes = Vec_IntAlloc( 100 );
+ Vec_Int_t * vLeaves = Vec_IntAlloc( 100 );
+ int i, k;
+ Gia_ManForEachClass0( p, i )
+ {
+ Vec_IntClear( vRoots );
+ if ( i % 100 != 0 )
+ continue;
+ Vec_IntPush( vRoots, i );
+ Gia_ClassForEachObj1( p, i, k )
+ Vec_IntPush( vRoots, k );
+ Gia_ManCollectTfi( p, vRoots, vNodes );
+ printf( "Class %6d : ", i );
+ printf( "Roots = %6d ", Vec_IntSize(vRoots) );
+ printf( "Nodes = %6d ", Vec_IntSize(vNodes) );
+ printf( "\n" );
+ }
+ Vec_IntFree( vRoots );
+ Vec_IntFree( vNodes );
+ Vec_IntFree( vLeaves );
+}
+void Cec4_ManPrintStats( Gia_Man_t * p, Cec_ParFra_t * pPars, Cec4_Man_t * pMan, int fSim )
+{
+ static abctime clk = 0;
+ abctime clkThis = 0;
+ int i, nLits, Counter = 0, Counter0 = 0, CounterX = 0;
+ if ( !pPars->fVerbose )
+ return;
+ if ( pMan->nItersSim + pMan->nItersSat )
+ clkThis = Abc_Clock() - clk;
+ clk = Abc_Clock();
+ for ( i = 0; i < Gia_ManObjNum(p); i++ )
+ {
+ if ( Gia_ObjIsHead(p, i) )
+ Counter++;
+ else if ( Gia_ObjIsConst(p, i) )
+ Counter0++;
+ else if ( Gia_ObjIsNone(p, i) )
+ CounterX++;
+ }
+ nLits = Gia_ManObjNum(p) - Counter - CounterX;
+ if ( fSim )
+ {
+ printf( "Sim %4d : ", pMan->nItersSim++ + pMan->nItersSat );
+ printf( "%6.2f %% ", 100.0*nLits/Gia_ManCandNum(p) );
+ }
+ else
+ {
+ printf( "SAT %4d : ", pMan->nItersSim + pMan->nItersSat++ );
+ printf( "%6.2f %% ", 100.0*pMan->nAndNodes/Gia_ManAndNum(p) );
+ }
+ printf( "P =%7d ", pMan ? pMan->nSatUnsat : 0 );
+ printf( "D =%7d ", pMan ? pMan->nSatSat : 0 );
+ printf( "F =%8d ", pMan ? pMan->nSatUndec : 0 );
+ //printf( "Last =%6d ", pMan ? pMan->iLastConst : 0 );
+ Abc_Print( 1, "cst =%9d cls =%8d lit =%9d ", Counter0, Counter, nLits );
+ Abc_PrintTime( 1, "Time", clkThis );
+}
+void Cec4_ManPrintClasses2( Gia_Man_t * p )
+{
+ int i, k;
+ Gia_ManForEachClass0( p, i )
+ {
+ printf( "Class %d : ", i );
+ Gia_ClassForEachObj1( p, i, k )
+ printf( "%d ", k );
+ printf( "\n" );
+ }
+}
+void Cec4_ManPrintClasses( Gia_Man_t * p )
+{
+ int k, Count = 0;
+ Gia_ClassForEachObj1( p, 0, k )
+ Count++;
+ printf( "Const0 class has %d entries.\n", Count );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Verify counter-example.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Cec4_ManVerify_rec( Gia_Man_t * p, int iObj, sat_solver * pSat )
+{
+ int Value0, Value1;
+ Gia_Obj_t * pObj = Gia_ManObj( p, iObj );
+ if ( iObj == 0 ) return 0;
+ if ( Gia_ObjIsTravIdCurrentId(p, iObj) )
+ return pObj->fMark1;
+ Gia_ObjSetTravIdCurrentId(p, iObj);
+ if ( Gia_ObjIsCi(pObj) )
+ return pObj->fMark1 = sat_solver_read_cex_varvalue(pSat, Cec4_ObjSatId(p, pObj));
+ assert( Gia_ObjIsAnd(pObj) );
+ Value0 = Cec4_ManVerify_rec( p, Gia_ObjFaninId0(pObj, iObj), pSat ) ^ Gia_ObjFaninC0(pObj);
+ Value1 = Cec4_ManVerify_rec( p, Gia_ObjFaninId1(pObj, iObj), pSat ) ^ Gia_ObjFaninC1(pObj);
+ return pObj->fMark1 = Gia_ObjIsXor(pObj) ? Value0 ^ Value1 : Value0 & Value1;
+}
+void Cec4_ManVerify( Gia_Man_t * p, int iObj0, int iObj1, int fPhase, sat_solver * pSat )
+{
+ int Value0, Value1;
+ Gia_ManIncrementTravId( p );
+ Value0 = Cec4_ManVerify_rec( p, iObj0, pSat );
+ Value1 = Cec4_ManVerify_rec( p, iObj1, pSat );
+ if ( (Value0 ^ Value1) == fPhase )
+ printf( "CEX verification FAILED for obj %d and obj %d.\n", iObj0, iObj1 );
+// else
+// printf( "CEX verification succeeded for obj %d and obj %d.\n", iObj0, iObj1 );;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Verify counter-example.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Cec4_ManCexVerify_rec( Gia_Man_t * p, int iObj )
+{
+ int Value0, Value1;
+ Gia_Obj_t * pObj = Gia_ManObj( p, iObj );
+ if ( iObj == 0 ) return 0;
+ if ( Gia_ObjIsTravIdCurrentId(p, iObj) )
+ return pObj->fMark1;
+ Gia_ObjSetTravIdCurrentId(p, iObj);
+ if ( Gia_ObjIsCi(pObj) )
+ return pObj->fMark1 = Cec4_ObjSimGetInputBit(p, iObj);
+ assert( Gia_ObjIsAnd(pObj) );
+ Value0 = Cec4_ManCexVerify_rec( p, Gia_ObjFaninId0(pObj, iObj) ) ^ Gia_ObjFaninC0(pObj);
+ Value1 = Cec4_ManCexVerify_rec( p, Gia_ObjFaninId1(pObj, iObj) ) ^ Gia_ObjFaninC1(pObj);
+ return pObj->fMark1 = Gia_ObjIsXor(pObj) ? Value0 ^ Value1 : Value0 & Value1;
+}
+void Cec4_ManCexVerify( Gia_Man_t * p, int iObj0, int iObj1, int fPhase )
+{
+ int Value0, Value1;
+ Gia_ManIncrementTravId( p );
+ Value0 = Cec4_ManCexVerify_rec( p, iObj0 );
+ Value1 = Cec4_ManCexVerify_rec( p, iObj1 );
+ if ( (Value0 ^ Value1) == fPhase )
+ printf( "CEX verification FAILED for obj %d and obj %d.\n", iObj0, iObj1 );
+// else
+// printf( "CEX verification succeeded for obj %d and obj %d.\n", iObj0, iObj1 );;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Packs simulation patterns into array of simulation info.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+*************************************`**********************************/
+void Cec4_ManPackAddPatterns( Gia_Man_t * p, int iBit, Vec_Int_t * vLits )
+{
+ int k, Limit = Abc_MinInt( Vec_IntSize(vLits), 64 * p->nSimWords - 1 );
+ for ( k = 0; k < Limit; k++ )
+ {
+ int i, Lit, iBitLocal = (iBit + k + 1) % Limit + 1;
+ assert( iBitLocal > 0 && iBitLocal < 64 * p->nSimWords );
+ Vec_IntForEachEntry( vLits, Lit, i )
+ {
+ word * pInfo = Vec_WrdEntryP( p->vSims, p->nSimWords * Abc_Lit2Var(Lit) );
+ word * pPres = Vec_WrdEntryP( p->vSimsPi, p->nSimWords * Abc_Lit2Var(Lit) );
+ if ( Abc_InfoHasBit( (unsigned *)pPres, iBitLocal ) )
+ continue;
+ if ( Abc_InfoHasBit( (unsigned *)pInfo, iBitLocal ) != Abc_LitIsCompl(Lit ^ (i == k)) )
+ Abc_InfoXorBit( (unsigned *)pInfo, iBitLocal );
+ }
+ }
+}
+int Cec4_ManPackAddPatternTry( Gia_Man_t * p, int iBit, Vec_Int_t * vLits )
+{
+ int i, Lit;
+ assert( p->iPatsPi > 0 && p->iPatsPi < 64 * p->nSimWords );
+ Vec_IntForEachEntry( vLits, Lit, i )
+ {
+ word * pInfo = Vec_WrdEntryP( p->vSims, p->nSimWords * Abc_Lit2Var(Lit) );
+ word * pPres = Vec_WrdEntryP( p->vSimsPi, p->nSimWords * Abc_Lit2Var(Lit) );
+ if ( Abc_InfoHasBit( (unsigned *)pPres, iBit ) &&
+ Abc_InfoHasBit( (unsigned *)pInfo, iBit ) != Abc_LitIsCompl(Lit) )
+ return 0;
+ }
+ Vec_IntForEachEntry( vLits, Lit, i )
+ {
+ word * pInfo = Vec_WrdEntryP( p->vSims, p->nSimWords * Abc_Lit2Var(Lit) );
+ word * pPres = Vec_WrdEntryP( p->vSimsPi, p->nSimWords * Abc_Lit2Var(Lit) );
+ Abc_InfoSetBit( (unsigned *)pPres, iBit );
+ if ( Abc_InfoHasBit( (unsigned *)pInfo, iBit ) != Abc_LitIsCompl(Lit) )
+ Abc_InfoXorBit( (unsigned *)pInfo, iBit );
+ }
+ return 1;
+}
+int Cec4_ManPackAddPattern( Gia_Man_t * p, Vec_Int_t * vLits, int fExtend )
+{
+ int k;
+ for ( k = 1; k < 64 * p->nSimWords - 1; k++ )
+ {
+ if ( ++p->iPatsPi == 64 * p->nSimWords - 1 )
+ p->iPatsPi = 1;
+ if ( Cec4_ManPackAddPatternTry( p, p->iPatsPi, vLits ) )
+ {
+ if ( fExtend )
+ Cec4_ManPackAddPatterns( p, p->iPatsPi, vLits );
+ break;
+ }
+ }
+ if ( k == 64 * p->nSimWords - 1 )
+ {
+ p->iPatsPi = k;
+ if ( !Cec4_ManPackAddPatternTry( p, p->iPatsPi, vLits ) )
+ printf( "Internal error.\n" );
+ else if ( fExtend )
+ Cec4_ManPackAddPatterns( p, p->iPatsPi, vLits );
+ return 64 * p->nSimWords;
+ }
+ return k;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Generates counter-examples to refine the candidate equivalences.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Cec4_ObjFan0IsAssigned( Gia_Obj_t * pObj )
+{
+ return Gia_ObjFanin0(pObj)->fMark0 || Gia_ObjFanin0(pObj)->fMark1;
+}
+static inline int Cec4_ObjFan1IsAssigned( Gia_Obj_t * pObj )
+{
+ return Gia_ObjFanin1(pObj)->fMark0 || Gia_ObjFanin1(pObj)->fMark1;
+}
+static inline int Cec4_ObjFan0HasValue( Gia_Obj_t * pObj, int v )
+{
+ return (v ^ Gia_ObjFaninC0(pObj)) ? Gia_ObjFanin0(pObj)->fMark1 : Gia_ObjFanin0(pObj)->fMark0;
+}
+static inline int Cec4_ObjFan1HasValue( Gia_Obj_t * pObj, int v )
+{
+ return (v ^ Gia_ObjFaninC1(pObj)) ? Gia_ObjFanin1(pObj)->fMark1 : Gia_ObjFanin1(pObj)->fMark0;
+}
+static inline int Cec4_ObjObjIsImpliedValue( Gia_Obj_t * pObj, int v )
+{
+ assert( !pObj->fMark0 && !pObj->fMark1 ); // not visited
+ if ( v )
+ return Cec4_ObjFan0HasValue(pObj, 1) && Cec4_ObjFan1HasValue(pObj, 1);
+ return Cec4_ObjFan0HasValue(pObj, 0) || Cec4_ObjFan1HasValue(pObj, 0);
+}
+static inline int Cec4_ObjFan0IsImpliedValue( Gia_Obj_t * pObj, int v )
+{
+ return Gia_ObjIsAnd(Gia_ObjFanin0(pObj)) && Cec4_ObjObjIsImpliedValue( Gia_ObjFanin0(pObj), v ^ Gia_ObjFaninC0(pObj) );
+}
+static inline int Cec4_ObjFan1IsImpliedValue( Gia_Obj_t * pObj, int v )
+{
+ return Gia_ObjIsAnd(Gia_ObjFanin1(pObj)) && Cec4_ObjObjIsImpliedValue( Gia_ObjFanin1(pObj), v ^ Gia_ObjFaninC1(pObj) );
+}
+int Cec4_ManGeneratePatterns_rec( Gia_Man_t * p, Gia_Obj_t * pObj, int Value, Vec_Int_t * vPat, Vec_Int_t * vVisit )
+{
+ Gia_Obj_t * pFan0, * pFan1;
+ assert( !pObj->fMark0 && !pObj->fMark1 ); // not visited
+ if ( Value ) pObj->fMark1 = 1; else pObj->fMark0 = 1;
+ Vec_IntPush( vVisit, Gia_ObjId(p, pObj) );
+ if ( Gia_ObjIsCi(pObj) )
+ {
+ Vec_IntPush( vPat, Abc_Var2Lit(Gia_ObjId(p, pObj), Value) );
+ return 1;
+ }
+ assert( Gia_ObjIsAnd(pObj) );
+ pFan0 = Gia_ObjFanin0(pObj);
+ pFan1 = Gia_ObjFanin1(pObj);
+ if ( Gia_ObjIsXor(pObj) )
+ {
+ int Ass0 = Cec4_ObjFan0IsAssigned(pObj);
+ int Ass1 = Cec4_ObjFan1IsAssigned(pObj);
+ assert( Gia_ObjFaninC0(pObj) == 0 && Gia_ObjFaninC1(pObj) == 0 );
+ if ( Ass0 && Ass1 )
+ return Value == (Cec4_ObjFan0HasValue(pObj, 1) ^ Cec4_ObjFan1HasValue(pObj, 1));
+ if ( Ass0 )
+ {
+ int ValueInt = Value ^ Cec4_ObjFan0HasValue(pObj, 1);
+ if ( !Cec4_ManGeneratePatterns_rec(p, pFan1, ValueInt, vPat, vVisit) )
+ return 0;
+ }
+ else if ( Ass1 )
+ {
+ int ValueInt = Value ^ Cec4_ObjFan1HasValue(pObj, 1);
+ if ( !Cec4_ManGeneratePatterns_rec(p, pFan0, ValueInt, vPat, vVisit) )
+ return 0;
+ }
+ else if ( Abc_Random(0) & 1 )
+ {
+ if ( !Cec4_ManGeneratePatterns_rec(p, pFan0, 0, vPat, vVisit) )
+ return 0;
+ if ( Cec4_ObjFan1HasValue(pObj, !Value) || (!Cec4_ObjFan1HasValue(pObj, Value) && !Cec4_ManGeneratePatterns_rec(p, pFan1, Value, vPat, vVisit)) )
+ return 0;
+ }
+ else
+ {
+ if ( !Cec4_ManGeneratePatterns_rec(p, pFan0, 1, vPat, vVisit) )
+ return 0;
+ if ( Cec4_ObjFan1HasValue(pObj, Value) || (!Cec4_ObjFan1HasValue(pObj, !Value) && !Cec4_ManGeneratePatterns_rec(p, pFan1, !Value, vPat, vVisit)) )
+ return 0;
+ }
+ assert( Value == (Cec4_ObjFan0HasValue(pObj, 1) ^ Cec4_ObjFan1HasValue(pObj, 1)) );
+ return 1;
+ }
+ else if ( Value )
+ {
+ if ( Cec4_ObjFan0HasValue(pObj, 0) || Cec4_ObjFan1HasValue(pObj, 0) )
+ return 0;
+ if ( !Cec4_ObjFan0HasValue(pObj, 1) && !Cec4_ManGeneratePatterns_rec(p, pFan0, !Gia_ObjFaninC0(pObj), vPat, vVisit) )
+ return 0;
+ if ( !Cec4_ObjFan1HasValue(pObj, 1) && !Cec4_ManGeneratePatterns_rec(p, pFan1, !Gia_ObjFaninC1(pObj), vPat, vVisit) )
+ return 0;
+ assert( Cec4_ObjFan0HasValue(pObj, 1) && Cec4_ObjFan1HasValue(pObj, 1) );
+ return 1;
+ }
+ else
+ {
+ if ( Cec4_ObjFan0HasValue(pObj, 1) && Cec4_ObjFan1HasValue(pObj, 1) )
+ return 0;
+ if ( Cec4_ObjFan0HasValue(pObj, 0) || Cec4_ObjFan1HasValue(pObj, 0) )
+ return 1;
+ if ( Cec4_ObjFan0HasValue(pObj, 1) )
+ {
+ if ( !Cec4_ManGeneratePatterns_rec(p, pFan1, Gia_ObjFaninC1(pObj), vPat, vVisit) )
+ return 0;
+ }
+ else if ( Cec4_ObjFan1HasValue(pObj, 1) )
+ {
+ if ( !Cec4_ManGeneratePatterns_rec(p, pFan0, Gia_ObjFaninC0(pObj), vPat, vVisit) )
+ return 0;
+ }
+ else
+ {
+ if ( Cec4_ObjFan0IsImpliedValue( pObj, 0 ) )
+ {
+ if ( !Cec4_ManGeneratePatterns_rec(p, pFan0, Gia_ObjFaninC0(pObj), vPat, vVisit) )
+ return 0;
+ }
+ else if ( Cec4_ObjFan1IsImpliedValue( pObj, 0 ) )
+ {
+ if ( !Cec4_ManGeneratePatterns_rec(p, pFan1, Gia_ObjFaninC1(pObj), vPat, vVisit) )
+ return 0;
+ }
+ else if ( Cec4_ObjFan0IsImpliedValue( pObj, 1 ) )
+ {
+ if ( !Cec4_ManGeneratePatterns_rec(p, pFan1, Gia_ObjFaninC1(pObj), vPat, vVisit) )
+ return 0;
+ }
+ else if ( Cec4_ObjFan1IsImpliedValue( pObj, 1 ) )
+ {
+ if ( !Cec4_ManGeneratePatterns_rec(p, pFan0, Gia_ObjFaninC0(pObj), vPat, vVisit) )
+ return 0;
+ }
+ else if ( Abc_Random(0) & 1 )
+ {
+ if ( !Cec4_ManGeneratePatterns_rec(p, pFan1, Gia_ObjFaninC1(pObj), vPat, vVisit) )
+ return 0;
+ }
+ else
+ {
+ if ( !Cec4_ManGeneratePatterns_rec(p, pFan0, Gia_ObjFaninC0(pObj), vPat, vVisit) )
+ return 0;
+ }
+ }
+ assert( Cec4_ObjFan0HasValue(pObj, 0) || Cec4_ObjFan1HasValue(pObj, 0) );
+ return 1;
+ }
+}
+int Cec4_ManGeneratePatternOne( Gia_Man_t * p, int iRepr, int iReprVal, int iCand, int iCandVal, Vec_Int_t * vPat, Vec_Int_t * vVisit )
+{
+ int Res, k;
+ Gia_Obj_t * pObj;
+ assert( iCand > 0 );
+ if ( !iRepr && iReprVal )
+ return 0;
+ Vec_IntClear( vPat );
+ Vec_IntClear( vVisit );
+ //Gia_ManForEachObj( p, pObj, k )
+ // assert( !pObj->fMark0 && !pObj->fMark1 );
+ Res = (!iRepr || Cec4_ManGeneratePatterns_rec(p, Gia_ManObj(p, iRepr), iReprVal, vPat, vVisit)) && Cec4_ManGeneratePatterns_rec(p, Gia_ManObj(p, iCand), iCandVal, vPat, vVisit);
+ Gia_ManForEachObjVec( vVisit, p, pObj, k )
+ pObj->fMark0 = pObj->fMark1 = 0;
+ return Res;
+}
+void Cec4_ManCandIterStart( Cec4_Man_t * p )
+{
+ int i, * pArray;
+ assert( p->iPosWrite == 0 );
+ assert( p->iPosRead == 0 );
+ assert( Vec_IntSize(p->vCands) == 0 );
+ for ( i = 1; i < Gia_ManObjNum(p->pAig); i++ )
+ if ( Gia_ObjRepr(p->pAig, i) != GIA_VOID )
+ Vec_IntPush( p->vCands, i );
+ pArray = Vec_IntArray( p->vCands );
+ for ( i = 0; i < Vec_IntSize(p->vCands); i++ )
+ {
+ int iNew = Abc_Random(0) % Vec_IntSize(p->vCands);
+ ABC_SWAP( int, pArray[i], pArray[iNew] );
+ }
+}
+int Cec4_ManCandIterNext( Cec4_Man_t * p )
+{
+ while ( Vec_IntSize(p->vCands) > 0 )
+ {
+ int fStop, iCand = Vec_IntEntry( p->vCands, p->iPosRead );
+ if ( (fStop = (Gia_ObjRepr(p->pAig, iCand) != GIA_VOID)) )
+ Vec_IntWriteEntry( p->vCands, p->iPosWrite++, iCand );
+ if ( ++p->iPosRead == Vec_IntSize(p->vCands) )
+ {
+ Vec_IntShrink( p->vCands, p->iPosWrite );
+ p->iPosWrite = 0;
+ p->iPosRead = 0;
+ }
+ if ( fStop )
+ return iCand;
+ }
+ return 0;
+}
+int Cec4_ManGeneratePatterns( Cec4_Man_t * p )
+{
+ abctime clk = Abc_Clock();
+ int i, iCand, nPats = 100 * 64 * p->pAig->nSimWords, CountPat = 0, Packs = 0;
+ //int iRepr;
+ //Vec_IntForEachEntryDouble( p->vDisprPairs, iRepr, iCand, i )
+ // if ( iRepr == Gia_ObjRepr(p->pAig, iCand) )
+ // printf( "Pair %6d (%6d, %6d) (new repr = %9d) is FAILED to disprove.\n", i, iRepr, iCand, Gia_ObjRepr(p->pAig, iCand) );
+ // else
+ // printf( "Pair %6d (%6d, %6d) (new repr = %9d) is disproved.\n", i, iRepr, iCand, Gia_ObjRepr(p->pAig, iCand) );
+ //Vec_IntClear( p->vDisprPairs );
+ p->pAig->iPatsPi = 0;
+ Vec_WrdFill( p->pAig->vSimsPi, Vec_WrdSize(p->pAig->vSimsPi), 0 );
+ for ( i = 0; i < nPats; i++ )
+ if ( (iCand = Cec4_ManCandIterNext(p)) )
+ {
+ int iRepr = Gia_ObjRepr( p->pAig, iCand );
+ int iCandVal = Gia_ManObj(p->pAig, iCand)->fPhase;
+ int iReprVal = Gia_ManObj(p->pAig, iRepr)->fPhase;
+ int Res = Cec4_ManGeneratePatternOne( p->pAig, iRepr, iReprVal, iCand, !iCandVal, p->vPat, p->vVisit );
+ if ( !Res )
+ Res = Cec4_ManGeneratePatternOne( p->pAig, iRepr, !iReprVal, iCand, iCandVal, p->vPat, p->vVisit );
+ if ( Res )
+ {
+ int Ret = Cec4_ManPackAddPattern( p->pAig, p->vPat, 1 );
+ if ( p->pAig->vPats )
+ {
+ Vec_IntPush( p->pAig->vPats, Vec_IntSize(p->vPat)+2 );
+ Vec_IntAppend( p->pAig->vPats, p->vPat );
+ Vec_IntPush( p->pAig->vPats, -1 );
+ }
+ //Vec_IntPushTwo( p->vDisprPairs, iRepr, iCand );
+ Packs += Ret;
+ if ( Ret == 64 * p->pAig->nSimWords )
+ break;
+ if ( ++CountPat == 8 * 64 * p->pAig->nSimWords )
+ break;
+ //Cec4_ManCexVerify( p->pAig, iRepr, iCand, iReprVal ^ iCandVal );
+ //Gia_ManCleanMark01( p->pAig );
+ }
+ }
+ p->timeGenPats += Abc_Clock() - clk;
+ p->nSatSat += CountPat;
+ //printf( "%3d : %6.2f %% : Generated %6d CEXs after trying %6d pairs. Ave packs = %9.2f Ave tries = %9.2f (Limit = %9.2f)\n",
+ // p->nItersSim++, 100.0*Vec_IntSize(p->vCands)/Gia_ManAndNum(p->pAig),
+ // CountPat, i, (float)Packs / Abc_MaxInt(1, CountPat), (float)i / Abc_MaxInt(1, CountPat), (float)nPats / p->pPars->nItersMax );
+ return CountPat >= i / p->pPars->nItersMax;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Internal simulation APIs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Cec4_ManSatSolverRecycle( Cec4_Man_t * p )
+{
+ Gia_Obj_t * pObj;
+ int i;
+ //printf( "Solver size = %d.\n", sat_solver_varnum(p->pSat) );
+ p->nRecycles++;
+ p->nCallsSince = 0;
+ sat_solver_reset( p->pSat );
+ // clean mapping of AigIds into SatIds
+ Gia_ManForEachObjVec( &p->pNew->vSuppVars, p->pNew, pObj, i )
+ Cec4_ObjCleanSatId( p->pNew, pObj );
+ Vec_IntClear( &p->pNew->vSuppVars ); // AigIds for which SatId is defined
+ Vec_IntClear( &p->pNew->vCopiesTwo ); // pairs (CiAigId, SatId)
+ Vec_IntClear( &p->pNew->vVarMap ); // mapping of SatId into AigId
+}
+int Cec4_ManSolveTwo( Cec4_Man_t * p, int iObj0, int iObj1, int fPhase, int * pfEasy, int fVerbose, int fEffort )
+{
+ abctime clk;
+ int nBTLimit = fEffort ? p->pPars->nBTLimitPo : (Vec_BitEntry(p->vFails, iObj0) || Vec_BitEntry(p->vFails, iObj1)) ? Abc_MaxInt(1, p->pPars->nBTLimit/10) : p->pPars->nBTLimit;
+ int nConfEnd, nConfBeg, status, iVar0, iVar1, Lits[2];
+ int UnsatConflicts[3] = {0};
+ //printf( "%d ", nBTLimit );
+ if ( iObj1 < iObj0 )
+ iObj1 ^= iObj0, iObj0 ^= iObj1, iObj1 ^= iObj0;
+ assert( iObj0 < iObj1 );
+ *pfEasy = 0;
+ // check if SAT solver needs recycling
+ p->nCallsSince++;
+ if ( p->nCallsSince > p->pPars->nCallsRecycle &&
+ Vec_IntSize(&p->pNew->vSuppVars) > p->pPars->nSatVarMax && p->pPars->nSatVarMax )
+ Cec4_ManSatSolverRecycle( p );
+ // add more logic to the solver
+ if ( !iObj0 && Cec4_ObjSatId(p->pNew, Gia_ManConst0(p->pNew)) == -1 )
+ Cec4_ObjSetSatId( p->pNew, Gia_ManConst0(p->pNew), sat_solver_addvar(p->pSat) );
+ clk = Abc_Clock();
+ iVar0 = Cec4_ObjGetCnfVar( p, iObj0 );
+ iVar1 = Cec4_ObjGetCnfVar( p, iObj1 );
+ if( p->pPars->jType > 0 )
+ {
+ sat_solver_start_new_round( p->pSat );
+ sat_solver_mark_cone( p->pSat, Cec4_ObjSatId(p->pNew, Gia_ManObj(p->pNew, iObj0)) );
+ sat_solver_mark_cone( p->pSat, Cec4_ObjSatId(p->pNew, Gia_ManObj(p->pNew, iObj1)) );
+ }
+ p->timeCnf += Abc_Clock() - clk;
+ // perform solving
+ Lits[0] = Abc_Var2Lit(iVar0, 1);
+ Lits[1] = Abc_Var2Lit(iVar1, fPhase);
+ sat_solver_set_conflict_budget( p->pSat, nBTLimit );
+ nConfBeg = sat_solver_conflictnum( p->pSat );
+ status = sat_solver_solve( p->pSat, Lits, 2 );
+ nConfEnd = sat_solver_conflictnum( p->pSat );
+ assert( nConfEnd >= nConfBeg );
+ if ( fVerbose )
+ {
+ if ( status == GLUCOSE_SAT )
+ {
+ p->nConflicts[0][0] += nConfEnd == nConfBeg;
+ p->nConflicts[0][1] += nConfEnd - nConfBeg;
+ p->nConflicts[0][2] = Abc_MaxInt(p->nConflicts[0][2], nConfEnd - nConfBeg);
+ *pfEasy = nConfEnd == nConfBeg;
+ }
+ else if ( status == GLUCOSE_UNSAT )
+ {
+ if ( iObj0 > 0 )
+ {
+ UnsatConflicts[0] = nConfEnd == nConfBeg;
+ UnsatConflicts[1] = nConfEnd - nConfBeg;
+ UnsatConflicts[2] = Abc_MaxInt(p->nConflicts[1][2], nConfEnd - nConfBeg);
+ }
+ else
+ {
+ p->nConflicts[1][0] += nConfEnd == nConfBeg;
+ p->nConflicts[1][1] += nConfEnd - nConfBeg;
+ p->nConflicts[1][2] = Abc_MaxInt(p->nConflicts[1][2], nConfEnd - nConfBeg);
+ *pfEasy = nConfEnd == nConfBeg;
+ }
+ }
+ }
+ if ( status == GLUCOSE_UNSAT && iObj0 > 0 )
+ {
+ Lits[0] = Abc_Var2Lit(iVar0, 0);
+ Lits[1] = Abc_Var2Lit(iVar1, !fPhase);
+ sat_solver_set_conflict_budget( p->pSat, nBTLimit );
+ nConfBeg = sat_solver_conflictnum( p->pSat );
+ status = sat_solver_solve( p->pSat, Lits, 2 );
+ nConfEnd = sat_solver_conflictnum( p->pSat );
+ assert( nConfEnd >= nConfBeg );
+ if ( fVerbose )
+ {
+ if ( status == GLUCOSE_SAT )
+ {
+ p->nConflicts[0][0] += nConfEnd == nConfBeg;
+ p->nConflicts[0][1] += nConfEnd - nConfBeg;
+ p->nConflicts[0][2] = Abc_MaxInt(p->nConflicts[0][2], nConfEnd - nConfBeg);
+ *pfEasy = nConfEnd == nConfBeg;
+ }
+ else if ( status == GLUCOSE_UNSAT )
+ {
+ UnsatConflicts[0] &= nConfEnd == nConfBeg;
+ UnsatConflicts[1] += nConfEnd - nConfBeg;
+ UnsatConflicts[2] = Abc_MaxInt(p->nConflicts[1][2], nConfEnd - nConfBeg);
+
+ p->nConflicts[1][0] += UnsatConflicts[0];
+ p->nConflicts[1][1] += UnsatConflicts[1];
+ p->nConflicts[1][2] = Abc_MaxInt(p->nConflicts[1][2], UnsatConflicts[2]);
+ *pfEasy = UnsatConflicts[0];
+ }
+ }
+ }
+ //if ( status == GLUCOSE_UNDEC )
+ // printf( "* " );
+ return status;
+}
+int Cec4_ManSweepNode( Cec4_Man_t * p, int iObj, int iRepr )
+{
+ abctime clk = Abc_Clock();
+ int i, IdAig, IdSat, status, fEasy, RetValue = 1;
+ Gia_Obj_t * pObj = Gia_ManObj( p->pAig, iObj );
+ Gia_Obj_t * pRepr = Gia_ManObj( p->pAig, iRepr );
+ int fCompl = Abc_LitIsCompl(pObj->Value) ^ Abc_LitIsCompl(pRepr->Value) ^ pObj->fPhase ^ pRepr->fPhase;
+ int fEffort = p->vCoDrivers ? Vec_BitEntry(p->vCoDrivers, iObj) || Vec_BitEntry(p->vCoDrivers, iRepr) : 0;
+ status = Cec4_ManSolveTwo( p, Abc_Lit2Var(pRepr->Value), Abc_Lit2Var(pObj->Value), fCompl, &fEasy, p->pPars->fVerbose, fEffort );
+ if ( status == GLUCOSE_SAT )
+ {
+ int iLit;
+ //int iPatsOld = p->pAig->iPatsPi;
+ //printf( "Disproved: %d == %d.\n", Abc_Lit2Var(pRepr->Value), Abc_Lit2Var(pObj->Value) );
+ p->nSatSat++;
+ p->nPatterns++;
+ Vec_IntClear( p->vPat );
+ if ( p->pPars->jType == 0 )
+ {
+ Vec_IntForEachEntryDouble( &p->pNew->vCopiesTwo, IdAig, IdSat, i )
+ Vec_IntPush( p->vPat, Abc_Var2Lit(IdAig, sat_solver_read_cex_varvalue(p->pSat, IdSat)) );
+ }
+ else
+ {
+ int * pCex = sat_solver_read_cex( p->pSat );
+ int * pMap = Vec_IntArray(&p->pNew->vVarMap);
+ for ( i = 0; i < pCex[0]; )
+ Vec_IntPush( p->vPat, Abc_Lit2LitV(pMap, Abc_LitNot(pCex[++i])) );
+ }
+ assert( p->pAig->iPatsPi >= 0 && p->pAig->iPatsPi < 64 * p->pAig->nSimWords - 1 );
+ p->pAig->iPatsPi++;
+ Vec_IntForEachEntry( p->vPat, iLit, i )
+ Cec4_ObjSimSetInputBit( p->pAig, Abc_Lit2Var(iLit), Abc_LitIsCompl(iLit) );
+ if ( p->pAig->vPats )
+ {
+ Vec_IntPush( p->pAig->vPats, Vec_IntSize(p->vPat)+2 );
+ Vec_IntAppend( p->pAig->vPats, p->vPat );
+ Vec_IntPush( p->pAig->vPats, -1 );
+ }
+ //Cec4_ManPackAddPattern( p->pAig, p->vPat, 0 );
+ //assert( iPatsOld + 1 == p->pAig->iPatsPi );
+ if ( fEasy )
+ p->timeSatSat0 += Abc_Clock() - clk;
+ else
+ p->timeSatSat += Abc_Clock() - clk;
+ RetValue = 0;
+ // this is not needed, but we keep it here anyway, because it takes very little time
+ //Cec4_ManVerify( p->pNew, Abc_Lit2Var(pRepr->Value), Abc_Lit2Var(pObj->Value), fCompl, p->pSat );
+ // resimulated once in a while
+ if ( p->pAig->iPatsPi == 64 * p->pAig->nSimWords - 2 )
+ {
+ abctime clk2 = Abc_Clock();
+ Cec4_ManSimulate( p->pAig, p );
+ //printf( "FasterSmall = %d. FasterBig = %d.\n", p->nFaster[0], p->nFaster[1] );
+ p->nFaster[0] = p->nFaster[1] = 0;
+ //if ( p->nSatSat && p->nSatSat % 100 == 0 )
+ Cec4_ManPrintStats( p->pAig, p->pPars, p, 0 );
+ Vec_IntFill( p->vCexStamps, Gia_ManObjNum(p->pAig), 0 );
+ p->pAig->iPatsPi = 0;
+ Vec_WrdFill( p->pAig->vSimsPi, Vec_WrdSize(p->pAig->vSimsPi), 0 );
+ p->timeResimGlo += Abc_Clock() - clk2;
+ }
+ }
+ else if ( status == GLUCOSE_UNSAT )
+ {
+ //printf( "Proved: %d == %d.\n", Abc_Lit2Var(pRepr->Value), Abc_Lit2Var(pObj->Value) );
+ p->nSatUnsat++;
+ pObj->Value = Abc_LitNotCond( pRepr->Value, fCompl );
+ Gia_ObjSetProved( p->pAig, iObj );
+ if ( iRepr == 0 )
+ p->iLastConst = iObj;
+ if ( fEasy )
+ p->timeSatUnsat0 += Abc_Clock() - clk;
+ else
+ p->timeSatUnsat += Abc_Clock() - clk;
+ RetValue = 1;
+ }
+ else
+ {
+ p->nSatUndec++;
+ assert( status == GLUCOSE_UNDEC );
+ Gia_ObjSetFailed( p->pAig, iObj );
+ Vec_BitWriteEntry( p->vFails, iObj, 1 );
+ //if ( iRepr )
+ //Vec_BitWriteEntry( p->vFails, iRepr, 1 );
+ p->timeSatUndec += Abc_Clock() - clk;
+ RetValue = 2;
+ }
+ return RetValue;
+}
+Gia_Obj_t * Cec4_ManFindRepr( Gia_Man_t * p, Cec4_Man_t * pMan, int iObj )
+{
+ abctime clk = Abc_Clock();
+ int iMem, iRepr;
+ assert( Gia_ObjHasRepr(p, iObj) );
+ assert( !Gia_ObjProved(p, iObj) );
+ iRepr = Gia_ObjRepr(p, iObj);
+ assert( iRepr != iObj );
+ assert( !Gia_ObjProved(p, iRepr) );
+ Cec4_ManSimulate_rec( p, pMan, iObj );
+ Cec4_ManSimulate_rec( p, pMan, iRepr );
+ if ( Cec4_ObjSimEqual(p, iObj, iRepr) )
+ {
+ pMan->timeResimLoc += Abc_Clock() - clk;
+ return Gia_ManObj(p, iRepr);
+ }
+ Gia_ClassForEachObj1( p, iRepr, iMem )
+ {
+ if ( iObj == iMem )
+ break;
+ if ( Gia_ObjProved(p, iMem) || Gia_ObjFailed(p, iMem) )
+ continue;
+ Cec4_ManSimulate_rec( p, pMan, iMem );
+ if ( Cec4_ObjSimEqual(p, iObj, iMem) )
+ {
+ pMan->nFaster[0]++;
+ pMan->timeResimLoc += Abc_Clock() - clk;
+ return Gia_ManObj(p, iMem);
+ }
+ }
+ pMan->nFaster[1]++;
+ pMan->timeResimLoc += Abc_Clock() - clk;
+ return NULL;
+}
+int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** ppNew, int fSimOnly )
+{
+ Cec4_Man_t * pMan = Cec4_ManCreate( p, pPars );
+ Gia_Obj_t * pObj, * pRepr;
+ int i, fSimulate = 1;
+ if ( pPars->fVerbose )
+ printf( "Solver type = %d. Simulate %d words in %d rounds. SAT with %d confs. Recycle after %d SAT calls.\n",
+ pPars->jType, pPars->nWords, pPars->nRounds, pPars->nBTLimit, pPars->nCallsRecycle );
+
+ // this is currently needed to have a correct mapping
+ Gia_ManForEachCi( p, pObj, i )
+ assert( Gia_ObjId(p, pObj) == i+1 );
+
+ // check if any output trivially fails under all-0 pattern
+ Gia_ManRandom( 1 );
+ Gia_ManSetPhase( p );
+ if ( pPars->nLevelMax )
+ Gia_ManLevelNum(p);
+ //Gia_ManStaticFanoutStart( p );
+ if ( pPars->fCheckMiter )
+ {
+ Gia_ManForEachCo( p, pObj, i )
+ if ( pObj->fPhase )
+ {
+ p->pCexSeq = Cec4_ManDeriveCex( p, i, -1 );
+ goto finalize;
+ }
+ }
+
+ // simulate one round and create classes
+ Cec4_ManSimAlloc( p, pPars->nWords );
+ Cec4_ManSimulateCis( p );
+ Cec4_ManSimulate( p, pMan );
+ if ( pPars->fCheckMiter && !Cec4_ManSimulateCos(p) ) // cex detected
+ goto finalize;
+ if ( pPars->fVerbose )
+ Cec4_ManPrintStats( p, pPars, pMan, 1 );
+
+ // perform simulation
+ for ( i = 0; i < pPars->nRounds; i++ )
+ {
+ Cec4_ManSimulateCis( p );
+ Cec4_ManSimulate( p, pMan );
+ if ( pPars->fCheckMiter && !Cec4_ManSimulateCos(p) ) // cex detected
+ goto finalize;
+ if ( i && i % (pPars->nRounds / 5) == 0 && pPars->fVerbose )
+ Cec4_ManPrintStats( p, pPars, pMan, 1 );
+ }
+ if ( fSimOnly )
+ goto finalize;
+
+ // perform additional simulation
+ Cec4_ManCandIterStart( pMan );
+ for ( i = 0; fSimulate && i < pPars->nGenIters; i++ )
+ {
+ Cec4_ManSimulateCis( p );
+ fSimulate = Cec4_ManGeneratePatterns( pMan );
+ Cec4_ManSimulate( p, pMan );
+ if ( pPars->fCheckMiter && !Cec4_ManSimulateCos(p) ) // cex detected
+ goto finalize;
+ if ( i && i % 5 == 0 && pPars->fVerbose )
+ Cec4_ManPrintStats( p, pPars, pMan, 1 );
+ }
+ if ( i && i % 5 && pPars->fVerbose )
+ Cec4_ManPrintStats( p, pPars, pMan, 1 );
+
+ p->iPatsPi = 0;
+ Vec_WrdFill( p->vSimsPi, Vec_WrdSize(p->vSimsPi), 0 );
+ pMan->nSatSat = 0;
+ pMan->pNew = Cec4_ManStartNew( p );
+ Gia_ManForEachAnd( p, pObj, i )
+ {
+ Gia_Obj_t * pObjNew;
+ pMan->nAndNodes++;
+ if ( Gia_ObjIsXor(pObj) )
+ pObj->Value = Gia_ManHashXorReal( pMan->pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+ else
+ pObj->Value = Gia_ManHashAnd( pMan->pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+ if ( pPars->nLevelMax && Gia_ObjLevel(p, pObj) > pPars->nLevelMax )
+ continue;
+ pObjNew = Gia_ManObj( pMan->pNew, Abc_Lit2Var(pObj->Value) );
+ if ( Gia_ObjIsAnd(pObjNew) )
+ if ( Vec_BitEntry(pMan->vFails, Gia_ObjFaninId0(pObjNew, Abc_Lit2Var(pObj->Value))) ||
+ Vec_BitEntry(pMan->vFails, Gia_ObjFaninId1(pObjNew, Abc_Lit2Var(pObj->Value))) )
+ Vec_BitWriteEntry( pMan->vFails, Abc_Lit2Var(pObjNew->Value), 1 );
+ //if ( Gia_ObjIsAnd(pObjNew) )
+ // Gia_ObjSetAndLevel( pMan->pNew, pObjNew );
+ // select representative based on candidate equivalence classes
+ pRepr = Gia_ObjReprObj( p, i );
+ if ( pRepr == NULL )
+ continue;
+ if ( 1 ) // select representative based on recent counter-examples
+ {
+ pRepr = Cec4_ManFindRepr( p, pMan, i );
+ if ( pRepr == NULL )
+ continue;
+ }
+ if ( Abc_Lit2Var(pObj->Value) == Abc_Lit2Var(pRepr->Value) )
+ {
+ assert( (pObj->Value ^ pRepr->Value) == (pObj->fPhase ^ pRepr->fPhase) );
+ Gia_ObjSetProved( p, i );
+ if ( Gia_ObjId(p, pRepr) == 0 )
+ pMan->iLastConst = i;
+ continue;
+ }
+ if ( Cec4_ManSweepNode(pMan, i, Gia_ObjId(p, pRepr)) && Gia_ObjProved(p, i) )
+ pObj->Value = Abc_LitNotCond( pRepr->Value, pObj->fPhase ^ pRepr->fPhase );
+ }
+ if ( p->iPatsPi > 0 )
+ {
+ abctime clk2 = Abc_Clock();
+ Cec4_ManSimulate( p, pMan );
+ p->iPatsPi = 0;
+ Vec_IntFill( pMan->vCexStamps, Gia_ManObjNum(p), 0 );
+ pMan->timeResimGlo += Abc_Clock() - clk2;
+ }
+ if ( pPars->fVerbose )
+ Cec4_ManPrintStats( p, pPars, pMan, 0 );
+ if ( ppNew )
+ {
+ Gia_ManForEachCo( p, pObj, i )
+ pObj->Value = Gia_ManAppendCo( pMan->pNew, Gia_ObjFanin0Copy(pObj) );
+ *ppNew = Gia_ManCleanup( pMan->pNew );
+ }
+finalize:
+ if ( pPars->fVerbose )
+ printf( "SAT calls = %d: P = %d (0=%d a=%.2f m=%d) D = %d (0=%d a=%.2f m=%d) F = %d Sim = %d Recyc = %d Xor = %.2f %%\n",
+ pMan->nSatUnsat + pMan->nSatSat + pMan->nSatUndec,
+ pMan->nSatUnsat, pMan->nConflicts[1][0], (float)pMan->nConflicts[1][1]/Abc_MaxInt(1, pMan->nSatUnsat-pMan->nConflicts[1][0]), pMan->nConflicts[1][2],
+ pMan->nSatSat, pMan->nConflicts[0][0], (float)pMan->nConflicts[0][1]/Abc_MaxInt(1, pMan->nSatSat -pMan->nConflicts[0][0]), pMan->nConflicts[0][2],
+ pMan->nSatUndec,
+ pMan->nSimulates, pMan->nRecycles, 100.0*pMan->nGates[1]/Abc_MaxInt(1, pMan->nGates[0]+pMan->nGates[1]) );
+ Cec4_ManDestroy( pMan );
+ //Gia_ManStaticFanoutStop( p );
+ //Gia_ManEquivPrintClasses( p, 1, 0 );
+ return p->pCexSeq ? 0 : 1;
+}
+Gia_Man_t * Cec4_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars )
+{
+ Gia_Man_t * pNew = NULL;
+ Cec4_ManPerformSweeping( p, pPars, &pNew, 0 );
+ return pNew;
+}
+void Cec4_ManSimulateTest2( Gia_Man_t * p, int nConfs, int fVerbose )
+{
+ abctime clk = Abc_Clock();
+ Cec_ParFra_t ParsFra, * pPars = &ParsFra;
+ Cec4_ManSetParams( pPars );
+ Cec4_ManPerformSweeping( p, pPars, NULL, 0 );
+ pPars->fVerbose = fVerbose;
+ pPars->nBTLimit = nConfs;
+ if ( fVerbose )
+ Abc_PrintTime( 1, "New choice computation time", Abc_Clock() - clk );
+}
+Gia_Man_t * Cec4_ManSimulateTest3( Gia_Man_t * p, int nBTLimit, int fVerbose )
+{
+ Gia_Man_t * pNew = NULL;
+ Cec_ParFra_t ParsFra, * pPars = &ParsFra;
+ Cec4_ManSetParams( pPars );
+ pPars->fVerbose = fVerbose;
+ pPars->nBTLimit = nBTLimit;
+ Cec4_ManPerformSweeping( p, pPars, &pNew, 0 );
+ return pNew;
+}
+Gia_Man_t * Cec4_ManSimulateTest4( Gia_Man_t * p, int nBTLimit, int nBTLimitPo, int fVerbose )
+{
+ Gia_Man_t * pNew = NULL;
+ Cec_ParFra_t ParsFra, * pPars = &ParsFra;
+ Cec4_ManSetParams( pPars );
+ pPars->fVerbose = fVerbose;
+ pPars->nBTLimit = nBTLimit;
+ pPars->nBTLimitPo = nBTLimitPo;
+ Cec4_ManPerformSweeping( p, pPars, &pNew, 0 );
+ return pNew;
+}
+int Cec4_ManSimulateOnlyTest( Gia_Man_t * p, int fVerbose )
+{
+ Cec_ParFra_t ParsFra, * pPars = &ParsFra;
+ Cec4_ManSetParams( pPars );
+ pPars->fVerbose = fVerbose;
+ return Cec4_ManPerformSweeping( p, pPars, NULL, 1 );
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/proof/cec/cecSim.c b/src/proof/cec/cecSim.c
index 92f8fc2e..48a789f3 100644
--- a/src/proof/cec/cecSim.c
+++ b/src/proof/cec/cecSim.c
@@ -6,7 +6,7 @@
PackageName [Combinational equivalence checking.]
- Synopsis [Simulation manager.]
+ Synopsis [Simulation.]
Author [Alan Mishchenko]
@@ -19,14 +19,40 @@
***********************************************************************/
#include "cecInt.h"
+#include "aig/gia/giaAig.h"
+#include "misc/util/utilTruth.h"
-ABC_NAMESPACE_IMPL_START
+ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
+#define SIM_RANDS 113
+
+typedef struct Cec_ManS_t_ Cec_ManS_t;
+struct Cec_ManS_t_
+{
+ int nWords;
+ int nLevelMax;
+ int nLevelMin;
+ int iRand;
+ Gia_Man_t * pAig;
+ Vec_Int_t * vInputs;
+ Vec_Wec_t * vLevels;
+ Vec_Wrd_t * vSims;
+ word * pTemp[4];
+ word Rands[SIM_RANDS];
+ int nSkipped;
+ int nVisited;
+ int nCexes;
+ abctime clkSat;
+ abctime clkUnsat;
+};
+
+static inline word * Cec_ManSSim( Cec_ManS_t * p, int iNode, int Value ) { return Vec_WrdEntryP(p->vSims, p->nWords*(iNode+iNode+Value)); }
+
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
@@ -36,12 +62,340 @@ ABC_NAMESPACE_IMPL_START
Synopsis []
Description []
-
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Cec_ManS_t * Cec_ManSStart( Gia_Man_t * pAig, int nWords )
+{
+ Cec_ManS_t * p; int i;
+ p = ABC_ALLOC( Cec_ManS_t, 1 );
+ memset( p, 0, sizeof(Cec_ManS_t) );
+ p->nWords = nWords;
+ p->pAig = pAig;
+ p->vInputs = Vec_IntAlloc( 100 );
+ p->vLevels = Vec_WecStart( Gia_ManLevelNum(pAig) + 1 );
+ p->vSims = Vec_WrdStart( Gia_ManObjNum(pAig) * nWords * 2 );
+ p->pTemp[0] = ABC_ALLOC( word, 4*nWords );
+ for ( i = 1; i < 4; i++ )
+ p->pTemp[i] = p->pTemp[i-1] + nWords;
+ for ( i = 0; i < SIM_RANDS; i++ )
+ p->Rands[i] = Gia_ManRandomW(0);
+ return p;
+}
+void Cec_ManSStop( Cec_ManS_t * p )
+{
+ Vec_IntFree( p->vInputs );
+ Vec_WecFree( p->vLevels );
+ Vec_WrdFree( p->vSims );
+ ABC_FREE( p->pTemp[0] );
+ ABC_FREE( p );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Verify counter-example.]
+
+ Description []
+
SideEffects []
SeeAlso []
***********************************************************************/
+int Cec_ManSVerify_rec( Gia_Man_t * p, int iObj )
+{
+ int Value0, Value1;
+ Gia_Obj_t * pObj = Gia_ManObj( p, iObj );
+ if ( iObj == 0 ) return 0;
+ if ( Gia_ObjIsTravIdCurrentId(p, iObj) )
+ return pObj->fMark1;
+ Gia_ObjSetTravIdCurrentId(p, iObj);
+ if ( Gia_ObjIsCi(pObj) )
+ return pObj->fMark1;
+ assert( Gia_ObjIsAnd(pObj) );
+ Value0 = Cec_ManSVerify_rec( p, Gia_ObjFaninId0(pObj, iObj) ) ^ Gia_ObjFaninC0(pObj);
+ Value1 = Cec_ManSVerify_rec( p, Gia_ObjFaninId1(pObj, iObj) ) ^ Gia_ObjFaninC1(pObj);
+ return pObj->fMark1 = Gia_ObjIsXor(pObj) ? Value0 ^ Value1 : Value0 & Value1;
+}
+void Cec_ManSVerifyTwo( Gia_Man_t * p, int iObj0, int iObj1 )
+{
+ int Value0, Value1;
+ Gia_ManIncrementTravId( p );
+ Value0 = Cec_ManSVerify_rec( p, iObj0 );
+ Value1 = Cec_ManSVerify_rec( p, iObj1 );
+ if ( (Value0 ^ Value1) == Gia_ObjPhaseDiff(p, iObj0, iObj1) )
+ printf( "CEX verification FAILED for obj %d and obj %d.\n", iObj0, iObj1 );
+// else
+// printf( "CEX verification succeeded for obj %d and obj %d.\n", iObj0, iObj1 );;
+}
+void Cec_ManSVerify( Cec_ManS_t * p, int iObj0, int iObj1 )
+{
+ int fDoVerify = 0;
+ int w, i, iObj, nCares;
+ word * pCare = Vec_WrdArray(p->vSims);
+ if ( Vec_IntSize(p->vInputs) == 0 )
+ {
+ printf( "No primary inputs.\n" );
+ return;
+ }
+ Vec_IntForEachEntry( p->vInputs, iObj, i )
+ {
+ word * pSim_0 = Cec_ManSSim( p, iObj, 0 );
+ word * pSim_1 = Cec_ManSSim( p, iObj, 1 );
+ if ( p->nWords == 1 )
+ pCare[0] |= pSim_0[0] & pSim_1[0];
+ else
+ Abc_TtOrAnd( pCare, pSim_0, pSim_1, p->nWords );
+ }
+ nCares = Abc_TtCountOnesVec( pCare, p->nWords );
+ if ( nCares == 64*p->nWords )
+ {
+ printf( "No CEXes.\n" );
+ return;
+ }
+ assert( Vec_IntSize(p->vInputs) > 0 );
+ for ( w = 0; w < 64*p->nWords; w++ )
+ {
+ if ( Abc_TtGetBit(pCare, w) )
+ continue;
+ if ( !fDoVerify )
+ continue;
+ Vec_IntForEachEntry( p->vInputs, iObj, i )
+ Gia_ManObj(p->pAig, iObj)->fMark1 = Abc_TtGetBit( Cec_ManSSim(p, iObj, 1), w );
+ Cec_ManSVerifyTwo( p->pAig, iObj0, iObj1 );
+ }
+ printf( "Considered %d CEXes of nodes %d and %d.\n", 64*p->nWords - nCares, iObj0, iObj1 );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Cec_ManSRunImply( Cec_ManS_t * p, int iNode )
+{
+ Gia_Obj_t * pNode = Gia_ManObj( p->pAig, iNode );
+ if ( Gia_ObjIsAnd(pNode) )
+ {
+ int iFan0 = Gia_ObjFaninId0( pNode, iNode );
+ int iFan1 = Gia_ObjFaninId1( pNode, iNode );
+ word * pSim__ = Cec_ManSSim( p, 0, 0 );
+ word * pSim_0 = Cec_ManSSim( p, iNode, 0 );
+ word * pSim_1 = Cec_ManSSim( p, iNode, 1 );
+ word * pSim00 = Cec_ManSSim( p, iFan0, Gia_ObjFaninC0(pNode) );
+ word * pSim01 = Cec_ManSSim( p, iFan0, !Gia_ObjFaninC0(pNode) );
+ word * pSim10 = Cec_ManSSim( p, iFan1, Gia_ObjFaninC1(pNode) );
+ word * pSim11 = Cec_ManSSim( p, iFan1, !Gia_ObjFaninC1(pNode) );
+ if ( p->nWords == 1 )
+ {
+ pSim_0[0] |= pSim00[0] | pSim10[0];
+ pSim_1[0] |= pSim01[0] & pSim11[0];
+ pSim__[0] |= pSim_0[0] & pSim_1[0];
+ pSim_0[0] &= ~pSim__[0];
+ pSim_1[0] &= ~pSim__[0];
+ }
+ else
+ {
+ Abc_TtOr( pSim_0, pSim_0, pSim00, p->nWords );
+ Abc_TtOr( pSim_0, pSim_0, pSim10, p->nWords );
+ Abc_TtOrAnd( pSim_1, pSim01, pSim11, p->nWords );
+ Abc_TtOrAnd( pSim__, pSim_0, pSim_1, p->nWords );
+ Abc_TtAndSharp( pSim_0, pSim_0, pSim__, p->nWords, 1 );
+ Abc_TtAndSharp( pSim_1, pSim_1, pSim__, p->nWords, 1 );
+ }
+ }
+}
+int Cec_ManSRunPropagate( Cec_ManS_t * p, int iNode )
+{
+ Gia_Obj_t * pNode = Gia_ManObj( p->pAig, iNode );
+ int iFan0 = Gia_ObjFaninId0( pNode, iNode );
+ int iFan1 = Gia_ObjFaninId1( pNode, iNode );
+ word * pSim_0 = Cec_ManSSim( p, iNode, 0 );
+ word * pSim_1 = Cec_ManSSim( p, iNode, 1 );
+ if ( Abc_TtIsConst0(pSim_0, p->nWords) && Abc_TtIsConst0(pSim_1, p->nWords) )
+ {
+ p->nSkipped++;
+ return 0;
+ }
+ p->nVisited++;
+ //Cec_ManSRunImply( p, iFan0 );
+ //Cec_ManSRunImply( p, iFan1 );
+ {
+ word * pSim__ = Cec_ManSSim( p, 0, 0 );
+ word * pSim00 = Cec_ManSSim( p, iFan0, Gia_ObjFaninC0(pNode) );
+ word * pSim01 = Cec_ManSSim( p, iFan0, !Gia_ObjFaninC0(pNode) );
+ word * pSim10 = Cec_ManSSim( p, iFan1, Gia_ObjFaninC1(pNode) );
+ word * pSim11 = Cec_ManSSim( p, iFan1, !Gia_ObjFaninC1(pNode) );
+ p->iRand = p->iRand == SIM_RANDS-1 ? 0 : p->iRand + 1;
+ if ( p->nWords == 1 )
+ {
+ pSim01[0] |= pSim_1[0];
+ pSim11[0] |= pSim_1[0];
+
+ pSim00[0] |= pSim_0[0] & (pSim11[0] | ~p->Rands[p->iRand]);
+ pSim10[0] |= pSim_0[0] & (pSim01[0] | p->Rands[p->iRand]);
+
+ pSim__[0] |= pSim00[0] & pSim01[0];
+ pSim__[0] |= pSim10[0] & pSim11[0];
+
+ pSim00[0] &= ~pSim__[0];
+ pSim01[0] &= ~pSim__[0];
+ pSim10[0] &= ~pSim__[0];
+ pSim11[0] &= ~pSim__[0];
+ }
+ else
+ {
+ int w;
+ for ( w = 0; w < p->nWords; w++ )
+ p->pTemp[0][w] = ~p->Rands[(p->iRand + w) % SIM_RANDS];
+
+ Abc_TtOr( pSim01, pSim01, pSim_1, p->nWords );
+ Abc_TtOr( pSim11, pSim11, pSim_1, p->nWords );
+
+ Abc_TtOr( p->pTemp[1], pSim11, p->pTemp[0], p->nWords );
+ Abc_TtOrAnd( pSim00, pSim_0, p->pTemp[1], p->nWords );
+
+ Abc_TtNot( p->pTemp[0], p->nWords );
+ Abc_TtOr( p->pTemp[1], pSim01, p->pTemp[0], p->nWords );
+ Abc_TtOrAnd( pSim10, pSim_0, p->pTemp[1], p->nWords );
+
+ Abc_TtOrAnd( pSim__, pSim00, pSim01, p->nWords );
+ Abc_TtOrAnd( pSim__, pSim10, pSim11, p->nWords );
+
+ Abc_TtAndSharp( pSim00, pSim00, pSim__, p->nWords, 1 );
+ Abc_TtAndSharp( pSim01, pSim01, pSim__, p->nWords, 1 );
+ Abc_TtAndSharp( pSim10, pSim10, pSim__, p->nWords, 1 );
+ Abc_TtAndSharp( pSim11, pSim11, pSim__, p->nWords, 1 );
+ }
+ }
+ return 1;
+}
+void Cec_ManSInsert( Cec_ManS_t * p, int iNode )
+{
+ Gia_Obj_t * pNode; int Level;
+ assert( iNode > 0 );
+ if ( Gia_ObjIsTravIdCurrentId(p->pAig, iNode) )
+ return;
+ Gia_ObjSetTravIdCurrentId(p->pAig, iNode);
+ pNode = Gia_ManObj( p->pAig, iNode );
+ if ( Gia_ObjIsCi(pNode) )
+ {
+ Vec_IntPush( p->vInputs, iNode );
+ return;
+ }
+ assert( Gia_ObjIsAnd(pNode) );
+ Level = Gia_ObjLevelId( p->pAig, iNode );
+ assert( Level > 0 );
+ Vec_WecPush( p->vLevels, Level, iNode );
+ p->nLevelMax = Abc_MaxInt( p->nLevelMax, Level );
+ p->nLevelMin = Abc_MinInt( p->nLevelMin, Level );
+ assert( p->nLevelMin <= p->nLevelMax );
+}
+int Cec_ManSRunSimInt( Cec_ManS_t * p )
+{
+ Vec_Int_t * vLevel;
+ int i, k, iNode, fSolved = 0;
+ Vec_WecForEachLevelReverseStartStop( p->vLevels, vLevel, i, p->nLevelMax+1, p->nLevelMin )
+ {
+ Vec_IntForEachEntry( vLevel, iNode, k )
+ {
+ Gia_Obj_t * pNode = Gia_ManObj( p->pAig, iNode );
+ if ( !fSolved && Cec_ManSRunPropagate( p, iNode ) )
+ {
+ Cec_ManSInsert( p, Gia_ObjFaninId0(pNode, iNode) );
+ Cec_ManSInsert( p, Gia_ObjFaninId1(pNode, iNode) );
+ if ( Abc_TtIsConst1(Vec_WrdArray(p->vSims), p->nWords) )
+ fSolved = 1;
+ }
+ Abc_TtClear( Cec_ManSSim(p, iNode, 0), 2*p->nWords );
+ }
+ Vec_IntClear( vLevel );
+ }
+ //Vec_WecForEachLevel( p->vLevels, vLevel, i )
+ // assert( Vec_IntSize(vLevel) == 0 );
+ return fSolved;
+}
+int Cec_ManSRunSim( Cec_ManS_t * p, int iNode0, int iNode1 )
+{
+ abctime clk = Abc_Clock();
+ //Vec_Int_t * vLevel;
+ //int pNodes[2] = { iNode0, iNode1 };
+ int i, iNode, Status, fDiff = Gia_ObjPhaseDiff( p->pAig, iNode0, iNode1 );
+ word * pSim00 = Cec_ManSSim( p, iNode0, 0 );
+ word * pSim01 = Cec_ManSSim( p, iNode0, 1 );
+ word * pSim10 = Cec_ManSSim( p, iNode1, fDiff );
+ word * pSim11 = Cec_ManSSim( p, iNode1, !fDiff );
+ Abc_TtClear( Vec_WrdArray(p->vSims), p->nWords );
+ //for ( i = 0; i < Vec_WrdSize(p->vSims); i++ )
+ // assert( p->vSims->pArray[i] == 0 );
+ assert( Vec_IntSize(p->vInputs) == 0 );
+ if ( iNode0 == 0 )
+ Abc_TtFill( pSim11, p->nWords );
+ else
+ {
+ if ( p->nWords == 1 )
+ {
+ pSim00[0] = (word)0xFFFFFFFF;
+ pSim11[0] = (word)0xFFFFFFFF;
+ pSim01[0] = pSim00[0] << 32;
+ pSim10[0] = pSim11[0] << 32;
+ }
+ else
+ {
+ assert( p->nWords % 2 == 0 );
+ Abc_TtFill( pSim00, p->nWords/2 );
+ Abc_TtFill( pSim11, p->nWords/2 );
+ Abc_TtFill( pSim01 + p->nWords/2, p->nWords/2 );
+ Abc_TtFill( pSim10 + p->nWords/2, p->nWords/2 );
+ }
+ }
+ p->nLevelMin = ABC_INFINITY;
+ p->nLevelMax = 0;
+ Gia_ManIncrementTravId( p->pAig );
+ if ( iNode0 )
+ Cec_ManSInsert( p, iNode0 );
+ Cec_ManSInsert( p, iNode1 );
+ p->nSkipped = p->nVisited = 0;
+ Status = Cec_ManSRunSimInt( p );
+ if ( Status == 0 )
+ p->clkSat += Abc_Clock() - clk;
+ else
+ p->clkUnsat += Abc_Clock() - clk;
+// if ( Status == 0 )
+// printf( "Solving %6d and %6d. Skipped = %6d. Visited = %6d. Cone = %6d. Min = %3d. Max = %3d.\n",
+// iNode0, iNode1, p->nSkipped, p->nVisited, Gia_ManConeSize(p->pAig, pNodes, 2), p->nLevelMin, p->nLevelMax );
+ if ( Status == 0 )
+ Cec_ManSVerify( p, iNode0, iNode1 ), p->nCexes++;
+ Vec_IntForEachEntry( p->vInputs, iNode, i )
+ Abc_TtClear( Cec_ManSSim(p, iNode, 0), 2*p->nWords );
+ Vec_IntClear( p->vInputs );
+ return Status;
+}
+void Cec_ManSRunTest( Gia_Man_t * pAig )
+{
+ abctime clk = Abc_Clock();
+ Cec_ManS_t * p;
+ int i, k, nWords = 1;
+ Gia_ManRandomW( 1 );
+ p = Cec_ManSStart( pAig, nWords );
+ Gia_ManForEachClass0( p->pAig, i )
+ Gia_ClassForEachObj1( p->pAig, i, k )
+ Cec_ManSRunSim( p, i, k );
+ printf( "Detected %d CEXes. ", p->nCexes );
+ Abc_PrintTime( 1, "Time ", Abc_Clock() - clk );
+ Abc_PrintTime( 1, "Sat ", p->clkSat );
+ Abc_PrintTime( 1, "Unsat", p->clkUnsat );
+ Cec_ManSStop( p );
+}
////////////////////////////////////////////////////////////////////////
diff --git a/src/proof/cec/cecSolve.c b/src/proof/cec/cecSolve.c
index af6a4fdb..f8342859 100644
--- a/src/proof/cec/cecSolve.c
+++ b/src/proof/cec/cecSolve.c
@@ -696,7 +696,7 @@ Abc_Cex_t * Cex_ManGenCex( Cec_ManSat_t * p, int iOut )
}
return pCex;
}
-void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_Int_t * vIdsOrig, Vec_Int_t * vMiterPairs, Vec_Int_t * vEquivPairs )
+void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_Int_t * vIdsOrig, Vec_Int_t * vMiterPairs, Vec_Int_t * vEquivPairs, int f0Proved )
{
Bar_Progress_t * pProgress = NULL;
Cec_ManSat_t * p;
@@ -747,6 +747,9 @@ clk2 = Abc_Clock();
if ( pPars->fSaveCexes && status != -1 )
Vec_PtrWriteEntry( pAig->vSeqModelVec, i, status ? (Abc_Cex_t *)(ABC_PTRINT_T)1 : Cex_ManGenCex(p, i) );
+ if ( f0Proved && status == 1 )
+ Gia_ManPatchCoDriver( pAig, i, 0 );
+
/*
if ( status == -1 )
{
@@ -807,7 +810,7 @@ void Cec_ManSatSolveCSat( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t *
{
Vec_Str_t * vStatus;
Vec_Int_t * vPat = Vec_IntAlloc( 1000 );
- Vec_Int_t * vCexStore = Cbs_ManSolveMiterNc( pAig, pPars->nBTLimit, &vStatus, 0 );
+ Vec_Int_t * vCexStore = Cbs_ManSolveMiterNc( pAig, pPars->nBTLimit, &vStatus, 0, 0 );
Gia_Obj_t * pObj;
int i, status, iStart = 0;
assert( Vec_StrSize(vStatus) == Gia_ManCoNum(pAig) );
diff --git a/src/proof/cec/cecSolveG.c b/src/proof/cec/cecSolveG.c
new file mode 100644
index 00000000..0bb68a7f
--- /dev/null
+++ b/src/proof/cec/cecSolveG.c
@@ -0,0 +1,641 @@
+/**CFile****************************************************************
+
+ FileName [cecSolve.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Combinational equivalence checking.]
+
+ Synopsis [Performs one round of SAT solving.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: cecSolve.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "cecInt.h"
+
+
+#define USE_GLUCOSE2
+
+#ifdef USE_GLUCOSE2
+
+#include "sat/glucose2/AbcGlucose2.h"
+
+#define sat_solver bmcg2_sat_solver
+#define sat_solver_start bmcg2_sat_solver_start
+#define sat_solver_stop bmcg2_sat_solver_stop
+#define sat_solver_addclause bmcg2_sat_solver_addclause
+#define sat_solver_add_and bmcg2_sat_solver_add_and
+#define sat_solver_add_xor bmcg2_sat_solver_add_xor
+#define sat_solver_addvar bmcg2_sat_solver_addvar
+#define sat_solver_reset bmcg2_sat_solver_reset
+#define sat_solver_set_conflict_budget bmcg2_sat_solver_set_conflict_budget
+#define sat_solver_conflictnum bmcg2_sat_solver_conflictnum
+#define sat_solver_solve bmcg2_sat_solver_solve
+#define sat_solver_read_cex_varvalue bmcg2_sat_solver_read_cex_varvalue
+#define sat_solver_read_cex bmcg2_sat_solver_read_cex
+#define sat_solver_jftr bmcg2_sat_solver_jftr
+#define sat_solver_set_jftr bmcg2_sat_solver_set_jftr
+#define sat_solver_set_var_fanin_lit bmcg2_sat_solver_set_var_fanin_lit
+#define sat_solver_start_new_round bmcg2_sat_solver_start_new_round
+#define sat_solver_mark_cone bmcg2_sat_solver_mark_cone
+//#define sat_solver_set_nvars bmcg2_sat_solver_set_nvars
+#define sat_solver_varnum bmcg2_sat_solver_varnum
+#else
+
+#include "sat/glucose/AbcGlucose.h"
+
+#define sat_solver bmcg_sat_solver
+#define sat_solver_start bmcg_sat_solver_start
+#define sat_solver_stop bmcg_sat_solver_stop
+#define sat_solver_addclause bmcg_sat_solver_addclause
+#define sat_solver_add_and bmcg_sat_solver_add_and
+#define sat_solver_add_xor bmcg_sat_solver_add_xor
+#define sat_solver_addvar bmcg_sat_solver_addvar
+#define sat_solver_reset bmcg_sat_solver_reset
+#define sat_solver_set_conflict_budget bmcg_sat_solver_set_conflict_budget
+#define sat_solver_conflictnum bmcg_sat_solver_conflictnum
+#define sat_solver_solve bmcg_sat_solver_solve
+#define sat_solver_read_cex_varvalue bmcg_sat_solver_read_cex_varvalue
+#define sat_solver_read_cex bmcg_sat_solver_read_cex
+#define sat_solver_jftr bmcg_sat_solver_jftr
+#define sat_solver_set_jftr bmcg_sat_solver_set_jftr
+#define sat_solver_set_var_fanin_lit bmcg_sat_solver_set_var_fanin_lit
+#define sat_solver_start_new_round bmcg_sat_solver_start_new_round
+#define sat_solver_mark_cone bmcg_sat_solver_mark_cone
+#define sat_solver_set_nvars bmcg_sat_solver_set_nvars
+
+#endif
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+static inline int CecG_ObjSatNum( Cec_ManSat_t * p, Gia_Obj_t * pObj ) { return p->pSatVars[Gia_ObjId(p->pAig,pObj)]; }
+static inline void CecG_ObjSetSatNum( Cec_ManSat_t * p, Gia_Obj_t * pObj, int Num ) { p->pSatVars[Gia_ObjId(p->pAig,pObj)] = Num; }
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Returns value of the SAT variable.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int CecG_ObjSatVarValue( Cec_ManSat_t * p, Gia_Obj_t * pObj )
+{
+ return sat_solver_read_cex_varvalue( p->pSat, CecG_ObjSatNum(p, pObj) );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Addes clauses to the solver.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void CecG_AddClausesMux( Cec_ManSat_t * p, Gia_Obj_t * pNode )
+{
+ Gia_Obj_t * pNodeI, * pNodeT, * pNodeE;
+ int pLits[4], RetValue, VarF, VarI, VarT, VarE, fCompT, fCompE;
+
+ assert( !Gia_IsComplement( pNode ) );
+ assert( Gia_ObjIsMuxType( pNode ) );
+ // get nodes (I = if, T = then, E = else)
+ pNodeI = Gia_ObjRecognizeMux( pNode, &pNodeT, &pNodeE );
+ // get the variable numbers
+ VarF = CecG_ObjSatNum(p,pNode);
+ VarI = CecG_ObjSatNum(p,pNodeI);
+ VarT = CecG_ObjSatNum(p,Gia_Regular(pNodeT));
+ VarE = CecG_ObjSatNum(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] = toLitCond(VarI, 1);
+ pLits[1] = toLitCond(VarT, 1^fCompT);
+ pLits[2] = toLitCond(VarF, 0);
+ if ( p->pPars->fPolarFlip )
+ {
+ if ( pNodeI->fPhase ) pLits[0] = lit_neg( pLits[0] );
+ if ( Gia_Regular(pNodeT)->fPhase ) pLits[1] = lit_neg( pLits[1] );
+ if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] );
+ }
+ RetValue = sat_solver_addclause( p->pSat, pLits, 3 );
+ assert( RetValue );
+ pLits[0] = toLitCond(VarI, 1);
+ pLits[1] = toLitCond(VarT, 0^fCompT);
+ pLits[2] = toLitCond(VarF, 1);
+ if ( p->pPars->fPolarFlip )
+ {
+ if ( pNodeI->fPhase ) pLits[0] = lit_neg( pLits[0] );
+ if ( Gia_Regular(pNodeT)->fPhase ) pLits[1] = lit_neg( pLits[1] );
+ if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] );
+ }
+ RetValue = sat_solver_addclause( p->pSat, pLits, 3 );
+ assert( RetValue );
+ pLits[0] = toLitCond(VarI, 0);
+ pLits[1] = toLitCond(VarE, 1^fCompE);
+ pLits[2] = toLitCond(VarF, 0);
+ if ( p->pPars->fPolarFlip )
+ {
+ if ( pNodeI->fPhase ) pLits[0] = lit_neg( pLits[0] );
+ if ( Gia_Regular(pNodeE)->fPhase ) pLits[1] = lit_neg( pLits[1] );
+ if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] );
+ }
+ RetValue = sat_solver_addclause( p->pSat, pLits, 3 );
+ assert( RetValue );
+ pLits[0] = toLitCond(VarI, 0);
+ pLits[1] = toLitCond(VarE, 0^fCompE);
+ pLits[2] = toLitCond(VarF, 1);
+ if ( p->pPars->fPolarFlip )
+ {
+ if ( pNodeI->fPhase ) pLits[0] = lit_neg( pLits[0] );
+ if ( Gia_Regular(pNodeE)->fPhase ) pLits[1] = lit_neg( pLits[1] );
+ if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] );
+ }
+ RetValue = sat_solver_addclause( p->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] = toLitCond(VarT, 0^fCompT);
+ pLits[1] = toLitCond(VarE, 0^fCompE);
+ pLits[2] = toLitCond(VarF, 1);
+ if ( p->pPars->fPolarFlip )
+ {
+ if ( Gia_Regular(pNodeT)->fPhase ) pLits[0] = lit_neg( pLits[0] );
+ if ( Gia_Regular(pNodeE)->fPhase ) pLits[1] = lit_neg( pLits[1] );
+ if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] );
+ }
+ RetValue = sat_solver_addclause( p->pSat, pLits, 3 );
+ assert( RetValue );
+ pLits[0] = toLitCond(VarT, 1^fCompT);
+ pLits[1] = toLitCond(VarE, 1^fCompE);
+ pLits[2] = toLitCond(VarF, 0);
+ if ( p->pPars->fPolarFlip )
+ {
+ if ( Gia_Regular(pNodeT)->fPhase ) pLits[0] = lit_neg( pLits[0] );
+ if ( Gia_Regular(pNodeE)->fPhase ) pLits[1] = lit_neg( pLits[1] );
+ if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] );
+ }
+ RetValue = sat_solver_addclause( p->pSat, pLits, 3 );
+ assert( RetValue );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Addes clauses to the solver.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void CecG_AddClausesSuper( Cec_ManSat_t * p, Gia_Obj_t * pNode, Vec_Ptr_t * vSuper )
+{
+ 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] = toLitCond(CecG_ObjSatNum(p,Gia_Regular(pFanin)), Gia_IsComplement(pFanin));
+ pLits[1] = toLitCond(CecG_ObjSatNum(p,pNode), 1);
+ if ( p->pPars->fPolarFlip )
+ {
+ if ( Gia_Regular(pFanin)->fPhase ) pLits[0] = lit_neg( pLits[0] );
+ if ( pNode->fPhase ) pLits[1] = lit_neg( pLits[1] );
+ }
+ RetValue = sat_solver_addclause( p->pSat, pLits, 2 );
+ assert( RetValue );
+ }
+ // add A & B => C or !A + !B + C
+ Vec_PtrForEachEntry( Gia_Obj_t *, vSuper, pFanin, i )
+ {
+ pLits[i] = toLitCond(CecG_ObjSatNum(p,Gia_Regular(pFanin)), !Gia_IsComplement(pFanin));
+ if ( p->pPars->fPolarFlip )
+ {
+ if ( Gia_Regular(pFanin)->fPhase ) pLits[i] = lit_neg( pLits[i] );
+ }
+ }
+ pLits[nLits-1] = toLitCond(CecG_ObjSatNum(p,pNode), 0);
+ if ( p->pPars->fPolarFlip )
+ {
+ if ( pNode->fPhase ) pLits[nLits-1] = lit_neg( pLits[nLits-1] );
+ }
+ RetValue = sat_solver_addclause( p->pSat, pLits, nLits );
+ assert( RetValue );
+ ABC_FREE( pLits );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Collects the supergate.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void CecG_CollectSuper_rec( Gia_Obj_t * pObj, Vec_Ptr_t * vSuper, int fFirst, int fUseMuxes, int fUseSuper )
+{
+ // 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 && Gia_ObjIsMuxType(pObj)) )
+ {
+ Vec_PtrPushUnique( vSuper, pObj );
+ return;
+ }
+ if( !fUseSuper ){
+ Vec_PtrPushUnique( vSuper, Gia_ObjChild0(pObj) );
+ Vec_PtrPushUnique( vSuper, Gia_ObjChild1(pObj) );
+ return ;
+ }
+ // go through the branches
+ CecG_CollectSuper_rec( Gia_ObjChild0(pObj), vSuper, 0, fUseMuxes, fUseSuper );
+ CecG_CollectSuper_rec( Gia_ObjChild1(pObj), vSuper, 0, fUseMuxes, fUseSuper );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Collects the supergate.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void CecG_CollectSuper( Gia_Obj_t * pObj, int fUseMuxes, int fUseSuper, Vec_Ptr_t * vSuper )
+{
+ assert( !Gia_IsComplement(pObj) );
+ assert( !Gia_ObjIsCi(pObj) );
+ Vec_PtrClear( vSuper );
+ CecG_CollectSuper_rec( pObj, vSuper, 1, fUseMuxes, fUseSuper );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Updates the solver clause database.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void CecG_ObjAddToFrontier( Cec_ManSat_t * p, Gia_Obj_t * pObj, Vec_Ptr_t * vFrontier )
+{
+ assert( !Gia_IsComplement(pObj) );
+ if ( CecG_ObjSatNum(p,pObj) )
+ return;
+ assert( CecG_ObjSatNum(p,pObj) == 0 );
+ if ( Gia_ObjIsConst0(pObj) )
+ return;
+ Vec_PtrPush( p->vUsedNodes, pObj );
+ CecG_ObjSetSatNum( p, pObj, sat_solver_addvar( p->pSat ) );
+ if ( Gia_ObjIsAnd(pObj) )
+ Vec_PtrPush( vFrontier, pObj );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Updates the solver clause database.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void CecG_CnfNodeAddToSolver( Cec_ManSat_t * p, Gia_Obj_t * pObj )
+{
+ Vec_Ptr_t * vFrontier;
+ Gia_Obj_t * pNode, * pFanin;
+ int i, k, fUseMuxes = 0 == p->pPars->SolverType;
+ // quit if CNF is ready
+ if ( CecG_ObjSatNum(p,pObj) )
+ return;
+ if ( Gia_ObjIsCi(pObj) )
+ {
+ Vec_PtrPush( p->vUsedNodes, pObj );
+ CecG_ObjSetSatNum( p, pObj, sat_solver_addvar( p->pSat ) );
+ return;
+ }
+ assert( Gia_ObjIsAnd(pObj) );
+
+ // start the frontier
+ vFrontier = Vec_PtrAlloc( 100 );
+ CecG_ObjAddToFrontier( p, pObj, vFrontier );
+ // explore nodes in the frontier
+ Vec_PtrForEachEntry( Gia_Obj_t *, vFrontier, pNode, i )
+ {
+ // create the supergate
+ assert( CecG_ObjSatNum(p,pNode) );
+ if ( fUseMuxes && Gia_ObjIsMuxType(pNode) )
+ {
+ 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 )
+ CecG_ObjAddToFrontier( p, Gia_Regular(pFanin), vFrontier );
+ CecG_AddClausesMux( p, pNode );
+ }
+ else
+ {
+ CecG_CollectSuper( pNode, fUseMuxes, 0 == p->pPars->SolverType, p->vFanins );
+ Vec_PtrForEachEntry( Gia_Obj_t *, p->vFanins, pFanin, k )
+ CecG_ObjAddToFrontier( p, Gia_Regular(pFanin), vFrontier );
+
+ if( p->pPars->SolverType < 2 )
+ CecG_AddClausesSuper( p, pNode, p->vFanins );
+ }
+ assert( Vec_PtrSize(p->vFanins) > 1 );
+ }
+ if( p->pPars->SolverType )
+ Vec_PtrForEachEntry( Gia_Obj_t *, vFrontier, pNode, i ){
+ int var = CecG_ObjSatNum( p, pNode );
+ int Lit0 = Abc_Var2Lit( CecG_ObjSatNum( p, Gia_ObjFanin0(pNode) ), Gia_ObjFaninC0(pNode) );
+ int Lit1 = Abc_Var2Lit( CecG_ObjSatNum( p, Gia_ObjFanin1(pNode) ), Gia_ObjFaninC1(pNode) );
+ assert(Gia_ObjIsAnd(pNode));
+ if ( (Lit0 > Lit1) ^ Gia_ObjIsXor(pNode) )
+ Lit1 ^= Lit0, Lit0 ^= Lit1, Lit1 ^= Lit0;
+ sat_solver_set_var_fanin_lit( p->pSat, var, Lit0, Lit1 );
+ }
+ Vec_PtrFree( vFrontier );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Recycles the SAT solver.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void CecG_ManSatSolverRecycle( Cec_ManSat_t * p )
+{
+ int Lit;
+ if ( p->pSat )
+ {
+ Gia_Obj_t * pObj;
+ int i;
+ Vec_PtrForEachEntry( Gia_Obj_t *, p->vUsedNodes, pObj, i )
+ CecG_ObjSetSatNum( p, pObj, 0 );
+ Vec_PtrClear( p->vUsedNodes );
+// memset( p->pSatVars, 0, sizeof(int) * Gia_ManObjNumMax(p->pAigTotal) );
+ sat_solver_stop( p->pSat );
+ }
+ p->pSat = sat_solver_start();
+ assert( 0 <= p->pPars->SolverType && p->pPars->SolverType <= 2 );
+ sat_solver_set_jftr( p->pSat, p->pPars->SolverType );
+ //sat_solver_setnvars( p->pSat, 1000 ); // minisat only
+ //p->pSat->factors = ABC_CALLOC( double, p->pSat->cap );
+ // var 0 is not used
+ // var 1 is reserved for const0 node - add the clause
+
+// p->nSatVars = 0;
+ CecG_ObjSetSatNum( p, Gia_ManConst0(p->pAig), sat_solver_addvar( p->pSat ) );
+ Lit = toLitCond( CecG_ObjSatNum( p, Gia_ManConst0(p->pAig) ), 1 );
+ sat_solver_addclause( p->pSat, &Lit, 1 );
+// if ( p->pPars->fPolarFlip ) // no need to normalize const0 node (bug fix by SS on 9/17/2012)
+// Lit = lit_neg( Lit );
+
+ p->nRecycles++;
+ p->nCallsSince = 0;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Runs equivalence test for the two nodes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int CecG_ManSatCheckNode( Cec_ManSat_t * p, Gia_Obj_t * pObj )
+{
+ Gia_Obj_t * pObjR = Gia_Regular(pObj);
+ int nBTLimit = p->pPars->nBTLimit;
+ int Lit, RetValue, nConflicts;
+ abctime clk = Abc_Clock();
+
+ if ( pObj == Gia_ManConst0(p->pAig) )
+ return 1;
+ if ( pObj == Gia_ManConst1(p->pAig) )
+ {
+ assert( 0 );
+ return 0;
+ }
+
+ p->nCallsSince++; // experiment with this!!!
+ p->nSatTotal++;
+
+ // check if SAT solver needs recycling
+ if ( p->pSat == NULL ||
+ (p->pPars->nSatVarMax &&
+ sat_solver_varnum(p->pSat) > p->pPars->nSatVarMax &&
+ p->nCallsSince > p->pPars->nCallsRecycle) )
+ CecG_ManSatSolverRecycle( p );
+
+ // if the nodes do not have SAT variables, allocate them
+ CecG_CnfNodeAddToSolver( p, pObjR );
+
+ if( p->pPars->SolverType ){
+ sat_solver_start_new_round( p->pSat );
+ sat_solver_mark_cone( p->pSat, CecG_ObjSatNum(p, pObjR) );
+ }
+
+ // propage unit clauses // minisat only
+ //if ( p->pSat->qtail != p->pSat->qhead )
+ //{
+ // status = sat_solver_simplify(p->pSat);
+ // assert( status != 0 );
+ // assert( p->pSat->qtail == p->pSat->qhead );
+ //}
+
+ // solve under assumptions
+ // A = 1; B = 0 OR A = 1; B = 1
+ Lit = toLitCond( CecG_ObjSatNum(p,pObjR), Gia_IsComplement(pObj) );
+ if ( p->pPars->fPolarFlip )
+ {
+ if ( pObjR->fPhase ) Lit = lit_neg( Lit );
+ }
+ nConflicts = sat_solver_conflictnum(p->pSat);
+
+ sat_solver_set_conflict_budget( p->pSat, nBTLimit );
+ RetValue = sat_solver_solve( p->pSat, &Lit, 1 );
+ //RetValue = sat_solver_solve( p->pSat, &Lit, &Lit + 1,
+ // (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
+ if ( RetValue == l_False )
+ {
+p->timeSatUnsat += Abc_Clock() - clk;
+ Lit = lit_neg( Lit );
+ RetValue = sat_solver_addclause( p->pSat, &Lit, 1 );
+ assert( RetValue );
+ p->nSatUnsat++;
+ p->nConfUnsat += sat_solver_conflictnum(p->pSat) - nConflicts;
+//Abc_Print( 1, "UNSAT after %d conflicts\n", sat_solver_conflictnum(p->pSat) - nConflicts );
+ return 1;
+ }
+ else if ( RetValue == l_True )
+ {
+p->timeSatSat += Abc_Clock() - clk;
+ p->nSatSat++;
+ p->nConfSat += sat_solver_conflictnum(p->pSat) - nConflicts;
+//Abc_Print( 1, "SAT after %d conflicts\n", sat_solver_conflictnum(p->pSat) - nConflicts );
+ return 0;
+ }
+ else // if ( RetValue == l_Undef )
+ {
+p->timeSatUndec += Abc_Clock() - clk;
+ p->nSatUndec++;
+ p->nConfUndec += sat_solver_conflictnum(p->pSat) - nConflicts;
+//Abc_Print( 1, "UNDEC after %d conflicts\n", sat_solver_conflictnum(p->pSat) - nConflicts );
+ return -1;
+ }
+}
+
+void CecG_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars, int f0Proved )
+{
+ Bar_Progress_t * pProgress = NULL;
+ Cec_ManSat_t * p;
+ Gia_Obj_t * pObj;
+ int i, status;
+ abctime clk = Abc_Clock(), clk2;
+ Vec_PtrFreeP( &pAig->vSeqModelVec );
+ if( pPars->SolverType )
+ pPars->fPolarFlip = 0;
+ // reset the manager
+ if ( pPat )
+ {
+ pPat->iStart = Vec_StrSize(pPat->vStorage);
+ pPat->nPats = 0;
+ pPat->nPatLits = 0;
+ pPat->nPatLitsMin = 0;
+ }
+ Gia_ManSetPhase( pAig );
+ Gia_ManLevelNum( pAig );
+ Gia_ManIncrementTravId( pAig );
+ p = Cec_ManSatCreate( pAig, pPars );
+ pProgress = Bar_ProgressStart( stdout, Gia_ManPoNum(pAig) );
+ Gia_ManForEachCo( pAig, pObj, i )
+ {
+ if ( Gia_ObjIsConst0(Gia_ObjFanin0(pObj)) )
+ {
+ status = !Gia_ObjFaninC0(pObj);
+ pObj->fMark0 = (status == 0);
+ pObj->fMark1 = (status == 1);
+ continue;
+ }
+ Bar_ProgressUpdate( pProgress, i, "SAT..." );
+clk2 = Abc_Clock();
+ status = CecG_ManSatCheckNode( p, Gia_ObjChild0(pObj) );
+ pObj->fMark0 = (status == 0);
+ pObj->fMark1 = (status == 1);
+
+ if ( f0Proved && status == 1 )
+ Gia_ManPatchCoDriver( pAig, i, 0 );
+/*
+ if ( status == -1 )
+ {
+ Gia_Man_t * pTemp = Gia_ManDupDfsCone( pAig, pObj );
+ Gia_AigerWrite( pTemp, "gia_hard.aig", 0, 0, 0 );
+ Gia_ManStop( pTemp );
+ Abc_Print( 1, "Dumping hard cone into file \"%s\".\n", "gia_hard.aig" );
+ }
+*/
+ if ( status != 0 )
+ continue;
+ // save the pattern
+ //if ( pPat )
+ //{
+ // abctime clk3 = Abc_Clock();
+ // Cec_ManPatSavePattern( pPat, p, pObj );
+ // pPat->timeTotalSave += Abc_Clock() - clk3;
+ //}
+ // quit if one of them is solved
+ if ( pPars->fCheckMiter )
+ break;
+ }
+ p->timeTotal = Abc_Clock() - clk;
+ printf("Recycles %d\n", p->nRecycles);
+ Bar_ProgressStop( pProgress );
+ if ( pPars->fVerbose )
+ Cec_ManSatPrintStats( p );
+ if( p->pSat )
+ sat_solver_stop( p->pSat );
+ p->pSat = NULL;
+ Cec_ManSatStop( p );
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/proof/cec/cecSweep.c b/src/proof/cec/cecSweep.c
index 55f2219f..abe77960 100644
--- a/src/proof/cec/cecSweep.c
+++ b/src/proof/cec/cecSweep.c
@@ -289,6 +289,9 @@ p->timeSim += Abc_Clock() - clk;
p->nAllFailed++;
}
}
+ p->nAllProvedS += p->nAllProved;
+ p->nAllDisprovedS += p->nAllDisproved;
+ p->nAllFailedS += p->nAllFailed;
return 0;
}
diff --git a/src/proof/cec/module.make b/src/proof/cec/module.make
index 86ec2677..23595f23 100644
--- a/src/proof/cec/module.make
+++ b/src/proof/cec/module.make
@@ -8,8 +8,11 @@ SRC += src/proof/cec/cecCec.c \
src/proof/cec/cecPat.c \
src/proof/cec/cecSat.c \
src/proof/cec/cecSatG.c \
+ src/proof/cec/cecSatG2.c \
src/proof/cec/cecSeq.c \
+ src/proof/cec/cecSim.c \
src/proof/cec/cecSolve.c \
+ src/proof/cec/cecSolveG.c \
src/proof/cec/cecSplit.c \
src/proof/cec/cecSynth.c \
src/proof/cec/cecSweep.c
diff --git a/src/proof/dch/dch.h b/src/proof/dch/dch.h
index 5d644643..07f6a1d2 100644
--- a/src/proof/dch/dch.h
+++ b/src/proof/dch/dch.h
@@ -52,6 +52,7 @@ struct Dch_Pars_t_
int fPower; // uses power-aware rewriting
int fUseGia; // uses GIA package
int fUseCSat; // uses circuit-based solver
+ int fUseNew; // uses new implementation
int fLightSynth; // uses lighter version of synthesis
int fSkipRedSupp; // skip choices with redundant support vars
int fVerbose; // verbose stats
diff --git a/src/proof/dch/dchCore.c b/src/proof/dch/dchCore.c
index 0da65bee..19907f00 100644
--- a/src/proof/dch/dchCore.c
+++ b/src/proof/dch/dchCore.c
@@ -90,7 +90,7 @@ Aig_Man_t * Dch_ComputeChoices( Aig_Man_t * pAig, Dch_Pars_t * pPars )
{
Dch_Man_t * p;
Aig_Man_t * pResult;
- abctime clk, clkTotal = Abc_Clock();
+ abctime clk, clk2 = Abc_Clock(), clkTotal = Abc_Clock();
// reset random numbers
Aig_ManRandom(1);
// start the choicing manager
@@ -106,6 +106,8 @@ p->timeSimInit = Abc_Clock() - clk;
// free memory ahead of time
p->timeTotal = Abc_Clock() - clkTotal;
Dch_ManStop( p );
+ if ( pPars->fVerbose )
+ Abc_PrintTime( 1, "Old choice computation time", Abc_Clock() - clk2 );
// create choices
ABC_FREE( pAig->pTable );
pResult = Dch_DeriveChoiceAig( pAig, pPars->fSkipRedSupp );
diff --git a/src/proof/dch/dchSimSat.c b/src/proof/dch/dchSimSat.c
index d3dbbe16..bbab0529 100644
--- a/src/proof/dch/dchSimSat.c
+++ b/src/proof/dch/dchSimSat.c
@@ -91,8 +91,8 @@ void Dch_ManCollectTfoCands( Dch_Man_t * p, Aig_Obj_t * pObj1, Aig_Obj_t * pObj2
Aig_ObjSetTravIdCurrent( p->pAigTotal, Aig_ManConst1(p->pAigTotal) );
Dch_ManCollectTfoCands_rec( p, pObj1 );
Dch_ManCollectTfoCands_rec( p, pObj2 );
- Vec_PtrSort( p->vSimRoots, (int (*)(void))Aig_ObjCompareIdIncrease );
- Vec_PtrSort( p->vSimClasses, (int (*)(void))Aig_ObjCompareIdIncrease );
+ Vec_PtrSort( p->vSimRoots, (int (*)(const void *, const void *))Aig_ObjCompareIdIncrease );
+ Vec_PtrSort( p->vSimClasses, (int (*)(const void *, const void *))Aig_ObjCompareIdIncrease );
Vec_PtrForEachEntry( Aig_Obj_t *, p->vSimClasses, pObj, i )
pObj->fMarkA = 0;
}
diff --git a/src/proof/fra/fraSec.c b/src/proof/fra/fraSec.c
index 7e382fc8..eadd06c9 100644
--- a/src/proof/fra/fraSec.c
+++ b/src/proof/fra/fraSec.c
@@ -20,6 +20,7 @@
#include "fra.h"
#include "aig/ioa/ioa.h"
+#include "aig/gia/giaAig.h"
#include "proof/int/int.h"
#include "proof/ssw/ssw.h"
#include "aig/saig/saig.h"
@@ -92,6 +93,28 @@ void Fra_SecSetDefaultParams( Fra_Sec_t * p )
SeeAlso []
***********************************************************************/
+Aig_Man_t * Fra_FraigEquivence2( Aig_Man_t * pAig, int nConfs, int fVerbose )
+{
+ extern Gia_Man_t * Cec4_ManSimulateTest3( Gia_Man_t * p, int nBTLimit, int fVerbose );
+ Gia_Man_t * pGia = Gia_ManFromAig( pAig );
+ Gia_Man_t * pGiaNew = Cec4_ManSimulateTest3( pGia, nConfs, 0 );
+ Aig_Man_t * pAigNew = Gia_ManToAig( pGiaNew, 0 );
+ Gia_ManStop( pGiaNew );
+ Gia_ManStop( pGia );
+ return pAigNew;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
int Fra_FraigSec( Aig_Man_t * p, Fra_Sec_t * pParSec, Aig_Man_t ** ppResult )
{
Ssw_Pars_t Pars2, * pPars2 = &Pars2;
@@ -267,6 +290,7 @@ ABC_PRT( "Time", Abc_Clock() - clk );
{
clk = Abc_Clock();
pNew = Fra_FraigEquivence( pTemp = pNew, 100, 0 );
+ //pNew = Fra_FraigEquivence2( pTemp = pNew, 100, 0 );
Aig_ManStop( pTemp );
if ( pParSec->fVerbose )
{
diff --git a/src/proof/int/int.h b/src/proof/int/int.h
index 906d8aaf..3dc8490d 100644
--- a/src/proof/int/int.h
+++ b/src/proof/int/int.h
@@ -24,7 +24,7 @@
/*
The interpolation algorithm implemented here was introduced in the paper:
- K. L. McMillan. Interpolation and SAT-based model checking. CAV’03, pp. 1-13.
+ K. L. McMillan. Interpolation and SAT-based model checking. CAV 03, pp. 1-13.
*/
////////////////////////////////////////////////////////////////////////
diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c
index f71569a3..d77fd4e1 100644
--- a/src/proof/pdr/pdrCore.c
+++ b/src/proof/pdr/pdrCore.c
@@ -157,7 +157,7 @@ int Pdr_ManPushClauses( Pdr_Man_t * p )
assert( p->iUseFrame > 0 );
Vec_VecForEachLevelStartStop( p->vClauses, vArrayK, k, iStartFrame, kMax )
{
- Vec_PtrSort( vArrayK, (int (*)(void))Pdr_SetCompare );
+ Vec_PtrSort( vArrayK, (int (*)(const void *, const void *))Pdr_SetCompare );
vArrayK1 = Vec_VecEntry( p->vClauses, k+1 );
Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCubeK, j )
{
@@ -216,7 +216,7 @@ int Pdr_ManPushClauses( Pdr_Man_t * p )
// clean up the last one
vArrayK = Vec_VecEntry( p->vClauses, kMax );
- Vec_PtrSort( vArrayK, (int (*)(void))Pdr_SetCompare );
+ Vec_PtrSort( vArrayK, (int (*)(const void *, const void *))Pdr_SetCompare );
Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCubeK, j )
{
// remove cubes in the same frame that are contained by pCubeK
diff --git a/src/proof/pdr/pdrIncr.c b/src/proof/pdr/pdrIncr.c
index f4f2c8c8..9ca72ba6 100644
--- a/src/proof/pdr/pdrIncr.c
+++ b/src/proof/pdr/pdrIncr.c
@@ -47,7 +47,7 @@ Vec_Ptr_t * IPdr_ManPushClausesK( Pdr_Man_t * p, int k )
assert( Vec_VecSize(p->vClauses) == k + 1 );
vArrayK = Vec_VecEntry( p->vClauses, k );
- Vec_PtrSort( vArrayK, (int (*)(void))Pdr_SetCompare );
+ Vec_PtrSort( vArrayK, (int (*)(const void *, const void *))Pdr_SetCompare );
vArrayK1 = Vec_PtrAlloc( 100 );
Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCubeK, j )
{
@@ -117,7 +117,7 @@ void IPdr_ManPrintClauses( Vec_Vec_t * vClauses, int kStart, int nRegs )
int i, k, Counter = 0;
Vec_VecForEachLevelStart( vClauses, vArrayK, k, kStart )
{
- Vec_PtrSort( vArrayK, (int (*)(void))Pdr_SetCompare );
+ Vec_PtrSort( vArrayK, (int (*)(const void *, const void *))Pdr_SetCompare );
Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCube, i )
{
Abc_Print( 1, "Frame[%4d]Cube[%4d] = ", k, Counter++ );
diff --git a/src/proof/pdr/pdrInv.c b/src/proof/pdr/pdrInv.c
index ba4f0448..ae61ce2c 100644
--- a/src/proof/pdr/pdrInv.c
+++ b/src/proof/pdr/pdrInv.c
@@ -248,7 +248,7 @@ void Pdr_ManPrintClauses( Pdr_Man_t * p, int kStart )
int i, k, Counter = 0;
Vec_VecForEachLevelStart( p->vClauses, vArrayK, k, kStart )
{
- Vec_PtrSort( vArrayK, (int (*)(void))Pdr_SetCompare );
+ Vec_PtrSort( vArrayK, (int (*)(const void *, const void *))Pdr_SetCompare );
Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCube, i )
{
Abc_Print( 1, "C=%4d. F=%4d ", Counter++, k );
@@ -370,7 +370,7 @@ void Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName, int fProved )
vCubes = Pdr_ManCollectCubes( p, kStart );
else
vCubes = Vec_PtrDup( p->vInfCubes );
- Vec_PtrSort( vCubes, (int (*)(void))Pdr_SetCompare );
+ Vec_PtrSort( vCubes, (int (*)(const void *, const void *))Pdr_SetCompare );
// Pdr_ManDumpAig( p->pAig, vCubes );
// count cubes
Count = 0;
@@ -446,7 +446,7 @@ Vec_Str_t * Pdr_ManDumpString( Pdr_Man_t * p )
vCubes = Pdr_ManCollectCubes( p, kStart );
else
vCubes = Vec_PtrDup( p->vInfCubes );
- Vec_PtrSort( vCubes, (int (*)(void))Pdr_SetCompare );
+ Vec_PtrSort( vCubes, (int (*)(const void *, const void *))Pdr_SetCompare );
// collect variable appearances
vFlopCounts = p->pPars->fUseSupp ? Pdr_ManCountFlops( p, vCubes ) : NULL;
// output cubes
generated by cgit v1.2.3 (git 2.25.1) at 2025-07-02 20:31:06 +0000