dense.h File Reference

#include "watch.h"
#include "global.h"

Include dependency graph for dense.h:

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

Go to the source code of this file.

Functions
ABC_NAMESPACE_HEADER_START void	kissat_enter_dense_mode (struct kissat *, litpairs *saved_irredundant_binary_clauses)
void	kissat_resume_sparse_mode (struct kissat *, bool flush_eliminated, litpairs *)

Function Documentation

kissat_enter_dense_mode()

ABC_NAMESPACE_HEADER_START void kissat_enter_dense_mode	(	struct kissat *	solver,
		litpairs *	saved_irredundant_binary_clauses )

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	(	struct 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: