collect.h File Reference

#include "internal.h"
#include "global.h"

Include dependency graph for collect.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 bool	kissat_compacting (kissat *)
void	kissat_dense_collect (kissat *)
void	kissat_sparse_collect (kissat *, bool compact, reference start)
void	kissat_initial_sparse_collect (kissat *)
void	kissat_update_last_irredundant (kissat *, clause *last_irredundant)
void	kissat_update_first_reducible (kissat *, clause *first_reducible)

Function Documentation

kissat_compacting()

ABC_NAMESPACE_HEADER_START bool kissat_compacting

(

kissat *

solver

)

Definition at line 635 of file collect.c.

                                        {
  if (!GET_OPTION (compact))
    return false;
  unsigned inactive = solver->vars - solver->active;
  unsigned limit = GET_OPTION (compactlim) / 1e2 * solver->vars;
  bool compact = (inactive > limit);
  LOG ("%u inactive variables %.0f%% <= limit %u %.0f%%", inactive,
       kissat_percent (inactive, solver->vars), limit,
       kissat_percent (limit, solver->vars));
  return compact;
}

Here is the caller graph for this function:

kissat_dense_collect()

void kissat_dense_collect

(

kissat *

solver

)

Definition at line 730 of file collect.c.

                                           {
  KISSAT_assert (!solver->watching);
  KISSAT_assert (!solver->level);
  START (collect);
  INC (garbage_collections);
  INC (dense_garbage_collections);
  REPORT (1, 'G');
  dense_sweep_garbage_clauses (solver);
  REPORT (1, 'C');
  STOP (collect);
}

kissat_initial_sparse_collect()

void kissat_initial_sparse_collect

(

kissat *

solver

)

Definition at line 647 of file collect.c.

                                                    {
  KISSAT_assert (!solver->level);
  KISSAT_assert (!solver->inconsistent);
  KISSAT_assert (solver->watching);
  KISSAT_assert (kissat_trail_flushed (solver));
  if (solver->statistics_.units) {
    bool compact = GET_OPTION (compact);
    kissat_sparse_collect (solver, compact, 0);
  }
  REPORT (0, '.');
}

Here is the call graph for this function:

Here is the caller graph for this function:

kissat_sparse_collect()

void kissat_sparse_collect	(	kissat *	solver,
		bool	compact,
		reference	start )

Definition at line 610 of file collect.c.

                                                                           {
  KISSAT_assert (solver->watching);
  START (collect);
  INC (garbage_collections);
  INC (sparse_gcs);
  REPORT (1, 'G');
  unsigned vars, mfixed;
  if (compact)
    vars = kissat_compact_literals (solver, &mfixed);
  else {
    vars = solver->vars;
    mfixed = INVALID_LIT;
  }
  flush_all_watched_clauses (solver, compact, start);
  reference move = sparse_sweep_garbage_clauses (solver, compact, start);
  if (compact)
    kissat_finalize_compacting (solver, vars, mfixed);
  if (move != INVALID_REF)
    move_redundant_clauses_to_the_end (solver, move);
  rewatch_clauses (solver, start);
  REPORT (1, 'C');
  kissat_check_statistics (solver);
  STOP (collect);
}

Here is the call graph for this function:

Here is the caller graph for this function:

kissat_update_first_reducible()

void kissat_update_first_reducible	(	kissat *	solver,
		clause *	first_reducible )

Definition at line 185 of file collect.c.

                                                                       {
  KISSAT_assert (reducible);
  KISSAT_assert (!reducible->garbage);
  KISSAT_assert (reducible->redundant);
  if (solver->first_reducible != INVALID_REF) {
    reference ref = kissat_reference_clause (solver, reducible);
    if (ref >= solver->first_reducible) {
      LOG ("no need to update larger first reducible");
      return;
    }
  }
  clause *end = (clause *) END_STACK (solver->arena);
  update_first_reducible (solver, end, reducible);
}

kissat_update_last_irredundant()

void kissat_update_last_irredundant	(	kissat *	solver,
		clause *	last_irredundant )

Definition at line 200 of file collect.c.

                                                                          {
  KISSAT_assert (irredundant);
  KISSAT_assert (!irredundant->garbage);
  KISSAT_assert (!irredundant->redundant);
  if (solver->last_irredundant != INVALID_REF) {
    reference ref = kissat_reference_clause (solver, irredundant);
    if (ref <= solver->last_irredundant) {
      LOG ("no need to update smaller last irredundant");
      return;
    }
  }
  clause *end = (clause *) END_STACK (solver->arena);
  update_last_irredundant (solver, end, irredundant);
}

Here is the call graph for this function:

Here is the caller graph for this function: