Index of values


( * ) [Numeral]
Product
( * ) [Decimal]
Product
( *@ ) [Term.Abbrev]
Infix operator to create an integer or real product
(!@) [Term.Abbrev]
Prefix operator to create an Boolean negation
(&@) [Term.Abbrev]
Infix operator to create a Boolean conjunction
(+) [Numeral]
Sum
(+) [Decimal]
Sum
(+@) [Term.Abbrev]
Infix operator to create an integer or real sum
(-) [Numeral]
Difference
(-) [Decimal]
Difference
(-@) [Term.Abbrev]
Infix operator to create an integer or real difference
(/%@) [Term.Abbrev]
Infix operator to create an integer quotient
(/) [Numeral]
Quotient
(/) [Decimal]
Quotient
(//@) [Term.Abbrev]
Infix operator to create a real quotient
(<) [Numeral]
Less than predicate
(<) [Decimal]
Less than predicate
(<=) [Numeral]
Less than or equal predicate
(<=) [Decimal]
Less than or equal predicate
(<=@) [Term.Abbrev]
Infix operator to create a less-or-equal predicate
(<>) [Numeral]
Disequality
(<>) [Decimal]
Disequality
(<@) [Term.Abbrev]
Infix operator to create a less-than predicate
(=) [Numeral]
Equality
(=) [Decimal]
Equality
(=>@) [Term.Abbrev]
Infix operator to create a Boolean implication
(=@) [Term.Abbrev]
Infix operator to create an equality
(>) [Numeral]
Greater than predicate
(>) [Decimal]
Greater than predicate
(>=) [Numeral]
Greater than or equal predicate
(>=) [Decimal]
Greater than or equal predicate
(>=@) [Term.Abbrev]
Infix operator to create a greater-or-equal predicate
(>@) [Term.Abbrev]
Infix operator to create a greater-than predicate
(@::) [Lib]
Add element to the head of the list if the option value is not None.
(mod) [Numeral]
Remainder
(mod) [Decimal]
Remainder
(|@) [Term.Abbrev]
Infix operator to create a Boolean disjunction
(~-) [Numeral]
Unary negation
(~-) [Decimal]
Unary negation
(~@) [Term.Abbrev]
Prefix operator to create an integer or real negation
?%@ [Term.Abbrev]
Prefix operator to create an numeral
__ocaml_lex_custom_rec [YicesLexer]
__ocaml_lex_error_msg_rec [YicesLexer]
__ocaml_lex_main_rec [SExprLexer]
__ocaml_lex_ruleTail_rec [SExprLexer]
__ocaml_lex_scan_block_comment_rec [SExprLexer]
__ocaml_lex_scan_quoted_rec [SExprLexer]
__ocaml_lex_scan_string_rec [SExprLexer]
__ocaml_lex_tables [SExprLexer]
__ocaml_lex_tables [YicesLexer]
__ocaml_lex_token_rec [YicesLexer]

A
abs [Numeral]
Absolute value
abs [Decimal]
Absolute value
abs_ident [LustreIdent]
Identifier for abstracted variables
abs_ident_string [Lib.ReservedIds]
New variables from abstraction.
abstr [Flags.Certif]
Use abstract type indexes in certificates/proofs.
abstr [Flags.IC3]
Abstraction mechanism IC3 should use.
abstract_subsystems [TestgenStrategies.Sig]
Returns true if the strategy requires subsystems to be abstracted.
activate [TestgenLib]
Calls the actlit_implications field of a context on its input list of actlit / term pair.
active [Flags.Testgen]
Activates test generation.
actlit_of_frame [Clause]
Create or return an activation literal for the given frame
actlit_p0_of_clause [Clause]
Return the activation literal for the positive unprimed clause
actlit_p0_of_prop_set [Clause]
Return the activation literal for the positive conjunction of properties
actlit_p1_of_clause [Clause]
Return the activation literal for the positive primed clause
actlit_p1_of_prop_set [Clause]
Return the activation literal for the positive primed conjunction of properties
actlit_symbol_of_frame [Clause]
Create or return the uninterpreted functoin symbol for the activation literal for the given frame
actlits_n0_of_clause [Clause]
Return the activation literals for the negated clause literals
actlits_n0_of_prop_set [Clause]
Return the (singleton list of) activation literals for the negated conjunction of properties
actlits_n1_of_clause [Clause]
Return the activation literals for the negated, primed literals
actlits_n1_of_prop_set [Clause]
Return the (singleton list of) activation literals for the negated primed conjunction of properties
add [Numeral]
Sum
add [Decimal]
Sum
add [Trie.S]
Bind a value to the key in the trie
add_ass [LustreContract]
Adds assumes to a contract.
add_colors [Pretty]
add color tags to a formatter
add_contract_node_decl_to_context [LustreContext]
Add a contract node to the context for inlining later
add_expr_for_ident [LustreContext]
Add a binding of an identifier to an expression to context
add_free_constant [LustreContext]
Register a free constant, shadows previous declarations
add_gua [LustreContract]
Adds guarantees to a contract.
add_input_file [Flags]
add_invariant [TransSys]
Add an invariant to the transition system.
add_modes [LustreContract]
Adds modes to a contract.
add_node_ass [LustreContext]
Adds assumptions to a node.
add_node_assert [LustreContext]
Add assertion to context
add_node_call [LustreContext]
Add node call to context
add_node_equation [LustreContext]
Add equation to context
add_node_gua [LustreContext]
Adds guarantees to a node (boolean is the candidate flag).
add_node_input [LustreContext]
Add node input to context
add_node_local [LustreContext]
Add node local to context
add_node_mode [LustreContext]
Add modes to node
add_node_output [LustreContext]
Add node output to context
add_node_property [LustreContext]
Add property to context
add_node_to_context [LustreContext]
Return a context that is identical to the previous context with the node constructed in the current context added
add_properties [TransSys]
Add properties to the transition system
add_scoped_invariant [TransSys]
Add an invariant to the transition system.
add_two_polys [Poly]
Add two polynomials with a ordering of varialbes and a accumulator
add_type_for_ident [LustreContext]
Add a binding of an identifier to a type to context
all_ens_ident_string [Lib.ReservedIds]
New variables from node instance.
all_index_types_of_array [Type]
Return all array index types of a nested array type
all_input_files [Flags]
All lustre files in the cone of influence of the input file.
all_out [Flags.Invgen]
Forces invgen to consider a huge number of candidates.
all_props_proved [TransSys]
Return true if all properties which are not candidates are either valid or invalid
all_req_ident_string [Lib.ReservedIds]
Observer for contract ensures.
all_stats [Event]
Return the last statistics received
all_subsystems [SubSystem]
Return all subsystems in topological order with the top system at the head of the list
analysis_time [Stat]
append [Stat]
Append at the end of an integers statistics list
apply_subst [LustreExpr]
apply_subst [Term]
Apply a substitution variable -> term
are_definitions_allowed [LustreContext]
Returns true if new definitions are allowed in the context
arg_type_of_uf_symbol [UfSymbol]
Return the type of the arguments of the uninterpreted symbol
arith_eq_only [Flags.Invgen]
Forces arith invgen to look for equalities only.
array_and_indexes_of_select [Term]
array_bounds_of_index [LustreIndex]
Return the list of bounds of the array indexes in the index
array_max [Lib]
Returns the maximum element of a non-empty array
array_vars_of_index [LustreIndex]
Return the list of array variables of the array indexes in the index
assert_0_to [Unroller]
Asserts some terms from 0 to k-1.
assert_1_to [Unroller]
Asserts some terms from 1 to k-1.
assert_expr [SMTSolver]
Assert an SMT expression in the current context
assert_expr [SolverSig.Inst]
Assert the expression
assert_named_term [SMTSolver]
Name a term, convert a term to an SMT expression and assert
assert_named_term_wr [SMTSolver]
Name a term, convert a term to an SMT expression and assert, and return the name
assert_new_invs_to [Unroller]
Asserts some new one- and two-state invariant up to k-1, starting at * 0 for one-state invariants, * 1 for two-state invariants.
assert_term [SMTSolver]
Convert a term to an SMT expression and assert
assignable_state_var_of_ident [LustreContext]
Return the respective state variable if the expression denotes an output or a local variable of the node in the context
assumptions_empty [Analysis]
Merges two assumptions.
assumptions_fold [Analysis]
assumptions_merge [Analysis]
Assumptions of a transition system.
assumptions_of_sys [Analysis]
Fold over assumptions.
ast_of_file [LustreInput]
Parse from the file, returns the AST.

B
base_add_invariants [LockStepDriver]
Adds some invariants to a base checker.
base_offset [LustreExpr]
Offset of state variable at first instant
base_state_vars_of_init_expr [LustreExpr]
Return all state variables of the initial state expression at the base instant
base_term_of_expr [LustreExpr]
Term at first instant with the given offset as zero
base_term_of_state_var [LustreExpr]
Term of instance of state variable at first instant with the given offset as zero
base_term_of_t [LustreExpr]
Term at first instant with the given offset as zero
base_var_of_state_var [LustreExpr]
Instance of state variable at first instant with the given offset as zero
bindings [Trie.S]
Return an association list of key to bindings in the trie
blit [HString]
block_in_future [Flags.IC3]
Block counterexample in future frames.
block_in_future_first [Flags.IC3]
Block counterexample in future frames first before returning to frame.
blocking_path_of [TestgenTree]
Returns the term encoding the path of modes leading to the current node but blocking its mode conjunction and explored modes.
bmc_k [Stat]
Highest k reached
bmc_stats [Stat]
BMC statistics
bmc_stats_title [Stat]
Title for BMC statistics
bmc_stop_timers [Stat]
Stop and record all timers
bmc_total_time [Stat]
Total time in BMC
bool_eq_only [Flags.Invgen]
Forces bool invgen to look for equalities only.
bool_of_hstring [GenericSMTLIBDriver]
bool_of_symbol [Symbol]
Return true for the `TRUE symbol and false for the `FALSE symbol
bool_of_term [Term]
Return Boolean constant of a term
bool_of_value [Eval]
Cast a value to a Boolean, raise Invalid_argument if value is not a Boolean
bounds_of_int_range [Type]
Return bounds of an integer range type, fail with Invalid_argument "bounds_of_int_range" if the type is not an integer range type.
bump_and_apply_k [Term]
Apply function to term for instants 0..k
bump_and_merge [Model]
Combine assignments of two models into one as in Model.merge, but bump the variables in the second model by the given offset before merging.
bump_offset_of_state_var_instance [Var]
Return a new variable with the offset of the state variable instance incremented by the given value
bump_state [Term]
Add to offset of state variable instances
bump_var [Model]
Add k to offset of all variables in model

C
c2i [Debug]
c2i_model_comp_time [Stat]
Time spent comparing models.
c2i_move_time [Stat]
Time spent in moving and evaluating.
c2i_moves [Stat]
Number of random moves made.
c2i_query_time [Stat]
Time spent querying solvers.
c2i_stats [Stat]
All C2I statistics.
c2i_stats_title [Stat]
Title for C2I statistics.
c2i_stop_timers [Stat]
Stop and record all timers.
c2i_str_invs [Stat]
Number of strengthening invariants found.
c2i_total_time [Stat]
Total time.
c2i_zero_cost [Stat]
Number of zero-cost candidates found.
call_outputs_of_node_call [LustreContext]
Return variables capturing outputs of node call if a node call with the same input parameters and activation condition is in the context.
capitalize [HString]
cardinal [Trie.S]
Return the number of bindings in the trie
catch_break [TermLib.Signals]
Raise exception on ctrl+c if true.
certif [Debug]
certif [Flags.Certif]
Certification only.
certif_cvc4_time [Stat]
certif_frontend_time [Stat]
certif_gen_time [Stat]
certif_k [Stat]
certif_min_time [Stat]
certif_old_k [Stat]
certif_old_size [Stat]
certif_size [Stat]
certif_stats [Stat]
Certificate statistics
certif_stats_title [Stat]
Title for certificate statistics
certif_stop_timers [Stat]
cex_to_inputs_csv [TestgenLib]
Converts a model to the system's input values in csv.
cex_to_outputs_csv [TestgenLib]
Converts a model to the system's output values in csv.
cformula_contains_variable [Poly]
Return true when the cformula contains the variable, false otherwise
chain [Res]
Feeds a result to a function returning a result, propagates if argument's an error.
chain_list [Lib]
chain_list [e1; e2; ...] is [[e1; e2]; [e2; e3]; ... ]
change_type_of_state_var [StateVar]
Change the type of a state variable
char_for_backslash [SExprLexer]
check_and_block [Compress]
Given an inductive counterexample return a list of terms to force those states on the path to be different that are equivalent under some simulation relations.
check_graph [InvGenGraph.Graph]
Checks that a graph makes sense.
check_implem [Flags.Contracts]
Check modes.
check_inductive [Flags.IC3]
Check inductiveness of blocking clauses.
check_modes [Flags.Contracts]
Check modes.
check_sat [SMTSolver]
Check satisfiability of the current context
check_sat [SolverSig.Inst]
Check satisfiability of the asserted expressions
check_sat_and_get_term_values [SMTSolver]
Checks satisfiability of the current context, and evaluate one of two continuation functions depending on the result
check_sat_assume [Flags.Smt]
Use check-sat with assumptions, or simulate with push/pop
check_sat_assuming [SMTSolver]
Checks satisfiability of the current context assuming the given list of literals, and evaluate one of two continuation functions depending on the result
check_sat_assuming [SolverSig.Inst]
Check satisfiability of the asserted expressions assuming the input literals.
check_sat_assuming_ab [SMTSolver]
Check satisfiability under assumptions as with SMTSolver.check_sat_assuming, but the two continuations can return different values that are wrappen in the SMTSolver.sat_or_unsat type
check_sat_assuming_and_get_term_values [SMTSolver]
Check satisfiability under assumptions as with SMTSolver.check_sat_assuming, but if the solver returns satisfiable, the values of the terms in the current context are given to the continuation t as its second argument
check_sat_assuming_cmd [YicesDriver]
check_sat_assuming_cmd [Yices2SMT2Driver]
check_sat_assuming_cmd [Z3Driver]
check_sat_assuming_cmd [GenericSMTLIBDriver]
check_sat_assuming_cmd [CVC4Driver]
check_sat_assuming_cmd [SolverDriver.S]
Special command for check-sat-assuming
check_sat_assuming_supported [YicesDriver]
check_sat_assuming_supported [Yices2SMT2Driver]
check_sat_assuming_supported [Z3Driver]
check_sat_assuming_supported [GenericSMTLIBDriver]
check_sat_assuming_supported [CVC4Driver]
check_sat_assuming_supported [SolverDriver.S]
Returns true if check-sat-assuming functionality is supported
check_sat_assuming_supported [SolverSig.Inst]
Indicates whether the solver supports the check-sat-assuming command.
check_sat_assuming_tf [SMTSolver]
Check satisfiability under assumptions as with SMTSolver.check_sat_assuming, but return true or false without continuations as arguments
check_sat_limited_cmd [YicesDriver]
check_sat_limited_cmd [Yices2SMT2Driver]
check_sat_limited_cmd [Z3Driver]
check_sat_limited_cmd [GenericSMTLIBDriver]
check_sat_limited_cmd [CVC4Driver]
check_sat_limited_cmd [SolverDriver.S]
Internal command for check-sat with timeout in milliseconds
check_termination [Messaging.S]
Returns true if a termination message was received.
check_termination [Event]
Terminates if a termination message was received.
check_type [Type]
check_type s t returns true if s is a subtype of t
check_unroll [Flags.BmcKind]
Check that the unrolling of the system alone is satisfiable.
check_vars_defined [LustreContext]
Check that the node being defined has no undefined local or output variables
checksat [TestgenSolver]
checksat t n term actlits terms Checks the satisfiability of term term in conjunction with activation literals actlits with the system unrolled up to n.
choose [Trie.S]
class_count [InvGenGraph.Graph]
Total number of classes in the graph.
clause_of_prop_set [Clause]
Return the unit clause containing the conjunction of the properties as a literals
clause_of_term_time [Stat]
clear [Hashcons.S]
clear [Hashcons]
Removes all elements from the table.
clear_input_files [Flags]
Adds a lustre file in the cone of influence of the input file.
clone [InvGenGraph.Graph]
Clones a graph.
close_expr [LustreContext]
Replace unguarded pre operators with oracle constants and return expression and modified context.
cmd_line [YicesDriver]
cmd_line [Yices2SMT2Driver]
cmd_line [Z3Driver]
cmd_line [GenericSMTLIBDriver]
cmd_line [CVC4Driver]
cmd_line [SolverDriver.S]
Command line options
cmp [InvGenDomain.Domain]
Creates the term corresponding to the equality of two terms.
color [Flags]
Colored output.
comment [TestgenLib]
Calls the trace_comment field of a context on its input string.
comment [TestgenSolver]
Comment trace for the underlying solver.
comment_delims [YicesDriver]
comment_delims [GenericSMTLIBDriver]
comment_delims [SolverDriver.S]
Begin / end delimiters for comments
compare [Numeral]
Comparison
compare [HString]
Comparison function on hashconsed strings
compare [Hashcons]
compare [Decimal]
Comparison
compare [LustreExpr]
Total order on lustre expressions
compare [LustreIdent]
Total ordering of identifiers
compare [Trie.S]
Comparision function on tries
compare [Term]
Comparison function on terms
compare [Scope]
Total order of scopes
compare [Ltree.S]
Comparison function on terms
compare [Ident]
Total order of identifiers
compare_attrs [TermAttr]
Comparison function on attributes
compare_expr [LustreExpr]
Total order on expressions
compare_indexes [LustreIndex]
Total order of indexes
compare_lists [Lib]
Lexicographic comparison of lists
compare_pairs [Lib]
Lexicographic comparison of pairs
compare_pos [Lib]
Comparision on positions
compare_scope [TransSys]
Compare transition systems by their scope
compare_state_vars [StateVar]
Comparison function on state variables
compare_symbols [Symbol]
Comparison function on symbols
compare_types [Type]
Comparison function on types
compare_uf_symbols [UfSymbol]
Comparison function on uninterpreted function symbols
compare_variables [Poly]
Comparison of variables: variables to be eliminated earlier are smaller, compare as terms if none is to be eliminated
compare_vars [Var]
Comparison function on variables
compatible_indexes [LustreIndex]
compile_oracle_to_rust [InputSystem]
Compiles a system (scope) to Rust as an oracle to the folder specified as a crate.
compile_to_rust [InputSystem]
Compiles a system (scope) to Rust to the folder specified as a crate.
compositional [Flags.Contracts]
Compositional analysis.
compress [Debug]
compress [Flags.BmcKind]
Compress inductive counterexample.
compress_equal [Flags.BmcKind]
Compress inductive counterexample when states are equal modulo inputs.
compress_same_pred [Flags.BmcKind]
Compress inductive counterexample when states have same predecessors.
compress_same_succ [Flags.BmcKind]
Compress inductive counterexample when states have same successors.
concat [HString]
const_of_smtlib_atom [GenericSMTLIBDriver]
construct [Term]
Convert a flat term to a term
construct [Ltree.S]
Convert the flattened representation back into a term
constructors_of_enum [Type]
Return constructors of an enumerated datatype
contains [HString]
contains_from [HString]
contract_gen [Flags.Contracts]
Contract generation.
contract_gen_depth [Flags.Contracts]
Contract generation: max depth.
contract_gen_file [Lib.Names]
Contract generation.
contract_gen_param [InputSystem]
Parameter for contract generation.
contract_has_pre_or_arrow [LustreAst]
Returns true iff a contract mentions a `pre` or a `->`.
contract_name [Lib.Names]
Invariant logging.
contract_node_decl_of_ident [LustreContext]
Return a contract node by its identifier
contract_nodes [LustreContext]
The contract nodes in the context.
contract_scope_of [LustreContext]
The contract scope of a context.
convert_select [Term]
Convert terms of the form (select (select a i) j) to (select a i j) for multi-dimensional arrays
converter [SMTSolver]
copy_clause [Clause]
copy_clause_block_prop [Clause]
Return a copy of the clause with fresh activation literal
copy_clause_fwd_prop [Clause]
create [HString]
create [Hashcons.S]
create [Hashcons]
create n creates an empty table of initial size n.
create [Model]
Create a model of the given size
create_and_assert_fresh_actlit [Clause]
Create a fresh activation literal, declare it in the solver, and assert a term guarded with it
create_dir [Lib]
Create a directory if it does not already exists.
create_function [LustreContext]
Return a copy of the context with an empty function of the given name in the context
create_instance [SMTSolver]
Create a new instance of an SMT solver of the given kind and with the given flags
create_node [LustreContext]
Return a copy of the context with an empty node of the given name and is extern flag in the context
create_path [Model]
Create a path of the given size
cur_offset [LustreExpr]
Offset of state variable at current instant
cur_state_vars_of_step_expr [LustreExpr]
Return all state variables of the step expression at the current instant
cur_term_of_expr [LustreExpr]
Term at current instant with the given offset as zero
cur_term_of_state_var [LustreExpr]
Term of instance of state variable at current instant with the given offset as zero
cur_term_of_t [LustreExpr]
Term at current instant with the given offset as zero
cur_var_of_state_var [LustreExpr]
Instance of state variable at current instant with the given offset as zero
current_node_calls [LustreContext]
Returns the calls made by the current node, if any.
current_node_map [LustreContext]
Maps something to the current node.
current_node_modes [LustreContext]
Returns the modes of the current node.
current_node_name [LustreContext]
Returns the name of the current node, if any.
custom [YicesResponse]
custom [YicesLexer]
cvc4_bin [Flags.Smt]
Executable of CVC4 solver
cvc4_expr_or_lambda_of_string_sexpr' [CVC4Driver]

D
deactivate_clause [Clause]
Assert the negation of all activation literals of clause in the solver instance
debug [Flags]
Debug sections to enable
debug_log [Flags]
Logfile for debug output
dec_code [SExprLexer]
dec_of_value [Eval]
Cast a value to a float, raise Invalid_argument if value is not a float
decimal_of_symbol [Symbol]
Return the decimal in a `DECIMAL _ symbol
decimal_of_term [Term]
Return decimal constant of a term
declarations_to_nodes [LustreDeclarations]
declare [TestgenLib]
Calls the declare field of a context on its input list of actlit / term pair.
declare_const_vars [TransSys]
declare_constant_vars [Var]
Declares constant variables as constant ufsymbols using the provided function.
declare_fun [SMTSolver]
Define uninterpreted symbol
declare_fun [SolverSig.Inst]
Declare a new function symbol
declare_init_flag_of_bounds [TransSys]
Declare the init flag of the transition system between given instants
declare_sort [SMTSolver]
Define uninterpreted sort
declare_sort [SolverSig.Inst]
Declare a new sort symbol
declare_vars [Var]
Declares non constant variables as constant ufsymbols using the provided function.
declare_vars_of_bounds [TransSys]
Declare variables of the transition system between given instants
decr [Numeral]
Decrement a numeral in a reference by one
default_log_level [Lib]
Default log level.
default_of_type [TermLib]
Return the default value of the type:
define_and_declare_of_bounds [TransSys]
Define predicates and declare constant and global state variables, declare state variables of top system between and including the given offsets
define_fun [SMTSolver]
Define uninterpreted symbol
define_fun [SolverSig.Inst]
Define a new function symbol as an abbreviation for an expression
delete_instance [SMTSolver]
Delete an instance of an SMT solver
delete_instance [SolverSig.Inst]
Delete and stops the instance of the solver
depth_input_string [Lib.ReservedIds]
Abstraction depth input string.
depth_of [TestgenTree]
Depth of the current node of a tree.
description_of_contract_testcase [TestgenLib]
Constructs the text description of a test case.
destroy_all [SMTSolver]
Destroys all live solver instances.
destruct [Term]
Flatten top node of term
destruct [Ltree.S]
Return the top symbol of a term along with its subterms
dimension_of_map [Model]
Returns the bounds / dimension of the array value represented by the map in the model
disable [Flags]
Manually disables a module.
div [Numeral]
Division
div [Decimal]
Quotient
divisible_to_mod [Term]
Convert (divisble n t) to (= 0 (mod t n))
dnf_size [Flags.C2I]
Number of disjuncts in the DNF constructed by C2I.
done_tag [Pretty]
Done tag.
drop_class_member [InvGenGraph.Graph]
Drops a term from the class corresponding to a representative.
dummy [TestgenStrategies]
First class dummy strategy module.
dummy_pos [Lib]
Dummy position different from any valid position
dump_native [NativeInput]
Dump a transition system to a file in native format
dump_native_to [NativeInput]
Dump a transition system to a given file in native format

E
elem_type_of_array [Type]
Return type of array elements
eliminate [CooperQE]
Eliminate quantifiers of a list of variables in a formula
empty [LustreContract]
Creates an empty contract.
empty [Trie.S]
The empty trie
empty_index [LustreIndex]
The empty index
empty_node [LustreNode]
Return a node of the given name and is extern flag without inputs, outputs, oracles, equations, etc.
enabled [Flags]
The modules enabled.
encode_select [Var]
encode array select operation
encode_select [StateVar]
encode array select operation.
enum_of_constr [Type]
Return the enumerated dataype to which the constructor belongs
eq [InvGenDomain.Domain]
Ordering relation.
equal [Numeral]
Equality
equal [HStringSExpr]
equal [HString]
Equality function on hashconsed strings
equal [Hashcons.HashedType]
equal [Hashcons]
equal [Decimal]
Equality
equal [LustreExpr]
Equality of expressions
equal [LustreIdent]
Equality on identifiers
equal [Trie.S]
Equality predicate on tries
equal [Term]
Equality function on terms
equal [Scope]
Equality of scopes
equal [Ltree.S]
Equality function on terms
equal [Ident]
Equality of identifiers
equal_attrs [TermAttr]
Equality function on attributes
equal_expr [LustreExpr]
Equality of expressions
equal_index [LustreIndex]
Equality of indexes
equal_scope [TransSys]
Return true if scopes of transition systems are equal
equal_state_vars [StateVar]
Equality function on state variables
equal_symbols [Symbol]
Equality function on symbols
equal_types [Type]
Equality function on types
equal_uf_symbols [UfSymbol]
Equality function on uninterpreted function symbols
equal_value [Model]
Equality over values of model
equal_vars [Var]
Equality function on variables
equalities_of [InvGenGraph.Graph]
Equalities coming from the equivalence classes of a graph.
equation_of_svar [LustreNode]
Returns the equation for a state variable if any.
error [Lib.ExitCodes]
Exit status if kid caught a signal, the signal number is added to the value
error_count [TestgenIO]
The number of errors generated.
error_msg [YicesLexer]
error_tag [Pretty]
Error tag.
escaped [HString]
eval [InvGenDomain.Domain]
Mines a transition system for candidate terms.
eval_ast_expr [LustreSimplify]
eval_ast_type [LustreSimplify]
eval_bool_ast_expr [LustreSimplify]
eval_lambda [Term]
Beta-evaluate a lambda expression
eval_lambda [Ltree.S]
Beta-evaluate a lambda expression
eval_t [Term]
Evaluate the term bottom-up and right-to-left.
eval_t [Ltree.S]
Evaluate the term bottom-up and right-to-left.
eval_term [Eval]
Evaluate a term to a value, given an assignment to all free variables
event [Debug]
exception_on_signal [Lib]
Raise exception on signal
execute_custom_check_sat_command [SMTSolver]
Execute the a custom command in place of check-sat
execute_custom_check_sat_command [SolverSig.Inst]
execute_custom_command [SMTSolver]
Execute the a custom command with the given arguments, and expect the given number of S-expressions as a result
execute_custom_command [SolverSig.Inst]
Execute a custom command and return its result
execution_path [Event]
Broadcast an execution path
exists [Trie.S]
Return true if there is a key value pair in the trie for which the given predicate evaluates to true
exists2 [Trie.S]
Check if there is a binding in the trie that satisfies the predicate
exists_node_of_name [LustreNode]
Return true if a node of the given name exists in the a list of nodes
exists_on_path [Model]
Return true if the predicate p applies at one step of the path
exit [Messaging.S]
Request the background thread of a worker process to terminate
exit [InvGen.Out]
exit [InvGen]
Temporary exit point for boolean invariant generation.
exit [Event]
Send all queued messages and exit the background thread
expr_in_context [LustreContext]
Return true if the identifier denotes an expression in the context
expr_of_ident [LustreContext]
Resolve an indentifier to an expression.
expr_of_string_sexpr [GenericSMTLIBDriver]
expr_of_string_sexpr [SMTLIBSolver.SMTLIBSolverDriver]
expr_or_lambda_of_string_sexpr [GenericSMTLIBDriver]
expr_or_lambda_of_string_sexpr [SMTLIBSolver.SMTLIBSolverDriver]
extend_contract_testcases [TestgenLib]
Extends some test cases: creates the new test cases made of the input ones extended with one transition to whatever mode they can activate.
extract [Debug]
extract [Extract]
Extract an active path from a formula and return a conjunction that is true in the model given.
extract [Flags.IC3]
Heuristic for extraction of implicants in IC3.
extract_scope_name [Lib]
Extract scope from a concatenated name

F
fail_at_position [LustreContext]
Output a fatal error at position and raise an error
fail_no_position [LustreContext]
Output a fatal error without reporting a position and raise an error
fail_on_new_definition [LustreContext]
Return a context that raises an error when defining an expression.
failure_tag [Pretty]
Failure tag.
false_of_any [Lib]
Return false
false_of_unit [Lib]
Returns false when given unit.
fec [Debug]
file_copy [Lib]
Copying file: file_copy from to copies file from to file to
file_row_col_of_pos [Lib]
Return the file, line and column of a position; fail with Invalid_argument "file_row_col_of_pos" if the position is a dummy position
files_cat_open [Lib]
fill [HString]
filter [Trie.S]
Return a trie that only contains the key value pairs that satisfy the predicate
find [Hashcons.S]
find [Trie.S]
Return the value for the key in the trie
find_main [LustreNode]
Return name of the first node annotated with --%MAIN.
find_on_path [Lib]
Return full path to executable, search PATH environment variable and current working directory
find_prefix [Trie.S]
Return the subtrie starting at the given key prefix
find_subsystem [SubSystem]
Return the subsystem of the given scope
find_subsystem_of_scope [TransSys]
Find the named subsystem
first_rep_of [InvGenDomain.Domain]
Returns true iff the input term is bottom.
fmt [InvGenDomain.Domain]
Equality over values.
fmt_as_cex_step_json [LustreContract.ModeTrace]
fmt_as_cex_step_xml [LustreContract.ModeTrace]
Formats a tree as a cex step in JSON
fmt_graph_classes_dot [InvGenGraph.Graph]
fmt_graph_dot [InvGenGraph.Graph]
Formats a graph in dot format.
fold [Hashcons.S]
fold [Hashcons]
fold f t a computes (f xN ...
fold [Trie.S]
Reduce trie to a value by applying the function to all values
fold [StateVar]
fold f a computes (f sN tN uN ... (f s2 t2 u2 (f s1 t1 u1
    a))...)
, where sI, tI and uI, respectively are the name of the state variable, its types and its associated uninterpreted function symbol.
fold2 [Trie.S]
Fold over two tries with identical keys
fold_node_calls_with_trans_sys [LustreNode]
Fold bottom-up over node calls together with the transition system
fold_subsystem_instances [TransSys]
Fold bottom-up over subsystem instances
fold_subsystems [TransSys]
Fold bottom-up over subsystems, including or excluding the top level system, without repeating subsystems already seen
fold_uf_declarations [UfSymbol]
fold_declarations f a computes (f sN aN rN ... (f s2 a2 r2 (f
    s1 a1 r1 a))...)
, where sI, aI and rI, respectively are the name of the uninterpreted symbol, the types of its arguments and the type of its value.
for_all [Trie.S]
Return true if the given predicate evaluates to true for all key value pairs in the trie
for_all2 [Trie.S]
Check if all pairs of bindings in the trie satisfy the predicate
for_all_on_path [Model]
Return true if the predicate p applies at each step of the path
for_inv_gen [StateVar]
Return true if state variable is to be used in invariant generation
found_newline [SExprLexer]
free_constant_expr_of_ident [LustreContext]
Return the free constant corresponding to an identifier if any
free_var_of_term [Term]
Return the variable of a free variable term
fresh_actlit [Actlit]
Creates a fresh actlit as a bool UF constant.
fresh_actlit_count [Actlit]
Returns the number of fresh actlits created this far.
function_of_inputs [Lib.ReservedIds]
fundef [TermAttr]
Return a fun-def attribute
fwd_prop_ind_gen [Flags.IC3]
Inductively generalize all clauses after forward propagation.
fwd_prop_non_gen [Flags.IC3]
Also propagate clauses before generalization.
fwd_prop_subsume [Flags.IC3]
Subsumption in forward propagation.

G
gen_bindings_of_string_sexpr [GenericSMTLIBDriver]
gen_bound_vars_of_string_sexpr [GenericSMTLIBDriver]
gen_expr_of_string_sexpr [GenericSMTLIBDriver]
gen_expr_of_string_sexpr' [GenericSMTLIBDriver]
gen_expr_or_lambda_of_string_sexpr [GenericSMTLIBDriver]
gen_expr_or_lambda_of_string_sexpr' [GenericSMTLIBDriver]
general_lbound [Flags.QE]
Choose lower bounds containing variables *
generalize [QE]
generalize f m evaluates the term f with the model m and returns a term g that is implied by the model m and that implies the term f with the post-state variables existentially quantified.
generalize [Type]
Generalize a type (remove actual intranges)
geq [Numeral]
Greater than or equal predicate
geq [Decimal]
Greater than or equal predicate
get [Stat]
Get the value of an integer statistics item
get [Lib]
Return the value of an option type, raise Invalid_argument "get" if the option value is None
get [HString]
get_all_abstr_types [Type]
Return abstract types that have been built
get_all_invariants [TransSys]
Returns the invariants for all (sub)systems.
get_candidate_properties [TransSys]
Return list of candidate invariants properties
get_candidates [TransSys]
Return list of candidate invariants
get_coe_in_poly [Poly]
Return the coefficient of a variable in a polynomial
get_constr_of_num [Type]
Return the constructor encoded by the numeral argument
get_float [Stat]
Get the value of a float statistics item
get_free_constants [LustreContext]
Return declared free constants
get_int_list [Stat]
Get the value of an integer statistics list
get_interpolants [SMTSolver]
get_invariants [TransSys]
Return invariants with their certificates
get_log_format [Log.Sig]
Returns the log format
get_log_level [Lib]
Gets the log level.
get_logic [TransSys]
Return the logic fragment needed to express the transition system
get_max_depth [TransSys]
get_mode_requires [TransSys]
Returns the optional assumption term and the mode requirement terms for each mode.
get_model [SMTSolver]
Return a model of the current context if satisfiable
get_model [SolverSig.Inst]
Get the assigned values of expressions in the current model
get_module [Log.Sig]
Get module currently running
get_node [LustreContext]
Return the current node in context.
get_node_function_flag [LustreContext]
Checks if the current node, if any, is a function.
get_nodes [LustreContext]
Return the nodes in the context
get_num_of_constr [Type]
Return the numeral encoding of a construcor of an enumerated datatype
get_oracle_state_var_map [LustreNode]
get_prop_status [TransSys]
Return current status of the property
get_prop_status [Property]
get_prop_status_all_nocands [TransSys]
Return current status of all properties excepted candidates
get_prop_status_all_unknown [TransSys]
Return current status of all unknown properties
get_prop_term [TransSys]
Return term of the property
get_properties [TransSys]
Returns the properties in a transition system.
get_real_properties [TransSys]
Return current status of all real (not candidate) properties
get_select_ufs [StateVar]
Return select function that were created
get_split_properties [TransSys]
Returns the list of properties in a transition system, split by their status as valid, invalid, unknown.
get_state_var_bounds [LustreContext]
Return state vars bounds hash table
get_state_var_bounds [TransSys]
Return arrays bounds of state variables of array type used in the system
get_state_var_expr_map [LustreNode]
get_state_var_instances [LustreNode]
get all instances of a state variable
get_state_var_source [LustreNode]
Get source of state variable
get_subsystem_instances [TransSys]
Return the direct subsystems of a system and their instances
get_subsystems [TransSys]
Return the direct subsystems of a system
get_uid [Analysis]
Provides a different id every time.
get_unknown_candidates [TransSys]
Return candidate invariants that have not been proved or disproved yet
get_unsat_core [SolverSig.Inst]
Get an unsatisfiable core of named expressions
get_unsat_core_lits [SMTSolver]
Interpret unsatisfiable core as literals and return as terms
get_unsat_core_of_names [SMTSolver]
Return an unsatisfiable core of named expressions if the current context is unsatisfiable
get_value [SolverSig.Inst]
Get the assigned values of expressions in the current model
get_values [TestgenLib]
Calls the checksat_getvalues field of a context on its input list of actlits.
get_var_values [SMTSolver]
Return a values of the terms in the current context if satisfiable
graph_only [Flags.Testgen]
Only generate graph of reachable modes, do not log testcases.
gt [Numeral]
Greater than predicate
gt [Decimal]
Greater than predicate
guard_flag [LustreContext]
The value of the flag indicating there are unguarded pre's in the lustre code, and we need to guard them.

H
handler_string [Lib.ReservedIds]
has_contract [LustreNode]
Return true if the node has a global or at least one mode contract
has_division_by_zero_happened [Simplify]
Returns true iff a division by zero happened in a simplification since this function was last called.
has_indexes [LustreExpr]
Returns true if the expression has index variables.
has_pre_or_arrow [LustreAst]
Returns true if the expression has a `pre` or a `->`.
has_pre_var [LustreExpr]
Return true if the expression contains a previous state variable
has_properties [TransSys]
Returns true iff sys has at least one property.
has_quantifier [Term]
Returns true if the term has quantifiers
has_quantifier [Ltree.S]
Returns true if the term has quantifiers
has_svars [InvGenGraph.Graph]
Checks whether at least one candidate mentions a state variable.
has_unguarded_pre [LustreAst]
Returns true if the expression has unguareded pre's
hash [HString]
Hashing function on hashconsed strings
hash [Hashcons.HashedType]
hash [Hashcons]
hash [LustreExpr]
Equality of expressions
hash [LustreIdent]
Hash an identifier
hash [Term]
Hashing function on terms
hash [Scope]
Hash of a scope
hash [Ltree.S]
Hash function on terms
hash_attr [TermAttr]
Hashing function on attribute
hash_of_attr [Ltree.BaseTypes]
Hash value of an attribute
hash_of_sort [Ltree.BaseTypes]
Hash value of a sort
hash_of_symbol [Ltree.BaseTypes]
Hash value of a symbol
hash_of_var [Ltree.BaseTypes]
Hash value of a variable
hash_state_var [StateVar]
Hashing function on state variables
hash_symbol [Symbol]
Hashing function on symbols
hash_type [Type]
Hashing function on types
hash_uf_symbol [UfSymbol]
Hashing function on uninterpreted function symbols
hash_var [Var]
Hashing function on variables
hashcons [Hashcons.S]
hashcons [Hashcons]
hashcons t n hash-cons the value n using table t i.e.
headers [YicesDriver]
headers [Z3Driver]
headers [GenericSMTLIBDriver]
headers [SolverDriver.S]
Solver specific headers to add at the beginning of the file
hex_code [SExprLexer]
hstring_of_free_var [Var]
Return a string for a free variable
hstring_symbol_table [GenericSMTLIBDriver]

I
ic3 [Debug]
ic3_activation_literals [Stat]
Number of activation literals
ic3_back_subsumed [Stat]
Number of backward subsumed clauses
ic3_find_cex_time [Stat]
Time spent searching counterexamples
ic3_frame_sizes [Stat]
Frame sizes in
ic3_fwd_fixpoint [Stat]
Fixpoint in forward propagation
ic3_fwd_gen_propagated [Stat]
Number of forward propagations without generalization
ic3_fwd_prop_time [Stat]
Time spent forward propagating
ic3_fwd_propagated [Stat]
Number of forward propagations
ic3_fwd_subsumed [Stat]
Number of forward subsumed clauses
ic3_generalize_time [Stat]
Time spent generalizing
ic3_ind_gen_time [Stat]
Time spent inductively generalizing counterexample
ic3_inductive_blocking_clauses [Stat]
Blocking clauses proved inductive
ic3_inductive_check_time [Stat]
Time checking inductiveness of blocking clauses
ic3_k [Stat]
Highest k reached
ic3_restarts [Stat]
Number of restarts
ic3_stale_activation_literals [Stat]
Number of permanently false activation literals
ic3_stats [Stat]
IC3 statistics
ic3_stats_title [Stat]
Title for IC3 statistics
ic3_stop_timers [Stat]
Stop and record all timers
ic3_strengthen_time [Stat]
Time spent strengthening
ic3_total_time [Stat]
Total time in IC3
ic3ia_interpolation_time [Stat]
Total time for interpolation
ic3ia_num_simulations [Stat]
Number of abstraction refinements
ic3ia_refinements [Stat]
Indices of discoveredi interpolants relative to end of frame
ic3ia_refinements_end [Stat]
Indices of discoveredi interpolants relative to end of frame
ic3ia_stats [Stat]
IC3IA statistics
ic3ia_stats_title [Stat]
Title for IC3IA statistics
id [SolverSig.Params]
id_of_clause [Clause]
Return unique identifier of clause
id_of_instance [SMTSolver]
Return the unique identifier of the solver instance
ident_of_top [LustreNode]
Return the identifier of the top node
identity [Lib]
Identity function.
ignore_or_fprintf [Lib]
Return Format.fprintf if level is is of higher or equal priority than current log level, otherwise return Format.ifprintf
ignore_sigalrm [TermLib.Signals]
Sets the handler for sigalrm to ignore.
ignore_sigint [TermLib.Signals]
Sets the handler for sigint to ignore.
ignore_sigpipe [TermLib.Signals]
Sets the handler for sigpipe to ignore.
ignore_sigquit [TermLib.Signals]
Sets the handler for sigquit to ignore.
ignore_sigterm [TermLib.Signals]
Sets the handler for sigterm to ignore.
ignoring_sigalrm [TermLib.Signals]
Runs something while ignoring sigalrm.
implem [Lib.Paths]
implem_to_rust [LustreToRust]
Compiles a lustre node to Rust as a project in the directory given as first argument.
import [HString]
Import a string from a different instance into this hashcons table
import [Var]
Import a variable from a different instance into this hashcons table
import [UfSymbol]
Import an uninterpreted symbol from a different instance into this hashcons table
import [Type]
Import a type from a different instance into this hashcons table
import [Term]
Import a term from a different instance into this hashcons table
import [Symbol]
Import symbol from a different instance into this hashcons table
import [StateVar]
Import a state variable from a different instance into this hashcons table
import [Ltree.S]
Import a term into the hashcons table by rebuilding it bottom up
import_lambda [Term]
Import a term from a different instance into this hashcons table
import_lambda [Ltree.S]
Import a lambda abstraction into the hashcons table by rebuilding it bottom up
import_sort [Ltree.BaseTypes]
import_symbol [Ltree.BaseTypes]
import_value [Model]
Import a variable assignment from a different instance
import_var [Ltree.BaseTypes]
in_automaton [LustreContext]
The value of the flag indicating we are evaluating an automaton.
incr [Stat]
Increment an integers statistics item
incr [Numeral]
Increment a numeral in a reference by one
incr_k [Compress]
incr_last [Stat]
Increment the last element of an integers statistics list
ind_compress_equal_mod_input [Stat]
Number clauses to compress inductive counterexamples
ind_compress_same_predecessors [Stat]
Number clauses to compress inductive counterexamples
ind_compress_same_successors [Stat]
Number clauses to compress inductive counterexamples
ind_k [Stat]
Highest k reached
ind_lazy_invariants_count [Stat]
Total time in BMC
ind_lazy_invariants_time [Stat]
Total time in BMC
ind_restarts [Stat]
Number of restarts
ind_stats [Stat]
Inductive step statistics
ind_stats_title [Stat]
Title for inductive step statistics
ind_stop_timers [Stat]
Stop and record all timers
ind_total_time [Stat]
Total time in BMC
index [HString]
index_from [HString]
index_ident [LustreIdent]
Identifier for index variables in arrays
index_ident_string [Lib.ReservedIds]
index_type_of_array [Type]
Return type of array index
indexes_and_var_of_select [Term]
Return the indexes and the array variable of the select operator
indexes_of_state_var [Term]
Return (array) indexes of a state variable appearing in a term
indexes_of_state_vars_in_init [LustreExpr]
indexes_of_state_vars_in_step [LustreExpr]
inductively_generalize [Flags.IC3]
Tighten blocking clauses to an unsatisfiable core.
info_clone [Analysis]
info_of_param [Analysis]
The info or a param.
init [Compress]
Initialize compression
init_base [TransSys]
Offset of the current state variables in initial state constraint
init_flag_ident [LustreIdent]
Identifier for first instant flag
init_flag_ident_string [Lib.ReservedIds]
Observer for contract requirements.
init_flag_of_bound [TransSys]
Return the init flag at the given bound
init_flag_state_var [TransSys]
Return the state variable for the init flag
init_flag_string [Lib.ReservedIds]
Init flag string.
init_formals [TransSys]
Variables in the initial state constraint
init_fun_of [TransSys]
Builds a call to the initial function on state k.
init_im [Messaging.S]
Create a messaging context and bind ports for the invariant manager.
init_of_bound [TransSys]
Close the initial state constraint by binding all instance identifiers, and bump the state variable offsets to be at the given bound
init_trans_open [TransSys]
Return the instance variables of this transition system, the initial state constraint at init_base and the transition relation at trans_base with the instance variables free.
init_uf_string [Lib.ReservedIds]
Transition relation.
init_uf_symbol [TransSys]
Predicate for the initial state constraint
init_worker [Messaging.S]
Create a messaging context and bind given ports for a worker process.
inline [Flags.Arrays]
Inline arrays with fixed bounds
input_file [Flags.Interpreter]
Read input from file.
input_file [Flags]
Input file
input_format [Flags]
inst_ident [LustreIdent]
Identifier for instantiated variables in node calls
inst_ident_string [Lib.ReservedIds]
Initial predicate.
instance_ident [LustreIdent]
Identifier for unique identifier for node instance
instance_ident_string [Lib.ReservedIds]
First instant flag.
instantiate [Ltree.S]
instantiate_term_all_levels [TransSys]
Instantiate a term of a given scope from all instances of the system of that scope upwards to the top system
instantiate_term_cert_all_levels [TransSys]
Same as above but with certificates
int_cube_size [Flags.C2I]
Number of int cubes in the DNF constructed by C2I.
int_of_index_var [LustreExpr]
Return the number/position of the index variable.
int_of_kind_module [Lib]
String representation of a process type
int_of_log_level [Lib]
Associate an integer with each level to induce a total ordering
int_of_yices_id [YicesResponse]
interpr_type [YicesDriver]
interpr_type [GenericSMTLIBDriver]
interpr_type [SolverDriver.S]
Can interpret type in a supported sort.
interruption_tag [Pretty]
Interruption tag.
inv_log_contract_name [Lib.Names]
inv_log_file [Lib.Names]
Contract name for invariant logging.
invariant [Event]
Broadcast a discovered top level invariant
invars_of_bound [TransSys]
Instantiate invariants and valid properties to the bound
invgen_enabled [Flags]
Returns the invariant generation techniques currently enabled.
invgencand [Debug]
invgengraph_os_candidate_term_count [Stat]
Total number of candidate terms.
invgengraph_os_graph_rewriting_time [Stat]
Time spent rewriting graphs.
invgengraph_os_implication_count [Stat]
Total number of invariants discovered by invariant generation which were implications.
invgengraph_os_invariant_count [Stat]
Total number of invariants discovered by invariant generation for all systems.
invgengraph_os_k [Stat]
Hightest k reached.
invgengraph_os_stats [Stat]
All INVGENOS statistics
invgengraph_os_stats_title [Stat]
Title for INVGENOS statistics
invgengraph_os_stop_timers [Stat]
Stop and record all timers
invgengraph_os_total_time [Stat]
Time spent rewriting graphs.
invgengraph_ts_candidate_term_count [Stat]
Total number of candidate terms.
invgengraph_ts_graph_rewriting_time [Stat]
Time spent rewriting graphs.
invgengraph_ts_implication_count [Stat]
Total number of invariants discovered by invariant generation which were implications.
invgengraph_ts_invariant_count [Stat]
Total number of invariants discovered by invariant generation for all systems.
invgengraph_ts_k [Stat]
Hightest k reached.
invgengraph_ts_stats [Stat]
All INVGENTS statistics
invgengraph_ts_stats_title [Stat]
Title for INVGENTS statistics
invgengraph_ts_stop_timers [Stat]
Stop and record all timers
invgengraph_ts_total_time [Stat]
Time spent rewriting graphs.
is_abstr [Type]
Return true if the type is abstract
is_active [PostAnalysis.PostAnalysis]
Performs the treatment.
is_array [Type]
Return true if the type is an array type
is_atom [Term]
Return true if the term is a simple Boolean atom, that is, has type Boolean and does not contain subterms of type Boolean
is_automaton_state_var [LustreNode]
Return the automaton to which the state variable belongs if any
is_bool [Type]
Return true if the type is the Boolean type
is_bool [Term]
Return true if the term is a Boolean constant
is_bool [Symbol]
Return true if the symbol is `TRUE or `FALSE
is_bot [InvGenDomain.Domain]
Returns true iff the input term is top.
is_bound_var [Term]
Return true if the term is a bound variable
is_candidate [TransSys]
Return true if the property is a candidate invariant
is_const [LustreExpr]
Return true if the expression is constant
is_const [StateVar]
Return true if the state variable is constant
is_const_expr [LustreExpr]
Return true if the expression is constant
is_const_state_var [Var]
Return true if the variable is a constant state variable
is_const_var [LustreExpr]
Return true if expression is a constant state variable
is_decimal [Term]
Return true if the term is a decimal constant
is_decimal [Symbol]
Return true if the symbol is a decimal
is_disproved [TransSys]
Return true if the property is proved not invariant
is_dummy_pos [Lib]
Return true if the position is not a valid position in the input
is_empty [Trie.S]
Return true if the trie is empty
is_enum [Type]
Return true if the type is an integer range type
is_exists [Term]
Return true if the term is an existential quantifier
is_forall [Term]
Return true if the term is a universal quantifier
is_free_var [Var]
Return true if the variable is a free variable
is_free_var [Term]
Return true if the term is a free variable
is_fundef [TermAttr]
Return true if the attribute is a name
is_input [StateVar]
Return true if the state variable is an input
is_int [Decimal]
Return true if decimal coincides with an integer
is_int [Type]
Return true if the type is the integer type
is_int_range [Type]
Return true if the type is an integer range type
is_inv [TransSys]
Returns true if the input term is a known invariant of the system.
is_lambda_identity [Term]
Returns true if the lamda expression is the identity, i.e.
is_leaf [Term]
Return true if the term is a leaf symbol
is_let [Term]
Return true if the term is a let binding
is_lustre_input [InputSystem]
is_named [Term]
Return true if the term is a named term
is_named [TermAttr]
Return true if the attribute is a name
is_negated [Term]
Return true if the top symbol of the term is a negation
is_node [Term]
Return true if the term is a function application
is_numeral [LustreExpr]
is_numeral [Term]
Return true if the term is an integer constant
is_numeral [Symbol]
Return true if the symbol is a numeral
is_os_running [InvGenDomain.Domain]
is_pre_var [LustreExpr]
Return true if expression is a previous state variable
is_proved [TransSys]
Return true if the property is proved invariant
is_real [Type]
Return true if the type is the real type
is_select [LustreExpr]
Returns true if the expression is a selection in an array
is_select [Term]
Return true if the term is an application of the select operator
is_select [Symbol]
Return true if the symbol is select from array
is_select_array_var [LustreExpr]
Returns true if the expression is a selection of an array variable
is_select_hstring [GenericSMTLIBDriver]
is_stale [InvGenGraph.Graph]
Returns true if all classes in the graph only have one candidate term.
is_state_var_instance [Var]
Return true if the variable is an instance of a state variable
is_store [LustreExpr]
Returns true if this is a store in an array
is_store [Term]
Return true if the term is an application of the store operator
is_subsumed [Trie.S]
Return true if there is a key in the trie such that all elements of that key are in the given key.
is_top [InvGenDomain.Domain]
Returns true iff the one state invgen technique for this domain is running.
is_true_expr [LustreExpr]
Returns true iff the expr is the constant true.
is_uf [Symbol]
Return true if the symbol is uninterpreted
is_var [LustreExpr]
Return true if expression is a current state variable
iter [HString]
iter [Hashcons.S]
iter [Hashcons]
iter f t iterates f over all elements of t.
iter [Trie.S]
Apply unit-valued function to each value in trie
iter [StateVar]
iter f calls f s t u for every state variable with s being the name of the variable, t its type and u its associated uninterpreted function symbol.
iter2 [Trie.S]
Iterate over two tries with identical keys
iter_subsystems [TransSys]
Iterate bottom-up over subsystems, including the top level system without repeating subsystems already seen
iter_uf_declarations [UfSymbol]
iter_declarations f t iterates f over all declarations, calling f s a r on each, where s, a and r, respectively are the name of the uninterpreted symbol, the types of its arguments and the type of its value.
iteri [HString]

J
jkind_bin [Flags.Certif]
Binary for JKind

K
keys [Trie.S]
Return the keys in the trie
keywords [YicesLexer]
kid_status [Lib.ExitCodes]
kill_base [LockStepDriver]
Kills a base checker.
kill_pruning [LockStepDriver]
Kills a pruning checker.
kill_step [LockStepDriver]
Kills a step checker.
kind [SMTSolver]
kind2 [Debug]
kind_module_of_string [Lib]
Kind module of a string

L
l_fold [Res]
Fold over a list of results.
l_iter [Res]
Iterate over a list with a result-producing function.
l_map [Res]
Map over a list with a result-producing function.
lambda_of_string_sexpr [CVC4Driver]
last_elem_type_of_array [Type]
Return all array index types of a nested array type
lazy_invariants [Flags.BmcKind]
Lazy assertion of invariants.
leaf_of_term [Term]
Return the symbol of a leaf term
len [Flags.Testgen]
Length of the test case generated.
length [HString]
length_of_cex [Property]
length_of_clause [Clause]
Return the number of literals in the clause
leq [Numeral]
Less than or equal predicate
leq [Decimal]
Less than or equal predicate
lexbuf_init [LustreLexer]
Initialize the lexing function
lexeme_len [SExprLexer]
lf [SExprLexer]
lift_candidates [Flags.Invgen]
InvGen will lift candidate terms from subsystems.
list_diff_uniq [Lib]
From two sorted lists without physical duplicates return a sorted list without physical duplicates containing elements in the first but not in the second list
list_eq [TestgenLib]
Compares two lists using physical equality.
list_extract_nth [Lib]
Remove and returns the nth element form a list
list_filter_nth [Lib]
list_filter_nth l [p1; p2; ...] returns the elements l at positions p1, p2 etc.
list_index [Lib]
Return the index of the first element that satisfies the predicate p, raise excpetion Not_found if no element satisfies the predicate.
list_indexes [Lib]
list_indexes l1 l2 returns the indexes in list l2 of elements in list l1
list_init [Lib]
Creates a size-n list equal to f 0; f 1; ... ; f (n-1)
list_inter_uniq [Lib]
From two sorted lists without physical duplicates return a sorted list without physical duplicates containing elements in both lists
list_join [Lib]
Given two ordered association lists with identical keys, push the values of each element of the first association list to the list of elements of the second association list.
list_max [Lib]
Returns the maximum element of a non-empty list
list_merge_uniq [Lib]
Merge two sorted lists without physical duplicates to a sorted list without physical duplicates
list_subset_uniq [Lib]
For two sorted lists without physical duplicates return true if the first list contains a physically equal element for each element in the second list
list_subtract [Lib]
Return a list containing all values in the first list that are not in the second list
list_uniq [Lib]
From a sorted list return a list with physical duplicates removed
literals_of_clause [Clause]
Return the literals in the clause
log [Log.SLog]
log m l f v ... outputs a message from module m on level l, formatted with the parameterized string f and the values v ...
log_analysis_end [Event]
Logs the end of an analysis.
log_analysis_start [Event]
Logs the start of an analysis.
log_deadlock [TestgenIO]
log_deadlock t modes model k logs a deadlock trace of length k represented by model model and activating modes modes using the info in t.
log_disproved [Event]
Log a disproved property
log_format_xml [Flags]
Output in XML format
log_interruption [Event]
Logs an interruption for some signal.
log_invs [Flags]
Minimizes and logs invariants as contracts.
log_level [Flags]
Verbosity level
log_level_of_int [Lib]
log_post_analysis_end [Event]
Logs the end of a post-analysis treatment.
log_post_analysis_start [Event]
Logs the start of a post-analysis treatment.
log_ppf [Lib]
Current formatter for output
log_prefix [TestgenDF]
Prefix for logging testgen related things.
log_prop_status [Event]
Log summary of status of properties
log_proved [Event]
Log a proved property
log_run_end [Event]
Logs the end of a run.
log_stat [Event]
Log statistics
log_step_cex [Event]
Logs a step counterexample.
log_test_glue_file [TestgenIO]
Logs the top level XML glue file.
log_test_glue_file [TestgenDF]
Logs the top level XML glue file.
log_testcase [TestgenIO]
log_testcase t modes model k logs a test case of length k represented by model model and activating modes modes using the info in t.
log_timeout [Event]
Logs a timeout.
log_to_file [Lib]
Ouputs all log messages to the given file
log_to_stdout [Lib]
Write all log messages to the standard output
log_trust [Flags.Certif]
Log trusted parts of proofs.
log_uncond [Log.SLog]
log_uncond m f v ... outputs a message from module m unconditionally, formatted with the parameterized string f and the values v ...
logic [SolverSig.Params]
logic [Flags.Smt]
Logic to send to the SMT solver
logic_allow_arrays [TermLib]
Returns true if the logic potentially has arrays
logic_of_sort [TermLib]
Returns the logic fragment of a type
logic_of_term [TermLib]
Returns the logic fragment used by a term
lowercase [HString]
lt [Numeral]
Less than predicate
lt [Decimal]
Less than predicate
ltree [Debug]
lus_compile [Flags]
Activates compilation to Rust.
lus_main [Flags]
Main node in Lustre file
lus_strict [Flags]
Strict Lustre mode.

M
main [TestgenDF]
Entry point.
main [SExprLexer]
main [LustreParser]
main [Interpreter]
Entry point
main [InvGen.Out]
Runs the invariant generator.
main [IC3]
Entry point
main [Step]
Runs the step instance.
main [Base]
Runs the base instance.
main [Kind2]
main [InvarManager]
Entry point.
main_bool [InvGen]
Temporary entry point for boolean invariant generation.
main_failure [SExprLexer]
main_int [InvGen]
Temporary entry point for integer invariant generation.
main_real [InvGen]
Temporary entry point for real invariant generation.
make [HString]
map [Res]
Maps a function to a result if it's Ok.
map [HString]
map [LustreExpr]
Tail-recursive bottom-up right-to-left map on the expression
map [Trie.S]
Return a new trie with the function applied to the values
map [Term]
Tail-recursive bottom-up right-to-left map on the term
map [Ltree.S]
Tail-recursive bottom-up right-to-left map on the term
map2 [Trie.S]
Map over two tries with identical keys
map_cex_prop_to_subsystem [TransSys]
map_err [Res]
Maps a function to a result if it's Err.
map_res [Res]
Maps functions to Ok or Err.
map_state_var [Var]
Return a new variable with the state variable replaced
map_state_vars [Term]
Return a new term with each state variable replaced
map_svars_in_equation [LustreNode]
Replace state variables in equation
map_vars [LustreExpr]
Replace state variables in expression
map_vars [Term]
Return a new term with each variable instance replaced
map_vars_expr [LustreExpr]
Replace state variables in internal expression
mapi [Trie.S]
Return a new trie with the function applied to the values
max [Numeral]
Return greater of two numerals
max [Flags.BmcKind]
Maximal number of iterations in BMC.
max_binding [Trie.S]
max_depth [Flags.Invgen]
max_depth_input_string [Lib.ReservedIds]
Suffix used for the name of the function encoding functional systems.
max_succ [Flags.Invgen]
Number of unrollings invariant generation should perform between switching to a different systems.
maximal_abstraction_for_testgen [InputSystem]
Returns the analysis param for top that abstracts all its abstractable subsystems if top has a contract.
mem [Trie.S]
Return true if there is a value for the key in the trie
mem_prefix [Trie.S]
Return true if there is a subtrie starting at the given key prefix
merge [Certificate]
Merge certificates into one.
merge [Trie.S]
merge [Model]
Combine assignments of two models into one.
message_of_strings [Messaging.RelayMessage]
Convert a message to a strings for message frames
messaging [Debug]
min [Numeral]
Return smaller of two numerals
min_binding [Trie.S]
mine [InvGenGraph.Graph]
Mines a system and creates the relevant graphs.
mine [InvGenDomain.Domain]
Representative of the first equivalence class.
mine [InvGenMiner.CandGen]
Generates sets of candidate terms from a transition system, and its subsystems if the second flag require it.
mine_trans [Flags.Invgen]
InvGen will look for candidate terms in the transition predicate.
mininvs [Flags.Certif]
Minimization stragegy for invariants
minisleep [Lib]
Sleep for seconds, resolution is in ms
mink [Flags.Certif]
Minimization stragegy for k
misc_stats [Stat]
General statistics
misc_stats_title [Stat]
Title of the general statistics section
misc_stop_timers [Stat]
Stop and record all timers
mk [TestgenTree]
Creates a reversed partial tree.
mk [TestgenSolver]
Creates a new solver wrapper.
mk [TestgenIO]
mk [LustreContract]
Creates a new contract from a set of assumes, a set of guarantess, and a list of modes.
mk [InvGenGraph.Graph]
Creates a graph from a single equivalence class and its representative.
mk_abs [Term]
Create an absolute value
mk_abstr [Type]
Return an abstract type
mk_and [LustreExpr]
Return the Boolean conjunction of the two expressions.
mk_and [Term]
Create an Boolean conjunction
mk_and_n [LustreExpr]
Return the Boolean conjunction of the list of expressions.
mk_annot [Ltree.S]
Constructor for an annotated term
mk_app [Term]
Create a function application of a hashconsed symbol
mk_app [Ltree.S]
Constructor for a function application
mk_app_of_symbol_node [Term]
Create a function application
mk_array [LustreExpr]
mk_array [Type]
Return an array type of index sort and element sort
mk_arrow [LustreExpr]
Apply the followed by operator -> to the two expressions.
mk_base_checker [LockStepDriver]
Creates a base checker for some system at some depth.
mk_bool [Type]
Return the boolean type
mk_bool [Term]
Create the propositional constant true or false
mk_clause_of_literals [Clause]
Create a clause from a set of literals
mk_cmp [InvGenDomain.Domain]
Evaluates a term.
mk_const [Term]
Create constant of a hashconsed symbol
mk_const [Ltree.S]
Constructor for a constant
mk_const_of_symbol_node [Term]
Create a constant
mk_const_state_var [Var]
Return a constant state variable.
mk_constr [LustreExpr]
Return a constructor
mk_constr [Term]
Create a constructor encoded as a numeral
mk_context [TestgenLib]
Construction helper for context.
mk_context [TestgenStrategies.Sig]
Creates a context for this strategy.
mk_dec [Term]
Create a floating point decimal
mk_depth_input [StateVar]
Creates a scoped depth input.
mk_dir [Lib]
mk_distinct [Term]
Create an pairwise distinct predicate
mk_div [LustreExpr]
Return the quotient of the two expressions.
mk_div [Term]
Create a real quotient
mk_divisible [Term]
Create a predicate for divisibility by a constant integer
mk_empty_context [LustreContext]
Create an initial empty context.
mk_enum [Type]
Return an enumerated datatype type
mk_eq [LustreExpr]
Return the equality relation on the two expressions.
mk_eq [InvGenDomain.Domain]
Creates the term corresponding to the ordering of two terms.
mk_eq [Term]
Create an equality
mk_exists [LustreExpr]
Return the existential quantification of an expression.
mk_exists [Term]
Return a hashconsed existentially quantified term
mk_exists [Ltree.S]
Constructor for an existential quantification over an indexed free variable
mk_false [Term]
Create the propositional constant false
mk_forall [LustreExpr]
Return the universal quantification of an expression.
mk_forall [Term]
Return a hashconsed universally quantified term
mk_forall [Ltree.S]
Constructor for a universal quantification over an indexed free variable
mk_free_var [LustreExpr]
mk_free_var [Var]
Return a free variable
mk_fresh_local [LustreContext]
Create a fresh local state variable in the context.
mk_fresh_oracle [LustreContext]
Create a fresh oracle state variable in the context.
mk_fresh_oracle_for_state_var [LustreContext]
Create a fresh oracle state variable for the pre-initial value of the given state variable in the context, or return a previously created oracle for this state variable.
mk_fresh_uf_symbol [UfSymbol]
Return a fresh uninterpreted symbol
mk_fresh_var [Var]
Return a fresh free variable
mk_fresh_var [Ltree.BaseTypes]
mk_geq [Term]
Create a greater-or-equal predicate
mk_gt [LustreExpr]
Return the greater-than relation on the two expressions.
mk_gt [Term]
Create a greater-than predicate
mk_gte [LustreExpr]
Return the greater-than-or-equal relation on the two expressions.
mk_hstring [HString]
Hashcons a string
mk_impl [LustreExpr]
Return the Boolean implication of the two expressions.
mk_implies [Term]
Create a Boolean implication
mk_index_var [LustreExpr]
Return an expression for the i-th index variable.
mk_init_flag [StateVar]
Creates a scoped init flag.
mk_int [LustreExpr]
Return an expression of an integer numeral.
mk_int [Type]
Return the integer type
mk_int_expr [LustreExpr]
Return an expression of a numeral
mk_int_range [Type]
Return the integer range type
mk_intdiv [LustreExpr]
Return the integer quotient of the two expressions.
mk_intdiv [Term]
Create an integer quotient
mk_is_int [Term]
Create a predicate for coincidence of a real with an integer
mk_ite [LustreExpr]
Return an if-then-else expression.
mk_ite [Term]
Create an if-then-else term
mk_lambda [Term]
Create a hashconsed lambda expression
mk_lambda [Ltree.S]
Constructor for a lambda expression
mk_leq [Term]
Create a less-or-equal predicate
mk_let [LustreExpr]
mk_let [Term]
Create a binding of symbols to terms
mk_let [Ltree.S]
Constructor for a let binding
mk_let_cur [LustreExpr]
Substitute state variable at current instant with expression
mk_let_elim [Ltree.S]
Constructor for a let binding
mk_let_pre [LustreExpr]
Substitute state variable at previous instant with expression
mk_local_for_expr [LustreContext]
Define the expression with a fresh state variable, or the variable previously used for the same expression (if the optinal argument reuse is set to true), record the definition in the context and return the context.
mk_lt [LustreExpr]
Return the less-than relation on the two expressions.
mk_lt [Term]
Create a less-than predicate
mk_lte [LustreExpr]
Return the less-than-or-equal relation on the two expressions.
mk_max_depth_input [StateVar]
Creates a scoped depth input.
mk_minus [LustreExpr]
Return the difference of the two expressions.
mk_minus [Term]
Create an integer or real difference
mk_minus_simplify [Term]
mk_mod [LustreExpr]
Return the integer modulus of the two expressions.
mk_mod [Term]
Create an integer modulus
mk_mode [LustreContract]
mk_named [Term]
Uniquely name a term with an integer and return a named term and its name
mk_named [TermAttr]
Return a name attribute
mk_named_unsafe [Term]
Name term with the given integer in a given namespace
mk_neq [LustreExpr]
Return the disequality relation on the two expressions.
mk_not [LustreExpr]
Return the Boolean negation of the expression.
mk_not [Term]
Create an Boolean negation
mk_num [Term]
Create an integer numeral
mk_num_of_int [Term]
Create an integer numeral
mk_of_expr [LustreExpr]
Return an expression with the same term on both sides of the ->
mk_or [LustreExpr]
Return the Boolean disjunction of the two expressions.
mk_or [Term]
Create an Boolean disjunction
mk_or_n [LustreExpr]
Return the Boolean disjunction of the list of expressions.
mk_plus [LustreExpr]
Return the sum of the two expressions.
mk_plus [Term]
Create an integer or real sum
mk_pre [LustreExpr]
Apply the pre operator to the expression, abstract the expression to a fresh variable if it is not a variable at the current state.
mk_pred [Term]
Decrement integer or real term by one
mk_pruning_checker [LockStepDriver]
Creates a pruning checker for a system.
mk_real [LustreExpr]
Return an expression of a floating point decimal.
mk_real [Type]
Return the real decimal type
mk_result [Analysis]
Returns a result from an analysis.
mk_results [Analysis]
Creates a new results.
mk_scope [Scope]
Construct a scope from a list of identifiers
mk_select [LustreExpr]
Select from an array
mk_select [Term]
Create select from an array at a particular index
mk_state_var [LustreContext]
mk_state_var [StateVar]
mk_state_var n s t declares a state variable of name n with scope s, and type t.
mk_state_var_instance [Var]
Return an instance of a state variable.
mk_store [LustreExpr]
Store in an array
mk_store [Term]
Functionnaly update an array at a given index
mk_string_ident [LustreIdent]
Construct an identifier of a string
mk_succ [Term]
Increment integer or real term by one
mk_svar [LustreContract]
Creates a svar.
mk_symbol [Symbol]
Create a symbol
mk_term [Term]
Create a hashconsed term
mk_term [Ltree.S]
Constructor for a term
mk_times [LustreExpr]
Return the product of the two expressions.
mk_times [Term]
Create an integer or real product
mk_to_int [LustreExpr]
Return a conversion to an integer numeral.
mk_to_int [Term]
Create a conversion to an integer numeral
mk_to_real [LustreExpr]
Return a conversion to a floating-point decimal.
mk_to_real [Term]
Create a conversion to a real decimal
mk_trans_sys [TransSys]
mk_true [Term]
Create the propositional constant true
mk_type [Type]
Hashcons a type
mk_uf [Term]
Create an uninterpreted constant or function
mk_uf_symbol [UfSymbol]
Declare an uninterpreted symbol
mk_uminus [LustreExpr]
Return the unary minus of the expression.
mk_var [LustreExpr]
Return an expression of a variable.
mk_var [Term]
Create a symbol to be bound to a term
mk_var [Ltree.S]
Constructor for a free variable with indexes
mk_xor [LustreExpr]
Return the Boolean exclusive disjunction of the two expressions.
mk_xor [Term]
Create an Boolean exclusive disjunction
mod_to_divisible [Term]
Convert (= 0 (mod t n)) to (divisble n t)
mode_path_of [TestgenTree]
Returns the list of mode conjunctions corresponding to a partial tree.
mode_paths_to_tree [LustreContract.ModeTrace]
Turns a trace of lists of mode paths into a trace of trees.
mode_trace_to_tree [LustreContract.ModeTrace]
Formats a tree as a cex step in xml.
model_at_k_of_path [Model]
Extract values at instant k from the path and return a model
models_of_path [Model]
Return a list of models, one for each step on the path
modes [Flags.C2I]
Whether mode sub candidate is activated in c2i.
modes_of [TestgenModes]
modes_of_sys [TestgenModes]
modular [Flags]
Modular analysis.
monolithic [Strategy]
Works almost the same as next_analysis, but returns a single analysis parameter for a monolithic analysis.
mult [Numeral]
Product
mult [Decimal]
Product
multiply_two_polys [Poly]
Multiply two polynomials, one of them must be constant

N
name [TestgenStrategies.Sig]
Name of the strategy, for logging.
name [InvGenDomain.Domain]
Short string description of the values, used in the logging prefix.
name [PostAnalysis.PostAnalysis]
Name of the treatment.
name_of_enum [Type]
Return the name of an enumerated datatype encoded as int ranges
name_of_named [Term]
Return the name of a named term
name_of_node [LustreNode]
Return the name of the node
name_of_state_var [StateVar]
Return the name of the state variable
name_of_uf_symbol [UfSymbol]
Return the name of the uninterpreted function symbol
named_of_attr [TermAttr]
Return the name in a name attribute, raises Invalid_argument for other attributes
native [Debug]
neg [Numeral]
Unary negation
neg [Decimal]
Unary negation
negate [Term]
Negate term, avoiding double negation
negate_poly [Poly]
Negate a polynomial
negate_simplify [Term]
Negates a term by modifying the top node if it is a not, true, false, or an arithmetic inequality.
newline [YicesLexer]
next_analysis [Strategy]
Takes some results and some information about (sub)systems, and returns the next analysis to perform, if any.
next_analysis_of_strategy [InputSystem]
Return the next system to analyze and the systems to abstract
no_stuttering [TestgenStrategies.Sig]
Returns true if the strategy requires succeeding input tuples to be different.
node_args_of_term [Term]
Return the arguments of a function application
node_call_of_svar [LustreNode]
Returns the node call the svar is (one of) the output(s) of, if any.
node_in_context [LustreContext]
Return true if the identifier denotes a node in the context
node_is_abstract [LustreSlicing]
Return true if the node is flagged as abstract in abstraction_map.
node_is_state_handler [LustreNode]
Return the state that is handled by the node if any.
node_is_visible [LustreNode]
Return true if the node should be visible to the user, false if it was created internally.
node_item_has_pre_or_arrow [LustreAst]
Checks whether a node equation has a `pre` or a `->`.
node_local_decl_has_pre_or_arrow [LustreAst]
Checks whether a node local declaration has a `pre` or a `->`.
node_of_lambda [Ltree.S]
Return the node of a hashconsed lamda abstraction
node_of_name [LustreContext]
Return the node of the given name from the context
node_of_name [LustreNode]
Return the node of the given name from a list of nodes
node_of_symbol [Symbol]
Return the node of the hashconsed symbol
node_of_t [Ltree.S]
Return the node of a hashconsed term
node_of_term [Term]
Return the node of the hashconsed term
node_of_type [Type]
Return the value Type.kindtype in a hashconsed type
node_symbol_of_term [Term]
Return the symbol of a function application
nodes_of_subsystem [LustreNode]
Return list of topologically ordered list of nodes from subsystem.
none_of_unit [Lib]
Returns None when given unit.
note_tag [Pretty]
Note tag.
nu_query_step [LockStepDriver]
Queries step, returns an option of the model.
num_of_value [Eval]
Cast a value to an integer, raise Invalid_argument if value is not an integer
numeral_of_expr [LustreExpr]
numeral_of_symbol [Symbol]
Return the numeral in a `NUMERAL _ symbol
numeral_of_term [Term]
Return integer constant of a term
nums_to_pos_nums [Term]
Convert negative numerals and decimals to negations of their absolute value

O
of_big_int [Numeral]
Convert an arbitrary large integer numeral to numeral
of_big_int [Decimal]
Convert an arbitrary large integer to a rational
of_channel [NativeInput]
Parse from the channel
of_file [NativeInput]
Parse from the file
of_file [LustreInput]
Parse from the file, return an input system for further slicing and refinement from analysis strategies.
of_int [Numeral]
Convert an integer to a numeral
of_int [Decimal]
Convert an integer to a rational
of_list [Model]
Create a model of an association list
of_num [Decimal]
Convert an ocaml Num to a rational
of_scope [LustreIdent]
Construct an identifier of a scope
of_string [Numeral]
Convert a string to numeral
of_string [Decimal]
Convert a string in floating-point notation 1.2E3 to rational number
of_string [Ident]
Construct an identifier from a string
offset_of_state_var_instance [Var]
Return the offset of a state variable instance
on_exit [TestgenDF]
Clean exit.
on_exit [Interpreter]
Cleanup before exit
on_exit [QE]
Cleanup before exit
on_exit [IC3]
Cleanup before exit
on_exit [Step]
on_exit [Base]
on_exit [InvarManager]
Cleanup before exit
one [Numeral]
The numeral one
one [Decimal]
The rational number one
one_expr [LustreParser]
only_user_candidates [Flags.Certif]
oracle [Lib.Paths]
Rust generation path.
oracle_ident [LustreIdent]
Identifier for oracle inputs
oracle_ident_string [Lib.ReservedIds]
Unique identifier for node instance.
oracle_to_rust [LustreToRust]
Compiles a lustre node as an oracle.
order_equations [LustreSlicing]
Return equations of node in topological order of their dependencies
order_var_by_elim [Flags.QE]
Order variables in polynomials by order of elimination *
ordered_equations_of_node [LustreNode]
ordered_equations_of_node n stateful init Returns the equations of n, topologically sorted by their base (step) expression if init (not init).
ordered_scopes_of [InputSystem]
Returns the scopes of all the systems in an input systems, in topological order.
out_dir [TestgenStrategies.Sig]
output_dir [Flags]
Output directory for the files Kind 2 generates.
output_on_level [Lib]
Return true if given log level is of higher or equal priority than current log level?
outputs_of_current_node [LustreContext]
The output state variables of the current node.

P
package_name [Version]
Name of the program
package_name [Kind2Config]
package_version [Kind2Config]
param_assumptions_of_scope [Analysis]
Retrieve the assumptions of a scope from a param.
param_clone [Analysis]
param_scope_is_abstract [Analysis]
Return true if a scope is flagged as abstract in the abstraction_map of a param.
paren_string_of_string_list [Lib]
Return the strings as a parenthesized and space separated list
parse [Debug]
parse_log_json [Log.Sig]
parse_log_xml [Log.Sig]
partial_eval_lambda [Term]
Partialy Beta-evaluate a lambda expression
partial_eval_lambda [Ltree.S]
Partialy Beta-evaluate a lambda expression
partial_selects [Term]
Use fresh function symbols to encode partial select applications and add constraint that forall i, fresh a i = select a i, returns the modified term and the list of new fresh symbols to declare.
path_from_model [Model]
Convert a model to a path
path_length [Model]
Return the length of the value paths
path_of [TestgenTree]
Returns the term encoding the path of modes represented by a tree.
path_of_list [Model]
Create a model of an association list
path_of_term_list [Model]
Create a model of an association list
path_offset [Model]
Offset of the variables at each step of a path.
path_to_list [Model]
Return an association list with the assignments in the model
poly_is_constant [Poly]
Return true when the polynomial is a constant, false otherwise
pop [TestgenTree]
Pops the current node.
pop [SMTSolver]
Pop one scope from the context stack
pop [SolverSig.Inst]
Pop a number of assertion sets from the stack
pop_contract_scope [LustreContext]
Remove topmost contract scope from context
pop_scope [LustreContext]
Remove topmost scope from context
pos_of_expr [LustreAst]
Returns the position of an expression
pos_of_file_row_col [Lib]
position_of_lexing [Lib]
Convert a position of the lexer to a position
pp_print_array_slice [LustreAst]
pp_print_arrayi [Lib]
Pretty-print an array with given separator
pp_print_atom [SExprBase.SExprAtom]
pp_print_atom [HStringSExpr.HStringAtom]
pp_print_attr [TermAttr]
Pretty-print a hashconsed attribute
pp_print_attr [Ltree.BaseTypes]
Pretty-print an attribute
pp_print_banner [Lib]
Output the banner on the formatter
pp_print_bmc_stats [Stat]
Print statistics for BMC
pp_print_c2i_stats [Stat]
Pretty-print C2I statistics items
pp_print_call [LustreNode]
Pretty-print a node call in Lustre format
pp_print_certif_stats [Stat]
Print statistics for certificate
pp_print_cformula [Poly]
Print a cformula
pp_print_clock_expr [LustreAst]
pp_print_clocked_typed_ident [LustreAst]
pp_print_const_clocked_typed_ident [LustreAst]
pp_print_const_decl [LustreAst]
pp_print_contract [LustreContract]
Pretty prints a contract.
pp_print_contract_item [LustreAst]
pp_print_contract_node [LustreAst]
pp_print_contract_testcase [TestgenLib]
Pretty prints a test case.
pp_print_contract_testcase_named [TestgenLib]
Pretty prints a test case with the name of the modes it triggers.
pp_print_contract_testcases [TestgenLib]
Pretty prints a list of test cases.
pp_print_contract_testcases_named [TestgenLib]
Pretty prints a list of test cases with the name of the modes they trigger.
pp_print_custom_arg [SMTExpr.Conv]
Pretty-print a custom argument
pp_print_decimal [Decimal]
Pretty-print a rational
pp_print_decimal_as_float [Decimal]
Pretty-print a rational as an f64 (used by compilation to Rust)
pp_print_decimal_as_lus_real [Decimal]
Pretty-print a rational as an f64 (used by contract generation)
pp_print_decimal_sexpr [Decimal]
Pretty-print a rational as an S-expression
pp_print_declaration [LustreAst]
pp_print_event [Event]
Pretty-print an event
pp_print_expr [YicesDriver]
pp_print_expr [GenericSMTLIBDriver]
pp_print_expr [SolverDriver.S]
Pretty-print an expression
pp_print_expr [SMTExpr.Conv]
Pretty-print a term in SMTLIB format
pp_print_expr [LustreExpr]
Pretty-print a Lustre expression.
pp_print_expr [LustreAst]
pp_print_field_assign [LustreAst]
pp_print_hstring [HString]
Pretty-print a hashconsed string
pp_print_ic3_stats [Stat]
Print statistics for IC3
pp_print_ic3ia_stats [Stat]
Print statistics for IC3IA
pp_print_ident [LustreIdent]
Pretty-print an identifier
pp_print_ident [LustreAst]
pp_print_ident [Ident]
Pretty-print an identifier
pp_print_if_not_empty [Lib]
Pretty-print if list is not empty
pp_print_ind_stats [Stat]
Print statistics for inductive step
pp_print_index [LustreIndex]
Pretty-print an list of indexes
pp_print_index_trie [LustreIndex]
Pretty print a trie of indexes
pp_print_invgengraph_os_stats [Stat]
Pretty-print INVGENOS statistics items
pp_print_invgengraph_ts_stats [Stat]
Pretty-print INVGENTS statistics items
pp_print_kind_module [Lib]
Pretty-print the name of a kind module
pp_print_kind_module_xml_src [Log.Sig]
pp_print_lambda [Term]
Pretty-print a lambda abstraction
pp_print_lambda [Ltree.S]
Pretty-print a lambda abstraction
pp_print_lambda_w [Ltree.S]
pp_print_let_bindings [YicesDriver]
pp_print_list [Lib]
Pretty-print a list with given separator
pp_print_list2i [Lib]
Pretty-print two lists of the same length with given separator and maintain a counter of their elements.
pp_print_listi [Lib]
Pretty-print a list with given separator and maintain a counter of elements
pp_print_logic [TermLib]
Print a logic
pp_print_logic [YicesDriver]
pp_print_logic [Z3Driver]
pp_print_logic [GenericSMTLIBDriver]
pp_print_logic [CVC4Driver]
pp_print_logic [SolverDriver.S]
Pretty-print a logic in SMTLIB format
pp_print_logic [SMTExpr.Conv]
Pretty-print a logic in SMTLIB format
pp_print_lustre_expr [LustreExpr]
Pretty-print a Lustre expression
pp_print_lustre_type [LustreExpr]
Pretty-print a Lustre type
pp_print_lustre_type [LustreAst]
pp_print_lustre_var [LustreExpr]
Pretty-print a Lustre variable
pp_print_lustre_var_typed [LustreExpr]
Pretty-print a Lustre variable with its type
pp_print_message [Messaging.RelayMessage]
Pretty-print a message
pp_print_misc_stats [Stat]
Print general statistics
pp_print_mode [TestgenModes]
pp_print_mode [LustreContract]
Pretty prints a mode.
pp_print_model [CooperQE]
Print a model
pp_print_model [Model]
Pretty-print a model
pp_print_modes [TestgenModes]
pp_print_native [NativeInput]
Print a transition system in native format
pp_print_node [LustreNode]
Pretty-print a node in Lustre format
pp_print_node_debug [LustreNode]
Pretty-print the node as a record with all information
pp_print_node_equation [LustreNode]
Pretty-print a node equation in Lustre format
pp_print_node_item [LustreAst]
pp_print_node_local_decl [LustreAst]
pp_print_node_local_decl_const [LustreAst]
pp_print_node_local_decl_var [LustreAst]
pp_print_node_param_list [LustreAst]
Pretty-printers
pp_print_node_signature [LustreNode]
Pretty-prints the signature of a node in Lustre format, WITHOUT NODE KEYWORD AND NAME.
pp_print_numeral [Numeral]
Pretty-print a numeral, e.g.
pp_print_numeral_sexpr [Numeral]
Pretty-print a numeral in s-expression, e.g.
pp_print_one_index [LustreIndex]
Pretty-print a single index
pp_print_option [Lib]
Pretty-print an option type
pp_print_param [Analysis]
Pretty printer for param.
pp_print_path [Model]
Pretty-print a path
pp_print_path_in_csv [LustrePath]
Outputs a model as a sequence of inputs in CSV.
pp_print_path_in_csv [InputSystem]
Output a model as a sequnce of inputs in CSV.
pp_print_path_json [LustrePath]
Output a counterexample as a Lustre execution in JSON format
pp_print_path_json [InputSystem]
Output a path in the input system
pp_print_path_pt [LustrePath]
Output a counterexample as a Lustre execution as plain text with pre-processing reverted
pp_print_path_pt [InputSystem]
Output a path in the input system
pp_print_path_pt [Event]
pp_print_path_xml [LustrePath]
Output a counterexample as a Lustre execution in XML format
pp_print_path_xml [InputSystem]
Output a path in the input system
pp_print_poly [Poly]
Print a polynomial
pp_print_pos [Lib]
Pretty-print a position in a concise way
pp_print_position [Lib]
Pretty-print a position
pp_print_process_status [Lib]
Pretty-print the termination status of a process
pp_print_program [LustreAst]
pp_print_prop_quiet [Property]
Pretty-prints a property (name and source only).
pp_print_prop_source [Property]
Pretty-prints a property source.
pp_print_prop_status [Property]
Pretty-prints a property status.
pp_print_property [Property]
Pretty-prints a property.
pp_print_response [SolverResponse]
Pretty-print a response to a command
pp_print_result [Analysis]
Pretty printer for result.
pp_print_result_quiet [Analysis]
Pretty printer for result, quiet version.
pp_print_scope [Scope]
Pretty-print a scope
pp_print_sexpr [SExprBase.S]
Pretty-print an S-expression
pp_print_sexpr_indent [SExprBase.S]
Pretty-print an S-expression
pp_print_sexpr_indent_compact [SExprBase.S]
pp_print_sexpr_list [SExprBase.S]
Pretty-print a list of S-expressions enclosed in parentheses
pp_print_signals [TermLib.Signals]
Pretty printer for signal info.
pp_print_smt_stats [Stat]
Print statistics for SMT
pp_print_sort [YicesDriver]
pp_print_sort [GenericSMTLIBDriver]
pp_print_sort [SolverDriver.S]
Print a sort
pp_print_sort [SMTExpr.Conv]
Pretty-print a sort in SMTLIB format
pp_print_sort [Ltree.BaseTypes]
Pretty-print a sort
pp_print_state_var [StateVar]
Pretty-print a state variable
pp_print_state_var_source [LustreNode]
Pretty-print a source of a state variable
pp_print_stats [Stat]
Print statistics
pp_print_stats_json [Stat]
Print statistics in JSON
pp_print_stats_xml [Stat]
Print statistics in XML
pp_print_struct_item [LustreAst]
pp_print_svar [LustreContract]
Pretty prints a svar wrapper.
pp_print_symbol [YicesDriver]
pp_print_symbol [GenericSMTLIBDriver]
pp_print_symbol [SolverDriver.S]
Pretty-print a symbol
pp_print_symbol [Symbol]
Pretty-print a symbol
pp_print_symbol [Ltree.BaseTypes]
Pretty-print a symbol
pp_print_symbol_node [YicesDriver]
pp_print_symbol_node [GenericSMTLIBDriver]
pp_print_sys_modes [TestgenModes]
pp_print_term [YicesDriver]
pp_print_term [GenericSMTLIBDriver]
pp_print_term [Term]
Pretty-print a term
pp_print_term [Ltree.S]
Pretty-print a term
pp_print_term' [YicesDriver]
pp_print_term_as_expr [LustreExpr]
Pretty-print a term as an expr.
pp_print_term_w [Ltree.S]
pp_print_testgen_stats [Stat]
pp_print_trans_sys [TransSys]
Pretty-print a transition system
pp_print_trans_sys_name [TransSys]
Pretty-print the name of a transition system
pp_print_tree [TestgenLib]
Pretty printer for the tree structure.
pp_print_tree [TestgenTree]
Quiet tree pretty printer.
pp_print_trie [Trie.S]
Pretty-print bindings in the trie with a printer for key and value pairs
pp_print_trie_expr [LustreIndex]
Pretty print a trie with expressions
pp_print_type [YicesDriver]
pp_print_type [Type]
Pretty-print a type
pp_print_type_decl [LustreAst]
pp_print_type_node [YicesDriver]
pp_print_type_node [Type]
Pretty-print a type
pp_print_typed_ident [LustreAst]
pp_print_typed_var_list [YicesDriver]
pp_print_uf_symbol [UfSymbol]
Pretty-print a symbol
pp_print_value [Model]
Pretty-print a value
pp_print_value [Eval]
pp_print_value_xml [Model]
Pretty-print a value in xml format
pp_print_var [Var]
Pretty-print a hashconsed variable
pp_print_var [Ltree.BaseTypes]
Pretty-print a variable
pp_print_var_decl [LustreAst]
pp_print_version [Lib]
Output the version number on the formatter
pp_print_yices_id [YicesResponse]
pre_is_unguarded [LustreExpr]
Return true if there is an unguarded pre operator in the expression.
pre_offset [LustreExpr]
Offset of state variable at previous instant
pre_term_of_expr [LustreExpr]
Term at previous instant with the given offset as zero
pre_term_of_state_var [LustreExpr]
Term of instance of state variable at previous instant with the given offset as zero
pre_term_of_t [LustreExpr]
Term at previous instant with the given offset as zero
pre_var_of_state_var [LustreExpr]
Instance of state variable at previous instant with the given offset as zero
pred [Numeral]
Predecessor
pred [Decimal]
Predecessor
prefix [TestgenStrategies.Sig]
Prefix which should be unique to a strategy.
prelude [YicesDriver]
prelude [GenericSMTLIBDriver]
prelude [SolverDriver.S]
Solver specific commands to add at the beginning of the file
prev [LustreContext]
return previous context
print_attr [TermAttr]
Pretty-print a hashconsed attribute to the standard formatter
print_backtrace [Lib]
Pretty print a backtrace
print_cex [Flags.BmcKind]
Print counterexamples to induction.
print_double_line [Pretty]
prints separating double line
print_expr [YicesDriver]
print_expr [GenericSMTLIBDriver]
print_expr [SolverDriver.S]
Pretty-print an expression to the default formatter
print_expr [SMTExpr.Conv]
Pretty-print a term in SMTLIB format to the standard formatter
print_hstring [HString]
Pretty-print a hashconsed term to the standard formatter
print_lambda [Term]
Pretty-print a lambda abstraction to the standard formatter
print_lambda [Ltree.S]
Pretty-print a lambda abstraction
print_line [Pretty]
prints separating line
print_pass [Lib]
Prints the first argument and returns the second.
print_sexpr [SExprBase.S]
Pretty-print an S-expression to the standard formatter
print_stats [InvarManager]
Prints statistics and properties status.
print_term [Term]
Pretty-print a term to the standard formatter
print_term [Ltree.S]
Pretty-print a term
print_to_file [Flags.IC3]
File for inductive blocking clauses.
print_type [Type]
Pretty-print a type to the standard formatter
print_var [Var]
Pretty-print a hashconsed variable to the standard formatter
print_xml_trailer [Log.Sig]
printf_json [Log.Sig]
printf_xml [Log.Sig]
produce_assignments [SolverSig.Params]
produce_cores [SolverSig.Params]
produce_proofs [SolverSig.Params]
progress [Event]
Output the progress of the module
proof [Flags.Certif]
Proof production.
prop_base [TransSys]
Offset of current state variables in properties and invariants, subtract one for the offset of the previous state variables
prop_name_in_context [LustreContext]
Return true if the identifier denotes a property in the context
prop_name_of_svar [LustreContract]
Generates a property name.
prop_set_of_props [Clause]
Create a property set from a list of named properties
prop_status [Event]
Broadcast a property status
prop_status_known [Property]
Return true if the status of the property is known
property_of_name [TransSys]
props_list_of_bound [TransSys]
Instantiate all properties to the bound
props_of_prop_set [Clause]
Return the named properties of the property set
prune_trivial [Flags.Invgen]
InvGen will remove trivial invariants, i.e.
pruning_add_invariants [LockStepDriver]
Adds invariants to a pruning checker.
pruning_sys [LockStepDriver]
System associated with a pruning checker.
psummand_contains_variable [Poly]
Return true when the psummand contains the variable, false otherwise
push [TestgenTree]
Pushes a node on top of the current one, activating a mode conjunction.
push [SMTSolver]
Push a new scope to the context stack
push [SolverSig.Inst]
Push a number of empty assertion sets to the stack
push_contract_scope [LustreContext]
Add contract scope to context.
push_index [LustreIdent]
Add the given integer as an index to the identifier
push_scope [LustreContext]
Add scope to context

Q
qe [Debug]
qe [Flags.IC3]
The QE algorithm IC3 should use.
qedetailed [Debug]
quantified_smtexpr_of_term [SMTExpr.Conv]
Convert a term to an SMT expression, quantifying over the given variables quantified_smtexpr_of_term q v t returns the SMT expression exists (v) t or forall (v) t if q is true or false, respectively, where all variables in t except those in v are converted to uninterpreted functions.
query_base [LockStepDriver]
Checks whether some terms are falsifiable k states away from the initial state, where k is the internal depth of the base checker.
query_pruning [LockStepDriver]
Checks if some terms are trivially implied by the transition relation.
query_step [LockStepDriver]
Queries step.

R
raise_no_new_definition_exc [LustreContext]
rcontains_from [HString]
read_file [InputParser]
Parse a CSV input file
read_from_lexbuf_stack [LustreLexer]
Create a lexer reading from a stack of nested include files
read_input_lustre [InputSystem]
Read input from file
read_input_native [InputSystem]
Read native input from file
real_cube_size [Flags.C2I]
Number of real cubes in the DNF constructed by C2I.
recdef [Flags.Arrays]
Define recursive functions for arrays
reconstruct_lustre_streams [LustrePath]
Reconstruct Lustre streams from state variables
reconstruct_lustre_streams [InputSystem]
record_time [Stat]
Record the time since the call to Stat.start_timer of this statistics item, stop the timer
recv [Messaging.S]
Receive messages queued by the background thread
recv [Event]
Receive all queued events
refinement [Flags.Contracts]
Activate refinement.
reinterpret_select [Term]
Inverse transformation of !convert_select
relations_of [InvGenGraph.Graph]
Appends the relations from a graph to the input term list.
rem [Numeral]
Remainder
rem [Decimal]
Remainder
remove [Trie.S]
Remove key from trie
remove_expr_for_ident [LustreContext]
Remove the binding of an identifier from the context
renice [Flags.Invgen]
Renice invariant generation process.
replace_lasts [LustreAst]
replace_lasts allowed prefix acc e replaces last x expressions in AST e by abstract identifiers prefixed with prefix.
res_type_of_uf_symbol [UfSymbol]
Return the type of the result of the uninterpreted symbol
reserved_scope [LustreIdent]
Scope for reserved identifiers
reserved_strings [Lib.ReservedIds]
All reserved identifiers.
reserved_word_list [YicesDriver]
reset [Stat]
Reset an integer statistics item to its initial value
reset_float [Stat]
Reset a float statistics item to its initial value
reset_fresh_actlit_count [Actlit]
Resets the internal counter for fresh actlits.
reset_gc_params [Lib]
Reset the parameters of the GC to its default values.
reset_guard_flag [LustreContext]
Resets the flag indicating there are unguarded pre's in the lustre code, and we need to guard them.
reset_in_automaton [LustreContext]
Resets the flag indicating we are evaluating an automaton.
reset_int_list [Stat]
Reset an integer list statistics item to its initial value
restart [TestgenSolver]
Restarts a solver.
restart_selected_next_string [Lib.ReservedIds]
restart_selected_string [Lib.ReservedIds]
restart_string [Lib.ReservedIds]
result_is_all_proved [Analysis]
Returns true if all properties in the system in a result have been proved.
result_is_some_falsified [Analysis]
Returns true if some properties in the system in a result have been falsified.
results_add [Analysis]
Adds a result to a results.
results_clean [Analysis]
Cleans the results by removing nodes that don't have any property or contract.
results_find [Analysis]
Returns the list of results for a top scope.
results_is_safe [Analysis]
Returns None if no properties were falsified but some could not be proved, Some true if all properties were proved, and Some false if some were falsified.
results_last [Analysis]
Returns the last result corresponding to a scope.
results_length [Analysis]
Returns the total number of results stored in a results.
rindex [HString]
rindex_from [HString]
rm [TestgenSolver]
Destroys the underlying solver.
rm [TestgenIO]
Closes internal file descriptors.
ruleTail [SExprLexer]
run [PostAnalysis.PostAnalysis]
run [PostAnalysis]
Runs the post-analysis things on a system and its results.
run [Kind2Flow]
run_im [Messaging.S]
Start the background thread for the invariant manager, using the given context and sockets.
run_im [Event]
Start messaging for the invariant manager
run_process [Event]
Start messaging for another process
run_worker [Messaging.S]
Start the background thread for a worker process, using the given context and sockets.

S
s_and [Symbol]
Constant conjunction symbol
s_array [GenericSMTLIBDriver]
s_bool [YicesDriver]
s_bool [GenericSMTLIBDriver]
s_define_fun [GenericSMTLIBDriver]
s_define_fun [SMTLIBSolver.SMTLIBSolverDriver]
s_div [Symbol]
Constant division operator symbol
s_eq [Symbol]
Constant equality symbol
s_false [Symbol]
Constant Boolean value symbol
s_geq [Symbol]
Constant greater than or equal symbol
s_gt [Symbol]
Constant greater than symbol
s_implies [Symbol]
Constant implication symbol
s_int [YicesDriver]
s_int [GenericSMTLIBDriver]
s_ite [Symbol]
Constant ite symbol
s_lambda [CVC4Driver]
s_leq [Symbol]
Constant less than or equal symbol
s_lt [Symbol]
Constant less than symbol
s_minus [Symbol]
Constant minus operator symbol
s_mod [Symbol]
Constant modulus operator symbol
s_not [Symbol]
Constant negation symbol
s_or [Symbol]
Constant disjunction symbol
s_plus [Symbol]
Constant plus operator symbol
s_real [YicesDriver]
s_real [GenericSMTLIBDriver]
s_select [Symbol]
Array read operator
s_store [Symbol]
array store symbol
s_subrange [YicesDriver]
s_times [Symbol]
Constant times operator symbol
s_true [Symbol]
Constant Boolean value symbol
safe [Lib.ExitCodes]
Exit code for an error.
safe_hash_interleave [Lib]
safe_hash_interleave h m i compute m * h + i and makes sure that the result does not overflow to a negtive number
scan_block_comment [SExprLexer]
scan_quoted [SExprLexer]
scan_string [SExprLexer]
scope_of_context [LustreContext]
scope_of_node [LustreNode]
Return the scope of the node
scope_of_state_var [StateVar]
Return the scope of the state variable
scope_of_trans_sys [TransSys]
Return the scope identifying the transition system
select_symbols_of_term [Term]
Return the select symbols occurring in the term
select_terms [Term]
Return the terms of the form (select ...) that appear in a term
send_output_message [Messaging.S]
Send a message to the invariant manager for output to the user
send_relay_message [Messaging.S]
Broadcast a message to the worker processes
send_term_message [Messaging.S]
Send a termination message to the invariant manager
set [Stat]
Set an integer statistics item
set [HString]
set_float [Stat]
Set a float statistics item
set_for_inv_gen [StateVar]
Set or unset flag to use state variable in invariant generation
set_formatter [Debug]
Set the formatter for debugging
set_guard_flag [LustreContext]
Sets the flag indicating there are unguarded pre's in the lustre code, and we need to guard them.
set_in_automaton [LustreContext]
Sets the flag indicating we are evaluating an automaton.
set_int_list [Stat]
Set an integer statistics list
set_liberal_gc [Lib]
Changes garbage collector parameters limit its effect
set_log_format [Log.Sig]
Chooses the log format
set_log_format_json [Log.Sig]
Set log format to JSON
set_log_format_pt [Log.Sig]
Set log format to plain text
set_log_format_xml [Log.Sig]
Set log format to XML
set_log_level [Lib]
Set log level
set_max_depth [Flags.Invgen]
Sets the max depth for invariant generation.
set_module [Log.Sig]
Set module currently running
set_node_function [LustreContext]
Mark node as function
set_node_main [LustreContext]
Mark node as main
set_offset_of_state_var_instance [Var]
Return a new variable with the offset of the state variable instance set to the given value
set_oracle_state_var [LustreNode]
set_prop_false [TransSys]
Mark property as false
set_prop_false [Property]
set_prop_invariant [TransSys]
Mark property as invariant
set_prop_invariant [Property]
set_prop_ktrue [TransSys]
Mark property as k-true
set_prop_ktrue [Property]
set_prop_status [TransSys]
Update current status of the property
set_prop_status [Property]
set_qe [Flags.IC3]
Sets qe.
set_relay_log [Event]
Relay log messages to invariant manager (overrides function from Log)
set_relay_log [Log.Sig]
Relay log messages to invariant manager, takes printing function as argument for relay messages.
set_short_names [Flags.Smt]
Change sending of short names to SMT solver
set_sigalrm_exn [TermLib.Signals]
Sets an exception handler for sigalarm.
set_sigalrm_timeout [TermLib.Signals]
Sets a timeout handler for sigalrm.
set_sigalrm_timeout_from_flag [TermLib.Signals]
Sets a timeout based on the flag value and the total time elapsed this far.
set_sigint [TermLib.Signals]
Sets a handler for sigint.
set_sigpipe [TermLib.Signals]
Sets a handler for sigpipe.
set_sigquit [TermLib.Signals]
Sets a handler for sigquit.
set_sigterm [TermLib.Signals]
Sets a handler for sigterm.
set_solver [Flags.Smt]
Set SMT solver and executable
set_state_var_alias [LustreNode]
Sets the first svar as alias for the second svar.
set_state_var_expr [LustreNode]
set_state_var_instance [LustreNode]
State variable is identical to a state variable in a node instance
set_state_var_node_call [LustreNode]
Register state var as tied to a node call if not already registered.
set_state_var_source [LustreContext]
set_state_var_source [LustreNode]
Set source of state variable
set_state_var_source_if_undef [LustreNode]
Set source of state variable if not already defined.
set_timeout [TermLib.Signals]
Sets a timeout.
set_trace [Flags.Smt]
Forces SMT traces.
set_var_offset [Model]
Set offset of all variables in model to k
setup [Kind2]
setup [Event]
Create contexts and bind ports for all processes
short_name_of_kind_module [Lib]
Return a short representation of kind module
short_names [Flags.Smt]
Send short names to SMT solver
shrink_info_to_sys [Analysis]
Shrinks an abstraction map to the subsystems of a system.
shrink_param_to_sys [Analysis]
Shrinks a param to a system.
silent_contracts_of [InputSystem]
Returns the silent contract associated to each system.
simplify [Debug]
simplify_term [Simplify]
Simplify a term
simplify_term_model [Simplify]
Simplify a term given an assignment to variables
singleton [LustreIndex]
Return a trie with a single element for the empty index
size [Certificate]
Gives a measure to compare the size of the inductive invariants contained in a certificate.
slice_to_abstraction [LustreSlicing]
Return a node hierarchy reduced to the cone of influence of properties and contracts, given a list of which nodes should be abstracted.
slice_to_abstraction_and_property [LustreSlicing]
slice_to_abstraction_and_property [InputSystem]
smt [Debug]
smt [Flags.Arrays]
Use builtin theory of arrays in SMT solver
smt_check_sat_time [Stat]
Time in check-sat calls
smt_get_unsat_core_time [Stat]
Time in get-unsat-core calls
smt_get_value_time [Stat]
Time in get-value calls
smt_stats [Stat]
SMT statistics
smt_stats_title [Stat]
Title for SMT statistics
smt_stop_timers [Stat]
Stop and record all timers
smtexpr [Debug]
smtexpr_of_term [SMTExpr.Conv]
Convert a term to an SMT expression
smtexpr_of_term_time [Stat]
smtexpr_of_var [SMTExpr.Conv]
Convert a variable to an SMT expression
smtlib_reserved_word_list [GenericSMTLIBDriver]
smtlib_string_sexpr_conv [GenericSMTLIBDriver]
smtlib_string_symbol_list [GenericSMTLIBDriver]
smtsort_of_type [SMTExpr.Conv]
Convert a variable to an SMT expression
solve_fref [LustreContext]
Resolve a forward reference, fails if a circular dependency is detected.
solver [Flags.Smt]
Which SMT solver to use.
sort_of_var [Ltree.BaseTypes]
Return the sort of a variable
sorts_of_lambda [Ltree.S]
Return the sorts of a hashconsed lambda abstraction
source_of_clause [Clause]
Return the source of the clause
source_of_svar [LustreNode]
Returns the equation for a state variable if any.
split [Certificate]
Split a certificate following the boolean strucutre of its inductive invariant
split [Trie.S]
split_certs [Certificate]
Split a list of certificates
split_expr_list [LustreExpr]
Split a list of Lustre expressions into a list of pairs of expressions for the initial step and the transition steps, respectively
stabilize [InvGenGraph.Graph]
Queries the lsd and updates the graph.
start_timer [Stat]
Start a timer for the float statistics item
stat [Event]
Output the statistics of the module
state_selected_next_string [Lib.ReservedIds]
state_selected_string [Lib.ReservedIds]
state_string [Lib.ReservedIds]
Automaton state encoding.
state_var_instance_of_symbol [Var]
Gets the state var instance associated with a constant unrolled uf.
state_var_instance_of_uf_symbol [Var]
Gets the state var instance associated with a constant unrolled uf.
state_var_is_input [LustreNode]
Return true if the state variable is an input
state_var_is_local [LustreNode]
Return true if the state variable is a local variable
state_var_is_output [LustreNode]
Return true if the state variable is an output
state_var_is_visible [LustreNode]
Return true if the state variable should be visible to the user, false if it was created internally
state_var_of_expr [LustreExpr]
Return the state variable of a variable
state_var_of_long_string [StateVar]
Return a previously declared state variable from a string consisting of the concatenation of all scopes and the state variable.
state_var_of_state_var_instance [Var]
Return the state variable of a state variable instance
state_var_of_string [StateVar]
Return a previously declared state variable
state_var_of_uf_symbol [StateVar]
Return the state variable corresponding to an uninterpreted function symbol
state_vars [TransSys]
Return the state variables of a transition system
state_vars_at_offset_of_term [Term]
Return the state variables at given offset in term
state_vars_of_expr [LustreExpr]
Return all state variables occurring in the expression in a set
state_vars_of_term [Term]
Return the state variables occurring in the term
stateful_vars_of_node [LustreNode]
Return all stateful variables from expressions in a node
stats [Hashcons.S]
stats [Hashcons]
Return statistics on the table.
stats [Var]
stats [Term]
return statistics of hashconsing
stats [Symbol]
stats [StateVar]
stats [Ltree.S]
step_add_invariants [LockStepDriver]
Adds invariants to a step checker.
step_cert [LockStepDriver]
Certificate (k) of a step checker.
step_cex [Event]
Broadcast a step cex
step_stabilize [InvGenGraph.Graph]
Clones the graph, and splits it in step.
steps [Flags.Interpreter]
Run number of steps, override the number of steps given in the input file.
strategy_info_of [SubSystem]
Strategy info of a subsystem.
string_buf [YicesLexer]
string_of_attr [TermAttr]
Return a string representation of a hashconsed attribute
string_of_custom_arg [SMTExpr.Conv]
Return an string representation of a custom argument
string_of_decimal [Decimal]
Return a string representation of a rational
string_of_decimal_sexpr [Decimal]
Return an S-expression string representation of a rational
string_of_expr [YicesDriver]
string_of_expr [GenericSMTLIBDriver]
string_of_expr [SolverDriver.S]
Return a string representation of an expression
string_of_expr [SMTExpr.Conv]
Return an SMTLIB string expression of a term
string_of_hstring [HString]
Return the string
string_of_ident [LustreIdent]
Return a string representation of the identifier
string_of_index [LustreIndex]
Return a string representation of indexes
string_of_kind_module [Lib]
String representation of a process type
string_of_lambda [Term]
Return a string representation of a lambda abstraction
string_of_log_level [Lib]
string_of_logic [TermLib]
String correspinding to a logic
string_of_logic [YicesDriver]
string_of_logic [Z3Driver]
string_of_logic [GenericSMTLIBDriver]
string_of_logic [CVC4Driver]
string_of_logic [SolverDriver.S]
Return an SMTLIB string expression for the logic
string_of_logic [SMTExpr.Conv]
Return an SMTLIB string expression for the logic
string_of_numeral [Numeral]
Return a string representation of a numeral
string_of_sexpr [SExprBase.S]
Return a string representation of an S-Expression
string_of_signal [Lib]
String representation of signal
string_of_sort [YicesDriver]
string_of_sort [GenericSMTLIBDriver]
string_of_sort [SolverDriver.S]
Return an SMTLIB string expression of a sort
string_of_sort [SMTExpr.Conv]
Return an SMTLIB string expression of a sort
string_of_state_var [StateVar]
Return a string representation of a symbol
string_of_symbol [YicesDriver]
string_of_symbol [GenericSMTLIBDriver]
string_of_symbol [SolverDriver.S]
Return a string representation of a symbol
string_of_symbol [Symbol]
Return a string representation of a symbol
string_of_symbol_node [Symbol]
Return a string representation of a symbol
string_of_t [Lib]
Pretty-print into a string
string_of_term [Term]
Return a string representation of a term
string_of_type [Type]
Return a string representation of a type
string_of_uf_symbol [UfSymbol]
Return a string representation of a symbol
string_of_var [Var]
Return a string representation of a hashconsed variable
string_starts_with [Lib]
string_starts_with s1 s2 returns true if the first characters of s1 up to the length of s2 are ientical to s2.
string_symbol_list [YicesDriver]
strings_of_message [Messaging.RelayMessage]
Convert string from message frames to a message
sub [Numeral]
Difference
sub [HString]
sub [Decimal]
Difference
subdir_for [Flags]
Path to subdirectory for a system (in the output directory).
substitute_definitions_in_expr [LustrePath]
Recursively substitute the state variables in a term with their definition in equations.
subsume [Trie.S]
Return a new trie containing only entries with keys that are not subsets of the given key
subsystem_of_nodes [LustreNode]
Return a tree-like subsystem hierarchy from a flat list of nodes, where the top node is at the head of the list.
succ [Numeral]
Successor
succ [Decimal]
Successor
success [YicesResponse]
success_tag [Pretty]
Success tag.
sup_logics [TermLib]
Returns the sup of the logics given as arguments
sv_at_0 [TestgenModes]
svars_of [LustreContract]
symbol_of_smtlib_atom [GenericSMTLIBDriver]
syscall [Lib]
Get standard output of command

T
t_bool [Type]
The boolean type
t_false [LustreExpr]
The propositional constant false
t_false [Term]
The propositional constant false
t_int [Type]
The integer type
t_real [Type]
The real decimal type
t_true [LustreExpr]
The propositional constant true
t_true [Term]
The propositional constant true
tag [Term]
Unique identifier for terms
tag [Ltree.S]
Unique identifier for term
tag_of_level [Pretty]
tag_of_t [Ltree.S]
Return the unique tag of a hashconsed term
term_count [InvGenGraph.Graph]
Total number of terms in the graph.
term_of [TestgenLib]
Turns an actlit uf in a term.
term_of_actlit [Actlit]
Returns the term corresponding to the input actlit.
term_of_cformula [Presburger]
Convert a presburger formula to a term
term_of_clause [Clause]
Return the conjunction of all literals in the clause
term_of_named [Term]
Return the term of a named term
term_of_poly [Presburger]
Convert a polynomial to a term
term_of_prop_set [Clause]
Return the conjunction of the properties
term_of_smtexpr [SMTExpr.Conv]
Convert an SMT expression to a term
term_of_smtexpr_time [Stat]
term_of_value [Eval]
Cast a value to a term, raise Invalid_argument if value is unknown
terminate [Event]
Broadcast a termination message
terminate_log [Event]
Terminate log, called at the very end of a run.
terms_of [InvGenGraph.Graph]
Minimal list of terms encoding the current state of the graph.
testcase_count [TestgenIO]
The number of testcases generated.
testcase_gen [TestgenLib]
Generates the actual test cases in csv using a get-model function.
testcase_gen [TestgenStrategies.Sig]
Generates test cases using a get_model function.
testcases_to_tree [TestgenLib]
Converts some test cases to a tree.
testgen [Lib.Paths]
Test generation files path.
testgen_backward_time [Stat]
Time spent going backward.
testgen_deadlocks [Stat]
testgen_enumerate_time [Stat]
Time spent enumerating.
testgen_forward_time [Stat]
Time spent going forward.
testgen_restarts [Stat]
testgen_stats [Stat]
testgen_stats_title [Stat]
testgen_stop_timers [Stat]
testgen_testcases [Stat]
testgen_total_time [Stat]
time_fun [Stat]
Time a function call and add to the statistics item
timeout_analysis [Flags]
Per-run wallclock timeout.
timeout_tag [Pretty]
Timeout tag.
timeout_wall [Flags]
Wallclock timeout.
title [PostAnalysis.PostAnalysis]
Indicates whether the module is active.
to_big_int [Numeral]
Convert a numeral to an arbitrary large integer
to_big_int [Decimal]
Convert a rational number to an arbitrary large integer
to_int [Numeral]
Convert a numeral to an integer
to_int [Decimal]
Convert a rational number to a rational
to_list [Model]
Return an association list with the assignments in the model
to_presburger [Presburger]
Normalize the term into a Presburger formula
to_scope [LustreIdent]
Return a scope of an identifier
to_step [LockStepDriver]
Transforms a base checker into a step checker.
to_string [Scope]
to_string [Ident]
Return a string representation of an identifier x
token [YicesLexer]
token [LustreLexer]
Entry point for the lexer
top_max_index [LustreIndex]
If the first index is a list, return the greatest integer in a trie of indexes.
top_only [Flags.Invgen]
InvGen will generate invariants only for top level.
total_time [Stat]
Total time
trace [Flags.Smt]
trace_comment [SMTSolver]
Output a comment into the trace
trace_comment [SolverSig.Inst]
trace_dir [Flags.Smt]
Path to the smt trace directory.
trace_extension [YicesDriver]
trace_extension [GenericSMTLIBDriver]
trace_extension [SolverDriver.S]
File extension for traces
trace_svars_of [LustreContext]
The svars in the COI of the input expression, in the current node.
trans_base [TransSys]
Offset of current state variables in transition relation, subtract one for the offset of the previous state variables
trans_formals [TransSys]
Variables in the transition relation
trans_fun_of [TransSys]
Builds a call to the transition relation function linking state k and k'.
trans_of_bound [TransSys]
Close the initial state constraint by binding all instance identifiers, and bump the state variable offsets to be at the given bound
trans_sys_of_analysis [InputSystem]
Return a transition system for an analysis run
trans_sys_of_nodes [LustreTransSys]
trans_uf_string [Lib.ReservedIds]
New clock initialization flag.
trans_uf_symbol [TransSys]
Predicate for the transition relation
translate_contracts [Flags.Contracts]
Translate contracts.
translate_contracts_lustre [InputSystem]
Translate lustre contracts to properties.
transsys [Debug]
trim [HString]
true_of_any [Lib]
Return true
true_of_unit [Lib]
Returns true when given unit.
two_state [Flags.Invgen]
InvGen will run in two state mode.
type_in_context [LustreContext]
Return true if the identifier denotes a type in the context
type_of_expr [LustreExpr]
Return the type of the expression
type_of_ident [LustreContext]
Resolve an indentifier to a type.
type_of_lustre_expr [LustreExpr]
Return the type of the expression
type_of_smtlib_sexpr [GenericSMTLIBDriver]
type_of_state_var [StateVar]
Return the type of the variable
type_of_string_sexpr [YicesDriver]
type_of_term [Term]
Return the type of the term
type_of_var [Var]
Return the type of the variable

U
uf_defs [TransSys]
Return predicate definitions of initial state and transition relation of the top system and all its subsystem in reverse topological order
uf_of_symbol [Symbol]
Return the uninterpreted symbol of a symbol
uf_symbol_of_state_var [StateVar]
Return the uninterpreted function symbol of the variable
uf_symbol_of_string [UfSymbol]
Return a previously declared uninterpreted function symbol
uncapitalize [HString]
undo_ind_gen [Clause]
If the clause is an inductive generalization, return the clause before generalization
unit_mode_switch [TestgenStrategies]
First class unit mode switch module.
unknown [Lib.ExitCodes]
Exit code for an unknown result.
unless_string [Lib.ReservedIds]
unnegate [Term]
Remove top negation from term, otherwise return term unchanged
unpause_time [Stat]
Unpauses a timer previously paused by record_time.
unroll_test_case [TestgenLib]
Constructs the explicit unrolling of a test case.
unrolled_uf_of_state_var_instance [Var]
unsafe [Lib.ExitCodes]
Exit code for a safe result.
unsafe_expr_of_term [LustreExpr]
unsafe_term_of_expr [LustreExpr]
unset_relay_log [Log.Sig]
Cancel relaying of log messages
unset_timeout [TermLib.Signals]
Deactivates timeout.
unsliced_trans_sys_of [InputSystem]
Transition system for contract generation or interpreter, without any slicing.
unwrap [Res]
Unwraps a result.
update [TestgenTree]
Updates the current mode.
update_child_processes_list [Messaging.S]
Notifies the background thread of a new list of child processes.
update_child_processes_list [Event]
Notifies the background thread of a new list of child processes.
update_time [Stat]
Record the time since the call to Stat.start_timer of this statistics item, do not stop the timer
update_trans_sys [Event]
Update transition system from events and return new top level invariants and properties with changed status.
update_trans_sys_sub [Event]
Update transition system from events and return new invariants INCLUDING subsystem ones, scoped and properties with changed status.
uppercase [HString]
use_invgen [Flags.IC3]
Use invariants from invariant generators.
user_scope [LustreIdent]
Scope for identifiers in user input

V
value_is_unknown [Eval]
Check if the value is unknown
values [Trie.S]
Return the values in the trie
var_of_array_select [LustreExpr]
var_of_expr [LustreExpr]
Return the free variable of a variable
var_of_select_store [Term]
var_offsets_of_term [Term]
Return the minimal and maximal offset of state variable instances
var_size [Flags.Arrays]
Allow non constant array sizes
var_term_of_smtexpr [SMTExpr.Conv]
Convert an SMT expression to a variable
vars_at_offset_of_term [Term]
Return the state variables at given offset in term
vars_of_bounds [TransSys]
Return instances of the state variables of the transition system between given instants
vars_of_expr [LustreExpr]
vars_of_term [Term]
Return the variables occurring in the term
version [Version]
vt_width [Pretty]
Width of the virtual terminal (80 if cannot be detected)

W
warn_at_position [LustreContext]
Output a warning at position
warn_no_position [LustreContext]
Output a warning without a position
warning_tag [Pretty]
Warning tag.
weakhcons [Flags]
Use weak hash-consing.
width_of_string [Lib]
Return the width of the string, meaning the wisth of it's longest line
work [TestgenStrategies.Sig]
Works on the k^th unrolling of the system.
write_dot_to [InvGenGraph]
write_dot_to path name suff fmt graph Writes a graph in graphviz to file <path>/<name>_<suff>.dot.

Y
yices2smt2_bin [Flags.Smt]
Executable of Yices2 SMT2 solver
yices_bin [Flags.Smt]
Executable of Yices solver
yices_id_of_int [YicesResponse]

Z
z3_bin [Flags.Smt]
Executable of Z3 solver
zero [Numeral]
The numeral zero
zero [Decimal]
The rational number zero