236 lines
6.6 KiB
Prolog
236 lines
6.6 KiB
Prolog
/*==============================================================================
|
|
* LPAD and CP-Logic reasoning suite
|
|
* File best.pl
|
|
* Goal oriented interpreter for LPADs based on SLDNF
|
|
* Copyright (c) 2009, Stefano Bragaglia
|
|
*============================================================================*/
|
|
|
|
:- dynamic rule/4, def_rule/2.
|
|
|
|
/* EXTERNAL FILE
|
|
* -------------
|
|
* The following libraries are required by the program to work fine.
|
|
*/
|
|
:- use_module(library(lists)).
|
|
:- use_module(library(system)).
|
|
:- use_module(library(ugraphs)).
|
|
:- use_module(params).
|
|
:- use_module(tptree_lpad).
|
|
:- use_module(utility).
|
|
|
|
% :- source.
|
|
% :- yap_flag(single_var_warnings, on).
|
|
|
|
|
|
|
|
|
|
|
|
/* SOLVING PREDICATES
|
|
* ------------------
|
|
* The predicates in this section solve any given problem with several class of
|
|
* algorithms.
|
|
*
|
|
* Note: the original predicates (no more need and eligible to be deleted) have
|
|
* been moved to the end of the file.
|
|
*/
|
|
|
|
/* solve(GoalsList, Prob, ResTime, BddTime)
|
|
* ----------------------------------------
|
|
* This predicate computes the probability of a given list of goals using an
|
|
* exact algorithm. It also returns the number of handled BDDs (trivial but
|
|
* present for simmetry with other solving predicates), CPUTime spent in
|
|
* performing resolution and in handling the BDDs.
|
|
*
|
|
* INPUT
|
|
* - GoalsList: given list of goal to work on.
|
|
*
|
|
* OUTPUT
|
|
* - Prob: the resulting exact probability for the given list of goals.
|
|
* - Count: number of BDDs handled by the algorithm (trivial, since it's always 1).
|
|
* - ResTime: cpu time spent on performing resolution.
|
|
* - BddTime: cpu time spent on handling BDDs.
|
|
*/
|
|
solve(GoalsList, Prob, ResTime, BddTime) :-
|
|
% Resetting the clocks...
|
|
statistics(walltime, [_, _]),
|
|
|
|
% Performing resolution...
|
|
findall(Deriv, exact(GoalsList, Deriv), List),
|
|
|
|
% Taking elapsed times...
|
|
statistics(walltime, [_, ElapResTime]),
|
|
ResTime is ElapResTime/1000,
|
|
|
|
% Building and solving equivalent bdds...
|
|
init_ptree(1),
|
|
fatto(List),
|
|
insert_list_ptree(List, 1),
|
|
bdd_ptree_map(1, 'bdd.txt', 'bdd.par', 'bdd.map'),
|
|
delete_ptree(1),
|
|
run_file('bdd.txt','bdd.par', Temp),
|
|
(Temp == timeout ->
|
|
Prob is -1.0;
|
|
Prob is Temp),
|
|
|
|
% Taking elapsed times
|
|
statistics(walltime, [_, ElapBddTime]),
|
|
BddTime is ElapBddTime/1000.
|
|
|
|
|
|
|
|
/* exact(GoalsList, CIn, COut) takes a list of goals and an input C set
|
|
and returns an output C set
|
|
The C set is a list of triple (N, R, S) where
|
|
- N is the index of the head atom used, starting from 0
|
|
- R is the index of the non ground rule used, starting from 1
|
|
- S is the substitution of rule R, in the form of a list whose elements
|
|
are of the form 'VarName'=value
|
|
*/
|
|
exact(GoalsList, Deriv) :-
|
|
exact(GoalsList, [], Deriv).
|
|
|
|
exact([], C, C) :- !.
|
|
|
|
exact([bagof(V, EV^G, L)|T], CIn, COut) :- !,
|
|
list2and(GL, G),
|
|
bagof((V, C), EV^exact(GL, CIn, C), LD),
|
|
length(LD, N),
|
|
build_initial_graph(N, GrIn),
|
|
build_graph(LD, 0, GrIn, Gr),
|
|
clique(Gr, Clique),
|
|
build_Cset(LD, Clique, L, [], C1),
|
|
remove_duplicates_eq(C1, C2),
|
|
exact(T, C2, COut).
|
|
|
|
exact([bagof(V, G, L)|T], CIn, COut) :- !,
|
|
list2and(GL, G),
|
|
bagof((V, C), exact(GL, CIn, C), LD),
|
|
length(LD, N),
|
|
build_initial_graph(N, GrIn),
|
|
build_graph(LD, 0, GrIn, Gr),
|
|
clique(Gr, Clique),
|
|
build_Cset(LD, Clique, L, [], C1),
|
|
remove_duplicates_eq(C1, C2),
|
|
exact(T, C2, COut).
|
|
|
|
exact([setof(V, EV^G, L)|T], CIn, COut) :- !,
|
|
list2and(GL, G),
|
|
setof((V, C), EV^exact(GL, CIn, C), LD),
|
|
length(LD, N),
|
|
build_initial_graph(N, GrIn),
|
|
build_graph(LD, 0, GrIn, Gr),
|
|
clique(Gr, Clique),
|
|
build_Cset(LD, Clique, L1, [], C1),
|
|
remove_duplicates(L1, L),
|
|
exact(T, C1, COut).
|
|
|
|
exact([setof(V, G, L)|T], CIn, COut) :- !,
|
|
list2and(GL, G),
|
|
setof((V, C), exact(GL, CIn, C), LD),
|
|
length(LD, N),
|
|
build_initial_graph(N, GrIn),
|
|
build_graph(LD, 0, GrIn, Gr),
|
|
clique(Gr, Clique),
|
|
build_Cset(LD, Clique, L1, [], C1),
|
|
remove_duplicates(L1, L),
|
|
exact(T, C1, COut).
|
|
|
|
exact([\+ H|T], CIn, COut) :-
|
|
builtin(H), !,
|
|
call((\+ H)),
|
|
exact(T, CIn, COut).
|
|
|
|
exact([\+ H |T], CIn, COut) :- !,
|
|
list2and(HL, H),
|
|
findall(D, find_deriv(HL, D), L),
|
|
choose_clauses(CIn, L, C1),
|
|
exact(T, C1, COut).
|
|
|
|
exact([H|T], CIn, COut) :-
|
|
builtin(H), !,
|
|
call(H),
|
|
exact(T, CIn, COut).
|
|
|
|
exact([H|T], CIn, COut) :-
|
|
def_rule(H, B),
|
|
append(B, T, NG),
|
|
exact(NG, CIn, COut).
|
|
|
|
exact([H|T], CIn, COut) :-
|
|
find_rule(H, (R, S, N), B, CIn),
|
|
solve_pres(R, S, N, B, T, CIn, COut).
|
|
|
|
|
|
|
|
solve_pres(R, S, N, B, T, CIn, COut) :-
|
|
member_eq((N, R, S), CIn), !,
|
|
append(B, T, NG),
|
|
exact(NG, CIn, COut).
|
|
|
|
solve_pres(R, S, N, B, T, CIn, COut) :-
|
|
append(CIn, [(N, R, S)], C1),
|
|
append(B, T, NG),
|
|
exact(NG, C1, COut).
|
|
|
|
|
|
|
|
/* find_rule(G, (R, S, N), Body, C)
|
|
* --------------------------------
|
|
* This predicate takes a goal G and the current C set and returns the index R
|
|
* of a disjunctive rule resolving with G together with the index N of the
|
|
* resolving head, the substitution S and the Body of the rule.
|
|
*/
|
|
find_rule(H, (R, S, N), Body, C) :-
|
|
rule(H, _P, N, R, S, _NH, _Head, Body),
|
|
not_already_present_with_a_different_head(N, R, S, C).
|
|
|
|
/* run_file(BDDFile, BDDParFile, Prob)
|
|
* -----------------------------------
|
|
* This predicate calls for the resolution of a BDD via file.
|
|
*/
|
|
run_file(BDDFile, BDDParFile, Prob) :-
|
|
ResultFile = 'result.txt',
|
|
library_directory(Dir),
|
|
setting(timeout, BDDTime),
|
|
(BDDTime = no ->
|
|
atomic_concat([Dir, '/LPADBDD -l ', BDDFile, ' -i ', BDDParFile,' > ', ResultFile], Command);
|
|
atomic_concat([Dir, '/LPADBDD -l ', BDDFile, ' -i ', BDDParFile,' -t ', BDDTime,' > ', ResultFile], Command)),
|
|
|
|
%statistics(walltime,_),
|
|
|
|
shell(Command, Return),
|
|
(Return =\= 0 ->
|
|
Status = timeout,
|
|
Prob = Status;
|
|
|
|
see(ResultFile),
|
|
read(elapsed_construction(_TimeConstruction)),
|
|
read(probability(Prob)),
|
|
read(elapsed_traversing(_TimeTraversing)),
|
|
seen,
|
|
|
|
%write(probability(Prob)),nl,
|
|
%read(_),
|
|
%delete_file(ResultFile),
|
|
|
|
Status = ok
|
|
% format("Construction time ~f traversing time ~f~Number",[TimeConstruction, TimeTraversing])
|
|
).
|
|
|
|
%statistics(walltime,[_,E3]),
|
|
%format(user,'~w ms BDD processing~Number',[E3]),
|
|
% format("Status ~a~Number",[Status]).
|
|
|
|
|
|
|
|
/* insert_list_ptree([Head|Tail], Trie)
|
|
* ------------------------------------
|
|
* This predicate inserts the given list in a trie.
|
|
*/
|
|
insert_list_ptree([], _Trie).
|
|
|
|
insert_list_ptree([Head|Tail], Trie) :-
|
|
reverse(Head, Head1),
|
|
insert_ptree(Head1, Trie),
|
|
insert_list_ptree(Tail, Trie).
|