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
|
