BoolSexpFsm.c
Implementation of class 'BoolSexpFsm'
Expr.c
Abstraction for expression type impemented as node_ptr
SexpFsm.c
The SexpFsm implementation

BoolSexpFsm.c

Implementation of class 'BoolSexpFsm'

By: Roberto Cavada

This module defines a class representing a boolean sexp-based FSM. The class BoolSexpFsm derives from SexpFsm.

See AlsoBoolSexpFsm.h


Expr.c

Abstraction for expression type impemented as node_ptr

By: Roberto Cavada

Expr_true()
Returns the true expression value
Expr_false()
Returns the false expression value
Expr_is_true()
Checkes whether given value is the true value
Expr_is_false()
Checkes whether given value is the false value
Expr_and()
Builds the logical/bitwise AND of given operators
Expr_and_nil()
Builds the logical/bitwise AND of given operators, considering Nil as the true value
Expr_and_from_list()
Builds the logical/bitwise AND of all elements in the list
Expr_not()
Builds the logical/bitwise NOT of given operator
Expr_or()
Builds the logical/bitwise OR of given operators
Expr_xor()
Builds the logical/bitwise XOR of given operators
Expr_xnor()
Builds the logical/bitwise XNOR of given operators
Expr_iff()
Builds the logical/bitwise IFF of given operators
Expr_simplify_iff()
Builds the logical/bitwise IFF of given operators
Expr_implies()
Builds the logical/bitwise IMPLIES of given operators
Expr_ite()
Builds the If-Then-Else node with given operators
Expr_next()
Constructs a NEXT node of given expression
Expr_equal()
Builds the logical EQUAL of given operators
Expr_simplify_equal()
Builds the logical EQUAL of given operators
Expr_notequal()
Builds the logical NOTEQUAL of given operators
Expr_simplify_notequal()
Builds the logical NOTEQUAL of given operators
Expr_lt()
Builds the predicate LT (less-then) of given operators
Expr_simplify_lt()
Builds the predicate LT (less-then) of given operators
Expr_le()
Builds the predicate LE (less-then-equal) of given operators
Expr_simplify_le()
Builds the predicate LE (less-then-equal) of given operators
Expr_gt()
Builds the predicate GT (greater-then) of given operators
Expr_simplify_gt()
Builds the predicate GT (greater-then) of given operators
Expr_ge()
Builds the predicate GE (greater-then-equal) of given operators
Expr_simplify_ge()
Builds the predicate GE (greater-then-equal) of given operators
Expr_plus()
Builds the scalar node for PLUS of given operators
Expr_minus()
Builds the scalar node for MINUS of given operators
Expr_times()
Builds the scalar node for TIMES of given operators
Expr_divide()
Builds the scalar node for DIVIDE of given operators
Expr_mod()
Builds the scalar node for MODule of given operators
Expr_unary_minus()
Builds the scalar node for UMINUS (unary minus) of given operators
Expr_word_left_shift()
Builds the node left shifting of words. Description [Works with words. Performs local syntactic simplification
Expr_word_right_shift()
Builds the node right shifting of words. Description [Works with words. Performs local syntactic simplification
Expr_word_left_rotate()
Builds the node left rotation of words. Description [Works with words. Performs local syntactic simplification
Expr_word_right_rotate()
Builds the node right rotation of words. Description [Works with words. Performs local syntactic simplification
Expr_word_bit_select()
Builds the node for bit selection of words. Description [Works with words. Performs local syntactic simplification
Expr_simplify_word_bit_select()
Builds the node for bit selection of words. Description [Works with words. Performs local semantic and syntactic simplification
Expr_word_concatenate()
Builds the node for word concatenation. Description [Works with words. Performs local syntactic simplification
Expr_word1_to_bool()
Builds the node for casting word1 to boolean. Description [Works with words with width 1. Performs local syntactic simplification
Expr_bool_to_word1()
Builds the node for casting boolean to word1. Description [Works with booleans. Performs local syntactic simplification
Expr_signed_word_to_unsigned()
Builds the node for casting signed words to unsigned words. Description [Works with words. Performs local syntactic simplification
Expr_unsigned_word_to_signed()
Builds the node for casting unsigned words to signed words. Description [Works with words. Performs local syntactic simplification
Expr_simplify_word_resize()
Builds the node for resizing a word.
Expr_word_extend()
Builds the node for extending a word.
Expr_simplify_word_extend()
Builds the node for extending a word.
Expr_attime()
Creates a ATTIME node
Expr_attime_get_time()
Retrieves the time out of an ATTIME node
Expr_attime_get_untimed()
Retrieves the untimed node out of an ATTIME node
Expr_union()
Makes a union node
Expr_range()
Makes a TWODOTS node, representing an integer range
Expr_setin()
Makes a setin node, with possible syntactic simplification.
Expr_function()
Builds an Uninterpreted function
Expr_resolve()
This is the top-level function that simplifiers can use to simplify expressions. This evaluates constant values in operands left and right with respect to the operation required with parameter type.
Expr_simplify()
Top-level simplifier that evaluates constants and simplifies syntactically the given expression
Expr_is_booleanizable()
Check if an expr is of a finite range type
Expr_is_timed()
Determines whether a formula has ATTIME nodes in it
Expr_get_time()
Obtain the base time of an expression
Expr_time_is_dont_care()
Returns true if the time (obtained by Expr_get_time) is dont't care
Expr_time_is_current()
Returns true if the time (obtained by Expr_get_time) is current
Expr_time_is_next()
Returns true if the time (obtained by Expr_get_time) is next
Expr_untimed()
Returns the untimed version of an expression
Expr_untimed_explicit_time()
Returns the untimed version of an expression without searching for the current time
expr_timed_to_untimed()
Converts a timed node into an untimed node
expr_get_curr_time()
Calculates current time for an expression
expr_is_timed_aux()
true if expression is timed
expr_is_booleanizable_aux()
true if expression is booleanizable

SexpFsm.c

The SexpFsm implementation

By: Roberto Cavada

A SexpFsm instance represents a scalar FSM, but it is used also as base class for boolean FSMs which are instances of derived class BoolSexpFsm

See AlsoSexpFsm.h SexpFsm_private.h

()
Set to 1 (needs recompilation) to force auto-check of the SexpFsm
SexpFsm_create()
Costructor for a scalar sexp fsm
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_is_boolean()
Use to check if this FSM is a scalar or boolean fsm
SexpFsm_get_symb_table()
Returns the symbol table that is connected to the BoolEnc instance connected to self
SexpFsm_get_hierarchy()
Returns the internal 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 set of variables in the FSM
SexpFsm_get_symbols_list()
Returns the set of symbols in the FSM
SexpFsm_get_vars()
Returns the set of variables in the FSM
SexpFsm_apply_synchronous_product()
Performs the synchronous product of two FSMs
SexpFsm_is_syntactically_universal()
Checks if the SexpFsm is syntactically universal
SexpFsm_self_check()
Self-check for the instance
sexp_fsm_create_vars_dag()
sexp_fsm_init()
Initializes the sexp fsm
sexp_fsm_deinit()
Initializes the vars fsm hash
sexp_fsm_copy_aux()
private service for copying self to other
__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_copy()
This is called by the virtual copy constructor
sexp_fsm_finalize()
The SexpFsm class virtual finalizer
sexp_fsm_hash_var_fsm_init()
Initializes the vars fsm hash
sexp_fsm_simplify_expr()
removes duplicates from expression containing AND nodes
_subst_expr()
Substitutes all expressions of subst keys c inside expr by the corresponding value into subst, ignoring left side of EQDEF. Defines are expanded. Output parameter assg will contain the set of substuituted assignments
__add_edge_aux()
Private service of sexp_fsm_add_edge
sexp_fsm_add_edge()
Adds an edgs to the graph. If to is null, adds only the vertex from
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_equal_eqdef()
Traverses the given expression searching for assignments and equalities concerning given variable name.
sexp_fsm_dag_get_subst_hash()
returns an hash table for variable inlining substitution. The hash is created by using a scheduling.
sexp_fsm_conj_equals()
Private service of sexp_fsm_apply_inlining
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()
var_fsm_synchronous_product()
Returns new var fsm that is synchronous product of var fsms.

Last updated on 2010/05/19 22h:26