summaryrefslogtreecommitdiffstats
path: root/src/sat/msat/msat.h
blob: 37e0bbeb9cc98f161af8dc4ab12de38c464b50bc (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
154
155
156
157
158
159
160
/**CFile****************************************************************

  FileName    [msat.h]

  PackageName [A C version of SAT solver MINISAT, originally developed 
  in C++ by Niklas Een and Niklas Sorensson, Chalmers University of 
  Technology, Sweden: http://www.cs.chalmers.se/~een/Satzoo.]

  Synopsis    [External definitions of the solver.]

  Author      [Alan Mishchenko <alanmi@eecs.berkeley.edu>]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - January 1, 2004.]

  Revision    [$Id: msat.h,v 1.6 2004/05/12 06:30:20 satrajit Exp $]

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

#ifndef __MSAT_H__
#define __MSAT_H__

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

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

////////////////////////////////////////////////////////////////////////
///                    STRUCTURE DEFINITIONS                         ///
////////////////////////////////////////////////////////////////////////

#ifdef bool
#undef bool
#endif

#ifndef __MVTYPES_H__
typedef int  bool;
#endif

typedef struct Msat_Solver_t_      Msat_Solver_t;

// the vector of intergers and of clauses
typedef struct Msat_IntVec_t_      Msat_IntVec_t;
typedef struct Msat_ClauseVec_t_   Msat_ClauseVec_t;
typedef struct Msat_VarHeap_t_     Msat_VarHeap_t;

// the return value of the solver
typedef enum { MSAT_FALSE = -1, MSAT_UNKNOWN = 0, MSAT_TRUE = 1 } Msat_Type_t;

// representation of variables and literals
// the literal (l) is the variable (v) and the sign (s)
// s = 0 the variable is positive
// s = 1 the variable is negative
#define MSAT_VAR2LIT(v,s) (2*(v)+(s)) 
#define MSAT_LITNOT(l)    ((l)^1)
#define MSAT_LITSIGN(l)   ((l)&1)     
#define MSAT_LIT2VAR(l)   ((l)>>1)

////////////////////////////////////////////////////////////////////////
///                       GLOBAL VARIABLES                           ///
////////////////////////////////////////////////////////////////////////

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

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

/*=== satRead.c ============================================================*/
extern bool             Msat_SolverParseDimacs( FILE * pFile, Msat_Solver_t ** p, int fVerbose );
/*=== satSolver.c ===========================================================*/
// adding vars, clauses, simplifying the database, and solving
extern bool             Msat_SolverAddVar( Msat_Solver_t * p );
extern bool             Msat_SolverAddClause( Msat_Solver_t * p, Msat_IntVec_t * pLits );
extern bool             Msat_SolverSimplifyDB( Msat_Solver_t * p );
extern bool             Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * pVecAssumps, int nBackTrackLimit, int nTimeLimit );
// printing stats, assignments, and clauses
extern void             Msat_SolverPrintStats( Msat_Solver_t * p );
extern void             Msat_SolverPrintAssignment( Msat_Solver_t * p );
extern void             Msat_SolverPrintClauses( Msat_Solver_t * p );
extern void             Msat_SolverWriteDimacs( Msat_Solver_t * p, char * pFileName );
// access to the solver internal data
extern int              Msat_SolverReadVarNum( Msat_Solver_t * p );
extern int              Msat_SolverReadVarAllocNum( Msat_Solver_t * p );
extern int *            Msat_SolverReadAssignsArray( Msat_Solver_t * p );
extern int *            Msat_SolverReadModelArray( Msat_Solver_t * p );
extern unsigned         Msat_SolverReadTruth( Msat_Solver_t * p );
extern int              Msat_SolverReadBackTracks( Msat_Solver_t * p );
extern void             Msat_SolverSetVerbosity( Msat_Solver_t * p, int fVerbose );
extern void             Msat_SolverSetProofWriting( Msat_Solver_t * p, int fProof );
extern void             Msat_SolverSetVarTypeA( Msat_Solver_t * p, int Var );
extern void             Msat_SolverSetVarMap( Msat_Solver_t * p, Msat_IntVec_t * vVarMap );
extern void             Msat_SolverMarkLastClauseTypeA( Msat_Solver_t * p );
extern void             Msat_SolverMarkClausesStart( Msat_Solver_t * p );
// returns the solution after incremental solving
extern int              Msat_SolverReadSolutions( Msat_Solver_t * p );
extern int *            Msat_SolverReadSolutionsArray( Msat_Solver_t * p );
extern Msat_ClauseVec_t *  Msat_SolverReadAdjacents( Msat_Solver_t * p );
extern Msat_IntVec_t *  Msat_SolverReadConeVars( Msat_Solver_t * p );
extern Msat_IntVec_t *  Msat_SolverReadVarsUsed( Msat_Solver_t * p );
/*=== satSolverSearch.c ===========================================================*/
extern void             Msat_SolverRemoveLearned( Msat_Solver_t * p );
extern void             Msat_SolverRemoveMarked( Msat_Solver_t * p );
/*=== satSolverApi.c ===========================================================*/
// allocation, cleaning, and freeing the solver
extern Msat_Solver_t *  Msat_SolverAlloc( int nVars, double dClaInc, double dClaDecay, double dVarInc, double dVarDecay, bool fVerbose );
extern void             Msat_SolverResize( Msat_Solver_t * pMan, int nVarsAlloc );
extern void             Msat_SolverClean( Msat_Solver_t * p, int nVars );
extern void             Msat_SolverPrepare( Msat_Solver_t * pSat, Msat_IntVec_t * vVars );
extern void             Msat_SolverFree( Msat_Solver_t * p );
/*=== satVec.c ===========================================================*/
extern Msat_IntVec_t *  Msat_IntVecAlloc( int nCap );
extern Msat_IntVec_t *  Msat_IntVecAllocArray( int * pArray, int nSize );
extern Msat_IntVec_t *  Msat_IntVecAllocArrayCopy( int * pArray, int nSize );
extern Msat_IntVec_t *  Msat_IntVecDup( Msat_IntVec_t * pVec );
extern Msat_IntVec_t *  Msat_IntVecDupArray( Msat_IntVec_t * pVec );
extern void             Msat_IntVecFree( Msat_IntVec_t * p );
extern void             Msat_IntVecFill( Msat_IntVec_t * p, int nSize, int Entry );
extern int *            Msat_IntVecReleaseArray( Msat_IntVec_t * p );
extern int *            Msat_IntVecReadArray( Msat_IntVec_t * p );
extern int              Msat_IntVecReadSize( Msat_IntVec_t * p );
extern int              Msat_IntVecReadEntry( Msat_IntVec_t * p, int i );
extern int              Msat_IntVecReadEntryLast( Msat_IntVec_t * p );
extern void             Msat_IntVecWriteEntry( Msat_IntVec_t * p, int i, int Entry );
extern void             Msat_IntVecGrow( Msat_IntVec_t * p, int nCapMin );
extern void             Msat_IntVecShrink( Msat_IntVec_t * p, int nSizeNew );
extern void             Msat_IntVecClear( Msat_IntVec_t * p );
extern void             Msat_IntVecPush( Msat_IntVec_t * p, int Entry );
extern int              Msat_IntVecPushUnique( Msat_IntVec_t * p, int Entry );
extern void             Msat_IntVecPushUniqueOrder( Msat_IntVec_t * p, int Entry, int fIncrease );
extern int              Msat_IntVecPop( Msat_IntVec_t * p );
extern void             Msat_IntVecSort( Msat_IntVec_t * p, int fReverse );
/*=== satHeap.c ===========================================================*/
extern Msat_VarHeap_t * Msat_VarHeapAlloc();
extern void             Msat_VarHeapSetActivity( Msat_VarHeap_t * p, double * pActivity );
extern void             Msat_VarHeapStart( Msat_VarHeap_t * p, int * pVars, int nVars, int nVarsAlloc );
extern void             Msat_VarHeapGrow( Msat_VarHeap_t * p, int nSize );
extern void             Msat_VarHeapStop( Msat_VarHeap_t * p );
extern void             Msat_VarHeapPrint( FILE * pFile, Msat_VarHeap_t * p );
extern void             Msat_VarHeapCheck( Msat_VarHeap_t * p );
extern void             Msat_VarHeapCheckOne( Msat_VarHeap_t * p, int iVar );
extern int              Msat_VarHeapContainsVar( Msat_VarHeap_t * p, int iVar );
extern void             Msat_VarHeapInsert( Msat_VarHeap_t * p, int iVar );  
extern void             Msat_VarHeapUpdate( Msat_VarHeap_t * p, int iVar );  
extern void             Msat_VarHeapDelete( Msat_VarHeap_t * p, int iVar );  
extern double           Msat_VarHeapReadMaxWeight( Msat_VarHeap_t * p );
extern int              Msat_VarHeapCountNodes( Msat_VarHeap_t * p, double WeightLimit );  
extern int              Msat_VarHeapReadMax( Msat_VarHeap_t * p );  
extern int              Msat_VarHeapGetMax( Msat_VarHeap_t * p );  

////////////////////////////////////////////////////////////////////////
///                       END OF FILE                                ///
////////////////////////////////////////////////////////////////////////
#endif