Dynamic Predicates: b_global_constant/3 used_b_global_constant/3 inferred_minimum_global_set_cardinality/2 inferred_maximum_global_set_cardinality/2 lookup_global_constant/2 b_global_constant_hash/4 b_precompiled_global_set/1 b_exists_global_set_with_potential_symmetry/0 precompilation_phase/1 is_global_set_of_cardinality_one/2 b_supplementary_global_set/1 b_replaced_global_set/2 extract_setsize_from_machine_cache/3 find_minimum_cardinality_cache/2 global_set_user_defined_scope/2 start_extracting_setsize/1 enumerated_set/1 fixed_deferred_set_size/2

1535 Lines

142 Predicates

Imported Modules: debug tools lists ordsets self_check preferences error_manager bsyntaxtree fd_utils_clpfd

62 Exports

28 specified Imports

Imports	Exports
Name: between/3 Module: between Name: gensym/2 Module: gensym Name: module_info/2 Module: module_information Name: b_get_properties_from_machine/1 Module: bmachine Name: b_get_machine_constants/1 Module: bmachine Name: b_get_machine_variables/1 Module: bmachine Name: b_get_named_machine_set/2 Module: bmachine Name: b_get_machine_set/1 Module: bmachine Name: b_get_all_used_identifiers/1 Module: bmachine Name: b_get_disjoint_constants_of_type/3 Module: bmachine Name: b_extract_values_clause_assignment/3 Module: bmachine Name: b_get_typed_definition/3 Module: bmachine Name: b_get_machine_setscope/2 Module: bmachine Name: term_hash/2 Module: terms Name: avl_fetch/2 Module: avl Name: static_symmetry_reduction_possible/5 Module: static_symmetry_reduction Name: perform_ssr/8 Module: static_symmetry_reduction Name: ord_domain_list_to_avl/2 Module: avl_tools Name: transform_bexpr_with_scoping/3 Module: bsyntaxtree Name: ord_member_nonvar_chk/2 Module: tools_lists Name: ord_nonmember/2 Module: ordsets Name: print_error/1 Module: tools_printing Name: format_error_with_nl/2 Module: tools_printing Name: is_disjoint_pred/4 Module: partition_detection Name: conjunction_to_list/2 Module: bsyntaxtree Name: translate_bexpression/2 Module: translate Name: all_strings_wf/2 Module: kernel_objects Name: gen_enum_warning_wf/6 Module: kernel_objects	Name: b_get_global_constants/1 Name: b_get_enumerated_set_constants/1 Name: b_get_global_enumerated_sets/1 Name: b_get_global_sets/1 Name: lookup_global_constant/2 Name: is_b_global_constant/3 Name: is_b_global_constant_hash/3 Name: is_used_b_global_constant/3 Name: is_unused_b_global_constant/2 Name: b_global_set/1 Name: b_non_empty_global_set/1 Name: b_empty_global_set/1 Name: b_global_deferred_set/1 Name: b_global_set_with_potential_symmetry/1 Name: b_global_deferred_set_with_card_gt1/1 Name: b_partially_deferred_set/1 Name: enumerated_set/1 Name: unfixed_deferred_set/1 Name: unfixed_deferred_set_exists/0 Name: fixed_deferred_set_size/2 Name: provably_finite_global_set/1 Name: infinite_global_set/1 Name: contains_unfixed_deferred_set/1 Name: contains_unfixed_deferred_set/2 Name: b_supplementary_global_set/1 Name: inferred_minimum_global_set_cardinality/2 Name: inferred_maximum_global_set_cardinality/2 Name: b_exists_global_set_with_potential_symmetry/0 Name: b_global_set_cardinality/2 Name: b_clear_global_set_type_definitions/0 Name: b_check_and_precompile_enumerated_sets/0 Name: b_check_and_precompile_deferred_sets/0 Name: b_check_and_precompile_global_set_symmetry/0 Name: register_enumerated_sets/2 Name: b_get_prob_deferred_set_elements/2 Name: add_prob_deferred_set_elements_to_store/3 Name: inline_prob_deferred_set_elements_into_bexpr/2 Name: prob_deferred_set_element/4 Name: find_inequal_global_set_identifiers/4 Name: static_symmetry_reduction_for_global_sets/1 Name: b_integer_set/1 Name: b_integer_or_real_or_string_set/1 Name: b_integer_or_real_set/1 Name: b_type2_set/2 Name: try_b_type2global_set/2 Name: b_get_fd_type_bounds/3 Name: b_fd_card/2 Name: is_global_set_of_cardinality_one/2 Name: global_type/2 Name: global_type_wf/3 Name: get_global_type_value/3 Name: enum_global_type_limited/2 Name: enumerate_global_type_with_enum_warning/4 Name: all_elements_of_type/2 Name: all_elements_of_type_wf/3 Name: all_elements_of_type_rand_wf/3 Name: set_user_defined_scope/2 Name: get_user_defined_scope/4 Name: generate_fresh_supplementary_global_set/1 Name: register_replaced_global_set/2 Name: b_replaced_global_set/2 Name: list_contains_unfixed_deferred_set_id/1

Imports

Exports

Name: between/3

Module: between

Name: gensym/2

Module: gensym

Name: module_info/2

Module: module_information

Name: b_get_properties_from_machine/1

Module: bmachine

Name: b_get_machine_constants/1

Module: bmachine

Name: b_get_machine_variables/1

Module: bmachine

Name: b_get_named_machine_set/2

Module: bmachine

Name: b_get_machine_set/1

Module: bmachine

Name: b_get_all_used_identifiers/1

Module: bmachine

Name: b_get_disjoint_constants_of_type/3

Module: bmachine

Name: b_extract_values_clause_assignment/3

Module: bmachine

Name: b_get_typed_definition/3

Module: bmachine

Name: b_get_machine_setscope/2

Module: bmachine

Name: term_hash/2

Module: terms

Name: avl_fetch/2

Module: avl

Name: static_symmetry_reduction_possible/5

Module: static_symmetry_reduction

Name: perform_ssr/8

Module: static_symmetry_reduction

Name: ord_domain_list_to_avl/2

Module: avl_tools

Name: transform_bexpr_with_scoping/3

Module: bsyntaxtree

Name: ord_member_nonvar_chk/2

Module: tools_lists

Name: ord_nonmember/2

Module: ordsets

Name: print_error/1

Module: tools_printing

Name: format_error_with_nl/2

Module: tools_printing

Name: is_disjoint_pred/4

Module: partition_detection

Name: conjunction_to_list/2

Module: bsyntaxtree

Name: translate_bexpression/2

Module: translate

Name: all_strings_wf/2

Module: kernel_objects

Name: gen_enum_warning_wf/6

Module: kernel_objects

Name: b_get_global_constants/1

Name: b_get_enumerated_set_constants/1

Name: b_get_global_enumerated_sets/1

Name: b_get_global_sets/1

Name: lookup_global_constant/2

Name: is_b_global_constant/3

Name: is_b_global_constant_hash/3

Name: is_used_b_global_constant/3

Name: is_unused_b_global_constant/2

Name: b_global_set/1

Name: b_non_empty_global_set/1

Name: b_empty_global_set/1

Name: b_global_deferred_set/1

Name: b_global_set_with_potential_symmetry/1

Name: b_global_deferred_set_with_card_gt1/1

Name: b_partially_deferred_set/1

Name: enumerated_set/1

Name: unfixed_deferred_set/1

Name: unfixed_deferred_set_exists/0

Name: fixed_deferred_set_size/2

Name: provably_finite_global_set/1

Name: infinite_global_set/1

Name: contains_unfixed_deferred_set/1

Name: contains_unfixed_deferred_set/2

Name: b_supplementary_global_set/1

Name: inferred_minimum_global_set_cardinality/2

Name: inferred_maximum_global_set_cardinality/2

Name: b_exists_global_set_with_potential_symmetry/0

Name: b_global_set_cardinality/2

Name: b_clear_global_set_type_definitions/0

Name: b_check_and_precompile_enumerated_sets/0

Name: b_check_and_precompile_deferred_sets/0

Name: b_check_and_precompile_global_set_symmetry/0

Name: register_enumerated_sets/2

Name: b_get_prob_deferred_set_elements/2

Name: add_prob_deferred_set_elements_to_store/3

Name: inline_prob_deferred_set_elements_into_bexpr/2

Name: prob_deferred_set_element/4

Name: find_inequal_global_set_identifiers/4

Name: static_symmetry_reduction_for_global_sets/1

Name: b_integer_set/1

Name: b_integer_or_real_or_string_set/1

Name: b_integer_or_real_set/1

Name: b_type2_set/2

Name: try_b_type2global_set/2

Name: b_get_fd_type_bounds/3

Name: b_fd_card/2

Name: is_global_set_of_cardinality_one/2

Name: global_type/2

Name: global_type_wf/3

Name: get_global_type_value/3

Name: enum_global_type_limited/2

Name: enumerate_global_type_with_enum_warning/4

Name: all_elements_of_type/2

Name: all_elements_of_type_wf/3

Name: all_elements_of_type_rand_wf/3

Name: set_user_defined_scope/2

Name: get_user_defined_scope/4

Name: generate_fresh_supplementary_global_set/1

Name: register_replaced_global_set/2

Name: b_replaced_global_set/2

Name: list_contains_unfixed_deferred_set_id/1

Predicates

Predicates:

add_named_constants_to_global_set/3

add_new_global_set/1

add_prob_deferred_set_elements_to_store/3

all_diff_aux/5

all_different/4

all_elements_of_type/2

all_elements_of_type2/3

all_elements_of_type_rand2/3

all_elements_of_type_rand_wf/3

all_elements_of_type_wf/3

assert_enumerated_set/4

assert_extract_setsize_from_machine_cache/3

b_check_and_precompile_deferred_sets/0

b_check_and_precompile_enumerated_sets/0

b_check_and_precompile_global_set_symmetry/0

b_clear_global_set_type_definitions/0

b_empty_global_set/1

b_extract_fd_type/3

b_fd_card/2

b_get_enumerated_set_constants/1

b_get_fd_type_bounds/3

b_get_fd_type_bounds_limited/3

b_get_fd_type_bounds_with_enum_warning/6

b_get_global_constants/1

b_get_global_enumerated_sets/1

b_get_global_sets/1

b_get_prob_deferred_set_elements/2

b_global_deferred_set/1

b_global_deferred_set_with_card_gt1/1

b_global_set/1

b_global_set_cardinality/2

b_global_set_with_potential_symmetry/1

b_integer_or_real_or_string_set/1

b_integer_or_real_set/1

b_integer_set/1

b_non_empty_global_set/1

b_partially_deferred_set/1

b_precompiled_global_set/1

b_reset_global_set_type_definitions/0

b_supplementary_global_set/1

b_type2_set/2

check_compatible_with_user_scope/3

check_enumerated_set_scope/1

contains_unfixed_deferred_set/1

contains_unfixed_deferred_set/2

default_deferred_set_bounds/2

deferred_sets_precompiled/0

enum_global_type_aux/4

enum_global_type_limited/2

enumerate_global_type_with_enum_warning/4

enumerated_sets_precompiled/0

equality/3

evaluable_integer_expression/3

extract_DEFERRED_setsize_from_machine/3

extract_integer_range/3

extract_min_or_exact_value_for_id/3

extract_setsize_from_defs/4

extract_setsize_from_machine/3

extract_setsize_from_machine_cache/3

find_a_transitive_partition/2

find_all_used_enumerated_elements/1

find_inequal_global_set_identifiers/4

find_inequal_global_set_identifiers2/4

find_inquality/4

find_maximum_cardinality/2

find_maximum_cardinality1/2

find_maximum_cardinality2/4

find_min_card_of_disjoint_sets/3

find_minimum_cardinality/2

find_minimum_cardinality2/4

find_minimum_cardinality3/4

fixed_finite_deferred_set_size/2

gen_int_set/3

generate_fresh_supplementary_global_set/1

get_card_upper_bound/3

get_equality/4

get_global_type_value/3

get_minimum_or_exact_value/3

get_minimum_or_exact_value_aux/3

get_relevant_partition_preds/3

get_texpr_integer/2

get_user_defined_scope/4

get_value_bound/3

global_set_identifier/2

global_set_identifier2/2

infinite_global_set/1

inline_prob_deferred_set_elements_into_bexpr/2

inline_state/4

inline_subsets/4

is_b_global_constant/3

is_b_global_constant_hash/3

is_b_precompiled_globalset/1

is_equality_card_expression/4

is_equality_card_global_set/4

is_greaterequalthan_card_global_set/4

is_greaterequalthan_card_global_set_id/5

is_infinite_global_set_pred/2

is_relevant_partition/4

is_surjection/3

is_unused_b_global_constant/2

is_used_b_global_constant/3

list_contains_unfixed_deferred_set_id/1

max_card_of_partition_list/4

maximum_cardinality_of_expression/3

maximum_cardinality_of_expression2/3

maximum_cardinality_of_identifier/3

min_card_of_identifier/5

minimum_cardinality/2

minimum_cardinality2/3

minimum_cardinality_of_set/3

minimum_cardinality_of_set_aux/4

not_empty/2

not_empty_aux/2

perform_static_symmetry_reduction/2

portray_global_sets/0

pre_register_enumerated_set/1

pre_register_enumerated_set_with_elems/2

precompile_global_set/1

prob_deferred_set_element/4

provably_finite_global_set/1

register_enumerated_sets/2

register_replaced_global_set/2

reset_global_set_user_defined_scope/0

set_extension_list/3

set_ids/4

set_user_defined_scope/2

start_extracting_setsize_from_machine/1

static_symmetry_reduction_for_global_sets/1

try_b_type2global_set/2

try_extract_setsize_from_machine/3

unfixed_deferred_set/1

unfixed_deferred_set_exists/0

user_forced_symmetry/1

add_named_constants_to_global_set/3

add_new_global_set/1

add_prob_deferred_set_elements_to_store/3

all_diff_aux/5

all_different/4

all_elements_of_type/2

all_elements_of_type2/3

all_elements_of_type2('STRING',Res,WF) :- !,
    all_strings_wf(Res,WF).

all_elements_of_type2('NAT',Res,_WF) :- !, get_preference(maxint,MaxInt),
    gen_int_set(0,MaxInt,Res).

all_elements_of_type2('NATURAL',Res,WF) :- !, get_preference(maxint,MaxInt),
    gen_enum_warning_wf('NATURAL',0:sup,0:MaxInt,trigger_throw('NATURAL'),unknown,WF), %print('### Warning: expanding NATURAL'),nl,
    gen_int_set(0,MaxInt,Res).

all_elements_of_type2('NAT1',Res,_WF) :- !, get_preference(maxint,MaxInt),
    gen_int_set(1,MaxInt,Res).

all_elements_of_type2('NATURAL1',Res,WF) :- !,
    get_preference(maxint,MaxInt),
    gen_enum_warning_wf('NATURAL1',1:sup,1:MaxInt,trigger_throw('NATURAL1'),unknown,WF), %print('### Warning: expanding NATURAL1'),nl,
    gen_int_set(1,MaxInt,Res).

all_elements_of_type2('INT',Res,_WF) :- !, get_preference(maxint,MaxInt),
    get_preference(minint,MinInt),
    gen_int_set(MinInt,MaxInt,Res).

all_elements_of_type2('INTEGER',Res,WF) :- !, get_preference(maxint,MaxInt),
    get_preference(minint,MinInt),
    gen_enum_warning_wf('INTEGER',inf:sup,MinInt:MaxInt,trigger_throw('INTEGER'),unknown,WF), %print('### Warning: expanding INTEGER'),nl,
    gen_int_set(MinInt,MaxInt,Res).

all_elements_of_type2('FLOAT',Res,WF) :- !, all_elements_of_type2('REAL',Res,WF).

all_elements_of_type2('REAL',Res,WF) :- !,
    gen_enum_warning_wf('REAL',inf:sup,0.0:1.0,trigger_throw('REAL'),unknown,WF),
    Res = [term(floating(0.0)),term(floating(1.0))]. % not sure this will ever be used

all_elements_of_type2(Type,Set,WF) :-
    b_get_fd_type_bounds(Type,Low,Up),
    (Up=inf
    -> get_preference(maxint,MaxInt), % infinite deferred set
    gen_enum_warning_wf(Type,Low:Up,Low:MaxInt,trigger_throw(Type),unknown,WF),
    findall(fd(El,Type),enum_fd_linear(El,Low,MaxInt),Set)
    ; % ensure we do not use Random enumeration
    findall(fd(El,Type),enum_fd_linear(El,Low,Up),Set)
).

all_elements_of_type_rand2/3

all_elements_of_type_rand_wf/3

Block: all_elements_of_type_rand_wf(-,?,?)

all_elements_of_type_wf/3

Block: all_elements_of_type_wf(-,?,?)

assert_enumerated_set/4

assert_extract_setsize_from_machine_cache/3

b_check_and_precompile_deferred_sets/0

b_check_and_precompile_enumerated_sets/0

b_check_and_precompile_global_set_symmetry/0

b_clear_global_set_type_definitions/0

b_empty_global_set/1

b_extract_fd_type/3

b_fd_card/2

Description:
Note: The Disprover now checks whether unfixed_deferred sets were involved; keeping track of implicit enumerations of deferred sets is just too difficult

b_get_enumerated_set_constants/1

b_get_fd_type_bounds/3

b_get_fd_type_bounds_limited/3

b_get_fd_type_bounds_with_enum_warning/6

b_get_global_constants/1

b_get_global_enumerated_sets/1

Description:
b_get_global_enumerated_sets(-GSets).

b_get_global_sets/1

b_get_prob_deferred_set_elements/2

b_global_deferred_set/1

b_global_deferred_set_with_card_gt1/1

b_global_set/1

b_global_set_cardinality/2

b_global_set_with_potential_symmetry/1

b_integer_or_real_or_string_set/1

b_integer_or_real_set/1

b_integer_set/1

b_non_empty_global_set/1

b_partially_deferred_set/1

b_precompiled_global_set/1

Dynamic: true

b_reset_global_set_type_definitions/0

b_supplementary_global_set/1

Dynamic: true

b_type2_set/2

check_compatible_with_user_scope/3

check_enumerated_set_scope/1

contains_unfixed_deferred_set/1

contains_unfixed_deferred_set/2

default_deferred_set_bounds/2

deferred_sets_precompiled/0

enum_global_type_aux/4

enum_global_type_limited/2

enumerate_global_type_with_enum_warning/4

enumerated_sets_precompiled/0

equality/3

evaluable_integer_expression/3

extract_DEFERRED_setsize_from_machine/3

extract_DEFERRED_setsize_from_machine(GlobalSetName,L,U) :-
    b_extract_values_clause_assignment(GlobalSetName,_Type,TVal), % VALUES clause
    (get_interval(TVal,Low,Up) -> true
    ; add_error(b_global_sets,'VALUES clause must set deferred set to an interval: ',GlobalSetName,TVal),fail),
    (evaluable_integer_expression(Low,[],LowBound) -> true
    ; add_error(b_global_sets,'Cannot extract lower bound from VALUES interval for: ',GlobalSetName,Low),fail),
    (evaluable_integer_expression(Up,[],UpBound) -> true
    ; add_error(b_global_sets,'Cannot extract upper bound from VALUES interval for: ',GlobalSetName,Up),fail),
    !,
    check_compatible_with_user_scope(GlobalSetName,UpBound,LowBound),
    LowBound=L,UpBound=U.

extract_DEFERRED_setsize_from_machine(GlobalSetName,L,U) :-
    b_get_properties_from_machine(Properties), member_in_conjunction(C,Properties),
    (is_equality_card_global_set(C,GlobalSetName,Properties,Card)
    % check if the PROPERTIES contain an expression of the form card(GS) = Nr
    -> true
    ; is_infinite_global_set_pred(C,GlobalSetName)
    % look for predicates which stipulate that the set is infinite
    -> Card=inf
    ),
    !,
    assertz(fixed_deferred_set_size(GlobalSetName,Card)),
    LowBound=1, UpBound = Card,
    check_compatible_with_user_scope(GlobalSetName,UpBound,LowBound),
    LowBound=L,UpBound=U.

extract_DEFERRED_setsize_from_machine(GlobalSetName,L,U) :- /* check if there is a scope_ DEFINITION */
    get_user_defined_scope(GlobalSetName,LowBound,UpBound,_),!,
    LowBound=L,UpBound=U.

extract_DEFERRED_setsize_from_machine(GlobalSetName,LowBound,UpBound) :-
    get_preference(globalsets_fdrange,DefaultUpperBound),
    find_minimum_cardinality(GlobalSetName,MinCard),
    assertz(inferred_minimum_global_set_cardinality(GlobalSetName,MinCard)),
    !,
    LowBound = 1,
    (find_maximum_cardinality(GlobalSetName,MaxCard)
    -> (MaxCard=MinCard -> assertz(fixed_deferred_set_size(GlobalSetName,MinCard)),
    debug_println(9,fixed_deferred_set_size(GlobalSetName,MinCard)),
    UpBound = MinCard
    ; DefaultUpperBound>MaxCard ->
    debug_println(9,reducing_deferred_set_size(GlobalSetName,MaxCard)),
    UpBound=MaxCard
    ; DefaultUpperBound<MinCard ->
    debug_println(9,inferred_minimum_global_set_cardinality(GlobalSetName,MinCard)),
    UpBound=MinCard
    ; UpBound is MinCard
    )
    ; MinCard>DefaultUpperBound -> UpBound=MinCard
    ; UpBound=DefaultUpperBound),
    debug_println(4,inferred(GlobalSetName,UpBound)).

extract_DEFERRED_setsize_from_machine(GlobalSetName,LowBound,UpBound) :-
    % No Minimum cardinality was inferred
    LowBound=1, get_preference(globalsets_fdrange,DefaultUpperBound),
    find_maximum_cardinality(GlobalSetName,MaxCard),
    !,
    (MaxCard=1 -> UpBound=1, assertz(fixed_deferred_set_size(GlobalSetName,1))
    ; inf_greater(DefaultUpperBound,MaxCard) ->
    debug_println(9,reducing_deferred_set_size(GlobalSetName,MaxCard)),
    UpBound=MaxCard
    % does not have the case: DefaultUpperBound UpBound=MinCard
    ; UpBound=DefaultUpperBound).

extract_DEFERRED_setsize_from_machine(_GlobalSetName,LowBound,UpBound) :-
    % No Minimum cardinality was inferred
    default_deferred_set_bounds(LowBound,UpBound).

extract_integer_range/3

extract_min_or_exact_value_for_id/3

extract_setsize_from_defs/4

extract_setsize_from_machine/3

extract_setsize_from_machine_cache/3

Dynamic: true

find_a_transitive_partition/2

find_all_used_enumerated_elements/1

find_inequal_global_set_identifiers/4

find_inequal_global_set_identifiers2/4

find_inquality/4

find_maximum_cardinality/2

find_maximum_cardinality1/2

find_maximum_cardinality2/4

find_min_card_of_disjoint_sets/3

find_minimum_cardinality/2

find_minimum_cardinality2/4

find_minimum_cardinality3/4

fixed_finite_deferred_set_size/2

gen_int_set/3

generate_fresh_supplementary_global_set/1

get_card_upper_bound/3

get_equality/4

get_global_type_value/3

get_minimum_or_exact_value/3

Description:
print(not_equal(GlobalSet,_X)),nl.

get_minimum_or_exact_value_aux/3

get_relevant_partition_preds/3

get_texpr_integer/2

get_user_defined_scope/4

get_value_bound/3

global_set_identifier/2

global_set_identifier2/2

inequality_aux(not_equal(I1,I2),GS,ID,OtherID,_) :-
    gs_identifier(I1,GS,ID1), gs_identifier(I2,GS,ID2),
    (ID=ID1 -> OtherID=ID2 ; ID=ID2,OtherID=ID1).

inequality_aux(not_equal(I1,I2),GS,ID,OtherID,_) :- % treat {aa} \= {bb} or more generally {aa,bb} \= {aa,cc}
    % two identifiers of global sets need not be different
    % in order for two set extensions to be inequal
    % first we check if I1, I2 are in fact subsets of global sets
    get_texpr_type(I1,set(global(_))),
    get_texpr_expr(I1,set_extension(IDs1)), % TODO: is there something more general than a set_extension?
    get_texpr_expr(I2,set_extension(IDs2)), % should full sets or set identifiers added?
    % remove the common elements and see if we find a pair of identifiers
    maplist(remove_all_infos_and_ground,IDs1,IDs1NoInfos),
    maplist(remove_all_infos_and_ground,IDs2,IDs2NoInfos),
    % TODO: maybe it is same to assume the order?
    list_to_ord_set(IDs1NoInfos,IDs1Set), list_to_ord_set(IDs2NoInfos,IDs2Set),
    ord_subtract(IDs1Set,IDs2Set,[E1]), % each set has one identifier that is not in the other one
    ord_subtract(IDs2Set,IDs1Set,[E2]),
    E1 \= E2, % and they are not the same
    gs_identifier(E1,GS,ID1), gs_identifier(E2,GS,ID2),
    set_ids(ID1,ID2,ID,OtherID).

inequality_aux(negation( b(equal(I1,I2),pred,_)),GS,ID,OtherID,_) :-
    gs_identifier(I1,GS,ID1), gs_identifier(I2,GS,ID2),
    set_ids(ID1,ID2,ID,OtherID).

inequality_aux(partition(Set,DisjSets),GS,ID,OtherID,Preds) :-
    get_texpr_type(Set,set(GS)), % only look at relevant partitions of correct type
    %nl,print(part(_Set,DisjSets,GS,ID,OtherID)),nl,
    % detect such things as partition(_,{...ID...},...{...OtherID...}...)
    select(Set1,DisjSets,Rest), set_extension_list(Set1,Preds,List1),
    member(O1,List1), gs_identifier(O1,GS,ID),
    member(Set2,Rest), set_extension_list(Set2,Preds,List2),
    member(O2,List2), gs_identifier(O2,GS,OtherID).

inequality_aux(member(I1,SetDiff),GS,ID,OtherID,_Preds) :-
    % detect ID : SUPERSET - { ... OtherID ...} => ID:SUPERSET & ID /= OtherID
    get_texpr_expr(SetDiff,set_subtraction(_SuperSet,b(OtherSet,_,_))),
    gs_identifier(I1,GS,ID1),
    id_element_of_set(OtherSet,GS,ID2),
    set_ids(ID1,ID2,ID,OtherID).

inequality_aux(AllDiff,GS,ID,OtherID,Preds) :-
    all_different(AllDiff,List1,GS,Preds),
    select(O1,List1,RestList), gs_identifier(O1,GS,ID),
    member(O2,RestList), gs_identifier(O2,GS,OtherID).

inf_add/3

inf_greater/2

infinite_global_set/1

inline_prob_deferred_set_elements_into_bexpr/2

inline_state/4

inline_subsets/4

is_b_global_constant/3

is_b_global_constant_hash/3

is_b_precompiled_globalset/1

is_equality_card_expression/4

is_equality_card_global_set/4

is_greaterequalthan_card_global_set/4

is_greaterequalthan_card_global_set_id/5

Description:
preferences:get_preference(allow_empty_global_sets,false), preference no longer exists

is_infinite_global_set_pred/2

is_relevant_partition/4

is_surjection/3

is_unused_b_global_constant/2

is_used_b_global_constant/3

list_contains_unfixed_deferred_set_id/1

Description:
list_contains_unfixed_deferred_set_id(+TypedIds).

max_card_of_partition_list/4

maximum_cardinality_of_expression/3

maximum_cardinality_of_expression2/3

maximum_cardinality_of_identifier/3

min_card_of_identifier/5

minimum_cardinality/2

minimum_cardinality2/3

minimum_cardinality_of_set/3

minimum_cardinality_of_set_aux/4

not_empty/2

not_empty_aux/2

perform_static_symmetry_reduction/2

portray_global_sets/0

pre_register_enumerated_set/1

pre_register_enumerated_set_with_elems/2

precompile_global_set/1

prob_deferred_set_element/4

provably_finite_global_set/1

register_enumerated_sets/2

register_replaced_global_set/2

reset_global_set_user_defined_scope/0

set_extension_list/3

set_ids/4

set_user_defined_scope/2

start_extracting_setsize_from_machine/1

static_symmetry_reduction_for_global_sets/1

try_b_type2global_set/2

try_extract_setsize_from_machine/3

unfixed_deferred_set/1

Description:
b_try_update_fd_cardinality has been removed

unfixed_deferred_set_exists/0

user_forced_symmetry/1

Determinacy Checker

Determinacy Checker:

! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_enter_debugger_upon_error,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_use_timer,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(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 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'),_64345,[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(prob_release,true)
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(error_manager) does not exist
! goal: absolute_file_name(probsrc(error_manager),_74549,[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),_72885,[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),_54377,[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'),_23535,[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 extrasrc(json_parser) does not exist
! goal: absolute_file_name(extrasrc(json_parser),_44135,[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 covsrc(coverage_tools_annotations) does not exist
! goal: absolute_file_name(covsrc(coverage_tools_annotations),_79247,[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 extension('random_permutations/random_permutations') does not exist
! goal: absolute_file_name(extension('random_permutations/random_permutations'),_79247,[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 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),_104533,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/kernel_tools.pl')])
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_debug_watch_flag,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_safe_mode,true)
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(kernel_waitflags) does not exist
! goal: absolute_file_name(probsrc(kernel_waitflags),_106677,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/runtime_profiler.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(tools) does not exist
! goal: absolute_file_name(probsrc(tools),_120337,[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),_120049,[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),_120337,[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(eventhandling) does not exist
! goal: absolute_file_name(probsrc(eventhandling),_159141,[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),_160947,[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 chrsrc(chr_integer_inequality) does not exist
! goal: absolute_file_name(chrsrc(chr_integer_inequality),_221739,[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(closures) does not exist
! goal: absolute_file_name(probsrc(closures),_221739,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/memoization.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(preferences) does not exist
! goal: absolute_file_name(probsrc(preferences),_227709,[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:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_use_timer,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_debug_watch_flag,true)
! Existence error in argument 1 of absolute_file_name/3
! file extension('counter/counter') does not exist
! goal: absolute_file_name(extension('counter/counter'),_217749,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/state_space.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file extrasrc(external_functions_reals) does not exist
! goal: absolute_file_name(extrasrc(external_functions_reals),_216985,[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),_216985,[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 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),_218601,[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),_212197,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/external_functions.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(kernel_reals) does not exist
! goal: absolute_file_name(probsrc(kernel_reals),_207923,[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),_202229,[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),_185317,[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'),_185317,[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),_178775,[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'),_178921,[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),_178775,[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'),_182055,[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'),_178921,[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),_179063,[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),_166553,[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(error_manager) does not exist
! goal: absolute_file_name(probsrc(error_manager),_159141,[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(eventhandling) does not exist
! goal: absolute_file_name(probsrc(eventhandling),_155719,[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(bsyntaxtree) does not exist
! goal: absolute_file_name(probsrc(bsyntaxtree),_156007,[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),_124611,[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 probsrc(b_state_model_check) does not exist
! goal: absolute_file_name(probsrc(b_state_model_check),_120195,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/b_read_write_info.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(bmachine_eventb) does not exist
! goal: absolute_file_name(probsrc(bmachine_eventb),_112797,[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(kernel_waitflags) does not exist
! goal: absolute_file_name(probsrc(kernel_waitflags),_104533,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/delay.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(performance_messages) does not exist
! goal: absolute_file_name(probsrc(performance_messages),_104533,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/b_compiler.pl')])
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_safe_mode,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_safe_mode,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(no_wd_checking,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_data_validation_mode,xxxtrue)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_data_validation_mode,true)
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(bsyntaxtree) does not exist
! goal: absolute_file_name(probsrc(bsyntaxtree),_79247,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/custom_explicit_sets.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file extension('counter/counter') does not exist
! goal: absolute_file_name(extension('counter/counter'),_53393,[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),_47699,[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),_44135,[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),_14869,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/bsyntaxtree.pl')])
* Non-determinate: b_global_sets:is_b_global_constant/3 (clause 1)
* Calls nondet predicate b_global_sets:b_global_constant/3 .
* Non-determinate: b_global_sets:is_unused_b_global_constant/2 (clause 1)
* Calls nondet predicate b_global_sets:between/3 .
* Non-determinate: b_global_sets:is_used_b_global_constant/3 (clause 1)
* Calls nondet predicate b_global_sets:used_b_global_constant/3 .
! warning: predicate b_global_sets:b_global_constant_hash/4 is dynamic.
! Some nondeterminism may have been missed.
! Add (or move) the directive
! :- dynamic b_global_sets:b_global_constant_hash/4 .
! near the top of this file.
* Non-determinate: b_global_sets:b_global_set/1 (clause 1)
* This clause contains a disjunction not forced to be deterministic.
* Non-determinate: b_global_sets:b_check_and_precompile_enumerated_sets/0 (clause 2)
* Calls nondet predicate b_global_sets:debug_nl/1 .
* Non-determinate: b_global_sets:b_check_and_precompile_deferred_sets/0 (clause 3)
* Calls nondet predicate b_global_sets:debug_nl/1 .
* Non-determinate: b_global_sets:enumerated_sets_precompiled/0 (clause 1)
* Calls nondet predicate b_global_sets:precompilation_phase/1 .
* Non-determinate: b_global_sets:deferred_sets_precompiled/0 (clause 1)
* Calls nondet predicate b_global_sets:precompilation_phase/1 .
* Non-determinate: b_global_sets:precompile_global_set/1 (clause 1)
* Calls nondet predicate b_global_sets:debug_print/2 .
* Non-determinate: b_global_sets:b_check_and_precompile_global_set_symmetry/0 (clause 2)
* Calls nondet predicate b_global_sets:debug_println/2 .
! warning: predicate b_global_sets:global_set_user_defined_scope/2 is dynamic.
! Some nondeterminism may have been missed.
! Add (or move) the directive
! :- dynamic b_global_sets:global_set_user_defined_scope/2 .
! near the top of this file.
* Non-determinate: b_global_sets:inline_prob_deferred_set_elements_into_bexpr/2 (clause 1)
* Calls nondet predicate b_global_sets:debug_println/2 .
* Non-determinate: b_global_sets:prob_deferred_set_element/4 (clause 1)
* Calls nondet predicate b_global_sets:debug_format/3 .
! warning: predicate b_global_sets:b_supplementary_global_set/1 is dynamic.
! Some nondeterminism may have been missed.
! Add (or move) the directive
! :- dynamic b_global_sets:b_supplementary_global_set/1 .
! near the top of this file.
! warning: predicate b_global_sets:b_replaced_global_set/2 is dynamic.
! Some nondeterminism may have been missed.
! Add (or move) the directive
! :- dynamic b_global_sets:b_replaced_global_set/2 .
! near the top of this file.
! warning: predicate b_global_sets:enumerated_set/1 is dynamic.
! Some nondeterminism may have been missed.
! Add (or move) the directive
! :- dynamic b_global_sets:enumerated_set/1 .
! near the top of this file.
! warning: predicate b_global_sets:fixed_deferred_set_size/2 is dynamic.
! Some nondeterminism may have been missed.
! Add (or move) the directive
! :- dynamic b_global_sets:fixed_deferred_set_size/2 .
! near the top of this file.
! warning: predicate b_global_sets:extract_setsize_from_machine_cache/3 is dynamic.
! Some nondeterminism may have been missed.
! Add (or move) the directive
! :- dynamic b_global_sets:extract_setsize_from_machine_cache/3 .
! near the top of this file.
! warning: predicate b_global_sets:find_minimum_cardinality_cache/2 is dynamic.
! Some nondeterminism may have been missed.
! Add (or move) the directive
! :- dynamic b_global_sets:find_minimum_cardinality_cache/2 .
! near the top of this file.
* Non-determinate: b_global_sets:generate_fresh_supplementary_global_set/1 (clause 1)
* Calls nondet predicate b_global_sets:debug_println/2 .
* Non-determinate: b_global_sets:extract_setsize_from_machine/3 (clause 4)
* Calls nondet predicate b_global_sets:debug_format/3 .
* Non-determinate: b_global_sets:extract_DEFERRED_setsize_from_machine/3 (clause 4)
* Calls nondet predicate b_global_sets:debug_println/2 .
* Non-determinate: b_global_sets:extract_DEFERRED_setsize_from_machine/3 (clause 5)
* Calls nondet predicate b_global_sets:debug_println/2 .
* Non-determinate: b_global_sets:find_maximum_cardinality2/4 (clause 1)
* Indexing cannot distinguish this from clause 2.
* Non-determinate: b_global_sets:find_maximum_cardinality2/4 (clause 2)
* Indexing cannot distinguish this from clause 3.
* Non-determinate: b_global_sets:get_equality/4 (clause 1)
* This clause contains a disjunction not forced to be deterministic.
* Non-determinate: b_global_sets:get_card_upper_bound/3 (clause 1)
* This clause contains a disjunction not forced to be deterministic.
* Non-determinate: b_global_sets:maximum_cardinality_of_identifier/3 (clause 2)
* Indexing cannot distinguish this from clause 3.
* Non-determinate: b_global_sets:find_minimum_cardinality/2 (clause 2)
* Calls nondet predicate b_global_sets:debug_println/2 .
* Non-determinate: b_global_sets:find_minimum_cardinality2/4 (clause 1)
* Indexing cannot distinguish this from clause 2.
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(error_manager) does not exist
! goal: absolute_file_name(probsrc(error_manager),_178165,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/partition_detection.pl')])
* Non-determinate: b_global_sets:find_minimum_cardinality3/4 (clause 1)
* Indexing cannot distinguish this from clause 2.
* Non-determinate: b_global_sets:find_minimum_cardinality3/4 (clause 2)
* Indexing cannot distinguish this from clause 3.
* Non-determinate: b_global_sets:find_minimum_cardinality3/4 (clause 3)
* Indexing cannot distinguish this from clause 4.
* Non-determinate: b_global_sets:is_surjection/3 (clause 1)
* Indexing cannot distinguish this from clause 2.
* Non-determinate: b_global_sets:is_surjection/3 (clause 2)
* Indexing cannot distinguish this from clause 3.
* Non-determinate: b_global_sets:is_surjection/3 (clause 3)
* Indexing cannot distinguish this from clause 4.
* Non-determinate: b_global_sets:is_surjection/3 (clause 4)
* Indexing cannot distinguish this from clause 5.
* Non-determinate: b_global_sets:inequality_aux/5 (clause 1)
* Indexing cannot distinguish this from clause 2.
* Non-determinate: b_global_sets:inequality_aux/5 (clause 2)
* Indexing cannot distinguish this from clause 6.
* Non-determinate: b_global_sets:inequality_aux/5 (clause 3)
* Indexing cannot distinguish this from clause 6.
* Non-determinate: b_global_sets:inequality_aux/5 (clause 4)
* Indexing cannot distinguish this from clause 6.
* Non-determinate: b_global_sets:inequality_aux/5 (clause 4)
* Calls nondet predicate b_global_sets:select/3 .
* Non-determinate: b_global_sets:inequality_aux/5 (clause 5)
* Indexing cannot distinguish this from clause 6.
* Non-determinate: b_global_sets:inequality_aux/5 (clause 6)
* Calls nondet predicate b_global_sets:select/3 .
* Non-determinate: b_global_sets:all_different/4 (clause 1)
* This clause contains a disjunction not forced to be deterministic.
* Non-determinate: b_global_sets:set_extension_list/3 (clause 1)
* Indexing cannot distinguish this from clause 2.
* Non-determinate: b_global_sets:equality/3 (clause 1)
* This clause contains a disjunction not forced to be deterministic.
* Non-determinate: b_global_sets:is_equality_card_expression/4 (clause 1)
* This clause contains a disjunction not forced to be deterministic.
* Non-determinate: b_global_sets:evaluable_integer_expression/3 (clause 2)
* Calls nondet predicate preferences:preference/2 .
* Non-determinate: b_global_sets:evaluable_integer_expression/3 (clause 3)
* Calls nondet predicate preferences:preference/2 .
* Non-determinate: b_global_sets:is_greaterequalthan_card_global_set_id/5 (clause 1)
* Indexing cannot distinguish this from clause 2.
* Non-determinate: b_global_sets:is_greaterequalthan_card_global_set_id/5 (clause 1)
* This clause contains a disjunction not forced to be deterministic.
* Non-determinate: b_global_sets:is_greaterequalthan_card_global_set_id/5 (clause 2)
* Indexing cannot distinguish this from clause 3.
* Non-determinate: b_global_sets:is_greaterequalthan_card_global_set_id/5 (clause 2)
* This clause contains a disjunction not forced to be deterministic.
* Non-determinate: b_global_sets:get_value_bound/3 (clause 1)
* Indexing cannot distinguish this from clause 2.
! warning: predicate b_global_sets:start_extracting_setsize/1 is dynamic.
! Some nondeterminism may have been missed.
! Add (or move) the directive
! :- dynamic b_global_sets:start_extracting_setsize/1 .
! near the top of this file.
* Non-determinate: b_global_sets:fixed_finite_deferred_set_size/2 (clause 1)
* Calls nondet predicate b_global_sets:fixed_deferred_set_size/2 .
* Non-determinate: b_global_sets:pre_register_enumerated_set_with_elems/2 (clause 1)
* Calls nondet predicate b_global_sets:debug_format/3 .
* Non-determinate: b_global_sets:pre_register_enumerated_set/1 (clause 1)
* Calls nondet predicate b_global_sets:debug_format/3 .
* Non-determinate: b_global_sets:is_b_precompiled_globalset/1 (clause 1)
* Calls nondet predicate b_global_sets:extract_setsize_from_machine_cache/3 .
* Non-determinate: b_global_sets:b_integer_or_real_or_string_set/1 (clause 1)
* Indexing cannot distinguish this from clause 4.
* Non-determinate: b_global_sets:b_integer_or_real_or_string_set/1 (clause 2)
* Indexing cannot distinguish this from clause 4.
* Non-determinate: b_global_sets:b_integer_or_real_or_string_set/1 (clause 3)
* Indexing cannot distinguish this from clause 4.
* Non-determinate: b_global_sets:b_integer_or_real_set/1 (clause 1)
* Indexing cannot distinguish this from clause 3.
* Non-determinate: b_global_sets:b_integer_or_real_set/1 (clause 2)
* Indexing cannot distinguish this from clause 3.

Name: fail
Name: assertz/1
Name: term_hash/2	Module: terms
Name: is/2
Name: true
Name: add_internal_error/2	Module: foo_error
Name: =/2
Name: ->/3
Name: lookup_global_constant/2	dynamic predicate
Name: nth0/3	Module: foo_error
Name: add_error_fail/3	Module: foo_error
Name: b_global_constant/3	dynamic predicate

Name: pre_register_enumerated_set_with_elems/2	Module: b_global_sets
Name: extract_setsize_from_machine/3	Module: b_global_sets
Name: assert_enumerated_set/4	Module: b_global_sets

Name: assertz/1
Name: add_warning/3	Module: foo_error
Name: b_integer_or_real_or_string_set/1	Module: b_global_sets
Name: ->/3
Name: add_internal_error/2	Module: foo_error
Name: b_precompiled_global_set/1	Module: b_global_sets

Name: =/2
Name: add_internal_error/2	Module: foo_error
Name: findall/4
Name: !
Name: is_list/1	Module: foo_error

Name: extend_state_with_probids_and_lets/2	Module: eval_let_store
Name: eval_formula_in_state/4	Module: external_functions
Name: get_expanded_bstate/2	Module: visb_visualiser
Name: translate_json_para/4	Module: b_intelligent_trace_replay
Name: check_additional_guard_when_bound/6	Module: b_interpreter
Name: find_successor_state/4	Module: b_trace_checking
Name: inline_prob_deferred_set_elements_into_bexpr/2	Module: b_global_sets
Name: execute_operation_by_predicate_in_state2/7	Module: b_state_model_check
Name: test_formula_in_state/4	Module: external_functions
Name: get_bstate_with_deferred_sets/5	Module: prob2_interface
Name: get_tree_from_expr/4	Module: bvisual
Name: predicate_satisfiable5/5	Module: b_state_model_check

Name: length/2
Name: evaluable_integer_expression/3	Module: b_global_sets
Name: set_extension_list/3	Module: b_global_sets
Name: get_texpr_type/2	Module: foo_error
Name: =/2

Name: normalise2/2	Module: store
Name: translate_b_constant/2	Module: xtl_interface
Name: rewrite_set_aux/6	Module: set_rewriter
Name: dot_state_node/6	Module: visualize_graph
Name: create_atoms_for_type/7	Module: kodkod2
Name: source_code_for_identifier/6	Module: bmachine
Name: set_of_values/2	Module: state_permuter
Name: rewrite_value/4	Module: set_rewriter

Name: findall/3
Name: gen_enum_warning_wf/6	Module: kernel_objects
Name: get_preference/2	Module: foo_error
Name: =/2
Name: ->/3
Name: b_get_fd_type_bounds/3	Module: b_global_sets
Name: !
Name: RECURSIVE_CALL/3	Module: b_global_sets
Name: gen_int_set/3	Module: b_global_sets
Name: all_strings_wf/2	Module: kernel_objects

Name: all_elements_of_type_rand2/3	Module: b_global_sets
Name: all_elements_of_type_wf/3	Module: b_global_sets

Name: all_elements_of_type2/3	Module: b_global_sets
Name: findall/3
Name: b_get_fd_type_bounds/3	Module: b_global_sets
Name: !
Name: b_global_set/1	Module: b_global_sets

Name: expand_custom_set_wf/4	Module: custom_explicit_sets
Name: all_elements_of_type/2	Module: b_global_sets
Name: expand_only_custom_closure_global/4	Module: custom_explicit_sets

Name: add_named_constants_to_global_set/3	Module: b_global_sets
Name: assert_extract_setsize_from_machine_cache/3	Module: b_global_sets
Name: length/2
Name: =/2
Name: pre_register_enumerated_set/1	Module: b_global_sets

Name: debug_nl/1	Module: foo_error
Name: assertz/1
Name: retractall/1
Name: fail
Name: precompile_global_set/1	Module: b_global_sets
Name: b_get_named_machine_set/2	Module: bmachine
Name: not/1
Name: b_get_machine_set/1	Module: bmachine
Name: debug_print/2	Module: foo_error
Name: debug_println/2	Module: foo_error
Name: check_enumerated_set_scope/1	Module: b_global_sets
Name: add_internal_error/2	Module: foo_error
Name: true
Name: enumerated_sets_precompiled/0	Module: b_global_sets
Name: ->/3
Name: deferred_sets_precompiled/0	Module: b_global_sets

Name: reset_global_set_user_defined_scope/0	Module: b_global_sets
Name: debug_nl/1	Module: foo_error
Name: true
Name: debug_println/2	Module: foo_error
Name: assertz/1
Name: b_global_set_with_potential_symmetry/1	Module: b_global_sets
Name: ->/3
Name: fail
Name: avl_fetch/2	Module: avl
Name: is_b_global_constant_hash/3	Module: b_global_sets
Name: nl
Name: print/1
Name: user_forced_symmetry/1	Module: b_global_sets
Name: is_b_global_constant/3	Module: b_global_sets
Name: ->/2
Name: b_extract_fd_type/3	Module: b_global_sets
Name: find_all_used_enumerated_elements/1	Module: b_global_sets
Name: add_internal_error/2	Module: foo_error
Name: precompilation_phase/1	dynamic predicate
Name: retract/1

Name: retractall/1
Name: b_reset_global_set_type_definitions/0	Module: b_global_sets

Name: create_z_machine/8	Module: proz
Name: b_machine_reset/0	Module: bmachine
Name: run_testcase/4	Module: test_typechecker

Name: non_empty_type/1	Module: typing_tools
Name: is_empty_explicit_set/1	Module: custom_explicit_sets
Name: test_empty_explicit_set_wf/3	Module: custom_explicit_sets

Name: b_preference_par/3	Module: specfile
Name: b_global_set_cardinality/2	Module: b_global_sets
Name: try_get_finite_max_card_from_ground_value/2	Module: custom_explicit_sets

Name: b_get_fd_type_bounds_limited/3	Module: b_global_sets
Name: global_type2/2	Module: b_global_sets
Name: not_element_of_wf/3	Module: kernel_objects
Name: inst2/2	Module: typing_tools
Name: ordered_value/2	Module: kernel_ordering
Name: reify_avl_mem2/5	Module: custom_explicit_sets
Name: b_fd_card/2	Module: b_global_sets
Name: b_get_fd_type_bounds_with_enum_warning/6	Module: b_global_sets
Name: all_elements_of_type_rand2/3	Module: b_global_sets
Name: equality_fd_objects/4	Module: kernel_equality
Name: enum_global_type_limited/2	Module: b_global_sets
Name: prob_deferred_set_element/4	Module: b_global_sets
Name: all_elements_of_type2/3	Module: b_global_sets
Name: global_type_wf/3	Module: b_global_sets
Name: global_type/2	Module: b_global_sets

Name: =/2
Name: add_message/3	Module: foo_error
Name: ->/3
Name: b_get_fd_type_bounds/3	Module: b_global_sets

Name: get_top_level_symmetry_breaking_predicates_decomposed/2	Module: smt_symmetry_breaking
Name: setup_sets/3	Module: smt_solvers_interface
Name: add_symmetry_breaking_predicates/2	Module: smt_symmetry_breaking

Name: inf_greater/2	Module: b_global_sets
Name: extract_setsize_from_machine_cache/3	Module: b_global_sets
Name: b_global_deferred_set/1	Module: b_global_sets

Name: marker/3	Module: symmetry_marker
Name: count_obj/4	Module: symmetry_marker
Name: permute_value/4	Module: state_permuter
Name: b_global_set_with_potential_symmetry/1	Module: b_global_sets
Name: not_symmetric/1	Module: symmetry_marker

Name: is_global_set_id/2	Module: well_def_prover
Name: print_sets/0	Module: prob_cli
Name: unfixed_deferred_set/1	Module: b_global_sets
Name: b_partially_deferred_set/1	Module: b_global_sets
Name: b_global_deferred_set/1	Module: b_global_sets
Name: is_global_type_variable_name/3	Module: model_translation
Name: is_base_expression2/1	Module: kodkod
Name: translate_b_constant/2	Module: xtl_interface
Name: b_extract_fd_type/3	Module: b_global_sets
Name: prob_deferred_set_element/4	Module: b_global_sets
Name: unfixed_deferred_set_exists/0	Module: b_global_sets
Name: lookup_identifier/3	Module: b2setlog
Name: try_b_type2global_set/2	Module: b_global_sets
Name: b_preference_par/3	Module: specfile
Name: dot_subgraph/3	Module: visualize_graph
Name: register_replaced_global_set/2	Module: b_global_sets
Name: dot_state_node/6	Module: visualize_graph
Name: z3_type_to_b_type/2	Module: model_translation
Name: all_elements_of_type_rand2/3	Module: b_global_sets
Name: enum_global_type_limited/2	Module: b_global_sets
Name: b_global_set_with_potential_symmetry/1	Module: b_global_sets
Name: do_not_prime_identifier/1	Module: predicate_handling
Name: contains_invalid_user_set/1	Module: eval_let_store
Name: is_a_machine_identifier/1	Module: eval_let_store

Name: compute_card_of_set/4	Module: well_def_prover
Name: is_definitely_maximal_list/2	Module: custom_explicit_sets
Name: maximal_set_extension/2	Module: well_def_prover
Name: finite_value/3	Module: b_enumerate
Name: card_for_specific_custom_set/3	Module: custom_explicit_sets
Name: explicit_set_cardinality_wf/3	Module: custom_explicit_sets
Name: max_type_cardinality/2	Module: predicate_analysis

prob_prolog/src/b_global_sets.pl

Modules

Predicates of b_global_sets

Module Information

1535 Lines

142 Predicates

Imported Modules: debug tools lists ordsets self_check preferences error_manager bsyntaxtree fd_utils_clpfd

62 Exports

28 specified Imports

Predicates:

Name: fail
Name: true
Name: \=/2
Name: is_unused_b_global_constant/2	Module: b_global_sets
Name: ->/3
Name: b_global_deferred_set_with_card_gt1/1	Module: b_global_sets
Name: b_global_set/1	Module: b_global_sets

Name: non_symmetric_type/1	Module: symmetry_marker
Name: b_check_and_precompile_global_set_symmetry/0	Module: b_global_sets

Name: add_new_global_set/1	Module: b_global_sets
Name: normalise2/2	Module: store

Name: equality_explicit_sets_wf/4	Module: custom_explicit_sets
Name: b_integer_or_real_or_string_set/1	Module: b_global_sets
Name: b_integer_or_real_set/1	Module: b_global_sets
Name: equal_explicit_sets4/4	Module: custom_explicit_sets

Name: not_empty_value/1	Module: bsyntaxtree
Name: is_non_empty_explicit_set_wf/2	Module: custom_explicit_sets

Name: initialise_node_colours/0	Module: graph_iso_nauty
Name: portray_global_sets/0	Module: b_global_sets

Name: extract_setsize_from_machine/3	Module: b_global_sets
Name: abstract_type/4	Module: prob_rule_compiler
Name: b_global_set/1	Module: b_global_sets

Name: translate_z3_expr/4	Module: model_translation
Name: construct_complement_closure_if_necessary/3	Module: custom_explicit_sets

Name: true
Name: add_error/4	Module: foo_error
Name: =\=/2
Name: get_user_defined_scope/4	Module: b_global_sets
Name: ->/3

Name: list_contains_unfixed_deferred_set_id/1	Module: b_global_sets
Name: unfixed_typed_id_in_list/3	Module: solver_interface