append_sequence(Seq,El,Res,WF) :- nonvar(Res),is_custom_explicit_set_nonvar(Res), % we know result: deconstruct into last El and front Seq front_sequence_custom_explicit_set(Res,Last,Front), !, equal_object_wf(El,Last,append_sequence,WF), equal_sequence(Seq,Front,WF).
apply_closure_to_nonvar_groundx(X,Y,P,T,B,Span,WF) :- kernel_tools:ground_bexpr(B), !, % then if the element of function succeeds there is no need to check WD if(check_element_of_function_closure(X,Y,P,T,B,WF), true, % No need to check for well-definedness; no pending choice points apply_closure_to_nonvar_wd_check(X,P,T,B,Span,WF) % here we need to check; it could be that the result Y was instantiated ).
apply_to(R,X,Y,_FunctionType,Span,WF) :- % we could check if WD condition discharged in Span (\+ preferences:preference(find_abort_values,false) ; preference(data_validation_mode,true)), !, apply_to_var_block_abort(R,X,Y,R,Span,WF). % we have to know R before we can do anything
apply_to4(EqResX,EqResY,Y2, Tail,X,Y,InitialRel,Span,WF) :- var(EqResX),!, % Tail bound (Tail == [] -> (preferences:preference(find_abort_values,false) -> EqResX = pred_true, apply_to4(EqResX,EqResY,Y2, Tail,X,Y,InitialRel,Span,WF) ; apply_to4_block(EqResX,EqResY,Y2, Tail,X,Y,InitialRel,Span,WF) ) ; Tail = avl_set(_) -> apply_to4_block(EqResX,EqResY,Y2, Tail,X,Y,InitialRel,Span,WF) % TO DO: improve ! (e.g., expand to list if small or check if X can be in domain,...) ; Tail = closure(_,_,_) -> apply_to4_block(EqResX,EqResY,Y2, Tail,X,Y,InitialRel,Span,WF) ; Tail \= [_|_] -> add_internal_error('Illegal Tail: ',apply_to4(EqResX,EqResY,Y2, Tail,X,Y,InitialRel,Span,WF)),fail ; Tail = [(X3,Y3)|T3], % setup equality check with X3, purpose: detect, e.g., when no other element in tail can match we can force EqResX to pred_true apply_to4_call5(EqResX,EqResY,Y2, Tail,X,Y,InitialRel,Span,WF, X3,Y3,T3) ).
apply_to4_call5(EqResX,EqResY,Y2, _Tail,X,Y,InitialRel,Span,WF, X3,Y3,T3) :- % X3 must now be bound equality_objects_wf(X3,X,EqRes3,WF), apply_to5(EqResX,EqResY,EqRes3, Y2,X3,Y3,T3, X,Y, InitialRel,Span,WF).
apply_to5(EqRes,EqResY,EqRes3, Y2,_X3,Y3,T3, X,Y, InitialRel,Span,WF) :- var(EqRes),!, % EqRes3 and T3 must be known; TO DO: improve predicate so that we have to wait on T3 only when EqRes3=pred_false (EqRes3 = pred_false -> % we cannot match next element, move tail one forward (T3 = [] -> EqRes=pred_true ; true), apply_to4(EqRes,EqResY,Y2,T3,X,Y,InitialRel,Span,WF) ; /* EqRes3 = pred_true */ % we match the next entry in the list; discard Y2 and jump to (X3,Y3) and return as solution equal_object_wf(Y3,Y,apply_to6,WF), optional_functionality_check(T3,X,WF), % TO DO: we could also do equality_objects if necessary between Y and Y3, as in apply_to4 for Y and Y2 opt_force_false(EqRes) ).
apply_to5(pred_false,_EqResY,EqRes3, _Y2,_X3,Y3,T3, X,Y, InitialRel,Span,WF) :- (var(EqRes3) -> % it can be that EqRes3 is about to be triggered equality_objects_wf(Y3,Y,EqResY3,WF), prop_apply_eqxy(EqResY3,EqRes3) % propagate: if Y/=Y3 => X/=X3 ; EqResY3=not_called), apply_to4(EqRes3,EqResY3,Y3, T3,X,Y,InitialRel,Span,WF).
apply_to_nonvar([(X2,Y2)|T],X,Y,InitialRel,Span,WF) :- equality_objects_wf(X2,X,EqRes,WF), % this check on Y2 below is important if both Y and Y2 are instantiated but X,X2 not yet % example: aload_R07_cbc.mch (Savary) or cbc_sequence check for R08_ByteArray for aload_R07 event (test 1349) % however: slows down test 583 ! (var(EqRes) -> equality_objects_wf(Y2,Y,EqResY,WF), prop_apply_eqxy(EqResY,EqRes) % propagate: if Y/=Y2 => X/=X2 ; EqResY=not_called), apply_to4(EqRes,EqResY,Y2,T,X,Y,InitialRel,Span,WF).
apply_to_nonvar(closure(P,T,B),X,Y,_InitialRel,Span,WF) :- %is_custom_explicit_set(Closure,apply), % should also work for avl_set,... (is_memoization_closure(P,T,B,MemoID) % Function application with memoization; currently enabled by add /*@desc memo */ pragma to abstract constant -> apply_to_memoize(MemoID,P,T,B,X,Y,Span,WF) ; is_recursive_closure(P,T,B) % TO DO: maybe we should do the same for functions marked as memoize symbolic/uni-directional/computed ? (although we have new rule for check_element_of_function_closure which makes this redundant ??) -> % print_term_summary(apply_recursive_closure(X,P,T,B)), %hit_profiler:add_profile_hit(rec_apply_closure_to_nonvar(X,Y,P,T,B,Span,WF)), ground_value_check(X,XV), block_apply_closure_to_nonvar_groundx(XV,X,Y,P,T,B,Span,WF) ; %hit_profiler:add_profile_hit(apply_closure_to_nonvar(X,Y,P,T,B,Span,WF)), apply_closure_to_nonvar(X,Y,P,T,B,Span,WF)).
apply_to_var(R,X,Y,InitialRel,Span,WF) :- get_wait_flag(1.0,apply_to_var,WF,WF1), % see tests 1393, 1562?? % was: get_wait_flag0(WF,WF1), but see test 1706 (in conjunction for improvement for test 2033) when(((nonvar(WF1),ground(X));nonvar(R)), % only instantiate R when X sufficiently instantiated (TO DO: maybe use some for of equality_objects with existing relation R set up so far ??) (var(R) -> R=[(X,Y)|Tail], optional_functionality_check(Tail,X,WF) ; apply_to_nonvar(R,X,Y,InitialRel,Span,WF))).
card_greater_equal_check(_,_,Flag) :- nonvar(Flag),!. % no longer required; even though we could prune failure !? done later in newrange2/newdomain2 ??!!
card_greater_equal_check([],Set2,Flag) :- !,empty_set(Set2), Flag=pred_false. % Flag set indicates that both sets have same size
compute_large(Dom,Large) :- % check if the domain is large; ensure that we compute this only once (nonvar(Large) -> true ; var(Dom) -> true ; dont_expand_this_explicit_set(Dom) -> Large=large ; Large=false).
compute_trans_closure2(Relation,Result,WF) :- one_closure_iteration(Relation,Relation,Relation,Result1,WF), ( equal_object_wf(Result1,Relation,relational_trans_closure_wf,WF), % should we do equality_objects here? equal_object_optimized_wf(Result,Result1,compute_trans_closure,WF) ; % TO DO: use reification instead of is_full_relation check above ?? not_equal_object(Result1,Relation), % not a fixpoint; continue compute_trans_closure2(Result1,Result,WF) ).
concat_sequence(S1,S2,Res,WF) :- (var(S1),var(S2) -> get_wait_flag(2,concat,WF,LWF) % we have at least two solutions; TODO maybe use cardinality as wait_flag? ; LWF=1), concat_sequence2(LWF,S1,S2,Res,WF).
concat_sequence_aux(Size1,_S1,_S2,Res,WF) :- nonvar(Res),Res=avl_set(_), size_of_custom_explicit_set(Res,int(RSize),WF), number(RSize), Size1 > RSize,!, % S1 is longer than Res; no solution (prevent WD error below) fail.
concat_sequence_aux(Size1,S1,S2,Res,WF) :- nonvar(Res),Res=avl_set(_), % split Result into prefix and suffix prefix_of_custom_explicit_set(Res,Size1,Prefix,WF), % we could call versions which do not check WD suffix_of_custom_explicit_set(Res,Size1,Postfix,WF), !, equal_sequence(S1,Prefix,WF), equal_sequence(S2,Postfix,WF).
concat_sequence_aux(Size1,S1,S2,Res,WF) :- shift_seq_indexes(S2,Size1,NewS2,WF), % We can do something stronger than disjoint union: we know that the indexes are disjoint! % Hence: if (int(X),Y) : Res & (int(X),Z) : S1 => Y=Z % Hence: if (int(X),Y) : Res & (int(X),Z) : S2 => Y=Z unify_same_index_elements(S1,Res,WF), unify_same_index_elements(Res,S1,WF), unify_same_index_elements(NewS2,Res,WF), unify_same_index_elements(Res,NewS2,WF), disjoint_union_wf(S1,NewS2,Res,WF).
direct_product_tuple3(pred_true,X,Y,Z,CT,Res,WF) :- equal_cons_wf(Res,(X,(Y,Z)),CT,WF). /* no need for add_element as output uniquely determines X,Y,Z !?*/
disj_union2([X|TX],Y,Res,FullRes,WF) :- remove_element_wf(X,Res,TR,WF), % was: equal_cons_wf(Res,X,TR,WF) but error was that it could force X to be a certain value kernel_tools:ground_value_check(X,XV), (nonvar(XV) -> equal_cons_wf(Res,X,TR,WF) ; check_element_of_wf(X,FullRes,WF), % ensure that we set up proper constraints for X; e.g., for x \/ y = 1..10 & x /\ y = {} when(nonvar(XV), equal_cons_wf(Res,X,TR,WF)) ), % ensure that we instantiate Res if TR known; otherwise we may get pending co-routines, e.g. test 506, SyracuseGrammar disj_union3(TX,Y,TR,FullRes,WF).
disjoint_union0(S1,S2,Res,_F,WF,_CWF) :- ground_value(Res), ( ground_value(S1) -> !, check_subset_of_wf(S1,Res,WF), % TO DO: check if we can merge the check_subset and difference set in one predicate difference_set_wf(Res,S1,S2,WF) ; ground_value(S2) -> !, check_subset_of_wf(S2,Res,WF), difference_set_wf(Res,S2,S1,WF) ; var(S1),var(S2) -> !, % CWF nonvar % see test 1408; allows to generate subsets of Res and avoid enumeration warnings check_subset_of_wf(S1,Res,WF), %check_subset_of(S1,Res), % without waitflag: will generate ground version difference_set_wf(Res,S1,S2,WF) ).
disjoint_union_generalized_wf(ListOfSets,Res,WF) :- %expand_custom_set_to_list_wf(SetsOfSets,ESetsOfSets,_,disjoint_union_generalized_wf,WF), % this is a list of sets disjoint_union_generalized2(ListOfSets,[],Res,WF).
disjoint_union_wf(Set1,Set2,Res,WF) :- (var(Res) -> disjoint_union_wf0(Set1,Set2,DRes,DRes,WF), equal_object_optimized(Res,DRes) % try and convert result to AVL ; disjoint_union_wf0(Set1,Set2,Res,Res,WF)).
domain_restriction_wf(S,R,Res,WF) :- /* S <| R */ ok_to_try_restriction_explicit_set(S,R,Res), domain_restriction_explicit_set_wf(S,R,SR,WF),!, equal_object_wf(SR,Res,domain_restriction,WF).
domain_restriction_wf(S,R,Res,WF) :- /* S <| R */ expand_custom_set_to_list_wf(R,ER,_,domain_restriction,WF), relation_restriction_wf(ER,S,Res,pred_true,domain,WF).
domain_subtraction_wf(S,R,Res,WF) :- /* S <<| R */ ok_to_try_restriction_explicit_set(S,R,Res), domain_subtraction_explicit_set_wf(S,R,SR,WF),!, equal_object_wf(SR,Res,domain_subtraction2,WF).
domain_subtraction_wf(S,R,Res,WF) :- /* S <<| R */ expand_custom_set_to_list_wf(R,ER,_,domain_subtraction,WF), try_expand_and_convert_to_avl_with_check(S,AS,keep_intervals(500),domain_subtraction), % (ground(ER) -> domain_subtraction_acc(ER,AS,[],Res) ; relation_restriction_wf(ER,AS,Res,pred_false,domain,WF) % ) .
equal_sequence(X,Y,WF) :- nonvar(X),nonvar(Y), get_seq_head(X,XI,XEl,XT), get_seq_head(Y,YI,YEl,YT), XI==YI,!, % THIS CURRENTLY ONLY CHECKS FRONTMOST indexes equal_object_wf(XEl,YEl,equal_sequence_1,WF), equal_sequence(XT,YT,WF).
equal_sequence(X,Y,WF) :- /* (is_custom_explicit_set(Y) -> monitor_equal_sequence_againts_custom_set(X,Y,WF) ; is_custom_explicit_set(X) -> monitor_equal_sequence_againts_custom_set(Y,X,WF) ; true), does not seem to buy anything; equal_object already powerful enough */ equal_object_wf(X,Y,equal_sequence_2,WF).
event_b_identity_for_type(Type,Res,WF) :- create_texpr(identifier('_zzzz_unary'),Type,[],TIdentifier1), % was [generated] create_texpr(identifier('_zzzz_binary'),Type,[],TIdentifier2), % was [generated] (is_infinite_type(Type) -> Info = [prob_annotation('SYMBOLIC')] ; Info =[]), create_texpr(equal(TIdentifier1,TIdentifier2),pred,Info,TPred), construct_closure(['_zzzz_unary','_zzzz_binary'],[Type,Type],TPred,CRes), % for small types we could do: all_objects_of_type(Type,All), identity_relation_over_wf(All,CRes,WF) %, print(constructed_eventb_identity(Res)),nl equal_object_wf(Res,CRes,WF).
expand_and_convert_to_avl_set_catch(R,_AS,_Origin,_Operator,ResultStatus) :- is_infinite_explicit_set(R),!, % we could also use is_infinite_or_symbolic_closure ResultStatus=keep_symbolic.
expand_and_convert_to_avl_set_catch(R,AS,Origin,Operator,ResultStatus) :- on_exception(enumeration_warning(_,_,_,_,_), (expand_and_convert_to_avl_set(R,AS,Origin,Operator),ResultStatus=avl_set), (add_message(Origin,'Attempting symbolic treatment, enumeration warning occured while expanding ARG for ',Operator,b(value(R),any,[])), ResultStatus=keep_symbolic)).
expand_and_convert_to_avl_set_warn(R,AS,Origin,Operator) :- % TO DO: check for not fully instantiated closures, like memoization closures where ID not yet known % it is used before a cut: we need to expand straightaway without choice points observe_enumeration_warnings(expand_and_convert_to_avl_set(R,AS,Origin,Operator), add_message(Origin,'Enumeration warning occured while expanding argument ARG for predicate ',Operator,b(value(R),any,[]))).
force_in_domain(pred_true,A,Relation,WF) :- % force A to be in domain, avoid enumeration warnings,... % maybe only for non-ground A in_domain_wf_lazy(A,Relation,WF). % slowdown Loop.mch (tests 634, 637) if we use in_domain_wf ?
get_global_cardinality_list(global_set(G),Type,GCL,list) :- !, all_elements_of_type(G,Values), % can only work for finite sets, not for STRING, NATURAL, REAL, ... (b_integer_set(G) -> Type=integer ; Type=global(G)), findall(X-1,(get_simple_fd_value(Type,VV,X),member(VV,Values)),GCL).
get_global_cardinality_list(avl_set(A),Type,GCL,list) :- !, A = node(TopValue,_True,_,_,_), get_simple_fd_value(Type,TopValue,_), % we have CLPFD values avl:avl_domain(A,Values), findall(X-1,(get_simple_fd_value(Type,VV,X),member(VV,Values)),GCL).
get_relation_types(Value,Domain,Range) :- kernel_objects:infer_value_type(Value,VT), unify_types_strict(VT,set(couple(Domain,Range))). % deal also with seq types
global_cardinality_range([],Acc,_Type,GCL,WF) :- clpfd:global_cardinality(Acc,GCL,[consistency(value)]), add_fd_variables_for_labeling(Acc,WF). % this is needed for efficiency for NQueens40_perm !!
image1(Rel,Set,Res,WF) :- keep_symbolic(Rel), (preferences:get_preference(convert_comprehension_sets_into_closures,true), % in this case keep_symbolic is always true nonvar(Set),is_infinite_explicit_set(Set) % in this case we have to expand Rel below; what if Rel also infinite ?? --> TO DO : symbolic treatment -> debug_println(9,infinite_for_image1(Set)), fail ; true), ( dom_for_specific_closure(Rel,Domain,function(_)) -> !, expand_custom_set_to_list_wf(Set,ESet,_,image1,WF), % TO DO: what if keep_symbolic(Set) image_for_inf_fun(ESet,Domain,Rel,[],Res,WF) ; get_relation_types(Rel,DomType,RangeType),!, expand_custom_set_to_list_wf(Set,ESet,_,image1_2,WF), kernel_tools:ground_value_check(Rel,GRel), when(nonvar(GRel), image_for_large_relation(ESet,Rel,DomType,RangeType,[],Res,WF)) /* ; get_relation_types(Rel,DomType,RangeType),!, % Rel should not be expanded, compute closure by calculating {yy|#(xx).(xx:Set & xx|->yy:Rel)} print_term_summary(image_for_large_relation(DomType,RangeType,Set,Rel)),nl, image_closure(Set,Rel,DomType,RangeType,Closure ), translate:print_bvalue(Closure),nl, expand_custom_set(Closure,CRes), print(expanded),nl, equal_object(CRes,Res,image1_2) */ ).
image1(Rel,S,Res,WF) :- expand_custom_set_to_list_wf(Rel,Relation,_,image1_2,WF), % bad if Rel is a big closure ! % image_for_list_relation(Relation,S,Res). propagate_singleton_image(Relation,S,Res,WF), image_for_list_relation(Relation,S,[],Res,WF). %,print_term_summary(image2_res(Relation,S,Res)).
image5(pred_true,_Y,T,S,ImageSoFar,Res,WF) :- /* we have already added Y to the image */ image_for_list_relation(T,S,ImageSoFar,Res,WF).
image5(pred_false,Y,T,S,ImageSoFar,Res,WF) :- add_element_wf(Y,ImageSoFar,ImageSoFar2,WF), kernel_objects:mark_as_non_free(Y,image), % Y has been added to image, no longer freely choosable equal_cons_wf(Res,Y,Res2,WF), image_for_list_relation(T,S,ImageSoFar2,Res2,WF).
image_for_closure1_check_fix(_,Rel,Acc,Res1,Res,WF,FIRST) :- %try_expand_and_convert_to_avl_unless_large(Res1,ERes1), difference_set(Res1,Acc,New), try_expand_and_convert_to_avl(New,ENew), % we compute difference_set below; we most definitely will need an explicit finite representation (not_empty_set_wf(ENew,WF), union(ENew,Acc,Acc1), % Note: we do not call union_wf - should we do this % upon first iteration remove also S from New -> New2 and pass New2 to image_for_closure1_iterate % TO DO: investigate whether this also makes sense for further iterations; always remove S (FIRST=first_iteration(S) -> difference_set(ENew,S,New2) ; New2=ENew), image_for_closure1_iterate(Rel,New2,Acc1,Res,WF,not_first) ; empty_set_wf(ENew,WF),equal_object_optimized_wf(Acc,Res,image_for_closure1_check_fix,WF)).
image_for_closure1_wf_aux(Rel,S,Res,WF) :- ((nonvar(S),S=avl_set(_)) -> closure1_for_explicit_set_from(Rel,S,Closure1Rel),!, % if S is known: start from S (currently only deals with Rel=avl_set(_) range_wf(Closure1Rel,Res,WF) ; Rel=avl_set(AR), avl_height(AR,AR_Height), ((set_smaller_than(S,4),AR_Height>4) -> !, % TO DO: we could do the same for small S if Rel is large when(ground(S), (expand_and_convert_to_avl_set(S,ES,image_for_closure1_wf_aux,'closure1(ARG)[?]') -> closure1_for_explicit_set_from(Rel,avl_set(ES),Closure1Rel), range_wf(Closure1Rel,Res,WF) ; image_for_closure1_iterate(Rel,S,[],Res,WF,first_iteration(S)) )) ; % Don't do this if avl_height too large; then it is probably better to compute the image for S only AR_Height < 13, % how big should we make this magic constant; or should we time-out ? 2^14=16384 closure1_for_explicit_set(Rel,Closure1Rel),!, % we can compute it effiently; don't use code below image_wf(Closure1Rel,S,Res,WF) ) ).
image_for_inf_fun_aux(pred_true,X,T,Dom,Fun,Acc,CompRes,WF) :- apply_to(Fun,X,FX,WF), % TO DO: generalize to image so that we can apply it also to infinite relations ? add_element_wf(FX,Acc,NewAcc,WF), % will block until Acc Known !! % TO DO USE: equal_cons_wf(CompRes,FX,CT,WF) + accumulator !, image_for_inf_fun(T,Dom,Fun,NewAcc,CompRes,WF).
image_for_large_relation([XX|T],Rel,DomType,RangeType,Acc,Res,WF) :- Body = b(member(b(couple(b(value(XX),DomType,[]), b(identifier(yy),RangeType,[])),couple(DomType,RangeType),[]), b(value(Rel),set(couple(DomType,RangeType)),[])),pred,[]), % TO DO: simplify above if we have Rel = closure(P,T,B); which we usually will custom_explicit_sets:expand_normal_closure_direct([yy],[RangeType],Body,HRes,_Done,WF), % do not memoize this (many different values) union_wf(Acc,HRes,NewAcc,WF), (T == [] -> equal_object_wf(NewAcc,Res,WF) ; image_for_large_relation(T,Rel,DomType,RangeType,NewAcc,Res,WF)).
image_for_list_relation([(X,Y)|T],S,ImageSoFar,Res,WF) :- ((T==[], definitely_not_empty(Res)) -> MemRes=pred_true, % we need at least one more element for Res check_element_of_wf(X,S,WF) ; (Res==[],ImageSoFar==[]) -> MemRes=pred_false, not_element_of_wf(X,S,WF) % Result empty: X cannot be in S ; membership_test_wf(S,X,MemRes,WF) ), image4(MemRes,Y,T,S,ImageSoFar,Res,WF).
in_domain_restriction_wf(Pair,Set,Rel,WF) :- (treat_arg_symbolically(Set) ; treat_arg_symbolically(Rel) ; preference(convert_comprehension_sets_into_closures,true)), !, Rel \== [], % avoid setting up check_element_of for X then % x |-> y : Set <| Rel <=> x|->y : Rel & x: Set check_element_of_wf(Pair,Rel,WF), Pair = (P1,_), check_element_of_wf(P1,Set,WF).
in_domain_subtraction_wf(Pair,Set,Rel,WF) :- (treat_arg_symbolically(Set) ; treat_arg_symbolically(Rel) ; preference(convert_comprehension_sets_into_closures,true)), !, Rel \== [], % avoid setting up check_element_of for X then % x |-> y : Set <<| Rel <=> x|->y : Rel & x/: Set check_element_of_wf(Pair,Rel,WF), Pair = (P1,_), not_element_of_wf(P1,Set,WF).
in_domain_wf_lazy(El,Rel,WF) :- expand_custom_set_to_list_wf(Rel,Relation,Done,in_domain_wf_lazy,WF), get_binary_choice_wait_flag(in_domain_wf_lazy(El),WF,LWF), % TO DO: get_pow2_binary_choice_priority(Len,Prio), get_binary_choice_wait_flag_exp_backoff % if Done == true -> we can use maybe clpfd_inlist or clpfd:element or quick_propagate quick_propagation_domain_element_list(Done,Relation,El,WF), in_domain2(El,Relation,WF,LWF).
in_range_restriction_wf(Pair,Rel,Set,WF) :- (treat_arg_symbolically(Set) ; treat_arg_symbolically(Rel) ; preference(convert_comprehension_sets_into_closures,true)), !, Rel \== [], % avoid setting up check_element_of for X then % x |-> y : Rel |>> Set <=> x|->y : Rel & y: Set check_element_of_wf(Pair,Rel,WF), Pair = (_,P2), check_element_of_wf(P2,Set,WF).
in_range_subtraction_wf(Pair,Rel,Set,WF) :- (treat_arg_symbolically(Set) ; treat_arg_symbolically(Rel) ; preference(convert_comprehension_sets_into_closures,true)), !, Rel \== [], % avoid setting up check_element_of for X then % x |-> y : Rel |>> Set <=> x|->y : Rel & y/: Set check_element_of_wf(Pair,Rel,WF), Pair = (_,P2), not_element_of_wf(P2,Set,WF).
injective([(_From,To)|T],SoFar,WF) :- not_element_of_wf(To,SoFar,WF), /* check that it is injective */ add_new_element_wf(To,SoFar,SoFar2,WF), %SoFar2=[To|SoFar], could also work and be faster ? injective(T,SoFar2,WF).
is_sequence2([(int(Idx),X)|Tail],IndexesSoFar,Type,Size,MinSize,WF) :- less_than_direct(0,Idx), %is_index_greater_zero(Idx), not_element_of_wf(int(Idx),IndexesSoFar,WF), check_element_of_wf(X,Type,WF), S1 is Size+1, clpfd_interface:clpfd_leq(Idx,MinSize,_Posted), (var(Tail) -> clpfd_interface:clpfd_domain(MinSize,Low,_Up), % TO DO: ensure that final size at least Low (number(Low),Low>S1 -> Tail = [_|_] % TO DO: proper reification; what if MinSize gets constrained later ; expand_seq_if_necessary(Idx,S1,Tail)) % the sequence must be longer; force it ; true ), is_sequence2(Tail,[int(Idx)|IndexesSoFar],Type,S1,MinSize,WF).
is_sequence_wf_ex(FF,Range,WF,FF) :- nonvar(FF), FF = closure(_,_,_), custom_explicit_sets:is_definitely_maximal_set(Range), % we do not need the Range; this means we can match more closures (e.g., lambda) custom_explicit_sets:dom_for_specific_closure(FF,FFDomain,function(_)),!, is_sequence_domain(FFDomain,WF).
newdomain2([(X,Y)|T],SoFar,Res,WF) :- (Res==[] -> MemRes=pred_true, % no new elements can appear, all Xs must already be in SoFar check_element_of_wf(X,SoFar,WF) ; membership_test_wf(SoFar,X,MemRes,WF), % now check that card of Relation is greater or equal to Result; if equal set MemRes to pred_false % if card(Result)=card(dom(Result)) => all elements in Result must be fresh domain elements card_greater_equal_check([(X,Y)|T],Res,MemRes) ), newdomain3(MemRes,X,T,SoFar,Res,WF).
newdomain3(pred_false,X,T,SoFar,Res,WF) :- kernel_objects:mark_as_non_free(X,domain), % X is linked to a particular Y -> it is not free add_element_wf(X,SoFar,SoFar2,WF), equal_cons_wf(Res,X,Res2,WF), newdomain1(T,SoFar2,Res2,WF).
newrange2([(X,Y)|T],SoFar,Res,WF) :- (Res==[] -> MemRes=pred_true, check_element_of_wf(Y,SoFar,WF) ; membership_test_wf(SoFar,Y,MemRes,WF), card_greater_equal_check([(X,Y)|T],Res,MemRes), % check that card of Relation is greater or equal to Result; if equal set MemRes to pred_false (var(MemRes) -> prop_empty_pred_true(Res,MemRes) %,print(delay_range(Y,T)),nl % TO DO: we could look further in T if we can decide membership for other elements in T ? ; true) ), newrange3(MemRes,Y,T,SoFar,Res,WF).
newrange3(pred_false,Y,T,SoFar,Res,WF) :- kernel_objects:mark_as_non_free(Y,range), % Y is linked to a particular X -> it is not free add_element_wf(Y,SoFar,SoFar2,WF), equal_cons_wf(Res,Y,Res2,WF), newrange2(T,SoFar2,Res2,WF).
not_empty_set_unless_closure_wf(closure(_,_,_),_) :- !. % do not check this; in_domain_wf or other call will find a solution anyway; no need to set up closure constraints twice
not_is_sequence_wf(FF,Range,WF) :- nonvar(FF),custom_explicit_sets:is_definitely_maximal_set(Range), % we do not need the Range; this means we can match more closures (e.g., lambda) custom_explicit_sets:dom_for_specific_closure(FF,FFDomain,function(_)),!, not_is_sequence_domain(FFDomain,WF).
not_partial_function(FF,Domain,Range,WF) :- nonvar(FF),custom_explicit_sets:is_definitely_maximal_set(Range), % we do not need the Range; this means we can match more closures (e.g., lambda) custom_explicit_sets:dom_for_specific_closure(FF,FFDomain,function(_)),!, not_subset_of_wf(FFDomain,Domain,WF).
not_partial_function(FF,Domain,Range,WF) :- nonvar(FF), FF=closure(P,T,Pred), % example: f = %t.(t : NATURAL|t + 100) & f /: NATURAL +-> NATURAL is_lambda_value_domain_closure(P,T,Pred, FFDomain,_Expr), get_range_id_expression(P,T,TRangeID),!, subset_test(FFDomain,Domain,SubRes,WF), when(nonvar(SubRes), (SubRes=pred_false -> true % not a subset -> it is not a partial function over the domain ; check_not_lambda_closure_range(P,T,Pred,TRangeID,Range,WF))).
not_partial_function(R,Domain,Range,WF) :- expand_and_convert_to_avl_set(R,AER,not_partial_function,'ARG /: ? +-> ?'),!, % TO DO: expand_and_convert_to_avl_set_catch and provide symbolic treatment similar to partial_function is_not_avl_partial_function(AER,Domain,Range,WF).
not_permutation_sequence1(avl_set(A),Type,_,WF) :- is_ground_set(Type), !, Seq=avl_set(A), if(not_injective_sequence(Seq,Type,WF), true, % no backtracking required; we could even use regular if with -> not_surj_avl(Seq,Type,WF) ).
not_pf2(pred_true,_X,_Y,_T,_SoFar,_Dom,_Ran,_WF). /* then not a function */
not_pf2(pred_false,X,Y,T,SoFar,Dom,Ran,WF) :- membership_test_wf_with_force(Dom,X,MemRes,WF), % creates a choice point in SMT mode not_pf2a(MemRes,X,Y,T,SoFar,Dom,Ran,WF).
not_pf2b(_Done, X,Y,T, SoFar,Dom2,Ran, WF) :- add_element_wf(X,SoFar,SoFar2,WF), (T==[] -> not_element_of_wf(Y,Ran,WF) ; membership_test_wf_with_force(Ran,Y,MemRes,WF), prop_empty_pred_false(T,MemRes), % if T=[] -> Y must not be in Ran not_pf3(MemRes,T,SoFar2,Dom2,Ran,WF)).
not_relation_over(FF,Domain,Range,WF) :- nonvar(FF),custom_explicit_sets:is_definitely_maximal_set(Range), % we do not need the Range; this means we can match more closures (e.g., lambda) custom_explicit_sets:dom_for_specific_closure(FF,FFDomain,_),!, not_subset_of_wf(FFDomain,Domain,WF).
not_tf4(pred_true,X,_Y,T,SoFar,Dom2,Ran,WF) :- %check_element_of_wf(Y,Ran,WF), %DO WE NEED THIS ???? add_new_element_wf(X,SoFar,SoFar2,WF), not_tf(T,SoFar2,Dom2,Ran,WF).
not_tot_surj_rel([_|_],Done,_DelDom,Dom,_DelRan,_Ran,_WF) :- nonvar(Done), Done \= no_check_to_be_done, nonvar(Dom),is_infinite_explicit_set(Dom), !. % a finite expanded list can never be a total relation over an infinite domain
not_total_function(FF,Domain,Range,WF) :- nonvar(FF),custom_explicit_sets:is_definitely_maximal_set(Range), % we do not need the Range; this means we can match more closures (e.g., lambda) custom_explicit_sets:dom_for_specific_closure(FF,FFDomain,function(_)),!, not_equal_object_wf(FFDomain,Domain,WF).
not_total_function(FF,Domain,Range,WF) :- nonvar(FF), custom_explicit_sets:dom_range_for_specific_closure(FF,FFDomain,FFRange,function(_)),!, equality_objects_wf(FFDomain,Domain,Result,WF), % not yet implemented ! % TODO ! -> sub_set,equal,super_set when(nonvar(Result),(Result=pred_false -> true ; not_subset_of_wf(FFRange,Range,WF))).
not_total_function(FF,Domain,Range,WF) :- nonvar(FF), FF=closure(P,T,Pred), % example: f = %t.(t : NATURAL|t + 100) & f /: NATURAL +-> NATURAL is_lambda_value_domain_closure(P,T,Pred, FFDomain,_Expr), get_range_id_expression(P,T,TRangeID),!, equality_objects_wf(FFDomain,Domain,SubRes,WF), % compare: subset_test for not_partial_function when(nonvar(SubRes), (SubRes=pred_false -> true % not equal -> it is not a total function over the domain ; check_not_lambda_closure_range(P,T,Pred,TRangeID,Range,WF))).
not_total_function_avl(_AER,Domain,_Range,_WF) :- is_infinite_explicit_set(Domain),!, true. % a finite AVL set cannot be a total function over an infinite domain
not_total_injection2(pred_true,R,DomType,RangeType,WF) :- % TO DO: replace DomType and RangeType by full Type not_injection_wf(R,DomType,RangeType,WF).
not_total_relation_wf(FF,Domain,Range,WF) :- nonvar(FF),custom_explicit_sets:is_definitely_maximal_set(Range), % we do not need the Range; this means we can match more closures (e.g., lambda) custom_explicit_sets:dom_for_specific_closure(FF,FFDomain,function(_)),!, not_equal_object_wf(FFDomain,Domain,WF).
not_total_relation_wf(FF,Domain,Range,WF) :- nonvar(FF), custom_explicit_sets:dom_range_for_specific_closure(FF,FFDomain,FFRange,function(_)),!, equality_objects_wf(FFDomain,Domain,Result,WF), % not yet implemented ! % TODO ! -> sub_set,equal,super_set when(nonvar(Result),(Result=pred_false -> true ; not_subset_of_wf(FFRange,Range,WF))).
not_total_relation_wf(R,Domain,Range,WF) :- expand_custom_set_to_list_wf(R,ER,Done,not_total_relation_wf,WF), not_tot_surj_rel(ER,Done,Domain,Domain,[],Range,WF). % empty DelRange means we don't do surjective test
not_tr2(pred_true,X,Y,T,DelDom,Dom,DelRan,Ran,WF) :- delete_element_wf(X,DelDom,DelDom2,WF), % set DelDom initially to [] to avoid totality check membership_test_wf(Ran,Y,MemRes,WF), not_tr3(MemRes,Y,T,DelDom2,Dom,DelRan,Ran,WF).
not_tr3(pred_true,Y,T,DelDom2,Dom,DelRan,Ran,WF) :- delete_element_wf(Y,DelRan,DelRan2,WF), % set DelRan initially to [] to avoid surjection check not_tot_surj_rel(T,no_check_to_be_done,DelDom2,Dom,DelRan2,Ran,WF).
opt_force_false(EqRes) :- (preference(find_abort_values,false) -> EqRes=pred_false ; true). % TO DO: if EqRes becomes pred_true: raise abort_error as the relation was not a function
optional_functionality_check(Tail,X,WF) :- preferences:preference(disprover_mode,true),!, not_in_domain_wf(X,Tail,WF). % we assert that R is a function ; when disproving we can assume well-definedness
optional_functionality_check(_,_X,_WF). % TO DO: maybe lazily check if we have other elements with X as first arg if find_abort_values is true
override2c(pred_true,_V,_W,T,X,Y,_Remainder,Res,WF) :- equal_cons_wf(Res,(X,Y),T2,WF), override2(T,X,Y,[],T2,WF). /* set remainder to [], we have already added (X,Y) */
override_relation(R,S,Res,WF) :- /* R <+ S */ override_custom_explicit_set_wf(R,S,ORes,WF),!, equal_object_wf(ORes,Res,override_relation3,WF).
override_relation(R,S,Res,WF) :- /* R <+ S */ /* TO DO: first check if S is empty */ domain_wf(S,DS,WF), domain_subtraction_wf(DS,R,DSR,WF), union_wf(DSR,S,Res,WF).
partial_function_test_wf(FF,Domain,Range,Res,WF) :- Res==pred_false,!, not_partial_function(FF,Domain,Range,WF). % TO DO: remove not_partial_function to use check_is_partial_function?
partial_function_test_wf(FF,Domain,Range,Res,WF) :- nonvar(FF), custom_explicit_sets:is_definitely_maximal_set(Range), % we do not need the Range; this means we can match more closures (e.g., lambda) custom_explicit_sets:dom_for_specific_closure(FF,FFDomain,function(_)),!, subset_test(FFDomain,Domain,Res,WF).
partial_function_test_wf(FF,Domain,Range,Res,WF) :- nonvar(FF), % TODO: this will fail if is_definitely_maximal_set was true above ! custom_explicit_sets:dom_range_for_specific_closure(FF,FFDomain,FFRange,function(_)),!, % same as for total_function_wf check subset_test(FFDomain,Domain,DomainOk,WF), (DomainOk==pred_false -> Res = pred_false ; conjoin_test(DomainOk,RangeOk,Res,WF), subset_test(FFRange,Range,RangeOk,WF)).
partial_function_test_wf(R,Domain,Range,Res,WF) :- expand_and_convert_to_avl_set_warn(R,AER,partial_function_test_wf,'ARG : ? +-> ?'),!, % TO DO: use expand_and_convert_to_avl_set_catch (is_avl_partial_function(AER) -> % TO DO: we could do something similar to this instead: is_not_avl_relation_over_domain_range domain_of_explicit_set_wf(avl_set(AER),FFDomain,WF), subset_test(FFDomain,Domain,DomainOk,WF), (DomainOk == pred_false -> Res=pred_false ; range_of_explicit_set_wf(avl_set(AER),FFRange,WF), conjoin_test(DomainOk,RangeOk,Res,WF), subset_test(FFRange,Range,RangeOk,WF) ) ; Res=pred_false).
Description: Maybe we should only enumerate partial functions for domain variables ; e.g., not f <+ {x |-> y} : T +-> S print_bt_message(pf_dom_card(Card)),nl, %%%
partial_function_wf(FF,Domain,Range,WF) :- nonvar(FF), custom_explicit_sets:is_definitely_maximal_set(Range), % we do not need the Range; this means we can match more closures (e.g., lambda) custom_explicit_sets:dom_for_specific_closure(FF,FFDomain,function(_)),!, check_subset_of_wf(FFDomain,Domain,WF).
partial_function_wf(FF,Domain,Range,WF) :- nonvar(FF), % TODO: this will fail if is_definitely_maximal_set was true above ! custom_explicit_sets:dom_range_for_specific_closure(FF,FFDomain,FFRange,function(_)),!, % same as for total_function_wf check check_subset_of_wf(FFDomain,Domain,WF), check_subset_of_wf(FFRange,Range,WF).
partial_function_wf(FF,Domain,Range,WF) :- nonvar(FF), FF=closure(P,T,Pred), % example: f = %x.(x:NATURAL1|x+1) & f: NATURAL1 +-> NATURAL is_lambda_value_domain_closure(P,T,Pred, FFDomain,_Expr), get_range_id_expression(P,T,TRangeID), !, check_subset_of_wf(FFDomain,Domain,WF), check_lambda_closure_range(P,T,Pred,TRangeID,Range,WF). % we could use symbolic_range_subset_check
partial_function_wf(R,Domain,Range,WF) :- expand_and_convert_to_avl_set_catch(R,AER,partial_function_wf,'ARG : ? +-> ?',ResultStatus),!, (ResultStatus=avl_set -> is_avl_partial_function_over(AER,Domain,Range,WF) ; % keep symbolic (debug_mode(xoff) -> true ; print('SYMBOLIC +-> check : '),translate:print_bvalue(R),nl), % can deal with, e.g., f = %x.(x:NATURAL|x+1) & g = f <+ {0|->0} & g : INTEGER +-> INTEGER symbolic_domain_subset_check(R,Domain,WF), symbolic_range_subset_check(R,Range,WF), symbolic_functionality_check(R,WF) ).
partial_function_wf(R,Domain,Range,WF) :- get_cardinality_powset_wait_flag(Domain,partial_function_wf,WF,Card,CWF), % probably we should compute real cardinality of set of partial functions over Domain +-> Range ? % the powset waitflag uses 2^Card as priority; is the number of partial functions when Range contains just a single element % slows down test 1088: TO DO investigate % get_cardinality_partial_function_wait_flag(Domain,Range,partial_function_wf,WF,Card,_,CWF), %% Maybe we should only enumerate partial functions for domain variables ; e.g., not f <+ {x |-> y} : T +-> S %% print_bt_message(pf_dom_card(Card)),nl, % probably we should use a special version when R is var propagate_empty_set(Domain,R), propagate_empty_set(Range,R), (var(R) -> pf_var_r(R,var,Domain,Range,Card,WF,CWF) ; pf_var_r(R,nonvar,Domain,Range,Card,WF,CWF)).
pf(LIST,SoFar,Dom,Ran,Card,Large,WF,LWF) :- (var(LIST) -> ListWasVar = true ; ListWasVar = false), % is ListWasVar = true we are doing the enumeration driven by LWF being ground LIST = [(X,Y)|T], dec_card(Card,NC),/* Card ensures we do not build too big lists */ Dom \== [], remove_domain_element(ListWasVar,X,Y,Dom,Dom2,Large,WF,LWF,Done), check_element_of_wf(Y,Ran,WF), pf1(Done, X,Y,T,SoFar,Dom2,Ran,NC,Large,WF,LWF).
Description: check_element_of_wf(Y,Ran,WF), % this check is now done above in pf
Block: pf1(-,?,?,?,?,?,?,?,?,?,?)
pf1(_Done, X,_Y,T,SoFar,Dom2,Ran,Card,Large,WF,LWF) :- not_element_of_wf(X,SoFar,WF), /* check that it is a function */ %% check_element_of_wf(Y,Ran,WF), % this check is now done above in pf add_new_element_wf(X,SoFar,SoFar2,WF), pf_w(T,SoFar2,Dom2,Ran,Card,Large,WF,LWF).
pf_var_r(R,var,Domain,Range,_Card,WF,_CWF) :- % if R was var: see if it is now an AVL set; otherwise we have already checked it expand_and_convert_to_avl_set_warn(R,AER,pf_var_r,'ARG : ? +-> ?'),!, is_avl_partial_function_over(AER,Domain,Range,WF).
prefix_sequence1(_Seq,Num,_Res,WF) :- Num<0,!, % according to version 1.8.8 of Atelier-B manual Num must be in 0..size(_Seq) add_wd_error('negative index in prefix_sequence (/|\\)! ', Num,WF).
prefix_sequence1(Seq,Num,Res,WF) :- is_custom_explicit_set(Seq,prefix), prefix_of_custom_explicit_set(Seq,Num,ERes,WF),!, % TO DO: check Num <= size(Seq) equal_object_wf(Res,ERes,prefix_sequence1,WF).
propagate_range_membership([(_,RanEl)|T],X) :- nonvar(RanEl), preferences:preference(use_clpfd_solver,true), preferences:preference(find_abort_values,false), get_finite_fdset_information(RanEl,Info), % TO DO: try and detect if we can apply element/3 from clpfd \+ ground(X), get_fdset_information(X,InfoX), Info \= InfoX, % avoids NQueens slowdown; TO DO: check if more precise than InfoX; otherwise no use in collecting info !, propagate_range_membership(T,Info,X).
propagate_range_membership([],Info,El) :- !, % note: the information for the first few elements might have become more precise; TO DO: wait until list known and then propagate ?+ keep on propagating ?? assert_fdset_information(Info,El).
propagate_range_membership([(_,RanEl)|T],Acc,X) :- nonvar(RanEl), % otherwise we have no info: we may just as well stop get_finite_fdset_information(RanEl,RInfo), combine_fdset_information(Acc,RInfo,NewAcc), NewAcc \= no_fdset_info, !, propagate_range_membership(T,NewAcc,X).
propagate_result_to_input(Result,OriginalRel,DomOrRange,WF) :- propagate_empty_set(Result,OriginalRel), % this will trigger before LWF ground (preferences:preference(use_smt_mode,true) -> propagate_result_to_input1(Result,OriginalRel,1,DomOrRange) % hopefully full CHR implementation will avoid the need for this hack % ; kernel_objects:is_marked_to_be_computed(OriginalRel) -> true % get_last_wait_flag(propagate_result_to_input,WF,LWF) ; get_wait_flag(2000,propagate_result_to_input,WF,LWF), % TO DO: determine right value for Priority ? % higher number for data_validation mode seems slightly counterproductive (on private_source_not_available tests) propagate_result_to_input1(Result,OriginalRel,LWF,DomOrRange) % this slows down test 289 if not guarded, 1088 if guarded ).
propagate_result_to_input2([],_Rel,_,_) :- !. % nothing can be said; we could have repeated entries for previous domain elements
propagate_result_to_input2([D|T],Rel,LWF,DomOrRange) :- %print(propagate_result_to_input2([D|T],Rel,LWF,DomOrRange)),nl, !, (Rel == [] -> fail % we would need more relation elements to generate the domain/range ; nonvar(Rel) -> true % no propagation ; (DomOrRange=domain -> Rel = [(D,_)|RT] ; Rel = [(_,D)|RT]), propagate_result_to_input2(T,RT,LWF,DomOrRange) ).
propagate_singleton_image(Relation,S,avl_set(Res),WF) :- custom_explicit_sets:singleton_set(S,El), % we have the image by a singleton set {El} expand_custom_set_to_list_wf(avl_set(Res),LR,_,prop_singleton,WF), !, l_check_element_of(LR, El, Relation, WF). % propagate x|->ri : f (will force membership)
propagate_size(Res,Num,WF) :- var(Res),!, (Num<0 -> preferences:preference(disprover_mode,false) % don't do anything; we may want to generate WD error ; size_of_sequence(Res,int(Num),WF)).
propagate_size(_,Num,_) :- number(Num), !. % no need to propagate
propagate_size(_,_Num,_) :- \+ preferences:preference(find_abort_values,false), !. % do not propagate as we could prevent detection of WD errors below
propagate_size([],Num,_WF) :- !, Num=0. % Note: this could prevent a wd-error being detected
propagate_size(avl_set(A),Num,WF) :- var(Num), % with partially instantated sets we get slowdowns (SimpleCSGGrammar2_SlowCLPFD) % TO DO: treat list skeletons !, size_of_sequence(avl_set(A),int(Num),WF). % Note: this could prevent a wd-error being detected
propagate_size(_,_,_). % should we also propagate the other way around ?
quick_propagate_domain([(X,_)|T],FullRes,WF) :- quick_propagation_element_information(FullRes,X,WF,FullRes1), % should we use a stronger check ? quick_propagate_domain(T,FullRes1,WF).
quick_propagate_range([(_,Y)|T],FullRes,WF) :- quick_propagation_element_information(FullRes,Y,WF,FullRes1), % should we use a stronger check ? quick_propagate_range(T,FullRes1,WF).
quick_propagation_domain_element_list(_,RelList,El,WF) :- try_in_fd_value_list_check(RelList,(El,_),couple_left(_),WF). % use couple_left to ignore range values
range_restriction_wf(R,S,Res,WF) :- /* R |> S */ ok_to_try_restriction_explicit_set(S,R,Res), range_restriction_explicit_set_wf(R,S,SR,WF),!, equal_object_wf(SR,Res,range_restriction,WF).
range_restriction_wf(R,S,Res,WF) :- /* R |> S */ expand_custom_set_to_list_wf(R,ER,_,range_restriction,WF), relation_restriction_wf(ER,S,Res,pred_true,range,WF).
range_subtraction_wf(R,S,Res,WF) :- /* R |>> S */ S==[],!, equal_object_wf(R,Res,range_subtraction1,WF).
range_subtraction_wf(R,S,Res,WF) :- /* R |>> S */ ok_to_try_restriction_explicit_set(S,R,Res), range_subtraction_explicit_set_wf(R,S,SR,WF),!, equal_object_wf(SR,Res,range_subtraction2,WF).
range_subtraction_wf(R,S,Res,WF) :- /* R |>> S */ expand_custom_set_to_list_wf(R,ER,_,range_subtraction,WF), relation_restriction_wf(ER,S,Res,pred_false,range,WF).
range_wf1(Rel,Res,WF) :- % TO DO : propagate information that card of Res <= card of Rel; similar thing for domain expand_custom_set_to_list_wf(Rel,Relation,_,range_wf1,WF), newrange2(Relation,[],Res,WF), quick_propagate_range(Relation,Res,WF).
rel_compose2([(X,Y)|T],Rel2,Out,WF) :- rel_extract(Rel2,X,Y,OutXY,[],WF), % rel_extract(Rel2,X,Y,Out,OutRem), rel_compose2(T,Rel2,OutRem,WF), union_wf(OutRem,OutXY,Out,WF). % used to call union wihout wf; makes test 1394 fail
rel_compose_with_inf_fun_acc_aux(pred_true,X,Y,T,Dom,Fun,Acc,CompRes,WF) :- apply_to(Fun,Y,FY,WF), % TO DO: generalize to image so that we can apply it also to infinite relations ? add_element_wf((X,FY),Acc,NewAcc,WF), rel_compose_with_inf_fun_acc(T,Dom,Fun,NewAcc,CompRes,WF).
rel_composition1(Rel1,Rel2,Comp,WF) :- rel_composition_for_explicit_set(Rel1,Rel2,Res),!, % treats finite Rel1 and avl_set for Rel2 equal_object_wf(Res,Comp,rel_composition1_1,WF).
rel_composition1(Rel1,Rel2,Comp,WF) :- Rel2=closure(_,_,_), keep_symbolic(Rel2), (dom_for_specific_closure(Rel2,Domain,function(_)) % TO DO: also deal with relations; in SYMBOLIC mode this may be counter productive; see function_composition ast cleanup rule -> !, expand_custom_set_to_list_wf(Rel1,Relation1,_,rel_composition1,WF), rel_compose_with_inf_fun(Relation1,Domain,Rel2,Comp,WF) % this is like map Rel2 over Rel1 in functional programmming ; symbolic_composition(Rel1,Rel2,false,Rel3), !, expand_custom_set_wf(Rel3,CRes,rel_composition,WF),% do we need to expand ? equal_object_optimized(CRes,Comp,rel_composition1_3) ).
relation_over1(FF,Domain,Range,WF,_WFR,_MaxCard,_MaxNrOfRels) :- nonvar(FF), custom_explicit_sets:is_definitely_maximal_set(Range), % we do not need the Range; this means we can match more closures (e.g., lambda) custom_explicit_sets:dom_for_specific_closure(FF,FFDomain,_),!, check_subset_of_wf(FFDomain,Domain,WF).
relation_restriction_aux(MemRes,X,Y,T,S,Res,AddWhen,DomOrRange,WF) :- MemRes==AddWhen,!, % (X,Y) should be added to result % TO DO: collect result until we delay ? and then do equal_object ? equal_cons(Res,(X,Y),RT), % was : equal_object([(X,Y)|RT],Res), %equal_cons_wf(Res,(X,Y),RT,WF), % makes tests 982, 1302, 1303 fail; TO DO: investigate %when(nonvar(RT), % causes problem for test 982 relation_restriction_wf(T,S,RT,AddWhen,DomOrRange,WF).
relation_restriction_aux(_MemRes,_X,_,T,S,RT,AddWhen,DomOrRange,WF) :- % the couple is filtered out relation_restriction_wf(T,S,RT,AddWhen,DomOrRange,WF).
relation_restriction_wf([(X,Y)|T],S,Res,AddWhen,DomOrRange,WF) :- (DomOrRange=domain -> membership_test_wf(S,X,MemRes,WF) % TO DO: pass WF ! ; membership_test_wf(S,Y,MemRes,WF)), (nonvar(MemRes) %MemRes==AddWhen % MemRes already set; we will ensure that (X,Y) in Res below; this slows down Alstom Compilation Regle ! % doing the membership_test on the result Res if MemRes\==AddWhen only makes sense if we cannot fully compute the restriction ?? i.e. if T is not a closed list ? -> true %,(MemRes==AddWhen -> true ; print_term_summary(relation_restriction([(X,Y)|T],S,Res,AddWhen,DomOrRange)),nl) ; (AddWhen=pred_true -> InResult=MemRes ; negate(InResult,MemRes)), % from bool_pred membership_test_wf(Res,(X,Y),InResult,WF) % TO DO: same for explicit version; gets called e.g. if S = 1..n (1..n <| [1,2,3] = [1,2]) % can now solve e.g. {x|x <| [1,2,3] = [1,2] & card(x)=2} = {{1,2}} % or x <| s = [1,2,3] \/ {29|->29} & x <: 1..100 & s = %i.(i:1..50|i) ), relation_restriction_aux(MemRes,X,Y,T,S,Res,AddWhen,DomOrRange,WF).
remove_a_minimal_element2(X,ESet,EDone,Res,WF,Done) :- var(ESet), % should not happen as we wait for EDone add_internal_error('Illegal call: ',remove_a_minimal_element2(X,ESet,EDone,Res,WF,Done)), fail.
remove_a_minimal_element2(X,ESet,_EDone,Res,WF,Done) :- ESet \= [], (ESet = [El] -> X=El, empty_set_wf(Res,WF), Done=true % only one choice ; get_cardinality_wait_flag(ESet,remove_a_minimal_element2,WF,CWF), remove_a_minimal_element3(X,ESet,Res,WF,Done,CWF) ).
remove_a_minimal_element3(X,ESet,Res,WF,Done,_) :- var(Res), !, append(_,[X|TRes],ESet), % WHAT IF Res has been instantiated in the meantime ??? equal_object_wf(Res,TRes,remove_a_minimal_element2_2,WF),Done=true.
Description: (X, Y are free and we drive the enumeration: we can influence which element is taken from Dom added Jul 15 2008
remove_domain_element(ListWasVar,X,Y,Dom,Dom2,Large,WF,LWF,Done) :- compute_large(Dom,Large), ((ListWasVar==true,var(X),var(Y),Large==false, preference(convert_comprehension_sets_into_closures,false), % not in symbolic mode kernel_tools:ground_value(Dom)) -> %% (X, Y are free and we drive the enumeration: we can influence which element is taken from Dom remove_a_minimal_element(X,Dom,Dom2,WF,Done) %%%%%%%%%% added Jul 15 2008 ; remove_element_wf_if_not_infinite_or_closure(X,Dom,Dom2,WF,LWF,Done) ).
rev_sequence2(S1,Res,WF) :- expand_custom_set_to_list_wf(S1,ES1,_,rev_sequence2,WF), size_of_sequence(ES1,int(Size1),WF), % TO DO: we could also try and get the size from the result Res rev_sequence3(ES1,Size1,Res,WF).
rev_sequence3(E,Size,Res,WF) :- var(Size), !, % try to obtain size from result as well size_of_sequence(Res,int(Size),WF), rev_sequence3b(E,Size,Res,WF).
set_up_sequence_skel_aux(Seq,Res,_Trigger,WF) :- get_large_finite_wait_flag(set_up_sequence_skel,WF,LWF), % delay, avoid costly unification with partially instantaited list skeleton; TO DO: in future we may use the kernel_cardinality attribute instead when((nonvar(LWF) ; nonvar(Seq) ; nonvar(Res)), (nonvar(Seq) -> true ; gen_seq_for_res(Res,Seq))).
shift_seq_indexes(Seq,Offset,ShiftedSeq,WF) :- nonvar(Seq),!, expand_custom_set_to_list_wf(Seq,ESeq,_,shift_seq_indexes,WF), shift_seq_indexes2(ESeq,Offset,ShiftedSeq,WF,Done), (Done == done -> true ; % also propagate in the other way: TO DO: make a more efficient fine-grained two-ways propagation; maybe using CHR NegOffset is -Offset, expand_custom_set_to_list_wf(ShiftedSeq,ESeq1,_,shift_seq_indexes,WF), shift_seq_indexes2(ESeq1,NegOffset,ESeq,WF,_)).
shift_seq_indexes(Seq,Offset,ShiftedSeq,WF) :- NegOffset is -Offset, % compute in the other direction; TO DO: make a more efficient fine-grained two-ways propagation; maybe using CHR expand_custom_set_to_list_wf(ShiftedSeq,ESeq,_,shift_seq_indexes,WF), shift_seq_indexes2(ESeq,NegOffset,Seq,WF,Done), (Done == done -> true ; % also propagate in the original way: expand_custom_set_to_list_wf(Seq,ESeq1,_,shift_seq_indexes,WF), shift_seq_indexes2(ESeq1,Offset,ESeq,WF,_)).
size_of_sequence1(Seq,Size,WF) :- expand_custom_set_to_list_wf(Seq,ESeq,_,size_of_sequence1,WF), (var(ESeq),nonvar(Size) -> size_of_var_seq(ESeqR,0,Size), ESeqR=ESeq % unify after to do propagation in one go, without triggering coroutines inbetween ; size_of_seq2(ESeq,0,Size), (var(Size),var(ESeq) -> less_than_equal_direct(0,Size) % propagate that Size is positive ; true) ).
surjection_relation_wf(R,Domain,Range,WF) :- is_surjective(R,Range,WF), % TODO: is not optimal since ran(R)<:Range is already implied by is_surjective and % checked a second time by relation_over_wf/4 relation_over_wf(R,Domain,Range,WF).
surjective_iseq_0(SkelSeq,_ESeq,Type,WF,_Card,Ground) :- nonvar(Ground), nonvar(SkelSeq), preference(use_clpfd_solver,true), % try and use an optimized version calling global_cardinality in CLPFD module get_global_cardinality_list(Type,YType,GCL,_), % this dramatically reduces runtime for NQueens40_perm; maybe we should do this only when necessary, i.e., when surjective_iseq blocks on PreviousRemoveDone % check why it slows down SortByPermutation_v2 !, global_cardinality_range(SkelSeq,[],YType,GCL,WF).
surjective_iseq_0(_,ESeq,Type,WF,Card,_) :- %quick_propagate_range(ESeq,Type,WF), % ensure that we propagate type information to all elements; p:perm(5..20) & p(10)=21 will fail straightaway (surjective_iseq will block); % but this slows down EulerWay.mch ; maybe because it sets up enumerators ? TO DO: investigate surjective_iseq(ESeq,Type,WF,Card).
tf(FUN,SoFar,s(Card),Dom,Ran,WF,LWF) :- var(FUN),nonvar(Dom), % try setting up skeleton for total fun remove_exact_first_element(X,Dom,Dom2),not_element_of_wf(X,SoFar,WF),var(FUN),!, FUN = [(X,Y)|T], tf1(X,Y,T,SoFar,Card,Dom2,Ran,WF,LWF).
tf([(X,Y)|T],SoFar,s(Card),Dom,Ran,WF,LWF) :- not_element_of_wf(X,SoFar,WF), remove_element_wf(X,Dom,Dom2,WF), %mal: 17/3/08 changed to _wf version tf1(X,Y,T,SoFar,Card,Dom2,Ran,WF,LWF).
tf_var(F,_,Card,Dom,_,WF) :- Card==0,!,F=[],empty_set_wf(Dom,WF). % avoid choice point
tf_var([],_,0,Dom,_,WF) :- empty_set_wf(Dom,WF).
tf_var([(X,Y)|T],SoFar,s(Card),Dom,Ran,WF) :- /* supposes that X + Y are unbound */ /* TO DO: rewrite like enumerate <-------------------------- */ ((var(X),var(Y)) -> true ; (print_message(warning,'Nonvar in tf_var: '), print_message(warning,((X,Y))))), remove_exact_first_element(X,Dom,Dom2), not_element_of_wf(X,SoFar,WF), check_element_of_wf(Y,Ran,WF), add_new_element_wf(X,SoFar,SoFar2,WF), tf_var(T,SoFar2,Card,Dom2,Ran,WF).
total_bijection_wf(R,Domain,Range,WF) :- same_cardinality_wf(Domain,Range,WF), total_injection_wf2(R,Domain,Range,WF). % TO DO: use cardinality_as_int_wf ? makes test 1194 fail
total_function2(ER,Card,Domain,Range,WF) :- (ground(Card) -> get_wait_flag(0,tot_fun,WF,LWF) % we seem to know the domain exactly now; see e.g. test 1316 ; get_wait_flag(2,total_function2,WF,LWF)), % ensure we don't start binding function as soon as Card is bound; important for test 1393; should we use another priority ? tf(ER,[],Card,Domain,Range,WF,LWF).
total_function_wf(FF,Domain,Range,WF) :- Range == [],!, empty_set_wf(FF,WF), empty_set_wf(Domain,WF).
total_function_wf(FF,Domain,Range,WF) :- % TO DO: if FF or Domain nonvar but \= [] -> check if other variable becomes [] total_function_wf1(FF,Domain,Range,WF).
total_function_wf1(FF,Domain,Range,WF) :- %print_term_summary(total_function_wf1(FF,Domain,Range,WF)),nl,trace, custom_explicit_sets:is_definitely_maximal_set(Range), % we do not need the Range; this means we can match more closures (e.g., lambda) (nonvar(FF), custom_explicit_sets:dom_for_specific_closure(FF,FFDomain,function(_)) -> !, equal_object_wf(FFDomain,Domain,total_function_wf1_1,WF) ; var(FF), get_wait_flag1(WF,WF1), var(WF1), \+ (custom_explicit_sets:get_card_for_specific_custom_set(Domain,Card), number(Card)), % we have a total_function over a possibly infinite domain, % better wait: maybe a recursive of other closure will be produced for FF !, when( (nonvar(FF) ; nonvar(WF1)), total_function_wf1(FF,Domain,Range,WF)) ).
total_function_wf1(FF,Domain,Range,WF) :- % want to replace FF by closure: needs to be a variable! var(FF), % if the total function can not be build up explicitly (i.e. infinite domain) % TODO: can / should this be relaxed? custom_explicit_sets:is_infinite_explicit_set(Domain), % get_card_for_specific_custom_set or is_infinite_or_symbolic_closure % TO DO: delay if Domain infinite or closure and not yet known and range is type kernel_objects:infer_value_type(Domain,set(DomT)), kernel_objects:infer_value_type(Range,set(RanT)), !, % IDEA : TF = %x.(x:Domain|DEFAULT) <+ SFF, where SFF is partial function and DEFAULT is some default value % build up a partial function instead (fulfilling all constraints) % better? : %x.(x:Domain|IF x:dom(SFF) THEN SFF(x) ELSE DEFAULT)? partial_function_wf(SFF,Domain,Range,WF), % next, build up a total function mapping everything to a default value % this function will be overriden by the partial function to fulfilling % given constraints % 1. identifiers for closure create_texpr(identifier('__domid__'),DomT,[],TDomId), create_texpr(identifier('__ranid__'),RanT,[],TRanId), % 2. domain identifier might take all values of the domain create_texpr(member(TDomId,b(value(Domain),set(DomT),[])),pred,[],DomMember), % 3. pick a single value for the range identifier check_element_of_wf(RangeElement,Range,WF), %% external_functions:observe_value(RangeElement,"range"),external_functions:observe_value(SFF,"pf"), create_texpr(equal(TRanId,b(value(RangeElement),RanT,[])),pred,[],RanMember), % 4. conjunct and form closure (should be treated symbolically) conjunct_predicates([RanMember,DomMember],Pred), Default = closure(['__domid__','__ranid__'],[DomT,RanT],Pred), % 5. override default values where needed override_relation(Default,SFF,FF,WF).
total_function_wf1(R,Domain,Range,WF) :- try_expand_and_convert_to_avl_with_check(Domain,EDomain,keep_intervals(1000),total_function), % avoid multiple expansions, but useless when dom_for_lambda_closure case triggers below ! TO DO: fix % TO DO: maybe avoid converting intervals which are not fully instantiated ? % TODO: done by clause above? % TO DO ?: if Range singleton set {R} and Domain infinite: return %x.(x:Domain|R); if Range not empty choose one element try_expand_and_convert_to_avl_unless_large(R,ER), total_function_wf2(ER,EDomain,Range,WF).
total_function_wf3(FF,Card,Domain,Range,WF) :- nonvar(FF), (number(Card) -> (Card >= 1000 -> true ; is_symbolic_closure(FF)) ; true), % note: we can have symbolic closures with a finite domain: /*@symbolic */ %p.(p:BOOL|(%t.(t:NATURAL|t+100))) custom_explicit_sets:dom_for_lambda_closure(FF,FFDomain), % we have a lambda closure where we cannot determine the range, otherwise dom_range_for_specific_closure would have succeeded % example: f = %x.(x:NATURAL1|x+1) & f: NATURAL1 --> NATURAL FF = closure(P,T,Pred), get_range_id_expression(P,T,TRangeID), !, equal_object_wf(FFDomain,Domain,total_function1_closure,WF), % CHECK not(#P.(Pred & P /: Range)) check_lambda_closure_range(P,T,Pred,TRangeID,Range,WF).
total_function_wf3(R,Card,Domain,Range,WF) :- card_convert_int_to_peano(Card,PeanoCard), ((nonvar(R);ground(PeanoCard)) -> true ; get_last_wait_flag(total_fun(Domain),WF,WF1)), when((nonvar(R);ground(PeanoCard); (nonvar(PeanoCard),nonvar(WF1))), /* mal 12/5/04: changed , into ; 17/3/2008: added WF1 */ /* reason for delaying nonvar(Card): Card grounded bit by bit by cardinality; avoid triggering too early and missing tf_var */ total_function1(R,Card,PeanoCard,Domain,Range,WF )).
total_injection_wf(R,DomType,RangeType,WF) :- check_card_greater_equal(RangeType,geq,DomType,_,_), % there must be more Range elements than domain elements; pigeonhole principle total_injection_wf2(R,DomType,RangeType,WF).
total_surjection_relation_wf(R,Domain,Range,WF) :- relation_over_wf(R,Domain,Range,WF), check_relation_is_total(R,Domain,WF), % calls domain which now instantiates R if Domain known check_relation_is_surjective(R,Range,WF).
total_surjection_wf(R,DomType,RangeType,WF) :- check_card_greater_equal(DomType,geq,RangeType,CardDom,CardRange), total_function_wf(R,DomType,RangeType,WF), % setup_surj_range(RangeType,R,WF). (surjection_has_to_be_total_injection(CardDom,CardRange) % LAW: card(setX) = card(setY) => ff: setX -->> setY <=> ff: setX >-> setY -> injective(R,WF) % if domain and range have same cardinality: injection ensures surjectivity, and is more efficient to check/propagate; example when using queens 1..n -->> 1..n for NQueens ; check_relation_is_surjective(R,RangeType,WF)).
try_find_index_element(Idx,El,AVL,WF) :- avl_fetch_pair(int(Idx),AVL,AvlEl), !, % We have found an entry with the same index: El and AvlEl must be identical: equal_object_wf(El,AvlEl,try_find_index_element,WF).
! 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(plspec_patch_libraries,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_debug_flag,true)
! Existence error in debug:global_debug_flag/0
! procedure debug:global_debug_flag/0
does not exist
! goal: debug:global_debug_flag
! Existence error in debug:use_timer/0
! procedure debug:use_timer/0
does not exist
! goal: debug:use_timer
! 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_core_only,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'),_24599,[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),_110935,[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'),_136651,[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(clpfd_interface) does not exist
! goal: absolute_file_name(probsrc(clpfd_interface),_140499,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/typing_tools.pl')])
! Existence error in user:environ/2
! procedure user:environ/2
does not exist
! goal: user:environ(no_wd_checking,true)
! Existence error in user:environ/2
! procedure user:environ/2
does not exist
! goal: user:environ(cogen,true)
! Existence error in user:environ/2
! procedure user:environ/2
does not exist
! goal: user:environ(disable_chr,true)
! Existence error in user:environ/2
! procedure user:environ/2
does not exist
! goal: user:environ(enable_time_out_for_constraints,true)
! Existence error in user:environ/2
! procedure user:environ/2
does not exist
! goal: user:environ(enable_time_out_for_constraints,true)
! Existence error in user:environ/2
! procedure user:environ/2
does not exist
! goal: user:environ(enable_time_out_for_constraints,true)
! Existence error in user:environ/2
! procedure user:environ/2
does not exist
! goal: user:environ(enable_time_out_for_constraints,true)
! 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'),_175753,[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),_181723,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/kernel_z.pl')])
! Existence error in debug:use_timer/0
! procedure debug:use_timer/0
does not exist
! goal: debug:use_timer
! Existence error in user:environ/2
! procedure user:environ/2
does not exist
! goal: user:environ(prob_profile,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'),_165643,[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 prob_rewrite_rules(b_ast_cleanup_rewrite_rules) does not exist
! goal: absolute_file_name(prob_rewrite_rules(b_ast_cleanup_rewrite_rules),_165643,[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),_171053,[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 extension('regexp/regexp') does not exist
! goal: absolute_file_name(extension('regexp/regexp'),_165643,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/external_functions.pl')])
! Existence error in debug:global_debug_flag/0
! procedure debug:global_debug_flag/0
does not exist
! goal: debug:global_debug_flag
! Existence error in argument 1 of absolute_file_name/3
! file extension('counter/counter') does not exist
! goal: absolute_file_name(extension('counter/counter'),_179441,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/succeed_max.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file extension('counter/counter') does not exist
! goal: absolute_file_name(extension('counter/counter'),_183715,[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 extension('probhash/probhash') does not exist
! goal: absolute_file_name(extension('probhash/probhash'),_182717,[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'),_179441,[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 probcspsrc(haskell_csp) does not exist
! goal: absolute_file_name(probcspsrc(haskell_csp),_179295,[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 probcspsrc(haskell_csp) does not exist
! goal: absolute_file_name(probcspsrc(haskell_csp),_169061,[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 kodkodsrc(kodkod) does not exist
! goal: absolute_file_name(kodkodsrc(kodkod),_163083,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/b_interpreter.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(custom_explicit_sets) does not exist
! goal: absolute_file_name(probsrc(custom_explicit_sets),_161369,[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(disable_chr,true)
! 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),_161657,[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: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 extension('random_permutations/random_permutations') does not exist
! goal: absolute_file_name(extension('random_permutations/random_permutations'),_111223,[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(b_state_model_check) does not exist
! goal: absolute_file_name(probsrc(b_state_model_check),_108227,[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(specfile) does not exist
! goal: absolute_file_name(probsrc(specfile),_101823,[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),_101823,[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),_103203,[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),_101823,[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),_98543,[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),_98831,[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),_72973,[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(gensym) does not exist
! goal: absolute_file_name(probsrc(gensym),_49381,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/translate.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(btypechecker) does not exist
! goal: absolute_file_name(probsrc(btypechecker),_26931,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/bsyntaxtree.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(tools_lists) does not exist
! goal: absolute_file_name(probsrc(tools_lists),_23083,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/kernel_tools.pl')])
! Existence error in debug:global_debug_flag/0
! procedure debug:global_debug_flag/0
does not exist
! goal: debug:global_debug_flag
! 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_profile,true)
* Non-determinate: bsets_clp:not_is_non_empty_sequence/2
(clause 2)
* This clause contains a disjunction not forced to be deterministic.
* Non-determinate: bsets_clp:not_injective_sequence1/4
(clause 1)
* This clause contains a disjunction not forced to be deterministic.
* Non-determinate: bsets_clp:not_non_empty_injective_sequence/3
(clause 2)
* This clause contains a disjunction not forced to be deterministic.
* Non-determinate: bsets_clp:not_permutation_sequence1/4
(clause 2)
* This clause contains a disjunction not forced to be deterministic.
* Non-determinate: bsets_clp:not_permutation_sequence2/4
(clause 1)
* Indexing cannot distinguish this from clause 2.
* Non-determinate: bsets_clp:propagate_size/3
(clause 1)
* Calls nondet predicate preferences:preference/2
.
* Non-determinate: bsets_clp:prefix_seq2/7
(clause 1)
* This clause contains a disjunction not forced to be deterministic.
* Non-determinate: bsets_clp:suffix_seq2/7
(clause 1)
* This clause contains a disjunction not forced to be deterministic.
* Non-determinate: bsets_clp:concs2/3
(clause 2)
* Indexing cannot distinguish this from clause 3.
* Non-determinate: bsets_clp:relation_over2/9
(clause 1)
* Indexing cannot distinguish this from clause 2.
* Non-determinate: bsets_clp:pf/8
(clause 3)
* Indexing cannot distinguish this from clause 4.
* Non-determinate: bsets_clp:tf/7
(clause 1)
* Indexing cannot distinguish this from clause 2.
* Non-determinate: bsets_clp:treat_arg_symbolically/1
(clause 2)
* This clause contains a disjunction not forced to be deterministic.
* Non-determinate: bsets_clp:image_for_closure1_check_fix/7
(clause 1)
* This clause contains a disjunction not forced to be deterministic.
! warning: predicate bsets_clp:preference/2
is dynamic.
! Some nondeterminism may have been missed.
! Add (or move) the directive
! :- dynamic bsets_clp:preference/2
.
! near the top of this file.
! Existence error in user:environ/2
! procedure user:environ/2
does not exist
! goal: user:environ(no_wd_checking,true)
* Non-determinate: bsets_clp:apply_closure_to_nonvar/7
(clause 1)
* Indexing cannot distinguish this from clause 2.
* Non-determinate: bsets_clp:at_least_one_set_not_empty/3
(clause 2)
* Indexing cannot distinguish this from clause 3.
* Non-determinate: bsets_clp:compute_trans_closure2/3
(clause 1)
* This clause contains a disjunction not forced to be deterministic.
* Non-determinate: bsets_clp:add_tuples/6
(clause 2)
* This clause contains a disjunction not forced to be deterministic.