NuSMV/code/nusmv/core/wff/ExprMgr.h File Reference

#include "nusmv/core/utils/utils.h"
#include "nusmv/core/cinit/NuSMVEnv.h"
#include "nusmv/core/node/node.h"
#include "nusmv/core/compile/symb_table/SymbTable.h"

Go to the source code of this file.

Defines
#define	EXPR(x)   ((Expr_ptr) x)
#define	EXPR_CHECK_INSTANCE(x)   (nusmv_assert(EXPR(x) != EXPR(NULL)))
#define	Expr_get_type(t)   node_get_type(t)
#define	EXPR_MGR(self)   ((ExprMgr_ptr) self)
	To cast and check instances of class ExprMgr.
#define	EXPR_MGR_CHECK_INSTANCE(self)   (nusmv_assert(EXPR_MGR(self) != EXPR_MGR(NULL)))
#define	EXPR_TIME_OFS   10
#define	EXPR_UNTIMED_CURRENT   -2
	Public interface of class 'ExprMgr'.
#define	EXPR_UNTIMED_DONTCARE   -3
#define	EXPR_UNTIMED_NEXT   -1
Typedefs
typedef node_ptr	Expr_ptr
	The Expr type.
typedef struct ExprMgr_TAG *	ExprMgr_ptr
Enumerations
enum	ExprKind { EXPR_SIMPLE, EXPR_NEXT, EXPR_LTL, EXPR_CTL }
	The type of an expression. More...
Functions
boolean	ExprMgr_is_syntax_correct (Expr_ptr exp, ExprKind expectedKind)
	Check if "exp" belongs to the "expectedKind".

---

Define Documentation

#define EXPR

(

x

)

((Expr_ptr) x)

Todo:

Missing synopsis

Todo:

Missing description

#define EXPR_CHECK_INSTANCE

(

x

)

(nusmv_assert(EXPR(x) != EXPR(NULL)))

Todo:

Missing synopsis

Todo:

Missing description

#define Expr_get_type

(

t

)

node_get_type(t)

Todo:

Missing synopsis

Todo:

Missing description

#define EXPR_MGR

(

self

)

((ExprMgr_ptr) self)

To cast and check instances of class ExprMgr.

These macros must be used respectively to cast and to check instances of class ExprMgr

#define EXPR_MGR_CHECK_INSTANCE

(

self

)

(nusmv_assert(EXPR_MGR(self) != EXPR_MGR(NULL)))

Todo:

Missing synopsis

Todo:

Missing description

#define EXPR_TIME_OFS   10

Todo:

Missing synopsis

Todo:

Missing description

#define EXPR_UNTIMED_CURRENT   -2

Public interface of class 'ExprMgr'.

Author:

Alessandro Mariotti

Todo:

: Missing description

Todo:

Missing synopsis

Todo:

Missing description

#define EXPR_UNTIMED_DONTCARE   -3

Todo:

Missing synopsis

Todo:

Missing description

#define EXPR_UNTIMED_NEXT   -1

Todo:

Missing synopsis

Todo:

Missing description

---

Typedef Documentation

typedef node_ptr Expr_ptr

The Expr type.

An Expr is any expression represented as a sexpr object

typedef struct ExprMgr_TAG* ExprMgr_ptr

---

Enumeration Type Documentation

enum ExprKind

The type of an expression.

this enum is used to distinguish different kinds of expressions: SIMPLE, NEXT, CTL and LTL

See also:

EXP_KIND in grammar.y; ExprMgr_is_syntax_correct

Enumerator:

EXPR_SIMPLE
EXPR_NEXT
EXPR_LTL
EXPR_CTL

---

Function Documentation

boolean ExprMgr_is_syntax_correct	(	Expr_ptr	exp,
		ExprKind	expectedKind
	)

Check if "exp" belongs to the "expectedKind".

expectedKind can be EXPR_LTL, EXPR_CTL, EXPR_SIMPLE or EXPR_NEXT

See also:

parser.grammar.y:static isCorrectExp