queue.c File Reference

#include "inline.h"
#include "inlinequeue.h"
#include "print.h"

Include dependency graph for queue.c:

Go to the source code of this file.

Functions
ABC_NAMESPACE_IMPL_START void	kissat_init_queue (kissat *solver)
void	kissat_reset_search_of_queue (kissat *solver)
void	kissat_reassign_queue_stamps (kissat *solver)

Function Documentation

kissat_init_queue()

ABC_NAMESPACE_IMPL_START void kissat_init_queue

(

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

(

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

(

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);
}