classify.h File Reference

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

Include dependency graph for classify.h:

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

Go to the source code of this file.

Classes
struct	classification

Typedefs
typedef struct classification	classification

Functions
void	kissat_classify (struct kissat *)

Typedef Documentation

classification

typedef struct classification classification

Definition at line 16 of file classify.h.

Function Documentation

kissat_classify()

void kissat_classify

(

struct kissat *

solver

)

Definition at line 7 of file classify.c.

                                             {
  statistics *s = &solver->statistics_;
  uint64_t clauses = s->clauses_binary + s->clauses_irredundant;
  unsigned small_clauses_limit = GET_OPTION (smallclauses);
  if (clauses <= small_clauses_limit) {
    solver->classification.small = true;
    solver->classification.bigbig = false;
  } else {
    solver->classification.small = false;
    unsigned bigbigfraction = GET_OPTION (bigbigfraction);
    double percent = bigbigfraction / 1000.0;
    double actual = kissat_percent (s->clauses_binary, clauses);
    if (actual >= percent)
      solver->classification.bigbig = true;
    else
      solver->classification.bigbig = false;
  }
  kissat_very_verbose (
      solver, "formula classified as having a %s total number of clauses",
      solver->classification.small ? "small" : "large");
  kissat_very_verbose (
      solver, "formula classified to have a %s binary clauses fraction",
      solver->classification.bigbig ? "large" : "small");
}

Here is the caller graph for this function: