dense.c File Reference

#include "dense.h"
#include "inline.h"
#include "proprobe.h"
#include "propsearch.h"
#include "trail.h"
#include "sort.c"
#include <string.h>

Include dependency graph for dense.c:

Go to the source code of this file.

Macros
#define	INLINE_SORT

Functions
void	kissat_enter_dense_mode (kissat *solver, litpairs *irredundant)
void	kissat_resume_sparse_mode (kissat *solver, bool flush_eliminated, litpairs *irredundant)

Macro Definition Documentation

INLINE_SORT

#define INLINE_SORT

Definition at line 1 of file dense.c.

Function Documentation

kissat_enter_dense_mode()

void kissat_enter_dense_mode	(	kissat *	solver,
		litpairs *	irredundant )

Definition at line 101 of file dense.c.

                                                                     {
  KISSAT_assert (!solver->level);
  KISSAT_assert (solver->watching);
  KISSAT_assert (kissat_propagated (solver));
  LOG ("entering dense mode with full occurrence lists");
  if (irredundant)
    flush_large_watches (solver, irredundant);
  else
    kissat_flush_large_watches (solver);
  LOG ("switched to full occurrence lists");
  solver->watching = false;
}

Here is the call graph for this function:

Here is the caller graph for this function:

kissat_resume_sparse_mode()

void kissat_resume_sparse_mode	(	kissat *	solver,
		bool	flush_eliminated,
		litpairs *	irredundant )

Definition at line 201 of file dense.c.

                                                       {
  KISSAT_assert (!solver->level);
  KISSAT_assert (!solver->watching);
  if (solver->inconsistent)
    return;
  LOG ("resuming sparse mode watching clauses");
  kissat_flush_large_connected (solver);
  LOG ("switched to watching clauses");
  solver->watching = true;
  if (irredundant) {
    LOG ("resuming watching %zu irredundant binaries",
         SIZE_STACK (*irredundant));
    resume_watching_irredundant_binaries (solver, irredundant);
  }
  if (flush_eliminated)
    resume_watching_large_clauses_after_elimination (solver);
  else
    kissat_watch_large_clauses (solver);
  LOG ("forcing to propagate units on all clauses");
  kissat_reset_propagate (solver);
 
  clause *conflict;
  if (solver->probing)
    conflict = kissat_probing_propagate (solver, 0, true);
  else
    conflict = kissat_search_propagate (solver);
 
#ifndef KISSAT_NDEBUG
  if (conflict)
    KISSAT_assert (solver->inconsistent);
  else
    KISSAT_assert (kissat_trail_flushed (solver));
#else
  (void) conflict;
#endif
}

Here is the call graph for this function:

Here is the caller graph for this function: