#include <satSolver.h>

Collaboration diagram for sat_solver_t:

[legend]

Public Attributes
int	size

int	cap

int	qhead

int	qtail

Sat_Mem_t	Mem

int	hLearnts

int	hBinary

clause *	binary

veci *	wlists

int	iVarPivot

int	iTrailPivot

int	hProofPivot

int	VarActType

int	ClaActType

word	var_inc

word	var_inc2

word	var_decay

word *	activity

word *	activity2

unsigned	cla_inc

unsigned	cla_decay

veci	act_clas

char *	pFreqs

int	nVarUsed

int *	levels

char *	assigns

char *	polarity

char *	tags

char *	loads

int *	orderpos

int *	reasons

lit *	trail

veci	tagged

veci	stack

veci	order

veci	trail_lim

int *	model

veci	conf_final

int	root_level

int	simpdb_assigns

int	simpdb_props

double	random_seed

double	progress_estimate

int	verbosity

int	fVerbose

int	fPrintClause

stats_t	stats

int	nLearntMax

int	nLearntStart

int	nLearntDelta

int	nLearntRatio

int	nDBreduces

ABC_INT64_T	nConfLimit

ABC_INT64_T	nInsLimit

abctime	nRuntimeLimit

veci	act_vars

double *	factors

int	nRestarts

int	nCalls

int	nCalls2

veci	unit_lits

veci	pivot_vars

int	fSkipSimplify

int	fNotUseRandom

int	fNoRestarts

int *	pGlobalVars

void *	pStore

int	fSolved

FILE *	pFile

int	nClauses

int	nRoots

veci	temp_clause

veci	user_vars

veci	user_values

void *	pCnfMan

int(*	pCnfFunc )(void *p, int)

int	RunId

int(*	pFuncStop )(int)

Detailed Description

Definition at line 100 of file satSolver.h.

Member Data Documentation

◆ act_clas

veci sat_solver_t::act_clas

Definition at line 129 of file satSolver.h.

◆ act_vars

veci sat_solver_t::act_vars

Definition at line 174 of file satSolver.h.

◆ activity

word* sat_solver_t::activity

Definition at line 125 of file satSolver.h.

◆ activity2

word* sat_solver_t::activity2

Definition at line 126 of file satSolver.h.

◆ assigns

char* sat_solver_t::assigns

Definition at line 136 of file satSolver.h.

◆ binary

clause* sat_solver_t::binary

Definition at line 111 of file satSolver.h.

◆ cap

int sat_solver_t::cap

Definition at line 103 of file satSolver.h.

◆ cla_decay

unsigned sat_solver_t::cla_decay

Definition at line 128 of file satSolver.h.

◆ cla_inc

unsigned sat_solver_t::cla_inc

Definition at line 127 of file satSolver.h.

◆ ClaActType

int sat_solver_t::ClaActType

Definition at line 121 of file satSolver.h.

◆ conf_final

veci sat_solver_t::conf_final

Definition at line 151 of file satSolver.h.

◆ factors

double* sat_solver_t::factors

Definition at line 175 of file satSolver.h.

◆ fNoRestarts

int sat_solver_t::fNoRestarts

Definition at line 184 of file satSolver.h.

◆ fNotUseRandom

int sat_solver_t::fNotUseRandom

Definition at line 183 of file satSolver.h.

◆ fPrintClause

int sat_solver_t::fPrintClause

Definition at line 161 of file satSolver.h.

◆ fSkipSimplify

int sat_solver_t::fSkipSimplify

Definition at line 182 of file satSolver.h.

◆ fSolved

int sat_solver_t::fSolved

Definition at line 189 of file satSolver.h.

◆ fVerbose

int sat_solver_t::fVerbose

Definition at line 160 of file satSolver.h.

◆ hBinary

int sat_solver_t::hBinary

Definition at line 110 of file satSolver.h.

◆ hLearnts

int sat_solver_t::hLearnts

Definition at line 109 of file satSolver.h.

◆ hProofPivot

int sat_solver_t::hProofPivot

Definition at line 117 of file satSolver.h.

◆ iTrailPivot

int sat_solver_t::iTrailPivot

Definition at line 116 of file satSolver.h.

◆ iVarPivot

int sat_solver_t::iVarPivot

Definition at line 115 of file satSolver.h.

◆ levels

int* sat_solver_t::levels

Definition at line 135 of file satSolver.h.

◆ loads

char* sat_solver_t::loads

Definition at line 139 of file satSolver.h.

◆ Mem

Sat_Mem_t sat_solver_t::Mem

Definition at line 108 of file satSolver.h.

◆ model

int* sat_solver_t::model

Definition at line 150 of file satSolver.h.

◆ nCalls

int sat_solver_t::nCalls

Definition at line 177 of file satSolver.h.

◆ nCalls2

int sat_solver_t::nCalls2

Definition at line 178 of file satSolver.h.

◆ nClauses

int sat_solver_t::nClauses

Definition at line 193 of file satSolver.h.

◆ nConfLimit

ABC_INT64_T sat_solver_t::nConfLimit

Definition at line 170 of file satSolver.h.

◆ nDBreduces

int sat_solver_t::nDBreduces

Definition at line 168 of file satSolver.h.

◆ nInsLimit

ABC_INT64_T sat_solver_t::nInsLimit

Definition at line 171 of file satSolver.h.

◆ nLearntDelta

int sat_solver_t::nLearntDelta

Definition at line 166 of file satSolver.h.

◆ nLearntMax

int sat_solver_t::nLearntMax

Definition at line 164 of file satSolver.h.

◆ nLearntRatio

int sat_solver_t::nLearntRatio

Definition at line 167 of file satSolver.h.

◆ nLearntStart

int sat_solver_t::nLearntStart

Definition at line 165 of file satSolver.h.

◆ nRestarts

int sat_solver_t::nRestarts

Definition at line 176 of file satSolver.h.

◆ nRoots

int sat_solver_t::nRoots

Definition at line 194 of file satSolver.h.

◆ nRuntimeLimit

abctime sat_solver_t::nRuntimeLimit

Definition at line 172 of file satSolver.h.

◆ nVarUsed

int sat_solver_t::nVarUsed

Definition at line 132 of file satSolver.h.

◆ order

veci sat_solver_t::order

Definition at line 147 of file satSolver.h.

◆ orderpos

int* sat_solver_t::orderpos

Definition at line 141 of file satSolver.h.

◆ pCnfFunc

int(* sat_solver_t::pCnfFunc) (void *p, int)

Definition at line 204 of file satSolver.h.

◆ pCnfMan

void* sat_solver_t::pCnfMan

Definition at line 203 of file satSolver.h.

◆ pFile

FILE* sat_solver_t::pFile

Definition at line 192 of file satSolver.h.

◆ pFreqs

char* sat_solver_t::pFreqs

Definition at line 131 of file satSolver.h.

◆ pFuncStop

int(* sat_solver_t::pFuncStop) (int)

Definition at line 208 of file satSolver.h.

◆ pGlobalVars

int* sat_solver_t::pGlobalVars

Definition at line 186 of file satSolver.h.

◆ pivot_vars

veci sat_solver_t::pivot_vars

Definition at line 180 of file satSolver.h.

◆ polarity

char* sat_solver_t::polarity

Definition at line 137 of file satSolver.h.

◆ progress_estimate

double sat_solver_t::progress_estimate

Definition at line 158 of file satSolver.h.

◆ pStore

void* sat_solver_t::pStore

Definition at line 188 of file satSolver.h.

◆ qhead

int sat_solver_t::qhead

Definition at line 104 of file satSolver.h.

◆ qtail

int sat_solver_t::qtail

Definition at line 105 of file satSolver.h.

◆ random_seed

double sat_solver_t::random_seed

Definition at line 157 of file satSolver.h.

◆ reasons

int* sat_solver_t::reasons

Definition at line 142 of file satSolver.h.

◆ root_level

int sat_solver_t::root_level

Definition at line 154 of file satSolver.h.

◆ RunId

int sat_solver_t::RunId

Definition at line 207 of file satSolver.h.

◆ simpdb_assigns

int sat_solver_t::simpdb_assigns

Definition at line 155 of file satSolver.h.

◆ simpdb_props

int sat_solver_t::simpdb_props

Definition at line 156 of file satSolver.h.

◆ size

int sat_solver_t::size

Definition at line 102 of file satSolver.h.

◆ stack

veci sat_solver_t::stack

Definition at line 145 of file satSolver.h.

◆ stats

stats_t sat_solver_t::stats

Definition at line 163 of file satSolver.h.

◆ tagged

veci sat_solver_t::tagged

Definition at line 144 of file satSolver.h.

◆ tags

char* sat_solver_t::tags

Definition at line 138 of file satSolver.h.

◆ temp_clause

veci sat_solver_t::temp_clause

Definition at line 196 of file satSolver.h.

◆ trail

lit* sat_solver_t::trail

Definition at line 143 of file satSolver.h.

◆ trail_lim

veci sat_solver_t::trail_lim

Definition at line 148 of file satSolver.h.

◆ unit_lits

veci sat_solver_t::unit_lits

Definition at line 179 of file satSolver.h.

◆ user_values

veci sat_solver_t::user_values

Definition at line 200 of file satSolver.h.

◆ user_vars

veci sat_solver_t::user_vars

Definition at line 199 of file satSolver.h.

◆ var_decay

word sat_solver_t::var_decay

Definition at line 124 of file satSolver.h.

◆ var_inc

word sat_solver_t::var_inc

Definition at line 122 of file satSolver.h.

◆ var_inc2

word sat_solver_t::var_inc2

Definition at line 123 of file satSolver.h.

◆ VarActType

int sat_solver_t::VarActType

Definition at line 120 of file satSolver.h.

◆ verbosity

int sat_solver_t::verbosity

Definition at line 159 of file satSolver.h.

◆ wlists

veci* sat_solver_t::wlists

Definition at line 112 of file satSolver.h.

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

src/sat/bsat/satSolver.h

Public Attributes