#include <satSolver3.h>

Collaboration diagram for sat_solver3_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

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

void *	pCnfMan

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

Detailed Description

Definition at line 99 of file satSolver3.h.

Member Data Documentation

◆ act_clas

veci sat_solver3_t::act_clas

Definition at line 128 of file satSolver3.h.

◆ act_vars

veci sat_solver3_t::act_vars

Definition at line 172 of file satSolver3.h.

◆ activity

word* sat_solver3_t::activity

Definition at line 124 of file satSolver3.h.

◆ activity2

word* sat_solver3_t::activity2

Definition at line 125 of file satSolver3.h.

◆ assigns

char* sat_solver3_t::assigns

Definition at line 135 of file satSolver3.h.

◆ binary

clause* sat_solver3_t::binary

Definition at line 110 of file satSolver3.h.

◆ cap

int sat_solver3_t::cap

Definition at line 102 of file satSolver3.h.

◆ cla_decay

unsigned sat_solver3_t::cla_decay

Definition at line 127 of file satSolver3.h.

◆ cla_inc

unsigned sat_solver3_t::cla_inc

Definition at line 126 of file satSolver3.h.

◆ ClaActType

int sat_solver3_t::ClaActType

Definition at line 120 of file satSolver3.h.

◆ conf_final

veci sat_solver3_t::conf_final

Definition at line 150 of file satSolver3.h.

◆ factors

double* sat_solver3_t::factors

Definition at line 173 of file satSolver3.h.

◆ fNoRestarts

int sat_solver3_t::fNoRestarts

Definition at line 182 of file satSolver3.h.

◆ fNotUseRandom

int sat_solver3_t::fNotUseRandom

Definition at line 181 of file satSolver3.h.

◆ fSkipSimplify

int sat_solver3_t::fSkipSimplify

Definition at line 180 of file satSolver3.h.

◆ fSolved

int sat_solver3_t::fSolved

Definition at line 187 of file satSolver3.h.

◆ fVerbose

int sat_solver3_t::fVerbose

Definition at line 159 of file satSolver3.h.

◆ hBinary

int sat_solver3_t::hBinary

Definition at line 109 of file satSolver3.h.

◆ hLearnts

int sat_solver3_t::hLearnts

Definition at line 108 of file satSolver3.h.

◆ hProofPivot

int sat_solver3_t::hProofPivot

Definition at line 116 of file satSolver3.h.

◆ iTrailPivot

int sat_solver3_t::iTrailPivot

Definition at line 115 of file satSolver3.h.

◆ iVarPivot

int sat_solver3_t::iVarPivot

Definition at line 114 of file satSolver3.h.

◆ levels

int* sat_solver3_t::levels

Definition at line 134 of file satSolver3.h.

◆ loads

char* sat_solver3_t::loads

Definition at line 138 of file satSolver3.h.

◆ Mem

Sat_Mem_t sat_solver3_t::Mem

Definition at line 107 of file satSolver3.h.

◆ model

int* sat_solver3_t::model

Definition at line 149 of file satSolver3.h.

◆ nCalls

int sat_solver3_t::nCalls

Definition at line 175 of file satSolver3.h.

◆ nCalls2

int sat_solver3_t::nCalls2

Definition at line 176 of file satSolver3.h.

◆ nClauses

int sat_solver3_t::nClauses

Definition at line 191 of file satSolver3.h.

◆ nConfLimit

ABC_INT64_T sat_solver3_t::nConfLimit

Definition at line 168 of file satSolver3.h.

◆ nDBreduces

int sat_solver3_t::nDBreduces

Definition at line 166 of file satSolver3.h.

◆ nInsLimit

ABC_INT64_T sat_solver3_t::nInsLimit

Definition at line 169 of file satSolver3.h.

◆ nLearntDelta

int sat_solver3_t::nLearntDelta

Definition at line 164 of file satSolver3.h.

◆ nLearntMax

int sat_solver3_t::nLearntMax

Definition at line 162 of file satSolver3.h.

◆ nLearntRatio

int sat_solver3_t::nLearntRatio

Definition at line 165 of file satSolver3.h.

◆ nLearntStart

int sat_solver3_t::nLearntStart

Definition at line 163 of file satSolver3.h.

◆ nRestarts

int sat_solver3_t::nRestarts

Definition at line 174 of file satSolver3.h.

◆ nRoots

int sat_solver3_t::nRoots

Definition at line 192 of file satSolver3.h.

◆ nRuntimeLimit

abctime sat_solver3_t::nRuntimeLimit

Definition at line 170 of file satSolver3.h.

◆ nVarUsed

int sat_solver3_t::nVarUsed

Definition at line 131 of file satSolver3.h.

◆ order

veci sat_solver3_t::order

Definition at line 146 of file satSolver3.h.

◆ orderpos

int* sat_solver3_t::orderpos

Definition at line 140 of file satSolver3.h.

◆ pCnfFunc

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

Definition at line 198 of file satSolver3.h.

◆ pCnfMan

void* sat_solver3_t::pCnfMan

Definition at line 197 of file satSolver3.h.

◆ pFile

FILE* sat_solver3_t::pFile

Definition at line 190 of file satSolver3.h.

◆ pFreqs

char* sat_solver3_t::pFreqs

Definition at line 130 of file satSolver3.h.

◆ pGlobalVars

int* sat_solver3_t::pGlobalVars

Definition at line 184 of file satSolver3.h.

◆ pivot_vars

veci sat_solver3_t::pivot_vars

Definition at line 178 of file satSolver3.h.

◆ polarity

char* sat_solver3_t::polarity

Definition at line 136 of file satSolver3.h.

◆ progress_estimate

double sat_solver3_t::progress_estimate

Definition at line 157 of file satSolver3.h.

◆ pStore

void* sat_solver3_t::pStore

Definition at line 186 of file satSolver3.h.

◆ qhead

int sat_solver3_t::qhead

Definition at line 103 of file satSolver3.h.

◆ qtail

int sat_solver3_t::qtail

Definition at line 104 of file satSolver3.h.

◆ random_seed

double sat_solver3_t::random_seed

Definition at line 156 of file satSolver3.h.

◆ reasons

int* sat_solver3_t::reasons

Definition at line 141 of file satSolver3.h.

◆ root_level

int sat_solver3_t::root_level

Definition at line 153 of file satSolver3.h.

◆ simpdb_assigns

int sat_solver3_t::simpdb_assigns

Definition at line 154 of file satSolver3.h.

◆ simpdb_props

int sat_solver3_t::simpdb_props

Definition at line 155 of file satSolver3.h.

◆ size

int sat_solver3_t::size

Definition at line 101 of file satSolver3.h.

◆ stack

veci sat_solver3_t::stack

Definition at line 144 of file satSolver3.h.

◆ stats

stats_t sat_solver3_t::stats

Definition at line 161 of file satSolver3.h.

◆ tagged

veci sat_solver3_t::tagged

Definition at line 143 of file satSolver3.h.

◆ tags

char* sat_solver3_t::tags

Definition at line 137 of file satSolver3.h.

◆ temp_clause

veci sat_solver3_t::temp_clause

Definition at line 194 of file satSolver3.h.

◆ trail

lit* sat_solver3_t::trail

Definition at line 142 of file satSolver3.h.

◆ trail_lim

veci sat_solver3_t::trail_lim

Definition at line 147 of file satSolver3.h.

◆ unit_lits

veci sat_solver3_t::unit_lits

Definition at line 177 of file satSolver3.h.

◆ var_decay

word sat_solver3_t::var_decay

Definition at line 123 of file satSolver3.h.

◆ var_inc

word sat_solver3_t::var_inc

Definition at line 121 of file satSolver3.h.

◆ var_inc2

word sat_solver3_t::var_inc2

Definition at line 122 of file satSolver3.h.

◆ VarActType

int sat_solver3_t::VarActType

Definition at line 119 of file satSolver3.h.

◆ verbosity

int sat_solver3_t::verbosity

Definition at line 158 of file satSolver3.h.

◆ wlists

veci* sat_solver3_t::wlists

Definition at line 111 of file satSolver3.h.

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

src/sat/bsat/satSolver3.h

Public Attributes