NuSMV/code/nusmv/core/dd/dd.h

Go to the documentation of this file.

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


  This file is part of the ``dd'' package of NuSMV version 2. 
  Copyright (C) 1998-2001 by CMU and 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_DD_DD_H__
#define __NUSMV_CORE_DD_DD_H__

#include "nusmv/core/dd/DDMgr.h"
#include "nusmv/core/utils/utils.h"
#include "nusmv/core/utils/array.h"
#include "nusmv/core/utils/avl.h"
#include "nusmv/core/node/node.h"
#include "cudd/cudd.h"
#include "nusmv/core/opt/OptsHandler.h"
#include "nusmv/core/cinit/NuSMVEnv.h"

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

typedef struct DdNode * add_ptr;
typedef struct DdNode * bdd_ptr;
typedef struct DdNode * dd_ptr; /* represents both add_ptr and bdd_ptr */

typedef struct MtrNode dd_block;

typedef Cudd_ReorderingType dd_reorderingtype;

typedef void (*VPFDD)(DDMgr_ptr , bdd_ptr);

typedef node_ptr (*NPFDD)(DDMgr_ptr , bdd_ptr);
typedef void (*VPFCVT)(CUDD_VALUE_TYPE);
typedef void (*VPFDDCVT)(DDMgr_ptr, CUDD_VALUE_TYPE);
typedef node_ptr (*NPFCVT)(CUDD_VALUE_TYPE);

typedef add_ptr (*FP_A_DA)(DDMgr_ptr , add_ptr);
typedef add_ptr (*FP_A_DAA)(DDMgr_ptr , add_ptr, add_ptr);

typedef node_ptr (*NPFNNE)(node_ptr, node_ptr, const NuSMVEnv_ptr);

typedef DdGen dd_gen;

typedef enum DdDynVarOrderAction_TAG {
  DD_DYN_VAR_ORDER_ACTION_DISABLE = 1,
  DD_DYN_VAR_ORDER_ACTION_ENABLE,
  DD_DYN_VAR_ORDER_ACTION_FORCE
} DdDynVarOrderAction;

DdDynVarOrderAction Dd_action_str_to_enum(char* action);
char* Dd_action_enum_to_str(DdDynVarOrderAction action);

/*---------------------------------------------------------------------------*/
/* Macro declarations                                                        */
/*---------------------------------------------------------------------------*/
#ifndef MAX_VAR_INDEX

#define MAX_VAR_INDEX            CUDD_MAXINDEX
#endif

/* initial size of the unique tables */

#define UNIQUE_SLOTS             CUDD_UNIQUE_SLOTS

/* initial size of the cache */

#define CACHE_SLOTS              CUDD_CACHE_SLOTS

/* use value currently stored in the manager. */

#define REORDER_SAME             CUDD_REORDER_SAME
/* no reardering at all */

#define REORDER_NONE             CUDD_REORDER_NONE

#define REORDER_RANDOM           CUDD_REORDER_RANDOM

#define REORDER_RANDOM_PIVOT     CUDD_REORDER_RANDOM_PIVOT

#define REORDER_SIFT             CUDD_REORDER_SIFT

#define REORDER_SIFT_CONV        CUDD_REORDER_SIFT_CONVERGE

#define REORDER_SYMM_SIFT        CUDD_REORDER_SYMM_SIFT

#define REORDER_SYMM_SIFT_CONV   CUDD_REORDER_SYMM_SIFT_CONV

#define REORDER_WINDOW2          CUDD_REORDER_WINDOW2

#define REORDER_WINDOW3          CUDD_REORDER_WINDOW3

#define REORDER_WINDOW4          CUDD_REORDER_WINDOW4

#define REORDER_WINDOW2_CONV     CUDD_REORDER_WINDOW2_CONV

#define REORDER_WINDOW3_CONV     CUDD_REORDER_WINDOW3_CONV

#define REORDER_WINDOW4_CONV     CUDD_REORDER_WINDOW4_CONV

#define REORDER_GROUP_SIFT       CUDD_REORDER_GROUP_SIFT

#define REORDER_GROUP_SIFT_CONV  CUDD_REORDER_GROUP_SIFT_CONV

#define REORDER_ANNEALING        CUDD_REORDER_ANNEALING

#define REORDER_GENETIC          CUDD_REORDER_GENETIC

#define REORDER_LINEAR           CUDD_REORDER_LINEAR

#define REORDER_LINEAR_CONV      CUDD_REORDER_LINEAR_CONVERGE

#define REORDER_EXACT            CUDD_REORDER_EXACT

#define DEFAULT_REORDER          REORDER_SIFT /* The default value in the CUDD package */

#define DEFAULT_MINSIZE          10 /* 10 = whatever (Verbatim from file cuddTable.c) */

#define ADD_FOREACH_NODE(manager, f, gen, node) \
  Cudd_ForeachNode(DDMgr_get_dd_manager(manager), f, gen, node)

#define BDD_FOREACH_NODE(manager, f, gen, node) \
  ADD_FOREACH_NODE(manager, f, gen, node)

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

void Dd_init(NuSMVEnv_ptr env);

void Dd_quit(NuSMVEnv_ptr env);

int Dd_dynamic_var_ordering(NuSMVEnv_ptr env,
                                   DDMgr_ptr dd,
                                   int dynOrderingMethod,
                                   DdDynVarOrderAction action);

int Dd_set_bdd_parameters(NuSMVEnv_ptr env,
                                 DDMgr_ptr dd_manager,
                                 boolean showAfter);

node_ptr map_dd(DDMgr_ptr , NPFDD, node_ptr);

void     walk_dd(DDMgr_ptr , VPFDD, node_ptr);

dd_block* dd_new_var_block(DDMgr_ptr , int, int);

int      dd_free_var_block(DDMgr_ptr , dd_block*);

int      dd_get_index_at_level(DDMgr_ptr , int);

int      dd_get_level_at_index(DDMgr_ptr , int);

int      dd_get_size(DDMgr_ptr );

int      dd_set_order(DDMgr_ptr , int *permutation);

void     dd_autodyn_enable(DDMgr_ptr , dd_reorderingtype);

void     dd_autodyn_disable(DDMgr_ptr );

int      dd_reordering_status(DDMgr_ptr , dd_reorderingtype *);

int      dd_reorder(DDMgr_ptr , int, int);

int      dd_get_reorderings(DDMgr_ptr );

dd_reorderingtype dd_get_ordering_method(DDMgr_ptr );

int      StringConvertToDynOrderType(char *string);

char *   DynOrderTypeConvertToString(int method);

int      dd_checkzeroref(DDMgr_ptr );

int      dd_set_parameters(DDMgr_ptr , OptsHandler_ptr, FILE *);

int      dd_print_stats(NuSMVEnv_ptr, DDMgr_ptr , FILE *);

int      dd_printminterm(DDMgr_ptr , dd_ptr);

int      dd_dump_dot(DDMgr_ptr , int, dd_ptr *, const char **, const char **, FILE *);

int      dd_dump_davinci(DDMgr_ptr , int, dd_ptr *, const char **, const char **, FILE *);

bdd_ptr  add_to_bdd(DDMgr_ptr , add_ptr);

bdd_ptr  add_to_bdd_strict_threshold(DDMgr_ptr , add_ptr, int);

add_ptr  bdd_to_add(DDMgr_ptr , bdd_ptr);

add_ptr  bdd_to_01_add(DDMgr_ptr , bdd_ptr);

add_ptr  add_exist_abstract(DDMgr_ptr dd, add_ptr a, bdd_ptr b);


/* ADD Interface **************************************************************/

add_ptr  add_true(DDMgr_ptr );

add_ptr  add_then(DDMgr_ptr , add_ptr);

add_ptr  add_else(DDMgr_ptr , add_ptr);

int      add_index(DDMgr_ptr , add_ptr);

add_ptr  add_false(DDMgr_ptr );

int      add_is_true(DDMgr_ptr , add_ptr);

int      add_is_false(DDMgr_ptr , add_ptr);

add_ptr  add_one(DDMgr_ptr );

add_ptr  add_zero(DDMgr_ptr );

int      add_is_one(DDMgr_ptr , add_ptr);

int      add_is_zero(DDMgr_ptr , add_ptr);

void     add_ref(add_ptr);

void     add_deref(add_ptr);

add_ptr  add_dup(add_ptr);

void     add_free(DDMgr_ptr , add_ptr);

add_ptr  add_new_var_with_index(DDMgr_ptr , int);

add_ptr  add_build(DDMgr_ptr , int, add_ptr , add_ptr);

add_ptr  add_new_var_at_level(DDMgr_ptr , int);

int      add_isleaf(add_ptr);

add_ptr  add_leaf(DDMgr_ptr , node_ptr);

node_ptr add_get_leaf(DDMgr_ptr , add_ptr);

add_ptr  add_and(DDMgr_ptr , add_ptr, add_ptr);

void     add_and_accumulate(DDMgr_ptr , add_ptr *, add_ptr);

add_ptr  add_or(DDMgr_ptr , add_ptr, add_ptr);

void     add_or_accumulate(DDMgr_ptr , add_ptr *, add_ptr);

add_ptr  add_not(DDMgr_ptr , add_ptr);

add_ptr  add_implies(DDMgr_ptr , add_ptr, add_ptr);

add_ptr  add_iff(DDMgr_ptr , add_ptr, add_ptr);

add_ptr  add_xor(DDMgr_ptr , add_ptr, add_ptr);

add_ptr  add_xnor(DDMgr_ptr , add_ptr, add_ptr);

add_ptr  add_apply(DDMgr_ptr , NPFNNE, add_ptr, add_ptr);

add_ptr  add_monadic_apply(DDMgr_ptr , NPFNNE/*NPFCVT*/, add_ptr);

add_ptr  add_ifthenelse(DDMgr_ptr , add_ptr, add_ptr, add_ptr);

add_ptr  add_cube_diff(DDMgr_ptr , add_ptr , add_ptr);

add_ptr  add_simplify_assuming(DDMgr_ptr , add_ptr, add_ptr);

add_ptr  add_permute(DDMgr_ptr , add_ptr, int *);

add_ptr  add_support(DDMgr_ptr , add_ptr);

void     add_walkleaves(DDMgr_ptr , VPFDDCVT, add_ptr);

int      add_size(DDMgr_ptr , add_ptr);

double   add_count_minterm(DDMgr_ptr , add_ptr, int);

int      get_dd_nodes_allocated(DDMgr_ptr );

node_ptr add_value(DDMgr_ptr , add_ptr);

add_ptr  add_if_then(DDMgr_ptr , add_ptr, add_ptr);


/* BDD Interface **************************************************************/

int      bdd_isleaf(bdd_ptr);

void     bdd_ref(bdd_ptr);

void     bdd_deref(bdd_ptr);

bdd_ptr  bdd_dup(bdd_ptr);

bdd_ptr  bdd_true(DDMgr_ptr );

bdd_ptr  bdd_false(DDMgr_ptr );

int      bdd_is_true(DDMgr_ptr , bdd_ptr);

int      bdd_is_false(DDMgr_ptr , bdd_ptr);

int      bdd_isnot_true(DDMgr_ptr , bdd_ptr);

int      bdd_isnot_false(DDMgr_ptr , bdd_ptr);

void     bdd_free(DDMgr_ptr , bdd_ptr);

bdd_ptr  bdd_not(DDMgr_ptr , bdd_ptr);

bdd_ptr  bdd_and(DDMgr_ptr , bdd_ptr, bdd_ptr);

void     bdd_and_accumulate(DDMgr_ptr , bdd_ptr *, bdd_ptr);

bdd_ptr  bdd_or(DDMgr_ptr , bdd_ptr, bdd_ptr);

void     bdd_or_accumulate(DDMgr_ptr , bdd_ptr *, bdd_ptr);

bdd_ptr  bdd_xor(DDMgr_ptr , bdd_ptr, bdd_ptr);

bdd_ptr  bdd_iff(DDMgr_ptr , bdd_ptr, bdd_ptr);

bdd_ptr  bdd_imply(DDMgr_ptr , bdd_ptr, bdd_ptr);

bdd_ptr  bdd_forsome(DDMgr_ptr , bdd_ptr, bdd_ptr);

bdd_ptr  bdd_forall(DDMgr_ptr , bdd_ptr, bdd_ptr);

bdd_ptr  bdd_permute(DDMgr_ptr , bdd_ptr, int *);

bdd_ptr  bdd_and_abstract(DDMgr_ptr , bdd_ptr, bdd_ptr, bdd_ptr);

bdd_ptr  bdd_simplify_assuming(DDMgr_ptr , bdd_ptr, bdd_ptr);

bdd_ptr  bdd_minimize(DDMgr_ptr , bdd_ptr, bdd_ptr);

bdd_ptr  bdd_cofactor(DDMgr_ptr , bdd_ptr, bdd_ptr);

bdd_ptr  bdd_between(DDMgr_ptr , bdd_ptr, bdd_ptr);

int      bdd_entailed(DDMgr_ptr dd, bdd_ptr f, bdd_ptr g);

int      bdd_intersected(DDMgr_ptr dd, bdd_ptr f, bdd_ptr g);

bdd_ptr  bdd_then(DDMgr_ptr , bdd_ptr);

bdd_ptr  bdd_else(DDMgr_ptr , bdd_ptr);

bdd_ptr  bdd_ite(DDMgr_ptr , bdd_ptr, bdd_ptr, bdd_ptr);

int      bdd_iscomplement(DDMgr_ptr , bdd_ptr);

int      bdd_readperm(DDMgr_ptr , bdd_ptr);

int      bdd_index(DDMgr_ptr , bdd_ptr);

bdd_ptr  bdd_pick_one_minterm(DDMgr_ptr , bdd_ptr, bdd_ptr *, int);

bdd_ptr  bdd_pick_one_minterm_rand(DDMgr_ptr , bdd_ptr, bdd_ptr *, int);

int      bdd_pick_all_terms(DDMgr_ptr , bdd_ptr,  bdd_ptr *, int, bdd_ptr *, int);

bdd_ptr  bdd_support(DDMgr_ptr , bdd_ptr);

int      bdd_size(DDMgr_ptr , bdd_ptr);

double   bdd_count_minterm(DDMgr_ptr , bdd_ptr, int);

bdd_ptr  bdd_new_var_with_index(DDMgr_ptr , int);

bdd_ptr bdd_get_one_sparse_sat(DDMgr_ptr , bdd_ptr);

bdd_ptr  bdd_cube_diff(DDMgr_ptr , bdd_ptr, bdd_ptr);

bdd_ptr  bdd_cube_union(DDMgr_ptr , bdd_ptr, bdd_ptr);

bdd_ptr  bdd_cube_intersection(DDMgr_ptr , bdd_ptr, bdd_ptr);

int      bdd_get_lowest_index(DDMgr_ptr , bdd_ptr);

bdd_ptr  bdd_largest_cube(DDMgr_ptr , bdd_ptr, int *);

bdd_ptr  bdd_compute_prime_low(DDMgr_ptr , bdd_ptr, bdd_ptr);

array_t * bdd_compute_primes_low(DDMgr_ptr , bdd_ptr, bdd_ptr);

array_t * bdd_compute_primes(DDMgr_ptr dd, bdd_ptr b);

bdd_ptr  bdd_make_prime(DDMgr_ptr dd, bdd_ptr cube, bdd_ptr b);

bdd_ptr  bdd_compute_essentials(DDMgr_ptr dd, bdd_ptr b);

int      bdd_DumpBlif(DDMgr_ptr dd, int n, bdd_ptr *f, char **inames, char **onames, char *mname, FILE *fp);

int      bdd_DumpBlifBody(DDMgr_ptr dd, int n, bdd_ptr *f, char **inames, char **onames, FILE *fp);

int      bdd_leq(DDMgr_ptr dd, bdd_ptr f, bdd_ptr g);

bdd_ptr  bdd_swap_variables(DDMgr_ptr dd, bdd_ptr f, bdd_ptr *x_varlist, bdd_ptr *y_varlist, int n);

bdd_ptr  bdd_compose(DDMgr_ptr dd, bdd_ptr f, bdd_ptr g, int v);

int      bdd_ref_count(DDMgr_ptr dd, bdd_ptr n);

int      calculate_bdd_value(DDMgr_ptr mgr, bdd_ptr f, int* values);



#endif /* __NUSMV_CORE_DD_DD_H__ */

---