NuSMV/code/nusmv/core/bmc/sbmc/sbmcUtils.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_UTILS_H__
#define __NUSMV_CORE_BMC_SBMC_SBMC_UTILS_H__

#include "nusmv/core/prop/propPkg.h"
#include "nusmv/core/bmc/sbmc/sbmcStructs.h"
#include "nusmv/core/enc/enc.h"
#include "nusmv/core/enc/be/BeEnc.h"
#include "nusmv/core/trace/Trace.h"
#include "nusmv/core/trace/TraceMgr.h"
#include "nusmv/core/sat/sat.h" /* for solver and result */
#include "nusmv/core/utils/utils.h"
#include "nusmv/core/utils/assoc.h"

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


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

typedef struct sbmc_MetaSolver_TAG sbmc_MetaSolver;

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


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


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

#define sbmc_SNH_text "%s:%d: Should not happen"

#define sbmc_SNYI_text "%s:%d: Something not yet implemented\n"


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

int sbmc_get_unique_id(const NuSMVEnv_ptr env);

void sbmc_reset_unique_id(const NuSMVEnv_ptr env);

void sbmc_increment_unique_id(const NuSMVEnv_ptr env);

void sbmc_print_node(const NuSMVEnv_ptr env,
                            FILE * out, const char * prefix, node_ptr node,
                            const char * postfix);

void sbmc_print_node_list(const NuSMVEnv_ptr env,
                                 FILE *out, lsList l);

node_ptr sbmc_add_new_state_variable(const NuSMVEnv_ptr env,
                                            SymbLayer_ptr layer,
                                            const char *name);

lsList sbmc_find_formula_vars(const NuSMVEnv_ptr env, node_ptr ltlspec);

void sbmc_print_varmap(const NuSMVEnv_ptr env, FILE *out,
                              node_ptr node, sbmc_node_info *info);

void sbmc_print_Gvarmap(const NuSMVEnv_ptr env, FILE *out,
                               node_ptr var, node_ptr formula);

void sbmc_print_Fvarmap(const NuSMVEnv_ptr env, FILE *out,
                               node_ptr var, node_ptr formula);

node_ptr sbmc_1_fresh_state_var(const NuSMVEnv_ptr env,
                                       SymbLayer_ptr layer, unsigned int *index);

array_t * sbmc_n_fresh_state_vars(const NuSMVEnv_ptr env,
                                         SymbLayer_ptr layer, const unsigned int n,
                            unsigned int *index);

void sbmc_allocate_trans_vars(const NuSMVEnv_ptr env,
                                     sbmc_node_info *info, SymbLayer_ptr layer,
                                     lsList state_vars_formula_pd0,
                                     lsList state_vars_formula_pdx,
                                     unsigned int *new_var_index);

node_ptr sbmc_make_boolean_formula(BddEnc_ptr bdd_enc, Prop_ptr ltlprop);

void sbmc_find_relevant_vars(state_vars_struct *svs,
                                        BeFsm_ptr be_fsm, node_ptr bltlspec);

Trace_ptr
Sbmc_Utils_generate_cntexample(BeEnc_ptr be_enc, sbmc_MetaSolver * solver,
                               node_ptr l_var, const int k,
                               const char * trace_name,
                               NodeList_ptr symbols);

Trace_ptr
Sbmc_Utils_generate_and_print_cntexample(BeEnc_ptr be_enc,
                                         TraceMgr_ptr tm,
                                         sbmc_MetaSolver * solver,
                                         node_ptr l_var,
                                         const int k,
                                         const char * trace_name,
                                         NodeList_ptr symbols);

Trace_ptr
Sbmc_Utils_fill_cntexample(BeEnc_ptr be_enc, sbmc_MetaSolver * solver,
                           node_ptr l_var, const int k, Trace_ptr trace);

int sbmc_L_state(void);

int sbmc_E_state(void);

int sbmc_real_k(int k);

unsigned int sbmc_model_k(int k);

char* sbmc_real_k_string(const unsigned int k_real);

sbmc_MetaSolver * sbmc_MS_create(BeEnc_ptr be_enc);

void sbmc_MS_destroy(sbmc_MetaSolver *ms);

void sbmc_MS_create_volatile_group(sbmc_MetaSolver *ms);

void sbmc_MS_destroy_volatile_group(sbmc_MetaSolver *ms);

void sbmc_MS_switch_to_permanent_group(sbmc_MetaSolver *ms);

void sbmc_MS_switch_to_volatile_group(sbmc_MetaSolver *ms);

void sbmc_MS_goto_permanent_group(sbmc_MetaSolver *ms);

void sbmc_MS_goto_volatile_group(sbmc_MetaSolver *ms);

void sbmc_MS_force_true(sbmc_MetaSolver *ms, be_ptr be_constraint,
                        Be_CnfAlgorithm cnf_alg);

void sbmc_MS_force_constraint_list(sbmc_MetaSolver *ms, lsList constraints,
                                   Be_CnfAlgorithm cnf_alg);

SatSolverResult sbmc_MS_solve(sbmc_MetaSolver *ms);

SatSolverResult sbmc_MS_solve_assume(sbmc_MetaSolver *ms, Slist_ptr assumptions);

SatSolver_ptr sbmc_MS_get_solver(sbmc_MetaSolver *ms);

Slist_ptr sbmc_MS_get_conflicts(sbmc_MetaSolver *ms);

Slist_ptr sbmc_MS_get_model(sbmc_MetaSolver *ms);

void sbmc_add_loop_variable(BddEnc_ptr bdd_enc, BeFsm_ptr fsm);

void sbmc_remove_loop_variable(BddEnc_ptr bdd_enc, BeFsm_ptr fsm);

void sbmc_loop_var_name_set(const NuSMVEnv_ptr env, node_ptr n);

node_ptr sbmc_loop_var_name_get(const NuSMVEnv_ptr env);

#endif /* __NUSMV_CORE_BMC_SBMC_SBMC_UTILS_H__ */

---