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