-
Expr_and_from_list()
- Builds the logical/bitwise AND of all elements in the
list
-
Expr_and_nil()
- Builds the logical/bitwise AND of given operators,
considering Nil as the true value
-
Expr_and()
- Builds the logical/bitwise AND of given operators
-
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_attime()
- Creates a ATTIME node
-
Expr_bool_to_word1()
- Builds the node for casting boolean to word1.
Description [Works with booleans.
Performs local syntactic simplification
-
Expr_divide()
- Builds the scalar node for DIVIDE of given operators
-
Expr_equal()
- Builds the logical EQUAL of given operators
-
Expr_false()
- Returns the false expression value
-
Expr_function()
- Builds an Uninterpreted function
-
Expr_get_time()
- Obtain the base time of an expression
-
Expr_ge()
- Builds the predicate GE (greater-then-equal)
of given operators
-
Expr_gt()
- Builds the predicate GT (greater-then)
of given operators
-
Expr_iff()
- Builds the logical/bitwise IFF of given operators
-
Expr_implies()
- Builds the logical/bitwise IMPLIES of given operators
-
Expr_is_false()
- Checkes whether given value is the false value
-
Expr_is_timed()
- Determines whether a formula has ATTIME nodes in it
-
Expr_is_true()
- Checkes whether given value is the true value
-
Expr_ite()
- Builds the If-Then-Else node with given operators
-
Expr_le()
- Builds the predicate LE (less-then-equal)
of given operators
-
Expr_lt()
- Builds the predicate LT (less-then) of given operators
-
Expr_minus()
- Builds the scalar node for MINUS of given operators
-
Expr_mod()
- Builds the scalar node for MODule of given operators
-
Expr_next()
- Constructs a NEXT node of given expression
-
Expr_notequal()
- Builds the logical NOTEQUAL of given operators
-
Expr_not()
- Builds the logical/bitwise NOT of given operator
-
Expr_or()
- Builds the logical/bitwise OR of given operators
-
Expr_plus()
- Builds the scalar node for PLUS of given operators
-
Expr_range()
- Makes a TWODOTS node, representing an integer range
-
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_setin()
- Makes a setin node, with possible 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_simplify_equal()
- Builds the logical EQUAL of given operators
-
Expr_simplify_ge()
- Builds the predicate GE (greater-then-equal)
of given operators
-
Expr_simplify_gt()
- Builds the predicate GT (greater-then)
of given operators
-
Expr_simplify_iff()
- Builds the logical/bitwise IFF of given operators
-
Expr_simplify_le()
- Builds the predicate LE (less-then-equal)
of given operators
-
Expr_simplify_lt()
- Builds the predicate LT (less-then) of given operators
-
Expr_simplify_notequal()
- Builds the logical NOTEQUAL of given operators
-
Expr_simplify_word_bit_select()
- Builds the node for bit selection of words.
Description [Works with words. Performs local semantic and syntactic
simplification
-
Expr_simplify_word_extend()
- Builds the node for extending a word.
-
Expr_simplify_word_resize()
- Builds the node for resizing a word.
-
Expr_simplify()
- Top-level simplifier that evaluates constants and
simplifies syntactically the given expression
-
Expr_time_is_current()
- Returns true if the time (obtained by Expr_get_time) is
current
-
Expr_time_is_dont_care()
- Returns true if the time (obtained by Expr_get_time) is
dont't care
-
Expr_time_is_next()
- Returns true if the time (obtained by Expr_get_time) is
next
-
Expr_times()
- Builds the scalar node for TIMES of given operators
-
Expr_true()
- Returns the true expression value
-
Expr_unary_minus()
- Builds the scalar node for UMINUS (unary minus) of given
operators
-
Expr_union()
- Makes a union node
-
Expr_unsigned_word_to_signed()
- Builds the node for casting unsigned words to signed words.
Description [Works with words.
Performs local syntactic simplification
-
Expr_untimed_explicit_time()
- Returns the untimed version of an expression without
searching for the current time
-
Expr_untimed()
- Returns the untimed version of an expression
-
Expr_word1_to_bool()
- Builds the node for casting word1 to boolean.
Description [Works with words with width 1.
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_word_concatenate()
- Builds the node for word concatenation.
Description [Works with words.
Performs local syntactic simplification
-
Expr_word_extend()
- Builds the node for extending a word.
-
Expr_word_left_rotate()
- Builds the node left rotation of words.
Description [Works with words.
Performs local syntactic simplification
-
Expr_word_left_shift()
- Builds the node left shifting 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_right_shift()
- Builds the node right shifting of words.
Description [Works with words.
Performs local syntactic simplification
-
Expr_xnor()
- Builds the logical/bitwise XNOR of given operators
-
Expr_xor()
- Builds the logical/bitwise XOR of given operators
-
SexpFsm_apply_synchronous_product()
- Performs the synchronous product of two FSMs
-
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 sexp fsm
-
SexpFsm_destroy()
- Destructor
-
SexpFsm_get_compassion()
- Gets the list of sexp expressions defining the set of
compassion constraints for this machine.
-
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_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_symbols_list()
- Returns the set of symbols in the FSM
-
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 set of variables in the FSM
-
SexpFsm_get_vars()
- Returns the set of variables in the FSM
-
SexpFsm_is_boolean()
- Use to check if this FSM is a scalar or boolean fsm
-
SexpFsm_is_syntactically_universal()
- Checks if the SexpFsm is syntactically universal
-
SexpFsm_self_check()
- Self-check for the instance
-
expr_get_curr_time()
- Calculates current time for an expression
-
expr_is_timed_aux()
- true if expression is timed
-
expr_timed_to_untimed()
- Converts a timed node into an untimed node
-
sexp_fsm_callback_var_fsm_free()
- Private callback that destroys a single variable fsm
contained into the var fsm hash
-
sexp_fsm_const_var_fsm_init()
- Initializes the const_var_fsm field
-
sexp_fsm_copy_aux()
- private service for copying self to other
-
sexp_fsm_copy()
- This is called by the virtual copy constructor
-
sexp_fsm_deinit()
- Initializes the vars fsm hash
-
sexp_fsm_finalize()
- The SexpFsm class virtual finalizer
-
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 the sexp fsm
-
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()
-
-
var_fsm_synchronous_product()
- Returns new var fsm that is synchronous product of var
fsms.
-
()
- Set to 1 (needs recompilation) to force auto-check of the
SexpFsm
Last updated on 2010/11/04 13h:33