NuSMV/code/nusmv/core/rbc/rbc.h

Go to the documentation of this file.

/* ---------------------------------------------------------------------------


  This file is part of the ``rbc'' package of NuSMV version 2.
  Copyright (C) 2000-2001 by University of Genova.

  NuSMV version 2 is free software; you can redistribute it and/or
  modify it under the terms of the GNU Lesser General Public
  License as published by the Free Software Foundation; either
  version 2 of the License, or (at your option) any later version.

  NuSMV version 2 is distributed in the hope that it will be useful,
  but WITHOUT ANY WARRANTY; without even the implied warranty of
  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
  Lesser General Public License for more details.

  You should have received a copy of the GNU Lesser General Public
  License along with this library; if not, write to the Free Software
  Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307  USA.

  For more information on NuSMV see <http://nusmv.fbk.eu>
  or email to <nusmv-users@fbk.eu>.
  Please report bugs to <nusmv-users@fbk.eu>.

  To contact the NuSMV development board, email to <nusmv@fbk.eu>.

-----------------------------------------------------------------------------*/

#ifndef __NUSMV_CORE_RBC_RBC_H__
#define __NUSMV_CORE_RBC_RBC_H__


#if HAVE_CONFIG_H
# include "nusmv-config.h"
#endif

/* Standard includes. */
#if NUSMV_HAVE_MALLOC_H
# if NUSMV_HAVE_SYS_TYPES_H
#  include <sys/types.h>
# endif
# include <malloc.h>
#elif defined(NUSMV_HAVE_SYS_MALLOC_H) && NUSMV_HAVE_SYS_MALLOC_H
# if NUSMV_HAVE_SYS_TYPES_H
#  include <sys/types.h>
# endif
# include <sys/malloc.h>
#elif NUSMV_HAVE_STDLIB_H
# include <stdlib.h>
#endif

#include <stdio.h>

/* Submodule includes. */
#include "nusmv/core/dag/dag.h"
#include "nusmv/core/utils/Slist.h"
#include "nusmv/core/cinit/NuSMVEnv.h"

/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/

#define RBC_TSEITIN_CONVERSION_NAME  "tseitin"

#define RBC_SHERIDAN_CONVERSION_NAME "sheridan"

#define RBC_INVALID_CONVERSION_NAME  "invalid"

/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/

typedef enum _Rbc_2CnfAlgorithm {
  RBC_INVALID_CONVERSION = 0,
  RBC_TSEITIN_CONVERSION,
  RBC_SHERIDAN_CONVERSION
} Rbc_2CnfAlgorithm;

typedef enum Rbc_Bool {
  RBC_FALSE = DAG_ANNOTATION_BIT,
  RBC_TRUE = 0
} Rbc_Bool_c;

typedef struct RbcManager Rbc_Manager_t;

typedef Dag_Vertex_t      Rbc_t;

typedef Dag_DfsFunctions_t RbcDfsFunctions_t;

typedef void (*Rbc_ProcPtr_t)(void);

typedef int (*Rbc_IntPtr_t)(void);

/*---------------------------------------------------------------------------*/
/* Structure declarations                                                     */
/*---------------------------------------------------------------------------*/
struct RbcDfsFunctions {
  Rbc_IntPtr_t   Set;
  Rbc_ProcPtr_t  FirstVisit;
  Rbc_ProcPtr_t  BackVisit;
  Rbc_ProcPtr_t  LastVisit;
};

/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/
/*---------------------------------------------------------------------------*/
/* Macro declarations                                                        */
/*---------------------------------------------------------------------------*/

#define RBC_INVALID_SUBST_VALUE \
   INT_MAX


/*---------------------------------------------------------------------------*/
/* Function prototypes                                                       */
/*---------------------------------------------------------------------------*/

void Rbc_pkg_init(void);

void Rbc_pkg_quit(void);

int Rbc_Convert2Cnf(Rbc_Manager_t* rbcManager, Rbc_t* f,
                    int polarity, Rbc_2CnfAlgorithm alg,
                    /* outputs: */
                    Slist_ptr clauses, Slist_ptr vars,
                    int* literalAssignedToWholeFormula);

int Rbc_CnfVar2RbcIndex(Rbc_Manager_t* rbcManager, int cnfVar);

int Rbc_RbcIndex2CnfVar(Rbc_Manager_t* rbcManager, int rbcIndex);

Rbc_t* Rbc_GetOne(Rbc_Manager_t* rbcManager);

Rbc_t* Rbc_GetZero(Rbc_Manager_t* rbcManager);

boolean Rbc_IsConstant(Rbc_Manager_t* manager, Rbc_t* f);

Rbc_t* Rbc_GetIthVar(Rbc_Manager_t* rbcManager, int varIndex);

Rbc_t* Rbc_MakeNot(Rbc_Manager_t* rbcManager, Rbc_t* left);

Rbc_t* Rbc_MakeAnd(Rbc_Manager_t* rbcManager, Rbc_t* left, Rbc_t* right, Rbc_Bool_c sign);

Rbc_t* Rbc_MakeOr(Rbc_Manager_t* rbcManager, Rbc_t* left, Rbc_t* right, Rbc_Bool_c sign);

Rbc_t* Rbc_MakeIff(Rbc_Manager_t* rbcManager, Rbc_t* left, Rbc_t* right, Rbc_Bool_c sign);

Rbc_t* Rbc_MakeXor(Rbc_Manager_t* rbcManager, Rbc_t* left, Rbc_t* right, Rbc_Bool_c sign);

Rbc_t* Rbc_MakeIte(Rbc_Manager_t* rbcManager, Rbc_t* c, Rbc_t* t, Rbc_t* e,
Rbc_Bool_c sign);

Rbc_t* Rbc_GetLeftOpnd(Rbc_t* f);

Rbc_t* Rbc_GetRightOpnd(Rbc_t* f);

int Rbc_GetVarIndex(Rbc_t* f);

void Rbc_Mark(Rbc_Manager_t* rbc, Rbc_t* f);

void Rbc_Unmark(Rbc_Manager_t* rbc, Rbc_t* f);

Rbc_Manager_t* Rbc_ManagerAlloc(const NuSMVEnv_ptr env, int varCapacity);

void Rbc_ManagerReserve(Rbc_Manager_t* rbcManager, int newVarCapacity);

void Rbc_ManagerReset(Rbc_Manager_t* rbcManager);

int Rbc_ManagerCapacity(Rbc_Manager_t* rbcManager);

void Rbc_ManagerFree(Rbc_Manager_t* rbcManager);

void Rbc_ManagerGC(Rbc_Manager_t* rbcManager);

NuSMVEnv_ptr Rbc_ManagerGetEnvironment(Rbc_Manager_t* rbcManager);

void
Rbc_OutputDaVinci(Rbc_Manager_t* rbcManager, Rbc_t* f, FILE* outFile);

void
Rbc_OutputSexpr(Rbc_Manager_t* rbcManager, Rbc_t* f, FILE* outFile);

void
Rbc_OutputGdl(Rbc_Manager_t* rbcManager, Rbc_t* f, FILE* outFile);

Rbc_t*
Rbc_Subst(Rbc_Manager_t* rbcManager, Rbc_t* f, int* subst);

Rbc_t* Rbc_LogicalSubst(Rbc_Manager_t* rbcManager, Rbc_t* f,
                               int* subst, const int* log2phy,
                               const int* phy2log);

Rbc_t* Rbc_Shift(Rbc_Manager_t* rbcManager, Rbc_t* f, int shift);

Rbc_t*
Rbc_LogicalShift(Rbc_Manager_t* rbcManager, Rbc_t* f,
                 int shift, const int* log2phy, const int* phy2log);

Rbc_t*
Rbc_SubstRbc(Rbc_Manager_t* rbcManager, Rbc_t* f, Rbc_t** substRbc);

Rbc_t*
Rbc_LogicalSubstRbc(Rbc_Manager_t* rbcManager, Rbc_t* f,
                    Rbc_t** substRbc, int* phy2log);

void
Rbc_PrintStats(Rbc_Manager_t* rbcManager, int clustSz, FILE* outFile);

Slist_ptr
RbcUtils_get_dependencies(Rbc_Manager_t* rbcManager, Rbc_t* f,
                          boolean reset_dag);

struct InlineResult_TAG*
RbcInline_apply_inlining(Rbc_Manager_t* rbcm, Rbc_t* f);

Rbc_2CnfAlgorithm
Rbc_CnfConversionAlgorithmFromStr(const char* str);

const char *
Rbc_CnfConversionAlgorithm2Str(Rbc_2CnfAlgorithm algo);

const char *
Rbc_CnfGetValidRbc2CnfAlgorithms(void);

boolean Rbc_is_top(Rbc_t* rbc);

boolean Rbc_is_var(Rbc_t* rbc);

boolean Rbc_is_and(Rbc_t* rbc);

boolean Rbc_is_iff(Rbc_t* rbc);

boolean Rbc_is_ite(Rbc_t* rbc);

RbcDfsFunctions_t*
Rbc_ManagerGetDfsCleanFun(Rbc_Manager_t* rbcManager);

void Rbc_Dfs_exported(Rbc_t* dfsRoot,
                             RbcDfsFunctions_t* dfsFun,
                             void* dfsData,
                             Rbc_Manager_t* manager);

void Rbc_Dfs_clean_exported(Rbc_t* dfsRoot,
                                   Rbc_Manager_t* manager);

#endif /* __NUSMV_CORE_RBC_RBC_H__ */

---