1		% (c) 2019-2022 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(dpllt_preprocessing, [preprocess_predicate/6,
5		optimize_clause_size_by_rewriting/5,
6		simplify_negation/2,
7		get_wd_theory_implications/3]).
8
9		:- use_module(library(sets)).
10		:- use_module(library(lists)).
11		:- use_module(library(plunit)).
12		:- use_module(library(terms), [term_size/2]).
13		:- use_module(dpllt_solver('difference_logic/ast_to_difference_logic')).
14		:- use_module(probsrc(bsyntaxtree), [find_identifier_uses/3,
15		remove_all_infos/2,
16		unique_typed_id/3,
17		syntaxtransformation/5,
18		disjunct_predicates/2,
19		conjunct_predicates/2,
20		safe_create_texpr/4,
21		create_negation/2,
22		create_implication/3,
23		get_texpr_expr/2,
24		get_texpr_type/2]).
25		:- use_module(probsrc(bsyntaxtree),[map_over_bexpr/2]).
26		:- use_module(probsrc('well_def/well_def_analyser'), [prove_sequent/1]).
27		:- use_module(probsrc(error_manager), [add_internal_error/2]).
28		:- use_module(probsrc(module_information), [module_info/2]).
29
30		:- module_info(group, dpllt).
31		:- module_info(description,'This module provides several preprocessing steps for the DPLL(T) based solver such as lifting negations from B operators.').
32
33		%%%
34		% Theory deduction for well-definedness to support the theory solver.
35		% For instance, deduce x:Dom for arr: Dom --> Ran & x:dom(arr).
36		% TO DO: improve code
37		get_wd_theory_implications(CandidateImpls, WDCandidateImpls, WDTheoryImpls) :-
38		CandidateImpls = candidate_impls(global(Global),integer(Integer),integer_ground(_),set(Set),set_ground(_)),
39		WDCandidateImpls = candidate_impls(global(WDGlobal),integer(WDInteger),integer_ground(_),set(WDSet),set_ground(_)),
40		append(WDInteger, WDSet, WDCandidates),
41		get_wd_theory_implications_for_candidates(Global, WDGlobal, GlobalImpls),
42		get_wd_theory_implications_for_candidates(Integer, WDCandidates, IntegerImpls),
43		get_wd_theory_implications_for_candidates(Set, WDCandidates, SetImpls),
44		conjunct_predicates([GlobalImpls,IntegerImpls,SetImpls], WDTheoryImpls).
45
46		b_function(total_function(Domain,_), Domain).
47		b_function(total_surjection(Domain,_), Domain).
48		b_function(total_injection(Domain,_), Domain).
49		b_function(total_bijection(Domain,_), Domain).
50		b_function(partial_function(Domain,_), Domain).
51		b_function(partial_surjection(Domain,_), Domain).
52		b_function(partial_injection(Domain,_), Domain).
53		b_function(partial_bijection(Domain,_), Domain).
54		b_function(surjection_relation(Domain,_), Domain).
55		b_function(total_relation(Domain,_), Domain).
56		b_function(relations(Domain,_), Domain).
57
58		b_function_membership(b(member(Id,Function),pred,_), Id, Domain) :-
59		get_texpr_expr(Function, Expr),
60		b_function(Expr, Domain).
61
62		get_wd_theory_implications_for_candidates(_, [], Out) :-
63		!,
64		Out = b(truth,pred,[]).
65		get_wd_theory_implications_for_candidates(Candidates, WDCandidates, ImplsConj) :-
66		collect_function_constraints(Candidates, FunctionConstraints),
67		get_wd_theory_implications_of_function_memberships(FunctionConstraints, WDCandidates, Impls),
68		conjunct_predicates(Impls, ImplsConj).
69
70		get_wd_theory_implications_of_function_memberships([], _, []).
71		get_wd_theory_implications_of_function_memberships([FunMem-Id-Domain|T], WDCandidates, Impls) :-
72		remove_all_infos(Id, CId),
73		memberchk(b(member(DomId,b(domain(CId),DType,DInfo)),pred,MInfo), WDCandidates),
74		!,
75		safe_create_texpr(member(DomId,b(domain(CId),DType,DInfo)), pred, MInfo, DomMember),
76		safe_create_texpr(disjunct(b(disjunct(b(negation(DomMember),pred,[]),b(negation(FunMem),pred,[])),pred,[]),b(member(DomId,Domain),pred,[])), pred, [], Impl),
77		Impls = [Impl|NT],
78		get_wd_theory_implications_of_function_memberships(T, WDCandidates, NT).
79		get_wd_theory_implications_of_function_memberships([_|T], WDCandidates, NT) :-
80		get_wd_theory_implications_of_function_memberships(T, WDCandidates, NT).
81
82		collect_function_constraints([], []).
83		collect_function_constraints([Candidate|T], FunctionConstraints) :-
84		b_function_membership(Candidate, Id, Domain),
85		!,
86		FunctionConstraints = [Candidate-Id-Domain|NT],
87		collect_function_constraints(T, NT).
88		collect_function_constraints([_|T], NT) :-
89		collect_function_constraints(T, NT).
90		%%%
91
92		negate_bool_expr(boolean_true, boolean_false).
93		negate_bool_expr(boolean_false, boolean_true).
94		negate_bool_expr(value(pred_true), boolean_false).
95		negate_bool_expr(value(pred_false), boolean_true).
96
97		is_boolean_true(b(boolean_true,boolean,_)).
98		is_boolean_true(b(value(pred_true),boolean,_)).
99
100		% convenience predicates:
101		disjunct_two_preds(A,B,Expr) :-
102		disjunct_predicates([A,B],b(Expr,_,_)).
103		conjunct_two_preds(A,B,Expr) :-
104		conjunct_predicates([A,B],b(Expr,_,_)).
105
106		simplify_negation(Ast, Simplified) :-
107		Ast = b(Expr,Type,Info),
108		simplify_negation_e(Expr, SimplifiedExpr),
109		safe_create_texpr(SimplifiedExpr, Type, Info, Simplified).
110
111		simplify_negation_e(negation(A), SimplifiedExpr) :-
112		A = b(truth,pred,_),
113		!,
114		SimplifiedExpr = falsity.
115		simplify_negation_e(negation(A), SimplifiedExpr) :-
116		A = b(falsity,pred,_),
117		!,
118		SimplifiedExpr = truth.
119		simplify_negation_e(negation(A), SimplifiedExpr) :-
120		A = b(Expr,pred,_),
121		negated_b_operator(Expr, NExpr),
122		!,
123		SimplifiedExpr=NExpr.
124		simplify_negation_e(negation(BoolEq), SimplifiedExpr) :-
125		% important for SAT constraints such as x=TRUE & not(x=TRUE)
126		( BoolEq = b(equal(Bool,Id),pred,_)
127		; BoolEq = b(equal(Id,Bool),pred,_)
128		),
129		Id = b(identifier(_),boolean,_),
130		Bool = b(Expr,boolean,Info),
131		negate_bool_expr(Expr, NExpr),
132		safe_create_texpr(NExpr, boolean, Info, NBool),
133		!,
134		SimplifiedExpr = equal(NBool,Id).
135		simplify_negation_e(negation(Neg), SimplifiedExpr) :-
136		Neg = b(negation(A),pred,_),
137		!,
138		A = b(SimplifiedExpr,_,_).
139		simplify_negation_e(negation(Conj), SimplifiedExpr) :-
140		Conj = b(conjunct(A,B),pred,_),
141		!,
142		simplify_negation(b(negation(A),pred,[]), SimplifiedA),
143		simplify_negation(b(negation(B),pred,[]), SimplifiedB),
144		disjunct_two_preds(SimplifiedA,SimplifiedB,SimplifiedExpr).
145		simplify_negation_e(negation(Disj), SimplifiedExpr) :-
146		Disj = b(disjunct(A,B),pred,_),
147		!,
148		simplify_negation(b(negation(A),pred,[]), SimplifiedA),
149		simplify_negation(b(negation(B),pred,[]), SimplifiedB),
150		conjunct_two_preds(SimplifiedA,SimplifiedB,SimplifiedExpr).
151		simplify_negation_e(negation(Impl), SimplifiedExpr) :-
152		Impl = b(implication(A,B),pred,_),
153		!,
154		simplify_negation_e(conjunct(A,b(negation(B),pred,[])), SimplifiedExpr).
155		simplify_negation_e(negation(Equi), SimplifiedExpr) :-
156		Equi = b(equivalence(A,B),pred,_),
157		!,
158		simplify_negation_e(disjunct(b(negation(b(implication(A,B),pred,[])),pred,[]),
159		b(negation(b(implication(B,A),pred,[])),pred,[])), SimplifiedExpr).
160		simplify_negation_e(Conn, SimplifiedExpr) :-
161		( Conn = conjunct(A,B)
162		; Conn = disjunct(A,B)
163		; Conn = implication(A,B)
164		; Conn = equivalence(A,B)
165		),
166		!,
167		simplify_negation(A, SimplifiedA),
168		simplify_negation(B, SimplifiedB),
169		( Conn = conjunct(A,B) ->
170		SimplifiedExpr = conjunct(SimplifiedA,SimplifiedB)
171		; Conn = disjunct(A,B) ->
172		SimplifiedExpr = disjunct(SimplifiedA,SimplifiedB)
173		; Conn = implication(A,B) ->
174		SimplifiedExpr = implication(SimplifiedA,SimplifiedB)
175		; Conn = equivalence(A,B) ->
176		SimplifiedExpr = equivalence(SimplifiedA,SimplifiedB)
177		).
178		simplify_negation_e(Expr, Expr).
179
180		is_literal(b(truth,pred,[])).
181		is_literal(b(falsity,pred,[])).
182		is_literal(b(equal(b(_,boolean,_),b(identifier(_),boolean,_)),pred,[])).
183		is_literal(b(equal(b(identifier(_),boolean,_),b(_,boolean,_)),pred,[])).
184
185		%% optimize_clause_size_by_rewriting(+BoolFormula, +SatVars, -OptBoolFormula, -NewSatVars, -NewVarConj).
186		% CNF construction can suffer from exponential blowup in size.
187		% We thus rewrite
188		% - nested equivalences TO DO
189		% - equivalences under disjunctions TO DO
190		% - conjunctions which are directly under a disjunction
191		% Rewriting means to introduce a new boolean variable to break nested distributivity.
192		% For instance, A <-> (B <-> (C <-> D)) is rewritten to A <-> (B <-> R) & R <-> (C <-> D).
193		% A or (B <-> C) is rewritten to A or R & (R <-> (B <-> C))
194		% (A & B & C) or (B & C & D) is rewritten to (A & B & C) or R & (R <-> (B & C & D))
195		% Note: Assumes that negation has been pushed to literals.
196		% TO DO: use only "obvious" rewritings and not all
197		optimize_clause_size_by_rewriting(BoolFormula, SatVars, OptBoolFormula, NewSatVars, NewVarConj) :-
198		BoolFormula = b(Expr,Type,Info),
199		optimize_clause_size_by_rewriting_expr(Expr, SatVars, OptExpr, NewSatVars, NewVarConj),
200		safe_create_texpr(OptExpr, Type, Info, OptBoolFormula).
201
202		%% get_larger_conj(+C1, +C2, -Larger, -Other).
203		% Return the conjunction with the larger term size
204		% but at least one conjunction has to be nested.
205		get_larger_conj(C1, C2, Larger, Other) :-
206		C1 = b(conjunct(C1A,C1B),pred,_),
207		C2 \= b(conjunct(_,_),pred,_),
208		( \+ is_literal(C1A); \+ is_literal(C1B)),
209		!,
210		Larger = C1,
211		Other = C2.
212		get_larger_conj(C1, C2, Larger, Other) :-
213		C2 = b(conjunct(C2A,C2B),pred,_),
214		C1 \= b(conjunct(_,_),pred,_),
215		( \+ is_literal(C2A); \+ is_literal(C2B)),
216		!,
217		Larger = C2,
218		Other = C1.
219		get_larger_conj(C1, C2, Larger, Other) :-
220		C1 = b(conjunct(C1A,C1B),pred,_),
221		C2 = b(conjunct(C2A,C2B),pred,_),
222		( \+ is_literal(C1A)
223		; \+ is_literal(C1B)
224		; \+ is_literal(C2A)
225		; \+ is_literal(C2B)
226		),
227		term_size(C1, S1),
228		term_size(C2, S2),
229		( S1 > S2
230		-> Larger = C1,
231		Other = C2
232		; Larger = C2,
233		Other = C1
234		).
235
236		optimize_clause_size_by_rewriting_expr(disjunct(D1,D2), SatVars, OptExpr, NewSatVars, NewVarConj) :-
237		D1 = b(conjunct(_,_),pred,_),
238		D2 \= b(conjunct(_,_),pred,_),
239		!,
240		optimize_clause_size_by_rewriting_expr(disjunct(D2,D1), SatVars, OptExpr, NewSatVars, NewVarConj).
241		optimize_clause_size_by_rewriting_expr(disjunct(D1,D2), SatVars, OptExpr, NewSatVars, NewVarConj) :-
242		get_larger_conj(D1, D2, ToReplace, ToKeep),
243		!,
244		unique_typed_id("_cnf_opt", boolean, NewSatVar),
245		optimize_clause_size_by_rewriting(ToReplace, SatVars, NToReplace, SatVars1, NewVarConj1),
246		safe_create_texpr(equal(NewSatVar,b(boolean_true,boolean,[])), pred, [], NewVarTrue),
247		safe_create_texpr(equal(NewSatVar,b(boolean_false,boolean,[])), pred, [], NewVarFalse),
248		safe_create_texpr(disjunct(NewVarFalse,NToReplace), pred, [], NewVarImpl1),
249		safe_create_texpr(negation(NToReplace), pred, [], ToReplaceNeg),
250		negate_bool_formula(ToReplaceNeg, ToReplaceNegClean),
251		optimize_clause_size_by_rewriting(ToReplaceNegClean, SatVars1, NToReplaceNegClean, SatVars2, NewVarConj2),
252		NewVarImpl2 = b(disjunct(NewVarTrue,NToReplaceNegClean),pred,[]),
253		optimize_clause_size_by_rewriting(ToKeep, SatVars2, NToKeep, SatVars3, NewVarConj3),
254		OptExpr = disjunct(NToKeep,NewVarTrue),
255		NewSatVars = [NewSatVar|SatVars3],
256		append([NewVarConj1, NewVarConj2, NewVarConj3], TNewVarConj),
257		safe_create_texpr(conjunct(NewVarImpl1,NewVarImpl2), pred, [], Conj),
258		NewVarConj = [Conj|TNewVarConj].
259		optimize_clause_size_by_rewriting_expr(Binary, SatVars, NBinary, NewSatVars, NewVarConj) :-
260		functor(Binary, Functor, 2),
261		(Functor = conjunct; Functor = disjunct; Functor = implication; Functor = equivalence),
262		!,
263		arg(1, Binary, Arg1),
264		arg(2, Binary, Arg2),
265		optimize_clause_size_by_rewriting(Arg1, SatVars, NArg1, SatVars1, NewVarConj1),
266		optimize_clause_size_by_rewriting(Arg2, SatVars1, NArg2, NewSatVars, NewVarConj2),
267		functor(NBinary, Functor, 2),
268		arg(1, NBinary, NArg1),
269		arg(2, NBinary, NArg2),
270		append(NewVarConj1, NewVarConj2, NewVarConj).
271		optimize_clause_size_by_rewriting_expr(Expr, SatVars, Expr, SatVars, []).
272
273		%% preprocess_predicate(+PerformStaticAnalysis, +RewriteToIdl, +Pred, -LiftedPred, -FilteredCandidateImplsConj, -CandidateImpls).
274		preprocess_predicate(PerformStaticAnalysis, RewriteToIdl, Pred, LiftedPred, FilteredCandidateImplsConj, CandidateImpls) :-
275		empty_candidate_impls_acc(CandidateAcc),
276		lift_negations_find_impls(Pred, RewriteToIdl, CandidateAcc, TLiftedPred, CandidateImpls), !,
277		LiftedPred = TLiftedPred,
278		( PerformStaticAnalysis=true
279		-> process_candidate_impls(CandidateImpls, FilteredCandidateImplsConj)
280		; FilteredCandidateImplsConj = b(truth,pred,[])
281		).
282
283		%% process_candidate_impls(+CandidateImpls, -FilteredCandidateImplsConj).
284		% Given a candidate like x>y, get partner candidates like y<x, y=<x and x=y.
285		% Filter those partner candidates that exist in the given formula (prevent introducing redundant SAT variables)
286		% and create the implication, e.g., x>y => (not(y<x) & not(y=<x) & not(x=y)).
287		process_candidate_impls(CandidateImpls, FilteredCandidateImplsConj) :-
288		CandidateImpls = candidate_impls(global(Global),integer(Integer),integer_ground(IntegerGrnd),set(Set),set_ground(SetGrnd)),
289		process_candidate_impls_list(true, Global, GlobalImplsConj),
290		process_candidate_impls_list(false, Integer, IntImplsConj),
291		process_candidate_impls_list(false, IntegerGrnd, IntGrndImplsConj),
292		process_candidate_impls_list(false, Set, SetImplsConj),
293		process_candidate_impls_list(false, SetGrnd, SetGrndImplsConj),
294		conjunct_predicates([GlobalImplsConj,IntImplsConj,IntGrndImplsConj,SetImplsConj,SetGrndImplsConj], FilteredCandidateImplsConj).
295
296		process_candidate_impls_list(IsGlobalType, GrndCandidateImpls, ImplsConj) :-
297		process_candidate_impls_list(IsGlobalType, GrndCandidateImpls, [], Impls),
298		conjunct_predicates(Impls, ImplsConj).
299
300		process_candidate_impls_list(_, [], Acc, ImplsConj) :- !, ImplsConj=Acc.
301		process_candidate_impls_list(IsGlobalType, [GrndCandidateImpl|T], Acc, ImplsConj) :-
302		( is_true(IsGlobalType)
303		-> get_global_type_partner_candidates(GrndCandidateImpl, T, Partners, _RestT)
304		; get_partner_candidates(GrndCandidateImpl, T, Partners, _RestT)
305		),
306		Partners \== [],
307		!,
308		build_implications_from_ground_candidates(GrndCandidateImpl, Partners, PartialImplsConj),
309		process_candidate_impls_list(IsGlobalType, T, [PartialImplsConj|Acc], ImplsConj).
310		process_candidate_impls_list(IsGlobalType, [_|T], Acc, ImplsConj) :-
311		process_candidate_impls_list(IsGlobalType, T, Acc, ImplsConj).
312
313		%% build_implications_from_ground_candidates(+GrndCandidateImpl, +Partners, -PartialImplsConj).
314		% Given GrndCandidateImpl and some matching partner candidates, collect proven implications:
315		% p in Partners, add one of 'GrndCandidateImpl => p', 'p => GrndCandidateImpl' or nothing
316		build_implications_from_ground_candidates(GrndCandidateImpl, Partners, PartialImplsConj) :-
317		build_implications_from_ground_candidates(GrndCandidateImpl, Partners, [], PartialImplsConj).
318		% TO DO: improve, sometimes too much overhead
319		%build_conj_implications_from_ground_candidates(GrndCandidateImpl, Partners, Partners, [], PartialImplsConj2),
320		%conjunct_predicates([PartialImplsConj1,PartialImplsConj2], PartialImplsConj).
321
322		%build_conj_implications_from_ground_candidates(_, [], _, Acc, PartialImplsConj) :-
323		% conjunct_predicates(Acc, PartialImplsConj).
324		%build_conj_implications_from_ground_candidates(GrndCandidateImpl, [Partner|T], Partners, Acc, PartialImplsConj) :-
325		% select(Partner, Partners, Rest),
326		% NegConj = b(disjunct(b(negation(GrndCandidateImpl),pred,[]),b(negation(Partner),pred,[])),pred,[]),
327		% remove_zero_var(NegConj, NegConjNoZero),
328		% build_conj_implications_from_ground_conj(NegConj, NegConjNoZero, Rest, Acc, NewAcc),
329		% build_conj_implications_from_ground_candidates(GrndCandidateImpl, T, Partners, NewAcc, PartialImplsConj).
330		%
331		%build_conj_implications_from_ground_conj(_, _, [], Acc, Acc).
332		%build_conj_implications_from_ground_conj(NegConj, NegConjNoZero, [Partner|T], Acc, Impls) :-
333		% remove_zero_var(Partner, PartnerNoZero),
334		% Impl1 = b(disjunct(NegConj,Partner),pred,[]),
335		% Impl1NoZero = b(disjunct(NegConjNoZero,PartnerNoZero),pred,[]),
336		% Impl2 = b(disjunct(NegConj,b(negation(Partner),pred,[])),pred,[]),
337		% Impl2NoZero = b(disjunct(NegConjNoZero,b(negation(PartnerNoZero),pred,[])),pred,[]),
338		% ( %nl,write('Try Impl1: '), nl, translate:print_bexpr(Impl1NoZero), nl,
339		% prove_sequent(Impl1NoZero)%, write('True'),nl
340		% -> NewAcc = [Impl1|Acc]
341		% ; %nl,write('Try Impl2: '), nl, translate:print_bexpr(Impl2NoZero), nl,
342		% ( prove_sequent(Impl2NoZero),%, write('True'),nl,
343		% NewAcc = [Impl2|Acc]
344		% ; NewAcc = Acc
345		% )
346		% ),
347		% build_conj_implications_from_ground_conj(NegConj, NegConjNoZero, T, NewAcc, Impls).
348
349		/*
350		prove_with_prob(Constraint) :-
351		find_typed_identifier_uses(Constraint, [], TypedIds),
352		translate:generate_typing_predicates(TypedIds, TypingPreds),
353		conjunct_predicates(TypingPreds, TypingPred),
354		Forall = b(forall(TypedIds,TypingPred,Constraint),pred,[]),
355		solver_interface:solve_predicate(Forall, _, Res),
356		Res == solution([]).
357		*/
358
359		build_implications_from_ground_candidates(_, [], Acc, PartialImplsConj) :-
360		conjunct_predicates(Acc, PartialImplsConj).
361		build_implications_from_ground_candidates(GrndCandidateImpl, [Partner|T], Acc, PartialImplsConj) :-
362		safe_create_texpr(negation(GrndCandidateImpl), pred, [], NegGrndCandidateImpl),
363		NegPartner = b(negation(Partner),pred,[]),
364		% possibly remove zero var from idl solver
365		safe_create_texpr(disjunct(NegGrndCandidateImpl,Partner), pred, [], Impl1),
366		remove_zero_var(Impl1, Impl1NoZero),
367		safe_create_texpr(disjunct(NegPartner,GrndCandidateImpl), pred, [], Impl2),
368		remove_zero_var(Impl2, Impl2NoZero),
369		safe_create_texpr(disjunct(NegGrndCandidateImpl,b(negation(Partner),pred,[])), pred, [], Impl3),
370		remove_zero_var(Impl3, Impl3NoZero),
371		safe_create_texpr(disjunct(NegPartner,b(negation(GrndCandidateImpl),pred,[])), pred, [], Impl4),
372		remove_zero_var(Impl4, Impl4NoZero),
373		( %nl,write('Try Impl1: '), nl, translate:print_bexpr(Impl1NoZero), nl,
374		prove_sequent(Impl1NoZero)% write('True'),nl
375		-> NewAcc = [Impl1|Acc]
376		; %nl,write('Try Impl2: '), nl, translate:print_bexpr(Impl2NoZero), nl,
377		prove_sequent(Impl2NoZero)% write('True'),nl
378		-> NewAcc = [Impl2|Acc]
379		; %nl,write('Try Impl3: '), nl, translate:print_bexpr(Impl3NoZero), nl,
380		prove_sequent(Impl3NoZero)% write('True'),nl
381		-> NewAcc = [Impl3|Acc]
382		; %nl,write('Try Impl4: '), nl, translate:print_bexpr(Impl4NoZero), nl,
383		prove_sequent(Impl4NoZero)% write('True'),nl
384		-> NewAcc = [Impl4|Acc]
385		; NewAcc = Acc
386		),
387		build_implications_from_ground_candidates(GrndCandidateImpl, T, NewAcc, PartialImplsConj).
388
389		%create_var_bindings([], []).
390		%create_var_bindings([Id|T], [bind(Id,_)|NT]) :-
391		% create_var_bindings(T, NT).
392		%
393		%get_var_bindings_for_ast(Ast, Bindings) :-
394		% find_identifier_uses(Ast, [], Ids),
395		% create_var_bindings(Ids, Bindings).
396
397		uses_exactly_same_ids(A, UsedIds) :-
398		find_identifier_uses(A, [], UsedA),
399		sets:subset(UsedA, UsedIds),
400		sets:subset(UsedIds, UsedA), !.
401
402		uses_same_id(A, UsedIds) :-
403		find_identifier_uses(A, [], UsedA),
404		sets:intersection(UsedA, UsedIds, Inter),
405		Inter \== [].
406
407		%% get_partner_candidates(+Id, +Rest, -Partners, -RestRest).
408		% ASTs in Rest have the same type.
409		% idea: given, e.g., 1<x: search for all comparisons between x and a ground value like 0<x, x<10 etc.
410		% afterwards, evaluate the constraints and try to build implications like 1<x => 0<x
411		get_partner_candidates(GrndCandidateImpl, Rest, Partners, RestRest) :-
412		find_identifier_uses(GrndCandidateImpl, [], UsedIds),
413		get_partner_candidates(UsedIds, Rest, [], Partners, [], RestRest),!.
414
415		get_partner_candidates(_, [], PartnersAcc, PartnersAcc, RestAcc, RestAcc).
416		get_partner_candidates(UsedIds, Rest, PartnersAcc, Partners, RestAcc, RestRest) :-
417		select(Partner, Rest, TRest),
418		( uses_exactly_same_ids(Partner, UsedIds)
419		-> NPartnersAcc = [Partner|PartnersAcc],
420		NRestAcc = RestAcc
421		; NPartnersAcc = PartnersAcc,
422		NRestAcc = [Partner|RestAcc]
423		),
424		!,
425		get_partner_candidates(UsedIds, TRest, NPartnersAcc, Partners, NRestAcc, RestRest).
426
427		get_global_type_partner_candidates(GrndCandidateImpl, Rest, Partners, RestRest) :-
428		find_identifier_uses(GrndCandidateImpl, [], UsedIds),
429		get_global_type_partner_candidates(UsedIds, Rest, [], Partners, [], RestRest),!.
430
431		get_global_type_partner_candidates(_, [], PartnersAcc, PartnersAcc, RestAcc, RestAcc).
432		get_global_type_partner_candidates(UsedIds, Rest, PartnersAcc, Partners, RestAcc, RestRest) :-
433		select(Partner, Rest, TRest),
434		( uses_same_id(Partner, UsedIds)
435		-> NPartnersAcc = [Partner|PartnersAcc],
436		NRestAcc = RestAcc
437		; NPartnersAcc = PartnersAcc,
438		NRestAcc = [Partner|RestAcc]
439		),
440		!,
441		get_global_type_partner_candidates(UsedIds, TRest, NPartnersAcc, Partners, NRestAcc, RestRest).
442
443		candidate_impl_binary_operator(equal, global).
444		candidate_impl_binary_operator(member, global).
445		candidate_impl_binary_operator(equal, integer).
446		candidate_impl_binary_operator(member, integer).
447		candidate_impl_binary_operator(equal, set).
448		candidate_impl_binary_operator(less, integer).
449		candidate_impl_binary_operator(less_equal, integer).
450		candidate_impl_binary_operator(greater, integer).
451		candidate_impl_binary_operator(greater_equal, integer).
452		candidate_impl_binary_operator(member, set).
453		candidate_impl_binary_operator(subset, set).
454		candidate_impl_binary_operator(subset_strict, set).
455
456		ground_b_ast(Ast) :-
457		( var(Ast)
458		-> fail
459		; ground_b_ast_nonvar(Ast)
460		).
461
462		ground_b_ast_nonvar(b(truth,_,_)).
463		ground_b_ast_nonvar(b(falsity,_,_)).
464		ground_b_ast_nonvar(b(integer(Int),_,_)) :-
465		ground(Int).
466		ground_b_ast_nonvar(b(value(int(Int)),_,_)) :-
467		ground(Int).
468		ground_b_ast_nonvar(b(interval(Min,Max),_,_)) :-
469		Min = b(integer(I1),integer,_),
470		Max = b(integer(I2),integer,_),
471		integer(I1),
472		integer(I2).
473		ground_b_ast_nonvar(b(set_extension(AstList),_,_)) :-
474		maplist(ground_b_ast, AstList).
475		ground_b_ast_nonvar(b(value(Set),_,_)) :-
476		ground(Set).
477
478		%% extend_candidate_impls_acc(+Type, +Functor, +Arg1, +Arg2, +Ast, +CandidateAcc, -NewCandidateAcc) :-
479		% Collect ASTs with functor in candidate_impl_binary_operator/2 and both arguments being
480		% an identifier or ground value.
481		extend_candidate_impls_acc(Type, Functor, Arg1, Arg2, Ast, CandidateAcc, NewCandidateAcc) :-
482		Type == pred,
483		Arg1 = b(_,AType,_),
484		functor(AType, FType, _),
485		candidate_impl_binary_operator(Functor, FType),
486		( (ground_b_ast(Arg1),
487		is_id_or_pred_containing_id(Arg2))
488		;
489		(ground_b_ast(Arg2),
490		is_id_or_pred_containing_id(Arg1))
491		),
492		remove_all_infos(Ast, AstClean),
493		ast_not_in_candidate_acc(ground, FType, AstClean, CandidateAcc),
494		!,
495		extend_candidate_impls_acc_safe_ground(FType, CandidateAcc, Ast, NewCandidateAcc).
496		extend_candidate_impls_acc(Type, Functor, Arg1, Arg2, Ast, CandidateAcc, NewCandidateAcc) :-
497		Type == pred,
498		Arg1 = b(_,AType,_),
499		functor(AType, FType, _),
500		candidate_impl_binary_operator(Functor, FType),
501		is_id_or_pred_containing_id(Arg1),
502		is_id_or_pred_containing_id(Arg2),
503		remove_all_infos(Ast, AstClean),
504		ast_not_in_candidate_acc(var, FType, AstClean, CandidateAcc),
505		!,
506		extend_candidate_impls_acc_safe(FType, CandidateAcc, Ast, NewCandidateAcc).
507		extend_candidate_impls_acc(_, _, _, _, _, CandidateAcc, CandidateAcc).
508
509		is_identifier(identifier(_)).
510
511		is_id_or_pred_containing_id(TExpr) :-
512		get_texpr_expr(TExpr, Expr),
513		functor(Expr, Functor, _),
514		% no ASTs with local identifiers
515		\+ member(Functor, [forall,exists,comprehension_set,lambda,general_sum,general_product,event_b_comprehension_set,quantified_union,quantified_intersection]),
516		map_over_bexpr(is_identifier, TExpr).
517
518		%% ast_not_in_candidate_acc(+VarOrGround, +Type, +AstClean, +CandidateAcc).
519		ast_not_in_candidate_acc(var, global, AstClean, candidate_impls(global(Global),integer(_),integer_ground(_),set(_),set_ground(_))) :-
520		\+ member(AstClean, Global).
521		ast_not_in_candidate_acc(var, integer, AstClean, candidate_impls(global(_),integer(Integer),integer_ground(_),set(_),set_ground(_))) :-
522		\+ member(AstClean, Integer).
523		ast_not_in_candidate_acc(ground, integer, AstClean, candidate_impls(global(_),integer(_),integer_ground(IntegerGrnd),set(_),set_ground(_))) :-
524		\+ member(AstClean, IntegerGrnd).
525		ast_not_in_candidate_acc(var, set, AstClean, candidate_impls(global(_),integer(_),integer_ground(_),set(Set),set_ground(_))) :-
526		\+ member(AstClean, Set).
527		ast_not_in_candidate_acc(ground, set, AstClean, candidate_impls(global(_),integer(_),integer_ground(_),set(_),set_ground(SetGrnd))) :-
528		\+ member(AstClean, SetGrnd).
529
530		% TO DO: use get_sorted_equality/3 for equalities
531		extend_candidate_impls_acc_safe_ground(integer, candidate_impls(global(Global),integer(Integer),integer_ground(IntegerGrnd),set(Set),set_ground(SetGrnd)), Ast, candidate_impls(global(Global),integer(Integer),integer_ground([Ast|IntegerGrnd]),set(Set),set_ground(SetGrnd))).
532		extend_candidate_impls_acc_safe_ground(set, candidate_impls(global(Global),integer(Integer),integer_ground(IntegerGrnd),set(Set),set_ground(SetGrnd)), Ast, candidate_impls(global(Global),integer(Integer),integer_ground(IntegerGrnd),set(Set),set_ground([Ast|SetGrnd]))).
533
534		extend_candidate_impls_acc_safe(global, candidate_impls(global(Global),integer(Integer),integer_ground(IntegerGrnd),set(Set),set_ground(SetGrnd)), Ast, candidate_impls(global([Ast|Global]),integer(Integer),integer_ground(IntegerGrnd),set(Set),set_ground(SetGrnd))).
535		extend_candidate_impls_acc_safe(integer, candidate_impls(global(Global),integer(Integer),integer_ground(IntegerGrnd),set(Set),set_ground(SetGrnd)), Ast, candidate_impls(global(Global),integer([Ast|Integer]),integer_ground(IntegerGrnd),set(Set),set_ground(SetGrnd))).
536		extend_candidate_impls_acc_safe(set, candidate_impls(global(Global),integer(Integer),integer_ground(IntegerGrnd),set(Set),set_ground(SetGrnd)), Ast, candidate_impls(global(Global),integer(Integer),integer_ground(IntegerGrnd),set([Ast|Set]),set_ground(SetGrnd))).
537
538		empty_candidate_impls_acc(candidate_impls(global([]),integer([]),integer_ground([]),set([]),set_ground([]))).
539
540		%% lift_negations_find_impls(+Pred, +RewriteToIdl, +CandidateAcc, -LPred, -CandidateImpls).
541		lift_negations_find_impls(Pred, RewriteToIdl, CandidateAcc, LPred, CandidateImpls) :-
542		Pred = b(Expr,Type,Info),
543		!,
544		lift_negations_find_impls_e(Expr, Type, Info, RewriteToIdl, CandidateAcc, LExpr, CandidateImpls),
545		safe_create_texpr(LExpr,Type,Info,LPred).
546		lift_negations_find_impls(Pred, _, CandidateAcc, Pred, CandidateAcc).
547
548		%% lift_negations_find_impls_e(+Expr, +Type, +RewriteToIdl, +CandidateAcc, -LExpr, -CandidateImpls).
549		% Unfold negated operators like not_equal to detect equal ASTs when introducing
550		% boolean variables for the SAT formula. For instance, it improves performance
551		% to transform 'x={} & x/={}' to 'x={} & not(x={})' first, since we can then translate to
552		% 'A & not(A)' in SAT rather than 'A & B'.
553		% Collect specific operators that might imply each other like 'x>0' and 'x>1' result to 'x>1 => x>0' (see candidate_impl_binary_operator/2).
554		% Note: only binary operators are checked recursively since we transform SMT to SAT on the level of conjunct, disjunct and implication
555		% Note: CandidateImpls contains true asts of lifted predicates, e.g., 'x:{1,2}' is stored for 'x/:{1,2}'
556		lift_negations_find_impls_e(Expr, _, _, _, _, _, _) :- var(Expr),!,
557		add_internal_error('Illegal var B AST: ',lift_negations_find_impls_e(Expr, _, _, _, _, _, _)),fail.
558		lift_negations_find_impls_e(Expr, _, _, _, CandidateAcc, LPred, CandidateImpls) :-
559		% important to use the same SAT variables, e.g., for x=TRUE & x=FALSE
560		(Expr = equal(Bool,BoolId) ; Expr = equal(BoolId,Bool)),
561		BoolId = b(identifier(_),boolean,_),
562		is_boolean_true(Bool),
563		!,
564		LPred = negation(b(equal(b(boolean_false,boolean,[]),BoolId),pred,[])),
565		CandidateImpls = CandidateAcc.
566		lift_negations_find_impls_e(Expr, _, Info, RewriteToIdl, CandidateAcc, LPred, CandidateImpls) :-
567		Expr = equivalence(Lhs,Rhs),
568		!,
569		create_implication(Lhs,Rhs,Impl1),
570		create_implication(Rhs,Lhs,Impl2),
571		Rewritten = conjunct(Impl1,Impl2),
572		/*Disj1 = b(conjunct(Lhs,Rhs),pred,[]),
573		Disj2 = b(conjunct(b(negation(Lhs),pred,[]),b(negation(Rhs),pred,[])),pred,[]),
574		Rewritten = b(disjunct(Disj1,Disj2),pred,[]),*/
575		lift_negations_find_impls_e(Rewritten, pred, Info, RewriteToIdl, CandidateAcc, LPred, CandidateImpls).
576		lift_negations_find_impls_e(Expr, _, Info, RewriteToIdl, CandidateAcc, LExpr, CandidateImpls) :-
577		Expr = implication(Lhs,Rhs),
578		!,
579		create_negation(Lhs,NLhs),
580		Rewritten = disjunct(NLhs,Rhs),
581		lift_negations_find_impls_e(Rewritten, pred, Info, RewriteToIdl, CandidateAcc, LExpr, CandidateImpls).
582		lift_negations_find_impls_e(Expr, _, Info, RewriteToIdl, CandidateAcc, LExpr, CandidateImpls) :-
583		Expr = negation(b(negation(Pos),pred,_)),
584		get_texpr_expr(Pos, PosExpr),
585		get_texpr_type(Pos, PosType),
586		!,
587		lift_negations_find_impls_e(PosExpr, PosType, Info, RewriteToIdl, CandidateAcc, LExpr, CandidateImpls).
588		lift_negations_find_impls_e(Expr, _, _, _, CandidateAcc, LExpr, CandidateImpls) :-
589		Expr = negation(b(truth,pred,_)),
590		!,
591		LExpr = falsity,
592		CandidateImpls = CandidateAcc.
593		lift_negations_find_impls_e(Expr, _, _, _, CandidateAcc, LExpr, CandidateImpls) :-
594		Expr = negation(b(falsity,pred,_)),
595		!,
596		LExpr = truth,
597		CandidateImpls = CandidateAcc.
598		lift_negations_find_impls_e(Inequality, _, _, RewriteToIdl, CandidateAcc, LExpr, CandidateImpls) :-
599		is_true(RewriteToIdl),
600		( Inequality = not_equal(b(_,integer,[]),_)
601		%IEQ = Inequality
602		; Inequality = negation(b(equal(b(_,integer,[]),_),pred,_))
603		%IEQ = b(not_equal(Arg1,Arg2),pred,EQInfo)
604		),
605		rewrite_inequality_to_idl_disj_no_zero(b(Inequality,pred,[]), DLConstraint),
606		!,
607		DLConstraint = b(disjunct(Lhs,Rhs),pred,_),
608		create_negation(LhsPos,Lhs),
609		create_negation(RhsPos,Rhs),
610		safe_create_texpr(less_equal(LArg1,LArg2),pred,[],LhsPos),
611		safe_create_texpr(less_equal(RArg1,RArg2),pred,[],RhsPos),
612		disjunct_two_preds(Lhs,Rhs,LExpr),
613		%extend_candidate_impls_acc(pred, not_equal, Arg1, Arg2, IEQ, CandidateAcc, CandidateAcc1),
614		extend_candidate_impls_acc(pred, less_equal, LArg1, LArg2, LhsPos, CandidateAcc, CandidateAcc1),
615		extend_candidate_impls_acc(pred, less_equal, RArg1, RArg2, RhsPos, CandidateAcc1, CandidateImpls).
616		lift_negations_find_impls_e(Equality, _, _, RewriteToIdl, CandidateAcc, LPred, CandidateImpls) :-
617		is_true(RewriteToIdl),
618		( Equality = equal(b(_,integer,_),_)
619		%EQ = Equality
620		; Equality = negation(b(not_equal(b(_,integer,_),_),pred,_))
621		%EQ = b(equal(Arg1,Arg2),pred,EQInfo)
622		),
623		rewrite_to_idl_no_zero(b(Equality,pred,[]), ConjList),
624		!,
625		ConjList = [TLhs,TRhs],
626		% don't create _zero var from idl solver in SAT formula
627		remove_idl_origin_from_info(TLhs, Lhs),
628		remove_idl_origin_from_info(TRhs, Rhs),
629		safe_create_texpr(less_equal(LArg1,LArg2),pred,[],Lhs),
630		safe_create_texpr(less_equal(RArg1,RArg2),pred,[],Rhs),
631		conjunct_two_preds(Lhs,Rhs,LPred),
632		extend_candidate_impls_acc(pred, less_equal, LArg1, LArg2, Lhs, CandidateAcc, CandidateAcc1),
633		extend_candidate_impls_acc(pred, less_equal, RArg1, RArg2, Rhs, CandidateAcc1, CandidateImpls).
634		lift_negations_find_impls_e(Expr, Type, _, _, CandidateAcc, LExpr, CandidateImpls) :-
635		negated_b_operator(Expr, TrueNode),
636		!,
637		safe_create_texpr(TrueNode,Type,[],TrueAst),
638		TrueNode =.. [NFunctor, Arg1, Arg2],
639		extend_candidate_impls_acc(Type, NFunctor, Arg1, Arg2, TrueAst, CandidateAcc, CandidateImpls),
640		LExpr = negation(TrueAst).
641		% simplify negated conjunction or disjunction possibly introduced by rewriting equivalence and implication
642		lift_negations_find_impls_e(Expr, _, Info, RewriteToIdl, CandidateAcc, LExpr, CandidateImpls) :-
643		Expr = negation(Arg),
644		Arg = b(conjunct(Conj1,Conj2),pred,_),
645		!,
646		create_negation(Conj1,NConj1),
647		create_negation(Conj2,NConj2),
648		disjunct_two_preds(NConj1,NConj2,Rewritten),
649		lift_negations_find_impls_e(Rewritten, pred, Info, RewriteToIdl, CandidateAcc, LExpr, CandidateImpls).
650		lift_negations_find_impls_e(Expr, _, Info, RewriteToIdl, CandidateAcc, LExpr, CandidateImpls) :-
651		Expr = negation(Arg),
652		Arg = b(disjunct(Conj1,Conj2),pred,_),
653		!,
654		create_negation(Conj1,NConj1),
655		create_negation(Conj2,NConj2),
656		Rewritten = conjunct(NConj1,NConj2),
657		lift_negations_find_impls_e(Rewritten, pred, Info, RewriteToIdl, CandidateAcc, LExpr, CandidateImpls).
658		lift_negations_find_impls_e(Expr, pred, _Info, RewriteToIdl, CandidateAcc, LExpr, CandidateImpls) :-
659		Expr = negation(Arg),
660		Arg = b(ArgExpr,ArgType,ArgInfo),
661		lift_negations_find_impls_e(ArgExpr, ArgType, ArgInfo, RewriteToIdl, CandidateAcc, LArgExpr, CandidateImpls),
662		safe_create_texpr(LArgExpr,pred,ArgInfo,TLA),
663		create_negation(TLA,b(LExpr,_,_)).
664		lift_negations_find_impls_e(Expr, pred, Info, RewriteToIdl, CandidateAcc, LExpr, CandidateImpls) :-
665		functor(Expr, Functor, 2),
666		Names = [], % quantifications (comprehension_set, exists) will be abstracted by a single SAT variable
667		syntaxtransformation(Expr,[Arg1,Arg2],Names,[LLhs,LRhs],LExpr), % TODO REVIEW: syntaxtransformation could have two subarguments even if arity is not 2
668		!,
669		extend_candidate_impls_acc(pred, Functor, Arg1, Arg2, b(Expr,pred,Info), CandidateAcc, CandidateAcc1),
670		lift_negations_find_impls(Arg1, RewriteToIdl, CandidateAcc1, LLhs, CandidateAcc2),
671		lift_negations_find_impls(Arg2, RewriteToIdl, CandidateAcc2, LRhs, CandidateImpls).
672		lift_negations_find_impls_e(Expr, _, _, _, CandidateAcc, Expr, CandidateAcc).
673
674		is_true(X) :- (X==true -> true
675		; X== false -> fail
676		; add_internal_error('Illegal call:',is_true(X)), fail
677		).
678
679		%get_sorted_equality(Lhs, Rhs, Equality) :-
680		% Lhs @> Rhs,
681		% !,
682		% safe_create_texpr(equal(Rhs,Lhs), pred, [], Equality).
683		%get_sorted_equality(Lhs, Rhs, b(equal(Lhs,Rhs),pred,[])).
684
685		%binary_connective(conjunct).
686		%binary_connective(disjunct).
687		%binary_connective(implication).
688		%binary_connective(equivalence).
689
690		negated_b_operator(not_equal(A,B), equal(A,B)).
691		negated_b_operator(not_member(A,B), member(A,B)).
692		negated_b_operator(not_subset(A,B), subset(A,B)).
693		negated_b_operator(not_subset_strict(A,B), subset_strict(A,B)).
694
695		negate_bool_formula(b(negation(b(truth,pred,Info)),pred,_), b(falsity,pred,Info)).
696		negate_bool_formula(b(negation(b(falsity,pred,Info)),pred,_), b(truth,pred,Info)).
697		negate_bool_formula(b(negation(Eq),pred,_), b(equal(Id,Negated),pred,EqInfo)) :-
698		( Eq = b(equal(Bool,Id),pred,EqInfo)
699		; Eq = b(equal(Id,Bool),pred,EqInfo)
700		),
701		Bool = b(Expr,boolean,BoolInfo),
702		negate_bool_expr(Expr, NExpr),
703		safe_create_texpr(NExpr, boolean, BoolInfo, Negated),
704		Id = b(identifier(_),_,_).
705		negate_bool_formula(b(negation(b(conjunct(A,B),pred,I)),pred,_), New) :-
706		negate_bool_formula(b(negation(A),pred,[]), NewA),
707		negate_bool_formula(b(negation(B),pred,[]), NewB),
708		safe_create_texpr(disjunct(NewA,NewB), pred, I, New).
709		negate_bool_formula(b(negation(b(disjunct(A,B),pred,I)),pred,_), New) :-
710		negate_bool_formula(b(negation(A),pred,[]), NewA),
711		negate_bool_formula(b(negation(B),pred,[]), NewB),
712		safe_create_texpr(conjunct(NewA,NewB), pred, I, New).
713
714		%%%%%%%%%%%%%%%%%%%%% Unit Tests %%%%%%%%%%%%%%%%%%%%%
715		:- begin_tests(extend_candidate_impls_acc).
716
717		test(extend_candidate_impls_acc_less, [true(NewAcc == candidate_impls(global([]),integer([]),integer_ground([b(less(b(identifier(x),integer,[]),b(integer(7),integer,[])),pred,[])]),set([]),set_ground([])))]) :-
718		empty_candidate_impls_acc(EmptyAcc),
719		Arg1 = b(identifier(x),integer,[]),
720		Arg2 = b(integer(7),integer,[]),
721		Ast = b(less(Arg1,Arg2),pred,[]),
722		extend_candidate_impls_acc(pred, less, Arg1, Arg2, Ast, EmptyAcc, NewAcc).
723
724		test(extend_candidate_impls_acc_less_non_ground, [true(NewAcc == candidate_impls(global([]),integer([]),integer_ground([]),set([]),set_ground([])))]) :-
725		empty_candidate_impls_acc(EmptyAcc),
726		Arg1 = b(identifier(x),set(set(integer)),[]),
727		Arg2 = b(set_extension([_]),set(set(integer)),[]),
728		Ast = b(less(Arg1,Arg2),pred,[]),
729		extend_candidate_impls_acc(pred, less, Arg1, Arg2, Ast, EmptyAcc, NewAcc).
730
731		test(extend_candidate_impls_acc_less_no_identifier, [true(NewAcc == candidate_impls(global([]),integer([]),integer_ground([]),set([]),set_ground([])))]) :-
732		empty_candidate_impls_acc(EmptyAcc),
733		Arg1 = b(comprehension_set([b(identifier(x),integer,[])],b(member(b(identifier(x),integer,[]), b(set_extension([b(integer(234),integer,[]),b(integer(34),integer,[])]),set(integer),[])),pred,[])),set(integer),[some,info]),
734		Arg2 = b(set_extension([b(set_extension([b(integer(27),integer,[])]),set(integer),[])]),set(set(integer)),[]),
735		Ast = b(less(Arg1,Arg2),pred,[]),
736		extend_candidate_impls_acc(pred, less, Arg1, Arg2, Ast, EmptyAcc, NewAcc).
737
738		test(extend_candidate_impls_acc_less_eq, [true(NewAcc == candidate_impls(global([]),integer([]),integer_ground([b(less_equal(b(identifier(x),integer,[]),b(integer(7),integer,[])),pred,[])]),set([]),set_ground([])))]) :-
739		empty_candidate_impls_acc(EmptyAcc),
740		Arg1 = b(identifier(x),integer,[]),
741		Arg2 = b(integer(7),integer,[]),
742		Ast = b(less_equal(Arg1,Arg2),pred,[]),
743		extend_candidate_impls_acc(pred, less_equal, Arg1, Arg2, Ast, EmptyAcc, NewAcc).
744
745		test(extend_candidate_impls_acc_less_eq_non_ground, [true(NewAcc == candidate_impls(global([]),integer([]),integer_ground([]),set([]),set_ground([])))]) :-
746		empty_candidate_impls_acc(EmptyAcc),
747		Arg1 = b(identifier(x),set(set(integer)),[]),
748		Arg2 = b(set_extension([_]),set(set(integer)),[]),
749		Ast = b(less_equal(Arg1,Arg2),pred,[]),
750		extend_candidate_impls_acc(pred, less_equal, Arg1, Arg2, Ast, EmptyAcc, NewAcc).
751
752		test(extend_candidate_impls_acc_less_eq_no_identifier, [true(NewAcc == candidate_impls(global([]),integer([]),integer_ground([]),set([]),set_ground([])))]) :-
753		empty_candidate_impls_acc(EmptyAcc),
754		Arg1 = b(comprehension_set([b(identifier(x),integer,[])],b(member(b(identifier(x),integer,[]), b(set_extension([b(integer(234),integer,[]),b(integer(34),integer,[])]),set(integer),[])),pred,[])),set(integer),[some,info]),
755		Arg2 = b(set_extension([b(set_extension([b(integer(27),integer,[])]),set(integer),[])]),set(set(integer)),[]),
756		Ast = b(less_equal(Arg1,Arg2),pred,[]),
757		extend_candidate_impls_acc(pred, less_equal, Arg1, Arg2, Ast, EmptyAcc, NewAcc).
758
759		test(extend_candidate_impls_acc_subset, [true(NewAcc == candidate_impls(global([]),integer([]),integer_ground([]),set([]),set_ground([b(subset(b(identifier(x),set(set(integer)),[]),b(set_extension([b(set_extension([b(integer(27),integer,[])]),set(integer),[])]),set(set(integer)),[])),pred,[])])))]) :-
760		empty_candidate_impls_acc(EmptyAcc),
761		Arg1 = b(identifier(x),set(set(integer)),[]),
762		Arg2 = b(set_extension([b(set_extension([b(integer(27),integer,[])]),set(integer),[])]),set(set(integer)),[]),
763		Ast = b(subset(Arg1,Arg2),pred,[]),
764		extend_candidate_impls_acc(pred, subset, Arg1, Arg2, Ast, EmptyAcc, NewAcc).
765
766		test(extend_candidate_impls_acc_subset_non_ground, [true(NewAcc == candidate_impls(global([]),integer([]),integer_ground([]),set([]),set_ground([])))]) :-
767		empty_candidate_impls_acc(EmptyAcc),
768		Arg1 = b(identifier(x),set(set(integer)),[]),
769		Arg2 = b(set_extension([_]),set(set(integer)),[]),
770		Ast = b(subset(Arg1,Arg2),pred,[]),
771		extend_candidate_impls_acc(pred, subset, Arg1, Arg2, Ast, EmptyAcc, NewAcc).
772
773		test(extend_candidate_impls_acc_subset_no_identifier, [true(NewAcc == candidate_impls(global([]),integer([]),integer_ground([]),set([]),set_ground([])))]) :-
774		empty_candidate_impls_acc(EmptyAcc),
775		Arg1 = b(comprehension_set([b(identifier(x),integer,[])],b(member(b(identifier(x),integer,[]), b(set_extension([b(integer(234),integer,[]),b(integer(34),integer,[])]),set(integer),[])),pred,[])),set(integer),[some,info]),
776		Arg2 = b(set_extension([b(set_extension([b(integer(27),integer,[])]),set(integer),[])]),set(set(integer)),[]),
777		Ast = b(subset(Arg1,Arg2),pred,[]),
778		extend_candidate_impls_acc(pred, subset, Arg1, Arg2, Ast, EmptyAcc, NewAcc).
779
780		test(extend_candidate_impls_acc_subset_strict, [true(NewAcc == candidate_impls(global([]),integer([]),integer_ground([]),set([]),set_ground([b(subset_strict(b(identifier(x),set(set(integer)),[]),b(set_extension([b(set_extension([b(integer(27),integer,[])]),set(integer),[])]),set(set(integer)),[])),pred,[])])))]) :-
781		empty_candidate_impls_acc(EmptyAcc),
782		Arg1 = b(identifier(x),set(set(integer)),[]),
783		Arg2 = b(set_extension([b(set_extension([b(integer(27),integer,[])]),set(integer),[])]),set(set(integer)),[]),
784		Ast = b(subset_strict(Arg1,Arg2),pred,[]),
785		extend_candidate_impls_acc(pred, subset_strict, Arg1, Arg2, Ast, EmptyAcc, NewAcc).
786
787		test(extend_candidate_impls_acc_subset_strict_non_ground, [true(NewAcc == candidate_impls(global([]),integer([]),integer_ground([]),set([]),set_ground([])))]) :-
788		empty_candidate_impls_acc(EmptyAcc),
789		Arg1 = b(identifier(x),set(set(integer)),[]),
790		Arg2 = b(set_extension([_]),set(set(integer)),[]),
791		Ast = b(subset_strict(Arg1,Arg2),pred,[]),
792		extend_candidate_impls_acc(pred, subset_strict, Arg1, Arg2, Ast, EmptyAcc, NewAcc).
793
794		test(extend_candidate_impls_acc_subset_strict_no_identifier, [true(NewAcc == candidate_impls(global([]),integer([]),integer_ground([]),set([]),set_ground([])))]) :-
795		empty_candidate_impls_acc(EmptyAcc),
796		Arg1 = b(comprehension_set([b(identifier(x),integer,[])],b(member(b(identifier(x),integer,[]), b(set_extension([b(integer(234),integer,[]),b(integer(34),integer,[])]),set(integer),[])),pred,[])),set(integer),[some,info]),
797		Arg2 = b(set_extension([b(set_extension([b(integer(27),integer,[])]),set(integer),[])]),set(set(integer)),[]),
798		Ast = b(subset_strict(Arg1,Arg2),pred,[]),
799		extend_candidate_impls_acc(pred, subset_strict, Arg1, Arg2, Ast, EmptyAcc, NewAcc).
800
801		test(extend_candidate_impls_acc_equal, [true(NewAcc == candidate_impls(global([]),integer([]),integer_ground([]),set([]),set_ground([b(equal(b(identifier(x),set(set(integer)),[]),b(set_extension([b(set_extension([b(integer(27),integer,[])]),set(integer),[])]),set(set(integer)),[])),pred,[])])))]) :-
802		empty_candidate_impls_acc(EmptyAcc),
803		Arg1 = b(identifier(x),set(set(integer)),[]),
804		Arg2 = b(set_extension([b(set_extension([b(integer(27),integer,[])]),set(integer),[])]),set(set(integer)),[]),
805		Ast = b(equal(Arg1,Arg2),pred,[]),
806		extend_candidate_impls_acc(pred, equal, Arg1, Arg2, Ast, EmptyAcc, NewAcc).
807
808		test(extend_candidate_impls_acc_member, [true(NewAcc == candidate_impls(global([]),integer([]),integer_ground([]),set([]),set_ground([b(member(b(identifier(x),set(integer),[]),b(set_extension([b(set_extension([b(integer(27),integer,[])]),set(integer),[])]),set(set(integer)),[])),pred,[])])))]) :-
809		empty_candidate_impls_acc(EmptyAcc),
810		Arg1 = b(identifier(x),set(integer),[]),
811		Arg2 = b(set_extension([b(set_extension([b(integer(27),integer,[])]),set(integer),[])]),set(set(integer)),[]),
812		Ast = b(member(Arg1,Arg2),pred,[]),
813		extend_candidate_impls_acc(pred, member, Arg1, Arg2, Ast, EmptyAcc, NewAcc).
814
815		test(extend_candidate_impls_acc_member_non_ground_type, [true(NewAcc == candidate_impls(global([]),integer([]),integer_ground([]),set([]),set_ground([])))]) :-
816		empty_candidate_impls_acc(EmptyAcc),
817		Arg1 = b(identifier(x),set(integer),[]),
818		Arg2 = b(set_extension([b(set_extension([b(integer(27),integer,[])]),set(integer),[])]),set(set(integer)),[]),
819		Ast = b(member(Arg1,Arg2),pred,[]),
820		extend_candidate_impls_acc(_Type, member, Arg1, Arg2, Ast, EmptyAcc, NewAcc).
821
822		test(extend_candidate_impls_acc_add, [true(NewAcc == candidate_impls(global([]),integer([]),integer_ground([]),set([]),set_ground([])))]) :-
823		empty_candidate_impls_acc(EmptyAcc),
824		Arg1 = b(integer(1),integer,[]),
825		Arg2 = b(integer(1),integer,[]),
826		Ast = b(add(Arg1,Arg2),integer,[]),
827		extend_candidate_impls_acc(integer, add, Arg1, Arg2, Ast, EmptyAcc, NewAcc).
828
829		test(extend_candidate_impls_acc_overwrite, [true(NewAcc == candidate_impls(global([]),integer([]),integer_ground([]),set([]),set_ground([])))]) :-
830		empty_candidate_impls_acc(EmptyAcc),
831		Arg1 = b(set_extension([b(couple(b(integer(1),integer,[]),b(integer(2),integer,[])),couple(integer,integer),[info(o),o])]),set(couple(integer,integer)),[]),
832		Arg2 = b(set_extension([b(couple(b(integer(1),integer,[]),b(integer(2),integer,[])),couple(integer,integer),[ein(e),wei(t,e(re)),info])]),set(couple(integer,integer)),[]),
833		Ast = b(overwrite(Arg1,Arg2),set(couple(integer,integer)),[]),
834		extend_candidate_impls_acc(integer, add, Arg1, Arg2, Ast, EmptyAcc, NewAcc).
835
836		test(extend_candidate_impls_acc_overwrite_non_ground_type, [true(NewAcc == candidate_impls(global([]),integer([]),integer_ground([]),set([]),set_ground([])))]) :-
837		empty_candidate_impls_acc(EmptyAcc),
838		Arg1 = b(set_extension([b(couple(b(integer(1),integer,[]),b(integer(2),integer,[])),couple(integer,integer),[info(o),o])]),set(couple(integer,integer)),[]),
839		Arg2 = b(set_extension([b(couple(b(integer(1),integer,[]),b(integer(2),integer,[])),couple(integer,integer),[ein(e),wei(t,e(re)),info])]),set(couple(integer,integer)),[]),
840		Ast = b(overwrite(Arg1,Arg2),set(couple(integer,integer)),[]),
841		extend_candidate_impls_acc(_Type, add, Arg1, Arg2, Ast, EmptyAcc, NewAcc).
842
843		:- end_tests(extend_candidate_impls_acc).
844