Msat_Solver_t_ Struct Reference
#include <msatInt.h>
Collaboration diagram for Msat_Solver_t_:
Data Fields | |
| 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 |
| bool | 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 112 of file msatInt.h.
Field Documentation
| double Msat_Solver_t_::dClaDecay |
| double Msat_Solver_t_::dClaInc |
| double Msat_Solver_t_::dProgress |
| double Msat_Solver_t_::dRandSeed |
| double Msat_Solver_t_::dVarDecay |
| double Msat_Solver_t_::dVarInc |
| double* Msat_Solver_t_::pdActivity |
| float* Msat_Solver_t_::pFactors |
The documentation for this struct was generated from the following file:
- src/sat/msat/msatInt.h
