1		:- module(welldef, [ensure_wd/2,
2		po_on_lhs/1,
3		po_on_lhs/2,
4		strip_pos/2,
5		strip_pos_keep_toplevel_conj/2,
6		wd_pos/2,
7		filter_typing_pos/1,
8		preprocess_pos_for_cdclt/1]).
9
10		:- use_module(library(lists), [maplist/3, maplist/4, append/2]).
11
12		:- use_module(wdsrc(well_def_hyps), [empty_hyps/1, push_hyp/4, negate_hyp/2]).
13		:- use_module(wdsrc(well_def_analyser), [transform_wd/4, compute_wd/4,
14		toplevel_wd_pos/3]).
15		:- use_module(probsrc(bsyntaxtree), [repair_used_ids/3, add_texpr_infos/3, get_texpr_info/2]).
16		:- use_module(probsrc(b_ast_cleanup), [clean_up_pred/3]).
17		:- use_module(probsrc(preferences), [get_preference/2]).
18		:- use_module(cdclt_solver('cdclt_preprocessing')).
19
20		:- use_module(fuzztypes).
21
22		:- dynamic filter_typing_pos/0, preprocess_pos_for_cdclt/0.
23
24		% Removes some POs that just define the type.
25		filter_typing_pos(true) :-
26		filter_typing_pos, !.
27		filter_typing_pos(true) :-
28		\+ filter_typing_pos,
29		!,
30		asserta(filter_typing_pos).
31		filter_typing_pos(false) :-
32		retractall(filter_typing_pos).
33
34		% Some preprocessing for CDCL(T) such as rewriting WD POs to IDL.
35		preprocess_pos_for_cdclt(true) :-
36		preprocess_pos_for_cdclt, !.
37		preprocess_pos_for_cdclt(true) :-
38		\+ preprocess_pos_for_cdclt,
39		!,
40		asserta(preprocess_pos_for_cdclt).
41		preprocess_pos_for_cdclt(false) :-
42		retractall(preprocess_pos_for_cdclt).
43
44		%% wd_pos(Predicate, ProofObligations).
45		%
46		% Returns a list of proof obligations for the given predicate.
47		wd_pos(Pred, WDPOs) :-
48		empty_hyps(Hyps),
49		findall(WDPO, compute_wd(Pred, Hyps, [discharge_po], WDPO), WDPOs).
50
51
52		%% ensure_wd(+Predicate, -PredicateWithProofObligations).
53		%
54		% Ensures that the given predicate is well-defined by adding open
55		% proof obligations for all well-definedness conditions as additional conjuncts.
56		ensure_wd(Pred, WDPred) :-
57		empty_hyps(Hyps),
58		% push_hyp(Hyps, Pred, [create_full_po], FullHyps),
59		% transform_bexpr(b_ast_cleanup:compute_wd_info, Pred, InterPred),
60		transform_wd(Pred, Hyps, [discharge_po], AnnotatedPred),
61	?	ensure_wd_node(AnnotatedPred, Hyps, _, PrelimWD),
62		repair_used_ids('Welldef Enforcer', PrelimWD, WDPred).
63
64		%% ensure_wd_node(+Ast, +Hyps, -RemainingGoals, -WdAst).
65		%
66		% Implements any WD conditions into the closest predicate nodes.
67		% When not possible the remaining conditions are returned via `RemainingGoals`.
68		ensure_wd_node([N | Ns], H, RemainingPOs, [Wd|Wds]) :-
69		!, % Special case: List.
70		ensure_wd_node_list([N | Ns], H, NestedRemainingPOs, [Wd|Wds]),
71		append(NestedRemainingPOs, RemainingPOs).
72		ensure_wd_node(field(Name,Expr), H, RemainingPOs, NewAst) :-
73		% special case for records b(rec([field(Name,Expr),...]),_,_)
74		!,
75		ensure_wd_node(Expr, H, RemainingPOs, WdExpr),
76		NewAst = field(Name,WdExpr).
77		ensure_wd_node(b(record_field(Id,Atom),Type,Info), _, [], NewAst) :-
78		!,
79		NewAst = b(record_field(Id,Atom),Type,Info).
80		ensure_wd_node(b(Node, Type, Info), H, RemainingPOs, NewAst) :-
81		% Special cases: POs to LHS (middle child)
82		Cases = [general_sum, general_product, quantified_intersection, quantified_union, lambda, forall],
83		node_split(Node, Name, [Ids, Pred, Expr]),
84	?	member(Name, Cases),
85		!,
86		wd_to_lhs(Pred, Expr, H, WdPred, WdExpr),
87		node_split(WdNode, Name, [Ids, WdPred, WdExpr]),
88		WdAst = b(WdNode, Type, Info),
89		toplevel_wd_pos(WdAst, H, RootPOs),
90		conjunct_or_propagate_pos(WdAst, RootPOs, NewAst, RemainingPOs).
91		ensure_wd_node(b(Node, Type, Info), H, RemainingPOs, NewAst) :-
92		% Special cases: POs to RHS (last child)
93		Cases = [event_b_comprehension_set],
94		node_split(Node, Name, [Ids, Expr, Pred]),
95		member(Name, Cases),
96		!,
97		wd_to_rhs(Expr, Pred, H, WdExpr, WdPred),
98		node_split(WdNode, Name, [Ids, WdExpr, WdPred]),
99		WdAst = b(WdNode, Type, Info),
100		toplevel_wd_pos(WdAst, H, RootPOs),
101		conjunct_or_propagate_pos(WdAst, RootPOs, NewAst, RemainingPOs).
102		ensure_wd_node(b(assertion_expression(Test, ErrText, Value), Type, Info), H, POs, Result) :-
103		Result = b(assertion_expression(Test, ErrText, WdValue), Type, Info),
104		ensure_wd_node(Value, H, POs, WdValue).
105		ensure_wd_node(b(if_then_else(If, Then, Else), Type, Info), H, POs, WdIfThenElse) :-
106		Type \= pred, !, % Special case for If-Expressions.
107		ensure_wd_node(If, H, [], WdIf),
108		push_hyp(H, If, [create_full_po], ThenH),
109		transform_wd(Then, H, [discharge_po], TThen),
110		ensure_wd_node(TThen, ThenH, ThenPOs, WdThen),
111		negate_hyp(If, NotIf),
112		push_hyp(H, NotIf, [create_full_po], ElseH),
113		ensure_wd_node(Else, ElseH, ElsePOs, WdElse),
114		if_then_else_po(WdIf, ThenPOs, IfThen),
115		ensure_wd_node(NotIf, H, [], WdNotIf),
116		if_then_else_po(WdNotIf, ElsePOs, NotIfElse),
117		WdIfThenElse = b(if_then_else(WdIf, WdThen, WdElse), Type, Info),
118		append(IfThen, NotIfElse, POs).
119		ensure_wd_node(b(Node, Type, Info), H, RemainingPOs, NewAst) :-
120		% Special cases: WD constraints from LHS chain into RHS
121		Cases = [conjunct,implication],
122		node_split(Node, Name, [Lhs, Rhs]),
123	?	member(Name, Cases),
124		!,
125	?	ensure_wd_node(Lhs, H, [], WdLhs),
126		push_hyp(H, WdLhs, [create_full_po], RhsH),
127	?	ensure_wd_node(Rhs, RhsH, [], WdRhs),
128		node_split(WdNode, Name, [WdLhs, WdRhs]),
129		WdAst = b(WdNode, Type, Info),
130		toplevel_wd_pos(WdAst, H, RootPOs),
131		conjunct_or_propagate_pos(WdAst, RootPOs, NewAst, RemainingPOs).
132		ensure_wd_node(Node, H, RemainderPOs, WdPred) :-
133	?	wd_children_and_pos(Node, H, POs, InterNode),
134		conjunct_or_propagate_pos(InterNode, POs, WdPred, RemainderPOs).
135
136
137		ensure_wd_node_list([], _, [], []) :- !.
138		ensure_wd_node_list([N | Ns], H, [R | Rs], [Wd | Wds]) :-
139	?	ensure_wd_node(N, H, R, Wd),
140	?	ensure_wd_node_list(Ns, H, Rs, Wds).
141
142
143
144		% Helper for repetitive code.
145		wd_children_and_pos(b(Node, Type, Info), H, POs, UpdatedNode) :-
146		node_split(Node, Name, Children),
147	?	ensure_wd_node_list(Children, H, Remainders, WdChildren),
148		append(Remainders, ChildPOs),
149		node_split(NewNode, Name, WdChildren),
150		UpdatedNode = b(NewNode, Type, Info),
151		toplevel_wd_pos(UpdatedNode, H, RootPOs),
152		append(ChildPOs, RootPOs, POs).
153
154
155		% Helps dispatching whether the POs need to be included into a predicate or
156		% an expression needs to propagate them upwards.
157		conjunct_or_propagate_pos(b(Node, pred, Info), POs, WdPred, []) :-
158		!, % predicates conjunct the POs into themselves.
159		filter_discharged_pos(POs, UndischargedPOs),
160		( filter_typing_pos
161		-> filter_typing_pos(UndischargedPOs, FilteredPOs)
162		; FilteredPOs = UndischargedPOs
163		),
164		( preprocess_pos_for_cdclt
165		-> clean_up_pos_for_cdclt(FilteredPOs, CleanPOs)
166		; CleanPOs = FilteredPOs
167		),
168		include_pos(CleanPOs, b(Node, pred, Info), WdPred).
169		conjunct_or_propagate_pos(Node, POs, Node, POs). % Expressions remain unchanged.
170
171
172
173
174
175		% Assumes Lhs is predicate and Rhs is expression.
176		wd_to_lhs(Lhs, Rhs, H, WdLhs, Rhs2) :-
177		ensure_wd_node(Lhs, H, [], Lhs2),
178		push_hyp(H, Lhs2, [create_full_po], NewH),
179		wd_children_and_pos(Rhs, NewH, POs, Rhs2),
180		filter_discharged_pos(POs, UndischargedPOs),
181		( filter_typing_pos
182		-> filter_typing_pos(UndischargedPOs, FilteredPOs)
183		; FilteredPOs = UndischargedPOs
184		),
185		( preprocess_pos_for_cdclt
186		-> clean_up_pos_for_cdclt(FilteredPOs, CleanPOs)
187		; CleanPOs = FilteredPOs
188		),
189		include_pos(CleanPOs, Lhs2, WdLhs).
190		% Assumes Lhs is expression and Rhs is predicate.
191		wd_to_rhs(Lhs, Rhs, H, WdLhs, WdRhs) :-
192		wd_to_lhs(Rhs, Lhs, H, WdRhs, WdLhs).
193
194
195		if_then_else_po(Condition, BranchPOs, Res) :-
196		filter_discharged_pos(BranchPOs, UndischargedPOs),
197		( filter_typing_pos
198		-> filter_typing_pos(UndischargedPOs, FilteredPOs)
199		; FilteredPOs = UndischargedPOs
200		),
201		( preprocess_pos_for_cdclt
202		-> clean_up_pos_for_cdclt(FilteredPOs, CleanPOs)
203		; CleanPOs = FilteredPOs
204		),
205		if_then_else_implication(CleanPOs, Condition, Res).
206
207		if_then_else_implication([], _, []) :- !.
208		if_then_else_implication(POs, Condition, [Res]) :-
209		po_conjunct(POs, BranchConjunct),
210		Res = b(implication(Condition, BranchConjunct), pred, [contains_wd_condition]).
211
212
213
214
215		%% include_pos(ProofObligations, Predicate, PredicateWithPOs).
216		%
217		% Returns a predicate with the given proof obligations included via `conjunct` nodes.
218		include_pos([], Pred, Pred) :- !.
219		include_pos(POs, Pred, b(conjunct(POsConj, Pred), pred, [contains_wd_condition,fuzzed_with_wd_po_included])) :-
220		po_conjunct(POs, POsConj).
221
222		filter_typing_pos([], []).
223		filter_typing_pos([PO|POs], [PO|Rest]) :-
224	?	\+ is_typing_pred_without_wd(PO),
225		!,
226		filter_typing_pos(POs, Rest).
227		filter_typing_pos([_|POs], Filtered) :-
228		filter_typing_pos(POs, Filtered).
229
230		filter_discharged_pos([], []).
231		filter_discharged_pos([PO | POs], [PO | NonDischarged]) :-
232		PO = b(Node, _, Info),
233		Node \= unknown_truth_value(_), % e.g., from external predicate calls such as RPOW
234	?	\+ member(discharged(true, _), Info), !,
235		filter_discharged_pos(POs, NonDischarged).
236		filter_discharged_pos([_|POs], NonDischarged) :-
237		filter_discharged_pos(POs, NonDischarged).
238
239		po_conjunct([PO], PO) :- !.
240		po_conjunct([PO | POs], b(conjunct(PO, POsConj), pred, [contains_wd_condition])) :-
241		po_conjunct(POs, POsConj).
242
243		%% po_on_lhs(+AST).
244		%
245		% Succeeds if the left side of the AST is marked as POs.
246		% This will be the case, if the b/3 structure contains the
247		% `fuzzed_with_wd_po_included` flag.
248		%
249		% AST: The AST to check.
250		po_on_lhs(b(conjunct(_, _), _, Info)) :-
251		member(fuzzed_with_wd_po_included, Info).
252
253		%% po_on_lhs(+AST, -RHS).
254		%
255		% Succeeds if the left side of the AST is marked as POs.
256		% This will be the case, if the b/3 structure contains the
257		% `fuzzed_with_wd_po_included` flag.
258		%
259		% AST: The AST to check.
260		% RHS: The non-PO part of the AST.
261		po_on_lhs(b(conjunct(_, RHS), _, Info), RHS) :-
262		member(fuzzed_with_wd_po_included, Info).
263
264
265		%% strip_pos(+Ast, -AstWithoutPOs).
266		%
267		% Removes any subtrees which are generated by `ensure_wd` from the predicate.
268		strip_pos([A|As], Raws) :-
269		!,
270		maplist(strip_pos, [A|As], Raws).
271		strip_pos(Ast, RawAst) :-
272		po_on_lhs(Ast, InterAst),
273		!,
274		strip_pos(InterAst, RawAst).
275		strip_pos(b(assertion_expression(_, _, SecuredPred), _, _), Result) :-
276		!, % assertion expressions are discarded.
277		strip_pos(SecuredPred, Result).
278		strip_pos(field(Name,Expr), field(Name,SExpr)) :-
279		% special case for records b(rec([field(Name,Expr),...]),_,_)
280		!,
281		strip_pos(Expr, SExpr).
282		strip_pos(b(Node, Type, Info), b(NewNode, Type, Info)) :-
283		node_split(Node, Name, Children),
284		maplist(strip_pos, Children, NewChildren),
285		node_split(NewNode, Name, NewChildren).
286
287		strip_pos_keep_toplevel_conj(b(Node,Type,Info), Raw) :-
288		strip_pos_keep_toplevel_conj_e(Node, Type, Info, RawNode),
289		Raw = b(RawNode,Type,Info).
290
291		strip_pos_keep_toplevel_conj_e(conjunct(Arg1,Arg2), _, _, RawNode) :-
292		!,
293		strip_pos_keep_toplevel_conj(Arg1, RawArg1),
294		strip_pos_keep_toplevel_conj(Arg2, RawArg2),
295		( RawArg1 == truth
296		-> RawNode = RawArg2
297		; RawArg2 == truth
298		-> RawNode = RawArg1
299		; RawNode = conjunct(RawArg1,RawArg2)
300		).
301		strip_pos_keep_toplevel_conj_e(disjunct(_,_), _, Info, RawNode) :-
302		% introduced from IDL solver in CDCL(T)
303		member(fuzzed_with_wd_po_included, Info),
304		!,
305		RawNode = truth.
306		strip_pos_keep_toplevel_conj_e(Node, Type, Info, RawNode) :-
307		strip_pos(b(Node,Type,Info), RawAst),
308		RawAst = b(RawNode,_,_).
309
310		node_split(Node, Name, [b(Child1, T1, I1) | OtherChildren]) :-
311		Node =.. [Name, b(Child1, T1, I1) | OtherChildren], !.
312		node_split(Node, Name, [[A|As] | OtherChildren]) :-
313		Node =.. [Name, [A|As] | OtherChildren], !.
314		node_split(Node, Node, []). % Catches things like integer(42) or integer_set('NAT').
315
316		% Some adjustments to be used in the CDCL(T) solver
317		% just some hard coded cases that occurred often
318		is_typing_pred_without_wd(b(member(Id,B),pred,_)) :-
319		B \= b(domain(_),_,_),
320		B \= b(empty_set,_,_),
321		B \= b(value([]),_,_),
322		B \= b(seq(_),_,_), % seq typing has a wd condition
323		B \= b(seq1(_),_,_),
324		Id = b(identifier(_),_,_).
325		is_typing_pred_without_wd(b(subset(Id,B),pred,_)) :-
326		B \= b(domain(_),_,_),
327		B \= b(empty_set,_,_),
328		B \= b(value([]),_,_),
329		B \= b(seq(_),_,_),
330		B \= b(seq1(_),_,_),
331		Id = b(identifier(_),_,_).
332		is_typing_pred_without_wd(b(subset_strict(Id,B),pred,_)) :-
333		B \= b(domain(_),_,_),
334		B \= b(empty_set,_,_),
335		B \= b(value([]),_,_),
336		B \= b(seq(_),_,_),
337		B \= b(seq1(_),_,_),
338		Id = b(identifier(_),_,_).
339		% from rewriting let-expressions
340		is_typing_pred_without_wd(b(member(b(comprehension_set([b(identifier('_zzzz_unary'),boolean,[]),b(identifier('_zzzz_binary'),integer,[])],_),_,_),_),pred,_)).
341		is_typing_pred_without_wd(b(exists([b(identifier('_zzzz_binary'),integer,_)],_),pred,_)).
342
343		clean_up_pos_for_cdclt([], []).
344		clean_up_pos_for_cdclt([PO|POs], [Clean|Rest]) :-
345		clean_up_and_preprocess_pos_for_cdclt(PO, Clean),
346		!,
347		clean_up_pos_for_cdclt(POs, Rest).
348
349		clean_up_and_preprocess_pos_for_cdclt(Pred, Clean) :-
350		clean_up_pred(Pred, _, TClean),
351		get_preference(cdclt_use_idl_theory_solver, RewriteToIdl), % possibly rewrite WD condition to IDL
352		preprocess_predicate(false, RewriteToIdl, TClean, TLiftedPred, _, _),
353		!,
354		add_texpr_infos(TLiftedPred, [fuzzed_with_wd_po_included], LiftedPred),
355		rewrite_emptyset(LiftedPred, Clean).
356
357		rewrite_emptyset(b(negation(b(equal(A,b(empty_set,Type,Info)),pred,Info2)),pred,Info3), Out) :-
358		% important if we use b_compile on the full predicate in cdclt_solver.pl since empty_set is compiled to value([])
359		!,
360		Out = b(negation(b(equal(A,b(value([]),Type,Info)),pred,Info2)),pred,Info3).
361		rewrite_emptyset(Out, Out).