#include "saig.h"
#include "sat/bsat/satSolver.h"
#include "sat/bsat/satStore.h"

Include dependency graph for saigGlaPba.c:

Classes
struct	Aig_Gla2Man_t_

Typedefs
typedef typedefABC_NAMESPACE_IMPL_START struct Aig_Gla2Man_t_	Aig_Gla2Man_t
	DECLARATIONS ///.

Functions
int	Aig_Gla2FetchVar (Aig_Gla2Man_t p, Aig_Obj_t pObj, int k)

void	Aig_Gla2AssignVars_rec (Aig_Gla2Man_t p, Aig_Obj_t pObj, int f)

int	Aig_Gla2CreateSatSolver (Aig_Gla2Man_t *p)

Aig_Gla2Man_t *	Aig_Gla2ManStart (Aig_Man_t *pAig, int nStart, int nFramesMax, int fVerbose)

void	Aig_Gla2ManStop (Aig_Gla2Man_t *p)

Vec_Int_t *	Saig_AbsSolverUnsatCore (sat_solver pSat, int nConfMax, int fVerbose, int piRetValue)

Vec_Int_t *	Aig_Gla2ManCollect (Aig_Gla2Man_t p, Vec_Int_t vCore)

Vec_Int_t *	Aig_Gla2ManPerform (Aig_Man_t *pAig, int nStart, int nFramesMax, int nConfLimit, int TimeLimit, int fSkipRand, int fVerbose)

Typedef Documentation

◆ Aig_Gla2Man_t

typedef typedefABC_NAMESPACE_IMPL_START struct Aig_Gla2Man_t_ Aig_Gla2Man_t

DECLARATIONS ///.

CFile****************************************************************

FileName [saigGlaPba.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Sequential AIG package.]

Synopsis [Gate level abstraction.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 20, 2005.]

Revision [

Id: saigGlaPba.c,v 1.00 2005/06/20 00:00:00 alanmi Exp

]

Definition at line 32 of file saigGlaPba.c.

Function Documentation

◆ Aig_Gla2AssignVars_rec()

void Aig_Gla2AssignVars_rec	(	Aig_Gla2Man_t *	p,
		Aig_Obj_t *	pObj,
		int	f )

Function*************************************************************

Synopsis [Assigns variables to the AIG nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 188 of file saigGlaPba.c.

{
    int nVars = Vec_IntSize(p->vVar2Inf);
    Aig_Gla2FetchVar( p, pObj, f );
    if ( nVars == Vec_IntSize(p->vVar2Inf) )
        return;
    if ( Aig_ObjIsConst1(pObj) )
        return;
    if ( Saig_ObjIsPo( p->pAig, pObj ) )
    {
        Aig_Gla2AssignVars_rec( p, Aig_ObjFanin0(pObj), f );
        return;
    }
    if ( Aig_ObjIsCi( pObj ) )
    {
        if ( Saig_ObjIsLo(p->pAig, pObj) && f > 0 )
            Aig_Gla2AssignVars_rec( p, Aig_ObjFanin0( Saig_ObjLoToLi(p->pAig, pObj) ), f-1 );
        return;
    }
    assert( Aig_ObjIsNode(pObj) );
    Aig_Gla2AssignVars_rec( p, Aig_ObjFanin0(pObj), f );
    Aig_Gla2AssignVars_rec( p, Aig_ObjFanin1(pObj), f );
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Aig_Gla2CreateSatSolver()

int Aig_Gla2CreateSatSolver ( Aig_Gla2Man_t * p )

Function*************************************************************

Synopsis [Creates SAT solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 223 of file saigGlaPba.c.

{
    Vec_Int_t * vPoLits;
    Aig_Obj_t * pObj;
    int i, f, ObjId, nVars, RetValue = 1;
 
    // assign variables
    for ( f = p->nFramesMax - 1; f >= 0; f-- )
//    for ( f = 0; f < p->nFramesMax; f++ )
        Aig_Gla2AssignVars_rec( p, Aig_ManCo(p->pAig, 0), f );
 
    // create SAT solver
    p->pSat = sat_solver_new();
    sat_solver_store_alloc( p->pSat ); 
    sat_solver_setnvars( p->pSat, Vec_IntSize(p->vVar2Inf)/2 );
 
    // add clauses
    nVars = Vec_IntSize( p->vVar2Inf );
    Vec_IntForEachEntryDouble( p->vVar2Inf, ObjId, f, i )
    {
        if ( ObjId == -1 )
            continue;
        pObj = Aig_ManObj( p->pAig, ObjId );
        if ( Aig_ObjIsNode(pObj) )
        {
            RetValue &= Aig_Gla2AddNode( p->pSat, Aig_Gla2FetchVar(p, pObj, f), 
                                                  Aig_Gla2FetchVar(p, Aig_ObjFanin0(pObj), f), 
                                                  Aig_Gla2FetchVar(p, Aig_ObjFanin1(pObj), f), 
                                                  Aig_ObjFaninC0(pObj), Aig_ObjFaninC1(pObj) );
            Vec_IntPush( p->vCla2Obj, ObjId );
            Vec_IntPush( p->vCla2Obj, ObjId );
            Vec_IntPush( p->vCla2Obj, ObjId );
 
            Vec_IntPush( p->vCla2Fra, f );
            Vec_IntPush( p->vCla2Fra, f );
            Vec_IntPush( p->vCla2Fra, f );
        }
        else if ( Saig_ObjIsLo(p->pAig, pObj) )
        {
            if ( f == 0 )
            {
                RetValue &= Aig_Gla2AddConst( p->pSat, Aig_Gla2FetchVar(p, pObj, f), 1 );
                Vec_IntPush( p->vCla2Obj, ObjId );
 
                Vec_IntPush( p->vCla2Fra, f );
            }
            else
            {
                Aig_Obj_t * pObjLi = Saig_ObjLoToLi(p->pAig, pObj);
                RetValue &= Aig_Gla2AddBuffer( p->pSat, Aig_Gla2FetchVar(p, pObj, f), 
                                                        Aig_Gla2FetchVar(p, Aig_ObjFanin0(pObjLi), f-1), 
                                                        Aig_ObjFaninC0(pObjLi) );
                Vec_IntPush( p->vCla2Obj, ObjId );
                Vec_IntPush( p->vCla2Obj, ObjId );
 
                Vec_IntPush( p->vCla2Fra, f );
                Vec_IntPush( p->vCla2Fra, f );
            }
        }
        else if ( Saig_ObjIsPo(p->pAig, pObj) )
        {
            RetValue &= Aig_Gla2AddBuffer( p->pSat, Aig_Gla2FetchVar(p, pObj, f), 
                                                    Aig_Gla2FetchVar(p, Aig_ObjFanin0(pObj), f), 
                                                    Aig_ObjFaninC0(pObj) );
            Vec_IntPush( p->vCla2Obj, ObjId );
            Vec_IntPush( p->vCla2Obj, ObjId );
 
            Vec_IntPush( p->vCla2Fra, f );
            Vec_IntPush( p->vCla2Fra, f );
        }
        else if ( Aig_ObjIsConst1(pObj) )
        {
            RetValue &= Aig_Gla2AddConst( p->pSat, Aig_Gla2FetchVar(p, pObj, f), 0 );
            Vec_IntPush( p->vCla2Obj, ObjId );
 
            Vec_IntPush( p->vCla2Fra, f );
        }
        else assert( Saig_ObjIsPi(p->pAig, pObj) );
    }
 
    // add output clause
    vPoLits = Vec_IntAlloc( p->nFramesMax );
    for ( f = p->nStart; f < p->nFramesMax; f++ )
        Vec_IntPush( vPoLits, 2 * Aig_Gla2FetchVar(p, Aig_ManCo(p->pAig, 0), f) );
    RetValue &= sat_solver_addclause( p->pSat, Vec_IntArray(vPoLits), Vec_IntArray(vPoLits) + Vec_IntSize(vPoLits) );
    Vec_IntFree( vPoLits );
    Vec_IntPush( p->vCla2Obj, 0 );
    Vec_IntPush( p->vCla2Fra, 0 );
    assert( Vec_IntSize(p->vCla2Fra) == Vec_IntSize(p->vCla2Obj) );
 
    assert( nVars == Vec_IntSize(p->vVar2Inf) );
    assert( ((Sto_Man_t *)p->pSat->pStore)->nClauses == Vec_IntSize(p->vCla2Obj) );
//    Sto_ManDumpClauses( ((Sto_Man_t *)p->pSat->pStore), "temp_sto.cnf" );
    sat_solver_store_mark_roots( p->pSat ); 
 
    if ( p->fVerbose )
        printf( "The resulting SAT problem contains %d variables and %d clauses.\n", 
            p->pSat->size, p->pSat->stats.clauses );
    return RetValue;
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Aig_Gla2FetchVar()

int Aig_Gla2FetchVar	(	Aig_Gla2Man_t *	p,
		Aig_Obj_t *	pObj,
		int	k )

Function*************************************************************

Synopsis [Finds existing SAT variable or creates a new one.]

Description []

SideEffects []

SeeAlso []

Definition at line 154 of file saigGlaPba.c.

{
    int i, iVecId, iSatVar;
    assert( k < p->nFramesMax );
    iVecId = Vec_IntEntry( p->vObj2Vec, Aig_ObjId(pObj) );
    if ( iVecId == 0 )
    {
        iVecId = Vec_IntSize( p->vVec2Var ) / p->nFramesMax;
        for ( i = 0; i < p->nFramesMax; i++ )
            Vec_IntPush( p->vVec2Var, 0 );
        Vec_IntWriteEntry( p->vObj2Vec, Aig_ObjId(pObj), iVecId );
    }
    iSatVar = Vec_IntEntry( p->vVec2Var, iVecId * p->nFramesMax + k );
    if ( iSatVar == 0 )
    {
        iSatVar = Vec_IntSize( p->vVar2Inf ) / 2;
        Vec_IntPush( p->vVar2Inf, Aig_ObjId(pObj) );
        Vec_IntPush( p->vVar2Inf, k );
        Vec_IntWriteEntry( p->vVec2Var, iVecId * p->nFramesMax + k, iSatVar );
    }
    return iSatVar;
}

Here is the caller graph for this function:

◆ Aig_Gla2ManCollect()

Vec_Int_t * Aig_Gla2ManCollect	(	Aig_Gla2Man_t *	p,
		Vec_Int_t *	vCore )

Function*************************************************************

Synopsis [Collects abstracted objects.]

Description []

SideEffects []

SeeAlso []

Definition at line 454 of file saigGlaPba.c.

{
    Vec_Int_t * vResult;
    Aig_Obj_t * pObj;
    int i, ClaId, iVecId;
//    p->vVec2Use = Vec_IntStart( Vec_IntSize(p->vVec2Var) );
 
    vResult = Vec_IntStart( Aig_ManObjNumMax(p->pAig) );
    Vec_IntWriteEntry( vResult, 0, 1 ); // add const1
    Vec_IntForEachEntry( vCore, ClaId, i )
    {
        pObj = Aig_ManObj( p->pAig, Vec_IntEntry(p->vCla2Obj, ClaId) );
        if ( Saig_ObjIsPi(p->pAig, pObj) || Saig_ObjIsPo(p->pAig, pObj) || Aig_ObjIsConst1(pObj) )
            continue;
        assert( Saig_ObjIsLo(p->pAig, pObj) || Aig_ObjIsNode(pObj) );
        Vec_IntWriteEntry( vResult, Aig_ObjId(pObj), 1 );
/*
        // add flop inputs with multiple fanouts
        if ( Saig_ObjIsLo(p->pAig, pObj) )
        {
            Aig_Obj_t * pObjLi = Saig_ObjLoToLi(p->pAig, pObj);
            if ( !Saig_ObjIsPi(p->pAig, Aig_ObjFanin0(pObjLi)) )
//            if ( Aig_ObjRefs( Aig_ObjFanin0(pObjLi) ) > 1 )
                Vec_IntWriteEntry( vResult, Aig_ObjFaninId0(pObjLi), 1 );
        }
        else
        {
            if ( !Saig_ObjIsPi(p->pAig, Aig_ObjFanin0(pObj)) )
                Vec_IntWriteEntry( vResult, Aig_ObjFaninId0(pObj), 1 );
            if ( !Saig_ObjIsPi(p->pAig, Aig_ObjFanin1(pObj)) )
                Vec_IntWriteEntry( vResult, Aig_ObjFaninId1(pObj), 1 );
        }
*/
        if ( p->vVec2Use )
        {
            iVecId = Vec_IntEntry( p->vObj2Vec, Aig_ObjId(pObj) );
            Vec_IntWriteEntry( p->vVec2Use, iVecId * p->nFramesMax + Vec_IntEntry(p->vCla2Fra, ClaId), 1 );
        }
    }
//    printf( "Number of entries %d\n", Vec_IntCountPositive(vResult) );
 
    // count the number of objects in each frame
    if ( p->vVec2Use )
    {
        Vec_Int_t * vCounts = Vec_IntStart( p->nFramesMax );
        int v, f, Entry, nVecIds = Vec_IntSize(p->vVec2Use) / p->nFramesMax;
        for ( f = 0; f < p->nFramesMax; f++ )
        for ( v = 0; v < nVecIds; v++ )
            if ( Vec_IntEntry( p->vVec2Use, v * p->nFramesMax + f ) )
                Vec_IntAddToEntry( vCounts, f, 1 );
        Vec_IntForEachEntry( vCounts, Entry, f )
            printf( "%d ", Entry );
        printf( "\n" );
        Vec_IntFree( vCounts );
    }
    return vResult;
}

Here is the caller graph for this function:

◆ Aig_Gla2ManPerform()

Vec_Int_t * Aig_Gla2ManPerform	(	Aig_Man_t *	pAig,
		int	nStart,
		int	nFramesMax,
		int	nConfLimit,
		int	TimeLimit,
		int	fSkipRand,
		int	fVerbose )

Function*************************************************************

Synopsis [Performs gate-level localization abstraction.]

Description [Returns array of objects included in the abstraction. This array may contain only const1, flop outputs, and internal nodes, that is, objects that should have clauses added to the SAT solver.]

SideEffects []

SeeAlso []

Definition at line 525 of file saigGlaPba.c.

{
    Aig_Gla2Man_t * p;
    Vec_Int_t * vCore, * vResult;
    clock_t nTimeToStop = TimeLimit ? TimeLimit * CLOCKS_PER_SEC + clock(): 0;
    clock_t clk, clk2 = clock();
    assert( Saig_ManPoNum(pAig) == 1 );
 
    if ( fVerbose )
    {
        if ( TimeLimit )
            printf( "Abstracting from frame %d to frame %d with timeout %d sec.\n", nStart, nFramesMax, TimeLimit );
        else
            printf( "Abstracting from frame %d to frame %d with no timeout.\n", nStart, nFramesMax );
    }
 
    // start the solver
    clk = clock();
    p = Aig_Gla2ManStart( pAig, nStart, nFramesMax, fVerbose );
    if ( !Aig_Gla2CreateSatSolver( p ) )
    {
        printf( "Error!  SAT solver became UNSAT.\n" );
        Aig_Gla2ManStop( p );
        return NULL;
    }
    sat_solver_set_random( p->pSat, fSkipRand );
    p->timePre += clock() - clk;
 
    // set runtime limit
    if ( TimeLimit )
        sat_solver_set_runtime_limit( p->pSat, nTimeToStop );
 
    // compute UNSAT core
    clk = clock();
    vCore = Saig_AbsSolverUnsatCore( p->pSat, nConfLimit, fVerbose, NULL );
    if ( vCore == NULL )
    {
        Aig_Gla2ManStop( p );
        return NULL;
    }
    p->timeSat += clock() - clk;
    p->timeTotal += clock() - clk2;
 
    // print stats
    if ( fVerbose )
    {
        ABC_PRTP( "Pre   ", p->timePre,   p->timeTotal );
        ABC_PRTP( "Sat   ", p->timeSat,   p->timeTotal );
        ABC_PRTP( "Total ", p->timeTotal, p->timeTotal );
    }
 
    // prepare return value
    vResult = Aig_Gla2ManCollect( p, vCore );
    Vec_IntFree( vCore );
    Aig_Gla2ManStop( p );
    return vResult;
}

Here is the call graph for this function:

◆ Aig_Gla2ManStart()

Aig_Gla2Man_t * Aig_Gla2ManStart	(	Aig_Man_t *	pAig,
		int	nStart,
		int	nFramesMax,
		int	fVerbose )

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 335 of file saigGlaPba.c.

{
    Aig_Gla2Man_t * p;
    int i;
 
    p = ABC_CALLOC( Aig_Gla2Man_t, 1 );
    p->pAig       = pAig;
 
    p->vObj2Vec   = Vec_IntStart( Aig_ManObjNumMax(pAig) );
    p->vVec2Var   = Vec_IntAlloc( 1 << 20 );
    p->vVar2Inf   = Vec_IntAlloc( 1 << 20 );
    p->vCla2Obj   = Vec_IntAlloc( 1 << 20 );
    p->vCla2Fra   = Vec_IntAlloc( 1 << 20 );
 
    // skip first vector ID
    p->nStart     = nStart;
    p->nFramesMax = nFramesMax;
    p->fVerbose   = fVerbose;
    for ( i = 0; i < p->nFramesMax; i++ )
        Vec_IntPush( p->vVec2Var, -1 );
 
    // skip  first SAT variable
    Vec_IntPush( p->vVar2Inf, -1 );
    Vec_IntPush( p->vVar2Inf, -1 );
    return p;
}

Here is the caller graph for this function:

◆ Aig_Gla2ManStop()

void Aig_Gla2ManStop ( Aig_Gla2Man_t * p )

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 373 of file saigGlaPba.c.

{
    Vec_IntFreeP( &p->vObj2Vec );
    Vec_IntFreeP( &p->vVec2Var );
    Vec_IntFreeP( &p->vVar2Inf );
    Vec_IntFreeP( &p->vCla2Obj );
    Vec_IntFreeP( &p->vCla2Fra );
    Vec_IntFreeP( &p->vVec2Use );
 
    if ( p->pSat )
        sat_solver_delete( p->pSat );
    ABC_FREE( p );
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Saig_AbsSolverUnsatCore()

Vec_Int_t * Saig_AbsSolverUnsatCore	(	sat_solver *	pSat,
		int	nConfMax,
		int	fVerbose,
		int *	piRetValue )

Function*************************************************************

Synopsis [Finds the set of clauses involved in the UNSAT core.]

Description []

SideEffects []

SeeAlso []

Definition at line 399 of file saigGlaPba.c.

{
    Vec_Int_t * vCore;
    void * pSatCnf; 
    Intp_Man_t * pManProof;
    int RetValue;
    clock_t clk = clock();
    if ( piRetValue )
        *piRetValue = -1;
    // solve the problem
    RetValue = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfMax, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
    if ( RetValue == l_Undef )
    {
        printf( "Conflict limit is reached.\n" );
        return NULL;
    }
    if ( RetValue == l_True )
    {
        printf( "The BMC problem is SAT.\n" );
        if ( piRetValue )
            *piRetValue = 0;
        return NULL;
    }
    if ( fVerbose )
    {
        printf( "SAT solver returned UNSAT after %7d conflicts.      ", (int)pSat->stats.conflicts );
        Abc_PrintTime( 1, "Time", clock() - clk );
    }
    assert( RetValue == l_False );
    pSatCnf = sat_solver_store_release( pSat ); 
    // derive the UNSAT core
    clk = clock();
    pManProof = Intp_ManAlloc();
    vCore = (Vec_Int_t *)Intp_ManUnsatCore( pManProof, (Sto_Man_t *)pSatCnf, 0, 0 );
    Intp_ManFree( pManProof );
    if ( fVerbose )
    {
        printf( "SAT core contains %8d clauses (out of %8d).   ", Vec_IntSize(vCore), sat_solver_nclauses(pSat) );
        Abc_PrintTime( 1, "Time", clock() - clk );
    }
    Sto_ManFree( (Sto_Man_t *)pSatCnf );
    return vCore;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Classes

Typedefs

Functions

Typedef Documentation

◆ Aig_Gla2Man_t

Function Documentation

◆ Aig_Gla2AssignVars_rec()

◆ Aig_Gla2CreateSatSolver()

◆ Aig_Gla2FetchVar()

◆ Aig_Gla2ManCollect()

◆ Aig_Gla2ManPerform()

◆ Aig_Gla2ManStart()

◆ Aig_Gla2ManStop()

◆ Saig_AbsSolverUnsatCore()