summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/aig/gia/giaJf.c48
-rw-r--r--src/sat/bmc/bmcBmcAnd.c198
2 files changed, 242 insertions, 4 deletions
diff --git a/src/aig/gia/giaJf.c b/src/aig/gia/giaJf.c
index 414d4f63..9ab27c7c 100644
--- a/src/aig/gia/giaJf.c
+++ b/src/aig/gia/giaJf.c
@@ -159,7 +159,7 @@ void Jf_ManGenCnf( word uTruth, int iLitOut, Vec_Int_t * vLeaves, Vec_Int_t * vL
}
}
}
-Cnf_Dat_t * Jf_ManCreateCnf( Gia_Man_t * p, Vec_Int_t * vLits, Vec_Int_t * vClas )
+Cnf_Dat_t * Jf_ManCreateCnfRemap( Gia_Man_t * p, Vec_Int_t * vLits, Vec_Int_t * vClas )
{
Cnf_Dat_t * pCnf;
Gia_Obj_t * pObj;
@@ -189,6 +189,42 @@ Cnf_Dat_t * Jf_ManCreateCnf( Gia_Man_t * p, Vec_Int_t * vLits, Vec_Int_t * vClas
pCnf->pVarNums = pMap;
return pCnf;
}
+Cnf_Dat_t * Jf_ManCreateCnf( Gia_Man_t * p, Vec_Int_t * vLits, Vec_Int_t * vClas )
+{
+ Cnf_Dat_t * pCnf;
+ int i, Entry, iOut;
+ // generate CNF
+ pCnf = ABC_CALLOC( Cnf_Dat_t, 1 );
+ pCnf->pMan = (Aig_Man_t *)p;
+ pCnf->nVars = Gia_ManObjNum(p);
+ pCnf->nLiterals = Vec_IntSize(vLits);
+ pCnf->nClauses = Vec_IntSize(vClas);
+ pCnf->pClauses = ABC_ALLOC( int *, pCnf->nClauses+1 );
+ pCnf->pClauses[0] = Vec_IntReleaseArray(vLits);
+ Vec_IntForEachEntry( vClas, Entry, i )
+ pCnf->pClauses[i] = pCnf->pClauses[0] + Entry;
+ pCnf->pClauses[i] = pCnf->pClauses[0] + pCnf->nLiterals;
+ // create mapping of objects into their clauses
+ pCnf->pObj2Clause = ABC_FALLOC( int, Gia_ManObjNum(p) );
+ pCnf->pObj2Count = ABC_FALLOC( int, Gia_ManObjNum(p) );
+ for ( i = 0; i < pCnf->nClauses; i++ )
+ {
+ iOut = Abc_Lit2Var(pCnf->pClauses[i][0]);
+ if ( pCnf->pObj2Clause[iOut] == -1 )
+ {
+// printf( "\n" );
+ pCnf->pObj2Clause[iOut] = i;
+ pCnf->pObj2Count[iOut] = 1;
+ }
+ else
+ {
+ assert( pCnf->pObj2Count[iOut] > 0 );
+ pCnf->pObj2Count[iOut]++;
+ }
+//printf( "%d ", iOut );
+ }
+ return pCnf;
+}
/**Function*************************************************************
@@ -1713,7 +1749,7 @@ Gia_Man_t * Jf_ManPerformMapping( Gia_Man_t * pGia, Jf_Par_t * pPars )
Jf_ManFree( p );
return pNew;
}
-void Jf_ManTestCnf( Gia_Man_t * p )
+Cnf_Dat_t * Jf_ManDeriveCnf( Gia_Man_t * p )
{
Cnf_Dat_t * pCnf;
Gia_Man_t * pNew;
@@ -1722,8 +1758,14 @@ void Jf_ManTestCnf( Gia_Man_t * p )
pPars->fGenCnf = 1;
pNew = Jf_ManPerformMapping( p, pPars );
pCnf = (Cnf_Dat_t *)pNew->pData; pNew->pData = NULL;
- Gia_ManStop( pNew );
+// Gia_ManStop( pNew );
+ return pCnf;
+}
+void Jf_ManTestCnf( Gia_Man_t * p )
+{
+ Cnf_Dat_t * pCnf = Jf_ManDeriveCnf( p );
Cnf_DataWriteIntoFile( pCnf, "test.cnf", 0, NULL, NULL );
+ Gia_ManStop( (Gia_Man_t *)pCnf->pMan );
Cnf_DataFree(pCnf);
}
diff --git a/src/sat/bmc/bmcBmcAnd.c b/src/sat/bmc/bmcBmcAnd.c
index 1172227c..8a7a1932 100644
--- a/src/sat/bmc/bmcBmcAnd.c
+++ b/src/sat/bmc/bmcBmcAnd.c
@@ -34,6 +34,7 @@ typedef struct Bmc_Mna_t_ Bmc_Mna_t;
struct Bmc_Mna_t_
{
Gia_Man_t * pFrames; // time frames
+ Cnf_Dat_t * pCnf; // CNF derived for the timeframes
Vec_Int_t * vPiMap; // maps unrolled GIA PIs into user GIA PIs
Vec_Int_t * vId2Var; // maps GIA IDs into SAT vars
Vec_Int_t * vInputs; // inputs of the cone
@@ -396,10 +397,12 @@ Bmc_Mna_t * Bmc_MnaAlloc()
p->pSat = sat_solver_new();
p->nSatVars = 1;
p->clkStart = Abc_Clock();
+ sat_solver_setnvars( p->pSat, 1000 );
return p;
}
void Bmc_MnaFree( Bmc_Mna_t * p )
{
+ Cnf_DataFree( p->pCnf );
Vec_IntFreeP( &p->vPiMap );
Vec_IntFreeP( &p->vId2Var );
Vec_IntFreeP( &p->vInputs );
@@ -767,7 +770,7 @@ Abc_Cex_t * Gia_ManBmcCexGen( Bmc_Mna_t * pMan, Gia_Man_t * p, int iOut )
SeeAlso []
***********************************************************************/
-int Gia_ManBmcPerform( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
+int Gia_ManBmcPerform_old_cnf( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
{
Bmc_Mna_t * p;
int nFramesMax, f, i=0, Lit, status, RetValue = -2;
@@ -851,6 +854,199 @@ int Gia_ManBmcPerform( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
return RetValue;
}
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Cnf_Dat_t * Cnf_DeriveGia( Gia_Man_t * p )
+{
+ Aig_Man_t * pAig = Gia_ManToAigSimple( p );
+ Cnf_Dat_t * pCnf = Cnf_DeriveOther( pAig, 1 );
+ Aig_ManStop( pAig );
+ return pCnf;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Gia_ManBmcAddCnfNew_rec( Bmc_Mna_t * p, Gia_Obj_t * pObj )
+{
+ int iObj = Gia_ObjId( p->pFrames, pObj );
+ if ( Gia_ObjIsAnd(pObj) && p->pCnf->pObj2Count[iObj] == -1 )
+ {
+ Gia_ManBmcAddCnfNew_rec( p, Gia_ObjFanin0(pObj) );
+ Gia_ManBmcAddCnfNew_rec( p, Gia_ObjFanin1(pObj) );
+ return;
+ }
+ if ( Vec_IntEntry(p->vId2Var, iObj) > 0 )
+ return;
+ Vec_IntWriteEntry(p->vId2Var, iObj, p->nSatVars++);
+ if ( Gia_ObjIsAnd(pObj) || Gia_ObjIsPo(p->pFrames, pObj) )
+ {
+ int i, nClas, iCla;
+ Gia_ManBmcAddCnfNew_rec( p, Gia_ObjFanin0(pObj) );
+ if ( Gia_ObjIsAnd(pObj) )
+ Gia_ManBmcAddCnfNew_rec( p, Gia_ObjFanin1(pObj) );
+ // extend the SAT solver
+ if ( p->nSatVars > sat_solver_nvars(p->pSat) )
+ sat_solver_setnvars( p->pSat, p->nSatVars );
+ // add clauses
+ nClas = p->pCnf->pObj2Count[iObj];
+ iCla = p->pCnf->pObj2Clause[iObj];
+ for ( i = 0; i < nClas; i++ )
+ {
+ int nLits, pLits[8];
+ int * pClauseThis = p->pCnf->pClauses[iCla+i];
+ int * pClauseNext = p->pCnf->pClauses[iCla+i+1];
+ for ( nLits = 0; pClauseThis + nLits < pClauseNext; nLits++ )
+ {
+ assert( pClauseThis[nLits] > 1 && pClauseThis[nLits] < 2*Gia_ManObjNum(p->pFrames) );
+ pLits[nLits] = Abc_Lit2LitV( Vec_IntArray(p->vId2Var), pClauseThis[nLits] );
+ }
+ assert( nLits < 8 );
+ if ( !sat_solver_addclause( p->pSat, pLits, pLits + nLits ) )
+ break;
+ }
+ if ( i < nClas )
+ printf( "SAT solver became UNSAT after adding clauses.\n" );
+ }
+ else assert( Gia_ObjIsCi(pObj) );
+}
+void Gia_ManBmcAddCnfNew( Bmc_Mna_t * p, int iStart, int iStop )
+{
+ Gia_Obj_t * pObj;
+ int i;
+ for ( i = iStart; i < iStop; i++ )
+ {
+ pObj = Gia_ManPo(p->pFrames, i);
+ if ( Gia_ObjFanin0(pObj) == Gia_ManConst0(p->pFrames) )
+ continue;
+ Gia_ManBmcAddCnfNew_rec( p, pObj );
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Gia_ManBmcPerform( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
+{
+ extern Cnf_Dat_t * Jf_ManDeriveCnf( Gia_Man_t * p );
+ Bmc_Mna_t * p;
+ int nFramesMax, f, i=0, Lit, status, RetValue = -2;
+ abctime clk = Abc_Clock();
+ p = Bmc_MnaAlloc();
+ p->pFrames = Gia_ManBmcUnroll( pGia, pPars->nFramesMax, pPars->nFramesAdd, pPars->fVeryVerbose, &p->vPiMap );
+ nFramesMax = Gia_ManPoNum(p->pFrames) / Gia_ManPoNum(pGia);
+ if ( pPars->fVerbose )
+ {
+ printf( "Unfolding for %d frames with first non-trivial PO %d. ", nFramesMax, Gia_ManBmcFindFirst(p->pFrames) );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+ }
+ if ( pPars->fUseSynth )
+ {
+ Gia_Man_t * pTemp = p->pFrames;
+ p->pFrames = Gia_ManAigSyn2( pTemp, pPars->fVerbose, 0 );
+ Gia_ManStop( pTemp );
+ }
+ else if ( pPars->fVerbose )
+ Gia_ManPrintStats( p->pFrames, NULL );
+ if ( pPars->fDumpFrames )
+ {
+ Gia_AigerWrite( p->pFrames, "frames.aig", 0, 0 );
+ printf( "Dumped unfolded frames into file \"frames.aig\".\n" );
+ }
+// p->pCnf = Jf_ManDeriveCnf( p->pFrames );
+// Gia_ManStop( p->pFrames );
+// p->pFrames = (Gia_Man_t *)p->pCnf->pMan; p->pCnf->pMan = NULL;
+ p->pCnf = Cnf_DeriveGia( p->pFrames );
+ Vec_IntFillExtra( p->vId2Var, Gia_ManObjNum(p->pFrames), 0 );
+ for ( f = 0; f < nFramesMax; f++ )
+ {
+ if ( !Gia_ManBmcCheckOutputs( p->pFrames, f * Gia_ManPoNum(pGia), (f+1) * Gia_ManPoNum(pGia) ) )
+ {
+ // create another slice
+// Gia_ManBmcAddCone( p, f * Gia_ManPoNum(pGia), (f+1) * Gia_ManPoNum(pGia) );
+ // create CNF in the SAT solver
+// Gia_ManBmcAddCnf( p, p->pFrames, p->vInputs, p->vNodes, p->vOutputs );
+ Gia_ManBmcAddCnfNew( p, f * Gia_ManPoNum(pGia), (f+1) * Gia_ManPoNum(pGia) );
+ // try solving the outputs
+ for ( i = f * Gia_ManPoNum(pGia); i < (f+1) * Gia_ManPoNum(pGia); i++ )
+ {
+ Gia_Obj_t * pObj = Gia_ManPo(p->pFrames, i);
+ if ( Gia_ObjChild0(pObj) == Gia_ManConst0(p->pFrames) )
+ continue;
+ if ( Gia_ObjChild0(pObj) == Gia_ManConst1(p->pFrames) )
+ {
+ printf( "Output %d is trivially SAT.\n", i );
+ continue;
+ }
+ Lit = Abc_Var2Lit( Vec_IntEntry(p->vId2Var, Gia_ObjId(p->pFrames, pObj)), 0 );
+ status = sat_solver_solve( p->pSat, &Lit, &Lit + 1, (ABC_INT64_T)pPars->nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
+ if ( status == l_False ) // unsat
+ continue;
+ if ( status == l_True ) // sat
+ RetValue = 0;
+ if ( status == l_Undef ) // undecided
+ RetValue = -1;
+ break;
+ }
+ // report statistics
+ if ( pPars->fVerbose )
+ {
+ printf( "%4d : PI =%9d. AIG =%9d. Var =%8d. In =%6d. And =%9d. Cla =%9d. Conf =%9d. Mem =%7.1f MB ",
+ f, Gia_ManPiNum(p->pFrames), Gia_ManAndNum(p->pFrames),
+ p->nSatVars-1, Vec_IntSize(p->vInputs), Vec_IntSize(p->vNodes),
+ sat_solver_nclauses(p->pSat), sat_solver_nconflicts(p->pSat), Gia_ManMemory(p->pFrames)/(1<<20) );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - p->clkStart );
+ }
+ }
+ if ( RetValue != -2 )
+ {
+ if ( RetValue == -1 )
+ printf( "SAT solver reached conflict/runtime limit in frame %d.\n", f );
+ else
+ {
+ ABC_FREE( pGia->pCexSeq );
+ pGia->pCexSeq = Gia_ManBmcCexGen( p, pGia, i );
+ printf( "Output %d of miter \"%s\" was asserted in frame %d. ",
+ i - f * Gia_ManPoNum(pGia), Gia_ManName(pGia), f );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - p->clkStart );
+ }
+ break;
+ }
+ pPars->iFrame = f;
+ }
+ if ( RetValue == -2 )
+ RetValue = -1;
+ // cleanup
+ Gia_ManStop( p->pFrames );
+ Bmc_MnaFree( p );
+ return RetValue;
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-30 19:24:29 +0000