shrink.c File Reference

#include "shrink.h"
#include "allocate.h"
#include "inline.h"
#include "minimize.h"

Include dependency graph for shrink.c:

Go to the source code of this file.

Functions
void	kissat_shrink_clause (kissat *solver)

Function Documentation

kissat_shrink_clause()

void kissat_shrink_clause

(

kissat *

solver

)

Definition at line 362 of file shrink.c.

                                           {
  KISSAT_assert (GET_OPTION (minimize) > 0);
  KISSAT_assert (GET_OPTION (shrink) > 0);
  KISSAT_assert (!EMPTY_STACK (solver->clause));
 
  START (shrink);
 
  unsigned total_shrunken = 0;
  unsigned total_minimized = 0;
 
  unsigned *begin_lits = BEGIN_STACK (solver->clause);
  unsigned *end_lits = END_STACK (solver->clause);
 
  unsigned *end_block = END_STACK (solver->clause);
 
  while (end_block != begin_lits)
    end_block = minimize_and_shrink_block (
        solver, begin_lits, end_block, &total_shrunken, &total_minimized);
  unsigned *q = begin_lits;
  for (const unsigned *p = q; p != end_lits; p++) {
    const unsigned lit = *p;
    if (lit != INVALID_LIT)
      *q++ = lit;
  }
  LOG ("clause shrunken by %u literals (including %u minimized)",
       total_shrunken, total_minimized);
  KISSAT_assert (q + total_shrunken == end_lits);
  SET_END_OF_STACK (solver->clause, q);
  ADD (literals_shrunken, total_shrunken);
  ADD (literals_minshrunken, total_minimized);
 
  LOGTMP ("shrunken learned");
  kissat_reset_poisoned (solver);
 
  STOP (shrink);
}

Here is the call graph for this function:

Here is the caller graph for this function: