src/sat/bsat/satStore.h

Go to the documentation of this file.

#ifndef __PR_H__
#define __PR_H__

/*
    The trace of SAT solving contains the original clause of the problem
    along with the learned clauses derived during SAT solving.
    The first line of the resulting file contains 3 numbers instead of 2:
    c <num_vars> <num_all_clauses> <num_root_clauses>
*/

#ifdef __cplusplus
extern "C" {
#endif

#ifdef _WIN32
#define inline __inline // compatible with MS VS 6.0
#endif

#ifndef PRT
#define PRT(a,t)  printf("%s = ", (a)); printf("%6.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC))
#endif

#define STO_MAX(a,b)  ((a) > (b) ? (a) : (b))




typedef unsigned lit;

typedef struct Sto_Cls_t_ Sto_Cls_t;
struct Sto_Cls_t_
{
    Sto_Cls_t *     pNext;        // the next clause
    Sto_Cls_t *     pNext0;       // the next 0-watch
    Sto_Cls_t *     pNext1;       // the next 0-watch
    int             Id;           // the clause ID
    unsigned        fA     :  1;  // belongs to A
    unsigned        fRoot  :  1;  // original clause
    unsigned        fVisit :  1;  // visited clause
    unsigned        nLits  : 24;  // the number of literals
    lit             pLits[0];     // literals of this clause
};

typedef struct Sto_Man_t_ Sto_Man_t;
struct Sto_Man_t_
{
    // general data
    int             nVars;        // the number of variables
    int             nRoots;       // the number of root clauses
    int             nClauses;     // the number of all clauses
    int             nClausesA;    // the number of clauses of A 
    Sto_Cls_t *     pHead;        // the head clause
    Sto_Cls_t *     pTail;        // the tail clause
    Sto_Cls_t *     pEmpty;       // the empty clause
    // memory management
    int             nChunkSize;   // the number of bytes in a chunk
    int             nChunkUsed;   // the number of bytes used in the last chunk
    char *          pChunkLast;   // the last memory chunk
};

// variable/literal conversions (taken from MiniSat)
static inline lit   toLit    (int v)        { return v + v;  }
static inline lit   toLitCond(int v, int c) { return v + v + (c != 0); }
static inline lit   lit_neg  (lit l)        { return l ^ 1;  }
static inline int   lit_var  (lit l)        { return l >> 1; }
static inline int   lit_sign (lit l)        { return l & 1;  }
static inline int   lit_print(lit l)        { return lit_sign(l)? -lit_var(l)-1 : lit_var(l)+1; }
static inline lit   lit_read (int s)        { return s > 0 ? toLit(s-1) : lit_neg(toLit(-s-1)); }
static inline int   lit_check(lit l, int n) { return l >= 0 && lit_var(l) < n;                  }

// iterators through the clauses
#define Sto_ManForEachClause( p, pCls )      for( pCls = p->pHead; pCls; pCls = pCls->pNext )
#define Sto_ManForEachClauseRoot( p, pCls )  for( pCls = p->pHead; pCls && pCls->fRoot; pCls = pCls->pNext )



/*=== satStore.c ==========================================================*/
extern Sto_Man_t *  Sto_ManAlloc();
extern void         Sto_ManFree( Sto_Man_t * p );
extern int          Sto_ManAddClause( Sto_Man_t * p, lit * pBeg, lit * pEnd );
extern int          Sto_ManMemoryReport( Sto_Man_t * p );
extern void         Sto_ManMarkRoots( Sto_Man_t * p );
extern void         Sto_ManMarkClausesA( Sto_Man_t * p );
extern void         Sto_ManDumpClauses( Sto_Man_t * p, char * pFileName );
extern Sto_Man_t *  Sto_ManLoadClauses( char * pFileName );

/*=== satInter.c ==========================================================*/
typedef struct Int_Man_t_ Int_Man_t;
extern Int_Man_t *  Int_ManAlloc( int nVarsAlloc );
extern void         Int_ManFree( Int_Man_t * p );
extern int          Int_ManInterpolate( Int_Man_t * p, Sto_Man_t * pCnf, int fVerbose, unsigned ** ppResult );

#ifdef __cplusplus
}
#endif

#endif

---