Expr.c
Abstraction for expression type impemented as node_ptr
SexpFsm.c
The SexpFsm implementation

Expr.c

Abstraction for expression type impemented as node_ptr

By: Roberto Cavada


SexpFsm.c

The SexpFsm implementation

By: Roberto Cavada

See AlsoSexpFsm.h

SexpFsm_create()
Costructor for a scalar and boolean sexp fsm. If det_layer is null, then a scalar fsm will be created, otherwise a boolean fsm will be created. When the sexp fsm is not booleanizable, det_layer *must* be NULL and BddEnc *can* be NULL. inl_layer is a layer used for inlining (syntactic simplification) of the FSM (can be NULL for no-simplification)
SexpFsm_copy()
Copy costructor
SexpFsm_create_predicate_normalised_copy()
Copy the Sexp FSM and perform predicate-normalisation on all the expressions.
SexpFsm_destroy()
Destructor
SexpFsm_get_bool_enc()
Returns the BoolEnc instance connected to self
SexpFsm_get_symb_table()
Returns the symbol table that is connected to the BoolEnc instance connected to self
SexpFsm_scalar_to_boolean()
Construct a boolean fsm from a scalar one
SexpFsm_is_boolean()
Returns true if self if a booleanized fsm, false if it is scalar
SexpFsm_get_hierarchy()
Returns a copy of the complete hierarchy
SexpFsm_get_init()
Returns an Expr that collects init states for all variables handled by self
SexpFsm_get_invar()
Returns an Expr that collects invar states for all variables handled by self
SexpFsm_get_trans()
Returns an Expr that collects all next states for all variables handled by self
SexpFsm_get_input()
Returns an Expr that collects all input states for all variables handled by self
SexpFsm_get_var_init()
Gets the sexp expression defining the initial state for the variable "v".
SexpFsm_get_var_invar()
Gets the sexp expression defining the state constraints for the variable "v".
SexpFsm_get_var_trans()
Gets the sexp expression defining the transition relation for the variable "v".
SexpFsm_get_var_input()
Gets the sexp expression defining the input relation for the variable "v".
SexpFsm_get_justice()
Gets the list of sexp expressions defining the set of justice constraints for this machine.
SexpFsm_get_compassion()
Gets the list of sexp expressions defining the set of compassion constraints for this machine.
SexpFsm_get_vars_list()
Returns the list of variables in the FSM
sexp_fsm_create_vars_dag()
sexp_fsm_init()
Initializes either the boolean or scalar sexp fsm
__free_nodelist()
private service used as callback by sexp_fsm_destroy_vars_dag
sexp_fsm_destroy_vars_dag()
Destroyer for the vars dag, used by inlining
sexp_fsm_deinit()
Initializes the vars fsm hash
sexp_fsm_copy()
Copies members from self to copy
sexp_fsm_hash_var_fsm_init()
Initializes the vars fsm hash
sexp_fsm_simplify_expr()
removes duplicates from expression containing AND nodes
sexp_fsm_booleanize_expr()
Booleanizes the given expression, keeping each top level part of a possible conjuction
_subst_expr()
Substitutes all expressions of subst keys c inside expr by the cooresponding value into subst, ignoring left side of EQDEF
__add_vertex_aux()
Private service of sexp_fsm_add_vertex
sexp_fsm_add_vertex()
sexp_fsm_dag_get_roots()
returns the roots in the graph. Returned list must be destroyed
sexp_fsm_remove_dep_dag_node()
Removes the given node from deps dag
sexp_fsm_add_vertices_from_expr()
private service of create_vars_dag
__search_eqdef()
returns an EQDEF node assigning name, searching into expr. expr can be either a conjunction or a EQDEF node
sexp_fsm_dag_get_subst_hash()
returns an hash table for variable inlining substitution. The hash is created by using a scheduling.
sexp_fsm_apply_inlining()
Called during initialization to perform inlining.
simplifier_hash_create()
This is used when creating cluster list from vars list
simplifier_hash_destroy()
Call after sexp_fsm_cluster_hash_create
simplifier_hash_add_expr()
To insert a new node in the hash
simplifier_hash_query_expr()
Queries for an element in the hash, returns True if found
sexp_fsm_hash_var_fsm_destroy()
Call to destroy the var fsm hash
sexp_fsm_callback_var_fsm_free()
Private callback that destroys a single variable fsm contained into the var fsm hash
sexp_fsm_hash_var_fsm_lookup_var()
Given a variable name, returns the corresponding variable fsm, or NULL if not found
sexp_fsm_hash_var_fsm_insert_var()
Adds a var fsm to the internal hash. Private.
var_fsm_create()
Creates a var fsm
var_fsm_destroy()
It does not destroy the init, trans and invar nodes. It destroys only the support nodes
var_fsm_get_init()
var_fsm_get_invar()
var_fsm_get_next()
var_fsm_get_input()

Last updated on 2009/01/30 14h:53