ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
Public Attributes | List of all members
Msat_Solver_t_ Struct Reference

#include <msatInt.h>

Collaboration diagram for Msat_Solver_t_:
Collaboration graph
[legend]

Public Attributes

int nClauses
 
int nClausesStart
 
Msat_ClauseVec_t * vClauses
 
Msat_ClauseVec_t * vLearned
 
double dClaInc
 
double dClaDecay
 
double * pdActivity
 
float * pFactors
 
double dVarInc
 
double dVarDecay
 
Msat_Order_t * pOrder
 
Msat_ClauseVec_t ** pvWatched
 
Msat_Queue_t * pQueue
 
int nVars
 
int nVarsAlloc
 
int * pAssigns
 
int * pModel
 
Msat_IntVec_t * vTrail
 
Msat_IntVec_t * vTrailLim
 
Msat_Clause_t ** pReasons
 
int * pLevel
 
int nLevelRoot
 
double dRandSeed
 
int fVerbose
 
double dProgress
 
Msat_IntVec_t * vConeVars
 
Msat_IntVec_t * vVarsUsed
 
Msat_ClauseVec_t * vAdjacents
 
int * pSeen
 
int nSeenId
 
Msat_IntVec_t * vReason
 
Msat_IntVec_t * vTemp
 
int * pFreq
 
Msat_MmStep_t * pMem
 
Msat_SolverStats_t Stats
 
int nTwoLits
 
int nTwoLitsL
 
int nClausesInit
 
int nClausesAlloc
 
int nClausesAllocL
 
int nBackTracks
 

Detailed Description

Definition at line 97 of file msatInt.h.

Member Data Documentation

◆ dClaDecay

double Msat_Solver_t_::dClaDecay

Definition at line 104 of file msatInt.h.

◆ dClaInc

double Msat_Solver_t_::dClaInc

Definition at line 103 of file msatInt.h.

◆ dProgress

double Msat_Solver_t_::dProgress

Definition at line 128 of file msatInt.h.

◆ dRandSeed

double Msat_Solver_t_::dRandSeed

Definition at line 125 of file msatInt.h.

◆ dVarDecay

double Msat_Solver_t_::dVarDecay

Definition at line 109 of file msatInt.h.

◆ dVarInc

double Msat_Solver_t_::dVarInc

Definition at line 108 of file msatInt.h.

◆ fVerbose

int Msat_Solver_t_::fVerbose

Definition at line 127 of file msatInt.h.

◆ nBackTracks

int Msat_Solver_t_::nBackTracks

Definition at line 152 of file msatInt.h.

◆ nClauses

int Msat_Solver_t_::nClauses

Definition at line 99 of file msatInt.h.

◆ nClausesAlloc

int Msat_Solver_t_::nClausesAlloc

Definition at line 150 of file msatInt.h.

◆ nClausesAllocL

int Msat_Solver_t_::nClausesAllocL

Definition at line 151 of file msatInt.h.

◆ nClausesInit

int Msat_Solver_t_::nClausesInit

Definition at line 149 of file msatInt.h.

◆ nClausesStart

int Msat_Solver_t_::nClausesStart

Definition at line 100 of file msatInt.h.

◆ nLevelRoot

int Msat_Solver_t_::nLevelRoot

Definition at line 123 of file msatInt.h.

◆ nSeenId

int Msat_Solver_t_::nSeenId

Definition at line 137 of file msatInt.h.

◆ nTwoLits

int Msat_Solver_t_::nTwoLits

Definition at line 147 of file msatInt.h.

◆ nTwoLitsL

int Msat_Solver_t_::nTwoLitsL

Definition at line 148 of file msatInt.h.

◆ nVars

int Msat_Solver_t_::nVars

Definition at line 115 of file msatInt.h.

◆ nVarsAlloc

int Msat_Solver_t_::nVarsAlloc

Definition at line 116 of file msatInt.h.

◆ pAssigns

int* Msat_Solver_t_::pAssigns

Definition at line 117 of file msatInt.h.

◆ pdActivity

double* Msat_Solver_t_::pdActivity

Definition at line 106 of file msatInt.h.

◆ pFactors

float* Msat_Solver_t_::pFactors

Definition at line 107 of file msatInt.h.

◆ pFreq

int* Msat_Solver_t_::pFreq

Definition at line 140 of file msatInt.h.

◆ pLevel

int* Msat_Solver_t_::pLevel

Definition at line 122 of file msatInt.h.

◆ pMem

Msat_MmStep_t* Msat_Solver_t_::pMem

Definition at line 143 of file msatInt.h.

◆ pModel

int* Msat_Solver_t_::pModel

Definition at line 118 of file msatInt.h.

◆ pOrder

Msat_Order_t* Msat_Solver_t_::pOrder

Definition at line 110 of file msatInt.h.

◆ pQueue

Msat_Queue_t* Msat_Solver_t_::pQueue

Definition at line 113 of file msatInt.h.

◆ pReasons

Msat_Clause_t** Msat_Solver_t_::pReasons

Definition at line 121 of file msatInt.h.

◆ pSeen

int* Msat_Solver_t_::pSeen

Definition at line 136 of file msatInt.h.

◆ pvWatched

Msat_ClauseVec_t** Msat_Solver_t_::pvWatched

Definition at line 112 of file msatInt.h.

◆ Stats

Msat_SolverStats_t Msat_Solver_t_::Stats

Definition at line 146 of file msatInt.h.

◆ vAdjacents

Msat_ClauseVec_t* Msat_Solver_t_::vAdjacents

Definition at line 133 of file msatInt.h.

◆ vClauses

Msat_ClauseVec_t* Msat_Solver_t_::vClauses

Definition at line 101 of file msatInt.h.

◆ vConeVars

Msat_IntVec_t* Msat_Solver_t_::vConeVars

Definition at line 131 of file msatInt.h.

◆ vLearned

Msat_ClauseVec_t* Msat_Solver_t_::vLearned

Definition at line 102 of file msatInt.h.

◆ vReason

Msat_IntVec_t* Msat_Solver_t_::vReason

Definition at line 138 of file msatInt.h.

◆ vTemp

Msat_IntVec_t* Msat_Solver_t_::vTemp

Definition at line 139 of file msatInt.h.

◆ vTrail

Msat_IntVec_t* Msat_Solver_t_::vTrail

Definition at line 119 of file msatInt.h.

◆ vTrailLim

Msat_IntVec_t* Msat_Solver_t_::vTrailLim

Definition at line 120 of file msatInt.h.

◆ vVarsUsed

Msat_IntVec_t* Msat_Solver_t_::vVarsUsed

Definition at line 132 of file msatInt.h.

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