factor.c File Reference

#include "factor.h"
#include "bump.h"
#include "clause.h"
#include "dense.h"
#include "heap.h"
#include "import.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 "terminate.h"
#include "vector.h"
#include "watch.h"
#include <string.h>

Include dependency graph for factor.c:

Go to the source code of this file.

Classes
struct	quotient
struct	scores
struct	factoring

Macros
#define	FACTOR   1
#define	QUOTIENT   2
#define	NOUNTED   4

Typedefs
typedef struct quotient	quotient
typedef struct scores	scores
typedef struct factoring	factoring

Functions
void	kissat_factor (kissat *solver)

Macro Definition Documentation

FACTOR

#define FACTOR   1

Definition at line 24 of file factor.c.

NOUNTED

#define NOUNTED   4

Definition at line 26 of file factor.c.

QUOTIENT

#define QUOTIENT   2

Definition at line 25 of file factor.c.

Typedef Documentation

factoring

typedef struct factoring factoring

Definition at line 65 of file factor.c.

quotient

typedef struct quotient quotient

Definition at line 37 of file factor.c.

scores

typedef struct scores scores

Definition at line 44 of file factor.c.

Function Documentation

kissat_factor()

void kissat_factor

(

kissat *

solver

)

Definition at line 1083 of file factor.c.

                                    {
  KISSAT_assert (!solver->level);
  if (solver->inconsistent)
    return;
  if (!GET_OPTION (factor))
    return;
  statistics *s = &solver->statistics_;
  if (solver->limits.factor.marked >= s->literals_factor) {
    kissat_extremely_verbose (
        solver,
        "factorization skipped as no literals have been marked to be added "
        "(%" PRIu64 " < %" PRIu64,
        solver->limits.factor.marked, s->literals_factor);
    return;
  }
  START (factor);
  INC (factorizations);
  kissat_phase (solver, "factorization", GET (factorizations),
                "binary clause bounded variable addition");
  uint64_t limit = GET_OPTION (factoriniticks);
  if (s->factorizations > 1) {
    SET_EFFORT_LIMIT (tmp, factor, factor_ticks);
    limit = tmp;
  } else {
    kissat_very_verbose (solver,
                         "initially limiting to %" PRIu64
                         " million factorization ticks",
                         limit);
    limit *= 1e6;
    limit += s->factor_ticks;
  }
#ifndef KISSAT_QUIET
  struct {
    int64_t variables, binary, clauses, ticks;
  } before, after, delta;
  before.variables = s->variables_extension + s->variables_original;
  before.binary = BINARY_CLAUSES;
  before.clauses = IRREDUNDANT_CLAUSES;
  before.ticks = s->factor_ticks;
#endif
  kissat_enter_dense_mode (solver, 0);
  connect_clauses_to_factor (solver);
  bool completed = run_factorization (solver, limit);
  kissat_resume_sparse_mode (solver, false, 0);
#ifndef KISSAT_QUIET
  after.variables = s->variables_extension + s->variables_original;
  after.binary = BINARY_CLAUSES;
  after.clauses = IRREDUNDANT_CLAUSES;
  after.ticks = s->factor_ticks;
  delta.variables = after.variables - before.variables;
  delta.binary = before.binary - after.binary;
  delta.clauses = before.clauses - after.clauses;
  delta.ticks = after.ticks - before.ticks;
  kissat_very_verbose (solver, "used %f million factorization ticks",
                       delta.ticks * 1e-6);
  kissat_phase (solver, "factorization", GET (factorizations),
                "introduced %" PRId64 " extension variables %.0f%%",
                delta.variables,
                kissat_percent (delta.variables, before.variables));
  kissat_phase (solver, "factorization", GET (factorizations),
                "removed %" PRId64 " binary clauses %.0f%%", delta.binary,
                kissat_percent (delta.binary, before.binary));
  kissat_phase (solver, "factorization", GET (factorizations),
                "removed %" PRId64 " large clauses %.0f%%", delta.clauses,
                kissat_percent (delta.clauses, before.clauses));
#endif
  if (completed)
    solver->limits.factor.marked = s->literals_factor;
  STOP (factor);
}

Here is the call graph for this function: