compact.h File Reference

#include "global.h"

Include dependency graph for compact.h:

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

Go to the source code of this file.

Functions
unsigned	kissat_compact_literals (struct kissat *, unsigned *mfixed_ptr)
void	kissat_finalize_compacting (struct kissat *, unsigned vars, unsigned mfixed)

Function Documentation

kissat_compact_literals()

unsigned kissat_compact_literals	(	struct kissat *	solver,
		unsigned *	mfixed_ptr )

Definition at line 21 of file compact.c.

                                                                        {
  INC (compacted);
#if !defined(KISSAT_QUIET) || !defined(KISSAT_NDEBUG)
  const unsigned active = solver->active;
#ifndef KISSAT_QUIET
  const unsigned inactive = solver->vars - active;
  kissat_phase (solver, "compact", GET (compacted),
                "compacting garbage collection "
                "(%u inactive variables %.2f%%)",
                inactive, kissat_percent (inactive, solver->vars));
#endif
#endif
#ifdef LOGGING
  KISSAT_assert (!solver->compacting);
  solver->compacting = true;
#endif
  unsigned mfixed = INVALID_LIT;
  unsigned vars = 0;
  for (all_variables (iidx)) {
    const flags *const flags = FLAGS (iidx);
    if (flags->eliminated)
      continue;
    const unsigned ilit = LIT (iidx);
    unsigned mlit;
    if (flags->fixed) {
      const value value = kissat_fixed (solver, ilit);
      KISSAT_assert (value);
      if (mfixed == INVALID_LIT) {
        mlit = mfixed = LIT (vars);
        LOG2 ("first fixed %u mapped to %u assigned to %d", ilit, mfixed,
              value);
        if (value < 0)
          mfixed = NOT (mfixed);
        LOG2 ("all other fixed mapped to %u", mfixed);
        vars++;
      } else if (value < 0) {
        mlit = NOT (mfixed);
        LOG2 ("negatively fixed %u mapped to %u", ilit, mlit);
      } else {
        mlit = mfixed;
        LOG2 ("positively fixed %u mapped to %u", ilit, mlit);
      }
    } else if (flags->active) {
      KISSAT_assert (flags->active);
      mlit = LIT (vars);
      LOG2 ("remapping %u to %u", ilit, mlit);
      vars++;
    } else {
      const int elit = PEEK_STACK (solver->export_, iidx);
      if (elit) {
        const unsigned eidx = ABS (elit);
        import *import = &PEEK_STACK (solver->import, eidx);
        KISSAT_assert (import->imported);
        KISSAT_assert (!import->eliminated);
        import->imported = false;
        LOG2 ("external variable %d not imported anymore", eidx);
        POKE_STACK (solver->export_, iidx, 0);
      } else
        LOG2 ("skipping inactive %u", ilit);
      continue;
    }
    KISSAT_assert (mlit <= ilit);
    KISSAT_assert (mlit != NOT (ilit));
    if (mlit == ilit)
      continue;
    const int elit = PEEK_STACK (solver->export_, iidx);
    const unsigned eidx = ABS (elit);
    if (elit < 0)
      mlit = NOT (mlit);
    reimport_literal (solver, eidx, mlit);
  }
  *mfixed_ptr = mfixed;
  LOG ("compacting to %u variables %.2f%% from %u", vars,
       kissat_percent (vars, solver->vars), solver->vars);
  KISSAT_assert (vars == active || vars == active + 1);
  return vars;
}

Here is the caller graph for this function:

kissat_finalize_compacting()

void kissat_finalize_compacting	(	struct kissat *	solver,
		unsigned	vars,
		unsigned	mfixed )

Definition at line 322 of file compact.c.

                                                  {
  LOG ("finalizing compacting");
  KISSAT_assert (vars <= solver->vars);
#ifdef LOGGING
  KISSAT_assert (solver->compacting);
#endif
  if (vars == solver->vars) {
#ifdef LOGGING
    solver->compacting = false;
    LOG ("number of variables does not change");
#endif
    return;
  }
 
  unsigned reduced = solver->vars - vars;
  LOG ("compacted number of variables from %u to %u", solver->vars, vars);
 
  bool first = true;
  for (all_variables (iidx)) {
    flags *flags = FLAGS (iidx);
    if (flags->fixed && first)
      first = false;
    else if (!flags->active)
      POKE_STACK (solver->export_, iidx, 0);
  }
 
  compact_trail (solver);
 
  for (all_variables (iidx)) {
    const unsigned ilit = LIT (iidx);
    const unsigned mlit = kissat_map_literal (solver, ilit, true);
    if (mlit != INVALID_LIT && ilit != mlit)
      compact_literal (solver, mlit, ilit);
  }
 
  if (mfixed != INVALID_LIT)
    compact_units (solver, mfixed);
 
  memset (solver->assigned + vars, 0, reduced * sizeof (assigned));
  memset (solver->flags + vars, 0, reduced * sizeof (flags));
  memset (solver->values + 2 * vars, 0, 2 * reduced * sizeof (value));
  memset (solver->watches + 2 * vars, 0, 2 * reduced * sizeof (watches));
 
  compact_queue (solver);
  compact_stack (solver, &solver->sweep_schedule);
  compact_scores (solver, SCORES, vars);
  compact_frames (solver);
  compact_export (solver, vars);
  compact_best_and_target_values (solver, vars);
 
  solver->vars = vars;
#ifdef LOGGING
  solver->compacting = false;
#endif
  kissat_decrease_size (solver);
}

Here is the call graph for this function:

Here is the caller graph for this function: