abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
msatSolverSearch.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [msatSolverSearch.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 [The search part 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: msatSolverSearch.c,v 1.0 2004/01/01 1:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "msatInt.h"
22 
24 
25 
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29 
30 static void Msat_SolverUndoOne( Msat_Solver_t * p );
31 static void Msat_SolverCancel( Msat_Solver_t * p );
33 static void Msat_SolverAnalyze( Msat_Solver_t * p, Msat_Clause_t * pC, Msat_IntVec_t * vLits_out, int * pLevel_out );
34 static void Msat_SolverReduceDB( Msat_Solver_t * p );
35 
36 ////////////////////////////////////////////////////////////////////////
37 /// FUNCTION DEFINITIONS ///
38 ////////////////////////////////////////////////////////////////////////
39 
40 /**Function*************************************************************
41 
42  Synopsis [Makes the next assumption (Lit).]
43 
44  Description [Returns FALSE if immediate conflict.]
45 
46  SideEffects []
47 
48  SeeAlso []
49 
50 ***********************************************************************/
52 {
53  assert( Msat_QueueReadSize(p->pQueue) == 0 );
54  if ( p->fVerbose )
55  printf(L_IND"assume("L_LIT")\n", L_ind, L_lit(Lit));
56  Msat_IntVecPush( p->vTrailLim, Msat_IntVecReadSize(p->vTrail) );
57 // assert( Msat_IntVecReadSize(p->vTrailLim) <= Msat_IntVecReadSize(p->vTrail) + 1 );
58 // assert( Msat_IntVecReadSize( p->vTrailLim ) < p->nVars );
59  return Msat_SolverEnqueue( p, Lit, NULL );
60 }
61 
62 /**Function*************************************************************
63 
64  Synopsis [Reverts one variable binding on the trail.]
65 
66  Description []
67 
68  SideEffects []
69 
70  SeeAlso []
71 
72 ***********************************************************************/
74 {
75  Msat_Lit_t Lit;
77  Lit = Msat_IntVecPop( p->vTrail );
78  Var = MSAT_LIT2VAR(Lit);
79  p->pAssigns[Var] = MSAT_VAR_UNASSIGNED;
80  p->pReasons[Var] = NULL;
81  p->pLevel[Var] = -1;
82 // Msat_OrderUndo( p->pOrder, Var );
83  Msat_OrderVarUnassigned( p->pOrder, Var );
84 
85  if ( p->fVerbose )
86  printf(L_IND"unbind("L_LIT")\n", L_ind, L_lit(Lit));
87 }
88 
89 /**Function*************************************************************
90 
91  Synopsis [Reverts to the state before last Msat_SolverAssume().]
92 
93  Description []
94 
95  SideEffects []
96 
97  SeeAlso []
98 
99 ***********************************************************************/
101 {
102  int c;
103  assert( Msat_QueueReadSize(p->pQueue) == 0 );
104  if ( p->fVerbose )
105  {
106  if ( Msat_IntVecReadSize(p->vTrail) != Msat_IntVecReadEntryLast(p->vTrailLim) )
107  {
108  Msat_Lit_t Lit;
109  Lit = Msat_IntVecReadEntry( p->vTrail, Msat_IntVecReadEntryLast(p->vTrailLim) );
110  printf(L_IND"cancel("L_LIT")\n", L_ind, L_lit(Lit));
111  }
112  }
113  for ( c = Msat_IntVecReadSize(p->vTrail) - Msat_IntVecPop( p->vTrailLim ); c != 0; c-- )
114  Msat_SolverUndoOne( p );
115 }
116 
117 /**Function*************************************************************
118 
119  Synopsis [Reverts to the state at given level.]
120 
121  Description []
122 
123  SideEffects []
124 
125  SeeAlso []
126 
127 ***********************************************************************/
129 {
130  while ( Msat_IntVecReadSize(p->vTrailLim) > Level )
132 }
133 
134 
135 /**Function*************************************************************
136 
137  Synopsis [Record a clause and drive backtracking.]
138 
139  Description [vLits[0] must contain the asserting literal.]
140 
141  SideEffects []
142 
143  SeeAlso []
144 
145 ***********************************************************************/
147 {
148  Msat_Clause_t * pC;
149  int Value;
150  assert( Msat_IntVecReadSize(vLits) != 0 );
151  Value = Msat_ClauseCreate( p, vLits, 1, &pC );
152  assert( Value );
153  Value = Msat_SolverEnqueue( p, Msat_IntVecReadEntry(vLits,0), pC );
154  assert( Value );
155  if ( pC )
156  Msat_ClauseVecPush( p->vLearned, pC );
157  return pC;
158 }
159 
160 /**Function*************************************************************
161 
162  Synopsis [Enqueues one variable assignment.]
163 
164  Description [Puts a new fact on the propagation queue and immediately
165  updates the variable value. Should a conflict arise, FALSE is returned.
166  Otherwise returns TRUE.]
167 
168  SideEffects []
169 
170  SeeAlso []
171 
172 ***********************************************************************/
174 {
175  Msat_Var_t Var = MSAT_LIT2VAR(Lit);
176 
177  // skip literals that are not in the current cone
178  if ( !Msat_IntVecReadEntry( p->vVarsUsed, Var ) )
179  return 1;
180 
181 // assert( Msat_QueueReadSize(p->pQueue) == Msat_IntVecReadSize(p->vTrail) );
182  // if the literal is assigned
183  // return 1 if the assignment is consistent
184  // return 0 if the assignment is inconsistent (conflict)
185  if ( p->pAssigns[Var] != MSAT_VAR_UNASSIGNED )
186  return p->pAssigns[Var] == Lit;
187  // new fact - store it
188  if ( p->fVerbose )
189  {
190 // printf(L_IND"bind("L_LIT")\n", L_ind, L_lit(Lit));
191  printf(L_IND"bind("L_LIT") ", L_ind, L_lit(Lit));
193  }
194  p->pAssigns[Var] = Lit;
195  p->pLevel[Var] = Msat_IntVecReadSize(p->vTrailLim);
196 // p->pReasons[Var] = p->pLevel[Var]? pC: NULL;
197  p->pReasons[Var] = pC;
198  Msat_IntVecPush( p->vTrail, Lit );
199  Msat_QueueInsert( p->pQueue, Lit );
200 
201  Msat_OrderVarAssigned( p->pOrder, Var );
202  return 1;
203 }
204 
205 /**Function*************************************************************
206 
207  Synopsis [Propagates the assignments in the queue.]
208 
209  Description [Propagates all enqueued facts. If a conflict arises,
210  the conflicting clause is returned, otherwise NULL.]
211 
212  SideEffects [The propagation queue is empty, even if there was a conflict.]
213 
214  SeeAlso []
215 
216 ***********************************************************************/
218 {
219  Msat_ClauseVec_t ** pvWatched = p->pvWatched;
220  Msat_Clause_t ** pClauses;
221  Msat_Clause_t * pConflict;
222  Msat_Lit_t Lit, Lit_out;
223  int i, j, nClauses;
224 
225  // propagate all the literals in the queue
226  while ( (Lit = Msat_QueueExtract( p->pQueue )) >= 0 )
227  {
228  p->Stats.nPropagations++;
229  // get the clauses watched by this literal
230  nClauses = Msat_ClauseVecReadSize( pvWatched[Lit] );
231  pClauses = Msat_ClauseVecReadArray( pvWatched[Lit] );
232  // go through the watched clauses and decide what to do with them
233  for ( i = j = 0; i < nClauses; i++ )
234  {
235  p->Stats.nInspects++;
236  // clear the returned literal
237  Lit_out = -1;
238  // propagate the clause
239  if ( !Msat_ClausePropagate( pClauses[i], Lit, p->pAssigns, &Lit_out ) )
240  { // the clause is unit
241  // "Lit_out" contains the new assignment to be enqueued
242  if ( Msat_SolverEnqueue( p, Lit_out, pClauses[i] ) )
243  { // consistent assignment
244  // no changes to the implication queue; the watch is the same too
245  pClauses[j++] = pClauses[i];
246  continue;
247  }
248  // remember the reason of conflict (will be returned)
249  pConflict = pClauses[i];
250  // leave the remaning clauses in the same watched list
251  for ( ; i < nClauses; i++ )
252  pClauses[j++] = pClauses[i];
253  Msat_ClauseVecShrink( pvWatched[Lit], j );
254  // clear the propagation queue
255  Msat_QueueClear( p->pQueue );
256  return pConflict;
257  }
258  // the clause is not unit
259  // in this case "Lit_out" contains the new watch if it has changed
260  if ( Lit_out >= 0 )
261  Msat_ClauseVecPush( pvWatched[Lit_out], pClauses[i] );
262  else // the watch did not change
263  pClauses[j++] = pClauses[i];
264  }
265  Msat_ClauseVecShrink( pvWatched[Lit], j );
266  }
267  return NULL;
268 }
269 
270 /**Function*************************************************************
271 
272  Synopsis [Simplifies the data base.]
273 
274  Description [Simplify all constraints according to the current top-level
275  assigment (redundant constraints may be removed altogether).]
276 
277  SideEffects []
278 
279  SeeAlso []
280 
281 ***********************************************************************/
283 {
284  Msat_ClauseVec_t * vClauses;
285  Msat_Clause_t ** pClauses;
286  int nClauses, Type, i, j;
287  int * pAssigns;
288  int Counter;
289 
291  if ( Msat_SolverPropagate(p) != NULL )
292  return 0;
293 //Msat_SolverPrintClauses( p );
294 //Msat_SolverPrintAssignment( p );
295 //printf( "Simplification\n" );
296 
297  // simplify and reassign clause numbers
298  Counter = 0;
299  pAssigns = Msat_SolverReadAssignsArray( p );
300  for ( Type = 0; Type < 2; Type++ )
301  {
302  vClauses = Type? p->vLearned : p->vClauses;
303  nClauses = Msat_ClauseVecReadSize( vClauses );
304  pClauses = Msat_ClauseVecReadArray( vClauses );
305  for ( i = j = 0; i < nClauses; i++ )
306  if ( Msat_ClauseSimplify( pClauses[i], pAssigns ) )
307  Msat_ClauseFree( p, pClauses[i], 1 );
308  else
309  {
310  pClauses[j++] = pClauses[i];
311  Msat_ClauseSetNum( pClauses[i], Counter++ );
312  }
313  Msat_ClauseVecShrink( vClauses, j );
314  }
315  p->nClauses = Counter;
316  return 1;
317 }
318 
319 /**Function*************************************************************
320 
321  Synopsis [Cleans the clause databased from the useless learnt clauses.]
322 
323  Description [Removes half of the learnt clauses, minus the clauses locked
324  by the current assignment. Locked clauses are clauses that are reason
325  to a some assignment.]
326 
327  SideEffects []
328 
329  SeeAlso []
330 
331 ***********************************************************************/
333 {
334  Msat_Clause_t ** pLearned;
335  int nLearned, i, j;
336  double dExtraLim = p->dClaInc / Msat_ClauseVecReadSize(p->vLearned);
337  // Remove any clause below this activity
338 
339  // sort the learned clauses in the increasing order of activity
340  Msat_SolverSortDB( p );
341 
342  // discard the first half the clauses (the less active ones)
343  nLearned = Msat_ClauseVecReadSize( p->vLearned );
344  pLearned = Msat_ClauseVecReadArray( p->vLearned );
345  for ( i = j = 0; i < nLearned / 2; i++ )
346  if ( !Msat_ClauseIsLocked( p, pLearned[i]) )
347  Msat_ClauseFree( p, pLearned[i], 1 );
348  else
349  pLearned[j++] = pLearned[i];
350  // filter the more active clauses and leave those above the limit
351  for ( ; i < nLearned; i++ )
352  if ( !Msat_ClauseIsLocked( p, pLearned[i] ) &&
353  Msat_ClauseReadActivity(pLearned[i]) < dExtraLim )
354  Msat_ClauseFree( p, pLearned[i], 1 );
355  else
356  pLearned[j++] = pLearned[i];
357  Msat_ClauseVecShrink( p->vLearned, j );
358 }
359 
360 /**Function*************************************************************
361 
362  Synopsis [Removes the learned clauses.]
363 
364  Description []
365 
366  SideEffects []
367 
368  SeeAlso []
369 
370 ***********************************************************************/
372 {
373  Msat_Clause_t ** pLearned;
374  int nLearned, i;
375 
376  // discard the learned clauses
377  nLearned = Msat_ClauseVecReadSize( p->vLearned );
378  pLearned = Msat_ClauseVecReadArray( p->vLearned );
379  for ( i = 0; i < nLearned; i++ )
380  {
381  assert( !Msat_ClauseIsLocked( p, pLearned[i]) );
382 
383  Msat_ClauseFree( p, pLearned[i], 1 );
384  }
385  Msat_ClauseVecShrink( p->vLearned, 0 );
386  p->nClauses = Msat_ClauseVecReadSize(p->vClauses);
387 
388  for ( i = 0; i < p->nVarsAlloc; i++ )
389  p->pReasons[i] = NULL;
390 }
391 
392 /**Function*************************************************************
393 
394  Synopsis [Removes the recently added clauses.]
395 
396  Description []
397 
398  SideEffects []
399 
400  SeeAlso []
401 
402 ***********************************************************************/
404 {
405  Msat_Clause_t ** pLearned, ** pClauses;
406  int nLearned, nClauses, i;
407 
408  // discard the learned clauses
409  nClauses = Msat_ClauseVecReadSize( p->vClauses );
410  pClauses = Msat_ClauseVecReadArray( p->vClauses );
411  for ( i = p->nClausesStart; i < nClauses; i++ )
412  {
413 // assert( !Msat_ClauseIsLocked( p, pClauses[i]) );
414  Msat_ClauseFree( p, pClauses[i], 1 );
415  }
416  Msat_ClauseVecShrink( p->vClauses, p->nClausesStart );
417 
418  // discard the learned clauses
419  nLearned = Msat_ClauseVecReadSize( p->vLearned );
420  pLearned = Msat_ClauseVecReadArray( p->vLearned );
421  for ( i = 0; i < nLearned; i++ )
422  {
423 // assert( !Msat_ClauseIsLocked( p, pLearned[i]) );
424  Msat_ClauseFree( p, pLearned[i], 1 );
425  }
426  Msat_ClauseVecShrink( p->vLearned, 0 );
427  p->nClauses = Msat_ClauseVecReadSize(p->vClauses);
428 /*
429  // undo the previous data
430  for ( i = 0; i < p->nVarsAlloc; i++ )
431  {
432  p->pAssigns[i] = MSAT_VAR_UNASSIGNED;
433  p->pReasons[i] = NULL;
434  p->pLevel[i] = -1;
435  p->pdActivity[i] = 0.0;
436  }
437  Msat_OrderClean( p->pOrder, p->nVars, NULL );
438  Msat_QueueClear( p->pQueue );
439 */
440 }
441 
442 
443 
444 /**Function*************************************************************
445 
446  Synopsis [Analyze conflict and produce a reason clause.]
447 
448  Description [Current decision level must be greater than root level.]
449 
450  SideEffects [vLits_out[0] is the asserting literal at level pLevel_out.]
451 
452  SeeAlso []
453 
454 ***********************************************************************/
455 void Msat_SolverAnalyze( Msat_Solver_t * p, Msat_Clause_t * pC, Msat_IntVec_t * vLits_out, int * pLevel_out )
456 {
457  Msat_Lit_t LitQ, Lit = MSAT_LIT_UNASSIGNED;
458  Msat_Var_t VarQ, Var;
459  int * pReasonArray, nReasonSize;
460  int j, pathC = 0, nLevelCur = Msat_IntVecReadSize(p->vTrailLim);
461  int iStep = Msat_IntVecReadSize(p->vTrail) - 1;
462 
463  // increment the seen counter
464  p->nSeenId++;
465  // empty the vector array
466  Msat_IntVecClear( vLits_out );
467  Msat_IntVecPush( vLits_out, -1 ); // (leave room for the asserting literal)
468  *pLevel_out = 0;
469  do {
470  assert( pC != NULL ); // (otherwise should be UIP)
471  // get the reason of conflict
472  Msat_ClauseCalcReason( p, pC, Lit, p->vReason );
473  nReasonSize = Msat_IntVecReadSize( p->vReason );
474  pReasonArray = Msat_IntVecReadArray( p->vReason );
475  for ( j = 0; j < nReasonSize; j++ ) {
476  LitQ = pReasonArray[j];
477  VarQ = MSAT_LIT2VAR(LitQ);
478  if ( p->pSeen[VarQ] != p->nSeenId ) {
479  p->pSeen[VarQ] = p->nSeenId;
480 
481  // added to better fine-tune the search
482  Msat_SolverVarBumpActivity( p, LitQ );
483 
484  // skip all the literals on this decision level
485  if ( p->pLevel[VarQ] == nLevelCur )
486  pathC++;
487  else if ( p->pLevel[VarQ] > 0 ) {
488  // add the literals on other decision levels but
489  // exclude variables from decision level 0
490  Msat_IntVecPush( vLits_out, MSAT_LITNOT(LitQ) );
491  if ( *pLevel_out < p->pLevel[VarQ] )
492  *pLevel_out = p->pLevel[VarQ];
493  }
494  }
495  }
496  // Select next clause to look at:
497  do {
498 // Lit = Msat_IntVecReadEntryLast(p->vTrail);
499  Lit = Msat_IntVecReadEntry( p->vTrail, iStep-- );
500  Var = MSAT_LIT2VAR(Lit);
501  pC = p->pReasons[Var];
502 // Msat_SolverUndoOne( p );
503  } while ( p->pSeen[Var] != p->nSeenId );
504  pathC--;
505  } while ( pathC > 0 );
506  // we do not unbind the variables above
507  // this will be done after conflict analysis
508 
509  Msat_IntVecWriteEntry( vLits_out, 0, MSAT_LITNOT(Lit) );
510  if ( p->fVerbose )
511  {
512  printf( L_IND"Learnt {", L_ind );
513  nReasonSize = Msat_IntVecReadSize( vLits_out );
514  pReasonArray = Msat_IntVecReadArray( vLits_out );
515  for ( j = 0; j < nReasonSize; j++ )
516  printf(" "L_LIT, L_lit(pReasonArray[j]));
517  printf(" } at level %d\n", *pLevel_out);
518  }
519 }
520 
521 /**Function*************************************************************
522 
523  Synopsis [The search procedure called between the restarts.]
524 
525  Description [Search for a satisfying solution as long as the number of
526  conflicts does not exceed the limit (nConfLimit) while keeping the number
527  of learnt clauses below the provided limit (nLearnedLimit). NOTE! Use
528  negative value for nConfLimit or nLearnedLimit to indicate infinity.]
529 
530  SideEffects []
531 
532  SeeAlso []
533 
534 ***********************************************************************/
535 Msat_Type_t Msat_SolverSearch( Msat_Solver_t * p, int nConfLimit, int nLearnedLimit, int nBackTrackLimit, Msat_SearchParams_t * pPars )
536 {
537  Msat_Clause_t * pConf;
538  Msat_Var_t Var;
539  int nLevelBack, nConfs, nAssigns, Value;
540  int i;
541 
542  assert( Msat_SolverReadDecisionLevel(p) == p->nLevelRoot );
543  p->Stats.nStarts++;
544  p->dVarDecay = 1 / pPars->dVarDecay;
545  p->dClaDecay = 1 / pPars->dClaDecay;
546 
547  // reset the activities
548  for ( i = 0; i < p->nVars; i++ )
549  p->pdActivity[i] = (double)p->pFactors[i];
550 // p->pdActivity[i] = 0.0;
551 
552  nConfs = 0;
553  while ( 1 )
554  {
555  pConf = Msat_SolverPropagate( p );
556  if ( pConf != NULL ){
557  // CONFLICT
558  if ( p->fVerbose )
559  {
560 // printf(L_IND"**CONFLICT**\n", L_ind);
561  printf(L_IND"**CONFLICT** ", L_ind);
562  Msat_ClausePrintSymbols( pConf );
563  }
564  // count conflicts
565  p->Stats.nConflicts++;
566  nConfs++;
567 
568  // if top level, return UNSAT
569  if ( Msat_SolverReadDecisionLevel(p) == p->nLevelRoot )
570  return MSAT_FALSE;
571 
572  // perform conflict analysis
573  Msat_SolverAnalyze( p, pConf, p->vTemp, &nLevelBack );
574  Msat_SolverCancelUntil( p, (p->nLevelRoot > nLevelBack)? p->nLevelRoot : nLevelBack );
575  Msat_SolverRecord( p, p->vTemp );
576 
577  // it is important that recording is done after cancelling
578  // because canceling cleans the queue while recording adds to it
581 
582  }
583  else{
584  // NO CONFLICT
585  if ( Msat_IntVecReadSize(p->vTrailLim) == 0 ) {
586  // Simplify the set of problem clauses:
587 // Value = Msat_SolverSimplifyDB(p);
588 // assert( Value );
589  }
590  nAssigns = Msat_IntVecReadSize( p->vTrail );
591  if ( nLearnedLimit >= 0 && Msat_ClauseVecReadSize(p->vLearned) >= nLearnedLimit + nAssigns ) {
592  // Reduce the set of learnt clauses:
594  }
595 
596  Var = Msat_OrderVarSelect( p->pOrder );
597  if ( Var == MSAT_ORDER_UNKNOWN ) {
598  // Model found and stored in p->pAssigns
599  memcpy( p->pModel, p->pAssigns, sizeof(int) * p->nVars );
600  Msat_QueueClear( p->pQueue );
601  Msat_SolverCancelUntil( p, p->nLevelRoot );
602  return MSAT_TRUE;
603  }
604  if ( nConfLimit > 0 && nConfs > nConfLimit ) {
605  // Reached bound on number of conflicts:
606  p->dProgress = Msat_SolverProgressEstimate( p );
607  Msat_QueueClear( p->pQueue );
608  Msat_SolverCancelUntil( p, p->nLevelRoot );
609  return MSAT_UNKNOWN;
610  }
611  else if ( nBackTrackLimit > 0 && (int)p->Stats.nConflicts - p->nBackTracks > nBackTrackLimit ) {
612  // Reached bound on number of conflicts:
613  Msat_QueueClear( p->pQueue );
614  Msat_SolverCancelUntil( p, p->nLevelRoot );
615  return MSAT_UNKNOWN;
616  }
617  else{
618  // New variable decision:
619  p->Stats.nDecisions++;
620  assert( Var != MSAT_ORDER_UNKNOWN && Var >= 0 && Var < p->nVars );
621  Value = Msat_SolverAssume(p, MSAT_VAR2LIT(Var,0) );
622  assert( Value );
623  }
624  }
625  }
626 }
627 
628 ////////////////////////////////////////////////////////////////////////
629 /// END OF FILE ///
630 ////////////////////////////////////////////////////////////////////////
631 
632 
634 
int Msat_SolverReadDecisionLevel(Msat_Solver_t *p)
Definition: msatSolverApi.c:50
#define MSAT_LIT_UNASSIGNED
Definition: msatInt.h:69
int Msat_Var_t
Definition: msatInt.h:66
void Msat_SolverClaDecayActivity(Msat_Solver_t *p)
Definition: msatActivity.c:128
void Msat_ClauseFree(Msat_Solver_t *p, Msat_Clause_t *pC, int fRemoveWatched)
Definition: msatClause.c:223
void Msat_OrderVarAssigned(Msat_Order_t *p, int Var)
Definition: msatOrderH.c:220
#define MSAT_VAR_UNASSIGNED
Definition: msatInt.h:68
#define MSAT_ORDER_UNKNOWN
Definition: msatInt.h:70
static Llb_Mgr_t * p
Definition: llb3Image.c:950
#define L_lit(p)
Definition: satSolver.c:43
void Msat_QueueClear(Msat_Queue_t *p)
Definition: msatQueue.c:149
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 Msat_ClausePropagate(Msat_Clause_t *pC, Msat_Lit_t Lit, int *pAssigns, Msat_Lit_t *pLit_out)
Definition: msatClause.c:335
int Msat_IntVecReadEntryLast(Msat_IntVec_t *p)
Definition: msatVec.c:283
void Msat_QueueInsert(Msat_Queue_t *p, int Lit)
Definition: msatQueue.c:107
Msat_Clause_t * Msat_SolverPropagate(Msat_Solver_t *p)
#define MSAT_LIT2VAR(l)
Definition: msat.h:59
Msat_Type_t
Definition: msat.h:50
void Msat_IntVecClear(Msat_IntVec_t *p)
Definition: msatVec.c:335
#define L_ind
Definition: satSolver.c:41
Msat_Type_t Msat_SolverSearch(Msat_Solver_t *p, int nConfLimit, int nLearnedLimit, int nBackTrackLimit, Msat_SearchParams_t *pPars)
char * memcpy()
Definition: msat.h:50
int Msat_QueueReadSize(Msat_Queue_t *p)
Definition: msatQueue.c:91
int Msat_ClauseIsLocked(Msat_Solver_t *p, Msat_Clause_t *pC)
Definition: msatClause.c:278
typedefABC_NAMESPACE_HEADER_START struct Msat_Clause_t_ Msat_Clause_t
INCLUDES ///.
Definition: msatInt.h:57
int Msat_Lit_t
Definition: msatInt.h:65
int Msat_ClauseVecReadSize(Msat_ClauseVec_t *p)
void Msat_ClauseVecShrink(Msat_ClauseVec_t *p, int nSizeNew)
#define L_LIT
Definition: satSolver.c:42
ABC_NAMESPACE_IMPL_START void Msat_SolverVarBumpActivity(Msat_Solver_t *p, Msat_Lit_t Lit)
DECLARATIONS ///.
Definition: msatActivity.c:45
int Msat_OrderVarSelect(Msat_Order_t *p)
Definition: msatOrderH.c:183
void Msat_ClauseSetNum(Msat_Clause_t *pC, int Num)
Definition: msatClause.c:263
void Msat_SolverVarDecayActivity(Msat_Solver_t *p)
GLOBAL VARIABLES ///.
Definition: msatActivity.c:69
static ABC_NAMESPACE_IMPL_START void Msat_SolverUndoOne(Msat_Solver_t *p)
DECLARATIONS ///.
int Msat_IntVecReadSize(Msat_IntVec_t *p)
Definition: msatVec.c:233
#define MSAT_LITNOT(l)
Definition: msat.h:57
static void Msat_SolverAnalyze(Msat_Solver_t *p, Msat_Clause_t *pC, Msat_IntVec_t *vLits_out, int *pLevel_out)
void Msat_IntVecPush(Msat_IntVec_t *p, int Entry)
Definition: msatVec.c:351
int * Msat_SolverReadAssignsArray(Msat_Solver_t *p)
Definition: msatSolverApi.c:56
void Msat_SolverSortDB(Msat_Solver_t *p)
FUNCTION DEFINITIONS ///.
Definition: msatSort.c:61
void Msat_SolverRemoveLearned(Msat_Solver_t *p)
int Msat_ClauseSimplify(Msat_Clause_t *pC, int *pAssigns)
Definition: msatClause.c:374
Msat_Clause_t ** Msat_ClauseVecReadArray(Msat_ClauseVec_t *p)
Definition: msatClauseVec.c:85
static void Msat_SolverCancel(Msat_Solver_t *p)
int Msat_IntVecPop(Msat_IntVec_t *p)
Definition: msatVec.c:425
void Msat_SolverRemoveMarked(Msat_Solver_t *p)
void Msat_ClauseVecPush(Msat_ClauseVec_t *p, Msat_Clause_t *Entry)
void Msat_SolverCancelUntil(Msat_Solver_t *p, int Level)
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
int Msat_IntVecReadEntry(Msat_IntVec_t *p, int i)
Definition: msatVec.c:249
static int Counter
int Msat_SolverAssume(Msat_Solver_t *p, Msat_Lit_t Lit)
FUNCTION DEFINITIONS ///.
int Msat_SolverSimplifyDB(Msat_Solver_t *p)
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
#define L_IND
Definition: satSolver.c:40
static Msat_Clause_t * Msat_SolverRecord(Msat_Solver_t *p, Msat_IntVec_t *vLits)
int * Msat_IntVecReadArray(Msat_IntVec_t *p)
Definition: msatVec.c:217
static void Msat_SolverReduceDB(Msat_Solver_t *p)
int Var
Definition: SolverTypes.h:42
#define MSAT_VAR2LIT(v, s)
Definition: msat.h:56
void Msat_IntVecWriteEntry(Msat_IntVec_t *p, int i, int Entry)
Definition: msatVec.c:266
#define assert(ex)
Definition: util_old.h:213
void Msat_ClausePrintSymbols(Msat_Clause_t *pC)
Definition: msatClause.c:515
void Msat_OrderVarUnassigned(Msat_Order_t *p, int Var)
Definition: msatOrderH.c:235
int Msat_QueueExtract(Msat_Queue_t *p)
Definition: msatQueue.c:131
double Msat_SolverProgressEstimate(Msat_Solver_t *p)
int Msat_SolverEnqueue(Msat_Solver_t *p, Msat_Lit_t Lit, Msat_Clause_t *pC)
int Msat_ClauseCreate(Msat_Solver_t *p, Msat_IntVec_t *vLits, int fLearned, Msat_Clause_t **pClause_out)
FUNCTION DEFINITIONS ///.
Definition: msatClause.c:58
typedefABC_NAMESPACE_HEADER_START struct Msat_Solver_t_ Msat_Solver_t
INCLUDES ///.
Definition: msat.h:42
float Msat_ClauseReadActivity(Msat_Clause_t *pC)
Definition: msatClause.c:295