summaryrefslogtreecommitdiffstats
path: root/src/proof/int
diff options
context:
space:
mode:
Diffstat (limited to 'src/proof/int')
-rw-r--r--src/proof/int/intCheck.c8
-rw-r--r--src/proof/int/intContain.c10
-rw-r--r--src/proof/int/intCtrex.c4
-rw-r--r--src/proof/int/intDup.c24
-rw-r--r--src/proof/int/intFrames.c10
-rw-r--r--src/proof/int/intM114.c6
-rw-r--r--src/proof/int/intM114p.c8
7 files changed, 35 insertions, 35 deletions
diff --git a/src/proof/int/intCheck.c b/src/proof/int/intCheck.c
index 6b36fe30..57d6e7d0 100644
--- a/src/proof/int/intCheck.c
+++ b/src/proof/int/intCheck.c
@@ -67,13 +67,13 @@ Aig_Man_t * Inter_ManUnrollFrames( Aig_Man_t * pAig, int nFrames )
Aig_ManConst1(pAig)->pData = Aig_ManConst1( pFrames );
// create variables for register outputs
Saig_ManForEachLo( pAig, pObj, i )
- pObj->pData = Aig_ObjCreatePi( pFrames );
+ pObj->pData = Aig_ObjCreateCi( pFrames );
// add timeframes
for ( f = 0; f < nFrames; f++ )
{
// create PI nodes for this frame
Saig_ManForEachPi( pAig, pObj, i )
- pObj->pData = Aig_ObjCreatePi( pFrames );
+ pObj->pData = Aig_ObjCreateCi( pFrames );
// add internal nodes of this frame
Aig_ManForEachNode( pAig, pObj, i )
pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
@@ -84,7 +84,7 @@ Aig_Man_t * Inter_ManUnrollFrames( Aig_Man_t * pAig, int nFrames )
Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i )
{
pObjLo->pData = pObjLi->pData;
- Aig_ObjCreatePo( pFrames, (Aig_Obj_t *)pObjLo->pData );
+ Aig_ObjCreateCo( pFrames, (Aig_Obj_t *)pObjLo->pData );
}
}
Aig_ManCleanup( pFrames );
@@ -240,7 +240,7 @@ int Inter_CheckPerform( Inter_Check_t * p, Cnf_Dat_t * pCnfInt, int nTimeNewOut
assert( RetValue );
}
// add equality clauses for the flop variables
- Aig_ManForEachPi( pCnfInt->pMan, pObj, i )
+ Aig_ManForEachCi( pCnfInt->pMan, pObj, i )
{
pObj2 = f ? Aig_ManPo(p->pFrames, i + (f-1) * nRegs) : Aig_ManPi(p->pFrames, i);
Inter_CheckAddEqual( p, pCnfInt->pVarNums[pObj->Id], p->pCnf->pVarNums[pObj2->Id] );
diff --git a/src/proof/int/intContain.c b/src/proof/int/intContain.c
index 58b408d7..213c557c 100644
--- a/src/proof/int/intContain.c
+++ b/src/proof/int/intContain.c
@@ -121,7 +121,7 @@ Aig_Man_t * Inter_ManFramesLatches( Aig_Man_t * pAig, int nFrames, Vec_Ptr_t **
*pvMapReg = Vec_PtrAlloc( (nFrames+1) * Saig_ManRegNum(pAig) );
Saig_ManForEachLo( pAig, pObj, i )
{
- pObj->pData = Aig_ObjCreatePi( pFrames );
+ pObj->pData = Aig_ObjCreateCi( pFrames );
Vec_PtrPush( *pvMapReg, pObj->pData );
}
// add timeframes
@@ -129,7 +129,7 @@ Aig_Man_t * Inter_ManFramesLatches( Aig_Man_t * pAig, int nFrames, Vec_Ptr_t **
{
// create PI nodes for this frame
Saig_ManForEachPi( pAig, pObj, i )
- pObj->pData = Aig_ObjCreatePi( pFrames );
+ pObj->pData = Aig_ObjCreateCi( pFrames );
// add internal nodes of this frame
Aig_ManForEachNode( pAig, pObj, i )
pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
@@ -165,14 +165,14 @@ void Inter_ManAppendCone( Aig_Man_t * pOld, Aig_Man_t * pNew, Aig_Obj_t ** ppNew
// create the PIs
Aig_ManCleanData( pOld );
Aig_ManConst1(pOld)->pData = Aig_ManConst1(pNew);
- Aig_ManForEachPi( pOld, pObj, i )
+ Aig_ManForEachCi( pOld, pObj, i )
pObj->pData = ppNewPis[i];
// duplicate internal nodes
Aig_ManForEachNode( pOld, pObj, i )
pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
// add one PO to new
pObj = Aig_ManPo( pOld, 0 );
- Aig_ObjCreatePo( pNew, Aig_NotCond( Aig_ObjChild0Copy(pObj), fCompl ) );
+ Aig_ObjCreateCo( pNew, Aig_NotCond( Aig_ObjChild0Copy(pObj), fCompl ) );
}
@@ -287,7 +287,7 @@ int Inter_ManCheckUniqueness( Aig_Man_t * p, sat_solver * pSat, Cnf_Dat_t * pCnf
// get the counter-example
vPis = Vec_IntAlloc( 100 );
- Aig_ManForEachPi( pCnf->pMan, pObj, k )
+ Aig_ManForEachCi( pCnf->pMan, pObj, k )
Vec_IntPush( vPis, pCnf->pVarNums[Aig_ObjId(pObj)] );
assert( Vec_IntSize(vPis) == Aig_ManRegNum(p) + nFrames * Saig_ManPiNum(p) );
pCounterEx = Sat_SolverGetModel( pSat, vPis->pArray, vPis->nSize );
diff --git a/src/proof/int/intCtrex.c b/src/proof/int/intCtrex.c
index 9ba8c9df..22e689f4 100644
--- a/src/proof/int/intCtrex.c
+++ b/src/proof/int/intCtrex.c
@@ -61,7 +61,7 @@ Aig_Man_t * Inter_ManFramesBmc( Aig_Man_t * pAig, int nFrames )
{
// create PI nodes for this frame
Saig_ManForEachPi( pAig, pObj, i )
- pObj->pData = Aig_ObjCreatePi( pFrames );
+ pObj->pData = Aig_ObjCreateCi( pFrames );
// add internal nodes of this frame
Aig_ManForEachNode( pAig, pObj, i )
pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
@@ -76,7 +76,7 @@ Aig_Man_t * Inter_ManFramesBmc( Aig_Man_t * pAig, int nFrames )
}
// create POs for the output of the last frame
pObj = Aig_ManPo( pAig, 0 );
- Aig_ObjCreatePo( pFrames, Aig_ObjChild0Copy(pObj) );
+ Aig_ObjCreateCo( pFrames, Aig_ObjChild0Copy(pObj) );
Aig_ManCleanup( pFrames );
return pFrames;
}
diff --git a/src/proof/int/intDup.c b/src/proof/int/intDup.c
index 551473ef..adc692cb 100644
--- a/src/proof/int/intDup.c
+++ b/src/proof/int/intDup.c
@@ -52,9 +52,9 @@ Aig_Man_t * Inter_ManStartInitState( int nRegs )
ppInputs = ABC_ALLOC( Aig_Obj_t *, nRegs );
p = Aig_ManStart( nRegs );
for ( i = 0; i < nRegs; i++ )
- ppInputs[i] = Aig_Not( Aig_ObjCreatePi(p) );
+ ppInputs[i] = Aig_Not( Aig_ObjCreateCi(p) );
pRes = Aig_Multi( p, ppInputs, nRegs, AIG_OBJ_AND );
- Aig_ObjCreatePo( p, pRes );
+ Aig_ObjCreateCo( p, pRes );
ABC_FREE( ppInputs );
return p;
}
@@ -83,8 +83,8 @@ Aig_Man_t * Inter_ManStartDuplicated( Aig_Man_t * p )
// create the PIs
Aig_ManCleanData( p );
Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
- Aig_ManForEachPi( p, pObj, i )
- pObj->pData = Aig_ObjCreatePi( pNew );
+ Aig_ManForEachCi( p, pObj, i )
+ pObj->pData = Aig_ObjCreateCi( pNew );
// set registers
pNew->nTruePis = p->nTruePis;
pNew->nTruePos = Saig_ManConstrNum(p);
@@ -98,12 +98,12 @@ Aig_Man_t * Inter_ManStartDuplicated( Aig_Man_t * p )
{
if ( i < Saig_ManPoNum(p)-Saig_ManConstrNum(p) )
continue;
- Aig_ObjCreatePo( pNew, Aig_Not( Aig_ObjChild0Copy(pObj) ) );
+ Aig_ObjCreateCo( pNew, Aig_Not( Aig_ObjChild0Copy(pObj) ) );
}
// create register inputs with MUXes
Saig_ManForEachLi( p, pObj, i )
- Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
+ Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
Aig_ManCleanup( pNew );
return pNew;
}
@@ -133,11 +133,11 @@ Aig_Man_t * Inter_ManStartOneOutput( Aig_Man_t * p, int fAddFirstPo )
// create the PIs
Aig_ManCleanData( p );
Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
- Aig_ManForEachPi( p, pObj, i )
+ Aig_ManForEachCi( p, pObj, i )
{
if ( i == Saig_ManPiNum(p) )
- pCtrl = Aig_ObjCreatePi( pNew );
- pObj->pData = Aig_ObjCreatePi( pNew );
+ pCtrl = Aig_ObjCreateCi( pNew );
+ pObj->pData = Aig_ObjCreateCi( pNew );
}
// set registers
pNew->nRegs = fAddFirstPo? 0 : p->nRegs;
@@ -152,14 +152,14 @@ Aig_Man_t * Inter_ManStartOneOutput( Aig_Man_t * p, int fAddFirstPo )
{
if ( i < Saig_ManPoNum(p)-Saig_ManConstrNum(p) )
continue;
- Aig_ObjCreatePo( pNew, Aig_Not( Aig_ObjChild0Copy(pObj) ) );
+ Aig_ObjCreateCo( pNew, Aig_Not( Aig_ObjChild0Copy(pObj) ) );
}
// add the PO
if ( fAddFirstPo )
{
pObj = Aig_ManPo( p, 0 );
- Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
+ Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
}
else
{
@@ -168,7 +168,7 @@ Aig_Man_t * Inter_ManStartOneOutput( Aig_Man_t * p, int fAddFirstPo )
{
pObj = Aig_Mux( pNew, pCtrl, (Aig_Obj_t *)pObjLo->pData, Aig_ObjChild0Copy(pObjLi) );
// pObj = Aig_Mux( pNew, pCtrl, Aig_ManConst0(pNew), Aig_ObjChild0Copy(pObjLi) );
- Aig_ObjCreatePo( pNew, pObj );
+ Aig_ObjCreateCo( pNew, pObj );
}
}
Aig_ManCleanup( pNew );
diff --git a/src/proof/int/intFrames.c b/src/proof/int/intFrames.c
index 0fbab6cb..8e74d99a 100644
--- a/src/proof/int/intFrames.c
+++ b/src/proof/int/intFrames.c
@@ -63,14 +63,14 @@ Aig_Man_t * Inter_ManFramesInter( Aig_Man_t * pAig, int nFrames, int fAddRegOuts
else
{
Saig_ManForEachLo( pAig, pObj, i )
- pObj->pData = Aig_ObjCreatePi( pFrames );
+ pObj->pData = Aig_ObjCreateCi( pFrames );
}
// add timeframes
for ( f = 0; f < nFrames; f++ )
{
// create PI nodes for this frame
Saig_ManForEachPi( pAig, pObj, i )
- pObj->pData = Aig_ObjCreatePi( pFrames );
+ pObj->pData = Aig_ObjCreateCi( pFrames );
// add internal nodes of this frame
Aig_ManForEachNode( pAig, pObj, i )
pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
@@ -79,7 +79,7 @@ Aig_Man_t * Inter_ManFramesInter( Aig_Man_t * pAig, int nFrames, int fAddRegOuts
{
if ( i < Saig_ManPoNum(pAig)-Saig_ManConstrNum(pAig) )
continue;
- Aig_ObjCreatePo( pFrames, Aig_Not( Aig_ObjChild0Copy(pObj) ) );
+ Aig_ObjCreateCo( pFrames, Aig_Not( Aig_ObjChild0Copy(pObj) ) );
}
if ( f == nFrames - 1 )
break;
@@ -94,13 +94,13 @@ Aig_Man_t * Inter_ManFramesInter( Aig_Man_t * pAig, int nFrames, int fAddRegOuts
if ( fAddRegOuts )
{
Saig_ManForEachLi( pAig, pObj, i )
- Aig_ObjCreatePo( pFrames, Aig_ObjChild0Copy(pObj) );
+ Aig_ObjCreateCo( pFrames, Aig_ObjChild0Copy(pObj) );
}
// create the only PO of the manager
else
{
pObj = Aig_ManPo( pAig, 0 );
- Aig_ObjCreatePo( pFrames, Aig_ObjChild0Copy(pObj) );
+ Aig_ObjCreateCo( pFrames, Aig_ObjChild0Copy(pObj) );
}
Aig_ManCleanup( pFrames );
return pFrames;
diff --git a/src/proof/int/intM114.c b/src/proof/int/intM114.c
index 139c9bbd..c37cb2c6 100644
--- a/src/proof/int/intM114.c
+++ b/src/proof/int/intM114.c
@@ -113,7 +113,7 @@ sat_solver * Inter_ManDeriveSatSolver(
}
else
{
- Aig_ManForEachPi( pInter, pObj, i )
+ Aig_ManForEachCi( pInter, pObj, i )
{
pObj2 = Saig_ManLo( pAig, i );
@@ -137,7 +137,7 @@ sat_solver * Inter_ManDeriveSatSolver(
Vec_IntClear( vVarsAB );
if ( fUseBackward )
{
- Aig_ManForEachPo( pFrames, pObj, i )
+ Aig_ManForEachCo( pFrames, pObj, i )
{
assert( pCnfFrames->pVarNums[pObj->Id] >= 0 );
Vec_IntPush( vVarsAB, pCnfFrames->pVarNums[pObj->Id] );
@@ -155,7 +155,7 @@ sat_solver * Inter_ManDeriveSatSolver(
}
else
{
- Aig_ManForEachPi( pFrames, pObj, i )
+ Aig_ManForEachCi( pFrames, pObj, i )
{
if ( i == Aig_ManRegNum(pAig) )
break;
diff --git a/src/proof/int/intM114p.c b/src/proof/int/intM114p.c
index 7c011426..6164a389 100644
--- a/src/proof/int/intM114p.c
+++ b/src/proof/int/intM114p.c
@@ -87,7 +87,7 @@ M114p_Solver_t Inter_ManDeriveSatSolverM114p(
assert( 0 );
}
// connector clauses
- Aig_ManForEachPi( pInter, pObj, i )
+ Aig_ManForEachCi( pInter, pObj, i )
{
pObj2 = Saig_ManLo( pAig, i );
Lits[0] = toLitCond( pCnfInter->pVarNums[pObj->Id], 0 );
@@ -109,7 +109,7 @@ M114p_Solver_t Inter_ManDeriveSatSolverM114p(
assert( 0 );
}
// connector clauses
- Aig_ManForEachPi( pFrames, pObj, i )
+ Aig_ManForEachCi( pFrames, pObj, i )
{
if ( i == Aig_ManRegNum(pAig) )
break;
@@ -296,7 +296,7 @@ Aig_Man_t * Inter_ManInterpolateM114pPudlak( M114p_Solver_t s, Vec_Int_t * vMapR
Vec_IntFree( vLiterals );
Vec_IntFree( vClauses );
Vec_IntFree( vResolvent );
- Aig_ObjCreatePo( p, pInter );
+ Aig_ObjCreateCo( p, pInter );
Aig_ManCleanup( p );
return p;
}
@@ -372,7 +372,7 @@ Aig_Man_t * Inter_ManpInterpolateM114( M114p_Solver_t s, Vec_Int_t * vMapRoots,
assert( Vec_PtrSize(vInters) == M114p_SolverProofClauseNum(s) );
Vec_PtrFree( vInters );
- Aig_ObjCreatePo( p, pInter );
+ Aig_ObjCreateCo( p, pInter );
Aig_ManCleanup( p );
assert( Aig_ManCheck(p) );
return p;
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-04 01:05:10 +0000