walk.h File Reference

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

Include dependency graph for walk.h:

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

Go to the source code of this file.

Functions
bool	kissat_walking (struct kissat *)
void	kissat_walk (struct kissat *)

Function Documentation

kissat_walk()

void kissat_walk

(

struct 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

(

struct 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: