assign.h File Reference

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

Include dependency graph for assign.h:

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

Go to the source code of this file.

Classes
struct	assigned

Macros
#define	DECISION_REASON   UINT_MAX
#define	UNIT_REASON   (DECISION_REASON - 1)
#define	INVALID_LEVEL   UINT_MAX
#define	INVALID_TRAIL   UINT_MAX
#define	ASSIGNED(LIT)
#define	LEVEL(LIT)
#define	TRAIL(LIT)
#define	REASON(LIT)

Typedefs
typedef struct assigned	assigned

Functions
void	kissat_assign_unit (struct kissat *, unsigned lit, const char *)
void	kissat_learned_unit (struct kissat *, unsigned lit)
void	kissat_original_unit (struct kissat *, unsigned lit)
void	kissat_assign_decision (struct kissat *, unsigned lit)
void	kissat_assign_binary (struct kissat *, unsigned, unsigned)
void	kissat_assign_reference (struct kissat *, unsigned lit, reference, struct clause *)

Macro Definition Documentation

ASSIGNED

#define ASSIGNED

(

LIT

)

Value:

  (KISSAT_assert (VALID_INTERNAL_LITERAL (LIT)), solver->assigned + IDX (LIT))

Definition at line 31 of file assign.h.

#define ASSIGNED(LIT) \
  (KISSAT_assert (VALID_INTERNAL_LITERAL (LIT)), solver->assigned + IDX (LIT))

DECISION_REASON

#define DECISION_REASON   UINT_MAX

Definition at line 9 of file assign.h.

INVALID_LEVEL

#define INVALID_LEVEL   UINT_MAX

Definition at line 12 of file assign.h.

INVALID_TRAIL

#define INVALID_TRAIL   UINT_MAX

Definition at line 13 of file assign.h.

LEVEL

#define LEVEL

(

LIT

)

Value:

(ASSIGNED (LIT)->level)

Definition at line 34 of file assign.h.

REASON

#define REASON

(

LIT

)

Value:

(ASSIGNED (LIT)->reason)

Definition at line 36 of file assign.h.

TRAIL

#define TRAIL

(

LIT

)

Value:

(ASSIGNED (LIT)->trail)

Definition at line 35 of file assign.h.

UNIT_REASON

#define UNIT_REASON   (DECISION_REASON - 1)

Definition at line 10 of file assign.h.

Typedef Documentation

assigned

typedef struct assigned assigned

Definition at line 15 of file assign.h.

Function Documentation

kissat_assign_binary()

void kissat_assign_binary	(	struct kissat *	solver,
		unsigned	lit,
		unsigned	other )

Definition at line 34 of file assign.c.

                                                                         {
  KISSAT_assert (VALUE (other) < 0);
  assigned *assigned = solver->assigned;
  const unsigned other_idx = IDX (other);
  struct assigned *a = assigned + other_idx;
  unsigned level = a->level;
  if (GET_OPTION (jumpreasons) && level && a->binary) {
    LOGBINARY (lit, other, "jumping %s reason", LOGLIT (lit));
    INC (jumped_reasons);
    other = a->reason;
  }
  kissat_assign (solver, solver->probing, a->level, true, lit, other);
  LOGBINARY (lit, other, "assign %s reason", LOGLIT (lit));
}

Here is the caller graph for this function:

kissat_assign_decision()

void kissat_assign_decision	(	struct kissat *	solver,
		unsigned	lit )

Definition at line 28 of file assign.c.

                                                           {
  kissat_assign (solver, solver->probing, solver->level, false, lit,
                 DECISION_REASON);
  LOG ("assign %s decision", LOGLIT (lit));
}

Here is the caller graph for this function:

kissat_assign_reference()

void kissat_assign_reference	(	struct kissat *	solver,
		unsigned	lit,
		reference	ref,
		struct clause *	reason )

Definition at line 49 of file assign.c.

                                              {
  KISSAT_assert (reason == kissat_dereference_clause (solver, ref));
  assigned *assigned = solver->assigned;
  value *values = solver->values;
  const unsigned level =
      kissat_assignment_level (solver, values, assigned, lit, reason);
  KISSAT_assert (level <= solver->level);
  KISSAT_assert (ref != DECISION_REASON);
  KISSAT_assert (ref != UNIT_REASON);
  kissat_assign (solver, solver->probing, level, false, lit, ref);
  LOGREF (ref, "assign %s reason", LOGLIT (lit));
}

Here is the caller graph for this function:

kissat_assign_unit()

void kissat_assign_unit	(	struct kissat *	solver,
		unsigned	lit,
		const char *	reason )

Definition at line 10 of file assign.c.

                                                                           {
  kissat_assign (solver, solver->probing, 0, false, lit, UNIT_REASON);
  LOGUNARY (lit, "assign %s %s", LOGLIT (lit), reason);
#ifndef LOGGING
  (void) reason;
#endif
}

Here is the caller graph for this function:

kissat_learned_unit()

void kissat_learned_unit	(	struct kissat *	solver,
		unsigned	lit )

Definition at line 18 of file assign.c.

                                                        {
  kissat_assign_unit (solver, lit, "learned reason");
  CHECK_AND_ADD_UNIT (lit);
  ADD_UNIT_TO_PROOF (lit);
}

Here is the call graph for this function:

Here is the caller graph for this function:

kissat_original_unit()

void kissat_original_unit	(	struct kissat *	solver,
		unsigned	lit )

Definition at line 24 of file assign.c.

                                                         {
  kissat_assign_unit (solver, lit, "original reason");
}

Here is the call graph for this function:

Here is the caller graph for this function: