/*************************/ /* constructive negation */ /* (c) R. Bart½k */ /* 1994 */ /*************************/ % usage: ?-solve(InEqs-Goal,Answer). % where InEqs is a list of input inequalities, possibly empty (input) % Goal is a PROLOG goal (input) % Answer is output evaluation of variables from Goal (output) % example: ?-solve([X\=a]-(p(X),not q(X)),A). :-op(700,xfx,\=). solve(_-true,[]-[]). solve(UnEqs-Goal,Sol):- select_subgoal(Goal,A,Vars,Rest), transfer_subgoal(A,UnEqs,NewA,Unif,NewUnEqs), make_goal(Rest,NewA,Unif,NewGoal), solve(NewUnEqs-NewGoal,SubSol), customize_solution(SubSol,Unif,NewUnEqs,Vars,Sol). solve(_,fail). select_subgoal((A,B),G,Vars,[B|Rest]):- select_subgoal(A,G,SVars,Rest), vars(B,SVars,Vars). select_subgoal(G,G,Vars,[]):- G\==true,G\==(_,_), vars(G,[],Vars). transfer_subgoal(X=Y,UnEqs,true,Unif,NewUnEqs):-!, unify(X,Y,[],Unif), apply_subst_to_uneq(UnEqs,Unif,NewUnEqs). transfer_subgoal(X\=Y,UnEqs,true,[],NewUnEqs):-!, transfer_to_normal_uneq(X\=Y,U), add_uneq(U,UnEqs,NewUnEqs). transfer_subgoal(not A,UnEqs,true,Eqs,NewUnEqs):-!, complex_solve(UnEqs-A,CSol), neg_solution(CSol,[],[],Eqs,NewUnEqs). transfer_subgoal(A,UnEqs,B,Unif,NewUnEqs):- copy_term(A,CopyA), clause(CopyA,B), unify(CopyA,A,[],Unif), apply_subst_to_uneq(UnEqs,Unif,NewUnEqs). make_goal([B|Rest],A,Unif,Goal):- make_goal(Rest,A,Unif,NewA), apply_subst(B,Unif,NewB), and(NewA,NewB,Goal). make_goal([],A,Unif,NewA):- apply_subst(A,Unif,NewA). customize_solution(U-E,Unif,UnEqs,Vars,SolU-SolE):- apply_subst_to_uneq(UnEqs,E,SubUnEqs), apply_subst_to_eq(Unif,E,SubSol), append(SubSol,E,Sol1), select_eqs(Sol1,Vars,SolE), list_vars(SolE,Vars,ExVars), add_uneqs(SubUnEqs,U,SolU1), filter_uneqs(SolU1,ExVars,SolU). apply_subst_to_eq([X=Y|Rest],Subst,[X=NewY|NewRest]):- apply_subst(Y,Subst,NewY), apply_subst_to_eq(Rest,Subst,NewRest). apply_subst_to_eq([],_,[]). apply_subst_to_uneq([U|T],Subst,R):- apply_subst(U,Subst,NewU), transfer_to_normal_uneq(NewU,UnEq), apply_subst_to_uneq(T,Subst,NewT), add_uneq(UnEq,NewT,R). apply_subst_to_uneq([],_,[]). apply_subst(Expr,Subst,NewExpr):- nonvar(Expr), Expr=..[Functor|Args], apply_subst_to_list(Args,Subst,NewArgs), NewExpr=..[Functor|NewArgs]. apply_subst(Var,Subst,Expr):- var(Var), find_subst(Var,Subst,Expr),!. apply_subst(Var,_,Var):- var(Var). apply_subst_to_list([H|T],Subst,[NewH|NewT]):- apply_subst(H,Subst,NewH), apply_subst_to_list(T,Subst,NewT). apply_subst_to_list([],_,[]). select_eqs([X=Exp|T],Vars,[X=Exp|NewT]):- member(X,Vars,NewVars),!, select_eqs(T,NewVars,NewT). select_eqs([_|T],Vars,NewT):- select_eqs(T,Vars,NewT). select_eqs([],_,[]). find_subst(Var,[A=Expr|_],Expr):- Var==A,!. find_subst(Var,[_|Rest],Expr):- find_subst(Var,Rest,Expr). vars(Expr,OldVars,NewVars):- nonvar(Expr), Expr=..[_|Args], list_vars(Args,OldVars,NewVars). vars(Var,OldVars,NewVars):- var(Var), add_to_set(Var,OldVars,NewVars). list_vars([H|T],OldVars,NewVars):- vars(H,OldVars,SVars), list_vars(T,SVars,NewVars). list_vars([],Vars,Vars). add_to_set(X,[Y|Rest],[Y|Rest]):- X==Y,!. add_to_set(X,[Y|Rest],[Y|NewRest]):- add_to_set(X,Rest,NewRest). add_to_set(X,[],[X]). and(true,A,A):-!. and(A,true,A):-!. and(A,B,(A,B)). unify(A,B,OldUnif,[A=B|NewUnif]):- var(A),!, apply_subst_to_list(OldUnif,[A=B],NewUnif). unify(A,B,OldUnif,[B=A|NewUnif]):- var(B),!, apply_subst_to_list(OldUnif,[B=A],NewUnif). unify(A,B,OldUnif,Unif):- A=..[F|ArgsA], B=..[F|ArgsB], unify_lists(ArgsA,ArgsB,OldUnif,Unif). unify_lists([HA|TA],[HB|TB],OldUnif,Unif):- unify(HA,HB,OldUnif,UnifH), apply_subst_to_list(TA,UnifH,TA1), apply_subst_to_list(TB,UnifH,TB1), unify_lists(TA1,TB1,UnifH,Unif). unify_lists([],[],U,U). append([H|T],R,[H|TR]):- append(T,R,TR). append([],T,T). member(X,[Y|T],T):- X==Y,!. member(X,[Y|T],[Y|NewT]):- member(X,T,NewT). transfer_to_normal_uneq(X\=Y,X\=Y):- var(X),!,X\==Y. transfer_to_normal_uneq(X\=Y,Y\=X):- var(Y),!. transfer_to_normal_uneq(X\=Y,true):- X=..[F|ArgF], Y=..[G|ArgG], F\==G. transfer_to_normal_uneq(X\=Y,UnEq):- X=..[F|ArgF], Y=..[F|ArgG], transfer_list_to_uneq(ArgF,ArgG,UnEq), UnEq\==fail. transfer_list_to_uneq([H1|T1],[H2|T2],UnEq):- ite(transfer_to_normal_uneq(H1\=H2,HUnEq), (transfer_list_to_uneq(T1,T2,TUnEq),join_uneqs(HUnEq,TUnEq,UnEq)), transfer_list_to_uneq(T1,T2,UnEq)). transfer_list_to_uneq([],[_|_],true). transfer_list_to_uneq([_|_],[],true). transfer_list_to_uneq([],[],fail). join_uneqs(true,_,true):-!. join_uneqs(_,true,true):-!. join_uneqs(U,fail,U):-!. join_uneqs(X\=Y,A\=B,R):- list(X),list(A), X=[HX|TX],Y=[HY|TY], join_uneqs(HX\=HY,A\=B,SubR), join_uneqs(TX\=TY,SubR,R). join_uneqs(X\=Y,A\=B,R):- list(X),not list(A), ite(is_covered(X\=Y,A\=B), R=(X\=Y), R=([A|X]\=[B|Y])). join_uneqs(X\=Y,A\=B,R):- not list(X),list(A), ite(is_covered(A\=B,X\=Y), R=(A\=B), R=([X|A]\=[Y|B])). join_uneqs(X\=Y,A\=B,R):- not list(A),not list(X), ite(same_uneqs(X\=Y,A\=B), R=(X\=Y), R=([X,A]\=[Y,B])). list(X):- nonvar(X),X=[_|_]. list(X):- X==[]. ite(C,A,B):-C,!,A. ite(_,_,B):-B. filter_uneqs([H|T],Vars,R):- filter_uneqs(T,Vars,SR), ite(is_suitable(H,Vars), R=[H|SR], R=SR). filter_uneqs([],_,[]). same_uneqs(X\=Y,A\=B):- X==A,Y==B,!. same_uneqs(X\=Y,A\=B):- X==B,Y==A,!. is_covered(A,B):- same_uneqs(A,B),!. is_covered(A\=B,X\=Y):- not list(X),list(A), A=[HA|TA],B=[HB|TB], ite(same_uneqs(HA\=HB,X\=Y), true, is_covered(TA\=TB,X\=Y)). is_covered(A\=B,X\=Y):- list(A),list(X), X=[HX|TX],Y=[HY|TY], is_covered(A\=B,HX\=HY), is_covered(A\=B,TX\=TY). is_covered(A\=B,X\=Y):- list(A),list(X), X=[],Y=[]. add_uneq(U,[H|T],R):- U\==true, ite(is_covered(U,H), R=[H|T], ite(is_covered(H,U), add_uneq(U,T,R), (add_uneq(U,T,T1),R=[H|T1]))). add_uneq(U,[],[U]):-U\==true. add_uneq(true,U,U). add_uneqs([H|T],Us,Res):- add_uneq(H,Us,SubR), add_uneqs(T,SubR,Res). add_uneqs([],Us,Us). is_suitable(X\=Y,Vars):- list(X),!, X=[HX|TY],Y=[HY|TY], is_suitable(HX\=HY,Vars), is_suitable(TX\=TY,Vars). is_suitable(X\=Y,Vars):- member(X,Vars,_) ; member(Y,Vars,_). complex_solve(Goal,_):- solve(Goal,Res), Res\==fail, assert(tmp(Goal,Res)),fail. complex_solve(Goal,Res):- collect(Goal,Res). collect(Goal,[NewU-NewE|SRes]):- retract(tmp(G,U-E)),!, unify(G,Goal,[],Unif), apply_subst_to_list(E,Unif,NewE), apply_subst_to_uneq(U,Unif,NewU), collect(Goal,SRes). collect(_,[]). neg_solution([U-E|T],OldEqs,OldUnEqs,NewEqs,NewUnEqs):- gen_mem(X=Y,E), apply_subst_to_uneq([X\=Y],OldEqs,[UnEq]), add_uneq(UnEq,OldUnEqs,UnEqs), neg_solution(T,OldEqs,UnEqs,NewEqs,NewUnEqs). neg_solution([U-E|T],OldEqs,OldUnEqs,NewEqs,NewUnEqs):- gen_mem(X\=Y,U), add_eqs([X=Y|E],OldEqs,Eqs), apply_subst_to_list(T,Eqs,NewT), apply_subst_to_uneq(OldUnEqs,Eqs,UnEqs), neg_solution(NewT,Eqs,UnEqs,NewEqs,NewUnEqs). neg_solution([],E,U,E,U). add_eqs([X=Y|T],OldEqs,NewEqs):- apply_subst(X,OldEqs,NewX), apply_subst(Y,OldEqs,NewY), unify(NewX,NewY,OldEqs,Eqs), add_eqs(T,Eqs,NewEqs). add_eqs([],E,E). gen_mem(X,[X|_]). gen_mem(X,[_|T]):- gen_mem(X,T).