flags.h File Reference

#include <stdbool.h>
#include "global.h"

Include dependency graph for flags.h:

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

Go to the source code of this file.

Classes
struct	flags

Macros
#define	FLAGS(IDX)
#define	ACTIVE(IDX)
#define	ELIMINATED(IDX)

Typedefs
typedef typedefABC_NAMESPACE_HEADER_START struct flags	flags

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

Macro Definition Documentation

ACTIVE

#define ACTIVE

(

IDX

)

Value:

(FLAGS (IDX)->active)

Definition at line 26 of file flags.h.

ELIMINATED

#define ELIMINATED

(

IDX

)

Value:

(FLAGS (IDX)->eliminated)

Definition at line 27 of file flags.h.

FLAGS

#define FLAGS

(

IDX

)

Value:

(KISSAT_assert ((IDX) < VARS), (solver->flags + (IDX)))

Definition at line 24 of file flags.h.

Typedef Documentation

flags

typedef typedefABC_NAMESPACE_HEADER_START struct flags flags

Definition at line 9 of file flags.h.

Function Documentation

kissat_activate_literal()

void kissat_activate_literal	(	struct 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	(	struct 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	(	struct 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	(	struct 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	(	struct 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	(	struct 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]);
}