giaCSatP.h File Reference

#include "gia.h"

Include dependency graph for giaCSatP.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes
struct	CbsP_Par_t_
struct	CbsP_Que_t_
struct	CbsP_Man_t_

Macros
#define	CBS_UNSAT   1
#define	CBS_SAT   0
#define	CBS_UNDEC   -1

Typedefs
typedef typedefABC_NAMESPACE_HEADER_START struct CbsP_Par_t_	CbsP_Par_t
	INCLUDES ///.
typedef struct CbsP_Que_t_	CbsP_Que_t
typedef struct CbsP_Man_t_	CbsP_Man_t

Functions
CbsP_Man_t *	CbsP_ManAlloc (Gia_Man_t *pGia)
void	CbsP_ManStop (CbsP_Man_t *p)
void	CbsP_ManSatPrintStats (CbsP_Man_t *p)
void	CbsP_PrintRecord (CbsP_Par_t *pPars)
int	CbsP_ManSolve2 (CbsP_Man_t *p, Gia_Obj_t *pObj, Gia_Obj_t *pObj2)

Macro Definition Documentation

CBS_SAT

#define CBS_SAT   0

Definition at line 111 of file giaCSatP.h.

CBS_UNDEC

#define CBS_UNDEC   -1

Definition at line 112 of file giaCSatP.h.

CBS_UNSAT

#define CBS_UNSAT   1

Definition at line 110 of file giaCSatP.h.

Typedef Documentation

CbsP_Man_t

typedef struct CbsP_Man_t_ CbsP_Man_t

Definition at line 75 of file giaCSatP.h.

CbsP_Par_t

typedef typedefABC_NAMESPACE_HEADER_START struct CbsP_Par_t_ CbsP_Par_t

INCLUDES ///.

PARAMETERS ///

Definition at line 19 of file giaCSatP.h.

CbsP_Que_t

typedef struct CbsP_Que_t_ CbsP_Que_t

Definition at line 66 of file giaCSatP.h.

Function Documentation

CbsP_ManAlloc()

CbsP_Man_t * CbsP_ManAlloc

(

Gia_Man_t *

pGia

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 173 of file giaCSatP.c.

{
    CbsP_Man_t * p;
    p = ABC_CALLOC( CbsP_Man_t, 1 );
    p->pProp.nSize = p->pJust.nSize = p->pClauses.nSize = 10000;
    p->pProp.pData = ABC_ALLOC( Gia_Obj_t *, p->pProp.nSize );
    p->pJust.pData = ABC_ALLOC( Gia_Obj_t *, p->pJust.nSize );
    p->pClauses.pData = ABC_ALLOC( Gia_Obj_t *, p->pClauses.nSize );
    p->pClauses.iHead = p->pClauses.iTail = 1;
    p->vModel   = Vec_IntAlloc( 1000 );
    p->vLevReas = Vec_IntAlloc( 1000 );
    p->vTemp    = Vec_PtrAlloc( 1000 );
    p->pAig     = pGia;
    p->vValue   = Vec_IntAlloc( Gia_ManObjNum(pGia) );
    Vec_IntFill( p->vValue, Gia_ManObjNum(pGia), ~0 );
    //memset( p->vValue->pArray, (unsigned) ~0, sizeof(int) * Gia_ManObjNum(pGia) );
    CbsP_SetDefaultParams( &p->Pars );
    return p;
}

Here is the call graph for this function:

Here is the caller graph for this function:

CbsP_ManSatPrintStats()

void CbsP_ManSatPrintStats

(

CbsP_Man_t *

p

)

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

Synopsis [Prints statistics of the manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 1073 of file giaCSatP.c.

{
    printf( "CO = %8d  ", Gia_ManCoNum(p->pAig) );
    printf( "AND = %8d  ", Gia_ManAndNum(p->pAig) );
    printf( "Conf = %6d  ", p->Pars.nBTLimit );
    printf( "JustMax = %5d  ", p->Pars.nJustLimit );
    printf( "\n" );
    printf( "Unsat calls %6d  (%6.2f %%)   Ave conf = %8.1f   ", 
        p->nSatUnsat, p->nSatTotal? 100.0*p->nSatUnsat/p->nSatTotal :0.0, p->nSatUnsat? 1.0*p->nConfUnsat/p->nSatUnsat :0.0 );
    ABC_PRTP( "Time", p->timeSatUnsat, p->timeTotal );
    printf( "Sat   calls %6d  (%6.2f %%)   Ave conf = %8.1f   ", 
        p->nSatSat,   p->nSatTotal? 100.0*p->nSatSat/p->nSatTotal :0.0, p->nSatSat? 1.0*p->nConfSat/p->nSatSat : 0.0 );
    ABC_PRTP( "Time", p->timeSatSat,   p->timeTotal );
    printf( "Undef calls %6d  (%6.2f %%)   Ave conf = %8.1f   ", 
        p->nSatUndec, p->nSatTotal? 100.0*p->nSatUndec/p->nSatTotal :0.0, p->nSatUndec? 1.0*p->nConfUndec/p->nSatUndec : 0.0 );
    ABC_PRTP( "Time", p->timeSatUndec, p->timeTotal );
    ABC_PRT( "Total time", p->timeTotal );
}

Here is the caller graph for this function:

CbsP_ManSolve2()

int CbsP_ManSolve2	(	CbsP_Man_t *	p,
		Gia_Obj_t *	pObj,
		Gia_Obj_t *	pObj2 )

Definition at line 1017 of file giaCSatP.c.

{
    abctime clk = Abc_Clock();
    int RetValue = 0;
//    s_Counter = 0;
    assert( !p->pProp.iHead && !p->pProp.iTail );
    assert( !p->pJust.iHead && !p->pJust.iTail );
    assert( p->pClauses.iHead == 1 && p->pClauses.iTail == 1 );
    p->Pars.nBTThis = p->Pars.nJustThis = p->Pars.nBTThisNc = 0;
    p->Pars.nJscanThis = p->Pars.nRscanThis = p->Pars.nPropThis = 0;
    CbsP_ManAssign( p, pObj, 0, NULL, NULL );
    if ( pObj2 ) 
    CbsP_ManAssign( p, pObj2, 0, NULL, NULL );
    if ( !CbsP_ManSolve_rec(p, 0) && !CbsP_ManCheckLimits(p) )
        CbsP_ManSaveModel( p, p->vModel );
    else 
        RetValue = 1;
    CbsP_ManCancelUntil( p, 0 );
 
    p->pJust.iHead = p->pJust.iTail = 0;
    p->pClauses.iHead = p->pClauses.iTail = 1;
    p->Pars.nBTTotal += p->Pars.nBTThis;
    p->Pars.nJustTotal = Abc_MaxInt( p->Pars.nJustTotal, p->Pars.nJustThis );
    if ( CbsP_ManCheckLimits( p ) )
        RetValue = -1;
 
    if( CBS_SAT == RetValue ){
        p->nSatSat ++;
        p->timeSatSat   += Abc_Clock() - clk;
        p->nConfSat     += p->Pars.nBTThis;
    } else
    if( CBS_UNSAT == RetValue ){
        p->nSatUnsat ++;
        p->timeSatUnsat += Abc_Clock() - clk;
        p->nConfUnsat   += p->Pars.nBTThis;
    } else {
        p->nSatUndec ++;
        p->timeSatUndec += Abc_Clock() - clk;
        p->nConfUndec   += p->Pars.nBTThis;
    }
//    printf( "%d ", s_Counter );
    CbsP_UpdateRecord(&p->Pars,RetValue);
    return RetValue;
}

Here is the call graph for this function:

Here is the caller graph for this function:

CbsP_ManStop()

void CbsP_ManStop

(

CbsP_Man_t *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 204 of file giaCSatP.c.

{
    Vec_IntFree( p->vLevReas );
    Vec_IntFree( p->vModel );
    Vec_PtrFree( p->vTemp );
    Vec_IntFree( p->vValue );
    ABC_FREE( p->pClauses.pData );
    ABC_FREE( p->pProp.pData );
    ABC_FREE( p->pJust.pData );
    ABC_FREE( p );
}

Here is the caller graph for this function:

CbsP_PrintRecord()

void CbsP_PrintRecord

(

CbsP_Par_t *

pPars

)

Definition at line 148 of file giaCSatP.c.

                                           {
    printf("max of solved: jscan# %13d rscan %13d prop %13d\n"   , pPars->maxJscanSolved, pPars->maxRscanSolved , pPars->maxPropSolved );
    printf("max of  undec: jscan# %13d rscan %13d prop %13d\n"   , pPars->maxJscanUndec , pPars->maxRscanUndec  , pPars->maxPropUndec  );
    printf("acc of    sat: jscan# %13ld rscan %13ld prop %13ld\n", pPars->accJscanSat   , pPars->accRscanSat    , pPars->accPropSat    );
    printf("acc of  unsat: jscan# %13ld rscan %13ld prop %13ld\n", pPars->accJscanUnsat , pPars->accRscanUnsat  , pPars->accPropUnsat  );
    printf("acc of  undec: jscan# %13ld rscan %13ld prop %13ld\n", pPars->accJscanUndec , pPars->accRscanUndec  , pPars->accPropUndec  );
    if( pPars->nSat )
        printf("avg of    sat: jscan# %13ld rscan %13ld prop %13ld\n", pPars->accJscanSat   / pPars->nSat   , pPars->accRscanSat   / pPars->nSat   , pPars->accPropSat   / pPars->nSat   );
    if( pPars->nUnsat )
        printf("avg of  unsat: jscan# %13ld rscan %13ld prop %13ld\n", pPars->accJscanUnsat / pPars->nUnsat , pPars->accRscanUnsat / pPars->nUnsat , pPars->accPropUnsat / pPars->nUnsat );
    if( pPars->nUndec )
        printf("avg of  undec: jscan# %13ld rscan %13ld prop %13ld\n", pPars->accJscanUndec / pPars->nUndec , pPars->accRscanUndec / pPars->nUndec , pPars->accPropUndec / pPars->nUndec );
}

Here is the caller graph for this function: