giaCTas2.c File Reference

#include "gia.h"

Go to the source code of this file.

Data Structures
struct	Tas_Par_t_
struct	Tas_Sto_t_
struct	Tas_Que_t_
struct	Tas_Var_t_
struct	Tas_Cls_t_
struct	Tas_Man_t_

Macros
#define	Tas_ClaForEachVar(p, pClause, pVar, i)   for ( pVar = Tas_ManVar(p, pClause->pVars[(i=0)]); pClause->pVars[i]; pVar = (Tas_Var_t *)(((char *)pVar + pClause->pVars[++i])) )
#define	Tas_QueForEachVar(p, pQue, pVar, i)   for ( pVar = Tas_ManVar(p, pQue->pVars[(i=pQue->iHead)]); i < pQue->iTail; pVar = Tas_ManVar(p, pQue->pVars[i++]) )

Typedefs
typedef typedefABC_NAMESPACE_IMPL_START struct Tas_Par_t_	Tas_Par_t
	DECLARATIONS ///. More...
typedef struct Tas_Sto_t_	Tas_Sto_t
typedef struct Tas_Que_t_	Tas_Que_t
typedef struct Tas_Var_t_	Tas_Var_t
typedef struct Tas_Cls_t_	Tas_Cls_t
typedef struct Tas_Man_t_	Tas_Man_t

Functions
static int	Tas_VarIsAssigned (Tas_Var_t *pVar)
static void	Tas_VarAssign (Tas_Var_t *pVar)
static void	Tas_VarUnassign (Tas_Var_t *pVar)
static int	Tas_VarValue (Tas_Var_t *pVar)
static void	Tas_VarSetValue (Tas_Var_t *pVar, int v)
static int	Tas_VarIsJust (Tas_Var_t *pVar)
static int	Tas_VarFanin0Value (Tas_Var_t *pVar)
static int	Tas_VarFanin1Value (Tas_Var_t *pVar)
static int	Tas_VarDecLevel (Tas_Man_t *p, Tas_Var_t *pVar)
static Tas_Var_t *	Tas_VarReason0 (Tas_Man_t *p, Tas_Var_t *pVar)
static Tas_Var_t *	Tas_VarReason1 (Tas_Man_t *p, Tas_Var_t *pVar)
static int	Tas_ClauseDecLevel (Tas_Man_t *p, int hClause)
static Tas_Var_t *	Tas_ManVar (Tas_Man_t *p, int h)
static Tas_Cls_t *	Tas_ManClause (Tas_Man_t *p, int h)
Tas_Var_t *	Tas_ManCreateVar (Tas_Man_t *p)
	FUNCTION DEFINITIONS ///. More...
Tas_Var_t *	Tas_ManObj2Var (Tas_Man_t *p, Gia_Obj_t *pObj)

Macro Definition Documentation

#define Tas_ClaForEachVar	(		p,
			pClause,
			pVar,
			i
	)		for ( pVar = Tas_ManVar(p, pClause->pVars[(i=0)]); pClause->pVars[i]; pVar = (Tas_Var_t *)(((char *)pVar + pClause->pVars[++i])) )

Definition at line 141 of file giaCTas2.c.

#define Tas_QueForEachVar	(		p,
			pQue,
			pVar,
			i
	)		for ( pVar = Tas_ManVar(p, pQue->pVars[(i=pQue->iHead)]); i < pQue->iTail; pVar = Tas_ManVar(p, pQue->pVars[i++]) )

Definition at line 144 of file giaCTas2.c.

Typedef Documentation

typedef struct Tas_Cls_t_ Tas_Cls_t

Definition at line 85 of file giaCTas2.c.

typedef struct Tas_Man_t_ Tas_Man_t

Definition at line 93 of file giaCTas2.c.

typedef typedefABC_NAMESPACE_IMPL_START struct Tas_Par_t_ Tas_Par_t

DECLARATIONS ///.

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

FileName [giaCSat2.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Scalable AIG package.]

Synopsis [Circuit-based SAT solver.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id:

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

]

Definition at line 30 of file giaCTas2.c.

typedef struct Tas_Que_t_ Tas_Que_t

Definition at line 52 of file giaCTas2.c.

typedef struct Tas_Sto_t_ Tas_Sto_t

Definition at line 44 of file giaCTas2.c.

typedef struct Tas_Var_t_ Tas_Var_t

Definition at line 61 of file giaCTas2.c.

Function Documentation

static int Tas_ClauseDecLevel ( Tas_Man_t *  p, int  hClause  )

inlinestatic

Definition at line 136 of file giaCTas2.c.

{ return Tas_VarDecLevel( p, p->pClauses.pData[hClause] );                               }

static Tas_Cls_t* Tas_ManClause ( Tas_Man_t *  p, int  h  )

inlinestatic

Definition at line 139 of file giaCTas2.c.

{ return (Tas_Cls_t *)(p->pClauses->pBuffer + h);            }

Tas_Var_t* Tas_ManCreateVar

(

Tas_Man_t *

p

)

FUNCTION DEFINITIONS ///.

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 163 of file giaCTas2.c.

{
    Tas_Var_t * pVar;
    if ( p->pVars->iCur + sizeof(Tas_Var_t) > p->pVars->nSize )
    {
        p->pVars->nSize *= 2;
        p->pVars->pData = ABC_REALLOC( char, p->pVars->pData, p->pVars->nSize ); 
    }
    pVar = p->pVars->pData + p->pVars->iCur;
    p->pVars->iCur += sizeof(Tas_Var_t);
    memset( pVar, 0, sizeof(Tas_Var_t) );
    pVar->Id = pVar - ((Tas_Var_t *)p->pVars->pData);
    return pVar;
}

Tas_Var_t* Tas_ManObj2Var	(	Tas_Man_t *	p,
		Gia_Obj_t *	pObj
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 189 of file giaCTas2.c.

{
    Tas_Var_t * pVar;
    assert( !Gia_ObjIsComplement(pObj) );
    if ( pObj->Value == 0 )
    {
        pVar = Tas_ManCreateVar( p );
        pVar->

    }
    return Tas_ManVar( p, pObj->Value );
}

static Tas_Var_t* Tas_ManVar ( Tas_Man_t *  p, int  h  )

inlinestatic

Definition at line 138 of file giaCTas2.c.

{ return (Tas_Var_t *)(p->pVars->pBuffer + h);               }

static void Tas_VarAssign ( Tas_Var_t *  pVar )

inlinestatic

Definition at line 125 of file giaCTas2.c.

{ assert(!pVar->fAssign); pVar->fAssign = 1;                 }

static int Tas_VarDecLevel ( Tas_Man_t *  p, Tas_Var_t *  pVar  )

inlinestatic

Definition at line 133 of file giaCTas2.c.

{ assert( pVar->Value != ~0 ); return Vec_IntEntry(p->vLevReas, 3*pVar->Value);          }

static int Tas_VarFanin0Value ( Tas_Var_t *  pVar )

inlinestatic

Definition at line 130 of file giaCTas2.c.

{ return !Tas_VarIsAssigned(Gia_ObjFanin0(pVar)) ? 2 : (Tas_VarValue(Gia_ObjFanin0(pVar)) ^ Gia_ObjFaninC0(pVar)); }

static int Tas_VarFanin1Value ( Tas_Var_t *  pVar )

inlinestatic

Definition at line 131 of file giaCTas2.c.

{ return !Tas_VarIsAssigned(Gia_ObjFanin1(pVar)) ? 2 : (Tas_VarValue(Gia_ObjFanin1(pVar)) ^ Gia_ObjFaninC1(pVar)); }

static int Tas_VarIsAssigned ( Tas_Var_t *  pVar )

inlinestatic

Definition at line 124 of file giaCTas2.c.

{ return pVar->fAssign;                                      }

static int Tas_VarIsJust ( Tas_Var_t *  pVar )

inlinestatic

Definition at line 129 of file giaCTas2.c.

{ return Gia_ObjIsAnd(pVar) && !Tas_VarIsAssigned(Gia_ObjFanin0(pVar)) && !Tas_VarIsAssigned(Gia_ObjFanin1(pVar)); } 

static Tas_Var_t* Tas_VarReason0 ( Tas_Man_t *  p, Tas_Var_t *  pVar  )

inlinestatic

Definition at line 134 of file giaCTas2.c.

{ assert( pVar->Value != ~0 ); return pVar + Vec_IntEntry(p->vLevReas, 3*pVar->Value+1); }

static Tas_Var_t* Tas_VarReason1 ( Tas_Man_t *  p, Tas_Var_t *  pVar  )

inlinestatic

Definition at line 135 of file giaCTas2.c.

{ assert( pVar->Value != ~0 ); return pVar + Vec_IntEntry(p->vLevReas, 3*pVar->Value+2); }

static void Tas_VarSetValue ( Tas_Var_t *  pVar, int  v  )

inlinestatic

Definition at line 128 of file giaCTas2.c.

{ assert(pVar->fAssign);  pVar->fVal = v;                    }

static void Tas_VarUnassign ( Tas_Var_t *  pVar )

inlinestatic

Definition at line 126 of file giaCTas2.c.

{ assert(pVar->fAssign);  pVar->fAssign = 0; pVar->fVal = 0; }

static int Tas_VarValue ( Tas_Var_t *  pVar )

inlinestatic

Definition at line 127 of file giaCTas2.c.

{ assert(pVar->fAssign);  return pVar->fVal;                 }