6131 Lines

607 Predicates

Imported Modules: error_manager self_check avl kernel_waitflags kernel_tools delay tools avl_tools clpfd closures b_compiler performance_messages kernel_card_arithmetic debug bool_pred clpfd_tables b_enumerate terms

172 Exports

104 specified Imports

Imports	Exports
Name: module_info/2 Module: module_information Name: print_term_summary/1 Module: tools_printing Name: print_error/1 Module: tools_printing Name: preference/2 Module: preferences Name: equal_object/2 Module: kernel_objects Name: equal_object/3 Module: kernel_objects Name: enumerate_freetype_wf/4 Module: kernel_freetypes Name: freetype_cardinality/2 Module: kernel_freetypes Name: is_infinite_freetype/1 Module: kernel_freetypes Name: is_empty_freetype/1 Module: kernel_freetypes Name: is_non_empty_freetype/1 Module: kernel_freetypes Name: test_empty_freetype/2 Module: kernel_freetypes Name: try_post_constraint/1 Module: clpfd_interface Name: clpfd_reify_inlist/4 Module: clpfd_interface Name: safe_sort/3 Module: tools Name: translate_bvalue/2 Module: translate Name: unify_types_strict/2 Module: btypechecker Name: get_texpr_pos/2 Module: bsyntaxtree Name: eq_atomic/4 Module: kernel_equality Name: equality_objects/3 Module: kernel_equality Name: equality_objects_wf_no_enum/4 Module: kernel_equality Name: equality_objects_with_type_wf/5 Module: kernel_equality Name: empty_cartesian_product_wf/4 Module: kernel_equality Name: safe_syntaxelement_det/5 Module: bsyntaxtree Name: is_set_type/2 Module: bsyntaxtree Name: get_texpr_ids/2 Module: bsyntaxtree Name: get_texpr_expr/2 Module: bsyntaxtree Name: get_negated_operator_expr/2 Module: bsyntaxtree Name: split_names_and_types/3 Module: bsyntaxtree Name: b_empty_global_set/1 Module: b_global_sets Name: b_non_empty_global_set/1 Module: b_global_sets Name: b_global_set_cardinality/2 Module: b_global_sets Name: maplist/3 Module: lists Name: maplist/4 Module: lists Name: couplise_list/2 Module: btypechecker Name: is_truth/1 Module: bsyntaxtree Name: empty_set_test/2 Module: kernel_equality Name: block_inf_greater/2 Module: inf_arith Name: get_texpr_info/2 Module: bsyntaxtree Name: get_texpr_id/2 Module: bsyntaxtree Name: infinite_global_set/1 Module: b_global_sets Name: infgreater/2 Module: inf_arith Name: is_a_disjunct/3 Module: bsyntaxtree Name: compute_memo_hash/2 Module: memoization Name: get_stored_memo_expansion/3 Module: memoization Name: store_memo_expansion/3 Module: memoization Name: create_negation/2 Module: bsyntaxtree Name: test_interval_subset_wf/6 Module: kernel_equality Name: create_typed_id/3 Module: bsyntaxtree Name: create_exists_opt_liftable/3 Module: bsyntaxtree Name: select/3 Module: lists Name: get_unique_id/2 Module: b_ast_cleanup Name: conjunct_predicates/2 Module: bsyntaxtree Name: disjunct_predicates/2 Module: bsyntaxtree Name: create_typed_id/3 Module: bsyntaxtree Name: get_texpr_type/2 Module: bsyntaxtree Name: get_domain_range_for_closure_types/3 Module: closures Name: membership_test_wf/4 Module: kernel_equality Name: b_type2_set/2 Module: b_global_sets Name: rename_bt/3 Module: bsyntaxtree Name: extract_info/2 Module: bsyntaxtree Name: extract_info_wo_used_ids/2 Module: bsyntaxtree Name: extract_info/3 Module: bsyntaxtree Name: rename_bt/3 Module: bsyntaxtree Name: replace_id_by_expr/4 Module: bsyntaxtree Name: couplise_list/2 Module: btypechecker Name: ord_union/3 Module: ordsets Name: reverse/2 Module: lists Name: is_maximal_freetype/1 Module: kernel_freetypes Name: avl_approximate_size_from_height/2 Module: avl_tools Name: safe_create_texpr/4 Module: bsyntaxtree Name: create_texpr/4 Module: bsyntaxtree Name: conjunct_predicates/2 Module: bsyntaxtree Name: mark_bexpr_as_symbolic/2 Module: bsyntaxtree Name: ord_subtract/3 Module: ordsets Name: last/2 Module: lists Name: all_elements_of_type_wf/3 Module: b_global_sets Name: all_elements_of_type_rand_wf/3 Module: b_global_sets Name: expand_freetype/3 Module: kernel_freetypes Name: equal_object_wf/4 Module: kernel_objects Name: element_of_global_set/2 Module: kernel_objects Name: element_of_global_set_wf/3 Module: kernel_objects Name: try_get_fd_value_list/4 Module: clpfd_lists Name: get_fd_value/3 Module: clpfd_lists Name: in_fd_value_list_wf/4 Module: clpfd_lists Name: avl_fd_value_check/4 Module: clpfd_lists Name: catch_and_ignore_clpfd_overflow/2 Module: clpfd_interface Name: random/3 Module: random Name: check_element_of_wf/3 Module: kernel_objects Name: not_element_of_wf/3 Module: kernel_objects Name: element_of_memoization_closure/6 Module: memoization Name: set_up_localstate/4 Module: store Name: not_element_of_global_set/2 Module: kernel_objects Name: get_global_type_value/3 Module: b_global_sets Name: not_element_of_memoization_closure/6 Module: memoization Name: same_length/2 Module: lists Name: convert_list_into_pairs/2 Module: tools Name: b_test_boolean_expression/4 Module: b_interpreter Name: b_not_test_boolean_expression/4 Module: b_interpreter Name: create_typed_ids/3 Module: bsyntaxtree Name: is_memoization_closure/4 Module: memoization Name: get_complete_memoization_expansion/6 Module: memoization Name: split_names_and_types/3 Module: bsyntaxtree Name: def_get_texpr_id/2 Module: bsyntaxtree	Name: is_set_value/2 Name: is_custom_explicit_set/1 Name: is_custom_explicit_set/2 Name: is_custom_explicit_set_nonvar/1 Name: equal_explicit_sets_wf/3 Name: not_equal_explicit_sets_wf/3 Name: equality_explicit_sets_wf/4 Name: same_texpr_body/2 Name: same_closure/2 Name: is_empty_explicit_set/1 Name: is_empty_explicit_set_wf/2 Name: is_empty_closure_wf/4 Name: is_non_empty_explicit_set/1 Name: is_non_empty_explicit_set_wf/2 Name: is_non_empty_closure_wf/4 Name: test_empty_explicit_set_wf/3 Name: test_empty_closure_wf/5 Name: is_definitely_maximal_set/1 Name: explicit_set_cardinality/2 Name: explicit_set_cardinality_wf/3 Name: explicit_set_cardinality_for_wf/2 Name: card_for_specific_custom_set/3 Name: card_for_specific_closure/4 Name: efficient_card_for_set/3 Name: quick_custom_explicit_set_approximate_size/2 Name: avl_approximate_size/2 Name: avl_approximate_size/3 Name: is_infinite_explicit_set/1 Name: is_infinite_closure/3 Name: is_infinite_global_set/2 Name: is_simple_infinite_set/1 Name: dont_expand_this_explicit_set/1 Name: dont_expand_this_explicit_set/2 Name: dont_expand_symbolic_explicit_set/1 Name: definitely_expand_this_explicit_set/1 Name: is_infinite_or_very_large_explicit_set/1 Name: is_infinite_or_very_large_explicit_set/2 Name: is_cartesian_product_closure/3 Name: expand_custom_set/2 Name: expand_custom_set_wf/4 Name: try_expand_custom_set/2 Name: try_expand_custom_set_with_catch/3 Name: try_expand_custom_set_wf/4 Name: expand_custom_set_to_list/2 Name: expand_custom_set_to_list/4 Name: expand_custom_set_to_list_wf/5 Name: try_expand_custom_set_to_list_wf/5 Name: expand_custom_set_to_list_no_dups_wf/5 Name: expand_custom_set_to_list_gg/4 Name: try_expand_custom_set_to_list/4 Name: expand_interval_closure_to_avl/3 Name: expand_custom_set_to_list_now/2 Name: expand_closure_to_avl_or_list/6 Name: expand_closure_to_list/7 Name: expand_only_custom_closure_global/4 Name: expand_and_convert_to_avl_set/4 Name: ord_list_to_avlset_direct/3 Name: sorted_ground_normalised_list_to_avlset/3 Name: try_expand_and_convert_to_avl/2 Name: convert_to_avl/2 Name: should_be_converted_to_avl_from_lists/1 Name: should_be_converted_to_avl/1 Name: try_expand_and_convert_to_avl_with_check/3 Name: try_expand_and_convert_to_avl_with_check/4 Name: try_expand_and_convert_to_avl_unless_large_wf/3 Name: try_expand_and_convert_to_avl_if_smaller_than/3 Name: is_small_specific_custom_set/2 Name: quick_propagation_element_information/4 Name: element_of_custom_set/2 Name: element_of_custom_set_wf/3 Name: element_of_closure/5 Name: check_element_of_function_closure/6 Name: not_element_of_custom_set_wf/3 Name: membership_custom_set/3 Name: membership_custom_set_wf/4 Name: membership_avl_set_wf/4 Name: quick_test_avl_membership/3 Name: lazy_check_elements_of_closure/6 Name: is_efficient_custom_set/1 Name: remove_minimum_element_custom_set/3 Name: is_maximal_global_set/1 Name: quick_is_definitely_maximal_set/1 Name: quick_definitely_maximal_set_avl/1 Name: is_one_element_custom_set/2 Name: singleton_set/2 Name: construct_singleton_avl_set/2 Name: is_one_element_avl/2 Name: construct_one_element_custom_set/2 Name: avl_is_interval/3 Name: closure1_for_explicit_set/2 Name: closure1_for_explicit_set_from/3 Name: check_in_domain_of_avlset/2 Name: check_unique_in_domain_of_avlset/2 Name: domain_of_explicit_set_wf/3 Name: range_of_explicit_set_wf/3 Name: is_avl_partial_function/1 Name: is_not_avl_partial_function/2 Name: is_avl_total_function_over_domain/2 Name: quick_definitely_maximal_total_function_avl/1 Name: is_avl_relation/1 Name: is_avl_relation_over_domain/3 Name: is_avl_relation_over_range/3 Name: is_not_avl_relation_over_domain_range/4 Name: is_not_avl_relation_over_range/3 Name: is_avl_sequence/1 Name: safe_is_avl_sequence/1 Name: get_avl_sequence/2 Name: is_injective_avl_relation/2 Name: invert_explicit_set/2 Name: union_of_explicit_set/3 Name: union_generalized_explicit_set/3 Name: difference_of_explicit_set_wf/4 Name: intersection_of_explicit_set_wf/4 Name: intersection_with_interval_closure/3 Name: disjoint_intervals_with_inf/4 Name: image_for_id_closure/3 Name: image_for_explicit_set/4 Name: rel_composition_for_explicit_set/3 Name: element_can_be_added_or_removed_to_avl/1 Name: add_element_to_explicit_set_wf/4 Name: remove_element_from_explicit_set/3 Name: delete_element_from_explicit_set/3 Name: at_most_one_match_possible/3 Name: apply_to_avl_set/5 Name: try_apply_to_avl_set/3 Name: min_of_explicit_set_wf/3 Name: max_of_explicit_set_wf/3 Name: sum_or_mul_of_explicit_set/3 Name: domain_restriction_explicit_set_wf/4 Name: range_restriction_explicit_set_wf/4 Name: domain_subtraction_explicit_set_wf/4 Name: range_subtraction_explicit_set_wf/4 Name: override_pair_explicit_set/4 Name: direct_product_explicit_set/3 Name: override_custom_explicit_set_wf/4 Name: symbolic_functionality_check_closure/2 Name: symbolic_injectivity_check_closure/2 Name: subset_of_explicit_set/4 Name: not_subset_of_explicit_set/4 Name: test_subset_of_explicit_set/5 Name: conc_custom_explicit_set/2 Name: prefix_of_custom_explicit_set/4 Name: suffix_of_custom_explicit_set/4 Name: concat_custom_explicit_set/4 Name: prepend_custom_explicit_set/3 Name: append_custom_explicit_set/4 Name: tail_sequence_custom_explicit_set/5 Name: last_sequence_explicit_set/2 Name: front_sequence_custom_explicit_set/3 Name: reverse_custom_explicit_set/2 Name: size_of_custom_explicit_set/3 Name: get_first_avl_elements/4 Name: construct_avl_from_lists/2 Name: construct_avl_from_lists_wf/3 Name: equal_avl_tree/2 Name: check_avl_in_interval/3 Name: check_interval_in_custom_set/4 Name: check_avl_subset/2 Name: construct_closure/4 Name: is_closure/4 Name: construct_member_closure/5 Name: construct_interval_closure/3 Name: is_interval_closure/3 Name: is_interval_closure/5 Name: is_interval_closure_or_integerset/3 Name: is_interval_with_integer_bounds/3 Name: is_powerset_closure/3 Name: dom_range_for_specific_closure/5 Name: dom_for_specific_closure/4 Name: dom_for_lambda_closure/2 Name: portray_custom_explicit_set/1 Name: closure_occurs_check/4

Imports

Exports

Name: module_info/2

Module: module_information

Name: print_term_summary/1

Module: tools_printing

Name: print_error/1

Module: tools_printing

Name: preference/2

Module: preferences

Name: equal_object/2

Module: kernel_objects

Name: equal_object/3

Module: kernel_objects

Name: enumerate_freetype_wf/4

Module: kernel_freetypes

Name: freetype_cardinality/2

Module: kernel_freetypes

Name: is_infinite_freetype/1

Module: kernel_freetypes

Name: is_empty_freetype/1

Module: kernel_freetypes

Name: is_non_empty_freetype/1

Module: kernel_freetypes

Name: test_empty_freetype/2

Module: kernel_freetypes

Name: try_post_constraint/1

Module: clpfd_interface

Name: clpfd_reify_inlist/4

Module: clpfd_interface

Name: safe_sort/3

Module: tools

Name: translate_bvalue/2

Module: translate

Name: unify_types_strict/2

Module: btypechecker

Name: get_texpr_pos/2

Module: bsyntaxtree

Name: eq_atomic/4

Module: kernel_equality

Name: equality_objects/3

Module: kernel_equality

Name: equality_objects_wf_no_enum/4

Module: kernel_equality

Name: equality_objects_with_type_wf/5

Module: kernel_equality

Name: empty_cartesian_product_wf/4

Module: kernel_equality

Name: safe_syntaxelement_det/5

Module: bsyntaxtree

Name: is_set_type/2

Module: bsyntaxtree

Name: get_texpr_ids/2

Module: bsyntaxtree

Name: get_texpr_expr/2

Module: bsyntaxtree

Name: get_negated_operator_expr/2

Module: bsyntaxtree

Name: split_names_and_types/3

Module: bsyntaxtree

Name: b_empty_global_set/1

Module: b_global_sets

Name: b_non_empty_global_set/1

Module: b_global_sets

Name: b_global_set_cardinality/2

Module: b_global_sets

Name: maplist/3

Module: lists

Name: maplist/4

Module: lists

Name: couplise_list/2

Module: btypechecker

Name: is_truth/1

Module: bsyntaxtree

Name: empty_set_test/2

Module: kernel_equality

Name: block_inf_greater/2

Module: inf_arith

Name: get_texpr_info/2

Module: bsyntaxtree

Name: get_texpr_id/2

Module: bsyntaxtree

Name: infinite_global_set/1

Module: b_global_sets

Name: infgreater/2

Module: inf_arith

Name: is_a_disjunct/3

Module: bsyntaxtree

Name: compute_memo_hash/2

Module: memoization

Name: get_stored_memo_expansion/3

Module: memoization

Name: store_memo_expansion/3

Module: memoization

Name: create_negation/2

Module: bsyntaxtree

Name: test_interval_subset_wf/6

Module: kernel_equality

Name: create_typed_id/3

Module: bsyntaxtree

Name: create_exists_opt_liftable/3

Module: bsyntaxtree

Name: select/3

Module: lists

Name: get_unique_id/2

Module: b_ast_cleanup

Name: conjunct_predicates/2

Module: bsyntaxtree

Name: disjunct_predicates/2

Module: bsyntaxtree

Name: create_typed_id/3

Module: bsyntaxtree

Name: get_texpr_type/2

Module: bsyntaxtree

Name: get_domain_range_for_closure_types/3

Module: closures

Name: membership_test_wf/4

Module: kernel_equality

Name: b_type2_set/2

Module: b_global_sets

Name: rename_bt/3

Module: bsyntaxtree

Name: extract_info/2

Module: bsyntaxtree

Name: extract_info_wo_used_ids/2

Module: bsyntaxtree

Name: extract_info/3

Module: bsyntaxtree

Name: rename_bt/3

Module: bsyntaxtree

Name: replace_id_by_expr/4

Module: bsyntaxtree

Name: couplise_list/2

Module: btypechecker

Name: ord_union/3

Module: ordsets

Name: reverse/2

Module: lists

Name: is_maximal_freetype/1

Module: kernel_freetypes

Name: avl_approximate_size_from_height/2

Module: avl_tools

Name: safe_create_texpr/4

Module: bsyntaxtree

Name: create_texpr/4

Module: bsyntaxtree

Name: conjunct_predicates/2

Module: bsyntaxtree

Name: mark_bexpr_as_symbolic/2

Module: bsyntaxtree

Name: ord_subtract/3

Module: ordsets

Name: last/2

Module: lists

Name: all_elements_of_type_wf/3

Module: b_global_sets

Name: all_elements_of_type_rand_wf/3

Module: b_global_sets

Name: expand_freetype/3

Module: kernel_freetypes

Name: equal_object_wf/4

Module: kernel_objects

Name: element_of_global_set/2

Module: kernel_objects

Name: element_of_global_set_wf/3

Module: kernel_objects

Name: try_get_fd_value_list/4

Module: clpfd_lists

Name: get_fd_value/3

Module: clpfd_lists

Name: in_fd_value_list_wf/4

Module: clpfd_lists

Name: avl_fd_value_check/4

Module: clpfd_lists

Name: catch_and_ignore_clpfd_overflow/2

Module: clpfd_interface

Name: random/3

Module: random

Name: check_element_of_wf/3

Module: kernel_objects

Name: not_element_of_wf/3

Module: kernel_objects

Name: element_of_memoization_closure/6

Module: memoization

Name: set_up_localstate/4

Module: store

Name: not_element_of_global_set/2

Module: kernel_objects

Name: get_global_type_value/3

Module: b_global_sets

Name: not_element_of_memoization_closure/6

Module: memoization

Name: same_length/2

Module: lists

Name: convert_list_into_pairs/2

Module: tools

Name: b_test_boolean_expression/4

Module: b_interpreter

Name: b_not_test_boolean_expression/4

Module: b_interpreter

Name: create_typed_ids/3

Module: bsyntaxtree

Name: is_memoization_closure/4

Module: memoization

Name: get_complete_memoization_expansion/6

Module: memoization

Name: split_names_and_types/3

Module: bsyntaxtree

Name: def_get_texpr_id/2

Module: bsyntaxtree

Name: is_set_value/2

Name: is_custom_explicit_set/1

Name: is_custom_explicit_set/2

Name: is_custom_explicit_set_nonvar/1

Name: equal_explicit_sets_wf/3

Name: not_equal_explicit_sets_wf/3

Name: equality_explicit_sets_wf/4

Name: same_texpr_body/2

Name: same_closure/2

Name: is_empty_explicit_set/1

Name: is_empty_explicit_set_wf/2

Name: is_empty_closure_wf/4

Name: is_non_empty_explicit_set/1

Name: is_non_empty_explicit_set_wf/2

Name: is_non_empty_closure_wf/4

Name: test_empty_explicit_set_wf/3

Name: test_empty_closure_wf/5

Name: is_definitely_maximal_set/1

Name: explicit_set_cardinality/2

Name: explicit_set_cardinality_wf/3

Name: explicit_set_cardinality_for_wf/2

Name: card_for_specific_custom_set/3

Name: card_for_specific_closure/4

Name: efficient_card_for_set/3

Name: quick_custom_explicit_set_approximate_size/2

Name: avl_approximate_size/2

Name: avl_approximate_size/3

Name: is_infinite_explicit_set/1

Name: is_infinite_closure/3

Name: is_infinite_global_set/2

Name: is_simple_infinite_set/1

Name: dont_expand_this_explicit_set/1

Name: dont_expand_this_explicit_set/2

Name: dont_expand_symbolic_explicit_set/1

Name: definitely_expand_this_explicit_set/1

Name: is_infinite_or_very_large_explicit_set/1

Name: is_infinite_or_very_large_explicit_set/2

Name: is_cartesian_product_closure/3

Name: expand_custom_set/2

Name: expand_custom_set_wf/4

Name: try_expand_custom_set/2

Name: try_expand_custom_set_with_catch/3

Name: try_expand_custom_set_wf/4

Name: expand_custom_set_to_list/2

Name: expand_custom_set_to_list/4

Name: expand_custom_set_to_list_wf/5

Name: try_expand_custom_set_to_list_wf/5

Name: expand_custom_set_to_list_no_dups_wf/5

Name: expand_custom_set_to_list_gg/4

Name: try_expand_custom_set_to_list/4

Name: expand_interval_closure_to_avl/3

Name: expand_custom_set_to_list_now/2

Name: expand_closure_to_avl_or_list/6

Name: expand_closure_to_list/7

Name: expand_only_custom_closure_global/4

Name: expand_and_convert_to_avl_set/4

Name: ord_list_to_avlset_direct/3

Name: sorted_ground_normalised_list_to_avlset/3

Name: try_expand_and_convert_to_avl/2

Name: convert_to_avl/2

Name: should_be_converted_to_avl_from_lists/1

Name: should_be_converted_to_avl/1

Name: try_expand_and_convert_to_avl_with_check/3

Name: try_expand_and_convert_to_avl_with_check/4

Name: try_expand_and_convert_to_avl_unless_large_wf/3

Name: try_expand_and_convert_to_avl_if_smaller_than/3

Name: is_small_specific_custom_set/2

Name: quick_propagation_element_information/4

Name: element_of_custom_set/2

Name: element_of_custom_set_wf/3

Name: element_of_closure/5

Name: check_element_of_function_closure/6

Name: not_element_of_custom_set_wf/3

Name: membership_custom_set/3

Name: membership_custom_set_wf/4

Name: membership_avl_set_wf/4

Name: quick_test_avl_membership/3

Name: lazy_check_elements_of_closure/6

Name: is_efficient_custom_set/1

Name: remove_minimum_element_custom_set/3

Name: is_maximal_global_set/1

Name: quick_is_definitely_maximal_set/1

Name: quick_definitely_maximal_set_avl/1

Name: is_one_element_custom_set/2

Name: singleton_set/2

Name: construct_singleton_avl_set/2

Name: is_one_element_avl/2

Name: construct_one_element_custom_set/2

Name: avl_is_interval/3

Name: closure1_for_explicit_set/2

Name: closure1_for_explicit_set_from/3

Name: check_in_domain_of_avlset/2

Name: check_unique_in_domain_of_avlset/2

Name: domain_of_explicit_set_wf/3

Name: range_of_explicit_set_wf/3

Name: is_avl_partial_function/1

Name: is_not_avl_partial_function/2

Name: is_avl_total_function_over_domain/2

Name: quick_definitely_maximal_total_function_avl/1

Name: is_avl_relation/1

Name: is_avl_relation_over_domain/3

Name: is_avl_relation_over_range/3

Name: is_not_avl_relation_over_domain_range/4

Name: is_not_avl_relation_over_range/3

Name: is_avl_sequence/1

Name: safe_is_avl_sequence/1

Name: get_avl_sequence/2

Name: is_injective_avl_relation/2

Name: invert_explicit_set/2

Name: union_of_explicit_set/3

Name: union_generalized_explicit_set/3

Name: difference_of_explicit_set_wf/4

Name: intersection_of_explicit_set_wf/4

Name: intersection_with_interval_closure/3

Name: disjoint_intervals_with_inf/4

Name: image_for_id_closure/3

Name: image_for_explicit_set/4

Name: rel_composition_for_explicit_set/3

Name: element_can_be_added_or_removed_to_avl/1

Name: add_element_to_explicit_set_wf/4

Name: remove_element_from_explicit_set/3

Name: delete_element_from_explicit_set/3

Name: at_most_one_match_possible/3

Name: apply_to_avl_set/5

Name: try_apply_to_avl_set/3

Name: min_of_explicit_set_wf/3

Name: max_of_explicit_set_wf/3

Name: sum_or_mul_of_explicit_set/3

Name: domain_restriction_explicit_set_wf/4

Name: range_restriction_explicit_set_wf/4

Name: domain_subtraction_explicit_set_wf/4

Name: range_subtraction_explicit_set_wf/4

Name: override_pair_explicit_set/4

Name: direct_product_explicit_set/3

Name: override_custom_explicit_set_wf/4

Name: symbolic_functionality_check_closure/2

Name: symbolic_injectivity_check_closure/2

Name: subset_of_explicit_set/4

Name: not_subset_of_explicit_set/4

Name: test_subset_of_explicit_set/5

Name: conc_custom_explicit_set/2

Name: prefix_of_custom_explicit_set/4

Name: suffix_of_custom_explicit_set/4

Name: concat_custom_explicit_set/4

Name: prepend_custom_explicit_set/3

Name: append_custom_explicit_set/4

Name: tail_sequence_custom_explicit_set/5

Name: last_sequence_explicit_set/2

Name: front_sequence_custom_explicit_set/3

Name: reverse_custom_explicit_set/2

Name: size_of_custom_explicit_set/3

Name: get_first_avl_elements/4

Name: construct_avl_from_lists/2

Name: construct_avl_from_lists_wf/3

Name: equal_avl_tree/2

Name: check_avl_in_interval/3

Name: check_interval_in_custom_set/4

Name: check_avl_subset/2

Name: construct_closure/4

Name: is_closure/4

Name: construct_member_closure/5

Name: construct_interval_closure/3

Name: is_interval_closure/3

Name: is_interval_closure/5

Name: is_interval_closure_or_integerset/3

Name: is_interval_with_integer_bounds/3

Name: is_powerset_closure/3

Name: dom_range_for_specific_closure/5

Name: dom_for_specific_closure/4

Name: dom_for_lambda_closure/2

Name: portray_custom_explicit_set/1

Name: closure_occurs_check/4

Predicates

Predicates:

add_closure_warning_wf/6

add_element_to_explicit_set_wf/4

add_ground_element_to_explicit_set_wf/4

add_recursive_parameter/9

all_image_pairs_ground/4

all_images/3

allow_expansion/2

append_custom_explicit_set/4

apply_check_tuple/5

apply_check_tuple_delay/9

apply_to_avl_set/5

apply_to_avl_set_aux/6

at_least_two_vars/3

at_most_one_match_possible/3

avl_approximate_size/2

avl_approximate_size/3

avl_domain_subtraction_singleton/3

avl_equal_to_interval/3

avl_equality_to_interval/5

avl_fetch_indexed/4

avl_height_less_than_with_solver_strength/2

avl_integer_set/1

avl_is_interval/3

avl_mem_construct/2

avl_member_blocking/2

avl_member_blocking4/4

avl_member_blocking_aux/5

avl_member_opt/2

avl_member_pair_arg1_ground/3

avl_not_equal_to_interval/4

avl_size_possible/2

avl_to_list_dcg/3

avl_to_list_dcg_offset/5

b_not_test_closure_enum/6

b_not_test_closure_enum_aux/4

b_not_test_closure_wf/5

b_test_closure/6

b_test_closure_wo_enum/5

basic_type_list_cardinality/2

block_card_of_interval_inf/3

block_closure_membership_ground_wf_aux/6

block_compare/5

block_compare_atomic/3

block_compare_aux/6

block_copy_waitflag_store/5

block_couple_element_of_avl_set_grX_grY_wf1/8

block_couple_element_of_avl_set_grX_wf1/7

blocking_normalised_list_to_avl/3

blocking_safe_mul/3

blocking_safe_mul2/3

blocking_safe_pow2/2

calc_direct_product/5

call_card_for_relations/3

card_for_member_closure/4

card_for_specific_closure/3

card_for_specific_closure/4

card_for_specific_closure2/5

card_for_specific_closure3/6

card_for_specific_custom_set/3

card_of_interval_inf/3

check_avl_in_interval/3

check_avl_not_in_interval/3

check_avl_not_in_interval4/4

check_avl_subset/2

check_avl_subset_loop/4

check_dups/3

check_element_of_function_closure/6

check_in_domain_of_avlset/2

check_interval_in_custom_set/4

check_interval_in_custom_set_aux/5

check_list/2

check_sorted/2

check_sorted2/3

check_unique_in_domain_of_avlset/2

closure1_for_explicit_set/2

closure1_for_explicit_set_direct/2

closure1_for_explicit_set_from/3

closure_cardinality/5

closure_cardinality2/5

closure_membership_ground_wf/4

closure_membership_ground_wf_aux/4

closure_membership_wf/6

closure_not_member/5

closure_occurs_check/4

conc_custom_explicit_set/2

concat_custom_explicit_set/4

cond_assign_eq_obj_wf/5

construct_avl_from_lists/2

construct_avl_from_lists_wf/3

construct_avl_set/2

construct_complement_closure_if_necessary/3

construct_disjunct/3

construct_interval_closure/3

construct_interval_list/3

construct_interval_ord_list/3

construct_interval_set/3

construct_one_element_custom_set/2

construct_singleton_avl_set/2

conv2/4

convert_cons_to_avl_inside_set_wf/4

convert_fields/2

convert_sol_list_into_pairs/3

convert_to_avl/2

convert_to_avl_inside_set/2

convert_to_avl_inside_set_wf/3

convert_to_avl_wf/3

convert_value_or_field/2

copy_field_names/2

copy_identifier_infos/3

copy_to_true_list/3

couple_element_of_avl_set/6

couple_prj1_in_range/4

create_couple_term/3

create_renaming/3

cs_greater_than_equal/2

dec/2

decompose_avl_set_into_cartesian_product_wf/4

decompose_cart/5

decompose_value_into_cartesian_product/3

definitely_expand/2

definitely_expand_this_explicit_set/1

delete_element_from_explicit_set/3

delta_witness/3

diff1/4

diff2/3

difference_interval/6

difference_of_explicit_set/3

difference_of_explicit_set2/6

difference_of_explicit_set3/3

difference_of_explicit_set_wf/4

difference_with_avl/5

direct_product3/3

direct_product_explicit_set/3

direct_product_explicit_set_aux/3

direct_remove_element_from_avl/3

disjoint_intervals_with_inf/4

do_not_convert_aux/1

does_not_contain_closure/1

does_not_contain_closure_fields/1

dom_for_lambda_closure/2

dom_for_specific_closure/4

dom_for_specific_closure_aux/6

dom_range_for_member_closure/5

dom_range_for_specific_closure/5

dom_range_for_specific_closure2/7

dom_symbolic/2

domain_aux/5

domain_blocking_aux/3

domain_of_avl_set/2

domain_of_explicit_set_wf/3

domain_of_list_blocking/2

domain_of_sorted_list/3

domain_restrict_singleton_element/3

domain_restriction_explicit_set_wf/4

domain_subtraction_explicit_set_wf/4

dont_expand_symbolic_explicit_set/1

dont_expand_this_closure/3

dont_expand_this_closure/4

dont_expand_this_explicit_set/1

dont_expand_this_explicit_set/2

efficient_card_for_set/3

element_can_be_added_or_removed_to_avl/1

element_of_avl_set_wf/3

element_of_avl_set_wf/4

element_of_avl_set_wf3/5

element_of_closure/5

element_of_custom_set/2

element_of_custom_set2/2

element_of_custom_set_wf/3

element_of_custom_set_wf2/3

element_of_normal_closure/5

element_of_special_closure/6

equal_avl_tree/2

equal_cartesian_product_wf/5

equal_expansions/5

equal_expansions2/5

equal_expansions3/4

equal_explicit_sets4/4

equal_explicit_sets_wf/3

equality_cart_product2/7

equality_cartesian_product_wf/6

equality_explicit_sets_wf/4

evaluate_result_expr/6

exists_should_be_lifted/4

expand_and_convert_to_avl_set/4

expand_and_convert_to_avl_set_unless_very_large/3

expand_closure_to_avl_or_list/6

expand_closure_to_avl_wf/5

expand_closure_to_list/7

expand_custom_set/2

expand_custom_set/3

expand_custom_set_to_list/2

expand_custom_set_to_list/4

expand_custom_set_to_list2/6

expand_custom_set_to_list3/5

expand_custom_set_to_list_gg/4

expand_custom_set_to_list_k_wf/6

expand_custom_set_to_list_no_dups_wf/5

expand_custom_set_to_list_now/2

expand_custom_set_to_list_wf/5

expand_custom_set_to_sorted_list/5

expand_custom_set_wf/4

expand_if_avl/5

expand_interval_closure_to_avl/3

expand_interval_closure_to_list/4

expand_normal_closure/7

expand_normal_closure2/7

expand_normal_closure_direct/6

expand_normal_closure_memo/7

expand_only_custom_closure_global/4

expand_pair_closure/6

explicit_set_cardinality/2

explicit_set_cardinality_for_wf/2

explicit_set_cardinality_wf/3

explicit_tvalue/1

explicit_value/1

expression_contains_setvar/2

expression_contains_setvar_aux/2

fetch/5

filter_start_relation/3

finish_restriction/3

force_comp/3

front_sequence_custom_explicit_set/3

gen_typed_ids/3

generate_couple_types/3

generate_renaming_list/3

generate_typed_id_pairs/3

geq_inf/2

get_avl_sequence/2

get_avl_sequence_dcg/3

get_avl_sets/4

get_bounds2/6

get_card_for_specific_custom_set/2

get_closure/4

get_dom_couple_aux/6

get_domain_id_or_expr/4

get_field_cardinality/2

get_field_val/2

get_field_val_type/3

get_fields_template/3

get_first_avl_elements/4

get_first_els/5

get_fresh_id/4

get_geq_leq_bounds/4

get_identity_as_equivalence/4

get_identity_as_equivalence_aux/3

get_integer_set_interval/3

get_inversion_penalty/1

get_min_max_card/3

get_next_mapped_to/4

get_next_mapped_to_eq/4

get_pos_infos_for_explicit_set/2

get_prj1/2

get_range_id_or_expr/4

get_subset_counter_aux/9

get_subset_counter_example_closure/7

get_template/3

get_template2/3

get_value_bounds/3

get_witness_element/2

ground_element_can_be_added_or_removed_to_avl/1

image_explicit_aux_ground/6

image_explicit_ground/5

image_for_closure/6

image_for_explicit_avl_set/4

image_for_explicit_set/4

image_for_id_closure/3

intersect_avl_interval/4

intersect_intervals_with_inf/6

intersection_of_explicit_set_wf/4

intersection_with_interval_closure/3

intersection_with_interval_closure_aux/4

interval_image_for_explicit_avl_set/5

interval_in_avl_block/4

interval_in_avl_loop/4

inv/3

inv_and_norm/2

inverse_apply_ok/4

inverse_get_possible_values/4

invert_explicit_set/2

invert_member_predicate/4

is_a_relation/7

is_avl_fd_index_set/2

is_avl_inj_list/3

is_avl_partial_function/1

is_avl_partial_function2/3

is_avl_relation/1

is_avl_relation_over_domain/3

is_avl_relation_over_domain2/3

is_avl_relation_over_range/3

is_avl_relation_over_range2/3

is_avl_total_function_over_domain/2

is_cartesian_product_closure/3

is_cartesian_product_closure_aux/5

is_closure1_value_closure/4

is_converted_lambda_closure/3

is_custom_explicit_set/1

is_custom_explicit_set/2

is_custom_explicit_set_nonvar/1

is_definitely_finite/1

is_definitely_maximal_closure/3

is_definitely_maximal_list/2

is_definitely_maximal_set/1

is_definitely_maximal_set2/1

is_definitely_not_empty/1

is_definitely_not_empty_with_witness/2

is_efficient_custom_set/1

is_empty_closure_now/4

is_empty_closure_wf/4

is_empty_explicit_set/1

is_empty_explicit_set_wf/2

is_full_fdlist/3

is_full_fdlist2/3

is_full_powerset_or_relations_or_struct_closure/2

is_full_powset_aux/3

is_geq_leq_interval_closure/5

is_infinite_closure/3

is_infinite_explicit_set/1

is_infinite_global_set/2

is_infinite_or_symbolic_closure/3

is_infinite_or_very_large_closure/4

is_infinite_or_very_large_explicit_set/1

is_infinite_or_very_large_explicit_set/2

is_injective_avl_relation/2

is_interval_closure/3

is_interval_closure/5

is_interval_closure_aux/4

is_interval_closure_body/4

is_interval_closure_or_integerset/3

is_interval_with_integer_bounds/3

is_list/1

is_list_skeleton/1

is_maximal_global_set/1

is_maximal_global_set/2

is_non_empty_closure_wf/4

is_non_empty_explicit_set/1

is_non_empty_explicit_set_wf/2

is_not_avl_partial_function/2

is_not_avl_partial_function2/4

is_not_avl_rel_dom1/7

is_not_avl_rel_dom2/7

is_not_avl_rel_ran2/6

is_not_avl_relation_over_domain_range/4

is_not_avl_relation_over_range/3

is_one_element_avl/2

is_one_element_custom_set/2

is_powerset_closure/3

is_powset_aux/3

is_set_value/2

is_simple_infinite_set/1

is_small_specific_custom_set/2

is_special_closure/4

is_symbolic_closure_or_symbolic_mode/3

is_very_large_maximal_global_set/2

is_very_large_or_symbolic_closure/4

iterate_closure/4

known_length/3

l_card_for_member_closure/4

l_convert_to_avl_wf/3

l_is_definitely_maximal_set/1

last_sequence_explicit_set/2

lazy_check_elements6/6

lazy_check_elements_of_closure/6

length_at_least/2

length_larger_than/2

leq0/2

list_does_not_contain_closure/1

low_border/3

match_key/4

match_possible/3

match_possible_atomic/3

max_of_explicit_set_wf/3

maximum_with_inf/3

maximum_with_inf1/3

membership_avl_set_wf/4

membership_avl_set_wf2/4

membership_custom_set/3

membership_custom_set_wf/4

membership_global_set/4

membership_interval/4

min_of_explicit_set_wf/3

minimum_with_inf/3

minimum_with_inf1/3

must_be_in_domain_check/7

my_avl_member/2

my_length/3

no_conversion_nec_term/1

no_conversion_necessary/1

norm/3

normal_closure_not_member/5

normalise_avl_set/2

normalised_list_to_avl/2

normalised_list_to_avl_when_ground/2

not_check_avl_subset/2

not_element_of_avl_set_block/3

not_element_of_custom_set/2

not_element_of_custom_set_wf/3

not_element_of_custom_set_wf2/3

not_element_of_special_closure/6

not_equal_cartesian_product_wf/5

not_equal_expansions/5

not_equal_explicit_sets_wf/3

not_infinite_bound/1

not_subset_of_explicit_set/4

not_subset_of_explicit_set_aux/4

number_card_of_interval_inf_aux/3

ord_list_to_avlset/2

ord_list_to_avlset/3

ord_list_to_avlset_direct/3

override_custom_explicit_set2/4

override_custom_explicit_set_aux/4

override_custom_explicit_set_wf/4

override_list/4

override_pair_explicit_set/4

portray_custom_explicit_set/1

prefix_of_custom_explicit_set/4

prefix_of_custom_explicit_set2/4

prepend_custom_explicit_set/3

project_avl_domain/2

project_avl_domain_on_fd/2

propagate_apply/9

propagate_atomic_value/2

propagate_avl_el_large_block/4

propagate_avl_element_information/4

propagate_avl_element_information_direct/4

propagate_avl_element_information_large/3

propagate_avl_element_information_small/3

propagate_avl_not_element_information/3

propagate_avl_not_element_information3/3

propagate_closure_body_for_all/6

propagate_closure_body_value_set/6

propagate_fd_dom/2

propagate_fd_membership/3

propagate_not_membership/3

propagate_value/2

quantifier_construct/4

quick_custom_explicit_set_approximate_size/2

quick_definitely_maximal_set_avl/1

quick_definitely_maximal_set_avl_aux/2

quick_definitely_maximal_total_function_avl/1

quick_is_definitely_maximal_set/1

quick_is_definitely_maximal_set_aux/1

quick_non_ground_check/1

quick_propagation_element_information/4

quick_size_check_larger_than/3

quick_test_avl_membership/3

ran_for_specific_closure/3

ran_symbolic/2

ran_symbolic_closure/6

range_of_explicit_set_wf/3

range_restriction_explicit_set_wf/4

range_subtraction_explicit_set_wf/4

reify_avl_mem2/5

reify_avl_membership/4

reify_integer_avl_mem/3

rel_avl_compose2/4

rel_avl_compose2_ground/4

rel_composition_for_explicit_set/3

remove_element_from_explicit_set/3

remove_minimum_element_custom_set/3

remove_minimum_element_custom_set2/4

rename_lambda_result_id/4

rename_ran_ids/5

reset_closure_solution_counter/1

restrict2/7

restrict2_avl/6

restrict3/10

restriction_explicit_set_wf/6

reverse_custom_explicit_set/2

safe_avl_member_block/4

safe_avl_member_default/2

safe_avl_member_default_wf/3

safe_avl_member_pair/3

safe_avl_member_pair_wf/4

safe_dec/2

safe_is_avl_sequence/1

same_closure/2

same_closure_body/6

same_closure_body_with_parameter_renaming/6

same_fields_inside_closure/2

same_quantified_expression/5

same_sub_expressions/3

same_texpr_with_rewrite/3

same_types/2

same_value_inside_closure/2

shift_avl_sequence_to_ord_list/3

shift_seq/3

should_be_converted_to_avl/1

should_be_converted_to_avl_from_lists/1

size_of_avl_sequence/3

size_of_custom_explicit_set/3

small_enough_for_expansion/2

small_interval/2

sort_when_done/4

sorted_ground_normalised_list_to_avlset/3

split_conjunct/5

split_conjunct_aux/6

strict_subset_constructor/2

subset_constructor/3

subset_of_explicit_set/4

suffix_of_custom_explicit_set/4

suffix_of_custom_explicit_set2/4

sum_interval/3

sum_interval_clpfd_prop/3

sum_or_mul_of_explicit_set/3

symbolic_functionality_check_closure/2

symbolic_injectivity_check_closure/2

symbolic_subset_of_explicit_set/5

tail_sequence_custom_explicit_set/5

test_avl_in_interval/5

test_avl_set/1

test_closure/1

test_closure_and_convert/5

test_empty_closure_wf/5

test_empty_closure_wf2/5

test_empty_explicit_set_wf/3

test_subset_of_explicit_set/5

transform_global_set_into_closure_aux/2

transform_global_sets_into_closure/2

try_apply_to_avl_set/3

try_convert_to_avl/2

try_convert_to_avl_wf/3

try_expand_and_convert_to_avl/2

try_expand_and_convert_to_avl/4

try_expand_and_convert_to_avl_if_smaller_than/3

try_expand_and_convert_to_avl_set/3

try_expand_and_convert_to_avl_unless_large_wf/4

try_expand_and_convert_to_avl_unless_large_wf/3

try_expand_and_convert_to_avl_unless_very_large_wf/3

try_expand_and_convert_to_avl_wf/5

try_expand_and_convert_to_avl_with_catch_wf/4

try_expand_and_convert_to_avl_with_check/3

try_expand_and_convert_to_avl_with_check/4

try_expand_custom_set/2

try_expand_custom_set_to_list/4

try_expand_custom_set_to_list_wf/5

try_expand_custom_set_wf/4

try_expand_custom_set_with_catch/3

try_expconv_to_avl_with_size/4

try_get_finite_max_card_from_fields/2

try_get_finite_max_card_from_ground_value/2

unify_after_wf/2

unify_clos_lt/10

unify_closure_predicates/10

union_complement_set/4

union_complement_set2/4

union_generalized_explicit_set/3

union_of_avl/3

union_of_avl1/5

union_of_avl_set/3

union_of_avl_set_with_closure/5

union_of_avl_with_acc/3

union_of_avls/3

union_of_closure/5

union_of_explicit_set/3

union_of_interval/6

unique_id_comparison/2

unique_id_comparison_aux/3

up_border/3

update_closure_solution_counter/2

value_contains_setvar/2

very_approximate_cardinality/3

add_closure_warning_wf/6

add_element_to_explicit_set_wf/4

Description:
was element_can_be_added_or_removed_to_avl(Element),

add_ground_element_to_explicit_set_wf/4

add_recursive_parameter/9

all_image_pairs_ground/4

all_images/3

allow_expansion/2

append_custom_explicit_set/4

apply_check_tuple/5

apply_check_tuple_delay/9

Block: apply_check_tuple_delay(?,?,?,?,?,?,-,-,-)

apply_check_tuple_delay(X,Y,AVL,_ApproxSizeA,Span,WF,GroundX,WF1,_) :-
    (nonvar(GroundX);nonvar(WF1)),!,
    apply_check_tuple(X,Y,AVL,Span,WF).

apply_check_tuple_delay(X,Y,AVL,ApproxSizeA,Span,WF,_GroundX,_WF1,_GroundY) :-
    % Y is ground; try to do an inverse function lookup
    inverse_apply_ok(Y,X,AVL,ApproxSizeA),
    !,
    % print(inverse_apply(Y,X,ApproxSizeA,_GroundX)),nl,
    inverse_get_possible_values(X,Y,AVL,Res),
    Res=avl_set(InvAVL), % if empty set : we fail
    (preference(data_validation_mode,true),
    avl_approximate_size(InvAVL,10,ApproxSize),
    ApproxSize>1
    -> A2 is (ApproxSize*15*ApproxSize)//ApproxSizeA, % used to be A2 is ApproxSize*100,
    A22 is max(A2,ApproxSize),
    (get_inversion_penalty(Span)
    -> A23 is A22 * 100 %, add_message(f,'Inversion Penalty: ',Y:A22,Span)
    ; A23=A22),
    % give lower priority for backwards propagation, upto 15 times if no reduction from backwards propagation
    % but also take into account how much we reduce the size by inverting
    % relevant for, e.g., Machines_perf_0111/Thales_All/rule_OPS_SDS_3940.mch
    % or rule_OPS_SDS_6496 -> 15 instead of 150 improves performance
    get_bounded_wait_flag(A23,element_of_avl_inverse_apply_ok(X),WF,WF2),
    % does not call propagate_avl_element_information(X,InvAVL,ApproxSize,WF) or avl_to_table
    element_of_avl_set_wf3(X,InvAVL,ApproxSize,WF2,WF) % TODO: pass GroundX
    %apply_check_tuple_delay(X,Y,AVL,ApproxSizeA,Span,WF,GroundX,WF1,_) % now wait on WF1 or GroundX
    ; element_of_avl_set_wf(InvAVL,X,WF)
).

apply_check_tuple_delay(X,Y,AVL,ApproxSizeA,Span,WF,GroundX,WF1,_GroundY) :-
    apply_check_tuple_delay(X,Y,AVL,ApproxSizeA,Span,WF,GroundX,WF1,_). % now wait on WF1 or GroundX

apply_to_avl_set/5

apply_to_avl_set_aux/6

apply_to_avl_set_aux(A,X,Y,GroundX,Span,WF) :- nonvar(GroundX),!,
    apply_check_tuple(X,Y,A,Span,WF). % we could call apply_check_tuple_ground to avoid one ground test

apply_to_avl_set_aux(A,X,Y,GroundX,Span,WF) :-
    %(preference(data_validation_mode,true); % we now reduce priority of backpropagation below
    preference(find_abort_values,true),
    % do not try inverse propagation onto argument X of function application A(X) = Y
    !,
    avl_approximate_size(A,3,ApproxSizeA),
    apply_check_tuple_delay(X,Y,A,ApproxSizeA,Span,WF,GroundX,_,_).

apply_to_avl_set_aux(A,X,Y,GroundX,Span,WF) :-
    ground_value_check(Y,GroundY),
    avl_approximate_size(A,3,ApproxSizeA), % exact size for height <= 3; approximate size above
    (ApproxSizeA < 4 -> SPrio=ApproxSizeA ; SPrio is ApproxSizeA * 10), % magic number; ideally we want X or Y to be known beforehand; if none are known we may miss WD errors and may enumerate useless intermediate variables
    get_bounded_wait_flag(SPrio,apply_to_explicit(X,Y),WF,WF1), % this only makes sense if X is a domain variable to be enumerated
    %propagate_avl_element_information((X,Y),A,ApproxSizeA,WF), % could be done; but would prevent WD problems from being detected
    % this waitflag is used when neither X nor Y are ground;
    % quite often not much is gained by enumerating possible values; unless X or Y are constrained or trigger other computations
    % WSz is 10*ApproxSizeA, % magic value
    %(ApproxSizeA > 100 -> InversePrioSize = 4
    % ; avl_range_size_and_propagate_element_info(A,X,Y,RSize), InversePrioSize is ApproxSizeA // RSize), % we could probably compute the exact worst case with the same complexity
    % delay_get_wait_flag(GroundY,GroundX,WF1,InversePrioSize,apply_to_explicit_inverse(X,Y),WF,WF2),
    %(ApproxSizeA<4000 -> propagate_apply(X,Y,A,ApproxSizeA,WF,GroundX,GroundY) ; true),
    apply_check_tuple_delay(X,Y,A,ApproxSizeA,Span,WF,GroundX,WF1,GroundY),
    (preference(use_clpfd_solver,false) -> true
    % should we also check: preference(find_abort_values,true)?
    ; get_wait_flag0(WF,WF0),
    propagate_apply(X,Y,A,ApproxSizeA,WF,WF0,GroundX,WF1,GroundY)).

at_least_two_vars/3

at_most_one_match_possible/3

avl_approximate_size/2

avl_approximate_size/3

avl_domain_subtraction_singleton/3

avl_equal_to_interval/3

avl_equality_to_interval/5

avl_fetch_indexed/4

avl_height_less_than_with_solver_strength/2

avl_integer_set/1

avl_is_interval/3

avl_mem_construct/2

avl_member_blocking/2

avl_member_blocking4/4

avl_member_blocking_aux/5

Block: avl_member_blocking_aux(-,?,?,?,?)

avl_member_opt/2

avl_member_pair_arg1_ground/3

avl_not_equal_to_interval/4

avl_size_possible/2

avl_to_list_dcg/3

avl_to_list_dcg_offset/5

b_not_test_closure_enum/6

Block: b_not_test_closure_enum(-,?,?,?,?,?)

b_not_test_closure_enum_aux/4

Block: b_not_test_closure_enum_aux(-,-,?,?)

b_not_test_closure_wf/5

Block: b_not_test_closure_wf(?,?,?,-,?)

b_test_closure/6

Block: b_test_closure(?,?,-,?,?,?)

b_test_closure(Parameters,ParameterTypes,ClosureBody, FullParValues, NegationContext, OuterWF) :-
    (preference(data_validation_mode,true)
    -> true % avoids ineraction between domain and range expression enumeration; see
    % private_examples/ClearSy/2019_May/perf_3264/rule_186.mch or
    % computation of 631 ic___DMI_MRGATKSAAT___Parametre_Identifiant_indices_function in rule_FICHIER_MRGATKSAATPAR_RVF219_MRGA_DE.mch
    % however, as b_optimize below does *not* evaluate nested set comprehensions, there can be a slowdown:
    % the nested set comprehension gets re-evaluated for every soluiton of the lambda parameters !
    % this was the case of private_examples/ClearSy/2019_Nov/rule_Regle_31C_0005/rule.mch before using SORT
    ; \+ preferences:preference(use_smt_mode,false)), % TO DO: enable in normal mode when performance of 1336 fixed
    % print(test_closure(Parameters,FullParValues)),nl,
    is_lambda_closure(Parameters,ParameterTypes,ClosureBody, OtherIDs,OtherTypes, DomainPred, EXPR),
    % TO DO: detect not only equalities at end, but any equality which is irrelevant for the rest
    % nl,print(lambda_closure(OtherIDs)),nl, translate:print_bexpr(EXPR),nl,
    append(ParValues,[LambdaResult],FullParValues),
    !,
    get_texpr_info(ClosureBody,BInfo),
    b_interpreter:set_up_typed_localstate2(OtherIDs,OtherTypes,BInfo,ParValues,TypedVals,[],LocalState,NegationContext),
    simplify_span(ClosureBody,BSpan), % sometimes BInfo no longer contains a position info, but first_sub_expr does
    init_quantifier_wait_flag(OuterWF,comprehension_set(NegationContext),OtherIDs,ParValues,BSpan,WF),
    b_test_boolean_expression(DomainPred,LocalState,[],WF),
    %print('PRED: '),translate:print_bexpr(ClosureBody),nl,
    b_tighter_enumerate_values_in_ctxt(TypedVals,DomainPred,WF), % also does: project_away_useless_enumeration_values
    init_quantifier_wait_flag(OuterWF,comprehension_set(NegationContext),OtherIDs,ParValues,BSpan,WF2),
    b_compiler:b_optimize(EXPR,[],LocalState,[],CEXPR,WF), % already pre-compile lookup, without constraint processing; is not sufficient for test 1336
    ground_wait_flags(WF), % TODO: also call ground inner WF in context
    b_interpreter:b_compute_expression(CEXPR,LocalState,[],LambdaResult,WF2),
    ground_inner_wait_flags_in_context(NegationContext,WF2).

b_test_closure(Parameters,ParameterTypes,ClosureBody,ParValues,NegationContext, OuterWF) :-
    % tools:print_bt_message(b_test_closure_testing_closure(Parameters,ParValues)),
    get_texpr_info(ClosureBody,BInfo),
    b_interpreter:set_up_typed_localstate2(Parameters,ParameterTypes,BInfo,
    ParValues,TypedVals,[],LocalState,NegationContext),
    % print_message(b_interpreter:b_test_boolean_expression(ClosureBody,LocalState,[],WF)),
    simplify_span(ClosureBody,BSpan), % sometimes BInfo no longer contains a position info, but first_sub_expr does
    init_quantifier_wait_flag(OuterWF,comprehension_set(NegationContext),Parameters,ParValues,BSpan,WF),
    %external_functions:observe_parameters(Parameters,LocalState),
    b_test_boolean_expression(ClosureBody,LocalState,[],WF),
    % tools:print_bt_message(tested_bool_expr), translate:print_bexpr(ClosureBody),nl,
    b_enumerate:b_tighter_enumerate_values_in_ctxt(TypedVals,ClosureBody,WF), % also detects useless enumeration ids
    ground_inner_wait_flags_in_context(NegationContext,WF).

b_test_closure_wo_enum/5

Block: b_test_closure_wo_enum(?,?,-,?,?)

basic_type_list_cardinality/2

block_card_of_interval_inf/3

Block: block_card_of_interval_inf(-,?,-) block_card_of_interval_inf(?,-,-)

block_closure_membership_ground_wf_aux/6

Block: block_closure_membership_ground_wf_aux(?,?,?,?,-,?) block_closure_membership_ground_wf_aux(?,?,-,-,?,?)

block_compare/5

Block: block_compare(-,?,?,?,?) block_compare(?,-,?,?,?)

block_compare_atomic/3

Block: block_compare_atomic(-,?,?) block_compare_atomic(?,-,?)

block_compare_aux/6

Block: block_compare_aux(-,?,?,?,?,?)

block_copy_waitflag_store/5

Block: block_copy_waitflag_store(?,?,-,-,-)

block_couple_element_of_avl_set_grX_grY_wf1/8

Block: block_couple_element_of_avl_set_grX_grY_wf1(?,?,?,?,-,-,-,?)

block_couple_element_of_avl_set_grX_wf1/7

Block: block_couple_element_of_avl_set_grX_wf1(?,-,?,?,-,-,?)

blocking_normalised_list_to_avl/3

Block: blocking_normalised_list_to_avl(-,?,?)

blocking_safe_mul/3

Block: blocking_safe_mul(-,-,?)

blocking_safe_mul2/3

Block: blocking_safe_mul2(-,?,?) blocking_safe_mul2(?,-,?)

blocking_safe_pow2/2

Block: blocking_safe_pow2(-,?)

calc_direct_product/5

call_card_for_relations/3

Meta: call_card_for_relations(-,-,0)

Block: call_card_for_relations(-,?,?) call_card_for_relations(?,-,?)

card_for_member_closure/4

card_for_member_closure(parallel_product(b(value(A1),ST1,_),b(value(A2),ST1,_)),_T,Card,CodeToComputeCard) :- !,
    nonvar(A1), nonvar(A2),
    efficient_card_for_set(A1,Card1,Code1),
    CodeToComputeCard = (Code1,Code2, custom_explicit_sets:blocking_safe_mul(Card1,Card2,Card)),
    % cardinality computed like for cartesian_product.
    efficient_card_for_set(A2,Card2,Code2).

card_for_member_closure(seq(b(value(SET1),ST1,_)),_SEQT,Card,CodeToComputeCard) :- !, /* _SEQT=seq(T1) */
    is_set_type(ST1,_T1),
    CodeToComputeCard = custom_explicit_sets:seq_card(SET1,Card).

card_for_member_closure(seq1(b(value(SET1),ST1,_)),_SEQT,Card,CodeToComputeCard) :- !, /* _SEQT=seq1(T1) */
    is_set_type(ST1,_T1),
    CodeToComputeCard = custom_explicit_sets:seq1_card(SET1,Card).

card_for_member_closure(perm(b(value(SET1),ST1,_)),_SEQT,Card,CodeToComputeCard) :- !, /* _SEQT=perm(T1) */
    is_set_type(ST1,_T1),
    CodeToComputeCard = (kernel_objects:cardinality_as_int(SET1,int(SCard)),
    custom_explicit_sets:blocking_factorial(SCard,Card)).

card_for_member_closure(iseq(b(value(SET1),ST1,_)),_SEQT,Card,CodeToComputeCard) :- !, /* _SEQT=iseq(T1) */
    is_set_type(ST1,_T1),
    CodeToComputeCard = (kernel_objects:cardinality_as_int(SET1,int(SCard)),
    kernel_card_arithmetic:blocking_nr_iseq(SCard,Card)).

card_for_member_closure(iseq1(b(value(SET1),ST1,_)),_SEQT,Card,CodeToComputeCard) :- !, /* _SEQT=iseq1(T1) */
    is_set_type(ST1,_T1),
    CodeToComputeCard = (kernel_objects:cardinality_as_int(SET1,int(SCard)),
    kernel_card_arithmetic:blocking_nr_iseq1(SCard,Card)).

card_for_member_closure(identity(b(value(SET1),ST1,_)),_SEQT,Card,CodeToComputeCard) :- !, /* _SEQT=id(T1) */
    is_set_type(ST1,_T1),
    CodeToComputeCard =
    kernel_objects:cardinality_as_int(SET1,int(Card)).

card_for_member_closure(struct(b(RecVal,record(_FieldSetTypes),_)), record(_FieldTypes), % set of records
    Card,CodeToComputeCard) :-
    !,
    (RecVal=value(RECF), nonvar(RECF), RECF=rec(FIELDS) % value has been computed:
    -> CodeToComputeCard = custom_explicit_sets:get_field_cardinality(FIELDS,Card)
    ; RecVal = rec(TypedFields), % we still have a typed AST
    maplist(get_field_val_type,TypedFields,Exprs,Types),
    l_card_for_member_closure(Exprs,Types,Card, CodeToComputeCard)
).

card_for_member_closure(POW,TYPE, Card,CodeToComputeCard) :-
    (POW = pow_subset(b(value(SET),TYPE,_)) ;
    POW = fin_subset(b(value(SET),TYPE,_))),!,
    CodeToComputeCard =
    (kernel_objects:cardinality_as_int(SET,int(SCard)),
    custom_explicit_sets:blocking_safe_pow2(SCard,Card)
).

card_for_member_closure(POW,TYPE, Card,CodeToComputeCard) :-
    (POW = pow1_subset(b(value(SET),TYPE,_)) ;
    POW = fin1_subset(b(value(SET),TYPE,_))),!,
    CodeToComputeCard =
    (kernel_objects:cardinality_as_int(SET,int(SCard)),
    custom_explicit_sets:blocking_safe_pow2(SCard,C1),
    custom_explicit_sets:safe_dec(C1,Card)
).

card_for_member_closure(RELEXPR,SType, Card,CodeToComputeCard) :-
    is_set_type(SType,couple(T1,T2)),
    is_a_relation(RELEXPR, b(value(DOM),set(T1),_),
    b(value(RAN),set(T2),_), DCard,RCard,Card,RELCODE),!,
    CodeToComputeCard =
    (
    kernel_objects:cardinality_as_int(DOM,int(DCard)),
    kernel_objects:cardinality_as_int(RAN,int(RCard)),
    custom_explicit_sets:call_card_for_relations(DCard,RCard,RELCODE)
).

card_for_member_closure(BODY, integer, Card,CodeToComputeCard) :-
    is_interval_with_integer_bounds(BODY,Low,Up),!,
    CodeToComputeCard = custom_explicit_sets:card_of_interval_inf(Low,Up,Card).

card_for_member_closure(value(Value), _Type, Card,CodeToComputeCard) :-
    % we have a closure of the type {x|x:S}; equivalent to S
    (nonvar(Value),
    Value=closure(P,T,B)
    -> % cardinality_as_int may expand it ! is bad if e.g. we called this code to check if a closure is infinite
    card_for_specific_closure2(P,T,B,Card,CodeToComputeCard) % will not expand, but fail if cannot be computed
    % TO DO: provide an argument: precise_or_efficient
    ; CodeToComputeCard = kernel_objects:cardinality_as_int(Value,int(Card))
).

card_for_specific_closure/3

card_for_specific_closure/4

card_for_specific_closure2/5

card_for_specific_closure3/6

card_for_specific_custom_set/3

card_of_interval_inf/3

check_avl_in_interval/3

check_avl_not_in_interval/3

Block: check_avl_not_in_interval(?,-,?)

check_avl_not_in_interval4/4

check_avl_subset/2

check_avl_subset_loop/4

check_dups/3

Block: check_dups(-,?,?)

check_element_of_function_closure/6

check_element_of_function_closure(X,Y,Parameters,PT,CondClosure,WF) :-
    is_special_closure(Parameters,PT,CondClosure, SpecialClosure),!, % this covers recursive closures
    element_of_special_closure(SpecialClosure,(X,Y),WF,Parameters,PT,CondClosure).

check_element_of_function_closure(X,Y, P,T,ClosureBody, WF) :-
    % affects test 1312, unless we add s:seq(0..9) before calling num
    % a special rule which tries and avoid enumerating solutions to arguments of function application
    % usually a function application will either be given all arguments or maybe be used in inverse
    is_converted_lambda_closure(P,T,ClosureBody), %is_converted_non_recursive_lambda_closure(P,T,ClosureBody),
    % TO DO: also make this work for recursive closures by adding recursive args (see e.g. test 1302)
    is_lambda_closure(P,T,ClosureBody, OtherIDs, OtherTypes, DomainPred, EXPR),
    (debug:debug_level_active_for(4) ->
    print('Apply Fun : '), translate:print_bexpr(DomainPred), print(' | '), translate:print_bexpr(EXPR),nl,
    get_texpr_info(ClosureBody,I), print(info(I,WF)),nl,
    print_term_summary((X,Y)),nl %,trace
    ; true),
    !,
    % alternative: annotate X,Y as inner variable ?
    get_texpr_info(ClosureBody,BInfo),
    b_interpreter:set_up_typed_localstate2(OtherIDs,OtherTypes,BInfo,ParValues,_TypedVals,[],LocalState,positive),
    convert_list_into_pairs(ParValues,SingleParValue),
    kernel_objects:equal_object_wf(X,SingleParValue,check_element_of_function_closure,WF),
    (is_truth(DomainPred) -> true
    ; init_wait_flags(InnerWF,[check_element_of_function_closure]),
    %copy_wf01e_wait_flags(WF,InnerWF), % we could delay copying WF0 until after test_boolean_expression of DomainPred ?
    b_test_boolean_expression(DomainPred,LocalState,[],InnerWF),
    get_wait_flag0(WF,WF0), get_wait_flag0(InnerWF,WF0), % was: ground_wait_flag0(InnerWF), but this can result in inner WF0 being set when outer is not yet set; see test 1948
    ground_value_check(X,GrX),
    (nonvar(GrX) -> copy_waitflag_store(InnerWF,WF) % block would trigger already
    ; ground_value_check(Y,GrY),
    (nonvar(GrY) -> copy_waitflag_store(InnerWF,WF) % block would trigger already
    ; get_last_wait_flag(check_element_of_function_closure(OtherIDs),WF,LastWF),
    block_copy_waitflag_store(InnerWF,WF,GrX,GrY,LastWF)
    )
    )
    ),
    b_interpreter:b_compute_expression(EXPR,LocalState,[],Y,WF).

check_element_of_function_closure(X,Y, P,T,ClosureBody, WF) :-
    element_of_normal_closure((X,Y),P,T,ClosureBody,WF).

check_in_domain_of_avlset/2

check_interval_in_custom_set/4

check_interval_in_custom_set_aux/5

Block: check_interval_in_custom_set_aux(-,?,?,?,-)

check_list/2

check_sorted/2

check_sorted2/3

check_unique_in_domain_of_avlset/2

closure1_for_explicit_set/2

closure1_for_explicit_set_direct/2

closure1_for_explicit_set_from/3

closure_cardinality/5

closure_cardinality2/5

closure_membership_ground_wf/4

closure_membership_ground_wf_aux/4

closure_membership_wf/6

closure_membership_wf(X,[ZZZZ],[integer],CondClosure,Res,_WF) :-
    is_interval_closure_body(CondClosure,ZZZZ,LOW,UP),!,
    kernel_equality:in_nat_range_test(X,int(LOW),int(UP),Res).

closure_membership_wf(X,Par,Types,Body,Res,WF) :-
    is_member_closure(Par,Types,Body,_Type,VAL),
    (VAL=value(_) ; VAL = cartesian_product(b(value(A),_,_),b(value(B),_,_))),!,
    (VAL=value(Set)
    -> kernel_objects:membership_test_wf(Set,X,Res,WF)
    ; kernel_equality:cartesian_pair_test_wf(X,A,B,Res,WF)).

closure_membership_wf(X,Par,Typ,Body,Res,WF) :-
    is_not_member_closure(Par,Typ,Body,_Type,value(Set)),!,
    bool_pred:negate(ResXSet,Res), % was kernel_equality:inv_mem_obj(ResXSet,Res),
    kernel_objects:membership_test_wf(Set,X,ResXSet,WF).

closure_membership_wf(X,Par,Types,Body,Res,WF) :- ground_value(X),!,
    closure_membership_ground_wf(X,closure(Par,Types,Body),Res,WF).

closure_membership_wf(X,Par,Types,Body,Res,WF) :-
    CS = closure(Par,Types,Body),
    is_small_specific_custom_set(CS,100),
    try_expand_and_convert_to_avl_wf(CS,Expanded,closure_membership_wf,'',WF),
    nonvar(Expanded), Expanded=avl_set(_),
    !,
    membership_custom_set_wf(Expanded,X,Res,WF).

closure_membership_wf(X,Par,Types,Body,Res,WF) :-
    Body \= b(member(_,_),_,_), % otherwise we may have an infinite loop; b_check_boolean_expression will generate a closure which will call closure_membership_wf again; TO DO: refine to allow certain memberships to go through
    get_texpr_info(Body,BodyInfo),
    \+ member(prob_annotation(recursive(_RID)),BodyInfo), % otherwise we can get errors as recursive identifier _RID needs to be added to local state ! (test 1151 fails otherwise)
    % TO DO: add recursive parameter below in set_up_typed_localstate2; + in which other circumstances do we need to set up recursion identifier !
    % Try reifiyng the body
    NegationContext=positive,
    copy_wf_start(WF,closure_membership_wf,CWF),
    b_interpreter:set_up_typed_localstate2(Par,Types,BodyInfo,ParValues,TypedVals,[],State,NegationContext),
    %couplise_list(Types,XType),
    convert_list_into_pairs(ParValues,SingleParValue),
    kernel_objects:equal_object(X,SingleParValue,closure_membership_wf),
    b_interpreter_check:b_check_boolean_expression(Body,[],State,CWF,PredRes),
    !,
    (debug_mode(on) -> print('REIFICATION of closure: '), translate:print_bexpr(Body),nl, print(pred_res(X,PredRes)),nl ; true),
    b_enumerate:b_tighter_enumerate_all_values(TypedVals,WF), % not necessary ?? as X should get enumerated
    Res=PredRes,
    copy_wf_finish(WF,CWF).

closure_membership_wf(X,Par,Types,Body,Res,WF) :-
    when( (ground(X);nonvar(Res)),
    % used to be ground(X), % with (ground(X);nonvar(Res)), test 292 failed {x,t|t : BOOL & (x : POW(1024 .. 1025) & bool(x : POW(NATURAL1)) = t)} = {{} |-> TRUE,{1024} |-> TRUE,{1024,1025} |-> TRUE,{1025} |-> TRUE} and test 1088 failed
    closure_membership_ground_wf(X,closure(Par,Types,Body),Res,WF)).

closure_not_member/5

Block: closure_not_member(?,-,?,?,?)

closure_occurs_check/4

conc_custom_explicit_set/2

concat_custom_explicit_set/4

cond_assign_eq_obj_wf/5

Block: cond_assign_eq_obj_wf(-,?,?,?,?)

construct_avl_from_lists/2

construct_avl_from_lists_wf/3

construct_avl_set/2

construct_complement_closure_if_necessary/3

Block: construct_complement_closure_if_necessary(-,?,?)

construct_disjunct/3

construct_interval_closure/3

construct_interval_list/3

construct_interval_ord_list/3

construct_interval_set/3

construct_one_element_custom_set/2

construct_singleton_avl_set/2

conv2/4

convert_cons_to_avl_inside_set_wf/4

convert_fields/2

convert_sol_list_into_pairs/3

convert_to_avl/2

convert_to_avl_inside_set/2

convert_to_avl_inside_set_wf/3

convert_to_avl_wf/3

convert_value_or_field/2

copy_field_names/2

copy_identifier_infos/3

copy_to_true_list/3

Block: copy_to_true_list(-,?,?)

couple_element_of_avl_set/6

couple_prj1_in_range/4

create_couple_term/3

create_renaming/3

cs_greater_than_equal/2

dec/2

decompose_avl_set_into_cartesian_product_wf/4

decompose_cart/5

decompose_value_into_cartesian_product/3

definitely_expand/2

definitely_expand_this_explicit_set/1

delete_element_from_explicit_set/3

delta_witness/3

diff1/4

diff2/3

difference_interval/6

difference_of_explicit_set/3

difference_of_explicit_set2/6

Block: difference_of_explicit_set2(?,?,?,?,?,-)

difference_of_explicit_set3/3

difference_of_explicit_set_wf/4

difference_of_explicit_set_wf(_S1,S2,R,_) :-
    is_definitely_maximal_set(S2), !, R=[].

difference_of_explicit_set_wf(S1,S2,R,_) :- nonvar(S2), S2=[],!, R=S1.

difference_of_explicit_set_wf(S1,S2,R,_) :-
    %nonvar(S1),
    is_very_large_maximal_global_set(S1,Type), !, % TO DO: also for freetype ? cartesian products,...
    /* we have a complement-set */
    complement_set(S2,Type,R).

difference_of_explicit_set_wf(S1,S2,Result,_) :-
    is_not_member_value_closure(S1,Type,MS1),
    nonvar(MS1), is_custom_explicit_set(MS1,difference_of_explicit_set_wf),!,
    union_complement_set(MS1,S2,Type,Result).

difference_of_explicit_set_wf(_,S2,_,_) :- var(S2), !, fail. % then we cannot do anything below

difference_of_explicit_set_wf(S1,S2,R,WF) :-
    is_not_member_value_closure(S2,_Type,MS2), nonvar(MS2),
    intersection_of_explicit_set_wf(MS2,S1,R,WF),!.

difference_of_explicit_set_wf(I1,I2,R,_) :-
    is_interval_closure_or_integerset(I1,From1,To1),
    is_interval_closure_or_integerset(I2,From2,To2),
    difference_interval(From1,To1,From2,To2,FromRes,ToRes),
    % TO DO: also treat case when difference yields two disjoint intervals
    % i.e., do not fail and forget info about interval bounds in case we cannot compute difference as a an interval, e.g., INT - {0}
    !,
    construct_interval_closure(FromRes,ToRes,R).

difference_of_explicit_set_wf(avl_set(A1),S2,R,WF) :-
    (S2=avl_set(A2) ;
    ground_value(S2), expand_and_convert_to_avl_set_unless_very_large(S2,A2,WF)),!,
    avl_height(A2,H2),
    %avl_min(A1,Min1),avl_max(A1,Max1), avl_min(A2,Min2),avl_max(A2,Max2), avl_height(A1,H1),nl,print(diff(avl(H1,Min1,Max1),avl(H2,Min2,Max2))),nl,
    avl_height(A1,H1),
    ((H2<2 -> true ; H1 > H2+1) % then it is more efficient to expand A2 and remove the A2 elements from A1;
    % note that difference_of_explicit_set2 now also sometimes expands both:
    % exact threshold when it is beneficial: difference_of_explicit_set2/3
    % for {x|x:1..200000 & x mod 2 = 0} - {y|y:2500..29010 & y mod 2 = 0} -> 150 ms vs 80 ms avl(17,int(2),int(200000)),avl(14,int(2500),int(29010)
    % {x|x:1..200000 & x mod 2 = 0} - {y|y:2500..59010 & y mod 2 = 0} -> 180 ms vs 80 ms avl(17,int(2),int(200000)),avl(15,int(2500),int(59010))
    % {x|x:1..200000 & x mod 2 = 0} - {y|y:500..159010 & y mod 2 = 0} -> 180 ms vs 250 ms avl(17,int(2),int(200000)),avl(17,int(500),int(159010))
    -> expand_custom_set_to_sorted_list(S2,ES,_,difference_of_explicit_set1,WF),
    difference_of_explicit_set3(ES,A1,R)
    ; expand_custom_set_to_sorted_list(avl_set(A1),ES,Done,difference_of_explicit_set2,WF),
    difference_of_explicit_set2(ES,H1,A2,H2,R,Done)).

difference_of_explicit_set_wf(S1,S2,R,WF) :-
    (S2=avl_set(A2) ;
    ground_value(S2), expand_and_convert_to_avl_set_unless_very_large(S2,A2,WF)),!,
    avl_height(A2,A2Height),
    difference_with_avl(S1,A2,A2Height,R,WF).

difference_with_avl/5

direct_product3/3

direct_product_explicit_set/3

direct_product_explicit_set_aux/3

direct_remove_element_from_avl/3

disjoint_intervals_with_inf/4

do_not_convert_aux/1

does_not_contain_closure/1

does_not_contain_closure_fields/1

dom_for_lambda_closure/2

dom_for_specific_closure/4

dom_for_specific_closure_aux/6

dom_range_for_member_closure/5

dom_range_for_specific_closure/5

dom_range_for_specific_closure2/7

dom_symbolic/2

domain_aux/5

domain_blocking_aux/3

Block: domain_blocking_aux(-,?,?)

domain_of_avl_set/2

domain_of_explicit_set_wf/3

domain_of_list_blocking/2

Block: domain_of_list_blocking(-,?)

domain_of_sorted_list/3

domain_restrict_singleton_element/3

domain_restriction_explicit_set_wf/4

domain_subtraction_explicit_set_wf/4

dont_expand_symbolic_explicit_set/1

dont_expand_this_closure/3

dont_expand_this_closure/4

dont_expand_this_explicit_set/1

dont_expand_this_explicit_set/2

efficient_card_for_set/3

element_can_be_added_or_removed_to_avl/1

element_of_avl_set_wf/3

element_of_avl_set_wf/4

element_of_avl_set_wf3/5

Description:
((var(WF1), \+ ground(X)) -> print(avl_relation_check(X,Y)),nl, %%
copy_term((X,Y),Copy), findall(Copy,safe_avl_member(Copy,AVL),Cs), print(Cs),nl, Cs \=[] %% check that at least one element exists
; true),

Block: element_of_avl_set_wf3(-,?,?,-,?)

element_of_closure/5

Block: element_of_closure(?,-,?,?,?) element_of_closure(?,?,?,-,?)

element_of_custom_set/2

element_of_custom_set2/2

element_of_custom_set_wf/3

element_of_custom_set_wf2/3

element_of_normal_closure/5

element_of_special_closure/6

equal_avl_tree/2

equal_cartesian_product_wf/5

equal_expansions/5

Block: equal_expansions(-,?,?,?,?)

equal_expansions2/5

Block: equal_expansions2(-,?,?,?,?) equal_expansions2(?,-,?,?,?)

equal_expansions3/4

equal_explicit_sets4/4

equal_explicit_sets4(global_set(X),global_set(Y),_,_WF) :- !,X=Y.

equal_explicit_sets4(global_set(B),avl_set(A),E,WF) :- !,equal_explicit_sets4(avl_set(A),global_set(B),E,WF).

equal_explicit_sets4(freetype(X),freetype(Y),_,_WF) :- !,X=Y.

equal_explicit_sets4(avl_set(A),avl_set(B),_,_WF) :- !,
    equal_avl_tree(A,B). % alternatively, we could normalise avl_trees and only store normalised versions

equal_explicit_sets4(avl_set(A),I2,_,_WF) :-
    is_interval_closure_or_integerset(I2,L2,U2),!, % also covers I2=global_set(...)
    avl_equal_to_interval(A,L2,U2).

equal_explicit_sets4(avl_set(A),global_set(B),_,WF) :- \+ b_global_sets:b_integer_set(B), !, % integersets dealt with above
    explicit_set_cardinality_wf(global_set(B),Card,WF),
    is_finite_card(Card), % Card \= inf as avl_set must be finite
    explicit_set_cardinality_wf(avl_set(A),Card,WF). /* the sets must be identical as global_set contains all values */

equal_explicit_sets4(avl_set(A),CPB,_,WF) :-
    is_cartesian_product_closure(CPB,B1,B2),!,
    decompose_avl_set_into_cartesian_product_wf(A,A1,A2,WF),
    kernel_objects:equal_object_wf(A1,B1,equal_explicit_sets4,WF),
    kernel_objects:equal_object_wf(A2,B2,equal_explicit_sets4,WF).

equal_explicit_sets4(closure(P,T,B),avl_set(A),E,WF) :- !, equal_explicit_sets4(avl_set(A),closure(P,T,B),E,WF).

equal_explicit_sets4(I1,I2,_,_WF) :- is_interval_closure_or_integerset(I1,L1,U1),
    is_interval_closure_or_integerset(I2,L2,U2), !,
    L1=L2, U1=U2.

equal_explicit_sets4(CPA,CPB,_,WF) :-
    is_cartesian_product_closure(CPA,A1,A2),
    is_cartesian_product_closure(CPB,B1,B2),!,
    equal_cartesian_product_wf(A1,A2,B1,B2,WF).

equal_explicit_sets4(S1,S2,_,WF) :-
    is_not_member_value_closure_or_integerset(S1,TYPE,MS1),
    is_not_member_value_closure_or_integerset(S2,TYPE,MS2),
    !,
    kernel_objects:equal_object_wf(MS1,MS2,equal_explicit_sets4,WF).

equal_explicit_sets4(closure(P1,T1,B1),closure(P2,T2,B2),_,_WF) :-
    same_closure_body(P1,T1,B1,P2,T2,B2),!.

equal_explicit_sets4(Set1,Set2,allow_expansion,WF) :-
    %kernel_objects:test_finite_set_wf(Set1,F1,WF), kernel_objects:test_finite_set_wf(Set2,F2,WF), equal_expansions(F1,F2,Set1,Set2)
    card_for_specific_custom_set(Set1,Card1,Code1), % TO DO: do not throw info away if Set2 cannot be determined
    card_for_specific_custom_set(Set2,Card2,Code2),
    !,
    call(Code1), call(Code2),
    % TO DO: if one of the two sets is infinite, then it would be enough to know that the other is not infinite for failure without expansion
    equal_expansions(Card1,Card2,Set1,Set2,WF).

equal_explicit_sets4(Set1,Set2,allow_expansion,WF) :- equal_expansions(0,0,Set1,Set2,WF).

equal_explicit_sets_wf/3

Block: equal_explicit_sets_wf(-,?,?) equal_explicit_sets_wf(?,-,?)

equality_cart_product2/7

Block: equality_cart_product2(-,?,?,?,?,?,?)

equality_cartesian_product_wf/6

equality_explicit_sets_wf/4

equality_explicit_sets_wf(global_set(X),global_set(Y),R,_WF) :- !, eq_atomic(X,Y,set,R).

equality_explicit_sets_wf(global_set(B),avl_set(A),R,WF) :- !,equality_explicit_sets_wf(avl_set(A),global_set(B),R,WF).

equality_explicit_sets_wf(freetype(X),freetype(Y),R,_) :- !, eq_atomic(X,Y,set,R).

equality_explicit_sets_wf(avl_set(A),avl_set(B),R,_) :- !,
    (equal_avl_tree(A,B) -> R=pred_true ; R=pred_false). % alternatively, we could normalise avl_trees and only store normalised versions

equality_explicit_sets_wf(avl_set(A),I2,R,WF) :- is_interval_closure_or_integerset(I2,L2,U2),!, % also covers I2=global_set(...)
    avl_equality_to_interval(A,L2,U2,R,WF).

equality_explicit_sets_wf(avl_set(A),global_set(B),R,WF) :- \+ b_global_sets:b_integer_set(B), !,
    explicit_set_cardinality_wf(global_set(B),Card,WF),
    (is_finite_card(Card), % Card \= inf, %as avl_set must be finite
    explicit_set_cardinality_wf(avl_set(A),Card,WF)
    -> R=pred_true /* the sets must be identical as global_set contains all values */
    ; R=pred_false).

equality_explicit_sets_wf(avl_set(A),CPB,R,WF) :-
    is_cartesian_product_closure(CPB,B1,B2),!,
    if(decompose_avl_set_into_cartesian_product_wf(A,A1,A2,WF), % should not produce pending co-routines
    equality_cartesian_product_wf(A1,A2,B1,B2,R,WF),
    R=pred_false % no cartesian product can be equal to this avl_set
).

equality_explicit_sets_wf(closure(P,T,B),avl_set(A),R,WF) :- !,
    equality_explicit_sets_wf(avl_set(A),closure(P,T,B),R,WF).

equality_explicit_sets_wf(I1,I2,R,WF) :- is_interval_closure_or_integerset(I1,L1,U1),
    is_interval_closure_or_integerset(I2,L2,U2), !,
    equality_objects_wf_no_enum((int(L1),int(U1)),(int(L2),int(U2)),R,WF).

equality_explicit_sets_wf(CPA,CPB,R,WF) :-
    is_cartesian_product_closure(CPA,A1,A2), is_cartesian_product_closure(CPB,B1,B2),!,
    equality_cartesian_product_wf(A1,A2,B1,B2,R,WF).

equality_explicit_sets_wf(S1,S2,R,WF) :-
    is_not_member_value_closure_or_integerset(S1,TYPE,MS1),
    is_not_member_value_closure_or_integerset(S2,TYPE,MS2),!,
    equality_objects_with_type_wf(TYPE,MS1,MS2,R,WF).

equality_explicit_sets_wf(closure(P,T,B),closure(P,T,B2),R,_) :-
    same_texpr_body(B,B2),!,R=pred_true.

evaluate_result_expr/6

Block: evaluate_result_expr(-,?,?,?,?,?)

exists_should_be_lifted/4

expand_and_convert_to_avl_set/4

expand_and_convert_to_avl_set_unless_very_large/3

expand_closure_to_avl_or_list/6

expand_closure_to_avl_wf/5

expand_closure_to_list/7

expand_custom_set/2

expand_custom_set/3

expand_custom_set_to_list/2

expand_custom_set_to_list/4

expand_custom_set_to_list2/6

expand_custom_set_to_list3/5

Block: expand_custom_set_to_list3(-,-,?,?,?)

expand_custom_set_to_list_gg/4

expand_custom_set_to_list_k_wf/6

Block: expand_custom_set_to_list_k_wf(-,-,?,?,?,?)

expand_custom_set_to_list_no_dups_wf/5

expand_custom_set_to_list_now/2

expand_custom_set_to_list_wf/5

expand_custom_set_to_sorted_list/5

Block: expand_custom_set_to_sorted_list(-,-,?,?,?)

expand_custom_set_wf/4

expand_if_avl/5

Block: expand_if_avl(?,?,-,?,?)

expand_interval_closure_to_avl/3

Block: expand_interval_closure_to_avl(-,?,?) expand_interval_closure_to_avl(?,-,?)

expand_interval_closure_to_list/4

Block: expand_interval_closure_to_list(-,?,?,?) expand_interval_closure_to_list(?,-,?,?)

expand_normal_closure/7

expand_normal_closure2/7

expand_normal_closure2(_CHECK,Parameters,ParameterTypes,ClosureBody,FullResult,Done,WF) :-
    % TO DO: add more symbolic member closures who have expression computation code
    is_closure1_value_closure(Parameters,ParameterTypes,ClosureBody,VAL),!,
    bsets_clp:relational_trans_closure_wf(VAL,FullResult,WF),
    ground_value_check(FullResult,FRGr),
    when(nonvar(FRGr),Done=true).

expand_normal_closure2(CHECK,Parameters,ParameterTypes,ClosureBody,FullResult,Done,WF) :-
    % special treatment for lambda closures: Advantage: we don't have to wait for variables in EXPR body of closure
    % Disadvantage: EXPR only gets evaluated after a solution has been found for args: can mean repeated computations !
    % (cf pas_as_env_inv_cv_sui, negated version of !(cv_i).(cv_i : t_cv_pas => closure(%cv_o2.((...|>> {cv_i} : t_cv_pas <-> t_cv_pas) ASSERTION
    % Advantage: it can solve constraints such as f = %x.(x:1..10|x+y) & f(5)=1005 (finding y without enumeration); see test 1168
    \+ preferences:preference(use_smt_mode,false),
    is_lambda_closure(Parameters,ParameterTypes,ClosureBody, OtherIDs,OtherTypes, DomainPred, EXPR),
    \+ ground_bexpr(EXPR), % if EXPR is ground, there is nothing to be gained by special treatment here
    WF \= no_wf_available, % otherwise we may have to enumerate EXPR result leading to choice points, e.g. in phase 0
    !,
    bexpr_variables(DomainPred,ClosureWaitVars),
    (CHECK=no_check -> TIMEOUTCODE = true ;
    TIMEOUTCODE = add_closure_warning_wf(CHECK,Parameters,ParameterTypes,ClosureBody,
    'TIME-OUT occurred while ProB was expanding: ',WF)),
    (CHECK=check_no_inf -> VIRTUALTIMEOUTCODE=true ; VIRTUALTIMEOUTCODE=TIMEOUTCODE),
    delay_setof_check_wf( ParTuple,
    (custom_explicit_sets:b_test_closure(OtherIDs,OtherTypes,DomainPred,OtherValues,all_solutions,WF),
    convert_list_into_pairs(OtherValues,ParTuple)
    % TO DO: compile EXPR when we start expanding the closure: to avoid repeated re-computation of expressions for every instance
    ),
    Result, ClosureWaitVars, __Done,
    TIMEOUTCODE,VIRTUALTIMEOUTCODE,WF,DomainPred),
    (WF = no_wf_available
    -> init_wait_flags(WF1,[expansion_context(lambda_function_result,Parameters)])
    ; WF1=WF
    ),
    evaluate_result_expr(Result,EXPR,OtherIDs,EvResult,EvDone,WF1),
    when(nonvar(EvDone),(
    (WF = no_wf_available -> ground_wait_flags(WF1) ; true),
    kernel_objects:equal_object_wf(EvResult,FullResult,expand_normal_closure2,WF),
    Done=true)).

expand_normal_closure2(no_check,Parameters,ParameterTypes,ClosureBody,Result,Done,WF) :- !,
    expand_normal_closure_direct(Parameters,ParameterTypes,ClosureBody,Result,Done,WF).

expand_normal_closure2(CHECK,Parameters,ParameterTypes,ClosureBody,Result,Done,WF) :-
    bexpr_variables(ClosureBody,ClosureWaitVars),
    TIMEOUTCODE = add_closure_warning_wf(CHECK,Parameters,ParameterTypes,ClosureBody,
    'TIME-OUT occurred while ProB was expanding: ',WF),
    (CHECK=check_no_inf -> VIRTUALTIMEOUTCODE=true ; VIRTUALTIMEOUTCODE=TIMEOUTCODE),
    % Note: delay_setof_check_wf will throw enumeration warning for virtual timeouts, after VIRTUALTIMEOUTCODE
    delay_setof_check_wf( ParTuple,
    custom_explicit_sets:test_closure_and_convert(Parameters,ParameterTypes,ClosureBody, ParTuple,WF),
    Result, ClosureWaitVars, Done, TIMEOUTCODE, VIRTUALTIMEOUTCODE,WF,ClosureBody).

expand_normal_closure_direct/6

expand_normal_closure_memo/7

expand_only_custom_closure_global/4

expand_pair_closure/6

explicit_set_cardinality/2

explicit_set_cardinality_for_wf/2

explicit_set_cardinality_wf/3

explicit_tvalue/1

explicit_value/1

expression_contains_setvar/2

expression_contains_setvar_aux/2

fetch/5

filter_start_relation/3

finish_restriction/3

Block: finish_restriction(-,?,?)

force_comp/3

Block: force_comp(-,?,?)

front_sequence_custom_explicit_set/3

gen_typed_ids/3

generate_couple_types/3

generate_renaming_list/3

generate_typed_id_pairs/3

geq_inf/2

Block: geq_inf(-,?) geq_inf(?,-)

get_avl_sequence/2

get_avl_sequence_dcg/3

get_avl_sets/4

get_bounds2/6

get_card_for_specific_custom_set/2

get_closure/4

get_dom_couple_aux/6

get_domain_id_or_expr/4

get_field_cardinality/2

get_field_val/2

get_field_val_type/3

get_fields_template/3

get_first_avl_elements/4

get_first_els/5

get_fresh_id/4

get_geq_leq_bounds/4

get_identity_as_equivalence/4

get_identity_as_equivalence_aux/3

get_integer_set_interval/3

get_inversion_penalty/1

get_min_max_card/3

get_next_mapped_to/4

get_next_mapped_to_eq/4

get_pos_infos_for_explicit_set/2

get_prj1/2

get_range_id_or_expr/4

get_subset_counter_aux/9

get_subset_counter_example_closure/7

get_template/3

get_template2/3

get_value_bounds/3

get_witness_element/2

ground_element_can_be_added_or_removed_to_avl/1

gt0/1

Block: gt0(-)

identifier_info/2

image_explicit/5

Block: image_explicit(-,?,?,?,?)

image_explicit_aux/7

Block: image_explicit_aux(-,?,?,?,?,?,?)

image_explicit_aux_ground/6

image_explicit_ground/5

image_for_closure/6

image_for_explicit_avl_set/4

image_for_explicit_set/4

image_for_id_closure/3

intersect_avl_interval/4

intersect_intervals_with_inf/6

intersection_of_explicit_set_wf/4

intersection_of_explicit_set_wf(global_set(GS),S2,R,_WF) :- is_maximal_global_set(GS), !, R=S2.

intersection_of_explicit_set_wf(freetype(_GS),S2,R,_WF) :- !, R=S2.

intersection_of_explicit_set_wf(_,S2,_,_WF) :- var(S2),!,fail. % code below may instantiate S2

intersection_of_explicit_set_wf(S1,S2,R,_WF) :- is_definitely_maximal_set(S2), !, R=S1.

intersection_of_explicit_set_wf(_S1,[],R,_WF) :-!, R=[].

intersection_of_explicit_set_wf(avl_set(A1),I2,R,_WF) :-
    is_interval_closure_or_integerset(I2,From1,To1),
    !,
    intersect_avl_interval(A1,From1,To1,R).

intersection_of_explicit_set_wf(I1,I2,R,_WF) :-
    intersection_with_interval_closure(I1,I2,R),!.

intersection_of_explicit_set_wf(S1,S2,R,_WF) :-
    get_avl_sets(S1,S2,A1,A2),
    !, % if too large: better to apply normal intersection code ?
    % if one of the args is an interval this is already caught in kernel_objects calling intersection_with_interval_closure; see SetIntersectionBig.mch
    avl_domain(A1,ES), % A1 has the smaller height; important for e.g. SetIntersectionBig2.mch
    inter2(ES,A2,IRes),
    ord_list_to_avlset(IRes,R,intersection). % we have generated the elements in the right order already

intersection_of_explicit_set_wf(Set1,Set2,R,WF) :-
    transform_global_sets_into_closure(Set1,closure(P1,T1,B1)),
    transform_global_sets_into_closure(Set2,closure(P2,T2,B2)),
    % gets called, e.g., for {x|x /: NATURAL1} /\ NATURAL1
    unify_closure_predicates(P1,T1,B1, P2,T2,B2 , NewP,NewT, NewB1,NewB2),
    debug:debug_println(9,intersection_of_two_closures(P1,P2,NewP,NewT)),
    conjunct_predicates([NewB1,NewB2],BI),
    % create a conjunction: can be much more efficient than seperately expanding;
    % also works well if one of the closures is infinite
    C = closure(NewP,NewT,BI),
    expand_custom_set_wf(C,R,intersection_of_explicit_set_wf,WF). % we could keep it symbolic; maybe use SYMBOLIC pref

intersection_with_interval_closure/3

intersection_with_interval_closure_aux/4

interval_image_for_explicit_avl_set/5

Block: interval_image_for_explicit_avl_set(-,?,?,?,?) interval_image_for_explicit_avl_set(?,-,?,?,?)

interval_in_avl_block/4

Block: interval_in_avl_block(-,?,?,?) interval_in_avl_block(?,-,?,?)

interval_in_avl_loop/4

inv/3

Block: inv(-,?,?)

inv_and_norm/2

Block: inv_and_norm(-,?)

inverse_apply_ok/4

inverse_get_possible_values/4

invert_explicit_set/2

Description:
convert to AVL ?

invert_member_predicate/4

is_a_relation/7

Description:
'<->'
'+->'
'-->'
'>+>>'
'>->>'
'>->'
'>+>'
'-->>'
'+->>'
'<<->'
'<->>'

is_a_relation(relations(Domain,Range),Domain,Range,DCard,RCard,Card,Code) :- %% '<->'
    Code = (kernel_card_arithmetic:safe_mul(DCard,RCard,Exp), kernel_card_arithmetic:safe_pow2(Exp,Card)).

is_a_relation(partial_function(Domain,Range),Domain,Range,DCard,RCard,Card,Code) :- %% '+->'
    Code = (kernel_card_arithmetic:safe_add_card(RCard,1,R1),kernel_card_arithmetic:safe_pown(R1,DCard,Card)).

is_a_relation(total_function(Domain,Range),Domain,Range,DCard,RCard,Card,Code) :- %% '-->'
    Code = (kernel_card_arithmetic:safe_pown(RCard,DCard,Card)).

is_a_relation(partial_bijection(Domain,Range),Domain,Range,DCard,RCard,Card,Code) :- %% '>+>>'
    Code = (kernel_card_arithmetic:partial_bijection_card(DCard,RCard,Card)).

is_a_relation(total_bijection(Domain,Range),Domain,Range,DCard,RCard,Card,Code) :- %% '>->>'
    Code = (kernel_card_arithmetic:total_bijection_card(DCard,RCard,Card)).

is_a_relation(total_injection(Domain,Range),Domain,Range,DCard,RCard,Card,Code) :- %% '>->'
    Code = (kernel_card_arithmetic:blocking_factorial_k(RCard,DCard,Card)).

is_a_relation(partial_injection(Domain,Range),Domain,Range,DCard,RCard,Card,Code) :- %% '>+>'
    Code = (kernel_card_arithmetic:partial_injection_card(DCard,RCard,Card)).

is_a_relation(total_surjection(Domain,Range),Domain,Range,DCard,RCard,Card,Code) :- %% '-->>'
    Code = (kernel_card_arithmetic:total_surjection_card(DCard,RCard,Card)).

is_a_relation(partial_surjection(Domain,Range),Domain,Range,DCard,RCard,Card,Code) :- %% '+->>'
    Code = (kernel_card_arithmetic:partial_surjection_card(DCard,RCard,Card)).

is_a_relation(total_relation(Domain,Range),Domain,Range,DCard,RCard,Card,Code) :- %% '<<->'
    Code = (kernel_card_arithmetic:total_relation_card(DCard,RCard,Card)).

is_a_relation(surjection_relation(Domain,Range),Domain,Range,DCard,RCard,Card,Code) :- %% '<->>'
    % just swap args: card(A<->>B) = card(B<<->A)
    Code = (kernel_card_arithmetic:total_relation_card(RCard,DCard,Card)).

is_avl_fd_index_set/2

is_avl_inj_list/3

is_avl_partial_function/1

is_avl_partial_function2/3

is_avl_relation/1

is_avl_relation_over_domain/3

is_avl_relation_over_domain2/3

is_avl_relation_over_range/3

is_avl_relation_over_range2/3

is_avl_total_function_over_domain/2

is_cartesian_product_closure/3

is_cartesian_product_closure_aux/5

is_closure1_value_closure/4

is_converted_lambda_closure/3

Description:
TODO: also prevent expansion of things like ff = %x.(x:STRING & REGEX_MATCH(x,"[a-z]+")=TRUE|TRUE)

is_custom_explicit_set/1

is_custom_explicit_set/2

is_custom_explicit_set_nonvar/1

is_definitely_finite/1

is_definitely_maximal_closure/3

is_definitely_maximal_list/2

is_definitely_maximal_set/1

is_definitely_maximal_set2/1

is_definitely_not_empty/1

is_definitely_not_empty_with_witness/2

is_efficient_custom_set/1

is_empty_closure_now/4

is_empty_closure_wf/4

is_empty_explicit_set/1

is_empty_explicit_set_wf/2

is_full_fdlist/3

is_full_fdlist2/3

is_full_powerset_or_relations_or_struct_closure/2

is_full_powset_aux/3

is_geq_leq_interval_closure/5

is_infinite_closure/3

is_infinite_explicit_set/1

is_infinite_global_set/2

Block: is_infinite_global_set(-,?)

is_infinite_or_symbolic_closure/3

is_infinite_or_very_large_closure/4

is_infinite_or_very_large_explicit_set/1

is_infinite_or_very_large_explicit_set/2

is_injective_avl_relation/2

is_interval_closure/3

is_interval_closure/5

is_interval_closure_aux/4

is_interval_closure_body/4

is_interval_closure_or_integerset/3

Description:
is_interval_closure_or_integerset(+I,-L,-U)

is_interval_with_integer_bounds/3

is_list/1

is_list_skeleton/1

is_maximal_global_set/1

is_maximal_global_set/2

is_non_empty_closure_wf/4

is_non_empty_explicit_set/1

is_non_empty_explicit_set_wf/2

is_not_avl_partial_function/2

is_not_avl_partial_function2/4

is_not_avl_rel_dom1/7

Block: is_not_avl_rel_dom1(-,?,?,?,?,?,?)

is_not_avl_rel_dom2/7

Block: is_not_avl_rel_dom2(-,?,?,?,?,?,?)

is_not_avl_rel_ran2/6

Block: is_not_avl_rel_ran2(-,?,?,?,?,?)

is_not_avl_relation_over_domain_range/4

is_not_avl_relation_over_range/3

is_one_element_avl/2

is_one_element_custom_set/2

is_powerset_closure/3

is_powset_aux/3

is_set_value/2

is_simple_infinite_set/1

is_small_specific_custom_set/2

is_special_closure/4

is_symbolic_closure_or_symbolic_mode/3

is_very_large_maximal_global_set/2

is_very_large_or_symbolic_closure/4

iterate_closure/4

known_length/3

l_card_for_member_closure/4

l_convert_to_avl_wf/3

l_is_definitely_maximal_set/1

last_sequence_explicit_set/2

lazy_check_elements6/6

Block: lazy_check_elements6(-,-,?,?,?,?)

lazy_check_elements_of_closure/6

length_at_least/2

length_larger_than/2

leq0/2

Block: leq0(-,?)

list_does_not_contain_closure/1

low_border/3

match_key/4

match_possible/3

Description:
WF <--- TO DO

Block: match_possible(-,?,?) match_possible(?,-,?)

match_possible_atomic/3

Block: match_possible_atomic(-,?,?) match_possible_atomic(?,-,?)

max_of_explicit_set_wf/3

maximum_with_inf/3

Block: maximum_with_inf(-,-,?)

maximum_with_inf1/3

Block: maximum_with_inf1(-,?,?) maximum_with_inf1(?,-,?)

membership_avl_set_wf/4

membership_avl_set_wf2/4

membership_custom_set/3

membership_custom_set_wf/4

membership_global_set/4

membership_interval/4

min_of_explicit_set_wf/3

minimum_with_inf/3

Block: minimum_with_inf(-,-,?)

minimum_with_inf1/3

Block: minimum_with_inf1(-,?,?) minimum_with_inf1(?,-,?)

must_be_in_domain_check/7

Block: must_be_in_domain_check(-,?,?,?,?,-,?) must_be_in_domain_check(-,?,-,?,?,?,?)

my_avl_member/2

my_length/3

Block: my_length(-,?,?)

no_conversion_nec_term/1

no_conversion_necessary/1

norm/3

Block: norm(-,?,?)

normal_closure_not_member/5

normalise_avl_set/2

normalised_list_to_avl/2

normalised_list_to_avl_when_ground/2

Block: normalised_list_to_avl_when_ground(-,?)

not_check_avl_subset/2

not_element_of_avl_set_block/3

Description:
IMPROVE ??

Block: not_element_of_avl_set_block(-,?,?)

not_element_of_custom_set/2

not_element_of_custom_set_wf/3

not_element_of_custom_set_wf2/3

not_element_of_special_closure/6

not_equal_cartesian_product_wf/5

not_equal_expansions/5

Block: not_equal_expansions(-,?,?,?,?) not_equal_expansions(?,-,?,?,?)

not_equal_explicit_sets_wf/3

Block: not_equal_explicit_sets_wf(-,?,?) not_equal_explicit_sets_wf(?,-,?)

not_equal_explicit_sets_wf(global_set(X),global_set(Y),_) :- !,dif(X,Y).

not_equal_explicit_sets_wf(global_set(B),avl_set(A),WF) :- !,
    \+ equal_explicit_sets4(avl_set(A),global_set(B),allow_expansion,WF).

not_equal_explicit_sets_wf(freetype(X),freetype(Y),_) :- !,dif(X,Y).

not_equal_explicit_sets_wf(avl_set(A),avl_set(B),_) :- !,
    \+ equal_avl_tree(A,B).

not_equal_explicit_sets_wf(avl_set(A),I2,WF) :- is_interval_closure_or_integerset(I2,L2,U2),!, % also covers I2=global_set(...)
    avl_not_equal_to_interval(A,L2,U2,WF).

not_equal_explicit_sets_wf(avl_set(A),global_set(B),WF) :- !,
    \+ equal_explicit_sets4(avl_set(A),global_set(B),allow_expansion,WF).

not_equal_explicit_sets_wf(avl_set(A),CPB,WF) :-
    is_cartesian_product_closure(CPB,B1,B2),!,
    if(decompose_avl_set_into_cartesian_product_wf(A,A1,A2,WF), % should not produce pending co-routines, but better safe
    kernel_objects:not_equal_object_wf((A1,A2),(B1,B2),WF),
    true % no cartesian product can be equal to this avl_set
).

not_equal_explicit_sets_wf(closure(P,T,B),avl_set(A),WF) :- !,
    not_equal_explicit_sets_wf(avl_set(A),closure(P,T,B),WF).

not_equal_explicit_sets_wf(I1,I2,_) :- is_interval_closure_or_integerset(I1,L1,U1),
    is_interval_closure_or_integerset(I2,L2,U2), !,
    dif((L1,U1),(L2,U2)). % maybe we should call not_equal_objects on integers (not on inf values)?

not_equal_explicit_sets_wf(CPA,CPB,WF) :-
    is_cartesian_product_closure(CPA,A1,A2), is_cartesian_product_closure(CPB,B1,B2),!,
    not_equal_cartesian_product_wf(A1,A2,B1,B2,WF).

not_equal_explicit_sets_wf(S1,S2,WF) :-
    is_not_member_value_closure_or_integerset(S1,TYPE,MS1),
    is_not_member_value_closure_or_integerset(S2,TYPE,MS2),!,
    kernel_objects:not_equal_object_wf(MS1,MS2,WF).

not_equal_explicit_sets_wf(closure(P,T,B),closure(P,T,B2),_) :-
    same_texpr_body(B,B2),!,fail.

not_equal_explicit_sets_wf(Set1,Set2,WF) :-
    card_for_specific_custom_set(Set1,Card1,Code1), card_for_specific_custom_set(Set2,Card2,Code2),
    call(Code1), call(Code2),!,
    not_equal_expansions(Card1,Card2,Set1,Set2,WF).

not_equal_explicit_sets_wf(Set1,Set2,WF) :- not_equal_expansions(0,0,Set1,Set2,WF).

not_infinite_bound/1

not_subset_of_explicit_set/4

not_subset_of_explicit_set_aux/4

number_card_of_interval_inf_aux/3

ord_list_to_avlset/2

ord_list_to_avlset/3

ord_list_to_avlset_direct/3

override_custom_explicit_set2/4

override_custom_explicit_set_aux/4

Description:
hit_profiler:add_profile_hit(override(R,S),3), %%

override_custom_explicit_set_aux(CL,Rel2,Res,_WF) :-
    CL=closure(P0,T,B0),
    % TO DO: maybe call keep_symbolic in bsets_clp ??
    ( preferences:get_preference(convert_comprehension_sets_into_closures,true),
    (var(Rel2) -> true ; Rel2 \= avl_set(_)) % if Rel2 is avl_set then maybe better to compute explicitly; unless infinite
    ; quick_size_check_larger_than(Rel2,Size2,133) ->
    % if we have a large AVL set anyway; then allow expansion up to a larger limit; cf machine 670_002.mch
    % a lot of machines use A*B*C <+ {....} to more compactly define large explicit sets
    (Size2=inf -> Limit = 200000
    ; Limit is min(200000,Size2*150)), dont_expand_this_closure(P0,T,B0,Limit)
    ; dont_expand_this_closure(P0,T,B0) % use default limit
    ),
    !,
    rename_ran_ids(P0,B0,[],P,B), % any '_lambda_result_' id is no longer guaranteed to be assigned a value in all cases
    NewClosure=closure(P,T,NewBody),
    % B <+ Rel2 ---> NewBody = P:Rel2 or (prj1(P) /: dom(Rel2) & B)
    % TODO better? : %x.(x:Domain|IF x:dom(SFF) THEN SFF(x) ELSE DEFAULT)?
    generate_typed_id_pairs(P,T,NestedPairs),
    get_texpr_type(NestedPairs,PairsType),
    RelPairsType = set(PairsType),
    ValS = b(value(Rel2),RelPairsType,[]),
    MemS = b(member(NestedPairs,ValS),pred,[]), % P:Rel2
    get_prj1(NestedPairs,DomExpr),
    get_texpr_type(DomExpr,DomType),
    Domain = b(domain(ValS),set(DomType),[]), % TO DO: perform some optimisations like dom(%x.(P|E)) --> {x|P}
    %bsets_clp:domain_wf(Rel2,DomainOfRel2,WF), Domain = b(value(DomainOfRel2),DomType,[]), % this DOES NOT work for 1619, 1706 where override is used for infinite functions
    NotMemDomS = b(not_member(DomExpr,Domain),pred,[]), % prj1(P) /: dom(Rel2)
    conjunct_predicates([NotMemDomS,B],RHS),
    disjunct_predicates([MemS,RHS],NewBody),
    %print(override),nl, bsyntaxtree:check_used_ids_in_ast(NewBody),
    mark_closure_as_symbolic(NewClosure,Res).

override_custom_explicit_set_aux(R,S,Res,WF) :-
    is_custom_explicit_set(R,override_custom_explicit_set),
    nonvar(S), is_custom_explicit_set(S,override_custom_explicit_set),
    %% hit_profiler:add_profile_hit(override(R,S),3),
    override_custom_explicit_set2(R,S,Res,WF).

override_custom_explicit_set_wf/4

override_list/4

Block: override_list(-,?,?,?) override_list(?,-,?,?)

override_pair_explicit_set/4

portray_custom_explicit_set/1

prefix_of_custom_explicit_set/4

prefix_of_custom_explicit_set2/4

prepend_custom_explicit_set/3

project_avl_domain/2

project_avl_domain_on_fd/2

propagate_apply/9

Block: propagate_apply(?,?,?,?,?,-,?,?,?)

propagate_atomic_value/2

Block: propagate_atomic_value(-,?)

propagate_avl_el_large_block/4

Block: propagate_avl_el_large_block(?,?,?,-)

propagate_avl_element_information/4

propagate_avl_element_information_direct/4

propagate_avl_element_information_large/3

propagate_avl_element_information_small/3

propagate_avl_not_element_information/3

propagate_avl_not_element_information3/3

propagate_closure_body_for_all/6

Block: propagate_closure_body_for_all(?,?,?,-,-,?)

propagate_closure_body_value_set/6

Block: propagate_closure_body_value_set(?,?,?,-,-,?)

propagate_fd_dom/2

propagate_fd_membership/3

Block: propagate_fd_membership(-,-,?)

propagate_not_membership/3

Block: propagate_not_membership(-,?,?)

propagate_value/2

Description:
integer(X) -> R=int(X) ; % relevant for SWI 8.5.10 and older where fd_set fails for integers, see test 788; should be fixed in next release
integer(X) -> R=fd(X,T) ; % for SWI 8.5.10 and older, see above

Block: propagate_value(-,?)

quantifier_construct/4

quick_custom_explicit_set_approximate_size/2

quick_definitely_maximal_set_avl/1

quick_definitely_maximal_set_avl_aux/2

quick_definitely_maximal_total_function_avl/1

quick_is_definitely_maximal_set/1

quick_is_definitely_maximal_set_aux/1

quick_non_ground_check/1

quick_propagation_element_information/4

Block: quick_propagation_element_information(-,?,?,?)

quick_size_check_larger_than/3

quick_test_avl_membership/3

ran_for_specific_closure/3

ran_symbolic/2

ran_symbolic_closure/6

Block: range_blocking(-,?)

range_of_explicit_set_wf/3

range_restriction_explicit_set_wf/4

range_subtraction_explicit_set_wf/4

reify_avl_mem2/5

reify_avl_membership/4

reify_integer_avl_mem/3

rel_avl_compose2/4

Block: rel_avl_compose2(-,?,?,?)

rel_avl_compose2_ground/4

rel_composition_for_explicit_set/3

remove_element_from_explicit_set/3

remove_minimum_element_custom_set/3

remove_minimum_element_custom_set2/4

Block: remove_minimum_element_custom_set2(?,?,?,-)

rename_lambda_result_id/4

rename_ran_ids/5

reset_closure_solution_counter/1

restrict2/7

restrict2_avl/6

restrict3/10

Block: restrict3(-,?,?,?,?,?,?,?,?,?)

restriction_explicit_set_wf/6

reverse_custom_explicit_set/2

safe_avl_member_block/4

Block: safe_avl_member_block(?,?,-,-)

safe_avl_member_default/2

safe_avl_member_default_wf/3

safe_avl_member_pair/3

safe_avl_member_pair_wf/4

safe_dec/2

Block: safe_dec(-,?)

safe_is_avl_sequence/1

same_closure/2

same_closure_body/6

same_closure_body_with_parameter_renaming/6

same_fields_inside_closure/2

same_quantified_expression/5

same_sub_expressions/3

same_texpr_with_rewrite/3

same_types/2

same_value_inside_closure/2

seq1_card/2

Block: seq1_card(-,?)

seq_card/2

Block: seq_card(-,?)

set_card/3

Block: set_card(-,?,?)

setup_typed_ids/3

shift_avl_sequence_to_ord_list/3

shift_seq/3

should_be_converted_to_avl/1

should_be_converted_to_avl_from_lists/1

Description:
singleton_set(+Set,-Element).

size_of_avl_sequence/3

size_of_custom_explicit_set/3

small_enough_for_expansion/2

small_interval/2

sort_when_done/4

Block: sort_when_done(-,?,?,?)

sorted_ground_normalised_list_to_avlset/3

split_conjunct/5

split_conjunct_aux/6

strict_subset_constructor/2

subset_constructor/3

subset_of_explicit_set/4

subset_of_explicit_set(AVL,Closure,Code,_WF) :- nonvar(AVL),AVL=avl_set(A),
    is_interval_closure_or_integerset(Closure,Low,Up),!,
    Code=custom_explicit_sets:check_avl_in_interval(A,Low,Up).

subset_of_explicit_set(Closure,CS,Code,WF) :- nonvar(CS), is_custom_explicit_set(CS),
    is_interval_closure_or_integerset(Closure,Low,Up),!,
    Code=custom_explicit_sets:check_interval_in_custom_set(Low,Up,CS,WF).

subset_of_explicit_set(AVL1,AVL2,Code,_WF) :-
    nonvar(AVL1),AVL1=avl_set(A1), nonvar(AVL2),AVL2=avl_set(A2),!,
    Code = custom_explicit_sets:check_avl_subset(A1,A2).

subset_of_explicit_set(C1,AVL2,Code,_WF) :- nonvar(C1),
    simple_finite_set(AVL2),
    is_simple_infinite_set(C1),!, % infinite set cannot be subset of finite one
    Code = fail.

subset_of_explicit_set(C1,C2,Code,WF) :- nonvar(C1),
    is_cartesian_product_closure(C1,S11,S12),!,
    ((S11==[] ; S12==[]) -> Code=true /* we always have a subset */
    ; is_definitely_not_empty(S11),
    is_definitely_not_empty(S12), % only use optimisation if we know S11, S12 to be non-empty
    nonvar(C2), is_cartesian_product_closure(C2,S21,S22),
    Code = (kernel_objects:check_subset_of_wf(S11,S21,WF),
    kernel_objects:check_subset_of_wf(S12,S22,WF) )
).

subset_of_explicit_set(Set1,Set2,Code,WF) :-
    nonvar(Set2),is_cartesian_product_closure(Set2,S21,S22),!,
    % TO DO: maybe don't do this if Set1 is avl_set ??
    debug_println(9,'Applying C <: S21*S22 <=> C : S21 <-> S22'),
    Code = bsets_clp:relation_over_wf(Set1,S21,S22,WF).

subset_of_explicit_set(C1,C2,Code,WF) :- nonvar(C1), nonvar(C2),
    is_powerset_closure(C1,Constructor1,Set1),
    is_powerset_closure(C2,Constructor2,Set2),
    subset_constructor(Constructor1,Constructor2,R),
    !,
    Code = (R=pred_true, kernel_objects:check_subset_of_wf(Set1,Set2,WF)).

subset_of_explicit_set(Set1,Set2,Code,WF) :-
    AllowRegularClosure=false,
    symbolic_subset_of_explicit_set(Set1,Set2,AllowRegularClosure,Code,WF).

suffix_of_custom_explicit_set/4

suffix_of_custom_explicit_set2/4

sum_interval/3

Block: sum_interval(-,?,?) sum_interval(?,-,?)

sum_interval_clpfd_prop/3

sum_or_mul_of_explicit_set/3

symbolic_functionality_check_closure/2

symbolic_injectivity_check_closure/2

symbolic_subset_of_explicit_set/5

tail_sequence_custom_explicit_set/5

test_avl_in_interval/5

test_avl_set/1

test_closure/1

test_closure_and_convert/5

test_closure_and_convert(Parameters,ParameterTypes,ClosureBody, ParTuple, WF) :-
    is_recursive_closure(Parameters,ParameterTypes,ClosureBody),
    get_recursive_identifier_of_closure_body(ClosureBody,TRID),!,
    def_get_texpr_id(TRID,RID), get_texpr_type(TRID,RType),
    %print(test_recursion(RID)),nl, translate:nested_print_bexpr(ClosureBody),nl,
    RecVal = closure(Parameters,ParameterTypes,ClosureBody), % Recursive Value added to parameters
    same_length(Parameters,ParValues),
    reset_closure_solution_counter(Parameters),
    b_test_closure([RID|Parameters],[RType|ParameterTypes],ClosureBody,[RecVal|ParValues],all_solutions,WF),
    convert_sol_list_into_pairs(ParValues,Parameters,ParTuple). % convert tuple without recursive value to ParTuple

test_closure_and_convert(Parameters,ParameterTypes,b(exists(EParAndTypes,ClosureBody),pred,OuterInfo), ParTuple, WF) :-
    % Motivation: enumerating Parameters can be quite inefficient
    % if for example we have something like {x|#y.(y:SmallSet & x=f(y))}
    % Problem: the existential quantifier will be delayed until the Parameters are instantiated !
    % relevant test: 1162
    % Note: this is duplicating to some extent the code in b_test_exists_wo_expansion
    % However, here we can also apply lambda_closure optimisation in b_test_closure below, this is
    % relevant for private_examples/2023/.../rule_FICHIER_MRGATKSAATPAR_RVF219_MRGA_DE.mch
    exists_should_be_lifted(Parameters,ParameterTypes,OuterInfo,ClosureBody),
    split_names_and_types(EParAndTypes,EPar,ETypes),
    !,
    % print(' Lifting existential quantifier (i.e., enumerating paras with closure paras): '), print(EPar),nl,
    % print(outer_paras(Parameters)),nl,
    % append Parameters at end; in case we have a lambda function
    append(EPar,Parameters,FullPar), length(Parameters,NrParas),
    append(ETypes,ParameterTypes,FullTypes),
    length(EPar,NrExistsParas),
    length(IrrelevantParas,NrExistsParas), length(Suffix,NrParas),
    append(IrrelevantParas,Suffix,FullParList),
    copy_identifier_infos(OuterInfo,ClosureBody,ClosureBody2),
    reset_closure_solution_counter(Parameters),
    % bsyntaxtree:check_used_ids_in_ast(ClosureBody2),
    b_test_closure(FullPar,FullTypes,ClosureBody2, FullParList,all_solutions,WF),
    convert_sol_list_into_pairs(Suffix,Parameters,ParTuple).

test_closure_and_convert(Parameters,ParameterTypes,ClosureBody, ParTuple, WF) :-
    reset_closure_solution_counter(Parameters),
    % print(test),nl, translate:nested_print_bexpr(ClosureBody),nl,
    length(Parameters,Len), length(ParValues,Len),
    %(annotate_exists(Parameters,ParameterTypes,ClosureBody,Body2) -> true ; Body2=ClosureBody),
    b_test_closure(Parameters,ParameterTypes,ClosureBody,ParValues,all_solutions,WF),
    convert_sol_list_into_pairs(ParValues,Parameters,ParTuple). % ,print(solution(ParTuple)),nl,nl.

test_empty_closure_wf/5

test_empty_closure_wf2/5

test_empty_explicit_set_wf/3

test_subset_of_explicit_set/5

transform_global_set_into_closure_aux/2

transform_global_sets_into_closure/2

try_apply_to_avl_set/3

try_convert_to_avl/2

try_convert_to_avl_wf/3

try_expand_and_convert_to_avl/2

try_expand_and_convert_to_avl/4

try_expand_and_convert_to_avl_if_smaller_than/3

try_expand_and_convert_to_avl_set/3

try_expand_and_convert_to_avl_unless_large_wf/4

Description:
-> try_expand_and_convert_to_avl(CS,Res)

try_expand_and_convert_to_avl_unless_large_wf/3

try_expand_and_convert_to_avl_unless_very_large_wf/3

try_expand_and_convert_to_avl_wf/5

try_expand_and_convert_to_avl_with_catch_wf/4

try_expand_and_convert_to_avl_with_check/3

try_expand_and_convert_to_avl_with_check/4

try_expand_custom_set/2

try_expand_custom_set_to_list/4

try_expand_custom_set_to_list_wf/5

try_expand_custom_set_wf/4

try_expand_custom_set_with_catch/3

try_expconv_to_avl_with_size/4

try_get_finite_max_card_from_fields/2

try_get_finite_max_card_from_ground_value/2

unify_after_wf/2

unify_clos_lt/10

unify_closure_predicates/10

union_complement_set/4

union_complement_set2/4

union_generalized_explicit_set/3

union_of_avl/3

union_of_avl1/5

union_of_avl_set/3

union_of_avl_set_with_closure/5

union_of_avl_with_acc/3

union_of_avls/3

union_of_closure/5

union_of_explicit_set/3

union_of_explicit_set(global_set(GS),_,R) :- is_maximal_global_set(GS), !,
    R= global_set(GS). /* global_set is already maximal */

union_of_explicit_set(freetype(GS),_,R) :- !, R= freetype(GS). /* freetype is already maximal */

union_of_explicit_set(closure(P,T,B),_,R) :- is_definitely_maximal_closure(P,T,B), !,
    R= closure(P,T,B). /* global_set is already maximal */

union_of_explicit_set(_,S2,R) :- is_definitely_maximal_set(S2),!, % will also look at AVL set
    R=S2.

union_of_explicit_set(S1,S2,R) :- nonvar(S2), S2 = [], !, R=S1.

union_of_explicit_set(S1,S2,_) :- (var(S1);var(S2)),!,fail. % then we cannot compute it here

union_of_explicit_set(S2,S1,R) :-
    is_not_member_value_closure(S1,TYPE,MS1), nonvar(MS1), is_efficient_custom_set(MS1),
    % also works if S2 is complement closure
    difference_of_explicit_set(MS1,S2,Diff),!,
    construct_complement_closure_if_necessary(Diff,TYPE,R).

union_of_explicit_set(avl_set(A1),S2,R) :- !, union_of_avl_set(S2,A1,R).

union_of_explicit_set(S1,S2,R) :-
    is_not_member_value_closure(S1,TYPE,MS1), nonvar(MS1), is_efficient_custom_set(MS1),
    difference_of_explicit_set(MS1,S2,Diff),!,
    construct_complement_closure_if_necessary(Diff,TYPE,R).

union_of_explicit_set(S1,avl_set(A2),R) :- !, union_of_avl_set(S1,A2,R).

union_of_explicit_set(I1,I2,R) :- is_interval_closure_or_integerset(I1,From1,To1), ground(From1), ground(To1),
    is_interval_closure_or_integerset(I2,From2,To2), ground(From2), ground(To2),
    !,
    (union_of_interval(From1,To1,From2,To2,FromRes,ToRes)
    -> construct_interval_closure(FromRes,ToRes,R)
    ; small_enough_for_expansion(From1,To1),small_enough_for_expansion(From2,To2) ->
    % do not attempt union_of_closure below
    expand_interval_closure_to_avl(From1,To1,R1), R1=avl_set(A1), % empty interval already dealt with above !?
    expand_interval_closure_to_avl(From2,To2,R2), R2=avl_set(A2), % Note: unification after call as expand_interval calls equal_object (which gets confused by partially instantiated avl_set(_))
    union_of_avl(A1,A2,ARes),R=avl_set(ARes) /* AVL not normalised */
    ; transform_global_sets_into_closure(I1,closure(Par,T,Body)),
    union_of_closure(I2,Par,T,Body,R)
).

union_of_explicit_set(closure(P,T,B),C2,Res) :-
    union_of_closure(C2,P,T,B,Res).

union_of_interval/6

unique_id_comparison/2

unique_id_comparison_aux/3

up_border/3

update_closure_solution_counter/2

value_contains_setvar/2

very_approximate_cardinality/3

Block: very_approximate_cardinality(-,?,?)

Determinacy Checker

Determinacy Checker:

! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_release,true)
! Existence error in argument 1 of absolute_file_name/3
! file extension('dll_path/dll_path') does not exist
! goal: absolute_file_name(extension('dll_path/dll_path'),_69377,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/pathes.pl')])
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(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 argument 1 of absolute_file_name/3
! file probsrc(error_manager) does not exist
! goal: absolute_file_name(probsrc(error_manager),_79581,[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),_77917,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/xml_prob.pl')])
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_profile,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_src_profile,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_safe_mode,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_core_only,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_myheap,false)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(disable_chr,true)
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(tools_strings) does not exist
! goal: absolute_file_name(probsrc(tools_strings),_59409,[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'),_28553,[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 covsrc(coverage_tools_annotations) does not exist
! goal: absolute_file_name(covsrc(coverage_tools_annotations),_29583,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/kernel_waitflags.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file extrasrc(json_parser) does not exist
! goal: absolute_file_name(extrasrc(json_parser),_63457,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/translate.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(tools) does not exist
! goal: absolute_file_name(probsrc(tools),_152297,[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 prob_rewrite_rules(b_ast_cleanup_rewrite_rules) does not exist
! goal: absolute_file_name(prob_rewrite_rules(b_ast_cleanup_rewrite_rules),_152009,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/b_ast_cleanup.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(tools_strings) does not exist
! goal: absolute_file_name(probsrc(tools_strings),_152297,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/input_syntax_tree.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(b_state_model_check) does not exist
! goal: absolute_file_name(probsrc(b_state_model_check),_152155,[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 extension('counter/counter') does not exist
! goal: absolute_file_name(extension('counter/counter'),_157707,[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 probsrc(kernel_waitflags) does not exist
! goal: absolute_file_name(probsrc(kernel_waitflags),_157565,[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 extrasrc(external_functions_reals) does not exist
! goal: absolute_file_name(extrasrc(external_functions_reals),_156943,[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),_156943,[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),_158239,[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),_157565,[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),_158559,[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),_152155,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/external_functions.pl')])
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_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(closures) does not exist
! goal: absolute_file_name(probsrc(closures),_202353,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/memoization.pl')])
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_use_timer,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),_194089,[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(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),_199929,[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),_194235,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/kernel_equality.pl')])
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(no_wd_checking,true)
! Existence error in user:exists_source/1
! procedure user:exists_source/1 does not exist
! goal: user:exists_source(library(atts))
! Existence error in user:exists_source/1
! procedure user:exists_source/1 does not exist
! goal: user:exists_source(library(atts))
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(avl_tools) does not exist
! goal: absolute_file_name(probsrc(avl_tools),_177323,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/bsets_clp.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file extension('counter/counter') does not exist
! goal: absolute_file_name(extension('counter/counter'),_177323,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/kernel_reals.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file kodkodsrc(kodkod) does not exist
! goal: absolute_file_name(kodkodsrc(kodkod),_170781,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/b_interpreter.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file extension('counter/counter') does not exist
! goal: absolute_file_name(extension('counter/counter'),_170927,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/succeed_max.pl')])
! Existence error in user:exists_source/1
! procedure user:exists_source/1 does not exist
! goal: user:exists_source(library(logarr))
! Existence error in argument 1 of absolute_file_name/3
! file probcspsrc(haskell_csp) does not exist
! goal: absolute_file_name(probcspsrc(haskell_csp),_170781,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/xtl_interface.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file extension('probhash/probhash') does not exist
! goal: absolute_file_name(extension('probhash/probhash'),_174061,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/b_machine_hierarchy.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file extension('probhash/probhash') does not exist
! goal: absolute_file_name(extension('probhash/probhash'),_170927,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/value_persistance.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(avl_tools) does not exist
! goal: absolute_file_name(probsrc(avl_tools),_171069,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/state_packing.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(btypechecker) does not exist
! goal: absolute_file_name(probsrc(btypechecker),_158417,[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(eventhandling) does not exist
! goal: absolute_file_name(probsrc(eventhandling),_152155,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/parsercall.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(bmachine_eventb) does not exist
! goal: absolute_file_name(probsrc(bmachine_eventb),_144757,[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),_144757,[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),_146563,[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),_144757,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/bmachine_static_checks.pl')])
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_safe_mode,true)
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(bsyntaxtree) does not exist
! goal: absolute_file_name(probsrc(bsyntaxtree),_141623,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/bmachine_eventb.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file kodkodsrc(kodkod) does not exist
! goal: absolute_file_name(kodkodsrc(kodkod),_110227,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/bmachine.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file extension('random_permutations/random_permutations') does not exist
! goal: absolute_file_name(extension('random_permutations/random_permutations'),_110951,[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),_108949,[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'),_72715,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/kernel_objects.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(eventhandling) does not exist
! goal: absolute_file_name(probsrc(eventhandling),_67021,[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),_63457,[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 probsrc(custom_explicit_sets) does not exist
! goal: absolute_file_name(probsrc(custom_explicit_sets),_34049,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/bsyntaxtree.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),_29917,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/kernel_tools.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(performance_messages) does not exist
! goal: absolute_file_name(probsrc(performance_messages),_36959,[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)
* Non-determinate: custom_explicit_sets:no_conversion_nec_term/1 (clause 1)
* Indexing cannot distinguish this from clause 2.
* Non-determinate: custom_explicit_sets:get_identity_as_equivalence/4 (clause 1)
* This clause contains a disjunction not forced to be deterministic.
* Non-determinate: custom_explicit_sets:rewrite_glob_set/2 (clause 1)
* Indexing cannot distinguish this from clause 4.
* Non-determinate: custom_explicit_sets:rewrite_glob_set/2 (clause 2)
* Indexing cannot distinguish this from clause 4.
* Non-determinate: custom_explicit_sets:rewrite_glob_set/2 (clause 3)
* Indexing cannot distinguish this from clause 4.
* Non-determinate: custom_explicit_sets:test_empty_explicit_set_wf/3 (clause 4)
* This clause contains a disjunction not forced to be deterministic.
* Non-determinate: custom_explicit_sets:not_infinite_bound/1 (clause 1)
* This clause contains a disjunction not forced to be deterministic.
* Non-determinate: custom_explicit_sets:get_bounds2/6 (clause 1)
* Indexing cannot distinguish this from clause 2.
* Non-determinate: custom_explicit_sets:get_bounds2/6 (clause 3)
* Indexing cannot distinguish this from clause 4.
* Non-determinate: custom_explicit_sets:get_bounds2/6 (clause 5)
* Indexing cannot distinguish this from clause 6.
* Non-determinate: custom_explicit_sets:get_bounds2/6 (clause 7)
* Indexing cannot distinguish this from clause 8.
* Non-determinate: custom_explicit_sets:is_infinite_global_set/2 (clause 1)
* Indexing cannot distinguish this from clause 7.
* Non-determinate: custom_explicit_sets:is_infinite_global_set/2 (clause 2)
* Indexing cannot distinguish this from clause 7.
* Non-determinate: custom_explicit_sets:is_infinite_global_set/2 (clause 3)
* Indexing cannot distinguish this from clause 7.
* Non-determinate: custom_explicit_sets:is_infinite_global_set/2 (clause 4)
* Indexing cannot distinguish this from clause 7.
* Non-determinate: custom_explicit_sets:is_infinite_global_set/2 (clause 5)
* Indexing cannot distinguish this from clause 7.
* Non-determinate: custom_explicit_sets:is_infinite_global_set/2 (clause 6)
* Indexing cannot distinguish this from clause 7.
* Non-determinate: custom_explicit_sets:definitely_expand/2 (clause 1)
* Indexing cannot distinguish this from clause 2.
* Non-determinate: custom_explicit_sets:dont_expand_this_closure/4 (clause 2)
* Indexing cannot distinguish this from clause 3.
* Non-determinate: custom_explicit_sets:is_symbolic_closure_or_symbolic_mode/3 (clause 1)
* Calls nondet predicate custom_explicit_sets:preference/2 .
* Non-determinate: custom_explicit_sets:test_subset_of_explicit_set/5 (clause 4)
* Indexing cannot distinguish this from clause 6.
* Non-determinate: custom_explicit_sets:not_subset_of_explicit_set_aux/4 (clause 2)
* Indexing cannot distinguish this from clause 3.
! warning: predicate custom_explicit_sets:debug_println/2 is dynamic.
! Some nondeterminism may have been missed.
! Add (or move) the directive
! :- dynamic custom_explicit_sets:debug_println/2 .
! near the top of this file.
! warning: predicate custom_explicit_sets:debug_mode/1 is dynamic.
! Some nondeterminism may have been missed.
! Add (or move) the directive
! :- dynamic custom_explicit_sets:debug_mode/1 .
! near the top of this file.
* Non-determinate: custom_explicit_sets:propagate_value/2 (clause 4)
* Calls nondet predicate custom_explicit_sets:debug_println/2 .
* Non-determinate: custom_explicit_sets:propagate_value/2 (clause 5)
* Calls nondet predicate custom_explicit_sets:debug_println/2 .
* Non-determinate: custom_explicit_sets:propagate_atomic_value/2 (clause 1)
* Calls nondet predicate custom_explicit_sets:debug_println/2 .
* Non-determinate: custom_explicit_sets:quick_non_ground_check/1 (clause 8)
* This clause contains a disjunction not forced to be deterministic.
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(no_wd_checking,true)
* Non-determinate: custom_explicit_sets:union_of_closure/5 (clause 2)
* Calls nondet predicate debug:debug_println/2 .
* Non-determinate: custom_explicit_sets:union_of_avl_set_with_closure/5 (clause 1)
* Calls nondet predicate debug:debug_println/2 .
* Non-determinate: custom_explicit_sets:intersection_of_explicit_set_wf/4 (clause 9)
* Calls nondet predicate debug:debug_println/2 .
* Non-determinate: custom_explicit_sets:intersection_with_interval_closure/3 (clause 1)
* Indexing cannot distinguish this from clause 2.
* Non-determinate: custom_explicit_sets:quick_definitely_maximal_set_avl_aux/2 (clause 1)
* Calls nondet predicate preferences:preference/2 .
* Non-determinate: custom_explicit_sets:is_very_large_maximal_global_set/2 (clause 2)
* Indexing cannot distinguish this from clause 3.
* Non-determinate: custom_explicit_sets:is_very_large_maximal_global_set/2 (clause 3)
* Indexing cannot distinguish this from clause 4.
* Non-determinate: custom_explicit_sets:sum_or_mul_of_explicit_set/3 (clause 1)
* Indexing cannot distinguish this from clause 2.
* Non-determinate: custom_explicit_sets:try_expconv_to_avl_with_size/4 (clause 1)
* Calls nondet predicate custom_explicit_sets:debug_format/3 .
* Non-determinate: custom_explicit_sets:try_expconv_to_avl_with_size/4 (clause 2)
* Calls nondet predicate custom_explicit_sets:debug_format/3 .
* Non-determinate: custom_explicit_sets:try_expconv_to_avl_with_size/4 (clause 3)
* Calls nondet predicate custom_explicit_sets:debug_format/3 .
* Non-determinate: custom_explicit_sets:membership_avl_set_wf2/4 (clause 4)
* This clause contains a disjunction not forced to be deterministic.
! 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)
* Non-determinate: custom_explicit_sets:random_avl_member/3 (clause 1)
* This clause contains a disjunction not forced to be deterministic.
* Non-determinate: custom_explicit_sets:random_avl_member/3 (clause 2)
* This clause contains a disjunction not forced to be deterministic.
* Non-determinate: custom_explicit_sets:random_avl_member/3 (clause 3)
* This clause contains a disjunction not forced to be deterministic.
* Non-determinate: custom_explicit_sets:avl_member_opt/2 (clause 1)
* This clause contains a disjunction not forced to be deterministic.
* Non-determinate: custom_explicit_sets:add_recursive_parameter/9 (clause 1)
* Calls nondet predicate custom_explicit_sets:debug_println/2 .
* Non-determinate: custom_explicit_sets:avl_height_less_than_with_solver_strength/2 (clause 1)
* Calls nondet predicate custom_explicit_sets:preference/2 .
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(bsyntaxtree) does not exist
! goal: absolute_file_name(probsrc(bsyntaxtree),_261,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/custom_explicit_sets.pl')])

Name: debug_println/1	Module: foo_error
Name: debug_print/2	Module: foo_error
Name: add_warning_wf/5	Module: foo_error
Name: get_texpr_info/2	Module: bsyntaxtree
Name: call_cleanup/2
Name: temporary_set_preference/3	Module: preferences
Name: =/2
Name: debug_mode/1	Module: foo_error
Name: ->/3
Name: format/2
Name: !
Name: preference/2	Module: preferences

Name: =/2
Name: !
Name: avl_store/4	Module: foo_error
Name: convert_to_avl_inside_set_wf/3	Module: custom_explicit_sets
Name: ground_value/1	Module: foo_error
Name: is_maximal_freetype/1	Module: kernel_freetypes
Name: is_maximal_global_set/1	Module: custom_explicit_sets

Name: add_element_to_explicit_set_wf/4	Module: custom_explicit_sets
Name: =/2
Name: !
Name: avl_store/4	Module: foo_error
Name: convert_to_avl_inside_set_wf/3	Module: custom_explicit_sets

Name: =/2
Name: debug_println/2	Module: foo_error
Name: pending_abort_error/1	Module: kernel_waitflags
Name: ->/3
Name: append/3

Name: not_element_of_special_closure/6	Module: custom_explicit_sets
Name: element_of_special_closure/6	Module: custom_explicit_sets

Name: is/2
Name: avl_to_list_dcg_offset/5	Module: custom_explicit_sets
Name: =/2

Name: RECURSIVE_CALL/3	Module: custom_explicit_sets
Name: avl_store/4	Module: foo_error

Name: image_explicit_aux/7	Module: custom_explicit_sets
Name: image_explicit_aux_ground/6	Module: custom_explicit_sets
Name: rel_avl_compose2_ground/4	Module: custom_explicit_sets
Name: union_of_avl1/5	Module: custom_explicit_sets
Name: add_tuples/6	Module: custom_explicit_sets
Name: rel_avl_compose2/4	Module: custom_explicit_sets

Name: add_to_avl/3	Module: custom_explicit_sets
Name: findall/3

Name: add_ground_element_to_explicit_set_wf/4	Module: custom_explicit_sets
Name: is/2
Name: size_of_avl_sequence/3	Module: custom_explicit_sets
Name: element_can_be_added_or_removed_to_avl/1	Module: custom_explicit_sets

Name: add_wd_error_span/4	Module: foo_error
Name: equal_object_wf/4	Module: kernel_objects
Name: safe_avl_member_default_wf/3	Module: custom_explicit_sets
Name: if/3
Name: !
Name: preference/2	Module: preferences
Name: avl_apply/5	Module: foo_error
Name: convert_to_avl_inside_set_wf/3	Module: custom_explicit_sets
Name: ground_value/1	Module: foo_error

Name: apply_to_avl_set_aux/6	Module: custom_explicit_sets
Name: apply_check_tuple_delay/9	Module: custom_explicit_sets

Name: RECURSIVE_CALL/9	Module: custom_explicit_sets
Name: element_of_avl_set_wf/3	Module: custom_explicit_sets
Name: element_of_avl_set_wf3/5	Module: custom_explicit_sets
Name: get_bounded_wait_flag/4	Module: foo_error
Name: =/2
Name: is/2
Name: get_inversion_penalty/1	Module: custom_explicit_sets
Name: ->/3
Name: >/2
Name: avl_approximate_size/3	Module: custom_explicit_sets
Name: preference/2	Module: preferences
Name: inverse_get_possible_values/4	Module: custom_explicit_sets
Name: !
Name: inverse_apply_ok/4	Module: custom_explicit_sets
Name: apply_check_tuple/5	Module: custom_explicit_sets
Name: nonvar/1

Name: apply_to_avl_set_aux/6	Module: custom_explicit_sets
Name: ground_value_check/2	Module: foo_error

Name: propagate_apply/9	Module: custom_explicit_sets
Name: get_wait_flag0/2	Module: foo_error
Name: true
Name: preference/2	Module: preferences
Name: ->/3
Name: apply_check_tuple_delay/9	Module: custom_explicit_sets
Name: get_bounded_wait_flag/4	Module: foo_error
Name: is/2
Name: =/2
Name: </2
Name: avl_approximate_size/3	Module: custom_explicit_sets
Name: ground_value_check/2	Module: foo_error
Name: !
Name: apply_check_tuple/5	Module: custom_explicit_sets
Name: nonvar/1

Name: var/1
Name: number/1
Name: not_infinite_bound/1	Module: custom_explicit_sets
Name: ->/3
Name: !

Name: \=/2
Name: findall/3
Name: convert_to_avl_inside_set/2	Module: custom_explicit_sets
Name: element_can_be_added_or_removed_to_avl/1	Module: custom_explicit_sets
Name: =/2
Name: nonvar/1

Name: avl_size/2	Module: foo_error
Name: is/2
Name: >/2
Name: ->/3
Name: avl_height/2	Module: foo_error
Name: =/2
Name: add_internal_error/2	Module: foo_error
Name: !
Name: var/1

Name: equal_explicit_sets4/4	Module: custom_explicit_sets
Name: rewrite_value_aux/3	Module: custom_explicit_sets
Name: same_texpr_value2/3	Module: custom_explicit_sets

Name: equality_explicit_sets_wf/4	Module: custom_explicit_sets
Name: avl_not_equal_to_interval/4	Module: custom_explicit_sets

Name: avl_height_less_than/2	Module: foo_error
Name: is/2
Name: preference/2	Module: preferences

Name: reify_integer_avl_mem/3	Module: custom_explicit_sets
Name: propagate_avl_not_element_information/3	Module: custom_explicit_sets

Name: avl_size/2	Module: foo_error
Name: avl_size_possible/2	Module: custom_explicit_sets
Name: is/2
Name: avl_max/2	Module: foo_error
Name: avl_min/2	Module: foo_error
Name: avl_integer_set/1	Module: custom_explicit_sets

Name: is_interval_aux/3	Module: bsyntaxtree
Name: check_member_of_set/4	Module: well_def_prover
Name: propagate_avl_not_element_information/3	Module: custom_explicit_sets
Name: is_interval_aux/3	Module: well_def_prover

Name: avl_member_blocking4/4	Module: custom_explicit_sets
Name: =/2

prob_prolog/src/custom_explicit_sets.pl

Modules

Predicates of custom_explicit_sets

Module Information

6131 Lines

607 Predicates

Imported Modules: error_manager self_check avl kernel_waitflags kernel_tools delay tools avl_tools clpfd closures b_compiler performance_messages kernel_card_arithmetic debug bool_pred clpfd_tables b_enumerate terms

172 Exports

104 specified Imports

Predicates:

Name: avl_member_blocking_aux/5	Module: custom_explicit_sets
Name: compare_blocking/5	Module: custom_explicit_sets
Name: true
Name: nonvar/1
Name: ->/3
Name: =/2
Name: force_comp/3	Module: custom_explicit_sets
Name: dif/2
Name: avl_max/2	Module: foo_error
Name: avl_min/2	Module: foo_error
Name: match_possible/3	Module: custom_explicit_sets
Name: !

Name: RECURSIVE_CALL/2	Module: custom_explicit_sets
Name: =/2
Name: ->/3

Name: find_value/6	Module: tcltk_interface
Name: my_avl_member/2	Module: custom_explicit_sets

Name: safe_avl_member_default/2	Module: custom_explicit_sets
Name: unify_after_wf/2	Module: custom_explicit_sets
Name: avl_fetch_pair/3	Module: foo_error
Name: get_template/3	Module: custom_explicit_sets
Name: !
Name: convert_to_avl_inside_set/2	Module: custom_explicit_sets

Name: safe_avl_member_pair_wf/4	Module: custom_explicit_sets
Name: try_apply_to_avl_set/3	Module: custom_explicit_sets

Name: =</2
Name: get_min_max_card/3	Module: custom_explicit_sets
Name: avl_height/2	Module: foo_error

Name: =/2
Name: is/2
Name: RECURSIVE_CALL/5	Module: custom_explicit_sets

Name: reverse_custom_explicit_set/2	Module: custom_explicit_sets
Name: add_seq/5	Module: custom_explicit_sets

Name: b_not_test_closure_enum_aux/4	Module: custom_explicit_sets
Name: true
Name: ground_typedvals_check/2	Module: foo_error
Name: var/1
Name: ->/3
Name: b_extract_typedvalc/5	Module: b_enumerate

Name: b_not_test_closure_enum/6	Module: custom_explicit_sets
Name: get_texpr_info/2	Module: bsyntaxtree
Name: get_last_wait_flag/3	Module: foo_error
Name: b_not_test_boolean_expression/4	Module: b_interpreter
Name: b_type_values_in_store/3	Module: b_enumerate
Name: set_up_localstate/4	Module: store