Rbc_Manager_t Struct Reference

RBC manager. More...

#include <rbcInt.h>

Detailed Description

RBC manager.

Handles rbcs:

dagManager, to handle the associated pool of vertices;
varTable, to index variable vertices;
varCapacity, the maximum number of variables;
one and zero, the logical constants true and false;
rbcNode2cnfVar: RBC node -> CNF var (used only in CNF convertion);
cnfVar2rbcNode: CNF var -> RBC node; (used only to obtain original variables from CNF formula solution);
maxUnchangedRbcVariable is the maximal RBC var that will have the same index in CNF (used for ease the readability of CNF formulas) It is set during the first invocation of Rbc_Convert2Cnf;
maxCnfVariable is maximal variable used in CNF formula, used to generate new unique CNF variables.
stats, for bookkeeping.

hash_ptr Rbc_Manager_t::cnfVar2rbcNode_cnf

hash_ptr Rbc_Manager_t::cnfVar2rbcNode_model

Dag_Manager_t* Rbc_Manager_t::dagManager

NuSMVEnv_ptr Rbc_Manager_t::environment

LRUCache_ptr Rbc_Manager_t::inlining_cache

int Rbc_Manager_t::maxCnfVariable

int Rbc_Manager_t::maxUnchangedRbcVariable

Rbc_t* Rbc_Manager_t::one

hash_ptr Rbc_Manager_t::rbcNode2cnfVar_cnf

hash_ptr Rbc_Manager_t::rbcNode2cnfVar_model

int Rbc_Manager_t::stats[RBCMAX_STAT]

int Rbc_Manager_t::varCapacity

Rbc_t** Rbc_Manager_t::varTable

Rbc_t* Rbc_Manager_t::zero

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