:- module(scryerfdj,[run/0]). :- use_module(library(dif)). :- use_module(library(lists)). :- use_module(library(iso_ext)). :- use_module(library(format)). :- use_module(library(time)). :- use_module(library(dcgs)). :- use_module(library(clpz)). :- use_module(library(reif)). /* condor */ :- dynamic(callnr/1). callnr(0). _^G_0 :- G_0. :- multifile(message_hook/3). message_hook(informational, loaded(_,_,_,_,_,_),_). message_hook(informational, loading(_,_,_), _). nextuniquename(Uniquename) :- callnr(N0), N1 is N0+1, number_chars(N0, Chs), atom_chars(Uniquename,[p|Chs]), retractall(callnr(_)), assert(callnr(N1)), ( N0 mod 10000 =:= 0 -> writeq(nr(N0)),nl ; true ). call_compiled(Arg, Goal_0) :- nextuniquename(Uname), Head =.. [Uname,Arg], Rule = ( Head :- Goal_0 ), open(temp(Uname), write, S, [if_exists(generate_unique_name)]), stream_property(S, file_name(Name)), portray_clause(S, Rule), close(S), compile(Name), delete_file(Name), % asserta(Rule), % better! with compile('/dev/null'), call(Uname, Arg), abolish(Uname/1,[force(true)]). condor1(UProc) :- Proc is UProc, % Max is Start + Proc + Mod * Batch, call_nth((between(1,5,N),gst_goal(E,N,0)),Nth), Nth =:= Proc, !, $(Proc^(Nth/N)^uxtestsample(E)), !, halt(-2). run :- ( N = 1; N = 2 ; N = 3 ; N = 4 ; N = 5 ; N = 6 ), % E = (_,_), %E = (_#=_), gst_body(E,N,0), %\+ ( term_subterm(E, S), nonvar(S), ( S = max(_,_) ; S = min(_,_) ; S = div(_,_) ) ), %\+ subsumes_term(_#>max(_,_), E), %subsumes_term((_#=>_#>_), E), %\+ subsumes_term(_#>_,E), %\+ subsumes_term(_#=_,E), %\+ variant(E, (_#>_#<=>_) ), % Segmentation fault %\+ variant(E, (_#>=_#<=>_) ), % segmentation violation %\+ variant(E, (_#=_#<=>_) ), % segmentation violation %\+ variant(E, (_#\=_#<=>_) ), % segmentation violation %\+ variant(E, A#=_/max(A,_) ), % incorrect %\+ variant(E, _#=_/max(_,_) ), % incorrect %\+ variant(E, _#=_/min(_,_) ), % incorrect %\+ variant(E, _/min(_,_)#=_), %\+ variant(E, _/max(_,_)#=_), % \+ \+ ( term_subterm(E,Sub),nonvar(Sub), Sub = nvalue(_,_) ), $(N^uxtestsample_to((_ in {1}\/{3}, E))). term_subterm(A, A). term_subterm(A, S) :- nonvar(A), A =.. [_|As], member(E, As), term_subterm(E, S). eq_utr(A, B) :- subsumes_term(A, B), subsumes_term(B, A). % uxtestsample(A#=_/max(A,_)). /* | ?- ( A=0,B=2,C=3 ; true), A in -1..0, B in 1..2, A#=B/max(A,C), A=0,B=2,C=3. | ?- G=(A=0,B=2,C=3), (G;true), A in -1..0, B in 1..2, A#=B/max(A,C),A=0,B=2. A = 0, B = 2, C = 3, G = (0=0,2=2,3=3) */ list([]) --> []. list([E|Es]) --> [E], list(Es). ... --> [] | [_], ... . :- op(950,fy, [$]). :- op(950,fy, [*]). *_. $(X) :- putnl, portray_clause(call:X), bb_put(current_col,0), catch((X,Res = success),Pat,Res = exc(Pat)), ( Res == time_out -> portray_clause(timeout:X), fail ; Res = exc(Pat) -> putnl, portray_clause(Res:X), bb_put(current_col,0), fail ; putnl, portray_clause(exit:X), bb_put(current_col,0) ). %$(X) :- % portray_clause(fail:X), % fail. list_els_elsxx([A,B,C,D,E,F], [A,B,C,F], [D,E]). %list_els_els([A, B, C, D], [A, B, C, D], []). list_els_els([],[],[]). list_els_els([E|Es], [E|Fs], Gs) :- list_els_els(Es, Fs, Gs). list_els_els([E|Es], Fs, [E|Gs]) :- list_els_els(Es, Fs, Gs). qs3([]). qs3([Z|Zs]) :- (Z in -3..0;Z in 1..3), qs3(Zs). qs5([]). qs5([Z|Zs]) :- (Z in -5..0;Z in 1..5), qs5(Zs). uxtestsample_to(E) :- term_variables(E, Vars), alleq(Vars), term_variables(Vars, UVars), uxtestsample(E,UVars). time_out(Goal_0, _, success) :- Goal_0. domain(Vars, Min,Max) :- Vars ins Min..Max. call_timedout(Goal_0) :- time_out(Goal_0, 300, R), ( R == time_out -> % putnl, % portray_clause(timeout:Goal_0), % bb_put(current_col,0), throw(error(time_out,Goal_0)) ; true ). safecall(Goal_0) :- catch(( Goal_0, R = success ), error(E,IE), R = exc(error(E,IE)) ), ( R == success -> true ; R = exc(error(time_out,_)) -> putcc(t),fail ; R = exc(error(representation_error(max_clpfd_integer),_)) -> putcc(o), fail ; R = exc(error(representation_error(min_clpfd_integer),_)) -> putcc(u), fail ; portray_clause(error(E,IE)), bb_put(current_col, 0), halt ). putnl :- ( bb_get(current_col,0) -> true ; nl, bb_put(current_col,0) ). putcc(Ch) :- ( bb_get(current_col, C0), C0 < 100 -> C1 is C0+1 ; nl, C1 = 0 ), bb_put(current_col,C1), put_char(Ch). uxtestsample(E,Vars) :- XD = domain(Vars,-1000,1000), RangeMax = 3, RangeMin= -3, % Range = (RangeMin..RangeMax), SVars =.. [v|Vars], D = call_timedout(domain(Vars,RangeMin,RangeMax)), D1 = call_timedout(domain(Vars1,RangeMin,RangeMax)), D2 = call_timedout(domain(Vars2,RangeMin,RangeMax)), Q1 = call_timedout(qs3(Vars1)), L = call_timedout(labeling([],Vars)), L1 = call_timedout(labeling([],Vars1)), L2 = call_timedout(labeling([],Vars2)), M = call_timedout(member(SVars,ISols)), I = ( ISols = Sols ), findall(SVars,(D,call_timedout(E),L),Sols), sort(Sols,SolsU), length(Sols,NrSols), ( Sols \== SolsU ; \+ ground(Sols) ; list_els_elsxx(Vars, Vars1, Vars2), Vars1 = [_,_,_,_], Vars2 = [_,_], ( Fall=1,Goals = (XD, D1,L1,E,D,L2) ; Fall=2,Goals = (I,D1,XD,L1,E,M) ; Fall=3,Goals = (XD,D1,E,L1,D2,L2) ; Fall=4,Goals = (D1,D2,L1,E,L2) ; Fall=5,Goals = (I,Q1,XD,E,L1,M) ), % portray_clause(findall(SVars,Goals,Solsx)), %writeq(fall=Fall),nl, findall(SVars,Goals, Solsx), sort(Solsx, SolsxU), ( SolsxU \== SolsU, l_l_diffs(SolsU,SolsxU,Diffs), ( $ ((Fall:Goals:Diffs)^true) -> true ), writeq(ineq), nl ; \+ ( length(Solsx,NrSolsx), NrSolsx == NrSols ), writeq(dl), nl ) ). bug :- uxtestsample_to((_#>A-B,A#<==>B)). l_l_diffs([], [], []). l_l_diffs([], [F|Fs], [+F|Diffs]) :- l_l_diffs([], Fs, Diffs). l_l_diffs([E|Es], [], [-E|Diffs]) :- l_l_diffs(Es, [], Diffs). l_l_diffs([E|Es], [F|Fs], Diffs1) :- compare(R, E, F), ( R = (=), l_l_diffs(Es, Fs, Diffs1) ; R = (<), Diffs1 = [-E|Diffs2], l_l_diffs(Es, [F|Fs], Diffs2) ; R = (>), Diffs1 = [+E|Diffs2], l_l_diffs([E|Es], Fs, Diffs2) ). call_nth(Goal, C) :- State = count(0), Goal, arg(1, State, C1), C2 is C1+1, nb_setarg(1, State, C2), C = C2. g_reifying( #\(A1,A2), A1, A2). g_reifying( #==>(A1,A2), A1, A2). %g_reifying( #<=(A1,A2), A1, A2). g_reifying( #/\(A1,A2), A1, A2). g_reifying( #\/(A1,A2), A1, A2). g_reifying(#<==>(A1,A2), A1, A2). % ! segmentation violation g_arithrel( #>(A1,A2), A1, A2). %g_arithrel( #<(A1,A2), A1, A2). g_arithrel(#>=(A1,A2), A1, A2). %g_arithrel(#=<(A1,A2), A1, A2). g_arithrel( #=(A1,A2), A1, A2). g_arithrel(#\=(A1,A2), A1, A2). g_exprop(-1*E, E). g_exprop(abs(E), E).% infinite g_exprop(mod(E1,E2), E1,E2). %g_exprop(rem(E1,E2), E1,E2). g_exprop(max(E1,E2), E1,E2). g_exprop(min(E1,E2), E1,E2). g_exprop(+(E1,E2), E1,E2). g_exprop(-(E1,E2), E1,E2). g_exprop(*(E1,E2), E1,E2). g_exprop(div(E1,E2), E1,E2). int_to_sx(I0, S0) :- I0 > 0, !, I1 is I0 - 1, S0 = s(S1), int_to_sx(I1, S1). int_to_sx(0, 0). gst_body(G, I0,C) :- int_to_sx(I0, C0), gs_body(G, C0,C). gst_goal(G, I0, C) :- int_to_sx(I0, C0), gs_goal(G, C0,C). gs_body(B, C0,C) :- C0 = s(_), gs_goal(B, C0,C). gs_body((B1,B2), s(C1),C) :- gs_body(B1, C1,C2), gs_body(B2, C2,C). % gs_goal(G, s(C),C) :- % G = all_distinct([_,_,_]). % gs_goal(G, s(C),C) :- % G = element(_,[_,_],_). % gs_goal(G, s(C),C) :- % G = (domain(Zs,-5,5),nvalue(_,Zs)), % Zs = [_,_,_]. gs_goal(G, s(C0),C) :- gs_reifyinggoal(G, C0,C). gs_goal(nvalue(_,[_,_,_]), s(s(C)),C). gs_reifyinggoal(G, C0,C) :- gs_arithrelation(G, C0,C). gs_reifyinggoal(#\G, C1,C) :- gs_boolgoal(G, C1,C). gs_reifyinggoal(G, C1,C) :- g_reifying(G, A1, A2), gs_boolgoal(A1, C1,C2), gs_boolgoal(A2, C2,C). gs_boolgoal(_V, C, C). gs_boolgoal(G, s(C0), C) :- gs_reifyinggoal(G, C0, C). gs_arithrelation(R, C1,C) :- g_arithrel(R, A1, A2), gs_arithexpr(A1, C1,C2), gs_arithexpr(A2, C2,C). gs_arithexpr(_V, C,C). gs_arithexpr(E1, s(C1),C) :- g_exprop(E1,E2), gs_arithexpr(E2, C1,C). gs_arithexpr(E, s(C1),C) :- g_exprop(E, E1, E2), gs_arithexpr(E1, C1,C2), gs_arithexpr(E2, C2,C). seq(Es,Es) --> []. seq([E|Es0],Es) --> [E], seq(Es0,Es). spec(Es0,Es) --> seq(_,_), [E], seq(Es0,Es1), rspec(E,Es1,Es). rspec(E,Es0,Es) --> [E], seq(Es0,Es1), ( {Es1=Es} | rspec(E,Es1,Es) ). alleq(_). alleq(Xs1) :- phrase(spec(Xs2,[]),Xs1), alleq(Xs2).