summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/sat/bmc/bmcBmcAnd.c170
-rw-r--r--src/sat/bmc/bmcUnroll.c1
2 files changed, 138 insertions, 33 deletions
diff --git a/src/sat/bmc/bmcBmcAnd.c b/src/sat/bmc/bmcBmcAnd.c
index 51239d7d..2bd4d90d 100644
--- a/src/sat/bmc/bmcBmcAnd.c
+++ b/src/sat/bmc/bmcBmcAnd.c
@@ -19,6 +19,8 @@
***********************************************************************/
#include "bmc.h"
+#include "sat/bsat/satStore.h"
+#include "sat/cnf/cnf.h"
ABC_NAMESPACE_IMPL_START
@@ -27,6 +29,19 @@ ABC_NAMESPACE_IMPL_START
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
+typedef struct Bmc_Mna_t_ Bmc_Mna_t;
+struct Bmc_Mna_t_
+{
+ Gia_Man_t * pFrames; // time frames
+ Vec_Int_t * vId2Var; // maps GIA IDs into SAT vars
+ Vec_Int_t * vInputs; // inputs of the cone
+ Vec_Int_t * vOutputs; // outputs of the cone
+ Vec_Int_t * vNodes; // internal nodes of the cone
+ sat_solver * pSat; // SAT solver
+ int nSatVars; // the counter of SAT variables
+ abctime clkStart; // starting time
+};
+
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
@@ -42,20 +57,111 @@ ABC_NAMESPACE_IMPL_START
SeeAlso []
***********************************************************************/
-int Gia_ManCountUnmarked_rec( Gia_Obj_t * pObj )
+Bmc_Mna_t * Bmc_MnaAlloc()
+{
+ Bmc_Mna_t * p;
+ p = ABC_CALLOC( Bmc_Mna_t, 1 );
+ p->vId2Var = Vec_IntAlloc( 0 );
+ p->vInputs = Vec_IntAlloc( 1000 );
+ p->vOutputs = Vec_IntAlloc( 1000 );
+ p->vNodes = Vec_IntAlloc( 10000 );
+ p->pSat = sat_solver_new();
+ p->nSatVars = 1;
+ p->clkStart = Abc_Clock();
+ return p;
+}
+void Bmc_MnaFree( Bmc_Mna_t * p )
+{
+ Vec_IntFreeP( &p->vId2Var );
+ Vec_IntFreeP( &p->vInputs );
+ Vec_IntFreeP( &p->vOutputs );
+ Vec_IntFreeP( &p->vNodes );
+ sat_solver_delete( p->pSat );
+ ABC_FREE( p );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns 1 if all outputs are trivial.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Gia_ManBmcCheckOutputs( Gia_Man_t * pFrames, int iStart )
+{
+ int i;
+ for ( i = iStart; i < Gia_ManPoNum(pFrames); i++ )
+ if ( Gia_ObjChild0(Gia_ManPo(pFrames, i)) != Gia_ManConst0(pFrames) )
+ return 0;
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Collects new nodes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Gia_ManBmcAndCone_rec( Bmc_Mna_t * p, Gia_Obj_t * pObj )
{
- if ( !Gia_ObjIsAnd(pObj) || pObj->fMark0 )
- return 0;
+ int iObj;
+ if ( pObj->fMark0 )
+ return;
pObj->fMark0 = 1;
- return 1 + Gia_ManCountUnmarked_rec( Gia_ObjFanin0(pObj) ) +
- Gia_ManCountUnmarked_rec( Gia_ObjFanin1(pObj) );
+ iObj = Gia_ObjId( p->pFrames, pObj );
+ if ( Gia_ObjIsAnd(pObj) && Vec_IntEntry(p->vId2Var, iObj) == 0 )
+ {
+ Gia_ManBmcAndCone_rec( p, Gia_ObjFanin0(pObj) );
+ Gia_ManBmcAndCone_rec( p, Gia_ObjFanin1(pObj) );
+ Vec_IntPush( p->vNodes, iObj );
+ }
+ else
+ Vec_IntPush( p->vInputs, iObj );
}
-int Gia_ManCountUnmarked( Gia_Man_t * p, int iStart )
+void Gia_ManBmcAndCone( Bmc_Mna_t * p, int iStart )
{
- int i, Counter = 0;
- for ( i = iStart; i < Gia_ManPoNum(p); i++ )
- Counter += Gia_ManCountUnmarked_rec( Gia_ObjFanin0(Gia_ManPo(p, i)) );
- return Counter;
+ Gia_Obj_t * pObj;
+ int i;
+ Vec_IntClear( p->vNodes );
+ Vec_IntClear( p->vInputs );
+ Vec_IntClear( p->vOutputs );
+ Vec_IntFillExtra( p->vId2Var, Gia_ManObjNum(p->pFrames), 0 );
+ for ( i = iStart; i < Gia_ManPoNum(p->pFrames); i++ )
+ {
+ pObj = Gia_ManPo(p->pFrames, i);
+ if ( Gia_ObjChild0(pObj) == Gia_ManConst0(p->pFrames) )
+ continue;
+ Gia_ManBmcAndCone_rec( p, Gia_ObjFanin0(pObj) );
+ Vec_IntPush( p->vOutputs, Gia_ObjId(p->pFrames, pObj) );
+ }
+ // clean attributes and create new variables
+ Gia_ManForEachObjVec( p->vInputs, p->pFrames, pObj, i )
+ {
+ int iObj = Vec_IntEntry(p->vInputs, i);
+ pObj->fMark0 = 0;
+ if ( Vec_IntEntry( p->vId2Var, iObj ) == 0 )
+ Vec_IntWriteEntry( p->vId2Var, iObj, p->nSatVars++ );
+ }
+ Gia_ManForEachObjVec( p->vNodes, p->pFrames, pObj, i )
+ {
+ int iObj = Vec_IntEntry(p->vNodes, i);
+ pObj->fMark0 = 0;
+ assert( Vec_IntEntry( p->vId2Var, iObj ) == 0 );
+ Vec_IntWriteEntry( p->vId2Var, iObj, p->nSatVars++ );
+ }
+ // extend the SAT solver
+ if ( p->nSatVars > sat_solver_nvars(p->pSat) )
+ sat_solver_setnvars( p->pSat, p->nSatVars );
+
}
/**Function*************************************************************
@@ -71,46 +177,44 @@ int Gia_ManCountUnmarked( Gia_Man_t * p, int iStart )
***********************************************************************/
int Gia_ManBmcPerform( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
{
- Unr_Man_t * p;
- Gia_Man_t * pFrames;
- abctime clk = Abc_Clock();
+ Unr_Man_t * pUnroll;
+ Bmc_Mna_t * p = Bmc_MnaAlloc();
int nFramesMax = pPars->nFramesMax ? pPars->nFramesMax : ABC_INFINITY;
- int i, f, iStart, status = -1;//, Counter = 0;
- p = Unr_ManUnrollStart( pGia, pPars->fVeryVerbose );
+ int f, iStart, status = -1;
+ pUnroll = Unr_ManUnrollStart( pGia, pPars->fVeryVerbose );
for ( f = 0; f < nFramesMax; f++ )
{
- pFrames = Unr_ManUnrollFrame( p, f );
- assert( Gia_ManPoNum(pFrames) == (f + 1) * Gia_ManPoNum(pGia) );
+ p->pFrames = Unr_ManUnrollFrame( pUnroll, f );
iStart = f * Gia_ManPoNum(pGia);
- for ( i = iStart; i < Gia_ManPoNum(pFrames); i++ )
- if ( Gia_ObjChild0(Gia_ManPo(pFrames, i)) != Gia_ManConst0(pFrames) )
- break;
- if ( i == Gia_ManPoNum(pFrames) )
+ if ( Gia_ManBmcCheckOutputs(p->pFrames, iStart) )
{
if ( pPars->fVerbose )
{
- printf( "Frame %4d : PI =%9d. AIG =%9d. Trivally UNSAT. Mem =%7.1f Mb ",
- f, Gia_ManPiNum(pFrames), Gia_ManAndNum(pFrames), Gia_ManMemory(pFrames) );
- Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+ printf( "%4d : PI =%9d. AIG =%9d. Var =%8d. Trivially UNSAT. Mem =%7.1f Mb ",
+ f, Gia_ManPiNum(p->pFrames), Gia_ManAndNum(p->pFrames),
+ p->nSatVars-1, Gia_ManMemory(p->pFrames) );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - p->clkStart );
}
continue;
}
+ // create another slice
+ Gia_ManBmcAndCone(p, iStart);
if ( pPars->fVerbose )
{
- printf( "Frame %4d : PI =%9d. AIG =%9d. And =%9d. Mem =%7.1f Mb ",
- f, Gia_ManPiNum(pFrames), Gia_ManAndNum(pFrames), Gia_ManCountUnmarked(pFrames, iStart), Gia_ManMemory(pFrames) );
- Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+ printf( "%4d : PI =%9d. AIG =%9d. Var =%8d. In =%6d. And =%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), Gia_ManMemory(p->pFrames) );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - p->clkStart );
}
-// if ( ++Counter == 10 )
-// break;
}
// dump unfolded frames
- pFrames = Gia_ManCleanup( pFrames );
- Gia_AigerWrite( pFrames, "frames.aig", 0, 0 );
+ p->pFrames = Gia_ManCleanup( p->pFrames );
+ Gia_AigerWrite( p->pFrames, "frames.aig", 0, 0 );
printf( "Dumped unfolded frames into file \"frames.aig\".\n" );
- Gia_ManStop( pFrames );
+ Gia_ManStop( p->pFrames );
// cleanup
- Unr_ManFree( p );
+ Unr_ManFree( pUnroll );
+ Bmc_MnaFree( p );
return status;
}
diff --git a/src/sat/bmc/bmcUnroll.c b/src/sat/bmc/bmcUnroll.c
index 9cabcd8b..a1b51471 100644
--- a/src/sat/bmc/bmcUnroll.c
+++ b/src/sat/bmc/bmcUnroll.c
@@ -408,6 +408,7 @@ Gia_Man_t * Unr_ManUnrollFrame( Unr_Man_t * p, int f )
hStart += Unr_ObjSize( pUnrObj );
}
assert( p->pObjs + hStart == p->pEnd );
+ assert( Gia_ManPoNum(p->pFrames) == (f + 1) * Gia_ManPoNum(p->pGia) );
return p->pFrames;
}
Gia_Man_t * Unr_ManUnroll( Gia_Man_t * pGia, int nFrames )
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-05 01:48:30 +0000