%% -*- prolog -*- %% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% %% Copyright 2016 Éric Würbel, LSIS-CNRS, AMU %% %% This file is part of PASP, a possibilistic ASP solver. %% PASP is free software: you can redistribute it and/or %% modify it under the terms of the GNU General Public License as %% published by the Free Software Foundation, either version 3 of %% the License, or (at your option) any qlater version. %% %% PASP is distributed in the hope that it will be useful, %% but WITHOUT ANY WARRANTY; without even the implied warranty of %% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU %% General Public License for more details. %% %% You should have received a copy of the GNU General Public %% License along with PASP. If not, see %% <http://www.gnu.org/licenses/>. %% %% PASP implements the simulation of possibilistic ASP with %% a classical ASP solver. %% %% This module defines predicates for handling the generation of an ASP %% progam from a PASP program %% %% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% :-module(generator, [ certp/2, necessity/2, pasp_to_asp/3 ]). :-use_module(library(clpfd)). :-use_module(library(apply)). :-use_module(logic). :-use_module(asp). %% cert(+Wff, -Cert) % % compute the cert set (see Bauters & al 2013) cert((A,B),Cert) :- cert(A,CertA), cert(B,CertB), union(CertA,CertB,Cert) . cert((:-B),[N]) :- conjunct_member(nec__(N),B) . cert((_:-B), [N]) :- conjunct_member(nec__(N),B) . %% certp(+Wff, -Certp) % % Compute the cert+ set certp(Wff,Certp) :- cert(Wff,Cert1), nec_complement(Cert1,L2), reverse(L2,Cert2), union(Cert1,Cert2,Cert3), union(Cert3,[0, 50, 100],Certp1), sort(Certp1,Certp) . nec_complement([],[]). nec_complement([N1|L1],[N2|L2]) :- N2 #= 100 - N1, nec_complement(L1,L2) . %% necessity(+Rule, -Necessity) % % Necessity measure of a rule. necessity((:-B),N) :- conjunct_member(nec__(N),B) . necessity((_:-B),N) :- conjunct_member(nec__(N),B) . %% necesity(+Rule, -NewRule, -Necessity) % % Necessity measure of a rule. NewRule is the rule without the % necessity atom. necessity((:-B),(:-NewB),N) :- conjunct_member(nec__(N),B), apply_to_conjuncts(B,is_necessity,B1), flatten_conjunction(B1,NewB) . necessity((H:-B),(H:-NewB),N) :- conjunct_member(nec__(N),B), apply_to_conjuncts(B,is_necessity,B1), flatten_conjunction(B1,NewB) . %% is_necessity(?Atom1, ?Atom2) % % unifies Atom2 with true whenever Atom1 unifies with nec__/1. % Otherwise unifies Atom1 with Atom2. is_necessity(nec__(_),true) :- !. is_necessity(A,A). %% pasp_to_asp(+Pasp, +Certp, -ASP) % % Generate an ASP program from a PASP program, using a cert+ set. % pasp_to_asp(PASP,Certp,ASP) :- collect_pasp_to_asp(PASP,Certp,true,ASP). collect_pasp_to_asp((A,B),Certp,InASP,OutASP) :- collect_pasp_to_asp(A,Certp,InASP,OutASP1), collect_pasp_to_asp(B,Certp,OutASP1,OutASP) . collect_pasp_to_asp((:-B),Certp,InASP,OutASP) :- pasp_rule_to_asp_rules((:-B),Certp,InASP,OutASP) . collect_pasp_to_asp((H:-B),Certp,InASP,OutASP) :- pasp_rule_to_asp_rules((H:-B),Certp,InASP,OutASP) . %% pasp_rule_to_asp_rules(+Rule, +Certp, +InASP, -OutASP) % % Generate the ASP rules corresponding to a PASP rule. pasp_rule_to_asp_rules((H:-B),Certp,InASP,OutASP) :- necessity((H:-B),(H:-NewB),N), include(between(0,N),Certp,[0|L]), rule2rules((H:-NewB),Certp,L,Rules), conjoin(InASP,Rules,OutASP) . pasp_rule_to_asp_rules((:-B),Certp,InASP,OutASP) :- necessity((:-B),(:-NewB),N), include(between(0,N),Certp,[0|L]), rule2rules((:-NewB),Certp,L,Rules), conjoin(InASP,Rules,OutASP) . rule2rules(_,_,[],true). rule2rules((H:-B),Certp,[Cp|L],Rules) :- splitbody(B,PB,NB), % NB \= true, % peut etre inutile. À voir. D #= 100 - Cp, include(between(D,100),Certp,[V1,V2|_]), ( V1 =:= D -> MaxD = V2 ; MaxD = V1 ), newlit(H,Cp,H1), ( PB = true -> PosB = true ; new_posbody(PB,Cp,PosB) ), ( NB = true -> NegB = true ; new_negbody(NB,MaxD,NegB) ), conjoin(PosB,NegB,B1), flatten_conjunction(B1,Body), rule2rules((H:-B),Certp,L,Rules1), ( Body = true -> conjoin(H1,Rules1,Rules) ; conjoin((H1:-Body),Rules1,Rules) ) . rule2rules((:-B),Certp,[Cp|L],Rules) :- splitbody(B,PB,NB), % NB \= true, % peut etre inutile. À voir. D #= 100 - Cp, include(between(D,100),Certp,[V1,V2|_]), ( V1 =:= D -> MaxD = V2 ; MaxD = V1 ), ( PB = true -> PosB = true ; new_posbody(PB,Cp,PosB) ), ( NB = true -> NegB = true ; new_negbody(NB,MaxD,NegB) ), conjoin(PosB,NegB,B1), flatten_conjunction(B1,Body), rule2rules((:-B),Certp,L,Rules1), ( Body = true -> error('empty constraint : ~w~n', [(:-B)]) ; conjoin((:-Body),Rules1,Rules) ) . newlit(-A,V,-Lit) :- atom(A), Lit =.. [A,V] . newlit(A,V,Lit) :- atom(A), A \= -_, Lit =.. [A,V] . newlit(-A,V,-Lit) :- compound(A), A =.. [F|Args], append(Args,[V],NArgs), Lit =.. [F|NArgs] . newlit(A,V,Lit) :- A \= -_, compound(A), A =.. [F|Args], append(Args,[V],NArgs), Lit =.. [F|NArgs] . new_posbody((A,B),V,PosB) :- new_posbody(A,V,A1), new_posbody(B,V,B1), conjoin(A1,B1,PosB) . new_posbody(Lit,V,NewLit) :- Lit \= (_,_), is_asp_literal(Lit), newlit(Lit,V,NewLit) . new_negbody((A,B),V,NegB) :- new_negbody(A,V,A1), new_negbody(B,V,B1), conjoin(A1,B1,NegB) . new_negbody((not Lit),V,(not NewLit)) :- Lit \= (_,_), is_asp_literal(Lit), newlit(Lit,V,NewLit) .