1		% (c) 2019-2023 Lehrstuhl fuer Softwaretechnik und Programmiersprachen,
2		% Heinrich Heine Universitaet Duesseldorf
3		% This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html)
4		:- module(smt_symmetry_breaking, [init_graph/0,
5		get_top_level_symmetry_breaking_predicates/3,
6		get_top_level_symmetry_breaking_predicates_decomposed/2,
7		add_symmetry_breaking_predicates/2,
8		get_amount_of_found_sbps/1]).
9
10		:- use_module(library(plunit)).
11		:- use_module(library(codesio), [write_to_codes/2]).
12		:- use_module(library(samsort), [samsort/3]).
13		:- use_module(library(lists), [select/3, maplist/3]).
14		:- use_module(extension('bliss/bliss_interface')).
15		:- use_module(probsrc(b_global_sets), [b_get_global_enumerated_sets/1]).
16		:- use_module(probsrc(bmachine), [b_get_machine_set/1]).
17		:- use_module(probsrc(error_manager), [add_message/2,add_warning/3]).
18		:- use_module(probsrc(b_interpreter_check),[norm_pred_check/2,norm_expr_check/2]).
19		:- use_module(probsrc(tools_meta),[safe_time_out/3]).
20		:- use_module(probsrc(bsyntaxtree), [get_texpr_expr/2,
21		conjunct_predicates/2,
22		conjunction_to_list/2,
23		disjunction_to_list/2,
24		predicate_components_in_scope/3,
25		remove_all_infos_and_ground/2,
26		find_typed_identifier_uses/3,
27		safe_create_texpr/4]).
28
29		% Foundation: "SyMT: Finding Symmetries in SMT formulas" by Areces et al.
30		% Possible improvement (TODO): "Advances in Symmetry Breaking for SAT Modulo Theories" by Dinliwal et al.
31
32		:- dynamic next_color/1, color/2, seen_pred/2, seen_upred/2, seen_expr/2, seen_uexpr/2, node_id_to_ast/2, ast_to_node_id/3.
33		:- volatile next_color/1, color/2, seen_pred/2, seen_upred/2, seen_expr/2, seen_uexpr/2, node_id_to_ast/2, ast_to_node_id/3.
34
35		init_graph :-
36		bliss_interface:init_bliss_interface,
37		bliss_interface:init_directed_graph,
38		retractall(node_id_to_ast(_,_)),
39		retractall(ast_to_node_id(_,_,_)),
40		retractall(seen_pred(_,_)),
41		retractall(seen_upred(_,_)),
42		retractall(seen_expr(_,_)),
43		retractall(seen_uexpr(_,_)),
44		retractall(color(_,_)),
45		asserta(color(arg, 0)), % all argument nodes have the same unique color
46		retractall(next_color(_)),
47		asserta(next_color(1)).
48
49		get_texpr_expr_functor_and_type(b(Expr,Type,_), Expr, Type, Functor) :-
50		functor(Expr, Functor, _).
51
52		%% get_top_level_symmetry_breaking_predicates_decomposed(+SmtFormula, -SBPs).
53		% Decompose constraint into independent components and conjunct symmetry breaking predicates of each component.
54		get_top_level_symmetry_breaking_predicates_decomposed(SmtFormula, SBPs) :-
55		( SmtFormula = b(truth,pred,_)
56		; SmtFormula = b(falsity,pred,_)
57		),
58		!,
59		SBPs = b(truth,pred,[]).
60		get_top_level_symmetry_breaking_predicates_decomposed(SmtFormula, SBPs) :-
61		findall(DeferredSetId, b_get_machine_set(DeferredSetId), DeferredSetIds),
62		predicate_components_in_scope(SmtFormula, DeferredSetIds, Components),
63		b_get_global_enumerated_sets(EnumeratedSets),
64		get_top_level_symmetry_breaking_predicates_from_components(Components, EnumeratedSets, SBPs).
65
66		get_top_level_symmetry_breaking_predicates_from_components([component(SingleComponent,_)|T], EnumeratedSets, SBPs) :-
67		reset_found_sbps,
68		get_top_level_symmetry_breaking_predicates(SingleComponent, EnumeratedSets, CSBPs),
69		log_found_sbps(CSBPs),
70		get_top_level_symmetry_breaking_predicates_from_components(T, CSBPs, EnumeratedSets, SBPs).
71
72		get_top_level_symmetry_breaking_predicates_from_components([], Acc, _, Acc).
73		get_top_level_symmetry_breaking_predicates_from_components([component(SingleComponent,_)|T], Acc, EnumeratedSets, SBPs) :-
74		get_top_level_symmetry_breaking_predicates(SingleComponent, EnumeratedSets, CSBPs),
75		log_found_sbps(CSBPs),
76		conjunct_predicates([Acc,CSBPs], NAcc),
77		get_top_level_symmetry_breaking_predicates_from_components(T, NAcc, EnumeratedSets, SBPs).
78
79		%% get_top_level_symmetry_breaking_predicates(+SmtFormula, +EnumeratedSets, -SBPs).
80		% Assuming that the AST has been normalized by B AST cleanup.
81		get_top_level_symmetry_breaking_predicates(SmtFormula, EnumeratedSets, SBPs) :-
82		get_top_level_symmetry_breaking_predicates(SmtFormula, EnumeratedSets, SBPs, _).
83
84		%% get_top_level_symmetry_breaking_predicates(+SmtFormula, -SBPs, -Generators).
85		get_top_level_symmetry_breaking_predicates(SmtFormula, EnumeratedSets, SBPs, Generators) :-
86		find_typed_identifier_uses(SmtFormula, [], UsedIds),
87		remove_all_infos_and_ground(SmtFormula, CSmtFormula),
88		order_variables(UsedIds, _TypeOrdering, VariableOrdering),
89		( VariableOrdering == []
90		-> SBPs = b(truth,pred,[])
91		; init_graph,
92		build_colored_graph(CSmtFormula),
93		%graph_to_dot_file('sym_graph.dot'),
94		!,
95		bliss_interface:find_automorphisms(TGenerators),
96		%nl, write('Generators: '), write(Generators),nl,
97		get_sbps_from_generators(TGenerators, VariableOrdering, EnumeratedSets, TSBPs),
98		!,
99		SBPs = TSBPs,
100		Generators = TGenerators
101		).
102
103		get_amount_of_found_sbps(FoundSBPs) :-
104		found_sbps(FoundSBPs).
105
106		:- dynamic found_sbps/1.
107		:- volatile found_sbps/1.
108
109		found_sbps(0).
110
111		reset_found_sbps :-
112		retractall(found_sbps(_)),
113		asserta(found_sbps(0)).
114
115		log_found_sbps(SymBreakPs) :-
116		SymBreakPs \= b(truth,pred,_),
117		conjunction_to_list(SymBreakPs, L),
118		length(L, Len),
119		retract(found_sbps(FoundSBPs)),
120		NFoundSBPs is FoundSBPs + Len,
121		asserta(found_sbps(NFoundSBPs)).
122		log_found_sbps(_).
123
124		%% add_symmetry_breaking_predicates(+SmtFormula, -NSmtFormula).
125		% Adds symmetry breaking predicates to quantifiers as well.
126		add_symmetry_breaking_predicates(SmtFormula, NSmtFormula) :-
127		reset_found_sbps,
128		b_get_global_enumerated_sets(EnumeratedSets),
129		safe_time_out(add_symmetry_breaking_predicates(SmtFormula, EnumeratedSets, NSmtFormula), 10000, TORes),
130		( TORes == time_out
131		-> NSmtFormula = SmtFormula
132		; true
133		).
134
135		%% add_symmetry_breaking_predicates(+SmtFormula, +EnumeratedSets, -NSmtFormula).
136		add_symmetry_breaking_predicates(SmtFormula, EnumeratedSets, NSmtFormula) :-
137		( get_top_level_symmetry_breaking_predicates(SmtFormula, EnumeratedSets, SymBreakPs)
138		-> log_found_sbps(SymBreakPs)
139		; add_message(smt_symmetry_breaking, 'Skip top-level symmetry breaking due to failure'),
140		SymBreakPs = b(truth,pred,[])
141		),
142		add_sbps_to_quantifiers(SmtFormula, EnumeratedSets, TSmtFormula),
143		safe_create_texpr(conjunct(SymBreakPs,TSmtFormula), pred, [] ,NSmtFormula).
144
145		%% add_sbps_to_quantifiers(+Ast, +EnumeratedSets, -SmtFormula).
146		add_sbps_to_quantifiers(b(Expr,Type,Info), EnumeratedSets, NSmtFormula) :-
147		!,
148		add_sbps_to_quantifiers_expr(Expr, EnumeratedSets, NExpr),
149		safe_create_texpr(NExpr, Type, Info, NSmtFormula).
150		add_sbps_to_quantifiers(Formula, _, Formula).
151
152		add_sbps_to_quantifiers_expr(forall(Ids,Lhs,Rhs), EnumeratedSets, NExpr) :-
153		!,
154		get_top_level_symmetry_breaking_predicates(Rhs, EnumeratedSets, SBPs),
155		log_found_sbps(SBPs),
156		add_sbps_to_quantifiers(Rhs, EnumeratedSets, NRhs),
157		( SBPs = b(truth,pred,_)
158		-> NExpr = forall(Ids,Lhs,NRhs)
159		; safe_create_texpr(conjunct(SBPs,Lhs), pred, [], NLhs),
160		NExpr = forall(Ids,NLhs,NRhs)
161		).
162		add_sbps_to_quantifiers_expr(exists(Ids,Body), EnumeratedSets, NExpr) :-
163		!,
164		get_top_level_symmetry_breaking_predicates(Body, EnumeratedSets, SBPs),
165		log_found_sbps(SBPs),
166		add_sbps_to_quantifiers(Body, EnumeratedSets, NBody),
167		( SBPs = b(truth,pred,_)
168		-> NExpr = exists(Ids,NBody)
169		; safe_create_texpr(conjunct(SBPs,NBody), pred, [], NNBody),
170		NExpr = exists(Ids,NNBody)
171		).
172		add_sbps_to_quantifiers_expr(Expr, _, NExpr) :-
173		( is_interpreted_symbol(Expr)
174		; is_uninterpreted_symbol(Expr)
175		),
176		!,
177		NExpr = Expr.
178		add_sbps_to_quantifiers_expr(Expr, EnumeratedSets, NExpr) :-
179		functor(Expr, Functor, 2),
180		!,
181		arg(1, Expr, Arg1),
182		arg(2, Expr, Arg2),
183		add_sbps_to_quantifiers(Arg1, EnumeratedSets, NArg1),
184		add_sbps_to_quantifiers(Arg2, EnumeratedSets, NArg2),
185		functor(NExpr, Functor, 2),
186		arg(1, NExpr, NArg1),
187		arg(2, NExpr, NArg2).
188		add_sbps_to_quantifiers_expr(Expr, EnumeratedSets, NExpr) :-
189		functor(Expr, Functor, 1),
190		!,
191		arg(1, Expr, Arg),
192		add_sbps_to_quantifiers(Arg, EnumeratedSets, NArg),
193		functor(NExpr, Functor, 1),
194		arg(1, NExpr, NArg).
195		add_sbps_to_quantifiers_expr(Expr, _, Expr).
196
197		%% get_sbps_from_generators(+Generators, +VariableOrdering, -SBPs).
198		get_sbps_from_generators(Generators, VariableOrdering, EnumeratedSets, SBPs) :-
199		add_sbps_from_generators(Generators, VariableOrdering, EnumeratedSets, b(truth,pred,[]), SBPs).
200
201		%% add_sbps_from_generators(+Generators, +VariableOrdering, +Acc, -SBPs).
202		add_sbps_from_generators([], _, _, Acc, Acc).
203		add_sbps_from_generators([Generator|T], VariableOrdering, EnumeratedSets, Acc, SBPs) :-
204		add_sbps_from_generator(VariableOrdering, Generator, EnumeratedSets, Acc , NAcc),
205		add_sbps_from_generators(T, VariableOrdering, EnumeratedSets, NAcc, SBPs).
206
207		%% add_sbps_from_generator(+Generators, +VariableOrdering, +Acc, -SBPs).
208		add_sbps_from_generator([], _, _, Acc, Acc).
209		add_sbps_from_generator([FirstVarAst|T], Generator, EnumeratedSets, Acc, NAcc) :-
210		FirstVarAst = b(Node,_,_),
211		ast_to_node_id(Node, NType, FirstVarId), % use stored type since it can e.g. be either set(couple(integer,boolean)) or seq(boolean)
212		NFirstVarAst = b(Node,NType,[]),
213		!,
214		image_of_generator(Generator, FirstVarId, ImageId),
215		node_id_to_ast(ImageId, ImageAst),
216		get_texpr_expr(ImageAst, Id1),
217		( Id1 == Node
218		-> % tautology
219		add_sbps_from_generator(T, Generator, EnumeratedSets, Acc, NAcc)
220		; safe_create_texpr(equal(NFirstVarAst,ImageAst), pred, [], Eq),
221		( (
222		\+ has_enumerated_set_type(NFirstVarAst, EnumeratedSets),
223		less_eq_for_type_except_enumerated_set(NFirstVarAst, ImageAst, LEq)
224		)
225		-> extend_conj_acc(Acc, LEq, NAcc1)
226		; NAcc1 = Acc
227		),
228		add_sbps_from_generator_eq_acc(T, Generator, Eq, EnumeratedSets, NAcc1, NAcc)
229		).
230		add_sbps_from_generator([FirstVarAst|_], _, _, _, _) :-
231		add_warning(smt_symmetry_breaking, 'Missing node id in symmetry breaking graph for AST ', [FirstVarAst]), !,
232		fail.
233
234		%% image_of_generator(+Generator, +Id, -ImageId).
235		image_of_generator([], Id, Id). % identity
236		image_of_generator([Cycle|_], Id, ImageId) :-
237		image_of_cycle(false, Cycle, Id, TImageId),
238		!,
239		ImageId = TImageId.
240		image_of_generator([_|T], Id, ImageId) :-
241		image_of_generator(T, Id, ImageId).
242
243		image_of_cycle(MapLastToFirst, [FirstCycleId|T], Id, ImageId) :-
244		image_of_cycle(MapLastToFirst, [FirstCycleId|T], FirstCycleId, Id, ImageId).
245
246		%% image_of_cycle(+MapLastToFirst, +FirstCycleId, +Id, -ImageId).
247		% Tautologies are generated in symmetry breaking if last element maps to first.
248		image_of_cycle(true, [Id], ImageId, Id, ImageId).
249		image_of_cycle(false, [Id], _, Id, Id).
250		image_of_cycle(_, [Id,TImageId|_], _, Id, ImageId) :-
251		ImageId = TImageId.
252		image_of_cycle(MapLastToFirst, [_|T], FirstCycleId, Id, ImageId) :-
253		image_of_cycle(MapLastToFirst, T, FirstCycleId, Id, ImageId).
254
255		%% add_sbps_from_generator(+VariableOrdering, +Generator, +EqAcc, +EnumeratedSets, +Acc, -NAcc).
256		add_sbps_from_generator_eq_acc([], _, _, _, Acc, Acc).
257		add_sbps_from_generator_eq_acc([VarAst|T], Generator, EqAcc, EnumeratedSets, Acc, NAcc) :-
258		VarAst = b(Node,_,_),
259		ast_to_node_id(Node, NType, VarId),
260		NVarAst = b(Node,NType,[]),
261		image_of_generator(Generator, VarId, ImageId),
262		node_id_to_ast(ImageId, ImageAst),
263		get_texpr_expr(ImageAst, Id1),
264		( Id1 == Node
265		-> % tautology
266		add_sbps_from_generator_eq_acc(T, Generator, EqAcc, EnumeratedSets, Acc, NAcc)
267		; safe_create_texpr(equal(NVarAst,ImageAst), pred, [], Eq),
268		( (
269		\+ has_enumerated_set_type(NVarAst, EnumeratedSets),
270		less_eq_for_type_except_enumerated_set(NVarAst, ImageAst, LEq)
271		)
272		-> safe_create_texpr(negation(EqAcc), pred, [], NegEqAcc),
273		safe_create_texpr(disjunct(NegEqAcc,LEq), pred, [], Impl),
274		extend_conj_acc(Acc, Impl, NAcc1),
275		safe_create_texpr(conjunct(EqAcc,Eq), pred, [], NEqAcc)
276		; NAcc1 = Acc,
277		NEqAcc = EqAcc
278		),
279		add_sbps_from_generator_eq_acc(T, Generator, NEqAcc, EnumeratedSets, NAcc1, NAcc)
280		).
281
282		% Enumerated sets are already ordered in ProB and thus do not contain any symmetries.
283		% In fact, when breaking symmetries for enumerated sets again we'd need to respect the internal ordering of ProB! (see get_ordering_for_enumerated_set_elements/4)
284		has_enumerated_set_type(b(_,Type,_), EnumeratedSets) :-
285		Type = global(EnumSet),
286		member(EnumSet, EnumeratedSets).
287
288		%% less_eq_for_type_except_enumerated_set(+VarAst, +ImageAst, -LEq).
289		less_eq_for_type_except_enumerated_set(VarAst, ImageAst, LEq) :-
290		OrderedList = [VarAst,ImageAst],
291		LEq = b(external_pred_call('LEQ_SYM', OrderedList),pred,[]).
292		less_eq_for_type_except_enumerated_set(VarAst, ImageAst, _) :-
293		VarAst = b(_,TypeA,_),
294		ImageAst = b(_,TypeB,_),
295		TypeA \== TypeB,
296		% don't throw an error here since we fail and CDCL(T) can try to solve without symmetry breaking
297		add_warning(less_eq_for_type_except_enumerated_set, 'Differently typed permutation mapping. Encoding for SMT symmetry breaking is defective.', [VarAst,ImageAst]), !,
298		fail.
299
300		%% extend_conj_acc(+Acc, +TConj, -Acc).
301		extend_conj_acc(b(truth,pred,[]), TConj, Conj) :-
302		!,
303		Conj = TConj.
304		extend_conj_acc(Acc, Conj, b(conjunct(Acc,Conj),pred,[])).
305
306		add_nodes_from_ast_list_commutative(_, []).
307		add_nodes_from_ast_list_commutative(RootNodeId, [Id|T]) :-
308		get_texpr_expr_functor_and_type(Id, IdExpr, IdType, IdFunctor),
309		add_term_and_symbol_nodes_to_graph(IdExpr, IdType, IdFunctor, IdRootNodeId),
310		add_node_to_colored_graph(arg, IdExpr, IdType, IdNodeId),
311		bliss_interface:add_edge(IdNodeId, IdRootNodeId),
312		bliss_interface:add_edge(RootNodeId, IdNodeId),
313		build_colored_graph(IdExpr, IdType, IdRootNodeId),
314		add_nodes_from_ast_list_commutative(RootNodeId, T).
315
316		split_associative_node(conjunct(A,B), AstList) :-
317		!,
318		conjunction_to_list(b(conjunct(A,B),pred,[]), AstList).
319		split_associative_node(disjunct(A,B), AstList) :-
320		!,
321		disjunction_to_list(b(disjunct(A,B),pred,[]), AstList).
322		split_associative_node(Expr, AstList) :-
323		functor(Expr, Functor, 2),
324		member(Functor, [add,multiplication,union,intersection]),
325		associative_ast_to_list(Functor, b(Expr,_,_), AstList).
326
327		associative_ast_to_list(Functor, Expr, AstList) :-
328		associative_ast_to_list(Functor, Expr, [], AstList).
329
330		associative_ast_to_list(Functor, b(Expr,_,_), Acc, AstList) :-
331		functor(Expr, Functor, 2),
332		!,
333		arg(1, Expr, Arg1),
334		arg(2, Expr, Arg2),
335		associative_ast_to_list(Functor, Arg1, Acc, NAcc),
336		associative_ast_to_list(Functor, Arg2, NAcc, AstList).
337		associative_ast_to_list(_, Ast, Acc, [Ast|Acc]).
338
339		%% build_colored_graph(+SmtFormula).
340		build_colored_graph(SmtFormula) :-
341		get_texpr_expr_functor_and_type(SmtFormula, Expr, Type, ExprFunctor),
342		add_term_and_symbol_nodes_to_graph(Expr, Type, ExprFunctor, RootNodeId),
343		build_colored_graph(Expr, Type, RootNodeId).
344
345		%% build_colored_graph(+Term, +TermRootNodeId).
346		build_colored_graph(truth, pred, _) :-
347		!.
348		build_colored_graph(falsity, pred, _) :-
349		!.
350		build_colored_graph(Expr, _, RootNodeId) :-
351		( Expr = set_extension(List)
352		; Expr = sequence_extension(List)
353		; Expr = rec(List)
354		),
355		!,
356		build_colored_graph_from_set(List, RootNodeId).
357		build_colored_graph(Expr, Type, RootNodeId) :-
358		( Expr = let_predicate(Ids, EqVals, Body)
359		; Expr = let_expression(Ids, EqVals, Body)
360		; Expr = lazy_let_pred(Ids, EqVals, Body)
361		),
362		!,
363		% non-commutative
364		zip_to_equalities_conj(Ids, EqVals, EqsConj),
365		get_texpr_expr_functor_and_type(EqsConj, EqsExpr, EqsType, EqsFunctor),
366		get_texpr_expr_functor_and_type(Body, BodyExpr, BodyType, BodyFunctor),
367		add_term_and_symbol_nodes_to_graph(EqsExpr, EqsType, EqsFunctor, EqsRootNodeId),
368		add_term_and_symbol_nodes_to_graph(BodyExpr, BodyType, BodyFunctor, BodyRootNodeId),
369		add_node_to_colored_graph(arg, EqsExpr, EqsType, EqsNodeId),
370		add_node_to_colored_graph(arg, BodyExpr, BodyType, BodyNodeId),
371		bliss_interface:add_edge(EqsNodeId, EqsRootNodeId),
372		bliss_interface:add_edge(BodyNodeId, BodyRootNodeId),
373		bliss_interface:add_edge(EqsNodeId, BodyNodeId),
374		bliss_interface:add_edge(RootNodeId, EqsNodeId),
375		build_colored_graph(EqsExpr, EqsType, EqsRootNodeId),
376		build_colored_graph(BodyExpr, Type, BodyRootNodeId).
377		build_colored_graph(partition(Set,AstList), _, RootNodeId) :-
378		!,
379		get_texpr_expr_functor_and_type(Set, SetExpr, SetType, SetFunctor),
380		add_term_and_symbol_nodes_to_graph(SetExpr, SetType, SetFunctor, SetRootNodeId),
381		add_nodes_from_ast_list_commutative(RootNodeId, AstList),
382		add_node_to_colored_graph(arg, SetExpr, SetType, SetNodeId),
383		bliss_interface:add_edge(SetNodeId, SetRootNodeId),
384		bliss_interface:add_edge(RootNodeId, SetNodeId),
385		build_colored_graph(SetExpr, SetType, SetRootNodeId).
386		build_colored_graph(if_then_else(Cond,If,Else), _, RootNodeId) :-
387		% non-commutative
388		!,
389		get_texpr_expr_functor_and_type(Cond, CondExpr, CondType, CondFunctor),
390		get_texpr_expr_functor_and_type(If, IfExpr, IfType, IfFunctor),
391		get_texpr_expr_functor_and_type(Else, ElseExpr, ElseType, ElseFunctor),
392		add_term_and_symbol_nodes_to_graph(CondExpr, CondType, CondFunctor, CondRootNodeId),
393		add_term_and_symbol_nodes_to_graph(IfExpr, IfType, IfFunctor, IfRootNodeId),
394		add_term_and_symbol_nodes_to_graph(ElseExpr, ElseType, ElseFunctor, ElseRootNodeId),
395		add_node_to_colored_graph(arg, CondExpr, CondType, CondNodeId),
396		add_node_to_colored_graph(arg, IfExpr, IfType, IfNodeId),
397		add_node_to_colored_graph(arg, ElseExpr, ElseType, ElseNodeId),
398		bliss_interface:add_edge(CondNodeId, CondRootNodeId),
399		bliss_interface:add_edge(IfNodeId, IfRootNodeId),
400		bliss_interface:add_edge(ElseNodeId, ElseRootNodeId),
401		bliss_interface:add_edge(CondNodeId, IfNodeId),
402		bliss_interface:add_edge(IfNodeId, ElseNodeId),
403		bliss_interface:add_edge(RootNodeId, CondNodeId),
404		build_colored_graph(CondExpr, CondType, CondRootNodeId),
405		build_colored_graph(IfExpr, IfType, IfRootNodeId),
406		build_colored_graph(ElseExpr, ElseType, ElseRootNodeId).
407		build_colored_graph(assertion_expression(Cond,_ErrMsg,Expr), _, RootNodeId) :-
408		% non-commutative
409		!,
410		get_texpr_expr_functor_and_type(Cond, CondExpr, CondType, CondFunctor),
411		get_texpr_expr_functor_and_type(Expr, ExprExpr, ExprType, ExprFunctor),
412		add_term_and_symbol_nodes_to_graph(CondExpr, CondType, CondFunctor, CondRootNodeId),
413		add_term_and_symbol_nodes_to_graph(ExprExpr, ExprType, ExprFunctor, ExprRootNodeId),
414		add_node_to_colored_graph(arg, CondExpr, CondType, CondNodeId),
415		add_node_to_colored_graph(arg, ExprExpr, ExprType, ExprNodeId),
416		bliss_interface:add_edge(CondNodeId, CondRootNodeId),
417		bliss_interface:add_edge(ExprNodeId, ExprRootNodeId),
418		bliss_interface:add_edge(CondNodeId, ExprNodeId),
419		bliss_interface:add_edge(RootNodeId, CondNodeId),
420		build_colored_graph(CondExpr, CondType, CondRootNodeId),
421		build_colored_graph(ExprExpr, ExprType, ExprRootNodeId).
422		build_colored_graph(forall(Ids,Lhs,Rhs), pred, RootNodeId) :-
423		!,
424		( Lhs = b(truth,pred,_) % typing information might have been removed
425		-> Body = Rhs
426		; Body = b(implication(Lhs,Rhs),pred,[])
427		),
428		create_nodes_for_ids(Ids),
429		get_texpr_expr_functor_and_type(Body, BodyExpr, BodyType, BodyFunctor),
430		add_term_and_symbol_nodes_to_graph(BodyExpr, BodyType, BodyFunctor, ArgRootNodeId),
431		add_node_to_colored_graph(arg, BodyExpr, BodyType, ArgNodeId),
432		bliss_interface:add_edge(ArgNodeId, ArgRootNodeId),
433		bliss_interface:add_edge(RootNodeId, ArgNodeId),
434		build_colored_graph(BodyExpr, BodyType, ArgRootNodeId).
435		build_colored_graph(Expr, _, RootNodeId) :-
436		( Expr = comprehension_set(Ids,Body)
437		; Expr = exists(Ids,Body)
438		),
439		!,
440		create_nodes_for_ids(Ids),
441		get_texpr_expr_functor_and_type(Body, BodyExpr, BodyType, BodyFunctor),
442		add_term_and_symbol_nodes_to_graph(BodyExpr, BodyType, BodyFunctor, ArgRootNodeId),
443		add_node_to_colored_graph(arg, BodyExpr, BodyType, ArgNodeId),
444		bliss_interface:add_edge(ArgNodeId, ArgRootNodeId),
445		bliss_interface:add_edge(RootNodeId, ArgNodeId),
446		build_colored_graph(BodyExpr, BodyType, ArgRootNodeId).
447		build_colored_graph(Fun, _, RootNodeId) :-
448		functor(Fun, Functor, 3),
449		member(Functor, [lambda,general_sum,general_product,quantified_union,quantified_intersection]),
450		arg(2, Fun, Pred),
451		arg(3, Fun, LExpr),
452		% non-commutative
453		!,
454		get_texpr_expr_functor_and_type(LExpr, LExprExpr, LExprType, LExprFunctor),
455		get_texpr_expr_functor_and_type(Pred, PredExpr, PredType, PredFunctor),
456		add_term_and_symbol_nodes_to_graph(LExpr, LExprExpr, LExprFunctor, LExprRootNodeId),
457		add_term_and_symbol_nodes_to_graph(Pred, PredType, PredFunctor, PredRootNodeId),
458		add_node_to_colored_graph(arg, LExprExpr, LExprType, LExprNodeId),
459		add_node_to_colored_graph(arg, PredExpr, PredType, PredNodeId),
460		bliss_interface:add_edge(LExprNodeId, LExprRootNodeId),
461		bliss_interface:add_edge(PredNodeId, PredRootNodeId),
462		bliss_interface:add_edge(LExprNodeId, PredNodeId),
463		bliss_interface:add_edge(RootNodeId, LExprNodeId),
464		build_colored_graph(LExprExpr, LExprType, LExprRootNodeId),
465		build_colored_graph(PredExpr, PredType, PredRootNodeId).
466		build_colored_graph(record_field(Record, FieldName), Type, RootNodeId) :-
467		% treated as a non-commutative operator but needs special case since the field name is just a Prolog atom and no B AST node
468		!,
469		get_texpr_expr_functor_and_type(Record, RecordExpr, RecordType, RecordFunctor),
470		add_term_and_symbol_nodes_to_graph(RecordExpr, RecordType, RecordFunctor, RecordRootNodeId),
471		( have_seen_expr(FieldName, Type, TNodeId)
472		-> FieldNameRootNodeId = TNodeId
473		; get_next_color(Color),
474		bliss_interface:add_node(FieldName, Color, FieldNameRootNodeId),
475		log_seen_expr(FieldName, Type, FieldNameRootNodeId)
476		%asserta(ast_to_node_id(Term,Type,RootNodeId))
477		%asserta(node_id_to_ast(RootNodeId,b(Term,Type,[])))
478		),
479		add_node_to_colored_graph(arg, RecordExpr, RecordType, RecordNodeId),
480		add_node_to_colored_graph(arg, FieldName, record_key, FieldNameNodeId), % use an artificial type record_key
481		% one edge from the argument node to the argument's root node
482		bliss_interface:add_edge(RecordNodeId, RecordRootNodeId),
483		bliss_interface:add_edge(FieldNameNodeId, FieldNameRootNodeId),
484		% edge from first to second argument to represent the ordering
485		bliss_interface:add_edge(RecordNodeId, FieldNameNodeId),
486		% add an edge from the root node to the first argument's argument node
487		bliss_interface:add_edge(RootNodeId, RecordNodeId),
488		build_colored_graph(RecordExpr, RecordType, RecordRootNodeId).
489		build_colored_graph(Binary, _Type, RootNodeId) :-
490		functor(Binary, Functor, Arity),
491		Arity == 2,
492		is_associative(Functor),
493		!,
494		split_associative_node(Binary, AstList),
495		add_nodes_from_ast_list_commutative(RootNodeId, AstList).
496		build_colored_graph(Binary, _Type, RootNodeId) :-
497		functor(Binary, Functor, Arity),
498		Arity == 2,
499		\+ is_binary_interpreted_symbol(Binary),
500		!,
501		arg(1, Binary, Arg1),
502		arg(2, Binary, Arg2),
503		get_texpr_expr_functor_and_type(Arg1, Arg1Expr, Arg1Type, Arg1Functor),
504		get_texpr_expr_functor_and_type(Arg2, Arg2Expr, Arg2Type, Arg2Functor),
505		% root nodes for arguments
506		add_term_and_symbol_nodes_to_graph(Arg1Expr, Arg1Type, Arg1Functor, Arg1RootNodeId),
507		add_term_and_symbol_nodes_to_graph(Arg2Expr, Arg2Type, Arg2Functor, Arg2RootNodeId),
508		( is_commutative_but_not_associative(Functor)
509		-> % add an edge from the root node to the root node of each argument
510		bliss_interface:add_edge(RootNodeId, Arg1RootNodeId),
511		bliss_interface:add_edge(RootNodeId, Arg2RootNodeId)
512		; % special argument node for each argument
513		add_node_to_colored_graph(arg, Arg1Expr, Arg1Type, Arg1NodeId),
514		add_node_to_colored_graph(arg, Arg2Expr, Arg2Type, Arg2NodeId),
515		% one edge from the argument node to the argument's root node
516		bliss_interface:add_edge(Arg1NodeId, Arg1RootNodeId),
517		bliss_interface:add_edge(Arg2NodeId, Arg2RootNodeId),
518		% edge from first to second argument to represent the ordering
519		bliss_interface:add_edge(Arg1NodeId, Arg2NodeId),
520		% add an edge from the root node to the first argument's argument node
521		bliss_interface:add_edge(RootNodeId, Arg1NodeId)
522		),
523		build_colored_graph(Arg1Expr, Arg1Type, Arg1RootNodeId),
524		build_colored_graph(Arg2Expr, Arg2Type, Arg2RootNodeId).
525		build_colored_graph(Term, _, _) :-
526		( is_interpreted_symbol(Term)
527		; is_uninterpreted_symbol(Term)
528		),
529		!.
530		build_colored_graph(Unary, _Type, RootNodeId) :-
531		functor(Unary, _Functor, Arity),
532		Arity == 1,
533		!,
534		arg(1, Unary, Arg),
535		get_texpr_expr_functor_and_type(Arg, ArgExpr, ArgType, ArgFunctor),
536		% root node for argument
537		add_term_and_symbol_nodes_to_graph(ArgExpr, ArgType, ArgFunctor, ArgRootNodeId),
538		% special argument node for each argument
539		add_node_to_colored_graph(arg, ArgExpr, ArgType, ArgNodeId),
540		% one edge from the argument node to the argument's root node
541		bliss_interface:add_edge(ArgNodeId, ArgRootNodeId),
542		% add an edge from the root node to the first argument's argument node
543		bliss_interface:add_edge(RootNodeId, ArgNodeId),
544		build_colored_graph(ArgExpr, ArgType, ArgRootNodeId).
545		build_colored_graph(Expr, _Type, _ExprRootNodeId) :-
546		add_warning(smt_symmetry_breaking, 'Missing implementation in build_colored_graph/3 for: ', [Expr]), !,
547		fail.
548
549		%% build_colored_graph_from_set(+List, +RootNodeId).
550		build_colored_graph_from_set([], _).
551		build_colored_graph_from_set([Elm|T], RootNodeId) :-
552		% commutative
553		( Elm = field(_,FieldElm) % Note: we treat records as sets for symmetry breaking, i.e., it's just a collection with no order
554		-> get_texpr_expr_functor_and_type(FieldElm, ElmExpr, ElmType, ElmFunctor)
555		; get_texpr_expr_functor_and_type(Elm, ElmExpr, ElmType, ElmFunctor)
556		),
557		add_term_and_symbol_nodes_to_graph(ElmExpr, ElmType, ElmFunctor, ElmRootNodeId),
558		bliss_interface:add_edge(RootNodeId, ElmRootNodeId),
559		build_colored_graph(ElmExpr, ElmType, ElmRootNodeId),
560		build_colored_graph_from_set(T, RootNodeId).
561
562		create_nodes_for_ids([]).
563		create_nodes_for_ids([b(identifier(Id),Type,_)|T]) :-
564		add_term_and_symbol_nodes_to_graph(identifier(Id), Type, identifier, _),
565		create_nodes_for_ids(T).
566
567		have_seen_expr(Term, Type, NodeId) :-
568		norm_expr_check(b(Term,Type,[]), Norm),
569		seen_expr(Norm, NodeId).
570
571		have_seen_pred(Term, NodeId) :-
572		norm_pred_check(b(Term,pred,[]), Norm),
573		seen_pred(Norm, NodeId).
574
575		log_seen_expr(Term, Type, RootNodeId) :-
576		norm_expr_check(b(Term,Type,[]), Norm),
577		asserta(seen_expr(Norm, RootNodeId)).
578
579		log_seen_pred(Term, RootNodeId) :-
580		norm_pred_check(b(Term,pred,[]), Norm),
581		asserta(seen_pred(Norm, RootNodeId)).
582
583		%% add_term_and_symbol_nodes_to_graph(+Term, +Type, +Functor, -RootNodeId).
584		% Add a root node for compound term f(t1,...,tn). Add an edge from the root node to the (unique) symbol node for f.
585		% Add a node for (un)interpreted symbols.
586		add_term_and_symbol_nodes_to_graph(Term, Type, _, RootNodeId) :-
587		is_interpreted_symbol(Term),
588		( have_seen_expr(Term, Type, TNodeId)
589		-> TRootNodeId = TNodeId
590		; get_next_color(Color),
591		term_to_label(Term, ATerm),
592		bliss_interface:add_node(ATerm, Color, RootNodeId),
593		log_seen_expr(Term, Type, RootNodeId)
594		%asserta(ast_to_node_id(Term,Type,RootNodeId))
595		%asserta(node_id_to_ast(RootNodeId,b(Term,Type,[])))
596		), !,
597		RootNodeId = TRootNodeId.
598		add_term_and_symbol_nodes_to_graph(Term, Type, _, RootNodeId) :-
599		is_uninterpreted_symbol(Term),
600		( have_seen_expr(Term, Type, TNodeId)
601		-> TRootNodeId = TNodeId
602		; get_color_for_type(Type, Term, Color),
603		term_to_label(Term, ATerm),
604		bliss_interface:add_node(ATerm, Color, RootNodeId),
605		log_seen_expr(Term, Type, RootNodeId),
606		asserta(ast_to_node_id(Term,Type,RootNodeId)),
607		asserta(node_id_to_ast(RootNodeId,b(Term,Type,[])))
608		), !,
609		RootNodeId = TRootNodeId.
610		add_term_and_symbol_nodes_to_graph(Term, Type, Functor, RootNodeId) :-
611		categorize_type(Type, Category, SymbolCategory),
612		add_node_to_colored_graph(SymbolCategory, Functor, Type, SymbolNodeId),
613		add_node_to_colored_graph(Category, Term, Type, RootNodeId),
614		% add an edge from the root node to the symbol node
615		bliss_interface:add_edge(RootNodeId, SymbolNodeId).
616
617		%% add_node_to_colored_graph(+Category, +Symbol, +Type, -NodeId).
618		% Symbol can be a compound term like conjunct(_,_) or uninterpreted symbol like conjunct.
619		% Argument nodes are assigned a specific, unique color.
620		% Uninterpreted symbol nodes and root nodes are assigned a color based on their type.
621		% Each interpreted symbol such as the integer 1 is assigned a unique color.
622		add_node_to_colored_graph(arg, _, _, ArgNodeId) :-
623		color(arg, Color),
624		bliss_interface:add_node('arg', Color, ArgNodeId), !.
625		%asserta(node_id_to_ast(ArgNodeId,b(Symbol,pred,[]))).
626		add_node_to_colored_graph(Category, Symbol, Type, NodeId) :-
627		( Category == pred, IsPred = true, IsExpr = false
628		; Category == expr, IsExpr = true, IsPred = false
629		),
630		( ( (IsPred, have_seen_pred(Symbol, TNodeId))
631		; (IsExpr, have_seen_expr(Symbol, Type, TNodeId))
632		)
633		-> NodeId = TNodeId
634		; get_color_for_type(Type, Symbol, Color),
635		term_to_label(Symbol, ASymbol),
636		bliss_interface:add_node(ASymbol, Color, NodeId),
637		( IsExpr
638		-> log_seen_expr(Symbol, Type, NodeId)
639		; log_seen_pred(Symbol, NodeId)
640		)
641		%asserta(node_id_to_ast(NodeId,b(Symbol,Type,[])))
642		), !.
643		add_node_to_colored_graph(upred, USymbol, pred, NodeId) :-
644		seen_upred(USymbol, TNodeId),
645		!,
646		NodeId = TNodeId.
647		add_node_to_colored_graph(upred, USymbol, pred, NodeId) :-
648		get_next_color(Color),
649		bliss_interface:add_node(USymbol, Color, NodeId),
650		asserta(seen_upred(USymbol,NodeId)), !.
651		add_node_to_colored_graph(uexpr, USymbol, _, NodeId) :-
652		seen_uexpr(USymbol, TNodeId),
653		!,
654		NodeId = TNodeId.
655		add_node_to_colored_graph(uexpr, USymbol, _, NodeId) :-
656		get_next_color(Color),
657		bliss_interface:add_node(USymbol, Color, NodeId),
658		asserta(seen_uexpr(USymbol,NodeId)), !.
659
660		expr_functor(b(Expr,_,_), Functor) :-
661		!,
662		functor(Expr, Functor, _).
663		expr_functor(Expr, Functor) :-
664		functor(Expr, Functor, _).
665
666		term_to_label(Term, Atom) :-
667		Term =.. [Functor|Args],
668		maplist(expr_functor, Args, ArgFunctors),
669		NTerm =.. [Functor|ArgFunctors],
670		write_to_codes(NTerm, Codes),
671		atom_codes(Atom, Codes).
672
673		%% get_color_for_type(+Type, +Symbol, -Color).
674		get_color_for_type(Type, _, Color) :-
675		color(Type, TColor),
676		!,
677		Color = TColor.
678		get_color_for_type(Type, _, Color) :-
679		get_next_color(Color),
680		asserta(color(Type,Color)).
681
682		%% get_next_color(-Color).
683		get_next_color(Color) :-
684		retract(next_color(Color)),
685		Color1 is Color + 1,
686		asserta(next_color(Color1)).
687
688		%% categorize_type(+Type, -Category, -SymbolCategory).
689		% Only used for a faster lookup of asserted facts.
690		categorize_type(Type, Category, SymbolCategory) :-
691		Type == pred,
692		!,
693		Category = pred,
694		SymbolCategory = upred.
695		categorize_type(_, expr, uexpr).
696
697		%% is_associative(+Term).
698		is_associative(conjunct).
699		is_associative(disjunct).
700		is_associative(add).
701		is_associative(multiplication).
702		is_associative(union).
703		is_associative(intersection).
704
705		%% is_commutative_but_not_associative(+Term).
706		is_commutative_but_not_associative(equivalence).
707		is_commutative_but_not_associative(equal).
708		is_commutative_but_not_associative(not_equal).
709
710		is_uninterpreted_symbol(identifier(_)).
711		%is_uninterpreted_symbol(record_field(_,_)).
712
713		is_interpreted_symbol(Symbol) :-
714		is_binary_interpreted_symbol(Symbol).
715		is_interpreted_symbol(boolean_true).
716		is_interpreted_symbol(boolean_false).
717		is_interpreted_symbol(max_int).
718		is_interpreted_symbol(min_int).
719		is_interpreted_symbol(empty_set).
720		is_interpreted_symbol(empty_sequence).
721		is_interpreted_symbol(bool_set).
722		is_interpreted_symbol(real_set).
723		is_interpreted_symbol(float_set).
724		is_interpreted_symbol(string_set).
725		is_interpreted_symbol(real(_)).
726		is_interpreted_symbol(integer(_)).
727		is_interpreted_symbol(string(_)).
728		is_interpreted_symbol(value(_)).
729		is_interpreted_symbol(integer_set(_)).
730		is_interpreted_symbol(event_b_identity).
731
732		is_binary_interpreted_symbol(interval(A,B)) :-
733		is_interpreted_symbol(A),
734		is_interpreted_symbol(B).
735
736		%% zip_to_equalities_conj(+Ids, +EqVals, -Eqs).
737		zip_to_equalities_conj([Id|T], [EqVal|VT], Eqs) :-
738		zip_to_equalities_conj(T, VT, b(equal(Id,EqVal),pred,[]), Eqs).
739
740		zip_to_equalities_conj([], [], Acc, Acc).
741		zip_to_equalities_conj([Id|T], [EqVal|VT], Acc, Eqs) :-
742		safe_create_texpr(conjunct(b(equal(Id,EqVal),pred,[]),Acc), pred, [], NAcc),
743		zip_to_equalities_conj(T, VT, NAcc, Eqs).
744
745		%% order_variables(+TypedVars, -TypeOrdering, -VariableOrdering).
746		% Assume that the variable set used in the SMT formula is an ordered set.
747		% Assume that there is some pre-defined ordering over types, and all the
748		% variables of a certain type ti appear before all the variables of another
749		% type tj in the variable ordering if type ti appears before type tj in the type ordering.
750		order_variables(TypedVars, TypeOrdering, VariableOrdering) :-
751		order_variables_by_type(TypedVars, [], VarsOrderedByType),
752		order_variables_within_typed_group(VarsOrderedByType, [], [], TypeOrdering, VariableOrdering).
753
754		%% order_variables_by_type(+TypedVars, +Acc, -VarsOrderedByType).
755		% Deterministic ordering of variables and corresponding types. The variables within the group of a type
756		% are sorted by their name using @<.
757		order_variables_by_type([], Acc, Acc).
758		order_variables_by_type([TypedVar|T], Acc, VarsOrderedByType) :-
759		TypedVar = b(_,Type,_),
760		extend_type_acc(Acc, Type, TypedVar, NAcc),
761		order_variables_by_type(T, NAcc, VarsOrderedByType).
762
763		%% order_variables_within_typed_group(+TypeVarsTuples, +VarAcc, +TypeAcc, -TypeOrdering, -VariableOrdering).
764		order_variables_within_typed_group([], VAcc, TAcc, TAcc, VAcc).
765		order_variables_within_typed_group([(Type,TypeVars)|T], VAcc, TAcc, TypeOrdering, VariableOrdering) :-
766		samsort(cmp_typed_identifier, TypeVars, STypeVars),
767		append(STypeVars, VAcc, NVAcc),
768		order_variables_within_typed_group(T, NVAcc, [Type|TAcc], TypeOrdering, VariableOrdering).
769
770		cmp_typed_identifier(b(identifier(Id1),_,_), b(identifier(Id2),_,_)) :-
771		Id1 @< Id2.
772
773		%% extend_type_acc(+Acc, +Type, +TypedVar, -NAcc).
774		% Acc is a list of tuples (Type,TypeVars).
775		extend_type_acc(Acc, Type, TypedVar, NAcc) :-
776		select((Type,TypedVars), Acc, RAcc),
777		!,
778		NAcc = [(Type,[TypedVar|TypedVars])|RAcc].
779		extend_type_acc(Acc, Type, TypedVar, NAcc) :-
780		NAcc = [(Type,[TypedVar])|Acc].
781
782		:- begin_tests(order_variables).
783
784		test(order_variables_empty, [true((VariableOrdering == ExpectedVars, TypeOrdering == ExpectedTypes))]) :-
785		Variables = [],
786		order_variables(Variables, TypeOrdering, VariableOrdering),
787		ExpectedVars = [],
788		ExpectedTypes = [].
789
790		test(order_variables_single_type, [true((VariableOrdering == ExpectedVars, TypeOrdering == ExpectedTypes))]) :-
791		Variables = [b(identifier(c),integer,[]),b(identifier(a),integer,[]),b(identifier(b),integer,[])],
792		order_variables(Variables, TypeOrdering, VariableOrdering),
793		ExpectedVars = [b(identifier(a),integer,[]),b(identifier(b),integer,[]),b(identifier(c),integer,[])],
794		ExpectedTypes = [integer].
795
796		test(order_variables_two_types, [true((VariableOrdering == ExpectedVars, TypeOrdering == ExpectedTypes))]) :-
797		Variables = [b(identifier(c),integer,[]),b(identifier(d),set(integer),[]),b(identifier(a),integer,[]),b(identifier(e),set(integer),[]),b(identifier(b),integer,[]),b(identifier(f),set(integer),[])],
798		order_variables(Variables, TypeOrdering, VariableOrdering),
799		ExpectedVars = [b(identifier(a),integer,[]),b(identifier(b),integer,[]),b(identifier(c),integer,[]),b(identifier(d),set(integer),[]),b(identifier(e),set(integer),[]),b(identifier(f),set(integer),[])],
800		ExpectedTypes = [integer,set(integer)].
801
802		test(order_variables_two_types_set_first, [true((VariableOrdering == ExpectedVars, TypeOrdering == ExpectedTypes))]) :-
803		Variables = [b(identifier(d),set(integer),[]),b(identifier(a),integer,[])],
804		order_variables(Variables, TypeOrdering, VariableOrdering),
805		ExpectedVars = [b(identifier(d),set(integer),[]),b(identifier(a),integer,[])],
806		ExpectedTypes = [set(integer),integer].
807
808		test(order_variables_two_types_integer_first, [true((VariableOrdering == ExpectedVars, TypeOrdering == ExpectedTypes))]) :-
809		Variables = [b(identifier(a),integer,[]),b(identifier(d),set(integer),[])],
810		order_variables(Variables, TypeOrdering, VariableOrdering),
811		ExpectedVars = [b(identifier(a),integer,[]),b(identifier(d),set(integer),[])],
812		ExpectedTypes = [integer,set(integer)].
813
814		test(order_variables_three_types, [true((VariableOrdering == ExpectedVars, TypeOrdering == ExpectedTypes))]) :-
815		Variables = [b(identifier(c),integer,[]),b(identifier(d),set(integer),[]),b(identifier(a),integer,[]),b(identifier(e),set(integer),[]),b(identifier(b),integer,[]),b(identifier(f),set(set(string)),[])],
816		order_variables(Variables, TypeOrdering, VariableOrdering),
817		ExpectedVars = [b(identifier(d),set(integer),[]),b(identifier(e),set(integer),[]),b(identifier(a),integer,[]),b(identifier(b),integer,[]),b(identifier(c),integer,[]),b(identifier(f),set(set(string)),[])],
818		ExpectedTypes = [set(integer),integer,set(set(string))].
819
820		:- end_tests(order_variables).
821
822
823		% The elements of enumerated sets already impose an order which has to be respected for symmetry breaking using the external prediate call LEQ_SYM.
824		%get_ordering_for_enumerated_set_elements(GlobalType, Ast1, Ast2, OrderedList) :-
825		% b_get_named_machine_set(GlobalType, EnumElements),
826		% Ast1 = b(identifier(Var1),global(GlobalType),_),
827		% Ast2 = b(identifier(Var2),global(GlobalType),_),
828		% nth0(Pos1, EnumElements, Var1),
829		% nth0(Pos2, EnumElements, Var2),
830		% % TODO: improve for "transitive" symmetries with non-static enumerated set elements
831		% ( Pos1 =< Pos2
832		% -> OrderedList = [Ast1,Ast2]
833		% ; OrderedList = [Ast2,Ast1]
834		% ).
835
836		%% get_equality_from_cycle(+Cycle, -Eq).
837		% Pairwise equality.
838		%get_equality_from_cycle([A,B|T], Eq) :-
839		% EqAcc = b(equal(A,B),pred,[]),
840		% get_equality_from_cycle([B|T], EqAcc, Eq).
841		%
842		%get_equality_from_cycle([_], EqAcc, EqAcc).
843		%get_equality_from_cycle([A,B|T], EqAcc, Eq) :-
844		% NEqAcc = b(conjunct(b(equal(A,B),pred,[]),EqAcc),pred,[]),
845		% get_equality_from_cycle([B|T], NEqAcc, Eq).