custom_explicit_sets.pl

add_id_pairs([],_,R,R).

add_id_pairs([Key|T],LastX,AVL,Res) :-
    (Key = (X,Y) -> true ; add_error_and_fail(add_id_pairs,'Not a relation element: ',Key)),
    (X=Y -> AVL2=AVL /* must already be in closure1 result */
    ; (LastX==X -> AVL1=AVL ; avl_store((X,X),AVL,true,AVL1)), % already added
    avl_store((Y,Y),AVL1,true,AVL2)
    ),
    add_id_pairs(T,X,AVL2,Res).

check_interval_in_avl(Low,Up,A,WF) :-
    Low \== minus_inf,
    Up \== inf,
    b_interpreter_check:check_arithmetic_operator('<=',Low,Up,LeqRes),
    print(check_interval_in_avl(LeqRes,Low,Up,A)),nl,
    (var(LeqRes) -> get_binary_choice_wait_flag_exp_backoff(16,check_interval_in_avl,WF,WF2) ; true),
    check_interval_in_avl_aux(LeqRes,Low,Up,A,WF2).

check_interval_in_avl(Low,Up,A,WF) :-
    Low \== minus_inf,
    Up \== inf,
    b_interpreter_check:check_arithmetic_operator('<=',Low,Up,LeqRes),
    %print(check_interval_in_avl(LeqRes,Low,Up,A)),nl,
    (var(LeqRes) -> get_binary_choice_wait_flag_exp_backoff(16,check_interval_in_avl,WF,WF2) ; true),
    check_interval_in_avl_aux(LeqRes,Low,Up,A,WF2).

check_interval_in_avl_aux(P,Low,Up,CS,WF2) :- print(check_interval_in_avl_aux(P,Low,Up,CS,WF2)),nl,fail.

check_interval_in_avl_aux(pred_true,Low,Up,CS,_WF2) :- print(not_empty),nl,
    element_of_custom_set_wf(int(Low),CS,WF),
    element_of_custom_set_wf(int(Up),CS,WF),
    interval_in_avl_block(Low,Up,CS,WF).

check_interval_in_avl_aux(pred_false,_Low,_Up,_CS,_WF2) :- print(empty),nl. % Interval is empty; but infinitely many solutions for Low and Up

check_interval_in_avl_aux(pred_true,Low,Up,A,_WF2) :- %print(not_empty),nl,
    element_of_avl_set_wf(A,int(Low),WF),
    element_of_avl_set_wf(A,int(Up),WF),
    interval_in_avl_block(Low,Up,A).

check_interval_in_avl_aux(pred_false,_Low,_Up,_A,_WF2) :- print(empty),nl. % Interval is empty; but infinitely many solutions for Low and Up

closure0_for_explicit_set(avl_set(A),Res) :-
    avl_domain(A,List),
    closure1_for_explicit_set(avl_set(A),Res1),
    (Res1==[] -> A2=empty ; Res1 = avl_set(A2)),
    add_id_pairs(List,none,A2,A3),
    construct_avl_set(A3,S3),
    kernel_objects:equal_object(Res,S3,closure0_for_explicit_set).

image_for_closure([X,Y],[_TX,TY],Pred,Set,Res,WF) :-
    singleton_set(Set,SX),
    nonvar(SX), % otherwise it may be better to use standard image propagation
    % e.g., testcase 1536 sqr = %x.(x>=0|x*x) & (sqr)[{xx,vv}] = {2500}
    % TO DO: improve equal_explicit_sets so that 1536 also works without nonvar(SX) test above; do we need this rule for singleton_sets anyway ?
    % what if Y=_lambda_result_
    !,
    b_compiler:b_compile(Pred,[Y],[],[bind(X,SX)],NewPred,WF),
    % compilation avoids introduction of let_predicate
    % Res = closure([Y],[TY],NewPred).
    construct_closure_if_necessary([Y],[TY],NewPred,Res).

in_closure0_membership_test_wf((A,B),CSRelation,MemRes,WF) :-
    equality_objects_wf(A,B,MemRes1,WF),
    (MemRes1==pred_true -> MemRes=pred_true
    ; in_closure1_membership_test_wf((A,B),CSRelation,MemRes2,WF),
    b_interpreter_check:disjoin(MemRes1,MemRes2,MemRes,priority(1),priority(1000),WF)
).

interval_in_avl_block(Low,Up,A) :- %print(interval_in_avl_block(Low,Up,A)),nl,
    Low1 is Low+1, interval_in_avl_loop(Low1,Up,A).

interval_in_avl_block(Low,Up,CS,WF) :- %print(interval_in_avl_block(Low,Up,CS)),nl,
    Low1 is Low+1, interval_in_avl_loop(Low1,Up,CS,WF).

interval_in_avl_loop(Low,Up,_A) :- Low>=Up,!. % Lower bound and upper bound already checked

interval_in_avl_loop(Low,Up,A) :- %print(chck(Low,Up,A)),nl,
    safe_avl_member(int(Low),A), L1 is Low+1, interval_in_avl_loop(L1,Up,A).

interval_in_avl_loop(Low,Up,_CS,_WF) :- Low>=Up,!. % Lower bound and upper bound already checked

interval_in_avl_loop(Low,Up,CS,WF) :- %print(chck(Low,Up,CS)),nl,
    element_of_custom_set_wf(int(Low),CS,WF), L1 is Low+1,
    interval_in_avl_loop(L1,Up,CS,WF).

relational_reflexive_closure(Relation,Result) :-
    try_expand_and_convert_to_avl_with_check(Relation,ARelation,relational_reflexive_closure),
    relational_reflexive_closure2(ARelation,Result).

relational_reflexive_closure2(ARelation,Result) :- % print_term_summary(closure(ARelation,Result)),
    (closure0_for_explicit_set(ARelation,Res)
    -> kernel_objects:equal_object(Res,Result)
    ; (expand_custom_set_to_list(ARelation,ERelation,_,relational_reflexive_closure2),
    is_full_relation(ERelation,WaitVar),
    compute_trans_closure(ERelation,Result1,WaitVar),
    % print(adding_id(ERelation,Result1)),nl,
    rel_iterate0(ERelation,Result1,Result)
%, print(done(Result)),nl
)
).

union_of_avl(A1,A2,ARes) :- MaxDiff=4,
    avl_tools:avl_height_compare_up_to(A1,A2,MaxDiff,SmHeight,Res),
    (SmHeight =< 2 -> union_of_avl2(A1,A2,ARes)
    ; Res =eq -> union_of_avl2(A1,A2,ARes)
    ; Res=lt -> union_of_avl1(A2,A1,ARes)
    ; union_of_avl1(A1,A2,ARes)).

union_of_avl1(A1,A2,ARes) :- %Sz2>2, Sz1 =< Sz2+3, % difference not too big; Sz2 at least a certain size
    %!,
    print(union(Sz1,Sz2)),nl,
    avl_to_list(A2,List2), % get all members
    avl_to_list(A1,List1),
    ord_union(List1,List2,L12),
    ord_list_to_avl(L12,ARes).

union_of_avl2(A1,A2,ARes) :- % this version is better when A2 is small compared to A1
    avl_domain(A2,List2), % get all members
    add_to_avl(List2,A1,ARes).