summaryrefslogtreecommitdiffstats
path: root/src/sat/bsat/satStore.h
blob: 027afcb401a51f92314c45e44c8622f113314bec (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
/**CFile****************************************************************

  FileName    [satStore.h]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Proof recording.]

  Synopsis    [External declarations.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

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

  Revision    [$Id: pr.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]

***********************************************************************/
 
#ifndef __SAT_STORE_H__
#define __SAT_STORE_H__

#include "satSolver.h"

/*
    The trace of SAT solving contains the original clauses 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))

////////////////////////////////////////////////////////////////////////
///                          INCLUDES                                ///
////////////////////////////////////////////////////////////////////////

////////////////////////////////////////////////////////////////////////
///                         PARAMETERS                               ///
////////////////////////////////////////////////////////////////////////

////////////////////////////////////////////////////////////////////////
///                         BASIC TYPES                              ///
////////////////////////////////////////////////////////////////////////

/*
typedef unsigned lit;
// 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;                  }
*/

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
};

// 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 )

////////////////////////////////////////////////////////////////////////
///                      MACRO DEFINITIONS                           ///
////////////////////////////////////////////////////////////////////////

////////////////////////////////////////////////////////////////////////
///                    FUNCTION DECLARATIONS                         ///
////////////////////////////////////////////////////////////////////////

/*=== 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();
extern int *        Int_ManSetGlobalVars( Int_Man_t * p, int nGloVars );
extern void         Int_ManFree( Int_Man_t * p );
extern int          Int_ManInterpolate( Int_Man_t * p, Sto_Man_t * pCnf, int fVerbose, unsigned ** ppResult );

/*=== satInterA.c ==========================================================*/
typedef struct Inta_Man_t_ Inta_Man_t;
extern Inta_Man_t * Inta_ManAlloc();
extern void         Inta_ManFree( Inta_Man_t * p );
extern void *       Inta_ManInterpolate( Inta_Man_t * p, Sto_Man_t * pCnf, void * vVarsAB, int fVerbose );

/*=== satInterP.c ==========================================================*/
typedef struct Intp_Man_t_ Intp_Man_t;
extern Intp_Man_t * Intp_ManAlloc();
extern void         Intp_ManFree( Intp_Man_t * p );
extern void *       Intp_ManUnsatCore( Intp_Man_t * p, Sto_Man_t * pCnf, int fVerbose );

#ifdef __cplusplus
}
#endif

#endif

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