1511 lines
35 KiB
Prolog
1511 lines
35 KiB
Prolog
/*
|
|
LPAD and CP-Logic reasoning suite
|
|
File lpadsld.pl
|
|
Goal oriented interpreter for LPADs based on SLDNF
|
|
Copyright (c) 2007, Fabrizio Riguzzi
|
|
*/
|
|
%:- set_prolog_flag(debug,on).
|
|
%:- set_prolog_flag(discontiguous_warnings,on).
|
|
%:- set_prolog_flag(single_var_warnings,on).
|
|
%:- source.
|
|
:-dynamic rule/5,rule_by_num/8,rule_uniform/8,def_rule/2,setting/2.
|
|
|
|
:-use_module(library(lists)).
|
|
:-use_module(library(ugraphs)).
|
|
|
|
:-load_foreign_files(['cplint'],[],init_my_predicates).
|
|
|
|
/* start of list of parameters that can be set by the user with
|
|
set(Parameter,Value) */
|
|
setting(epsilon_parsing,0.00001).
|
|
setting(save_dot,false).
|
|
setting(ground_body,true).
|
|
/* available values: true, false
|
|
if true, both the head and the body of each clause will be grounded, otherwise
|
|
only the head is grounded. In the case in which the body contains variables
|
|
not appearing in the head, the body represents an existential event */
|
|
setting(min_error,0.01).
|
|
setting(initial_depth_bound,4).
|
|
setting(depth_bound,4).
|
|
setting(prob_threshold,0.00001).
|
|
setting(prob_bound,0.01).
|
|
|
|
/* end of list of parameters */
|
|
|
|
/* s(GoalsLIst,Prob) compute the probability of a list of goals
|
|
GoalsLis can have variables, s returns in backtracking all the solutions with their
|
|
corresponding probability */
|
|
s(GoalsList,Prob):-
|
|
solve(GoalsList,Prob).
|
|
|
|
|
|
solve(GoalsList,Prob):-
|
|
setof(Deriv,find_deriv(GoalsList,Deriv),LDup),
|
|
rem_dup_lists(LDup,[],L),
|
|
build_formula(L,Formula,[],Var),
|
|
var2numbers(Var,0,NewVar),
|
|
(setting(save_dot,true)->
|
|
format("Variables: ~p~n",[Var]),
|
|
compute_prob(NewVar,Formula,Prob,1)
|
|
;
|
|
compute_prob(NewVar,Formula,Prob,0)
|
|
).
|
|
|
|
solve(GoalsList,0.0):-
|
|
\+ find_deriv(GoalsList,_Deriv).
|
|
|
|
/* s(GoalsList,Prob,CPUTime1,CPUTime2,WallTime1,WallTime2) compute the probability of a list of goals
|
|
GoalsLis can have variables, s returns in backtracking all the solutions with
|
|
their corresponding probability
|
|
CPUTime1 is the cpu time for performing resolution
|
|
CPUTime2 is the cpu time for elaborating the BDD
|
|
WallTime1 is the wall time for performing resolution
|
|
WallTime2 is the wall time for elaborating the BDD */
|
|
|
|
|
|
s(GoalsList,Prob,CPUTime1,CPUTime2,WallTime1,WallTime2):-
|
|
solve(GoalsList,Prob,CPUTime1,CPUTime2,WallTime1,WallTime2).
|
|
|
|
|
|
solve(GoalsList,Prob,CPUTime1,CPUTime2,WallTime1,WallTime2):-
|
|
statistics(cputime,[_,_]),
|
|
statistics(walltime,[_,_]),
|
|
(setof(Deriv,find_deriv(GoalsList,Deriv),LDup)->
|
|
rem_dup_lists(LDup,[],L),
|
|
statistics(cputime,[_,CT1]),
|
|
CPUTime1 is CT1/1000,
|
|
statistics(walltime,[_,WT1]),
|
|
WallTime1 is WT1/1000,
|
|
%print_mem,
|
|
build_formula(L,Formula,[],Var,0,Conj),
|
|
length(L,ND),
|
|
length(Var,NV),
|
|
format(user_error,"Disjunctions :~d~nConjunctions: ~d~nVariables ~d~n",[ND,Conj,NV]),
|
|
var2numbers(Var,0,NewVar),
|
|
(setting(save_dot,true)->
|
|
format("Variables: ~p~n",[Var]),
|
|
compute_prob(NewVar,Formula,Prob,1)
|
|
;
|
|
compute_prob(NewVar,Formula,Prob,0)
|
|
),
|
|
statistics(cputime,[_,CT2]),
|
|
CPUTime2 is CT2/1000,
|
|
statistics(walltime,[_,WT2]),
|
|
WallTime2 is WT2/1000
|
|
;
|
|
%print_mem,
|
|
Prob=0.0,
|
|
statistics(cputime,[_,CT1]),
|
|
CPUTime1 is CT1/1000,
|
|
statistics(walltime,[_,WT1]),
|
|
WallTime1 is WT1/1000,
|
|
CPUTime2 =0.0,
|
|
statistics(walltime,[_,WT2]),
|
|
WallTime2 =0.0
|
|
),!.
|
|
/*,
|
|
format(user_error,"~nMemory after inference~n",[]),
|
|
print_mem.*/
|
|
|
|
/* iterative deepening, depth bounded
|
|
for negative goals, if their derivation is cut, then they are
|
|
added to the head of the list of goals to be resolved at the next depth bound*/
|
|
si(GoalsList,ProbL,ProbU,CPUTime):-
|
|
statistics(cputime,[_,_]),
|
|
setting(initial_depth_bound,D),
|
|
solve_i([(GoalsList,[])],[],D,ProbL,ProbU),
|
|
statistics(cputime,[_,CT]),
|
|
CPUTime is CT/1000.
|
|
|
|
|
|
/* solve_i(L0,Succ,D,ProbL0,ProbU0): L0 is a list of couples (G,Der) where
|
|
G is a list of goals to be resolved and Der is an explanation, D is the
|
|
current depth, ProbL0 is the lower bound of the prob and ProbU0 is the upper
|
|
bound
|
|
*/
|
|
solve_i(L0,Succ,D,ProbL0,ProbU0):-
|
|
findall((G1,Deriv),(member((G0,C0),L0),solvei(G0,D,C0,Deriv,G1)),L),
|
|
% print_mem,
|
|
separate_ulbi(L,[],LL0,[],LU,[],Incomplete),
|
|
append(Succ,LL0,LL),
|
|
compute_prob_deriv(LL,ProbL),
|
|
append(Succ,LU,LU1),
|
|
compute_prob_deriv(LU1,ProbU),
|
|
Err is ProbU-ProbL,
|
|
setting(min_error,ME),
|
|
(Err<ME->
|
|
ProbU0=ProbU,
|
|
ProbL0=ProbL
|
|
;
|
|
setting(depth_bound,DB),
|
|
D1 is D+DB,
|
|
solve_i(Incomplete,LL,D1,ProbL0,ProbU0)
|
|
).
|
|
|
|
/* iterative deepening, problog style: each time
|
|
the derivation is restarted from the original goal */
|
|
sir(GoalsList,ProbL,ProbU,CPUTime):-
|
|
statistics(cputime,[_,_]),
|
|
setting(depth_bound,D),
|
|
solveir(GoalsList,D,ProbL,ProbU),
|
|
statistics(cputime,[_,CT]),
|
|
CPUTime is CT/1000.
|
|
|
|
|
|
/* solveir(GoalsList,D,ProbL0,ProbU0) GoalsLIst is the list
|
|
of goals to be derived, D is the depth bound, ProbL0,ProbU0 are the lower
|
|
and upper bound. If for a certain depth bound the error is not smaller
|
|
than the threshold, the depth bound is increased and the derivation is
|
|
restarted from the beginning */
|
|
solveir(GoalsList,D,ProbL0,ProbU0):-
|
|
(setof(Deriv,find_derivr(GoalsList,D,Deriv),LDup)->
|
|
rem_dup_lists(LDup,[],L),
|
|
% print_mem,
|
|
separate_ulb(L,[],LL,[],LU),
|
|
compute_prob_deriv(LL,ProbL),
|
|
compute_prob_deriv(LU,ProbU),
|
|
Err is ProbU-ProbL,
|
|
setting(min_error,ME),
|
|
(Err<ME->
|
|
ProbU0=ProbU,
|
|
ProbL0=ProbL
|
|
;
|
|
setting(depth_bound,DB),
|
|
D1 is D+DB,
|
|
solveir(GoalsList,D1,ProbL0,ProbU0)
|
|
)
|
|
;
|
|
% print_mem,
|
|
ProbL0=0.0,
|
|
ProbU0=0.0
|
|
).
|
|
|
|
/* approximate algorithm cilog2 style: the explanations with a prob below the
|
|
threshold are cut */
|
|
sic(GoalsList,ProbL,ProbU,CPUTime):-
|
|
statistics(cputime,[_,_]),
|
|
setting(depth_bound,D),
|
|
solveic(GoalsList,D,ProbL,ProbU),
|
|
statistics(cputime,[_,CT]),
|
|
CPUTime is CT/1000.
|
|
|
|
solveic(GoalsList,D,ProbL0,ProbU0):-
|
|
(setof((Deriv,P,Pruned),solvec(GoalsList,D,[],Deriv,1.0,P,Pruned),L)->
|
|
% print_mem,
|
|
separate_ulbc(L,[],LL,0,Err),
|
|
compute_prob_deriv(LL,ProbL0),
|
|
ProbU0 is ProbL0+Err
|
|
/*(ProbU>1.0->
|
|
ProbU0=1.0
|
|
;
|
|
ProbU0=ProbU
|
|
)*/
|
|
;
|
|
% print_mem,
|
|
ProbL0=0.0,
|
|
ProbU0=0.0
|
|
).
|
|
|
|
compute_prob_deriv(LL,ProbL):-
|
|
build_formula(LL,FormulaL,[],VarL,0,_ConjL),
|
|
%length(LL,NDL),
|
|
%length(VarL,NVL),
|
|
%format(user_error,"Disjunctions :~d~nConjunctions: ~d~nVariables ~d~n",[NDL,ConjL,NVL]),
|
|
var2numbers(VarL,0,NewVarL),
|
|
(FormulaL=[]->
|
|
ProbL=0.0
|
|
;
|
|
(FormulaL=[[]|_]->
|
|
ProbL=1.0
|
|
;
|
|
(setting(save_dot,true)->
|
|
% format("Variables: ~p~n",[VarL]),
|
|
compute_prob(NewVarL,FormulaL,ProbL,1)
|
|
;
|
|
compute_prob(NewVarL,FormulaL,ProbL,0)
|
|
)
|
|
)
|
|
).
|
|
|
|
print_mem:-
|
|
statistics(global_stack,[GS,GSF]),
|
|
statistics(local_stack,[LS,LSF]),
|
|
statistics(heap,[HP,HPF]),
|
|
statistics(trail,[TU,TF]),
|
|
format(user_error,"~nGloabal stack used ~d execution stack free: ~d~n",[GS,GSF]),
|
|
format(user_error,"Local stack used ~d execution stack free: ~d~n",[LS,LSF]),
|
|
format(user_error,"Heap used ~d heap free: ~d~n",[HP,HPF]),
|
|
format(user_error,"Trail used ~d Trail free: ~d~n",[TU,TF]).
|
|
|
|
find_deriv(GoalsList,Deriv):-
|
|
solve(GoalsList,[],DerivDup),
|
|
remove_duplicates(DerivDup,Deriv).
|
|
|
|
find_derivr(GoalsList,DB,Deriv):-
|
|
solver(GoalsList,DB,[],DerivDup),
|
|
remove_duplicates(DerivDup,Deriv).
|
|
|
|
|
|
/* duplicate can appear in the C set because two different unistantiated clauses may become the
|
|
same clause when instantiated */
|
|
|
|
/* sc(Goals,Evidence,Prob) compute the conditional probability of the list of goals
|
|
Goals given the list of goals Evidence
|
|
Goals and Evidence can have variables, sc returns in backtracking all the solutions with their
|
|
corresponding probability
|
|
*/
|
|
sc(Goals,Evidence,Prob):-
|
|
solve_cond(Goals,Evidence,Prob).
|
|
|
|
solve_cond(Goals,Evidence,Prob):-
|
|
(setof(DerivE,find_deriv(Evidence,DerivE),LDupE)->
|
|
rem_dup_lists(LDupE,[],LE),
|
|
(setof(DerivGE,find_deriv_GE(LE,Goals,DerivGE),LDupGE)->
|
|
%print_mem,
|
|
rem_dup_lists(LDupGE,[],LGE),
|
|
build_formula(LE,FormulaE,[],VarE),
|
|
var2numbers(VarE,0,NewVarE),
|
|
build_formula(LGE,FormulaGE,[],VarGE),
|
|
var2numbers(VarGE,0,NewVarGE),
|
|
compute_prob(NewVarE,FormulaE,ProbE,0),
|
|
call_compute_prob(NewVarGE,FormulaGE,ProbGE),
|
|
Prob is ProbGE/ProbE
|
|
;
|
|
%print_mem,
|
|
Prob=0.0
|
|
)
|
|
;
|
|
%print_mem,
|
|
Prob=undefined
|
|
).
|
|
/*,
|
|
format(user_error,"~nMemory after inference~n",[]),
|
|
print_mem. */
|
|
|
|
sci(Goals,Evidence,ProbL,ProbU,CPUTime):-
|
|
statistics(cputime,[_,_]),
|
|
setting(depth_bound,D),
|
|
append(Goals,Evidence,GE),
|
|
solve_condi([(GE,[])],[(Evidence,[])],[],[],D,ProbL,ProbU),
|
|
statistics(cputime,[_,CT]),
|
|
CPUTime is CT/1000.
|
|
|
|
solve_condi(LGoals,LEvidence,SuccGE,SuccE,D,ProbL0,ProbU0):-
|
|
findall((GE1,DerivE),
|
|
(member((GE,CE),LEvidence),solvei(GE,D,CE,DerivE,GE1)),
|
|
LE),
|
|
findall((GE1,DerivE),
|
|
(member((GE,CE),LGoals),solvei(GE,D,CE,DerivE,GE1)),
|
|
LGE),
|
|
separate_ulbi(LE,[],LLE0,[],LUE0,[],IncE),
|
|
append(SuccE,LUE0,LUE),
|
|
compute_prob_deriv(LUE,ProbUE),
|
|
(ProbUE\==0.0->
|
|
separate_ulbi(LGE,[],LLGE0,[],LUGE0,[],IncGE),
|
|
append(SuccGE,LLGE0,LLGE),
|
|
compute_prob_deriv(LLGE,ProbLGE),
|
|
ProbL is ProbLGE/ProbUE,
|
|
append(SuccE,LLE0,LLE),
|
|
compute_prob_deriv(LLE,ProbLE),
|
|
(ProbLE\==0.0->
|
|
append(SuccGE,LUGE0,LUGE),
|
|
compute_prob_deriv(LUGE,ProbUGE),
|
|
ProbU1 is ProbUGE/ProbLE
|
|
;
|
|
ProbU1=1.0
|
|
),
|
|
(ProbU1>1.0->
|
|
ProbU=1.0
|
|
;
|
|
ProbU=ProbU1
|
|
),
|
|
Err is ProbU-ProbL,
|
|
setting(min_error,ME),
|
|
(Err<ME->
|
|
ProbU0=ProbU,
|
|
ProbL0=ProbL
|
|
;
|
|
setting(depth_bound,DB),
|
|
D1 is D+DB,
|
|
solve_condi(IncGE,IncE,LLGE,LLE,D1,ProbL0,ProbU0)
|
|
)
|
|
;
|
|
ProbL0=undefined,
|
|
ProbU0=undefined
|
|
).
|
|
|
|
/* iterative deepening, problog style */
|
|
scir(Goals,Evidence,ProbL,ProbU,CPUTime):-
|
|
statistics(cputime,[_,_]),
|
|
setting(depth_bound,D),
|
|
solve_condir(Goals,Evidence,D,ProbL,ProbU),
|
|
statistics(cputime,[_,CT]),
|
|
CPUTime is CT/1000.
|
|
|
|
solve_condir(Goals,Evidence,D,ProbL0,ProbU0):-
|
|
(call_residue(setof(DerivE,find_derivr(Evidence,D,DerivE),LDupE),_R0)->
|
|
rem_dup_lists(LDupE,[],LE),
|
|
append(Evidence,Goals,EG),
|
|
(call_residue(setof(DerivGE,find_derivr(EG,D,DerivGE),LDupGE),_R1)->
|
|
rem_dup_lists(LDupGE,[],LGE),
|
|
separate_ulb(LGE,[],LLGE,[],LUGE),
|
|
compute_prob_deriv(LLGE,ProbLGE),
|
|
compute_prob_deriv(LUGE,ProbUGE),
|
|
separate_ulb(LE,[],LLE,[],LUE),
|
|
compute_prob_deriv(LLE,ProbLE),
|
|
compute_prob_deriv(LUE,ProbUE),
|
|
ProbL is ProbLGE/ProbUE,
|
|
(ProbLE=0.0->
|
|
ProbU1=1.0
|
|
;
|
|
ProbU1 is ProbUGE/ProbLE
|
|
),
|
|
(ProbU1>1.0->
|
|
ProbU=1.0
|
|
;
|
|
ProbU=ProbU1
|
|
),
|
|
Err is ProbU-ProbL,
|
|
setting(min_error,ME),
|
|
(Err<ME->
|
|
ProbU0=ProbU,
|
|
ProbL0=ProbL
|
|
;
|
|
setting(depth_bound,DB),
|
|
D1 is D+DB,
|
|
solve_condir(Goals,Evidence,D1,ProbL0,ProbU0)
|
|
)
|
|
;
|
|
ProbL0=0.0,
|
|
ProbU0=0.0
|
|
)
|
|
;
|
|
ProbL0=undefined,
|
|
ProbU0=undefined
|
|
).
|
|
|
|
/* approximate algorithm cilog2 style */
|
|
scic(Goals,Evidence,ProbL,ProbU,CPUTime):-
|
|
statistics(cputime,[_,_]),
|
|
setting(depth_bound,D),
|
|
solve_condic(Goals,Evidence,D,ProbL,ProbU),
|
|
statistics(cputime,[_,CT]),
|
|
CPUTime is CT/1000.
|
|
|
|
solve_condic(Goals,Evidence,D,ProbL0,ProbU0):-
|
|
(call_residue(setof((DerivE,P,Pruned),solvec(Evidence,D,[],DerivE,1.0,P,Pruned),LE),_R0)->
|
|
append(Evidence,Goals,EG),
|
|
(call_residue(setof((DerivGE,P,Pruned),solvec(EG,D,[],DerivGE,1.0,P,Pruned),LGE),_R1)->
|
|
separate_ulbc(LGE,[],LLGE,0.0,ErrGE),
|
|
compute_prob_deriv(LLGE,ProbLGE),
|
|
separate_ulbc(LE,[],LLE,0.0,ErrE),
|
|
compute_prob_deriv(LLE,ProbLE),
|
|
ProbUGE0 is ProbLGE+ErrGE,
|
|
(ProbUGE0>1.0->
|
|
ProbUGE=1.0
|
|
;
|
|
ProbUGE=ProbUGE0
|
|
),
|
|
ProbUE0 is ProbLE+ErrE,
|
|
(ProbUE0>1.0->
|
|
ProbUE=1.0
|
|
;
|
|
ProbUE=ProbUE0
|
|
),
|
|
ProbL0 is ProbLGE/ProbUE,
|
|
(ProbLE=0.0->
|
|
ProbU1=1.0
|
|
;
|
|
ProbU1 is ProbUGE/ProbLE
|
|
),
|
|
(ProbU1>1.0->
|
|
ProbU0=1.0
|
|
;
|
|
ProbU0=ProbU1
|
|
)
|
|
;
|
|
ProbL0=0.0,
|
|
ProbU0=0.0
|
|
)
|
|
;
|
|
ProbL0=undefined,
|
|
ProbU0=undefined
|
|
).
|
|
|
|
/* sc(Goals,Evidence,Prob,Time1,Time2) compute the conditional probability of the list of goals
|
|
Goals given the list of goals Evidence
|
|
Goals and Evidence can have variables, sc returns in backtracking all the solutions with their
|
|
corresponding probability
|
|
Time1 is the time for performing resolution
|
|
Time2 is the time for elaborating the two BDDs
|
|
*/
|
|
sc(Goals,Evidence,Prob,CPUTime1,CPUTime2,WallTime1,WallTime2):-
|
|
solve_cond(Goals,Evidence,Prob,CPUTime1,CPUTime2,WallTime1,WallTime2).
|
|
|
|
solve_cond(Goals,Evidence,Prob,CPUTime1,CPUTime2,WallTime1,WallTime2):-
|
|
statistics(cputime,[_,_]),
|
|
statistics(walltime,[_,_]),
|
|
(setof(DerivE,find_deriv(Evidence,DerivE),LDupE)->
|
|
rem_dup_lists(LDupE,[],LE),
|
|
(setof(DerivGE,find_deriv_GE(LE,Goals,DerivGE),LDupGE)->
|
|
rem_dup_lists(LDupGE,[],LGE),
|
|
statistics(cputime,[_,CT1]),
|
|
CPUTime1 is CT1/1000,
|
|
statistics(walltime,[_,WT1]),
|
|
WallTime1 is WT1/1000,
|
|
build_formula(LE,FormulaE,[],VarE),
|
|
var2numbers(VarE,0,NewVarE),
|
|
build_formula(LGE,FormulaGE,[],VarGE),
|
|
var2numbers(VarGE,0,NewVarGE),
|
|
compute_prob(NewVarE,FormulaE,ProbE,0),
|
|
call_compute_prob(NewVarGE,FormulaGE,ProbGE),
|
|
Prob is ProbGE/ProbE,
|
|
statistics(cputime,[_,CT2]),
|
|
CPUTime2 is CT2/1000,
|
|
statistics(walltime,[_,WT2]),
|
|
WallTime2 is WT2/1000
|
|
;
|
|
Prob=0.0,
|
|
statistics(cputime,[_,CT1]),
|
|
CPUTime1 is CT1/1000,
|
|
statistics(walltime,[_,WT1]),
|
|
WallTime1 is WT1/1000,
|
|
CPUTime2=0.0,
|
|
WallTime2=0.0
|
|
)
|
|
;
|
|
Prob=undefined,
|
|
statistics(cputime,[_,CT1]),
|
|
CPUTime1 is CT1/1000,
|
|
statistics(walltime,[_,WT1]),
|
|
WallTime1 is WT1/1000,
|
|
CPUTime2=0.0,
|
|
WallTime2=0.0
|
|
).
|
|
|
|
solve_cond_goals(Goals,LE,0,Time1,0):-
|
|
statistics(runtime,[_,_]),
|
|
\+ find_deriv_GE(LE,Goals,_DerivGE),
|
|
statistics(runtime,[_,T1]),
|
|
Time1 is T1/1000.
|
|
|
|
call_compute_prob(NewVarGE,FormulaGE,ProbGE):-
|
|
(FormulaGE=[]->
|
|
ProbGE=0.0
|
|
;
|
|
(FormulaGE=[[]|_]->
|
|
ProbGE=1.0
|
|
;
|
|
(setting(save_dot,true)->
|
|
format("Variables: ~p~n",[NewVarGE]),
|
|
compute_prob(NewVarGE,FormulaGE,ProbGE,1)
|
|
;
|
|
compute_prob(NewVarGE,FormulaGE,ProbGE,0)
|
|
)
|
|
)
|
|
).
|
|
|
|
find_deriv_GE(LD,GoalsList,Deriv):-
|
|
member(D,LD),
|
|
solve(GoalsList,D,DerivDup),
|
|
remove_duplicates(DerivDup,Deriv).
|
|
|
|
find_deriv_GE(LD,GoalsList,DB,Deriv):-
|
|
member(D,LD),
|
|
solve(GoalsList,DB,D,DerivDup),
|
|
remove_duplicates(DerivDup,Deriv).
|
|
|
|
/* solve(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
|
|
*/
|
|
solve([],C,C):-!.
|
|
|
|
solve([bagof(V,EV^G,L)|T],CIn,COut):-!,
|
|
list2and(GL,G),
|
|
bagof((V,C),EV^solve(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),
|
|
solve(T,C2,COut).
|
|
|
|
solve([bagof(V,G,L)|T],CIn,COut):-!,
|
|
list2and(GL,G),
|
|
bagof((V,C),solve(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),
|
|
solve(T,C2,COut).
|
|
|
|
|
|
solve([setof(V,EV^G,L)|T],CIn,COut):-!,
|
|
list2and(GL,G),
|
|
setof((V,C),EV^solve(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),
|
|
solve(T,C1,COut).
|
|
|
|
solve([setof(V,G,L)|T],CIn,COut):-!,
|
|
list2and(GL,G),
|
|
setof((V,C),solve(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),
|
|
solve(T,C1,COut).
|
|
|
|
solve([\+ H |T],CIn,COut):-!,
|
|
list2and(HL,H),
|
|
(setof(D,find_deriv(HL,D),LDup)->
|
|
rem_dup_lists(LDup,[],L),
|
|
choose_clauses(CIn,L,C1),
|
|
solve(T,C1,COut)
|
|
;
|
|
solve(T,CIn,COut)
|
|
).
|
|
|
|
solve([H|T],CIn,COut):-
|
|
builtin(H),!,
|
|
call(H),
|
|
solve(T,CIn,COut).
|
|
|
|
solve([H|T],CIn,COut):-
|
|
def_rule(H,B),
|
|
append(B,T,NG),
|
|
solve(NG,CIn,COut).
|
|
|
|
solve([H|T],CIn,COut):-
|
|
find_rule(H,(R,S,N),B,CIn),
|
|
solve_pres(R,S,N,B,T,CIn,COut).
|
|
|
|
|
|
solvei([],_DB,C,C,[]):-!.
|
|
|
|
solvei(G,0,C,C,G):-!.
|
|
|
|
solvei([\+ H |T],DB,CIn,COut,G):-!,
|
|
list2and(HL,H),
|
|
(findall((GH,D),solvei(HL,DB,CIn,D,GH),L)->
|
|
separate_ulbi(L,[],LB,[],_UB,[],I),
|
|
(I\=[]->
|
|
C1=CIn,
|
|
G=[\+ H|G1]
|
|
;
|
|
choose_clauses(CIn,LB,C1),
|
|
G=G1
|
|
),
|
|
solvei(T,DB,C1,COut,G1)
|
|
;
|
|
solvei(T,DB,CIn,COut,G1)
|
|
).
|
|
solvei([H|T],DB,CIn,COut,G):-
|
|
builtin(H),!,
|
|
call(H),
|
|
solvei(T,DB,CIn,COut,G).
|
|
|
|
solvei([H|T],DB,CIn,COut,G):-
|
|
def_rule(H,B),
|
|
append(B,T,NG),
|
|
DB1 is DB-1,
|
|
solvei(NG,DB1,CIn,COut,G).
|
|
|
|
solvei([H|T],DB,CIn,COut,G):-
|
|
find_rule(H,(R,S,N),B,CIn),
|
|
DB1 is DB-1,
|
|
solve_presi(R,S,N,B,T,DB1,CIn,COut,G).
|
|
|
|
solver([],_DB,C,C):-!.
|
|
|
|
solver(_G,0,C,[(_,pruned,_)|C]):-!.
|
|
|
|
solver([\+ H |T],DB,CIn,COut):-!,
|
|
list2and(HL,H),
|
|
(setof(D,find_derivr(HL,DB,D),LDup)->
|
|
rem_dup_lists(LDup,[],L),
|
|
separate_ulb(L,[],LB,[],UB),
|
|
(\+ LB=UB->
|
|
|
|
choose_clauses(CIn,LB,C0),
|
|
C1=[(_,pruned,_)|C0]
|
|
;
|
|
choose_clauses(CIn,L,C1)
|
|
),
|
|
solver(T,DB,C1,COut)
|
|
;
|
|
solver(T,DB,CIn,COut)
|
|
).
|
|
solver([H|T],DB,CIn,COut):-
|
|
builtin(H),!,
|
|
call(H),
|
|
solver(T,DB,CIn,COut).
|
|
|
|
solver([H|T],DB,CIn,COut):-
|
|
def_rule(H,B),
|
|
append(B,T,NG),
|
|
DB1 is DB-1,
|
|
solver(NG,DB1,CIn,COut).
|
|
|
|
solver([H|T],DB,CIn,COut):-
|
|
find_rule(H,(R,S,N),B,CIn),
|
|
DB1 is DB-1,
|
|
solve_presr(R,S,N,B,T,DB1,CIn,COut).
|
|
|
|
|
|
solvec([],_DB,C,C,P,P,false):-!.
|
|
|
|
solvec(_G,0,C,C,P,P,true):-!.
|
|
|
|
solvec(_G,_DB,C,C,P,P,true):-
|
|
setting(prob_threshold,T),
|
|
P=<T,!.
|
|
|
|
solvec([\+ H |T],DB,CIn,COut,P0,P1,Pruned):-!,
|
|
list2and(HL,H),
|
|
(setof((D,P,Pr),solvec(HL,DB,[],D,1,P,Pr),L)->
|
|
separate_ulbc(L,[],LB,0.0,PP),
|
|
(PP=\=0.0->
|
|
|
|
choose_clausesc(CIn,LB,C1,P0,P2),
|
|
Pruned=true,
|
|
solvec(T,DB,C1,COut,P2,P1,_)
|
|
|
|
;
|
|
choose_clausesc(CIn,LB,C1,P0,P2),
|
|
solvec(T,DB,C1,COut,P2,P1,Pruned)
|
|
)
|
|
;
|
|
solve(T,DB,CIn,COut,P0,P1,Pruned)
|
|
).
|
|
|
|
solvec([H|T],DB,CIn,COut,P0,P1,Pruned):-
|
|
builtin(H),!,
|
|
call(H),
|
|
solvec(T,DB,CIn,COut,P0,P1,Pruned).
|
|
|
|
solvec([H|T],DB,CIn,COut,P0,P1,Pruned):-
|
|
def_rule(H,B),
|
|
append(B,T,NG),
|
|
DB1 is DB-1,
|
|
solvec(NG,DB1,CIn,COut,P0,P1,Pruned).
|
|
|
|
solvec([H|T],DB,CIn,COut,P0,P1,Pruned):-
|
|
find_rulec(H,(R,S,N),B,CIn,P),
|
|
DB1 is DB-1,
|
|
solve_presc(R,S,N,B,T,DB1,CIn,COut,P,P0,P1,Pruned).
|
|
|
|
|
|
solve_pres(R,S,N,B,T,CIn,COut):-
|
|
member_eq((N,R,S),CIn),!,
|
|
append(B,T,NG),
|
|
solve(NG,CIn,COut).
|
|
|
|
solve_pres(R,S,N,B,T,CIn,COut):-
|
|
append(CIn,[(N,R,S)],C1),
|
|
append(B,T,NG),
|
|
solve(NG,C1,COut).
|
|
|
|
solve_presi(R,S,N,B,T,DB,CIn,COut,G):-
|
|
member_eq((N,R,S),CIn),!,
|
|
append(B,T,NG),
|
|
solvei(NG,DB,CIn,COut,G).
|
|
|
|
solve_presi(R,S,N,B,T,DB,CIn,COut,G):-
|
|
append(CIn,[(N,R,S)],C1),
|
|
append(B,T,NG),
|
|
solvei(NG,DB,C1,COut,G).
|
|
|
|
|
|
solve_presr(R,S,N,B,T,DB,CIn,COut):-
|
|
member_eq((N,R,S),CIn),!,
|
|
append(B,T,NG),
|
|
solver(NG,DB,CIn,COut).
|
|
|
|
solve_presr(R,S,N,B,T,DB,CIn,COut):-
|
|
append(CIn,[(N,R,S)],C1),
|
|
append(B,T,NG),
|
|
solver(NG,DB,C1,COut).
|
|
|
|
|
|
solve_presc(R,S,N,B,T,DB,CIn,COut,_,P0,P1,Pruned):-
|
|
member_eq((N,R,S),CIn),!,
|
|
append(B,T,NG),
|
|
solvec(NG,DB,CIn,COut,P0,P1,Pruned).
|
|
|
|
solve_presc(R,S,N,B,T,DB,CIn,COut,P,P0,P1,Pruned):-
|
|
append(CIn,[(N,R,S)],C1),
|
|
append(B,T,NG),
|
|
P2 is P0*P,
|
|
solvec(NG,DB,C1,COut,P2,P1,Pruned).
|
|
|
|
|
|
build_initial_graph(N,G):-
|
|
listN(0,N,Vert),
|
|
add_vertices([],Vert,G).
|
|
|
|
|
|
build_graph([],_N,G,G).
|
|
|
|
build_graph([(_V,C)|T],N,GIn,GOut):-
|
|
N1 is N+1,
|
|
compatible(C,T,N,N1,GIn,G1),
|
|
build_graph(T,N1,G1,GOut).
|
|
|
|
compatible(_C,[],_N,_N1,G,G).
|
|
|
|
compatible(C,[(_V,H)|T],N,N1,GIn,GOut):-
|
|
(compatible(C,H)->
|
|
add_edges(GIn,[N-N1,N1-N],G1)
|
|
;
|
|
G1=GIn
|
|
),
|
|
N2 is N1 +1,
|
|
compatible(C,T,N,N2,G1,GOut).
|
|
|
|
compatible([],_C).
|
|
|
|
compatible([(N,R,S)|T],C):-
|
|
not_present_with_a_different_head(N,R,S,C),
|
|
compatible(T,C).
|
|
|
|
not_present_with_a_different_head(_N,_R,_S,[]).
|
|
|
|
not_present_with_a_different_head(N,R,S,[(N,R,S)|T]):-!,
|
|
not_present_with_a_different_head(N,R,S,T).
|
|
|
|
not_present_with_a_different_head(N,R,S,[(_N1,R,S1)|T]):-
|
|
S\=S1,!,
|
|
not_present_with_a_different_head(N,R,S,T).
|
|
|
|
not_present_with_a_different_head(N,R,S,[(_N1,R1,_S1)|T]):-
|
|
R\=R1,
|
|
not_present_with_a_different_head(N,R,S,T).
|
|
|
|
|
|
|
|
build_Cset(_LD,[],[],C,C).
|
|
|
|
build_Cset(LD,[H|T],[V|L],CIn,COut):-
|
|
nth0(H,LD,(V,C)),
|
|
append(C,CIn,C1),
|
|
build_Cset(LD,T,L,C1,COut).
|
|
|
|
|
|
/* find_rule(G,(R,S,N),Body,C) 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,_,Head,Body),
|
|
member_head(H,Head,0,N),
|
|
not_already_present_with_a_different_head(N,R,S,C).
|
|
|
|
find_rule(H,(R,S,Number),Body,C):-
|
|
rule_uniform(H,R,S,_,1/_Num,_L,Number,Body),
|
|
not_already_present_with_a_different_head(Number,R,S,C).
|
|
|
|
find_rulec(H,(R,S,N),Body,C,P):-
|
|
rule(H,_P,N,R,S,_,Head,Body),
|
|
member_headc(H,Head,0,N,P),
|
|
not_already_present_with_a_different_head(N,R,S,C).
|
|
|
|
|
|
not_already_present_with_a_different_head(_N,_R,_S,[]).
|
|
|
|
|
|
not_already_present_with_a_different_head(N,R,S,[(N1,R,S1)|T]):-
|
|
not_different(N,N1,S,S1),!,
|
|
not_already_present_with_a_different_head(N,R,S,T).
|
|
|
|
not_already_present_with_a_different_head(N,R,S,[(_N1,R1,_S1)|T]):-
|
|
R\==R1,
|
|
not_already_present_with_a_different_head(N,R,S,T).
|
|
|
|
|
|
not_different(_N,_N1,S,S1):-
|
|
S\=S1,!.
|
|
|
|
not_different(N,N1,S,S1):-
|
|
N\=N1,!,
|
|
dif(S,S1).
|
|
|
|
not_different(N,N,S,S).
|
|
|
|
|
|
member_head(H,[(H:_P)|_T],N,N).
|
|
|
|
member_head(H,[(_H:_P)|T],NIn,NOut):-
|
|
N1 is NIn+1,
|
|
member_head(H,T,N1,NOut).
|
|
|
|
member_headc(H,[(H:P)|_T],N,N,P).
|
|
|
|
member_headc(H,[(_H:_P)|T],NIn,NOut,P):-
|
|
N1 is NIn+1,
|
|
member_headc(H,T,N1,NOut,P).
|
|
|
|
|
|
/* choose_clauses(CIn,LC,COut) takes as input the current C set and
|
|
the set of C sets for a negative goal and returns a new C set that
|
|
excludes all the derivations for the negative goals */
|
|
choose_clauses(C,[],C).
|
|
|
|
choose_clauses(CIn,[D|T],COut):-
|
|
member((N,R,S),D),
|
|
already_present_with_a_different_head(N,R,S,CIn),!,
|
|
choose_a_head(N,R,S,CIn,C1),
|
|
choose_clauses(C1,T,COut).
|
|
|
|
|
|
choose_clauses(CIn,[D|T],COut):-
|
|
member((N,R,S),D),
|
|
new_head(N,R,S,N1),
|
|
\+ already_present(N1,R,S,CIn),
|
|
impose_dif_cons(R,S,CIn),
|
|
choose_clauses([(N1,R,S)|CIn],T,COut).
|
|
|
|
choose_clausesc(C,[],C,P,P).
|
|
|
|
choose_clausesc(CIn,[D|T],COut,P0,P1):-
|
|
member((N,R,S),D),
|
|
already_present_with_a_different_head(N,R,S,CIn),!,
|
|
choose_a_headc(N,R,S,CIn,C1,P0,P2),
|
|
choose_clausesc(C1,T,COut,P2,P1).
|
|
|
|
|
|
choose_clausesc(CIn,[D|T],COut,P0,P1):-
|
|
member((N,R,S),D),
|
|
new_head(N,R,S,N1),
|
|
\+ already_present(N1,R,S,CIn),
|
|
impose_dif_cons(R,S,CIn),
|
|
rule_by_num(R,S,_Numbers,Head,_Body),
|
|
nth0(N1, Head, (_H:P), _Rest),
|
|
P2 is P0*P,
|
|
choose_clausesc([(N1,R,S)|CIn],T,COut,P2,P1).
|
|
|
|
|
|
choose_clauses_DB(C,[],C).
|
|
|
|
choose_clauses_DB(CIn,[D|T],COut):-
|
|
member((N,R,S),D),
|
|
ground((N,R,S)),
|
|
already_present_with_a_different_head(N,R,S,CIn),!,
|
|
choose_a_head(N,R,S,CIn,C1),
|
|
choose_clauses_DB(C1,T,COut).
|
|
|
|
choose_clauses_DB(CIn,[D|T],COut):-
|
|
member((N,R,S),D),
|
|
ground((N,R,S)),!,
|
|
new_head(N,R,S,N1),
|
|
\+ already_present(N1,R,S,CIn),
|
|
impose_dif_cons(R,S,CIn),
|
|
choose_clauses_DB([(N1,R,S)|CIn],T,COut).
|
|
|
|
|
|
impose_dif_cons(_R,_S,[]):-!.
|
|
|
|
impose_dif_cons(R,S,[(_NH,R,SH)|T]):-!,
|
|
dif(S,SH),
|
|
impose_dif_cons(R,S,T).
|
|
|
|
impose_dif_cons(R,S,[_H|T]):-
|
|
impose_dif_cons(R,S,T).
|
|
|
|
/* instantiation_present_with_the_same_head(N,R,S,C)
|
|
takes rule R with substitution S and selected head N and a C set
|
|
and asserts dif constraints for all the clauses in C of which RS
|
|
is an instantitation and have the same head selected */
|
|
instantiation_present_with_the_same_head(_N,_R,_S,[]).
|
|
|
|
instantiation_present_with_the_same_head(N,R,S,[(NH,R,SH)|T]):-
|
|
\+ \+ S=SH,!,
|
|
dif_head_or_subs(N,R,S,NH,SH,T).
|
|
|
|
instantiation_present_with_the_same_head(N,R,S,[_H|T]):-
|
|
instantiation_present_with_the_same_head(N,R,S,T).
|
|
|
|
dif_head_or_subs(N,R,S,NH,_SH,T):-
|
|
dif(N,NH),
|
|
instantiation_present_with_the_same_head(N,R,S,T).
|
|
|
|
dif_head_or_subs(N,R,S,N,SH,T):-
|
|
dif(S,SH),
|
|
instantiation_present_with_the_same_head(N,R,S,T).
|
|
|
|
/* case 1 of Select: a more general rule is present in C with
|
|
a different head, instantiate it */
|
|
choose_a_headc(N,R,S,[(NH,R,SH)|T],[(NH,R,SH)|T],P,P):-
|
|
S=SH,
|
|
dif(N,NH).
|
|
|
|
/* case 2 of Select: a more general rule is present in C with
|
|
a different head, ensure that they do not generate the same
|
|
ground clause */
|
|
choose_a_headc(N,R,S,[(NH,R,SH)|T],[(NH,R,S),(NH,R,SH)|T],P0,P1):-
|
|
\+ \+ S=SH, S\==SH,
|
|
dif(N,NH),
|
|
dif(S,SH),
|
|
rule_by_num(R,S,_Numbers,Head,_Body),
|
|
nth0(NH, Head, (_H:P), _Rest),
|
|
P1 is P0*P.
|
|
|
|
choose_a_headc(N,R,S,[H|T],[H|T1],P0,P1):-
|
|
choose_a_headc(N,R,S,T,T1,P0,P1).
|
|
|
|
/* case 1 of Select: a more general rule is present in C with
|
|
a different head, instantiate it */
|
|
choose_a_head(N,R,S,[(NH,R,SH)|T],[(NH,R,SH)|T]):-
|
|
S=SH,
|
|
dif(N,NH).
|
|
|
|
/* case 2 of Select: a more general rule is present in C with
|
|
a different head, ensure that they do not generate the same
|
|
ground clause */
|
|
choose_a_head(N,R,S,[(NH,R,SH)|T],[(NH,R,S),(NH,R,SH)|T]):-
|
|
\+ \+ S=SH, S\==SH,
|
|
dif(N,NH),
|
|
dif(S,SH).
|
|
|
|
choose_a_head(N,R,S,[H|T],[H|T1]):-
|
|
choose_a_head(N,R,S,T,T1).
|
|
|
|
|
|
/* select a head different from N for rule R with
|
|
substitution S, return it in N1 */
|
|
new_head(N,R,S,N1):-
|
|
rule_by_num(R,S,Numbers,Head,_Body),
|
|
Head\=uniform(_,_,_),!,
|
|
nth0(N, Numbers, _Elem, Rest),
|
|
member(N1,Rest).
|
|
|
|
new_head(N,R,S,N1):-
|
|
rule_by_num(R,S,Numbers,uniform(_A:1/Tot,_L,_Number),_Body),
|
|
listN(0,Tot,Numbers),
|
|
nth0(N, Numbers, _Elem, Rest),
|
|
member(N1,Rest).
|
|
|
|
already_present_with_a_different_head(N,R,S,[(NH,R,SH)|_T]):-
|
|
\+ \+ S=SH,NH \= N.
|
|
|
|
already_present_with_a_different_head(N,R,S,[_H|T]):-
|
|
already_present_with_a_different_head(N,R,S,T).
|
|
|
|
|
|
/* checks that a rule R with head N and selection S is already
|
|
present in C (or a generalization of it is in C) */
|
|
already_present(N,R,S,[(N,R,SH)|_T]):-
|
|
S=SH.
|
|
|
|
already_present(N,R,S,[_H|T]):-
|
|
already_present(N,R,S,T).
|
|
|
|
/* rem_dup_lists removes the C sets that are a superset of
|
|
another C sets further on in the list of C sets */
|
|
/* rem_dup_lists removes the C sets that are a superset of
|
|
another C sets further on in the list of C sets */
|
|
rem_dup_lists([],L,L).
|
|
|
|
rem_dup_lists([H|T],L0,L):-
|
|
(member_subset(H,T);member_subset(H,L0)),!,
|
|
rem_dup_lists(T,L0,L).
|
|
|
|
rem_dup_lists([H|T],L0,L):-
|
|
rem_dup_lists(T,[H|L0],L).
|
|
|
|
member_subset(E,[H|_T]):-
|
|
subset_my(H,E),!.
|
|
|
|
member_subset(E,[_H|T]):-
|
|
member_subset(E,T).
|
|
|
|
separate_ulbi([],L,L,U,U,I,I):-!.
|
|
|
|
separate_ulbi([([],H)|T],L0,[H|L1],U0,[H|U1],I0,I1):-
|
|
!,
|
|
separate_ulbi(T,L0,L1,U0,U1,I0,I1).
|
|
|
|
separate_ulbi([(G,H)|T],L0,L1,U0,[H1|U1],I0,[(G,H)|I1]):-
|
|
get_ground(H,H1),
|
|
separate_ulbi(T,L0,L1,U0,U1,I0,I1).
|
|
|
|
|
|
separate_ulb([],L,L,U,U):-!.
|
|
|
|
separate_ulb([H|T],L0,[H|L1],U0,[H|U1]):-
|
|
ground(H),!,
|
|
separate_ulb(T,L0,L1,U0,U1).
|
|
|
|
separate_ulb([H|T],L0,L1,U0,[H1|U1]):-
|
|
get_ground(H,H1),
|
|
separate_ulb(T,L0,L1,U0,U1).
|
|
|
|
|
|
separate_ulbc([],L,L,P,P):-!.
|
|
|
|
separate_ulbc([(_H,P,true)|T],L0,L1,P0,P1):-!,
|
|
P2 is P0+P,
|
|
separate_ulbc(T,L0,L1,P2,P1).
|
|
|
|
separate_ulbc([(H,_P,false)|T],L0,[H|L1],P0,P1):-
|
|
separate_ulbc(T,L0,L1,P0,P1).
|
|
|
|
get_ground([],[]):-!.
|
|
|
|
get_ground([H|T],[H|T1]):-
|
|
ground(H),!,
|
|
get_ground(T,T1).
|
|
|
|
get_ground([_H|T],T1):-
|
|
get_ground(T,T1).
|
|
|
|
|
|
/* predicates for building the formula to be converted into a BDD */
|
|
|
|
/* build_formula(LC,Formula,VarIn,VarOut) takes as input a set of C sets
|
|
LC and a list of Variables VarIn and returns the formula and a new list
|
|
of variables VarOut
|
|
Formula is of the form [Term1,...,Termn]
|
|
Termi is of the form [Factor1,...,Factorm]
|
|
Factorj is of the form (Var,Value) where Var is the index of
|
|
the multivalued variable Var and Value is the index of the value
|
|
*/
|
|
build_formula([],[],Var,Var,C,C).
|
|
|
|
build_formula([D|TD],[F|TF],VarIn,VarOut,C0,C1):-
|
|
length(D,NC),
|
|
C2 is C0+NC,
|
|
build_term(D,F,VarIn,Var1),
|
|
build_formula(TD,TF,Var1,VarOut,C2,C1).
|
|
|
|
build_formula([],[],Var,Var).
|
|
|
|
build_formula([D|TD],[F|TF],VarIn,VarOut):-
|
|
build_term(D,F,VarIn,Var1),
|
|
build_formula(TD,TF,Var1,VarOut).
|
|
|
|
|
|
build_term([],[],Var,Var).
|
|
|
|
build_term([(_,pruned,_)|TC],TF,VarIn,VarOut):-!,
|
|
build_term(TC,TF,VarIn,VarOut).
|
|
|
|
build_term([(N,R,S)|TC],[[NVar,N]|TF],VarIn,VarOut):-
|
|
(nth0_eq(0,NVar,VarIn,(R,S))->
|
|
Var1=VarIn
|
|
;
|
|
append(VarIn,[(R,S)],Var1),
|
|
length(VarIn,NVar)
|
|
),
|
|
build_term(TC,TF,Var1,VarOut).
|
|
|
|
/* nth0_eq(PosIn,PosOut,List,El) takes as input a List,
|
|
an element El and an initial position PosIn and returns in PosOut
|
|
the position in the List that contains an element exactly equal to El
|
|
*/
|
|
nth0_eq(N,N,[H|_T],El):-
|
|
H==El,!.
|
|
|
|
nth0_eq(NIn,NOut,[_H|T],El):-
|
|
N1 is NIn+1,
|
|
nth0_eq(N1,NOut,T,El).
|
|
|
|
/* var2numbers converts a list of couples (Rule,Substitution) into a list
|
|
of triples (N,NumberOfHeadsAtoms,ListOfProbabilities), where N is an integer
|
|
starting from 0 */
|
|
var2numbers([],_N,[]).
|
|
|
|
var2numbers([(R,S)|T],N,[[N,ValNumber,Probs]|TNV]):-
|
|
find_probs(R,S,Probs),
|
|
length(Probs,ValNumber),
|
|
N1 is N+1,
|
|
var2numbers(T,N1,TNV).
|
|
|
|
find_probs(R,S,Probs):-
|
|
rule_by_num(R,S,_N,Head,_Body),
|
|
get_probs(Head,Probs).
|
|
|
|
get_probs(uniform(_A:1/Num,_P,_Number),ListP):-
|
|
Prob is 1/Num,
|
|
list_el(Num,Prob,ListP).
|
|
|
|
get_probs([],[]).
|
|
|
|
get_probs([_H:P|T],[P1|T1]):-
|
|
P1 is P,
|
|
get_probs(T,T1).
|
|
|
|
list_el(0,_P,[]):-!.
|
|
|
|
list_el(N,P,[P|T]):-
|
|
N1 is N-1,
|
|
list_el(N1,P,T).
|
|
|
|
/* end of predicates for building the formula to be converted into a BDD */list_el(0,_P,[]):-!.
|
|
|
|
|
|
/* start of predicates for parsing an input file containing a program */
|
|
|
|
/* p(File) parses the file File.cpl. It can be called more than once without
|
|
exiting yap */
|
|
p(File):-
|
|
parse(File).
|
|
|
|
parse(File):-
|
|
atom_concat(File,'.cpl',FilePl),
|
|
open(FilePl,read,S),
|
|
read_clauses(S,C),
|
|
close(S),
|
|
retractall(rule_by_num(_,_,_,_,_)),
|
|
retractall(rule(_,_,_,_,_,_,_,_)),
|
|
retractall(def_rule(_,_)),
|
|
retractall(rule_uniform(_,_,_,_,_,_,_,_)),
|
|
process_clauses(C,1).
|
|
|
|
process_clauses([(end_of_file,[])],_N):-!.
|
|
|
|
process_clauses([((H:-B),V)|T],N):-
|
|
H=uniform(A,P,L),!,
|
|
list2and(BL,B),
|
|
process_body(BL,V,V1),
|
|
remove_vars([P],V1,V2),
|
|
append(BL,[length(L,Tot),nth0(Number,L,P)],BL1),
|
|
append(V2,['Tot'=Tot],V3),
|
|
assertz(rule_by_num(N,V3,_NH,uniform(A:1/Tot,L,Number),BL1)),
|
|
assertz(rule_uniform(A,N,V3,_NH,1/Tot,L,Number,BL1)),
|
|
N1 is N+1,
|
|
process_clauses(T,N1).
|
|
|
|
process_clauses([((H:-B),V)|T],N):-
|
|
H=(_;_),!,
|
|
list2or(HL1,H),
|
|
process_head(HL1,HL),
|
|
list2and(BL,B),
|
|
process_body(BL,V,V1),
|
|
length(HL,LH),
|
|
listN(0,LH,NH),
|
|
assert_rules(HL,0,HL,BL,NH,N,V1),
|
|
assertz(rule_by_num(N,V1,NH,HL,BL)),
|
|
N1 is N+1,
|
|
process_clauses(T,N1).
|
|
|
|
process_clauses([((H:-B),V)|T],N):-
|
|
H=(_:_),!,
|
|
list2or(HL1,H),
|
|
process_head(HL1,HL),
|
|
list2and(BL,B),
|
|
process_body(BL,V,V1),
|
|
length(HL,LH),
|
|
listN(0,LH,NH),
|
|
assert_rules(HL,0,HL,BL,NH,N,V1),
|
|
assertz(rule_by_num(N,V1,NH,HL,BL)),
|
|
N1 is N+1,
|
|
process_clauses(T,N1).
|
|
|
|
process_clauses([((H:-B),_V)|T],N):-!,
|
|
list2and(BL,B),
|
|
assert(def_rule(H,BL)),
|
|
process_clauses(T,N).
|
|
|
|
process_clauses([(H,V)|T],N):-
|
|
H=(_;_),!,
|
|
list2or(HL1,H),
|
|
process_head(HL1,HL),
|
|
length(HL,LH),
|
|
listN(0,LH,NH),
|
|
assert_rules(HL,0,HL,[],NH,N,V),
|
|
assertz(rule_by_num(N,V,NH,HL,[])),
|
|
N1 is N+1,
|
|
process_clauses(T,N1).
|
|
|
|
process_clauses([(H,V)|T],N):-
|
|
H=(_:_),!,
|
|
list2or(HL1,H),
|
|
process_head(HL1,HL),
|
|
length(HL,LH),
|
|
listN(0,LH,NH),
|
|
assert_rules(HL,0,HL,[],NH,N,V),
|
|
assertz(rule_by_num(N,V,NH,HL,[])),
|
|
N1 is N+1,
|
|
process_clauses(T,N1).
|
|
|
|
process_clauses([(H,_V)|T],N):-
|
|
assert(def_rule(H,[])),
|
|
process_clauses(T,N).
|
|
|
|
assert_rules([],_Pos,_HL,_BL,_Nh,_N,_V1):-!.
|
|
|
|
assert_rules(['':_P],_Pos,_HL,_BL,_Nh,_N,_V1):-!.
|
|
|
|
assert_rules([H:P|T],Pos,HL,BL,NH,N,V1):-
|
|
assertz(rule(H,P,Pos,N,V1,NH,HL,BL)),
|
|
Pos1 is Pos+1,
|
|
assert_rules(T,Pos1,HL,BL,NH,N,V1).
|
|
|
|
|
|
/* if the annotation in the head are not ground, the null atom is not added
|
|
and the eventual formulas are not evaluated */
|
|
|
|
process_head(HL,NHL):-
|
|
(ground_prob(HL)->
|
|
process_head_ground(HL,0,NHL)
|
|
;
|
|
NHL=HL
|
|
).
|
|
|
|
ground_prob([]).
|
|
|
|
ground_prob([_H:PH|T]):-
|
|
ground(PH),
|
|
ground_prob(T).
|
|
|
|
process_head_ground([H:PH],P,[H:PH1|Null]):-
|
|
PH1 is PH,
|
|
PNull is 1-P-PH1,
|
|
setting(epsilon_parsing,Eps),
|
|
EpsNeg is - Eps,
|
|
PNull > EpsNeg,
|
|
(PNull>Eps->
|
|
Null=['':PNull]
|
|
;
|
|
Null=[]
|
|
).
|
|
|
|
process_head_ground([H:PH|T],P,[H:PH1|NT]):-
|
|
PH1 is PH,
|
|
P1 is P+PH1,
|
|
process_head_ground(T,P1,NT).
|
|
|
|
/* setof must have a goal of the form B^G where B is a term containing the existential variables */
|
|
process_body([],V,V).
|
|
|
|
process_body([setof(A,B^_G,_L)|T],VIn,VOut):-!,
|
|
get_var(A,VA),
|
|
get_var(B,VB),
|
|
remove_vars(VA,VIn,V1),
|
|
remove_vars(VB,V1,V2),
|
|
process_body(T,V2,VOut).
|
|
|
|
process_body([setof(A,_G,_L)|T],VIn,VOut):-!,
|
|
get_var(A,VA),
|
|
remove_vars(VA,VIn,V1),
|
|
process_body(T,V1,VOut).
|
|
|
|
process_body([bagof(A,B^_G,_L)|T],VIn,VOut):-!,
|
|
get_var(A,VA),
|
|
get_var(B,VB),
|
|
remove_vars(VA,VIn,V1),
|
|
remove_vars(VB,V1,V2),
|
|
process_body(T,V2,VOut).
|
|
|
|
process_body([bagof(A,_G,_L)|T],VIn,VOut):-!,
|
|
get_var(A,VA),
|
|
remove_vars(VA,VIn,V1),
|
|
process_body(T,V1,VOut).
|
|
|
|
process_body([_H|T],VIn,VOut):-!,
|
|
process_body(T,VIn,VOut).
|
|
|
|
get_var_list([],[]).
|
|
|
|
get_var_list([H|T],[H|T1]):-
|
|
var(H),!,
|
|
get_var_list(T,T1).
|
|
|
|
get_var_list([H|T],VarOut):-!,
|
|
get_var(H,Var),
|
|
append(Var,T1,VarOut),
|
|
get_var_list(T,T1).
|
|
|
|
get_var(A,[A]):-
|
|
var(A),!.
|
|
|
|
get_var(A,V):-
|
|
A=..[_F|Args],
|
|
get_var_list(Args,V).
|
|
|
|
remove_vars([],V,V).
|
|
|
|
remove_vars([H|T],VIn,VOut):-
|
|
delete_var(H,VIn,V1),
|
|
remove_vars(T,V1,VOut).
|
|
|
|
delete_var(_H,[],[]).
|
|
|
|
delete_var(V,[VN=Var|T],[VN=Var|T1]):-
|
|
V\==Var,!,
|
|
delete_var(V,T,T1).
|
|
|
|
delete_var(_V,[_H|T],T).
|
|
|
|
/* predicates for reading in the program clauses */
|
|
read_clauses(S,Clauses):-
|
|
(setting(ground_body,true)->
|
|
read_clauses_ground_body(S,Clauses)
|
|
;
|
|
read_clauses_exist_body(S,Clauses)
|
|
).
|
|
|
|
|
|
read_clauses_ground_body(S,[(Cl,V)|Out]):-
|
|
read_term(S,Cl,[variable_names(V)]),
|
|
(Cl=end_of_file->
|
|
Out=[]
|
|
;
|
|
read_clauses_ground_body(S,Out)
|
|
).
|
|
|
|
|
|
read_clauses_exist_body(S,[(Cl,V)|Out]):-
|
|
read_term(S,Cl,[variable_names(VN)]),
|
|
extract_vars_cl(Cl,VN,V),
|
|
(Cl=end_of_file->
|
|
Out=[]
|
|
;
|
|
read_clauses_exist_body(S,Out)
|
|
).
|
|
|
|
|
|
extract_vars_cl(end_of_file,[]).
|
|
|
|
extract_vars_cl(Cl,VN,Couples):-
|
|
(Cl=(H:-_B)->
|
|
true
|
|
;
|
|
H=Cl
|
|
),
|
|
extract_vars(H,[],V),
|
|
pair(VN,V,Couples).
|
|
|
|
|
|
pair(_VN,[],[]).
|
|
|
|
pair([VN= _V|TVN],[V|TV],[VN=V|T]):-
|
|
pair(TVN,TV,T).
|
|
|
|
|
|
extract_vars(Var,V0,V):-
|
|
var(Var),!,
|
|
(member_eq(Var,V0)->
|
|
V=V0
|
|
;
|
|
append(V0,[Var],V)
|
|
).
|
|
|
|
extract_vars(Term,V0,V):-
|
|
Term=..[_F|Args],
|
|
extract_vars_list(Args,V0,V).
|
|
|
|
|
|
extract_vars_list([],V,V).
|
|
|
|
extract_vars_list([Term|T],V0,V):-
|
|
extract_vars(Term,V0,V1),
|
|
extract_vars_list(T,V1,V).
|
|
|
|
|
|
listN(N,N,[]):-!.
|
|
|
|
listN(NIn,N,[NIn|T]):-
|
|
N1 is NIn+1,
|
|
listN(N1,N,T).
|
|
/* end of predicates for parsing an input file containing a program */
|
|
|
|
/* start of utility predicates */
|
|
list2or([X],X):-
|
|
X\=;(_,_),!.
|
|
|
|
list2or([H|T],(H ; Ta)):-!,
|
|
list2or(T,Ta).
|
|
|
|
list2and([X],X):-
|
|
X\=(_,_),!.
|
|
|
|
list2and([H|T],(H,Ta)):-!,
|
|
list2and(T,Ta).
|
|
|
|
member_eq(A,[H|_T]):-
|
|
A==H,!.
|
|
|
|
member_eq(A,[_H|T]):-
|
|
member_eq(A,T).
|
|
|
|
subset_my([],_).
|
|
|
|
subset_my([H|T],L):-
|
|
member_eq(H,L),
|
|
subset_my(T,L).
|
|
|
|
remove_duplicates_eq([],[]).
|
|
|
|
remove_duplicates_eq([H|T],T1):-
|
|
member_eq(H,T),!,
|
|
remove_duplicates_eq(T,T1).
|
|
|
|
remove_duplicates_eq([H|T],[H|T1]):-
|
|
remove_duplicates_eq(T,T1).
|
|
|
|
builtin(_A is _B).
|
|
builtin(_A > _B).
|
|
builtin(_A < _B).
|
|
builtin(_A >= _B).
|
|
builtin(_A =< _B).
|
|
builtin(_A =:= _B).
|
|
builtin(_A =\= _B).
|
|
builtin(true).
|
|
builtin(false).
|
|
builtin(_A = _B).
|
|
builtin(_A==_B).
|
|
builtin(_A\=_B).
|
|
builtin(_A\==_B).
|
|
builtin(length(_L,_N)).
|
|
builtin(member(_El,_L)).
|
|
builtin(average(_L,_Av)).
|
|
builtin(max_list(_L,_Max)).
|
|
builtin(min_list(_L,_Max)).
|
|
builtin(nth0(_,_,_)).
|
|
builtin(nth(_,_,_)).
|
|
average(L,Av):-
|
|
sum_list(L,Sum),
|
|
length(L,N),
|
|
Av is Sum/N.
|
|
|
|
clique(Graph,Clique):-
|
|
vertices(Graph,Candidates),
|
|
extend_cycle(Graph,Candidates,[],[],Clique).
|
|
|
|
extend_cycle(G,[H|T],Not,CS,CSOut):-
|
|
neighbours(H, G, Neigh),
|
|
intersection(Neigh,T,NewCand),
|
|
intersection(Neigh,Not,NewNot),
|
|
extend(G,NewCand,NewNot,[H|CS],CSOut).
|
|
|
|
extend_cycle(G,[H|T],Not,CS,CSOut):-
|
|
extend_cycle(G,T,[H|Not],CS,CSOut).
|
|
|
|
extend(_G,[],[],CompSub,CompSub):-!.
|
|
|
|
extend(G,Cand,Not,CS,CSOut):-
|
|
extend_cycle(G,Cand,Not,CS,CSOut).
|
|
|
|
/* set(Par,Value) can be used to set the value of a parameter */
|
|
set(Parameter,Value):-
|
|
retract(setting(Parameter,_)),
|
|
assert(setting(Parameter,Value)).
|
|
|
|
/* end of utility predicates */
|