trail.c File Reference

#include "trail.h"
#include "backtrack.h"
#include "inline.h"
#include "propsearch.h"

Include dependency graph for trail.c:

Go to the source code of this file.

Functions
ABC_NAMESPACE_IMPL_START void	kissat_flush_trail (kissat *solver)
void	kissat_mark_reason_clauses (kissat *solver, reference start)
bool	kissat_flush_and_mark_reason_clauses (kissat *solver, reference start)
void	kissat_unmark_reason_clauses (kissat *solver, reference start)

Function Documentation

kissat_flush_and_mark_reason_clauses()

bool kissat_flush_and_mark_reason_clauses	(	kissat *	solver,
		reference	start )

Definition at line 49 of file trail.c.

                                                            {
  KISSAT_assert (solver->watching);
  KISSAT_assert (!solver->inconsistent);
  KISSAT_assert (kissat_propagated (solver));
 
  if (solver->unflushed) {
    LOG ("need to flush %u units from trail", solver->unflushed);
    kissat_backtrack_propagate_and_flush_trail (solver);
  } else {
    LOG ("no need to flush units from trail (all units already flushed)");
    kissat_mark_reason_clauses (solver, start);
  }
 
  return true;
}

Here is the call graph for this function:

Here is the caller graph for this function:

kissat_flush_trail()

ABC_NAMESPACE_IMPL_START void kissat_flush_trail

(

kissat *

solver

)

Definition at line 8 of file trail.c.

                                         {
  KISSAT_assert (!solver->level);
  KISSAT_assert (solver->unflushed);
  KISSAT_assert (!solver->inconsistent);
  KISSAT_assert (kissat_propagated (solver));
  KISSAT_assert (SIZE_ARRAY (solver->trail) == solver->unflushed);
  LOG ("flushed %zu units from trail", SIZE_ARRAY (solver->trail));
  CLEAR_ARRAY (solver->trail);
  kissat_reset_propagate (solver);
  solver->unflushed = 0;
}

kissat_mark_reason_clauses()

void kissat_mark_reason_clauses	(	kissat *	solver,
		reference	start )

Definition at line 20 of file trail.c.

                                                                  {
  LOG ("starting marking reason clauses at clause[%" REFERENCE_FORMAT "]",
       start);
  KISSAT_assert (!solver->unflushed);
#ifdef LOGGING
  unsigned reasons = 0;
#endif
  ward *arena = BEGIN_STACK (solver->arena);
  for (all_stack (unsigned, lit, solver->trail)) {
    assigned *a = ASSIGNED (lit);
    KISSAT_assert (a->level > 0);
    if (a->binary)
      continue;
    const reference ref = a->reason;
    KISSAT_assert (ref != UNIT_REASON);
    if (ref == DECISION_REASON)
      continue;
    if (ref < start)
      continue;
    clause *c = (clause *) (arena + ref);
    KISSAT_assert (kissat_clause_in_arena (solver, c));
    c->reason = true;
#ifdef LOGGING
    reasons++;
#endif
  }
  LOG ("marked %u reason clauses", reasons);
}

Here is the caller graph for this function:

kissat_unmark_reason_clauses()

void kissat_unmark_reason_clauses	(	kissat *	solver,
		reference	start )

Definition at line 66 of file trail.c.

                                                                    {
  LOG ("starting unmarking reason clauses at clause[%" REFERENCE_FORMAT "]",
       start);
  KISSAT_assert (!solver->unflushed);
#ifdef LOGGING
  unsigned reasons = 0;
#endif
  ward *arena = BEGIN_STACK (solver->arena);
  for (all_stack (unsigned, lit, solver->trail)) {
    assigned *a = ASSIGNED (lit);
    KISSAT_assert (a->level > 0);
    if (a->binary)
      continue;
    const reference ref = a->reason;
    KISSAT_assert (ref != UNIT_REASON);
    if (ref == DECISION_REASON)
      continue;
    if (ref < start)
      continue;
    clause *c = (clause *) (arena + ref);
    KISSAT_assert (kissat_clause_in_arena (solver, c));
    KISSAT_assert (c->reason);
    c->reason = false;
#ifdef LOGGING
    reasons++;
#endif
  }
  LOG ("unmarked %u reason clauses", reasons);
}

Here is the caller graph for this function: