abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
msatSolverApi.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [msatSolverApi.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 [APIs of the SAT 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: msatSolverApi.c,v 1.0 2004/01/01 1:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "msatInt.h"
22 
23 ABC_NAMESPACE_IMPL_START
24 
25 
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29 
30 static void Msat_SolverSetupTruthTables( unsigned uTruths[][2] );
31 
32 ////////////////////////////////////////////////////////////////////////
33 /// FUNCTION DEFINITIONS ///
34 ////////////////////////////////////////////////////////////////////////
35 
36 /**Function*************************************************************
37 
38  Synopsis [Simple SAT solver APIs.]
39 
40  Description []
41 
42  SideEffects []
43 
44  SeeAlso []
45 
46 ***********************************************************************/
47 int Msat_SolverReadVarNum( Msat_Solver_t * p ) { return p->nVars; }
48 int Msat_SolverReadClauseNum( Msat_Solver_t * p ) { return p->nClauses; }
49 int Msat_SolverReadVarAllocNum( Msat_Solver_t * p ) { return p->nVarsAlloc; }
50 int Msat_SolverReadDecisionLevel( Msat_Solver_t * p ) { return Msat_IntVecReadSize(p->vTrailLim); }
51 int * Msat_SolverReadDecisionLevelArray( Msat_Solver_t * p ) { return p->pLevel; }
52 Msat_Clause_t ** Msat_SolverReadReasonArray( Msat_Solver_t * p ) { return p->pReasons; }
53 Msat_Type_t Msat_SolverReadVarValue( Msat_Solver_t * p, Msat_Var_t Var ) { return (Msat_Type_t)p->pAssigns[Var]; }
54 Msat_ClauseVec_t * Msat_SolverReadLearned( Msat_Solver_t * p ) { return p->vLearned; }
55 Msat_ClauseVec_t ** Msat_SolverReadWatchedArray( Msat_Solver_t * p ) { return p->pvWatched; }
56 int * Msat_SolverReadAssignsArray( Msat_Solver_t * p ) { return p->pAssigns; }
57 int * Msat_SolverReadModelArray( Msat_Solver_t * p ) { return p->pModel; }
58 int Msat_SolverReadBackTracks( Msat_Solver_t * p ) { return (int)p->Stats.nConflicts; }
59 int Msat_SolverReadInspects( Msat_Solver_t * p ) { return (int)p->Stats.nInspects; }
60 Msat_MmStep_t * Msat_SolverReadMem( Msat_Solver_t * p ) { return p->pMem; }
61 int * Msat_SolverReadSeenArray( Msat_Solver_t * p ) { return p->pSeen; }
62 int Msat_SolverIncrementSeenId( Msat_Solver_t * p ) { return ++p->nSeenId; }
63 void Msat_SolverSetVerbosity( Msat_Solver_t * p, int fVerbose ) { p->fVerbose = fVerbose; }
64 void Msat_SolverClausesIncrement( Msat_Solver_t * p ) { p->nClausesAlloc++; }
65 void Msat_SolverClausesDecrement( Msat_Solver_t * p ) { p->nClausesAlloc--; }
66 void Msat_SolverClausesIncrementL( Msat_Solver_t * p ) { p->nClausesAllocL++; }
67 void Msat_SolverClausesDecrementL( Msat_Solver_t * p ) { p->nClausesAllocL--; }
68 void Msat_SolverMarkLastClauseTypeA( Msat_Solver_t * p ) { Msat_ClauseSetTypeA( Msat_ClauseVecReadEntry( p->vClauses, Msat_ClauseVecReadSize(p->vClauses)-1 ), 1 ); }
69 void Msat_SolverMarkClausesStart( Msat_Solver_t * p ) { p->nClausesStart = Msat_ClauseVecReadSize(p->vClauses); }
70 float * Msat_SolverReadFactors( Msat_Solver_t * p ) { return p->pFactors; }
71 
72 /**Function*************************************************************
73 
74  Synopsis [Reads the clause with the given number.]
75 
76  Description []
77 
78  SideEffects []
79 
80  SeeAlso []
81 
82 ***********************************************************************/
83 Msat_Clause_t * Msat_SolverReadClause( Msat_Solver_t * p, int Num )
84 {
85  int nClausesP;
86  assert( Num < p->nClauses );
87  nClausesP = Msat_ClauseVecReadSize( p->vClauses );
88  if ( Num < nClausesP )
89  return Msat_ClauseVecReadEntry( p->vClauses, Num );
90  return Msat_ClauseVecReadEntry( p->vLearned, Num - nClausesP );
91 }
92 
93 /**Function*************************************************************
94 
95  Synopsis [Reads the clause with the given number.]
96 
97  Description []
98 
99  SideEffects []
100 
101  SeeAlso []
102 
103 ***********************************************************************/
104 Msat_ClauseVec_t * Msat_SolverReadAdjacents( Msat_Solver_t * p )
105 {
106  return p->vAdjacents;
107 }
108 
109 /**Function*************************************************************
110 
111  Synopsis [Reads the clause with the given number.]
112 
113  Description []
114 
115  SideEffects []
116 
117  SeeAlso []
118 
119 ***********************************************************************/
120 Msat_IntVec_t * Msat_SolverReadConeVars( Msat_Solver_t * p )
121 {
122  return p->vConeVars;
123 }
124 
125 /**Function*************************************************************
126 
127  Synopsis [Reads the clause with the given number.]
128 
129  Description []
130 
131  SideEffects []
132 
133  SeeAlso []
134 
135 ***********************************************************************/
136 Msat_IntVec_t * Msat_SolverReadVarsUsed( Msat_Solver_t * p )
137 {
138  return p->vVarsUsed;
139 }
140 
141 
142 /**Function*************************************************************
143 
144  Synopsis [Allocates the solver.]
145 
146  Description [After the solver is allocated, the procedure
147  Msat_SolverClean() should be called to set the number of variables.]
148 
149  SideEffects []
150 
151  SeeAlso []
152 
153 ***********************************************************************/
154 Msat_Solver_t * Msat_SolverAlloc( int nVarsAlloc,
155  double dClaInc, double dClaDecay,
156  double dVarInc, double dVarDecay,
157  int fVerbose )
158 {
159  Msat_Solver_t * p;
160  int i;
161 
162  assert(sizeof(Msat_Lit_t) == sizeof(unsigned));
163  assert(sizeof(float) == sizeof(unsigned));
164 
165  p = ABC_ALLOC( Msat_Solver_t, 1 );
166  memset( p, 0, sizeof(Msat_Solver_t) );
167 
168  p->nVarsAlloc = nVarsAlloc;
169  p->nVars = 0;
170 
171  p->nClauses = 0;
172  p->vClauses = Msat_ClauseVecAlloc( 512 );
173  p->vLearned = Msat_ClauseVecAlloc( 512 );
174 
175  p->dClaInc = dClaInc;
176  p->dClaDecay = dClaDecay;
177  p->dVarInc = dVarInc;
178  p->dVarDecay = dVarDecay;
179 
180  p->pdActivity = ABC_ALLOC( double, p->nVarsAlloc );
181  p->pFactors = ABC_ALLOC( float, p->nVarsAlloc );
182  for ( i = 0; i < p->nVarsAlloc; i++ )
183  {
184  p->pdActivity[i] = 0.0;
185  p->pFactors[i] = 1.0;
186  }
187 
188  p->pAssigns = ABC_ALLOC( int, p->nVarsAlloc );
189  p->pModel = ABC_ALLOC( int, p->nVarsAlloc );
190  for ( i = 0; i < p->nVarsAlloc; i++ )
191  p->pAssigns[i] = MSAT_VAR_UNASSIGNED;
192 // p->pOrder = Msat_OrderAlloc( p->pAssigns, p->pdActivity, p->nVarsAlloc );
193  p->pOrder = Msat_OrderAlloc( p );
194 
195  p->pvWatched = ABC_ALLOC( Msat_ClauseVec_t *, 2 * p->nVarsAlloc );
196  for ( i = 0; i < 2 * p->nVarsAlloc; i++ )
197  p->pvWatched[i] = Msat_ClauseVecAlloc( 16 );
198  p->pQueue = Msat_QueueAlloc( p->nVarsAlloc );
199 
200  p->vTrail = Msat_IntVecAlloc( p->nVarsAlloc );
201  p->vTrailLim = Msat_IntVecAlloc( p->nVarsAlloc );
202  p->pReasons = ABC_ALLOC( Msat_Clause_t *, p->nVarsAlloc );
203  memset( p->pReasons, 0, sizeof(Msat_Clause_t *) * p->nVarsAlloc );
204  p->pLevel = ABC_ALLOC( int, p->nVarsAlloc );
205  for ( i = 0; i < p->nVarsAlloc; i++ )
206  p->pLevel[i] = -1;
207  p->dRandSeed = 91648253;
208  p->fVerbose = fVerbose;
209  p->dProgress = 0.0;
210 // p->pModel = Msat_IntVecAlloc( p->nVarsAlloc );
211  p->pMem = Msat_MmStepStart( 10 );
212 
213  p->vConeVars = Msat_IntVecAlloc( p->nVarsAlloc );
214  p->vAdjacents = Msat_ClauseVecAlloc( p->nVarsAlloc );
215  for ( i = 0; i < p->nVarsAlloc; i++ )
216  Msat_ClauseVecPush( p->vAdjacents, (Msat_Clause_t *)Msat_IntVecAlloc(5) );
217  p->vVarsUsed = Msat_IntVecAlloc( p->nVarsAlloc );
218  Msat_IntVecFill( p->vVarsUsed, p->nVarsAlloc, 1 );
219 
220 
221  p->pSeen = ABC_ALLOC( int, p->nVarsAlloc );
222  memset( p->pSeen, 0, sizeof(int) * p->nVarsAlloc );
223  p->nSeenId = 1;
224  p->vReason = Msat_IntVecAlloc( p->nVarsAlloc );
225  p->vTemp = Msat_IntVecAlloc( p->nVarsAlloc );
226  return p;
227 }
228 
229 /**Function*************************************************************
230 
231  Synopsis [Resizes the solver.]
232 
233  Description [Assumes that the solver contains some clauses, and that
234  it is currently between the calls. Resizes the solver to accomodate
235  more variables.]
236 
237  SideEffects []
238 
239  SeeAlso []
240 
241 ***********************************************************************/
242 void Msat_SolverResize( Msat_Solver_t * p, int nVarsAlloc )
243 {
244  int nVarsAllocOld, i;
245 
246  nVarsAllocOld = p->nVarsAlloc;
247  p->nVarsAlloc = nVarsAlloc;
248 
249  p->pdActivity = ABC_REALLOC( double, p->pdActivity, p->nVarsAlloc );
250  p->pFactors = ABC_REALLOC( float, p->pFactors, p->nVarsAlloc );
251  for ( i = nVarsAllocOld; i < p->nVarsAlloc; i++ )
252  {
253  p->pdActivity[i] = 0.0;
254  p->pFactors[i] = 1.0;
255  }
256 
257  p->pAssigns = ABC_REALLOC( int, p->pAssigns, p->nVarsAlloc );
258  p->pModel = ABC_REALLOC( int, p->pModel, p->nVarsAlloc );
259  for ( i = nVarsAllocOld; i < p->nVarsAlloc; i++ )
260  p->pAssigns[i] = MSAT_VAR_UNASSIGNED;
261 
262 // Msat_OrderRealloc( p->pOrder, p->pAssigns, p->pdActivity, p->nVarsAlloc );
263  Msat_OrderSetBounds( p->pOrder, p->nVarsAlloc );
264 
265  p->pvWatched = ABC_REALLOC( Msat_ClauseVec_t *, p->pvWatched, 2 * p->nVarsAlloc );
266  for ( i = 2 * nVarsAllocOld; i < 2 * p->nVarsAlloc; i++ )
267  p->pvWatched[i] = Msat_ClauseVecAlloc( 16 );
268 
269  Msat_QueueFree( p->pQueue );
270  p->pQueue = Msat_QueueAlloc( p->nVarsAlloc );
271 
272  p->pReasons = ABC_REALLOC( Msat_Clause_t *, p->pReasons, p->nVarsAlloc );
273  p->pLevel = ABC_REALLOC( int, p->pLevel, p->nVarsAlloc );
274  for ( i = nVarsAllocOld; i < p->nVarsAlloc; i++ )
275  {
276  p->pReasons[i] = NULL;
277  p->pLevel[i] = -1;
278  }
279 
280  p->pSeen = ABC_REALLOC( int, p->pSeen, p->nVarsAlloc );
281  for ( i = nVarsAllocOld; i < p->nVarsAlloc; i++ )
282  p->pSeen[i] = 0;
283 
284  Msat_IntVecGrow( p->vTrail, p->nVarsAlloc );
285  Msat_IntVecGrow( p->vTrailLim, p->nVarsAlloc );
286 
287  // make sure the array of adjucents has room to store the variable numbers
288  for ( i = Msat_ClauseVecReadSize(p->vAdjacents); i < p->nVarsAlloc; i++ )
289  Msat_ClauseVecPush( p->vAdjacents, (Msat_Clause_t *)Msat_IntVecAlloc(5) );
290  Msat_IntVecFill( p->vVarsUsed, p->nVarsAlloc, 1 );
291 }
292 
293 /**Function*************************************************************
294 
295  Synopsis [Prepares the solver.]
296 
297  Description [Cleans the solver assuming that the problem will involve
298  the given number of variables (nVars). This procedure is useful
299  for many small (incremental) SAT problems, to prevent the solver
300  from being reallocated each time.]
301 
302  SideEffects []
303 
304  SeeAlso []
305 
306 ***********************************************************************/
307 void Msat_SolverClean( Msat_Solver_t * p, int nVars )
308 {
309  int i;
310  // free the clauses
311  int nClauses;
312  Msat_Clause_t ** pClauses;
313 
314  assert( p->nVarsAlloc >= nVars );
315  p->nVars = nVars;
316  p->nClauses = 0;
317 
318  nClauses = Msat_ClauseVecReadSize( p->vClauses );
319  pClauses = Msat_ClauseVecReadArray( p->vClauses );
320  for ( i = 0; i < nClauses; i++ )
321  Msat_ClauseFree( p, pClauses[i], 0 );
322 // Msat_ClauseVecFree( p->vClauses );
323  Msat_ClauseVecClear( p->vClauses );
324 
325  nClauses = Msat_ClauseVecReadSize( p->vLearned );
326  pClauses = Msat_ClauseVecReadArray( p->vLearned );
327  for ( i = 0; i < nClauses; i++ )
328  Msat_ClauseFree( p, pClauses[i], 0 );
329 // Msat_ClauseVecFree( p->vLearned );
330  Msat_ClauseVecClear( p->vLearned );
331 
332 // ABC_FREE( p->pdActivity );
333  for ( i = 0; i < p->nVars; i++ )
334  p->pdActivity[i] = 0;
335 
336 // Msat_OrderFree( p->pOrder );
337 // Msat_OrderClean( p->pOrder, p->nVars, NULL );
338  Msat_OrderSetBounds( p->pOrder, p->nVars );
339 
340  for ( i = 0; i < 2 * p->nVars; i++ )
341 // Msat_ClauseVecFree( p->pvWatched[i] );
342  Msat_ClauseVecClear( p->pvWatched[i] );
343 // ABC_FREE( p->pvWatched );
344 // Msat_QueueFree( p->pQueue );
345  Msat_QueueClear( p->pQueue );
346 
347 // ABC_FREE( p->pAssigns );
348  for ( i = 0; i < p->nVars; i++ )
349  p->pAssigns[i] = MSAT_VAR_UNASSIGNED;
350 // Msat_IntVecFree( p->vTrail );
351  Msat_IntVecClear( p->vTrail );
352 // Msat_IntVecFree( p->vTrailLim );
353  Msat_IntVecClear( p->vTrailLim );
354 // ABC_FREE( p->pReasons );
355  memset( p->pReasons, 0, sizeof(Msat_Clause_t *) * p->nVars );
356 // ABC_FREE( p->pLevel );
357  for ( i = 0; i < p->nVars; i++ )
358  p->pLevel[i] = -1;
359 // Msat_IntVecFree( p->pModel );
360 // Msat_MmStepStop( p->pMem, 0 );
361  p->dRandSeed = 91648253;
362  p->dProgress = 0.0;
363 
364 // ABC_FREE( p->pSeen );
365  memset( p->pSeen, 0, sizeof(int) * p->nVars );
366  p->nSeenId = 1;
367 // Msat_IntVecFree( p->vReason );
368  Msat_IntVecClear( p->vReason );
369 // Msat_IntVecFree( p->vTemp );
370  Msat_IntVecClear( p->vTemp );
371 // printf(" The number of clauses remaining = %d (%d).\n", p->nClausesAlloc, p->nClausesAllocL );
372 // ABC_FREE( p );
373 }
374 
375 /**Function*************************************************************
376 
377  Synopsis [Frees the solver.]
378 
379  Description []
380 
381  SideEffects []
382 
383  SeeAlso []
384 
385 ***********************************************************************/
386 void Msat_SolverFree( Msat_Solver_t * p )
387 {
388  int i;
389 
390  // free the clauses
391  int nClauses;
392  Msat_Clause_t ** pClauses;
393 //printf( "clauses = %d. learned = %d.\n", Msat_ClauseVecReadSize( p->vClauses ),
394 // Msat_ClauseVecReadSize( p->vLearned ) );
395 
396  nClauses = Msat_ClauseVecReadSize( p->vClauses );
397  pClauses = Msat_ClauseVecReadArray( p->vClauses );
398  for ( i = 0; i < nClauses; i++ )
399  Msat_ClauseFree( p, pClauses[i], 0 );
400  Msat_ClauseVecFree( p->vClauses );
401 
402  nClauses = Msat_ClauseVecReadSize( p->vLearned );
403  pClauses = Msat_ClauseVecReadArray( p->vLearned );
404  for ( i = 0; i < nClauses; i++ )
405  Msat_ClauseFree( p, pClauses[i], 0 );
406  Msat_ClauseVecFree( p->vLearned );
407 
408  ABC_FREE( p->pdActivity );
409  ABC_FREE( p->pFactors );
410  Msat_OrderFree( p->pOrder );
411 
412  for ( i = 0; i < 2 * p->nVarsAlloc; i++ )
413  Msat_ClauseVecFree( p->pvWatched[i] );
414  ABC_FREE( p->pvWatched );
415  Msat_QueueFree( p->pQueue );
416 
417  ABC_FREE( p->pAssigns );
418  ABC_FREE( p->pModel );
419  Msat_IntVecFree( p->vTrail );
420  Msat_IntVecFree( p->vTrailLim );
421  ABC_FREE( p->pReasons );
422  ABC_FREE( p->pLevel );
423 
424  Msat_MmStepStop( p->pMem, 0 );
425 
426  nClauses = Msat_ClauseVecReadSize( p->vAdjacents );
427  pClauses = Msat_ClauseVecReadArray( p->vAdjacents );
428  for ( i = 0; i < nClauses; i++ )
429  Msat_IntVecFree( (Msat_IntVec_t *)pClauses[i] );
430  Msat_ClauseVecFree( p->vAdjacents );
431  Msat_IntVecFree( p->vConeVars );
432  Msat_IntVecFree( p->vVarsUsed );
433 
434  ABC_FREE( p->pSeen );
435  Msat_IntVecFree( p->vReason );
436  Msat_IntVecFree( p->vTemp );
437  ABC_FREE( p );
438 }
439 
440 /**Function*************************************************************
441 
442  Synopsis [Prepares the solver to run on a subset of variables.]
443 
444  Description []
445 
446  SideEffects []
447 
448  SeeAlso []
449 
450 ***********************************************************************/
451 void Msat_SolverPrepare( Msat_Solver_t * p, Msat_IntVec_t * vVars )
452 {
453 
454  int i;
455  // undo the previous data
456  for ( i = 0; i < p->nVarsAlloc; i++ )
457  {
458  p->pAssigns[i] = MSAT_VAR_UNASSIGNED;
459  p->pReasons[i] = NULL;
460  p->pLevel[i] = -1;
461  p->pdActivity[i] = 0.0;
462  }
463 
464  // set the new variable order
465  Msat_OrderClean( p->pOrder, vVars );
466 
467  Msat_QueueClear( p->pQueue );
468  Msat_IntVecClear( p->vTrail );
469  Msat_IntVecClear( p->vTrailLim );
470  p->dProgress = 0.0;
471 }
472 
473 /**Function*************************************************************
474 
475  Synopsis [Sets up the truth tables.]
476 
477  Description []
478 
479  SideEffects []
480 
481  SeeAlso []
482 
483 ***********************************************************************/
484 void Msat_SolverSetupTruthTables( unsigned uTruths[][2] )
485 {
486  int m, v;
487  // set up the truth tables
488  for ( m = 0; m < 32; m++ )
489  for ( v = 0; v < 5; v++ )
490  if ( m & (1 << v) )
491  uTruths[v][0] |= (1 << m);
492  // make adjustments for the case of 6 variables
493  for ( v = 0; v < 5; v++ )
494  uTruths[v][1] = uTruths[v][0];
495  uTruths[5][0] = 0;
496  uTruths[5][1] = ~((unsigned)0);
497 }
498 
499 ////////////////////////////////////////////////////////////////////////
500 /// END OF FILE ///
501 ////////////////////////////////////////////////////////////////////////
502 
503 
504 ABC_NAMESPACE_IMPL_END
505 
memset
char * memset()
Msat_SolverReadFactors
float * Msat_SolverReadFactors(Msat_Solver_t *p)
Definition: msatSolverApi.c:70
Msat_Var_t
int Msat_Var_t
Definition: msatInt.h:66
Msat_SolverReadAdjacents
Msat_ClauseVec_t * Msat_SolverReadAdjacents(Msat_Solver_t *p)
Definition: msatSolverApi.c:104
Msat_ClauseFree
void Msat_ClauseFree(Msat_Solver_t *p, Msat_Clause_t *pC, int fRemoveWatched)
Definition: msatClause.c:223
Msat_SolverReadVarNum
int Msat_SolverReadVarNum(Msat_Solver_t *p)
FUNCTION DEFINITIONS ///.
Definition: msatSolverApi.c:47
Msat_SolverResize
void Msat_SolverResize(Msat_Solver_t *p, int nVarsAlloc)
Definition: msatSolverApi.c:242
Msat_SolverReadModelArray
int * Msat_SolverReadModelArray(Msat_Solver_t *p)
Definition: msatSolverApi.c:57
Msat_QueueFree
void Msat_QueueFree(Msat_Queue_t *p)
Definition: msatQueue.c:74
MSAT_VAR_UNASSIGNED
#define MSAT_VAR_UNASSIGNED
Definition: msatInt.h:68
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Msat_QueueClear
void Msat_QueueClear(Msat_Queue_t *p)
Definition: msatQueue.c:149
Msat_SolverClausesDecrement
void Msat_SolverClausesDecrement(Msat_Solver_t *p)
Definition: msatSolverApi.c:65
Msat_SolverReadLearned
Msat_ClauseVec_t * Msat_SolverReadLearned(Msat_Solver_t *p)
Definition: msatSolverApi.c:54
Msat_ClauseSetTypeA
void Msat_ClauseSetTypeA(Msat_Clause_t *pC, int fTypeA)
Definition: msatClause.c:264
Msat_ClauseVecReadEntry
Msat_Clause_t * Msat_ClauseVecReadEntry(Msat_ClauseVec_t *p, int i)
Definition: msatClauseVec.c:225
ABC_REALLOC
#define ABC_REALLOC(type, obj, num)
Definition: abc_global.h:233
Msat_OrderSetBounds
void Msat_OrderSetBounds(Msat_Order_t *p, int nVarsMax)
Definition: msatOrderH.c:101
Msat_IntVec_t_
Definition: msatInt.h:162
Msat_SolverFree
void Msat_SolverFree(Msat_Solver_t *p)
Definition: msatSolverApi.c:386
Msat_Type_t
Msat_Type_t
Definition: msat.h:50
Msat_IntVecClear
void Msat_IntVecClear(Msat_IntVec_t *p)
Definition: msatVec.c:335
Msat_SolverReadMem
Msat_MmStep_t * Msat_SolverReadMem(Msat_Solver_t *p)
Definition: msatSolverApi.c:60
Msat_SolverReadDecisionLevelArray
int * Msat_SolverReadDecisionLevelArray(Msat_Solver_t *p)
Definition: msatSolverApi.c:51
Msat_SolverReadInspects
int Msat_SolverReadInspects(Msat_Solver_t *p)
Definition: msatSolverApi.c:59
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
Msat_Clause_t
typedefABC_NAMESPACE_HEADER_START struct Msat_Clause_t_ Msat_Clause_t
INCLUDES ///.
Definition: msatInt.h:57
Msat_Lit_t
int Msat_Lit_t
Definition: msatInt.h:65
Msat_ClauseVecReadSize
int Msat_ClauseVecReadSize(Msat_ClauseVec_t *p)
Definition: msatClauseVec.c:101
Msat_SolverAlloc
Msat_Solver_t * Msat_SolverAlloc(int nVarsAlloc, double dClaInc, double dClaDecay, double dVarInc, double dVarDecay, int fVerbose)
Definition: msatSolverApi.c:154
Msat_SolverReadClauseNum
int Msat_SolverReadClauseNum(Msat_Solver_t *p)
Definition: msatSolverApi.c:48
Msat_IntVecReadSize
int Msat_IntVecReadSize(Msat_IntVec_t *p)
Definition: msatVec.c:233
Msat_SolverMarkClausesStart
void Msat_SolverMarkClausesStart(Msat_Solver_t *p)
Definition: msatSolverApi.c:69
Msat_SolverReadAssignsArray
int * Msat_SolverReadAssignsArray(Msat_Solver_t *p)
Definition: msatSolverApi.c:56
Msat_ClauseVecReadArray
Msat_Clause_t ** Msat_ClauseVecReadArray(Msat_ClauseVec_t *p)
Definition: msatClauseVec.c:85
Msat_ClauseVecPush
void Msat_ClauseVecPush(Msat_ClauseVec_t *p, Msat_Clause_t *Entry)
Definition: msatClauseVec.c:169
Msat_OrderFree
void Msat_OrderFree(Msat_Order_t *p)
Definition: msatOrderH.c:163
Msat_SolverReadVarValue
Msat_Type_t Msat_SolverReadVarValue(Msat_Solver_t *p, Msat_Var_t Var)
Definition: msatSolverApi.c:53
Msat_IntVecFill
void Msat_IntVecFill(Msat_IntVec_t *p, int nSize, int Entry)
Definition: msatVec.c:177
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Msat_SolverClausesDecrementL
void Msat_SolverClausesDecrementL(Msat_Solver_t *p)
Definition: msatSolverApi.c:67
Msat_ClauseVecClear
void Msat_ClauseVecClear(Msat_ClauseVec_t *p)
Definition: msatClauseVec.c:153
Msat_IntVecAlloc
Msat_IntVec_t * Msat_IntVecAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: msatVec.c:48
Msat_IntVecFree
void Msat_IntVecFree(Msat_IntVec_t *p)
Definition: msatVec.c:160
Msat_OrderAlloc
Msat_Order_t * Msat_OrderAlloc(Msat_Solver_t *pSat)
FUNCTION DEFINITIONS ///.
Definition: msatOrderH.c:78
Msat_SolverClausesIncrementL
void Msat_SolverClausesIncrementL(Msat_Solver_t *p)
Definition: msatSolverApi.c:66
Msat_SolverIncrementSeenId
int Msat_SolverIncrementSeenId(Msat_Solver_t *p)
Definition: msatSolverApi.c:62
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Msat_SolverMarkLastClauseTypeA
void Msat_SolverMarkLastClauseTypeA(Msat_Solver_t *p)
Definition: msatSolverApi.c:68
Msat_SolverSetupTruthTables
static ABC_NAMESPACE_IMPL_START void Msat_SolverSetupTruthTables(unsigned uTruths[][2])
DECLARATIONS ///.
Definition: msatSolverApi.c:484
Msat_SolverReadVarsUsed
Msat_IntVec_t * Msat_SolverReadVarsUsed(Msat_Solver_t *p)
Definition: msatSolverApi.c:136
Msat_SolverReadReasonArray
Msat_Clause_t ** Msat_SolverReadReasonArray(Msat_Solver_t *p)
Definition: msatSolverApi.c:52
Msat_SolverReadSeenArray
int * Msat_SolverReadSeenArray(Msat_Solver_t *p)
Definition: msatSolverApi.c:61
Msat_SolverClean
void Msat_SolverClean(Msat_Solver_t *p, int nVars)
Definition: msatSolverApi.c:307
Msat_SolverReadWatchedArray
Msat_ClauseVec_t ** Msat_SolverReadWatchedArray(Msat_Solver_t *p)
Definition: msatSolverApi.c:55
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Minisat::Var
int Var
Definition: SolverTypes.h:42
Msat_OrderClean
void Msat_OrderClean(Msat_Order_t *p, Msat_IntVec_t *vCone)
Definition: msatOrderH.c:120
Msat_SolverReadBackTracks
int Msat_SolverReadBackTracks(Msat_Solver_t *p)
Definition: msatSolverApi.c:58
Msat_ClauseVecAlloc
ABC_NAMESPACE_IMPL_START Msat_ClauseVec_t * Msat_ClauseVecAlloc(int nCap)
DECLARATIONS ///.
Definition: msatClauseVec.c:45
Msat_SolverReadClause
Msat_Clause_t * Msat_SolverReadClause(Msat_Solver_t *p, int Num)
Definition: msatSolverApi.c:83
assert
#define assert(ex)
Definition: util_old.h:213
Msat_SolverSetVerbosity
void Msat_SolverSetVerbosity(Msat_Solver_t *p, int fVerbose)
Definition: msatSolverApi.c:63
Msat_IntVecGrow
void Msat_IntVecGrow(Msat_IntVec_t *p, int nCapMin)
Definition: msatVec.c:299
Msat_QueueAlloc
Msat_Queue_t * Msat_QueueAlloc(int nVars)
FUNCTION DEFINITIONS ///.
Definition: msatQueue.c:53
Msat_SolverReadConeVars
Msat_IntVec_t * Msat_SolverReadConeVars(Msat_Solver_t *p)
Definition: msatSolverApi.c:120
Msat_SolverReadDecisionLevel
int Msat_SolverReadDecisionLevel(Msat_Solver_t *p)
Definition: msatSolverApi.c:50
Msat_MmStepStart
Msat_MmStep_t * Msat_MmStepStart(int nSteps)
Definition: msatMem.c:423
Msat_MmStep_t_
Definition: msatMem.c:69
Msat_ClauseVec_t_
Definition: msatInt.h:155
Msat_MmStepStop
void Msat_MmStepStop(Msat_MmStep_t *p, int fVerbose)
Definition: msatMem.c:458
Msat_SolverClausesIncrement
void Msat_SolverClausesIncrement(Msat_Solver_t *p)
Definition: msatSolverApi.c:64
Msat_Solver_t
typedefABC_NAMESPACE_HEADER_START struct Msat_Solver_t_ Msat_Solver_t
INCLUDES ///.
Definition: msat.h:42
Msat_SolverReadVarAllocNum
int Msat_SolverReadVarAllocNum(Msat_Solver_t *p)
Definition: msatSolverApi.c:49
Msat_SolverPrepare
void Msat_SolverPrepare(Msat_Solver_t *p, Msat_IntVec_t *vVars)
Definition: msatSolverApi.c:451
Msat_ClauseVecFree
void Msat_ClauseVecFree(Msat_ClauseVec_t *p)
Definition: msatClauseVec.c:68