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

Go to the documentation of this file.

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


  This file is part of the ``enc.bdd'' package of NuSMV version 2.
  Copyright (C) 2003 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_CACHE_H__
#define __NUSMV_CORE_ENC_BDD_BDD_ENC_CACHE_H__

#include "nusmv/core/compile/symb_table/SymbTable.h"
#include "nusmv/core/dd/dd.h"

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

typedef struct BddEncCache_TAG*  BddEncCache_ptr;

#define BDD_ENC_CACHE(x) \
          ((BddEncCache_ptr) x)

#define BDD_ENC_CACHE_CHECK_INSTANCE(x) \
          ( nusmv_assert(BDD_ENC_CACHE(x) != BDD_ENC_CACHE(NULL)) )


/* ---------------------------------------------------------------------- */
/* Types                                                                  */
/* ---------------------------------------------------------------------- */

/* ---------------------------------------------------------------------- */
/* Public methods                                                         */
/* ---------------------------------------------------------------------- */

BddEncCache_ptr
BddEncCache_create(SymbTable_ptr symb_table, DDMgr_ptr dd);

void BddEncCache_destroy(BddEncCache_ptr self);

void
BddEncCache_new_constant(BddEncCache_ptr self, node_ptr constant,
                         add_ptr constant_add);

void
BddEncCache_remove_constant(BddEncCache_ptr self, node_ptr constant);

boolean
BddEncCache_is_constant_encoded(const BddEncCache_ptr self,
                                node_ptr constant);

add_ptr
BddEncCache_lookup_constant(const BddEncCache_ptr self,
                            node_ptr constant);

void
BddEncCache_new_boolean_var(BddEncCache_ptr self, node_ptr var_name,
                            add_ptr var_add);

void
BddEncCache_remove_boolean_var(BddEncCache_ptr self, node_ptr var_name);

boolean
BddEncCache_is_boolean_var_encoded(const BddEncCache_ptr self,
                                   node_ptr var_name);

add_ptr
BddEncCache_lookup_boolean_var(const BddEncCache_ptr self, node_ptr var_name);

void BddEncCache_set_evaluation(BddEncCache_ptr self,
                                       node_ptr expr,
                                       AddArray_ptr add_array);

void BddEncCache_remove_evaluation(BddEncCache_ptr self,
                                          node_ptr expr);

AddArray_ptr BddEncCache_get_evaluation(BddEncCache_ptr self,
                                               node_ptr expr);

void BddEncCache_clean_evaluation_about(BddEncCache_ptr self,
                                               NodeList_ptr symbs);

void BddEncCache_clean_evaluation(BddEncCache_ptr self);

#endif /* __NUSMV_CORE_ENC_BDD_BDD_ENC_CACHE_H__ */

---