diff options
| -rw-r--r-- | src/aig/gia/giaOf.c | 155 | ||||
| -rw-r--r-- | src/sat/bsat/satSolver.h | 9 |
2 files changed, 164 insertions, 0 deletions
diff --git a/src/aig/gia/giaOf.c b/src/aig/gia/giaOf.c index 4ee92126..5a0b94e3 100644 --- a/src/aig/gia/giaOf.c +++ b/src/aig/gia/giaOf.c @@ -27,6 +27,7 @@ #include "misc/vec/vecMem.h" #include "misc/vec/vecWec.h" #include "opt/dau/dau.h" +#include "sat/bsat/satStore.h" ABC_NAMESPACE_IMPL_START @@ -1499,6 +1500,159 @@ void Of_ManComputeBackwardDircon1( Of_Man_t * p ) /**Function************************************************************* + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Of_ManCreateSat( Of_Man_t * p, int nCutsAll, Vec_Int_t * vFirst, Vec_Int_t * vCutNum, Vec_Int_t * vBest ) +{ + Gia_Obj_t * pObj; + int * pCutSet, * pCut; + int i, k, v, c, Var, status, RetValue, nCutCount = 0; + Vec_Int_t * vLits = Vec_IntAlloc( 100 ); + abctime clk = Abc_Clock(); + + // start solver + sat_solver * pSat = sat_solver_new(); + sat_solver_setnvars( pSat, nCutsAll ); + sat_solver_start_cardinality( pSat, Vec_IntSize(vBest) ); + printf( "Setting candinality equal to %d.\n", pSat->nCard ); + + // set polarity +// Vec_IntPop( vBest ); +// sat_solver_set_polarity( pSat, Vec_IntArray(vBest), Vec_IntSize(vBest) ); + //Vec_IntPrint( vBest ); + + // mark CO drivers + Gia_ManForEachCo( p->pGia, pObj, i ) + Gia_ObjFanin0(pObj)->fMark0 = 1; + // add clauses + Gia_ManForEachAnd( p->pGia, pObj, i ) + { + if ( pObj->fMark0 ) + { + int iFirst = Vec_IntEntry(vFirst, i); + int nCuts = Vec_IntEntry(vCutNum, i); + Vec_IntClear( vLits ); + for ( c = 0; c < nCuts; c++ ) + Vec_IntPush( vLits, Abc_Var2Lit(iFirst + c, 0) ); + RetValue = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits) ); + assert( RetValue ); + } + } + // unmark CO drivers + Gia_ManForEachCo( p->pGia, pObj, i ) + Gia_ObjFanin0(pObj)->fMark0 = 0; + + // add clauses + Gia_ManForEachAnd( p->pGia, pObj, i ) + { + pCutSet = Of_ObjCutSet(p, i); + Of_SetForEachCut( pCutSet, pCut, k ) + { + Of_CutForEachVar( pCut, Var, v ) + { + if ( Gia_ObjIsAnd(Gia_ManObj(p->pGia, Var)) ) + { + int iFirst = Vec_IntEntry(vFirst, Var); + int nCuts = Vec_IntEntry(vCutNum, Var); + Vec_IntClear( vLits ); + Vec_IntPush( vLits, Abc_Var2Lit(nCutCount, 1) ); + for ( c = 0; c < nCuts; c++ ) + Vec_IntPush( vLits, Abc_Var2Lit(iFirst + c, 0) ); + RetValue = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits) ); + assert( RetValue ); + } + } + nCutCount++; + } + } + assert( nCutCount == nCutsAll ); + // solve the problem + status = sat_solver_solve( pSat, NULL, NULL, 1000000, 0, 0, 0 ); + if ( status == l_Undef ) + printf( "Undecided. " ); + if ( status == l_True ) + printf( "Satisfiable. " ); + if ( status == l_False ) + printf( "Unsatisfiable. " ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); + Sat_SolverPrintStats( stdout, pSat ); + if ( status == l_True ) + { + int nOnes = 0; + for ( v = 0; v < pSat->size; v++ ) + { + printf( "%d", sat_solver_var_value(pSat, v) ); + nOnes += sat_solver_var_value(pSat, v); + } + printf( " nOnes = %d\n", nOnes ); + } + + // cleanup + sat_solver_delete( pSat ); + Vec_IntFree( vLits ); +} +void Of_ManPrintCuts( Of_Man_t * p ) +{ + int fVerbose = 0; + Gia_Obj_t * pObj; + int * pCutSet, * pCut, * pCutBest; + int i, k, v, Var, nCuts; + int nAndsAll = 0, nLutsAll = 0, nCutsAll = 0; + Vec_Int_t * vFirst = Vec_IntStartFull( Gia_ManObjNum(p->pGia) ); + Vec_Int_t * vCutNum = Vec_IntStartFull( Gia_ManObjNum(p->pGia) ); + Vec_Int_t * vBest = Vec_IntAlloc( 100 ); + Gia_ManForEachAnd( p->pGia, pObj, i ) + { + nAndsAll++; + // get the best cut + pCutBest = NULL; + if ( Of_ObjRefNum(p, i) ) + pCutBest = Of_ObjCutBestP( p, i ), nLutsAll++; + // get the cutset + pCutSet = Of_ObjCutSet(p, i); + // count cuts + nCuts = 0; + Of_SetForEachCut( pCutSet, pCut, k ) + nCuts++; + // save + Vec_IntWriteEntry( vFirst, i, nCutsAll ); + Vec_IntWriteEntry( vCutNum, i, nCuts ); + // print cuts + if ( fVerbose ) + printf( "Node %d. Cuts %d.\n", i, nCuts ); + Of_SetForEachCut( pCutSet, pCut, k ) + { + if ( fVerbose ) + { + printf( "{ " ); + Of_CutForEachVar( pCut, Var, v ) + printf( "%d ", Var ); + printf( "} %s\n", pCutBest == pCut ? "best" :"" ); + } + if ( pCutBest == pCut ) + Vec_IntPush( vBest, nCutsAll ); + nCutsAll++; + } + } + printf( "Total: Ands = %d. Luts = %d. Cuts = %d.\n", nAndsAll, nLutsAll, nCutsAll ); + + // create SAT problem + Of_ManCreateSat( p, nCutsAll, vFirst, vCutNum, vBest ); + + Vec_IntFree( vFirst ); + Vec_IntFree( vCutNum ); + Vec_IntFree( vBest ); +} + +/**Function************************************************************* + Synopsis [Technology mappping.] Description [] @@ -1659,6 +1813,7 @@ Gia_Man_t * Of_ManPerformMapping( Gia_Man_t * pGia, Jf_Par_t * pPars ) pNew = Of_ManDeriveMapping( p ); Gia_ManMappingVerify( pNew ); +// Of_ManPrintCuts( p ); Of_StoDelete( p ); if ( pCls != pGia ) Gia_ManStop( pCls ); diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h index f1738eb5..fc92e557 100644 --- a/src/sat/bsat/satSolver.h +++ b/src/sat/bsat/satSolver.h @@ -301,6 +301,15 @@ static inline void sat_solver_start_cardinality(sat_solver* s, int nSize) s->nCard = nSize; s->nCardClauses = 0; } +static void sat_solver_set_polarity(sat_solver* s, int * pVars, int nVars ) +{ + int i; + for ( i = 0; i < s->size; i++ ) + s->polarity[i] = 0; + for ( i = 0; i < nVars; i++ ) + s->polarity[pVars[i]] = 1; +} + static inline int sat_solver_add_const( sat_solver * pSat, int iVar, int fCompl ) { lit Lits[1]; |