SexpFsm_ptr 
SexpFsm_copy(
  const SexpFsm_ptr  self 
)
Copy costructor

Defined in SexpFsm.c

SexpFsm_ptr 
SexpFsm_create_predicate_normalised_copy(
  const SexpFsm_ptr  self, 
  PredicateNormaliser_ptr  normaliser 
)
Predicate-normalisations means that an expression is modified in such a way that at the end the subexpressions of a not-boolean expression can be only not-boolean. This is performed by changing boolean expression "exp" (which is a subexpression of a not-boolean expression) to "ITE(exp, 1, 0)", and then pushing all ITE up to the root of not-boolean expressions. Constrain: the given Sexp FSM has to be NOT boolean. Otherwise, it is meaningless to apply normalisation functions, since all the exporessions are already boolean.

Side Effects SexpFsm_copy

Defined in SexpFsm.c

SexpFsm_ptr 
SexpFsm_create(
  BddEnc_ptr  enc, 
  SymbLayer_ptr  det_layer, 
  SymbLayer_ptr  inl_layer, 
  VarSet_ptr  vars_list, 
  FlatHierarchy_ptr  hierarchy 
)
If provided, the layer will be filled with the determinization variables that might derive from the booleanization. hierarchy will be copied, so the caller is responsible for its destruction.

Defined in SexpFsm.c

void 
SexpFsm_destroy(
  SexpFsm_ptr  self 
)
Destructor

Defined in SexpFsm.c

BoolEnc_ptr 
SexpFsm_get_bool_enc(
  const SexpFsm_ptr  self 
)
This method can be called only when a valid BddEnc was passed to the class constructor (not NULL). Returned instance do not belongs to the caller and must _not_ be destroyed

Defined in SexpFsm.c

node_ptr 
SexpFsm_get_compassion(
  const SexpFsm_ptr  self 
)
Gets the list of sexp expressions defining the set of compassion constraints for this machine.

Defined in SexpFsm.c

FlatHierarchy_ptr 
SexpFsm_get_hierarchy(
  const SexpFsm_ptr  self 
)
Returned hierarchy can be freely changed to create a new sexp fsm derived from self. In any case the caller *must* destroy the returned instance, as a copy of the internal hierarchy is returned. Also, notice that the SexpFsm constructor copies the passed hierarchy.

Defined in SexpFsm.c

Expr_ptr 
SexpFsm_get_init(
  const SexpFsm_ptr  self 
)
Returns an Expr that collects init states for all variables handled by self

Defined in SexpFsm.c

Expr_ptr 
SexpFsm_get_input(
  const SexpFsm_ptr  self 
)
Returns an Expr that collects all input states for all variables handled by self

Defined in SexpFsm.c

Expr_ptr 
SexpFsm_get_invar(
  const SexpFsm_ptr  self 
)
Returns an Expr that collects invar states for all variables handled by self

Defined in SexpFsm.c

node_ptr 
SexpFsm_get_justice(
  const SexpFsm_ptr  self 
)
Gets the list of sexp expressions defining the set of justice constraints for this machine.

Defined in SexpFsm.c

SymbTable_ptr 
SexpFsm_get_symb_table(
  const SexpFsm_ptr  self 
)
This method can be called only when a valid BddEnc was passed to the class constructor (not NULL). Returned instance do not belongs to the caller and must _not_ be destroyed

Defined in SexpFsm.c

Expr_ptr 
SexpFsm_get_trans(
  const SexpFsm_ptr  self 
)
Returns an Expr that collects all next states for all variables handled by self

Defined in SexpFsm.c

Expr_ptr 
SexpFsm_get_var_init(
  const SexpFsm_ptr  self, 
  node_ptr  var_name 
)
Gets the sexp expression defining the initial state for the variable "v".

Defined in SexpFsm.c

Expr_ptr 
SexpFsm_get_var_input(
  const SexpFsm_ptr  self, 
  node_ptr  var_name 
)
Gets the sexp expression defining the input relation for the variable "v".

Defined in SexpFsm.c

Expr_ptr 
SexpFsm_get_var_invar(
  const SexpFsm_ptr  self, 
  node_ptr  var_name 
)
Gets the sexp expression defining the state constraints for the variable "v".

Defined in SexpFsm.c

Expr_ptr 
SexpFsm_get_var_trans(
  const SexpFsm_ptr  self, 
  node_ptr  var_name 
)
Gets the sexp expression defining the transition relation for the variable "v".

Defined in SexpFsm.c

VarSet_ptr 
SexpFsm_get_vars_list(
  const SexpFsm_ptr  self 
)
Returned instance belongs to self

Defined in SexpFsm.c

boolean 
SexpFsm_is_boolean(
  const SexpFsm_ptr  self 
)
Returns true if self if a booleanized fsm, false if it is scalar

Defined in SexpFsm.c

SexpFsm_ptr 
SexpFsm_scalar_to_boolean(
  const SexpFsm_ptr  self, 
  SymbLayer_ptr  det_layer, 
  SymbLayer_ptr  inl_layer 
)
Given layer det_layer will be filled with the determinization variables coming from the booleanization process. Returns a copy if self is already booleanized. Optional inl_layer is used by the inlining simplification (can be NULL)

Defined in SexpFsm.c

static void 
__add_vertex_aux(
  hash_ptr  hash, 
  node_ptr  from, 
  node_ptr  to 
)
Used during inlining

Defined in SexpFsm.c

static enum st_retval 
__free_nodelist(
  char* key, 
  char* val, 
  char* data 
)
private service used as callback by sexp_fsm_destroy_vars_dag

Defined in SexpFsm.c

static node_ptr 
__search_eqdef(
  node_ptr  expr, 
  node_ptr  name 
)
Used during inlining

Defined in SexpFsm.c

static node_ptr 
_subst_expr(
  SymbTable_ptr  st, 
  node_ptr  expr, 
  hash_ptr  subst 
)
Used during inlining

Defined in SexpFsm.c

static void 
sexp_fsm_add_vertex(
  SexpFsm_ptr  self, 
  node_ptr  from, 
  node_ptr  to 
)
Used during inlining

Defined in SexpFsm.c

static boolean 
sexp_fsm_add_vertices_from_expr(
  SexpFsm_ptr  self, 
  node_ptr  name, 
  node_ptr  expr, 
  VarFilterType  filter 
)
Used during inlining

Defined in SexpFsm.c

static node_ptr 
sexp_fsm_apply_inlining(
  SexpFsm_ptr  self, 
  node_ptr  expr 
)
Top level function to apply inlining to the given expression. It has no effects if inl_layer has not been passed

Defined in SexpFsm.c

static Expr_ptr 
sexp_fsm_booleanize_expr(
  SexpFsm_ptr  self, 
  Expr_ptr  expr 
)
If the fsm is not boolean, the input expression is returned

Defined in SexpFsm.c

static assoc_retval 
sexp_fsm_callback_var_fsm_free(
  char * key, 
  char * data, 
  char * arg 
)
Private callback that destroys a single variable fsm contained into the var fsm hash

Defined in SexpFsm.c

static void 
sexp_fsm_copy(
  const SexpFsm_ptr  self, 
  SexpFsm_ptr  copy 
)
Copies members from self to copy

Defined in SexpFsm.c

static void 
sexp_fsm_create_vars_dag(
  SexpFsm_ptr  self 
)

Defined in SexpFsm.c

static NodeList_ptr 
sexp_fsm_dag_get_roots(
  SexpFsm_ptr  self 
)
Used during inlining

Defined in SexpFsm.c

static hash_ptr 
sexp_fsm_dag_get_subst_hash(
  SexpFsm_ptr  self 
)
Used during inlining. Returned hash must be NOT freed

Defined in SexpFsm.c

static void 
sexp_fsm_deinit(
  SexpFsm_ptr  self 
)
Initializes the vars fsm hash

Defined in SexpFsm.c

static void 
sexp_fsm_destroy_vars_dag(
  SexpFsm_ptr  self 
)
Destroyer for the vars dag, used by inlining

Defined in SexpFsm.c

static void 
sexp_fsm_hash_var_fsm_destroy(
  SexpFsm_ptr  self 
)
Private method, used internally

Defined in SexpFsm.c

static void 
sexp_fsm_hash_var_fsm_init(
  SexpFsm_ptr  self 
)
Initializes the vars fsm hash

Defined in SexpFsm.c

static void 
sexp_fsm_hash_var_fsm_insert_var(
  SexpFsm_ptr  self, 
  node_ptr  var, 
  VarFsm_ptr  varfsm 
)
Adds a var fsm to the internal hash. Private.

Defined in SexpFsm.c

static VarFsm_ptr 
sexp_fsm_hash_var_fsm_lookup_var(
  SexpFsm_ptr  self, 
  node_ptr  var 
)
Given a variable name, returns the corresponding variable fsm, or NULL if not found

Defined in SexpFsm.c

static void 
sexp_fsm_init(
  SexpFsm_ptr  self, 
  BddEnc_ptr  enc, 
  SymbLayer_ptr  det_layer, 
  SymbLayer_ptr  inl_layer, 
  VarSet_ptr  vars_list, 
  FlatHierarchy_ptr  hierarchy 
)
hierarchy is copied into an independent FlatHierarchy instance. If the new sexp must be based only on a set of variables, the hierarchy must be empty

Defined in SexpFsm.c

static void 
sexp_fsm_remove_dep_dag_node(
  SexpFsm_ptr  self, 
  node_ptr  from 
)
Used during inlining

Defined in SexpFsm.c

static Expr_ptr 
sexp_fsm_simplify_expr(
  SexpFsm_ptr  self, 
  hash_ptr  hash, 
  Expr_ptr  expr, 
  const int  group 
)
group identifies INVAR, TRANS or INIT group.

Defined in SexpFsm.c

static void 
simplifier_hash_add_expr(
  hash_ptr  hash, 
  Expr_ptr  expr, 
  const int  group 
)
group is INIT, INVAR or TRANS

Side Effects The hash can change

Defined in SexpFsm.c

static hash_ptr 
simplifier_hash_create(
    
)
This is used when creating cluster list from vars list

Defined in SexpFsm.c

static void 
simplifier_hash_destroy(
  hash_ptr  hash 
)
Call after sexp_fsm_cluster_hash_create

Defined in SexpFsm.c

static boolean 
simplifier_hash_query_expr(
  hash_ptr  hash, 
  Expr_ptr  expr, 
  const int  group 
)
Queries for an element in the hash, returns True if found

Defined in SexpFsm.c

static VarFsm_ptr 
var_fsm_create(
  Expr_ptr  init, 
  Expr_ptr  invar, 
  Expr_ptr  next 
)
Creates a var fsm

Defined in SexpFsm.c

static void 
var_fsm_destroy(
  VarFsm_ptr  self 
)
It does not destroy the init, trans and invar nodes. It destroys only the support nodes

Defined in SexpFsm.c

static Expr_ptr 
var_fsm_get_init(
  VarFsm_ptr  self 
)

Defined in SexpFsm.c

static Expr_ptr 
var_fsm_get_input(
  VarFsm_ptr  self 
)

Defined in SexpFsm.c

static Expr_ptr 
var_fsm_get_invar(
  VarFsm_ptr  self 
)

Defined in SexpFsm.c

static Expr_ptr 
var_fsm_get_next(
  VarFsm_ptr  self 
)

Defined in SexpFsm.c

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