NuSMV/code/nusmv/core/wff/wffRewrite.h

Go to the documentation of this file.

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


  This file is part of the ``wff'' package.
  %COPYRIGHT%


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

#ifndef __NUSMV_CORE_WFF_WFF_REWRITE_H__
#define __NUSMV_CORE_WFF_WFF_REWRITE_H__

#include "nusmv/core/utils/defs.h"
#include "nusmv/core/utils/Pair.h"
#include "nusmv/core/compile/FlatHierarchy.h"

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


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

enum WffRewriteFormulaKind_TAG {
  WFF_REWRITE_FORMULA_KIND_FIRST = 0,
  WFF_REWRITE_FORMULA_KIND_STATE = 1, /* non-temporal and without input vars or
                                      next operator */
  WFF_REWRITE_FORMULA_KIND_INPUT = 1 << 1, /* non-temporal but with input vars */
  WFF_REWRITE_FORMULA_KIND_NEXT = 1 << 2, /* non-temporal but with next operator */
  WFF_REWRITE_FORMULA_KIND_INPUT_NEXT =
  WFF_REWRITE_FORMULA_KIND_INPUT |
  WFF_REWRITE_FORMULA_KIND_NEXT, /* non-temporal but with input vars
                                           and next operator */
  WFF_REWRITE_FORMULA_KIND_TEMP = 1 << 3, /* temporal (it must be without input vars or
                                              next operator) */
  WFF_REWRITE_FORMULA_KIND_LAST = 1 << 4
};
typedef enum WffRewriteFormulaKind_TAG WffRewriteFormulaKind;

typedef enum {
  WFF_REWRITE_METHOD_STANDARD,
  WFF_REWRITE_METHOD_DEADLOCK_FREE,
} WffRewriteMethod;


typedef enum {
  WFF_REWRITER_REWRITE_INPUT_NEXT,
  WFF_REWRITER_LTL_2_INVAR
} WffRewriterExpectedProperty;

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


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


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


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

Pair_ptr Wff_Rewrite_rewrite_formula(NuSMVEnv_ptr const env,
                                            const WffRewriteMethod method,
                                            const WffRewriterExpectedProperty eproptype,
                                            SymbLayer_ptr layer,
                                            FlatHierarchy_ptr outfh,
                                            node_ptr const spec,
                                            const short int spec_type);

Pair_ptr Wff_Rewrite_rewrite_formula_generic(NuSMVEnv_ptr const env,
                                             const WffRewriteMethod method,
                                             const WffRewriterExpectedProperty eproptype,
                                             SymbLayer_ptr layer,
                                             FlatHierarchy_ptr outfh,
                                             node_ptr const spec,
                                             const short int spec_type,
                                             const boolean initialize_monitor_to_true,
                                             const boolean ltl2invar_negate_property);

boolean Wff_Rewrite_is_rewriting_needed(SymbTable_ptr st, node_ptr wff,
                                               node_ptr context);


#endif /* __NUSMV_CORE_WFF_WFF_REWRITE_H__ */

---