1		:- module(predicate_simplifier, [simplify_pred/2]).
2
3		:- use_module(library(plunit)).
4
5		%% simplify_pred(+Ast, -Simplified).
6		% Incoporate negations, rewrite implications.
7		simplify_pred(b(negation(b(negation(Inner),pred,_)),_,_), Simplified) :-
8		!,
9		simplify_pred(Inner, Simplified).
10		simplify_pred(b(negation(Implication),pred,NegInfo), Simplified) :-
11		Implication = b(implication(_,_),pred,_),
12		!,
13		rewrite_implication(Implication, Disjunction),
14		simplify_pred(b(negation(Disjunction),pred,NegInfo), Simplified).
15		simplify_pred(Implication, Simplified) :-
16		Implication = b(implication(_,_),pred,_),
17		!,
18		rewrite_implication(Implication, Disjunction),
19		simplify_pred(Disjunction, Simplified).
20		simplify_pred(b(negation(Conjunction),pred,NegInfo), Simplified) :-
21		Conjunction = b(conjunct(Lhs,Rhs),pred,_ConjInfo),
22		!,
23		NegLhs = b(negation(Lhs),pred,[]),
24		NegRhs = b(negation(Rhs),pred,[]),
25		simplify_pred(NegLhs, SimpLhs),
26		simplify_pred(NegRhs, SimpRhs),
27		Simplified = b(disjunct(SimpLhs,SimpRhs),pred,[was(negation(conjunct(Lhs,Rhs)))|NegInfo]).
28		simplify_pred(b(negation(Disjunction),pred,NegInfo), Simplified) :-
29		Disjunction = b(disjunct(Lhs,Rhs),pred,_DisjInfo),
30		!,
31		NegLhs = b(negation(Lhs),pred,[]),
32		NegRhs = b(negation(Rhs),pred,[]),
33		simplify_pred(NegLhs, SimpLhs),
34		simplify_pred(NegRhs, SimpRhs),
35		Simplified = b(conjunct(SimpLhs,SimpRhs),pred,[was(negation(disjunct(Lhs,Rhs)))|NegInfo]).
36		simplify_pred(b(negation(Pred),pred,NegInfo), Simplified) :-
37		Pred = b(Node,pred,_),
38		Node =.. [Functor,Lhs,Rhs],
39		negated_pred(Functor, NegFunctor),
40		!,
41		NegNode =.. [NegFunctor,Lhs,Rhs],
42		Simplified = b(NegNode,pred,[was(negation(Node))|NegInfo]).
43		simplify_pred(Ast, Ast).
44
45		rewrite_implication(b(implication(Lhs,Rhs),pred,ImplInfo), Disjunction) :-
46		NegLhs = b(negation(Lhs),pred,[]),
47		simplify_pred(NegLhs, SimpLhs),
48		Disjunction = b(disjunct(SimpLhs,Rhs),pred,[was(implication(Lhs,Rhs))|ImplInfo]).
49
50		negated_pred(member, not_member).
51		negated_pred(not_member, member).
52		negated_pred(less, greater_equal).
53		negated_pred(less_equal, greater).
54		negated_pred(greater, less_equal).
55		negated_pred(greater_equal, less).
56		negated_pred(equal, not_equal).
57		negated_pred(not_equal, equal).
58		negated_pred(subset, not_subset).
59		negated_pred(not_subset, subset).
60		negated_pred(subset_strict, not_subset_strict).
61		negated_pred(not_subset_strict, subset_strict).
62
63		:- begin_tests(simplify_pred).
64
65		test(simplify_neg_conj, [all(Simplified = [b(disjunct(b(less_equal(b(integer(1),integer,[]),b(integer(1),integer,[])),pred,_),b(less_equal(b(integer(1),integer,[]),b(integer(1),integer,[])),pred,_)),pred,_)])]) :-
66		IntOne = b(integer(1),integer,[]),
67		Greater = b(greater(IntOne,IntOne),pred,[]),
68		Pred = b(negation(b(conjunct(Greater,Greater),pred,[])),pred,[]),
69		simplify_pred(Pred, Simplified),
70		ground(Simplified).
71
72		test(simplify_neg_disj, [all(Simplified = [b(conjunct(b(less_equal(b(integer(1),integer,[]),b(integer(1),integer,[])),pred,_),b(less_equal(b(integer(1),integer,[]),b(integer(1),integer,[])),pred,_)),pred,_)])]) :-
73		IntOne = b(integer(1),integer,[]),
74		Greater = b(greater(IntOne,IntOne),pred,[]),
75		Pred = b(negation(b(disjunct(Greater,Greater),pred,[])),pred,[]),
76		simplify_pred(Pred, Simplified),
77		ground(Simplified).
78
79		test(simplify_neg_impl, [all(Simplified = [b(conjunct(b(greater(b(integer(1),integer,[]),b(integer(1),integer,[])),pred,_),b(less_equal(b(integer(1),integer,[]),b(integer(1),integer,[])),pred,_)),pred,_)])]) :-
80		IntOne = b(integer(1),integer,[]),
81		Greater = b(greater(IntOne,IntOne),pred,[]),
82		Pred = b(negation(b(implication(Greater,Greater),pred,[])),pred,[]),
83		simplify_pred(Pred, Simplified),
84		ground(Simplified).
85
86		test(simplify_neg_equal, [all(Simplified = [b(not_equal(b(integer(1),integer,[]),b(integer(1),integer,[])),pred,_)])]) :-
87		IntOne = b(integer(1),integer,[]),
88		Pred = b(negation(b(equal(IntOne,IntOne),pred,[])),pred,[]),
89		simplify_pred(Pred, Simplified),
90		ground(Simplified).
91
92		test(simplify_neg_not_equal, [all(Simplified = [b(equal(b(integer(1),integer,[]),b(integer(1),integer,[])),pred,_)])]) :-
93		IntOne = b(integer(1),integer,[]),
94		Pred = b(negation(b(not_equal(IntOne,IntOne),pred,[])),pred,[]),
95		simplify_pred(Pred, Simplified),
96		ground(Simplified).
97
98		test(simplify_impl, [all(Simplified = [b(disjunct(b(less_equal(IntOne,IntOne),pred,_),b(greater(IntOne,IntOne),pred,[])),pred,_)])]) :-
99		IntOne = b(integer(1),integer,[]),
100		Greater = b(greater(IntOne,IntOne),pred,[]),
101		Pred = b(implication(Greater,Greater),pred,[]),
102		simplify_pred(Pred, Simplified),
103		ground(Simplified).
104
105		:- end_tests(simplify_pred).