From e50fc467fd54420cf262bf5266959f6c02a65bf7 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 6 Nov 2015 13:49:23 -0800 Subject: Improvements to 'satclp' (unfinished). --- src/base/abci/abcCollapse.c | 46 ++++++++++++++++++++++++++++++--------------- 1 file changed, 31 insertions(+), 15 deletions(-) (limited to 'src/base') diff --git a/src/base/abci/abcCollapse.c b/src/base/abci/abcCollapse.c index f9b02fda..653618c5 100644 --- a/src/base/abci/abcCollapse.c +++ b/src/base/abci/abcCollapse.c @@ -643,12 +643,15 @@ int Abc_NtkCollapseCountVars( Vec_Str_t * vSop, Vec_Int_t * vSupp ) SeeAlso [] ***********************************************************************/ -sat_solver * Abc_NtkClpDeriveSatSolver( Cnf_Dat_t * pCnf, int iCoObjId, Vec_Int_t * vSupp, Vec_Int_t * vAnds, Vec_Int_t * vMap, sat_solver ** ppSat ) +sat_solver * Abc_NtkClpDeriveSatSolver( Cnf_Dat_t * pCnf, int iCoObjId, Vec_Int_t * vSupp, Vec_Int_t * vAnds, Vec_Int_t * vMap, sat_solver ** ppSat1, sat_solver ** ppSat2, sat_solver ** ppSat3 ) { int i, k, iObj, status, nVars = 2; +// int i, k, iObj, status, nVars = 1; Vec_Int_t * vLits = Vec_IntAlloc( 16 ); sat_solver * pSat = sat_solver_new(); - if ( ppSat ) *ppSat = sat_solver_new(); + if ( ppSat1 ) *ppSat1 = sat_solver_new(); + if ( ppSat2 ) *ppSat2 = sat_solver_new(); + if ( ppSat3 ) *ppSat3 = sat_solver_new(); // assign SAT variable numbers Vec_IntWriteEntry( vMap, iCoObjId, nVars++ ); Vec_IntForEachEntry( vSupp, iObj, k ) @@ -656,9 +659,13 @@ sat_solver * Abc_NtkClpDeriveSatSolver( Cnf_Dat_t * pCnf, int iCoObjId, Vec_Int_ Vec_IntForEachEntry( vAnds, iObj, k ) if ( pCnf->pObj2Clause[iObj] != -1 ) Vec_IntWriteEntry( vMap, iObj, nVars++ ); +// Vec_IntForEachEntry( vSupp, iObj, k ) +// Vec_IntWriteEntry( vMap, iObj, nVars++ ); // create clauses for the internal nodes and for the output sat_solver_setnvars( pSat, nVars ); - if ( ppSat ) sat_solver_setnvars( *ppSat, nVars ); + if ( ppSat1 ) sat_solver_setnvars( *ppSat1, nVars ); + if ( ppSat2 ) sat_solver_setnvars( *ppSat2, nVars ); + if ( ppSat3 ) sat_solver_setnvars( *ppSat3, nVars ); Vec_IntPush( vAnds, iCoObjId ); Vec_IntForEachEntry( vAnds, iObj, k ) { @@ -676,7 +683,9 @@ sat_solver * Abc_NtkClpDeriveSatSolver( Cnf_Dat_t * pCnf, int iCoObjId, Vec_Int_ status = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits)+Vec_IntSize(vLits) ); assert( status ); (void) status; - if ( ppSat ) sat_solver_addclause( *ppSat, Vec_IntArray(vLits), Vec_IntArray(vLits)+Vec_IntSize(vLits) ); + if ( ppSat1 ) sat_solver_addclause( *ppSat1, Vec_IntArray(vLits), Vec_IntArray(vLits)+Vec_IntSize(vLits) ); + if ( ppSat2 ) sat_solver_addclause( *ppSat2, Vec_IntArray(vLits), Vec_IntArray(vLits)+Vec_IntSize(vLits) ); + if ( ppSat3 ) sat_solver_addclause( *ppSat3, Vec_IntArray(vLits), Vec_IntArray(vLits)+Vec_IntSize(vLits) ); } } Vec_IntPop( vAnds ); @@ -696,15 +705,15 @@ sat_solver * Abc_NtkClpDeriveSatSolver( Cnf_Dat_t * pCnf, int iCoObjId, Vec_Int_ SeeAlso [] ***********************************************************************/ -Vec_Str_t * Abc_NtkClpGiaOne( Gia_Man_t * p, int iCo, int nCubeLim, int nBTLimit, int fVerbose, int fCanon, int fReverse, Vec_Int_t * vSupp ) +Vec_Str_t * Abc_NtkClpGiaOne( Gia_Man_t * p, int iCo, int nCubeLim, int nBTLimit, int fCanon, int fReverse, Vec_Int_t * vSupp, int fVerbose ) { Vec_Str_t * vSop; abctime clk = Abc_Clock(); - extern Vec_Str_t * Bmc_CollapseOne( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose ); + extern Vec_Str_t * Bmc_CollapseOneOld( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose ); Gia_Man_t * pGia = Gia_ManDupCones( p, &iCo, 1, 1 ); if ( fVerbose ) printf( "Output %4d: Supp = %4d. Cone =%6d.\n", iCo, Vec_IntSize(vSupp), Gia_ManAndNum(pGia) ); - vSop = Bmc_CollapseOne( pGia, nCubeLim, nBTLimit, fCanon, fReverse, fVerbose ); + vSop = Bmc_CollapseOneOld( pGia, nCubeLim, nBTLimit, fCanon, fReverse, fVerbose ); Gia_ManStop( pGia ); if ( vSop == NULL ) return NULL; @@ -718,13 +727,15 @@ Vec_Str_t * Abc_NtkClpGiaOne( Gia_Man_t * p, int iCo, int nCubeLim, int nBTLimit Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); return vSop; } -Vec_Str_t * Abc_NtkClpGiaOne2( Cnf_Dat_t * pCnf, Gia_Man_t * p, int iCo, int nCubeLim, int nBTLimit, int fVerbose, int fCanon, int fReverse, Vec_Int_t * vSupp, Vec_Int_t * vMap ) +Vec_Str_t * Abc_NtkClpGiaOne2( Cnf_Dat_t * pCnf, Gia_Man_t * p, int iCo, int nCubeLim, int nBTLimit, int fCanon, int fReverse, Vec_Int_t * vSupp, Vec_Int_t * vMap, int fVerbose ) { Vec_Str_t * vSop; - sat_solver * pSat, * pSat2 = NULL; + sat_solver * pSat, * pSat1 = NULL, * pSat2 = NULL, * pSat3 = NULL; Gia_Obj_t * pObj; abctime clk = Abc_Clock(); - extern Vec_Str_t * Bmc_CollapseOne_int( sat_solver * pSat, sat_solver * pSat2, int nVars, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose ); + extern Vec_Str_t * Bmc_CollapseOne_int( sat_solver * pSat, int nVars, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose ); + extern Vec_Str_t * Bmc_CollapseOne_int2( sat_solver * pSat, sat_solver * pSat2, int nVars, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose ); + extern Vec_Str_t * Bmc_CollapseOne_int3( sat_solver * pSat, sat_solver * pSat1, sat_solver * pSat2, sat_solver * pSat3, int nVars, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose ); int i, iCoObjId = Gia_ObjId( p, Gia_ManCo(p, iCo) ); Vec_Int_t * vAnds = Vec_IntAlloc( 100 ); Vec_Int_t * vSuppObjs = Vec_IntAlloc( 100 ); @@ -733,13 +744,18 @@ Vec_Str_t * Abc_NtkClpGiaOne2( Cnf_Dat_t * pCnf, Gia_Man_t * p, int iCo, int nCu Gia_ManIncrementTravId( p ); Gia_ManCollectAnds( p, &iCoObjId, 1, vAnds ); assert( Vec_IntSize(vAnds) > 0 ); - pSat = Abc_NtkClpDeriveSatSolver( pCnf, iCoObjId, vSuppObjs, vAnds, vMap, &pSat2 ); +// pSat = Abc_NtkClpDeriveSatSolver( pCnf, iCoObjId, vSuppObjs, vAnds, vMap, &pSat1, &pSat2, &pSat3 ); + pSat = Abc_NtkClpDeriveSatSolver( pCnf, iCoObjId, vSuppObjs, vAnds, vMap, NULL, NULL, NULL ); Vec_IntFree( vSuppObjs ); if ( fVerbose ) printf( "Output %4d: Supp = %4d. Cone =%6d.\n", iCo, Vec_IntSize(vSupp), Vec_IntSize(vAnds) ); - vSop = Bmc_CollapseOne_int( pSat, pSat2, Vec_IntSize(vSupp), nCubeLim, nBTLimit, fCanon, fReverse, fVerbose ); +// vSop = Bmc_CollapseOne_int3( pSat, pSat1, pSat2, pSat3, Vec_IntSize(vSupp), nCubeLim, nBTLimit, fCanon, fReverse, fVerbose ); +// vSop = Bmc_CollapseOne_int2( pSat, pSat1, Vec_IntSize(vSupp), nCubeLim, nBTLimit, fCanon, fReverse, fVerbose ); + vSop = Bmc_CollapseOne_int( pSat, Vec_IntSize(vSupp), nCubeLim, nBTLimit, fCanon, fReverse, fVerbose ); sat_solver_delete( pSat ); - sat_solver_delete( pSat2 ); + if ( pSat1 ) sat_solver_delete( pSat1 ); + if ( pSat2 ) sat_solver_delete( pSat2 ); + if ( pSat3 ) sat_solver_delete( pSat3 ); Vec_IntFree( vAnds ); if ( vSop == NULL ) return NULL; @@ -794,8 +810,8 @@ Vec_Ptr_t * Abc_GiaDeriveSops( Abc_Ntk_t * pNtkNew, Gia_Man_t * p, Vec_Wec_t * v Vec_PtrWriteEntry( vSopsRepr, iEntry, (void *)(ABC_PTRINT_T)1 ); continue; } -// vSop = Abc_NtkClpGiaOne( p, iCoThis, nCubeLim, nBTLimit, i ? 0 : fVerbose, fCanon, fReverse, vSupp ); - vSop = Abc_NtkClpGiaOne2( pCnf, p, iCoThis, nCubeLim, nBTLimit, i ? 0 : fVerbose, fCanon, fReverse, vSupp, vMap ); + vSop = Abc_NtkClpGiaOne( p, iCoThis, nCubeLim, nBTLimit, fCanon, fReverse, vSupp, i ? 0 : fVerbose ); +// vSop = Abc_NtkClpGiaOne2( pCnf, p, iCoThis, nCubeLim, nBTLimit, fCanon, fReverse, vSupp, vMap, i ? 0 : fVerbose ); if ( vSop == NULL ) goto finish; assert( Vec_IntSize( Vec_WecEntry(vSupps, iCoThis) ) == Abc_SopGetVarNum(Vec_StrArray(vSop)) ); -- cgit v1.2.3