queue.h File Reference

#include "global.h"

Include dependency graph for queue.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes
struct	links
struct	queue

Macros
#define	DISCONNECT   UINT_MAX
#define	DISCONNECTED(IDX)
#define	LINK(IDX)
#define	kissat_check_queue(...)

Typedefs
typedef struct links	links
typedef struct queue	queue

Functions
void	kissat_init_queue (struct kissat *)
void	kissat_reset_search_of_queue (struct kissat *)
void	kissat_reassign_queue_stamps (struct kissat *)

Macro Definition Documentation

DISCONNECT

#define DISCONNECT   UINT_MAX

Definition at line 7 of file queue.h.

DISCONNECTED

#define DISCONNECTED

(

IDX

)

Value:

((int) (IDX) < 0)

Definition at line 8 of file queue.h.

kissat_check_queue

#define kissat_check_queue

(

...

)

Value:

  do { \
  } while (0)

Definition at line 36 of file queue.h.

#define kissat_check_queue(...) \
  do { \
  } while (0)

LINK

#define LINK

(

IDX

)

Value:

(solver->links[KISSAT_assert ((IDX) < VARS), (IDX)])

Definition at line 31 of file queue.h.

Typedef Documentation

links

typedef struct links links

Definition at line 12 of file queue.h.

queue

typedef struct queue queue

Definition at line 13 of file queue.h.

Function Documentation

kissat_init_queue()

void kissat_init_queue

(

struct kissat *

solver

)

Definition at line 7 of file queue.c.

                                        {
  queue *queue = &solver->queue;
  queue->first = queue->last = DISCONNECT;
  KISSAT_assert (!queue->stamp);
  queue->search.idx = DISCONNECT;
  KISSAT_assert (!queue->search.stamp);
}

Here is the caller graph for this function:

kissat_reassign_queue_stamps()

void kissat_reassign_queue_stamps

(

struct kissat *

solver

)

Definition at line 24 of file queue.c.

                                                   {
  kissat_very_verbose (solver, "need to reassign enqueue stamps on queue");
 
  queue *queue = &solver->queue;
  links *links = solver->links;
  queue->stamp = 0;
 
  struct links *l;
  for (unsigned idx = queue->first; !DISCONNECTED (idx); idx = l->next)
    (l = links + idx)->stamp = ++queue->stamp;
 
  if (!DISCONNECTED (queue->search.idx))
    queue->search.stamp = links[queue->search.idx].stamp;
}

kissat_reset_search_of_queue()

void kissat_reset_search_of_queue

(

struct kissat *

solver

)

Definition at line 15 of file queue.c.

                                                   {
  LOG ("reset last search cache of queue");
  queue *queue = &solver->queue;
  links *links = solver->links;
  const unsigned last = queue->last;
  KISSAT_assert (!DISCONNECTED (last));
  kissat_update_queue (solver, links, last);
}