diff options
Diffstat (limited to 'src/aig/gia/giaSatEdge.c')
| -rw-r--r-- | src/aig/gia/giaSatEdge.c | 417 |
1 files changed, 417 insertions, 0 deletions
diff --git a/src/aig/gia/giaSatEdge.c b/src/aig/gia/giaSatEdge.c new file mode 100644 index 00000000..982aaa79 --- /dev/null +++ b/src/aig/gia/giaSatEdge.c @@ -0,0 +1,417 @@ +/**CFile**************************************************************** + + FileName [giaSatEdge.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Scalable AIG package.] + + Synopsis [] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: giaSatEdge.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "gia.h" +#include "misc/tim/tim.h" +#include "sat/bsat/satStore.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Seg_Man_t_ Seg_Man_t; +struct Seg_Man_t_ +{ + sat_solver * pSat; // SAT solver + Vec_Int_t * vCardVars; // candinality variables + int nVars; // max vars (edge num) + int LogN; // base-2 log of max vars + int Power2; // power-2 of LogN + int FirstVar; // first variable to be used + // parameters + int nBTLimit; // conflicts + int DelayMax; // external delay + int nEdges; // the number of edges + int fDelay; // delay mode + int fReverse; // reverse windowing + int fVerbose; // verbose + // window + Gia_Man_t * pGia; + Vec_Int_t * vEdges; // edges as fanin/fanout pairs + Vec_Int_t * vFirsts; // first SAT variable + Vec_Int_t * vNvars; // number of SAT variables + Vec_Int_t * vLits; // literals + int * pLevels; // levels + + // statistics + abctime timeStart; +}; + +extern sat_solver * Sbm_AddCardinSolver( int LogN, Vec_Int_t ** pvVars ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Count the number of edges between internal nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Seg_ManCountIntEdges( Gia_Man_t * p ) +{ + int i, iLut, iFanin; + Vec_Int_t * vEdges = Vec_IntAlloc( 1000 ); + assert( Gia_ManHasMapping(p) ); + Gia_ManForEachLut( p, iLut ) + Gia_LutForEachFanin( p, iLut, iFanin, i ) + if ( Gia_ObjIsAnd(Gia_ManObj(p, iFanin)) ) + { + //printf( "Var %d: %d -> %d\n", Vec_IntSize(vEdges)/2, iFanin, iLut ); + + Vec_IntPushTwo( vEdges, iFanin, iLut ); + } + return vEdges; +} +Vec_Wec_t * Seg_ManCollectObjEdges( Vec_Int_t * vEdges, int nObjs ) +{ + int iFanin, iObj, i; + Vec_Wec_t * vRes = Vec_WecStart( nObjs ); + Vec_IntForEachEntryDouble( vEdges, iFanin, iObj, i ) + { + Vec_WecPush( vRes, iFanin, i/2 ); + Vec_WecPush( vRes, iObj, i/2 ); + } + return vRes; +} +int Seg_ManCountIntLevels( Seg_Man_t * p, int iStartVar ) +{ + int iLut, nVars; + Vec_IntFill( p->vFirsts, Gia_ManObjNum(p->pGia), -1 ); + Vec_IntFill( p->vNvars, Gia_ManObjNum(p->pGia), 0 ); + ABC_FREE( p->pLevels ); + p->DelayMax = Gia_ManLutLevel( p->pGia, &p->pLevels ); + Gia_ManForEachLut( p->pGia, iLut ) + { + Vec_IntWriteEntry( p->vFirsts, iLut, iStartVar ); + assert( p->pLevels[iLut] > 0 ); + nVars = p->pLevels[iLut] == 1 ? 0 : p->pLevels[iLut]; + Vec_IntWriteEntry( p->vNvars, iLut, nVars ); + iStartVar += nVars; + } + return iStartVar; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Seg_Man_t * Seg_ManAlloc( Gia_Man_t * pGia ) +{ + int nVarsAll; + Seg_Man_t * p = ABC_CALLOC( Seg_Man_t, 1 ); + p->vEdges = Seg_ManCountIntEdges( pGia ); + p->nVars = Vec_IntSize(p->vEdges)/2; + p->LogN = Abc_Base2Log(p->nVars); + p->Power2 = 1 << p->LogN; + //p->pSat = Sbm_AddCardinSolver( p->LogN, &p->vCardVars ); + p->pSat = sat_solver_new(); + sat_solver_setnvars( p->pSat, p->nVars ); + p->FirstVar = sat_solver_nvars( p->pSat ); + sat_solver_bookmark( p->pSat ); + p->pGia = pGia; + // internal + p->vFirsts = Vec_IntAlloc( 0 ); + p->vNvars = Vec_IntAlloc( 0 ); + p->vLits = Vec_IntAlloc( 0 ); + nVarsAll = Seg_ManCountIntLevels( p, p->FirstVar ); + sat_solver_setnvars( p->pSat, nVarsAll ); +printf( "Edges = %d. Total = %d.\n", p->FirstVar, nVarsAll ); + // other + Gia_ManFillValue( pGia ); + return p; +} +void Seg_ManClean( Seg_Man_t * p ) +{ + p->timeStart = Abc_Clock(); + sat_solver_rollback( p->pSat ); + sat_solver_bookmark( p->pSat ); + // internal + Vec_IntClear( p->vEdges ); + Vec_IntClear( p->vFirsts ); + Vec_IntClear( p->vNvars ); + Vec_IntClear( p->vLits ); + // other + Gia_ManFillValue( p->pGia ); +} +void Seg_ManStop( Seg_Man_t * p ) +{ + sat_solver_delete( p->pSat ); + //Vec_IntFree( p->vCardVars ); + // internal + Vec_IntFree( p->vEdges ); + Vec_IntFree( p->vFirsts ); + Vec_IntFree( p->vNvars ); + Vec_IntFree( p->vLits ); + ABC_FREE( p->pLevels ); + // other + ABC_FREE( p ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Seg_ManCreateCnf( Seg_Man_t * p, int fTwo ) +{ + Gia_Obj_t * pObj; + Vec_Wec_t * vObjEdges; + Vec_Int_t * vLevel; + int iLut, iFanin, iFirst; + int pLits[3], Count = 0; + int i, k, nVars, value; + abctime clk = Abc_Clock(); + // edge delay constraints + int nConstr = sat_solver_nclauses(p->pSat); + Gia_ManForEachObj( p->pGia, pObj, iLut ) + { + int iFirstLut = Vec_IntEntry( p->vFirsts, iLut ); + int nVarsLut = Vec_IntEntry( p->vNvars, iLut ); + if ( !Gia_ObjIsLut(p->pGia, iLut) ) + continue; + Gia_LutForEachFanin( p->pGia, iLut, iFanin, i ) + if ( Gia_ObjIsAnd(Gia_ManObj(p->pGia, iFanin)) ) + { + iFirst = Vec_IntEntry( p->vFirsts, iFanin ); + nVars = Vec_IntEntry( p->vNvars, iFanin ); + assert( nVars != 1 && nVars < nVarsLut ); + // add initial + if ( nVars == 0 ) + { + pLits[0] = Abc_Var2Lit( Count, 1 ); + pLits[1] = Abc_Var2Lit( iFirstLut, 0 ); + value = sat_solver_addclause( p->pSat, pLits, pLits+2 ); + assert( value ); + + pLits[0] = Abc_Var2Lit( Count, 0 ); + pLits[1] = Abc_Var2Lit( iFirstLut+1, 0 ); + value = sat_solver_addclause( p->pSat, pLits, pLits+2 ); + assert( value ); + } + // add others + for ( k = 0; k < nVars; k++ ) + { + pLits[0] = Abc_Var2Lit( iFirst+k, 1 ); + pLits[1] = Abc_Var2Lit( Count, 1 ); + pLits[2] = Abc_Var2Lit( iFirstLut+k, 0 ); + value = sat_solver_addclause( p->pSat, pLits, pLits+3 ); + assert( value ); + + pLits[0] = Abc_Var2Lit( iFirst+k, 1 ); + pLits[1] = Abc_Var2Lit( Count, 0 ); + pLits[2] = Abc_Var2Lit( iFirstLut+k+1, 0 ); + value = sat_solver_addclause( p->pSat, pLits, pLits+3 ); + assert( value ); + } + Count++; + } + } + assert( Count == p->nVars ); + printf( "Delay constraints = %d. ", sat_solver_nclauses(p->pSat) - nConstr ); + nConstr = sat_solver_nclauses(p->pSat); +/* + // delay relationship constraints + Vec_IntForEachEntryTwo( p->vFirsts, p->vNvars, iFirst, nVars, iLut ) + { + if ( nVars < 2 ) + continue; + for ( i = 1; i < nVars; i++ ) + { + pLits[0] = Abc_Var2Lit( iFirst + i - 1, 1 ); + pLits[1] = Abc_Var2Lit( iFirst + i, 0 ); + value = sat_solver_addclause( p->pSat, pLits, pLits+2 ); + assert( value ); + } + } +*/ + // edge compatibility constraint + vObjEdges = Seg_ManCollectObjEdges( p->vEdges, Gia_ManObjNum(p->pGia) ); + Vec_WecForEachLevel( vObjEdges, vLevel, i ) + { + int v1, v2, v3, Var1, Var2, Var3; + if ( !fTwo && Vec_IntSize(vLevel) >= 2 ) + { + Vec_IntForEachEntry( vLevel, Var1, v1 ) + Vec_IntForEachEntryStart( vLevel, Var2, v2, v1 + 1 ) + { + pLits[0] = Abc_Var2Lit( Var1, 1 ); + pLits[1] = Abc_Var2Lit( Var2, 1 ); + value = sat_solver_addclause( p->pSat, pLits, pLits+2 ); + assert( value ); + } + } + else if ( fTwo && Vec_IntSize(vLevel) >= 3 ) + { + Vec_IntForEachEntry( vLevel, Var1, v1 ) + Vec_IntForEachEntryStart( vLevel, Var2, v2, v1 + 1 ) + Vec_IntForEachEntryStart( vLevel, Var3, v3, v2 + 1 ) + { + pLits[0] = Abc_Var2Lit( Var1, 1 ); + pLits[1] = Abc_Var2Lit( Var2, 1 ); + pLits[2] = Abc_Var2Lit( Var3, 1 ); + value = sat_solver_addclause( p->pSat, pLits, pLits+3 ); + assert( value ); + } + } + } + Vec_WecFree( vObjEdges ); + printf( "Edge constraints = %d. ", sat_solver_nclauses(p->pSat) - nConstr ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Seg_ManConvertResult( Seg_Man_t * p ) +{ + int iFanin, iObj, i; + Vec_Int_t * vEdges2 = Vec_IntAlloc( 1000 ); + Vec_IntForEachEntryDouble( p->vEdges, iFanin, iObj, i ) + if ( sat_solver_var_value(p->pSat, i/2) ) + Vec_IntPushTwo( vEdges2, iFanin, iObj ); + Gia_ManEdgeFromArray( p->pGia, vEdges2 ); + Vec_IntFree( vEdges2 ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Seg_ManComputeDelay( Gia_Man_t * pGia, int Delay, int fTwo, int fVerbose ) +{ + Gia_Obj_t * pObj; + abctime clk = Abc_Clock(); + int i, d, iLut, iFirst, nVars, status, Limit;//, value; + Seg_Man_t * p = Seg_ManAlloc( pGia ); + + //if ( fVerbose ) + printf( "Running SatEdge with delay %d and edge %d\n", Delay, fTwo+1 ); + + Seg_ManCreateCnf( p, fTwo ); + //Sat_SolverWriteDimacs( p->pSat, "test_edge.cnf", NULL, NULL, 0 ); + +// for ( Delay = p->DelayMax; Delay >= 2; Delay-- ) + { + // collect assumptions + Vec_IntClear( p->vLits ); + Gia_ManForEachCoDriver( p->pGia, pObj, i ) + { + if ( !Gia_ObjIsAnd(pObj) ) + continue; + iLut = Gia_ObjId( p->pGia, pObj ); + iFirst = Vec_IntEntry( p->vFirsts, iLut ); + nVars = Vec_IntEntry( p->vNvars, iLut ); + Limit = Abc_MinInt( nVars, Delay ); + +// for ( d = 0; d < Limit; d++ ) +// Vec_IntPush( p->vLits, Abc_Var2Lit(iFirst + d, 0) ); +// value = sat_solver_addclause( p->pSat, Vec_IntArray(p->vLits), Vec_IntLimit(p->vLits) ); +// assert( value ); + + for ( d = Delay; d < nVars; d++ ) + Vec_IntPush( p->vLits, Abc_Var2Lit(iFirst + d, 1) ); + + } + // solve with assumptions + status = sat_solver_solve( p->pSat, Vec_IntArray(p->vLits), Vec_IntLimit(p->vLits), 0, 0, 0, 0 ); + + //if ( status != l_True ) + // break; + + if ( status == l_True ) + { + int Count = 0; + for ( i = 0; i < p->nVars; i++ ) + Count += sat_solver_var_value(p->pSat, i); + + //printf( "\n" ); + //Vec_IntPrint( p->vLits ); + printf( "Solution with delay %d exists. Edges = %d. ", Delay, Count ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); + + if ( fVerbose ) + { + for ( i = 0; i < p->nVars; i++ ) + printf( "%d=%d ", i, sat_solver_var_value(p->pSat, i) ); + printf( " " ); + + for ( i = p->nVars; i < sat_solver_nvars(p->pSat); i++ ) + printf( "%d=%d ", i, sat_solver_var_value(p->pSat, i) ); + printf( "\n" ); + } + } + else + { + printf( "Proved UNSAT for delay %d. ", Delay ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); + } + } + // convert and quit + if ( status == l_True ) + Seg_ManConvertResult( p ); + Seg_ManStop( p ); +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + |