Dynamic Predicates: no_solution_found_for_constants/0 properties_were_filtered/1 unsat_properties_component/2 unsat_properties_enumeration_warning/1 unsat_properties_abort_error/1 unsat_properties_conjunct_inside_component/4 uses_implementable_integers/0 min_max_integer_value_used/2 project_properties_on_identifiers/1

4553 Lines

342 Predicates

Imported Modules: kernel_objects bsets_clp delay kernel_mappings b_global_sets store lists ordsets avl b_global_sets bmachine debug performance_messages self_check tools preferences error_manager typechecker bsyntaxtree translate kernel_waitflags kernel_reals kernel_records custom_explicit_sets state_space b_interpreter_eventb debug external_functions timeout b_interpreter_components b_interpreter_check b_compiler inf_arith static_ordering

35 Exports

80 specified Imports

Imports	Exports
Name: b_enumerate_values_in_store/5 Module: b_enumerate Name: b_tighter_enumerate_all_values/2 Module: b_enumerate Name: b_tighter_enumerate_values_in_ctxt/3 Module: b_enumerate Name: module_info/2 Module: module_information Name: state_corresponds_to_initialised_b_machine/2 Module: specfile Name: state_corresponds_to_set_up_constants_only/2 Module: specfile Name: is_symbolic_closure/1 Module: closures Name: mark_closure_as_symbolic/2 Module: closures Name: mark_closure_as_recursive/2 Module: closures Name: mark_closure/3 Module: closures Name: print_term_summary/1 Module: tools_printing Name: print_functor/1 Module: tools_printing Name: load_partial_constants/3 Module: value_persistance Name: lookup_cached_transitions/3 Module: value_persistance Name: negate/2 Module: bool_pred Name: sort_ids_by_usage/4 Module: static_ordering Name: reorder_state/3 Module: static_ordering Name: exclude_count/4 Module: tools_lists Name: optimized_nth1/3 Module: tools_lists Name: safe_time_out/3 Module: tools_meta Name: profile_single_call/3 Module: runtime_profiler Name: format_with_colour_nl/4 Module: tools_printing Name: prepare_state_for_specfile_trans/3 Module: specfile Name: expand_const_and_vars_to_full_store/2 Module: specfile Name: profile_single_call/3 Module: runtime_profiler Name: get_assertions_from_machine/2 Module: bmachine Name: b_machine_has_dynamic_assertions/0 Module: bmachine Name: b_machine_has_static_assertions/0 Module: bmachine Name: do_not_enumerate_binary_boolean_operator/3 Module: kernel_propagation Name: abstract_constant/2 Module: b_machine_hierarchy Name: concrete_constant/2 Module: b_machine_hierarchy Name: external_fun_can_be_inverted/1 Module: external_functions Name: not_element_of_list_wf/3 Module: kernel_lists Name: get_texpr_set_type/2 Module: bsyntaxtree Name: ground_value/1 Module: kernel_tools Name: get_set_type/2 Module: bsyntaxtree Name: is_set_type/2 Module: bsyntaxtree Name: finite_cardinality_as_int_with_type_wf/5 Module: kernel_cardinality_attr Name: equality_objects_wf/4 Module: kernel_equality Name: is_membership_or_equality/3 Module: bsyntaxtree Name: same_id/3 Module: bsyntaxtree Name: is_real/2 Module: kernel_reals Name: clpfd_sum/2 Module: clpfd_interface Name: clpfd_if_then_else/4 Module: clpfd_interface Name: get_global_type_value/3 Module: b_global_sets Name: catch_clpfd_overflow_call2/2 Module: clpfd_interface Name: construct_closure_if_necessary/4 Module: closures Name: is_inf_or_overflow_card/1 Module: kernel_card_arithmetic Name: safe_mul/3 Module: kernel_card_arithmetic Name: ground_bexpr/1 Module: kernel_tools Name: ground_bexpr_check/2 Module: kernel_tools Name: time_out/3 Module: timeout Name: quick_avl_approximate_size/2 Module: avl_tools Name: efficient_card_for_set/3 Module: custom_explicit_sets Name: clpfd_card_domain_for_var/3 Module: kernel_cardinality_attr Name: map_optlist/2 Module: tools Name: optlist_to_list/2 Module: tools Name: maplist/3 Module: lists Name: construct_typedval_infos/4 Module: b_enumerate Name: bexpr_variables/2 Module: kernel_tools Name: value_variables/3 Module: kernel_tools Name: remove_variables/3 Module: tools Name: value_variables/2 Module: kernel_tools Name: check_used_ids_info/4 Module: b_ast_cleanup Name: ground_state/1 Module: kernel_tools Name: registered_freetype/2 Module: kernel_freetypes Name: registered_freetype_case_value/3 Module: kernel_freetypes Name: opt_add_source_location_hits/2 Module: source_profiler Name: ground_state_check/2 Module: kernel_tools Name: ground_value_check/2 Module: kernel_tools Name: overwrite_record_wf/5 Module: kernel_records Name: any_value_for_type/2 Module: typing_tools Name: add_prob_deferred_set_elements_to_store/3 Module: b_global_sets Name: unsat_conjunct_inside_component/4 Module: b_interpreter_components Name: unsat_component_abort_error/1 Module: b_interpreter_components Name: unsat_component_enumeration_warning/1 Module: b_interpreter_components Name: get_specification_description/2 Module: specfile Name: no_value_for_variable/2 Module: store Name: b_check_valid_state/1 Module: b_state_model_check Name: register_event_listener/3 Module: eventhandling	Name: b_test_boolean_expression/4 Name: b_test_boolean_expression/6 Name: b_test_boolean_expression_cs/5 Name: b_test_boolean_expression_for_ground_state/4 Name: b_test_boolean_expression_for_ground_state/5 Name: b_not_test_boolean_expression/4 Name: b_not_test_boolean_expression/6 Name: b_not_test_boolean_expression_cs/5 Name: b_convert_bool/5 Name: b_convert_bool_timeout/7 Name: b_compute_expression/5 Name: b_execute_top_level_statement/7 Name: b_compute_expression_nowf/4 Name: b_compute_expression_nowf/6 Name: b_compute_expression_nowf/7 Name: b_set_up_concrete_constants/2 Name: b_partial_set_up_concrete_constants/1 Name: b_initialise_machine/4 Name: b_execute_top_level_operation_update/5 Name: b_execute_top_level_operation_wf/8 Name: convert_list_of_expressions_into_set_wf/4 Name: b_state_violates_invariant/2 Name: state_violates_assertions/2 Name: analyse_invariant_for_state/1 Name: insert_before_substitution_variables/5 Name: try_lookup_value_in_store_and_global_sets/3 Name: lookup_value_in_store_and_global_sets_wf/7 Name: set_up_typed_localstate/6 Name: set_up_typed_localstate2/8 Name: set_projection_on_static_assertions/1 Name: tcltk_unsatisfiable_components_exist/0 Name: tcltk_quick_describe_unsat_properties/2 Name: get_unsat_component_predicate/3 Name: properties_were_filtered/1 Name: b_generate_for_all_list_domain_nolwf/8

Imports

Exports

Name: b_enumerate_values_in_store/5

Module: b_enumerate

Name: b_tighter_enumerate_all_values/2

Module: b_enumerate

Name: b_tighter_enumerate_values_in_ctxt/3

Module: b_enumerate

Name: module_info/2

Module: module_information

Name: state_corresponds_to_initialised_b_machine/2

Module: specfile

Name: state_corresponds_to_set_up_constants_only/2

Module: specfile

Name: is_symbolic_closure/1

Module: closures

Name: mark_closure_as_symbolic/2

Module: closures

Name: mark_closure_as_recursive/2

Module: closures

Name: mark_closure/3

Module: closures

Name: print_term_summary/1

Module: tools_printing

Name: print_functor/1

Module: tools_printing

Name: load_partial_constants/3

Module: value_persistance

Name: lookup_cached_transitions/3

Module: value_persistance

Name: negate/2

Module: bool_pred

Name: sort_ids_by_usage/4

Module: static_ordering

Name: reorder_state/3

Module: static_ordering

Name: exclude_count/4

Module: tools_lists

Name: optimized_nth1/3

Module: tools_lists

Name: safe_time_out/3

Module: tools_meta

Name: profile_single_call/3

Module: runtime_profiler

Name: format_with_colour_nl/4

Module: tools_printing

Name: prepare_state_for_specfile_trans/3

Module: specfile

Name: expand_const_and_vars_to_full_store/2

Module: specfile

Name: profile_single_call/3

Module: runtime_profiler

Name: get_assertions_from_machine/2

Module: bmachine

Name: b_machine_has_dynamic_assertions/0

Module: bmachine

Name: b_machine_has_static_assertions/0

Module: bmachine

Name: do_not_enumerate_binary_boolean_operator/3

Module: kernel_propagation

Name: abstract_constant/2

Module: b_machine_hierarchy

Name: concrete_constant/2

Module: b_machine_hierarchy

Name: external_fun_can_be_inverted/1

Module: external_functions

Name: not_element_of_list_wf/3

Module: kernel_lists

Name: get_texpr_set_type/2

Module: bsyntaxtree

Name: ground_value/1

Module: kernel_tools

Name: get_set_type/2

Module: bsyntaxtree

Name: is_set_type/2

Module: bsyntaxtree

Name: finite_cardinality_as_int_with_type_wf/5

Module: kernel_cardinality_attr

Name: equality_objects_wf/4

Module: kernel_equality

Name: is_membership_or_equality/3

Module: bsyntaxtree

Name: same_id/3

Module: bsyntaxtree

Name: is_real/2

Module: kernel_reals

Name: clpfd_sum/2

Module: clpfd_interface

Name: clpfd_if_then_else/4

Module: clpfd_interface

Name: get_global_type_value/3

Module: b_global_sets

Name: catch_clpfd_overflow_call2/2

Module: clpfd_interface

Name: construct_closure_if_necessary/4

Module: closures

Name: is_inf_or_overflow_card/1

Module: kernel_card_arithmetic

Name: safe_mul/3

Module: kernel_card_arithmetic

Name: ground_bexpr/1

Module: kernel_tools

Name: ground_bexpr_check/2

Module: kernel_tools

Name: time_out/3

Module: timeout

Name: quick_avl_approximate_size/2

Module: avl_tools

Name: efficient_card_for_set/3

Module: custom_explicit_sets

Name: clpfd_card_domain_for_var/3

Module: kernel_cardinality_attr

Name: map_optlist/2

Module: tools

Name: optlist_to_list/2

Module: tools

Name: maplist/3

Module: lists

Name: construct_typedval_infos/4

Module: b_enumerate

Name: bexpr_variables/2

Module: kernel_tools

Name: value_variables/3

Module: kernel_tools

Name: remove_variables/3

Module: tools

Name: value_variables/2

Module: kernel_tools

Name: check_used_ids_info/4

Module: b_ast_cleanup

Name: ground_state/1

Module: kernel_tools

Name: registered_freetype/2

Module: kernel_freetypes

Name: registered_freetype_case_value/3

Module: kernel_freetypes

Name: opt_add_source_location_hits/2

Module: source_profiler

Name: ground_state_check/2

Module: kernel_tools

Name: ground_value_check/2

Module: kernel_tools

Name: overwrite_record_wf/5

Module: kernel_records

Name: any_value_for_type/2

Module: typing_tools

Name: add_prob_deferred_set_elements_to_store/3

Module: b_global_sets

Name: unsat_conjunct_inside_component/4

Module: b_interpreter_components

Name: unsat_component_abort_error/1

Module: b_interpreter_components

Name: unsat_component_enumeration_warning/1

Module: b_interpreter_components

Name: get_specification_description/2

Module: specfile

Name: no_value_for_variable/2

Module: store

Name: b_check_valid_state/1

Module: b_state_model_check

Name: register_event_listener/3

Module: eventhandling

Name: b_test_boolean_expression/4

Name: b_test_boolean_expression/6

Name: b_test_boolean_expression_cs/5

Name: b_test_boolean_expression_for_ground_state/4

Name: b_test_boolean_expression_for_ground_state/5

Name: b_not_test_boolean_expression/4

Name: b_not_test_boolean_expression/6

Name: b_not_test_boolean_expression_cs/5

Name: b_convert_bool/5

Name: b_convert_bool_timeout/7

Name: b_compute_expression/5

Name: b_execute_top_level_statement/7

Name: b_compute_expression_nowf/4

Name: b_compute_expression_nowf/6

Name: b_compute_expression_nowf/7

Name: b_set_up_concrete_constants/2

Name: b_partial_set_up_concrete_constants/1

Name: b_initialise_machine/4

Name: b_execute_top_level_operation_update/5

Name: b_execute_top_level_operation_wf/8

Name: convert_list_of_expressions_into_set_wf/4

Name: b_state_violates_invariant/2

Name: state_violates_assertions/2

Name: analyse_invariant_for_state/1

Name: insert_before_substitution_variables/5

Name: try_lookup_value_in_store_and_global_sets/3

Name: lookup_value_in_store_and_global_sets_wf/7

Name: set_up_typed_localstate/6

Name: set_up_typed_localstate2/8

Name: set_projection_on_static_assertions/1

Name: tcltk_unsatisfiable_components_exist/0

Name: tcltk_quick_describe_unsat_properties/2

Name: get_unsat_component_predicate/3

Name: properties_were_filtered/1

Name: b_generate_for_all_list_domain_nolwf/8

Predicates

Predicates:

add_additional_properties/2

add_lazy_let_id_and_expression/6

add_lazy_let_id_and_expression/7

add_lazy_let_id_to_local_state/5

add_typed_var_to_localstate/5

add_typed_vars_to_localstate/4

add_typed_vars_to_localstate_aux/4

add_wd_error_if_false/5

all_unsat_components_marked_prob_ignore/0

analyse_invariant_for_state/1

assert_unsat_component_infos/1

attempt_reification/0

b_add_constant_definition/9

b_add_constant_definition_aux/9

b_apply_function_set_extension/7

b_apply_function_set_extension_aux/9

b_assign_value_or_function/8

b_assign_values_or_functions/7

b_check_boolean_expression_with_enum/6

b_check_execute_while_loop1/11

b_check_execute_while_loop2/11

b_check_test_equivalence/8

b_clpfd_if_then_else/8

b_clpfd_if_then_else_block/9

b_compute_assign_expressions_when/6

b_compute_card/8

b_compute_card2/8

b_compute_comprehension_set/7

b_compute_comprehension_set_aux/4

b_compute_comprehension_set_sym/3

b_compute_comprehension_set_sym_msg/4

b_compute_comprehension_set_symbolic/7

b_compute_expression/5

b_compute_expression2/7

b_compute_expression_function/8

b_compute_expression_nowf/4

b_compute_expression_nowf/6

b_compute_expression_nowf/7

b_compute_expression_when2/6

b_compute_expressions/5

b_compute_expressions_when2/6

b_compute_field/5

b_compute_if_then_else/7

b_compute_max/7

b_compute_min/7

b_convert_bool/5

b_convert_bool_timeout/7

b_convert_bool_wf0/6

b_convert_bool_wf0_timeout/8

b_enum_not_test_equivalence/7

b_enum_test_equivalence/7

b_enumerate_exists/6

b_enumerate_exists_aux_ground/5

b_execute_assertion/8

b_execute_assertion_block/9

b_execute_becomes_such/7

b_execute_choice/8

b_execute_else_list/7

b_execute_else_list2/9

b_execute_else_list3/9

b_execute_initialisation_statement/7

b_execute_inner_statement/7

b_execute_inner_statement/9

b_execute_let_definitions/4

b_execute_operation2/12

b_execute_operation3/15

b_execute_operation_in_expression/7

b_execute_operation_with_parameters/12

b_execute_sequence/7

b_execute_statement/6

b_execute_statement/7

b_execute_statement2/8

b_execute_statement_list_when_state_set/8

b_execute_statement_when_state_set2/9

b_execute_statements_in_parallel/7

b_execute_top_level_operation_update/5

b_execute_top_level_operation_update_wf/6

b_execute_top_level_operation_wf/8

b_execute_top_level_statement/7

b_execute_top_level_statement2/8

b_execute_while/10

b_execute_while1/10

b_execute_while_body/10

b_execute_while_idle/11

b_execute_while_loop/10

b_execute_while_loop_block/11

b_execute_while_when_state_set/10

b_expand_closure_forall_to_list/3

b_expand_compute_comprehension_set/4

b_for_all_find_counter_example/7

b_general_sum_or_mul/10

b_general_sum_or_mul_over_set/9

b_generate_closure_if_necessary/6

b_generate_for_all_domain2/8

b_generate_for_all_list_domain1/9

b_generate_for_all_list_domain_nolwf/8

b_generate_forall_closure/6

b_generate_rec_closure_aux/7

b_generate_set_for_all_domain/7

b_global_set_or_free_type/3

b_initialise_machine/4

b_initialise_machine2/4

b_lambda_result_equal_boolean_expression/5

b_not_not_test_exists_aux/4

b_not_test_atomic_boolean_expression2/7

b_not_test_atomic_boolean_expression3/5

b_not_test_boolean_expression/4

b_not_test_boolean_expression/6

b_not_test_boolean_expression2/7

b_not_test_boolean_expression_cs/5

b_not_test_conjunction/7

b_not_test_conjunction_rhs/7

b_not_test_equivalence/7

b_not_test_exists/7

b_not_test_exists_aux/5

b_not_test_exists_aux2/5

b_not_test_inner_boolean_expression/4

b_not_test_list_of_boolean_expression/4

b_optimized_b_test_instance/4

b_partial_set_up_concrete_constants/1

b_partial_set_up_concrete_constants2/2

b_set_up_concrete_constants/2

b_state_violates_invariant/2

b_state_violates_invariant_aux/2

b_state_violates_spec_invariant/3

b_sum_or_mul_over_list/9

b_sum_or_mul_over_list_acc/11

b_sum_or_mul_over_list_acc2/12

b_sum_or_mul_over_list_clp/9

b_test_atomic_boolean_expression2/5

b_test_atomic_equal_boolean_expression/6

b_test_atomic_not_equal_boolean_expression/6

b_test_boolean_expression/4

b_test_boolean_expression/6

b_test_boolean_expression2/7

b_test_boolean_expression_cs/5

b_test_boolean_expression_for_ground_state/4

b_test_boolean_expression_for_ground_state/5

b_test_boolean_expression_for_ground_state1/5

b_test_boolean_expression_for_ground_state2/6

b_test_exists_wo_expansion/6

b_test_implication/8

b_test_inner_boolean_expression/4

b_test_list_of_boolean_expression_aux/5

b_test_list_of_boolean_expression_for_ground_state/4

b_test_member_expression/5

b_test_member_expression2/7

b_test_notmember_expression/7

b_trace_test_components_full/3

b_try_check_boolean_expression/5

b_try_check_boolean_expression_c/5

b_try_check_boolean_expression_c2/5

b_try_check_boolean_expression_lwf/7

b_try_check_boolean_expression_lwf_block/6

b_try_check_boolean_expression_lwf_c/7

b_try_check_boolean_expression_no_enum_wf/5

b_try_check_boolean_expression_wf/5

b_try_check_failed/7

binary_boolean_operator_trivially_true/2

binop_to_be_marked_as_symbolic/3

block_compute_comprehension_set_aux/6

block_execute_statement/7

block_lazy_compute_expression/8

block_test_implication/6

blocking_ground_copied_wait_flags/2

blocking_override/6

bring_ground_elements_forward/3

bselect/4

call_b_execute_operation2/11

can_be_used_for_unification/1

can_get_full_fd_value/1

check_additional_guard/4

check_additional_guard_when_bound/6

check_freetype_case/7

check_freetype_case2/8

check_invariant/3

check_invariant_predicate_aux/2

check_invariant_predicate_with_time_out/3

check_invariant_predicate_with_time_out_res/3

check_invariant_with_time_out/2

check_nth1_invariant/2

check_precondition_result/5

check_set_bounded_aux/2

check_set_lists_bounded/3

check_state_skeleton_bound/2

check_state_skeleton_bound_aux/3

check_time_out_res/2

check_uses_implementable_integers/1

compute_let_expressions/5

conjoin_simple/3

convert_list_of_expressions_into_sequence/2

convert_list_of_expressions_into_sequence/3

convert_list_of_expressions_into_set1/5

convert_list_of_expressions_into_set2/6

convert_list_of_expressions_into_set_wf/4

convert_to_prolog_pattern_match/6

convert_to_prolog_pattern_match2/6

create_any_bindings/3

create_full_operation/5

expand_forall_quantifier/6

fill_in_det_solutions/2

filter_and_convert_list_to_parameter_tuples/4

filter_and_convert_list_to_parameter_tuples_aux/6

filter_results/4

filter_states/5

finalise_clp/3

finite_reasonably_sized_set/1

flatten_pairs/3

flatten_pairs/4

force_evaluation_of_lazy_value/3

generate_assignment/4

generate_recursive_closure/8

generate_unsat_properties_warnings/0

get_acc_base/3

get_acc_result/3

get_assign_expr_priority_wf/3

get_component_enum_warning_message/2

get_exists_used_ids/4

get_max_card_for_value/2

get_property_components/1

get_unsat_component_description/8

get_unsat_component_predicate/3

get_value/3

get_wait_flag_if_necessary/5

get_while_reads_write_info_and_filter_state/6

ground_inner_wf/3

ground_wait_flags_for_exists/2

ground_wait_flags_for_exists2/3

id_check/2

identifiers_not_used_in_bexp/2

init_clp_acc/4

init_wait_flags_cs/5

insert_before_substitution_variables/5

intersect_invs/2

is_couple/4

is_extension_function/3

is_extension_function_aux/2

is_for_all_set_membership_predicate/5

is_for_all_set_membership_predicate2/8

is_lambda_result_id/1

is_sequence_extension_function/3

is_set_extension_function/2

keep_constant/2

l_compute_expression/5

l_compute_field/5

lazy_compute_expression/7

lazy_exclude/3

lazy_exclude_aux/5

list_of_expressions_is_ground/3

lookup_value_in_global_sets_wf/7

lookup_value_in_store_and_global_sets_wf/7

lookup_values_if_vars/4

make_couplise/2

max_cardinality_ok_for_expansion/4

max_cardinality_ok_for_expansion1/5

max_cardinality_ok_for_expansion2/5

member_conjunct/3

non_ignore_unsat_component/0

not_generated_exists_paras/1

not_inv_aux/1

not_invertible/1

not_with_enum_warning_and_possible_delay/4

not_with_enum_warning_delay/4

obvious_enumeration/2

other_warning/1

output_parameters_value/7

parameter_list_cardinality/2

pattern_match/3

peel_implications/6

prepare_eventb_initialisation/3

project_onto_static_assertions/4

reification_relevant_for_op/1

remove_ids_defined_by_equality/5

reset_b_interpreter/0

reset_unsat_component_infos/0

set_projection_on_static_assertions/1

set_up_localstate_for_global_let/6

set_up_localstate_for_let/7

set_up_typed_localstate/3

set_up_typed_localstate/6

set_up_typed_localstate2/8

setup_read_output_variable/2

setup_result_input_values/2

simple_expression/1

simple_expression_aux/1

solve_properties/3

solve_properties/4

sort_aux/4

sort_variable_binding/2

state_satisfies_assertions/3

state_satisfies_invariant_aux/2

state_violates_assertions/2

state_violates_assertions_aux/2

state_violates_invariant/2

store_values/3

tcltk_quick_describe_unsat_properties/2

tcltk_unsatisfiable_components_exist/0

test_forall_instance/5

to_be_marked_as_symbolic_aux/2

tp2/3

translate_init_statements/2

triggers_enum_warning/5

try_get_op_name/2

try_lookup_value_in_store_and_global_sets/3

unop_to_be_marked_as_symbolic/2

unused_localvariable/2

unused_variable/2

value_type/1

wrap_stmt/1

add_additional_properties/2

add_lazy_let_id_and_expression/6

add_lazy_let_id_and_expression/7

add_lazy_let_id_to_local_state/5

add_typed_var_to_localstate/5

Description:
when(ground(Val), (print(' ++ '),print(Var),print(' ---> '), print(Val),nl)),
,print(ok(Val)),nl.

add_typed_vars_to_localstate/4

add_typed_vars_to_localstate_aux/4

add_wd_error_if_false/5

Block: add_wd_error_if_false(-,?,?,?,?)

all_unsat_components_marked_prob_ignore/0

analyse_invariant_for_state/1

assert_unsat_component_infos/1

attempt_reification/0

b_add_constant_definition/9

b_add_constant_definition_aux/9

b_add_constant_definition_aux(Kind,ID,_Info,Arg1,SetType1,SymArg2,LocalState,State,WF) :-
    (preference(use_function_memoization,true), Kind=abstract ;
    constant_variable_marked_as_memo(ID)), % description(memo) as info field using @desc memo pragma; see
    !,
    b_compute_expression(Arg1,LocalState,State,SV1,WF), % the identifier
    (SymArg2 = b(recursive_let(TID,Body),_,_)
    -> get_texpr_id(TID,RecID),
    b_compute_expression(Body,[bind(RecID,RedIDVal)|LocalState],State,SV2,WF),
    RecValue='$recursion_value'(RedIDVal)
    ; b_compute_expression(SymArg2,LocalState,State,SV2,WF),
    RecValue='$no_recursion'
    ),
    (nonvar(SV2), SV2 \= closure(_,_,_)
    -> % value fully computed; no need to memoize
    debug_println(19,not_memoizing(ID)),
    kernel_call_predicate_equal_object_optimized(SV1,SV2,WF)
    ; mark_closure_as_symbolic(SV2,SV3),
    % what if SV2 is var?
    memoization:register_memoization_function(ID,SV3,SetType1,RecValue,MEMOID,SV4),
    debug_println(19,marking_for_memoization(ID,MEMOID)),
    %print_term_summary(registered_fun(ID,MEMOID,SV4)),nl,
    kernel_call_predicate_equal_object_optimized(SV1,SV4,WF)
).

b_add_constant_definition_aux(_Kind,ID,Info,Arg1,_,SymArg2,LocalState,State,WF) :-
    b_compute_expression(Arg1,LocalState,State,SV1,WF), % the identifier
    b_compute_expression(SymArg2,LocalState,State,SV2,WF),
    (constant_variable_marked_as_expand(ID)
    -> b_expand_compute_comprehension_set(SV2,Info,SV3,WF)
    ; definitely_expand_this_explicit_set(SV2) % check for a few patterns which should definitely be expanded;
    % in case user puts a set accidentally into the ABSTRACT_CONSTANTS section
    -> b_expand_compute_comprehension_set(SV2,Info,SV3,WF)
    ; var(SV2) -> SV3=SV2
    ; mark_closure_as_symbolic(SV2,SV3)
    ),
    kernel_call_predicate_equal_object_optimized(SV1,SV3,WF).

b_apply_function_set_extension/7

b_apply_function_set_extension_aux/9

Block: b_apply_function_set_extension_aux(-,?,?,?,?,?,?,?,?)

b_assign_value_or_function/8

b_assign_values_or_functions/7

b_check_boolean_expression_with_enum/6

b_check_execute_while_loop1/11

Block: b_check_execute_while_loop1(-,?,?,?,?,?,?,?,?,?,?)

b_check_execute_while_loop2/11

Block: b_check_execute_while_loop2(-,?,?,?,?,?,?,?,?,?,?)

b_check_test_equivalence/8

b_clpfd_if_then_else/8

b_clpfd_if_then_else_block/9

Block: b_clpfd_if_then_else_block(-,-,?,?,?,?,?,?,?)

b_compute_assign_expressions_when/6

b_compute_card/8

b_compute_card2/8

b_compute_comprehension_set/7

b_compute_comprehension_set_aux/4

b_compute_comprehension_set_sym/3

b_compute_comprehension_set_sym_msg/4

b_compute_comprehension_set_symbolic/7

b_compute_expression/5

b_compute_expression2/7

Description:
NOT COVERED (17)
NOT COVERED (30)
NOT COVERED (32)
NOT COVERED (34)

b_compute_expression2(value(Val),_T,_I,_LS,_S,V,WF) :- !, equal_object_wf(Val,V,WF). %Val=V.

b_compute_expression2(boolean_true,_T,_I,_LState,_State,Res,_WF) :- !, Res = pred_true /* bool_true */. % for simple types we can use ordinary unification

b_compute_expression2(boolean_false,_T,_I,_LState,_State,Res,_WF) :- !, Res = pred_false /* bool_false */.

b_compute_expression2(integer_set(NSET),_T,_I,_LState,_State,Res,WF) :- !, equal_object_wf(Res,global_set(NSET),WF). %Res = global_set(NSET).

b_compute_expression2(bool_set,_T,_I,_LState,_State,Res,WF) :- !, % b_type2_set(bool,Res).
    equal_object_wf(Res,avl_set(node(pred_false,true,1,empty,node(pred_true,true,0,empty,empty))),WF).

b_compute_expression2(float_set,_T,_I,_LState,_State,Res,WF) :- !, equal_object_wf(Res,global_set('FLOAT'),WF).

b_compute_expression2(real_set,_T,_I,_LState,_State,Res,WF) :- !, equal_object_wf(Res,global_set('REAL'),WF).

b_compute_expression2(string_set,_T,_I,_LState,_State,Res,WF) :- !, equal_object_wf(Res,global_set('STRING'),WF).

b_compute_expression2(string(S),_T,_I,_LState,_State,Res,_WF) :- !,
    % TODO(ML,26.8.2008): Check if we should use a different functor for syntax tree vs data
    Res = string(S).

b_compute_expression2(typeset,Type,_I,_LState,_State,Res,WF) :- !,
    is_set_type(Type,ElType), % we could generate global_set('STRING'),... for certain types
    equal_object_wf(Res,closure('_zzzz_unary',[ElType],b(truth,pred,[])),WF).

b_compute_expression2(empty_set,_T,_I,_LState,_State,Res,_WF) :- !, empty_set(Res).

b_compute_expression2(empty_sequence,_T,_I,_LState,_State,Res,_WF) :- !, empty_sequence(Res).

b_compute_expression2(event_b_identity,EType,_I,_LState,_State,Res,WF) :-
    get_set_type(EType,couple(Type,Type)),!,
    event_b_identity_for_type(Type,Res,WF).

b_compute_expression2(integer(Val),_T,_I,_LocalState,_State,Res,_WF) :- !, Res = int(Val).

b_compute_expression2(max_int,_T,_I,_LS,_S,Res,_WF) :-
    preferences:get_preference(maxint,CVal),!, Res = int(CVal).

b_compute_expression2(min_int,_T,_I,_LS,_S,Res,_WF) :-
    preferences:get_preference(minint,CVal),!, Res = int(CVal).

b_compute_expression2(identifier(Id),Type,Info,LocalState,State,Res,WF) :- !,
    lookup_value_in_store_and_global_sets_wf(Id,Type,LocalState,State,Value,Info,WF),
    equal_object_wf(Res,Value,WF).

b_compute_expression2(lazy_lookup_expr(Id),_Type,_Info,LocalState,_State,Res,WF) :- !,
    lookup_value_for_existing_id_wf(Id,LocalState,(Trigger,Value),WF), % should normally only occur in LocalState; value introduced by lazy_let
    Trigger = pred_true, % force evaluation
    equal_object_wf(Res,Value,WF).

b_compute_expression2(lazy_let_expr(Id,AssignmentExpr,Expr),_T,_I,LocalState,State,Value,WF) :-
    !,
    add_lazy_let_id_and_expression(Id,AssignmentExpr,LocalState,State,NewLocalState,WF),
    %Trigger = pred_true, % expressions cannot be delayed !? (TO DO: more refined check)
    %block_lazy_compute_expression(Trigger,_,AssignmentExpr,LocalState,State,IdValue,WF,Ai),
    b_compute_expression(Expr,NewLocalState,State,Value,WF).

b_compute_expression2(real(Atom),_T,_I,_LocalState,_State,Res,_WF) :- !, construct_real(Atom,Res).

b_compute_expression2(rec(Fields),_T,_I,LocalState,State,Record,WF) :- !,
    l_compute_field(Fields,LocalState,State,FieldValues,WF),
    construct_record_wf(FieldValues,Record,WF).

b_compute_expression2(record_field(RecEx,Name),_T,_I,LocalState,State,Value,WF) :- !,
    b_compute_expression(RecEx,LocalState,State,RecValue,WF),
    access_record_wf(RecValue,Name,Value,WF).

b_compute_expression2(freetype_set(Id),_T,_I,_LState,_State,Val,_WF) :- !, Val=freetype(Id). %% NOT COVERED (17)

b_compute_expression2(function(Function,FunArg),Type,Info,LocalState,State,Res,WF) :- !,
    b_compute_expression_function(Function,FunArg,Type,Info,LocalState,State,Res,WF).

b_compute_expression2(card(b(Arg1,Type,Info)),integer,OuterInfo,LocalState,State,Card,WF) :- !,
    b_compute_card(Arg1,Type,Info,OuterInfo,LocalState,State,Card,WF).

b_compute_expression2(max(b(Arg1,Type,Info)),integer,_I,LocalState,State,Max,WF) :- !,
    b_compute_max(Arg1,Type,Info,LocalState,State,Max,WF).

b_compute_expression2(min(b(Arg1,Type,Info)),integer,_I,LocalState,State,Min,WF) :- !,
    b_compute_min(Arg1,Type,Info,LocalState,State,Min,WF).

b_compute_expression2(set_extension(Ex),Type,_I,LocalState,State,Res,WF) :- !,
    b_compute_expressions(Ex,LocalState,State,ExValue,WF),
    kernel_call(b_interpreter:convert_list_of_expressions_into_set_wf(ExValue,ValueSet,Type,WF),ExValue,WF, set_extension(Ex)),
    equal_object_wf(Res,ValueSet,WF).

b_compute_expression2(sequence_extension(Ex),_T,_I,LocalState,State,ValueSeq,WF) :- !,
    b_compute_expressions(Ex,LocalState,State,Value,WF),
    kernel_call(b_interpreter:convert_list_of_expressions_into_sequence(Value,ValueSeq),Value,WF,sequence_extension(Ex)).

b_compute_expression2(convert_bool(PRED),_T,_I,LocalState,State,Val,WF) :- !, /* B bool(.) operator */
    b_convert_bool(PRED,LocalState,State,WF,Val).

b_compute_expression2(couple(El1,El2),_T,_I,LocalState,State,Result,WF) :- !, Result = (Val1,Val2),
    b_compute_expression(El1,LocalState,State,Val1,WF),
    b_compute_expression(El2,LocalState,State,Val2,WF).

b_compute_expression2(comprehension_set(Parameters,Condition),_T,Info,LocalState,State,Result,WF) :- !,
    b_compute_comprehension_set(Parameters,Condition,Info,LocalState,State,Result,WF).

b_compute_expression2(recursive_let(TId,TSet),OrigType,OrigInfo,LocalState,State,Result,WF) :- !,
    % LET TId = TSet in TSet
    ( get_texpr_expr(TSet,comprehension_set(Parameters,Condition)) ->
    true % if the argument TSet is a comprehension set,
    % we just add a recursive parameter
    ; get_texpr_set_type(TSet,Type) ->
    % if not, we construct a new comprehension set {x | x:TSet}
    unique_typed_id("_tmparg_",Type,TArg),
    Parameters=[TArg],
    safe_create_texpr(member(TArg,TSet),pred,Condition)
    ;
    add_internal_error('Expected set as argument to recursive_let',
    b_compute_expression2(recursive_let(TId,TSet),OrigType,OrigInfo,LocalState,State,Result,WF)),fail
    ),
    % Generate closure where the references to the recursion are kept
    % add recursion ID to parameters to prevent removal of references during compilation
    generate_recursive_closure(TId,recursion,[TId|Parameters],Condition,LocalState,State,Closure1,WF),
    % add_message(b_interpreter,'Recursive Let for: ',TId,TId),
    % remove recursion ID from parameters after compilation
    Closure1=closure([_|P],[_|T],Cond),RClosure=closure(P,T,Cond),
    % Generate closure where the references to the recursion are kept
    generate_recursive_closure(TId,RClosure,Parameters,Condition,LocalState,State,Result,WF).

b_compute_expression2(general_sum(Ids,Condition,Expression),Type,Info,LocalState,State,SumResult,WF) :- !,
    b_general_sum_or_mul(Ids,Condition,Expression,Type,Info,LocalState,State,SumResult,WF,sum).

b_compute_expression2(general_product(Ids,Condition,Expression),Type,Info,LocalState,State,MulResult,WF) :- !,
    b_general_sum_or_mul(Ids,Condition,Expression,Type,Info,LocalState,State,MulResult,WF,mul).

b_compute_expression2(if_then_else(If,Then,Else),T,_I,LocalState,State,Value,WF) :- !,
    b_try_check_boolean_expression_wf(If,LocalState,State,WF,PredRes),
    (var(PredRes), can_get_full_fd_value(T), preferences:preference(use_clpfd_solver,true),
    always_well_defined(Then), always_well_defined(Else)
    % Note: always_well_defined_or_disprover_mode probably not ok, as we evaluate the expressions unconditionally
    -> b_clpfd_if_then_else(PredRes,T,Then,Else,LocalState,State,Value,WF)
    ; b_compute_if_then_else(PredRes,Then,Else,LocalState,State,Value,WF)
).

b_compute_expression2(let_expression_global(Ids,AssignmentExprs,Expr),_T,Info,LocalState,State,Value,WF) :-
    debug_println(4,global_let(Ids,Info)),
    % store variables globally (not in LocalState) to be visible to subsidiary operation_calls
    !, set_up_localstate_for_global_let(Ids,AssignmentExprs,LocalState,State,LetState,WF),
    b_compute_expression(Expr,LocalState,LetState,Value,WF).

b_compute_expression2(let_expression(Ids,AssignmentExprs,Expr),_T,_I,LocalState,State,Value,WF) :-
    !, set_up_localstate_for_let(Ids,_ParaValues,AssignmentExprs,LocalState,State,LetState,WF),
    b_compute_expression(Expr,LetState,State,Value,WF). %% NOT COVERED (30)

b_compute_expression2(freetype_constructor(Id,Case,Expr),_T,_I,LocalState,State,FreeValue,WF) :-
    !, FreeValue = freeval(Id,Case,Value),
    b_compute_expression(Expr,LocalState,State,Value,WF). %% NOT COVERED (32)

b_compute_expression2(freetype_destructor(Id,Case,Expr),_T,Info,LocalState,State,Value,WF) :-
    !, b_compute_expression(Expr,LocalState,State,freeval(Id,VCase,VValue),WF),
    check_freetype_case(Id,Case,VCase,VValue,Value,Info,WF).

b_compute_expression2(assertion_expression(Cond,ErrMsg,Expr),T,Info,LocalState,State,Value,WF) :- !,
    opt_push_wait_flag_call_stack_info(WF,
    span_predicate(b(assertion_expression(Cond,ErrMsg,b(value(string('')),string,[])),T,Info),LocalState,State),WF2),
    % should we use another term for call stack?
    (get_preference(disprover_mode,true) -> PredRes = pred_true ; true), % in Disprover mode we know Cond must be true
    b_try_check_boolean_expression_no_enum_wf(Cond,LocalState,State,WF2,PredRes), % DO NOT ENUM, unless we cannot reify
    % does not make sense to enumerate PredRes as with pred_false we get no value anyway
    % however, we may get pending co-routines if Cond cannot be reified
    ( PredRes==pred_false ->
    translate_bexpression_with_limit(Cond,100,CS),
    add_wd_error_span(ErrMsg,CS,span_predicate(Cond,LocalState,State),WF2),
    get_last_wait_flag(assertion_expression,WF2,WFC),
    when(nonvar(WFC),
    (ground_value(Value) -> true % we have a WD Error, any Value goes
    ; b_compute_expression(Expr,LocalState,State,Value,WF2) % compute Value; avoid infinite enumeration of possible values; useful e.g. for prj1/prj2 assertion expressions
    ))
    ; b_compute_expression(Expr,LocalState,State,Value,WF),
    add_wd_error_if_false(PredRes,ErrMsg,Cond,span_predicate(Cond,LocalState,State),WF2)
). %% NOT COVERED (34)

b_compute_expression2(multiplication(Arg1,Arg2),integer,Info,LocalState,State,Value,WF) :-
    same_texpr(Arg1,Arg2), !, % is less useful when CLPFD is already turned on, calls square(Arg1,Value,WF)
    b_compute_expression(Arg1,LocalState,State,SV1,WF),
    unary_kernel_call(kernel_objects,square,SV1,Value,WF,multiplication(Arg1,Arg1),integer,Info).

b_compute_expression2(image(Relation,Set),_EType,_Info,LocalState,State,Value,WF) :-
    special_operator_for_image(Relation,Kind,Args),
    % we have closure1(Rel)[Set] or similar -> avoid computing full closure
    !,
    b_compute_expression(Set,LocalState,State,SV,WF),
    b_compute_expressions(Args,LocalState,State,EArgs,WF),
    kernel_call(bsets_clp:image_for_special_operator(Kind,EArgs,SV,Value,WF),[SV|EArgs],WF,image(Relation,Set)).

b_compute_expression2(external_function_call(FunName,Args),EType,Info,LocalState,State,Value,WF) :-
    !,
    b_compute_expressions(Args, LocalState,State, EvaluatedArgs, WF),
    push_wait_flag_call_stack_info(WF,external_call(FunName,EvaluatedArgs,Info),WF2),
    call_external_function(FunName,Args,EvaluatedArgs,Value,EType,Info,WF2).

b_compute_expression2(Expression,EType,Info,LocalState,State,Res,WF) :-
    is_set_type(EType,Type),
    /* avoid evaluating certain expensive expressions:
    convert them into symbolic closures and expand only if really required */
    functor(Expression,UnOp,1),
    symbolic_closure_unary_operator(UnOp),
    /* TO DO: UNFOLD THIS OR WRAP in CONSTRUCTOR */
    arg(1,Expression,BType),
    !, %preferences:get_preference(convert_types_into_closures,true),!,
    % print_message(delayed_un_op(UnOp,BType)),
    b_compute_expression(BType,LocalState,State,ArgValue,WF),
    ( do_not_keep_symbolic_unary(UnOp,ArgValue), unary_function(UnOp,Module,KernelFunction) ->
    /* special treatment for empty set: no need to keep symbolic */
    unary_kernel_call(Module,KernelFunction,ArgValue,Res,WF,Expression,EType,Info)
    ;
    get_texpr_type(BType,ArgType),
    create_texpr(value(ArgValue),ArgType,[],TValue),
    ClosureSetExpression =.. [UnOp,TValue],
    construct_member_closure('_zzzz_unary',Type,Info,ClosureSetExpression,Value),
    (unop_to_be_marked_as_symbolic(UnOp,ArgValue) ->
    mark_closure_as_symbolic(Value,SValue),
    equal_object_wf(Res,SValue,WF)
    ; equal_object_wf(Res,Value,WF))

).

b_compute_expression2(Expression,EType,Info,LocalState,State,Res,WF) :-
    is_set_type(EType,Type),
    /* avoid evaluating certain expensive expressions:
    convert them into symbolic closures and expand only if really required */
    functor(Expression,BinOp,2),
    arg(1,Expression,BType1),
    arg(2,Expression,BType2),
    kernel_mappings:symbolic_closure_binary_operator(BinOp),
    !,
    %preferences:get_preference(convert_types_into_closures,true),!,
    b_compute_expression(BType1,LocalState,State,ArgValue1,WF),
    (binary_arg1_determines_value(BinOp,ArgValue1,DetResult)
    -> /* print(det(BinOp,ArgValue1)),nl, */
    equal_object_wf(Res,DetResult,b_compute_expression2(BinOp),WF)
    ; b_compute_expression(BType2,LocalState,State,ArgValue2,WF),
    % print_message(delayed_bin_op(BinOp,ArgValue1,ArgValue2)),
    (is_definitely_empty(BinOp,ArgValue1,ArgValue2)
    -> empty_set(Res)
    ; if(do_not_keep_symbolic(BinOp,ArgValue1,ArgValue2,ERes,WF),
    % then:
    equal_object_wf(Res,ERes,b_compute_expression2(BinOp),WF),
    % else:
    (get_texpr_type(BType1,TypeArg1), create_texpr(value(ArgValue1),TypeArg1,[],TArg1),
    get_texpr_type(BType2,TypeArg2), create_texpr(value(ArgValue2),TypeArg2,[],TArg2),
    ClosureSetExpression =.. [BinOp,TArg1,TArg2],
    construct_member_closure('_zzzz_unary',Type,Info,ClosureSetExpression,Value),
    % print('Constructed Symbolic Closure : '), translate:print_bvalue(Value),nl,
    (binop_to_be_marked_as_symbolic(BinOp,ArgValue1,ArgValue2) ->
    mark_closure_as_symbolic(Value,SValue),
    equal_object_wf(Res,SValue,WF)
    ; equal_object_wf(Res,Value,WF))
)
) % if
)
).

b_compute_expression2(Expression,Type,Info,LocalState,State,Value,WF) :-
    functor(Expression,Op,1),
    unary_function(Op,Module,KernelFunction),
    arg(1,Expression,Arg1),!,
    %opt_push_wait_flag_call_stack_info(WF,b_operator_arg_evaluation(Op,1,[SV1],Arg1),WF1),
    b_compute_expression(Arg1,LocalState,State,SV1,WF),
    unary_kernel_call(Module,KernelFunction,SV1,Value,WF,Expression,Type,Info).

b_compute_expression2(Expression,Type,Info,LocalState,State,Value,WF) :-
    functor(Expression,Op,2),
    binary_function(Op,Module,KernelFunction),
    arg(1,Expression,Arg1),
    arg(2,Expression,Arg2),!,
    %opt_push_wait_flag_call_stack_info(WF,b_operator_arg_evaluation(Op,1,[SV1,_],Arg1),WF1),
    b_compute_expression(Arg1,LocalState,State,SV1,WF),
    (binary_arg1_determines_value(Op,SV1,Result) % we could disable this if find_abort_values=true or if SV1 not guaranteed to be wd
    ->
    equal_object_wf(Value,Result,b_compute_expression2(Op),WF)
    ; b_compute_expression(Arg2,LocalState,State,SV2,WF),
    binary_kernel_call(Module,KernelFunction,SV1,SV2,Value,WF,Expression,Type,Info)
).

b_compute_expression2(operation_call_in_expr(Operation,Parameters),_T,Info,LocalState,State,Value,WF) :-
    !, def_get_texpr_id(Operation,op(OperationName)),
    % TODO: check that this is a query operation; probably done in type checker
    b_execute_operation_in_expression(OperationName,LocalState,State,Parameters,Value,Info,WF).

b_compute_expression2(E,T,Info,_L,_S,_R,_WF) :-
    (T==pred -> add_internal_error('Uncovered expression; looks like a predicate in the wrong place: ',b(E,T,Info))
    ; T==subst -> add_internal_error('Uncovered expression; looks like a substitution in the wrong place: ',b(E,T,Info))
    ; add_internal_error('Uncovered expression: ',b(E,T,Info))
    ),
    print_functor(E), print(' : '), print(T),nl,fail.

b_compute_expression_function/8

b_compute_expression_function(Function,FunArg,Type,Info,LocalState,State,Res,WF) :-
    preferences:preference(find_abort_values,false), % the treatment below will not check, e.g., if the set extension is really a function
    is_extension_function(Function,FInfo,ExFun), !,
    /* a set extension applied to an argument: in some cases we can can first evaluate the argument,
    and then avoid having to compute the set_extension for all non-matching args */
    b_compute_expression(FunArg,LocalState,State,ArgValue,WF),
    % TO DO : should we only do this if ArgValue is known ?? otherwise the standard treatment is better ??
    % Note: b_compiler has a special rule to not remove this optimisation
    Span = span_predicate(b(function(Function,FunArg),Type,Info),LocalState,State),
    opt_push_wait_flag_call_stack_info(WF,function_call(Function,ArgValue,Info),WF2), % small performance hit; hence we only push onto call_stack in TRACE_INFO mode
    ((memberchk(contains_wd_condition,FInfo) ; % relevant for test 1302; but machine seems to contain real WD error
    preferences:preference(use_clpfd_solver,false) ;
    ground_value(ArgValue))
    -> b_apply_function_set_extension(ExFun,ArgValue,LocalState,State,Res,WF2,Span)
    ; /* the standard treatment can infer information about the result,... in clpfd_mode */
    b_compute_expression(Function,LocalState,State,FValue,WF),
    get_texpr_type(Function,FunctionType),
    kernel_call_apply_to(FValue,ArgValue,Res,FunctionType,Span,WF2)).

b_compute_expression_function(Function,FunArg,_Type,Info,LocalState,State,Value,WF) :-
    special_operator_for_image(Function,Kind,Args),!, % detect e.g. iterate(rel,k)(x)
    b_compute_expression(FunArg,LocalState,State,SV,WF),
    b_compute_expressions(Args,LocalState,State,EArgs,WF),
    kernel_call(bsets_clp:apply_fun_for_special_operator(Kind,EArgs,SV,Value,WF,Info),
    [SV|EArgs],WF,function(Function,FunArg)).

b_compute_expression_function(Function,Arg,Type,Info,LocalState,State,Value,WF) :-
    opt_push_wait_flag_call_stack_info(WF,function_call(Function,ArgValue,Info),WF2),
    b_compute_expression(Function,LocalState,State,FValue,WF2),
    b_compute_expression(Arg,LocalState,State,ArgValue,WF2),
    Span = span_predicate(b(function(Function,Arg),Type,Info),LocalState,State),
    get_texpr_type(Function,FunctionType),
    % TODO: do we still need the span predicate when we have the function_call call_stack infos?
    kernel_call_apply_to(FValue,ArgValue,Value,FunctionType,Span,WF2).

b_compute_expression_nowf/4

b_compute_expression_nowf/6

b_compute_expression_nowf/7

b_compute_expression_when2/6

Block: b_compute_expression_when2(?,?,?,?,?,-)

b_compute_expressions/5

b_compute_expressions_when2/6

b_compute_field/5

b_compute_if_then_else/7

Block: b_compute_if_then_else(-,?,?,?,?,?,?)

b_compute_max/7

b_compute_min/7

b_convert_bool/5

b_convert_bool_timeout/7

Description:
print('finished bool(.) check : '), translate:print_bexpr(Pred),nl,translate:print_bstate(LocalState),nl.

b_convert_bool_wf0/6

Description:
print('bool(.)=TRUE '), translate:print_bexpr(Pred),nl, %%
print('bool(.)=FALSE '), translate:print_bexpr(Pred),nl, %%
print('bool(.) check : '), translate:print_bexpr(Pred),nl, % obsv(LocalState),

Block: b_convert_bool_wf0(?,?,?,?,-,-)

b_convert_bool_wf0_timeout/8

Block: b_convert_bool_wf0_timeout(?,?,?,?,-,-,?,?)

b_enum_not_test_equivalence/7

Block: b_enum_not_test_equivalence(?,?,?,?,?,-,?)

b_enum_test_equivalence/7

Block: b_enum_test_equivalence(?,?,?,?,?,-,?)

b_enumerate_exists/6

b_enumerate_exists_aux_ground/5

Block: b_enumerate_exists_aux_ground(-,?,?,?,?)

b_execute_assertion/8

b_execute_assertion_block/9

Block: b_execute_assertion_block(-,?,?,?,?,?,?,?,?)

b_execute_becomes_such/7

b_execute_choice/8

Block: b_execute_choice(?,?,?,?,?,?,-,?)

b_execute_else_list/7

b_execute_else_list2/9

Block: b_execute_else_list2(-,?,?,?,?,?,?,-,?)

b_execute_else_list3/9

b_execute_initialisation_statement/7

b_execute_inner_statement/7

b_execute_inner_statement/9

Block: b_execute_inner_statement(?,?,?,?,?,?,?,-,?)

b_execute_let_definitions/4

b_execute_operation2/12

Description:
% we do not want skip the evaluation of a guard of an operation with parameters
(Parameters==[] ->true; retractall(pge_algo:do_not_evaluate_guard)),

b_execute_operation3/15

b_execute_operation3(classic,Name,Operation,InState,NewOutState,
    Body,Parameters,ParaValues,Results,ResultInputValues,NormalisedResultValues,TopLevel,
    [], % [path(Path)], % as path is currently filtered out anyway and not stored !
    WF,OR) :-
    %print('Attempting Operation ----> '),print(Name),nl,
    empty_state(EmptyState),
    set_up_typed_localstate(Parameters,ParaValues,ParamTypedVals,EmptyState,LocalState,positive),
    l_expand_and_normalise_values(ParaValues,NormalisedParaValues,Parameters), % not useful for call_b_execute_operation2
    create_full_operation(Name,Results,NormalisedParaValues, % ditto
    NormalisedResultValues,Operation),
    set_up_undefined_localstate_with_predefined(Results,ResultInputValues,InState,NewInState),
    /* to avoid error messages with sequential composition (store_intermediate_updates) */
    check_additional_guard(TopLevel,LocalState,NewInState,WF),
    (TopLevel==true
    -> b_execute_top_level_statement(Body,LocalState,NewInState,OutState,WF,_Path1,OR)
    ; b_execute_statement(Body,LocalState,NewInState,OutState,WF,_Path2,OR)
    ),
    b_tighter_enumerate_all_values(ParamTypedVals,WF), % moved afer execute for performance reasons; see PerformanceTests/ParameterEnumeration.mch
    % print_bt_message('Operation Successful ------> '),
    (preferences:preference(treat_outermost_pre_as_select,true),
    preferences:preference(require_operations_to_assign_all_outputs,true)
    -> ReportError = true ; ReportError = false),
    get_results(Results,OutState,NormalisedResultValues,NewOutState,ReportError,normalise_results,WF).

b_execute_operation3(eventb_operation(ChangeSet,ParaValues,Operation),
    _Name,Operation, InState,Updates,
    TBody,Parameters,ParaValues,[],[],[],true,TransInfo,WF,OutputRequired) :-
    % TO DO: check if need to pass _OutputRequired to b_event
    b_execute_event_with_change_set_wf(TBody,Parameters,ParaValues,InState,ChangeSet,Updates,TransInfo,WF,OutputRequired).

b_execute_operation_in_expression/7

b_execute_operation_with_parameters/12

b_execute_sequence/7

b_execute_statement/6

b_execute_statement/7

b_execute_statement2/8

Description:
NOT COVERED
TODO: remove this
observe_state(TypedVals,WF,0), b_tracetest_boolean_expression(PreCond,NewLocalState,InState,WF,one), %% comment in for debugging

b_execute_statement2(block(Stmt),_,LS,IS,OS,WF,Path,OR) :- !,
    b_execute_statement(Stmt,LS,IS,OS,WF,Path,OR). %% NOT COVERED

b_execute_statement2(assign(LHS,Exprs),Info,LocalState,InState,OutState,WF,assign,OR) :- !,
    /* Var1, ..., VarN := Expr1, ..., ExprN */
    /* also: Var1, fun1(arg), ... := Expr1, Expr2, ... */
    opt_add_source_location_hits(Info,1),
    b_compute_assign_expressions_when(Exprs,LocalState,InState,VALs,WF,OR),% VALs - a list of computed values
    b_assign_values_or_functions(LHS,VALs,LocalState,InState,OutState,WF,OR).

b_execute_statement2(assign_single_id(IDE,Expr),Info,LocalState,InState,OutState,WF,assign,_OR) :-
    get_texpr_id(IDE,ID),!,
    opt_add_source_location_hits(Info,1),
    b_compute_expression(Expr,LocalState,InState,Value,WF), % b_compute_assign_expressions_when
    %b_compute_assign_expressions_when([Expr],LocalState,InState,[Value],WF),
    OutState=[bind(ID,Value)].

b_execute_statement2(choice(ChoiceList),_,LocalState,InState,OutState,WF,Path,OR) :- !,
    /* CHOICE LHS OR RHS OR ... END */
    get_wait_flag(2,choice,WF,WFC), % % was 2.0, maybe use length of ChoiceList as Priority ??
    b_execute_choice(ChoiceList,LocalState,InState,OutState,WF,Path,WFC,OR).

b_execute_statement2(becomes_element_of(LHS,RHS), /* LHS :: RHS */
    Info,LocalState,InState,OutState,WF,becomes_element_of,_OR) :- !,
    % LHS must be of the form Var1,..,Vark where all variables are disjoint
    opt_add_source_location_hits(Info,1),
    b_compute_expression(RHS,LocalState,InState,ValueSet,WF),
    check_element_of_wf(SingleValue,ValueSet,WF),
    ground_det_wait_flag(WF), %% TODO: remove this
    convert_pairs_into_list(LHS,SingleValue,ValList),
    set_up_typed_localstate(LHS,ValList,TypedVals,[],OutState,positive),
    b_tighter_enumerate_all_values(TypedVals,WF).

b_execute_statement2(becomes_such(Vars,Condition), /* Vars : Condition */
    Info,LocalState,InState,OutState,WF,becomes_such,_OR) :- !,
    opt_add_source_location_hits(Info,1),
    b_execute_becomes_such(Vars,Condition,LocalState,InState,OutState,_,WF).

b_execute_statement2(sequence(Seq), /* LHS ; RHS */
    _,LocalState,InState,OutUpdates,WF,Path,OR) :- !, %pe_print(sequence(Seq,InState)),
    b_execute_sequence(Seq,LocalState,InState,OutUpdates,WF,Path,OR).

b_execute_statement2(precondition(PreCond,Body),_,LocalState,InState,OutState,WF,Path,OR) :- !,
    %print('*** Non-outermost PRE construct'),nl,
    Path=pre(PreRes,IPath),
    b_try_check_boolean_expression(PreCond,LocalState,InState,WF,PreRes),
    %used to be: ground_det_wait_flag(WF),
    check_precondition_result(PreRes,PreCond,LocalState,InState,WF),
    (PreRes == pred_true -> b_execute_statement(Body,LocalState,InState,OutState,WF,IPath,OR)
    ; PreRes == pred_false -> IPath = not_executed
    ; b_execute_inner_statement(Body,LocalState,InState,OutState,WF,IPath,OR) % with extra waitflag
).

b_execute_statement2(assertion(PreCond,Body),_,LocalState,InState,OutState,WF,Path,OR) :- !,
    b_execute_assertion(PreCond,Body,LocalState,InState,OutState,WF,Path,OR).

b_execute_statement2(select(Whens),_, LocalState, InState, OutState,WF,select(Nr,Path),OR) :- !,
    get_texpr_expr(TExpr,select_when(PreCond, Body)), % info field not used for select_when
    optimized_nth1(Nr, Whens, TExpr), % THIS IS A CHOICE POINT if length(Whens)>1 ! <-------- TO DO guard
    b_test_boolean_expression(PreCond,LocalState,InState,WF),
    %used to call: ground_det_wait_flag(WF), now execute inner statement delays
    b_execute_inner_statement(Body,LocalState,InState,OutState,WF,Path,OR).

b_execute_statement2(select(Whens,Else), Infos, LocalState, InState, OutState,WF,Path,OR) :- !,
    (
    b_execute_statement2(select(Whens), Infos, LocalState, InState, OutState,WF,Path,OR)
    ; % THIS IS A CHOICE POINT ! <-------- TO DO guard
    findall(PC,
    (member(SW,Whens),get_texpr_expr(SW,select_when(PC,_))), AllPreconds),
    b_not_test_list_of_boolean_expression(AllPreconds,LocalState,InState,WF),
    Path = select(else,IPath),
    b_execute_inner_statement(Else,LocalState,InState,OutState,WF,IPath,OR)
).

b_execute_statement2(var(Parameters,Body), /* VAR _ IN _ substitution */
    _,LocalState,InState,NewOutState,WF,var(Path),OR) :- !,
    /* introduces a new variable that can be assigned to */
    split_names_and_types(Parameters,Names,_),
    delete_variables_from_state(Names,InState,InState1), % in case any local parameter name is also a constant/variable: remove it % but if we do an operation_call: we leave context and it becomes visible again !!
    % otherwise we may think there are two updates, e.g., in WHILE loop; see Rule_DB_SIGAREA_0030 from test 1303
    set_up_undefined_localstate(Parameters,InState1,NewInState),
    delete_variables_from_state(Names,LocalState,NewLocalState),
    %check_valid_store(InState,var_in_state), check_valid_store(LocalState,var_local_state),
    b_execute_statement(Body,NewLocalState,NewInState,OutState,WF,Path,OR),
    % check_valid_store(OutState,var_out_state),
    filter_results(Parameters,OutState,NewOutState,WF)
.

b_execute_statement2(let(Parameters,Defs,Body), /* LET _ BE _ IN _ */
    _,LocalState,InState,OutState,WF,let(Path),OR) :- !,
    set_up_typed_localstate(Parameters,LocalState,NewLocalState),
    b_execute_let_definitions(Defs,NewLocalState,InState,WF),
    b_execute_statement(Body,NewLocalState,InState,OutState,WF,Path,OR).

b_execute_statement2(lazy_let_subst(Id,IdExpr,Body),_,LocalState,InState,OutState,WF,lazy_let(Path),OR) :-
    !,
    add_lazy_let_id_and_expression(Id,IdExpr,LocalState,InState,NewLocalState,WF),
    b_execute_statement(Body,NewLocalState,InState,OutState,WF,Path,OR).

b_execute_statement2(any(Parameters,PreCond,Body), /* ANY _ WHERE */
    Info,LocalState,InState,OutState,WF0,any(Bindings,Path),OR) :- !, %statistics(runtime,_),
    %print('ANY: '), print_bexpr(PreCond),nl,
    set_up_typed_localstate(Parameters,FreshVars,TypedVals,LocalState,NewLocalState,positive),
    create_any_bindings(Parameters,FreshVars,Bindings),
    push_wait_flag_call_stack_info(WF0,quantifier_call('ANY',Parameters,FreshVars,Info),WF),
    b_test_inner_boolean_expression(PreCond,NewLocalState,InState,WF), /* check WHERE */
    %%observe_state(TypedVals,WF,0), b_tracetest_boolean_expression(PreCond,NewLocalState,InState,WF,one), %% comment in for debugging
    b_tighter_enumerate_all_values(TypedVals,WF), % moved enumeration after test; in case WF already instantiated
    %TODO: check if we can use b_tighter_enumerate_values_in_ctxt
    b_execute_statement(Body,NewLocalState,InState,OutState,WF,Path,OR). /* should we use b_execute_inner_statement/LWF here ?? */

b_execute_statement2(skip, /* SKIP */
    Info,_LocalState,_InState,OutState,_WF,skip,_OR) :- !,
    opt_add_source_location_hits(Info,1),
    OutState = [].

b_execute_statement2(parallel(Statements), /* LHS || RHS */ %@@@
    _,LocalState,InState,OutState,WF,parallel(Paths),OR) :- !,
    b_execute_statements_in_parallel(Statements,LocalState,InState,OutState,WF,Paths,OR).

b_execute_statement2(init_statement(Stmt),_,LocalState,InState,OutState,WF,Path,OR) :- !,
    /* Like block: but
    writes error messages if statement fails */ %@@@
    (preferences:get_preference(provide_trace_information,true)
    -> nl,print(' =INIT=> '),translate:print_subst(Stmt),nl, flush_output(user_output),
    statistics(walltime,[Tot1,_])
    ; true),
    if(b_execute_initialisation_statement(Stmt,LocalState,InState,OutState,WF,Path,OR),
    (
    (preferences:get_preference(provide_trace_information,true)
    -> statistics(walltime,[Tot2,_]), Tot is Tot2-Tot1,
    format(' [=OK= ~w ms]~n',[Tot]), flush_output(user_output)
    ; true)
    ),
    (translate:translate_substitution(Stmt,TStmt),
    (bmachine:b_machine_temp_predicate(_)
    -> add_message_wf(initialisation_fails,'Initialisation statement cannot be executed with extra predicate: ',TStmt,Stmt,WF)
    ; add_error_wf(initialisation_fails,'Initialisation statement fails: ',TStmt,Stmt,WF)
    ), fail
)
).

b_execute_statement2(if(IfList),_,LocalState,InState,OutState,WF,if,OR) :- !,
    %LWF=1,
    LWF='$GENERATE_ON_DEMAND',
    b_execute_else_list(IfList,LocalState,InState,OutState,WF,LWF,OR).

b_execute_statement2(operation_call(Operation,Results,Parameters),Info,LocalState,InState,OutState,WF,
    operation_call(OperationName,ParamValues,ResultValues,InnerPath),OR) :- !,
    def_get_texpr_id(Operation,op(OperationName)),
    b_execute_operation_with_parameters(OperationName,LocalState,InState,Results,
    Parameters,OpOutState,ParamValues,ResultValues,InnerPath,Info,WF,OR),
    split_names_and_types(Results,ResultingIDs,_),
    store_values(ResultingIDs, ResultValues, ResultsOutState),
    combine_updates(ResultsOutState,OpOutState,OutState).

b_execute_statement2(while(COND,STMT,INV,VARIANT),
    Info,LocalState,InState,OutState,WF0,while,_OR) :- !,
    %hit_profiler:add_profile_hit(while(COND,WF),2),
    % we may go around the loop many times: avoid carrying around unused variables
    get_while_reads_write_info_and_filter_state(Info,LocalState,InState,LS,IS,ModVars),
    push_wait_flag_call_stack_info(WF0,b_operator_call('WHILE',[],Info),WF), % TODO: provide subst. call stack entry
    %print_message(execute_while(LocalState,InState)),
    b_compiler:b_optimize(INV,ModVars,LS,IS,CINV,WF),
    b_compiler:b_optimize(COND,ModVars,LS,IS,CCOND,WF),
    b_compiler:b_optimize(VARIANT,ModVars,LS,IS,CVARIANT,WF),
    %,b_compiler:b_compile(STMT,ModVars,LS,IS,CSTMT,WF)
    % TO DO: maybe exclude in one go; use ordered approach ?
    %exclude(unused_variable(ModVars),LS,LS2), % only keep modified vars; all other compiled
    %exclude(unused_variable(ModVars),IS,IS2), % only keep modified vars; all other compiled
    b_compute_expression(CVARIANT,LS,IS,VarVal,WF),
    b_execute_while(CCOND,STMT,CINV,CVARIANT,ModVars,VarVal,LS,IS,OutState,WF).

b_execute_statement2(external_subst_call(FunName,Args),Info,LocalState,State,OutState,WF,external(FunName),_OR) :-
    !, b_compute_expressions(Args, LocalState,State, EvaluatedArgs, WF),
    push_wait_flag_call_stack_info(WF,external_call(FunName,EvaluatedArgs,Info),WF2),
    call_external_substitution(FunName,EvaluatedArgs,State,OutState,Info,WF2).

b_execute_statement2(E,I,LS,S,O,WF,Path,OR) :-
    add_internal_error('Uncovered statement: ',b_execute_statement2(E,I,LS,S,O,WF,Path,OR)),
    print_functor(E),nl,fail.

b_execute_statement_list_when_state_set/8

b_execute_statement_when_state_set2/9

Block: b_execute_statement_when_state_set2(?,?,?,?,?,?,?,-,?)

b_execute_statements_in_parallel/7

b_execute_top_level_operation_update/5

b_execute_top_level_operation_update_wf/6

b_execute_top_level_operation_wf/8

b_execute_top_level_statement/7

b_execute_top_level_statement2/8

b_execute_while/10

Block: b_execute_while(?,?,?,?,?,-,?,?,?,?)

b_execute_while1/10

Block: b_execute_while1(?,?,?,?,?,-,?,?,?,?)

b_execute_while_body/10

b_execute_while_body(_COND,_STMT,_INVARIANT,VAR,_PV,VarVal,LocalState,InState,_OutState,WF) :-
    VarVal<0, !, % more efficient than is_not_natural(int(VarVal)),
    %ground_constraintprop_wait_flags(WF),
    % add_abort_error_span will fail; hence no need to set _OutState
    add_abort_error_span(while_variant_error,'While VARIANT not NATURAL:',VarVal,span_predicate(VAR,LocalState,InState),WF).

b_execute_while_body(_COND,_STMT,_INVARIANT,VAR,PrevVariantValue,VarVal,LocalState,InState,_OutState,WF) :-
    % check no longer required VarVal>=0,%is_natural(int(VarVal),WF),
    PrevVariantValue \= none,
    PrevVariantValue =< VarVal, !, %less_than_equal(int(PrevVariantValue),int(VarVal)),
    %ground_constraintprop_wait_flags(WF),
    % add_abort_error_span will fail; hence no need to set _OutState
    ajoin(['VARIANT = ',VarVal,', previous value = ',PrevVariantValue],Details),
    add_abort_error_span(while_variant_error,'While VARIANT not decreasing:',
    Details,span_predicate(VAR,LocalState,InState),WF).

b_execute_while_body(COND,STMT,INV,VARIANT,_PrevVariantValue,VarVal,LocalState,InState,OutState,WF) :-
    % check no longer required due to cuts above %VarVal>=0, %is_natural(int(VarVal),WF),
    %(PrevVariantValue==none -> true ; less_than(int(VarVal),int(PrevVariantValue))),
    %ground_constraintprop_wait_flags(WF), % seems to slow down interpretation
    copy_wf_start(WF,while_body,CWF),
    b_execute_statement(STMT,LocalState,InState,LHSUpdates,CWF,_Path1,output_required),
    copy_wf_finish(WF,CWF),
    ground_det_wait_flag(WF), % TODO: remove this
    store_intermediate_updates_wf(InState,LHSUpdates,IntermediateState,STMT,WF),
    check_state_skeleton_bound(LHSUpdates,Bound), % otherwise variable lookups will cause problems; ensures IntermediateState skeleton bound
    b_execute_while_when_state_set(COND,STMT,INV,VARIANT,VarVal,LocalState,IntermediateState,OutState,WF,Bound).

b_execute_while_idle/11

Block: b_execute_while_idle(?,?,?,?,?,?,?,?,?,?,-)

b_execute_while_loop/10

Block: b_execute_while_loop(?,?,?,?,-,?,?,?,?,?) b_execute_while_loop(?,?,?,?,?,-,?,?,?,?)

b_execute_while_loop_block/11

Block: b_execute_while_loop_block(-,?,?,?,?,?,?,?,?,?,?)

b_execute_while_when_state_set/10

Block: b_execute_while_when_state_set(?,?,?,?,?,?,?,?,?,-)

b_expand_closure_forall_to_list/3

Description:
(print_bt_message(expanding_forall_closure(Parameters,ClosureBody,ParValues)), %%
,print_bt_message(expanded(Parameters,ParValues)) ) %%

b_expand_compute_comprehension_set/4

b_for_all/7

b_for_all_aux/8

Block: b_for_all_aux(-,?,?,?,?,?,?,?)

b_for_all_aux2/7

b_for_all_aux3/8

b_for_all_find_counter_example/7

b_general_sum_or_mul/10

b_general_sum_or_mul_over_set/9

Block: b_general_sum_or_mul_over_set(?,-,?,?,?,?,?,?,?)

b_generate_closure_if_necessary/6

b_generate_for_all_domain2/8

b_generate_for_all_domain2(Closure,_Parameters,_,LHS,RHS,ForAllDomain,NewRHS,WF) :-
    (LHS=b(truth,pred,_) ; ground_value(Closure)),
    !, NewRHS=RHS, % nl,print('FORALL EXPAND: '),(ground_value(Closure) -> print(ground(_Parameters)),nl, print_bexpr(LHS),nl ; print('NONGROUND!!'),nl,print_bexpr(RHS),nl),
    b_expand_closure_forall_to_list(Closure,ForAllDomain,WF).

b_generate_for_all_domain2(_,Parameters,_,LHS,RHS,ForAllDomain,NewRHS,WF) :-
    is_a_conjunct(LHS,_,_), % otherwise we have already checked for set_membership above !
    LHS_Membership = b(member(_,_),_,_), % TO DO: also allow conjuncts
    member_conjunct(LHS_Membership,LHS,RestLHS),
    % !(x). ( x:Set & RestLHS => RHS) ---> !(x).(x:Set => (RestLHS => RHS))
    is_for_all_set_membership_predicate(LHS_Membership,Parameters,Set,Pattern,ParameterValues),
    max_cardinality_ok_for_expansion(Set,100,[],[]), % TO DO: simplify LS,S argument <----
    !,
    % as we expand Set without RHS predicate, check if this is ok
    % indeed maximum cardinality of Set could be infinite !! !x.(x:NATURAL1 & x P)
    % print('Splitting for all conjunct: '), print(Parameters),nl, print_bexpr(LHS_Membership),nl,print_bexpr(RestLHS),nl,
    perfmessage_bexpr(good(forall),'Splitting LHS of forall: ',LHS),
    NewRHS = b(implication(RestLHS,RHS),pred,[]), % TO DO: extract & join info
    b_generate_set_for_all_domain(Set,[],[],Pattern,ParameterValues,ForAllDomain,WF).

b_generate_for_all_domain2(Closure,_Parameters,ParCard,LHS,RHS,ForAllDomain,NewRHS,WF) :-
    (is_inf_or_overflow_card(ParCard) -> true ; ParCard>8),
    !,
    NewRHS=RHS,
    perfmessage_bexpr(forall,'No optimisations applicable to forall (will delay until all variables are bound): ',LHS), % maybe we should generate this message only if ForAllDomain is var ?
    b_expand_closure_forall_to_list(Closure,ForAllDomain,WF).

b_generate_for_all_domain2(_Closure,Parameters,ParCard,LHS,RHS,ForAllDomain,NewRHS,WF) :-
    NewLHS=b(truth,pred,[]), NewRHS=b(implication(LHS,RHS),pred,[]),
    b_generate_forall_closure(Parameters,NewLHS,[],[],Closure,WF),
    perfmessages_bexpr(good(forall),['Expanding forall with finite parameter type, card = ',ParCard,': '],LHS),
    b_expand_closure_forall_to_list(Closure,ForAllDomain,WF).

b_generate_for_all_list_domain1/9

b_generate_for_all_list_domain_nolwf/8

b_generate_forall_closure/6

b_generate_rec_closure_aux/7

b_generate_set_for_all_domain/7

b_global_set_or_free_type/3

b_initialise_machine/4

b_initialise_machine2/4

Description:
MOVED HERE TO AVOID that target values are enumerated before initialisation effect computed

b_initialise_machine2(ConstantsState,NormalisedInitialVarsState,FullInitialState,Path) :-
    /* InitialVarsState is an ouput */
    b_get_initialisation_from_machine(InitStatement,OType),
    ( InitStatement=[] ->
    Path = [],
    add_message(b_initialise_machine,'Machine has no INITIALISATION statement(s)!'),
    NormalisedInitialVarsState = [],
    FullInitialState = ConstantsState
    ; OType == classic ->
    Path = [path(PathInfo)],
    b_get_machine_variables(DeclaredVars),
    set_up_undefined_localstate(DeclaredVars,ConstantsState,NewInState),
    /* this is if the INITIALISATION has a sequential composition; to avoid error messages */
    get_texpr_info(InitStatement,PosInfo),
    init_wait_flags_with_call_stack(WF,[operation_call('INITIALISATION',[],PosInfo)]),
    (bmachine:b_machine_temp_predicate(_)
    -> InitStatement2=InitStatement /* avoid enumerating each init statement in parallel in case additional guard links them */
    ; translate_init_statements(InitStatement,InitStatement2)
    ),
    b_execute_statement(InitStatement2,[],NewInState,InitialVarsState,WF,PathInfo),
    check_additional_guard(true,InitialVarsState,ConstantsState,WF),
    % Warning: in Z mode (e.g. test 565) the variable skeleton may not yet be set up !
    sort_variable_binding(InitialVarsState,NormalisedInitialVarsState),
    append(NormalisedInitialVarsState,ConstantsState,FullInitialState), % put constants at end to make sharing of complete tail-list easier for successor states; should be compatible with order in expand_const_and_vars
    split_names_and_types(DeclaredVars,DeclaredNames,DeclaredTypes),
    ground_wait_flags(WF),

    b_enumerate_values_in_store(DeclaredNames,DeclaredTypes,_,InitialVarsState,WF) %% MOVED HERE TO AVOID that target values are enumerated before initialisation effect computed
    ; OType = eventb_operation(_ChangeSet,ParaValues,_Operation) ->
    prepare_eventb_initialisation(ConstantsState,InitialVarsUnNormState,FullInitialUnNormState),
    get_texpr_expr(InitStatement,
    rlevent(_Name,_Sec,_Stat,Parameters,_Grd,_Thm,_Act,_VWit,_PWit,_Unmod,_AbsEv)),
    b_execute_event('initialisation',InitStatement,Parameters,ParaValues,ConstantsState,FullInitialUnNormState,Path),
    normalise_store(InitialVarsUnNormState,NormalisedInitialVarsState),
    normalise_store(FullInitialUnNormState,FullInitialState) % a bit of redundant work here; we do the work twice and try to normalise constants again !
    ),
    b_check_valid_state(FullInitialState).

b_lambda_result_equal_boolean_expression/5

b_not_not_test_exists_aux/4

b_not_test_atomic_boolean_expression2/7

Description:
print('REUSED (not): '), translate:print_bexpr(Pred),nl,

b_not_test_atomic_boolean_expression2(exists(Parameters,RHS),Infos,LocalState,State,WF,Ai,Ao) :- !,
    /* #ID.(RHS) */
    Ai=Ao,
    b_not_test_exists(Parameters,RHS,Infos,LocalState,State,compile,WF).

b_not_test_atomic_boolean_expression2(forall(Parameters,LHS,RHS),Infos,LocalState,State,WF,Ai,Ao) :- !,
    /* !ID.(LHS => RHS) */
    Ai=Ao,
    safe_create_texpr(negation(RHS),pred,Negation),
    conjunct_predicates_with_pos_info(LHS,Negation,Condition),
    % conjunct_predicates merges the used_ids Info in Condition
    b_test_exists(Parameters,Condition,Infos,LocalState,State,WF).

b_not_test_atomic_boolean_expression2(let_predicate(Ids,AssignmentExprs,Pred),Infos,LocalState,State,WF,Ai,Ao) :-
    !,Ai=Ao, % any expression inside the LET cannot be safely reused
    set_up_localstate_for_let(Ids,ParaValues,AssignmentExprs,LocalState,State,LetState,WF),
    opt_push_wait_flag_call_stack_quantifier_info(WF,let_quantifier,Ids,ParaValues,Infos,WF2),
    b_not_test_boolean_expression(Pred,LetState,State,WF2). % NOT COVERED (10)

b_not_test_atomic_boolean_expression2(freetype_case(Freetype,Case,Expr),_,LocalState,State,WF,Ai,Ao) :-
    !,Ai=Ao,b_compute_expression(Expr,LocalState,State,freeval(Freetype,RealCase,_),WF),
    dif(RealCase,Case). % NOT COVERED (11)

b_not_test_atomic_boolean_expression2(finite(SetExpr),_,LocalState,State,WF,Ai,Ao) :-
    !, Ai=Ao,b_compute_expression(SetExpr,LocalState,State,Value,WF),
    kernel_call_predicate(is_infinite_set_wf(Value,WF),kernel_objects,WF,finite(SetExpr)).

b_not_test_atomic_boolean_expression2(kodkod(ProblemId,_),_,LocalState,State,WF,Ai,Ao) :-
    !,Ai=Ao,get_wait_flag1(kodkod_negative_call,WF,WF0),
    kodkod_request(ProblemId,neg,LocalState,State,WF0). % NOT COVERED (12)

b_not_test_atomic_boolean_expression2(partition(LHS,RHS),Info,LocalState,State,WF,Ai,Ao) :- !,
    b_interpreter_check:register_predicate(partition(LHS,RHS),Info,pred_false,Reused,Ai,Ao),
    (Reused==true -> true
    ; b_compute_expression(LHS,LocalState,State,SV1,WF),
    l_compute_expression(RHS,LocalState,State,SV2,WF), % RHS is Prolog list of expressions
    kernel_call_predicate(not_partition_wf(SV1,SV2,WF),kernel_objects,WF,partition(LHS,RHS))
).

b_not_test_atomic_boolean_expression2(external_pred_call(FunName,Args),Info,LocalState,State,WF,Ai,Ao) :-
    !, Ai=Ao,
    (do_not_evaluate_args(FunName) -> EvaluatedArgs=[]
    ; b_compute_expressions(Args, LocalState,State, EvaluatedArgs, WF)),
    push_wait_flag_call_stack_info(WF,external_call(FunName,EvaluatedArgs,Info),WF2),
    call_external_predicate(FunName,Args,EvaluatedArgs,LocalState,State,pred_false,Info,WF2).

b_not_test_atomic_boolean_expression2(Pred,Info,LocalState,State,WF,Ai,Ao) :-
    b_interpreter_check:register_predicate(Pred,Info,pred_false,Reused,Ai,Ao),
    (Reused==true
    -> %% print('REUSED (not): '), translate:print_bexpr(Pred),nl,
    true
    ; b_not_test_atomic_boolean_expression3(Pred,Info,LocalState,State,WF)).

b_not_test_atomic_boolean_expression3/5

b_not_test_boolean_expression/4

b_not_test_boolean_expression/6

b_not_test_boolean_expression2/7

b_not_test_boolean_expression2(truth,_,_,_,_WF,_Ai,_Ao) :- !,fail.

b_not_test_boolean_expression2(falsity,_,_,_,_WF,Ai,Ao) :- !,Ai=Ao. % NOT COVERED (2)

b_not_test_boolean_expression2(negation(BExpr),_,LocalState,State,WF,Ai,Ao) :- !,
    b_test_boolean_expression(BExpr,LocalState,State,WF,Ai,Ao).

b_not_test_boolean_expression2(conjunct(LHS,RHS),Infos,LocalState,State,WF,Ai,Ao) :- !,
    b(conjunct(LHS,RHS),pred,Infos) = Conj,
    copy_wf_start(WF,not_conjunct,CWF),
    if(b_check_boolean_expression(Conj,LocalState,State,CWF,PredRes,Ai,Ao),
    (PredRes=pred_false,
    copy_wf_finish(WF,CWF)
    ),
    if(b_check_boolean_expression(LHS,LocalState,State,CWF,LHSPredRes,Ai,Ao), % some redundant work with call above: TODO: avoid !
    (copy_wf_finish(WF,CWF),
    get_last_wait_flag(not_conjunct_rhs,WF,WF2), % before starting to enumerate infinite types: better try both possibilities:
    b_not_test_conjunction_rhs(LHSPredRes,RHS,LocalState,State,WF,Ai,WF2)
    ),
    (Ai=Ao,
    get_priority_of_boolean_expression2(disjunct(LHS,RHS),StartPrio),
    %get_wait_flag(Prio,not_conjunct,WF,WF2),
    get_binary_choice_wait_flag_exp_backoff(StartPrio,not_conjunct,WF,WF2),
    % TO DO: we could check if LHS or RHS are registered in Ai as pred_true/pred_false ??
    b_not_test_conjunction(LHS,RHS,LocalState,State,WF,WF2,Ai))
)
).

b_not_test_boolean_expression2(implication(LHS,RHS),_,LocalState,State,WF,Ai,Ao) :- !,
    b_test_boolean_expression(LHS,LocalState,State,WF,Ai,Aii),
    b_not_test_boolean_expression(RHS,LocalState,State,WF,Aii,Ao).

b_not_test_boolean_expression2(equivalence(LHS,RHS),_,LocalState,State,WF,Ai,Ao) :- !,
    b_not_test_equivalence(LHS,RHS,LocalState,State,WF,Ai,Ao).

b_not_test_boolean_expression2(disjunct(LHS,RHS),_,LocalState,State,WF,Ai,Ao) :- !,
    b_not_test_boolean_expression(LHS,LocalState,State,WF,Ai,Aii),
    b_not_test_boolean_expression(RHS,LocalState,State,WF,Aii,Ao).

b_not_test_boolean_expression2(lazy_let_pred(Id,AssignmentExpr,Expr),_I,LocalState,State,WF,Ai,Ao) :- !,
    add_lazy_let_id_and_expression(Id,AssignmentExpr,LocalState,State,NewLocalState,WF,Ai),
    b_not_test_boolean_expression(Expr,NewLocalState,State,WF,Ai,Ao). % we could use Ai,Ao version as lazy lets never interfere with each other and never invalidate existing expressions

b_not_test_boolean_expression2(lazy_lookup_pred(Id),_Info,LocalState,_State,WF,Ai,Ao) :- !, Ai=Ao,
    lookup_value_for_existing_id_wf(Id,LocalState,(Trigger,Value),WF), % should normally only occur in LocalState; value introduced by lazy_let
    (Trigger,Value) = (pred_true,pred_false). % force evaluation

b_not_test_boolean_expression2(value(PredVal),_Info,_LocalState,_State,_WF,Ai,Ao) :- !, % this can occur when lazy_lookup_pred gets compiled by b_compiler
    is_pred_false(PredVal),Ai=Ao.

b_not_test_boolean_expression2(Expr,Info,LocalState,State,WF,Ai,Ao) :-
    % TO DO: we could put some of the operators into the Ai store (comparison operators)
    b_not_test_atomic_boolean_expression2(Expr,Info,LocalState,State,WF,Ai,Ao).

b_not_test_boolean_expression_cs/5

b_not_test_conjunction/7

Block: b_not_test_conjunction(?,?,?,?,?,-,?)

b_not_test_conjunction_rhs/7

Block: b_not_test_conjunction_rhs(-,?,?,?,?,?,-)

b_not_test_equivalence/7

b_not_test_exists/7

Description:
print(b_not_test_exists(ParaIDs)),nl, print(state(LocalState,State)),nl, %%

b_not_test_exists_aux/5

Block: b_not_test_exists_aux(-,?,?,?,?)

b_not_test_exists_aux2/5

Block: b_not_test_exists_aux2(-,?,?,?,?)

b_not_test_inner_boolean_expression/4

b_not_test_list_of_boolean_expression/4

b_optimized_b_test_instance/4

b_partial_set_up_concrete_constants/1

b_partial_set_up_concrete_constants2/2

b_partial_set_up_concrete_constants2(NormalisedConstantsState,Status) :-
    b_get_machine_constants(Constants),
    Constants \= [],
    (det_solution_for_constant_was_stored(Cst1) -> true), % we have found a solution for at least one constant
    %set_up_typed_localstate(Constants,[],ConstantsState), -> can create call_residue due to typing fd/2 values
    findall(bind(ID,_),(member(TID,Constants),def_get_texpr_id(TID,ID)),ConstantsState),
    formatsilent('SETUP_CONSTANTS not successful, but solutions were found for some constants (e.g., ~w):~n',[Cst1]),
    (fill_in_det_solutions(ConstantsState,FC)
    -> All=all, TMSG = [')']
    ; All=some, TMSG = [', e.g., ',Cst1,')']
    ),
    (preference(allow_incomplete_partial_setup_constants,true)
    -> true
    ; % fill_in_det_solutions will fail if not all constants valued and
    % if allow_incomplete_partial_setup_constants is false
    get_specification_description(properties,PS),
    % TO DO: determine if time-out occurred or not
    (Status=false
    -> ajoin([PS,' are unsatisfiable (but ',All,' CONSTANTS valued'|TMSG],Msg),
    add_error(setup_constants_inconsistent,Msg)
    ; unsat_properties_abort_error(_)
    -> ajoin([PS,' are unknown due to well-definedness error(s) (but ',All,' CONSTANTS valued'|TMSG],Msg),
    add_error(setup_constants_unknown,Msg)
    ; unsat_component_enumeration_warning(_)
    -> ajoin([PS,' are unknown due to enumeration warning(s) (but ',All,' CONSTANTS valued'|TMSG],Msg),
    add_error(setup_constants_unknown,Msg)
    ; all_unsat_components_marked_prob_ignore
    -> ajoin([PS,' are unknown due to prob-ignore pragmas (but ',All,' CONSTANTS valued'|TMSG],Msg),
    add_message(setup_constants_unknown,Msg)
    ;
    ajoin([PS,' are unknown (but ',All,' CONSTANTS valued'|TMSG],Msg),
    add_error(setup_constants_unknown,Msg)
    ),
    All=all % only continue if all constants valued
    ),
    normalise_store(FC,NormalisedConstantsState).

b_set_up_concrete_constants/2

b_state_violates_invariant/2

b_state_violates_invariant_aux/2

b_state_violates_spec_invariant/3

b_sum_or_mul_over_list/9

b_sum_or_mul_over_list_acc/11

Block: b_sum_or_mul_over_list_acc(-,?,?,?,?,?,?,?,?,?,?)

b_sum_or_mul_over_list_acc2/12

Block: b_sum_or_mul_over_list_acc2(?,-,?,?,?,?,?,?,?,?,?,?) b_sum_or_mul_over_list_acc2(?,?,?,?,?,?,?,-,?,?,?,-) b_sum_or_mul_over_list_acc2(-,?,?,?,?,?,?,?,?,?,?,-)

b_sum_or_mul_over_list_clp/9

Block: b_sum_or_mul_over_list_clp(-,?,?,?,?,?,?,?,?)

b_test_atomic_boolean_expression2/5

b_test_atomic_boolean_expression2(partition(LHS,RHS),_,LocalState,State,WF) :- !,
    b_compute_expression(LHS,LocalState,State,SV1,WF), %print(lhs(SV1)),nl,
    l_compute_expression(RHS,LocalState,State,SV2,WF), % RHS is Prolog list of expressions
    kernel_call_predicate(partition_wf(SV1,SV2,WF),kernel_objects,WF,partition(LHS,RHS)).

b_test_atomic_boolean_expression2(member(TElem,TSet),_,LocalState,State,WF) :- !,
    b_test_member_expression(TElem,TSet,LocalState,State,WF).

b_test_atomic_boolean_expression2(not_member(TElem,TSet),Info,LocalState,State,WF) :- !,
    get_texpr_expr(TSet,Set),
    b_test_notmember_expression(Set,TElem,TSet,Info,LocalState,State,WF).

b_test_atomic_boolean_expression2(freetype_case(Freetype,Case,Expr),_,LocalState,State,WF) :-
    !,equal_object_wf(Value,freeval(Freetype,Case,_),b_test_atomic_boolean_expression2,WF),
    b_compute_expression(Expr,LocalState,State,Value,WF). % NOT COVERED (16)

b_test_atomic_boolean_expression2(finite(SetExpr),_,LocalState,State,WF) :-
    !, b_compute_expression(SetExpr,LocalState,State,Value,WF),
    kernel_call_predicate(is_finite_set_wf(Value,WF),kernel_objects,WF,finite(SetExpr)).

b_test_atomic_boolean_expression2(kodkod(ProblemId,_),_,LocalState,State,WF) :-
    !,get_wait_flag1(kodkod_call,WF,WF0),
    kodkod_request(ProblemId,pos,LocalState,State,WF0). % NOT COVERED (17)

b_test_atomic_boolean_expression2(equal(Arg1,Arg2),Info,LocalState,State,WF) :- !,
    b_test_atomic_equal_boolean_expression(Arg1,Arg2,Info,LocalState,State,WF).

b_test_atomic_boolean_expression2(not_equal(Arg1,Arg2),Info,LocalState,State,WF) :- !,
    b_test_atomic_not_equal_boolean_expression(Arg1,Arg2,Info,LocalState,State,WF).

b_test_atomic_boolean_expression2(less_equal(Arg1,Arg2),_Info,LocalState,State,WF) :-
    %get_texpr_type(Arg1,integer), % type checker already checks this
    preferences:preference(use_clpfd_solver,true),
    %\+ member(no_clpfd_arith_integer_expression,Info),
    !,
    b_compute_arith_expression(Arg1,LocalState,State,CLPFD_Expr1,WF),
    b_compute_arith_expression(Arg2,LocalState,State,CLPFD_Expr2,WF),
    clpfd_interface:clpfd_leq_expr(CLPFD_Expr1,CLPFD_Expr2).

b_test_atomic_boolean_expression2(greater_equal(Arg1,Arg2),_Info,LocalState,State,WF) :-
    %get_texpr_type(Arg1,integer), % type checker already checks this
    preferences:preference(use_clpfd_solver,true),
    %\+ member(no_clpfd_arith_integer_expression,Info),
    !,
    b_compute_arith_expression(Arg1,LocalState,State,CLPFD_Expr1,WF),
    b_compute_arith_expression(Arg2,LocalState,State,CLPFD_Expr2,WF),
    clpfd_interface:clpfd_leq_expr(CLPFD_Expr2,CLPFD_Expr1).

b_test_atomic_boolean_expression2(less(Arg1,Arg2),_Info,LocalState,State,WF) :-
    %get_texpr_type(Arg1,integer), % type checker already checks this
    preferences:preference(use_clpfd_solver,true),
    % \+ member(no_clpfd_arith_integer_expression,Info),
    !,
    b_compute_arith_expression(Arg1,LocalState,State,CLPFD_Expr1,WF),
    b_compute_arith_expression(Arg2,LocalState,State,CLPFD_Expr2,WF),
    clpfd_interface:clpfd_lt_expr(CLPFD_Expr1,CLPFD_Expr2).

b_test_atomic_boolean_expression2(greater(Arg1,Arg2),_Info,LocalState,State,WF) :-
    %get_texpr_type(Arg1,integer), % type checker already checks this
    preferences:preference(use_clpfd_solver,true),
    %\+ member(no_clpfd_arith_integer_expression,Info),
    !,
    b_compute_arith_expression(Arg1,LocalState,State,CLPFD_Expr1,WF),
    b_compute_arith_expression(Arg2,LocalState,State,CLPFD_Expr2,WF),
    clpfd_interface:clpfd_lt_expr(CLPFD_Expr2,CLPFD_Expr1).

b_test_atomic_boolean_expression2(external_pred_call(FunName,Args),Info,LocalState,State,WF) :-
    !,
    (do_not_evaluate_args(FunName) -> EvaluatedArgs=[]
    ; b_compute_expressions(Args, LocalState,State, EvaluatedArgs, WF)),
    push_wait_flag_call_stack_info(WF,external_call(FunName,EvaluatedArgs,Info),WF2),
    call_external_predicate(FunName,Args,EvaluatedArgs,LocalState,State,pred_true,Info,WF2).

b_test_atomic_boolean_expression2(Expression,Info,LocalState,State,WF) :-
    preferences:preference(use_clpfd_solver,false),
    special_binary_predicate(Expression,Module:Kernel_predicate,Arg1,T1,Arg2,T2),
    (nonmember(contains_wd_condition,Info) -> true ; preference(disprover_mode,true)),
    !,
    % print('Special call: '), print_bexpr(Expression),nl, print(Kernel_predicate),print(' : '),nl,
    %(Arg1==list_of_expressions -> b_compute_expressions ... % no longer needed
    b_compute_expression(Arg1,LocalState,State,SV1,WF),
    b_compute_expression(Arg2,LocalState,State,SV2,WF),
    KernelCall =.. [Kernel_predicate,SV1,T1,SV2,T2,WF],
    kernel_call_predicate(KernelCall,Module,WF,Expression).

b_test_atomic_boolean_expression2(Expression,_,LocalState,State,WF) :-
    functor(Expression,BOP,2),
    kernel_mappings:binary_boolean_operator(BOP,Module:Kernel_predicate,WFEnabled),!,
    arg(1,Expression,Arg1), arg(2,Expression,Arg2),
    b_compute_expression(Arg1,LocalState,State,SV1,WF),
    (binary_boolean_operator_trivially_true(BOP,SV1)
    -> check_well_defined(Arg2,LocalState,State,WF)
    ; b_compute_expression(Arg2,LocalState,State,SV2,WF),
    ( WFEnabled==yes ->
    KernelCall =.. [Kernel_predicate,SV1,SV2,WF2],
    (do_not_enumerate_binary_boolean_operator(BOP,Arg1,Arg2) % we assume: this is only true for WFEnabled predicates
    -> add_wait_flag_info(WF,wfx_no_enumeration,WF2)
    ; WF2=WF)
    ; KernelCall =.. [Kernel_predicate,SV1,SV2], WF2=WF % note: WF2 still used in kernel_call_predicate
    ),
    kernel_call_predicate(KernelCall,Module,WF2,Expression)).

b_test_atomic_boolean_expression2(E,Info,_LS,_S,_WF) :-
    add_internal_error('Uncovered boolean expression: ',b(E,pred,Info)),
    print_functor(E),nl,
    fail.

b_test_atomic_equal_boolean_expression/6

b_test_atomic_equal_boolean_expression(Arg1,Arg2,_Info,LocalState,State,WF) :-
    Arg1 = b(_,integer,_), %get_texpr_type(Arg1,integer),
    preferences:preference(use_clpfd_solver,true),!,
    (Arg2 = b(_,integer,_) -> true ; add_internal_error('Type error in AST, not wrapped integer: ',Arg2)),
    b_test_arith_equal_boolean_expression(Arg1,Arg2,LocalState,State,WF).

b_test_atomic_equal_boolean_expression(Arg1,Arg2,Info,LocalState,State,WF) :-
    member(prob_annotation('LAMBDA-EQUALITY'),Info),
    \+ simple_expression(Arg2),
    is_lambda_result_id(Arg1), %get_texpr_id(Arg1,'_lambda_result_'), % ensure we have not renamed it to was_lambda_result ?
    !, % this is an equality for the result of a lambda abstraction; only evaluate at the end
    b_compute_expression(Arg1,LocalState,State,SV1,WF), % this is the lambda result identifier _lambda_result_
    %get_enumeration_finished_wait_flag(WF,EWF),
    %get_wait_flag(10000,lambda_result,WF,EWF),
    % compute deterministic parts of Arg2 in wf0 phase: avoid computing this stuff over again
    %print('DELAY: '), translate:print_bexpr(Arg2),nl,
    kernel_waitflags:copy_wf01e_wait_flags(WF,WF2), b_compute_expression(Arg2,LocalState,State,SV2,WF2),
    get_last_wait_flag(lambda_result,WF,EWF),
    ground_value_check(SV2,G2),
    when((nonvar(G2);nonvar(SV1);nonvar(EWF)),b_lambda_result_equal_boolean_expression(SV1,SV2,WF,EWF,WF2)).

b_test_atomic_equal_boolean_expression(Arg1,Arg2,Info,LocalState,State,WF) :-
    (LocalState = []
    -> true % only check if we are at the outer level
    % (not inside a quantifier,...) or if we have CSE introduzed lazy_lets:
    ; preferences:preference(use_common_subexpression_elimination,true)
    % TO DO: check that we have only added @nr to local state from lazy_let; ADD INFO FIELD
    ),
    get_texpr_type(Arg1,Type1), is_set_type(Type1,SetType1),
    % previously we required SetType1 = couple(_,_)
    get_texpr_id(Arg1,ID),
    % we could check: \+ get_texpr_id(Arg2,_), % as we do not need to treat simple equations like ID = ID2; unless for memo?
    (abstract_constant(ID,_) % check if ABSTRACT_CONSTANT
    -> Kind=abstract,
    kernel_objects:max_cardinality(Type1,MaxCard1),
    (number(MaxCard1) % check that type is large enough to warrant recursive or symbolic treatment
    -> (MaxCard1>100 -> true ; constant_variable_marked_as_memo(ID))
    ; true)
    ; %fail,
    concrete_constant(ID,_)
    -> Kind=concrete,
    (constant_variable_marked_as_expand(ID)
    -> true % note: we also check for expand annotation in store (expand_closure_value),
    % but it is useful to expand ID already here to ease checking PROPERTIES
    ; constant_variable_marked_as_memo(ID))
    %; b_is_unused_constant(ID) -> ABSTRACT=true % TO DO: check if ID not used somewhere else in Properties ??!!
    ),
    % in future: we may do size change analysis, or something like that to check that we have properly defined
    % recursive function
    debug_format(19,'Equation defining ~w constant: ~w~n',[Kind,ID]),
    !,
    (constant_variable_marked_as_expand(ID) -> SymArg2 = Arg2 ; mark_bexpr_as_symbolic(Arg2,SymArg2)),
    b_add_constant_definition(Kind,ID,Info,Arg1,SetType1,SymArg2,LocalState,State,WF).

b_test_atomic_equal_boolean_expression(Arg1,Arg2,_Info,LocalState,State,WF) :-
    b_compute_expression(Arg1,LocalState,State,SV1,WF),
    b_compute_expression(Arg2,LocalState,State,SV2,WF),
    kernel_call_predicate_equal_object_optimized(SV1,SV2,WF).

b_test_atomic_not_equal_boolean_expression/6

b_test_atomic_not_equal_boolean_expression(Arg1,Arg2,_Info,LocalState,State,WF) :-
    get_texpr_type(Arg1,boolean),!, % special treatment : not_equal_object has no type information
    b_compute_expression(Arg1,LocalState,State,B1,WF),
    b_compute_expression(Arg2,LocalState,State,B2,WF),
    negate(B1,B2). % from bool_pred

b_test_atomic_not_equal_boolean_expression(Arg1,Arg2,_Info,LocalState,State,WF) :-
    get_texpr_type(Arg1,integer),
    preferences:preference(use_clpfd_solver,true),
    %\+ member(no_clpfd_arith_integer_expression,Info),
    !,
    % Note: calling b_compute_arith_expression will also instantiate a variable to at least the int(_) skeleton; thereby enabling propagation
    % this is potentially better than calling the default versions of the predicates, which may wait until the int(_) skeleton is set up before propagation
    b_compute_arith_expression(Arg1,LocalState,State,CLPFD_Expr1,WF),
    b_compute_arith_expression(Arg2,LocalState,State,CLPFD_Expr2,WF),
    clpfd_interface:clpfd_neq_expr(CLPFD_Expr1,CLPFD_Expr2).

b_test_atomic_not_equal_boolean_expression(Arg1,Arg2,_Info,LocalState,State,WF) :-
    b_compute_expression(Arg1,LocalState,State,SV1,WF),
    (nonvar(SV1), SV1=closure(_,_,_), % first argument is symbolic
    Arg2 = b(comprehension_set(PP,CC),_,InfoCS) % second arg is a comprehension set;
    % TODO: deal with other constructs which merit symbolic treatment; union of comprehension sets, ...
    % (see line 147 in AMASS_mchs/oriented_abscissa.mch)
    -> % print(symbolic_neq(PP)),nl,
    b_compute_comprehension_set_symbolic(PP,CC,InfoCS,LocalState,State,SV2,WF)
    % Note: this case occurs for symbolic abstract constants f when using DOUBLE_EVALUATION
    % in the evaluation view which are defined by f = %x... when checking f /= %x....
    ; b_compute_expression(Arg2,LocalState,State,SV2,WF)
    ),
    kernel_call_predicate_not_equal_object(SV1,SV2,WF,not_equal(Arg1,Arg2)).

b_test_boolean_expression/4

b_test_boolean_expression/6

b_test_boolean_expression2/7

Description:
print('REUSED: '), translate:print_bexpr(Pred),nl

b_test_boolean_expression2(truth,_,_,_,_WF,Ai,Ao) :- !,Ai=Ao.

b_test_boolean_expression2(falsity,_,_,_,_WF,_Ai,_Ao) :- !,fail.

b_test_boolean_expression2(negation(BExpr),_,LocalState,State,WF,Ai,Ao) :- !,
    b_not_test_boolean_expression(BExpr,LocalState,State,WF,Ai,Ao).

b_test_boolean_expression2(conjunct(LHS,RHS),_,LocalState,State,WF,Ai,Ao) :- !,
    b_test_boolean_expression(LHS,LocalState,State,WF,Ai,Aii),
    b_test_boolean_expression(RHS,LocalState,State,WF,Aii,Ao).

b_test_boolean_expression2(implication(LHS,RHS),Info,LocalState,State,WF,Ai,Ao) :-
    %b_compiler:b_compile(LHS,[],LocalState,State,CLHS), % this slows down Cruise benchmark from 3.75 s to 4.3
    !,
    b_test_implication(LHS,RHS,Info,LocalState,State,WF,Ai,Ao).

b_test_boolean_expression2(equivalence(LHS,RHS),_,LocalState,State,WF,Ai,Ao) :- !,
    b_test_equivalence(LHS,RHS,LocalState,State,WF,Ai,Ao).

b_test_boolean_expression2(disjunct(LHS,RHS),Info,LocalState,State,WF,Ai,Ao) :- !,
    % TO DO: normalise disjunct first ?
    copy_wf_start(WF,disjunct,CWF),
    if(b_check_boolean_expression(LHS,LocalState,State,CWF,PredRes,Ai,Aii),
    % we can check lhs
    if(b_interpreter_check:b_check_boolean_expression0(pred_false,PredRes,RHS,LocalState,State,CWF,RR,Aii,Ao),
    ( /* we can also check rhs */
    b_interpreter_check:disjoin(PredRes,RR,pred_true,LHS,RHS,WF),
    copy_wf_finish(WF,CWF)
    ),
    (
    Ao=Aii,
    copy_wf_finish(WF,CWF),
    imply_test_boolean_expression(PredRes,pred_false,RHS,LocalState,State,WF,Aii),
    perfmessagecall(choice_point,reification_of_disjunction_rhs_failed,translate:print_bexpr(RHS),Info),
    enumerate_bool(PredRes,15,WF)
    )
    ),
    % we cannot check lhs
    if((always_well_defined(RHS),
    b_check_boolean_expression(RHS,LocalState,State,CWF,PredRes,Ai,Aii)),
    (
    Ao=Aii,
    copy_wf_finish(WF,CWF),
    imply_test_boolean_expression(PredRes,pred_false,LHS,LocalState,State,WF,Aii),
    perfmessagecall(choice_point,reification_of_disjunction_lhs_failed,translate:print_bexpr(LHS),Info),
    enumerate_bool(PredRes,15,WF)
    ),
    % we cannot check neither lhs nor rhs:
    (Ai=Ao,
    get_priority_of_boolean_expression2(disjunct(LHS,RHS),StartPrio),
    %get_wait_flag(Prio,disjunct,WF,WF2),
    get_binary_choice_wait_flag_exp_backoff(StartPrio,disjunct,WF,WF2),
    % be sure that e.g. for (x=2 or x=3) both branches will be tested once deterministic propagation is over
    %print(prio(Prio)), print(' : '),print_bexpr(LHS), print(' or '), print_bexpr(RHS),nl,
    perfmessagecall(choice_point,reification_of_disjunction_failed,translate:print_bexpr(b(disjunct(LHS,RHS),pred,Info)),Info),
    b_test_disjunction(LHS,RHS,LocalState,State,WF,WF2,Ai)
)
)
).

b_test_boolean_expression2(exists(Parameters,RHS),Infos,LocalState,State,WF,Ai,Ao) :- !,Ai=Ao,
    b_test_exists(Parameters,RHS,Infos,LocalState,State,WF).

b_test_boolean_expression2(forall(Parameters,LHS,RHS),Infos,LocalState,State,WF,Ai,Ao) :- !,Ai=Ao,
    /* !ID.(LHS => RHS) */
    % print_message(forall(Parameters,LHS,RHS)),
    % get_wait_flag0(WF,WF0), when(nonvar(WF0),
    b_for_all(Parameters,Infos,LHS,RHS,LocalState,State,WF). %).

b_test_boolean_expression2(let_predicate(Ids,AssignmentExprs,Pred),Infos,LocalState,State,WF,Ai,Ao) :- !,
    Ai=Ao, % any expression inside the LET cannot be safely reused
    (is_truth(Pred)
    -> % useless let, only sense of computations below is in detecting WD errors
    get_enumeration_starting_wait_flag(useless_let_predicate(Ids),WF,ESWF),
    when(nonvar(ESWF),set_up_localstate_for_let(Ids,_,AssignmentExprs,LocalState,State,_LetState,WF))
    ; set_up_localstate_for_let(Ids,ParaValues,AssignmentExprs,LocalState,State,LetState,WF),
    opt_push_wait_flag_call_stack_quantifier_info(WF,let_quantifier,Ids,ParaValues,Infos,WF2),
    b_test_boolean_expression(Pred,LetState,State,WF2)). % we could pass Ai in if Ids fresh

b_test_boolean_expression2(lazy_let_pred(Id,AssignmentExpr,Expr),_I,LocalState,State,WF,Ai,Ao) :- !,
    add_lazy_let_id_and_expression(Id,AssignmentExpr,LocalState,State,NewLocalState,WF,Ai),
    b_test_boolean_expression(Expr,NewLocalState,State,WF,Ai,Ao). % we could use Ai,Ao version as lazy lets never interfere with each other and never invalidate existing expressions

b_test_boolean_expression2(lazy_lookup_pred(Id),_Info,LocalState,_State,WF,Ai,Ao) :- !, Ai=Ao,
    lookup_value_for_existing_id_wf(Id,LocalState,(Trigger,Value),WF), % should normally only occur in LocalState; value introduced by lazy_let
    (Trigger,Value) = (pred_true,pred_true). % force evaluation

b_test_boolean_expression2(value(PredVal),_Info,_LocalState,_State,_WF,Ai,Ao) :- !, % this can occur when lazy_lookup_pred gets compiled by b_compiler
    is_pred_true(PredVal),Ai=Ao.

b_test_boolean_expression2(Pred,Info,LocalState,State,WF,Ai,Ao) :-
    % TO DO: we could put some of the operators into the Ai store (comparison operators)
    b_interpreter_check:register_predicate(Pred,Info,pred_true,Reused,Ai,Ao),
    (Reused==true
    -> %% print('REUSED: '), translate:print_bexpr(Pred),nl
    true
    ; b_test_atomic_boolean_expression2(Pred,Info,LocalState,State,WF)).

b_test_boolean_expression_cs/5

b_test_boolean_expression_for_ground_state/4

b_test_boolean_expression_for_ground_state/5

b_test_boolean_expression_for_ground_state1/5

b_test_boolean_expression_for_ground_state2/6

b_test_disjunction/7

Block: b_test_disjunction(?,?,?,?,?,-,?)

b_test_equivalence/7

b_test_exists/6

b_test_exists/7

Block: b_test_exists(-,?,?,?,?,?,?)

b_test_exists_wo_expansion/6

Description:
TO DO: get flag when enumeration of infinite type starts; maybe if domain of exists is small we can start enumerating earlier ?? <-> relation with lifting exists in closure expansion heuristic

b_test_exists_wo_expansion(Parameters,Condition,Infos,LocalState,State,WF) :-
    %print(test_exists(Parameters,Infos)),nl,portray_waitflags(WF),nl,
    (preference(lift_existential_quantifiers,true) ; member(allow_to_lift_exists,Infos)),
    !, % we enumerate the exists normally; treat it just like an ordinary predicate
    % lifting may generate multiple solutions; but avoids delaying enumeration of quantified parameters
    % print('*Lifting existential quantifier: '), translate:print_bexpr(Condition),nl,
    set_up_typed_localstate(Parameters,ParaValues,TypedVals,LocalState,NewLocalState,positive),
    copy_wf_start(WF,b_test_exists_wo_expansion,CWF),
    opt_push_wait_flag_call_stack_quantifier_info(CWF,exists,Parameters,ParaValues,Infos,CWF2),
    b_test_boolean_expression(Condition,NewLocalState,State,CWF2),
    % often we do not need to enumerate TypedVals; they can be derived, but we could have #y.(y>x) and need to enum y
    b_tighter_enumerate_values_in_ctxt(TypedVals,Condition,CWF2),
    copy_wf_finish(WF,CWF2). % moving this before tighter_enum may mean that we have more precise ranges; but this can be counter-productive (e.g., for test 1162 unless we strengthen the useless enum analysis)

b_test_exists_wo_expansion(Parameters,Condition,Infos,LocalState,State,WF) :-
    get_exists_used_ids(Parameters,Condition,Infos,Used),
    % IT IS IMPORTANT THAT THE USED INFO IS CORRECT ; otherwise the WaitVars will be incorrect
    % The used_ids info does not include the Parameters of the existential quantifier !
    set_up_typed_localstate(Parameters,ParaValues,TypedVals,LocalState,NewLocalState,positive),
    lookup_values_if_vars(Used,LocalState,State,WaitVarsState), % TO DO: we could use b_compiler instead
    % What if the Condition was compiled and now contains a previously used_variable inside a closure/value ?
    %term_variables((Condition,WaitVarsState),WaitVars), % this can be expensive when we have large data values (see rule_RVF219/rule_RVF219_compo.mch)
    bexpr_variables(Condition,CondVars),
    value_variables(WaitVarsState,CondVars,WaitVars),
    % now determine which WaitVars are really worth waiting for, e.g., do not wait for res in #x.(x:E & ... res=min(f(x)))
    % relevant tests: 1868, 1194, 383, 1642, 1708, 1003, 1080, 1081, 1943
    (remove_ids_defined_by_equality(WaitVars,LocalState,State,Infos,RealWaitVars) -> RemovedVars=true
    ; RealWaitVars = WaitVars, RemovedVars=false),
    opt_push_wait_flag_call_stack_quantifier_info(WF,exists,Parameters,ParaValues,Infos,WF2),
    create_inner_wait_flags(WF2,expansion_context(b_test_exists,Parameters),LocalWF), % we are creating inner waitflags here as the exist will wait anyway; LocalWF shares just WFE flag with WF
    b_test_boolean_expression(Condition,NewLocalState,State,LocalWF), /* check Condition */
    ground_det_wait_flag(LocalWF), % print('det no contradiction'),nl,flush_output,
    b_tighter_enumerate_values_in_ctxt(TypedVals,Condition,LocalWF), % will not yet enumerate
    (% we could treat allow_to_lift_exists also here by setting ESWF=1; but 1162 then fails
    get_preference(data_validation_mode,true),
    not_generated_exists_paras(Parameters) % generated exists, e.g., for relational composition can lead to virtual timeouts, cf Thales_All/rule_zcpa2.mch in test 2287
    -> get_wait_flag(50000,b_test_exists(Parameters),WF,ESWF) % 100000 sufficient for test 1945; 869 for rule_CHAMPS in private_examples/ClearSy/2023
    ; get_enumeration_starting_wait_flag(b_test_exists(Parameters),WF,ESWF)), %% TO DO: get flag when enumeration of infinite type starts; maybe if domain of exists is small we can start enumerating earlier ?? <-> relation with lifting exists in closure expansion heuristic
    when((nonvar(ESWF);ground(RealWaitVars)),b_enumerate_exists(ESWF,RemovedVars,WaitVars,Parameters,LocalWF,WF)).

b_test_implication/8

Description:
print('checking => '), print_bexpr(LHS), print(' '), print(PredRes),nl,
The following improves constraint propagation; but can be tricky with undefinedness

b_test_inner_boolean_expression/4

b_test_list_of_boolean_expression_aux/5

b_test_list_of_boolean_expression_for_ground_state/4

b_test_member_expression/5

b_test_member_expression2/7

b_test_member_expression2(comprehension_set(Par,Cond),_Type,_Info,El,LocalState,State,WF) :-
    % used to call in next clause below: b_generate_closure_if_necessary(Par,Cond,LocalState,State,SetValue,WF) /* will not expand closure */
    /* optimized case for dealing with comprehension_set ; however, does not seem to buy anything over older version with b_generate_closure_if_necessary in test 1079 */
    /* new version buys about 6 % for {x| x:1..400000 & x:{n|n >= 9000 & n<= 600000 & n mod 100 = 0}} (Sep 3 2014) */
    set_up_typed_localstate(Par,ValueList,_TypedVals,LocalState,NewLocalState,positive),
    !,
    convert_list_into_pairs(ValueList,ElementVal),
    b_compute_expression(El,LocalState,State,ElementVal,WF),
    b_test_boolean_expression(Cond,NewLocalState,State,WF).

b_test_member_expression2(SymbolicSetConstant,_Type,_Info,El,LocalState,State,WF) :-
    %hit_profiler:add_profile_hit(SymbolicSetConstant),
    cst_in_boolean_type(SymbolicSetConstant,Module:Kernel_predicate),!, % two cases : string_set and integer_set
    b_compute_expression(El,LocalState,State,ElValue,WF),
    functor(KernelCall,Kernel_predicate,2),
    arg(1,KernelCall,ElValue),
    arg(2,KernelCall,WF),
    % print_message(cst_in_boolean_type_call(KernelCall)),
    kernel_call_predicate(KernelCall,Module,WF,SymbolicSetConstant). % should be member(... SymbolicSetConstant)

b_test_member_expression2(Expression,_Type,Info,El,LocalState,State,WF) :-
    functor(Expression,BOP,2),
    binary_in_boolean_type(BOP,Module:Kernel_predicate),!,
    b_compute_expression(El,LocalState,State,ElValue,WF),
    arg(1,Expression,Arg1),arg(2,Expression,Arg2),
    (binary_in_definitely_true(BOP,ElValue)
    -> % no need to compute arguments; unless required for WD:
    check_well_defined(Arg1,LocalState,State,WF),
    check_well_defined(Arg2,LocalState,State,WF)
    ; b_compute_expression(Arg1,LocalState,State,SV1,WF),
    b_compute_expression(Arg2,LocalState,State,SV2,WF),
    opt_push_wait_flag_call_stack_info(WF,b_operator_call(member,[ElValue,b_operator(BOP,[SV1,SV2])],Info),WF2),
    binary_in_kernel_call(Module,Kernel_predicate,ElValue,SV1,SV2,WF2,Expression)
).

b_test_member_expression2(Expression,_Type,Info,El,LocalState,State,WF) :-
    functor(Expression,UnOP,1),
    unary_in_boolean_type(UnOP,Module:Kernel_predicate),!,
    b_compute_expression(El,LocalState,State,ElValue,WF),
    arg(1,Expression,Arg1),
    (unary_in_definitely_true(UnOP,ElValue)
    -> % no need to compute arguments; unless required for WD:
    check_well_defined(Arg1,LocalState,State,WF)
    ; b_compute_expression(Arg1,LocalState,State,SV1,WF),
    opt_push_wait_flag_call_stack_info(WF,b_operator_call(member,[ElValue,b_operator(UnOP,[SV1])],Info),WF2),
    unary_in_kernel_call(Module,Kernel_predicate,ElValue,SV1,WF2,Expression)
).

b_test_member_expression2(SetExpression,Type,Info,El,LocalState,State,WF) :-
    b_compute_expression2(SetExpression,Type,Info,LocalState,State,SetValue,WF),
    (always_well_defined_or_disprover_mode(El)
    -> SetValue \== [] % if we have the empty set: check_element will always fail
    ; true % we could check SetValue \== [] if find_abort_values=false ??
    ),
    b_compute_expression(El,LocalState,State,Element,WF),
    Span = El, % Info is quite often the empty list
    (not_invertible(El) % then no sense in setting up member constraint f(...) : SetValue ;
    % we cannot used the info anyway; but we could enumerate
    -> % we wait until Element is fully known before doing the check
    ground_value_check(Element,GrEl),
    when(nonvar(GrEl),kernel_call_predicate_check_element_of_wf(Element,SetValue,WF,Span))
    ; kernel_call_predicate_check_element_of_wf(Element,SetValue,WF,Span)).

b_test_notmember_expression/7

b_test_notmember_expression(set_extension(Ex),El,_Set,_,LocalState,State,WF) :- !,
    b_compute_expressions(Ex,LocalState,State,ExValueList,WF),
    b_compute_expression(El,LocalState,State,ElementVal,WF),
    not_element_of_list_wf(ElementVal,ExValueList,WF).

b_test_notmember_expression(SymbolicSetCst,El,_Set,_,LocalState,State,WF) :-
    kernel_mappings:cst_not_in_boolean_type(SymbolicSetCst,Module:Kernel_predicate),!,
    b_compute_expression(El,LocalState,State,ElValue,WF),
    functor(KernelCall,Kernel_predicate,1),
    arg(1,KernelCall,ElValue),
    % debug_print(cst_not_in_boolean_type(9,KernelCall)),
    kernel_call_predicate(KernelCall,Module,WF,SymbolicSetCst).

b_test_notmember_expression(Expression,El,_Set,Info,LocalState,State,WF) :-
    functor(Expression,BOP,2),
    kernel_mappings:binary_not_in_boolean_type(BOP,Module:Kernel_predicate),!,
    b_compute_expression(El,LocalState,State,ElValue,WF),
    \+ binary_in_definitely_true(BOP,ElValue),
    arg(1,Expression,Arg1),arg(2,Expression,Arg2),
    b_compute_expression(Arg1,LocalState,State,SV1,WF),
    b_compute_expression(Arg2,LocalState,State,SV2,WF),
    % KernelCall =.. [Kernel_predicate,ElValue,SV1,SV2,WF],
    opt_push_wait_flag_call_stack_info(WF,b_operator_call(not_member,[ElValue,b_operator(BOP,[SV1,SV2])],Info),WF2),
    kernel_call_predicate3(Kernel_predicate,ElValue,SV1,SV2,Module,WF2,Expression).

b_test_notmember_expression(Expression,El,_Set,Info,LocalState,State,WF) :-
    functor(Expression,UnOP,1),
    unary_not_in_boolean_type(UnOP,Module:Kernel_predicate),!,
    b_compute_expression(El,LocalState,State,ElValue,WF),
    \+ unary_in_definitely_true(UnOP,ElValue),
    arg(1,Expression,Arg1),
    b_compute_expression(Arg1,LocalState,State,SV1,WF),
    %KernelCall =.. [Kernel_predicate,ElValue,SV1,WF],
    %kernel_call_predicate(KernelCall,Module,WF,Expression).
    opt_push_wait_flag_call_stack_info(WF,b_operator_call(not_member,[ElValue,b_operator(UnOP,[SV1])],Info),WF2),
    kernel_call_predicate2(Kernel_predicate,ElValue,SV1,Module,WF2,Expression).

b_test_notmember_expression(Expr,Elem,Set,_Info,LocalState,State,WF) :-
    (Expr=comprehension_set(Par,Cond)
    -> b_generate_closure_if_necessary(Par,Cond,LocalState,State,SetValue,WF) /* will not expand closure */
    ; b_compute_expression(Set,LocalState,State,SetValue,WF)
    ),
    (SetValue == []
    -> /* nothing can be member of empty set */
    check_well_defined(Elem,LocalState,State,WF)
    % we could disable this check if find_abort_values=true
    ; b_compute_expression(Elem,LocalState,State,ElemValue,WF),
    %kernel_call_predicate2(not_element_of_wf,ElemValue,SetValue,kernel_objects,WF,Expr)
    %kernel_call_predicate(not_element_of_wf(ElemValue,SetValue,WF),kernel_objects,WF,Expr)
    kernel_call_predicate_not_element_of_wf(ElemValue,SetValue,WF)
).

b_trace_test_components_full/3

b_try_check_boolean_expression/5

b_try_check_boolean_expression_c/5

b_try_check_boolean_expression_c2/5

b_try_check_boolean_expression_lwf/7

b_try_check_boolean_expression_lwf_block/6

Block: b_try_check_boolean_expression_lwf_block(?,?,?,?,-,-)

b_try_check_boolean_expression_lwf_c/7

b_try_check_boolean_expression_no_enum_wf/5

Description:
obsv([]).
obsv([bind(Var,Val) | T] ) :- when(ground(Val), format("~w = ~w~n",[Var,Val])), obsv(T).

b_try_check_boolean_expression_wf/5

b_try_check_failed/7

binary_boolean_operator_trivially_true/2

binop_to_be_marked_as_symbolic/3

block_compute_comprehension_set_aux/6

Block: block_compute_comprehension_set_aux(?,?,-,?,-,-)

block_execute_statement/7

Block: block_execute_statement(-,?,?,?,?,?,?)

block_lazy_compute_expression/8

Block: block_lazy_compute_expression(-,-,?,?,?,?,?,?)

block_test_implication/6

Block: block_test_implication(?,?,?,?,?,-)

blocking_ground_copied_wait_flags/2

Block: blocking_ground_copied_wait_flags(?,-)

blocking_override/6

Block: blocking_override(-,?,?,?,?,?)

bring_ground_elements_forward/3

bselect/4

Block: bselect(?,?,-,?)

call_b_execute_operation2/11

can_be_used_for_unification/1

can_get_full_fd_value/1

check_additional_guard/4

check_additional_guard_when_bound/6

Block: check_additional_guard_when_bound(-,?,?,?,?,?) check_additional_guard_when_bound(?,-,?,?,?,?)

check_freetype_case/7

check_freetype_case2/8

Block: check_freetype_case2(?,?,-,?,?,?,-,?)

check_invariant/3

check_invariant_predicate_aux/2

check_invariant_predicate_with_time_out/3

check_invariant_predicate_with_time_out_res/3

check_invariant_with_time_out/2

check_nth1_invariant/2

check_precondition_result/5

Block: check_precondition_result(-,?,?,?,?)

check_set_bounded_aux/2

Block: check_set_bounded_aux(-,?)

check_set_lists_bounded/3

check_state_skeleton_bound/2

Block: check_state_skeleton_bound(-,?)

check_state_skeleton_bound_aux/3

Block: check_state_skeleton_bound_aux(-,?,?)

check_time_out_res/2

check_uses_implementable_integers/1

check_well_defined/4

combine_updates/3

Block: combine_updates(-,?,?)

compose_acc/4

compose_clp/4

compute_let_expressions/5

conjoin_simple/3

Block: conjoin_simple(-,?,?)

convert_list_of_expressions_into_sequence/2

convert_list_of_expressions_into_sequence/3

convert_list_of_expressions_into_set1/5

convert_list_of_expressions_into_set2/6

convert_list_of_expressions_into_set_wf/4

convert_to_prolog_pattern_match/6

convert_to_prolog_pattern_match2/6

create_any_bindings/3

create_full_operation/5

describe_constants/2

enum_pred_result/3

Block: enum_pred_result(-,-,?)

enum_pred_result0/3

Block: enum_pred_result0(-,-,?)

enumerate_bool/3

enumerate_bool0/4

Block: enumerate_bool0(?,?,?,-)

enumerate_bool_aux/2

Block: enumerate_bool_aux(-,-)

expand_forall1/4

Description:
preferences:get_preference(double_evaluation_when_analysing,false), % causes test 1112 to fail TO DO:fix

expand_forall_quantifier/6

fill_in_det_solutions/2

filter_and_convert_list_to_parameter_tuples/4

Block: filter_and_convert_list_to_parameter_tuples(-,?,?,?)

filter_and_convert_list_to_parameter_tuples_aux/6

Block: filter_and_convert_list_to_parameter_tuples_aux(-,?,-,?,?,?)

filter_results/4

filter_states/5

finalise_clp/3

finite_reasonably_sized_set/1

flatten_pairs/3

flatten_pairs/4

force_evaluation_of_lazy_value/3

generate_assignment/4

generate_recursive_closure/8

generate_unsat_properties_warnings/0

get_acc_base/3

get_acc_result/3

get_assign_expr_priority_wf/3

get_component_enum_warning_message/2

get_exists_used_ids/4

Description:
comment in to check used_ids field

get_max_card_for_value/2

get_property_components/1

get_results/7

get_results1/7

Block: get_results1(?,-,?,?,?,?,?)

get_results2/11

Block: get_results2(-,?,?,?,?,?,?,?,?,?,?)

get_span_msg/3

get_unsat_component_description/8

get_unsat_component_predicate/3

get_value/3

get_wait_flag_if_necessary/5

Block: get_wait_flag_if_necessary(-,-,?,?,?)

get_while_reads_write_info_and_filter_state/6

ground_inner_wf/3

Block: ground_inner_wf(-,?,?) ground_inner_wf(?,-,?)

ground_wait_flags_for_exists/2

ground_wait_flags_for_exists2/3

id_check/2

identifiers_not_used_in_bexp/2

init_clp_acc/4

init_wait_flags_cs/5

insert_before_substitution_variables/5

intersect_invs/2

is_couple/4

is_extension_function/3

is_extension_function_aux/2

is_for_all_set_membership_predicate/5

is_for_all_set_membership_predicate2/8

is_lambda_result_id/1

is_member_test/3

is_member_test_aux/3

is_pred_false/1

Block: is_pred_false(-)

is_pred_true/1

Block: is_pred_true(-)

is_sequence_extension_function/3

is_set_extension_function/2

keep_constant/2

l_compute_expression/5

l_compute_field/5

lazy_compute_expression/7

lazy_exclude/3

Block: lazy_exclude(-,?,?)

lazy_exclude_aux/5

Block: lazy_exclude_aux(-,?,?,?,?)

list_of_expressions_is_ground/3

lookup_value_in_global_sets_wf/7

lookup_value_in_store_and_global_sets_wf/7

lookup_values_if_vars/4

make_couplise/2

max_cardinality_ok_for_expansion/4

max_cardinality_ok_for_expansion1/5

max_cardinality_ok_for_expansion2/5

max_cardinality_ok_for_expansion2(set_extension(E),Limit,_TC,_,_) :- !, length(E,Len), Len =< Limit.

max_cardinality_ok_for_expansion2(interval(Up,Low),Limit,_TC,LS,S) :- !,
    get_integer(UpI,Up,LS,S), get_integer(LowI,Low,LS,S),
    UpI-LowI<Limit.

max_cardinality_ok_for_expansion2(integer_set(GS),Limit,_TC,_LS,_S) :- !, b_global_set_cardinality(GS,Card),
    number(Card), Card =< Limit.

max_cardinality_ok_for_expansion2(set_subtraction(A,_),Limit,TC,LS,S) :- !,
    max_cardinality_ok_for_expansion1(A,Limit,TC,LS,S).

max_cardinality_ok_for_expansion2(image(RelA,_),Limit,TC,LS,S) :- !,
    max_cardinality_ok_for_expansion1(RelA,Limit,TC,LS,S).

max_cardinality_ok_for_expansion2(function(_RelA,_),_Limit,_TC,_LS,_S) :- !,
    fail. % TO DO: we should look at the size of the range elements

max_cardinality_ok_for_expansion2(intersection(A,B),Limit,TC,LS,S) :- !,
    (max_cardinality_ok_for_expansion1(A,Limit,TC,LS,S) -> true ; max_cardinality_ok_for_expansion1(B,Limit,TC,LS,S)).

max_cardinality_ok_for_expansion2(union(A,B),Limit,TC,LS,S) :- !,
    max_cardinality_ok_for_expansion1(A,Limit,TC,LS,S), max_cardinality_ok_for_expansion1(B,Limit,TC,LS,S).

max_cardinality_ok_for_expansion2(range(A),Limit,TC,LS,S) :- !,
    max_cardinality_ok_for_expansion1(A,Limit,TC,LS,S).

max_cardinality_ok_for_expansion2(domain(A),Limit,TC,LS,S) :- !,
    max_cardinality_ok_for_expansion1(A,Limit,TC,LS,S).

max_cardinality_ok_for_expansion2(direct_product(A,B),Limit,TC,LS,S) :- !,
    max_cardinality_ok_for_expansion2(cartesian_product(A,B),Limit,TC,LS,S).

max_cardinality_ok_for_expansion2(parallel_product(A,B),Limit,TC,LS,S) :- !,
    max_cardinality_ok_for_expansion2(cartesian_product(A,B),Limit,TC,LS,S).

max_cardinality_ok_for_expansion2(cartesian_product(A,B),Limit,TC,LS,S) :- !,
    ILimit is Limit//2, ILimit>0, %use sqrt ?
    max_cardinality_ok_for_expansion1(A,ILimit,TC,LS,S),
    max_cardinality_ok_for_expansion1(B,ILimit,TC,LS,S).

max_cardinality_ok_for_expansion2(value(S),Limit,_TC,_LS,_S) :- !,
    get_max_card_for_value(S,MaxCard),
    MaxCard =< Limit.

max_cardinality_ok_for_expansion2(identifier(_ID),_Limit,TC,_LS,_S) :- !, number(TC).

max_cardinality_ok_for_expansion2(external_function_call(_,_),_,_,_,_) :- !,fail.

max_cardinality_ok_for_expansion2(lazy_lookup_expr(_),_,_,_,_) :- !,fail.

max_cardinality_ok_for_expansion2(record_field(_,_),_Limit,_TC,_LS,_S) :- !, fail.

max_cardinality_ok_for_expansion2(E,Limit,TC,_LS,_S) :- functor(E,F,N),
    print(unknown_max_card(F/N,Limit,TC)),nl,fail.

member_conjunct/3

non_ignore_unsat_component/0

not_generated_exists_paras/1

not_inv_aux/1

not_invertible/1

not_with_enum_warning_and_possible_delay/4

Meta: not_with_enum_warning_and_possible_delay(0,-,?,?)

not_with_enum_warning_delay/4

Meta: not_with_enum_warning_delay(0,-,?,?)

Block: not_with_enum_warning_delay(?,-,?,?)

obvious_enumeration/2

other_warning/1

output_parameters_value/7

parameter_list_cardinality/2

pattern_match/3

peel_implications/6

prepare_eventb_initialisation/3

project_onto_static_assertions/4

Description:
set_projection_on_static_assertions(main), %% main or all %% set by probcli if we_need_only_static_assertions

reification_relevant_for_op/1

remove_ids_defined_by_equality/5

reset_b_interpreter/0

reset_unsat_component_infos/0

set_projection_on_static_assertions/1

set_up_localstate_for_global_let/6

set_up_localstate_for_let/7

set_up_typed_localstate/3

set_up_typed_localstate/6

set_up_typed_localstate2/8

setup_read_output_variable/2

setup_result_input_values/2

simple_expression/1

simple_expression_aux/1

solve_properties/3

solve_properties/4

solve_properties(sat,Properties,_TypedConstants,ConstantsState) :- !,
    b2sat:solve_predicate_with_satsolver_free(Properties, ConstantsState,Result,[]),
    Result=solution(_).

solve_properties('sat-z3',Properties,_TypedConstants,ConstantsState) :- !,
    b2sat:solve_predicate_with_satsolver_free(Properties, ConstantsState,Result,[use_satsolver(z3)]),
    Result=solution(_).

solve_properties(cdclt,Properties,_TypedConstants,ConstantsState) :- !,
    cdclt_solver:cdclt_solve_predicate(Properties, _,Result),
    Result=solution(ConstantsState).

solve_properties(kodkod,PProperties,PUnsortedConstants,ConstantsState) :- !,
    solve_properties(prob,PProperties,PUnsortedConstants,ConstantsState). % Kodkod processing is done elswehere

solve_properties(prob,PProperties,PUnsortedConstants,ConstantsState) :- !,
    (preferences:preference(use_static_ordering,true)
    -> sort_ids_by_usage(PUnsortedConstants,PProperties,Constants,no_warnings), % no_warnings as Ids could be used in operations, assertions, ...
    set_up_typed_localstate(Constants,_FreshVars,TypedVals,[],SortedState,positive),
    reorder_state(PUnsortedConstants,SortedState,ConstantsState)
    ; Constants = PUnsortedConstants,
    set_up_typed_localstate(Constants,_FreshVars,TypedVals,[],ConstantsState,positive)
    ),
    % now try and load saved constants from file for sub-machines when -cache is used:
    load_partial_constants(ConstantsState,PProperties,LPProperties), % Note: this can backtrack
    reset_component_info(true), % reset in case load_partial_constants backtracks! relevant for test 2112
    b_global_sets:static_symmetry_reduction_for_global_sets(ConstantsState),
    b_trace_test_components_full(LPProperties,ConstantsState,TypedVals).

solve_properties(SolverName,Properties,_TypedConstants,ConstantsState) :-
    temporary_set_preference(z3_solve_for_animation, true,Chng),
    call_cleanup(smt_solvers_interface:smt_solve_predicate_free(SolverName, Properties, ConstantsState),
    reset_temporary_preference(z3_solve_for_animation,Chng)).

sort_aux/4

sort_variable_binding/2

state_satisfies_assertions/3

state_satisfies_invariant_aux/2

state_violates_assertions/2

state_violates_assertions_aux/2

state_violates_invariant/2

store_values/3

tcltk_quick_describe_unsat_properties/2

tcltk_quick_describe_unsat_properties(list(FullDescr),STATUS) :-
    retractall(uses_implementable_integers),
    retractall(min_max_integer_value_used(_,_)), assertz(min_max_integer_value_used(none,none)),
    get_property_components(Components),
    (unsat_properties_conjunct_inside_component(_,_,false,_)
    -> STATUS='FALSE'
    ; all_unsat_components_marked_prob_ignore
    -> STATUS = 'prob-ignore'
    ; STATUS='UNKNOWN'
    ),
    findall(TP, (unsat_properties_conjunct_inside_component(CompNr,P,_Status,_ReasonMsg), % find individual conjuncts
    % Status can be false or unknown
    nth1(CompNr,Components,component(FullPred,_Vars)),
    check_uses_implementable_integers(FullPred), % for the min-max one may need to look at the entire component !
    translate_bexpression_with_limit(P,TrP),
    get_component_enum_warning_message(CompNr,EnumWarningAbortMsg),
    (EnumWarningAbortMsg = '' -> Prefix = '' ; Prefix = '\n '),
    get_span_msg(P,'\n ',SpanMsg),
    ajoin([' * ',TrP,Prefix,EnumWarningAbortMsg,SpanMsg,'\n'],TP)),
    D1),
    findall([Msg1,PS|DescrVars],
    (get_unsat_component_description(Components,CompNr,MaxCompNr,
    Size,PS,DescrVars,EnumWarningAbortMsg,SpanMsg),
    ajoin([' * Predicate Component ',EnumWarningAbortMsg,CompNr,'/',MaxCompNr,
    ' (with ',Size,' conjunct(s))',SpanMsg, ':'],Msg1)),
    UC),
    append(UC,UCL), % join all component descriptions
    (D1=[]
    % TO DO: adapt message for enumeration warning
    -> Descr = D2,
    (UCL=[] -> D2 = ['The properties were satisfiable']
    ; D2 = ['No solution found for the following predicates: '|UCL]
    )
    ; Descr = ['The following properties prevented finding a solution:\n'|D12],
    % Comment: the predicate can trigger the computation of another earlier registered predicate
    % Example f = {1|->2} & f: A --> B & A = 1..5; A=1..5 triggers the check for f
    (UCL=[] -> D2=[]
    ; D2 = ['\nIn addition no solution was found for the following predicates: '|UCL]
    ),
    append(D1,D2,D12)),
    findall(W,other_warning(W),Warnings),
    (Warnings = [] -> FullDescr=Descr ; append(Descr,['\nWARNINGS/MESSAGES:'|Warnings],FullDescr)).

tcltk_unsatisfiable_components_exist/0

test_forall_instance/5

to_be_marked_as_symbolic_aux/2

tp2/3

translate_init_statements/2

triggers_enum_warning/5

try_get_op_name/2

try_lookup_value_in_store_and_global_sets/3

unop_to_be_marked_as_symbolic/2

unused_localvariable/2

Determinacy Checker:

! 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(no_terminal_colors,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_release,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_release,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_avl_custom,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_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),_82983,[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'),_52709,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/error_manager.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),_45755,[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),_44091,[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 extension('counter/counter') does not exist
! goal: absolute_file_name(extension('counter/counter'),_106883,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/succeed_max.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(tools) does not exist
! goal: absolute_file_name(probsrc(tools),_154505,[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),_182925,[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),_182925,[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),_185069,[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),_191047,[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 probsrc(eventhandling) does not exist
! goal: absolute_file_name(probsrc(eventhandling),_194469,[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),_191047,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/typing_tools.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'),_196457,[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),_195693,[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),_195693,[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),_196989,[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),_196315,[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),_197309,[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),_191047,[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 probsrc(kernel_waitflags) does not exist
! goal: absolute_file_name(probsrc(kernel_waitflags),_182925,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/delay.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: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),_213795,[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),_208101,[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: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),_191189,[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 probsrc(custom_explicit_sets) does not exist
! goal: absolute_file_name(probsrc(custom_explicit_sets),_182925,[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),_157781,[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),_154217,[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(eventhandling) does not exist
! goal: absolute_file_name(probsrc(eventhandling),_157359,[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(b_state_model_check) does not exist
! goal: absolute_file_name(probsrc(b_state_model_check),_154363,[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(bmachine_eventb) does not exist
! goal: absolute_file_name(probsrc(bmachine_eventb),_147391,[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),_147391,[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),_148771,[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),_147391,[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: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),_149965,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/xtl_interface.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),_144257,[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 extension('probhash/probhash') does not exist
! goal: absolute_file_name(extension('probhash/probhash'),_143969,[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 kodkodsrc(kodkod) does not exist
! goal: absolute_file_name(kodkodsrc(kodkod),_113571,[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('probhash/probhash') does not exist
! goal: absolute_file_name(extension('probhash/probhash'),_106883,[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(btypechecker) does not exist
! goal: absolute_file_name(probsrc(btypechecker),_94657,[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 probsrc(gensym) does not exist
! goal: absolute_file_name(probsrc(gensym),_74621,[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(custom_explicit_sets) does not exist
! goal: absolute_file_name(probsrc(custom_explicit_sets),_45639,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/bsyntaxtree.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'),_47787,[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),_45785,[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'),_35835,[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 extension('counter/counter') does not exist
! goal: absolute_file_name(extension('counter/counter'),_9679,[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 kodkodsrc(kodkod) does not exist
! goal: absolute_file_name(kodkodsrc(kodkod),_261,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/b_interpreter.pl')])

Name: conjunct_predicates/2	Module: foo_error
Name: =/2
Name: ->/3
Name: findall/3
Name: b_machine_temp_predicate/1	Module: bmachine

Name: add_lazy_let_id_and_expression/7	Module: b_interpreter
Name: empty_avl/1	Module: foo_error

Name: basic_type/2	Module: kernel_objects
Name: add_var_to_localstate/4	Module: foo_error

Name: fail
Name: add_internal_error/2	Module: foo_error
Name: =/2
Name: add_typed_vars_to_localstate_aux/4	Module: b_interpreter
Name: flatten_pairs/3	Module: b_interpreter
Name: ->/3

Name: RECURSIVE_CALL/4	Module: b_interpreter
Name: add_typed_var_to_localstate/5	Module: b_interpreter
Name: get_texpr_type/2	Module: foo_error
Name: get_texpr_id/2	Module: foo_error
Name: !

Name: b_set_up_concrete_constants/2	Module: b_interpreter
Name: get_property_components/1	Module: b_interpreter

Name: b_test_boolean_expression2/7	Module: b_interpreter
Name: b_not_test_boolean_expression2/7	Module: b_interpreter
Name: add_lazy_let_id_and_expression/6	Module: b_interpreter

Name: lazy_compute_expression/7	Module: b_interpreter
Name: add_lazy_let_id_to_local_state/5	Module: b_interpreter

Name: b_sum_or_mul_over_list_acc/11	Module: b_interpreter
Name: b_sum_or_mul_over_list_clp/9	Module: b_interpreter

Name: add_wd_error_span/4	Module: foo_error
Name: translate_bexpression_with_limit/3	Module: foo_error

Name: non_ignore_unsat_component/0	Module: b_interpreter
Name: not/1
Name: !
Name: unsat_properties_conjunct_inside_component/4	dynamic predicate

Name: maplist/2	Module: foo_error
Name: prepare_state_for_specfile_trans/3	Module: specfile
Name: visited_expression/2	Module: foo_error
Name: b_invariant_number_list/1	Module: foo_error

Name: get_state_space_errors/0	Module: prob_cli
Name: cli_execute_aux/7	Module: prob_cli
Name: model_check_aux/5	Module: prob_cli

Name: b_test_exists/7	Module: b_interpreter
Name: b_optimized_b_test_instance/4	Module: b_interpreter

Name: kernel_call_predicate_equal_object_optimized/3	Module: foo_error
Name: mark_closure_as_symbolic/2	Module: closures
Name: =/2
Name: var/1
Name: ->/3
Name: b_expand_compute_comprehension_set/4	Module: b_interpreter
Name: definitely_expand_this_explicit_set/1	Module: foo_error
Name: constant_variable_marked_as_expand/1	Module: foo_error
Name: b_compute_expression/5	Module: b_interpreter
Name: debug_println/2	Module: foo_error
Name: register_memoization_function/6	Module: memoization
Name: \=/2
Name: nonvar/1
Name: get_texpr_id/2	Module: foo_error
Name: !
Name: constant_variable_marked_as_memo/1	Module: foo_error
Name: preference/2	Module: foo_error

Name: b_apply_function_set_extension_aux/9	Module: b_interpreter
Name: equality_objects_wf/4	Module: kernel_equality
Name: b_compute_expression/5	Module: b_interpreter
Name: add_wd_error_span/4	Module: foo_error

Name: b_apply_function_set_extension_aux/9	Module: b_interpreter
Name: b_compute_expression_function/8	Module: b_interpreter

Name: b_apply_function_set_extension/7	Module: b_interpreter
Name: equal_object_wf/4	Module: foo_error
Name: b_compute_expression/5	Module: b_interpreter

Name: fail
Name: add_internal_error_wf/5	Module: foo_error
Name: RECURSIVE_CALL/8	Module: b_interpreter
Name: get_texpr_expr/2	Module: foo_error
Name: overwrite_record_wf/5	Module: kernel_records
Name: b_compute_expression/5	Module: b_interpreter
Name: !
Name: blocking_override/6	Module: b_interpreter
Name: ground_value_check/2	Module: kernel_tools
Name: override/5	Module: foo_error
Name: =/2
Name: ->/3
Name: b_compute_assign_expressions_when/6	Module: b_interpreter
Name: equal_object_wf/4	Module: foo_error

Name: RECURSIVE_CALL/7	Module: b_interpreter
Name: b_assign_value_or_function/8	Module: b_interpreter
Name: get_texpr_expr/2	Module: foo_error

Name: b_execute_eventb_action/6	Module: b_interpreter_eventb
Name: b_execute_statement2/8	Module: b_interpreter

Name: enum_pred_result0/3	Module: b_interpreter
Name: get_wait_flag0/2	Module: foo_error
Name: enum_pred_result/3	Module: b_interpreter
Name: get_enumeration_finished_wait_flag/2	Module: foo_error
Name: ==/2
Name: ->/3
Name: true
Name: nonvar/1
Name: b_check_boolean_expression/5	Module: foo_error

Name: b_check_execute_while_loop2/11	Module: b_interpreter
Name: b_try_check_boolean_expression_c/5	Module: b_interpreter
Name: add_abort_error_span/5	Module: foo_error

Name: equiv_test_boolean_expression/7	Module: foo_error
Name: =/2
Name: equiv_bidrectional_test_boolean_expression/7	Module: foo_error
Name: b_check_boolean_expression/7	Module: foo_error
Name: var/1
Name: ->/3

Name: b_not_test_equivalence/7	Module: b_interpreter
Name: b_test_equivalence/7	Module: b_interpreter

prob_prolog/src/b_interpreter.pl

Modules

Predicates of b_interpreter

Module Information

4553 Lines

342 Predicates

35 Exports

80 specified Imports

Predicates:

Name: b_clpfd_if_then_else_block/9	Module: b_interpreter
Name: get_wait_flag0/2	Module: foo_error

Name: b_compute_expressions_when2/6	Module: b_interpreter
Name: get_assign_expr_priority_wf/3	Module: b_interpreter

Name: greater_than_equal/2	Module: kernel_objects
Name: in_nat_range/3	Module: kernel_objects
Name: number/1
Name: ->/3
Name: max_cardinality/2	Module: kernel_objects
Name: get_set_type/2	Module: bsyntaxtree
Name: true
Name: ground/1
Name: b_compute_card2/8	Module: b_interpreter

Name: must_succ_kernel_call/4	Module: kernel_mappings
Name: b_compute_expression2/7	Module: b_interpreter
Name: get_set_type/2	Module: bsyntaxtree
Name: b_compute_comprehension_set_symbolic/7	Module: b_interpreter
Name: !
Name: cardinality_of_range/3	Module: kernel_objects
Name: b_compute_expression/5	Module: b_interpreter
Name: cardinality_of_set_extension_list/3	Module: kernel_objects
Name: b_compute_expressions/5	Module: b_interpreter

Name: b_compute_comprehension_set_aux/4	Module: b_interpreter
Name: b_generate_closure_if_necessary/6	Module: b_interpreter

Name: b_general_sum_or_mul/10	Module: b_interpreter
Name: b_compute_expression2/7	Module: b_interpreter

Name: b_compute_comprehension_set_sym/3	Module: b_interpreter
Name: add_message/4	Module: foo_error
Name: =/2
Name: contains_info_pos/1	Module: foo_error
Name: ->/3
Name: !
Name: silent_mode/1	Module: foo_error

Name: b_compute_card2/8	Module: b_interpreter
Name: b_test_atomic_not_equal_boolean_expression/6	Module: b_interpreter

Name: b_compile1/8	Module: b_compiler
Name: b_compute_expressions/5	Module: b_interpreter
Name: b_test_atomic_equal_boolean_expression/6	Module: b_interpreter
Name: l_compute_expression/5	Module: b_interpreter
Name: compute_let_expressions/5	Module: b_interpreter
Name: evaluate_result_expr/6	Module: custom_explicit_sets
Name: b_apply_function_set_extension/7	Module: b_interpreter
Name: b_clpfd_if_then_else_block/9	Module: b_interpreter
Name: b_apply_function_set_extension_aux/9	Module: b_interpreter
Name: b_compute_if_then_else/7	Module: b_interpreter
Name: b_test_member_expression2/7	Module: b_interpreter
Name: SATSOLVER/6	Module: external_functions
Name: b_assign_value_or_function/8	Module: b_interpreter
Name: b_execute_while_when_state_set/10	Module: b_interpreter
Name: check_well_defined/4	Module: b_interpreter
Name: b_test_atomic_boolean_expression2/5	Module: b_interpreter
Name: check_element_of_function_closure/6	Module: custom_explicit_sets
Name: b_not_test_atomic_boolean_expression2/7	Module: b_interpreter
Name: b_test_closure/6	Module: custom_explicit_sets
Name: b_generate_set_for_all_domain/7	Module: b_interpreter
Name: b_compute_expression_when2/6	Module: b_interpreter
Name: b_compute_expression_nowf/7	Module: b_interpreter
Name: b_execute_statement2/8	Module: b_interpreter
Name: b_compute_expression2/7	Module: b_interpreter
Name: b_compute_card2/8	Module: b_interpreter
Name: b_compute_expression_function/8	Module: b_interpreter
Name: b_compute_field/5	Module: b_interpreter
Name: b_test_notmember_expression/7	Module: b_interpreter
Name: KODKOD/6	Module: external_functions
Name: b_general_sum_or_mul/10	Module: b_interpreter
Name: b_test_atomic_not_equal_boolean_expression/6	Module: b_interpreter
Name: optimizing_solve_predicate/7	Module: optimizing_solver
Name: b_sum_or_mul_over_list_acc/11	Module: b_interpreter
Name: b_execute_let_definitions/4	Module: b_interpreter
Name: b_sum_or_mul_over_list_clp/9	Module: b_interpreter
Name: b_add_constant_definition_aux/9	Module: b_interpreter

Name: fail
Name: nl
Name: print/1
Name: print_functor/1	Module: tools_printing
Name: add_internal_error/2	Module: foo_error
Name: ==/2
Name: ->/3
Name: b_execute_operation_in_expression/7	Module: b_interpreter
Name: def_get_texpr_id/2	Module: foo_error
Name: !
Name: binary_kernel_call/9	Module: foo_error
Name: b_compute_expression/5	Module: b_interpreter
Name: equal_object_wf/4	Module: foo_error
Name: binary_arg1_determines_value/3	Module: foo_error
Name: arg/3
Name: binary_function/3	Module: foo_error
Name: functor/3
Name: unary_kernel_call/8	Module: foo_error
Name: unary_function/3	Module: foo_error
Name: equal_object_wf/3	Module: foo_error
Name: mark_closure_as_symbolic/2	Module: closures
Name: binop_to_be_marked_as_symbolic/3	Module: b_interpreter
Name: construct_member_closure/5	Module: foo_error
Name: =../2
Name: create_texpr/4	Module: foo_error
Name: get_texpr_type/2	Module: foo_error
Name: do_not_keep_symbolic/5	Module: foo_error
Name: if/3
Name: empty_set/1	Module: foo_error
Name: is_definitely_empty/3	Module: foo_error
Name: symbolic_closure_binary_operator/1	Module: kernel_mappings
Name: is_set_type/2	Module: bsyntaxtree
Name: unop_to_be_marked_as_symbolic/2	Module: b_interpreter
Name: do_not_keep_symbolic_unary/2	Module: foo_error
Name: symbolic_closure_unary_operator/1	Module: foo_error
Name: call_external_function/7	Module: foo_error
Name: push_wait_flag_call_stack_info/3	Module: foo_error
Name: b_compute_expressions/5	Module: b_interpreter
Name: kernel_call/4	Module: foo_error
Name: special_operator_for_image/3	Module: foo_error
Name: same_texpr/2	Module: foo_error
Name: add_wd_error_if_false/5	Module: b_interpreter
Name: true
Name: ground_value/1	Module: kernel_tools
Name: nonvar/1
Name: when/2
Name: get_last_wait_flag/3	Module: foo_error
Name: add_wd_error_span/4	Module: foo_error
Name: translate_bexpression_with_limit/3	Module: foo_error
Name: b_try_check_boolean_expression_no_enum_wf/5	Module: b_interpreter
Name: =/2
Name: get_preference/2	Module: foo_error
Name: opt_push_wait_flag_call_stack_info/3	Module: foo_error
Name: check_freetype_case/7	Module: b_interpreter
Name: set_up_localstate_for_let/7	Module: b_interpreter
Name: set_up_localstate_for_global_let/6	Module: b_interpreter
Name: debug_println/2	Module: foo_error
Name: b_compute_if_then_else/7	Module: b_interpreter
Name: b_clpfd_if_then_else/8	Module: b_interpreter
Name: always_well_defined/1	Module: foo_error
Name: preference/2	Module: preferences
Name: can_get_full_fd_value/1	Module: b_interpreter
Name: var/1
Name: b_try_check_boolean_expression_wf/5	Module: b_interpreter
Name: b_general_sum_or_mul/10	Module: b_interpreter
Name: generate_recursive_closure/8	Module: b_interpreter
Name: safe_create_texpr/3	Module: foo_error
Name: unique_typed_id/3	Module: foo_error
Name: get_texpr_set_type/2	Module: bsyntaxtree
Name: get_texpr_expr/2	Module: foo_error
Name: b_compute_comprehension_set/7	Module: b_interpreter
Name: b_convert_bool/5	Module: b_interpreter
Name: b_compute_min/7	Module: b_interpreter
Name: b_compute_max/7	Module: b_interpreter
Name: b_compute_card/8	Module: b_interpreter
Name: b_compute_expression_function/8	Module: b_interpreter
Name: access_record_wf/4	Module: foo_error
Name: construct_record_wf/3	Module: foo_error
Name: l_compute_field/5	Module: b_interpreter
Name: construct_real/2	Module: foo_error
Name: add_lazy_let_id_and_expression/6	Module: b_interpreter
Name: lookup_value_for_existing_id_wf/4	Module: foo_error
Name: lookup_value_in_store_and_global_sets_wf/7	Module: b_interpreter
Name: get_preference/2	Module: preferences
Name: event_b_identity_for_type/3	Module: foo_error
Name: get_set_type/2	Module: bsyntaxtree
Name: empty_sequence/1	Module: foo_error