% Uncomment this for debugging. After that, use :- spy, trace. % to trace everything. % :- codegen_debug. % Uncomment this to eliminate trivial warnings. % :- warning(warning_off). %------------------------------------------------------------------------------ % Standard auxiliary routines %------------------------------------------------------------------------------ append([], B, B). append([X|A], B, [X|C]) :- append(A, B, C). len([], 0). len([_|R], I + 1) :- len(R, I). %------------------------------------------------------------------------------ % Tabling %------------------------------------------------------------------------------ % :- dynamic(subsumed_config0, 1). % :- dynamic(subsumed_config1, 1). % :- dynamic(subsumed_config2, 1). % :- dynamic(subsumed_config3, 1). % :- dynamic(subsumed_config4, 1). % :- dynamic(t0, 3). % :- dynamic(t1, 3). % :- dynamic(t2, 3). % :- dynamic(t3, 3). % :- dynamic(t4, 3). declare_dyn_table :- saved_base(N), declare_dyn_table_aux(N). declare_dyn_table_aux(0). declare_dyn_table_aux(I + 1) :- I >= 0, declare_dyn_table_aux(I), printf_to_atom(N1, "subsumed_config%d", [I]), dynamic(N1, 1), printf_to_atom(N2, "t%d", [I]), dynamic(N2, 3). :- declare_dyn_table. % check_subsumed_config(0, IpIdx) :- % subsumed_config0(IpIdx). % check_subsumed_config(1, IpIdx) :- % subsumed_config1(IpIdx). % check_subsumed_config(2, IpIdx) :- % subsumed_config2(IpIdx). % check_subsumed_config(3, IpIdx) :- % subsumed_config3(IpIdx). % check_subsumed_config(4, IpIdx) :- % subsumed_config4(IpIdx). :- dynamic(check_subsumed_config, 2). gen_check_subsumed_config :- saved_base(N), gen_check_subsumed_config_aux(N). gen_check_subsumed_config_aux(0). gen_check_subsumed_config_aux(I + 1) :- I >= 0, gen_check_subsumed_config_aux(I), printf_to_atom(N1, "subsumed_config%d", [I]), T =.. [N1, IpIdx], assert(check_subsumed_config(I, IpIdx) :- T). :- gen_check_subsumed_config. % check_t(0, IpIdx1, V1, L1) :- % t0(IpIdx1, V1, L1). % check_t(1, IpIdx1, V1, L1) :- % t1(IpIdx1, V1, L1). % check_t(2, IpIdx1, V1, L1) :- % t2(IpIdx1, V1, L1). % check_t(3, IpIdx1, V1, L1) :- % t3(IpIdx1, V1, L1). % check_t(4, IpIdx1, V1, L1) :- % t4(IpIdx1, V1, L1). :- dynamic(check_t, 4). gen_check_t :- saved_base(N), gen_check_t_aux(N). gen_check_t_aux(0). gen_check_t_aux(I + 1) :- I >= 0, gen_check_t_aux(I), printf_to_atom(N1, "t%d", [I]), T =.. [N1, IpIdx, V, L], assert(check_t(I, IpIdx, V, L) :- T). :- gen_check_t. % store_subsumed_config(0, IpIdx) :- % assert(subsumed_config0(IpIdx)). % store_subsumed_config(1, IpIdx) :- % assert(subsumed_config1(IpIdx)). % store_subsumed_config(2, IpIdx) :- % assert(subsumed_config2(IpIdx)). % store_subsumed_config(3, IpIdx) :- % assert(subsumed_config3(IpIdx)). % store_subsumed_config(4, IpIdx) :- % assert(subsumed_config4(IpIdx)). :- dynamic(store_subsumed_config, 2). gen_store_subsumed_config :- saved_base(N), gen_store_subsumed_config_aux(N). gen_store_subsumed_config_aux(0). gen_store_subsumed_config_aux(I + 1) :- I >= 0, gen_store_subsumed_config_aux(I), printf_to_atom(N1, "subsumed_config%d", [I]), T =.. [N1, IpIdx], assert(store_subsumed_config(I, IpIdx) :- assert(T)). :- gen_store_subsumed_config. % store_t(0, IpIdx, V, L) :- % assert(t0(IpIdx, V, L)). % store_t(1, IpIdx, V, L) :- % assert(t1(IpIdx, V, L)). % store_t(2, IpIdx, V, L) :- % assert(t2(IpIdx, V, L)). % store_t(3, IpIdx, V, L) :- % assert(t3(IpIdx, V, L)). % store_t(4, IpIdx, V, L) :- % assert(t4(IpIdx, V, L)). :- dynamic(store_t, 4). gen_store_t :- saved_base(N), gen_store_t_aux(N). gen_store_t_aux(0). gen_store_t_aux(I + 1) :- I >= 0, gen_store_t_aux(I), printf_to_atom(N1, "t%d", [I]), T =.. [N1, IpIdx, V, L], assert(store_t(I, IpIdx, V, L) :- assert(T)). :- gen_store_t. config_to_index(Cfg, N) :- saved_base(Base), config_to_index_aux(Base, Cfg, 0, N). config_to_index_aux(_, [], N, N). config_to_index_aux(Base, [PP|R], N, O) :- config_to_index_aux(Base, R, N * Base + PP, O). table(_IpIdx, Ip, V) :- have_symmetry(1), !, % printf("Intend to use symmetry\n", []), sort_cfg(Ip, Ip1, IpIdx1), % printf("Cfg sorted to %\n", [Ip1]), which_table(Ip1, TableId), % printf("I need to consult table t%d\n", [TableId]), !, table_sym_aux(Ip, V, TableId, IpIdx1). % not subsumed_symmetry(Ip, V, TableId, IpIdx1). table(IpIdx, Ip, V) :- which_table(Ip, TableId), table_nosym_aux(IpIdx, TableId, V). % not subsumed(IpIdx, TableId, V). table_sym_aux(Ip, V, TableId, IpIdx1) :- subsumed_symmetry(Ip, V, TableId, IpIdx1), !, fail. table_sym_aux(_, _, _, _). table_nosym_aux(IpIdx, TableId, V) :- subsumed(IpIdx, TableId, V), !, fail. table_nosym_aux(_, _, _). subsumed_symmetry(_Ip, _V, TableId, IpIdx1) :- check_subsumed_config(TableId, IpIdx1). subsumed_symmetry(Ip, V, TableId, IpIdx1) :- check_t(TableId, IpIdx1, _, _), !, set_counter(symmetry_retry, 0), symmetry(Ip, V, _Ip1, V1), N < 7, counter_value(symmetry_retry, N), add_counter(symmetry_retry, 1), check_t(TableId, IpIdx1, V1, L1), no_solution(L1), !. % subsumed_symmetry(Ip, V, TableId, IpIdx1) :- % symmetry(Ip, V, _Ip1, V1), !, % check_t(TableId, IpIdx1, V1, L1), % no_solution(L1), !. subsumed(IpIdx, TableId, _V) :- check_subsumed_config(TableId, IpIdx). subsumed(IpIdx, TableId, V) :- check_t(TableId, IpIdx, V, L), no_solution(L), !. no_solution([]). no_solution([C|R]) :- no_solution_aux(C), no_solution(R). no_solution_aux(C) :- constrain(C), !, fail. no_solution_aux(_). room_negate(room(L), room(L1)) :- room_negate_aux(L, L1, S), S = 1. room_negate_aux([], [], 0). room_negate_aux([A|R], [0|S], X) :- var(A), !, room_negate_aux(R, S, X). room_negate_aux([0|R], [A|S], A + X) :- !, room_negate_aux(R, S, X). room_negate_aux([1|R], [0|S], X) :- room_negate_aux(R, S, X). negate(quote(A = room(L)), quote(A = L1)) :- var(A), !, room_negate(room(L), L1). negate(quote(room(L) = A), quote(A = L1)) :- var(A), !, room_negate(room(L), L1). negate(quote(A = B), quote(A < B)). negate(quote(A = B), quote(A > B)) :- !. negate(quote(A < B), quote(A >= B)) :- !. negate(quote(A > B), quote(A <= B)) :- !. negate(quote(A <= B), quote(A > B)) :- !. negate(quote(A >= B), quote(A < B)) :- !. negate(quote(real(_)), ff) :- !. negate(A, A). negate_list([], []). negate_list([real(_)|R], S) :- !, negate_list(R, S). negate_list([C|R], [NC|S]) :- negate(C, NC), negate_list(R, S). constrain(quote(A = room(L))) :- var(A), !, A = room(L). constrain(quote(room(L) = A)) :- var(A), !, A = room(L). constrain(quote(room(L1) = room(L2))) :- !, L1 = L2. constrain(quote(A = B)) :- !, numconstrain(A, M), numconstrain(B, N), M = N. constrain(quote(A < B)) :- !, numconstrain(A, M), numconstrain(B, N), M < N. constrain(quote(A > B)) :- !, numconstrain(A, M), numconstrain(B, N), M > N. constrain(quote(A <= B)) :- !, numconstrain(A, M), numconstrain(B, N), M <= N. constrain(quote(A >= B)) :- !, numconstrain(A, M), numconstrain(B, N), M >= N. constrain(_). numconstrain(A, A) :- var(A), !. numconstrain(A, A) :- atomic(A), !. numconstrain(quote(-A), -N) :- !, numconstrain(A, N). numconstrain(quote(A + B), E + F) :- !, numconstrain(A, E), numconstrain(B, F). numconstrain(quote(A - B), E - F) :- !, numconstrain(A, E), numconstrain(B, F). numconstrain(quote(A * B), E * F) :- numconstrain(A, E), numconstrain(B, F). numconstrain(quote(A / B), E / F) :- numconstrain(A, E), numconstrain(B, F). store(IpIdx, Ip, V) :- genvars(V1), dump(V, V1, L), negate_list(L, L1), !, store_aux1(IpIdx, Ip, V1, L1). store_aux1(_IpIdx, Ip, V, L) :- have_symmetry(1), !, symmetry(Ip, V, Ip1, V1), !, config_to_index(Ip1, IpIdx1), store_aux(IpIdx1, Ip1, V1, L). store_aux1(IpIdx, Ip, V, L) :- store_aux(IpIdx, Ip, V, L). store_aux(IpIdx, Ip, _V, []) :- !, which_table(Ip, TableId), store_subsumed_config(TableId, IpIdx). store_aux(IpIdx, Ip, V, L) :- which_table(Ip, TableId), store_t(TableId, IpIdx, V, L). ttest1 :- X < Y, K = 0, store(100, [X, Y, K]). ttest2 :- store(100, [_, _, 3]). ttest3 :- X + 1 = Y, store(200, [X, Y, _]). ttest4 :- store(300, [_, _, _]). %------------------------------------------------------------------------------ % Simplifier % Routines to remove redundant constraints, retaining simpler constraints % whenever possible. %------------------------------------------------------------------------------ consistent_negation(C) :- set_counter(consistent_negation_flag, 0), negate(C, C1), constrain(C1), add_counter(consistent_negation_flag, 1), fail. consistent_negation(_) :- N > 0, counter_value(consistent_negation_flag, N). remove_redundant(_V, []). remove_redundant(V, [x(C, _)|R]) :- consistent_negation(C), !, constrain(C), remove_redundant(V, R). remove_redundant(V, [_|R]) :- remove_redundant(V, R). qsort_f(List, Sorted) :- qsort_f_aux(List, [], Sorted). qsort_f_aux([], Acc, Acc). qsort_f_aux([H|T], Acc, Sorted) :- pivoting_f(H, T, L1, L2), qsort_f_aux(L1, Acc, Sorted1), qsort_f_aux(L2, [H|Sorted1], Sorted). pivoting_f(_H, [], [], []). pivoting_f(x(HF, HS), [x(F, X)|T], [x(F, X)|L], G) :- X >= HS, pivoting_f(x(HF, HS), T, L, G). pivoting_f(x(HF, HS), [x(F, X)|T], L, [x(F, X)|G]) :- X < HS, pivoting_f(x(HF, HS), T, L, G). formula_size(quote(A = B), M + N) :- var(A), var(B), !, numformula_size(A, M), numformula_size(B, N). formula_size(quote(room(_) = A), 2) :- var(A), !. formula_size(quote(A = room(_)), 2) :- var(A), !. formula_size(quote(A = B), M + N) :- !, numformula_size(A, M), numformula_size(B, N). formula_size(quote(A < B), M + N) :- !, numformula_size(A, M), numformula_size(B, N). formula_size(quote(A > B), M + N) :- !, numformula_size(A, M), numformula_size(B, N). formula_size(quote(A <= B), M + N) :- !, numformula_size(A, M), numformula_size(B, N). formula_size(quote(A >= B), M + N) :- !, numformula_size(A, M), numformula_size(B, N). formula_size(_, 0). numformula_size(A, 1) :- var(A), !. numformula_size(A, 1) :- atomic(A), !. numformula_size(A, 1) :- A = [], !. numformula_size(A, 1) :- A = [_|_], !. numformula_size(quote(-A), N) :- !, numformula_size(A, N). numformula_size(quote(A + B), E + F) :- !, numformula_size(A, E), numformula_size(B, F). numformula_size(quote(A - B), E + F) :- !, numformula_size(A, E), numformula_size(B, F). numformula_size(quote(A * B), E + F) :- numformula_size(A, E), numformula_size(B, F). numformula_size(quote(A / B), E + F) :- numformula_size(A, E), numformula_size(B, F). size_formulas([], []). size_formulas([quote(real(_))|R], S) :- !, size_formulas(R, S). size_formulas([C|R], [x(C, N)|S]) :- size_formulas(R, S), formula_size(C, N). constrain_minimally(V, W) :- genvars(W), dump(V, W, L1), size_formulas(L1, L3), !, qsort_f(L3, L4), remove_redundant(W, L4). ctest :- 0 <= X0, 0 <= X1, 0 <= X2, X2 <= X0 + 2, X1 <= 2, X1 <= X0 + 2, X1 <= X2 + 2, 0.5 * X1 + 0.5 * X2 <= X0 + 2, X1 + X2 <= X0 + 4, X2 <= 2, K = [1, 0, 0], constrain_minimally([X0, X1, X2, K], V), dump([V]). ctest2 :- K = 0, J = 0, I = 1, S = 0, Y2 <= Y3 + 10, 0 <= Y2, 5 <= Y3, 10 <= Y1, Y1 <= 20, 0 <= X, Y2 <= 20, Y3 <= 20, constrain_minimally([Y1, Y2, Y3, X, K, J, I, S], V), dump(V, [y1, y2, y3, x, k, j, i, s]). check_invariant(V) :- set_counter(invariant_ok, 0), invariant(V), add_counter(invariant_ok, 1), fail. check_invariant(_) :- X > 0, counter_value(invariant_ok, X). cs(Depth, _, VarLabels, Ip, V) :- start_labels(Ip), start_mem(V), traceit4(Depth, VarLabels, Ip, V). % cs(Depth, Noise, VarLabels, Ip, V) :- % serialtrans(Ip, _, _, _), !, % serialtrans(Ip, V, Ipold, Vold), % constrain_minimally(Vold, Vold1), % sys(Depth, Noise, VarLabels, Ipold, Vold1), % Vold = Vold1, % traceit5(Depth, VarLabels, Ipold, Vold, Ip, V). cs(Depth, Noise, VarLabels, Ip, V) :- traceit2(Noise, VarLabels, Ip, V), add_counter(attempted_node, 1), config_to_index(Ip, IpIdx), table(IpIdx, Ip, V), !, add_counter(unsubsumed_node, 1), store(IpIdx, Ip, V), !, traceit3(Noise), trans(Ipold, Ip, Vold, V), check_invariant(Vold), constrain_minimally(Vold, Vold1), cs(Depth + 1, Noise, VarLabels, Ipold, Vold1), Vold = Vold1, traceit5(Depth, VarLabels, Ipold, Vold, Ip, V). % Noises traceit1(0, _, _, _). traceit1(_, [], _, _). traceit1(Noise, VarLabels, Ip, V) :- not Noise = 0, not VarLabels = [], config_to_index(Ip, IpIdx), printf("Cfg: % (%d)", [Ip, IpIdx]), dump(V, VarLabels). traceit2(0, _, _, _). traceit2(Noise, VarLabels, Ip, V) :- not Noise = 0, traceit1(Noise, VarLabels, Ip, V), % traceit6(Ip), writeln(tried). traceit3(0). traceit3(1) :- writeln(stored). traceit3(Noise) :- not Noise = 0, not Noise = 1, writeln(stored), read(_). traceit4(Depth, VarLabels, Ip, V) :- printf("INIT DEPTH %d\n", [Depth]), traceit1(1, VarLabels, Ip, V). traceit5(Depth, VarLabels, Ipold, Vold, Ip, V) :- printf("TRANS DEPTH %d\n", [Depth]), traceit1(1, VarLabels, Ipold, Vold), printf("---->", []), traceit1(1, VarLabels, Ip, V). traceit6(Ip) :- print_table_config(Ip), !, ls t, ls subsumed_config. traceit6(_). % Pretty print the table showtable(Ip, Labels) :- have_symmetry(1), sort_cfg(Ip, IpIdx), showtable_aux(IpIdx, Labels). showtable(Ip, Labels) :- not have_symmetry(1), config_to_index(Ip, IpIdx), showtable_aux(IpIdx, Labels). showtable(_, _). showtable_aux(IpIdx, Labels) :- printf("Tabled:\n", []), t(IpIdx, Labels, V), printf("Configuration: %d\n", [IpIdx]), printf("%\n", [V]). showtable_aux(_, _). showtable_all(Labels) :- t(N, Labels, V), printf("Configuration: %d\n", [N]), printf("%\n", [V]). showtable_all(_). % Some stats :- dynamic(table_check_ctr, 2), assert(table_check_ctr(-1, -1)). increment_table_check(IpIdx) :- not table_check_ctr(IpIdx, _), !, assert(table_check_ctr(IpIdx, 1)). increment_table_check(IpIdx) :- retract(table_check_ctr(IpIdx, N)), fassert(table_check_ctr(IpIdx, N + 1)), !. stat :- printf("Idx\tCfg\tGroups\tRepeat\tGrp Sizes\n", []), printf("---------------------------------------------------\n", []), set_counter(total_groups, 0), set_counter(total_states, 0), set_counter(total_repeats, 0), set_counter(total_primitives, 0), stat_aux, counter_value(total_groups, TotalGroups), counter_value(total_states, TotalStates), counter_value(total_repeats, TotalRepeats), counter_value(total_primitives, TotalPrimitives), printf("Repeats / Total Primitives : %d / %d\n", [TotalRepeats, TotalPrimitives]), space, counter_value(states, X), printf("Table Size : %d rules\n", [X]), printf("Stored Configurations : %d\n", [TotalStates]), printf("Average no. of Groups / Configuration : %\n", [TotalGroups / TotalStates]). :- dynamic(stated, 1), assert(stated(-1)). stat_aux :- t(IpIdx, _, _), not stated(IpIdx), assert(stated(IpIdx)), stat_repeat(IpIdx, RepeatNo, GroupSizes, PrimitivesNo), stat_aux1(IpIdx, RepeatNo, GroupSizes, PrimitivesNo), fail. stat_aux :- subsumed_config(IpIdx), not stated(IpIdx), assert(stated(IpIdx)), index_to_config(IpIdx, Cfg), cfg_ctrs(Cfg), printf("%d\t%\t%d\t%d\t%\n", [IpIdx, Cfg, 1, 0, [0]]), add_counter(total_groups, 1), add_counter(total_states, 1), fail. stat_aux :- retract(stated(_)), fail. stat_aux :- assert(stated(-1)). stat_aux1(IpIdx, RepeatNo, GroupSizes, PrimitivesNo) :- subsumed_config(IpIdx), !, len(GroupSizes, GroupNo), index_to_config(IpIdx, Cfg), cfg_ctrs(Cfg), printf("%d\t%\t%d\t%d\t%\n", [IpIdx, Cfg, GroupNo + 1, RepeatNo, [0|GroupSizes]]), add_counter(total_repeats, RepeatNo), add_counter(total_groups, GroupNo + 1), add_counter(total_states, 1), add_counter(total_primitives, PrimitivesNo). stat_aux1(IpIdx, RepeatNo, GroupSizes, PrimitivesNo) :- len(GroupSizes, GroupNo), index_to_config(IpIdx, Cfg), cfg_ctrs(Cfg), printf("%d\t%\t%d\t%d\t%\n", [IpIdx, Cfg, GroupNo, RepeatNo, GroupSizes]), add_counter(total_repeats, RepeatNo), add_counter(total_groups, GroupNo), add_counter(total_states, 1), add_counter(total_primitives, PrimitivesNo). stat_repeat(IpIdx, RepeatNo, GroupSizes, PrimitivesNo) :- t(IpIdx, V, _), !, collect_disjunct_lists(IpIdx, V, [], CL_List), !, % dump([CL_List]), read(_), stat_repeat_check(CL_List, RepeatNo), !, stat_lengths(CL_List, GroupSizes, PrimitivesNo). included(A, [A|_]) :- !. included(A, [B|R]) :- not A = B, included(A, R). collect_disjunct_lists(IpIdx, V, CL_List, CL_List) :- not collect_disjunct_lists_aux(IpIdx, V, CL_List), !. collect_disjunct_lists(IpIdx, V, CL_List1, CL_List2) :- t(IpIdx, V, CL), not included(CL, CL_List1), collect_disjunct_lists(IpIdx, V, [CL|CL_List1], CL_List2). collect_disjunct_lists_aux(IpIdx, V, CL_List) :- t(IpIdx, V, CL), not included(CL, CL_List). stat_lengths([], [], 0). stat_lengths([C|R], [L|S], L + M) :- stat_lengths(R, S, M), len(C, L). stat_repeat_check([], 0). stat_repeat_check([CL|CL_List], M + N) :- stat_repeat_check(CL_List, M), % writeln(comparing), % dump([CL, CL_List]), % read(_), repeats(CL, CL_List, N). repeats([], _CL_List, 0). repeats([C|R], CL_List, N + M) :- repeats(R, CL_List, M), repeats_aux(C, CL_List, N). repeats_aux(_C, [], 0). repeats_aux(C, [CL|R], M + N) :- repeats_aux2(C, CL, N), repeats_aux(C, R, M). repeats_aux2(_, [], 0). repeats_aux2(C, [C1|R], N + 1) :- not constrain_both(C, C1), !, % printf("Found repeat: % %\n", [C, C1]), repeats_aux2(C, R, N). repeats_aux2(C, [_|R], N) :- repeats_aux2(C, R, N). constrain_both(C, C1) :- negate(C1, C2), constrain(C), constrain(C2). index_to_config(N, Cfg) :- processnum(P), saved_base(B), index_to_config_aux(P, B, pow(B, P - 1), N, Cfg), !. index_to_config_aux(0, _, _, _, []) :- !. index_to_config_aux(I, B, D, N, [PP|R]) :- xmodulo(N, D, PP, M), index_to_config_aux(I - 1, B, D / B, M, R). % Fast modulo xmodulo(A, B, (((Q1 * B + Q2) * B + Q3) * B + Q4) * B + Q5, C) :- modulo(A, pow(B, 5), Q1, C1), modulo(C1, pow(B, 4), Q2, C2), modulo(C2, pow(B, 3), Q3, C3), modulo(C3, B * B, Q4, C4), modulo(C4, B, Q5, C). modulo(A, B, 0, A) :- A < B, !. modulo(A, B, N + 1, C) :- modulo(A - B, B, N, C). space :- set_counter(states, 0), t(_, _, _), add_counter(states, 1), fail. space :- subsumed_config(_), add_counter(states, 1), fail. space :- add_counter(states, -2). check_config :- cfg_ctrs_init, t(IpIdx, _, _), index_to_config(IpIdx, C), cfg_ctrs(C), fail. check_config :- subsumed_config(IpIdx), index_to_config(IpIdx, C), cfg_ctrs(C), fail. check_config. cfg_ctrs_init :- set_counter(c0, 0), set_counter(c1, 0), set_counter(c2, 0), set_counter(c3, 0), set_counter(c4, 0). % cfg_ctrs([_, 0|_]) :- % add_counter(c0, 1). % cfg_ctrs([_, 1|_]) :- % add_counter(c1, 1). % cfg_ctrs([_, 2|_]) :- % add_counter(c2, 1). % cfg_ctrs([_, 3|_]) :- % add_counter(c3, 1). % cfg_ctrs([_, 4|_]) :- % add_counter(c4, 1). cfg_ctrs([0|_]) :- add_counter(c0, 1). cfg_ctrs([1|_]) :- add_counter(c1, 1). cfg_ctrs([2|_]) :- add_counter(c2, 1). reinitialize :- set_counter(attempted_node, 0), set_counter(unsubsumed_node, 0). % Mutex violation generator mutex_violation(2, _, _, DangerPt, [DangerPt, DangerPt]) :- !. mutex_violation(Len, LowBounds, UpBounds, DangerPt, L) :- have_symmetry(1), !, gen_mutex_violation2(Len, LowBounds, UpBounds, DangerPt, L). mutex_violation(Len, LowBounds, UpBounds, DangerPt, L) :- gen_mutex_violation1(Len, LowBounds, UpBounds, DangerPt, L). gen_mutex_violation1(Len, LowBounds, UpBounds, DangerPt, L) :- N >= 2, gen_mutex_violation1_aux(DangerPt, Len, N, LowBounds, UpBounds, L). gen_mutex_violation1_aux(_, 0, 0, [], [], []). gen_mutex_violation1_aux(DangerPt, I + 1, N, [_|LR], [_|UR], [DangerPt|Out]) :- gen_mutex_violation1_aux(DangerPt, I, N - 1, LR, UR, Out). gen_mutex_violation1_aux(DangerPt, I + 1, N, [L|LR], [U|UR], [X|Out]) :- gen_bounded_int(L, U, X), not X = DangerPt, gen_mutex_violation1_aux(DangerPt, I, N, LR, UR, Out). gen_bounded_int(A, B, A) :- A <= B. gen_bounded_int(A, B, C) :- A <= B, gen_bounded_int(A + 1, B, C). gen_mutex_violation2(Len, LowBounds, UpBounds, DangerPt, [DangerPt, DangerPt|F]) :- LowBounds = [_, _|LowBounds1], UpBounds = [_, _|UpBounds1], gen_mutex_violation2_aux(Len - 2, LowBounds1, UpBounds1, F). %gen_mutex_violation2_aux(0, [], [], []). gen_mutex_violation2_aux(1, [L], [U], [N]) :- gen_bounded_int(L, U, N). gen_mutex_violation2_aux(I + 1, [L|RL], [U|RU], [N, M|R]) :- I >= 1, gen_mutex_violation2_aux(I, RL, RU, [M|R]), N <= M, gen_bounded_int(L, U, N).