#include <solver.h>

Collaboration diagram for solver_t_:

[legend]

Public Attributes
int	status

vec_uint_t *	assumptions

vec_uint_t *	final_conflict

struct cdb *	all_clauses

vec_uint_t *	learnts

vec_uint_t *	originals

vec_wl_t *	watches

act_t	var_act_inc

clause_act_t	clause_act_inc

vec_act_t *	activity

heap_t *	var_order

vec_uint_t *	levels

vec_uint_t *	reasons

vec_char_t *	assigns

vec_char_t *	polarity

vec_uint_t *	trail

vec_uint_t *	trail_lim

unsigned	i_qhead

unsigned	n_assigns_simplify

long	n_props_simplify

vec_uint_t *	temp_lits

vec_char_t *	seen

vec_uint_t *	tagged

vec_uint_t *	stack

vec_uint_t *	last_dlevel

b_queue_t *	bq_trail

b_queue_t *	bq_lbd

long	RC1

long	RC2

long	n_confl_bfr_reduce

float	sum_lbd

unsigned	cur_stamp

vec_uint_t *	stamps

unsigned	book_cl_orig

unsigned	book_cl_lrnt

unsigned	book_cdb

unsigned	book_vars

unsigned	book_trail

vec_char_t *	marks

abctime	nRuntimeLimit

int *	pstop

int	RunId

int(*	pFuncStop )(int)

struct satoko_stats	stats

struct satoko_opts	opts

Detailed Description

Definition at line 38 of file solver.h.

Member Data Documentation

◆ activity

vec_act_t* solver_t_::activity

Definition at line 55 of file solver.h.

◆ all_clauses

struct cdb* solver_t_::all_clauses

Definition at line 45 of file solver.h.

◆ assigns

vec_char_t* solver_t_::assigns

Definition at line 59 of file solver.h.

◆ assumptions

vec_uint_t* solver_t_::assumptions

Definition at line 41 of file solver.h.

◆ book_cdb

unsigned solver_t_::book_cdb

Definition at line 95 of file solver.h.

◆ book_cl_lrnt

unsigned solver_t_::book_cl_lrnt

Definition at line 94 of file solver.h.

◆ book_cl_orig

unsigned solver_t_::book_cl_orig

Definition at line 93 of file solver.h.

◆ book_trail

unsigned solver_t_::book_trail

Definition at line 97 of file solver.h.

◆ book_vars

unsigned solver_t_::book_vars

Definition at line 96 of file solver.h.

◆ bq_lbd

b_queue_t* solver_t_::bq_lbd

Definition at line 81 of file solver.h.

◆ bq_trail

b_queue_t* solver_t_::bq_trail

Definition at line 80 of file solver.h.

◆ clause_act_inc

clause_act_t solver_t_::clause_act_inc

Definition at line 52 of file solver.h.

◆ cur_stamp

unsigned solver_t_::cur_stamp

Definition at line 88 of file solver.h.

◆ final_conflict

vec_uint_t* solver_t_::final_conflict

Definition at line 42 of file solver.h.

◆ i_qhead

unsigned solver_t_::i_qhead

Definition at line 65 of file solver.h.

◆ last_dlevel

vec_uint_t* solver_t_::last_dlevel

Definition at line 77 of file solver.h.

◆ learnts

vec_uint_t* solver_t_::learnts

Definition at line 46 of file solver.h.

◆ levels

vec_uint_t* solver_t_::levels

Definition at line 57 of file solver.h.

◆ marks

vec_char_t* solver_t_::marks

Definition at line 101 of file solver.h.

◆ n_assigns_simplify

unsigned solver_t_::n_assigns_simplify

Definition at line 66 of file solver.h.

◆ n_confl_bfr_reduce

long solver_t_::n_confl_bfr_reduce

Definition at line 84 of file solver.h.

◆ n_props_simplify

long solver_t_::n_props_simplify

Definition at line 68 of file solver.h.

◆ nRuntimeLimit

abctime solver_t_::nRuntimeLimit

Definition at line 104 of file solver.h.

◆ opts

struct satoko_opts solver_t_::opts

Definition at line 110 of file solver.h.

◆ originals

vec_uint_t* solver_t_::originals

Definition at line 47 of file solver.h.

◆ pFuncStop

int(* solver_t_::pFuncStop) (int)

Definition at line 107 of file solver.h.

◆ polarity

vec_char_t* solver_t_::polarity

Definition at line 60 of file solver.h.

◆ pstop

int* solver_t_::pstop

Definition at line 105 of file solver.h.

◆ RC1

long solver_t_::RC1

Definition at line 82 of file solver.h.

◆ RC2

long solver_t_::RC2

Definition at line 83 of file solver.h.

◆ reasons

vec_uint_t* solver_t_::reasons

Definition at line 58 of file solver.h.

◆ RunId

int solver_t_::RunId

Definition at line 106 of file solver.h.

◆ seen

vec_char_t* solver_t_::seen

Definition at line 74 of file solver.h.

◆ stack

vec_uint_t* solver_t_::stack

Definition at line 76 of file solver.h.

◆ stamps

vec_uint_t* solver_t_::stamps

Definition at line 89 of file solver.h.

◆ stats

struct satoko_stats solver_t_::stats

Definition at line 109 of file solver.h.

◆ status

int solver_t_::status

Definition at line 39 of file solver.h.

◆ sum_lbd

float solver_t_::sum_lbd

Definition at line 85 of file solver.h.

◆ tagged

vec_uint_t* solver_t_::tagged

Definition at line 75 of file solver.h.

◆ temp_lits

vec_uint_t* solver_t_::temp_lits

Definition at line 73 of file solver.h.

◆ trail

vec_uint_t* solver_t_::trail

Definition at line 63 of file solver.h.

◆ trail_lim

vec_uint_t* solver_t_::trail_lim

Definition at line 64 of file solver.h.

◆ var_act_inc

act_t solver_t_::var_act_inc

Definition at line 51 of file solver.h.

◆ var_order

heap_t* solver_t_::var_order

Definition at line 56 of file solver.h.

◆ watches

vec_wl_t* solver_t_::watches

Definition at line 48 of file solver.h.

The documentation for this struct was generated from the following file:

src/sat/satoko/solver.h

Public Attributes