1		% (c) 2014-2023 Lehrstuhl fuer Softwaretechnik und Programmiersprachen,
2		% Heinrich Heine Universitaet Duesseldorf
3		% This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html)
4
5		:- module(b_simplifier, [simplify_b_predicate/2, tcltk_simplify_b_predicate/2, tcltk_simplify_b_predicate_error/2]).
6
7		/* Modules and Infos for the code coverage analysis */
8		:- use_module(probsrc(module_information)).
9		:- module_info(group,model_checker).
10		:- module_info(description,'This module provides predicates for simplifying B predicates').
11
12		% Classical B prolog modules
13		:- use_module(probsrc(bsyntaxtree), [get_texpr_expr/2, get_texpr_type/2, create_texpr/4,
14		same_texpr/2, different_texpr_values/2,
15		is_truth/1, is_falsity/1, is_negation_of/2,
16		is_a_conjunct/3, is_a_disjunct/3, is_an_implication/3,
17		conjunct_predicates/2, disjunct_predicates/2,
18		%% extract_info/3,
19		create_negation/2,
20		create_implication/3, create_equivalence/3,
21		create_forall/3, create_or_merge_exists/3]).
22		:- use_module(probsrc(bmachine),[b_parse_machine_predicate/2]).
23		:- use_module(probsrc(kernel_objects),[element_of_global_set/2]).
24
25		%% :- use_module(probsrc(parsercall), [parse_predicate/2]).
26
27		:- use_module(probsrc(preferences),[temporary_set_preference/3, reset_temporary_preference/2]).
28		:- use_module(probsrc(translate), [translate_bexpression/2, generate_typing_predicates/2]).
29		%% :- use_module(probsrc(debug), [debug_print/2, debug_println/2, debug_mode/1]).
30		:- use_module(probsrc(error_manager),[add_internal_error/2]).
31
32		% Importing unit tests predicates
33		:- use_module(probsrc(self_check)).
34
35		% SICSTUS libraries
36		:- use_module(library(avl)).
37		:- use_module(library(plunit)).
38
39
40		tcltk_simplify_b_predicate_error(String,StringResult) :-
41		if(tcltk_simplify_b_predicate(String,StringResult),true,
42		(StringResult = 'Error or User-Interrupt')).
43
44		% exported for the Tcl/Tk interface
45		tcltk_simplify_b_predicate(String,StringResult) :-
46		b_parse_machine_predicate(String,Tree),
47		simplify_b_predicate(Tree,Res),
48		translate_bexpression(Res,StringResult).
49
50		%% simplify_b_predicate(+Pred, -Res).
51		simplify_b_predicate(Pred,Res) :-
52		get_texpr_expr(Pred,Expr),
53		get_texpr_type(Pred,Type),
54		simplify_b_predicate2(Expr,Type,Res).
55
56		simplify_b_predicate2(truth,Type,Res) :- !,
57		create_texpr(truth,Type,[],Res).
58		simplify_b_predicate2(falsity,Type,Res) :- !,
59		create_texpr(falsity,Type,[],Res).
60		simplify_b_predicate2(negation(BExpr),_Type,Res) :- !,
61		simplify_negation(BExpr,Res).
62		simplify_b_predicate2(conjunct(LHS,RHS),Type,Res) :- !,
63		simplify_b_predicate(LHS,SimplifiedLHS),
64		( is_false_constant(SimplifiedLHS) -> % FALSE & f == FALSE
65		create_texpr(falsity,Type,[],Res)
66		; is_true_constant(SimplifiedLHS) -> % TRUE & f == f
67		simplify_b_predicate(RHS,Res)
68		;
69		simplify_b_predicate(RHS,SimplifiedRHS),
70		( is_false_constant(SimplifiedRHS) -> % f & FALSE == FALSE
71		create_texpr(falsity,Type,[],Res)
72		; is_true_constant(SimplifiedRHS) -> % f & TRUE == f
73		Res = SimplifiedLHS
74		; same_texpr(SimplifiedLHS,SimplifiedRHS) -> % f & f == f (idempotence)
75		Res = SimplifiedLHS
76		; is_absorption_rule_conjunct(SimplifiedLHS,SimplifiedRHS,Res) -> % f & (f or g) == f (absorption)
77		true
78		; test_transitivity(SimplifiedLHS,SimplifiedRHS,Res) -> % (f => g) & (g => h) == (f => h)
79		true
80		;
81		conjunct_predicates([SimplifiedLHS,SimplifiedRHS],Res)
82		)
83		).
84		simplify_b_predicate2(disjunct(LHS,RHS),Type,Res) :- !,
85		simplify_b_predicate(LHS,SimplifiedLHS),
86		( is_true_constant(SimplifiedLHS) -> % TRUE or f == TRUE
87		create_texpr(truth,Type,[],Res)
88		; is_false_constant(SimplifiedLHS) -> % FALSE or f == f
89		simplify_b_predicate(RHS,Res)
90		;
91		simplify_b_predicate(RHS,SimplifiedRHS),
92		( is_true_constant(SimplifiedRHS) -> % f or TRUE == TRUE
93		create_texpr(truth,Type,[],Res)
94		; is_false_constant(SimplifiedRHS) -> % f or FALSE == f
95		Res = SimplifiedLHS
96		; same_texpr(SimplifiedLHS,SimplifiedRHS) -> % f or f == f (idempotence)
97		Res = SimplifiedLHS
98		; is_absorption_rule_disjunct(LHS,RHS,Res) -> % f or (f & g) == f (absorption)
99		true
100		;
101		disjunct_predicates([SimplifiedLHS,SimplifiedRHS],Res)
102		)
103		).
104		simplify_b_predicate2(implication(LHS,RHS),_Type,Res) :- !,
105		simplify_b_predicate(RHS,SimplifiedRHS),
106		simplify_implication(LHS,SimplifiedRHS,Res).
107		simplify_b_predicate2(equivalence(LHS,RHS),Type,Res) :- !,
108		simplify_b_predicate(LHS,SimplifiedLHS),
109		simplify_b_predicate(RHS,SimplifiedRHS),
110		( same_texpr(SimplifiedLHS,SimplifiedRHS) -> % f <=> f == TRUE
111		create_texpr(truth,Type,[],Res)
112		; is_negation_of(SimplifiedLHS,SimplifiedRHS) -> % f <=> not(f) == FALSE
113		create_texpr(falsity,Type,[],Res)
114		;
115		create_equivalence(SimplifiedLHS,SimplifiedRHS,Res)
116		).
117		simplify_b_predicate2(equal(LHS,RHS),Type,Res) :- !,
118		print(equal(LHS,RHS)),nl,
119		simplify_b_predicate(LHS,SimplifiedLHS),
120		simplify_b_predicate(RHS,SimplifiedRHS),
121		(same_texpr(SimplifiedLHS,SimplifiedRHS) ->
122		create_texpr(truth,Type,[],Res)
123		; different_texpr_values(SimplifiedLHS,SimplifiedRHS) ->
124		create_texpr(falsity,Type,[],Res)
125		;
126		compare('==',SimplifiedLHS,SimplifiedRHS,equal,Type,Res)
127		%% extract_info(SimplifiedLHS,SimplifiedRHS,Info),
128		%% create_texpr(equal(SimplifiedLHS,SimplifiedRHS),Type,Info,Res)
129		).
130		simplify_b_predicate2(not_equal(LHS,RHS),Type,Res) :- !,
131		simplify_b_predicate(LHS,SimplifiedLHS),
132		simplify_b_predicate(RHS,SimplifiedRHS),
133		(same_texpr(SimplifiedLHS,SimplifiedRHS) ->
134		create_texpr(falsity,Type,[],Res)
135		; different_texpr_values(SimplifiedLHS,SimplifiedRHS) ->
136		create_texpr(truth,Type,[],Res)
137		;
138		compare('=\\=',SimplifiedLHS,SimplifiedRHS,not_equal,Type,Res)
139		%% extract_info(SimplifiedLHS,SimplifiedRHS,Info),
140		%% create_texpr(not_equal(SimplifiedLHS,SimplifiedRHS),Type,Info,Res)
141		).
142		simplify_b_predicate2(greater(LHS,RHS),Type,Res) :- !,
143		simplify_b_predicate(LHS,SimplifiedLHS),
144		simplify_b_predicate(RHS,SimplifiedRHS),
145		compare('>',SimplifiedLHS,SimplifiedRHS,greater,Type,Res).
146		simplify_b_predicate2(greater_equal(LHS,RHS),Type,Res) :- !,
147		simplify_b_predicate(LHS,SimplifiedLHS),
148		simplify_b_predicate(RHS,SimplifiedRHS),
149		compare('>=',SimplifiedLHS,SimplifiedRHS,greater_equal,Type,Res).
150		simplify_b_predicate2(less(LHS,RHS),Type,Res) :- !,
151		simplify_b_predicate(LHS,SimplifiedLHS),
152		simplify_b_predicate(RHS,SimplifiedRHS),
153		compare('<',SimplifiedLHS,SimplifiedRHS,less,Type,Res).
154		simplify_b_predicate2(less_equal(LHS,RHS),Type,Res) :- !,
155		simplify_b_predicate(LHS,SimplifiedLHS),
156		simplify_b_predicate(RHS,SimplifiedRHS),
157		compare('=<',SimplifiedLHS,SimplifiedRHS,less_equal,Type,Res).
158		/* Add more sophisticated implementations for simplifying predicates with quantifiers:
159		E.g.: !(x).(x:S => x<21) == max(S) < 21
160		!(x).(x:S => x/=3) == 3/:S */
161		% Quantified predcates
162		% !(x).(P => Q)
163		simplify_b_predicate2(forall(Ids,LHS,RHS),Type,Res) :- !,
164		simplify_b_predicate(RHS,SimplifiedRHS),
165		(is_true_constant(SimplifiedRHS) ->
166		create_texpr(truth,Type,[],Res)
167		;
168		simplify_b_predicate(LHS,SimplifiedLHS),
169		create_implication(SimplifiedLHS,SimplifiedRHS,ImplicationRes),
170		create_forall(Ids,ImplicationRes,Res)
171		).
172		% #(x).(P)
173		simplify_b_predicate2(exists(Ids,Pred),Type,Res) :- !,
174		simplify_b_predicate(Pred,SimplifiedPred),
175		(is_true_constant(SimplifiedPred) ->
176		create_texpr(truth,Type,[],Res)
177		; is_false_constant(SimplifiedPred) ->
178		create_texpr(falsity,Type,[],Res)
179		;
180		create_or_merge_exists(Ids,SimplifiedPred,Res)
181		).
182		% Simplifying membership relations
183		simplify_b_predicate2(member(Element,Set),Type,Res) :- !,
184		simplify_membership_predicate(Element,Set,Type,Res).
185		simplify_b_predicate2(not_member(Element,Set),Type,Res) :- !,
186		simplify_non_membership_predicate(Element,Set,Type,Res).
187		% TODO: do we need to safe additional information about the predicates
188		simplify_b_predicate2(BExpr,Type,Res) :-
189		create_texpr(BExpr,Type,[],Res).
190		%% (debug_mode(on) ->
191		%% print('Construct not covered yet (b_simplifier):'),nl,
192		%% print(BExpr),nl,
193		%% translate:print_bexpr(Res),nl
194		%% ; true).
195
196		simplify_negation(b(negation(BExpr),pred,_), Res) :- !, % double negation "not not f == f"
197		simplify_b_predicate(BExpr, Res).
198		simplify_negation(Impl, Res) :-
199		Impl = b(implication(Lhs,Rhs),pred,Info),
200		!,
201		simplify_b_predicate(Impl, SImpl),
202		( SImpl \= b(implication(_,_),pred,_)
203		-> % implication could be simplified to TRUTH, FALSITY or a single negation
204		simplify_b_predicate(b(negation(SImpl),pred,Info), Res)
205		; % "not (a => b) == a and not b"
206		NRhs = b(negation(Rhs),pred,[]),
207		simplify_b_predicate(b(conjunct(Lhs,NRhs),pred,Info), Res)
208		).
209		simplify_negation(b(conjunct(Lhs,Rhs),pred,Info), Res) :- !,
210		NLhs = b(negation(Lhs),pred,[]),
211		NRhs = b(negation(Rhs),pred,[]),
212		simplify_b_predicate(b(disjunct(NLhs,NRhs),pred,Info), Res).
213		simplify_negation(b(disjunct(Lhs,Rhs),pred,Info),Res) :- !,
214		NLhs = b(negation(Lhs),pred,[]),
215		NRhs = b(negation(Rhs),pred,[]),
216		simplify_b_predicate(b(conjunct(NLhs,NRhs),pred,Info), Res).
217		simplify_negation(b(forall(Ids,Lhs,Rhs),pred,Info),Res) :- !,
218		simplify_b_predicate(b(negation(b(implication(Lhs,Rhs),pred,Info)),pred,[]), Body),
219		Res = b(exists(Ids,Body),pred,Info).
220		simplify_negation(b(exists(Ids,Body),pred,Info),Res) :- !,
221		simplify_b_predicate(b(negation(Body),pred,[]), NBody),
222		generate_typing_predicates(Ids, TypingList),
223		conjunct_predicates(TypingList, Typing),
224		Res = b(forall(Ids,Typing,NBody),pred,Info).
225		simplify_negation(b(Node,pred,Info),Res) :-
226		Node =.. [Functor,Lhs,Rhs],
227		negated_binary_pred(Functor, NegFunctor),
228		!,
229		NegNode =.. [NegFunctor,Lhs,Rhs],
230		simplify_b_predicate(b(NegNode,pred,Info), Res).
231		simplify_negation(b(Node,pred,Info),Res) :-
232		Node =.. [Functor,Lhs,Rhs],
233		negate_and_swap(Functor, NegFunctor),
234		!,
235		NegNode =.. [NegFunctor,Rhs,Lhs],
236		simplify_b_predicate(b(NegNode,pred,Info), Res).
237		simplify_negation(BExpr, Res) :-
238		simplify_b_predicate(BExpr, SimplifiedBExpr),
239		% Simplifications like "not(FALSE) == TRUE" and "not(TRUE) == FALSE" will be applied by create_negation/2
240		create_negation(SimplifiedBExpr, Res).
241
242		negated_binary_pred(member, not_member).
243		negated_binary_pred(not_member, member).
244		negated_binary_pred(less, greater_equal).
245		negated_binary_pred(less_equal, greater).
246		negated_binary_pred(greater, less_equal).
247		negated_binary_pred(greater_equal, less).
248		negated_binary_pred(equal, not_equal).
249		negated_binary_pred(not_equal, equal).
250		negated_binary_pred(subset, not_subset).
251		negated_binary_pred(not_subset, subset).
252		negated_binary_pred(subset_strict, not_subset_strict).
253		negated_binary_pred(not_subset_strict, subset_strict).
254
255		negate_and_swap(less_real,less_equal_real).
256		negate_and_swap(less_equal_real,less_real).
257
258		simplify_implication(_LHS,SimplifiedRHS,Res) :-
259		is_true_constant(SimplifiedRHS),!, % f => TRUE == TRUE
260		create_texpr(truth,pred,[],Res).
261		simplify_implication(LHS,SimplifiedRHS,Res) :-
262		is_false_constant(SimplifiedRHS),!, % f => FALSE == neg(f)
263		simplify_b_predicate(LHS,SimplifiedLHS),
264		create_negation(SimplifiedLHS,Res).
265		simplify_implication(LHS,SimplifiedRHS,Res) :-
266		simplify_b_predicate(LHS,SimplifiedLHS),
267		(is_false_constant(SimplifiedLHS) -> % FALSE => f == TRUE
268		create_texpr(truth,pred,[],Res)
269		; is_true_constant(SimplifiedLHS) -> % TRUE => f == f
270		Res = SimplifiedRHS
271		; same_texpr(SimplifiedLHS,SimplifiedRHS) -> % f => f == TRUE
272		create_texpr(truth,pred,[],Res)
273		;
274		create_implication(SimplifiedLHS,SimplifiedRHS,Res)
275		).
276
277
278		%%%%%%%%% This is too trivial, we should consider the absorption and transition rules w.r.t. the origin predicate %%%%%%%%%
279		% P or (P & Q) == P
280		is_absorption_rule_disjunct(LHS,RHS,Res) :-
281		is_a_conjunct(RHS,P,Q),
282		(same_texpr(LHS,P); same_texpr(LHS,Q)),!,
283		Res = LHS.
284		% (P & Q) or P == P
285		is_absorption_rule_disjunct(LHS,RHS,Res) :-
286		is_a_conjunct(LHS,P,Q),
287		(same_texpr(RHS,P); same_texpr(RHS,Q)),!,
288		Res = RHS.
289
290		% P & (P or Q) == P
291		is_absorption_rule_conjunct(LHS,RHS,Res) :-
292		is_a_disjunct(RHS,P,Q),
293		(same_texpr(LHS,P); same_texpr(LHS,Q)),!,
294		Res = LHS.
295		% (P or Q) & P == P
296		is_absorption_rule_conjunct(LHS,RHS,Res) :-
297		is_a_disjunct(LHS,P,Q),
298		(same_texpr(RHS,P); same_texpr(RHS,Q)),!,
299		Res = RHS.
300
301		% (P => Q) & (Q => R) == (P => R)
302		test_transitivity(LHS,RHS,Res) :-
303		is_an_implication(LHS,P,Q),
304		is_an_implication(RHS,Q1,R),
305		same_texpr(Q,Q1),!,
306		create_implication(P,R,Res).
307		% (Q => R) & (P => Q) == (P => R)
308		test_transitivity(LHS,RHS,Res) :-
309		is_an_implication(LHS,Q,R),
310		is_an_implication(RHS,P,Q1),
311		same_texpr(Q,Q1),!,
312		create_implication(P,R,Res).
313
314
315		simplify_non_membership_predicate(Element,Set,Type,Res) :-
316		b_integer_value(Element,IsIntValue,EX,_NewElement),
317		IsIntValue,
318		test_integer_membership(Set,EX,Type,Res1),!,
319		(is_true_constant(Res1) ->
320		create_texpr(falsity,Type,[],Res)
321		; is_false_constant(Res1) ->
322		create_texpr(truth,Type,[],Res)
323		;
324		add_internal_error('Internal error: Unexpected result from test_integer_membership/4 predicate in simplify_membership_predicate/4: ',Res1)
325		).
326		simplify_non_membership_predicate(Element,Set,Type,Res) :-
327		b_integer_value(Element,_IsIntValue,_EX,NewElement),
328		create_texpr(not_member(NewElement,Set),Type,[],Res).
329
330		simplify_membership_predicate(Element,Set,Type,Res) :-
331		b_integer_value(Element,IsIntValue,EX,_NewElement),
332		IsIntValue,
333		test_integer_membership(Set,EX,Type,Res),!.
334		simplify_membership_predicate(Element,Set,Type,Res) :-
335		b_integer_value(Element,_IsIntValue,_EX,NewElement),
336		create_texpr(member(NewElement,Set),Type,[],Res).
337
338
339		test_integer_membership(b(empty_set,set(integer),_),_X,Type,Res) :- !,
340		create_texpr(falsity,Type,[],Res).
341		test_integer_membership(b(value(avl_set(AVLSet)),set(integer),_),X,Type,Res) :- !,
342		(avl_fetch(int(X),AVLSet) ->
343		create_texpr(truth,Type,[],Res)
344		;
345		create_texpr(falsity,Type,[],Res)
346		).
347		test_integer_membership(Set,X,Type,Res) :-
348		is_interval_set(Set,Low,Up),!,
349		((Low=<X,X=<Up) ->
350		create_texpr(truth,Type,[],Res)
351		;
352		create_texpr(falsity,Type,[],Res)
353		).
354		test_integer_membership(Set,X,Type,Res) :-
355		is_global_integer_set(Set,GlobalSet),!,
356		(element_of_global_set(int(X),GlobalSet) ->
357		create_texpr(truth,Type,[],Res)
358		;
359		create_texpr(falsity,Type,[],Res)
360		).
361
362		is_interval_set(b(interval(b(Low,integer,_),b(Up,integer,_)),set(integer),_),Low,Up).
363
364		is_global_integer_set(Set,GlobalSet) :-
365		get_texpr_expr(Set,SetExpr),
366		SetExpr = integer_set(GlobalSet),
367		memberchk(GlobalSet,['NATURAL','NAT','INTEGER','INT']).
368
369		is_true_constant(Expr) :-
370		(is_truth(Expr); Expr=boolean_true).
371
372		is_false_constant(Expr) :-
373		(is_falsity(Expr); Expr=boolean_false).
374
375		compare(Operator,LHS,RHS,Functor,Type,Res) :-
376		b_integer_value(LHS,IsIntValueX,EX,NewLHS),
377		b_integer_value(RHS,IsIntValueY,EY,NewRHS),
378		((IsIntValueX,IsIntValueY) ->
379		(memberchk(Operator,['<','>','=<','>=','==','=\\=']) ->
380		Call =.. [Operator,EX,EY],
381		(Call -> create_texpr(truth,Type,[],Res); create_texpr(falsity,Type,[],Res))
382		;
383		add_internal_error('Internal error: Unexpected arithmetic comparison Operator: ', Operator),
384		BExpr =.. [Functor,NewLHS,NewRHS],
385		create_texpr(BExpr,Type,[],Res)
386		)
387		;
388		BExpr =.. [Functor,NewLHS,NewRHS],
389		create_texpr(BExpr,Type,[],Res)
390		).
391
392		b_integer_value(BExpr,IsIntValue,Res,NewBExpr) :-
393		b_arithmetic_expression(BExpr,X),!,
394		Res is X,IsIntValue=true,
395		create_texpr(integer(Res),integer,[],NewBExpr).
396		b_integer_value(BExpr,IsIntValue,Res,NewBExpr) :-
397		Res = BExpr,IsIntValue=false,
398		NewBExpr=BExpr.
399
400		b_arithmetic_expression(BExpr,Res) :-
401		get_texpr_expr(BExpr,Expr),
402		get_texpr_type(BExpr,integer), % only an integer expression
403		b_arithmetic_expression1(Expr,Res).
404
405		b_arithmetic_expression1(integer(X),X) :- !,
406		number(X).
407		b_arithmetic_expression1(unary_minus(E),Res) :- !,
408		b_arithmetic_expression(E,ERes),
409		Res = '-'(ERes).
410		b_arithmetic_expression1(add(E1,E2),Res) :- !,
411		b_arithmetic_expression(E1,E1Res),
412		b_arithmetic_expression(E2,E2Res),
413		Res = '+'(E1Res,E2Res).
414		b_arithmetic_expression1(minus(E1,E2),Res) :- !,
415		b_arithmetic_expression(E1,E1Res),
416		b_arithmetic_expression(E2,E2Res),
417		Res = '-'(E1Res,E2Res).
418		b_arithmetic_expression1(multiplication(E1,E2),Res) :- !,
419		b_arithmetic_expression(E1,E1Res),
420		b_arithmetic_expression(E2,E2Res),
421		Res = '*'(E1Res,E2Res).
422		% it is not the same div as in Prolog X/Y will be rounded down
423		%% b_arithmetic_expression1(div(E1,E2),Res) :- !,
424		%% b_arithmetic_expression(E1,E1Res),
425		%% b_arithmetic_expression(E2,E2Res),
426		%% Res = '//'(E1Res,E2Res).
427
428
429		:- begin_tests(simplify_b_predicate).
430
431		test(simplify_neg_conj, [all(Simplified = [b(less_equal(b(identifier(x),integer,[]),b(integer(1),integer,[])),pred,[])])]) :-
432		IntOne = b(integer(1),integer,[]),
433		Id = b(identifier(x),integer,[]),
434		Greater = b(greater(Id,IntOne),pred,[]),
435		Pred = b(negation(b(conjunct(Greater,Greater),pred,[])),pred,[]),
436		simplify_b_predicate(Pred, Simplified),
437		ground(Simplified).
438
439		test(simplify_neg_disj, [all(Simplified = [b(less_equal(b(identifier(x),integer,[]),b(integer(1),integer,[])),pred,[])])]) :-
440		IntOne = b(integer(1),integer,[]),
441		Id = b(identifier(x),integer,[]),
442		Greater = b(greater(Id,IntOne),pred,[]),
443		Pred = b(negation(b(disjunct(Greater,Greater),pred,[])),pred,[]),
444		simplify_b_predicate(Pred, Simplified),
445		ground(Simplified).
446
447		test(simplify_neg_equal, [all(Simplified = [b(not_equal(b(identifier(x),integer,[]),b(integer(1),integer,[])),pred,_)])]) :-
448		IntOne = b(integer(1),integer,[]),
449		Id = b(identifier(x),integer,[]),
450		Pred = b(negation(b(equal(Id,IntOne),pred,[])),pred,[]),
451		simplify_b_predicate(Pred, Simplified),
452		ground(Simplified).
453
454		test(simplify_neg_not_equal, [all(Simplified = [b(equal(b(identifier(x),integer,[]),b(integer(1),integer,[])),pred,_)])]) :-
455		IntOne = b(integer(1),integer,[]),
456		Id = b(identifier(x),integer,[]),
457		Pred = b(negation(b(not_equal(Id,IntOne),pred,[])),pred,[]),
458		simplify_b_predicate(Pred, Simplified),
459		ground(Simplified).
460
461		test(simplify_impl_to_truth, [all(Simplified = [b(truth,pred,[])])]) :-
462		IntOne = b(integer(1),integer,[]),
463		Id = b(identifier(x),integer,[]),
464		Greater = b(greater(Id,IntOne),pred,[]),
465		Pred = b(implication(Greater,Greater),pred,[]),
466		simplify_b_predicate(Pred, Simplified),
467		ground(Simplified).
468
469		test(simplify_impl_to_falsity, [all(Simplified = [b(falsity,pred,[])])]) :-
470		IntOne = b(integer(1),integer,[]),
471		Id = b(identifier(x),integer,[]),
472		Greater = b(greater(Id,IntOne),pred,[]),
473		Pred = b(negation(b(implication(Greater,Greater),pred,[])),pred,[]),
474		simplify_b_predicate(Pred, Simplified),
475		ground(Simplified).
476
477		test(simplify_impl_same, [all(Simplified = [b(implication(b(greater(b(identifier(x),integer,[]),b(integer(1),integer,[])),pred,[]),b(less(b(identifier(y),integer,[]),b(integer(1),integer,[])),pred,[])),pred,[])])]) :-
478		IntOne = b(integer(1),integer,[]),
479		Id1 = b(identifier(x),integer,[]),
480		Id2 = b(identifier(y),integer,[]),
481		Greater = b(greater(Id1,IntOne),pred,[]),
482		Less = b(less(Id2,IntOne),pred,[]),
483		Pred = b(implication(Greater,Less),pred,[]),
484		simplify_b_predicate(Pred, Simplified),
485		ground(Simplified).
486
487		test(simplify_neg_impl, [all(Simplified = [b(conjunct(b(greater(b(identifier(x),integer,[]),b(integer(1),integer,[])),pred,[]),b(greater_equal(b(identifier(y),integer,[]),b(integer(1),integer,[])),pred,[])),pred,[])])]) :-
488		IntOne = b(integer(1),integer,[]),
489		Id1 = b(identifier(x),integer,[]),
490		Id2 = b(identifier(y),integer,[]),
491		Greater = b(greater(Id1,IntOne),pred,[]),
492		Less = b(less(Id2,IntOne),pred,[]),
493		Pred = b(negation(b(implication(Greater,Less),pred,[])),pred,[]),
494		simplify_b_predicate(Pred, Simplified),
495		ground(Simplified).
496
497		:- end_tests(simplify_b_predicate).
498