summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/aig/gia/giaAiger.c10
-rw-r--r--src/base/abc/abcHieCec.c2
-rw-r--r--src/base/abc/abcHieNew.c2
-rw-r--r--src/map/if/ifTune.c19
-rw-r--r--src/sat/bmc/bmc.h1
-rw-r--r--src/sat/bmc/bmcCexCare.c54
6 files changed, 76 insertions, 12 deletions
diff --git a/src/aig/gia/giaAiger.c b/src/aig/gia/giaAiger.c
index bc40e4ca..6457927b 100644
--- a/src/aig/gia/giaAiger.c
+++ b/src/aig/gia/giaAiger.c
@@ -680,8 +680,10 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipS
pNew->pCellStr = Abc_UtilStrsav( (char*)pCur ); pCur += strlen((char*)pCur) + 1;
nSize = nSize - strlen(pNew->pCellStr) - 1;
assert( nSize % 4 == 0 );
- pNew->vConfigs = Vec_IntStart(nSize / 4);
- memcpy(Vec_IntArray(pNew->vConfigs), pCur, nSize); pCur += nSize;
+ pNew->vConfigs = Vec_IntAlloc(nSize / 4);
+// memcpy(Vec_IntArray(pNew->vConfigs), pCur, nSize); pCur += nSize;
+ for ( i = 0; i < nSize / 4; i++ )
+ Vec_IntPush( pNew->vConfigs, Gia_AigerReadInt(pCur) ), pCur += 4;
assert( pCur == pCurTemp );
if ( fVerbose ) printf( "Finished reading extension \"b\".\n" );
}
@@ -1289,7 +1291,9 @@ void Gia_AigerWrite( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int
assert( p->pCellStr != NULL );
Gia_FileWriteBufferSize( pFile, 4*Vec_IntSize(p->vConfigs) + strlen(p->pCellStr) + 1 );
fwrite( p->pCellStr, 1, strlen(p->pCellStr) + 1, pFile );
- fwrite( Vec_IntArray(p->vConfigs), 1, 4*Vec_IntSize(p->vConfigs), pFile );
+// fwrite( Vec_IntArray(p->vConfigs), 1, 4*Vec_IntSize(p->vConfigs), pFile );
+ for ( i = 0; i < Vec_IntSize(p->vConfigs); i++ )
+ Gia_FileWriteBufferSize( pFile, Vec_IntEntry(p->vConfigs, i) );
}
// write choices
if ( Gia_ManHasChoices(p) )
diff --git a/src/base/abc/abcHieCec.c b/src/base/abc/abcHieCec.c
index 83683398..d9f413e8 100644
--- a/src/base/abc/abcHieCec.c
+++ b/src/base/abc/abcHieCec.c
@@ -642,7 +642,7 @@ int Abc_NtkCheckRecursive( Abc_Ntk_t * pNtk )
Abc_NtkForEachObj( pModel, pObj, k )
if ( Abc_ObjIsBox(pObj) && pObj->pData == (void *)pModel )
{
- printf( "WARNING: Model \"%s\" contains a recursive defition.\n", Abc_NtkName(pModel) );
+ printf( "WARNING: Model \"%s\" contains a recursive definition.\n", Abc_NtkName(pModel) );
RetValue = 1;
break;
}
diff --git a/src/base/abc/abcHieNew.c b/src/base/abc/abcHieNew.c
index db619260..d50c274e 100644
--- a/src/base/abc/abcHieNew.c
+++ b/src/base/abc/abcHieNew.c
@@ -676,7 +676,7 @@ int Au_NtkCheckRecursive( Au_Ntk_t * pNtk )
Au_NtkForEachObj( pModel, pObj, k )
if ( Au_ObjIsBox(pObj) && Au_ObjModel(pObj) == pModel )
{
- printf( "WARNING: Model \"%s\" contains a recursive defition.\n", Au_NtkName(pModel) );
+ printf( "WARNING: Model \"%s\" contains a recursive definition.\n", Au_NtkName(pModel) );
RetValue = 1;
break;
}
diff --git a/src/map/if/ifTune.c b/src/map/if/ifTune.c
index c55e97d2..7fe7a4bb 100644
--- a/src/map/if/ifTune.c
+++ b/src/map/if/ifTune.c
@@ -400,15 +400,15 @@ int Ifn_NtkParseInt2( char * pStr, Ifn_Ntk_t * p )
else if ( pStr[k+2] == '{' )
p->Nodes[i].Type = IFN_DSD_PRIME, Next = '}';
else
- return Ifn_ErrorMessage( "Cannot find openning operation symbol in the defition of of signal \'%c\'.\n", 'a' + i );
+ return Ifn_ErrorMessage( "Cannot find openning operation symbol in the definition of signal \'%c\'.\n", 'a' + i );
for ( n = k + 3; pStr[n]; n++ )
if ( pStr[n] == Next )
break;
if ( pStr[n] == 0 )
- return Ifn_ErrorMessage( "Cannot find closing operation symbol in the defition of of signal \'%c\'.\n", 'a' + i );
+ return Ifn_ErrorMessage( "Cannot find closing operation symbol in the definition of signal \'%c\'.\n", 'a' + i );
nFans = n - k - 3;
- if ( nFans < 1 || nFans > 8 )
- return Ifn_ErrorMessage( "Cannot find matching operation symbol in the defition of of signal \'%c\'.\n", 'a' + i );
+ if ( nFans > 8 )
+ return Ifn_ErrorMessage( "Cannot find matching operation symbol in the definition of signal \'%c\'.\n", 'a' + i );
for ( f = 0; f < nFans; f++ )
{
iFan = pStr[k + 3 + f] - 'a';
@@ -524,7 +524,7 @@ Gia_Man_t * Ifn_ManStrFindModel( Ifn_Ntk_t * p )
{
int n, Step, pVarsData[256];
int nMints = (1 << nFans);
- assert( nFans >= 1 && nFans <= 8 );
+ assert( nFans >= 0 && nFans <= 8 );
for ( k = 0; k < nMints; k++ )
pVarsData[k] = pVarMap[iFanin + k];
for ( Step = 1, k = 0; k < nFans; k++, Step <<= 1 )
@@ -1111,9 +1111,10 @@ int Ifn_NtkAddClauses( Ifn_Ntk_t * p, int * pValues, sat_solver * pSat )
int i, f, v, nLits, pLits[IFN_INS+2], pLits2[IFN_INS+2];
// assign new variables
int nSatVars = sat_solver_nvars(pSat);
- for ( i = 0; i < p->nObjs-1; i++ )
+// for ( i = 0; i < p->nObjs-1; i++ )
+ for ( i = 0; i < p->nObjs; i++ )
p->Nodes[i].Var = nSatVars++;
- p->Nodes[p->nObjs-1].Var = 0xFFFF;
+ //p->Nodes[p->nObjs-1].Var = 0xFFFF;
sat_solver_setnvars( pSat, nSatVars );
// verify variable values
for ( i = 0; i < p->nVars; i++ )
@@ -1237,6 +1238,10 @@ int Ifn_NtkAddClauses( Ifn_Ntk_t * p, int * pValues, sat_solver * pSat )
else assert( 0 );
//printf( "\n" );
}
+ // add last clause (not needed if the root node is IFN_DSD_PRIME)
+ pLits[0] = Abc_Var2Lit( p->Nodes[p->nObjs-1].Var, pValues[p->nObjs-1]==0 );
+ if ( !Ifn_AddClause( pSat, pLits, pLits + 1 ) )
+ return 0;
return 1;
}
diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h
index b0a9210d..19a4679d 100644
--- a/src/sat/bmc/bmc.h
+++ b/src/sat/bmc/bmc.h
@@ -161,6 +161,7 @@ extern int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t *
/*=== bmcBmcAnd.c ==========================================================*/
extern int Gia_ManBmcPerform( Gia_Man_t * p, Bmc_AndPar_t * pPars );
/*=== bmcCexCare.c ==========================================================*/
+extern Abc_Cex_t * Bmc_CexCareExtendToObjects( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexCare );
extern Abc_Cex_t * Bmc_CexCareMinimize( Aig_Man_t * p, Abc_Cex_t * pCex, int fCheck, int fVerbose );
extern void Bmc_CexCareVerify( Aig_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexMin, int fVerbose );
/*=== bmcCexCut.c ==========================================================*/
diff --git a/src/sat/bmc/bmcCexCare.c b/src/sat/bmc/bmcCexCare.c
index addb89fd..21fea429 100644
--- a/src/sat/bmc/bmcCexCare.c
+++ b/src/sat/bmc/bmcCexCare.c
@@ -34,6 +34,60 @@ ABC_NAMESPACE_IMPL_START
/**Function*************************************************************
+ Synopsis [Takes CEX and its care-set. Returns care-set of all objects.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Abc_Cex_t * Bmc_CexCareExtendToObjects( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexCare )
+{
+ Abc_Cex_t * pNew;
+ Gia_Obj_t * pObj;
+ int i, k;
+ assert( pCex->nPis == pCexCare->nPis );
+ assert( pCex->nRegs == pCexCare->nRegs );
+ assert( pCex->nBits == pCexCare->nBits );
+ // start the counter-example
+ pNew = Abc_CexAlloc( pCex->nRegs, Gia_ManObjNum(p), pCex->iFrame + 1 );
+ pNew->iFrame = pCex->iFrame;
+ pNew->iPo = pCex->iPo;
+ // initialize terminary simulation
+ Gia_ObjTerSimSet0( Gia_ManConst0(p) );
+ Gia_ManForEachRi( p, pObj, k )
+ Gia_ObjTerSimSet0( pObj );
+ for ( i = 0; i <= pCex->iFrame; i++ )
+ {
+ Gia_ManForEachPi( p, pObj, k )
+ {
+ if ( !Abc_InfoHasBit( pCexCare->pData, pCexCare->nRegs + i * pCexCare->nPis + k ) )
+ Gia_ObjTerSimSetX( pObj );
+ else if ( Abc_InfoHasBit( pCex->pData, pCex->nRegs + i * pCex->nPis + k ) )
+ Gia_ObjTerSimSet1( pObj );
+ else
+ Gia_ObjTerSimSet0( pObj );
+ }
+ Gia_ManForEachRo( p, pObj, k )
+ Gia_ObjTerSimRo( p, pObj );
+ Gia_ManForEachAnd( p, pObj, k )
+ Gia_ObjTerSimAnd( pObj );
+ Gia_ManForEachCo( p, pObj, k )
+ Gia_ObjTerSimCo( pObj );
+ // add cares to the exdended counter-example
+ Gia_ManForEachObj( p, pObj, k )
+ if ( !Gia_ObjTerSimGetX(pObj) )
+ Abc_InfoSetBit( pNew->pData, pNew->nRegs + pNew->nPis * i + k );
+ }
+ pObj = Gia_ManPo( p, pCex->iPo );
+ assert( Gia_ObjTerSimGet1(pObj) );
+ return pNew;
+}
+
+/**Function*************************************************************
+
Synopsis [Backward propagation.]
Description []
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-22 03:51:04 +0000