summaryrefslogtreecommitdiffstats
path: root/src/proof/int
diff options
context:
space:
mode:
Diffstat (limited to 'src/proof/int')
-rw-r--r--src/proof/int/intCheck.c20
-rw-r--r--src/proof/int/intContain.c10
-rw-r--r--src/proof/int/intCore.c10
-rw-r--r--src/proof/int/intCtrex.c2
-rw-r--r--src/proof/int/intDup.c4
-rw-r--r--src/proof/int/intFrames.c2
-rw-r--r--src/proof/int/intInter.c6
-rw-r--r--src/proof/int/intM114.c16
-rw-r--r--src/proof/int/intM114p.c8
9 files changed, 39 insertions, 39 deletions
diff --git a/src/proof/int/intCheck.c b/src/proof/int/intCheck.c
index 57d6e7d0..2b14d8ae 100644
--- a/src/proof/int/intCheck.c
+++ b/src/proof/int/intCheck.c
@@ -112,10 +112,10 @@ Inter_Check_t * Inter_CheckStart( Aig_Man_t * pTrans, int nFramesK )
p->vAssLits = Vec_IntAlloc( 100 );
// generate the timeframes
p->pFrames = Inter_ManUnrollFrames( pTrans, nFramesK );
- assert( Aig_ManPiNum(p->pFrames) == nFramesK * Saig_ManPiNum(pTrans) + Saig_ManRegNum(pTrans) );
- assert( Aig_ManPoNum(p->pFrames) == nFramesK * Saig_ManRegNum(pTrans) );
+ assert( Aig_ManCiNum(p->pFrames) == nFramesK * Saig_ManPiNum(pTrans) + Saig_ManRegNum(pTrans) );
+ assert( Aig_ManCoNum(p->pFrames) == nFramesK * Saig_ManRegNum(pTrans) );
// convert to CNF
- p->pCnf = Cnf_Derive( p->pFrames, Aig_ManPoNum(p->pFrames) );
+ p->pCnf = Cnf_Derive( p->pFrames, Aig_ManCoNum(p->pFrames) );
p->pSat = (sat_solver *)Cnf_DataWriteIntoSolver( p->pCnf, 1, 0 );
// assign parameters
p->nFramesK = nFramesK;
@@ -221,9 +221,9 @@ int Inter_CheckPerform( Inter_Check_t * p, Cnf_Dat_t * pCnfInt, int nTimeNewOut
{
Aig_Obj_t * pObj, * pObj2;
int i, f, VarA, VarB, RetValue, Entry, status;
- int nRegs = Aig_ManPiNum(pCnfInt->pMan);
- assert( Aig_ManPoNum(p->pCnf->pMan) == p->nFramesK * nRegs );
- assert( Aig_ManPoNum(pCnfInt->pMan) == 1 );
+ int nRegs = Aig_ManCiNum(pCnfInt->pMan);
+ assert( Aig_ManCoNum(p->pCnf->pMan) == p->nFramesK * nRegs );
+ assert( Aig_ManCoNum(pCnfInt->pMan) == 1 );
// set runtime limit
if ( nTimeNewOut )
@@ -242,7 +242,7 @@ int Inter_CheckPerform( Inter_Check_t * p, Cnf_Dat_t * pCnfInt, int nTimeNewOut
// add equality clauses for the flop variables
Aig_ManForEachCi( pCnfInt->pMan, pObj, i )
{
- pObj2 = f ? Aig_ManPo(p->pFrames, i + (f-1) * nRegs) : Aig_ManPi(p->pFrames, i);
+ pObj2 = f ? Aig_ManCo(p->pFrames, i + (f-1) * nRegs) : Aig_ManCi(p->pFrames, i);
Inter_CheckAddEqual( p, pCnfInt->pVarNums[pObj->Id], p->pCnf->pVarNums[pObj2->Id] );
}
// add final clauses
@@ -251,14 +251,14 @@ int Inter_CheckPerform( Inter_Check_t * p, Cnf_Dat_t * pCnfInt, int nTimeNewOut
if ( f == Vec_IntSize(p->vOrLits) ) // find time here
{
// add literal to this frame
- VarB = pCnfInt->pVarNums[ Aig_ManPo(pCnfInt->pMan, 0)->Id ];
+ VarB = pCnfInt->pVarNums[ Aig_ManCo(pCnfInt->pMan, 0)->Id ];
Vec_IntPush( p->vOrLits, VarB );
}
else
{
// add OR gate for this frame
VarA = Vec_IntEntry( p->vOrLits, f );
- VarB = pCnfInt->pVarNums[ Aig_ManPo(pCnfInt->pMan, 0)->Id ];
+ VarB = pCnfInt->pVarNums[ Aig_ManCo(pCnfInt->pMan, 0)->Id ];
Inter_CheckAddOrGate( p, VarA, VarB, p->nVars + pCnfInt->nVars );
Vec_IntWriteEntry( p->vOrLits, f, p->nVars + pCnfInt->nVars ); // using var ID!
}
@@ -266,7 +266,7 @@ int Inter_CheckPerform( Inter_Check_t * p, Cnf_Dat_t * pCnfInt, int nTimeNewOut
else
{
// add AND gate for this frame
- VarB = pCnfInt->pVarNums[ Aig_ManPo(pCnfInt->pMan, 0)->Id ];
+ VarB = pCnfInt->pVarNums[ Aig_ManCo(pCnfInt->pMan, 0)->Id ];
Vec_IntPush( p->vAndLits, VarB );
}
// update variable IDs
diff --git a/src/proof/int/intContain.c b/src/proof/int/intContain.c
index 213c557c..a031c7a4 100644
--- a/src/proof/int/intContain.c
+++ b/src/proof/int/intContain.c
@@ -161,7 +161,7 @@ void Inter_ManAppendCone( Aig_Man_t * pOld, Aig_Man_t * pNew, Aig_Obj_t ** ppNew
{
Aig_Obj_t * pObj;
int i;
- assert( Aig_ManPoNum(pOld) == 1 );
+ assert( Aig_ManCoNum(pOld) == 1 );
// create the PIs
Aig_ManCleanData( pOld );
Aig_ManConst1(pOld)->pData = Aig_ManConst1(pNew);
@@ -171,7 +171,7 @@ void Inter_ManAppendCone( Aig_Man_t * pOld, Aig_Man_t * pNew, Aig_Obj_t ** ppNew
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 );
+ pObj = Aig_ManCo( pOld, 0 );
Aig_ObjCreateCo( pNew, Aig_NotCond( Aig_ObjChild0Copy(pObj), fCompl ) );
}
@@ -283,7 +283,7 @@ int Inter_ManCheckUniqueness( Aig_Man_t * p, sat_solver * pSat, Cnf_Dat_t * pCnf
return 1;
// assert( Saig_ManPoNum(p) == 1 );
assert( Aig_ManRegNum(p) > 0 );
- assert( Aig_ManRegNum(p) < Aig_ManPiNum(p) );
+ assert( Aig_ManRegNum(p) < Aig_ManCiNum(p) );
// get the counter-example
vPis = Vec_IntAlloc( 100 );
@@ -303,12 +303,12 @@ int Inter_ManCheckUniqueness( Aig_Man_t * p, sat_solver * pSat, Cnf_Dat_t * pCnf
for ( i = 0; i < nFrames; i++ )
Aig_ManForEachPiSeq( p, pObj, k )
Fra_SmlAssignConst( pSml, pObj, pCounterEx[iBit++], i );
- assert( iBit == Aig_ManPiNum(pCnf->pMan) );
+ assert( iBit == Aig_ManCiNum(pCnf->pMan) );
// run simulation
Fra_SmlSimulateOne( pSml );
// check if the given output has failed
-// RetValue = !Fra_SmlNodeIsZero( pSml, Aig_ManPo(pAig, 0) );
+// RetValue = !Fra_SmlNodeIsZero( pSml, Aig_ManCo(pAig, 0) );
// assert( RetValue );
// check values at the internal nodes
diff --git a/src/proof/int/intCore.c b/src/proof/int/intCore.c
index 10a8fc74..8bef9c59 100644
--- a/src/proof/int/intCore.c
+++ b/src/proof/int/intCore.c
@@ -139,7 +139,7 @@ clk2 = clock();
p->pInter = Inter_ManStartOneOutput( pAig, 1 );
else
p->pInter = Inter_ManStartInitState( Aig_ManRegNum(pAig) );
- assert( Aig_ManPoNum(p->pInter) == 1 );
+ assert( Aig_ManCoNum(p->pInter) == 1 );
clk = clock();
p->pCnfInter = Cnf_Derive( p->pInter, 0 );
p->timeCnf += clock() - clk;
@@ -157,7 +157,7 @@ p->timeRwr += clock() - clk;
// can also do SAT sweeping on the timeframes...
clk = clock();
if ( pPars->fUseBackward )
- p->pCnfFrames = Cnf_Derive( p->pFrames, Aig_ManPoNum(p->pFrames) );
+ p->pCnfFrames = Cnf_Derive( p->pFrames, Aig_ManCoNum(p->pFrames) );
else
// p->pCnfFrames = Cnf_Derive( p->pFrames, 0 );
p->pCnfFrames = Cnf_DeriveSimple( p->pFrames, 0 );
@@ -285,7 +285,7 @@ clk = clock();
p->timeRwr += clock() - clk;
// check if interpolant is trivial
- if ( p->pInterNew == NULL || Aig_ObjChild0(Aig_ManPo(p->pInterNew,0)) == Aig_ManConst0(p->pInterNew) )
+ if ( p->pInterNew == NULL || Aig_ObjChild0(Aig_ManCo(p->pInterNew,0)) == Aig_ManConst0(p->pInterNew) )
{
// printf( "interpolant is constant 0\n" );
if ( pPars->fVerbose )
@@ -300,7 +300,7 @@ p->timeRwr += clock() - clk;
clk = clock();
if ( pPars->fCheckKstep ) // k-step unique-state induction
{
- if ( Aig_ManPiNum(p->pInterNew) == Aig_ManPiNum(p->pInter) )
+ if ( Aig_ManCiNum(p->pInterNew) == Aig_ManCiNum(p->pInter) )
{
if ( pPars->fTransLoop || pPars->fUseBackward || pPars->nFramesK > 1 )
{
@@ -326,7 +326,7 @@ timeTemp = clock() - clk2;
}
else // combinational containment
{
- if ( Aig_ManPiNum(p->pInterNew) == Aig_ManPiNum(p->pInter) )
+ if ( Aig_ManCiNum(p->pInterNew) == Aig_ManCiNum(p->pInter) )
Status = Inter_ManCheckContainment( p->pInterNew, p->pInter );
else
Status = 0;
diff --git a/src/proof/int/intCtrex.c b/src/proof/int/intCtrex.c
index 22e689f4..04aaa271 100644
--- a/src/proof/int/intCtrex.c
+++ b/src/proof/int/intCtrex.c
@@ -75,7 +75,7 @@ Aig_Man_t * Inter_ManFramesBmc( Aig_Man_t * pAig, int nFrames )
pObjLo->pData = pObjLi->pData;
}
// create POs for the output of the last frame
- pObj = Aig_ManPo( pAig, 0 );
+ pObj = Aig_ManCo( pAig, 0 );
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 adc692cb..d7bc73d6 100644
--- a/src/proof/int/intDup.c
+++ b/src/proof/int/intDup.c
@@ -141,7 +141,7 @@ Aig_Man_t * Inter_ManStartOneOutput( Aig_Man_t * p, int fAddFirstPo )
}
// set registers
pNew->nRegs = fAddFirstPo? 0 : p->nRegs;
- pNew->nTruePis = fAddFirstPo? Aig_ManPiNum(p) + 1 : p->nTruePis + 1;
+ pNew->nTruePis = fAddFirstPo? Aig_ManCiNum(p) + 1 : p->nTruePis + 1;
pNew->nTruePos = fAddFirstPo + Saig_ManConstrNum(p);
// duplicate internal nodes
Aig_ManForEachNode( p, pObj, i )
@@ -158,7 +158,7 @@ Aig_Man_t * Inter_ManStartOneOutput( Aig_Man_t * p, int fAddFirstPo )
// add the PO
if ( fAddFirstPo )
{
- pObj = Aig_ManPo( p, 0 );
+ pObj = Aig_ManCo( p, 0 );
Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
}
else
diff --git a/src/proof/int/intFrames.c b/src/proof/int/intFrames.c
index 8e74d99a..7c5231b7 100644
--- a/src/proof/int/intFrames.c
+++ b/src/proof/int/intFrames.c
@@ -99,7 +99,7 @@ Aig_Man_t * Inter_ManFramesInter( Aig_Man_t * pAig, int nFrames, int fAddRegOuts
// create the only PO of the manager
else
{
- pObj = Aig_ManPo( pAig, 0 );
+ pObj = Aig_ManCo( pAig, 0 );
Aig_ObjCreateCo( pFrames, Aig_ObjChild0Copy(pObj) );
}
Aig_ManCleanup( pFrames );
diff --git a/src/proof/int/intInter.c b/src/proof/int/intInter.c
index ef32294b..ffc462d3 100644
--- a/src/proof/int/intInter.c
+++ b/src/proof/int/intInter.c
@@ -45,10 +45,10 @@ ABC_NAMESPACE_IMPL_START
Aig_Man_t * Inter_ManDupExpand( Aig_Man_t * pInter, Aig_Man_t * pOther )
{
Aig_Man_t * pInterC;
- assert( Aig_ManPiNum(pInter) <= Aig_ManPiNum(pOther) );
+ assert( Aig_ManCiNum(pInter) <= Aig_ManCiNum(pOther) );
pInterC = Aig_ManDupSimple( pInter );
- Aig_IthVar( pInterC, Aig_ManPiNum(pOther)-1 );
- assert( Aig_ManPiNum(pInterC) == Aig_ManPiNum(pOther) );
+ Aig_IthVar( pInterC, Aig_ManCiNum(pOther)-1 );
+ assert( Aig_ManCiNum(pInterC) == Aig_ManCiNum(pOther) );
return pInterC;
}
diff --git a/src/proof/int/intM114.c b/src/proof/int/intM114.c
index c37cb2c6..ed3ef80e 100644
--- a/src/proof/int/intM114.c
+++ b/src/proof/int/intM114.c
@@ -61,10 +61,10 @@ sat_solver * Inter_ManDeriveSatSolver(
assert( Aig_ManRegNum(pInter) == 0 );
assert( Aig_ManRegNum(pAig) > 0 );
assert( Aig_ManRegNum(pFrames) == 0 );
- assert( Aig_ManPoNum(pInter) == 1 );
- assert( Aig_ManPoNum(pFrames) == fUseBackward? Saig_ManRegNum(pAig) : 1 );
- assert( fUseBackward || Aig_ManPiNum(pInter) == Aig_ManRegNum(pAig) );
-// assert( (Aig_ManPiNum(pFrames) - Aig_ManRegNum(pAig)) % Saig_ManPiNum(pAig) == 0 );
+ assert( Aig_ManCoNum(pInter) == 1 );
+ assert( Aig_ManCoNum(pFrames) == fUseBackward? Saig_ManRegNum(pAig) : 1 );
+ assert( fUseBackward || Aig_ManCiNum(pInter) == Aig_ManRegNum(pAig) );
+// assert( (Aig_ManCiNum(pFrames) - Aig_ManRegNum(pAig)) % Saig_ManPiNum(pAig) == 0 );
// prepare CNFs
Cnf_DataLift( pCnfAig, pCnfFrames->nVars );
@@ -93,12 +93,12 @@ sat_solver * Inter_ManDeriveSatSolver(
{
Saig_ManForEachLi( pAig, pObj2, i )
{
- if ( Saig_ManRegNum(pAig) == Aig_ManPiNum(pInter) )
- pObj = Aig_ManPi( pInter, i );
+ if ( Saig_ManRegNum(pAig) == Aig_ManCiNum(pInter) )
+ pObj = Aig_ManCi( pInter, i );
else
{
- assert( Aig_ManPiNum(pAig) == Aig_ManPiNum(pInter) );
- pObj = Aig_ManPi( pInter, Aig_ManPiNum(pAig)-Saig_ManRegNum(pAig) + i );
+ assert( Aig_ManCiNum(pAig) == Aig_ManCiNum(pInter) );
+ pObj = Aig_ManCi( pInter, Aig_ManCiNum(pAig)-Saig_ManRegNum(pAig) + i );
}
Lits[0] = toLitCond( pCnfInter->pVarNums[pObj->Id], 0 );
diff --git a/src/proof/int/intM114p.c b/src/proof/int/intM114p.c
index 6164a389..f143dc39 100644
--- a/src/proof/int/intM114p.c
+++ b/src/proof/int/intM114p.c
@@ -59,10 +59,10 @@ M114p_Solver_t Inter_ManDeriveSatSolverM114p(
assert( Aig_ManRegNum(pInter) == 0 );
assert( Aig_ManRegNum(pAig) > 0 );
assert( Aig_ManRegNum(pFrames) == 0 );
- assert( Aig_ManPoNum(pInter) == 1 );
- assert( Aig_ManPoNum(pFrames) == 1 );
- assert( Aig_ManPiNum(pInter) == Aig_ManRegNum(pAig) );
-// assert( (Aig_ManPiNum(pFrames) - Aig_ManRegNum(pAig)) % Saig_ManPiNum(pAig) == 0 );
+ assert( Aig_ManCoNum(pInter) == 1 );
+ assert( Aig_ManCoNum(pFrames) == 1 );
+ assert( Aig_ManCiNum(pInter) == Aig_ManRegNum(pAig) );
+// assert( (Aig_ManCiNum(pFrames) - Aig_ManRegNum(pAig)) % Saig_ManPiNum(pAig) == 0 );
// prepare CNFs
Cnf_DataLift( pCnfAig, pCnfFrames->nVars );
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-04 21:34:52 +0000