import.h File Reference

#include "global.h"

Include dependency graph for import.h:

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

Go to the source code of this file.

Functions
unsigned	kissat_import_literal (struct kissat *solver, int lit)
unsigned	kissat_fresh_literal (struct kissat *solver)

Function Documentation

kissat_fresh_literal()

unsigned kissat_fresh_literal

(

struct kissat *

solver

)

Definition at line 84 of file import.c.

                                               {
  size_t imported = SIZE_STACK (solver->import);
  KISSAT_assert (imported <= EXTERNAL_MAX_VAR);
  if (imported == EXTERNAL_MAX_VAR) {
    LOG ("can not get another external variable");
    return INVALID_LIT;
  }
  KISSAT_assert (imported <= (unsigned) INT_MAX);
  int eidx = (int) imported;
  unsigned res = import_literal (solver, eidx, true);
#ifndef KISSAT_NDEBUG
  struct import *import = &PEEK_STACK (solver->import, imported);
  KISSAT_assert (import->imported);
  KISSAT_assert (import->extension);
#endif
  INC (fresh);
  kissat_activate_literal (solver, res);
  return res;
}

Here is the call graph for this function:

kissat_import_literal()

unsigned kissat_import_literal	(	struct kissat *	solver,
		int	lit )

Definition at line 60 of file import.c.

                                                          {
  KISSAT_assert (VALID_EXTERNAL_LITERAL (elit));
  if (GET_OPTION (tumble))
    return import_literal (solver, elit, false);
  const unsigned eidx = ABS (elit);
  KISSAT_assert (SIZE_STACK (solver->import) <= UINT_MAX);
  unsigned other = SIZE_STACK (solver->import);
  if (eidx < other)
    return import_literal (solver, elit, false);
  if (!other)
    adjust_imports_for_external_literal (solver, other++);
 
  unsigned ilit = 0;
  do {
    KISSAT_assert (VALID_EXTERNAL_LITERAL ((int) other));
    ilit = import_literal (solver, other, false);
  } while (other++ < eidx);
 
  if (elit < 0)
    ilit = NOT (ilit);
 
  return ilit;
}

Here is the caller graph for this function: