From 2a5fa67d36393ab3ddb14e5bf542b0f29c8634e1 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 11 Feb 2017 17:28:37 -0800 Subject: Adding APIs to mark cones. Creating test-bench for incremental solving &satoko -i. --- src/aig/gia/giaSatoko.c | 133 ++++++++++++++++++++++++++++++++++++++---------- 1 file changed, 105 insertions(+), 28 deletions(-) (limited to 'src/aig') diff --git a/src/aig/gia/giaSatoko.c b/src/aig/gia/giaSatoko.c index db81bd85..7cbc4184 100644 --- a/src/aig/gia/giaSatoko.c +++ b/src/aig/gia/giaSatoko.c @@ -45,39 +45,93 @@ ABC_NAMESPACE_IMPL_START SeeAlso [] ***********************************************************************/ -satoko_t * Gia_ManCreateSatoko( Gia_Man_t * p ) +void Gia_ManCollectVars_rec( int Var, Vec_Int_t * vMapping, Vec_Int_t * vRes, Vec_Bit_t * vVisit ) +{ + int * pCut, i; + if ( Vec_BitEntry(vVisit, Var) ) + return; + Vec_BitWriteEntry(vVisit, Var, 1); + if ( Vec_IntEntry(vMapping, Var) ) // primary input or constant 0 + { + pCut = Vec_IntEntryP( vMapping, Vec_IntEntry(vMapping, Var) ); + for ( i = 1; i <= pCut[0]; i++ ) + Gia_ManCollectVars_rec( pCut[i], vMapping, vRes, vVisit ); + } + Vec_IntPush( vRes, Var ); +} +Vec_Int_t * Gia_ManCollectVars( int Root, Vec_Int_t * vMapping, int nVars ) +{ + Vec_Int_t * vRes = Vec_IntAlloc( 100 ); + Vec_Bit_t * vVisit = Vec_BitStart( nVars ); + assert( Vec_IntEntry(vMapping, Root) ); + Gia_ManCollectVars_rec( Root, vMapping, vRes, vVisit ); + Vec_BitFree( vVisit ); + return vRes; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +satoko_t * Gia_ManSatokoInit( Cnf_Dat_t * pCnf, satoko_opts_t * opts ) { satoko_t * pSat = satoko_create(); - Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8, 0, 1, 0, 0 ); - int i, status; + int i; //sat_solver_setnvars( pSat, p->nVars ); for ( i = 0; i < pCnf->nClauses; i++ ) { if ( !satoko_add_clause( pSat, (unsigned *)pCnf->pClauses[i], pCnf->pClauses[i+1]-pCnf->pClauses[i] ) ) { - Cnf_DataFree( pCnf ); satoko_destroy( pSat ); return NULL; } } + satoko_configure(pSat, opts); + return pSat; +} +void Gia_ManSatokoReport( int iOutput, int status, abctime clk ) +{ + if ( iOutput >= 0 ) + Abc_Print( 1, "Output %6d : ", iOutput ); + else + Abc_Print( 1, "Total: " ); + + if ( status == SATOKO_UNDEC ) + Abc_Print( 1, "UNDECIDED " ); + else if ( status == SATOKO_SAT ) + Abc_Print( 1, "SATISFIABLE " ); + else + Abc_Print( 1, "UNSATISFIABLE " ); + + Abc_PrintTime( 1, "Time", clk ); +} +satoko_t * Gia_ManSatokoCreate( Gia_Man_t * p, satoko_opts_t * opts ) +{ + Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8, 0, 1, 0, 0 ); + satoko_t * pSat = Gia_ManSatokoInit( pCnf, opts ); + int status = pSat ? satoko_simplify(pSat) : SATOKO_OK; Cnf_DataFree( pCnf ); - status = satoko_simplify(pSat); if ( status == SATOKO_OK ) return pSat; satoko_destroy( pSat ); return NULL; } -int Gia_ManCallSatokoOne( Gia_Man_t * p, satoko_opts_t * opts, int iOutput ) +int Gia_ManSatokoCallOne( Gia_Man_t * p, satoko_opts_t * opts, int iOutput ) { abctime clk = Abc_Clock(); satoko_t * pSat; int status, Cost = 0; - - pSat = Gia_ManCreateSatoko( p ); + pSat = Gia_ManSatokoCreate( p, opts ); if ( pSat ) { - satoko_configure(pSat, opts); status = satoko_solve( pSat ); Cost = (unsigned)pSat->stats.n_conflicts; satoko_destroy( pSat ); @@ -85,37 +139,60 @@ int Gia_ManCallSatokoOne( Gia_Man_t * p, satoko_opts_t * opts, int iOutput ) else status = SATOKO_UNSAT; - if ( iOutput >= 0 ) - Abc_Print( 1, "Output %6d : ", iOutput ); - else - Abc_Print( 1, "Total: " ); - - if ( status == SATOKO_UNDEC ) - Abc_Print( 1, "UNDECIDED " ); - else if ( status == SATOKO_SAT ) - Abc_Print( 1, "SATISFIABLE " ); - else - Abc_Print( 1, "UNSATISFIABLE " ); - - Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); + Gia_ManSatokoReport( iOutput, status, Abc_Clock() - clk ); return Cost; } -void Gia_ManCallSatoko( Gia_Man_t * p, satoko_opts_t * opts, int fSplit ) +void Gia_ManSatokoCall( Gia_Man_t * p, satoko_opts_t * opts, int fSplit, int fIncrem ) { + int fUseCone = 1; + Gia_Man_t * pOne; + Gia_Obj_t * pRoot; + Vec_Int_t * vCone; + int i, iLit, status; + if ( fIncrem ) + { + abctime clk = Abc_Clock(); + Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8, 0, 0, fUseCone, 0 ); + satoko_t * pSat = Gia_ManSatokoInit( pCnf, opts ); + Gia_ManForEachCo( p, pRoot, i ) + { + abctime clk = Abc_Clock(); + iLit = Abc_Var2Lit( i+1, 0 ); + satoko_assump_push( pSat, iLit ); + if ( fUseCone ) + { + vCone = Gia_ManCollectVars( i+1, pCnf->vMapping, pCnf->nVars ); + satoko_mark_cone( pSat, Vec_IntArray(vCone), Vec_IntSize(vCone) ); + printf( "Cone has %6d vars (out of %6d). ", Vec_IntSize(vCone), pCnf->nVars ); + status = satoko_solve( pSat ); + satoko_unmark_cone( pSat, Vec_IntArray(vCone), Vec_IntSize(vCone) ); + Vec_IntFree( vCone ); + } + else + { + status = satoko_solve( pSat ); + } + satoko_assump_pop( pSat ); + Gia_ManSatokoReport( i, status, Abc_Clock() - clk ); + } + Cnf_DataFree( pCnf ); + satoko_destroy( pSat ); + Abc_PrintTime( 1, "Total time", Abc_Clock() - clk ); + return; + } if ( fSplit ) { - Gia_Man_t * pOne; - Gia_Obj_t * pRoot; - int i; + abctime clk = Abc_Clock(); Gia_ManForEachCo( p, pRoot, i ) { pOne = Gia_ManDupDfsCone( p, pRoot ); - Gia_ManCallSatokoOne( pOne, opts, i ); + Gia_ManSatokoCallOne( pOne, opts, i ); Gia_ManStop( pOne ); } + Abc_PrintTime( 1, "Total time", Abc_Clock() - clk ); return; } - Gia_ManCallSatokoOne( p, opts, -1 ); + Gia_ManSatokoCallOne( p, opts, -1 ); } -- cgit v1.2.3