Dynamic Predicates: count_id_usage/2

3530 Lines

413 Predicates

Imported Modules: tools lists ordsets avl terms self_check error_manager

194 Exports

37 specified Imports

Imports	Exports
Name: module_info/2 Module: module_information Name: print_bexpr/1 Module: translate Name: translate_bexpression/2 Module: translate Name: gensym/2 Module: gensym Name: get_preference/2 Module: preferences Name: preference/2 Module: preferences Name: debug_mode/1 Module: debug Name: debug_format/3 Module: debug Name: is_finite_type_in_context/2 Module: typing_tools Name: normalize_type/2 Module: typing_tools Name: convlist_max/4 Module: tools_lists Name: check_unique_in_domain_of_avlset/2 Module: custom_explicit_sets Name: ground_value/1 Module: kernel_tools Name: is_provably_finite_type/1 Module: typing_tools Name: type_has_at_least_two_elements/1 Module: typing_tools Name: b_non_empty_global_set/1 Module: b_global_sets Name: avl_is_interval/3 Module: custom_explicit_sets Name: safe_sort/3 Module: tools Name: bmachine_is_precompiled/0 Module: bmachine Name: b_is_variable/2 Module: bmachine Name: b_is_constant/2 Module: bmachine Name: debug_println/2 Module: debug Name: b_get_global_constants/1 Module: b_global_sets Name: b_get_enumerated_set_constants/1 Module: b_global_sets Name: b_get_global_sets/1 Module: b_global_sets Name: prime_identifiers/2 Module: btypechecker Name: safe_univ_no_cutoff/2 Module: tools Name: valid_ground_type/1 Module: typing_tools Name: lookup_type_for_expr/2 Module: btypechecker Name: unify_types_werrors/4 Module: btypechecker Name: eventb_mode/0 Module: specfile Name: z_or_tla_minor_mode/0 Module: specfile Name: avl_min_pair/3 Module: avl_tools Name: check_used_ids_info/4 Module: b_ast_cleanup Name: unify_types_strict/2 Module: btypechecker Name: couplise_list/2 Module: btypechecker Name: check_is_non_empty_avl/1 Module: avl_tools	Name: is_texpr/1 Name: get_texpr_expr/2 Name: get_texpr_type/2 Name: get_texpr_info/2 Name: get_texpr_id/2 Name: def_get_texpr_id/2 Name: def_get_texpr_ids/2 Name: create_typed_id/3 Name: same_id/3 Name: same_ids/2 Name: same_ids_and_types/2 Name: split_names_and_types/3 Name: get_texpr_exprs/2 Name: get_texpr_types/2 Name: get_texpr_infos/2 Name: get_texpr_ids/2 Name: get_texpr_pos/2 Name: extract_pos_infos/2 Name: copy_pos_infos/3 Name: delete_pos_info/2 Name: propagate_pos_info_if_useful/3 Name: merge_info/3 Name: update_infos/3 Name: get_info_pos/2 Name: contains_info_pos/1 Name: same_texpr/2 Name: different_texpr_values/2 Name: create_texpr/4 Name: add_texpr_infos/3 Name: add_texpr_info_if_new/3 Name: add_texpr_infos_if_new/3 Name: add_info_if_new/3 Name: add_infos_if_new/3 Name: safe_create_texpr/3 Name: safe_create_texpr/4 Name: texpr_contains_wd_condition/1 Name: sub_expression_contains_wd_condition/1 Name: get_rodin_name/2 Name: get_rodin_model_name/2 Name: is_rodin_label_info/1 Name: get_texpr_label/2 Name: get_texpr_labels/2 Name: get_info_labels/2 Name: select_info_labels/3 Name: add_labels_to_texpr/3 Name: get_texpr_description/2 Name: add_texpr_description/3 Name: info_has_ignore_pragma/1 Name: predicate_has_ignore_pragma/1 Name: always_well_defined/1 Name: always_well_defined_or_disprover_mode/1 Name: always_well_defined_or_wd_reorderings_allowed/1 Name: always_well_defined_or_wd_improvements_allowed/1 Name: finite_wd_set_value/1 Name: finite_set_or_disprover_mode/1 Name: is_truth/1 Name: is_falsity/1 Name: conjunct_predicates/2 Name: conjunct_predicates_with_pos_info/3 Name: conjunct_predicates_with_pos_info/2 Name: is_a_conjunct/3 Name: is_a_conjunct_without_label/3 Name: decompose_conjunct/3 Name: is_a_disjunct/3 Name: is_an_implication/3 Name: is_an_equivalence/3 Name: is_a_negation/2 Name: conjunction_to_list/2 Name: conjunction_to_list_with_rodin_labels/2 Name: member_in_conjunction/2 Name: select_member_in_conjunction/3 Name: flatten_conjunctions/2 Name: size_of_conjunction/2 Name: member_in_conjunction_cse/3 Name: disjunct_predicates/2 Name: disjunct_predicates_with_pos_info/3 Name: disjunction_to_list/2 Name: is_a_disjunct_or_implication/4 Name: is_a_conjunct_or_neg_disj/3 Name: predicate_components/2 Name: predicate_components_in_scope/3 Name: predicate_components_with_restriction/4 Name: predicate_identifiers/2 Name: predicate_identifiers_in_scope/3 Name: project_predicate_on_identifiers/5 Name: find_identifier_uses_top_level/2 Name: find_identifier_uses/3 Name: find_identifier_uses_if_necessary/3 Name: find_identifier_uses_l/3 Name: find_typed_identifier_uses/3 Name: find_typed_identifier_uses/2 Name: find_typed_identifier_uses_l/3 Name: get_global_identifiers/1 Name: get_global_identifiers/2 Name: occurs_in_expr/2 Name: some_id_occurs_in_expr/2 Name: single_usage_identifier/3 Name: update_used_ids/3 Name: check_computed_used_ids/2 Name: create_exists/3 Name: create_or_merge_exists/3 Name: create_exists_or_let_predicate/3 Name: create_exists_opt_liftable/3 Name: create_exists_opt/3 Name: create_exists_opt/4 Name: create_exists_opt/5 Name: create_forall/3 Name: create_negation/2 Name: is_negation_of/2 Name: get_negated_operator_expr/2 Name: create_implication/3 Name: create_equivalence/3 Name: is_equality/3 Name: create_equality/3 Name: split_equality/3 Name: get_texpr_couple/3 Name: create_couple/3 Name: create_couple/2 Name: nested_couple_to_list/2 Name: create_comprehension_set/4 Name: is_eventb_comprehension_set/4 Name: is_eventb_comprehension_set/6 Name: singleton_set_extension/2 Name: is_membership/3 Name: is_membership_or_equality/3 Name: get_lambda_equality/4 Name: is_pow_subset/2 Name: is_pow1_subset/2 Name: detect_global_predicates/4 Name: definitely_not_empty_set/1 Name: definitely_empty_set/1 Name: definitely_not_empty_finite_value/1 Name: get_integer/2 Name: get_interval/3 Name: replace_id_by_expr/4 Name: replace_id_by_expr_with_count/5 Name: replace_ids_by_exprs/4 Name: remove_used_id_from_info/3 Name: remove_used_ids_from_info/3 Name: rename_bt/3 Name: rename_bt_l/3 Name: remove_bt/4 Name: syntaxtransformation/5 Name: syntaxtransformation_det/5 Name: map_over_bexpr/2 Name: map_over_typed_bexpr/2 Name: map_over_typed_bexpr/3 Name: map_over_typed_bexpr_with_names/2 Name: map_over_bexpr_top_down_acc/3 Name: map_over_typed_bexpr_top_down_acc/3 Name: reduce_over_bexpr/4 Name: transform_bexpr/3 Name: transform_bexpr_with_scoping/3 Name: transform_bexpr_td_with_scoping/3 Name: transform_bexpr_with_bup_accs/5 Name: transform_bexpr_with_acc/5 Name: non_det_transform_bexpr_with_acc/5 Name: uses_implementable_integers/1 Name: min_max_integer_value_used/3 Name: min_max_integer_value_used/5 Name: syntaxtraversion/6 Name: safe_syntaxelement/5 Name: safe_syntaxelement_det/5 Name: is_subst_syntaxelement/1 Name: is_syntax_constant/1 Name: remove_all_infos/2 Name: extract_info/2 Name: extract_info/3 Name: extract_info_wo_used_ids/2 Name: bsyntax_pattern/2 Name: remove_all_infos_and_ground/2 Name: check_if_typed_predicate/1 Name: check_if_typed_expression/1 Name: check_if_typed_substitution/1 Name: strip_and_norm_ast/2 Name: same_norm_texpr/2 Name: get_texpr_functor/3 Name: is_set_type/2 Name: get_set_type/2 Name: get_texpr_set_type/2 Name: is_just_type/1 Name: is_just_type/2 Name: create_recursive_compset/6 Name: unique_typed_id/3 Name: mark_bexpr_as_symbolic/2 Name: identifier_sub_ast/3 Name: exchange_ast_position/5 Name: has_declared_identifier/2 Name: add_declaration_for_identifier/3 Name: check_ast/1 Name: check_ast/2 Name: repair_used_ids/3 Name: print_ast/1 Name: rewrite_if_then_else_expr_to_b/2

Imports

Exports

Name: module_info/2

Module: module_information

Name: print_bexpr/1

Module: translate

Name: translate_bexpression/2

Module: translate

Name: gensym/2

Module: gensym

Name: get_preference/2

Module: preferences

Name: preference/2

Module: preferences

Name: debug_mode/1

Module: debug

Name: debug_format/3

Module: debug

Name: is_finite_type_in_context/2

Module: typing_tools

Name: normalize_type/2

Module: typing_tools

Name: convlist_max/4

Module: tools_lists

Name: check_unique_in_domain_of_avlset/2

Module: custom_explicit_sets

Name: ground_value/1

Module: kernel_tools

Name: is_provably_finite_type/1

Module: typing_tools

Name: type_has_at_least_two_elements/1

Module: typing_tools

Name: b_non_empty_global_set/1

Module: b_global_sets

Name: avl_is_interval/3

Module: custom_explicit_sets

Name: safe_sort/3

Module: tools

Name: bmachine_is_precompiled/0

Module: bmachine

Name: b_is_variable/2

Module: bmachine

Name: b_is_constant/2

Module: bmachine

Name: debug_println/2

Module: debug

Name: b_get_global_constants/1

Module: b_global_sets

Name: b_get_enumerated_set_constants/1

Module: b_global_sets

Name: b_get_global_sets/1

Module: b_global_sets

Name: prime_identifiers/2

Module: btypechecker

Name: safe_univ_no_cutoff/2

Module: tools

Name: valid_ground_type/1

Module: typing_tools

Name: lookup_type_for_expr/2

Module: btypechecker

Name: unify_types_werrors/4

Module: btypechecker

Name: eventb_mode/0

Module: specfile

Name: z_or_tla_minor_mode/0

Module: specfile

Name: avl_min_pair/3

Module: avl_tools

Name: check_used_ids_info/4

Module: b_ast_cleanup

Name: unify_types_strict/2

Module: btypechecker

Name: couplise_list/2

Module: btypechecker

Name: check_is_non_empty_avl/1

Module: avl_tools

Name: is_texpr/1

Name: get_texpr_expr/2

Name: get_texpr_type/2

Name: get_texpr_info/2

Name: get_texpr_id/2

Name: def_get_texpr_id/2

Name: def_get_texpr_ids/2

Name: create_typed_id/3

Name: same_id/3

Name: same_ids/2

Name: same_ids_and_types/2

Name: split_names_and_types/3

Name: get_texpr_exprs/2

Name: get_texpr_types/2

Name: get_texpr_infos/2

Name: get_texpr_ids/2

Name: get_texpr_pos/2

Name: extract_pos_infos/2

Name: copy_pos_infos/3

Name: delete_pos_info/2

Name: propagate_pos_info_if_useful/3

Name: merge_info/3

Name: update_infos/3

Name: get_info_pos/2

Name: contains_info_pos/1

Name: same_texpr/2

Name: different_texpr_values/2

Name: create_texpr/4

Name: add_texpr_infos/3

Name: add_texpr_info_if_new/3

Name: add_texpr_infos_if_new/3

Name: add_info_if_new/3

Name: add_infos_if_new/3

Name: safe_create_texpr/3

Name: safe_create_texpr/4

Name: texpr_contains_wd_condition/1

Name: sub_expression_contains_wd_condition/1

Name: get_rodin_name/2

Name: get_rodin_model_name/2

Name: is_rodin_label_info/1

Name: get_texpr_label/2

Name: get_texpr_labels/2

Name: get_info_labels/2

Name: select_info_labels/3

Name: add_labels_to_texpr/3

Name: get_texpr_description/2

Name: add_texpr_description/3

Name: info_has_ignore_pragma/1

Name: predicate_has_ignore_pragma/1

Name: always_well_defined/1

Name: always_well_defined_or_disprover_mode/1

Name: always_well_defined_or_wd_reorderings_allowed/1

Name: always_well_defined_or_wd_improvements_allowed/1

Name: finite_wd_set_value/1

Name: finite_set_or_disprover_mode/1

Name: is_truth/1

Name: is_falsity/1

Name: conjunct_predicates/2

Name: conjunct_predicates_with_pos_info/3

Name: conjunct_predicates_with_pos_info/2

Name: is_a_conjunct/3

Name: is_a_conjunct_without_label/3

Name: decompose_conjunct/3

Name: is_a_disjunct/3

Name: is_an_implication/3

Name: is_an_equivalence/3

Name: is_a_negation/2

Name: conjunction_to_list/2

Name: conjunction_to_list_with_rodin_labels/2

Name: member_in_conjunction/2

Name: select_member_in_conjunction/3

Name: flatten_conjunctions/2

Name: size_of_conjunction/2

Name: member_in_conjunction_cse/3

Name: disjunct_predicates/2

Name: disjunct_predicates_with_pos_info/3

Name: disjunction_to_list/2

Name: is_a_disjunct_or_implication/4

Name: is_a_conjunct_or_neg_disj/3

Name: predicate_components/2

Name: predicate_components_in_scope/3

Name: predicate_components_with_restriction/4

Name: predicate_identifiers/2

Name: predicate_identifiers_in_scope/3

Name: project_predicate_on_identifiers/5

Name: find_identifier_uses_top_level/2

Name: find_identifier_uses/3

Name: find_identifier_uses_if_necessary/3

Name: find_identifier_uses_l/3

Name: find_typed_identifier_uses/3

Name: find_typed_identifier_uses/2

Name: find_typed_identifier_uses_l/3

Name: get_global_identifiers/1

Name: get_global_identifiers/2

Name: occurs_in_expr/2

Name: some_id_occurs_in_expr/2

Name: single_usage_identifier/3

Name: update_used_ids/3

Name: check_computed_used_ids/2

Name: create_exists/3

Name: create_or_merge_exists/3

Name: create_exists_or_let_predicate/3

Name: create_exists_opt_liftable/3

Name: create_exists_opt/3

Name: create_exists_opt/4

Name: create_exists_opt/5

Name: create_forall/3

Name: create_negation/2

Name: is_negation_of/2

Name: get_negated_operator_expr/2

Name: create_implication/3

Name: create_equivalence/3

Name: is_equality/3

Name: create_equality/3

Name: split_equality/3

Name: get_texpr_couple/3

Name: create_couple/3

Name: create_couple/2

Name: nested_couple_to_list/2

Name: create_comprehension_set/4

Name: is_eventb_comprehension_set/4

Name: is_eventb_comprehension_set/6

Name: singleton_set_extension/2

Name: is_membership/3

Name: is_membership_or_equality/3

Name: get_lambda_equality/4

Name: is_pow_subset/2

Name: is_pow1_subset/2

Name: detect_global_predicates/4

Name: definitely_not_empty_set/1

Name: definitely_empty_set/1

Name: definitely_not_empty_finite_value/1

Name: get_integer/2

Name: get_interval/3

Name: replace_id_by_expr/4

Name: replace_id_by_expr_with_count/5

Name: replace_ids_by_exprs/4

Name: remove_used_id_from_info/3

Name: remove_used_ids_from_info/3

Name: rename_bt/3

Name: rename_bt_l/3

Name: remove_bt/4

Name: syntaxtransformation/5

Name: syntaxtransformation_det/5

Name: map_over_bexpr/2

Name: map_over_typed_bexpr/2

Name: map_over_typed_bexpr/3

Name: map_over_typed_bexpr_with_names/2

Name: map_over_bexpr_top_down_acc/3

Name: map_over_typed_bexpr_top_down_acc/3

Name: reduce_over_bexpr/4

Name: transform_bexpr/3

Name: transform_bexpr_with_scoping/3

Name: transform_bexpr_td_with_scoping/3

Name: transform_bexpr_with_bup_accs/5

Name: transform_bexpr_with_acc/5

Name: non_det_transform_bexpr_with_acc/5

Name: uses_implementable_integers/1

Name: min_max_integer_value_used/3

Name: min_max_integer_value_used/5

Name: syntaxtraversion/6

Name: safe_syntaxelement/5

Name: safe_syntaxelement_det/5

Name: is_subst_syntaxelement/1

Name: is_syntax_constant/1

Name: remove_all_infos/2

Name: extract_info/2

Name: extract_info/3

Name: extract_info_wo_used_ids/2

Name: bsyntax_pattern/2

Name: remove_all_infos_and_ground/2

Name: check_if_typed_predicate/1

Name: check_if_typed_expression/1

Name: check_if_typed_substitution/1

Name: strip_and_norm_ast/2

Name: same_norm_texpr/2

Name: get_texpr_functor/3

Name: is_set_type/2

Name: get_set_type/2

Name: get_texpr_set_type/2

Name: is_just_type/1

Name: is_just_type/2

Name: create_recursive_compset/6

Name: unique_typed_id/3

Name: mark_bexpr_as_symbolic/2

Name: identifier_sub_ast/3

Name: exchange_ast_position/5

Name: has_declared_identifier/2

Name: add_declaration_for_identifier/3

Name: check_ast/1

Name: check_ast/2

Name: repair_used_ids/3

Name: print_ast/1

Name: rewrite_if_then_else_expr_to_b/2

Predicates

Predicates:

add_declaration_for_identifier/3

add_info/3

add_info_if_new/3

add_infos_if_new/3

add_labels_to_texpr/3

add_non_default_declaration/3

add_rodin_label_info/3

add_symbolic_annotation/2

add_texpr_description/3

add_texpr_info_if_new/3

add_texpr_infos/3

add_texpr_infos_if_new/3

always_wd_avl_function/2

always_well_defined/1

always_well_defined_or_discharged/1

always_well_defined_or_disprover_mode/1

always_well_defined_or_wd_improvements_allowed/1

always_well_defined_or_wd_reorderings_allowed/1

apply_rename_list_to_ids/4

ceo_filter_used_ids/3

check_computed_used_ids/2

check_expr/3

check_ids/2

check_ids3/3

check_if_typed_expression/1

check_if_typed_predicate/1

check_if_typed_substitution/1

check_special_rules/3

check_used_ids_in_ast/1

check_used_ids_texpr/2

check_used_ids_texpr_fail/2

comm_assoc_subs/4

conjunct2/3

conjunct3/3

conjunct_predicates/2

conjunct_predicates_with_pos_info/2

conjunct_predicates_with_pos_info/3

conjunction_to_list/2

conjunction_to_list2/3

conjunction_to_list_with_labels2/3

conjunction_to_list_with_rodin_labels/2

create_comprehension_set/4

create_exists_detect_tautology_aux/4

create_exists_opt_liftable/3

create_exists_or_let_predicate/3

create_filtered_exists/6

create_forall/3

create_implication/3

create_negation/2

create_negation_aux/3

create_or_merge_exists/3

create_recursive_compset/6

default_declaration/4

definitely_empty_set/1

definitely_not_empty_finite_value/1

definitely_not_empty_seq/1

definitely_not_empty_set/1

definitely_not_non_empty_sequence/1

definitely_not_sequence/1

delete_pos_info/2

derived_pos/1

detect_global_predicates/4

different_texpr_values/2

disjunct_predicates/2

disjunct_predicates_with_pos_info/3

disjunction_to_list/2

disjunction_to_list2/3

exchange_ast_position/5

exists_ast/1

extract_all_predicates/7

extract_found_predicate/2

extract_imp_info1/2

extract_info/2

extract_info/3

extract_info_wo_used_ids/2

extract_info_wo_used_ids_and_pos/3

extract_just_important_info_aux/3

extract_pos_infos/2

field_is_just_type/2

find_and_remove_equalities/2

find_components/3

find_identifier_uses/3

find_identifier_uses_for_quantifier_body/3

find_identifier_uses_if_necessary/3

find_identifier_uses_l/3

find_identifier_uses_top_level/2

find_rhs_ids/2

find_typed_identifier_uses/2

find_typed_identifier_uses/3

find_typed_identifier_uses2/4

find_typed_identifier_uses2_l/4

find_typed_identifier_uses_l/3

find_variable_clashes/3

finite_set_or_disprover_mode/1

finite_wd_seq_value/1

finite_wd_set_value/1

flatten_conj_aux/3

flatten_conjunctions/2

gen_fresh_id_if_necessary/3

generate_rename_list/3

get_global_identifiers/1

get_global_identifiers/2

get_lambda_equality/4

get_negated_operator_expr/2

get_non_label_posinfo/2

get_rodin_model_name/2

get_rodin_name/2

get_set_type/2

get_texpr_couple/3

get_texpr_description/2

get_texpr_non_label_posinfo/2

has_declared_identifier/2

has_info_to_rename/1

identifier_equality/3

identifier_sub_ast/3

identifier_sub_ast_aux/5

identifier_sub_ast_aux2/3

illegal_id/1

important_info/1

indent_ws/1

indirectly_uses_identifiers/3

info_has_ignore_pragma/1

info_label/2

infos_to_rename/4

is_a_conjunct/3

is_a_conjunct_or_neg_disj/3

is_a_conjunct_without_label/3

is_a_disj_or_impl_aux/4

is_a_disjunct/3

is_a_disjunct_or_implication/4

is_eventb_comprehension_set/4

is_eventb_comprehension_set/6

is_membership_or_equality/3

is_negation_aux/2

is_negation_of/2

is_negation_of_disequality/3

is_negation_of_equality/3

is_pow1_subset/2

is_pow_subset/2

is_rodin_label_info/1

is_selected_predicate/1

is_set_type/2

is_subst_syntaxelement/1

l_always_well_defined/1

l_apply_rename_list/3

l_field_occurs_in_expr1/2

l_find_rhs_ids/2

l_nd_transform_bexpr_with_acc/5

l_occurs_in_expr1/2

l_predicate_identifiers/3

l_replace_id_by_expr2/8

l_replace_ids_by_exprs2/5

l_transform_bexpr/3

l_transform_bexpr_td_with_scoping/4

l_transform_bexpr_with_acc/5

l_transform_bexpr_with_bup_accs/5

l_transform_bexpr_with_scoping/4

last_non_truth/3

lookup_type/2

map_over_bexpr/2

map_over_bexpr_top_down_acc/3

map_over_full_bexpr_no_fail/2

map_over_typed_bexpr/2

map_over_typed_bexpr/3

map_over_typed_bexpr_top_down_acc/3

map_over_typed_bexpr_with_names/2

mark_aux/2

mark_bexpr_as_symbolic/2

member_in_conjunction/2

member_in_conjunction_cse/3

min_max_integer_value_used/3

min_max_integer_value_used/5

neg_bool_aux/2

neg_value/2

negate/2

negate_boolean_value/2

negate_expr_aux/2

nested_couple_to_list/2

nested_couple_to_list_dcg/3

nodeid_info_label/2

non_default_declaration/2

non_det_transform_bexpr_with_acc/5

non_empty_fin_wd_set2/1

non_empty_finite_wd_set_value/1

non_empty_seq2/1

non_empty_set/1

non_empty_wd_seq_value/1

ord_delete_existing_element/3

ord_restrict/3

parse_expr/2

parse_pred/2

predicate_components/2

predicate_components_in_scope/3

predicate_components_with_restriction/4

predicate_has_ignore_pragma/1

predicate_identifiers/2

predicate_identifiers_in_scope/3

print_ast/1

print_ast_td/3

project_predicate_on_identifiers/5

propagate_pos_info_if_useful/3

reduce_over_bexpr/4

remove_all_infos/2

remove_all_infos_and_ground/2

remove_all_infos_from_bvalue/2

remove_bt/4

remove_bt_and_used_ids/4

remove_hidden_names/3

remove_renamings/3

remove_used_id_from_info/3

remove_used_ids_from_info/3

rename_update_used_ids_info/3

repair_used_ids/3

repair_used_ids_info/3

replace_id_by_expr/4

replace_id_by_expr2/8

replace_id_by_expr_with_count/5

replace_ids_by_exprs/4

replace_ids_by_exprs2/5

requires_used_ids/1

rewrite_if_then_else_expr_to_b/2

safe_syntaxelement_det/5

same_sub_expressions/2

same_texpr/2

select_all_using_preds/3

select_info_labels/3

select_member_in_conjunction/3

single_usage_id_count/1

single_usage_identifier/3

singleton_set_extension/2

singleton_set_extension_aux/3

size_of_conjunction/2

size_of_conjunction/3

some_id_occurs_in_expr/2

split_equality/3

split_forall_body/3

split_names_and_types/3

split_predicate_local_global/4

strip_and_norm_ast/2

strip_and_norm_ast_aux/2

strip_and_norm_ast_l/2

sub_expression_contains_wd_condition/1

sub_expression_contains_wd_condition/2

syntaxelement/6

syntaxfields/3

syntaxtransformation/5

syntaxtransformation_det/5

syntaxtraversion/6

test_result/2

texpr_contains_wd_condition/1

transform_bexpr/3

transform_bexpr_td_with_scoping/3

transform_bexpr_td_with_scoping2/4

transform_bexpr_with_acc/5

transform_bexpr_with_bup_accs/5

transform_bexpr_with_scoping/3

transform_bexpr_with_scoping2/4

try_find_and_remove_equalities/2

try_get_merged_position_info/3

try_get_merged_position_info_aux/3

unique_typed_id/3

update_id/4

update_id_from_info_field/4

update_id_from_info_field2/4

update_infos/3

update_used_ids/3

update_used_ids/4

update_used_ids_info/4

used_ids_like_info/3

uses_an_identifier/2

uses_an_identifier/4

uses_implementable_integers/1

uses_implementable_integers_aux/1

value_which_can_be_replaced/1

value_which_can_be_replaced2/2

var_cst_type/2

add_declaration_for_identifier/3

add_info/3

add_info_if_new/3

add_infos_if_new/3

add_labels_to_texpr/3

add_non_default_declaration/3

add_rodin_label_info/3

add_symbolic_annotation/2

add_texpr_description/3

add_texpr_info_if_new/3

add_texpr_infos/3

add_texpr_infos_if_new/3

always_wd(power_of(X,Y)) :- get_integer(Y,Val), Val>=0,
    (eventb_mode -> get_integer(X,ValX), ValX >=0
    ; always_well_defined(X)).

always_wd(div(X,Y)) :- get_integer(Y,Val), Val\=0, always_well_defined(X).

always_wd(modulo(X,Y)) :- get_integer(Y,Val), Val>0, % Z Live allows negative numbers here it seems, cf modulo2
    (z_or_tla_minor_mode -> true % in Z, TLA we can have negative numbers here
    ; get_integer(X,ValX), ValX>=0).

always_wd(function(X,Y)) :- nonvar(X),
    X= b(value(AVLSET),_,_), nonvar(AVLSET), AVLSET=avl_set(AVL),
    always_wd_avl_function(AVL,Y).

always_wd(min(X)) :- non_empty_finite_wd_set_value(X).

always_wd(max(X)) :- non_empty_finite_wd_set_value(X).

always_wd(card(X)) :- finite_wd_set_value(X).

always_wd(size(X)) :- finite_wd_seq_value(X).

always_wd(first(X)) :- non_empty_wd_seq_value(X).

always_wd(front(X)) :- non_empty_wd_seq_value(X).

always_wd(last(X)) :- non_empty_wd_seq_value(X).

always_wd(tail(X)) :- non_empty_wd_seq_value(X). % TO DO: add restrict_front, restrict_tail ?

always_wd(general_intersection(X)) :- non_empty_finite_wd_set_value(X).

always_wd(value(_)). % we have already computed the value and will raise WD error; to be 100 % safe we could restrict this to ground values

always_wd(typeset).

always_wd(record_field(RecEx,FieldName)) :- ground(FieldName),
    always_well_defined(RecEx).

always_wd(unary_minus(A)) :- always_well_defined(A).

always_wd(unary_minus_real(A)) :- always_well_defined(A).

always_wd(first_of_pair(A)) :- always_well_defined(A).

always_wd(add(A,B)) :- always_well_defined(A),always_well_defined(B).

always_wd(add_real(A,B)) :- always_well_defined(A),always_well_defined(B).

always_wd(minus(A,B)) :- always_well_defined(A),always_well_defined(B).

always_wd(minus_real(A,B)) :- always_well_defined(A),always_well_defined(B).

always_wd(multiplication(A,B)) :- always_well_defined(A),always_well_defined(B).

always_wd(multiplication_real(A,B)) :- always_well_defined(A),always_well_defined(B).

always_wd(equal(A,B)) :- always_well_defined(A),always_well_defined(B).

always_wd(not_equal(A,B)) :- always_well_defined(A),always_well_defined(B).

always_wd(less_equal(A,B)) :- always_well_defined(A),always_well_defined(B).

always_wd(less_equal_real(A,B)) :- always_well_defined(A),always_well_defined(B).

always_wd(greater_equal(A,B)) :- always_well_defined(A),always_well_defined(B).

always_wd(less(A,B)) :- always_well_defined(A),always_well_defined(B).

always_wd(less_real(A,B)) :- always_well_defined(A),always_well_defined(B).

always_wd(greater(A,B)) :- always_well_defined(A),always_well_defined(B).

always_wd(couple(A,B)) :- always_well_defined(A),always_well_defined(B).

always_wd_avl_function/2

always_well_defined/1

always_well_defined_or_discharged/1

always_well_defined_or_disprover_mode/1

always_well_defined_or_wd_improvements_allowed/1

always_well_defined_or_wd_reorderings_allowed/1

apply_rename_list_to_ids/4

ceo_filter_used_ids/3

check_computed_used_ids/2

check_expr/3

check_ids/2

check_ids3/3

check_if_typed_expression/1

check_if_typed_predicate/1

check_if_typed_substitution/1

check_special_rules/3

Description:
comment in to check used_ids field

check_used_ids/2

check_used_ids_aux/1

check_used_ids_in_ast/1

check_used_ids_texpr/2

check_used_ids_texpr_fail/2

comm_assoc_subs/4

conjunct2/3

conjunct3/3

conjunct_predicates/2

conjunct_predicates_with_pos_info/2

conjunct_predicates_with_pos_info/3

conjunction_to_list/2

conjunction_to_list2/3

conjunction_to_list_with_labels2/3

conjunction_to_list_with_rodin_labels/2

create_comprehension_set/4

create_exists_detect_tautology_aux/4

create_exists_opt_liftable/3

create_exists_or_let_predicate/3

create_filtered_exists/6

create_forall/3

create_implication/3

create_negation/2

create_negation_aux/3

create_or_merge_exists/3

create_recursive_compset/6

default_declaration/4

definitely_empty_set/1

definitely_not_empty_finite_value/1

definitely_not_empty_seq/1

definitely_not_empty_set/1

definitely_not_non_empty_sequence/1

definitely_not_sequence/1

delete_pos_info/2

derived_pos/1

detect_global_predicates/4

different_texpr_values/2

disjunct_predicates/2

disjunct_predicates_with_pos_info/3

disjunction_to_list/2

disjunction_to_list2/3

exchange_ast_position/5

exists_ast/1

extract_all_predicates/7

extract_found_predicate/2

extract_imp_info1/2

extract_info/2

extract_info/3

extract_info_wo_used_ids/2

extract_info_wo_used_ids_and_pos/3

extract_just_important_info_aux/3

extract_pos_infos/2

field_is_just_type/2

find_and_remove_equalities/2

find_components/3

find_identifier_uses/3

find_identifier_uses_for_quantifier_body/3

find_identifier_uses_if_necessary/3

find_identifier_uses_l/3

find_identifier_uses_top_level/2

find_rhs_ids/2

find_typed_identifier_uses/2

find_typed_identifier_uses/3

find_typed_identifier_uses2/4

find_typed_identifier_uses2_l/4

find_typed_identifier_uses_l/3

find_variable_clashes/3

finite_set_or_disprover_mode/1

finite_wd_seq_value/1

finite_wd_set_value/1

flatten_conj_aux/3

flatten_conjunctions/2

gen_fresh_id_if_necessary/3

generate_rename_list/3

get_global_identifiers/1

get_global_identifiers/2

get_lambda_equality/4

get_negated_operator_expr/2

get_non_label_posinfo/2

get_rodin_model_name/2

get_rodin_name/2

get_set_type/2

get_texpr_couple/3

get_texpr_description/2

Description:
get_texpr_id(+Texpr,-Id)

get_texpr_non_label_posinfo/2

has_declared_identifier/2

has_info_to_rename/1

identifier_equality/3

identifier_sub_ast/3

identifier_sub_ast_aux/5

identifier_sub_ast_aux2/3

illegal_id/1

important_info/1

indent_ws/1

indirectly_uses_identifiers/3

info_has_ignore_pragma/1

info_label/2

infos_to_rename/4

is_a_conjunct/3

is_a_conjunct_or_neg_disj/3

is_a_conjunct_without_label/3

is_a_disj_or_impl_aux/4

is_a_disjunct/3

is_a_disjunct_or_implication/4

is_eventb_comprehension_set/4

is_eventb_comprehension_set/6

is_membership_or_equality/3

is_negation_aux/2

is_negation_of/2

is_negation_of_disequality/3

is_negation_of_equality/3

is_pow1_subset/2

is_pow_subset/2

is_rodin_label_info/1

is_selected_predicate/1

is_set_type/2

is_subst_syntaxelement/1

l_always_well_defined/1

l_apply_rename_list/3

l_field_occurs_in_expr1/2

l_find_rhs_ids/2

l_nd_transform_bexpr_with_acc/5

Meta: l_nd_transform_bexpr_with_acc(?,4,?,?,?)

l_occurs_in_expr1/2

l_predicate_identifiers/3

l_replace_id_by_expr2/8

l_replace_ids_by_exprs2/5

l_transform_bexpr/3

Meta: l_transform_bexpr(?,2,?)

l_transform_bexpr_td_with_scoping/4

l_transform_bexpr_with_acc/5

Meta: l_transform_bexpr_with_acc(?,4,?,?,?)

l_transform_bexpr_with_bup_accs/5

Meta: l_transform_bexpr_with_bup_accs(?,4,?,?,?)

l_transform_bexpr_with_scoping/4

Meta: l_transform_bexpr_with_scoping(?,3,?,?)

last_non_truth/3

lookup_type/2

map_over_bexpr/2

Meta: map_over_bexpr(1,?)

map_over_bexpr_top_down_acc/3

Meta: map_over_bexpr_top_down_acc(3,?,?)

map_over_full_bexpr_no_fail/2

Meta: map_over_full_bexpr_no_fail(1,?)

map_over_typed_bexpr/2

Meta: map_over_typed_bexpr(1,?)

map_over_typed_bexpr/3

Meta: map_over_typed_bexpr(2,?,?)

map_over_typed_bexpr_top_down_acc/3

Meta: map_over_typed_bexpr_top_down_acc(3,?,?)

map_over_typed_bexpr_with_names/2

mark_aux/2

mark_bexpr_as_symbolic/2

member_in_conjunction/2

member_in_conjunction_cse/3

min_max_integer_value_used/3

min_max_integer_value_used/5

neg_bool_aux/2

neg_value/2

negate/2

negate_boolean_value/2

negate_expr_aux/2

nested_couple_to_list/2

nested_couple_to_list_dcg/3

nodeid_info_label/2

non_default_declaration/2

non_det_transform_bexpr_with_acc/5

Meta: non_det_transform_bexpr_with_acc(4,?,?,?,?)

non_empty_fin_wd_set2/1

non_empty_finite_wd_set_value/1

non_empty_seq2/1

non_empty_set/1

non_empty_wd_seq_value/1

occurs_in_expr2(add(A,B),_,ID) :- !,
    (occurs_in_expr1(A,ID) -> true ; occurs_in_expr1(B,ID)).

occurs_in_expr2(conjunct(A,B),_,ID) :- !,
    (occurs_in_expr1(A,ID) -> true ; occurs_in_expr1(B,ID)).

occurs_in_expr2(couple(A,B),_,ID) :- !,
    (occurs_in_expr1(A,ID) -> true ; occurs_in_expr1(B,ID)).

occurs_in_expr2(member(A,B),_,ID) :- !,
    (occurs_in_expr1(A,ID) -> true ; occurs_in_expr1(B,ID)).

occurs_in_expr2(equal(A,B),_,ID) :- !,
    (occurs_in_expr1(A,ID) -> true ; occurs_in_expr1(B,ID)).

occurs_in_expr2(function(A,B),_,ID) :- !,
    (occurs_in_expr1(A,ID) -> true ; occurs_in_expr1(B,ID)).

occurs_in_expr2(image(A,B),_,ID) :- !,
    (occurs_in_expr1(A,ID) -> true ; occurs_in_expr1(B,ID)).

occurs_in_expr2(intersection(A,B),_,ID) :- !,
    (occurs_in_expr1(A,ID) -> true ; occurs_in_expr1(B,ID)).

occurs_in_expr2(interval(A,B),_,ID) :- !,
    (occurs_in_expr1(A,ID) -> true ; occurs_in_expr1(B,ID)).

occurs_in_expr2(not_equal(A,B),_,ID) :- !,
    (occurs_in_expr1(A,ID) -> true ; occurs_in_expr1(B,ID)).

occurs_in_expr2(assertion_expression(A,_Msg,B),_,ID) :- !,
    (occurs_in_expr1(A,ID) -> true ; occurs_in_expr1(B,ID)).

occurs_in_expr2(domain(A),_,ID) :- !, occurs_in_expr1(A,ID).

occurs_in_expr2(range(A),_,ID) :- !, occurs_in_expr1(A,ID).

occurs_in_expr2(record_field(A,_FieldName),_,ID) :- !, occurs_in_expr1(A,ID).

occurs_in_expr2(identifier(ID1),_,ID) :- !,
    ID1 = ID.

occurs_in_expr2(integer(_),_,_ID) :- !,fail.

occurs_in_expr2(string(_),_,_ID) :- !,fail.

occurs_in_expr2(value(_),_,_ID) :- !,fail.

occurs_in_expr2(truth,_,_ID) :- !,fail.

occurs_in_expr2(if_then_else(A,B,C),_,ID) :- !,
    (occurs_in_expr1(A,ID) -> true ; occurs_in_expr1(B,ID) -> true ; occurs_in_expr1(C,ID)).

occurs_in_expr2(rec(Fields),_,ID) :- !,
    l_field_occurs_in_expr1(Fields,ID).

occurs_in_expr2(set_extension(Elements),_,ID) :- !,
    l_occurs_in_expr1(Elements,ID).

occurs_in_expr2(sequence_extension(Elements),_,ID) :- !,
    l_occurs_in_expr1(Elements,ID).

occurs_in_expr2(Expr,_,ID) :-
    syntaxelement(Expr,List,[], [], [], _), % no bound quantifiers; TO DO: treat bound quantifiers
    !,
    l_occurs_in_expr1(List,ID).

occurs_in_expr2(_E,TExpr,ID) :-
    %functor(_E,F,N), print(occurs_in_expr2(F,N,ID)),nl,
    (find_identifier_uses_if_necessary(TExpr,[],Used)
    -> %check_sorted(Used),
    %add_message(bsyntaxtree,'Occurs check: ',ID:Used,TExpr), translate:nested_print_bexpr(TExpr),nl,
    ord_member(ID,Used)
    ; add_failed_call_error(find_identifier_uses(TExpr,[],_)),fail).

ord_delete_existing_element/3

ord_restrict/3

parse_expr/2

parse_pred/2

predicate_components/2

predicate_components_in_scope/3

predicate_components_with_restriction/4

Description:
(member(pred(P,Ids,X),PredIds2), nl,print(pred(Ids,X)),nl,translate:print_bexpr(P),nl,fail ; true),

predicate_has_ignore_pragma/1

predicate_identifiers/2

predicate_identifiers_in_scope/3

print_ast/1

print_ast_td/3

project_predicate_on_identifiers/5

propagate_pos_info_if_useful/3

reduce_over_bexpr/4

Meta: reduce_over_bexpr(3,?,?,?)

remove_all_infos/2

remove_all_infos_and_ground/2

remove_all_infos_from_bvalue/2

remove_bt/4

remove_bt_and_used_ids/4

remove_hidden_names/3

remove_renamings/3

remove_used_id_from_info/3

remove_used_ids_from_info/3

rename_update_used_ids_info/3

repair_used_ids/3

repair_used_ids_info/3

replace_id_by_expr/4

replace_id_by_expr2/8

replace_id_by_expr_with_count/5

replace_ids_by_exprs/4

replace_ids_by_exprs2/5

requires_used_ids/1

rewrite_if_then_else_expr_to_b/2

Description:
rewrite_if_then_else_expr_to_b(IfThenElseExpr, NExpr).

safe_syntaxelement_det/5

same_sub_expressions/2

same_texpr/2

select_all_using_preds/3

select_info_labels/3

select_member_in_conjunction/3

single_usage_id_count/1

single_usage_identifier/3

singleton_set_extension/2

singleton_set_extension_aux/3

size_of_conjunction/2

size_of_conjunction/3

some_id_occurs_in_expr/2

split_equality/3

split_forall_body/3

split_names_and_types/3

split_predicate_local_global/4

strip_and_norm_ast/2

strip_and_norm_ast_aux/2

strip_and_norm_ast_l/2

sub_expression_contains_wd_condition/1

sub_expression_contains_wd_condition/2

syntaxelement/6

syntaxelement(truth, [], [], [], [], pred).

syntaxelement(falsity, [], [], [], [], pred).

syntaxelement(unknown_truth_value(Msg),[], [], [], Msg, pred). % artificial, e.g., created by well_def_analyser

syntaxelement(conjunct(A,B), [A,B],[], [], [], pred).

syntaxelement(negation(A), [A], [], [], [], pred).

syntaxelement(disjunct(A,B), [A,B],[], [], [], pred).

syntaxelement(implication(A,B), [A,B],[], [], [], pred).

syntaxelement(equivalence(A,B), [A,B],[], [], [], pred).

syntaxelement(equal(A,B), [A,B],[], [], [], pred).

syntaxelement(not_equal(A,B), [A,B],[], [], [], pred).

syntaxelement(member(A,B), [A,B],[], [], [], pred).

syntaxelement(not_member(A,B), [A,B],[], [], [], pred).

syntaxelement(subset(A,B), [A,B],[], [], [], pred).

syntaxelement(subset_strict(A,B), [A,B],[], [], [], pred).

syntaxelement(not_subset(A,B), [A,B],[], [], [], pred).

syntaxelement(not_subset_strict(A,B),[A,B],[], [], [], pred).

syntaxelement(less_equal(A,B), [A,B],[], [], [], pred).

syntaxelement(less(A,B), [A,B],[], [], [], pred).

syntaxelement(less_equal_real(A,B), [A,B],[], [], [], pred).

syntaxelement(less_real(A,B), [A,B],[], [], [], pred).

syntaxelement(greater_equal(A,B), [A,B],[], [], [], pred).

syntaxelement(greater(A,B), [A,B],[], [], [], pred).

syntaxelement(forall(Ids,D,P), [D,P|Ids],Ids,[Ids], [], pred).

syntaxelement(exists(Ids,P), [P|Ids], Ids,[Ids], [], pred).

syntaxelement(finite(A), [A], [], [], [], pred/only_typecheck).

syntaxelement(partition(S,Es), [S|Es],[],[Es],[],pred).

syntaxelement(kodkod(PId,Ids), Ids,[],[Ids],PId, pred).

syntaxelement(external_pred_call(F,Args),Args,[],[Args],F,pred).

syntaxelement(value(V), [], [], [], V, expr).

syntaxelement(operation_call_in_expr(Id,As), As, [], [As], Id, expr). % Do not treat Id as a sub-expression for find_identifier_uses, ...

syntaxelement(boolean_true, [], [], [], [], expr).

syntaxelement(boolean_false, [], [], [], [], expr).

syntaxelement(max_int, [], [], [], [], expr).

syntaxelement(min_int, [], [], [], [], expr).

syntaxelement(empty_set, [], [], [], [], expr).

syntaxelement(bool_set, [], [], [], [], expr).

syntaxelement(float_set, [], [], [], [], expr).

syntaxelement(real(I), [], [], [], I, expr).

syntaxelement(real_set, [], [], [], [], expr).

syntaxelement(string_set, [], [], [], [], expr).

syntaxelement(convert_bool(A), [A], [], [], [], expr).

syntaxelement(convert_real(A), [A], [], [], [], expr).

syntaxelement(convert_int_floor(A), [A], [], [], [], expr).

syntaxelement(convert_int_ceiling(A), [A], [], [], [], expr).

syntaxelement(add(A,B), [A,B],[], [], [], expr).

syntaxelement(add_real(A,B), [A,B],[], [], [], expr).

syntaxelement(minus(A,B), [A,B],[], [], [], expr).

syntaxelement(minus_real(A,B), [A,B],[], [], [], expr).

syntaxelement(minus_or_set_subtract(A,B),[A,B],[], [], [], expr/only_typecheck).

syntaxelement(unary_minus(A), [A], [], [], [], expr).

syntaxelement(unary_minus_real(A), [A], [], [], [], expr).

syntaxelement(multiplication(A,B), [A,B],[], [], [], expr).

syntaxelement(multiplication_real(A,B),[A,B],[], [], [], expr).

syntaxelement(mult_or_cart(A,B), [A,B],[], [], [], expr/only_typecheck).

syntaxelement(cartesian_product(A,B), [A,B],[], [], [], expr).

syntaxelement(div(A,B), [A,B],[], [], [], expr).

syntaxelement(div_real(A,B), [A,B],[], [], [], expr).

syntaxelement(floored_div(A,B), [A,B],[], [], [], expr).

syntaxelement(modulo(A,B), [A,B],[], [], [], expr).

syntaxelement(power_of(A,B), [A,B],[], [], [], expr).

syntaxelement(power_of_real(A,B), [A,B],[], [], [], expr).

syntaxelement(successor, [], [], [], [], expr).

syntaxelement(predecessor, [], [], [], [], expr).

syntaxelement(max(A), [A], [], [], [], expr).

syntaxelement(max_real(A), [A], [], [], [], expr).

syntaxelement(min(A), [A], [], [], [], expr).

syntaxelement(min_real(A), [A], [], [], [], expr).

syntaxelement(card(A), [A], [], [], [], expr).

syntaxelement(couple(A,B), [A,B],[], [], [], expr).

syntaxelement(pow_subset(A), [A], [], [], [], expr).

syntaxelement(pow1_subset(A), [A], [], [], [], expr).

syntaxelement(fin_subset(A), [A], [], [], [], expr).

syntaxelement(fin1_subset(A), [A], [], [], [], expr).

syntaxelement(interval(A,B), [A,B],[], [], [], expr).

syntaxelement(union(A,B), [A,B],[], [], [], expr).

syntaxelement(intersection(A,B), [A,B],[], [], [], expr).

syntaxelement(set_subtraction(A,B), [A,B],[], [], [], expr).

syntaxelement(general_union(A), [A], [], [], [], expr).

syntaxelement(general_intersection(A), [A] , [], [], [], expr).

syntaxelement(relations(A,B), [A,B],[], [], [], expr).

syntaxelement(identity(A), [A], [], [], [], expr).

syntaxelement(event_b_identity, [], [], [], [], expr). % for Rodin 1.0, TO DO: Daniel please check

syntaxelement(reverse(A), [A], [], [], [], expr).

syntaxelement(first_projection(A,B), [A,B],[], [], [], expr/only_typecheck).

syntaxelement(first_of_pair(A), [A], [], [], [], expr).

syntaxelement(event_b_first_projection(A),[A], [], [], [], expr/only_typecheck).

syntaxelement(event_b_first_projection_v2,[], [], [], [], expr/only_typecheck). % for Rodin 1.0, TO DO: Daniel please check

syntaxelement(second_projection(A,B), [A,B],[], [], [], expr/only_typecheck).

syntaxelement(event_b_second_projection_v2,[], [], [], [], expr/only_typecheck). % for Rodin 1.0, TO DO: Daniel please check

syntaxelement(second_of_pair(A), [A], [], [], [], expr).

syntaxelement(event_b_second_projection(A),[A], [], [], [], expr/only_typecheck).

syntaxelement(composition(A,B), [A,B],[], [], [], expr).

syntaxelement(ring(A,B), [A,B],[], [], [], expr/only_typecheck).

syntaxelement(direct_product(A,B), [A,B],[], [], [], expr).

syntaxelement(parallel_product(A,B), [A,B],[], [], [], expr).

syntaxelement(trans_function(A), [A], [], [], [], expr).

syntaxelement(trans_relation(A), [A], [], [], [], expr).

syntaxelement(iteration(A,B), [A,B],[], [], [], expr).

syntaxelement(reflexive_closure(A), [A], [], [], [], expr).

syntaxelement(closure(A), [A], [], [], [], expr).

syntaxelement(domain(A), [A], [], [], [], expr).

syntaxelement(range(A), [A], [], [], [], expr).

syntaxelement(image(A,B), [A,B],[], [], [], expr).

syntaxelement(domain_restriction(A,B), [A,B],[], [], [], expr).

syntaxelement(domain_subtraction(A,B), [A,B],[], [], [], expr).

syntaxelement(range_restriction(A,B), [A,B],[], [], [], expr).

syntaxelement(range_subtraction(A,B), [A,B],[], [], [], expr).

syntaxelement(overwrite(A,B), [A,B],[], [], [], expr).

syntaxelement(partial_function(A,B), [A,B],[], [], [], expr).

syntaxelement(total_function(A,B), [A,B],[], [], [], expr).

syntaxelement(partial_injection(A,B), [A,B],[], [], [], expr).

syntaxelement(total_injection(A,B), [A,B],[], [], [], expr).

syntaxelement(partial_surjection(A,B), [A,B],[], [], [], expr).

syntaxelement(total_surjection(A,B), [A,B],[], [], [], expr).

syntaxelement(total_bijection(A,B), [A,B],[], [], [], expr).

syntaxelement(partial_bijection(A,B), [A,B],[], [], [], expr).

syntaxelement(total_relation(A,B), [A,B],[], [], [], expr).

syntaxelement(surjection_relation(A,B),[A,B],[], [], [], expr).

syntaxelement(total_surjection_relation(A,B),[A,B],[], [], [], expr).

syntaxelement(seq(A), [A], [], [], [], expr).

syntaxelement(seq1(A), [A], [], [], [], expr).

syntaxelement(iseq(A), [A], [], [], [], expr).

syntaxelement(iseq1(A), [A], [], [], [], expr).

syntaxelement(perm(A), [A], [], [], [], expr).

syntaxelement(empty_sequence, [], [], [], [], expr).

syntaxelement(size(A), [A], [], [], [], expr).

syntaxelement(first(A), [A], [], [], [], expr).

syntaxelement(last(A), [A], [], [], [], expr).

syntaxelement(front(A), [A], [], [], [], expr).

syntaxelement(tail(A), [A], [], [], [], expr).

syntaxelement(rev(A), [A], [], [], [], expr).

syntaxelement(concat(A,B), [A,B],[], [], [], expr).

syntaxelement(insert_front(A,B), [A,B],[], [], [], expr).

syntaxelement(insert_tail(A,B), [A,B],[], [], [], expr).

syntaxelement(restrict_front(A,B), [A,B],[], [], [], expr).

syntaxelement(restrict_tail(A,B), [A,B],[], [], [], expr).

syntaxelement(general_concat(A), [A], [], [], [], expr).

syntaxelement(function(A,B), [A,B],[], [], [], expr).

syntaxelement(external_function_call(F,Args),Args,[],[Args],F,expr).

syntaxelement(identifier(I), [], [], [], I, expr).

syntaxelement(lazy_lookup_expr(I), [], [], [], I, expr).

syntaxelement(lazy_lookup_pred(I), [], [], [], I, pred).

syntaxelement(integer(I), [], [], [], I, expr).

syntaxelement(integer_set(T), [], [], [], T, expr).

syntaxelement(string(S), [], [], [], S, expr).

syntaxelement(set_extension(L), L, [], [L], [], expr).

syntaxelement(sequence_extension(L), L, [], [L], [], expr).

syntaxelement(comprehension_set(Ids,P),[P|Ids], Ids,[Ids], [], expr).

syntaxelement(event_b_comprehension_set(Ids,E,P),[E,P|Ids], Ids,[Ids], [], expr/only_typecheck).

syntaxelement(lambda(Ids,P,E), [P,E|Ids],Ids,[Ids], [], expr).

syntaxelement(general_sum(Ids,P,E), [P,E|Ids],Ids,[Ids], [], expr).

syntaxelement(general_product(Ids,P,E), [P,E|Ids],Ids,[Ids], [], expr).

syntaxelement(quantified_union(Ids,P,E), [P,E|Ids],Ids,[Ids], [], expr).

syntaxelement(quantified_intersection(Ids,P,E), [P,E|Ids],Ids,[Ids], [], expr).

syntaxelement(struct(Rec), [Rec], [], [], [], expr).

syntaxelement(rec(Fields), FContent, [], [FContent], FNames, expr) :- syntaxfields(Fields,FContent, FNames).

syntaxelement(record_field(R,I), [R], [], [], I, expr).

syntaxelement(assertion_expression(Cond,ErrMsg,Expr), [Cond,Expr], [], [], ErrMsg, expr).

syntaxelement(typeset, [], [], [], [], expr/only_typecheck).

syntaxelement(tree(A), [A], [], [], [], expr).

syntaxelement(btree(A), [A], [], [], [], expr).

syntaxelement(const(A,B), [A,B],[], [], [], expr).

syntaxelement(top(A), [A], [], [], [], expr).

syntaxelement(sons(A), [A], [], [], [], expr).

syntaxelement(prefix(A), [A], [], [], [], expr).

syntaxelement(postfix(A), [A], [], [], [], expr).

syntaxelement(sizet(A), [A], [], [], [], expr).

syntaxelement(mirror(A), [A], [], [], [], expr).

syntaxelement(rank(A,B), [A,B],[], [], [], expr).

syntaxelement(father(A,B), [A,B],[], [], [], expr).

syntaxelement(son(A,B,C), [A,B,C],[], [], [], expr).

syntaxelement(subtree(A,B), [A,B],[], [], [], expr).

syntaxelement(arity(A,B), [A,B],[], [], [], expr).

syntaxelement(bin(A), [A],[], [], [], expr).

syntaxelement(bin(A,B,C), [A,B,C],[], [], [], expr).

syntaxelement(infix(A), [A], [], [], [], expr).

syntaxelement(left(A), [A], [], [], [], expr).

syntaxelement(right(A), [A], [], [], [], expr).

syntaxelement(skip, [], [], [], [], subst).

syntaxelement(precondition(A,B), [A,B],[], [], [], subst).

syntaxelement(assertion(A,B), [A,B],[], [], [], subst).

syntaxelement(witness_then(A,B), [A,B],[], [], [], subst).

syntaxelement(if_elsif(A,B), [A,B],[], [], [], subst/elsif).

syntaxelement(while(A,B,C,D), [A,B,C,D],[], [], [], subst).

syntaxelement(while1(A,B,C,D,E), [A,B,C,D],[], [], E, subst).

syntaxelement(select_when(A,B), [A,B],[], [], [], subst/when).

syntaxelement(block(S),[S],[],[],[], subst/only_typecheck).

syntaxelement(assign(Lhs,Rhs),Exprs,[],[Lhs,Rhs], [], subst) :- append(Lhs,Rhs,Exprs).

syntaxelement(assign_single_id(Id,Rhs),[Id,Rhs],[],[], [], subst).

syntaxelement(any(Ids,P,S),[P,S|Ids],Ids,[Ids], [], subst).

syntaxelement(var(Ids,S), [S|Ids], Ids,[Ids], [], subst).

syntaxelement(if(Ifs), Ifs, [], [Ifs], [], subst).

syntaxelement(parallel(Ss), Ss, [], [Ss], [], subst).

syntaxelement(sequence(Ss), Ss, [], [Ss], [], subst).

syntaxelement(becomes_element_of(Ids,E), [E|Ids], [], [Ids], [], subst).

syntaxelement(becomes_such(Ids,P), [P|Ids], [], [Ids], [], subst). % Ids are new value, Ids$0 is old value

syntaxelement(evb2_becomes_such(Ids,P), [P|Ids], [], [Ids], [], subst/only_typecheck).

syntaxelement(let(Ids,P,S), [P,S|Ids], Ids, [Ids], [], subst).

syntaxelement(operation_call(Id,Rs,As), [Id|Exprs], [], [Rs,As], [], subst) :- append(Rs,As,Exprs).

syntaxelement(case(E,Eithers,Else), [E,Else|Eithers], [], [Eithers], [], subst).

syntaxelement(case_or(Es,S), [S|Es], [], [Es], [], subst/caseor).

syntaxelement(choice(Ss), Ss, [], [Ss], [], subst).

syntaxelement(select(Whens), Whens, [], [Whens], [], subst).

syntaxelement(select(Whens,Else), [Else|Whens], [], [Whens], [], subst).

syntaxelement(operation(I,Rs,As,B), [I,B|Ids], Ids, [Rs,As], [], subst) :- append(Rs,As,Ids).

syntaxelement(external_subst_call(F,Args),Args,[],[Args],F,subst).

syntaxelement(values_entry(I,E),[I,E],[],[],[],values_entry).

syntaxelement(rlevent(I,Sec,St,Ps,G,Ts,As,VWs,PWs,Ums,Rs), Subs, [], [Ps,Ts,As,VWs,PWs,Ums,Rs], [I,Sec], subst) :-
append([[St],Ps,[G],Ts,As,VWs,PWs,Ums,Rs],Subs).

syntaxelement(witness(I,P), [I,P], [], [], [], witness).

syntaxelement(let_predicate(Ids,As,Pred), Exprs, Ids, [Ids,As], [], pred) :- append([Ids,As,[Pred]],Exprs).

syntaxelement(let_expression(Ids,As,Expr), Exprs, Ids, [Ids,As], [], expr) :- append([Ids,As,[Expr]],Exprs).

syntaxelement(let_expression_global(Ids,As,Expr), Exprs, Ids, [Ids,As], [], expr) :- % version used by b_compiler
append([Ids,As,[Expr]],Exprs).

syntaxelement(lazy_let_expr(TID,A,Expr), [TID, A, Expr], [TID], [[TID],[A]], [], expr).

syntaxelement(lazy_let_pred(TID,A,Expr), [TID, A, Expr], [TID], [[TID],[A]], [], pred).

syntaxelement(lazy_let_subst(TID,A,Expr), [TID, A, Expr], [TID], [[TID],[A]], [], subst).

syntaxelement(if_then_else(If,Then,Else),[If,Then,Else], [], [], [], expr).

syntaxelement(compaction(A), [A], [], [], [], expr).

syntaxelement(mu(A), [A], [], [], [], expr).

syntaxelement(bag_items(A), [A], [], [], [], expr).

syntaxelement(freetype_set(Id), [], [], [], Id, expr).

syntaxelement(freetype_case(Type,Case,Expr), [Expr], [], [], [Type,Case], pred).

syntaxelement(freetype_constructor(Type,Case,Expr), [Expr], [], [], [Type,Case], expr).

syntaxelement(freetype_destructor(Type,Case,Expr), [Expr], [], [], [Type,Case], expr).

syntaxelement(ordinary, [], [], [], [], status).

syntaxelement(anticipated(Variant), [Variant], [], [], [], status).

syntaxelement(convergent(Variant), [Variant], [], [], [], status).

syntaxelement(recursive_let(Id,C),[Id,C],[Id],[],[], expr). % Note: Id is not really introduced !

syntaxfields/3

syntaxtransformation/5

syntaxtransformation_det/5

syntaxtraversion/6

test_result/2

texpr_contains_wd_condition/1

transform_bexpr/3

Meta: transform_bexpr(2,?,?)

transform_bexpr_td_with_scoping/3

Meta: transform_bexpr_td_with_scoping(3,?,?)

transform_bexpr_td_with_scoping2/4

transform_bexpr_with_acc/5

Meta: transform_bexpr_with_acc(4,?,?,?,?)

transform_bexpr_with_bup_accs/5

Meta: transform_bexpr_with_bup_accs(4,?,?,?,?)

transform_bexpr_with_scoping/3

Meta: transform_bexpr_with_scoping(3,?,?)

transform_bexpr_with_scoping2/4

Meta: transform_bexpr_with_scoping2(3,?,?,?)

try_find_and_remove_equalities/2

try_get_merged_position_info/3

try_get_merged_position_info_aux/3

unique_typed_id/3

update_id/4

update_id_from_info_field/4

update_id_from_info_field2/4

update_infos/3

update_used_ids/3

update_used_ids/4

update_used_ids_info/4

used_ids_like_info/3

uses_an_identifier/2

uses_an_identifier/4

uses_implementable_integers/1

uses_implementable_integers_aux/1

value_which_can_be_replaced/1

value_which_can_be_replaced2/2

var_cst_type/2

Determinacy Checker

Determinacy Checker:

! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_release,true)
! Existence error in argument 1 of absolute_file_name/3
! file extension('dll_path/dll_path') does not exist
! goal: absolute_file_name(extension('dll_path/dll_path'),_61767,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/pathes.pl')])
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(no_terminal_colors,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_enter_debugger_upon_error,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_use_timer,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_profile,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_src_profile,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_safe_mode,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_core_only,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_myheap,false)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(disable_chr,true)
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(tools_strings) does not exist
! goal: absolute_file_name(probsrc(tools_strings),_92609,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/pathes_lib.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file extension('counter/counter') does not exist
! goal: absolute_file_name(extension('counter/counter'),_61767,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/error_manager.pl')])
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_debug_flag,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(plspec_patch_libraries,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_debug_flag,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_release,true)
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(error_manager) does not exist
! goal: absolute_file_name(probsrc(error_manager),_71971,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/xml_prob.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(debug) does not exist
! goal: absolute_file_name(probsrc(debug),_70307,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/xml_prob.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file extrasrc(json_parser) does not exist
! goal: absolute_file_name(extrasrc(json_parser),_45227,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/translate.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(tools) does not exist
! goal: absolute_file_name(probsrc(tools),_136549,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/kernel_records.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file covsrc(coverage_tools_annotations) does not exist
! goal: absolute_file_name(covsrc(coverage_tools_annotations),_165111,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/kernel_waitflags.pl')])
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_safe_mode,true)
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(tools_lists) does not exist
! goal: absolute_file_name(probsrc(tools_lists),_165111,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/kernel_tools.pl')])
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_debug_watch_flag,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_safe_mode,true)
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(kernel_waitflags) does not exist
! goal: absolute_file_name(probsrc(kernel_waitflags),_167255,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/runtime_profiler.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(closures) does not exist
! goal: absolute_file_name(probsrc(closures),_173375,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/memoization.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file extension('counter/counter') does not exist
! goal: absolute_file_name(extension('counter/counter'),_178927,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/state_space.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file extrasrc(external_functions_reals) does not exist
! goal: absolute_file_name(extrasrc(external_functions_reals),_178163,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/external_functions.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file extrasrc(external_functions_svg) does not exist
! goal: absolute_file_name(extrasrc(external_functions_svg),_178163,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/external_functions.pl')])
! Existence error in user:check_arithmetic_function/1
! procedure user:check_arithmetic_function/1 does not exist
! goal: user:check_arithmetic_function(log(2,4))
! Existence error in argument 1 of absolute_file_name/3
! file chrsrc(chr_integer_inequality) does not exist
! goal: absolute_file_name(chrsrc(chr_integer_inequality),_179459,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/clpfd_interface.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(preferences) does not exist
! goal: absolute_file_name(probsrc(preferences),_178785,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/kernel_z.pl')])
! Existence error in user:exists_source/1
! procedure user:exists_source/1 does not exist
! goal: user:exists_source(library(atts))
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(tools_strings) does not exist
! goal: absolute_file_name(probsrc(tools_strings),_179779,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/kernel_strings.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(kernel_freetypes) does not exist
! goal: absolute_file_name(probsrc(kernel_freetypes),_173375,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/external_functions.pl')])
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_use_timer,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_debug_watch_flag,true)
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(kernel_reals) does not exist
! goal: absolute_file_name(probsrc(kernel_reals),_196403,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/b_interpreter_check.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(clpfd_interface) does not exist
! goal: absolute_file_name(probsrc(clpfd_interface),_190709,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/kernel_equality.pl')])
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(no_wd_checking,true)
! Existence error in user:exists_source/1
! procedure user:exists_source/1 does not exist
! goal: user:exists_source(library(atts))
! Existence error in user:exists_source/1
! procedure user:exists_source/1 does not exist
! goal: user:exists_source(library(atts))
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(avl_tools) does not exist
! goal: absolute_file_name(probsrc(avl_tools),_173797,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/bsets_clp.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file extension('counter/counter') does not exist
! goal: absolute_file_name(extension('counter/counter'),_186453,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/succeed_max.pl')])
! Existence error in user:exists_source/1
! procedure user:exists_source/1 does not exist
! goal: user:exists_source(library(logarr))
! Existence error in argument 1 of absolute_file_name/3
! file probcspsrc(haskell_csp) does not exist
! goal: absolute_file_name(probcspsrc(haskell_csp),_186307,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/xtl_interface.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file extension('probhash/probhash') does not exist
! goal: absolute_file_name(extension('probhash/probhash'),_189587,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/b_machine_hierarchy.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file extension('probhash/probhash') does not exist
! goal: absolute_file_name(extension('probhash/probhash'),_186453,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/value_persistance.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(avl_tools) does not exist
! goal: absolute_file_name(probsrc(avl_tools),_186595,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/state_packing.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(btypechecker) does not exist
! goal: absolute_file_name(probsrc(btypechecker),_174085,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/specfile.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file extension('counter/counter') does not exist
! goal: absolute_file_name(extension('counter/counter'),_173797,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/kernel_reals.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file kodkodsrc(kodkod) does not exist
! goal: absolute_file_name(kodkodsrc(kodkod),_167255,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/b_interpreter.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(kernel_waitflags) does not exist
! goal: absolute_file_name(probsrc(kernel_waitflags),_165111,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/delay.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(performance_messages) does not exist
! goal: absolute_file_name(probsrc(performance_messages),_165111,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/b_compiler.pl')])
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_safe_mode,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_safe_mode,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(no_wd_checking,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_data_validation_mode,xxxtrue)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_data_validation_mode,true)
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(bsyntaxtree) does not exist
! goal: absolute_file_name(probsrc(bsyntaxtree),_139825,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/custom_explicit_sets.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file prob_rewrite_rules(b_ast_cleanup_rewrite_rules) does not exist
! goal: absolute_file_name(prob_rewrite_rules(b_ast_cleanup_rewrite_rules),_136261,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/b_ast_cleanup.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(tools_strings) does not exist
! goal: absolute_file_name(probsrc(tools_strings),_136549,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/input_syntax_tree.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(b_state_model_check) does not exist
! goal: absolute_file_name(probsrc(b_state_model_check),_136407,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/b_read_write_info.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(eventhandling) does not exist
! goal: absolute_file_name(probsrc(eventhandling),_136407,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/parsercall.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(bmachine_eventb) does not exist
! goal: absolute_file_name(probsrc(bmachine_eventb),_129009,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/btypechecker.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(eventhandling) does not exist
! goal: absolute_file_name(probsrc(eventhandling),_129009,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/pragmas.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(module_information) does not exist
! goal: absolute_file_name(probsrc(module_information),_130815,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/bmachine_static_checks.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(error_manager) does not exist
! goal: absolute_file_name(probsrc(error_manager),_129009,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/bmachine_static_checks.pl')])
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_safe_mode,true)
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(bsyntaxtree) does not exist
! goal: absolute_file_name(probsrc(bsyntaxtree),_125875,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/bmachine_eventb.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file kodkodsrc(kodkod) does not exist
! goal: absolute_file_name(kodkodsrc(kodkod),_94479,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/bmachine.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file extension('random_permutations/random_permutations') does not exist
! goal: absolute_file_name(extension('random_permutations/random_permutations'),_95203,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/fd_utils_clpfd.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(error_manager) does not exist
! goal: absolute_file_name(probsrc(error_manager),_93201,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/partition_detection.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file extension('counter/counter') does not exist
! goal: absolute_file_name(extension('counter/counter'),_56967,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/kernel_objects.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(eventhandling) does not exist
! goal: absolute_file_name(probsrc(eventhandling),_51273,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/kernel_freetypes.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(clpfd_interface) does not exist
! goal: absolute_file_name(probsrc(clpfd_interface),_47709,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/typing_tools.pl')])
* Non-determinate: bsyntaxtree:different_val_from/2 (clause 4)
* Indexing cannot distinguish this from clause 5.
* Non-determinate: bsyntaxtree:different_val_from/2 (clause 6)
* Indexing cannot distinguish this from clause 7.
* Non-determinate: bsyntaxtree:get_rodin_name/2 (clause 1)
* Indexing cannot distinguish this from clause 2.
* Non-determinate: bsyntaxtree:select_info_labels/3 (clause 1)
* Calls nondet predicate bsyntaxtree:select/3 .
* Non-determinate: bsyntaxtree:member_in_conjunction/2 (clause 1)
* This clause contains a disjunction not forced to be deterministic.
* Non-determinate: bsyntaxtree:member_in_conjunction_cse/3 (clause 1)
* This clause contains a disjunction not forced to be deterministic.
* Non-determinate: bsyntaxtree:select_member_in_conjunction/3 (clause 1)
* This clause contains a disjunction not forced to be deterministic.
* Non-determinate: bsyntaxtree:create_exists_detect_tautology_aux/4 (clause 1)
* Calls nondet predicate bsyntaxtree:debug_format/3 .
* Non-determinate: bsyntaxtree:create_exists_detect_tautology_aux/4 (clause 2)
* Calls nondet predicate bsyntaxtree:debug_format/3 .
* Non-determinate: bsyntaxtree:is_equal/3 (clause 1)
* This clause contains a disjunction not forced to be deterministic.
* Non-determinate: bsyntaxtree:negate/2 (clause 1)
* Indexing cannot distinguish this from clause 2.
* Non-determinate: bsyntaxtree:not_empty_set_aux/2 (clause 11)
* Indexing cannot distinguish this from clause 14.
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(custom_explicit_sets) does not exist
! goal: absolute_file_name(probsrc(custom_explicit_sets),_261,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/bsyntaxtree.pl')])

Name: add_used_ids/4	Module: bsyntaxtree
Name: add_non_default_declaration/3	Module: bsyntaxtree
Name: non_default_declaration/2	Module: bsyntaxtree
Name: ->/2
Name: default_declaration/4	Module: bsyntaxtree
Name: conjunct_predicates/2	Module: bsyntaxtree
Name: same_functor/2	Module: foo_error
Name: ->/3

Name: RECURSIVE_CALL/3	Module: bsyntaxtree
Name: add_info/3	Module: bsyntaxtree
Name: =/2

Name: =/2
Name: append/3
Name: select/3	Module: foo_error
Name: ->/3
Name: !

Name: create_texpr/4	Module: bsyntaxtree
Name: conjunct_predicates/2	Module: bsyntaxtree
Name: get_guard_and_copy/4	Module: bsyntaxtree
Name: ->/3

Name: =/2
Name: is_rodin_label_info/1	Module: bsyntaxtree
Name: member/2
Name: ->/3

Name: add_error/3	Module: foo_error
Name: true
Name: atom/1
Name: ->/3

Name: fail
Name: add_internal_error/2	Module: foo_error
Name: add_info_if_new/3	Module: bsyntaxtree
Name: !

Name: mark_generated_exists/2	Module: b_interpreter_components
Name: create_unsimplified_exists/3	Module: b_interpreter_components

Name: conjunct_predicates_with_pos_info/2	Module: bsyntaxtree
Name: clean_up_and_preprocess_pos_for_cdclt/2	Module: welldef
Name: reuse_or_introduce_bool_var/10	Module: cdclt_pred_to_sat
Name: disjunct_predicates_with_pos_info/3	Module: bsyntaxtree
Name: single_input_location_to_ast_aux/4	Module: location_vars_to_program
Name: rewrite_member_of_function/3	Module: ast_cleanup_for_smt
Name: conjunct_predicates_with_pos_info/3	Module: bsyntaxtree

Name: ord_union/3	Module: foo_error
Name: ord_subtract/3	Module: foo_error
Name: sort/2
Name: get_texpr_ids/2	Module: bsyntaxtree
Name: find_identifier_uses/3	Module: bsyntaxtree
Name: !
Name: update_used_ids/4	Module: bsyntaxtree

Name: replace_ids_by_exprs2/5	Module: bsyntaxtree
Name: replace_id_by_expr2/8	Module: bsyntaxtree

Name: RECURSIVE_CALL/2	Module: bsyntaxtree
Name: same_length/2	Module: foo_error
Name: add_error_fail/3	Module: foo_error
Name: var/1
Name: ->/3

Name: definitely_empty_set/1	Module: bsyntaxtree
Name: definitely_not_non_empty_sequence/1	Module: bsyntaxtree
Name: definitely_not_sequence/1	Module: bsyntaxtree
Name: z_or_tla_minor_mode/0	Module: specfile
Name: not/1
Name: </2
Name: get_integer/2	Module: bsyntaxtree
Name: true
Name: =</2
Name: ->/3
Name: ==/2
Name: eventb_mode/0	Module: specfile

Name: always_well_defined/1	Module: bsyntaxtree
Name: ground/1
Name: non_empty_finite_wd_set_value/1	Module: bsyntaxtree
Name: non_empty_wd_seq_value/1	Module: bsyntaxtree
Name: finite_wd_seq_value/1	Module: bsyntaxtree
Name: finite_wd_set_value/1	Module: bsyntaxtree
Name: always_wd_avl_function/2	Module: bsyntaxtree
Name: =/2
Name: nonvar/1
Name: >=/2
Name: get_integer/2	Module: bsyntaxtree
Name: true
Name: z_or_tla_minor_mode/0	Module: specfile
Name: ->/3
Name: >/2
Name: \=/2
Name: eventb_mode/0	Module: specfile

Name: always_well_defined/1	Module: bsyntaxtree
Name: always_well_defined_or_discharged/1	Module: bsyntaxtree

Name: quick_definitely_maximal_total_function_avl/1	Module: custom_explicit_sets
Name: always_well_defined/1	Module: bsyntaxtree
Name: check_unique_in_domain_of_avlset/2	Module: custom_explicit_sets
Name: !
Name: ground_value/1	Module: kernel_tools
Name: =/2
Name: nonvar/1

Name: always_wd_avl_function/2	Module: bsyntaxtree
Name: l_get_parameter_independent_guards/5	Module: b_operation_guards
Name: check_wd/1	Module: b_compiler
Name: get_ltsmin_guards/3	Module: ltsmin
Name: l_always_well_defined/1	Module: bsyntaxtree
Name: b_compile2/8	Module: b_compiler
Name: always_wd/1	Module: bsyntaxtree

Name: create_exists_detect_tautology_aux/4	Module: bsyntaxtree
Name: create_exists_opt2/7	Module: bsyntaxtree
Name: dom_for_specific_closure_aux/6	Module: custom_explicit_sets

Name: l_replace_id_by_expr2/8	Module: bsyntaxtree
Name: l_replace_ids_by_exprs2/5	Module: bsyntaxtree

Name: RECURSIVE_CALL/4	Module: bsyntaxtree
Name: ord_union/3	Module: foo_error
Name: ord_delete_existing_element/3	Module: bsyntaxtree
Name: ->/3

Name: =/2
Name: ord_add_element/3	Module: foo_error
Name: get_texpr_id/2	Module: bsyntaxtree
Name: ->/3
Name: replace_id_by_expr/4	Module: bsyntaxtree
Name: select/3	Module: foo_error

Name: bsyntax_pattern2/4	Module: bsyntaxtree
Name: !
Name: =/2
Name: functor/3
Name: remove_all_infos/2	Module: bsyntaxtree
Name: var/1

Name: maplist/3	Module: foo_error
Name: all_same_length/2	Module: bsyntaxtree
Name: true
Name: =/2
Name: ==/2
Name: ->/3
Name: syntaxelement/6	Module: bsyntaxtree
Name: create_texpr/4	Module: bsyntaxtree
Name: functor/3

Name: fail
Name: check_special_rules/3	Module: bsyntaxtree
Name: add_error/3	Module: foo_error
Name: true
Name: check_infos/2	Module: bsyntaxtree
Name: ->/3
Name: check_ast_typing/3	Module: bsyntaxtree
Name: safe_functor/2	Module: bsyntaxtree
Name: add_error/4	Module: foo_error
Name: check_type/2	Module: bsyntaxtree
Name: check_expr/3	Module: bsyntaxtree
Name: nl
Name: write/1
Name: print_bexpr/1	Module: translate
Name: debug_level_active_for/1	Module: debug
Name: =/2

Name: add_message/4	Module: foo_error
Name: !
Name: syntaxtransformation/5	Module: bsyntaxtree
Name: add_error/4	Module: foo_error
Name: maplist/3	Module: foo_error
Name: unify_types_werrors/4	Module: btypechecker
Name: ->/3
Name: fail
Name: add_warning/3	Module: foo_error
Name: true
Name: lookup_type/2	Module: bsyntaxtree
Name: check_names/2	Module: bsyntaxtree
Name: check_type/3	Module: bsyntaxtree
Name: get_texpr_type/2	Module: bsyntaxtree
Name: =/2
Name: non_value_type/1	Module: bsyntaxtree
Name: RECURSIVE_CALL/3	Module: bsyntaxtree
Name: check_set_type/3	Module: bsyntaxtree

prob_prolog/src/bsyntaxtree.pl

Modules

Predicates of bsyntaxtree

Module Information

Dynamic Predicates: count_id_usage/2

3530 Lines

413 Predicates

Imported Modules: tools lists ordsets avl terms self_check error_manager

194 Exports

37 specified Imports

Predicates:

Name: trace
Name: format/2
Name: add_error/4	Module: foo_error
Name: nl
Name: print/1
Name: =/2
Name: ->/3
Name: find_identifier_uses/3	Module: bsyntaxtree

Name: check_bvalue/2	Module: bsyntaxtree
Name: !
Name: check_used_ids/5	Module: bsyntaxtree
Name: create_implication/3	Module: bsyntaxtree
Name: add_error/3	Module: foo_error
Name: illegal_id/1	Module: bsyntaxtree
Name: add_warning/4	Module: foo_error
Name: translate_bexpression/2	Module: translate
Name: =/2
Name: get_preference/2	Module: preferences
Name: is_just_type/1	Module: bsyntaxtree
Name: always_not_wd_top/1	Module: bsyntaxtree
Name: nonmember/2
Name: ajoin/2	Module: tools
Name: functor/3
Name: fail
Name: ->/3
Name: sub_expression_contains_wd_condition/2	Module: bsyntaxtree

Name: ground/1
Name: \==/2
Name: =/2
Name: true
Name: ->/3
Name: syntaxelement/6	Module: bsyntaxtree

Name: check_normal_type/2	Module: bsyntaxtree
Name: maplist/2	Module: foo_error
Name: !
Name: fail
Name: add_error/3	Module: foo_error
Name: true
Name: ==/2
Name: ->/3
Name: var/1

Name: add_internal_error/2	Module: foo_error
Name: check_ids3/3	Module: bsyntaxtree
Name: !

Name: symbolic_functionality_check_closure/2	Module: custom_explicit_sets
Name: symbolic_injectivity_check_closure/2	Module: custom_explicit_sets
Name: dom_symbolic/2	Module: custom_explicit_sets

Name: fail
Name: !
Name: check_used_ids_texpr/2	Module: bsyntaxtree

Name: RECURSIVE_CALL/3	Module: bsyntaxtree
Name: conjunct3/3	Module: bsyntaxtree

Name: conjunct2/3	Module: bsyntaxtree
Name: fail
Name: add_internal_error/2	Module: foo_error
Name: !
Name: var/1

Name: smt_add_predicate_to_solver/5	Module: smt_solvers_interface
Name: build_implications_from_ground_candidates/4	Module: cdclt_preprocessing
Name: detect_global_predicates/4	Module: bsyntaxtree
Name: process_candidate_impls/2	Module: cdclt_preprocessing
Name: add_missing_equalities/3	Module: before_after_predicates
Name: add_typing_pred/2	Module: b2setlog
Name: ctgDown_aux2/8	Module: mic_generation
Name: if_wp/3	Module: weakest_preconditions
Name: instantiate_quantifier_possible/7	Module: quantifier_instantiation
Name: remove_free_predicates/3	Module: enabling_predicates
Name: x_check/4	Module: bvisual_any_maxsolver
Name: generate_synthesis_data_from_predicate_ast/5	Module: predicate_data_generator
Name: filter_lhs_distinct_from_ids/4	Module: quantifier_instantiation
Name: constraint_transitions/3	Module: bmc
Name: weakest_precondition2/3	Module: weakest_preconditions
Name: compute_cbc_enable_rel/4	Module: enabling_analysis
Name: get_wd_theory_implications/3	Module: cdclt_preprocessing
Name: check_if_coenabled/4	Module: static_analysis
Name: add_declaration_for_identifier/3	Module: bsyntaxtree
Name: get_full_pred/9	Module: smt_solvers_interface
Name: op_to_transition/2	Module: bmc
Name: before_after_predicate_for_operation_no_equalities/5	Module: before_after_predicates
Name: select_member_in_conjunction/3	Module: bsyntaxtree
Name: down_aux/3	Module: mic_generation
Name: chain/3	Module: smtlib2_translation
Name: test_enabledness_condition/9	Module: static_analysis
Name: common_literals/3	Module: mic_generation
Name: prove_sequent_with_setlog/4	Module: b2setlog
Name: project_predicate_on_identifiers/5	Module: bsyntaxtree
Name: translate_z3_expr/4	Module: model_translation
Name: push_generalization/4	Module: ic3
Name: is_eventb_comprehension_set/6	Module: bsyntaxtree
Name: create_state_pred/5	Module: prob_state_predicates
Name: simplify_negation/2	Module: b_simplifier
Name: ctgDown_aux_find_level/6	Module: mic_generation
Name: disprove3/5	Module: disprover
Name: restriction_explicit_set_wf/6	Module: custom_explicit_sets
Name: get_top_level_symmetry_breaking_predicates_from_components/4	Module: smt_symmetry_breaking
Name: action_simulation/6	Module: cbc_refinement_checks
Name: add_non_default_declaration/3	Module: bsyntaxtree
Name: signed_bv2nat/2	Module: smtlib2_translation
Name: cdcl_sat_solve_predicate_no_timeout/2	Module: cdclt_solver
Name: create_primary_inputs_predicate/2	Module: predicate_handling
Name: cbc_symbolic_invariant_violation_get_constraint/2	Module: cbc_ba
Name: operations_pos/7	Module: cbc_refinement_checks
Name: shorten_inv_list/2	Module: ltsmin
Name: ba_predicate_if/4	Module: before_after_predicates
Name: before_after_predicate_list_conjunct_with_equalities/3	Module: before_after_predicates
Name: get_unsat_core_from_negative_cycle/3	Module: difference_logic_solver
Name: compute_cbc_enabling_relation_and_assert/5	Module: pge_algo
Name: no_loop_constraint/2	Module: kinduction
Name: is_cartesian_product_closure_aux/5	Module: custom_explicit_sets
Name: op_to_step_constraint/2	Module: bmc
Name: disprove_predicate/3	Module: atelierb_provers_interface
Name: conjunct_predicates_with_pos_info/2	Module: bsyntaxtree
Name: b2p/3	Module: b2setlog
Name: op_to_transition/2	Module: predicate_handling
Name: get_dependency_enabling_predicate/9	Module: static_analysis
Name: check_negated/6	Module: disprover
Name: add_input_to_op/3	Module: predicate_handling
Name: combine_pred_and_ac/4	Module: ast_cleanup_for_smt
Name: inductive_clause/2	Module: ic3
Name: get_ltsmin_guards/3	Module: ltsmin
Name: predicate_to_sat_e/11	Module: cdclt_pred_to_sat
Name: create_exists_opt/5	Module: bsyntaxtree
Name: add_no_loop_constraint/4	Module: kinduction
Name: create_all_different/2	Module: set_rewriter
Name: guard_strengthening_aux/6	Module: cbc_refinement_checks
Name: generalize_and_add/12	Module: ctigar
Name: exclude_solution/3	Module: predicate_data_generator
Name: witness_feasibility_aux/6	Module: cbc_refinement_checks
Name: get_initial_state_predicate/1	Module: predicate_handling
Name: rewrite_member_of_function/3	Module: ast_cleanup_for_smt
Name: verify_alloy_command/5	Module: cbc_path_solver
Name: any_maxsolver/5	Module: bvisual_any_maxsolver
Name: portray_hyps/1	Module: well_def_hyps
Name: initial_state/1	Module: solver_handling
Name: disable_analysis/5	Module: static_analysis
Name: ctgDown_aux/7	Module: mic_generation
Name: get_minimum_unsat_core_with_fixed_conjuncts/3	Module: prob2_interface
Name: strengthen_loop/7	Module: ctigar
Name: get_constraint/2	Module: bmc
Name: get_subset_counter_aux/8	Module: custom_explicit_sets
Name: induction_symbolic_model_check/3	Module: kinduction
Name: create_state_preds_aux/6	Module: prob_state_predicates
Name: process_candidate_impls_list/3	Module: cdclt_preprocessing
Name: ba_predicate_sequence/3	Module: before_after_predicates
Name: translate_z3_connective/4	Module: model_translation
Name: compute_enabling_predicate/5	Module: enabling_predicates
Name: inductively_generalize/7	Module: ctigar
Name: perform_custom_operation_retry/2	Module: b_trace_checking
Name: symbolic_model_check/3	Module: ic3
Name: witness_feasibility_parameters/6	Module: cbc_refinement_checks
Name: nat2bv/3	Module: smtlib2_translation
Name: step_constraint_property/3	Module: kinduction
Name: merge_parallels1/6	Module: weakest_preconditions
Name: concrete_state_to_abstract_state/3	Module: predicate_abstraction
Name: prove_predicate/3	Module: atelierb_provers_interface
Name: cbc_dependence_analysis/3	Module: enabling_analysis
Name: create_state_predicate_aux/2	Module: predicate_handling
Name: add_primary_inputs/2	Module: predicate_handling
Name: expand_let_predicate/4	Module: b_to_cnf
Name: mic/6	Module: ic3
Name: generate_dot_from_assertions/1	Module: tcltk_interface
Name: op_to_step_constraint/2	Module: kinduction
Name: intersection_of_explicit_set_wf/4	Module: custom_explicit_sets
Name: combine_pred_and_ac/4	Module: seq_rewriter
Name: parse_tclk_parameter_values_and_pred/4	Module: tcltk_interface
Name: conjunct_two_preds/3	Module: cdclt_preprocessing
Name: push_generalization/6	Module: ctigar
Name: add_wd_condition/4	Module: prob_rule_compiler
Name: rewrite_pre/10	Module: seq_rewriter
Name: inductively_generalize_aux/6	Module: ctigar
Name: unsat_core_generalization_aux/6	Module: unsat_core_generalization
Name: perform_single_replay_step_statespace/6	Module: b_intelligent_trace_replay
Name: conjunct_predicates_with_pos_info/3	Module: bsyntaxtree
Name: strengthen_loop/5	Module: ic3
Name: action_simulation3/5	Module: cbc_refinement_checks
Name: construct_pre_post_predicate/5	Module: visb_visualiser
Name: get_outputs_for_input_examples/7	Module: operation_data_generator
Name: before_after_predicate_no_equalities_aux/3	Module: before_after_predicates
Name: strip_outer_exists/2	Module: solver_interface
Name: select_equality/6	Module: closures
Name: before_after_predicate_no_equalities_top_level_aux/4	Module: before_after_predicates
Name: insert_custom_predicate_into_guard/3	Module: tcltk_interface
Name: predicate_to_sat_neg_e/11	Module: cdclt_pred_to_sat
Name: get_wd_theory_implications_for_candidates/3	Module: cdclt_preprocessing
Name: interpret/3	Module: smtlib2_interpreter
Name: inductively_generalize/7	Module: ic3
Name: disprove_double_check/8	Module: disprover
Name: get_outputs_for_input_examples/5	Module: operation_data_generator
Name: cleanup_pre/9	Module: ast_cleanup_for_smt
Name: strengthen_get_property/4	Module: ctigar
Name: smt_term_to_prob_term/3	Module: smtlib2_translation
Name: get_step_constraint/2	Module: kinduction
Name: partition_predicate/4	Module: enabling_analysis
Name: location_vars_to_program_aux/10	Module: location_vars_to_program
Name: eval_predicate2/4	Module: prob2_interface
Name: guard_strengthening_single_event/10	Module: cbc_refinement_checks
Name: simplify_b_predicate2/3	Module: b_simplifier
Name: maximize_closure2/6	Module: external_functions
Name: inductive_clause/2	Module: ctigar
Name: proof_supported_transition_predicate/2	Module: bmc
Name: create_members/3	Module: weakest_preconditions
Name: get_unsat_core_from_smt_formula/3	Module: cdclt_sat_solver
Name: symbolic_functionality_check_closure/2	Module: custom_explicit_sets
Name: may_be_coenabled_guards/3	Module: ltsmin
Name: enable_analysis/6	Module: static_analysis
Name: normalise_to_deterministic_actions_event/6	Module: enabling_predicates
Name: down/5	Module: mic_generation
Name: symbolic_model_check/3	Module: ctigar
Name: mic/6	Module: ctigar
Name: inductively_generalize_aux/6	Module: ic3
Name: perform_single_replay_step_by_pred/5	Module: b_intelligent_trace_replay
Name: mk_expr_aux/7	Module: smt_solvers_interface
Name: mk_expr_skip/6	Module: smt_solvers_interface
Name: ctgDown/8	Module: mic_generation
Name: create_exists_opt1/6	Module: bsyntaxtree
Name: get_unsat_core_with_fixed_conjuncts/3	Module: prob2_interface
Name: conflict_driven_clause_learning_online/8	Module: cdclt_solver
Name: symbolic_injectivity_check_closure/2	Module: custom_explicit_sets
Name: translate_z3_predicate/3	Module: model_translation
Name: difference_with_avl/5	Module: custom_explicit_sets
Name: override_custom_explicit_set_aux/4	Module: custom_explicit_sets
Name: strengthen_get_property/4	Module: ic3
Name: extract_membership/5	Module: b2setlog
Name: get_conj_inv_predicate/3	Module: static_analysis
Name: cdclt_solve_predicate_no_timeout_setup/8	Module: cdclt_solver