minimize.c File Reference

#include "minimize.h"
#include "inline.h"

Include dependency graph for minimize.c:

Go to the source code of this file.

Functions
bool	kissat_minimize_literal (kissat *solver, unsigned lit, bool lit_in_clause)
void	kissat_reset_poisoned (kissat *solver)
void	kissat_minimize_clause (kissat *solver)

Function Documentation

kissat_minimize_clause()

void kissat_minimize_clause

(

kissat *

solver

)

Definition at line 157 of file minimize.c.

                                             {
  START (minimize);
 
  KISSAT_assert (EMPTY_STACK (solver->minimize));
  KISSAT_assert (EMPTY_STACK (solver->removable));
  KISSAT_assert (EMPTY_STACK (solver->poisoned));
  KISSAT_assert (!EMPTY_STACK (solver->clause));
 
  unsigned *lits = BEGIN_STACK (solver->clause);
  unsigned *end = END_STACK (solver->clause);
 
  assigned *assigned = solver->assigned;
#ifndef KISSAT_NDEBUG
  KISSAT_assert (lits < end);
  const unsigned not_uip = lits[0];
  KISSAT_assert (assigned[IDX (not_uip)].level == solver->level);
#endif
  for (const unsigned *p = lits; p != end; p++)
    kissat_push_removable (solver, assigned, IDX (*p));
 
  if (GET_OPTION (shrink) > 2) {
    STOP (minimize);
    return;
  }
 
  unsigned minimized = 0;
 
  for (unsigned *p = end; --p > lits;) {
    const unsigned lit = *p;
    KISSAT_assert (lit != not_uip);
    if (minimize_literal (solver, true, assigned, lit, 0)) {
      LOG ("minimized literal %s", LOGLIT (lit));
      *p = INVALID_LIT;
      minimized++;
    } else
      LOG ("keeping literal %s", LOGLIT (lit));
  }
 
  unsigned *q = lits;
  for (const unsigned *p = lits; p != end; p++) {
    const unsigned lit = *p;
    if (lit != INVALID_LIT)
      *q++ = lit;
  }
  KISSAT_assert (q + minimized == end);
  SET_END_OF_STACK (solver->clause, q);
  LOG ("clause minimization removed %u literals", minimized);
 
  KISSAT_assert (!solver->probing);
  ADD (literals_minimized, minimized);
 
  LOGTMP ("minimized learned");
 
  kissat_reset_poisoned (solver);
 
  STOP (minimize);
}

Here is the call graph for this function:

Here is the caller graph for this function:

kissat_minimize_literal()

bool kissat_minimize_literal	(	kissat *	solver,
		unsigned	lit,
		bool	lit_in_clause )

Definition at line 138 of file minimize.c.

                                                  {
  KISSAT_assert (EMPTY_STACK (solver->minimize));
  return minimize_literal (solver, false, solver->assigned, lit,
                           !lit_in_clause);
}

kissat_reset_poisoned()

void kissat_reset_poisoned

(

kissat *

solver

)

Definition at line 145 of file minimize.c.

                                            {
  LOG ("reset %zu poisoned variables", SIZE_STACK (solver->poisoned));
  assigned *assigned = solver->assigned;
  for (all_stack (unsigned, idx, solver->poisoned)) {
    KISSAT_assert (idx < VARS);
    struct assigned *a = assigned + idx;
    KISSAT_assert (a->poisoned);
    a->poisoned = false;
  }
  CLEAR_STACK (solver->poisoned);
}

Here is the caller graph for this function: