NuSMV/code/nusmv/core/be/be.h

Go to the documentation of this file.

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


  This file is part of the ``be'' package of NuSMV version 2.
  Copyright (C) 2000-2001 by FBK-irst and University of Trento.

  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_BE_BE_H__
#define __NUSMV_CORE_BE_BE_H__

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

typedef struct Be_Manager_TAG* Be_Manager_ptr; /* generic be manger */


typedef struct Be_Cnf_TAG* Be_Cnf_ptr; /* cnf representation */


typedef void* be_ptr;


typedef be_ptr (*Be_Spec2Be_fun)(Be_Manager_ptr self, void* spec_be);


typedef void*  (*Be_Be2Spec_fun)(Be_Manager_ptr self, be_ptr be);


#include "nusmv/core/rbc/rbc.h"
typedef Rbc_2CnfAlgorithm Be_CnfAlgorithm;


#include <limits.h>
/* ================================================== */
/* Put here any specific boolean expression manager
   interface header: */
#include "nusmv/core/be/beRbcManager.h"
/* ================================================== */

#include "nusmv/core/utils/Slist.h"
#include "nusmv/core/cinit/NuSMVEnv.h"


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

#define BE_INVALID_SUBST_VALUE RBC_INVALID_SUBST_VALUE

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

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


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

/* ================================================== */
/* Package constructor/destructor: */

void Be_Init(void);

void Be_Quit(void);
/* ================================================== */


/* ================================================== */
/* Be_Manager public interface: */

NuSMVEnv_ptr Be_Manager_GetEnvironment(const Be_Manager_ptr self);

be_ptr Be_Manager_Spec2Be(const Be_Manager_ptr self,
                                  void* spec_expr);

void* Be_Manager_Be2Spec(const Be_Manager_ptr self, be_ptr be);

void* Be_Manager_GetSpecManager(Be_Manager_ptr self);
/* ================================================== */


/* ==================================================  */
/* Be_Cnf class constructor, destructor and modifiers */

Be_Cnf_ptr Be_Cnf_Create(const be_ptr be);

void Be_Cnf_Delete(Be_Cnf_ptr self);

void Be_Cnf_RemoveDuplicateLiterals(Be_Cnf_ptr self);
/* ==================================================  */

/* ================================================== */
/* Be_Cnf class access members: (for special case,a constant,see Be_Cnf_ptr)*/

be_ptr Be_Cnf_GetOriginalProblem(const Be_Cnf_ptr self);

int Be_Cnf_GetFormulaLiteral(const Be_Cnf_ptr self);

Slist_ptr Be_Cnf_GetVarsList(const Be_Cnf_ptr self);

Slist_ptr Be_Cnf_GetClausesList(const Be_Cnf_ptr self);

int Be_Cnf_GetMaxVarIndex(const Be_Cnf_ptr self);

size_t Be_Cnf_GetVarsNumber(const Be_Cnf_ptr self);

size_t Be_Cnf_GetClausesNumber(const Be_Cnf_ptr self);

void Be_Cnf_SetFormulaLiteral(const Be_Cnf_ptr self,
                                         const int formula_literal);

void Be_Cnf_SetMaxVarIndex(const Be_Cnf_ptr self,
                                      const int max_idx);
/* ================================================== */


/* ================================================== */
/* BE logical operations interface: */

boolean Be_IsTrue(Be_Manager_ptr manager, be_ptr arg);

boolean Be_IsFalse(Be_Manager_ptr manager, be_ptr arg);

boolean Be_IsConstant(Be_Manager_ptr manager, be_ptr arg);

be_ptr  Be_Truth(Be_Manager_ptr manager);

be_ptr  Be_Falsity(Be_Manager_ptr manager);

be_ptr  Be_Not(Be_Manager_ptr manager, be_ptr arg);

be_ptr
Be_And(Be_Manager_ptr manager, be_ptr arg1, be_ptr arg2);

be_ptr
Be_Or(Be_Manager_ptr manager, be_ptr arg1, be_ptr arg2);

be_ptr
Be_Xor(Be_Manager_ptr manager, be_ptr arg1, be_ptr arg2);

be_ptr
Be_Implies(Be_Manager_ptr manager, be_ptr arg1, be_ptr arg2);

be_ptr
Be_Iff(Be_Manager_ptr manager, be_ptr arg1, be_ptr arg2);

be_ptr
Be_Ite(Be_Manager_ptr manager, be_ptr arg_if,
       be_ptr arg_then, be_ptr arg_else);

be_ptr
Be_LogicalShiftVar(Be_Manager_ptr manager, be_ptr f,
                   int shift,
                   const int* log2phy,
                   const int* phy2log);

be_ptr
Be_LogicalVarSubst(Be_Manager_ptr manager, be_ptr f,
                   int* subst,
                   const int* log2phy,
                   const int* phy2log);


/* ================================================== */


/* ================================================== */
/* Utilities interface: */

Be_Cnf_ptr
Be_ConvertToCnf(Be_Manager_ptr manager, be_ptr f, int polarity,
                Be_CnfAlgorithm alg);

int Be_CnfLiteral2BeLiteral(const Be_Manager_ptr self,
                                   int cnfLiteral);

int Be_BeLiteral2CnfLiteral(const Be_Manager_ptr self,
                                   int beLiteral);

int Be_BeLiteral2BeIndex(const Be_Manager_ptr self,
                                int beLiteral);

int Be_BeIndex2BeLiteral(const Be_Manager_ptr self,
                                int beIndex);

int Be_BeIndex2CnfLiteral(const Be_Manager_ptr self,
                                 int beIndex);

Slist_ptr Be_CnfModelToBeModel(Be_Manager_ptr manager,
                                      const Slist_ptr cnfModel);

void
Be_DumpDavinci(Be_Manager_ptr manager, be_ptr f, FILE* outFile);

void
Be_DumpGdl(Be_Manager_ptr manager, be_ptr f, FILE* outFile);

void
Be_DumpSexpr(Be_Manager_ptr manager, be_ptr f, FILE* outFile);

/* index<->be conversion layer: */

be_ptr Be_Index2Var(Be_Manager_ptr manager, int varIndex);

int Be_Var2Index(Be_Manager_ptr manager, be_ptr var);

/* miscellaneous */

boolean Be_CnfLiteral_IsSignPositive(const Be_Manager_ptr self,
                                            int cnfLiteral);

int Be_CnfLiteral_Negate(const Be_Manager_ptr self,
                                int cnfLiteral);

boolean Be_BeLiteral_IsSignPositive(const Be_Manager_ptr self,
                                           int beLiteral);

int Be_BeLiteral_Negate(const Be_Manager_ptr self,
                               int beLiteral);

be_ptr
Be_apply_inlining(Be_Manager_ptr self, be_ptr f, boolean add_conj);

void
Be_Cnf_PrintStat(const Be_Cnf_ptr self, FILE* outFile, char* prefix);

/* ================================================== */

#endif /* __NUSMV_CORE_BE_BE_H__ */

---