giaCTas2.c

Go to the documentation of this file.

/**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 $]

***********************************************************************/

#include "gia.h"

ABC_NAMESPACE_IMPL_START


////////////////////////////////////////////////////////////////////////
///                        DECLARATIONS                              ///
////////////////////////////////////////////////////////////////////////

typedef struct Tas_Par_t_ Tas_Par_t;
struct Tas_Par_t_
{
    // conflict limits
    int           nBTLimit;     // limit on the number of conflicts
    // current parameters
    int           nBTThis;      // number of conflicts
    int           nBTTotal;     // total number of conflicts
    // decision heuristics
    int           fUseHighest;  // use node with the highest ID
    // other parameters
    int           fVerbose;
};

typedef struct Tas_Sto_t_ Tas_Sto_t;
struct Tas_Sto_t_
{
    int           iCur;         // currently used
    int           nSize;        // allocated size
    char *        pBuffer;      // handles of objects stored in the queue
};

typedef struct Tas_Que_t_ Tas_Que_t;
struct Tas_Que_t_
{
    int           iHead;        // beginning of the queue
    int           iTail;        // end of the queue
    int           nSize;        // allocated size
    int *         pData;        // handles of objects stored in the queue
};

typedef struct Tas_Var_t_ Tas_Var_t;
struct Tas_Var_t_
{
    unsigned      fTerm   :  1; // terminal node
    unsigned      fVal    :  1; // current value
    unsigned      fValOld :  1; // previous value
    unsigned      fAssign :  1; // assigned status
    unsigned      fJQueue :  1; // part of J-frontier
    unsigned      fCompl0 :  1; // complemented attribute
    unsigned      fCompl1 :  1; // complemented attribute
    unsigned      fMark0  :  1; // multi-purpose mark
    unsigned      fMark1  :  1; // multi-purpose mark
    unsigned      fPhase  :  1; // polarity
    unsigned      Level   : 22; // decision level 
    int           Id;           // unique ID of this variable
    int           IdAig;        // original ID of this variable
    int           Reason0;      // reason of this variable
    int           Reason1;      // reason of this variable
    int           Diff0;        // difference for the first fanin 
    int           Diff1;        // difference for the second fanin 
    int           Watch0;       // handle of first watch
    int           Watch1;       // handle of second watch   
};

typedef struct Tas_Cls_t_ Tas_Cls_t;
struct Tas_Cls_t_
{
    int           Watch0;       // next clause to watch
    int           Watch1;       // next clause to watch
    int           pVars[0];     // variable handles
};
 
typedef struct Tas_Man_t_ Tas_Man_t;
struct Tas_Man_t_
{
    // user data
    Gia_Man_t *   pAig;         // AIG manager
    Tas_Par_t     Pars;         // parameters
    // solver data
    Tas_Sto_t *   pVars;        // variables
    Tas_Sto_t *   pClauses;     // clauses
    // state representation
    Tas_Que_t     pProp;        // propagation queue
    Tas_Que_t     pJust;        // justification queue
    Vec_Int_t *   vModel;       // satisfying assignment
    Vec_Ptr_t *   vTemp;        // temporary storage
    // SAT calls statistics
    int           nSatUnsat;    // the number of proofs
    int           nSatSat;      // the number of failure
    int           nSatUndec;    // the number of timeouts
    int           nSatTotal;    // the number of calls
    // conflicts
    int           nConfUnsat;   // conflicts in unsat problems
    int           nConfSat;     // conflicts in sat problems
    int           nConfUndec;   // conflicts in undec problems
    int           nConfTotal;   // total conflicts
    // runtime stats
    clock_t       timeSatUnsat; // unsat
    clock_t       timeSatSat;   // sat
    clock_t       timeSatUndec; // undecided
    clock_t       timeTotal;    // total runtime
};

static inline int         Tas_VarIsAssigned( Tas_Var_t * pVar )        { return pVar->fAssign;                                      }
static inline void        Tas_VarAssign( Tas_Var_t * pVar )            { assert(!pVar->fAssign); pVar->fAssign = 1;                 }
static inline void        Tas_VarUnassign( Tas_Var_t * pVar )          { assert(pVar->fAssign);  pVar->fAssign = 0; pVar->fVal = 0; }
static inline int         Tas_VarValue( Tas_Var_t * pVar )             { assert(pVar->fAssign);  return pVar->fVal;                 }
static inline void        Tas_VarSetValue( Tas_Var_t * pVar, int v )   { assert(pVar->fAssign);  pVar->fVal = v;                    }
static inline int         Tas_VarIsJust( Tas_Var_t * pVar )            { return Gia_ObjIsAnd(pVar) && !Tas_VarIsAssigned(Gia_ObjFanin0(pVar)) && !Tas_VarIsAssigned(Gia_ObjFanin1(pVar)); } 
static inline int         Tas_VarFanin0Value( Tas_Var_t * pVar )       { return !Tas_VarIsAssigned(Gia_ObjFanin0(pVar)) ? 2 : (Tas_VarValue(Gia_ObjFanin0(pVar)) ^ Gia_ObjFaninC0(pVar)); }
static inline int         Tas_VarFanin1Value( Tas_Var_t * pVar )       { return !Tas_VarIsAssigned(Gia_ObjFanin1(pVar)) ? 2 : (Tas_VarValue(Gia_ObjFanin1(pVar)) ^ Gia_ObjFaninC1(pVar)); }

static inline int         Tas_VarDecLevel( Tas_Man_t * p, Tas_Var_t * pVar )  { assert( pVar->Value != ~0 ); return Vec_IntEntry(p->vLevReas, 3*pVar->Value);          }
static inline Tas_Var_t * Tas_VarReason0( Tas_Man_t * p, Tas_Var_t * pVar )   { assert( pVar->Value != ~0 ); return pVar + Vec_IntEntry(p->vLevReas, 3*pVar->Value+1); }
static inline Tas_Var_t * Tas_VarReason1( Tas_Man_t * p, Tas_Var_t * pVar )   { assert( pVar->Value != ~0 ); return pVar + Vec_IntEntry(p->vLevReas, 3*pVar->Value+2); }
static inline int         Tas_ClauseDecLevel( Tas_Man_t * p, int hClause )    { return Tas_VarDecLevel( p, p->pClauses.pData[hClause] );                               }

static inline Tas_Var_t * Tas_ManVar( Tas_Man_t * p, int h )           { return (Tas_Var_t *)(p->pVars->pBuffer + h);               }
static inline Tas_Cls_t * Tas_ManClause( Tas_Man_t * p, int h )        { return (Tas_Cls_t *)(p->pClauses->pBuffer + h);            }

#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++]) )


////////////////////////////////////////////////////////////////////////
///                     FUNCTION DEFINITIONS                         ///
////////////////////////////////////////////////////////////////////////

/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Tas_Var_t * Tas_ManCreateVar( Tas_Man_t * p )
{
    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;
}

/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Tas_Var_t * Tas_ManObj2Var( Tas_Man_t * p, Gia_Obj_t * pObj )
{
    Tas_Var_t * pVar;
    assert( !Gia_ObjIsComplement(pObj) );
    if ( pObj->Value == 0 )
    {
        pVar = Tas_ManCreateVar( p );
        pVar->

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

////////////////////////////////////////////////////////////////////////
///                       END OF FILE                                ///
////////////////////////////////////////////////////////////////////////


ABC_NAMESPACE_IMPL_END