mutate(Predicate,TargetPred, conjunct_false(PosNr,SinglePred,InnerTree)) :-
is_a_conjunct(Predicate,_,_),
!,
% check that every conjunct can be set individually to false:
% A1 & ... Ai & ... Ak ----------> A1 & A2 ... not(Ai) & ... Ak
conjunction_to_list(Predicate,List),
select_pred(List, Rest1, SinglePred, Rest2, PosNr),
mutate(SinglePred, InnerTargetPred, InnerTree),
append(Rest1,[InnerTargetPred|Rest2],NewConj), % TO DO: better treatment for well-definedness !?
% if SinglePred is a WD-Guard for Rest2: do not require to analyse Rest2 ?!
conjunct_predicates(NewConj,TargetPred).
mutate(Predicate,TargetPred, disjunct(ITA,ITB)) :-
is_a_disjunct(Predicate,A,B),
!,
mutate(A,MutationA,ITA),
mutate(B,MutationB,ITB),
conjunct_predicates([MutationA,MutationB],TargetPred).
mutate(Predicate,TargetPred, implication_rhs(ITR)) :-
is_an_implication(Predicate,LHS,RHS),
!,
mutate(RHS,MutationRHS,ITR),
conjunct_predicates([LHS,MutationRHS],TargetPred).
mutate(Predicate,TargetPred, equivalence(Pos,ITR)) :-
is_an_equivalence(Predicate,LHS,RHS),
!,
(Pos=rhs,mutate(RHS,MutationRHS,ITR),
conjunct_predicates([LHS,MutationRHS],TargetPred)
;
Pos=lhs,mutate(LHS,MutationLHS,ITR),
conjunct_predicates([MutationLHS,RHS],TargetPred)
).
mutate(Predicate,TargetPred, negation) :-
is_a_negation(Predicate,NPred),
!,
TargetPred = NPred.
mutate(b(E,pred,Info),b(MutationE,pred,Info),atomic(E)) :-
mutate_atomic_pred(E,MutationE),
!.
mutate(Predicate,TargetPred,false(Predicate)) :- !, create_negation(Predicate,TargetPred).