:-module(_,[bsts/2],[]). '$applied_packages'([prelude,nonpure,condcomp,regtypes,assertions,rtchecks_shallow,fsyntax,predefres(res_steps),resdefs,resdefs/resources_decl,nativeprops,basicmodes,argnames,expander]). :-add_clause_trans(expander_tr:expand_clause/4,9910). :-prop bst/1. :-prop min_/2. :-prop max_/2. :-prop bst_/3. :-entry bsts(E,L):(num(E),bst(L)). :-check calls bsts(E,L):(num(E),bst(L)). :-true pred bsts(E,L):(num(E),term(L))=>(num(E),rt2(L)). :-true pred bsts(E,L):(mshare([[L]]),ground([E]))=>(mshare([[L]]),ground([E])). :-check calls bsts_i(E,L):(num(E),bst(L)). :-true pred bsts_i(E,L):(num(E),term(L))=>(num(E),rt2(L)). :-true pred bsts_i(E,L):(mshare([[L]]),ground([E]))=>(mshare([[L]]),ground([E])). :-prop bst(_A). :-prop min_(_A,_B). :-prop max_(_A,_B). :-prop bst_(_A,_B,_C). :-prop rt2/1+regtype. bsts(_1,_2) :- 'bsts$pre'(_1,_2), 'bsts$cls'(_1,_2). 'bsts$pre'(_2,_1) :- reify_check(bst(_1),[_1],_4), reify_check(num(_2),[_2],_3), _5 is _3/\_4, _6 is _5, _7 is _5, _8 is _6\/_7, warn_if_false(_8,'CP'). 'bsts$cls'(A,B) :- bsts_i(A,B). bsts_i(_3,_4) :- 'bsts_i$pre'(_3,_4), 'bsts_i$cls'(_3,_4). 'bsts_i$pre'(_4,_3) :- reify_check(bst(_3),[_3],_6), reify_check(num(_4),[_4],_5), _7 is _5/\_6, _8 is _7, _9 is _8, warn_if_false(_9,'CP'). 'bsts_i$cls'(E,t(_1,E,_2)) :- !. 'bsts_i$cls'(E,t(L,X,_1)) :- E<X, bsts_i(E,L). 'bsts_i$cls'(E,t(_1,X,R)) :- E>X, bsts_i(E,R). bst(nil). bst(t(nil,_E,nil)) :- !. bst(t(nil,E,R)) :- !, max_(R,Max), bst_(R,E,Max). bst(t(L,E,nil)) :- !, min_(L,Min), bst_(L,Min,E). bst(t(L,E,R)) :- min_(L,Min), max_(R,Max), bst_(L,Min,E), bst_(R,E,Max). min_(nil,_1) :- fail, !. min_(t(nil,E,_1),E) :- !. min_(t(L,_E,_R),Min) :- min_(L,Min). max_(nil,_1) :- fail, !. max_(t(_1,E,nil),E) :- !. max_(t(_L,_E,R),Max) :- max_(R,Max). bst_(nil,_1,_2) :- !. bst_(t(L,E,R),Min,Max) :- Min=<E, E=<Max, bst_(L,Min,E), bst_(R,E,Max). rt2(t(A,B,C)) :- term(A), arithexpression(B), term(C).