NuSMV/code/nusmv/core/enc/bdd/BddEnc.h

Go to the documentation of this file.

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

  This file is part of the ``enc.bdd'' package of NuSMV version 2.
  Copyright (C) 2004 by FBK-irst.

  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_ENC_BDD_BDD_ENC_H__
#define __NUSMV_CORE_ENC_BDD_BDD_ENC_H__

#include "nusmv/core/enc/bdd/bdd.h"
#include "nusmv/core/enc/base/BoolEncClient.h"
#include "nusmv/core/enc/bool/BoolEnc.h"
#include "nusmv/core/enc/utils/OrdGroups.h"

#include "nusmv/core/compile/symb_table/SymbTable.h"
#include "nusmv/core/wff/ExprMgr.h"
#include "nusmv/core/fsm/bdd/bdd.h"
#include "nusmv/core/dd/dd.h"
#include "nusmv/core/dd/VarsHandler.h"

#include "nusmv/core/utils/utils.h"
#include "nusmv/core/utils/object.h"
#include "nusmv/core/utils/assoc.h"
#include "nusmv/core/utils/OStream.h"

#include "nusmv/core/enc/utils/AddArray.h"

typedef struct BddEnc_TAG*  BddEnc_ptr;

typedef void (*VPFNNF)(FILE*, node_ptr, node_ptr);

typedef void (*VPFBEFNNV)(BddEnc_ptr, OStream_ptr, node_ptr, node_ptr, void*);

typedef enum { DUMP_FORMAT_INVALID,
               DUMP_FORMAT_DOT,
               DUMP_FORMAT_DAVINCI,
} t_format;

#define BDD_ENC(self) \
         ((BddEnc_ptr) self)

#define BDD_ENC_CHECK_INSTANCE(self) \
         (nusmv_assert(BDD_ENC(self) != BDD_ENC(NULL)))

typedef enum {
  DUMP_DEFAULT,
  DUMP_BITS,
  DUMP_SCALARS_ONLY
} VarOrderingType;



#define __BDDENC_LAZY_COMMIT_LAYER__ 1

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

BddEnc_ptr
BddEnc_create(SymbTable_ptr symb_table,
              BoolEnc_ptr bool_enc, VarsHandler_ptr dd_vars_hndr,
              OrdGroups_ptr ord_groups);

VIRTUAL
void BddEnc_destroy(BddEnc_ptr self);

VarsHandler_ptr
BddEnc_get_dd_vars_handler(const BddEnc_ptr self);

DDMgr_ptr BddEnc_get_dd_manager(const BddEnc_ptr self);

OrdGroups_ptr BddEnc_get_ord_groups(const BddEnc_ptr self);

add_ptr
BddEnc_expr_to_add(BddEnc_ptr self, const Expr_ptr expr,
                   const node_ptr context);

AddArray_ptr
BddEnc_expr_to_addarray(BddEnc_ptr self, const Expr_ptr expr,
                        const node_ptr context);

bdd_ptr
BddEnc_expr_to_bdd(BddEnc_ptr self, const Expr_ptr expr,
                   const node_ptr context);

node_ptr
BddEnc_add_to_expr(BddEnc_ptr self, const add_ptr add,
                   SymbLayer_ptr det_layer);

node_ptr
BddEnc_add_to_scalar_expr(BddEnc_ptr self, const add_ptr add,
                          SymbLayer_ptr det_layer);

node_ptr
BddEnc_bdd_to_expr(BddEnc_ptr self, const bdd_ptr bdd);

BddVarSet_ptr
BddEnc_get_state_vars_cube(const BddEnc_ptr self);

BddVarSet_ptr
BddEnc_get_next_state_vars_cube(const BddEnc_ptr self);

BddVarSet_ptr
BddEnc_get_frozen_vars_cube(const BddEnc_ptr self);

BddVarSet_ptr
BddEnc_get_state_frozen_vars_cube(const BddEnc_ptr self);

BddVarSet_ptr
BddEnc_get_state_next_state_frozen_vars_cube(const BddEnc_ptr self);

BddVarSet_ptr
BddEnc_get_input_vars_cube(const BddEnc_ptr self);

BddVarSet_ptr
BddEnc_get_layer_vars_cube(const BddEnc_ptr self,
                           SymbLayer_ptr layer,
                           SymbFilterType vt);

boolean
BddEnc_is_var_in_cube(const BddEnc_ptr self,
                      node_ptr name, add_ptr cube);

add_ptr
BddEnc_state_var_to_next_state_var_add(const BddEnc_ptr self,
                                       add_ptr add);

add_ptr
BddEnc_next_state_var_to_state_var_add(const BddEnc_ptr self,
                                       add_ptr add);

bdd_ptr
BddEnc_state_var_to_next_state_var(const BddEnc_ptr self, bdd_ptr bdd);

bdd_ptr
BddEnc_next_state_var_to_state_var(const BddEnc_ptr self, bdd_ptr bdd);

void
BddEnc_print_bdd_begin(BddEnc_ptr self, NodeList_ptr symbols,
                       boolean changes_only);

void
BddEnc_print_bdd_end(BddEnc_ptr self);

int
BddEnc_print_bdd(BddEnc_ptr self,
                 bdd_ptr bdd,
                 VPFBEFNNV p_fun,
                 OStream_ptr file,
                 void* arg);

void
BddEnc_print_set_of_states(BddEnc_ptr self,
                           bdd_ptr states,
                           boolean changes_only,
                           boolean print_defines,
                           VPFBEFNNV p_fun,
                           OStream_ptr file,
                           void* arg);

void
BddEnc_print_set_of_inputs(BddEnc_ptr self,
                           bdd_ptr inputs,
                           boolean changes_only,
                           VPFBEFNNV p_fun,
                           OStream_ptr file,
                           void* arg);

void
BddEnc_print_set_of_state_input_pairs(BddEnc_ptr self,
                                      bdd_ptr state_input_pairs,
                                      boolean changes_only,
                                      VPFBEFNNV p_fun,
                                      OStream_ptr file,
                                      void* arg);

void
BddEnc_print_set_of_trans_models(BddEnc_ptr self,
                                 bdd_ptr state_input_pairs,
                                 /* boolean changes_only, */
                                 OStream_ptr file);

node_ptr
BddEnc_assign_symbols(BddEnc_ptr self, bdd_ptr bdd,
                      NodeList_ptr symbols,
                      boolean onlyRequiredSymbs,
                      bdd_ptr* resultBdd);

void
BddEnc_print_vars_in_cube(BddEnc_ptr self, bdd_ptr cube,
                          node_ptr list_of_sym,
                          OStream_ptr file);

NodeList_ptr BddEnc_get_vars_in_cube(const BddEnc_ptr self,
                                     bdd_ptr cube,
                                     node_ptr list_of_sym,
                                     boolean include_next);

NodeList_ptr BddEnc_get_var_ordering(const BddEnc_ptr self,
                                     const VarOrderingType ord_type);

int
BddEnc_write_var_ordering(const BddEnc_ptr self,
                          const char* oo_filename,
                          const VarOrderingType dump_type);

int BddEnc_get_reordering_count(const BddEnc_ptr self);

void BddEnc_reset_reordering_count(BddEnc_ptr self);

double
BddEnc_count_states_of_add(const BddEnc_ptr self, add_ptr add);

double
BddEnc_count_states_of_bdd(const BddEnc_ptr self, bdd_ptr bdd);

double
BddEnc_count_inputs_of_bdd(const BddEnc_ptr self, bdd_ptr bdd);

double
BddEnc_count_states_inputs_of_bdd(const BddEnc_ptr self, bdd_ptr bdd);

double
BddEnc_get_minterms_of_add(const BddEnc_ptr self, add_ptr add);

double
BddEnc_get_minterms_of_bdd(const BddEnc_ptr self, bdd_ptr bdd);

bdd_ptr
BddEnc_pick_one_state(const BddEnc_ptr self, bdd_ptr states);

bdd_ptr
BddEnc_pick_one_input(const BddEnc_ptr self, bdd_ptr inputs);

bdd_ptr
BddEnc_pick_one_input_state(const BddEnc_ptr self,
                            bdd_ptr inputs_states);

boolean
BddEnc_pick_all_terms_states_inputs(const BddEnc_ptr self,
                                    bdd_ptr bdd,
                                    bdd_ptr* result_array,
                                    const int array_len);

boolean
BddEnc_pick_all_terms_states(const BddEnc_ptr self, bdd_ptr bdd,
                             bdd_ptr* result_array,
                             const int array_len);

boolean
BddEnc_pick_all_terms_inputs(const BddEnc_ptr self, bdd_ptr bdd,
                             bdd_ptr* result_array,
                             const int array_len);

bdd_ptr
BddEnc_pick_one_state_rand(const BddEnc_ptr self, bdd_ptr states);

bdd_ptr
BddEnc_pick_one_input_rand(const BddEnc_ptr self, bdd_ptr inputs);

bdd_ptr
BddEnc_pick_one_input_state_rand(const BddEnc_ptr self,
                                 bdd_ptr inputs_states);

node_ptr
BddEnc_get_var_name_from_index(const BddEnc_ptr self, int index);

boolean
BddEnc_has_var_at_index(const BddEnc_ptr self, int index);

int
BddEnc_get_var_index_from_name(const BddEnc_ptr self, node_ptr name);

add_ptr
BddEnc_constant_to_add(const BddEnc_ptr self, node_ptr constant);

add_ptr
BddEnc_eval_sign_add(BddEnc_ptr self, add_ptr a, int flag);

bdd_ptr
BddEnc_eval_sign_bdd(BddEnc_ptr self, bdd_ptr a, int flag);

int
BddEnc_eval_num(BddEnc_ptr self, node_ptr e, node_ptr context);

add_ptr
BddEnc_eval_constant(BddEnc_ptr self, Expr_ptr expr, node_ptr context);

AddArray_ptr
BddEnc_get_symbol_add(BddEnc_ptr self, node_ptr name);

add_ptr
BddEnc_get_state_frozen_vars_mask_add(BddEnc_ptr self);

add_ptr
BddEnc_get_input_vars_mask_add(BddEnc_ptr self);

add_ptr
BddEnc_get_state_frozen_input_vars_mask_add(BddEnc_ptr self);

bdd_ptr
BddEnc_get_state_frozen_vars_mask_bdd(BddEnc_ptr self);

bdd_ptr
BddEnc_get_input_vars_mask_bdd(BddEnc_ptr self);

bdd_ptr
BddEnc_get_state_frozen_input_vars_mask_bdd(BddEnc_ptr self);

add_ptr
BddEnc_apply_state_frozen_vars_mask_add(BddEnc_ptr self, add_ptr states);

add_ptr
BddEnc_apply_input_vars_mask_add(BddEnc_ptr self, add_ptr inputs);

add_ptr
BddEnc_apply_state_frozen_input_vars_mask_add(BddEnc_ptr self,
                                              add_ptr states_inputs);

BddStates
BddEnc_apply_state_frozen_vars_mask_bdd(BddEnc_ptr self,
                                        BddStates states);

BddInputs
BddEnc_apply_input_vars_mask_bdd(BddEnc_ptr self, BddInputs inputs);

BddStatesInputs
BddEnc_apply_state_frozen_input_vars_mask_bdd(BddEnc_ptr self,
                                           BddStatesInputs states_inputs);

add_ptr
BddEnc_get_var_mask(BddEnc_ptr self, node_ptr var_name);

array_t*
BddEnc_ComputePrimeImplicants(BddEnc_ptr self,
                              const array_t* layer_names,
                              bdd_ptr formula);

void
BddEnc_force_order(BddEnc_ptr self, OrdGroups_ptr new_po_grps);

void
BddEnc_force_order_from_file(BddEnc_ptr self, FILE* orderfile);

void
BddEnc_print_bdd_wff(BddEnc_ptr self, bdd_ptr bdd, NodeList_ptr vars,
                     boolean do_sharing, boolean do_indent,
                     int start_at_column, OStream_ptr out);

void
BddEnc_print_formula_info(BddEnc_ptr self, Expr_ptr formula,
                          boolean print_models, boolean print_formula,
                          OStream_ptr out);

node_ptr
BddEnc_bdd_to_wff(BddEnc_ptr self, bdd_ptr bdd, NodeList_ptr vars);

void
BddEnc_clean_evaluation_cache(BddEnc_ptr self);

BddVarSet_ptr BddEnc_get_vars_cube(const BddEnc_ptr self,
                                          Set_t vars,
                                          SymbFilterType vt);

BddVarSet_ptr
BddEnc_get_unfiltered_vars_cube(const BddEnc_ptr self, Set_t vars);

int BddEnc_dump_addarray_dot(BddEnc_ptr self,
                                    AddArray_ptr addarray,
                                    const char** labels,
                                    FILE* outfile);

int BddEnc_dump_addarray_davinci(BddEnc_ptr self,
                                        AddArray_ptr addarray,
                                        const char** labels,
                                        FILE* outfile);

/* Functions directly called by commands */

void
BddEnc_print_formula(const NuSMVEnv_ptr env, node_ptr constr,
                     const boolean verbose, const boolean formula);

int
BddEnc_dump_expr(const BddEnc_ptr self, const node_ptr parsed_expr,
                 const char* str_constr, const t_format format,
                 FILE* outfile);

#endif /* __NUSMV_CORE_ENC_BDD_BDD_ENC_H__ */

---