reorder.c File Reference

#include "reorder.h"
#include "backtrack.h"
#include "bump.h"
#include "inline.h"
#include "inlineheap.h"
#include "inlinequeue.h"
#include "inlinevector.h"
#include "internal.h"
#include "logging.h"
#include "print.h"
#include "report.h"
#include "sort.h"

Include dependency graph for reorder.c:

Go to the source code of this file.

Macros
#define	LESS_FOCUSED_ORDER(A, B)
#define	LESS_STABLE_ORDER(A, B)

Functions
ABC_NAMESPACE_IMPL_START bool	kissat_reordering (kissat *solver)
void	kissat_reorder (kissat *solver)

Macro Definition Documentation

LESS_FOCUSED_ORDER

#define LESS_FOCUSED_ORDER	(		A,
			B )

Value:

less_focused_order (A, B, links, weights)

Definition at line 137 of file reorder.c.

LESS_STABLE_ORDER

#define LESS_STABLE_ORDER	(		A,
			B )

Value:

less_stable_order (A, B, scores, weights)

Definition at line 139 of file reorder.c.

Function Documentation

kissat_reorder()

void kissat_reorder

(

kissat *

solver

)

Definition at line 205 of file reorder.c.

                                     {
  START (reorder);
  INC (reordered);
  KISSAT_assert (!solver->level);
  kissat_phase (solver, "reorder", GET (reordered),
                "reorder limit %" PRIu64 " hit a after %" PRIu64
                " conflicts in %s mode ",
                solver->limits.reorder.conflicts, CONFLICTS,
                solver->stable ? "stable" : "focused");
  if (solver->stable)
    reorder_stable (solver);
  else
    reorder_focused (solver);
  kissat_phase (solver, "reorder", GET (reordered),
                "reordered decisions in %s search mode",
                solver->stable ? "stable" : "focused");
  UPDATE_CONFLICT_LIMIT (reorder, reordered, LINEAR, false);
  REPORT (0, 'o');
  STOP (reorder);
}

Here is the caller graph for this function:

kissat_reordering()

ABC_NAMESPACE_IMPL_START bool kissat_reordering

(

kissat *

solver

)

Definition at line 16 of file reorder.c.

                                        {
  if (!GET_OPTION (reorder))
    return false;
  if (!solver->stable && GET_OPTION (reorder) < 2)
    return false;
  if (solver->level)
    return false;
  return CONFLICTS >= solver->limits.reorder.conflicts;
}

Here is the caller graph for this function: