internal.h File Reference

#include "arena.h"
#include "array.h"
#include "assign.h"
#include "averages.h"
#include "check.h"
#include "classify.h"
#include "clause.h"
#include "cover.h"
#include "extend.h"
#include "flags.h"
#include "format.h"
#include "frames.h"
#include "heap.h"
#include "kimits.h"
#include "kissat.h"
#include "literal.h"
#include "mode.h"
#include "options.h"
#include "phases.h"
#include "profile.h"
#include "proof.h"
#include "queue.h"
#include "random.h"
#include "reluctant.h"
#include "rephase.h"
#include "smooth.h"
#include "stack.h"
#include "statistics.h"
#include "value.h"
#include "vector.h"
#include "watch.h"
#include "global.h"

Include dependency graph for internal.h:

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

Go to the source code of this file.

Classes
struct	datarank
struct	import
struct	termination
struct	kissat

Macros
#define	VARS   (solver->vars)
#define	LITS   (2 * solver->vars)
#define	TIER1   (solver->tier1[0])
#define	TIER2   (solver->tier2[1])
#define	SCORES   (&solver->scores)
#define	all_variables(IDX)
#define	all_literals(LIT)
#define	all_clauses(C)
#define	capacity_last_learned    (sizeof solver->last_learned / sizeof *solver->last_learned)
#define	real_end_last_learned   (solver->last_learned + capacity_last_learned)
#define	really_all_last_learned(REF_PTR)

Typedefs
typedef typedefABC_NAMESPACE_HEADER_START struct datarank	datarank
typedef struct import	import
typedef struct termination	termination

Functions
typedef	STACK (value) eliminated
typedef	STACK (import) imports
typedef	STACK (datarank) dataranks
typedef	STACK (watch) statches
typedef	STACK (watch *) patches
void	kissat_reset_last_learned (kissat *solver)

Macro Definition Documentation

all_clauses

#define all_clauses

(

C

)

Value:

  clause *C = (clause *) BEGIN_STACK (solver->arena), \
         *const C##_END = (clause *) END_STACK (solver->arena), *C##_NEXT; \
  C != C##_END && (C##_NEXT = kissat_next_clause (C), true); \
  C = C##_NEXT

Definition at line 279 of file internal.h.

#define all_clauses(C) \
  clause *C = (clause *) BEGIN_STACK (solver->arena), \
         *const C##_END = (clause *) END_STACK (solver->arena), *C##_NEXT; \
  C != C##_END && (C##_NEXT = kissat_next_clause (C), true); \
  C = C##_NEXT

all_literals

#define all_literals

(

LIT

)

Value:

  unsigned LIT = 0, LIT##_END = LITS; \
  LIT != LIT##_END; \
  ++LIT

Definition at line 274 of file internal.h.

#define all_literals(LIT) \
  unsigned LIT = 0, LIT##_END = LITS; \
  LIT != LIT##_END; \
  ++LIT

all_variables

#define all_variables

(

IDX

)

Value:

  unsigned IDX = 0, IDX##_END = solver->vars; \
  IDX != IDX##_END; \
  ++IDX

Definition at line 269 of file internal.h.

#define all_variables(IDX) \
  unsigned IDX = 0, IDX##_END = solver->vars; \
  IDX != IDX##_END; \
  ++IDX

capacity_last_learned

#define capacity_last_learned    (sizeof solver->last_learned / sizeof *solver->last_learned)

Definition at line 285 of file internal.h.

#define capacity_last_learned \
  (sizeof solver->last_learned / sizeof *solver->last_learned)

LITS

#define LITS   (2 * solver->vars)

Definition at line 251 of file internal.h.

real_end_last_learned

#define real_end_last_learned   (solver->last_learned + capacity_last_learned)

Definition at line 288 of file internal.h.

really_all_last_learned

#define really_all_last_learned

(

REF_PTR

)

Value:

  reference *REF_PTR = solver->last_learned, \
            *REF_PTR##_END = real_end_last_learned; \
  REF_PTR != REF_PTR##_END; \
  REF_PTR++

Definition at line 290 of file internal.h.

#define really_all_last_learned(REF_PTR) \
  reference *REF_PTR = solver->last_learned, \
            *REF_PTR##_END = real_end_last_learned; \
  REF_PTR != REF_PTR##_END; \
  REF_PTR++

SCORES

#define SCORES   (&solver->scores)

Definition at line 262 of file internal.h.

TIER1

#define TIER1   (solver->tier1[0])

Definition at line 258 of file internal.h.

TIER2

#define TIER2   (solver->tier2[1])

Definition at line 259 of file internal.h.

VARS

#define VARS   (solver->vars)

Definition at line 250 of file internal.h.

Typedef Documentation

datarank

typedef typedefABC_NAMESPACE_HEADER_START struct datarank datarank

Definition at line 39 of file internal.h.

import

typedef struct import import

Definition at line 46 of file internal.h.

termination

typedef struct termination termination

Definition at line 55 of file internal.h.

Function Documentation

kissat_reset_last_learned()

void kissat_reset_last_learned

(

kissat *

solver

)

Definition at line 22 of file internal.c.

                                                {
  for (really_all_last_learned (p))
    *p = INVALID_REF;
}

Here is the caller graph for this function:

STACK() [1/5]

typedef STACK

(

datarank

)

STACK() [2/5]

typedef STACK

(

import

)

STACK() [3/5]

typedef STACK

(

value

)

STACK() [4/5]

typedef STACK

(

watch *

)

STACK() [5/5]

typedef STACK

(

watch

)