assign.c File Reference

#include "assign.h"
#include "inline.h"
#include "inlineassign.h"
#include "logging.h"
#include <limits.h>

Include dependency graph for assign.c:

Go to the source code of this file.

Functions
ABC_NAMESPACE_IMPL_START void	kissat_assign_unit (kissat *solver, unsigned lit, const char *reason)
void	kissat_learned_unit (kissat *solver, unsigned lit)
void	kissat_original_unit (kissat *solver, unsigned lit)
void	kissat_assign_decision (kissat *solver, unsigned lit)
void	kissat_assign_binary (kissat *solver, unsigned lit, unsigned other)
void	kissat_assign_reference (kissat *solver, unsigned lit, reference ref, clause *reason)

Function Documentation

kissat_assign_binary()

void kissat_assign_binary	(	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	(	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	(	kissat *	solver,
		unsigned	lit,
		reference	ref,
		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()

ABC_NAMESPACE_IMPL_START void kissat_assign_unit	(	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	(	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	(	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: