/**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 * vPolars; // polarity
Vec_Int_t * vToSkip; // edges to skip
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, Vec_Int_t * vPolars, Vec_Int_t * vToSkip, int nFanouts )
{
int i, iLut, iFanin;
Vec_Int_t * vEdges = Vec_IntAlloc( 1000 );
assert( Gia_ManHasMapping(p) );
Vec_IntClear( vPolars );
Vec_IntClear( vToSkip );
if ( nFanouts )
Gia_ManSetLutRefs( p );
Gia_ManForEachLut( p, iLut )
Gia_LutForEachFanin( p, iLut, iFanin, i )
if ( Gia_ObjIsAnd(Gia_ManObj(p, iFanin)) )
{
if ( p->vEdge1 && Gia_ObjCheckEdge(p, iFanin, iLut) )
Vec_IntPush( vPolars, Vec_IntSize(vEdges)/2 );
if ( nFanouts && Gia_ObjLutRefNumId(p, iFanin) >= nFanouts )
Vec_IntPush( vToSkip, Vec_IntSize(vEdges)/2 );
Vec_IntPushTwo( vEdges, iFanin, iLut );
}
if ( nFanouts )
ABC_FREE( p->pLutRefs );
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 )
{
Gia_Obj_t * pObj;
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 );
if ( p->pGia->pManTime )
{
p->DelayMax = Gia_ManLutLevelWithBoxes( p->pGia );
p->pLevels = Vec_IntReleaseArray( p->pGia->vLevels );
Vec_IntFreeP( &p->pGia->vLevels );
}
else
p->DelayMax = Gia_ManLutLevel( p->pGia, &p->pLevels );
Gia_ManForEachObj1( p->pGia, pObj, iLut )
{
if ( Gia_ObjIsCo(pObj) )
continue;
if ( Gia_ObjIsAnd(pObj) && !Gia_ObjIsLut(p->pGia, iLut) )
continue;
assert( Gia_ObjIsCi(pObj) || Gia_ObjIsLut(p->pGia, iLut) );
Vec_IntWriteEntry( p->vFirsts, iLut, iStartVar );
//assert( p->pLevels[iLut] > 0 );
nVars = p->pLevels[iLut] < 2 ? 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 nFanouts )
{
int nVarsAll;
Seg_Man_t * p = ABC_CALLOC( Seg_Man_t, 1 );
p->vPolars = Vec_IntAlloc( 1000 );
p->vToSkip = Vec_IntAlloc( 1000 );
p->vEdges = Seg_ManCountIntEdges( pGia, p->vPolars, p->vToSkip, nFanouts );
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 );
// 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 );
Vec_IntClear( p->vPolars );
Vec_IntClear( p->vToSkip );
// 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 );
Vec_IntFree( p->vPolars );
Vec_IntFree( p->vToSkip );
ABC_FREE( p->pLevels );
// other
ABC_FREE( p );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Seg_ManCreateCnf( Seg_Man_t * p, int fTwo, int fVerbose )
{
Tim_Man_t * pTim = (Tim_Man_t *)p->pGia->pManTime;
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, Edge, 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 ( pTim && Gia_ObjIsCi(pObj) )
{
int iBox = Tim_ManBoxForCi( pTim, Gia_ObjCioId(pObj) );
if ( nVarsLut > 0 && iBox >= 0 )
{
int iCiId = Tim_ManBoxOutputFirst( pTim, iBox );
if ( iCiId == Gia_ObjCioId(pObj) ) // first input
{
int nIns = Tim_ManBoxInputNum( pTim, iBox );
int iIn0 = Tim_ManBoxInputFirst( pTim, iBox );
for ( i = 0; i < nIns-1; i++ ) // skip carry-in pin
{
Gia_Obj_t * pOut = Gia_ManCo( p->pGia, iIn0+i );
int iDriverId = Gia_ObjFaninId0p( p->pGia, pOut );
int AddOn;
iFirst = Vec_IntEntry( p->vFirsts, iDriverId );
nVars = Vec_IntEntry( p->vNvars, iDriverId );
assert( nVars < nVarsLut );
AddOn = (int)(nVars < nVarsLut);
for ( k = 0; k < nVars; k++ )
{
pLits[0] = Abc_Var2Lit( iFirst+k, 1 );
pLits[1] = Abc_Var2Lit( iFirstLut+k+AddOn, 0 );
value = sat_solver_addclause( p->pSat, pLits, pLits+2 );
assert( value );
}
}
}
else // intermediate input
{
Gia_Obj_t * pIn = Gia_ManCi( p->pGia, iCiId );
int iObjId = Gia_ObjId( p->pGia, pIn );
iFirst = Vec_IntEntry( p->vFirsts, iObjId );
nVars = Vec_IntEntry( p->vNvars, iObjId );
if ( nVars > 0 )
{
for ( k = 0; k < nVars; k++ )
{
pLits[0] = Abc_Var2Lit( iFirst+k, 1 );
pLits[1] = Abc_Var2Lit( iFirstLut+k, 0 );
value = sat_solver_addclause( p->pSat, pLits, pLits+2 );
assert( value );
}
}
}
}
continue;
}
if ( !Gia_ObjIsLut(p->pGia, iLut) )
continue;
Gia_LutForEachFanin( p->pGia, iLut, iFanin, i )
if ( pTim && Gia_ObjIsCi(Gia_ManObj(p->pGia, iFanin)) )
{
iFirst = Vec_IntEntry( p->vFirsts, iFanin );
nVars = Vec_IntEntry( p->vNvars, iFanin );
assert( nVars <= nVarsLut );
if ( nVars > 0 )
{
for ( k = 0; k < nVars; k++ )
{
pLits[0] = Abc_Var2Lit( iFirst+k, 1 );
pLits[1] = Abc_Var2Lit( iFirstLut+k, 0 );
value = sat_solver_addclause( p->pSat, pLits, pLits+2 );
assert( value );
}
}
}
else 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 );
if ( fVerbose )
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) || (fTwo && Vec_IntSize(vLevel) > 10) )
{
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 );
// block forbidden edges
Vec_IntForEachEntry( p->vToSkip, Edge, i )
{
pLits[0] = Abc_Var2Lit( Edge, 1 );
value = sat_solver_addclause( p->pSat, pLits, pLits+1 );
assert( value );
}
if ( fVerbose )
printf( "Edge constraints = %d. ", sat_solver_nclauses(p->pSat) - nConstr );
if ( fVerbose )
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * 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 );
return vEdges2;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Seg_ManComputeDelay( Gia_Man_t * pGia, int DelayInit, int nFanouts, int fTwo, int fVerbose )
{
int nBTLimit = 0;
int nTimeOut = 0;
int fVeryVerbose = 0;
Gia_Obj_t * pObj;
abctime clk = Abc_Clock();
Vec_Int_t * vEdges2 = NULL;
int i, iLut, iFirst, nVars, status, Delay, nConfs;
Seg_Man_t * p = Seg_ManAlloc( pGia, nFanouts );
int DelayStart = DelayInit ? DelayInit : p->DelayMax;
if ( fVerbose )
printf( "Running SatEdge with starting delay %d and edge %d (edge vars %d, total vars %d)\n",
DelayStart, fTwo+1, p->FirstVar, sat_solver_nvars(p->pSat) );
Seg_ManCreateCnf( p, fTwo, fVerbose );
//Sat_SolverWriteDimacs( p->pSat, "test_edge.cnf", NULL, NULL, 0 );
// set resource limits
sat_solver_set_resource_limits( p->pSat, nBTLimit, 0, 0, 0 );
sat_solver_set_runtime_limit( p->pSat, nTimeOut ? nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0 );
sat_solver_set_random( p->pSat, 1 );
sat_solver_set_polarity( p->pSat, Vec_IntArray(p->vPolars), Vec_IntSize(p->vPolars) );
//sat_solver_set_var_activity( p->pSat, NULL, p->nVars );
// increment delay gradually
for ( Delay = p->DelayMax; Delay >= 0; Delay-- )
{
// we constrain COs, although it would be fine to constrain only POs
Gia_ManForEachCoDriver( p->pGia, pObj, i )
{
iLut = Gia_ObjId( p->pGia, pObj );
iFirst = Vec_IntEntry( p->vFirsts, iLut );
nVars = Vec_IntEntry( p->vNvars, iLut );
if ( Delay < nVars && !sat_solver_push(p->pSat, Abc_Var2Lit(iFirst + Delay, 1)) )
break;
}
if ( i < Gia_ManCoNum(p->pGia) )
{
printf( "Proved UNSAT for delay %d. ", Delay );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
break;
}
if ( Delay > DelayStart )
continue;
// solve with assumptions
//clk = Abc_Clock();
nConfs = sat_solver_nconflicts( p->pSat );
status = sat_solver_solve_internal( p->pSat );
nConfs = sat_solver_nconflicts( p->pSat ) - nConfs;
if ( status == l_True )
{
if ( fVerbose )
{
int Count = 0;
for ( i = 0; i < p->nVars; i++ )
Count += sat_solver_var_value(p->pSat, i);
printf( "Solution with delay %2d and %5d edges exists. Conf = %8d. ", Delay, Count, nConfs );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}
// save the result
Vec_IntFreeP( &vEdges2 );
vEdges2 = Seg_ManConvertResult( p );
if ( fVeryVerbose )
{
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
{
if ( fVerbose )
{
if ( status == l_False )
printf( "Proved UNSAT for delay %d. ", Delay );
else
printf( "Resource limit reached for delay %d. ", Delay );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}
break;
}
}
Gia_ManEdgeFromArray( p->pGia, vEdges2 );
Vec_IntFreeP( &vEdges2 );
Seg_ManStop( p );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END