abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
msatInt.h
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [msatInt.c]
4 
5  PackageName [A C version of SAT solver MINISAT, originally developed
6  in C++ by Niklas Een and Niklas Sorensson, Chalmers University of
7  Technology, Sweden: http://www.cs.chalmers.se/~een/Satzoo.]
8 
9  Synopsis [Internal definitions of the solver.]
10 
11  Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - January 1, 2004.]
16 
17  Revision [$Id: msatInt.c,v 1.0 2004/01/01 1:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #ifndef ABC__sat__msat__msatInt_h
22 #define ABC__sat__msat__msatInt_h
23 
24 
25 ////////////////////////////////////////////////////////////////////////
26 /// INCLUDES ///
27 ////////////////////////////////////////////////////////////////////////
28 
29 #include <stdio.h>
30 #include <stdlib.h>
31 #include <string.h>
32 #include <assert.h>
33 #include <math.h>
34 
35 #include "misc/util/abc_global.h"
36 #include "msat.h"
37 
39 
40 
41 ////////////////////////////////////////////////////////////////////////
42 /// PARAMETERS ///
43 ////////////////////////////////////////////////////////////////////////
44 
45 ////////////////////////////////////////////////////////////////////////
46 /// STRUCTURE DEFINITIONS ///
47 ////////////////////////////////////////////////////////////////////////
48 
49 // By default, custom memory management is used
50 // which guarantees constant time allocation/deallocation
51 // for SAT clauses and other frequently modified objects.
52 // For debugging, it is possible use system memory management
53 // directly. In which case, uncomment the macro below.
54 //#define USE_SYSTEM_MEMORY_MANAGEMENT
55 
56 // internal data structures
58 typedef struct Msat_Queue_t_ Msat_Queue_t;
59 typedef struct Msat_Order_t_ Msat_Order_t;
60 // memory managers (duplicated from Extra for stand-aloneness)
62 typedef struct Msat_MmFlex_t_ Msat_MmFlex_t;
63 typedef struct Msat_MmStep_t_ Msat_MmStep_t;
64 // variables and literals
65 typedef int Msat_Lit_t;
66 typedef int Msat_Var_t;
67 // the type of return value
68 #define MSAT_VAR_UNASSIGNED (-1)
69 #define MSAT_LIT_UNASSIGNED (-2)
70 #define MSAT_ORDER_UNKNOWN (-3)
71 
72 // printing the search tree
73 #define L_IND "%-*d"
74 #define L_ind Msat_SolverReadDecisionLevel(p)*3+3,Msat_SolverReadDecisionLevel(p)
75 #define L_LIT "%s%d"
76 #define L_lit(Lit) MSAT_LITSIGN(Lit)?"-":"", MSAT_LIT2VAR(Lit)+1
77 
80 {
81  ABC_INT64_T nStarts; // the number of restarts
82  ABC_INT64_T nDecisions; // the number of decisions
83  ABC_INT64_T nPropagations; // the number of implications
84  ABC_INT64_T nInspects; // the number of times clauses are vising while watching them
85  ABC_INT64_T nConflicts; // the number of conflicts
86  ABC_INT64_T nSuccesses; // the number of sat assignments found
87 };
88 
91 {
92  double dVarDecay;
93  double dClaDecay;
94 };
95 
96 // sat solver data structure visible through all the internal files
98 {
99  int nClauses; // the total number of clauses
100  int nClausesStart; // the number of clauses before adding
101  Msat_ClauseVec_t * vClauses; // problem clauses
102  Msat_ClauseVec_t * vLearned; // learned clauses
103  double dClaInc; // Amount to bump next clause with.
104  double dClaDecay; // INVERSE decay factor for clause activity: stores 1/decay.
105 
106  double * pdActivity; // A heuristic measurement of the activity of a variable.
107  float * pFactors; // the multiplicative factors of variable activity
108  double dVarInc; // Amount to bump next variable with.
109  double dVarDecay; // INVERSE decay factor for variable activity: stores 1/decay. Use negative value for static variable order.
110  Msat_Order_t * pOrder; // Keeps track of the decision variable order.
111 
112  Msat_ClauseVec_t ** pvWatched; // 'pvWatched[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true).
113  Msat_Queue_t * pQueue; // Propagation queue.
114 
115  int nVars; // the current number of variables
116  int nVarsAlloc; // the maximum allowed number of variables
117  int * pAssigns; // The current assignments (literals or MSAT_VAR_UNKOWN)
118  int * pModel; // The satisfying assignment
119  Msat_IntVec_t * vTrail; // List of assignments made.
120  Msat_IntVec_t * vTrailLim; // Separator indices for different decision levels in 'trail'.
121  Msat_Clause_t ** pReasons; // 'reason[var]' is the clause that implied the variables current value, or 'NULL' if none.
122  int * pLevel; // 'level[var]' is the decision level at which assignment was made.
123  int nLevelRoot; // Level of first proper decision.
124 
125  double dRandSeed; // For the internal random number generator (makes solver deterministic over different platforms).
126 
127  int fVerbose; // the verbosity flag
128  double dProgress; // Set by 'search()'.
129 
130  // the variable cone and variable connectivity
134 
135  // internal data used during conflict analysis
136  int * pSeen; // time when a lit was seen for the last time
137  int nSeenId; // the id of current seeing
138  Msat_IntVec_t * vReason; // the temporary array of literals
139  Msat_IntVec_t * vTemp; // the temporary array of literals
140  int * pFreq; // the number of times each var participated in conflicts
141 
142  // the memory manager
144 
145  // statistics
147  int nTwoLits;
153 };
154 
156 {
158  int nSize;
159  int nCap;
160 };
161 
163 {
164  int * pArray;
165  int nSize;
166  int nCap;
167 };
168 
169 ////////////////////////////////////////////////////////////////////////
170 /// GLOBAL VARIABLES ///
171 ////////////////////////////////////////////////////////////////////////
172 
173 ////////////////////////////////////////////////////////////////////////
174 /// MACRO DEFINITIONS ///
175 ////////////////////////////////////////////////////////////////////////
176 
177 ////////////////////////////////////////////////////////////////////////
178 /// FUNCTION DECLARATIONS ///
179 ////////////////////////////////////////////////////////////////////////
180 
181 /*=== satActivity.c ===========================================================*/
186 /*=== satSolverApi.c ===========================================================*/
187 extern Msat_Clause_t * Msat_SolverReadClause( Msat_Solver_t * p, int Num );
188 /*=== satSolver.c ===========================================================*/
195 extern int * Msat_SolverReadSeenArray( Msat_Solver_t * p );
204 extern int Msat_SolverEnqueue( Msat_Solver_t * p, Msat_Lit_t Lit, Msat_Clause_t * pC );
205 extern double Msat_SolverProgressEstimate( Msat_Solver_t * p );
206 /*=== satSolverSearch.c ===========================================================*/
207 extern int Msat_SolverAssume( Msat_Solver_t * p, Msat_Lit_t Lit );
209 extern void Msat_SolverCancelUntil( Msat_Solver_t * p, int Level );
210 extern Msat_Type_t Msat_SolverSearch( Msat_Solver_t * p, int nConfLimit, int nLearnedLimit, int nBackTrackLimit, Msat_SearchParams_t * pPars );
211 /*=== satQueue.c ===========================================================*/
212 extern Msat_Queue_t * Msat_QueueAlloc( int nVars );
213 extern void Msat_QueueFree( Msat_Queue_t * p );
214 extern int Msat_QueueReadSize( Msat_Queue_t * p );
215 extern void Msat_QueueInsert( Msat_Queue_t * p, int Lit );
216 extern int Msat_QueueExtract( Msat_Queue_t * p );
217 extern void Msat_QueueClear( Msat_Queue_t * p );
218 /*=== satOrder.c ===========================================================*/
219 extern Msat_Order_t * Msat_OrderAlloc( Msat_Solver_t * pSat );
220 extern void Msat_OrderSetBounds( Msat_Order_t * p, int nVarsMax );
221 extern void Msat_OrderClean( Msat_Order_t * p, Msat_IntVec_t * vCone );
222 extern int Msat_OrderCheck( Msat_Order_t * p );
223 extern void Msat_OrderFree( Msat_Order_t * p );
224 extern int Msat_OrderVarSelect( Msat_Order_t * p );
225 extern void Msat_OrderVarAssigned( Msat_Order_t * p, int Var );
226 extern void Msat_OrderVarUnassigned( Msat_Order_t * p, int Var );
227 extern void Msat_OrderUpdate( Msat_Order_t * p, int Var );
228 /*=== satClause.c ===========================================================*/
229 extern int Msat_ClauseCreate( Msat_Solver_t * p, Msat_IntVec_t * vLits, int fLearnt, Msat_Clause_t ** pClause_out );
232 extern int Msat_ClauseReadLearned( Msat_Clause_t * pC );
233 extern int Msat_ClauseReadSize( Msat_Clause_t * pC );
234 extern int * Msat_ClauseReadLits( Msat_Clause_t * pC );
235 extern int Msat_ClauseReadMark( Msat_Clause_t * pC );
236 extern void Msat_ClauseSetMark( Msat_Clause_t * pC, int fMark );
237 extern int Msat_ClauseReadNum( Msat_Clause_t * pC );
238 extern void Msat_ClauseSetNum( Msat_Clause_t * pC, int Num );
239 extern int Msat_ClauseReadTypeA( Msat_Clause_t * pC );
240 extern void Msat_ClauseSetTypeA( Msat_Clause_t * pC, int fTypeA );
241 extern int Msat_ClauseIsLocked( Msat_Solver_t * p, Msat_Clause_t * pC );
242 extern float Msat_ClauseReadActivity( Msat_Clause_t * pC );
243 extern void Msat_ClauseWriteActivity( Msat_Clause_t * pC, float Num );
244 extern void Msat_ClauseFree( Msat_Solver_t * p, Msat_Clause_t * pC, int fRemoveWatched );
245 extern int Msat_ClausePropagate( Msat_Clause_t * pC, Msat_Lit_t Lit, int * pAssigns, Msat_Lit_t * pLit_out );
246 extern int Msat_ClauseSimplify( Msat_Clause_t * pC, int * pAssigns );
247 extern void Msat_ClauseCalcReason( Msat_Solver_t * p, Msat_Clause_t * pC, Msat_Lit_t Lit, Msat_IntVec_t * vLits_out );
248 extern void Msat_ClauseRemoveWatch( Msat_ClauseVec_t * vClauses, Msat_Clause_t * pC );
249 extern void Msat_ClausePrint( Msat_Clause_t * pC );
250 extern void Msat_ClausePrintSymbols( Msat_Clause_t * pC );
251 extern void Msat_ClauseWriteDimacs( FILE * pFile, Msat_Clause_t * pC, int fIncrement );
252 extern unsigned Msat_ClauseComputeTruth( Msat_Solver_t * p, Msat_Clause_t * pC );
253 /*=== satSort.c ===========================================================*/
254 extern void Msat_SolverSortDB( Msat_Solver_t * p );
255 /*=== satClauseVec.c ===========================================================*/
256 extern Msat_ClauseVec_t * Msat_ClauseVecAlloc( int nCap );
257 extern void Msat_ClauseVecFree( Msat_ClauseVec_t * p );
260 extern void Msat_ClauseVecGrow( Msat_ClauseVec_t * p, int nCapMin );
261 extern void Msat_ClauseVecShrink( Msat_ClauseVec_t * p, int nSizeNew );
262 extern void Msat_ClauseVecClear( Msat_ClauseVec_t * p );
263 extern void Msat_ClauseVecPush( Msat_ClauseVec_t * p, Msat_Clause_t * Entry );
265 extern void Msat_ClauseVecWriteEntry( Msat_ClauseVec_t * p, int i, Msat_Clause_t * Entry );
267 
268 /*=== satMem.c ===========================================================*/
269 // fixed-size-block memory manager
270 extern Msat_MmFixed_t * Msat_MmFixedStart( int nEntrySize );
271 extern void Msat_MmFixedStop( Msat_MmFixed_t * p, int fVerbose );
272 extern char * Msat_MmFixedEntryFetch( Msat_MmFixed_t * p );
273 extern void Msat_MmFixedEntryRecycle( Msat_MmFixed_t * p, char * pEntry );
274 extern void Msat_MmFixedRestart( Msat_MmFixed_t * p );
276 // flexible-size-block memory manager
278 extern void Msat_MmFlexStop( Msat_MmFlex_t * p, int fVerbose );
279 extern char * Msat_MmFlexEntryFetch( Msat_MmFlex_t * p, int nBytes );
280 extern int Msat_MmFlexReadMemUsage( Msat_MmFlex_t * p );
281 // hierarchical memory manager
282 extern Msat_MmStep_t * Msat_MmStepStart( int nSteps );
283 extern void Msat_MmStepStop( Msat_MmStep_t * p, int fVerbose );
284 extern char * Msat_MmStepEntryFetch( Msat_MmStep_t * p, int nBytes );
285 extern void Msat_MmStepEntryRecycle( Msat_MmStep_t * p, char * pEntry, int nBytes );
286 extern int Msat_MmStepReadMemUsage( Msat_MmStep_t * p );
287 
288 ////////////////////////////////////////////////////////////////////////
289 /// END OF FILE ///
290 ////////////////////////////////////////////////////////////////////////
291 
292 
294 
295 #endif
int nClausesInit
Definition: msatInt.h:149
void Msat_SolverClausesDecrement(Msat_Solver_t *p)
Definition: msatSolverApi.c:65
int * Msat_ClauseReadLits(Msat_Clause_t *pC)
Definition: msatClause.c:257
int Msat_SolverReadDecisionLevel(Msat_Solver_t *p)
Definition: msatSolverApi.c:50
void Msat_ClauseSetMark(Msat_Clause_t *pC, int fMark)
Definition: msatClause.c:262
int Msat_Var_t
Definition: msatInt.h:66
void Msat_ClauseWriteDimacs(FILE *pFile, Msat_Clause_t *pC, int fIncrement)
Definition: msatClause.c:494
void Msat_OrderVarAssigned(Msat_Order_t *p, int Var)
Definition: msatOrderH.c:220
int Msat_MmFixedReadMemUsage(Msat_MmFixed_t *p)
Definition: msatMem.c:270
Msat_Clause_t * Msat_ClauseVecPop(Msat_ClauseVec_t *p)
void Msat_MmStepEntryRecycle(Msat_MmStep_t *p, char *pEntry, int nBytes)
Definition: msatMem.c:503
void Msat_QueueFree(Msat_Queue_t *p)
Definition: msatQueue.c:74
int * pModel
Definition: msatInt.h:118
int Msat_OrderCheck(Msat_Order_t *p)
Definition: msatOrderH.c:147
int * Msat_SolverReadSeenArray(Msat_Solver_t *p)
Definition: msatSolverApi.c:61
Msat_IntVec_t * vReason
Definition: msatInt.h:138
char * Msat_MmFlexEntryFetch(Msat_MmFlex_t *p, int nBytes)
Definition: msatMem.c:349
static Llb_Mgr_t * p
Definition: llb3Image.c:950
void Msat_QueueClear(Msat_Queue_t *p)
Definition: msatQueue.c:149
void Msat_ClauseVecGrow(Msat_ClauseVec_t *p, int nCapMin)
Msat_ClauseVec_t * vAdjacents
Definition: msatInt.h:133
Msat_Clause_t * Msat_ClauseVecReadEntry(Msat_ClauseVec_t *p, int i)
char * Msat_MmStepEntryFetch(Msat_MmStep_t *p, int nBytes)
Definition: msatMem.c:479
Msat_Clause_t * Msat_ClauseCreateFake(Msat_Solver_t *p, Msat_IntVec_t *vLits)
void Msat_ClauseVecFree(Msat_ClauseVec_t *p)
Definition: msatClauseVec.c:68
int * pAssigns
Definition: msatInt.h:117
ABC_INT64_T nInspects
Definition: msatInt.h:84
void Msat_QueueInsert(Msat_Queue_t *p, int Lit)
Definition: msatQueue.c:107
int * pLevel
Definition: msatInt.h:122
void Msat_OrderSetBounds(Msat_Order_t *p, int nVarsMax)
Definition: msatOrderH.c:101
Msat_IntVec_t * vTrail
Definition: msatInt.h:119
Msat_ClauseVec_t * Msat_SolverReadLearned(Msat_Solver_t *p)
Definition: msatSolverApi.c:54
Msat_Clause_t ** Msat_ClauseVecReadArray(Msat_ClauseVec_t *p)
Definition: msatClauseVec.c:85
void Msat_MmFixedRestart(Msat_MmFixed_t *p)
Definition: msatMem.c:232
Msat_Clause_t * Msat_ClauseCreateFakeLit(Msat_Solver_t *p, Msat_Lit_t Lit)
DECLARATIONS ///.
Definition: msatOrderH.c:31
int Msat_ClauseCreate(Msat_Solver_t *p, Msat_IntVec_t *vLits, int fLearnt, Msat_Clause_t **pClause_out)
FUNCTION DEFINITIONS ///.
Definition: msatClause.c:58
int nClausesAllocL
Definition: msatInt.h:151
Msat_MmStep_t * pMem
Definition: msatInt.h:143
Msat_Type_t Msat_SolverSearch(Msat_Solver_t *p, int nConfLimit, int nLearnedLimit, int nBackTrackLimit, Msat_SearchParams_t *pPars)
Msat_Type_t
Definition: msat.h:50
int Msat_SolverIncrementSeenId(Msat_Solver_t *p)
Definition: msatSolverApi.c:62
int Msat_ClauseReadTypeA(Msat_Clause_t *pC)
Definition: msatClause.c:260
void Msat_ClausePrint(Msat_Clause_t *pC)
Definition: msatClause.c:468
double dRandSeed
Definition: msatInt.h:125
Msat_Order_t * pOrder
Definition: msatInt.h:110
int Msat_QueueReadSize(Msat_Queue_t *p)
Definition: msatQueue.c:91
void Msat_SolverClaDecayActivity(Msat_Solver_t *p)
Definition: msatActivity.c:128
void Msat_MmFlexStop(Msat_MmFlex_t *p, int fVerbose)
Definition: msatMem.c:320
void Msat_MmFixedEntryRecycle(Msat_MmFixed_t *p, char *pEntry)
Definition: msatMem.c:212
typedefABC_NAMESPACE_HEADER_START struct Msat_Clause_t_ Msat_Clause_t
INCLUDES ///.
Definition: msatInt.h:57
int Msat_Lit_t
Definition: msatInt.h:65
ABC_INT64_T nDecisions
Definition: msatInt.h:82
int Msat_SolverEnqueue(Msat_Solver_t *p, Msat_Lit_t Lit, Msat_Clause_t *pC)
void Msat_ClauseRemoveWatch(Msat_ClauseVec_t *vClauses, Msat_Clause_t *pC)
Definition: msatClause.c:444
void Msat_SolverVarRescaleActivity(Msat_Solver_t *p)
Definition: msatActivity.c:86
float Msat_ClauseReadActivity(Msat_Clause_t *pC)
Definition: msatClause.c:295
Msat_ClauseVec_t ** pvWatched
Definition: msatInt.h:112
unsigned Msat_ClauseComputeTruth(Msat_Solver_t *p, Msat_Clause_t *pC)
int nVarsAlloc
Definition: msatInt.h:116
int Msat_ClauseSimplify(Msat_Clause_t *pC, int *pAssigns)
Definition: msatClause.c:374
int Msat_ClauseReadNum(Msat_Clause_t *pC)
Definition: msatClause.c:259
int Msat_OrderVarSelect(Msat_Order_t *p)
Definition: msatOrderH.c:183
int nLevelRoot
Definition: msatInt.h:123
void Msat_ClauseCalcReason(Msat_Solver_t *p, Msat_Clause_t *pC, Msat_Lit_t Lit, Msat_IntVec_t *vLits_out)
Definition: msatClause.c:418
int nBackTracks
Definition: msatInt.h:152
int Msat_ClausePropagate(Msat_Clause_t *pC, Msat_Lit_t Lit, int *pAssigns, Msat_Lit_t *pLit_out)
Definition: msatClause.c:335
Msat_Clause_t * Msat_SolverReadClause(Msat_Solver_t *p, int Num)
Definition: msatSolverApi.c:83
Msat_ClauseVec_t * vClauses
Definition: msatInt.h:101
Msat_Queue_t * pQueue
Definition: msatInt.h:113
int Msat_MmStepReadMemUsage(Msat_MmStep_t *p)
Definition: msatMem.c:526
Msat_ClauseVec_t * Msat_ClauseVecAlloc(int nCap)
DECLARATIONS ///.
Definition: msatClauseVec.c:45
void Msat_SolverSortDB(Msat_Solver_t *p)
FUNCTION DEFINITIONS ///.
Definition: msatSort.c:61
double dVarInc
Definition: msatInt.h:108
void Msat_ClauseVecWriteEntry(Msat_ClauseVec_t *p, int i, Msat_Clause_t *Entry)
void Msat_SolverVarBumpActivity(Msat_Solver_t *p, Msat_Lit_t Lit)
DECLARATIONS ///.
Definition: msatActivity.c:45
double dClaInc
Definition: msatInt.h:103
void Msat_ClauseVecClear(Msat_ClauseVec_t *p)
int Msat_ClauseReadMark(Msat_Clause_t *pC)
Definition: msatClause.c:258
double dProgress
Definition: msatInt.h:128
DECLARATIONS ///.
Definition: msatClause.c:30
int nClausesStart
Definition: msatInt.h:100
void Msat_SolverCancelUntil(Msat_Solver_t *p, int Level)
void Msat_ClauseVecPush(Msat_ClauseVec_t *p, Msat_Clause_t *Entry)
void Msat_OrderFree(Msat_Order_t *p)
Definition: msatOrderH.c:163
void Msat_ClauseSetTypeA(Msat_Clause_t *pC, int fTypeA)
Definition: msatClause.c:264
void Msat_SolverVarDecayActivity(Msat_Solver_t *p)
GLOBAL VARIABLES ///.
Definition: msatActivity.c:69
void Msat_SolverClaBumpActivity(Msat_Solver_t *p, Msat_Clause_t *pC)
Definition: msatActivity.c:105
DECLARATIONS ///.
Definition: msatMem.c:30
int nClauses
Definition: msatInt.h:99
Msat_IntVec_t * vTrailLim
Definition: msatInt.h:120
void Msat_ClauseFree(Msat_Solver_t *p, Msat_Clause_t *pC, int fRemoveWatched)
Definition: msatClause.c:223
int * pSeen
Definition: msatInt.h:136
float * pFactors
Definition: msatInt.h:107
#define ABC_NAMESPACE_HEADER_START
NAMESPACES ///.
Definition: abc_global.h:105
DECLARATIONS ///.
Definition: msatQueue.c:30
void Msat_SolverClausesIncrement(Msat_Solver_t *p)
Definition: msatSolverApi.c:64
Msat_MmStep_t * Msat_SolverReadMem(Msat_Solver_t *p)
Definition: msatSolverApi.c:60
ABC_INT64_T nPropagations
Definition: msatInt.h:83
#define ABC_NAMESPACE_HEADER_END
Definition: abc_global.h:106
int Msat_ClauseIsLocked(Msat_Solver_t *p, Msat_Clause_t *pC)
Definition: msatClause.c:278
Msat_MmFlex_t * Msat_MmFlexStart()
Definition: msatMem.c:288
Msat_Order_t * Msat_OrderAlloc(Msat_Solver_t *pSat)
FUNCTION DEFINITIONS ///.
Definition: msatOrderH.c:78
void Msat_SolverClaRescaleActivity(Msat_Solver_t *p)
Definition: msatActivity.c:144
ABC_INT64_T nStarts
Definition: msatInt.h:81
int Msat_MmFlexReadMemUsage(Msat_MmFlex_t *p)
Definition: msatMem.c:394
double dClaDecay
Definition: msatInt.h:104
void Msat_SolverClausesIncrementL(Msat_Solver_t *p)
Definition: msatSolverApi.c:66
Msat_Clause_t ** pReasons
Definition: msatInt.h:121
double * pdActivity
Definition: msatInt.h:106
double dVarDecay
Definition: msatInt.h:109
void Msat_ClausePrintSymbols(Msat_Clause_t *pC)
Definition: msatClause.c:515
Msat_ClauseVec_t ** Msat_SolverReadWatchedArray(Msat_Solver_t *p)
Definition: msatSolverApi.c:55
Msat_Clause_t ** Msat_SolverReadReasonArray(Msat_Solver_t *p)
Definition: msatSolverApi.c:52
Msat_Clause_t ** pArray
Definition: msatInt.h:157
Msat_IntVec_t * vVarsUsed
Definition: msatInt.h:132
Msat_Type_t Msat_SolverReadVarValue(Msat_Solver_t *p, Msat_Var_t Var)
Definition: msatSolverApi.c:53
Msat_ClauseVec_t * vLearned
Definition: msatInt.h:102
Msat_IntVec_t * vConeVars
Definition: msatInt.h:131
ABC_INT64_T nConflicts
Definition: msatInt.h:85
void Msat_MmFixedStop(Msat_MmFixed_t *p, int fVerbose)
Definition: msatMem.c:132
Msat_Clause_t * Msat_SolverPropagate(Msat_Solver_t *p)
int Msat_SolverAssume(Msat_Solver_t *p, Msat_Lit_t Lit)
FUNCTION DEFINITIONS ///.
int * pFreq
Definition: msatInt.h:140
int Var
Definition: SolverTypes.h:42
void Msat_OrderClean(Msat_Order_t *p, Msat_IntVec_t *vCone)
Definition: msatOrderH.c:120
void Msat_OrderUpdate(Msat_Order_t *p, int Var)
Definition: msatOrderH.c:257
int Msat_ClauseReadSize(Msat_Clause_t *pC)
Definition: msatClause.c:256
Msat_MmFixed_t * Msat_MmFixedStart(int nEntrySize)
FUNCTION DEFINITIONS ///.
Definition: msatMem.c:93
Msat_Queue_t * Msat_QueueAlloc(int nVars)
FUNCTION DEFINITIONS ///.
Definition: msatQueue.c:53
char * Msat_MmFixedEntryFetch(Msat_MmFixed_t *p)
Definition: msatMem.c:161
int * Msat_SolverReadDecisionLevelArray(Msat_Solver_t *p)
Definition: msatSolverApi.c:51
void Msat_OrderVarUnassigned(Msat_Order_t *p, int Var)
Definition: msatOrderH.c:235
ABC_INT64_T nSuccesses
Definition: msatInt.h:86
int * pArray
Definition: msatInt.h:164
Msat_MmStep_t * Msat_MmStepStart(int nSteps)
Definition: msatMem.c:423
int Msat_QueueExtract(Msat_Queue_t *p)
Definition: msatQueue.c:131
double Msat_SolverProgressEstimate(Msat_Solver_t *p)
Msat_IntVec_t * vTemp
Definition: msatInt.h:139
void Msat_MmStepStop(Msat_MmStep_t *p, int fVerbose)
Definition: msatMem.c:458
int Msat_ClauseReadLearned(Msat_Clause_t *pC)
Definition: msatClause.c:255
void Msat_ClauseVecShrink(Msat_ClauseVec_t *p, int nSizeNew)
int Msat_ClauseVecReadSize(Msat_ClauseVec_t *p)
void Msat_ClauseSetNum(Msat_Clause_t *pC, int Num)
Definition: msatClause.c:263
void Msat_ClauseWriteActivity(Msat_Clause_t *pC, float Num)
Definition: msatClause.c:314
typedefABC_NAMESPACE_HEADER_START struct Msat_Solver_t_ Msat_Solver_t
INCLUDES ///.
Definition: msat.h:42
void Msat_SolverClausesDecrementL(Msat_Solver_t *p)
Definition: msatSolverApi.c:67
Msat_SolverStats_t Stats
Definition: msatInt.h:146
int nClausesAlloc
Definition: msatInt.h:150