summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/aig/gia/gia.h3
-rw-r--r--src/aig/gia/giaDup.c30
-rw-r--r--src/aig/gia/giaEquiv.c4
-rw-r--r--src/aig/gia/giaSweeper.c25
-rw-r--r--src/aig/gia/giaTim.c2
-rw-r--r--src/base/abci/abc.c4
-rw-r--r--src/proof/cec/cecCec.c2
-rw-r--r--src/sat/bmc/bmcICheck.c2
8 files changed, 60 insertions, 12 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 9e82939d..c3e0d033 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -1007,7 +1007,8 @@ extern Gia_Man_t * Gia_ManDupWithNewPo( Gia_Man_t * p1, Gia_Man_t * p2 )
extern Gia_Man_t * Gia_ManDupDfsCiMap( Gia_Man_t * p, int * pCi2Lit, Vec_Int_t * vLits );
extern Gia_Man_t * Gia_ManDupDfsClasses( Gia_Man_t * p );
extern Gia_Man_t * Gia_ManDupTopAnd( Gia_Man_t * p, int fVerbose );
-extern Gia_Man_t * Gia_ManMiter( Gia_Man_t * pAig0, Gia_Man_t * pAig1, int nInsDup, int fDualOut, int fSeq, int fVerbose );
+extern Gia_Man_t * Gia_ManMiter( Gia_Man_t * pAig0, Gia_Man_t * pAig1, int nInsDup, int fDualOut, int fSeq, int fImplic, int fVerbose );
+extern Gia_Man_t * Gia_ManDupAnd( Gia_Man_t * p, int fCompl );
extern Gia_Man_t * Gia_ManDupZeroUndc( Gia_Man_t * p, char * pInit, int fVerbose );
extern Gia_Man_t * Gia_ManMiter2( Gia_Man_t * p, char * pInit, int fVerbose );
extern Gia_Man_t * Gia_ManTransformMiter( Gia_Man_t * p );
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index 30f9140d..92076573 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -1880,7 +1880,7 @@ int Gia_ManMiter_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
SeeAlso []
***********************************************************************/
-Gia_Man_t * Gia_ManMiter( Gia_Man_t * p0, Gia_Man_t * p1, int nInsDup, int fDualOut, int fSeq, int fVerbose )
+Gia_Man_t * Gia_ManMiter( Gia_Man_t * p0, Gia_Man_t * p1, int nInsDup, int fDualOut, int fSeq, int fImplic, int fVerbose )
{
Gia_Man_t * pNew, * pTemp;
Gia_Obj_t * pObj;
@@ -1951,7 +1951,12 @@ Gia_Man_t * Gia_ManMiter( Gia_Man_t * p0, Gia_Man_t * p1, int nInsDup, int fDual
Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(Gia_ManPo(p1,i)) );
}
- else
+ else if ( fImplic )
+ {
+ iLit = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Abc_LitNot(Gia_ObjFanin0Copy(Gia_ManPo(p1,i))) );
+ Gia_ManAppendCo( pNew, iLit );
+ }
+ else
{
iLit = Gia_ManHashXor( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin0Copy(Gia_ManPo(p1,i)) );
Gia_ManAppendCo( pNew, iLit );
@@ -1990,6 +1995,11 @@ Gia_Man_t * Gia_ManMiter( Gia_Man_t * p0, Gia_Man_t * p1, int nInsDup, int fDual
Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(Gia_ManCo(p1,i)) );
}
+ else if ( fImplic )
+ {
+ iLit = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Abc_LitNot(Gia_ObjFanin0Copy(Gia_ManPo(p1,i))) );
+ Gia_ManAppendCo( pNew, iLit );
+ }
else
{
iLit = Gia_ManHashXor( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin0Copy(Gia_ManCo(p1,i)) );
@@ -2008,6 +2018,22 @@ Gia_Man_t * Gia_ManMiter( Gia_Man_t * p0, Gia_Man_t * p1, int nInsDup, int fDual
/**Function*************************************************************
+ Synopsis [Computes the AND of all POs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManDupAnd( Gia_Man_t * p, int fCompl )
+{
+ return NULL;
+}
+
+/**Function*************************************************************
+
Synopsis [Transforms the circuit into a regular miter.]
Description []
diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c
index 13443414..c5dba25b 100644
--- a/src/aig/gia/giaEquiv.c
+++ b/src/aig/gia/giaEquiv.c
@@ -1882,7 +1882,7 @@ int Gia_ManFilterEquivsForSpeculation( Gia_Man_t * pGia, char * pName1, char * p
Abc_Print( 1, "Cannot read second file %s.\n", pName2 );
return 0;
}
- pMiter = Gia_ManMiter( pGia1, pGia2, 0, 0, 1, 0 );
+ pMiter = Gia_ManMiter( pGia1, pGia2, 0, 0, 1, 0, 0 );
if ( pMiter == NULL )
{
Gia_ManStop( pGia1 );
@@ -2021,7 +2021,7 @@ int Gia_ManFilterEquivsUsingParts( Gia_Man_t * pGia, char * pName1, char * pName
Abc_Print( 1, "Cannot read second file %s.\n", pName2 );
return 0;
}
- pMiter = Gia_ManMiter( pGia1, pGia2, 0, 0, 1, 0 );
+ pMiter = Gia_ManMiter( pGia1, pGia2, 0, 0, 1, 0, 0 );
if ( pMiter == NULL )
{
Gia_ManStop( pGia1 );
diff --git a/src/aig/gia/giaSweeper.c b/src/aig/gia/giaSweeper.c
index 4cad0bdc..838b9978 100644
--- a/src/aig/gia/giaSweeper.c
+++ b/src/aig/gia/giaSweeper.c
@@ -784,7 +784,7 @@ int Gia_SweeperCheckEquiv( Gia_Man_t * pGia, int Probe1, int Probe2 )
{
iLitAig = Gia_SweeperProbeLit( pGia, ProbeId );
Gia_ManCnfNodeAddToSolver( p, Abc_Lit2Var(iLitAig) );
- Vec_IntPush( p->vCondAssump, Swp_ManLit2Lit(p, iLitAig) );
+ Vec_IntPush( p->vCondAssump, Abc_LitNot(Swp_ManLit2Lit(p, iLitAig)) );
}
Gia_ManCnfNodeAddToSolver( p, Abc_Lit2Var(iLitOld) );
Gia_ManCnfNodeAddToSolver( p, Abc_Lit2Var(iLitNew) );
@@ -969,6 +969,27 @@ Vec_Int_t * Gia_SweeperGraft( Gia_Man_t * pDst, Vec_Int_t * vProbes, Gia_Man_t *
/**Function*************************************************************
+ Synopsis [Verification of the sweeper.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Gia_SweeperVerify( Gia_Man_t * p0, Gia_Man_t * p1, Gia_Man_t * pC )
+{
+ Gia_Man_t * pMiter = Gia_ManMiter( p0, p1, 0, 0, 0, 0, 0 );
+ Gia_Man_t * pConstr = Gia_ManDupAnd( pC, 0 );
+
+ Gia_ManStop( pConstr );
+ Gia_ManStop( pMiter );
+ return 1;
+}
+
+/**Function*************************************************************
+
Synopsis [Performs conditional sweeping of the cone.]
Description [Returns the result as a new GIA manager with as many inputs
@@ -995,7 +1016,7 @@ Gia_Man_t * Gia_SweeperSweep( Gia_Man_t * p, Vec_Int_t * vProbeOuts, int nWords,
pGiaCond = Gia_SweeperExtractUserLogic( p, vProbeConds, NULL, NULL );
pGiaOuts = Gia_SweeperExtractUserLogic( p, vProbeOuts, NULL, NULL );
Gia_ManSetPhase( pGiaOuts );
- // if there is no conditions, define constant true constrain (constant 0 output)
+ // if there is no conditions, define constant true constraint (constant 0 output)
if ( Gia_ManPoNum(pGiaCond) == 0 )
Gia_ManAppendCo( pGiaCond, Gia_ManConst0Lit() );
// perform sweeping under constraints
diff --git a/src/aig/gia/giaTim.c b/src/aig/gia/giaTim.c
index 16d09445..ea5ec003 100644
--- a/src/aig/gia/giaTim.c
+++ b/src/aig/gia/giaTim.c
@@ -554,7 +554,7 @@ int Gia_ManVerifyWithBoxes( Gia_Man_t * pGia, void * pParsInit )
pGia1 = Gia_ManDupCollapse( pGia, pGia->pAigExtra, NULL );
Vec_IntFreeP( &vBoxPres );
// compute the miter
- pMiter = Gia_ManMiter( pGia0, pGia1, 0, 1, 0, fVerbose );
+ pMiter = Gia_ManMiter( pGia0, pGia1, 0, 1, 0, 0, fVerbose );
if ( pMiter )
{
Cec_ParCec_t ParsCec, * pPars = &ParsCec;
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 0681f28e..e37944cf 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -27966,7 +27966,7 @@ int Abc_CommandAbc9Miter( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
}
// compute the miter
- pAux = Gia_ManMiter( pAbc->pGia, pSecond, nInsDup, fDualOut, fSeq, fVerbose );
+ pAux = Gia_ManMiter( pAbc->pGia, pSecond, nInsDup, fDualOut, fSeq, 0, fVerbose );
Gia_ManStop( pSecond );
Abc_FrameUpdateGia( pAbc, pAux );
return 0;
@@ -29352,7 +29352,7 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
}
// compute the miter
- pMiter = Gia_ManMiter( pAbc->pGia, pSecond, 0, 1, 0, pPars->fVerbose );
+ pMiter = Gia_ManMiter( pAbc->pGia, pSecond, 0, 1, 0, 0, pPars->fVerbose );
if ( pMiter )
{
if ( fDumpMiter )
diff --git a/src/proof/cec/cecCec.c b/src/proof/cec/cecCec.c
index 1d4c83b6..f3b1a3b0 100644
--- a/src/proof/cec/cecCec.c
+++ b/src/proof/cec/cecCec.c
@@ -301,7 +301,7 @@ int Cec_ManVerifyTwo( Gia_Man_t * p0, Gia_Man_t * p1, int fVerbose )
int RetValue;
Cec_ManCecSetDefaultParams( pPars );
pPars->fVerbose = fVerbose;
- pMiter = Gia_ManMiter( p0, p1, 0, 1, 0, pPars->fVerbose );
+ pMiter = Gia_ManMiter( p0, p1, 0, 1, 0, 0, pPars->fVerbose );
if ( pMiter == NULL )
return -1;
RetValue = Cec_ManVerify( pMiter, pPars );
diff --git a/src/sat/bmc/bmcICheck.c b/src/sat/bmc/bmcICheck.c
index e388db04..4376c336 100644
--- a/src/sat/bmc/bmcICheck.c
+++ b/src/sat/bmc/bmcICheck.c
@@ -206,7 +206,7 @@ void Bmc_PerformICheck( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fEmpty,
// create miter
pTemp = Gia_ManDup( p );
- pMiter = Gia_ManMiter( p, pTemp, 0, 1, 1, 0 );
+ pMiter = Gia_ManMiter( p, pTemp, 0, 1, 1, 0, 0 );
Gia_ManStop( pTemp );
assert( Gia_ManPoNum(pMiter) == 2 * Gia_ManPoNum(p) );
assert( Gia_ManRegNum(pMiter) == 2 * Gia_ManRegNum(p) );
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-02 22:45:44 +0000