flags.c File Reference

#include "inline.h"
#include "inlineheap.h"
#include "inlinequeue.h"

Include dependency graph for flags.c:

Go to the source code of this file.

Functions
void	kissat_activate_literal (kissat *solver, unsigned lit)
void	kissat_activate_literals (kissat *solver, unsigned size, unsigned *lits)
void	kissat_mark_fixed_literal (kissat *solver, unsigned lit)
void	kissat_mark_eliminated_variable (kissat *solver, unsigned idx)
void	kissat_mark_removed_literals (kissat *solver, unsigned size, unsigned *lits)
void	kissat_mark_added_literals (kissat *solver, unsigned size, unsigned *lits)

Function Documentation

kissat_activate_literal()

void kissat_activate_literal	(	kissat *	solver,
		unsigned	lit )

Definition at line 52 of file flags.c.

                                                            {
  activate_literal (solver, lit);
}

Here is the caller graph for this function:

kissat_activate_literals()

void kissat_activate_literals	(	kissat *	solver,
		unsigned	size,
		unsigned *	lits )

Definition at line 56 of file flags.c.

                                               {
  for (unsigned i = 0; i < size; i++)
    activate_literal (solver, lits[i]);
}

Here is the caller graph for this function:

kissat_mark_added_literals()

void kissat_mark_added_literals	(	kissat *	solver,
		unsigned	size,
		unsigned *	lits )

Definition at line 113 of file flags.c.

                                                 {
  for (unsigned i = 0; i < size; i++)
    kissat_mark_added_literal (solver, lits[i]);
}

kissat_mark_eliminated_variable()

void kissat_mark_eliminated_variable	(	kissat *	solver,
		unsigned	idx )

Definition at line 79 of file flags.c.

                                                                    {
  const unsigned lit = LIT (idx);
  KISSAT_assert (!VALUE (lit));
  LOG ("marking internal %s as eliminated", LOGVAR (idx));
  flags *f = FLAGS (idx);
  KISSAT_assert (f->active);
  KISSAT_assert (!f->eliminated);
  KISSAT_assert (!f->fixed);
  f->eliminated = true;
  deactivate_variable (solver, f, idx);
  int elit = kissat_export_literal (solver, lit);
  KISSAT_assert (elit);
  KISSAT_assert (elit != INT_MIN);
  unsigned eidx = ABS (elit);
  import *import = &PEEK_STACK (solver->import, eidx);
  KISSAT_assert (!import->eliminated);
  KISSAT_assert (import->imported);
  KISSAT_assert (STRIP (import->lit) == STRIP (lit));
  size_t pos = SIZE_STACK (solver->eliminated);
  KISSAT_assert (pos < (1u << 30));
  import->lit = pos;
  import->eliminated = true;
  PUSH_STACK (solver->eliminated, (value) 0);
  LOG ("marked external variable %u as eliminated", eidx);
  KISSAT_assert (solver->unassigned > 0);
  solver->unassigned--;
}

kissat_mark_fixed_literal()

void kissat_mark_fixed_literal	(	kissat *	solver,
		unsigned	lit )

Definition at line 62 of file flags.c.

                                                              {
  KISSAT_assert (VALUE (lit) > 0);
  const unsigned idx = IDX (lit);
  LOG ("marking internal %s as fixed", LOGVAR (idx));
  flags *f = FLAGS (idx);
  KISSAT_assert (f->active);
  KISSAT_assert (!f->eliminated);
  KISSAT_assert (!f->fixed);
  f->fixed = true;
  deactivate_variable (solver, f, idx);
  INC (units);
  int elit = kissat_export_literal (solver, lit);
  KISSAT_assert (elit);
  PUSH_STACK (solver->units, elit);
  LOG ("pushed external unit literal %d (internal %u)", elit, lit);
}

kissat_mark_removed_literals()

void kissat_mark_removed_literals	(	kissat *	solver,
		unsigned	size,
		unsigned *	lits )

Definition at line 107 of file flags.c.

                                                   {
  for (unsigned i = 0; i < size; i++)
    kissat_mark_removed_literal (solver, lits[i]);
}