#include "walk.h"
#include "allocate.h"
#include "decide.h"
#include "dense.h"
#include "inline.h"
#include "phases.h"
#include "print.h"
#include "rephase.h"
#include "report.h"
#include "terminate.h"
#include "warmup.h"
#include <string.h>

Include dependency graph for walk.c:

Classes
struct	tagged

struct	counter

Macros
#define	LD_MAX_WALK_REF 31

#define	MAX_WALK_REF ((1u << LD_MAX_WALK_REF) - 1)

#define	INVALID_BEST_TRAIL_POS UINT_MAX

#define	report_initial_minimum(...)

#define	report_minimum(...)

Typedefs
typedef typedefABC_NAMESPACE_IMPL_START struct tagged	tagged

typedef struct counter	counter

typedef struct walker	walker

Functions
typedef	STACK (double)

bool	kissat_walking (kissat *solver)

void	kissat_walk (kissat *solver)

Macro Definition Documentation

◆ INVALID_BEST_TRAIL_POS

#define INVALID_BEST_TRAIL_POS UINT_MAX

◆ LD_MAX_WALK_REF

#define LD_MAX_WALK_REF 31

Definition at line 21 of file walk.c.

◆ MAX_WALK_REF

#define MAX_WALK_REF ((1u << LD_MAX_WALK_REF) - 1)

Definition at line 22 of file walk.c.

◆ report_initial_minimum

#define report_initial_minimum ( ... )

Value:

do { \

} while (0)

Definition at line 364 of file walk.c.

#define report_initial_minimum(...) \
  do { \
  } while (0)

◆ report_minimum

#define report_minimum ( ... )

Value:

do { \

} while (0)

Definition at line 367 of file walk.c.

#define report_minimum(...) \
  do { \
  } while (0)

Typedef Documentation

◆ counter

typedef struct counter counter

Definition at line 18 of file walk.c.

◆ tagged

typedef typedefABC_NAMESPACE_IMPL_START struct tagged tagged

Definition at line 17 of file walk.c.

◆ walker

typedef struct walker walker

Definition at line 19 of file walk.c.

Function Documentation

◆ kissat_walk()

void kissat_walk ( kissat * solver )

Definition at line 938 of file walk.c.

                                  {
  KISSAT_assert (!solver->level);
  KISSAT_assert (!solver->inconsistent);
  KISSAT_assert (kissat_propagated (solver));
  KISSAT_assert (kissat_walking (solver));
 
  reference last_irredundant = solver->last_irredundant;
  if (last_irredundant == INVALID_REF)
    last_irredundant = SIZE_STACK (solver->arena);
 
  if (last_irredundant > MAX_WALK_REF) {
    kissat_phase (solver, "walk", GET (walks),
                  "last irredundant clause reference %u too large",
                  last_irredundant);
    return;
  }
 
  uint64_t clauses = BINIRR_CLAUSES;
  if (clauses > MAX_WALK_REF) {
    kissat_phase (solver, "walk", GET (walks),
                  "way too many irredundant clauses %" PRIu64, clauses);
    return;
  }
 
  if (GET_OPTION (warmup))
    kissat_warmup (solver);
 
  STOP_SEARCH_AND_START_SIMPLIFIER (walking);
  walking_phase (solver);
  STOP_SIMPLIFIER_AND_RESUME_SEARCH (walking);
}

Here is the call graph for this function:

◆ kissat_walking()

bool kissat_walking ( kissat * solver )

Definition at line 913 of file walk.c.

                                     {
  reference last_irredundant = solver->last_irredundant;
  if (last_irredundant == INVALID_REF)
    last_irredundant = SIZE_STACK (solver->arena);
 
  if (last_irredundant > MAX_WALK_REF) {
    kissat_extremely_verbose (solver,
                              "can not walk since last "
                              "irredundant clause reference %u too large",
                              last_irredundant);
    return false;
  }
 
  uint64_t clauses = BINIRR_CLAUSES;
  if (clauses > MAX_WALK_REF) {
    kissat_extremely_verbose (solver,
                              "can not walk due to "
                              "way too many irredundant clauses %" PRIu64,
                              clauses);
    return false;
  }
 
  return true;
}

Here is the caller graph for this function:

◆ STACK()

typedef STACK ( double )

Definition at line 41 of file walk.c.

              {
  kissat *solver;
 
  unsigned best_trail_pos;
  unsigned clauses;
  unsigned current;
  unsigned exponents;
  unsigned initial;
  unsigned minimum;
  unsigned offset;
 
  generator random;
 
  counter *counters;
  litpairs *binaries;
  tagged *refs;
  double *table;
 
  value *original_values;
  value *best_values;
 
  doubles scores;
  unsigneds unsat;
  unsigneds trail;
 
  double size;
  double epsilon;
 
  uint64_t limit;
  uint64_t flipped;
#ifndef KISSAT_QUIET
  uint64_t start;
  struct {
    uint64_t flipped;
    unsigned minimum;
  } report;
#endif
};