summaryrefslogtreecommitdiffstats
path: root/src/aig/saig/saigCexMin.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/saig/saigCexMin.c')
-rw-r--r--src/aig/saig/saigCexMin.c60
1 files changed, 30 insertions, 30 deletions
diff --git a/src/aig/saig/saigCexMin.c b/src/aig/saig/saigCexMin.c
index 824f9eb3..f1826f50 100644
--- a/src/aig/saig/saigCexMin.c
+++ b/src/aig/saig/saigCexMin.c
@@ -19,7 +19,7 @@
***********************************************************************/
#include "saig.h"
-#include "ioa.h"
+#include "src/aig/ioa/ioa.h"
ABC_NAMESPACE_IMPL_START
@@ -151,18 +151,18 @@ void Saig_ManCexMinDerivePhasePriority_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj )
Saig_ManCexMinDerivePhasePriority_rec( pAig, Aig_ObjFanin1(pObj) );
assert( Aig_ObjFanin0(pObj)->iData >= 0 );
assert( Aig_ObjFanin1(pObj)->iData >= 0 );
- fPhase0 = Aig_LitIsCompl( Aig_ObjFanin0(pObj)->iData ) ^ Aig_ObjFaninC0(pObj);
- fPhase1 = Aig_LitIsCompl( Aig_ObjFanin1(pObj)->iData ) ^ Aig_ObjFaninC1(pObj);
- iPrio0 = Aig_Lit2Var( Aig_ObjFanin0(pObj)->iData );
- iPrio1 = Aig_Lit2Var( Aig_ObjFanin1(pObj)->iData );
+ fPhase0 = Abc_LitIsCompl( Aig_ObjFanin0(pObj)->iData ) ^ Aig_ObjFaninC0(pObj);
+ fPhase1 = Abc_LitIsCompl( Aig_ObjFanin1(pObj)->iData ) ^ Aig_ObjFaninC1(pObj);
+ iPrio0 = Abc_Lit2Var( Aig_ObjFanin0(pObj)->iData );
+ iPrio1 = Abc_Lit2Var( Aig_ObjFanin1(pObj)->iData );
if ( fPhase0 && fPhase1 ) // both are one
- pObj->iData = Aig_Var2Lit( Abc_MinInt(iPrio0, iPrio1), 1 );
+ pObj->iData = Abc_Var2Lit( Abc_MinInt(iPrio0, iPrio1), 1 );
else if ( !fPhase0 && fPhase1 )
- pObj->iData = Aig_Var2Lit( iPrio0, 0 );
+ pObj->iData = Abc_Var2Lit( iPrio0, 0 );
else if ( fPhase0 && !fPhase1 )
- pObj->iData = Aig_Var2Lit( iPrio1, 0 );
+ pObj->iData = Abc_Var2Lit( iPrio1, 0 );
else // both are zero
- pObj->iData = Aig_Var2Lit( Abc_MaxInt(iPrio0, iPrio1), 0 );
+ pObj->iData = Abc_Var2Lit( Abc_MaxInt(iPrio0, iPrio1), 0 );
}
}
@@ -183,7 +183,7 @@ void Saig_ManCexMinVerifyPhase( Aig_Man_t * pAig, Abc_Cex_t * pCex, int f )
int i;
Aig_ManConst1(pAig)->fPhase = 1;
Saig_ManForEachPi( pAig, pObj, i )
- pObj->fPhase = Aig_InfoHasBit(pCex->pData, pCex->nRegs + f * pCex->nPis + i);
+ pObj->fPhase = Abc_InfoHasBit(pCex->pData, pCex->nRegs + f * pCex->nPis + i);
if ( f == 0 )
{
Saig_ManForEachLo( pAig, pObj, i )
@@ -266,7 +266,7 @@ Vec_Vec_t * Saig_ManCexMinCollectPhasePriority_( Aig_Man_t * pAig, Abc_Cex_t * p
// set the constant node to higher priority than the flops
vFramePPs = Vec_VecStart( pCex->iFrame+1 );
nPrioOffset = (pCex->iFrame + 1) * pCex->nPis;
- Aig_ManConst1(pAig)->iData = Aig_Var2Lit( nPrioOffset + pCex->nRegs, 1 );
+ Aig_ManConst1(pAig)->iData = Abc_Var2Lit( nPrioOffset + pCex->nRegs, 1 );
vRoots = Vec_IntAlloc( 1000 );
//printf( "Const1 = %d Offset = %d\n", Aig_ManConst1(pAig)->iData, nPrioOffset );
for ( f = 0; f <= pCex->iFrame; f++ )
@@ -280,9 +280,9 @@ Vec_Vec_t * Saig_ManCexMinCollectPhasePriority_( Aig_Man_t * pAig, Abc_Cex_t * p
{
assert( Aig_ObjIsPi(pObj) );
if ( Saig_ObjIsPi(pAig, pObj) )
- Vec_IntPush( vFramePPsOne, Aig_Var2Lit( (f+1) * pCex->nPis - nPiCount++, Aig_InfoHasBit(pCex->pData, pCex->nRegs + f * pCex->nPis + Aig_ObjPioNum(pObj)) ) );
+ Vec_IntPush( vFramePPsOne, Abc_Var2Lit( (f+1) * pCex->nPis - nPiCount++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + f * pCex->nPis + Aig_ObjPioNum(pObj)) ) );
else if ( f == 0 )
- Vec_IntPush( vFramePPsOne, Aig_Var2Lit( nPrioOffset + Saig_ObjRegId(pAig, pObj), 0 ) );
+ Vec_IntPush( vFramePPsOne, Abc_Var2Lit( nPrioOffset + Saig_ObjRegId(pAig, pObj), 0 ) );
else
{
Aig_Obj_t * pObj0 = Saig_ObjLoToLi(pAig, pObj);
@@ -298,7 +298,7 @@ Vec_Vec_t * Saig_ManCexMinCollectPhasePriority_( Aig_Man_t * pAig, Abc_Cex_t * p
Vec_IntFree( vRoots );
// check the output
pObj = Aig_ManPo( pAig, pCex->iPo );
- assert( Aig_LitIsCompl(pObj->iData) );
+ assert( Abc_LitIsCompl(pObj->iData) );
return vFramePPs;
}
@@ -327,7 +327,7 @@ Vec_Vec_t * Saig_ManCexMinCollectPhasePriority( Aig_Man_t * pAig, Abc_Cex_t * pC
// set the constant node to higher priority than the flops
vFramePPs = Vec_VecStart( pCex->iFrame+1 );
nPrioOffset = pCex->nRegs;
- Aig_ManConst1(pAig)->iData = Aig_Var2Lit( nPrioOffset + (pCex->iFrame + 1) * pCex->nPis, 1 );
+ Aig_ManConst1(pAig)->iData = Abc_Var2Lit( nPrioOffset + (pCex->iFrame + 1) * pCex->nPis, 1 );
vRoots = Vec_IntAlloc( 1000 );
//printf( "Const1 = %d Offset = %d\n", Aig_ManConst1(pAig)->iData, nPrioOffset );
for ( f = 0; f <= pCex->iFrame; f++ )
@@ -341,9 +341,9 @@ Vec_Vec_t * Saig_ManCexMinCollectPhasePriority( Aig_Man_t * pAig, Abc_Cex_t * pC
{
assert( Aig_ObjIsPi(pObj) );
if ( Saig_ObjIsPi(pAig, pObj) )
- Vec_IntPush( vFramePPsOne, Aig_Var2Lit( nPrioOffset + (f+1) * pCex->nPis - 1 - nPiCount++, Aig_InfoHasBit(pCex->pData, pCex->nRegs + f * pCex->nPis + Aig_ObjPioNum(pObj)) ) );
+ Vec_IntPush( vFramePPsOne, Abc_Var2Lit( nPrioOffset + (f+1) * pCex->nPis - 1 - nPiCount++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + f * pCex->nPis + Aig_ObjPioNum(pObj)) ) );
else if ( f == 0 )
- Vec_IntPush( vFramePPsOne, Aig_Var2Lit( Saig_ObjRegId(pAig, pObj), 0 ) );
+ Vec_IntPush( vFramePPsOne, Abc_Var2Lit( Saig_ObjRegId(pAig, pObj), 0 ) );
else
{
Aig_Obj_t * pObj0 = Saig_ObjLoToLi(pAig, pObj);
@@ -359,7 +359,7 @@ Vec_Vec_t * Saig_ManCexMinCollectPhasePriority( Aig_Man_t * pAig, Abc_Cex_t * pC
Vec_IntFree( vRoots );
// check the output
pObj = Aig_ManPo( pAig, pCex->iPo );
- assert( Aig_LitIsCompl(pObj->iData) );
+ assert( Abc_LitIsCompl(pObj->iData) );
return vFramePPs;
}
@@ -383,9 +383,9 @@ void Saig_ManCexMinCollectReason_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Int_t
if ( Aig_ObjIsPi(pObj) )
{
if ( fPiReason && Saig_ObjIsPi(p, pObj) )
- Vec_IntPush( vReason, Aig_Var2Lit( Aig_ObjPioNum(pObj), !Aig_LitIsCompl(pObj->iData) ) );
+ Vec_IntPush( vReason, Abc_Var2Lit( Aig_ObjPioNum(pObj), !Abc_LitIsCompl(pObj->iData) ) );
else if ( !fPiReason && Saig_ObjIsLo(p, pObj) )
- Vec_IntPush( vReason, Aig_Var2Lit( Saig_ObjRegId(p, pObj), !Aig_LitIsCompl(pObj->iData) ) );
+ Vec_IntPush( vReason, Abc_Var2Lit( Saig_ObjRegId(p, pObj), !Abc_LitIsCompl(pObj->iData) ) );
return;
}
if ( Aig_ObjIsPo(pObj) )
@@ -396,18 +396,18 @@ void Saig_ManCexMinCollectReason_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Int_t
if ( Aig_ObjIsConst1(pObj) )
return;
assert( Aig_ObjIsNode(pObj) );
- if ( Aig_LitIsCompl(pObj->iData) ) // value 1
+ if ( Abc_LitIsCompl(pObj->iData) ) // value 1
{
- int fPhase0 = Aig_LitIsCompl( Aig_ObjFanin0(pObj)->iData ) ^ Aig_ObjFaninC0(pObj);
- int fPhase1 = Aig_LitIsCompl( Aig_ObjFanin1(pObj)->iData ) ^ Aig_ObjFaninC1(pObj);
+ int fPhase0 = Abc_LitIsCompl( Aig_ObjFanin0(pObj)->iData ) ^ Aig_ObjFaninC0(pObj);
+ int fPhase1 = Abc_LitIsCompl( Aig_ObjFanin1(pObj)->iData ) ^ Aig_ObjFaninC1(pObj);
assert( fPhase0 && fPhase1 );
Saig_ManCexMinCollectReason_rec( p, Aig_ObjFanin0(pObj), vReason, fPiReason );
Saig_ManCexMinCollectReason_rec( p, Aig_ObjFanin1(pObj), vReason, fPiReason );
}
else
{
- int fPhase0 = Aig_LitIsCompl( Aig_ObjFanin0(pObj)->iData ) ^ Aig_ObjFaninC0(pObj);
- int fPhase1 = Aig_LitIsCompl( Aig_ObjFanin1(pObj)->iData ) ^ Aig_ObjFaninC1(pObj);
+ int fPhase0 = Abc_LitIsCompl( Aig_ObjFanin0(pObj)->iData ) ^ Aig_ObjFaninC0(pObj);
+ int fPhase1 = Abc_LitIsCompl( Aig_ObjFanin1(pObj)->iData ) ^ Aig_ObjFaninC1(pObj);
assert( !fPhase0 || !fPhase1 );
if ( !fPhase0 && fPhase1 )
Saig_ManCexMinCollectReason_rec( p, Aig_ObjFanin0(pObj), vReason, fPiReason );
@@ -415,8 +415,8 @@ void Saig_ManCexMinCollectReason_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Int_t
Saig_ManCexMinCollectReason_rec( p, Aig_ObjFanin1(pObj), vReason, fPiReason );
else
{
- int iPrio0 = Aig_Lit2Var( Aig_ObjFanin0(pObj)->iData );
- int iPrio1 = Aig_Lit2Var( Aig_ObjFanin1(pObj)->iData );
+ int iPrio0 = Abc_Lit2Var( Aig_ObjFanin0(pObj)->iData );
+ int iPrio1 = Abc_Lit2Var( Aig_ObjFanin1(pObj)->iData );
if ( iPrio0 >= iPrio1 )
Saig_ManCexMinCollectReason_rec( p, Aig_ObjFanin0(pObj), vReason, fPiReason );
else
@@ -514,7 +514,7 @@ Aig_Man_t * Saig_ManCexMinDupWithCubes( Aig_Man_t * pAig, Vec_Vec_t * vReg2Value
assert( pAig->nConstrs == 0 );
// start the new manager
pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) + Vec_VecSizeSize(vReg2Value) + Vec_VecSize(vReg2Value) );
- pAigNew->pName = Aig_UtilStrsav( pAig->pName );
+ pAigNew->pName = Abc_UtilStrsav( pAig->pName );
// map the constant node
Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew );
// create variables for PIs
@@ -532,8 +532,8 @@ Aig_Man_t * Saig_ManCexMinDupWithCubes( Aig_Man_t * pAig, Vec_Vec_t * vReg2Value
Vec_IntForEachEntry( vLevel, Lit, k )
{
assert( Lit >= 0 && Lit < 2 * Aig_ManRegNum(pAig) );
- pObj = Saig_ManLi( pAig, Aig_Lit2Var(Lit) );
- pMiter = Aig_And( pAigNew, pMiter, Aig_NotCond(Aig_ObjChild0Copy(pObj), Aig_LitIsCompl(Lit)) );
+ pObj = Saig_ManLi( pAig, Abc_Lit2Var(Lit) );
+ pMiter = Aig_And( pAigNew, pMiter, Aig_NotCond(Aig_ObjChild0Copy(pObj), Abc_LitIsCompl(Lit)) );
}
Aig_ObjCreatePo( pAigNew, pMiter );
}
generated by cgit v1.2.3 (git 2.25.1) at 2024-06-30 18:32:19 +0000