summaryrefslogtreecommitdiffstats
path: root/src/base
diff options
context:
space:
mode:
Diffstat (limited to 'src/base')
-rw-r--r--src/base/abc/abc.h1
-rw-r--r--src/base/abc/abcNtk.c4
-rw-r--r--src/base/abci/abc.c7
-rw-r--r--src/base/abci/abcDar.c25
-rw-r--r--src/base/abci/abcDprove2.c2
-rw-r--r--src/base/abci/abcLog.c2
-rw-r--r--src/base/abci/abcVerify.c4
-rw-r--r--src/base/cmd/cmdPlugin.c10
8 files changed, 25 insertions, 30 deletions
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index 3357ff46..c1c6a91c 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -38,6 +38,7 @@
#include "extra.h"
#include "stmm.h"
#include "nm.h"
+#include "utilCex.h"
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c
index 821cca4c..d58e9c72 100644
--- a/src/base/abc/abcNtk.c
+++ b/src/base/abc/abcNtk.c
@@ -131,9 +131,7 @@ Abc_Ntk_t * Abc_NtkStartFrom( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkFunc_
if ( pNtk->vOnehots )
pNtkNew->vOnehots = (Vec_Ptr_t *)Vec_VecDupInt( (Vec_Vec_t *)pNtk->vOnehots );
if ( pNtk->pSeqModel )
- {
- pNtkNew->pSeqModel = Gia_ManDupCounterExample( pNtk->pSeqModel, Abc_NtkLatchNum(pNtk) );
- }
+ pNtkNew->pSeqModel = Abc_CexDup( pNtk->pSeqModel, Abc_NtkLatchNum(pNtk) );
// check that the CI/CO/latches are copied correctly
assert( Abc_NtkCiNum(pNtk) == Abc_NtkCiNum(pNtkNew) );
assert( Abc_NtkCoNum(pNtk) == Abc_NtkCoNum(pNtkNew) );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 7ee6769e..4b95b900 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -17580,7 +17580,7 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pSimInfo[0] != 1 )
Abc_Print( 1, "ERROR in Abc_NtkMiterSat(): Generated counter example is invalid.\n" );
ABC_FREE( pSimInfo );
- pAbc->pCex = Gia_ManCreateFromComb( 0, Abc_NtkPiNum(pNtk), 0, pNtk->pModel );
+ pAbc->pCex = Abc_CexCreate( 0, Abc_NtkPiNum(pNtk), pNtk->pModel, 0, 0, 0 );
}
pAbc->Status = RetValue;
if ( RetValue == -1 )
@@ -19840,8 +19840,7 @@ int Abc_CommandTestCex( Abc_Frame_t * pAbc, int argc, char ** argv )
extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 1 );
Gia_Man_t * pGia = Gia_ManFromAigSimple( pAig );
- if ( !Gia_ManVerifyCounterExample( pGia, pAbc->pCex, 0 ) )
-// if ( !Ssw_SmlRunCounterExample( pAig, pAbc->pCex ) )
+ if ( !Gia_ManVerifyCex( pGia, pAbc->pCex, 0 ) )
Abc_Print( 1, "Main AIG: The cex does not fail any outputs.\n" );
else
Abc_Print( 1, "Main AIG: The cex is correct.\n" );
@@ -19860,7 +19859,7 @@ int Abc_CommandTestCex( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( 1, "And AIG: The number of POs (%d) is less than the PO index in cex (%d).\n", Gia_ManPoNum(pAbc->pGia), pAbc->pCex->iPo );
else
{
- if ( !Gia_ManVerifyCounterExample( pAbc->pGia, pAbc->pCex, 0 ) )
+ if ( !Gia_ManVerifyCex( pAbc->pGia, pAbc->pCex, 0 ) )
Abc_Print( 1, "And AIG: The cex does not fail any outputs.\n" );
else
Abc_Print( 1, "And AIG: The cex is correct.\n" );
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index a6fa9ce6..225bf1be 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -21,7 +21,6 @@
#include "abc.h"
#include "main.h"
#include "giaAig.h"
-#include "saig.h"
#include "dar.h"
#include "cnf.h"
#include "fra.h"
@@ -1790,7 +1789,7 @@ ABC_PRT( "Time", clock() - clk );
// verify counter-example
if ( pNtk->pSeqModel )
{
- status = Ssw_SmlRunCounterExample( pMan, pNtk->pSeqModel );
+ status = Saig_ManVerifyCex( pMan, pNtk->pSeqModel );
if ( status == 0 )
printf( "Abc_NtkDarBmc(): Counter-example verification has FAILED.\n" );
}
@@ -1857,7 +1856,7 @@ int Abc_NtkDarBmc3( Abc_Ntk_t * pNtk, Saig_ParBmc_t * pPars )
ABC_PRT( "Time", clock() - clk );
if ( pNtk->pSeqModel )
{
- status = Ssw_SmlRunCounterExample( pMan, pNtk->pSeqModel );
+ status = Saig_ManVerifyCex( pMan, pNtk->pSeqModel );
if ( status == 0 )
printf( "Abc_NtkDarBmc3(): Counter-example verification has FAILED.\n" );
}
@@ -1902,7 +1901,7 @@ int Abc_NtkDarBmcInter_int( Aig_Man_t * pMan, Inter_ManParams_t * pPars, Aig_Man
pTemp->pSeqModel = NULL;
RetValue = Fra_FraigSat( pTemp, pPars->nBTLimit, 0, 0, 0, 0 );
if ( pTemp->pData )
- pTemp->pSeqModel = Gia_ManCreateFromComb( Aig_ManRegNum(pMan), Saig_ManPiNum(pMan), i, (int *)pTemp->pData );
+ pTemp->pSeqModel = Abc_CexCreate( Aig_ManRegNum(pMan), Saig_ManPiNum(pMan), (int *)pTemp->pData, 0, i, 1 );
// pNtk->pModel = pTemp->pData, pTemp->pData = NULL;
}
else
@@ -2150,7 +2149,7 @@ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, Fra_Sec_t * pSecPar )
{
Abc_Cex_t * pCex = pNtk->pSeqModel;
printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness).\n", pCex->iPo, pCex->iFrame );
- if ( !Ssw_SmlRunCounterExample( pMan, pNtk->pSeqModel ) )
+ if ( !Saig_ManVerifyCex( pMan, pNtk->pSeqModel ) )
printf( "Abc_NtkDarProve(): Counter-example verification has FAILED.\n" );
}
}
@@ -2274,7 +2273,7 @@ int Abc_NtkDarPdr( Abc_Ntk_t * pNtk, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex )
Aig_Man_t * pTemp = Saig_ManDupOrpos( pMan );
RetValue = Pdr_ManSolve( pTemp, pPars, ppCex );
if ( RetValue == 0 )
- (*ppCex)->iPo = Ssw_SmlFindOutputCounterExample( pMan, *ppCex );
+ (*ppCex)->iPo = Saig_ManFindFailedPoCex( pMan, *ppCex );
Aig_ManStop( pTemp );
}
else
@@ -2290,7 +2289,7 @@ int Abc_NtkDarPdr( Abc_Ntk_t * pNtk, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex )
assert( 0 );
ABC_PRT( "Time", clock() - clk );
- if ( *ppCex && !Ssw_SmlRunCounterExample( pMan, *ppCex ) )
+ if ( *ppCex && !Saig_ManVerifyCex( pMan, *ppCex ) )
printf( "Abc_NtkDarPdr(): Counter-example verification has FAILED.\n" );
Aig_ManStop( pMan );
return RetValue;
@@ -2710,7 +2709,7 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, in
{
printf( "Simulation iterated %d times with %d words asserted output %d in frame %d. ",
nFrames, nWords, pCex->iPo, pCex->iFrame );
- status = Ssw_SmlRunCounterExample( pMan, pCex );
+ status = Saig_ManVerifyCex( pMan, pCex );
if ( status == 0 )
printf( "Abc_NtkDarSeqSim(): Counter-example verification has FAILED.\n" );
}
@@ -2737,7 +2736,7 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, in
{
printf( "Simulation of %d frames with %d words asserted output %d in frame %d. ",
nFrames, nWords, pCex->iPo, pCex->iFrame );
- status = Ssw_SmlRunCounterExample( pMan, pCex );
+ status = Saig_ManVerifyCex( pMan, pCex );
if ( status == 0 )
printf( "Abc_NtkDarSeqSim(): Counter-example verification has FAILED.\n" );
}
@@ -2767,7 +2766,7 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, in
{
printf( "Simulation of %d frames with %d words asserted output %d in frame %d. ",
nFrames, nWords, pCex->iPo, pCex->iFrame );
- status = Ssw_SmlRunCounterExample( pMan, pCex );
+ status = Saig_ManVerifyCex( pMan, pCex );
if ( status == 0 )
printf( "Abc_NtkDarSeqSim(): Counter-example verification has FAILED.\n" );
}
@@ -2798,7 +2797,7 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, in
{
printf( "Simulation of %d frames with %d words asserted output %d in frame %d. ",
nFrames, nWords, pGia->pCexSeq->iPo, pGia->pCexSeq->iFrame );
- status = Ssw_SmlRunCounterExample( pMan, pGia->pCexSeq );
+ status = Saig_ManVerifyCex( pMan, pGia->pCexSeq );
if ( status == 0 )
printf( "Abc_NtkDarSeqSim(): Counter-example verification has FAILED.\n" );
}
@@ -2825,7 +2824,7 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, in
{
printf( "Simulation of %d frames with %d words asserted output %d in frame %d. ",
nFrames, nWords, pCex->iPo, pCex->iFrame );
- status = Ssw_SmlRunCounterExample( pMan, pCex );
+ status = Saig_ManVerifyCex( pMan, pCex );
if ( status == 0 )
printf( "Abc_NtkDarSeqSim(): Counter-example verification has FAILED.\n" );
}
@@ -2847,7 +2846,7 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, in
{
printf( "Simulation of %d frames with %d words asserted output %d in frame %d. ",
nFrames, nWords, pCex->iPo, pCex->iFrame );
- status = Ssw_SmlRunCounterExample( pMan, pCex );
+ status = Saig_ManVerifyCex( pMan, pCex );
if ( status == 0 )
printf( "Abc_NtkDarSeqSim(): Counter-example verification has FAILED.\n" );
}
diff --git a/src/base/abci/abcDprove2.c b/src/base/abci/abcDprove2.c
index 7d432612..b9b2c10a 100644
--- a/src/base/abci/abcDprove2.c
+++ b/src/base/abci/abcDprove2.c
@@ -384,7 +384,7 @@ finish:
// verify counter-example
if ( pNtk->pSeqModel )
{
- int status = Ssw_SmlRunCounterExample( pMan, pNtk->pSeqModel );
+ int status = Saig_ManVerifyCex( pMan, pNtk->pSeqModel );
if ( status == 0 )
printf( "Abc_NtkDarBmc(): Counter-example verification has FAILED.\n" );
}
diff --git a/src/base/abci/abcLog.c b/src/base/abci/abcLog.c
index 071d7943..7eece0e3 100644
--- a/src/base/abci/abcLog.c
+++ b/src/base/abci/abcLog.c
@@ -197,7 +197,7 @@ int Abc_NtkReadLogFile( char * pFileName, Abc_Cex_t ** ppCex, int * pnFrames )
printf( "Incorrect number of bits.\n" );
return -1;
}
- pCex = Gia_ManAllocCounterExample( nRegs, (Vec_IntSize(vNums)-nRegs)/nFrames, nFrames );
+ pCex = Abc_CexAlloc( nRegs, (Vec_IntSize(vNums)-nRegs)/nFrames, nFrames );
pCex->iPo = iPo;
pCex->iFrame = nFrames - 1;
assert( Vec_IntSize(vNums) == pCex->nBits );
diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c
index 58b8fbb8..acdfcd93 100644
--- a/src/base/abci/abcVerify.c
+++ b/src/base/abci/abcVerify.c
@@ -24,6 +24,7 @@
#include "fraig.h"
#include "sim.h"
#include "aig.h"
+#include "saig.h"
#include "gia.h"
#include "ssw.h"
@@ -1029,7 +1030,6 @@ void Abc_NtkSimulteBuggyMiter( Abc_Ntk_t * pNtk )
int Abc_NtkIsTrueCex( Abc_Ntk_t * pNtk, Abc_Cex_t * pCex )
{
extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
-// extern int Ssw_SmlRunCounterExample( Aig_Man_t * pAig, Abc_Cex_t * p );
Aig_Man_t * pMan;
int status, fStrashed = 0;
if ( !Abc_NtkIsStrash(pNtk) )
@@ -1040,7 +1040,7 @@ int Abc_NtkIsTrueCex( Abc_Ntk_t * pNtk, Abc_Cex_t * pCex )
pMan = Abc_NtkToDar( pNtk, 0, 1 );
if ( pMan )
{
- status = Ssw_SmlRunCounterExample( pMan, pCex );
+ status = Saig_ManVerifyCex( pMan, pCex );
Aig_ManStop( pMan );
}
if ( fStrashed )
diff --git a/src/base/cmd/cmdPlugin.c b/src/base/cmd/cmdPlugin.c
index 116687c7..1e2b7712 100644
--- a/src/base/cmd/cmdPlugin.c
+++ b/src/base/cmd/cmdPlugin.c
@@ -484,20 +484,18 @@ int Cmd_CommandAbcPlugIn( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( 1, "Counter example has a wrong length.\n" );
else
{
- extern int Gia_ManVerifyCounterExampleAllOuts( Gia_Man_t * pAig, Abc_Cex_t * p );
-
Abc_Print( 1, "Problem is satisfiable. Found counter-example in frame %d. ", nFrames-1 );
Abc_PrintTime( 1, "Time", clk );
ABC_FREE( pAbc->pCex );
- pAbc->pCex = Gia_ManDeriveCexFromArray( pAbc->pGia, vCex, 0, nFrames-1 );
+ pAbc->pCex = Abc_CexCreate( Gia_ManRegNum(pAbc->pGia), Gia_ManPiNum(pAbc->pGia), Vec_IntArray(vCex), nFrames-1, 0, 0 );
-// Gia_ManPrintCex( pAbc->pCex );
+// Abc_CexPrint( pAbc->pCex );
-// if ( !Gia_ManVerifyCounterExample( pAbc->pGia, pAbc->pCex, 0 ) )
+// if ( !Gia_ManVerifyCex( pAbc->pGia, pAbc->pCex, 0 ) )
// Abc_Print( 1, "Generated counter-example is INVALID.\n" );
// remporary work-around to detect the output number - October 18, 2010
- pAbc->pCex->iPo = Gia_ManVerifyCounterExampleAllOuts( pAbc->pGia, pAbc->pCex );
+ pAbc->pCex->iPo = Gia_ManFindFailedPoCex( pAbc->pGia, pAbc->pCex );
if ( pAbc->pCex->iPo == -1 )
{
Abc_Print( 1, "Generated counter-example is INVALID.\n" );
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-07 19:54:12 +0000