Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Eric Wurbel
pasp
Commits
715289cc
Commit
715289cc
authored
Jun 10, 2016
by
Eric Würbel
Browse files
Initialisation.
parents
Changes
15
Hide whitespace changes
Inline
Side-by-side
asp.pl
0 → 100644
View file @
715289cc
%% -*- prolog -*-
/*
Copyright 2016 Éric Würbel, LSIS-CNRS, AMU
This file is part of PASP. 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 later 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 implements predicates which runs an ASP solver on some
program. It also declares necessary operators for ASP programs
generation.
*/
:-
module
(
asp
,[
run
/
2
,
run
/
3
,
op
(
900
,
fy
,
not
),
op
(
900
,
fy
,
'#minimize'
),
op
(
900
,
fy
,
'#domain'
),
op
(
900
,
fy
,
'#hide'
),
op
(
700
,
xfy
,
'..'
),
op
(
700
,
xfx
,
'!='
)
]).
:-
use_module
(
utils
,[
chars_codes
/
2
]).
:-
use_module
(
library
(
process
)).
:-
use_module
(
library
(
readutil
)).
:-
use_module
(
library
(
charsio
)).
:-
use_module
(
library
(
clpfd
)).
%% run(+File,-Results)
%
% Runs an asp solver on the specified File and collect
% Results. At this time, the only supportedd solver is solver is
% clingo.
run
(
File
,
Results
)
:-
run
(
File
,
Results
,[
opt
(
none
)])
.
%% run(+File,-Results,+Options)
%
% Runs an asp solver on the specified File and collect
% Results. At this time, the only supportedd solver is solver is
% clingo. Option is a list of options. Actually, the supported
% options are :
% - opt(none) synonym for no option
% - opt(inclmin) keep removed sets which are minimal with respect
% to set inclusion. Beware, this is performed by a
% post-processing, i.e. all removed sets are computed, and then
% the minimal ones are filtered.
% - opt(prog) : keep the removed sets computed by the optimization
% implemented inthe program.
run
(
File
,
Results
,[])
:-
run
(
File
,
Results
,[
opt
(
none
)]).
run
(
File
,
Results
,[
Opt
])
:-
nb_getval
(
clasppath
,
Path
),
% --opt-mode=optN is the new syntax of --opt-all (clingo 4.4.0)
nb_getval
(
claspver
,
V
),
(
V
#=
3
->
OPTOPT
=
'--opt-all'
;
OPTOPT
=
'--opt-mode=optN'
),
process_create
(
Path
,
[
0
,
OPTOPT
,
File
],
[
stdout
(
pipe
(
PH
)),
detached
(
true
)]),
collect_results
(
PH
,
Results1
),
close
(
PH
,[
force
(
true
)]),
% hack
post_process
(
Results1
,
Results
,
Opt
)
.
%% post_process(+InResults, -OutResults, +Option)
%
% Do some post processing on collected results.
% Option is a opt/1 term with the following significance :
% none : no optimization : collect all answer sets (i.e. all
% potiential removed sets).
% inclmin : keep inclusion-minimal potential remove sets.
% prog : keep removed sets given by the optimization implemented
% in the program.
% TODO : séparer (et autoriser) trois cas :
% - inclmin seul : comme avant : on garde les incl-min de tous les
% answer sets.
% - prog seul : comme avant : on garde les answer sets optimisés
% du prog.
% - prog+inclmin : on garde les answer sets optimisés, et parmi
% ceux-ci on garde les minimaux suivants l'inclusion.
post_process
(
InResults
,
OutResults
,
opt
(
none
))
:-
filter_nonopt_results
(
InResults
,
OutResults
)
.
post_process
(
InResults
,
OutResults
,
opt
(
inclmin
))
:-
filter_nonopt_results
(
InResults
,
R1
),
keep_inclmin
(
R1
,
OutResults
)
.
post_process
(
InResults
,
OutResults
,
opt
(
prog
))
:-
filter_results
(
InResults
,
R1
),
keep_min_opt
(
R1
,[],
R2
),
final_list
(
R2
,
OutResults
)
.
%% collect_results(+Stream, -Results)
%
% Reads, analyzes and collect results from clasp solver.
collect_results
(
Stream
,
Results
)
:-
read_line_to_codes
(
Stream
,
Line
),
chars_codes
(
LineC
,
Line
),
(
Line
=
end_of_file
->
Results
=
[];
% ->
parse_result_line
(
LineC
,
R
),
(
R
=
end
->
Results
=
[];
% true
(
R
=
garbage
->
collect_results
(
Stream
,
Results
);
% true
Results
=
[
R
|
Results1
],
collect_results
(
Stream
,
Results1
)
)
)
)
.
%% filter_nonopt_results(+In,-Out)
%
% Removes garbage from ASP solver output, i.e. keep only answer
% sets lines.
%
% !! CUT !!
filter_nonopt_results
([],[])
:-
!.
filter_nonopt_results
([
as
(
AS
)|
L1
],[
AS
|
L2
])
:-
!,
filter_nonopt_results
(
L1
,
L2
).
filter_nonopt_results
([
_
|
L1
],
L2
)
:-
filter_nonopt_results
(
L1
,
L2
)
.
%% filter_results(+In, -Out)
%
% Removes garbage, writes triples (Answer #, optimisation value,
% answer set) in a compact way.
%
% !! CUT !!
filter_results
([],[])
:-
!.
filter_results
([
garbage
|
L1
],
L2
)
:-
!,
filter_results
(
L1
,
L2
)
.
filter_results
([
answer_num
(
N
),
as
(
AS
),
optimization
(
O
)|
L1
],[
N
/
O
/
AS
|
L2
])
:-
filter_results
(
L1
,
L2
)
.
%% keep_inclmin(+Collection,?MinIncl)
%
% Succeeds if MinIncl is the collection of inclusion-minimal
% sets of Collection.
keep_inclmin
(
Collection
,
MinIncl
)
:-
keep_inclmin
([],[],
Collection
,
MinIncl
)
.
%% keep_inclmin(+Choosen,+Rejected,+Collection,?Result)
%
% Upon success, Result contains the sets from Collection
% which are minimal according to set inclusion in Collection U
% Rejected, plus the sets which are initially in Chosen. The set
% inclusion test is performed on rsf/2 atoms only.
% See keep_inclmin/2 for everyday use !
keep_inclmin
(
S
,
_
,[],
S
)
:-
!.
keep_inclmin
(
InS
,
R
,[
AS
|
L
],
OutS
)
:-
append
([
InS
,
R
,
L
],
Compare
),
is_incl_min
(
AS
,
Compare
),
!,
keep_inclmin
([
AS
|
InS
],
R
,
L
,
OutS
)
.
keep_inclmin
(
InS
,
R
,[
AS
|
L
],
OutS
)
:-
keep_inclmin
(
InS
,[
AS
|
R
],
L
,
OutS
)
.
%% is_incl_min(+Set, +Collection)
%
% Tests wether Set is minimal according to set inclusion in
% Collection. The set inclusion test is erformed on rsf/2 atoms
% only.
is_incl_min
(
_
,[]).
is_incl_min
(
S
,[
S1
|
L
])
:-
\
+
rsubset
(
S1
,
S
),
is_incl_min
(
S
,
L
)
.
is_incl_min
(
S
,[
S1
|
L
])
:-
rsubset
(
S1
,
S
),
rsubset
(
S
,
S1
),
is_incl_min
(
S
,
L
)
.
%% rsubset(?S1,?S2)
%
% True if all rsf/2 atoms in S1 are also in S2.
rsubset
([],
_
).
rsubset
([
rsf
(
X
,
Y
)|
L
],
S2
)
:-
member
(
rsf
(
X
,
Y
),
S2
),
rsubset
(
L
,
S2
)
.
rsubset
([
A
|
L
],
S2
)
:-
A
\
=
rsf
(
_
,
_
),
rsubset
(
L
,
S2
)
.
%% Keep minimize optimization results
keep_min_opt
([],
L
,
L
).
keep_min_opt
([
N
/
O
/
AS
|
L
],[],
Final
)
:-
keep_min_opt
(
L
,[
N
/
O
/
AS
],
Final
)
.
keep_min_opt
([
N
/
O
/
AS
|
L
],[
_
/
O1
/
_
|
_
],
Final
)
:-
O
#<
O1
,
keep_min_opt
(
L
,[
N
/
O
/
AS
],
Final
)
.
keep_min_opt
([
N
/
O
/
AS
|
L
],[
N1
/
O1
/
AS1
|
L1
],
Final
)
:-
O
#=
O1
,
keep_min_opt
(
L
,[
N
/
O
/
AS
,
N1
/
O1
/
AS1
|
L1
],
Final
)
.
keep_min_opt
([
_
/
O
/
_
|
L
],[
N1
/
O1
/
AS1
|
L1
],
Final
)
:-
O
#>
O1
,
keep_min_opt
(
L
,[
N1
/
O1
/
AS1
|
L1
],
Final
)
.
%% Remove AS number and optimization info.
final_list
([],[]).
final_list
([
_
/
_
/
AS
|
L1
],[
AS
|
L2
])
:-
final_list
(
L1
,
L2
)
.
%% Answer set solver results parser.
parse_result_line
(
Line
,
R
)
:-
phrase
(
result_line
(
R
),
Line
,
_
)
.
result_line
(
garbage
)
-->
[
'c'
,
'l'
,
'i'
,
'n'
,
'g'
,
'o'
],
space
,[
'v'
,
'e'
,
'r'
,
's'
,
'i'
,
'o'
,
'n'
],
space
,
versionspec
(
_
)
.
result_line
(
garbage
)
-->
[
'R'
,
'e'
,
'a'
,
'd'
,
'i'
,
'n'
,
'g'
],
space
,
[
'f'
,
'r'
,
'o'
,
'm'
],
space
,
dirspec
(
_
)
.
result_line
(
garbage
)
-->
[
'S'
,
'o'
,
'l'
,
'v'
,
'i'
,
'n'
,
'g'
,
'.'
,
'.'
,
'.'
]
.
result_line
(
answer_num
(
Num
))
-->
answernum
(
Num
)
.
result_line
(
optimization
(
Num
))
-->
optimize
(
Num
)
.
result_line
(
end
)
-->
[
'O'
,
'P'
,
'T'
,
'I'
,
'M'
,
'U'
,
'M'
,
' '
,
'F'
,
'O'
,
'U'
,
'N'
,
'D'
]
.
result_line
(
end
)
-->
[
'S'
,
'A'
,
'T'
,
'I'
,
'S'
,
'F'
,
'I'
,
'A'
,
'B'
,
'L'
,
'E'
]
.
result_line
(
as
(
AS
))
-->
answer_set
(
AS
)
.
%% version specification (unused for now)
versionspec
([
V
|
VS
])
-->
number
(
V
),
subversion
(
VS
).
subversion
([
V
|
VS
])
-->
[
'.'
],
number
(
V
),
subversion
(
VS
)
.
subversion
([])
-->
[]
.
dirspec
([
C
|
DS
])
-->
[
C
],
{
\
+
char_type
(
C
,
space
)},
dirspec
(
DS
)
.
dirspec
([])
-->
[]
.
%% Interpret the "Answer:" lines of clingo output.
answernum
(
Num
)
-->
[
'A'
,
'n'
,
's'
,
'w'
,
'e'
,
'r'
,
':'
],
space
,
number
(
Num
)
.
%% Interpret the "Optimization" lines of clingo output.
optimize
(
Num
)
-->
[
'O'
,
'p'
,
't'
,
'i'
,
'm'
,
'i'
,
'z'
,
'a'
,
't'
,
'i'
,
'o'
,
'n'
,
':'
],
space
,
number
(
Num
)
.
%% collect answer sets from clingo output
answer_set
([
T
|
L
])
-->
term
(
LT
),
{
LT
\
=
[],
chars_to_term
(
LT
,
T
)
},
end_answer_set
(
L
)
.
end_answer_set
([
T
|
L
])
-->
[
' '
],
term
(
LT
),
{
LT
\
=
[],
chars_to_term
(
LT
,
T
)
},
end_answer_set
(
L
)
.
end_answer_set
([])
-->
[
' '
]
.
end_answer_set
([])
-->
[]
.
term
([
C
|
L
])
-->
[
C
],
{
\
+
char_type
(
C
,
space
)},
term
(
L
)
.
term
([])
-->
[]
.
space
-->
[
' '
],
space
.
space
-->
[]
.
number
(
N
)
-->
digit
(
D0
),
digits
(
D
),
{
number_chars
(
N
,
[
D0
|
D
])
}
.
digits
([
D
|
T
])
-->
digit
(
D
),
digits
(
T
).
digits
([])
-->
[].
digit
(
D
)
-->
[
D
],
{
char_type
(
D
,
digit
)
}
.
chars_to_term
(
Chars
,
Term
)
:-
append
(
Chars
,[
'.'
],
Chars1
),
open_chars_stream
(
Chars1
,
S
),
read
(
S
,
Term
),
close
(
S
)
.
build-executable.sh
0 → 100755
View file @
715289cc
#! /bin/bash
# builing script for pasp.
function
usage
()
{
echo
"syntax :
$0
[-e]"
>
&2
echo
>
&2
echo
"Builds a standalone executable for pasp and paspfilter."
>
&2
echo
>
&2
echo
"options:"
>
&2
echo
"-e
\t
Specifies that external libs should be embeded in the executable"
>
&2
}
ext
=
false
while
getopts
"e"
o
;
do
case
"
$o
"
in
e
)
ext
=
true
;;
[
?]
)
usage
;
exit
1
;;
esac
done
opts
=
""
if
[
"
$ext
"
=
"true"
]
;
then
opts
=
"--foreign=save"
fi
swipl
$opts
--stand_alone
=
true
--goal
=
"go,halt"
--toplevel
=
"halt(1)"
-o
pasp
-c
loader.pl
swipl
$opts
--stand_alone
=
true
--goal
=
"go,halt"
--toplevel
=
"halt(1)"
-o
paspfilter
-c
postfilter_loader.pl
echo
"=================================================================================="
echo
"Compilation finished."
echo
"The command line executable is available in the pasp file."
echo
"The command line executable of the postfilter is available in the paspfilter file."
echo
"=================================================================================="
generator.pl
0 → 100644
View file @
715289cc
%% -*- 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
(
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
)])