summaryrefslogtreecommitdiffstats
path: root/src/aig/gia/giaSweeper.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/gia/giaSweeper.c')
-rw-r--r--src/aig/gia/giaSweeper.c56
1 files changed, 54 insertions, 2 deletions
diff --git a/src/aig/gia/giaSweeper.c b/src/aig/gia/giaSweeper.c
index 7835432f..07435d81 100644
--- a/src/aig/gia/giaSweeper.c
+++ b/src/aig/gia/giaSweeper.c
@@ -230,8 +230,6 @@ void Gia_SweeperSetRuntimeLimit( Gia_Man_t * p, int nSeconds )
{
Swp_Man_t * pSwp = (Swp_Man_t *)p->pData;
pSwp->nTimeOut = nSeconds;
- if ( nSeconds )
- sat_solver_set_runtime_limit( pSwp->pSat, nSeconds * CLOCKS_PER_SEC + clock() );
}
Vec_Int_t * Gia_SweeperGetCex( Gia_Man_t * p )
{
@@ -696,6 +694,10 @@ int Gia_SweeperCheckEquiv( Gia_Man_t * pGia, int Probe1, int Probe2 )
Vec_IntPush( p->vCondAssump, pLitsSat[0] );
Vec_IntPush( p->vCondAssump, Abc_LitNot(pLitsSat[1]) );
+ // set runtime limit for this call
+ if ( p->nTimeOut )
+ sat_solver_set_runtime_limit( p->pSat, p->nTimeOut * CLOCKS_PER_SEC + clock() );
+
clk = clock();
RetValue1 = sat_solver_solve( p->pSat, Vec_IntArray(p->vCondAssump), Vec_IntArray(p->vCondAssump) + Vec_IntSize(p->vCondAssump),
(ABC_INT64_T)p->nConfMax, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
@@ -798,6 +800,10 @@ int Gia_SweeperCondCheckUnsat( Gia_Man_t * pGia )
}
sat_solver_compress( p->pSat );
+ // set runtime limit for this call
+ if ( p->nTimeOut )
+ sat_solver_set_runtime_limit( p->pSat, p->nTimeOut * CLOCKS_PER_SEC + clock() );
+
clk = clock();
RetValue = sat_solver_solve( p->pSat, Vec_IntArray(p->vCondAssump), Vec_IntArray(p->vCondAssump) + Vec_IntSize(p->vCondAssump),
(ABC_INT64_T)p->nConfMax, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
@@ -825,6 +831,52 @@ p->timeSatUndec += clock() - clk;
}
}
+/**Function*************************************************************
+
+ Synopsis [Performs grafting from another manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Gia_SweeperGraft( Gia_Man_t * pDst, Vec_Int_t * vProbes, Gia_Man_t * pSrc )
+{
+ Vec_Int_t * vOutLits;
+ Gia_Obj_t * pObj;
+ int i;
+ assert( Vec_IntSize(vProbes) == Gia_ManPiNum(pSrc) );
+ assert( pDst->pHTable != NULL );
+ Gia_ManForEachPi( pSrc, pObj, i )
+ pObj->Value = Gia_SweeperProbeLit( pDst, Vec_IntEntry(vProbes, i) );
+ Gia_ManForEachAnd( pSrc, pObj, i )
+ pObj->Value = Gia_ManHashAnd( pDst, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+ vOutLits = Vec_IntAlloc( Gia_ManPoNum(pSrc) );
+ Gia_ManForEachPo( pSrc, pObj, i )
+ Vec_IntPush( vOutLits, Gia_ObjFanin0Copy(pObj) );
+ return vOutLits;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs conditional sweeping of the cone.]
+
+ Description [Returns the result as a new GIA manager with as many inputs
+ as the original manager and as many outputs as there are logic cones.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Gia_Man_t * Gia_SweeperSweep( Gia_Man_t * p, Vec_Int_t * vProbeConds, Vec_Int_t * vProbeOuts )
+{
+ return NULL;
+}
+
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////