summaryrefslogtreecommitdiff
path: root/src/proof
diff options
context:
space:
mode:
Diffstat (limited to 'src/proof')
-rw-r--r--src/proof/abs/absGla.c6
-rw-r--r--src/proof/abs/absGlaOld.c2
-rw-r--r--src/proof/abs/absVta.c2
-rw-r--r--src/proof/acec/acecCore.c2
-rw-r--r--src/proof/acec/acecOrder.c2
-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
-rw-r--r--src/proof/pdr/pdrCore.c1
12 files changed, 16 insertions, 15 deletions
diff --git a/src/proof/abs/absGla.c b/src/proof/abs/absGla.c
index 698d415..bd6b8c7 100644
--- a/src/proof/abs/absGla.c
+++ b/src/proof/abs/absGla.c
@@ -1430,7 +1430,7 @@ void Ga2_GlaDumpAbsracted( Ga2_Man_t * p, int fVerbose )
// dump abstraction map
Vec_IntFreeP( &p->pGia->vGateClasses );
p->pGia->vGateClasses = Ga2_ManAbsTranslate( p );
- Gia_AigerWrite( p->pGia, pFileName, 0, 0 );
+ Gia_AigerWrite( p->pGia, pFileName, 0, 0, 0 );
}
else if ( p->pPars->fDumpVabs )
{
@@ -1443,7 +1443,7 @@ void Ga2_GlaDumpAbsracted( Ga2_Man_t * p, int fVerbose )
vGateClasses = Ga2_ManAbsTranslate( p );
pAbs = Gia_ManDupAbsGates( p->pGia, vGateClasses );
Gia_ManCleanValue( p->pGia );
- Gia_AigerWrite( pAbs, pFileName, 0, 0 );
+ Gia_AigerWrite( pAbs, pFileName, 0, 0, 0 );
Gia_ManStop( pAbs );
Vec_IntFreeP( &vGateClasses );
}
@@ -1563,7 +1563,7 @@ int Gia_ManPerformGla( Gia_Man_t * pAig, Abs_Par_t * pPars )
Vec_IntWriteEntry( pAig->vGateClasses, i, 1 );
Gia_ManForEachRo( pAig, pObj, i )
Vec_IntWriteEntry( pAig->vGateClasses, Gia_ObjId(pAig, pObj), 1 );
- Gia_AigerWrite( pAig, pFileName, 0, 0 );
+ Gia_AigerWrite( pAig, pFileName, 0, 0, 0 );
Vec_IntFree( pAig->vGateClasses );
pAig->vGateClasses = vMap;
if ( p->pPars->fVerbose )
diff --git a/src/proof/abs/absGlaOld.c b/src/proof/abs/absGlaOld.c
index 70bd2e9..45ed139 100644
--- a/src/proof/abs/absGlaOld.c
+++ b/src/proof/abs/absGlaOld.c
@@ -1619,7 +1619,7 @@ void Gia_GlaDumpAbsracted( Gla_Man_t * p, int fVerbose )
pAbs = Gia_ManDupAbsGates( p->pGia0, vGateClasses );
Vec_IntFreeP( &vGateClasses );
// write into file
- Gia_AigerWrite( pAbs, pFileName, 0, 0 );
+ Gia_AigerWrite( pAbs, pFileName, 0, 0, 0 );
Gia_ManStop( pAbs );
}
diff --git a/src/proof/abs/absVta.c b/src/proof/abs/absVta.c
index 01680a3..597e4b7 100644
--- a/src/proof/abs/absVta.c
+++ b/src/proof/abs/absVta.c
@@ -1439,7 +1439,7 @@ void Gia_VtaDumpAbsracted( Vta_Man_t * p, int fVerbose )
pAbs = Gia_ManDupAbsGates( p->pGia, p->pGia->vGateClasses );
Vec_IntFreeP( &p->pGia->vGateClasses );
// send it out
- Gia_AigerWrite( pAbs, pFileName, 0, 0 );
+ Gia_AigerWrite( pAbs, pFileName, 0, 0, 0 );
Gia_ManStop( pAbs );
}
diff --git a/src/proof/acec/acecCore.c b/src/proof/acec/acecCore.c
index 1a575fb..033fbc3 100644
--- a/src/proof/acec/acecCore.c
+++ b/src/proof/acec/acecCore.c
@@ -527,7 +527,7 @@ int Acec_Solve( Gia_Man_t * pGia0, Gia_Man_t * pGia1, Acec_ParCec_t * pPars )
if ( fDumpMiter )
{
Abc_Print( 0, "The verification miter is written into file \"%s\".\n", "acec_miter.aig" );
- Gia_AigerWrite( pMiter, "acec_miter.aig", 0, 0 );
+ Gia_AigerWrite( pMiter, "acec_miter.aig", 0, 0, 0 );
}
status = Cec_ManVerify( pMiter, pCecPars );
ABC_SWAP( Abc_Cex_t *, pGia0->pCexComb, pMiter->pCexComb );
diff --git a/src/proof/acec/acecOrder.c b/src/proof/acec/acecOrder.c
index 93ef7f1..4eb79fe 100644
--- a/src/proof/acec/acecOrder.c
+++ b/src/proof/acec/acecOrder.c
@@ -173,7 +173,7 @@ Vec_Int_t * Gia_PolynFindOrder( Gia_Man_t * pGia, Vec_Int_t * vFadds, Vec_Int_t
{
Gia_Man_t * pNew;
pNew = Gia_ManDupAndCones( pGia, Vec_IntArray(vLeft), Vec_IntSize(vLeft), 0 );
- Gia_AigerWrite( pNew, "leftover.aig", 0, 0 );
+ Gia_AigerWrite( pNew, "leftover.aig", 0, 0, 0 );
printf( "Leftover AIG with %d nodes is dumped into file \"%s\".\n", Gia_ManAndNum(pNew), "leftover.aig" );
Gia_ManStop( pNew );
}
diff --git a/src/proof/cec/cecCec.c b/src/proof/cec/cecCec.c
index be6df65..ee45aa6 100644
--- a/src/proof/cec/cecCec.c
+++ b/src/proof/cec/cecCec.c
@@ -392,7 +392,7 @@ int Cec_ManVerify( Gia_Man_t * pInit, Cec_ParCec_t * pPars )
{
ABC_FREE( pNew->pReprs );
ABC_FREE( pNew->pNexts );
- Gia_AigerWrite( pNew, "gia_cec_undecided.aig", 0, 0 );
+ Gia_AigerWrite( pNew, "gia_cec_undecided.aig", 0, 0, 0 );
Abc_Print( 1, "The result is written into file \"%s\".\n", "gia_cec_undecided.aig" );
}
if ( pPars->TimeLimit && (Abc_Clock() - clkTotal)/CLOCKS_PER_SEC >= pPars->TimeLimit )
diff --git a/src/proof/cec/cecCore.c b/src/proof/cec/cecCore.c
index 250cb69..b952965 100644
--- a/src/proof/cec/cecCore.c
+++ b/src/proof/cec/cecCore.c
@@ -407,7 +407,7 @@ p->timeSim += Abc_Clock() - clk;
}
pSrm = Cec_ManFraSpecReduction( p );
-// Gia_AigerWrite( pSrm, "gia_srm.aig", 0, 0 );
+// Gia_AigerWrite( pSrm, "gia_srm.aig", 0, 0, 0 );
if ( pPars->fVeryVerbose )
Gia_ManPrintStats( pSrm, NULL );
@@ -493,7 +493,7 @@ p->timeSat += Abc_Clock() - clk;
Abc_Print( 1, "Increasing conflict limit to %d.\n", pParsSat->nBTLimit );
if ( fOutputResult )
{
- Gia_AigerWrite( p->pAig, "gia_cec_temp.aig", 0, 0 );
+ Gia_AigerWrite( p->pAig, "gia_cec_temp.aig", 0, 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 3bff4d3..fdc6029 100644
--- a/src/proof/cec/cecCorr.c
+++ b/src/proof/cec/cecCorr.c
@@ -1196,7 +1196,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_AigerWrite( pNew, "reduced.aig", 0, 0 );
+ //Gia_AigerWrite( pNew, "reduced.aig", 0, 0, 0 );
}
// report the results
if ( pPars->fVerbose )
diff --git a/src/proof/cec/cecSeq.c b/src/proof/cec/cecSeq.c
index f39fb2a..81420e0 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_AigerWrite( pAig, "gore.aig", 0, 0 );
+ Gia_AigerWrite( pAig, "gore.aig", 0, 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_AigerWrite( pReduce, "gsrm.aig", 0, 0 );
+ Gia_AigerWrite( pReduce, "gsrm.aig", 0, 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 ee9b8e7..02f14b7 100644
--- a/src/proof/cec/cecSolve.c
+++ b/src/proof/cec/cecSolve.c
@@ -742,7 +742,7 @@ clk2 = Abc_Clock();
if ( status == -1 )
{
Gia_Man_t * pTemp = Gia_ManDupDfsCone( pAig, pObj );
- Gia_AigerWrite( pTemp, "gia_hard.aig", 0, 0 );
+ Gia_AigerWrite( pTemp, "gia_hard.aig", 0, 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 6e5fd22..9465858 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_AigerWrite( pTemp, Buffer, 0, 0 );
+ Gia_AigerWrite( pTemp, Buffer, 0, 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 );
diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c
index 21c713b..4e206b9 100644
--- a/src/proof/pdr/pdrCore.c
+++ b/src/proof/pdr/pdrCore.c
@@ -1427,6 +1427,7 @@ int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars )
char * pFileName = Extra_FileNameGenericAppend(p->pAig->pName, "_inv.pla");
Abc_FrameSetInv( Pdr_ManDeriveInfinityClauses( p, RetValue!=1 ) );
Pdr_ManDumpClauses( p, pFileName, RetValue==1 );
+ printf( "Dumped inductive invariant in file \"%s\".\n", pFileName );
}
else if ( RetValue == 1 )
Abc_FrameSetInv( Pdr_ManDeriveInfinityClauses( p, RetValue!=1 ) );
generated by cgit v1.2.3 (git 2.25.1) at 2024-06-02 19:05:14 +0000