-
SexpFsm_copy()
- Copy costructor
-
SexpFsm_create_predicate_normalised_copy()
- Copy the Sexp FSM and perform predicate-normalisation
on all the expressions.
-
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_destroy()
- Destructor
-
SexpFsm_get_bool_enc()
- Returns the BoolEnc instance connected to self
-
SexpFsm_get_compassion()
- Gets the list of sexp expressions defining the set of
compassion constraints for this machine.
-
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_input()
- Returns an Expr that collects all input 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_justice()
- Gets the list of sexp expressions defining the set of justice
constraints for this machine.
-
SexpFsm_get_symb_table()
- Returns the symbol table that is connected to the
BoolEnc instance connected to self
-
SexpFsm_get_trans()
- Returns an Expr that collects all next 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_input()
- Gets the sexp expression defining the input relation
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_vars_list()
- Returns the list of variables in the FSM
-
SexpFsm_is_boolean()
- Returns true if self if a booleanized fsm, false if
it is scalar
-
SexpFsm_scalar_to_boolean()
- Construct a boolean fsm from a scalar one
-
__add_vertex_aux()
- Private service of sexp_fsm_add_vertex
-
__free_nodelist()
- private service used as callback by
sexp_fsm_destroy_vars_dag
-
__search_eqdef()
- returns an EQDEF node assigning name, searching into
expr. expr can be either a conjunction or a EQDEF node
-
_subst_expr()
- Substitutes all expressions of subst keys c inside expr by
the cooresponding value into subst, ignoring left side of EQDEF
-
sexp_fsm_add_vertex()
-
-
sexp_fsm_add_vertices_from_expr()
- private service of create_vars_dag
-
sexp_fsm_apply_inlining()
- Called during initialization to perform inlining.
-
sexp_fsm_booleanize_expr()
- Booleanizes the given expression, keeping each top level
part of a possible conjuction
-
sexp_fsm_callback_var_fsm_free()
- Private callback that destroys a single variable fsm
contained into the var fsm hash
-
sexp_fsm_copy()
- Copies members from self to copy
-
sexp_fsm_create_vars_dag()
-
-
sexp_fsm_dag_get_roots()
- returns the roots in the graph. Returned list must be
destroyed
-
sexp_fsm_dag_get_subst_hash()
- returns an hash table for variable inlining substitution. The
hash is created by using a scheduling.
-
sexp_fsm_deinit()
- Initializes the vars fsm hash
-
sexp_fsm_destroy_vars_dag()
- Destroyer for the vars dag, used by inlining
-
sexp_fsm_hash_var_fsm_destroy()
- Call to destroy the var fsm hash
-
sexp_fsm_hash_var_fsm_init()
- Initializes the vars fsm hash
-
sexp_fsm_hash_var_fsm_insert_var()
- Adds a var fsm to the internal hash. Private.
-
sexp_fsm_hash_var_fsm_lookup_var()
- Given a variable name, returns the corresponding variable
fsm, or NULL if not found
-
sexp_fsm_init()
- Initializes either the boolean or scalar sexp fsm
-
sexp_fsm_remove_dep_dag_node()
- Removes the given node from deps dag
-
sexp_fsm_simplify_expr()
- removes duplicates from expression containing AND nodes
-
simplifier_hash_add_expr()
- To insert a new node in the hash
-
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_query_expr()
- Queries for an element in the hash, returns True if
found
-
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_input()
-
-
var_fsm_get_invar()
-
-
var_fsm_get_next()
-
Last updated on 2009/01/30 14h:53