predicate_simplifier

negated_pred(member, not_member).

negated_pred(not_member, member).

negated_pred(less, greater_equal).

negated_pred(less_equal, greater).

negated_pred(greater, less_equal).

negated_pred(greater_equal, less).

negated_pred(equal, not_equal).

negated_pred(not_equal, equal).

negated_pred(subset, not_subset).

negated_pred(not_subset, subset).

negated_pred(subset_strict, not_subset_strict).

negated_pred(not_subset_strict, subset_strict).

rewrite_implication(b(implication(Lhs,Rhs),pred,ImplInfo), Disjunction) :-
    NegLhs = b(negation(Lhs),pred,[]),
    simplify_pred(NegLhs, SimpLhs),
    Disjunction = b(disjunct(SimpLhs,Rhs),pred,[was(implication(Lhs,Rhs))|ImplInfo]).

simplify_pred(b(negation(b(negation(Inner),pred,_)),_,_), Simplified) :-
    !,
    simplify_pred(Inner, Simplified).

simplify_pred(b(negation(Implication),pred,NegInfo), Simplified) :-
    Implication = b(implication(_,_),pred,_),
    !,
    rewrite_implication(Implication, Disjunction),
    simplify_pred(b(negation(Disjunction),pred,NegInfo), Simplified).

simplify_pred(Implication, Simplified) :-
    Implication = b(implication(_,_),pred,_),
    !,
    rewrite_implication(Implication, Disjunction),
    simplify_pred(Disjunction, Simplified).

simplify_pred(b(negation(Conjunction),pred,NegInfo), Simplified) :-
    Conjunction = b(conjunct(Lhs,Rhs),pred,_ConjInfo),
    !,
    NegLhs = b(negation(Lhs),pred,[]),
    NegRhs = b(negation(Rhs),pred,[]),
    simplify_pred(NegLhs, SimpLhs),
    simplify_pred(NegRhs, SimpRhs),
    Simplified = b(disjunct(SimpLhs,SimpRhs),pred,[was(negation(conjunct(Lhs,Rhs)))|NegInfo]).

simplify_pred(b(negation(Disjunction),pred,NegInfo), Simplified) :-
    Disjunction = b(disjunct(Lhs,Rhs),pred,_DisjInfo),
    !,
    NegLhs = b(negation(Lhs),pred,[]),
    NegRhs = b(negation(Rhs),pred,[]),
    simplify_pred(NegLhs, SimpLhs),
    simplify_pred(NegRhs, SimpRhs),
    Simplified = b(conjunct(SimpLhs,SimpRhs),pred,[was(negation(disjunct(Lhs,Rhs)))|NegInfo]).

simplify_pred(b(negation(Pred),pred,NegInfo), Simplified) :-
    Pred = b(Node,pred,_),
    Node =.. [Functor,Lhs,Rhs],
    negated_pred(Functor, NegFunctor),
    !,
    NegNode =.. [NegFunctor,Lhs,Rhs],
    Simplified = b(NegNode,pred,[was(negation(Node))|NegInfo]).

simplify_pred(Ast, Ast).

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,_)])]) :-
    IntOne = b(integer(1),integer,[]),
    Greater = b(greater(IntOne,IntOne),pred,[]),
    Pred = b(negation(b(conjunct(Greater,Greater),pred,[])),pred,[]),
    simplify_pred(Pred, Simplified),
    ground(Simplified).

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,_)])]) :-
    IntOne = b(integer(1),integer,[]),
    Greater = b(greater(IntOne,IntOne),pred,[]),
    Pred = b(negation(b(disjunct(Greater,Greater),pred,[])),pred,[]),
    simplify_pred(Pred, Simplified),
    ground(Simplified).

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,_)])]) :-
    IntOne = b(integer(1),integer,[]),
    Greater = b(greater(IntOne,IntOne),pred,[]),
    Pred = b(negation(b(implication(Greater,Greater),pred,[])),pred,[]),
    simplify_pred(Pred, Simplified),
    ground(Simplified).

test(simplify_neg_equal, [all(Simplified = [b(not_equal(b(integer(1),integer,[]),b(integer(1),integer,[])),pred,_)])]) :-
    IntOne = b(integer(1),integer,[]),
    Pred = b(negation(b(equal(IntOne,IntOne),pred,[])),pred,[]),
    simplify_pred(Pred, Simplified),
    ground(Simplified).

test(simplify_neg_not_equal, [all(Simplified = [b(equal(b(integer(1),integer,[]),b(integer(1),integer,[])),pred,_)])]) :-
    IntOne = b(integer(1),integer,[]),
    Pred = b(negation(b(not_equal(IntOne,IntOne),pred,[])),pred,[]),
    simplify_pred(Pred, Simplified),
    ground(Simplified).

test(simplify_impl, [all(Simplified = [b(disjunct(b(less_equal(IntOne,IntOne),pred,_),b(greater(IntOne,IntOne),pred,[])),pred,_)])]) :-
    IntOne = b(integer(1),integer,[]),
    Greater = b(greater(IntOne,IntOne),pred,[]),
    Pred = b(implication(Greater,Greater),pred,[]),
    simplify_pred(Pred, Simplified),
    ground(Simplified).