summaryrefslogtreecommitdiffstats
path: root/src/proof/cec
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2012-12-10 13:56:40 -0800
committerAlan Mishchenko <alanmi@berkeley.edu>2012-12-10 13:56:40 -0800
commit2575a5d6836c5bd8160b8e965c622e358b2dc742 (patch)
tree92eaa25ce4be9b47651e043e93fe55c7ea99b342 /src/proof/cec
parentf7b7ab59cf842053cc2819c9a569839dc970ed85 (diff)
downloadabc-2575a5d6836c5bd8160b8e965c622e358b2dc742.tar.gz
abc-2575a5d6836c5bd8160b8e965c622e358b2dc742.tar.bz2
abc-2575a5d6836c5bd8160b8e965c622e358b2dc742.zip
Unifification of custom extensions.
Diffstat (limited to 'src/proof/cec')
-rw-r--r--src/proof/cec/cecCec.c2
-rw-r--r--src/proof/cec/cecCore.c4
-rw-r--r--src/proof/cec/cecCorr.c2
-rw-r--r--src/proof/cec/cecSeq.c4
-rw-r--r--src/proof/cec/cecSolve.c2
-rw-r--r--src/proof/cec/cecSynth.c2
6 files changed, 8 insertions, 8 deletions
diff --git a/src/proof/cec/cecCec.c b/src/proof/cec/cecCec.c
index 30c930a0..72c3e7db 100644
--- a/src/proof/cec/cecCec.c
+++ b/src/proof/cec/cecCec.c
@@ -263,7 +263,7 @@ int Cec_ManVerify( Gia_Man_t * pInit, Cec_ParCec_t * pPars )
{
ABC_FREE( pNew->pReprs );
ABC_FREE( pNew->pNexts );
- Gia_WriteAiger( pNew, "gia_cec_undecided.aig", 0, 0 );
+ Gia_AigerWrite( pNew, "gia_cec_undecided.aig", 0, 0 );
Abc_Print( 1, "The result is written into file \"%s\".\n", "gia_cec_undecided.aig" );
}
if ( pPars->TimeLimit && (clock() - clkTotal)/CLOCKS_PER_SEC >= pPars->TimeLimit )
diff --git a/src/proof/cec/cecCore.c b/src/proof/cec/cecCore.c
index c45bd974..40d5fba6 100644
--- a/src/proof/cec/cecCore.c
+++ b/src/proof/cec/cecCore.c
@@ -398,7 +398,7 @@ p->timeSim += clock() - clk;
}
pSrm = Cec_ManFraSpecReduction( p );
-// Gia_WriteAiger( pSrm, "gia_srm.aig", 0, 0 );
+// Gia_AigerWrite( pSrm, "gia_srm.aig", 0, 0 );
if ( pPars->fVeryVerbose )
Gia_ManPrintStats( pSrm, 0, 0, 0 );
@@ -481,7 +481,7 @@ p->timeSat += clock() - clk;
Abc_Print( 1, "Increasing conflict limit to %d.\n", pParsSat->nBTLimit );
if ( fOutputResult )
{
- Gia_WriteAiger( p->pAig, "gia_cec_temp.aig", 0, 0 );
+ Gia_AigerWrite( p->pAig, "gia_cec_temp.aig", 0, 0 );
Abc_Print( 1,"The result is written into file \"%s\".\n", "gia_cec_temp.aig" );
}
}
diff --git a/src/proof/cec/cecCorr.c b/src/proof/cec/cecCorr.c
index f3a84d3a..ed5f9a8e 100644
--- a/src/proof/cec/cecCorr.c
+++ b/src/proof/cec/cecCorr.c
@@ -1124,7 +1124,7 @@ Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
pNew = Gia_ManCorrReduce( pAig );
pNew = Gia_ManSeqCleanup( pTemp = pNew );
Gia_ManStop( pTemp );
- //Gia_WriteAiger( pNew, "reduced.aig", 0, 0 );
+ //Gia_AigerWrite( pNew, "reduced.aig", 0, 0 );
}
// report the results
if ( pPars->fVerbose )
diff --git a/src/proof/cec/cecSeq.c b/src/proof/cec/cecSeq.c
index da60de1d..43bfa99c 100644
--- a/src/proof/cec/cecSeq.c
+++ b/src/proof/cec/cecSeq.c
@@ -401,14 +401,14 @@ int Cec_ManSeqSemiformal( Gia_Man_t * pAig, Cec_ParSmf_t * pPars )
}
// write equivalence classes
- Gia_WriteAiger( pAig, "gore.aig", 0, 0 );
+ Gia_AigerWrite( pAig, "gore.aig", 0, 0 );
// reduce the model
pReduce = Gia_ManSpecReduce( pAig, 0, 0, 1, 0, 0 );
if ( pReduce )
{
pReduce = Gia_ManSeqStructSweep( pAux = pReduce, 1, 1, 0 );
Gia_ManStop( pAux );
- Gia_WriteAiger( pReduce, "gsrm.aig", 0, 0 );
+ Gia_AigerWrite( pReduce, "gsrm.aig", 0, 0 );
// Abc_Print( 1, "Speculatively reduced model was written into file \"%s\".\n", "gsrm.aig" );
// Gia_ManPrintStatsShort( pReduce );
Gia_ManStop( pReduce );
diff --git a/src/proof/cec/cecSolve.c b/src/proof/cec/cecSolve.c
index 41053cf0..d560c37a 100644
--- a/src/proof/cec/cecSolve.c
+++ b/src/proof/cec/cecSolve.c
@@ -710,7 +710,7 @@ clk2 = clock();
if ( status == -1 )
{
Gia_Man_t * pTemp = Gia_ManDupDfsCone( pAig, pObj );
- Gia_WriteAiger( pTemp, "gia_hard.aig", 0, 0 );
+ Gia_AigerWrite( pTemp, "gia_hard.aig", 0, 0 );
Gia_ManStop( pTemp );
Abc_Print( 1, "Dumping hard cone into file \"%s\".\n", "gia_hard.aig" );
}
diff --git a/src/proof/cec/cecSynth.c b/src/proof/cec/cecSynth.c
index 6fc991a8..6ab88cbe 100644
--- a/src/proof/cec/cecSynth.c
+++ b/src/proof/cec/cecSynth.c
@@ -309,7 +309,7 @@ int Cec_SequentialSynthesisPart( Gia_Man_t * p, Cec_ParSeq_t * pPars )
{
pTemp = Gia_ManRegCreatePart( p, vPart, &nCountPis, &nCountRegs, NULL );
sprintf( Buffer, "part%03d.aig", i );
- Gia_WriteAiger( pTemp, Buffer, 0, 0 );
+ Gia_AigerWrite( pTemp, Buffer, 0, 0 );
Abc_Print( 1, "part%03d.aig : Reg = %4d. PI = %4d. (True = %4d. Regs = %4d.) And = %5d.\n",
i, Vec_IntSize(vPart), Gia_ManCiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Gia_ManAndNum(pTemp) );
Gia_ManStop( pTemp );