abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
Data Fields
sat_solver_t Struct Reference

#include <satSolver.h>

Data Fields

int size
 
int cap
 
int qhead
 
int qtail
 
Sat_Mem_t Mem
 
int hLearnts
 
int hBinary
 
clause * binary
 
veci * wlists
 
veci act_clas
 
int iVarPivot
 
int iTrailPivot
 
int hProofPivot
 
int var_inc
 
int var_inc2
 
int cla_inc
 
unsigned * activity
 
unsigned * activity2
 
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 * 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 91 of file satSolver.h.

Field Documentation

veci sat_solver_t::act_clas

Definition at line 104 of file satSolver.h.

veci sat_solver_t::act_vars

Definition at line 167 of file satSolver.h.

unsigned* sat_solver_t::activity

Definition at line 122 of file satSolver.h.

unsigned* sat_solver_t::activity2

Definition at line 123 of file satSolver.h.

char* sat_solver_t::assigns

Definition at line 130 of file satSolver.h.

clause* sat_solver_t::binary

Definition at line 102 of file satSolver.h.

int sat_solver_t::cap

Definition at line 94 of file satSolver.h.

int sat_solver_t::cla_inc

Definition at line 121 of file satSolver.h.

veci sat_solver_t::conf_final

Definition at line 145 of file satSolver.h.

double* sat_solver_t::factors

Definition at line 168 of file satSolver.h.

int sat_solver_t::fNotUseRandom

Definition at line 176 of file satSolver.h.

int sat_solver_t::fSkipSimplify

Definition at line 175 of file satSolver.h.

int sat_solver_t::fSolved

Definition at line 181 of file satSolver.h.

int sat_solver_t::fVerbose

Definition at line 154 of file satSolver.h.

int sat_solver_t::hBinary

Definition at line 101 of file satSolver.h.

int sat_solver_t::hLearnts

Definition at line 100 of file satSolver.h.

int sat_solver_t::hProofPivot

Definition at line 109 of file satSolver.h.

int sat_solver_t::iTrailPivot

Definition at line 108 of file satSolver.h.

int sat_solver_t::iVarPivot

Definition at line 107 of file satSolver.h.

int* sat_solver_t::levels

Definition at line 129 of file satSolver.h.

char* sat_solver_t::loads

Definition at line 133 of file satSolver.h.

Sat_Mem_t sat_solver_t::Mem

Definition at line 99 of file satSolver.h.

int* sat_solver_t::model

Definition at line 144 of file satSolver.h.

int sat_solver_t::nCalls

Definition at line 170 of file satSolver.h.

int sat_solver_t::nCalls2

Definition at line 171 of file satSolver.h.

int sat_solver_t::nClauses

Definition at line 185 of file satSolver.h.

ABC_INT64_T sat_solver_t::nConfLimit

Definition at line 163 of file satSolver.h.

int sat_solver_t::nDBreduces

Definition at line 161 of file satSolver.h.

ABC_INT64_T sat_solver_t::nInsLimit

Definition at line 164 of file satSolver.h.

int sat_solver_t::nLearntDelta

Definition at line 159 of file satSolver.h.

int sat_solver_t::nLearntMax

Definition at line 157 of file satSolver.h.

int sat_solver_t::nLearntRatio

Definition at line 160 of file satSolver.h.

int sat_solver_t::nLearntStart

Definition at line 158 of file satSolver.h.

int sat_solver_t::nRestarts

Definition at line 169 of file satSolver.h.

int sat_solver_t::nRoots

Definition at line 186 of file satSolver.h.

abctime sat_solver_t::nRuntimeLimit

Definition at line 165 of file satSolver.h.

int sat_solver_t::nVarUsed

Definition at line 126 of file satSolver.h.

veci sat_solver_t::order

Definition at line 141 of file satSolver.h.

int* sat_solver_t::orderpos

Definition at line 135 of file satSolver.h.

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

Definition at line 192 of file satSolver.h.

void* sat_solver_t::pCnfMan

Definition at line 191 of file satSolver.h.

FILE* sat_solver_t::pFile

Definition at line 184 of file satSolver.h.

char* sat_solver_t::pFreqs

Definition at line 125 of file satSolver.h.

int* sat_solver_t::pGlobalVars

Definition at line 178 of file satSolver.h.

veci sat_solver_t::pivot_vars

Definition at line 173 of file satSolver.h.

char* sat_solver_t::polarity

Definition at line 131 of file satSolver.h.

double sat_solver_t::progress_estimate

Definition at line 152 of file satSolver.h.

void* sat_solver_t::pStore

Definition at line 180 of file satSolver.h.

int sat_solver_t::qhead

Definition at line 95 of file satSolver.h.

int sat_solver_t::qtail

Definition at line 96 of file satSolver.h.

double sat_solver_t::random_seed

Definition at line 151 of file satSolver.h.

int* sat_solver_t::reasons

Definition at line 136 of file satSolver.h.

int sat_solver_t::root_level

Definition at line 148 of file satSolver.h.

int sat_solver_t::simpdb_assigns

Definition at line 149 of file satSolver.h.

int sat_solver_t::simpdb_props

Definition at line 150 of file satSolver.h.

int sat_solver_t::size

Definition at line 93 of file satSolver.h.

veci sat_solver_t::stack

Definition at line 139 of file satSolver.h.

stats_t sat_solver_t::stats

Definition at line 156 of file satSolver.h.

veci sat_solver_t::tagged

Definition at line 138 of file satSolver.h.

char* sat_solver_t::tags

Definition at line 132 of file satSolver.h.

veci sat_solver_t::temp_clause

Definition at line 188 of file satSolver.h.

lit* sat_solver_t::trail

Definition at line 137 of file satSolver.h.

veci sat_solver_t::trail_lim

Definition at line 142 of file satSolver.h.

veci sat_solver_t::unit_lits

Definition at line 172 of file satSolver.h.

int sat_solver_t::var_inc

Definition at line 119 of file satSolver.h.

int sat_solver_t::var_inc2

Definition at line 120 of file satSolver.h.

int sat_solver_t::verbosity

Definition at line 153 of file satSolver.h.

veci* sat_solver_t::wlists

Definition at line 103 of file satSolver.h.

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