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