NuSMV/code/nusmv/core/bmc/sbmc/sbmcStructs.h

Go to the documentation of this file.

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


  This file is part of the ``bmc.sbmc'' package of NuSMV version 2. 
  Copyright (C) 2006 by Tommi Junttila, Timo Latvala.

  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_BMC_SBMC_SBMC_STRUCTS_H__
#define __NUSMV_CORE_BMC_SBMC_SBMC_STRUCTS_H__


#include "nusmv/core/node/node.h"

#include "nusmv/core/utils/utils.h"
#include "nusmv/core/utils/list.h"
#include "nusmv/core/utils/assoc.h"
#include "nusmv/core/utils/array.h"

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


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

typedef struct state_vars_struct_TAG  state_vars_struct;

typedef struct sbmc_node_info_struct sbmc_node_info;

/*---------------------------------------------------------------------------*/
/* Structure declarations                                                    */
/*---------------------------------------------------------------------------*/


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


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


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

state_vars_struct* sbmc_state_vars_create(const NuSMVEnv_ptr env);

void sbmc_state_vars_destroy(state_vars_struct* svs);

lsList sbmc_state_vars_get_trans_state_vars(const state_vars_struct * ss);

node_ptr sbmc_state_vars_get_l_var(const state_vars_struct * ss);

node_ptr sbmc_state_vars_get_LoopExists_var(const state_vars_struct * ss);

node_ptr sbmc_state_vars_get_LastState_var(const state_vars_struct * ss);

lsList sbmc_state_vars_get_translation_vars_pd0(const state_vars_struct * ss);

lsList sbmc_state_vars_get_translation_vars_pdx(const state_vars_struct * ss);

lsList sbmc_state_vars_get_translation_vars_aux(const state_vars_struct * ss);

lsList sbmc_state_vars_get_formula_state_vars(const state_vars_struct * ss);

lsList sbmc_state_vars_get_formula_input_vars(const state_vars_struct * ss);

lsList sbmc_state_vars_get_simple_path_system_vars(const state_vars_struct * ss);

void sbmc_state_vars_set_trans_state_vars(state_vars_struct * ss, lsList f);

void sbmc_state_vars_set_l_var(state_vars_struct * ss, node_ptr f);

void sbmc_state_vars_set_LoopExists_var(state_vars_struct * ss, node_ptr f);

void sbmc_state_vars_set_LastState_var(state_vars_struct * ss, node_ptr f);

void sbmc_state_vars_set_translation_vars_pd0(state_vars_struct * ss, lsList f);

void sbmc_state_vars_set_translation_vars_pdx(state_vars_struct * ss, lsList f);

void sbmc_state_vars_set_translation_vars_aux(state_vars_struct * ss, lsList f);

void sbmc_state_vars_set_formula_state_vars(state_vars_struct * ss, lsList f);

void sbmc_state_vars_set_formula_input_vars(state_vars_struct * ss, lsList f);

void sbmc_state_vars_set_simple_path_system_vars(state_vars_struct * ss, lsList f);

void sbmc_state_vars_print(state_vars_struct *svs, FILE* out);

hash_ptr sbmc_set_create(void);

void sbmc_set_destroy(hash_ptr hash);

void sbmc_set_insert(hash_ptr hash, node_ptr bexp);

int sbmc_set_is_in(hash_ptr hash, node_ptr bexp);

sbmc_node_info * sbmc_alloc_node_info(void);

void sbmc_node_info_free(sbmc_node_info * info);

unsigned int sbmc_node_info_get_past_depth(sbmc_node_info * h);

array_t * sbmc_node_info_get_trans_vars(sbmc_node_info * h);

array_t * sbmc_node_info_get_trans_bes(sbmc_node_info * h);

node_ptr sbmc_node_info_get_aux_F_node(sbmc_node_info * h);

array_t * sbmc_node_info_get_aux_F_trans(sbmc_node_info * h);

node_ptr sbmc_node_info_get_aux_G_node(sbmc_node_info * h);

array_t * sbmc_node_info_get_aux_G_trans(sbmc_node_info * h);

void sbmc_node_info_set_past_depth(sbmc_node_info * h, unsigned int s);

void sbmc_node_info_set_past_trans_vars(sbmc_node_info * h, array_t * s);

void sbmc_node_info_set_trans_bes(sbmc_node_info * h, array_t * s);

void sbmc_node_info_set_aux_F_node(sbmc_node_info * h, node_ptr s);

void sbmc_node_info_set_aux_F_trans(sbmc_node_info * h, array_t * s);

void sbmc_node_info_set_aux_G_node(sbmc_node_info * h, node_ptr s);

void sbmc_node_info_set_aux_G_trans(sbmc_node_info * h, array_t * s);

sbmc_node_info * sbmc_node_info_assoc_find(hash_ptr a, node_ptr n);

void sbmc_node_info_assoc_insert(hash_ptr a, node_ptr n, sbmc_node_info * i);

void sbmc_node_info_assoc_free(hash_ptr * a);

hash_ptr sbmc_node_info_assoc_create(void);

#endif /* _SBCM_UTIL */

---