add ProbLog to YAP distribution

This commit is contained in:
Vitor Santos Costa 2009-02-10 23:57:45 +00:00
parent 9a0d481528
commit 76971fa724
19 changed files with 6984 additions and 0 deletions

14
ProbLog/Makefile.in Normal file
View File

@ -0,0 +1,14 @@
default:
@(cd simplecudd; \
echo Making simplecudd...; \
make)
pwd
cp simplecudd/ProblogBDD .
clean:
@(cd simplecudd; \
echo Cleaning simplecudd...; \
make clean; \
cd ..)
rm -rf ProblogBDD output queries

7
ProbLog/README Normal file
View File

@ -0,0 +1,7 @@
To compile ProbLog call
make
To clean the directory call
make clean
The make file will recursively call the make file of SimpleCudd and Cudd.
And it will finally copy the binary executable ProblogBDD to the main directory.

86
ProbLog/examples/graph.pl Normal file
View File

@ -0,0 +1,86 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% ProbLog program describing a probabilistic graph
% (running example from ProbLog presentations)
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
:- use_module('../problog').
%%%%
% background knowledge
%%%%
% definition of acyclic path using list of visited nodes
path(X,Y) :- path(X,Y,[X],_).
path(X,X,A,A).
path(X,Y,A,R) :-
X\==Y,
edge(X,Z),
absent(Z,A),
path(Z,Y,[Z|A],R).
% using directed edges in both directions
edge(X,Y) :- dir_edge(Y,X).
edge(X,Y) :- dir_edge(X,Y).
% checking whether node hasn't been visited before
absent(_,[]).
absent(X,[Y|Z]):-X \= Y, absent(X,Z).
%%%%
% probabilistic facts
%%%%
0.9::dir_edge(1,2).
0.8::dir_edge(2,3).
0.6::dir_edge(3,4).
0.7::dir_edge(1,6).
0.5::dir_edge(2,6).
0.4::dir_edge(6,5).
0.7::dir_edge(5,3).
0.2::dir_edge(5,4).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% example queries about path(1,4)
%
%%% explanation probability (and facts involved)
% ?- problog_max(path(1,4),Prob,FactsUsed).
% FactsUsed = [dir_edge(1,2),dir_edge(2,3),dir_edge(3,4)],
% Prob = 0.432 ?
% yes
%%% success probability
% ?- problog_exact(path(1,4),Prob,Status).
% 8 proofs
% Prob = 0.53864,
% Status = ok ?
% yes
%%% lower bound using 4 best proofs
% ?- problog_kbest(path(1,4),4,Prob,Status).
% 4 proofs
% Prob = 0.517344,
% Status = ok ?
% yes
%%% approximation using monte carlo, to reach 95%-confidence interval width 0.01
% ?- problog_montecarlo(path(1,4),0.01,Prob).
% Prob = 0.537525 ?
% yes
%%% upper and lower bound using iterative deepening, final interval width 0.01
% ?- problog_delta(path(1,4),0.01,Bound_low,Bound_up,Status).
% Bound_low = 0.5354096,
% Bound_up = 0.53864,
% Status = ok ?
% yes
%%% upper and lower bound obtained cutting the sld tree at probability 0.1 for each branch
% ?- problog_threshold(path(1,4),0.1,Bound_low,Bound_up,Status).
% 4 proofs
% Bound_low = 0.517344,
% Bound_up = 0.563728,
% Status = ok ?
% yes
%%% lower bound obtained cutting the sld tree at probability 0.2 for each branch
% ?- problog_low(path(1,4),0.2,Bound_low,Status).
% 1 proofs
% Bound_low = 0.432,
% Status = ok ?
% yes
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

View File

@ -0,0 +1,96 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% ProbLog program describing a probabilistic graph
% (running example from ProbLog presentations)
%
% example for parameter learning with LeProbLog
%
% training and test examples are included at the end of the file
%
% query ?- do_learning(20).
% will run 20 iterations of learning with default settings
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
:- use_module('../learning').
%%%%
% background knowledge
%%%%
% definition of acyclic path using list of visited nodes
path(X,Y) :- path(X,Y,[X],_).
path(X,X,A,A).
path(X,Y,A,R) :-
X\==Y,
edge(X,Z),
absent(Z,A),
path(Z,Y,[Z|A],R).
% using directed edges in both directions
edge(X,Y) :- dir_edge(Y,X).
edge(X,Y) :- dir_edge(X,Y).
% checking whether node hasn't been visited before
absent(_,[]).
absent(X,[Y|Z]):-X \= Y, absent(X,Z).
%%%%
% probabilistic facts
% - probability represented by t/1 term means learnable parameter
% - argument of t/1 is real value (used to compare against in evaluation when known), use t(_) if unknown
%%%%
t(0.9)::dir_edge(1,2).
t(0.8)::dir_edge(2,3).
t(0.6)::dir_edge(3,4).
t(0.7)::dir_edge(1,6).
t(0.5)::dir_edge(2,6).
t(0.4)::dir_edge(6,5).
t(0.7)::dir_edge(5,3).
t(0.2)::dir_edge(5,4).
%%%%%%%%%%%%%%
% training examples of form example(ID,Query,DesiredProbability)
%%%%%%%%%%%%%%
example(1,path(1,2),0.94).
example(2,path(1,3),0.81).
example(3,path(1,4),0.54).
example(4,path(1,5),0.70).
example(5,path(1,6),0.87).
example(6,path(2,3),0.85).
example(7,path(2,4),0.57).
example(8,path(2,5),0.72).
example(9,path(2,6),0.86).
example(10,path(3,4),0.66).
example(11,path(3,5),0.80).
example(12,path(3,6),0.75).
example(13,path(4,5),0.57).
example(14,path(4,6),0.51).
example(15,path(5,6),0.69).
% some examples for learning from proofs:
example(16,(dir_edge(2,3),dir_edge(2,6),dir_edge(6,5),dir_edge(5,4)),0.032).
example(17,(dir_edge(1,6),dir_edge(2,6),dir_edge(2,3),dir_edge(3,4)),0.168).
example(18,(dir_edge(5,3),dir_edge(5,4)),0.14).
example(19,(dir_edge(2,6),dir_edge(6,5)),0.2).
example(20,(dir_edge(1,2),dir_edge(2,3),dir_edge(3,4)),0.432).
%%%%%%%%%%%%%%
% test examples of form test_example(ID,Query,DesiredProbability)
% note: ID namespace is shared with training example IDs
%%%%%%%%%%%%%%
test_example(21,path(2,1),0.94).
test_example(22,path(3,1),0.81).
test_example(23,path(4,1),0.54).
test_example(24,path(5,1),0.70).
test_example(25,path(6,1),0.87).
test_example(26,path(3,2),0.85).
test_example(27,path(4,2),0.57).
test_example(28,path(5,2),0.72).
test_example(29,path(6,2),0.86).
test_example(30,path(4,3),0.66).
test_example(31,path(5,3),0.80).
test_example(32,path(6,3),0.75).
test_example(33,path(5,4),0.57).
test_example(34,path(6,4),0.51).
test_example(35,path(6,5),0.69).

1147
ProbLog/learning.yap Normal file

File diff suppressed because it is too large Load Diff

311
ProbLog/learning/logger.yap Normal file
View File

@ -0,0 +1,311 @@
%%% -*- Mode: Prolog; -*-
:- module(logger,[logger_define_variable/2,
logger_define_variables/2,
logger_set_filename/1,
logger_set_delimiter/1,
logger_set_variable/2,
logger_set_variable_again/2,
logger_get_variable/2,
logger_start_timer/1,
logger_stop_timer/1,
logger_write_data/0,
logger_write_header/0]).
:- use_module(library(system),[datime/1,mktime/2]).
:- use_module(library(lists),[append/3,member/2]).
:- yap_flag(unknown,error).
:- style_check(single_var).
:- bb_put(logger_filename,'out.dat').
:- bb_put(logger_delimiter,';').
:- bb_put(logger_variables,[]).
%========================================================================
%= Defines a new variable, possible types are: int, float and time
%=
%= +Name, +Type
%========================================================================
logger_define_variable(Name,int) :-
!,
is_variable_already_defined(Name),
bb_delete(logger_variables,OldVariables),
append(OldVariables,[(Name,int)],NewVariables),
bb_put(logger_variables,NewVariables),
atom_concat(logger_data_,Name,Key),
bb_put(Key,null).
logger_define_variable(Name,float) :-
!,
is_variable_already_defined(Name),
bb_delete(logger_variables,OldVariables),
append(OldVariables,[(Name,float)],NewVariables),
bb_put(logger_variables,NewVariables),
atom_concat(logger_data_,Name,Key),
bb_put(Key,null).
logger_define_variable(Name,time) :-
!,
is_variable_already_defined(Name),
bb_delete(logger_variables,OldVariables),
append(OldVariables,[(Name,time)],NewVariables),
bb_put(logger_variables,NewVariables),
atom_concat(logger_data_,Name,Key),
atom_concat(logger_start_time_,Name,Key2),
bb_put(Key,null),
bb_put(Key2,null).
logger_define_variable(Name,Unknown) :-
is_variable_already_defined(Name),
write('logger_define_variable, unknown type '),
write(Unknown),
write(' for variable '),
write(Name),
nl,
fail.
is_variable_already_defined(Name) :-
bb_get(logger_variables,Variables),
member((Name,_),Variables),!,
write('logger_define_variable, Variable '),
write(Name),
write(' is already defined!\n'),
fail;
true.
%========================================================================
%=
%=
%= +ListOfNames, +Type
%========================================================================
logger_define_variables([],_).
logger_define_variables([H|T],Type) :-
logger_define_variable(H,Type),
logger_define_variables(T,Type).
%========================================================================
%= Set the filename, to which the output should be appended
%=
%= +Name
%========================================================================
logger_set_filename(Name) :-
bb_put(logger_filename,Name).
%========================================================================
%= Set the delimiter for the fields
%=
%= +Delimiter
%========================================================================
logger_set_delimiter(Delimiter) :-
bb_put(logger_delimiter,Delimiter).
%========================================================================
%= Set the value of the variable name. If the value is already set or
%= if the variable does not exists, an error will be displayed and the
%= Prolog will be halted.
%=
%= +Name, +Value
%========================================================================
logger_set_variable(Name,Value) :-
atom_concat(logger_data_,Name,Key),
(
bb_get(Key,null)
->
(
bb_put(Key,Value)
);(
bb_get(Key,_)
->
(
write('logger_set_variable, Variable '),
write(Name),
write(' is already set'),
nl,
fail
) ; (
write('logger_set_variable, unknown variable '),
write(Name),
nl,
fail
)
)
),!.
%========================================================================
%= Set the value of the variable name. If the value is already set or
%= the old value is overwritten. If the variable does not exists, an
%= error will be displayed and the Prolog will be halted.
%=
%= +Name, +Value
%========================================================================
logger_set_variable_again(Name,Value) :-
atom_concat(logger_data_,Name,Key),
(
bb_get(Key,_)
->
(
bb_put(Key,Value)
);(
write('logger_set_variable, unknown variable '),
write(Name),
nl,
fail
)
),!.
logger_variable_is_set(Name) :-
atom_concat(logger_data_,Name,Key),
bb_get(Key,X),
X \= null.
%========================================================================
%= Get the value of the variable name. If the value is not yet set or
%= if the variable does not exists, an error will be displayed and the
%= Prolog will be halted.
%=
%= +Name, +Value
%========================================================================
logger_get_variable(Name,Value) :-
atom_concat(logger_data_,Name,Key),
(
bb_get(Key,null)
->
(
write('logger_get_variable, Variable '),
write(Name),
write(' is not yet set'),
nl,
fail
);(
bb_get(Key,Value)
;
(
write('logger_set_variable, unknown variable '),
write(Name),
nl,
fail
)
)
),!.
%========================================================================
%=
%=
%= +Name
%========================================================================
logger_start_timer(Name) :-
atom_concat(logger_start_time_,Name,Key),
(
bb_get(Key,null)
->
(
statistics(walltime,[StartTime,_]),
bb_put(Key,StartTime)
);(
bb_get(Key,_)
->
(
write('logger_start_timer, timer '),
write(Name),
write(' is already started'),
nl,
fail
);(
write('logger_start_timer, timer '),
write(Name),
write(' is not defined'),
nl,
fail
)
)
),!.
logger_stop_timer(Name) :-
atom_concat(logger_start_time_,Name,Key),
bb_delete(Key,StartTime),
statistics(walltime,[StopTime,_]),
bb_put(Key,null),
Duration is StopTime-StartTime,
(
logger_variable_is_set(Name)
->
(
logger_get_variable(Name,OldDuration),
NewDuration is Duration+OldDuration,
logger_set_variable_again(Name,NewDuration)
); logger_set_variable(Name,Duration)
),!.
%========================================================================
%= write a new line to the log file, which contains all the
%= values of the variables. afterwards, reset all variables to null.
%=
%========================================================================
logger_write_data :-
bb_get(logger_filename,FName),
bb_get(logger_variables,Variables),
open(FName,'append',Handle),
logger_write_data_intern(Variables,Handle),
close(Handle),
% reset variables
findall(_,(member((Name,_),Variables),atom_concat(logger_data_,Name,Key),bb_put(Key,null)),_),
findall(_,(member((Name,time),Variables),atom_concat(logger_start_time_,Name,Key2),bb_put(Key2,null)),_).
logger_write_data_intern([],_).
logger_write_data_intern([(Name,_Type)],Handle) :-
variablevalue_with_nullcheck(Name,Value),
write(Handle,Value),
write(Handle,'\n').
logger_write_data_intern([(Name,_Type),Next|T],Handle) :-
variablevalue_with_nullcheck(Name,Value),
bb_get(logger_delimiter,D),
write(Handle,Value),
write(Handle,D),
logger_write_data_intern([Next|T],Handle).
variablevalue_with_nullcheck(Name,Result) :-
atom_concat(logger_data_,Name,Key),
bb_get(Key,Value),
(
Value=null
->
Result = '' ;
Result=Value
).
%========================================================================
%=
%=
%=
%========================================================================
logger_write_header :-
bb_get(logger_filename,FName),
bb_get(logger_variables,Variables),
open(FName,'append',Handle),
write(Handle,'# '),
logger_write_header_intern(Variables,Handle),
write(Handle,'\n'),
close(Handle).
logger_write_header_intern([],_).
logger_write_header_intern([(Name,_Type)],Handle) :-
write(Handle,Name).
logger_write_header_intern([(Name,_Type),Next|T],Handle) :-
bb_get(logger_delimiter,D),
write(Handle,Name),
write(Handle,D),
logger_write_header_intern([Next|T],Handle).

958
ProbLog/problog.yap Normal file
View File

@ -0,0 +1,958 @@
%%% -*- Mode: Prolog; -*-
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% ProbLog inference
%
% assumes probabilistic facts as Prob::Fact and clauses in normal Prolog format
%
% provides following inference modes (16/12/2008):
% - approximation with interval width Delta (IJCAI07): problog_delta(+Query,+Delta,-Low,-High,-Status)
% - bounds based on single probability threshold: problog_threshold(+Query,+Threshold,-Low,-High,-Status)
% - as above, but lower bound only: problog_low(+Query,+Threshold,-Low,-Status)
% - lower bound based on K most likely proofs: problog_kbest(+Query,+K,-Low,-Status)
% - explanation probability (ECML07): problog_max(+Query,-Prob,-FactsUsed)
% - exact probability: problog_exact(+Query,-Prob,-Status)
% - sampling: problog_montecarlo(+Query,+Delta,-Prob)
%
%
% angelika.kimmig@cs.kuleuven.be
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
:- module(problog, [problog_delta/5,
problog_threshold/5,
problog_low/4,
problog_kbest/4,
problog_kbest_save/6,
problog_max/3,
problog_exact/3,
problog_montecarlo/3,
get_fact_probability/2,
set_fact_probability/2,
get_fact/2,
tunable_fact/2,
export_facts/1,
problog_help/0,
problog_dir/1,
set_problog_flag/2,
problog_flag/2,
problog_flags/0]).
:- style_check(all).
:- yap_flag(unknown,error).
% problog related modules
:- use_module('problog/flags',[set_problog_flag/2,
problog_flag/2,
problog_flags/0]).
:- use_module('problog/print', [print_sep_line/0,
print_inference/2]).
:- use_module('problog/tptree',[init_ptree/1,
delete_ptree/1,
insert_ptree/2,
count_ptree/2,
prune_check_ptree/2,
merge_ptree/3,
bdd_ptree_map/4,
bdd_ptree/3]).
% general yap modules
:- ensure_loaded(library(lists)).
:- ensure_loaded(library(terms)).
:- ensure_loaded(library(random)).
:- ensure_loaded(library(system)).
:- ensure_loaded(library(rbtrees)).
% op attaching probabilities to facts
:- op( 550, yfx, :: ).
%%%%%%%%%%%%%%%%%%%%%%%%
% control predicates on various levels
%%%%%%%%%%%%%%%%%%%%%%%%
% global over all inference methods, internal use only
:- dynamic problog_predicate/2.
% global over all inference methods, exported
:- dynamic tunable_fact/2.
:- dynamic problog_dir/1.
% global, manipulated via problog_control/2
:- dynamic up/0.
:- dynamic limit/0.
:- dynamic mc/0.
:- dynamic remember/0.
% local to problog_delta
:- dynamic low/2.
:- dynamic up/2.
:- dynamic stopDiff/1.
% local to problog_kbest
:- dynamic current_kbest/3.
% local to problog_max
:- dynamic max_probability/1.
:- dynamic max_proof/1.
% local to problog_montecarlo
:- dynamic mc_prob/1.
% directory where ProblogBDD executable is located
% automatically set during loading -- assumes it is in same place as this file (problog.yap)
:- getcwd(PD),retractall(problog_dir(_)),assert(problog_dir(PD)).
%%%%%%%%%%%%%%%%%%%%%%%%
% help
%%%%%%%%%%%%%%%%%%%%%%%%
problog_help :-
format('~2nProbLog inference currently offers the following inference methods:~n',[]),
show_inference,
format('~2nThe following global parameters are available:~n',[]),
problog_flags,
print_sep_line,
format('~n use problog_help/0 to display this information~n',[]),
format('~n use problog_flags/0 to display current parameter values~2n',[]),
print_sep_line,
nl,
flush_output.
show_inference :-
format('~n',[]),
print_sep_line,
print_inference(call,description),
print_sep_line,
print_inference('problog_delta(+Query,+Delta,-Low,-High,-Status)','approximation with interval width Delta (IJCAI07)'),
print_inference('problog_threshold(+Query,+Threshold,-Low,-High,-Status)','bounds based on single probability threshold'),
print_inference('problog_low(+Query,+Threshold,-Low,-Status)','lower bound based on single probability threshold'),
print_inference('problog_kbest(+Query,+K,-Low,-Status)','lower bound based on K most likely proofs'),
print_inference('problog_max(+Query,-Prob,-FactsUsed)','explanation probability (ECML07)'),
print_inference('problog_exact(+Query,-Prob,-Status)','exact probability'),
print_inference('problog_montecarlo(+Query,+Delta,-Prob)','sampling with 95\%-confidence-interval-width Delta'),
print_sep_line.
%%%%%%%%%%%%%%%%%%%%%%%%
% initialization of global parameters
%%%%%%%%%%%%%%%%%%%%%%%%
init_global_params :-
set_problog_flag(bdd_time,60),
set_problog_flag(first_threshold,0.1),
L is 10**(-30),
set_problog_flag(last_threshold,L),
set_problog_flag(id_stepsize,0.5),
set_problog_flag(prunecheck,off),
set_problog_flag(maxsteps,1000),
set_problog_flag(mc_batchsize,1000),
set_problog_flag(mc_logfile,'log.txt'),
set_problog_flag(bdd_file,example_bdd),
set_problog_flag(dir,output),
set_problog_flag(save_bdd,false),
% problog_flags,
print_sep_line,
format('~n use problog_help/0 for information~n',[]),
format('~n use problog_flags/0 to display current parameter values~2n',[]),
print_sep_line,
nl,
flush_output.
% parameter initialization to be called after returning to user's directory:
:- initialization(init_global_params).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% internal control flags
% if on
% - up: collect stopped derivations to build upper bound
% - limit: iterative deepening reached limit -> should go to next level
% - mc: using problog_montecarlo, i.e. proving with current sample instead of full program
% - remember: save BDD files containing script, params and mapping
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
problog_control(on,X) :-
call(X),!.
problog_control(on,X) :-
assert(X).
problog_control(off,X) :-
retractall(X).
problog_control(check,X) :-
call(X).
:- problog_control(off,up).
:- problog_control(off,mc).
:- problog_control(off,limit).
:- problog_control(off,remember).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% nice user syntax Prob::Fact
% automatic translation to internal hardware access format
%
% probabilities =1 are dropped -> normal Prolog fact
%
% internal fact representation
% - prefixes predicate name with problog_
% - adds unique ID as first argument
% - adds logarithm of probability as last argument
% - keeps original arguments in between
%
% for each predicate appearing as probabilistic fact, wrapper clause is introduced:
% - head is most general instance of original fact
% - body is corresponding version of internal fact plus call to add_to_proof/2 to update current state during proving
% example: edge(A,B) :- problog_edge(ID,A,B,LogProb), add_to_proof(ID,LogProb).
%
% dynamic predicate problog_predicate(Name,Arity) keeps track of predicates that already have wrapper clause
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
user:term_expansion(_P::( _Goal :- _Body ), _Error) :-
throw(error('we do not support this (yet?)!')).
user:term_expansion(P::Goal,Goal) :-
P \= t(_),
P =:= 1,
!.
user:term_expansion(P::Goal, problog:ProbFact) :-
functor(Goal, Name, Arity),
atomic_concat([problog_,Name],ProblogName),
Goal =.. [Name|Args],
append(Args,[LProb],L1),
probclause_id(IDName),
term_variables(Goal,GVars),
(GVars=[] -> ID=IDName; ID=..[IDName|GVars]),
ProbFact =.. [ProblogName,ID|L1],
(P = t(TrueProb) ->
assert(tunable_fact(ID,TrueProb)),
LProb is log(0.5)
;
LProb is log(P)
),
problog_predicate(Name, Arity, ProblogName).
% introduce wrapper clause if predicate seen first time
problog_predicate(Name, Arity, _) :-
problog_predicate(Name, Arity), !.
problog_predicate(Name, Arity, ProblogName) :-
functor(OriginalGoal, Name, Arity),
OriginalGoal =.. [_|Args],
append(Args,[Prob],L1),
ProbFact =.. [ProblogName,ID|L1],
prolog_load_context(module,Mod),
assert((Mod:OriginalGoal :- ProbFact, add_to_proof(ID,Prob))),
assert(problog_predicate(Name, Arity)),
ArityPlus2 is Arity+2,
dynamic(problog:ProblogName/ArityPlus2).
% generate next global identifier
probclause_id(ID) :-
nb_getval(probclause_counter,ID), !,
C1 is ID+1,
nb_setval(probclause_counter,C1), !.
probclause_id(0) :-
nb_setval(probclause_counter,1).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% access/update the probability of ID's fact
% hardware-access version: naively scan all problog-predicates
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
get_fact_probability(ID,Prob) :-
get_internal_fact(ID,ProblogTerm,_ProblogName,ProblogArity),
arg(ProblogArity,ProblogTerm,Log),
Prob is exp(Log).
set_fact_probability(ID,Prob) :-
get_internal_fact(ID,ProblogTerm,ProblogName,ProblogArity),
retract(ProblogTerm),
ProblogTerm =.. [ProblogName|ProblogTermArgs],
nth(ProblogArity,ProblogTermArgs,_,KeepArgs),
NewLogProb is log(Prob),
nth(ProblogArity,NewProblogTermArgs,NewLogProb,KeepArgs),
NewProblogTerm =.. [ProblogName|NewProblogTermArgs],
assert(NewProblogTerm).
get_internal_fact(ID,ProblogTerm,ProblogName,ProblogArity) :-
problog_predicate(Name,Arity),
atomic_concat([problog_,Name],ProblogName),
ProblogArity is Arity+2,
functor(ProblogTerm,ProblogName,ProblogArity),
arg(1,ProblogTerm,ID),
call(ProblogTerm).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% writing those facts with learnable parameters to File
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
export_facts(File) :-
tell(File),
export_facts,
flush_output,
told.
export_facts :-
tunable_fact(ID,_),
once(write_tunable_fact(ID)),
fail.
export_facts.
write_tunable_fact(ID) :-
get_internal_fact(ID,ProblogTerm,ProblogName,ProblogArity),
ProblogTerm =.. [_Functor,ID|Args],
atomic_concat('problog_',OutsideFunctor,ProblogName),
Last is ProblogArity-1,
nth(Last,Args,LogProb,OutsideArgs),
OutsideTerm =.. [OutsideFunctor|OutsideArgs],
Prob is exp(LogProb),
format('~w :: ~q.~n',[Prob,OutsideTerm]).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% recover fact for given id
% list version not exported (yet?)
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
get_fact(ID,OutsideTerm) :-
get_internal_fact(ID,ProblogTerm,ProblogName,ProblogArity),
ProblogTerm =.. [_Functor,ID|Args],
atomic_concat('problog_',OutsideFunctor,ProblogName),
Last is ProblogArity-1,
nth(Last,Args,_LogProb,OutsideArgs),
OutsideTerm =.. [OutsideFunctor|OutsideArgs].
get_fact_list([],[]).
get_fact_list([ID|IDs],[Fact|Facts]) :-
get_fact(ID,Fact),
get_fact_list(IDs,Facts).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% ProbLog inference, core methods
%
% state of proving saved in two backtrackable global variables
% - problog_current_proof holds list of IDs of clauses used
% - problog_probability holds the sum of their log probabilities
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% called "inside" probabilistic facts to update current state of proving:
% if number of steps exceeded, fail
% if fact used before, succeed and keep status as is
% if not prunable, calculate probability and
% if threshold exceeded, add stopped derivation to upper bound and fail
% else update state and succeed
add_to_proof(ID,Prob) :-
montecarlo_check(ID),
b_getval(problog_steps,MaxSteps),
b_getval(problog_probability, CurrentP),
nb_getval(problog_threshold, CurrentThreshold),
b_getval(problog_current_proof, IDs),
( MaxSteps =< 0 ->
fail
;
( memberchk(ID, IDs) ->
true
;
\+ prune_check([ID|IDs],1),
multiply_probabilities(CurrentP, Prob, NProb),
( NProb < CurrentThreshold ->
upper_bound([ID|IDs]),
fail
;
b_setval(problog_probability, NProb),
b_setval(problog_current_proof, [ID|IDs])
)
),
Steps is MaxSteps-1,
b_setval(problog_steps,Steps)
).
% if in monte carlo mode, check array to see if fact can be used
montecarlo_check(ID) :-
(
problog_control(check,mc)
->
(
array_element(mc_sample,ID,V),
(
V == 1 -> true
;
V == 2 -> fail
;
new_sample(ID)
)
)
;
true
).
new_sample(ID) :-
get_fact_probability(ID,Prob),
random(R),
R<Prob,
!,
update_array(mc_sample,ID,1).
new_sample(ID) :-
update_array(mc_sample,ID,2),
fail.
% if threshold reached, remember this by setting limit to on, then
% if up is on, store stopped derivation in second trie
%
% List always length>=1 -> don't need []=true-case for tries
upper_bound(List) :-
problog_control(on,limit),
problog_control(check,up),
reverse(List,R),
(prune_check(R,2) -> true; insert_ptree(R,2)).
multiply_probabilities(CurrentLogP, LogProb, NLogProb) :-
NLogProb is CurrentLogP+LogProb.
% this is called by all inference methods before the actual ProbLog goal
% to set up environment for proving
init_problog(Threshold) :-
LT is log(Threshold),
b_setval(problog_probability, 0.0),
b_setval(problog_current_proof, []),
nb_setval(problog_threshold, LT),
problog_flag(maxsteps,MaxS),
b_setval(problog_steps, MaxS),
problog_control(off,limit).
% idea: proofs that are refinements of known proof can be pruned as they don't add probability mass
% note that current ptree implementation doesn't provide the check as there's no efficient method known so far...
prune_check(Proof,TreeID) :-
problog_flag(prunecheck,on),
prune_check_ptree(Proof,TreeID).
% to call a ProbLog goal, patch all subgoals with the user's module context
% (as logical part is there, but probabilistic part in problog)
problog_call(Goal) :-
yap_flag(typein_module,Module),
put_module(Goal,Module,ModGoal),
call(ModGoal).
put_module((Mod:Goal,Rest),Module,(Mod:Goal,Transformed)) :-
!,
put_module(Rest,Module,Transformed).
put_module((Goal,Rest),Module,(Module:Goal,Transformed)) :-
!,
put_module(Rest,Module,Transformed).
put_module((Mod:Goal),_Module,(Mod:Goal)) :-
!.
put_module(Goal,Module,Module:Goal).
% end of core
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% evaluating a DNF given as trie using BDD
% input: ID of trie to be used
% output: probability and status (to catch potential failures/timeouts from outside)
%
% with internal BDD timeout (set using problog flag bdd_time)
%
% bdd_ptree/3 constructs files for ProblogBDD from the trie
%
% if calling ProblogBDD doesn't exit successfully, status will be timeout
%
% writes number of proofs in trie and BDD time to standard user output
%
% if remember is on, input files for ProblogBDD will be saved
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
eval_dnf(ID,Prob,Status) :-
((ID = 1, problog_flag(save_bdd,true)) -> problog_control(on,remember); problog_control(off,remember)),
count_ptree(ID,NX),
format(user,'~w proofs~n',[NX]),
problog_flag(dir,DirFlag),
problog_flag(bdd_file,BDDFileFlag),
atomic_concat([DirFlag,BDDFileFlag],BDDFile),
problog_flag(bdd_par_file,BDDParFileFlag),
atomic_concat([DirFlag,BDDParFileFlag],BDDParFile),
(problog_control(check,remember) ->
bdd_ptree_map(ID,BDDFile,BDDParFile,Mapping),
atomic_concat([DirFlag,'save_map'],MapFile),
tell(MapFile),
format('mapping(~q).~n',[Mapping]),
flush_output,
told
;
bdd_ptree(ID,BDDFile,BDDParFile)
),
problog_flag(bdd_time,BDDTime),
problog_flag(bdd_result,ResultFileFlag),
atomic_concat([DirFlag,ResultFileFlag],ResultFile),
problog_dir(PD),
atomic_concat([PD,'/ProblogBDD -l ',BDDFile,' -i ',BDDParFile,' -m p -t ', BDDTime,' > ', ResultFile],Command),
statistics(walltime,_),
shell(Command,Return),
(
Return =\= 0
->
Status = timeout
;
(
statistics(walltime,[_,E3]),
format(user,'~w ms BDD processing~n',[E3]),
see(ResultFile),
read(probability(Prob)),
seen,
delete_file(ResultFile),
Status = ok
)
),
(problog_control(check,remember) ->
atomic_concat([DirFlag,'save_script'],SaveBDDFile),
rename_file(BDDFile,SaveBDDFile),
atomic_concat([DirFlag,'save_params'],SaveBDDParFile),
rename_file(BDDParFile,SaveBDDParFile)
;
true
),
problog_control(off,remember).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% different inference methods
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% approximate inference: bounds based on single probability threshold
% problog_threshold(+Goal,+Threshold,-LowerBound,-UpperBound,-Status)
%
% use backtracking over problog_call to get all solutions
%
% trie 1 collects proofs, trie 2 collects stopped derivations, trie 3 is used to unit them for the upper bound
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
problog_threshold(Goal, Threshold, _, _, _) :-
problog_control(on,up),
init_problog_threshold(Threshold),
problog_call(Goal),
add_solution,
fail.
problog_threshold(_, _, LP, UP, Status) :-
compute_bounds(LP, UP, Status).
init_problog_threshold(Threshold) :-
init_ptree(1),
init_ptree(2),
init_problog(Threshold).
add_solution :-
b_getval(problog_current_proof, IDs),
(IDs == [] -> R = true ; reverse(IDs,R)),
insert_ptree(R,1).
compute_bounds(LP, UP, Status) :-
eval_dnf(1,LP,StatusLow),
(StatusLow \== ok ->
Status = StatusLow
;
merge_ptree(1,2,3),
eval_dnf(3,UP,Status)),
delete_ptree(1),
delete_ptree(2),
delete_ptree(3).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% approximate inference: lower bound based on all proofs above probability threshold
% problog_low(+Goal,+Threshold,-LowerBound,-Status)
%
% same as problog_threshold/5, but lower bound only (no stopped derivations stored)
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
problog_low(Goal, Threshold, _, _) :-
problog_control(off,up),
init_problog_low(Threshold),
problog_call(Goal),
add_solution,
fail.
problog_low(_, _, LP, Status) :-
eval_dnf(1,LP,Status),
delete_ptree(1).
init_problog_low(Threshold) :-
init_ptree(1),
init_problog(Threshold).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% approximate inference: bounds by iterative deepening up to interval width Delta
% problog_delta(+Goal,+Delta,-LowerBound,-UpperBound,-Status)
%
% wraps iterative deepening around problog_threshold, i.e.
% - starts with threshold given by first_threshold flag
% - if Up-Low >= Delta, multiply threshold by factor given in id_stepsize flag and iterate
% (does not use problog_threshold as trie 1 is kept over entire search)
%
% local dynamic predicates low/2, up/2, stopDiff/1
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
problog_delta(Goal, Delta, Low, Up, Status) :-
problog_control(on,up),
problog_flag(first_threshold,InitT),
init_problog_delta(InitT,Delta),
problog_delta_id(Goal,Status),
delete_ptree(1),
delete_ptree(2),
(retract(low(_,Low)) -> true; true),
(retract(up(_,Up)) -> true; true).
init_problog_delta(Threshold,Delta) :-
retractall(low(_,_)),
retractall(up(_,_)),
retractall(stopDiff(_)),
init_ptree(1),
init_ptree(2),
assert(low(0,0.0)),
assert(up(0,1.0)),
assert(stopDiff(Delta)),
init_problog(Threshold).
problog_delta_id(Goal, _) :-
problog_call(Goal),
add_solution, % reused from problog_threshold
fail.
problog_delta_id(Goal, Status) :-
evaluateStep(Ans,StatusE),
problog_flag(last_threshold_log,Stop),
nb_getval(problog_threshold,Min),
(StatusE \== ok ->
Status = StatusE
;
(
Ans = 1 ->
Status = ok
;
Min =< Stop ->
Status = stopreached
;
problog_control(check,limit) ->
problog_control(off,limit),
problog_flag(id_stepsize_log,Step),
New is Min+Step,
nb_setval(problog_threshold,New),
problog_delta_id(Goal, Status)
;
true
)).
% call the dnf evaluation where needed
evaluateStep(Ans,Status) :- once(evalStep(Ans,Status)).
evalStep(Ans,Status) :-
stopDiff(Delta),
count_ptree(1,NProofs),
count_ptree(2,NCands),
format(user,'~w proofs, ~w stopped derivations~n',[NProofs,NCands]),
flush_output(user),
eval_lower(NProofs,Low,StatusLow),
(StatusLow \== ok ->
Status = StatusLow
;
up(_,OUP),
IntDiff is OUP-Low,
((IntDiff < Delta; IntDiff =:= 0) ->
Up=OUP, StatusUp = ok
;
eval_upper(NCands,Up,StatusUp),
delete_ptree(2),
init_ptree(2),
delete_ptree(3)
),
(StatusUp \== ok ->
Status = StatusUp
;
Diff is Up-Low,
format(user,'difference: ~6f~n',[Diff]),
flush_output(user),
((Diff < Delta; Diff =:= 0) -> Ans = 1; Ans = 0),
Status = ok)).
% no need to re-evaluate if no new proofs found on this level
eval_lower(N,P,ok) :-
low(N,P).
% evaluate if there are proofs
eval_lower(N,P,Status) :-
N > 0,
low(OldN,_),
N \= OldN,
eval_dnf(1,P,Status),
(Status = ok ->
retract(low(_,_)),
assert(low(N,P)),
format(user,'lower bound: ~6f~n',[P]),
flush_output(user)
;
true).
% if no stopped derivations, up=low
eval_upper(0,P,ok) :-
retractall(up(_,_)),
low(N,P),
assert(up(N,P)).
% else merge proofs and stopped derivations to get upper bound
% in case of timeout or other problems, skip and use bound from last level
eval_upper(N,UpP,ok) :-
N > 0,
merge_ptree(1,2,3),
eval_dnf(3,UpP,StatusUp),
(StatusUp = ok ->
retract(up(_,_)),
assert(up(N,UpP))
;
format(user,'~w - continue using old up~n',[StatusUp]),
flush_output(user),
up(_,UpP)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% explanation probability - returns list of facts used or constant 'unprovable' as third argument
% problog_max(+Goal,-Prob,-Facts)
%
% uses iterative deepening with samw parameters as bounding algorithm
% threshold gets adapted whenever better proof is found
%
% uses local dynamic predicates max_probability/1 and max_proof/1
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
problog_max(Goal, Prob, Facts) :-
problog_control(off,up),
problog_flag(first_threshold,InitT),
init_problog_max(InitT),
problog_max_id(Goal, Prob, FactIDs),
( FactIDs == unprovable -> Facts = unprovable;
get_fact_list(FactIDs,Facts)).
init_problog_max(Threshold) :-
retractall(max_probability(_)),
retractall(max_proof(_)),
assert(max_probability(-999999)),
assert(max_proof(unprovable)),
init_problog(Threshold).
update_max :-
b_getval(problog_probability,CurrP),
max_probability(MaxP),
(CurrP =< MaxP ->
fail
;
b_getval(problog_current_proof, IDs),
reverse(IDs,R),
retractall(max_proof(_)),
assert(max_proof(R)),
nb_setval(problog_threshold, CurrP),
retractall(max_probability(_)),
assert(max_probability(CurrP))).
problog_max_id(Goal, _Prob, _Clauses) :-
problog_call(Goal),
update_max,
fail.
problog_max_id(Goal, Prob, Clauses) :-
max_probability(MaxP),
nb_getval(problog_threshold, LT),
problog_flag(last_threshold_log,ToSmall),
((MaxP >= LT ; \+ problog_control(check,limit); LT < ToSmall) ->
max_proof(Clauses),
Prob is exp(MaxP)
;
problog_flag(id_stepsize_log,Step),
NewLT is LT+Step,
nb_setval(problog_threshold, NewLT),
problog_control(off,limit),
problog_max_id(Goal, Prob, Clauses)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% lower bound using k best proofs
% problog_kbest(+Goal,+K,-Prob,-Status)
%
% does iterative deepening search similar to problog_max, but for k(>=1) most likely proofs
% afterwards uses BDD evaluation to calculate probability (also for k=1 -> uniform treatment in learning)
%
% uses dynamic local predicate current_kbest/3 to collect proofs,
% only builds trie at the end (as probabilities of single proofs are important here)
%
% note: >k proofs will be used if the one at position k shares its probability with others,
% as all proofs with that probability will be included
%
% version with _save at the end renames files for ProblogBDD to keep them
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
problog_kbest_save(Goal, K, Prob, Status, BDDFile, ParamFile) :-
problog_kbest(Goal, K, Prob, Status),
( Status=ok ->
problog_flag(bdd_file,InternBDDFlag),
problog_flag(bdd_par_file,InternParFlag),
problog_flag(dir,DirFlag),
atomic_concat([DirFlag,InternBDDFlag],InternBDD),
atomic_concat([DirFlag,InternParFlag],InternPar),
rename_file(InternBDD,BDDFile),
rename_file(InternPar,ParamFile)
;
true).
problog_kbest(Goal, K, Prob, Status) :-
problog_control(off,up),
problog_flag(first_threshold,InitT),
init_problog_kbest(InitT),
problog_kbest_id(Goal, K),
retract(current_kbest(_,ListFound,_NumFound)),
build_prefixtree(ListFound),
eval_dnf(1,Prob,Status),
delete_ptree(1).
init_problog_kbest(Threshold) :-
retractall(current_kbest(_,_,_)),
assert(current_kbest(-999999,[],0)), %(log-threshold,proofs,num_proofs)
init_ptree(1),
init_problog(Threshold).
problog_kbest_id(Goal, K) :-
problog_call(Goal),
update_kbest(K),
fail.
problog_kbest_id(Goal, K) :-
current_kbest(CurrentBorder,_,Found),
nb_getval(problog_threshold, Min),
problog_flag(last_threshold_log,ToSmall),
((Found>=K ; \+ problog_control(check,limit) ; Min < CurrentBorder ; Min < ToSmall) ->
true
;
problog_flag(id_stepsize_log,Step),
NewLT is Min+Step,
nb_setval(problog_threshold, NewLT),
problog_control(off,limit),
problog_kbest_id(Goal, K)).
update_kbest(K) :-
b_getval(problog_probability,NewLogProb),
current_kbest(LogThreshold,_,_),
(NewLogProb>=LogThreshold ->
b_getval(problog_current_proof,RevProof),
reverse(RevProof,Proof),
update_current_kbest(K,NewLogProb,Proof)
;
fail).
update_current_kbest(_,NewLogProb,Cl) :-
current_kbest(_,List,_),
memberchk(NewLogProb-Cl,List),
!.
update_current_kbest(K,NewLogProb,Cl) :-
retract(current_kbest(OldThres,List,Length)),
sorted_insert(NewLogProb-Cl,List,NewList),
NewLength is Length+1,
(NewLength < K ->
assert(current_kbest(OldThres,NewList,NewLength))
;
(NewLength>K ->
First is NewLength-K+1,
cutoff(NewList,NewLength,First,FinalList,FinalLength)
; FinalList=NewList, FinalLength=NewLength),
FinalList=[NewThres-_|_],
nb_setval(problog_threshold,NewThres),
assert(current_kbest(NewThres,FinalList,FinalLength))).
sorted_insert(A,[],[A]).
sorted_insert(A-LA,[B1-LB1|B], [A-LA,B1-LB1|B] ) :-
A =< B1.
sorted_insert(A-LA,[B1-LB1|B], [B1-LB1|C] ) :-
A > B1,
sorted_insert(A-LA,B,C).
% keeps all entries with lowest probability, even if implying a total of more than k
cutoff(List,Len,1,List,Len) :- !.
cutoff([P-L|List],Length,First,[P-L|List],Length) :-
nth(First,[P-L|List],PF-_),
PF=:=P,
!.
cutoff([_|List],Length,First,NewList,NewLength) :-
NextFirst is First-1,
NextLength is Length-1,
cutoff(List,NextLength,NextFirst,NewList,NewLength).
build_prefixtree([]).
build_prefixtree([_-[]|_List]) :-
!,
insert_ptree(true,1).
build_prefixtree([_-L|List]) :-
insert_ptree(L,1),
build_prefixtree(List).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% exact probability
% problog_exact(+Goal,-Prob,-Status)
%
% using all proofs = using all proofs with probability > 0
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
problog_exact(Goal,Prob,Status) :-
problog_low(Goal,0,Prob,Status).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% probability by sampling:
% running another N samples until 95percentCI-width<Delta
% lazy sampling using three-valued array indexed by internal fact IDs
%
% still collects actual proofs found in samples in ptree, though this is no longer used
% by method itself, only to write number to log-file
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
problog_montecarlo(Goal,Delta,Prob) :-
nb_getval(probclause_counter,ID), !,
C is ID+1,
static_array(mc_sample,C,char),
problog_control(off,up),
problog_flag(mc_batchsize,N),
problog_flag(mc_logfile,File1),
problog_flag(dir,Dir),
atomic_concat([Dir,File1],File),
montecarlo(Goal,Delta,N,File),
retract(mc_prob(Prob)).
montecarlo(Goal,Delta,K,File) :-
reset_static_array(mc_sample),
problog_control(on,mc),
open(File,write,Log),
format(Log,'# goal: ~q~n#delta: ~w~n',[Goal,Delta]),
format(Log,'# num_programs prob low high diff time cache_size num_pos~2n',[]),
close(Log),
statistics(walltime,[T1,_]),
init_ptree(1),
format('search for ~q~n',[Goal]),
montecarlo(Goal,Delta,K,0,File,0,T1),
problog_control(off,mc),
delete_ptree(1).
% calculate values after K samples
montecarlo(Goal,Delta,K,SamplesSoFar,File,PositiveSoFar,InitialTime) :-
SamplesNew is SamplesSoFar+1,
SamplesNew mod K =:= 0,
!,
copy_term(Goal,GoalC),
(mc_prove(GoalC) -> Next is PositiveSoFar+1; Next=PositiveSoFar),
Prob is Next/SamplesNew,
Epsilon is 2*sqrt(Prob*(1-Prob)/SamplesNew),
Low is Prob-Epsilon,
High is Prob+Epsilon,
Diff is 2*Epsilon,
statistics(walltime,[T2,_]),
Time is (T2-InitialTime)/1000,
count_ptree(1,CacheSize),
format('~n~w samples~nestimated probability ~w~n95 percent confidence interval [~w,~w]~n',[SamplesNew,Prob,Low,High]),
open(File,append,Log),
format(Log,'~w ~8f ~8f ~8f ~8f ~3f ~w ~w~n',[SamplesNew,Prob,Low,High,Diff,Time,CacheSize,Next]),
close(Log),
((Diff<Delta; Diff =:= 0) -> format('Runtime ~w sec~2n',[Time]),assert(mc_prob(Prob))
;
montecarlo(Goal,Delta,K,SamplesNew,File,Next,InitialTime)).
% continue until next K samples done
montecarlo(Goal,Delta,K,SamplesSoFar,File,PositiveSoFar,InitialTime) :-
SamplesNew is SamplesSoFar+1,
copy_term(Goal,GoalC),
(mc_prove(GoalC) -> Next is PositiveSoFar+1; Next=PositiveSoFar),
montecarlo(Goal,Delta,K,SamplesNew,File,Next,InitialTime).
mc_prove(A) :- !,
(get_some_proof(A) ->
clean_sample
;
clean_sample,fail
).
clean_sample :-
reset_static_array(mc_sample),
fail.
clean_sample.
% find new proof
get_some_proof(Goal) :-
init_problog(0),
problog_call(Goal),
b_getval(problog_current_proof,Used),
(Used == [] -> Proof=true; reverse(Used,Proof)),
insert_ptree(Proof,1).

284
ProbLog/problog/flags.yap Normal file
View File

@ -0,0 +1,284 @@
%%% -*- Mode: Prolog; -*-
:- module(flags, [set_problog_flag/2,
problog_flag/2,
problog_flags/0]).
:- style_check(all).
:- yap_flag(unknown,error).
:- use_module(print, [print_param/4,
print_sep_line/0]).
:- ensure_loaded(library(system)).
:- dynamic bdd_time/1, first_threshold/1, last_threshold/1, id_stepsize/1, prunecheck/1, maxsteps/1, mc_batchsize/1, mc_logfile/1, bdd_file/1, bdd_par_file/1, bdd_result/1, work_dir/1, save_bdd/1.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% global parameters that can be set using set_problog_flag/2
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
problog_flag(Flag,Option) :-
get_problog_flag(Flag,Option).
get_problog_flag(bdd_time,X) :-
bdd_time(X).
get_problog_flag(first_threshold,X) :-
first_threshold(X).
get_problog_flag(last_threshold,X) :-
last_threshold(L),
X is exp(L).
get_problog_flag(last_threshold_log,X) :-
last_threshold(X).
get_problog_flag(id_stepsize,X) :-
id_stepsize(L),
X is exp(L).
get_problog_flag(id_stepsize_log,X) :-
id_stepsize(X).
get_problog_flag(prunecheck,X) :-
prunecheck(X).
get_problog_flag(maxsteps,X) :-
maxsteps(X).
get_problog_flag(mc_batchsize,X) :-
mc_batchsize(X).
get_problog_flag(mc_logfile,X) :-
mc_logfile(X).
get_problog_flag(bdd_file,X) :-
bdd_file(X).
get_problog_flag(bdd_par_file,X) :-
bdd_par_file(X).
get_problog_flag(bdd_result,X) :-
bdd_result(X).
get_problog_flag(dir,X) :-
work_dir(X).
get_problog_flag(save_bdd,X) :-
save_bdd(X).
%%%%%%%%%%%%
% BDD timeout in seconds, used as option in BDD tool
%%%%%%%%%%%%
set_problog_flag(bdd_time,X) :-
(\+ integer(X); X<0),
!,
format(user,'\% ERROR: value must be positive integer!~n',[]),
flush_output(user),
fail.
set_problog_flag(bdd_time,X) :-
retractall(bdd_time(_)),
assert(bdd_time(X)).
%%%%%%%%%%%%
% iterative deepening on minimal probabilities (delta, max, kbest):
% - first threshold (not in log-space as only used to retrieve argument for init_threshold/1, which is also used with user-supplied argument)
% - last threshold to ensure termination in case infinite search space (saved in log-space for easy comparison with current values during search)
% - factor used to decrease threshold for next level, NewMin=Factor*OldMin (saved in log-space)
%%%%%%%%%%%%
set_problog_flag(first_threshold,X) :-
(\+ number(X); X<0 ; X>1),
!,
format(user,'\% ERROR: value must be in [0,1]!~n',[]),
flush_output(user),
fail.
set_problog_flag(first_threshold,X) :-
retractall(first_threshold(_)),
assert(first_threshold(X)).
set_problog_flag(last_threshold,X) :-
(\+ number(X); X<0 ; X>1),
!,
format(user,'\% ERROR: value must be in [0,1]!~n',[]),
flush_output(user),
fail.
set_problog_flag(last_threshold,X) :-
retractall(last_threshold(_)),
L is log(X),
assert(last_threshold(L)).
set_problog_flag(id_stepsize,X) :-
(\+ number(X); X=<0 ; X>=1),
!,
format(user,'\% ERROR: value must be in ]0,1[!~n',[]),
flush_output(user),
fail.
set_problog_flag(id_stepsize,X) :-
retractall(id_stepsize(_)),
L is log(X),
assert(id_stepsize(L)).
%%%%%%%%%%%%
% prune check stops derivations if they use a superset of facts already known to form a proof
% (very) costly test, can be switched on/off here
%%%%%%%%%%%%
set_problog_flag(prunecheck,on) :-
!,
format(user,'WARNING: prune check not implemented, will fail~n',[]),
flush_output(user),
retractall(prunecheck(_)),
assert(prunecheck(on)).
set_problog_flag(prunecheck,off) :-
!,
retractall(prunecheck(_)),
assert(prunecheck(off)).
set_problog_flag(prunecheck,_) :-
format(user,'\% ERROR: value must be \'on\' or \'off\'!~n',[]),
flush_output(user),
fail.
%%%%%%%%%%%%
% max number of calls to probabilistic facts per derivation (to ensure termination)
%%%%%%%%%%%%
set_problog_flag(maxsteps,X) :-
(\+ integer(X); X<0),
!,
format(user,'\% ERROR: value must be positive integer!~n',[]),
flush_output(user),
fail.
set_problog_flag(maxsteps,X) :-
retractall(maxsteps(_)),
assert(maxsteps(X)).
%%%%%%%%%%%%
% montecarlo: recalculate current approximation after N samples
%%%%%%%%%%%%
set_problog_flag(mc_batchsize,X) :-
(\+ integer(X); X<0),
!,
format(user,'\% ERROR: value must be positive integer!~n',[]),
flush_output(user),
fail.
set_problog_flag(mc_batchsize,X) :-
retractall(mc_batchsize(_)),
assert(mc_batchsize(X)).
%%%%%%%%%%%%
% montecarlo: write log to this file
%%%%%%%%%%%%
set_problog_flag(mc_logfile,X) :-
\+ atom(X),
!,
format(user,'\% ERROR: value must be atom!~n',[]),
flush_output(user),
fail.
set_problog_flag(mc_logfile,X) :-
retractall(mc_logfile(_)),
assert(mc_logfile(X)).
%%%%%%%%%%%%
% files to write BDD script and pars
% bdd_file overwrites bdd_par_file with matching extended name
% if different name wanted, respect order when setting
%%%%%%%%%%%%
set_problog_flag(bdd_file,X) :-
\+ atom(X),
!,
format(user,'\% ERROR: value must be atom!~n',[]),
flush_output(user),
fail.
set_problog_flag(bdd_file,X) :-
retractall(bdd_file(_)),
atomic_concat(X,'_probs',Y),
set_problog_flag(bdd_par_file,Y),
atomic_concat(X,'_res',Z),
set_problog_flag(bdd_result,Z),
assert(bdd_file(X)).
set_problog_flag(bdd_par_file,X) :-
\+ atom(X),
!,
format(user,'\% ERROR: value must be atom!~n',[]),
flush_output(user),
fail.
set_problog_flag(bdd_par_file,X) :-
retractall(bdd_par_file(_)),
assert(bdd_par_file(X)).
set_problog_flag(bdd_result,X) :-
\+ atom(X),
!,
format(user,'\% ERROR: value must be atom!~n',[]),
flush_output(user),
fail.
set_problog_flag(bdd_result,X) :-
retractall(bdd_result(_)),
assert(bdd_result(X)).
%%%%%%%%%%%%
% working directory: all the temporary and output files will be located there
%%%%%%%%%%%%
set_problog_flag(dir,X) :-
\+ atom(X),
!,
format(user,'\% ERROR: value must be atom!~n',[]),
flush_output(user),
fail.
set_problog_flag(dir,X) :-
retractall(work_dir(_)),
atomic_concat([X,'/'],D),
atomic_concat(['mkdir ',D],Mkdir),
(file_exists(X) -> true; shell(Mkdir)),
assert(work_dir(D)).
%%%%%%%%%%%%
% save BDD information for the (last) lower bound BDD used during inference
% produces three files named save_script, save_params, save_map
% located in the directory given by problog_flag dir
%%%%%%%%%%%%
set_problog_flag(save_bdd,true) :-
!,
retractall(save_bdd(_)),
assert(save_bdd(true)).
set_problog_flag(save_bdd,false) :-
!,
retractall(save_bdd(_)),
assert(save_bdd(false)).
set_problog_flag(save_bdd,_) :-
format(user,'\% ERROR: value must be \'true\' or \'false\'!~n',[]),
flush_output(user),
fail.
%%%%%%%%%%%%%%%%%%%%%%%%
% show values
%%%%%%%%%%%%%%%%%%%%%%%%
problog_flags :-
format('~n',[]),
print_sep_line,
format('problog flags: use set_problog_flag(Flag,Option) to change, problog_flag(Flag,Option) to view~n',[]),
print_sep_line,
print_param(description,value,flag,option),
print_sep_line,
problog_flag(bdd_time,StopBDD),
print_param('BDD computation timeout in seconds',StopBDD,'bdd_time','positive integer'),
problog_flag(first_threshold,First),
print_param('starting threshold iterative deepening',First,'first_threshold','0 =< Option =< 1'),
problog_flag(last_threshold,Last),
print_param('stopping threshold iterative deepening',Last,'last_threshold','0 =< Option =< 1'),
problog_flag(id_stepsize,Decrease),
print_param('threshold shrinking factor iterative deepening',Decrease,'id_stepsize','0 < Option < 1'),
problog_flag(prunecheck,Check),
print_param('stop derivations including all facts of known proof',Check,'prunecheck','on/off'),
problog_flag(maxsteps,Steps),
print_param('max. number of prob. steps per derivation',Steps,'maxsteps','positive integer'),
problog_flag(mc_batchsize,MCBatch),
print_param('number of samples before update in montecarlo',MCBatch,'mc_batchsize','positive integer'),
problog_flag(mc_logfile,MCFile),
print_param('logfile for montecarlo',MCFile,'mc_logfile','atom'),
problog_flag(bdd_file,BDDFile),
print_param('file for BDD script',BDDFile,'bdd_file','atom'),
problog_flag(dir,WorkDir),
print_param('directory for files',WorkDir,'dir','atom'),
problog_flag(save_bdd,Save),
print_param('save BDD files for (last) lower bound',Save,'save_bdd','true/false'),
print_sep_line,
format('~n',[]),
flush_output.

24
ProbLog/problog/print.yap Normal file
View File

@ -0,0 +1,24 @@
%%% -*- Mode: Prolog; -*-
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% printing functions used for problog_help and problog_flags
% collected here to have formatting at one place
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
:- module(print, [print_param/4,
print_sep_line/0,
print_inference/2]).
print_param(Keyword,Value,Function,Legal) :-
format(user,'~w~55+~q~15+~w~30+~w~25+~n',[Keyword,Value,Function,Legal]).
print_sep_line :-
sep_line(125).
sep_line(0) :-
!,
format('~n',[]).
sep_line(N) :-
format('-',[]),
NN is N-1,
sep_line(NN).
print_inference(Call,Description) :-
format(user,'~w~65+~w~60+~n',[Call,Description]).

500
ProbLog/problog/tptree.yap Normal file
View File

@ -0,0 +1,500 @@
%%% -*- Mode: Prolog; -*-
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% prefix-trees for managing a DNF
% remembers shortest prefix of a conjunction only (i.e. a*b+a*b*c results in a*b only, but b*a+a*b*c is not reduced)
% children are sorted, but branches aren't (to speed up search while keeping structure sharing from proof procedure)
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
:- module(ptree,[init_ptree/1,
delete_ptree/1,
rename_ptree/2,
member_ptree/2,
enum_member_ptree/2,
insert_ptree/2,
delete_ptree/2,
edges_ptree/2,
count_ptree/2,
prune_check_ptree/2,
empty_ptree/1,
merge_ptree/3,
bdd_ptree/3,
bdd_ptree_map/4
]).
:- use_module(library(tries),
[
trie_open/1,
trie_close/1,
trie_stats/4,
trie_check_entry/3,
trie_get_entry/2,
trie_put_entry/3,
trie_remove_entry/1,
trie_usage/4,
trie_dup/2,
trie_join/2,
trie_traverse/2
]).
:- use_module(library(ordsets),
[
ord_subset/2
]).
:- style_check(all).
:- yap_flag(unknown,error).
:- use_module(flags,[problog_flag/2]).
:- ensure_loaded(library(lists)).
:- ensure_loaded(library(system)).
% name lexicon external - internal
sym(1,tree1) :- !.
sym(2,tree2) :- !.
sym(3,tree3) :- !.
sym(N,AN) :- atomic_concat([tree,N],AN).
%%%%%%%%%%%%%%%%%%%%%%%%
% ptree basics
%%%%%%%%%%%%%%%%%%%%%%%%
init_ptree(ID) :-
sym(ID,Sym),
trie_open(Trie),
nb_setval(Sym, Trie).
delete_ptree(ID) :-
sym(ID,Sym),
nb_getval(Sym, Trie), !,
trie_close(Trie),
trie_open(NewTrie),
nb_setval(Sym, NewTrie).
delete_ptree(_).
rename_ptree(OldID,NewID) :-
sym(OldID,OldSym),
sym(NewID,NewSym),
nb_getval(OldSym, Trie),
nb_set_shared_val(NewSym, Trie).
empty_ptree(ID) :-
sym(ID,Sym),
nb_getval(Sym, Trie),
trie_usage(Trie, 0, 0, 0).
%%%%%%%%%%%%%%%%%%%%%%%%
% member
%%%%%%%%%%%%%%%%%%%%%%%%
% non-backtrackable (to check)
member_ptree(List,ID) :-
sym(ID,Sym),
nb_getval(Sym, Trie),
trie_check_entry(Trie, List, _).
% backtrackable (to list)
enum_member_ptree(ID,List) :-
sym(ID,Sym),
nb_getval(Sym, Tree),
trie_path(Tree, List).
trie_path(Tree, List) :-
trie_traverse(Tree,Ref),
trie_get_entry(Ref, List).
%%%%%%%%%%%%%%%%%%%%%%%%
% insert conjunction
%%%%%%%%%%%%%%%%%%%%%%%%
insert_ptree(true,ID) :-
sym(ID,Sym),
!,
nb_getval(Sym, Trie),
trie_close(Trie),
trie_open(NTrie),
trie_put_entry(NTrie, true, _).
insert_ptree(List,ID) :-
sym(ID,Sym),
nb_getval(Sym, Trie),
trie_put_entry(Trie, List, _).
%%%%%%%%%%%%%%%%%%%%%%%%
% delete conjunction
%%%%%%%%%%%%%%%%%%%%%%%%
delete_ptree(List,ID) :-
sym(ID,Sym),
nb_getval(Sym, Trie),
trie_check_entry(Trie, List, Ref),
trie_remove_entry(Ref).
%%%%%%%%
% return list -Edges of all edge labels in ptree
% doesn't use any heuristic to order those for the BDD
% (automatic reordering has to do the job)
%%%%%%%%%
edges_ptree(ID,[]) :-
empty_ptree(ID),
!.
edges_ptree(ID,[]) :-
sym(ID,Sym),
nb_getval(Sym, Trie),
trie_check_entry(Trie, true, _),
!.
edges_ptree(ID,Edges) :-
sym(ID,Sym),
nb_getval(Sym, Trie),
setof(X, trie_literal(Trie, X), Edges).
trie_literal(Trie, X) :-
trie_traverse(Trie,Ref),
trie_get_entry(Ref, List),
member(X, List).
%%%%%%%%
% number of conjunctions in the tree
%%%%%%%%%
count_ptree(ID,N) :-
sym(ID,Sym),
nb_getval(Sym, Trie),
trie_usage(Trie, N, _, _).
%%%%%%%%
% check whether some branch of ptree is a subset of conjunction List
% useful for pruning the search for proofs (optional due to time overhead)
% currently not implemented, just fails
%%%%%%%
prune_check_ptree(_List,_TreeID) :-
format(user,'FAIL: prune check currently not supported~n',[]),
flush_output(user),
fail.
%%%%%%%%%%%%%
% merge two ptrees
% - take care not to loose proper prefixes that are proofs!
%%%%%%%%%%%%%%%
merge_ptree(ID1,_,ID3) :-
sym(ID1,Sym1),
sym(ID3,Sym3),
nb_getval(Sym1, T1),
trie_check_entry(T1, true, _),
!,
trie_open(T3),
trie_put_entry(T3, true, _),
nb_setval(Sym3, T3).
merge_ptree(_,ID2,ID3) :-
sym(ID2,Sym2),
sym(ID3,Sym3),
nb_getval(Sym2, T2),
trie_check_entry(T2, true, _),
!,
trie_open(T3),
trie_put_entry(T3, true, _),
nb_setval(Sym3, T3).
merge_ptree(ID1,ID2,ID3) :-
sym(ID1,Sym1),
sym(ID2,Sym2),
sym(ID3,Sym3),
nb_getval(Sym1, T1),
nb_getval(Sym2, T2),
trie_dup(T1, T3),
trie_join(T3,T2),
nb_setval(Sym3, T3).
%%%%%%%%%%%%%%%%%%%%%%%%
% write BDD info for given ptree to file
% - initializes leaf BDDs (=variables) first
% - then compresses ptree to exploit subtree sharing
% - bdd_pt/1 does the work on the structure itself
%%%%%%%%%%%%%%%%%%%%%%%%
bdd_ptree(ID,FileBDD,FileParam) :-
bdd_ptree_script(ID,FileBDD,FileParam),
eraseall(map).
% version returning variable mapping
bdd_ptree_map(ID,FileBDD,FileParam,Mapping) :-
bdd_ptree_script(ID,FileBDD,FileParam),
findall(X,recorded(map,X,_),Map),
add_probs(Map,Mapping),
eraseall(map).
add_probs([],[]).
add_probs([m(A,Name)|Map],[m(A,Name,Prob)|Mapping]) :-
problog:get_fact_probability(A,Prob),
add_probs(Map,Mapping).
% number of variables may be to high:
% counted on trie, but conversion to old tree representation
% transforms A*B+A to A (prefix-test)
bdd_ptree_script(ID,FileBDD,FileParam) :-
edges_ptree(ID,Edges),
tell(FileParam),
bdd_vars_script(Edges),
flush_output,
told,
length(Edges,VarCount),
assert(c_num(1)),
bdd_pt(ID,CT),
c_num(NN),
IntermediateSteps is NN-1,
tell(FileBDD),
format('@BDD1~n~w~n~w~n~w~n',[VarCount,0,IntermediateSteps]),
output_compressed_script(CT),
told,
retractall(c_num(_)),
retractall(compression(_,_)).
% write parameter file by iterating over all var/not(var) occuring in the tree
bdd_vars_script(Edges) :-
bdd_vars_script(Edges,0).
bdd_vars_script([],_).
bdd_vars_script([A|B],N) :-
problog:get_fact_probability(A,P),
get_var_name(A,NameA),
format('@~w~n~12f~n',[NameA,P]),
NN is N+1,
bdd_vars_script(B,NN).
%%%%%%%%%%%%%%%%%%%%%%%%
% find top level symbol for script
%%%%%%%%%%%%%%%%%%%%%%%%
% special cases: variable-free formulae
bdd_pt(ID,false) :-
empty_ptree(ID),
!,
once(retractall(c_num(_))),
once(assert(c_num(2))).
bdd_pt(ID,true) :-
sym(ID,Sym),
nb_getval(Sym, Trie),
trie_check_entry(Trie, true, _),
!,
once(retractall(c_num(_))),
once(assert(c_num(2))).
% general case: transform trie to nested tree structure for compression
bdd_pt(ID,CT) :-
sym(ID,Sym),
nb_getval(Sym, Trie),
trie_to_tree(Trie, Tree),
compress_pt(Tree,CT).
trie_to_tree(Trie, Tree) :-
findall(Path,trie_path(Trie, Path), Paths),
add_trees(Paths, [], Tree).
add_trees([], Tree, Tree).
add_trees([List|Paths], Tree0, Tree) :-
ins_pt(List, Tree0, TreeI),
add_trees(Paths, TreeI, Tree).
ins_pt([],_T,[]) :- !.
ins_pt([A|B],[s(A1,AT)|OldT],NewT) :-
compare(Comp, A1, A),
(Comp == = ->
(AT == [] ->
NewT=[s(A1,AT)|OldT]
;
NewT = [s(A1,NewAT)|OldT],
ins_pt(B, AT, NewAT))
;
Comp == > ->
NewT = [s(A1,AT)|Tree],
ins_pt([A|B], OldT, Tree)
;
NewT = [s(A,BTree),s(A1,AT)|OldT],
ins_pt(B,[],BTree)
).
ins_pt([A|B],[],[s(A,NewAT)]) :-
ins_pt(B,[],NewAT).
%%%%%%%%%%%%
% BDD compression: alternates and- and or-levels to build BDD bottom-up
% each sub-BDD will be either a conjunction of a one-node BDD with some BDD or a disjunction of BDDs
% uses the internal database to temporarily store a map of components
%%%%%%%%%%%%
% T is completely compressed and contains single variable
% i.e. T of form x12
compress_pt(T,TT) :-
atom(T),
test_var_name(T),
!,
get_next_name(TT),
assertz(compression(TT,[T])).
% T is completely compressed and contains subtrees
% i.e. T of form 'L56'
compress_pt(T,T) :-
atom(T).
% T not yet compressed
% i.e. T is a tree-term (nested list & s/2 structure)
% -> execute one layer of compression, then check again
compress_pt(T,CT) :-
\+ atom(T),
and_or_compression(T,IT),
compress_pt(IT,CT).
% transform tree-term T into tree-term CT where last two layers have been processed
% i.e. introduce names for subparts (-> Map) and replace (all occurrenes of) subparts by this names
and_or_compression(T,CT) :-
and_comp(T,AT),
or_comp(AT,CT).
% replace leaves that are single child by variable representing father-AND-child
and_comp(T,AT) :-
all_leaves_pt(T,Leaves),
compression_mapping(Leaves,Map),
replace_pt(T,Map,AT).
% replace list of siblings by variable representing their disjunction
or_comp(T,AT) :-
all_leaflists_pt(T,Leaves),
compression_mapping(Leaves,Map),
replace_pt(T,Map,AT).
all_leaves_pt(T,L) :-
all(X,some_leaf_pt(T,X),L).
some_leaf_pt([s(A,[])|_],s(A,[])).
some_leaf_pt([s(A,L)|_],s(A,L)) :-
atom(L).
some_leaf_pt([s(_,L)|_],X) :-
some_leaf_pt(L,X).
some_leaf_pt([_|L],X) :-
some_leaf_pt(L,X).
all_leaflists_pt(L,[L]) :-
atomlist(L),!.
all_leaflists_pt(T,L) :-
all(X,some_leaflist_pt(T,X),L),!.
all_leaflists_pt(_,[]).
some_leaflist_pt([s(_,L)|_],L) :-
atomlist(L).
some_leaflist_pt([s(_,L)|_],X) :-
some_leaflist_pt(L,X).
some_leaflist_pt([_|L],X) :-
some_leaflist_pt(L,X).
atomlist([]).
atomlist([A|B]) :-
atom(A),
atomlist(B).
% for each subtree that will be compressed, add its name
% only introduce 'L'-based names when subtree composes elements, store these in compression/2 for printing the script
compression_mapping([],[]).
compression_mapping([First|B],[N-First|BB]) :-
(
First = s(A,[]) % subtree is literal -> use variable's name x17 from map
->
recorded(map,m(A,N),_)
;
(First = s(A,L),atom(L)) % subtree is node with single completely reduced child -> use next 'L'-based name
-> (get_next_name(N),
assertz(compression(N,s(A,L))))
;
(First = [L],atom(L)) % subtree is an OR with a single completely reduced element -> use element's name
-> N=L
;
(atomlist(First), % subtree is an OR with only (>1) completely reduced elements -> use next 'L'-based name
get_next_name(N),
assertz(compression(N,First)))
),
compression_mapping(B,BB).
% replace_pt(+T,+Map,-NT)
% given the tree-term T and the Map of Name-Subtree entries, replace each occurence of Subtree in T with Name -> result NT
replace_pt(T,[],T).
replace_pt([],_,[]).
replace_pt(L,M,R) :-
atomlist(L),
member(R-L,M),
!.
replace_pt([L|LL],[M|MM],R) :-
replace_pt_list([L|LL],[M|MM],R).
replace_pt_list([T|Tree],[M|Map],[C|Compr]) :-
replace_pt_single(T,[M|Map],C),
replace_pt_list(Tree,[M|Map],Compr).
replace_pt_list([],_,[]).
replace_pt_single(s(A,T),[M|Map],Res) :-
atomlist(T),
member(Res-s(A,T),[M|Map]),
!.
replace_pt_single(s(A,T),[M|Map],s(A,Res)) :-
atomlist(T),
member(Res-T,[M|Map]),
!.
replace_pt_single(s(A,T),[M|Map],Res) :-
member(Res-s(A,T),[M|Map]),
!.
replace_pt_single(s(A,T),[M|Map],s(A,TT)) :-
replace_pt_list(T,[M|Map],TT).
replace_pt_single(A,_,A) :-
atom(A).
%%%%%%%%%%%%
% output for script
% input argument is compressed tree, i.e. true/false or name assigned in last compression step
%%%%%%%%%%%%
output_compressed_script(false) :-
!,
format('L1 = FALSE~nL1~n',[]).
output_compressed_script(true) :-
!,
format('L1 = TRUE~nL1~n',[]).
% for each name-subtree pair, write corresponding line to script, e.g. L17 = x4 * L16
% stop after writing definition of root (last entry in compression/2), add it's name to mark end of script
output_compressed_script(T) :-
once(retract(compression(Short,Long))),
(T = Short ->
format('~w = ',[Short]),
format_compression_script(Long),
format('~w~n',[Short])
;
format('~w = ',[Short]),
format_compression_script(Long),
output_compressed_script(T)).
format_compression_script(s(A,B)) :-
recorded(map,m(A,C),_),
format('~w * ~w~n',[C,B]).
format_compression_script([A]) :-
format('~w~n',[A]).
format_compression_script([A,B|C]) :-
format('~w + ',[A]),
format_compression_script([B|C]).
%%%%%%%%%%%%%%%%%%%%%%%%
% auxiliaries for translation to BDD
%%%%%%%%%%%%%%%%%%%%%%%%
% prefix the current counter with "L"
get_next_name(Name) :-
retract(c_num(N)),
NN is N+1,
assert(c_num(NN)),
atomic_concat('L',N,Name).
% create BDD-var as fact id prefixed by x
% learning.yap relies on this format!
% when changing, also adapt test_var_name/1 below
get_var_name(A,NameA) :-
atomic_concat([x,A],NameA),
recorda(map,m(A,NameA),_).
% test used by base case of compression mapping to detect single-variable tree
% has to match above naming scheme
test_var_name(T) :-
atomic_concat(x,_,T).

View File

@ -0,0 +1,281 @@
/******************************************************************************\
* *
* SimpleCUDD library (www.cs.kuleuven.be/~theo/tools/simplecudd.html) *
* SimpleCUDD was developed at Katholieke Universiteit Leuven(www.kuleuven.be) *
* *
* Copyright T. Mantadelis and Katholieke Universiteit Leuven 2008 *
* *
* Author: Theofrastos Mantadelis *
* File: Example.c *
* *
********************************************************************************
* *
* The "Artistic License" *
* *
* Preamble *
* *
* The intent of this document is to state the conditions under which a *
* Package may be copied, such that the Copyright Holder maintains some *
* semblance of artistic control over the development of the package, *
* while giving the users of the package the right to use and distribute *
* the Package in a more-or-less customary fashion, plus the right to make *
* reasonable modifications. *
* *
* Definitions: *
* *
* "Package" refers to the collection of files distributed by the *
* Copyright Holder, and derivatives of that collection of files *
* created through textual modification. *
* *
* "Standard Version" refers to such a Package if it has not been *
* modified, or has been modified in accordance with the wishes *
* of the Copyright Holder as specified below. *
* *
* "Copyright Holder" is whoever is named in the copyright or *
* copyrights for the package. *
* *
* "You" is you, if you're thinking about copying or distributing *
* this Package. *
* *
* "Reasonable copying fee" is whatever you can justify on the *
* basis of media cost, duplication charges, time of people involved, *
* and so on. (You will not be required to justify it to the *
* Copyright Holder, but only to the computing community at large *
* as a market that must bear the fee.) *
* *
* "Freely Available" means that no fee is charged for the item *
* itself, though there may be fees involved in handling the item. *
* It also means that recipients of the item may redistribute it *
* under the same conditions they received it. *
* *
* 1. You may make and give away verbatim copies of the source form of the *
* Standard Version of this Package without restriction, provided that you *
* duplicate all of the original copyright notices and associated disclaimers. *
* *
* 2. You may apply bug fixes, portability fixes and other modifications *
* derived from the Public Domain or from the Copyright Holder. A Package *
* modified in such a way shall still be considered the Standard Version. *
* *
* 3. You may otherwise modify your copy of this Package in any way, provided *
* that you insert a prominent notice in each changed file stating how and *
* when you changed that file, and provided that you do at least ONE of the *
* following: *
* *
* a) place your modifications in the Public Domain or otherwise make them *
* Freely Available, such as by posting said modifications to Usenet or *
* an equivalent medium, or placing the modifications on a major archive *
* site such as uunet.uu.net, or by allowing the Copyright Holder to include *
* your modifications in the Standard Version of the Package. *
* *
* b) use the modified Package only within your corporation or organization. *
* *
* c) rename any non-standard executables so the names do not conflict *
* with standard executables, which must also be provided, and provide *
* a separate manual page for each non-standard executable that clearly *
* documents how it differs from the Standard Version. *
* *
* d) make other distribution arrangements with the Copyright Holder. *
* *
* 4. You may distribute the programs of this Package in object code or *
* executable form, provided that you do at least ONE of the following: *
* *
* a) distribute a Standard Version of the executables and library files, *
* together with instructions (in the manual page or equivalent) on where *
* to get the Standard Version. *
* *
* b) accompany the distribution with the machine-readable source of *
* the Package with your modifications. *
* *
* c) give non-standard executables non-standard names, and clearly *
* document the differences in manual pages (or equivalent), together *
* with instructions on where to get the Standard Version. *
* *
* d) make other distribution arrangements with the Copyright Holder. *
* *
* 5. You may charge a reasonable copying fee for any distribution of this *
* Package. You may charge any fee you choose for support of this *
* Package. You may not charge a fee for this Package itself. However, *
* you may distribute this Package in aggregate with other (possibly *
* commercial) programs as part of a larger (possibly commercial) software *
* distribution provided that you do not advertise this Package as a *
* product of your own. You may embed this Package's interpreter within *
* an executable of yours (by linking); this shall be construed as a mere *
* form of aggregation, provided that the complete Standard Version of the *
* interpreter is so embedded. *
* *
* 6. The scripts and library files supplied as input to or produced as *
* output from the programs of this Package do not automatically fall *
* under the copyright of this Package, but belong to whoever generated *
* them, and may be sold commercially, and may be aggregated with this *
* Package. If such scripts or library files are aggregated with this *
* Package via the so-called "undump" or "unexec" methods of producing a *
* binary executable image, then distribution of such an image shall *
* neither be construed as a distribution of this Package nor shall it *
* fall under the restrictions of Paragraphs 3 and 4, provided that you do *
* not represent such an executable image as a Standard Version of this *
* Package. *
* *
* 7. C subroutines (or comparably compiled subroutines in other *
* languages) supplied by you and linked into this Package in order to *
* emulate subroutines and variables of the language defined by this *
* Package shall not be considered part of this Package, but are the *
* equivalent of input as in Paragraph 6, provided these subroutines do *
* not change the language in any way that would cause it to fail the *
* regression tests for the language. *
* *
* 8. Aggregation of this Package with a commercial distribution is always *
* permitted provided that the use of this Package is embedded; that is, *
* when no overt attempt is made to make this Package's interfaces visible *
* to the end user of the commercial distribution. Such use shall not be *
* construed as a distribution of this Package. *
* *
* 9. The name of the Copyright Holder may not be used to endorse or promote *
* products derived from this software without specific prior written *
* permission. *
* *
* 10. THIS PACKAGE IS PROVIDED "AS IS" AND WITHOUT ANY EXPRESS OR *
* IMPLIED WARRANTIES, INCLUDING, WITHOUT LIMITATION, THE IMPLIED *
* WARRANTIES OF MERCHANTIBILITY AND FITNESS FOR A PARTICULAR PURPOSE. *
* *
* The End *
* *
\******************************************************************************/
#include "simplecudd.h"
typedef struct _extmanager {
DdManager *manager;
DdNode *t, *f;
hisqueue *his;
namedvars varmap;
} extmanager;
void DFS(extmanager MyManager, DdNode *Current);
int compexpand(extmanager MyManager, DdNode *Current, extmanager MyManager2, DdNode *Current2);
int bufstrcat(char *targetstr, int targetmem, const char *srcstr);
void getalltruepaths(extmanager MyManager, DdNode *Current, const char *startpath, const char *prevvar);
int main(int argc, char **arg) {
extmanager MyManager;
DdNode *bdd;
bddfileheader fileheader;
int code;
char yn;
code = -1;
if (argc != 2) {
fprintf(stderr, "\nUsage: %s [filename]\nGenerates and traverses a BDD from file\n", arg[0]);
fprintf(stderr, "\nUsage: %s -online\nGenerates and traverses a BDD online mode\n", arg[0]);
return code;
}
RAPIDLOADON;
if (strcmp("-online", arg[1]) == 0) {
MyManager.manager = simpleBDDinit(0);
MyManager.t = HIGH(MyManager.manager);
MyManager.f = LOW(MyManager.manager);
MyManager.varmap = InitNamedVars(1, 0);
bdd = OnlineGenerateBDD(MyManager.manager, &MyManager.varmap);
} else {
fileheader = ReadFileHeader(arg[1]);
switch(fileheader.filetype) {
case BDDFILE_SCRIPT:
MyManager.manager = simpleBDDinit(fileheader.varcnt);
MyManager.t = HIGH(MyManager.manager);
MyManager.f = LOW(MyManager.manager);
MyManager.varmap = InitNamedVars(fileheader.varcnt, fileheader.varstart);
bdd = FileGenerateBDD(MyManager.manager, MyManager.varmap, fileheader);
break;
case BDDFILE_NODEDUMP:
MyManager.manager = simpleBDDinit(fileheader.varcnt);
MyManager.t = HIGH(MyManager.manager);
MyManager.f = LOW(MyManager.manager);
MyManager.varmap = InitNamedVars(fileheader.varcnt, fileheader.varstart);
bdd = LoadNodeDump(MyManager.manager, MyManager.varmap, fileheader.inputfile);
break;
default:
fprintf(stderr, "Error: not a valid file format to load.\n");
return code;
break;
}
}
if (bdd != NULL) {
printf("Do you want to load parameter values from testdata.txt [y]? "); yn = getchar(); getchar();
if (yn == 'y') LoadVariableData(MyManager.varmap, "testdata.txt");
code = 0;
MyManager.his = InitHistory(GetVarCount(MyManager.manager));
if (strcmp("-online", arg[1]) != 0) {
DFS(MyManager, bdd);
printf("Do you need an export [y]? "); yn = getchar(); getchar();
if (yn == 'y') simpleNamedBDDtoDot(MyManager.manager, MyManager.varmap, bdd, "SimpleCUDDExport.dot");
printf("Do you want a save [y]? "); yn = getchar(); getchar();
if (yn == 'y') SaveNodeDump(MyManager.manager, MyManager.varmap, bdd, "SimpleCUDDSave.sav");
printf("Do you want to see all true paths [y]? "); yn = getchar(); getchar();
if (yn == 'y') {
ReInitHistory(MyManager.his, GetVarCount(MyManager.manager));
getalltruepaths(MyManager, bdd, "", "");
}
} else {
onlinetraverse(MyManager.manager, MyManager.varmap, MyManager.his, bdd);
}
}
if (MyManager.manager != NULL) KillBDD(MyManager.manager);
return code;
}
void DFS(extmanager MyManager, DdNode *Current) {
DdNode *h, *l;
hisnode *Found;
char *curnode;
curnode = GetNodeVarNameDisp(MyManager.manager, MyManager.varmap, Current);
if (GetIndex(Current) < MyManager.varmap.varcnt) {
printf("%s(%f,%i,%s)\n", curnode, MyManager.varmap.dvalue[GetIndex(Current)], MyManager.varmap.ivalue[GetIndex(Current)], MyManager.varmap.dynvalue[GetIndex(Current)]);
} else {
printf("%s\n", curnode);
}
if ((Current != MyManager.t) && (Current != MyManager.f) &&
((Found = GetNode(MyManager.his, MyManager.varmap.varstart, Current)) == NULL)) {
l = LowNodeOf(MyManager.manager, Current);
h = HighNodeOf(MyManager.manager, Current);
printf("l(%s)->", curnode);
DFS(MyManager, l);
printf("h(%s)->", curnode);
DFS(MyManager, h);
AddNode(MyManager.his, MyManager.varmap.varstart, Current, 0.0, 0, NULL);
}
}
void getalltruepaths(extmanager MyManager, DdNode *Current, const char *startpath, const char *prevvar) {
DdNode *h, *l;
char *curnode, *curpath;
int pathmaxsize = 1024;
curpath = (char *) malloc(sizeof(char) * pathmaxsize);
curpath[0] = '\0';
pathmaxsize = bufstrcat(curpath, pathmaxsize, startpath);
pathmaxsize = bufstrcat(curpath, pathmaxsize, prevvar);
pathmaxsize = bufstrcat(curpath, pathmaxsize, "*");
curnode = GetNodeVarNameDisp(MyManager.manager, MyManager.varmap, Current);
if (Current == MyManager.t) {
printf("%s\n", curpath);
} else if (Current != MyManager.f) {
h = HighNodeOf(MyManager.manager, Current);
if (h != MyManager.f) {
getalltruepaths(MyManager, h, curpath, curnode);
}
l = LowNodeOf(MyManager.manager, Current);
if (l != MyManager.f) {
pathmaxsize = bufstrcat(curpath, pathmaxsize, "~");
getalltruepaths(MyManager, l, curpath, curnode);
}
}
free(curpath);
}
int bufstrcat(char *targetstr, int targetmem, const char *srcstr) {
int strinc = strlen(srcstr), strsize = strlen(targetstr);
while ((strsize + strinc) > (targetmem - 1)) {
targetmem *= 2;
targetstr = (char *) realloc(targetstr, sizeof(char) * targetmem);
}
strcat(targetstr, srcstr);
return targetmem;
}

131
ProbLog/simplecudd/LICENCE Normal file
View File

@ -0,0 +1,131 @@
The "Artistic License"
Preamble
The intent of this document is to state the conditions under which a
Package may be copied, such that the Copyright Holder maintains some
semblance of artistic control over the development of the package,
while giving the users of the package the right to use and distribute
the Package in a more-or-less customary fashion, plus the right to make
reasonable modifications.
Definitions:
"Package" refers to the collection of files distributed by the
Copyright Holder, and derivatives of that collection of files
created through textual modification.
"Standard Version" refers to such a Package if it has not been
modified, or has been modified in accordance with the wishes
of the Copyright Holder as specified below.
"Copyright Holder" is whoever is named in the copyright or
copyrights for the package.
"You" is you, if you're thinking about copying or distributing
this Package.
"Reasonable copying fee" is whatever you can justify on the
basis of media cost, duplication charges, time of people involved,
and so on. (You will not be required to justify it to the
Copyright Holder, but only to the computing community at large
as a market that must bear the fee.)
"Freely Available" means that no fee is charged for the item
itself, though there may be fees involved in handling the item.
It also means that recipients of the item may redistribute it
under the same conditions they received it.
1. You may make and give away verbatim copies of the source form of the
Standard Version of this Package without restriction, provided that you
duplicate all of the original copyright notices and associated disclaimers.
2. You may apply bug fixes, portability fixes and other modifications
derived from the Public Domain or from the Copyright Holder. A Package
modified in such a way shall still be considered the Standard Version.
3. You may otherwise modify your copy of this Package in any way, provided
that you insert a prominent notice in each changed file stating how and
when you changed that file, and provided that you do at least ONE of the
following:
a) place your modifications in the Public Domain or otherwise make them
Freely Available, such as by posting said modifications to Usenet or
an equivalent medium, or placing the modifications on a major archive
site such as uunet.uu.net, or by allowing the Copyright Holder to include
your modifications in the Standard Version of the Package.
b) use the modified Package only within your corporation or organization.
c) rename any non-standard executables so the names do not conflict
with standard executables, which must also be provided, and provide
a separate manual page for each non-standard executable that clearly
documents how it differs from the Standard Version.
d) make other distribution arrangements with the Copyright Holder.
4. You may distribute the programs of this Package in object code or
executable form, provided that you do at least ONE of the following:
a) distribute a Standard Version of the executables and library files,
together with instructions (in the manual page or equivalent) on where
to get the Standard Version.
b) accompany the distribution with the machine-readable source of
the Package with your modifications.
c) give non-standard executables non-standard names, and clearly
document the differences in manual pages (or equivalent), together
with instructions on where to get the Standard Version.
d) make other distribution arrangements with the Copyright Holder.
5. You may charge a reasonable copying fee for any distribution of this
Package. You may charge any fee you choose for support of this
Package. You may not charge a fee for this Package itself. However,
you may distribute this Package in aggregate with other (possibly
commercial) programs as part of a larger (possibly commercial) software
distribution provided that you do not advertise this Package as a
product of your own. You may embed this Package's interpreter within
an executable of yours (by linking); this shall be construed as a mere
form of aggregation, provided that the complete Standard Version of the
interpreter is so embedded.
6. The scripts and library files supplied as input to or produced as
output from the programs of this Package do not automatically fall
under the copyright of this Package, but belong to whoever generated
them, and may be sold commercially, and may be aggregated with this
Package. If such scripts or library files are aggregated with this
Package via the so-called "undump" or "unexec" methods of producing a
binary executable image, then distribution of such an image shall
neither be construed as a distribution of this Package nor shall it
fall under the restrictions of Paragraphs 3 and 4, provided that you do
not represent such an executable image as a Standard Version of this
Package.
7. C subroutines (or comparably compiled subroutines in other
languages) supplied by you and linked into this Package in order to
emulate subroutines and variables of the language defined by this
Package shall not be considered part of this Package, but are the
equivalent of input as in Paragraph 6, provided these subroutines do
not change the language in any way that would cause it to fail the
regression tests for the language.
8. Aggregation of this Package with a commercial distribution is always
permitted provided that the use of this Package is embedded; that is,
when no overt attempt is made to make this Package's interfaces visible
to the end user of the commercial distribution. Such use shall not be
construed as a distribution of this Package.
9. The name of the Copyright Holder may not be used to endorse or promote
products derived from this software without specific prior written permission.
10. THIS PACKAGE IS PROVIDED "AS IS" AND WITHOUT ANY EXPRESS OR
IMPLIED WARRANTIES, INCLUDING, WITHOUT LIMITATION, THE IMPLIED
WARRANTIES OF MERCHANTIBILITY AND FITNESS FOR A PARTICULAR PURPOSE.
The End

View File

@ -0,0 +1,34 @@
CUDD = cudd-2.4.1
DYNAMIC =
FLAGS =
INCLUDE = -I $(CUDD)/include
LINKFLAGS = -lm
LINKLIBS = $(CUDD)/cudd/libcudd.a $(CUDD)/mtr/libmtr.a $(CUDD)/st/libst.a $(CUDD)/util/libutil.a $(CUDD)/epd/libepd.a
default: makecudd example problog
example: Example.o simplecudd.o general.o
@echo Making Example...
@echo Copyright T. Mantadelis and Katholieke Universiteit Leuven 2008
gcc Example.o simplecudd.o general.o $(LINKLIBS) $(LINKFLAGS) -o Example
problog: ProblogBDD.o simplecudd.o general.o
@echo Making ProblogBDD...
@echo Copyright T. Mantadelis, A. Kimmig, B. Gutmann and Katholieke Universiteit Leuven 2008
gcc ProblogBDD.o simplecudd.o general.o $(LINKLIBS) $(LINKFLAGS) -o ProblogBDD
makecudd:
@(cd $(CUDD); \
echo Making cudd...; \
make)
%.o : %.c
gcc $(FLAGS) $(INCLUDE) $(DYNAMIC) -c $<
clean: cleancudd
rm -f *.o ProblogBDD Example
cleancudd:
@(cd $(CUDD); \
echo Cleaning cudd...; \
make clean)

View File

@ -0,0 +1,670 @@
/******************************************************************************\
* *
* SimpleCUDD library (www.cs.kuleuven.be/~theo/tools/simplecudd.html) *
* SimpleCUDD was developed at Katholieke Universiteit Leuven(www.kuleuven.be) *
* *
* Copyright T. Mantadelis, A. Kimmig, B. Gutmann *
* and Katholieke Universiteit Leuven 2008 *
* *
* Author: Theofrastos Mantadelis, Angelika Kimmig, Bernd Gutmann *
* File: ProblogBDD.c *
* *
********************************************************************************
* *
* The "Artistic License" *
* *
* Preamble *
* *
* The intent of this document is to state the conditions under which a *
* Package may be copied, such that the Copyright Holder maintains some *
* semblance of artistic control over the development of the package, *
* while giving the users of the package the right to use and distribute *
* the Package in a more-or-less customary fashion, plus the right to make *
* reasonable modifications. *
* *
* Definitions: *
* *
* "Package" refers to the collection of files distributed by the *
* Copyright Holder, and derivatives of that collection of files *
* created through textual modification. *
* *
* "Standard Version" refers to such a Package if it has not been *
* modified, or has been modified in accordance with the wishes *
* of the Copyright Holder as specified below. *
* *
* "Copyright Holder" is whoever is named in the copyright or *
* copyrights for the package. *
* *
* "You" is you, if you're thinking about copying or distributing *
* this Package. *
* *
* "Reasonable copying fee" is whatever you can justify on the *
* basis of media cost, duplication charges, time of people involved, *
* and so on. (You will not be required to justify it to the *
* Copyright Holder, but only to the computing community at large *
* as a market that must bear the fee.) *
* *
* "Freely Available" means that no fee is charged for the item *
* itself, though there may be fees involved in handling the item. *
* It also means that recipients of the item may redistribute it *
* under the same conditions they received it. *
* *
* 1. You may make and give away verbatim copies of the source form of the *
* Standard Version of this Package without restriction, provided that you *
* duplicate all of the original copyright notices and associated disclaimers. *
* *
* 2. You may apply bug fixes, portability fixes and other modifications *
* derived from the Public Domain or from the Copyright Holder. A Package *
* modified in such a way shall still be considered the Standard Version. *
* *
* 3. You may otherwise modify your copy of this Package in any way, provided *
* that you insert a prominent notice in each changed file stating how and *
* when you changed that file, and provided that you do at least ONE of the *
* following: *
* *
* a) place your modifications in the Public Domain or otherwise make them *
* Freely Available, such as by posting said modifications to Usenet or *
* an equivalent medium, or placing the modifications on a major archive *
* site such as uunet.uu.net, or by allowing the Copyright Holder to include *
* your modifications in the Standard Version of the Package. *
* *
* b) use the modified Package only within your corporation or organization. *
* *
* c) rename any non-standard executables so the names do not conflict *
* with standard executables, which must also be provided, and provide *
* a separate manual page for each non-standard executable that clearly *
* documents how it differs from the Standard Version. *
* *
* d) make other distribution arrangements with the Copyright Holder. *
* *
* 4. You may distribute the programs of this Package in object code or *
* executable form, provided that you do at least ONE of the following: *
* *
* a) distribute a Standard Version of the executables and library files, *
* together with instructions (in the manual page or equivalent) on where *
* to get the Standard Version. *
* *
* b) accompany the distribution with the machine-readable source of *
* the Package with your modifications. *
* *
* c) give non-standard executables non-standard names, and clearly *
* document the differences in manual pages (or equivalent), together *
* with instructions on where to get the Standard Version. *
* *
* d) make other distribution arrangements with the Copyright Holder. *
* *
* 5. You may charge a reasonable copying fee for any distribution of this *
* Package. You may charge any fee you choose for support of this *
* Package. You may not charge a fee for this Package itself. However, *
* you may distribute this Package in aggregate with other (possibly *
* commercial) programs as part of a larger (possibly commercial) software *
* distribution provided that you do not advertise this Package as a *
* product of your own. You may embed this Package's interpreter within *
* an executable of yours (by linking); this shall be construed as a mere *
* form of aggregation, provided that the complete Standard Version of the *
* interpreter is so embedded. *
* *
* 6. The scripts and library files supplied as input to or produced as *
* output from the programs of this Package do not automatically fall *
* under the copyright of this Package, but belong to whoever generated *
* them, and may be sold commercially, and may be aggregated with this *
* Package. If such scripts or library files are aggregated with this *
* Package via the so-called "undump" or "unexec" methods of producing a *
* binary executable image, then distribution of such an image shall *
* neither be construed as a distribution of this Package nor shall it *
* fall under the restrictions of Paragraphs 3 and 4, provided that you do *
* not represent such an executable image as a Standard Version of this *
* Package. *
* *
* 7. C subroutines (or comparably compiled subroutines in other *
* languages) supplied by you and linked into this Package in order to *
* emulate subroutines and variables of the language defined by this *
* Package shall not be considered part of this Package, but are the *
* equivalent of input as in Paragraph 6, provided these subroutines do *
* not change the language in any way that would cause it to fail the *
* regression tests for the language. *
* *
* 8. Aggregation of this Package with a commercial distribution is always *
* permitted provided that the use of this Package is embedded; that is, *
* when no overt attempt is made to make this Package's interfaces visible *
* to the end user of the commercial distribution. Such use shall not be *
* construed as a distribution of this Package. *
* *
* 9. The name of the Copyright Holder may not be used to endorse or promote *
* products derived from this software without specific prior written *
* permission. *
* *
* 10. THIS PACKAGE IS PROVIDED "AS IS" AND WITHOUT ANY EXPRESS OR *
* IMPLIED WARRANTIES, INCLUDING, WITHOUT LIMITATION, THE IMPLIED *
* WARRANTIES OF MERCHANTIBILITY AND FITNESS FOR A PARTICULAR PURPOSE. *
* *
* The End *
* *
\******************************************************************************/
#include "simplecudd.h"
#include <signal.h>
typedef struct _parameters {
int loadfile;
int savedfile;
int exportfile;
int inputfile;
int debug;
int errorcnt;
int *error;
int method;
int queryid;
int timeout;
double sigmoid_slope;
int online;
int maxbufsize;
char *ppid;
} parameters;
typedef struct _gradientpair {
double probability;
double gradient;
} gradientpair;
typedef struct _extmanager {
DdManager *manager;
DdNode *t, *f;
hisqueue *his;
namedvars varmap;
} extmanager;
int argtype(const char *arg);
void printhelp(int argc, char **arg);
parameters loadparam(int argc, char **arg);
parameters params;
void handler(int num);
void pidhandler(int num);
void termhandler(int num);
double sigmoid(double x, double slope);
void myexpand(extmanager MyManager, DdNode *Current);
double CalcProbability(extmanager MyManager, DdNode *Current);
double CalcProbabilitySigmoid(extmanager MyManager, DdNode *Current);
gradientpair CalcGradient(extmanager MyManager, DdNode *Current, int TargetVar, char *TargetPattern);
int patterncalculated(char *pattern, extmanager MyManager, int loc);
char * extractpattern(char *thestr);
int main(int argc, char **arg) {
extmanager MyManager;
DdNode *bdd;
bddfileheader fileheader;
int i, ivarcnt, code;
gradientpair tvalue;
double probability = -1.0;
char *varpattern;
varpattern = NULL;
code = -1;
params = loadparam(argc, arg);
if (params.errorcnt > 0) {
printhelp(argc, arg);
for (i = 0; i < params.errorcnt; i++) {
fprintf(stderr, "Error: not known or error at parameter %s.\n", arg[params.error[i]]);
}
return -1;
}
if (params.online == 0 && params.loadfile == -1) {
printhelp(argc, arg);
fprintf(stderr, "Error: you must specify a loading file.\n");
return -1;
}
if (params.method != 0 && arg[params.method][0] != 'g' && arg[params.method][0] != 'p' && arg[params.method][0] != 'o') {
printhelp(argc, arg);
fprintf(stderr, "Error: you must choose a calculation method beetween [p]robability, [g]radient, [o]nline.\n");
return -1;
}
if (params.debug) DEBUGON;
RAPIDLOADON;
SETMAXBUFSIZE(params.maxbufsize);
signal(SIGINT, termhandler);
if (params.ppid != NULL) {
signal(SIGALRM, pidhandler);
alarm(5);
} else {
signal(SIGALRM, handler);
alarm(params.timeout);
}
if (params.online) {
MyManager.manager = simpleBDDinit(0);
MyManager.t = HIGH(MyManager.manager);
MyManager.f = LOW(MyManager.manager);
MyManager.varmap = InitNamedVars(1, 0);
bdd = OnlineGenerateBDD(MyManager.manager, &MyManager.varmap);
ivarcnt = GetVarCount(MyManager.manager);
} else {
fileheader = ReadFileHeader(arg[params.loadfile]);
switch(fileheader.filetype) {
case BDDFILE_SCRIPT:
if (params.inputfile == -1) {
printhelp(argc, arg);
fprintf(stderr, "Error: an input file is necessary for this type of loading file.\n");
return -1;
}
MyManager.manager = simpleBDDinit(fileheader.varcnt);
MyManager.t = HIGH(MyManager.manager);
MyManager.f = LOW(MyManager.manager);
MyManager.varmap = InitNamedVars(fileheader.varcnt, fileheader.varstart);
bdd = FileGenerateBDD(MyManager.manager, MyManager.varmap, fileheader);
ivarcnt = fileheader.varcnt;
break;
case BDDFILE_NODEDUMP:
if (params.inputfile == -1) {
printhelp(argc, arg);
fprintf(stderr, "Error: an input file is necessary for this type of loading file.\n");
return -1;
}
MyManager.manager = simpleBDDinit(fileheader.varcnt);
MyManager.t = HIGH(MyManager.manager);
MyManager.f = LOW(MyManager.manager);
MyManager.varmap = InitNamedVars(fileheader.varcnt, fileheader.varstart);
bdd = LoadNodeDump(MyManager.manager, MyManager.varmap, fileheader.inputfile);
ivarcnt = fileheader.varcnt;
break;
default:
fprintf(stderr, "Error: not a valid file format to load.\n");
return -1;
break;
}
}
alarm(0);
// problem specifics
if (bdd != NULL) {
ivarcnt = RepairVarcnt(&MyManager.varmap);
code = 0;
if (params.inputfile != -1) {
if (LoadVariableData(MyManager.varmap, arg[params.inputfile]) == -1) return -1;
if (!all_loaded(MyManager.varmap, 1)) return -1;
}
MyManager.his = InitHistory(ivarcnt);
if (params.method != 0) {
switch(arg[params.method][0]) {
case 'g':
for (i = 0; i < MyManager.varmap.varcnt; i++) {
if (MyManager.varmap.vars[i] != NULL) {
varpattern = extractpattern(MyManager.varmap.vars[i]);
if ((varpattern == NULL) || (!patterncalculated(varpattern, MyManager, i))) {
tvalue = CalcGradient(MyManager, bdd, i + MyManager.varmap.varstart, varpattern);
probability = tvalue.probability;
double factor = sigmoid(MyManager.varmap.dvalue[i], params.sigmoid_slope) * (1 - sigmoid(MyManager.varmap.dvalue[i], params.sigmoid_slope)) * params.sigmoid_slope;
if (varpattern == NULL) {
printf("query_gradient(%s,%s,%1.12f).\n", arg[params.queryid], MyManager.varmap.vars[i], tvalue.gradient * factor);
} else {
varpattern[strlen(varpattern) - 2] = '\0';
printf("query_gradient(%s,%s,%1.12f).\n", arg[params.queryid], varpattern, tvalue.gradient * factor);
}
ReInitHistory(MyManager.his, MyManager.varmap.varcnt);
}
if (varpattern != NULL) free(varpattern);
} else {
fprintf(stderr, "Error: no variable name given for parameter.\n");
}
}
if (probability < 0.0) {
// no nodes, so we have to calculate probability ourself
tvalue = CalcGradient(MyManager, bdd, 0 + MyManager.varmap.varstart, NULL);
probability = tvalue.probability;
}
printf("query_probability(%s,%1.12f).\n", arg[params.queryid], probability);
break;
case 'p':
printf("probability(%1.12f).\n", CalcProbability(MyManager, bdd));
break;
case 'o':
onlinetraverse(MyManager.manager, MyManager.varmap, MyManager.his, bdd);
break;
default:
myexpand(MyManager, bdd);
break;
}
} else {
myexpand(MyManager, bdd);
}
if (params.savedfile > -1) SaveNodeDump(MyManager.manager, MyManager.varmap, bdd, arg[params.savedfile]);
if (params.exportfile > -1) simpleNamedBDDtoDot(MyManager.manager, MyManager.varmap, bdd, arg[params.exportfile]);
ReInitHistory(MyManager.his, MyManager.varmap.varcnt);
free(MyManager.his);
}
if (MyManager.manager != NULL) {
KillBDD(MyManager.manager);
free(MyManager.varmap.dvalue);
free(MyManager.varmap.ivalue);
free(MyManager.varmap.dynvalue);
for (i = 0; i < MyManager.varmap.varcnt; i++)
free(MyManager.varmap.vars[i]);
free(MyManager.varmap.vars);
}
if (params.error != NULL) free(params.error);
return code;
}
/* Shell Parameters handling */
int argtype(const char *arg) {
if (strcmp(arg, "-l") == 0 || strcmp(arg, "--load") == 0) return 0;
if (strcmp(arg, "-e") == 0 || strcmp(arg, "--export") == 0) return 2;
if (strcmp(arg, "-m") == 0 || strcmp(arg, "--method") == 0) return 3;
if (strcmp(arg, "-i") == 0 || strcmp(arg, "--input") == 0) return 4;
if (strcmp(arg, "-h") == 0 || strcmp(arg, "--help") == 0) return 5;
if (strcmp(arg, "-d") == 0 || strcmp(arg, "--debug") == 0) return 6;
if (strcmp(arg, "-id") == 0 || strcmp(arg, "--queryid") == 0) return 7;
if (strcmp(arg, "-t") == 0 || strcmp(arg, "--timeout") == 0) return 8;
if (strcmp(arg, "-sd") == 0 || strcmp(arg, "--savedump") == 0) return 9;
if (strcmp(arg, "-sl") == 0 || strcmp(arg, "--slope") == 0) return 10;
if (strcmp(arg, "-o") == 0 || strcmp(arg, "--online") == 0) return 11;
if (strcmp(arg, "-bs") == 0 || strcmp(arg, "--bufsize") == 0) return 12;
if (strcmp(arg, "-pid") == 0 || strcmp(arg, "--pid") == 0) return 13;
return -1;
}
void printhelp(int argc, char **arg) {
fprintf(stderr, "\nUsage: %s -l [filename] -i [filename] -o (-s(d) [filename] -e [filename] -m [method] -id [queryid] -sl [double]) (-t [seconds] -d -h)\n", arg[0]);
fprintf(stderr, "Generates and traverses a BDD\nMandatory parameters:\n");
fprintf(stderr, "\t-l [filename]\t->\tfilename to load supports two formats:\n\t\t\t\t\t\t1. script with generation instructions\n\t\t\t\t\t\t2. node dump saved file\n");
fprintf(stderr, "\t-i [filename]\t->\tfilename to input problem specifics (mandatory with file formats 1, 2)\n");
fprintf(stderr, "\t-o\t\t->\tgenerates the BDD in online mode instead from a file can be used instead of -l\n");
fprintf(stderr, "Optional parameters:\n");
fprintf(stderr, "\t-sd [filename]\t->\tfilename to save generated BDD in node dump format (fast loading, traverse valid only)\n");
fprintf(stderr, "\t-e [filename]\t->\tfilename to export generated BDD in dot format\n");
fprintf(stderr, "\t-m [method]\t->\tthe calculation method to be used: none(default), [p]robability, [g]radient, [o]nline\n");
fprintf(stderr, "\t-id [queryid]\t->\tthe queries identity name (used by gradient) default: %s\n", arg[0]);
fprintf(stderr, "\t-sl [double]\t->\tthe sigmoid slope (used by gradient) default: 1.0\n");
fprintf(stderr, "Extra parameters:\n");
fprintf(stderr, "\t-t [seconds]\t->\tthe seconds (int) for BDD generation timeout default 0 = no timeout\n");
fprintf(stderr, "\t-pid [pid]\t->\ta process id (int) to check for termination default 0 = no process to check works only under POSIX OS\n");
fprintf(stderr, "\t-bs [bytes]\t->\tthe bytes (int) to use as a maximum buffer size to read files default 0 = no max\n");
fprintf(stderr, "\t-d\t\t->\tRun in debug mode (gives extra messages in stderr)\n");
fprintf(stderr, "\t-h\t\t->\tHelp (displays this message)\n\n");
fprintf(stderr, "Example: %s -l testbdd -i input.txt -m g -id testbdd\n", arg[0]);
}
parameters loadparam(int argc, char **arg) {
int i;
parameters params;
params.loadfile = -1;
params.savedfile = -1;
params.exportfile = -1;
params.method = 0;
params.inputfile = -1;
params.debug = 0;
params.errorcnt = 0;
params.queryid = 0;
params.timeout = 0;
params.sigmoid_slope = 1.0;
params.online = 0;
params.maxbufsize = 0;
params.ppid = NULL;
params.error = (int *) malloc(argc * sizeof(int));
for (i = 1; i < argc; i++) {
switch(argtype(arg[i])) {
case 0:
if (argc > i + 1) {
i++;
params.loadfile = i;
} else {
params.error[params.errorcnt] = i;
params.errorcnt++;
}
break;
case 2:
if (argc > i + 1) {
i++;
params.exportfile = i;
} else {
params.error[params.errorcnt] = i;
params.errorcnt++;
}
break;
case 3:
if (argc > i + 1) {
i++;
params.method = i;
} else {
params.error[params.errorcnt] = i;
params.errorcnt++;
}
break;
case 4:
if (argc > i + 1) {
i++;
params.inputfile = i;
} else {
params.error[params.errorcnt] = i;
params.errorcnt++;
}
break;
case 5:
printhelp(argc, arg);
break;
case 6:
params.debug = 1;
break;
case 7:
if (argc > i + 1) {
i++;
params.queryid = i;
} else {
params.error[params.errorcnt] = i;
params.errorcnt++;
}
break;
case 8:
if ((argc > i + 1) && (IsPosNumber(arg[i + 1]))) {
i++;
params.timeout = atoi(arg[i]);
} else {
params.error[params.errorcnt] = i;
params.errorcnt++;
}
break;
case 9:
if (argc > i + 1) {
i++;
params.savedfile = i;
} else {
params.error[params.errorcnt] = i;
params.errorcnt++;
}
break;
case 10:
if ((argc > i + 1) && (IsRealNumber(arg[i + 1]))) {
i++;
params.sigmoid_slope = atof(arg[i]);
} else {
params.error[params.errorcnt] = i;
params.errorcnt++;
}
break;
case 11:
params.online = 1;
break;
case 12:
if ((argc > i + 1) && (IsPosNumber(arg[i + 1]))) {
i++;
params.maxbufsize = atoi(arg[i]);
} else {
params.error[params.errorcnt] = i;
params.errorcnt++;
}
break;
case 13:
if ((argc > i + 1) && (IsPosNumber(arg[i + 1]))) {
i++;
params.ppid = (char *) malloc(sizeof(char) * (strlen(arg[i]) + 1));
strcpy(params.ppid, arg[i]);
} else {
params.error[params.errorcnt] = i;
params.errorcnt++;
}
break;
default:
params.error[params.errorcnt] = i;
params.errorcnt++;
break;
}
}
return params;
}
/* Error Handlers */
void handler(int num) {
fprintf(stderr, "Error: Timeout %i exceeded.\n", params.timeout);
exit(-1);
}
void pidhandler(int num) {
char *s;
if (params.timeout > 0) {
params.timeout -= 5;
if (params.timeout <= 0) {
fprintf(stderr, "Error: Timeout exceeded.\n");
exit(-1);
}
}
s = (char *) malloc(sizeof(char) * (19 + strlen(params.ppid)));
strcpy(s, "ps "); strcat(s, params.ppid); strcat(s, " >/dev/null");
if (system(s) != 0) exit(4);
signal(SIGALRM, pidhandler);
alarm(5);
free(s);
}
void termhandler(int num) {
exit(3);
}
/* General Functions */
double sigmoid(double x, double slope) {
return 1 / (1 + exp(-x * slope));
}
/* Debugging traverse function */
void myexpand(extmanager MyManager, DdNode *Current) {
DdNode *h, *l;
hisnode *Found;
char *curnode;
curnode = GetNodeVarNameDisp(MyManager.manager, MyManager.varmap, Current);
printf("%s\n", curnode);
if ((Current != MyManager.t) && (Current != MyManager.f) &&
((Found = GetNode(MyManager.his, MyManager.varmap.varstart, Current)) == NULL)) {
l = LowNodeOf(MyManager.manager, Current);
h = HighNodeOf(MyManager.manager, Current);
printf("l(%s)->", curnode);
myexpand(MyManager, l);
printf("h(%s)->", curnode);
myexpand(MyManager, h);
AddNode(MyManager.his, MyManager.varmap.varstart, Current, 0.0, 0, NULL);
}
}
/* Angelikas Algorithm */
double CalcProbability(extmanager MyManager, DdNode *Current) {
DdNode *h, *l;
hisnode *Found;
char *curnode;
double lvalue, hvalue, tvalue;
if (params.debug) {
curnode = GetNodeVarNameDisp(MyManager.manager, MyManager.varmap, Current);
fprintf(stderr, "%s\n", curnode);
}
if (Current == MyManager.t) return 1.0;
if (Current == MyManager.f) return 0.0;
if ((Found = GetNode(MyManager.his, MyManager.varmap.varstart, Current)) != NULL) return Found->dvalue;
l = LowNodeOf(MyManager.manager, Current);
h = HighNodeOf(MyManager.manager, Current);
if (params.debug) fprintf(stderr, "l(%s)->", curnode);
lvalue = CalcProbability(MyManager, l);
if (params.debug) fprintf(stderr, "h(%s)->", curnode);
hvalue = CalcProbability(MyManager, h);
tvalue = MyManager.varmap.dvalue[GetIndex(Current) - MyManager.varmap.varstart];
tvalue = tvalue * hvalue + lvalue * (1.0 - tvalue);
AddNode(MyManager.his, MyManager.varmap.varstart, Current, tvalue, 0, NULL);
return tvalue;
}
/* Bernds Algorithm */
gradientpair CalcGradient(extmanager MyManager, DdNode *Current, int TargetVar, char *TargetPattern) {
DdNode *h, *l;
hisnode *Found;
char *curnode;
gradientpair lvalue, hvalue, tvalue;
double this_probability;
double *gradient;
if (params.debug) {
curnode = GetNodeVarNameDisp(MyManager.manager, MyManager.varmap, Current);
fprintf(stderr, "%s\n", curnode);
}
if (Current == MyManager.t) {
tvalue.probability = 1.0;
tvalue.gradient = 0.0;
return tvalue;
}
if (Current == MyManager.f) {
tvalue.probability = 0.0;
tvalue.gradient = 0.0;
return tvalue;
}
if ((Found = GetNode(MyManager.his, MyManager.varmap.varstart, Current)) != NULL) {
tvalue.probability = Found->dvalue;
tvalue.gradient = *((double *) Found->dynvalue);
return tvalue;
}
l = LowNodeOf(MyManager.manager, Current);
h = HighNodeOf(MyManager.manager, Current);
if (params.debug) fprintf(stderr, "l(%s)->", curnode);
lvalue = CalcGradient(MyManager, l, TargetVar, TargetPattern);
if (params.debug) fprintf(stderr, "h(%s)->", curnode);
hvalue = CalcGradient(MyManager, h, TargetVar, TargetPattern);
this_probability = sigmoid(MyManager.varmap.dvalue[GetIndex(Current) - MyManager.varmap.varstart], params.sigmoid_slope);
tvalue.probability = this_probability * hvalue.probability + (1 - this_probability) * lvalue.probability;
tvalue.gradient = this_probability * hvalue.gradient + (1 - this_probability) * lvalue.gradient;
if ((GetIndex(Current) == TargetVar) ||
((TargetPattern != NULL) && patternmatch(TargetPattern, MyManager.varmap.vars[GetIndex(Current)]))) {
tvalue.gradient += hvalue.probability - lvalue.probability;
}
gradient = (double *) malloc(sizeof(double));
*gradient = tvalue.gradient;
AddNode(MyManager.his, MyManager.varmap.varstart, Current, tvalue.probability, 0, gradient);
return tvalue;
}
char * extractpattern(char *thestr) {
char *p;
int i = 0, sl = strlen(thestr);
while((thestr[i] != '_') && (i < sl)) i++;
if (i == sl) return NULL;
i++;
p = (char *) malloc(sizeof(char) * (i + 2));
strncpy(p, thestr, i);
p[i] = '*';
p[i + 1] = '\0';
return p;
}
int patterncalculated(char *pattern, extmanager MyManager, int loc) {
int i;
if (pattern == NULL) return 0;
for (i = loc - 1; i > -1; i--)
if (patternmatch(pattern, MyManager.varmap.vars[i])) return 1;
return 0;
}

View File

@ -0,0 +1,141 @@
:-use_module(library(system)).
%:-use_module(library(clib)).
bdd_init(FDO, FDI, PID):-
exec('/home/theo/BDDs/SimpleCUDD/Version4/Example -online', [pipe(FDO), pipe(FDI), std], PID).
%process_create('/home/theo/BDDs/SimpleCUDD/Version3/Example', ['-online'], [stdin(pipe(FDI)), stdout(pipe(FDO)), process(PID)]).
bdd_commit(FDO, LINE):-
write(FDO, LINE),
write(FDO, '\n').
bdd_kill(FDO, FDI, PID, S):-
bdd_commit(FDO, '@e'),
wait(PID, S),
%process_wait(PID, S),
close(FDO),
close(FDI).
bdd_line([], X, _, L):-
atomic(X),
X \= [],
(bdd_curinter(N) ->
retract(bdd_curinter(N))
;
N = 1
),
M is N + 1,
assert(bdd_curinter(M)),
atomic_concat(['L', N, '=', X], L).
bdd_line(L, X, O, NL):-
atomic(X),
X \= [],
atom(L),
L \= [],
atomic_concat([L, O, X], NL).
bdd_line(L, [], _, L):-!.
bdd_line(L, [X|T], O, R):-
bdd_line(L, X, O, NL),
bdd_line(NL, T, O, R).
bdd_AND(L, X, NL):-
bdd_line(L, X, '*', NL).
bdd_OR(L, X, NL):-
bdd_line(L, X, '+', NL).
bdd_XOR(L, X, NL):-
bdd_line(L, X, '#', NL).
bdd_NAND(L, X, NL):-
bdd_line(L, X, '~*', NL).
bdd_NOR(L, X, NL):-
bdd_line(L, X, '~+', NL).
bdd_XNOR(L, X, NL):-
bdd_line(L, X, '~#', NL).
bdd_not(X, NX):-
atomic(X),
atomic_concat(['~', X], NX).
bdd_laststep(L):-
bdd_curinter(N),
M is N - 1,
atomic_concat(['L', M], L),
!.
bdd_nextDFS(FDO):-
bdd_commit(FDO, '@n').
bdd_nextBFS(FDO):-
bdd_commit(FDO, '@n,BFS').
bdd_current(FDO, FDI, N, Qcnt):-
bdd_commit(FDO, '@c'),
read(FDI, F),
assert(F),
bdd_temp_value(N, Qcnt),
retract(F).
bdd_highnodeof(FDO, FDI, H):-
bdd_commit(FDO, '@h'),
read(FDI, F),
assert(F),
bdd_temp_value(H),
retract(F).
bdd_lownodeof(FDO, FDI, L):-
bdd_commit(FDO, '@l'),
read(FDI, F),
assert(F),
bdd_temp_value(L),
retract(F).
bdd_nodevaluesof(FDO, FDI, N, V):-
atomic_concat(['@v,', N], Q),
bdd_commit(FDO, Q),
read(FDI, F),
assert(F),
bdd_temp_value(V),
retract(F).
/*
bdd_addnodetohis(FDO, N, [D, I, Dyn]):-
atomic_concat(['@a,', N, ',', D, ',', I, ',', Dyn], Q),
bdd_commit(FDO, Q).
bdd_getnodefromhis(FDO, FDI, N, V):-
atomic_concat(['@g,', N], Q),
bdd_commit(FDO, Q),
read(FDI, F),
assert(F),
bdd_temp_value(V),
retract(F).
*/
runme:-
bdd_init(FDO, FDI, PID),
bdd_AND([], ['A', 'B', 'C', 'D', 'E'], L1),
bdd_laststep(L1S),
bdd_commit(FDO, L1),
bdd_AND([], ['A', 'F', 'G', '~B'], L2),
bdd_laststep(L2S),
bdd_commit(FDO, L2),
bdd_AND([], ['A', 'F', 'G', '~C'], L3),
bdd_laststep(L3S),
bdd_commit(FDO, L3),
bdd_OR([], [L1S, L2S, L3S], L4),
bdd_laststep(L4S),
bdd_commit(FDO, L4),
bdd_commit(FDO, L4S),
repeat,
bdd_current(FDO, FDI, N, I),
write(1),nl,
bdd_nodevaluesof(FDO, FDI, N, V),
write(N), write(' ('), write(V), write(')'), nl,
bdd_next(FDO),
I = 0, (N = 'TRUE' ; N = 'FALSE'),
bdd_kill(FDO, FDI, PID, S),
write('BDD terminated with state: '), write(S), nl.

View File

@ -0,0 +1,234 @@
/******************************************************************************\
* *
* SimpleCUDD library (www.cs.kuleuven.be/~theo/tools/simplecudd.html) *
* SimpleCUDD was developed at Katholieke Universiteit Leuven(www.kuleuven.be) *
* *
* Copyright T. Mantadelis and Katholieke Universiteit Leuven 2008 *
* *
* Author: Theofrastos Mantadelis *
* File: general.c *
* *
********************************************************************************
* *
* The "Artistic License" *
* *
* Preamble *
* *
* The intent of this document is to state the conditions under which a *
* Package may be copied, such that the Copyright Holder maintains some *
* semblance of artistic control over the development of the package, *
* while giving the users of the package the right to use and distribute *
* the Package in a more-or-less customary fashion, plus the right to make *
* reasonable modifications. *
* *
* Definitions: *
* *
* "Package" refers to the collection of files distributed by the *
* Copyright Holder, and derivatives of that collection of files *
* created through textual modification. *
* *
* "Standard Version" refers to such a Package if it has not been *
* modified, or has been modified in accordance with the wishes *
* of the Copyright Holder as specified below. *
* *
* "Copyright Holder" is whoever is named in the copyright or *
* copyrights for the package. *
* *
* "You" is you, if you're thinking about copying or distributing *
* this Package. *
* *
* "Reasonable copying fee" is whatever you can justify on the *
* basis of media cost, duplication charges, time of people involved, *
* and so on. (You will not be required to justify it to the *
* Copyright Holder, but only to the computing community at large *
* as a market that must bear the fee.) *
* *
* "Freely Available" means that no fee is charged for the item *
* itself, though there may be fees involved in handling the item. *
* It also means that recipients of the item may redistribute it *
* under the same conditions they received it. *
* *
* 1. You may make and give away verbatim copies of the source form of the *
* Standard Version of this Package without restriction, provided that you *
* duplicate all of the original copyright notices and associated disclaimers. *
* *
* 2. You may apply bug fixes, portability fixes and other modifications *
* derived from the Public Domain or from the Copyright Holder. A Package *
* modified in such a way shall still be considered the Standard Version. *
* *
* 3. You may otherwise modify your copy of this Package in any way, provided *
* that you insert a prominent notice in each changed file stating how and *
* when you changed that file, and provided that you do at least ONE of the *
* following: *
* *
* a) place your modifications in the Public Domain or otherwise make them *
* Freely Available, such as by posting said modifications to Usenet or *
* an equivalent medium, or placing the modifications on a major archive *
* site such as uunet.uu.net, or by allowing the Copyright Holder to include *
* your modifications in the Standard Version of the Package. *
* *
* b) use the modified Package only within your corporation or organization. *
* *
* c) rename any non-standard executables so the names do not conflict *
* with standard executables, which must also be provided, and provide *
* a separate manual page for each non-standard executable that clearly *
* documents how it differs from the Standard Version. *
* *
* d) make other distribution arrangements with the Copyright Holder. *
* *
* 4. You may distribute the programs of this Package in object code or *
* executable form, provided that you do at least ONE of the following: *
* *
* a) distribute a Standard Version of the executables and library files, *
* together with instructions (in the manual page or equivalent) on where *
* to get the Standard Version. *
* *
* b) accompany the distribution with the machine-readable source of *
* the Package with your modifications. *
* *
* c) give non-standard executables non-standard names, and clearly *
* document the differences in manual pages (or equivalent), together *
* with instructions on where to get the Standard Version. *
* *
* d) make other distribution arrangements with the Copyright Holder. *
* *
* 5. You may charge a reasonable copying fee for any distribution of this *
* Package. You may charge any fee you choose for support of this *
* Package. You may not charge a fee for this Package itself. However, *
* you may distribute this Package in aggregate with other (possibly *
* commercial) programs as part of a larger (possibly commercial) software *
* distribution provided that you do not advertise this Package as a *
* product of your own. You may embed this Package's interpreter within *
* an executable of yours (by linking); this shall be construed as a mere *
* form of aggregation, provided that the complete Standard Version of the *
* interpreter is so embedded. *
* *
* 6. The scripts and library files supplied as input to or produced as *
* output from the programs of this Package do not automatically fall *
* under the copyright of this Package, but belong to whoever generated *
* them, and may be sold commercially, and may be aggregated with this *
* Package. If such scripts or library files are aggregated with this *
* Package via the so-called "undump" or "unexec" methods of producing a *
* binary executable image, then distribution of such an image shall *
* neither be construed as a distribution of this Package nor shall it *
* fall under the restrictions of Paragraphs 3 and 4, provided that you do *
* not represent such an executable image as a Standard Version of this *
* Package. *
* *
* 7. C subroutines (or comparably compiled subroutines in other *
* languages) supplied by you and linked into this Package in order to *
* emulate subroutines and variables of the language defined by this *
* Package shall not be considered part of this Package, but are the *
* equivalent of input as in Paragraph 6, provided these subroutines do *
* not change the language in any way that would cause it to fail the *
* regression tests for the language. *
* *
* 8. Aggregation of this Package with a commercial distribution is always *
* permitted provided that the use of this Package is embedded; that is, *
* when no overt attempt is made to make this Package's interfaces visible *
* to the end user of the commercial distribution. Such use shall not be *
* construed as a distribution of this Package. *
* *
* 9. The name of the Copyright Holder may not be used to endorse or promote *
* products derived from this software without specific prior written *
* permission. *
* *
* 10. THIS PACKAGE IS PROVIDED "AS IS" AND WITHOUT ANY EXPRESS OR *
* IMPLIED WARRANTIES, INCLUDING, WITHOUT LIMITATION, THE IMPLIED *
* WARRANTIES OF MERCHANTIBILITY AND FITNESS FOR A PARTICULAR PURPOSE. *
* *
* The End *
* *
\******************************************************************************/
#include "general.h"
/* Number Handling */
int IsRealNumber(char *c) {
int i, l;
l = strlen(c);
if (l <= 0) return 0;
if (l == 1) return IsNumberDigit(c[0]);
for(i = 1; i < strlen(c); i++) {
if (c[i] == '.') return IsPosNumber(&c[i + 1]);
if (!IsNumberDigit(c[i])) return 0;
}
return (IsNumberDigit(c[0]) || IsSignDigit(c[0]));
}
int IsPosNumber(const char *c) {
int i, l;
l = strlen(c);
if (l <= 0) return 0;
for(i = 0; i < strlen(c); i++) {
if (!IsNumberDigit(c[i])) return 0;
}
return 1;
}
int IsNumber(const char *c) {
int i, l;
l = strlen(c);
if (l <= 0) return 0;
if (l == 1) return IsNumberDigit(c[0]);
for(i = 1; i < strlen(c); i++) {
if (!IsNumberDigit(c[i])) return 0;
}
return (IsNumberDigit(c[0]) || IsSignDigit(c[0]));
}
/* File Handling */
char * freadstr(FILE *fd, const char *separators) {
char *str;
int buf, icur = 0, max = 10;
str = (char *) malloc(sizeof(char) * max);
str[0] = '\0';
do {
if ((buf = fgetc(fd)) != EOF) {
if (icur == (max - 1)) {
max = max * 2;
str = (char *) realloc(str, sizeof(char) * max);
}
if (!CharIn((char) buf, separators)) {
str[icur] = (char) buf;
icur++;
str[icur] = '\0';
}
}
} while(!CharIn(buf, separators) && !feof(fd));
return str;
}
int CharIn(const char c, const char *in) {
int i;
for (i = 0; i < strlen(in); i++)
if (c == in[i]) return 1;
return 0;
}
/* string handling */
int patternmatch(char *pattern, char *thestr) {
int i, j = -1, pl = strlen(pattern), sl = strlen(thestr);
for(i = 0; i < pl; i++) {
if (pattern[i] == '*') {
do {
i++;
if (i == pl) return 1;
} while(pattern[i] == '*');
do {
j++;
if (j >= sl) return 0;
if ((thestr[j] == pattern[i]) && patternmatch(pattern + i, thestr + j)) return 1;
} while(1);
} else {
j++;
if (j >= sl) return 0;
if (pattern[i] != thestr[j]) return 0;
}
}
return (pl == sl);
}

View File

@ -0,0 +1,159 @@
/******************************************************************************\
* *
* SimpleCUDD library (www.cs.kuleuven.be/~theo/tools/simplecudd.html) *
* SimpleCUDD was developed at Katholieke Universiteit Leuven(www.kuleuven.be) *
* *
* Copyright T. Mantadelis and Katholieke Universiteit Leuven 2008 *
* *
* Author: Theofrastos Mantadelis *
* File: general.h *
* *
********************************************************************************
* *
* The "Artistic License" *
* *
* Preamble *
* *
* The intent of this document is to state the conditions under which a *
* Package may be copied, such that the Copyright Holder maintains some *
* semblance of artistic control over the development of the package, *
* while giving the users of the package the right to use and distribute *
* the Package in a more-or-less customary fashion, plus the right to make *
* reasonable modifications. *
* *
* Definitions: *
* *
* "Package" refers to the collection of files distributed by the *
* Copyright Holder, and derivatives of that collection of files *
* created through textual modification. *
* *
* "Standard Version" refers to such a Package if it has not been *
* modified, or has been modified in accordance with the wishes *
* of the Copyright Holder as specified below. *
* *
* "Copyright Holder" is whoever is named in the copyright or *
* copyrights for the package. *
* *
* "You" is you, if you're thinking about copying or distributing *
* this Package. *
* *
* "Reasonable copying fee" is whatever you can justify on the *
* basis of media cost, duplication charges, time of people involved, *
* and so on. (You will not be required to justify it to the *
* Copyright Holder, but only to the computing community at large *
* as a market that must bear the fee.) *
* *
* "Freely Available" means that no fee is charged for the item *
* itself, though there may be fees involved in handling the item. *
* It also means that recipients of the item may redistribute it *
* under the same conditions they received it. *
* *
* 1. You may make and give away verbatim copies of the source form of the *
* Standard Version of this Package without restriction, provided that you *
* duplicate all of the original copyright notices and associated disclaimers. *
* *
* 2. You may apply bug fixes, portability fixes and other modifications *
* derived from the Public Domain or from the Copyright Holder. A Package *
* modified in such a way shall still be considered the Standard Version. *
* *
* 3. You may otherwise modify your copy of this Package in any way, provided *
* that you insert a prominent notice in each changed file stating how and *
* when you changed that file, and provided that you do at least ONE of the *
* following: *
* *
* a) place your modifications in the Public Domain or otherwise make them *
* Freely Available, such as by posting said modifications to Usenet or *
* an equivalent medium, or placing the modifications on a major archive *
* site such as uunet.uu.net, or by allowing the Copyright Holder to include *
* your modifications in the Standard Version of the Package. *
* *
* b) use the modified Package only within your corporation or organization. *
* *
* c) rename any non-standard executables so the names do not conflict *
* with standard executables, which must also be provided, and provide *
* a separate manual page for each non-standard executable that clearly *
* documents how it differs from the Standard Version. *
* *
* d) make other distribution arrangements with the Copyright Holder. *
* *
* 4. You may distribute the programs of this Package in object code or *
* executable form, provided that you do at least ONE of the following: *
* *
* a) distribute a Standard Version of the executables and library files, *
* together with instructions (in the manual page or equivalent) on where *
* to get the Standard Version. *
* *
* b) accompany the distribution with the machine-readable source of *
* the Package with your modifications. *
* *
* c) give non-standard executables non-standard names, and clearly *
* document the differences in manual pages (or equivalent), together *
* with instructions on where to get the Standard Version. *
* *
* d) make other distribution arrangements with the Copyright Holder. *
* *
* 5. You may charge a reasonable copying fee for any distribution of this *
* Package. You may charge any fee you choose for support of this *
* Package. You may not charge a fee for this Package itself. However, *
* you may distribute this Package in aggregate with other (possibly *
* commercial) programs as part of a larger (possibly commercial) software *
* distribution provided that you do not advertise this Package as a *
* product of your own. You may embed this Package's interpreter within *
* an executable of yours (by linking); this shall be construed as a mere *
* form of aggregation, provided that the complete Standard Version of the *
* interpreter is so embedded. *
* *
* 6. The scripts and library files supplied as input to or produced as *
* output from the programs of this Package do not automatically fall *
* under the copyright of this Package, but belong to whoever generated *
* them, and may be sold commercially, and may be aggregated with this *
* Package. If such scripts or library files are aggregated with this *
* Package via the so-called "undump" or "unexec" methods of producing a *
* binary executable image, then distribution of such an image shall *
* neither be construed as a distribution of this Package nor shall it *
* fall under the restrictions of Paragraphs 3 and 4, provided that you do *
* not represent such an executable image as a Standard Version of this *
* Package. *
* *
* 7. C subroutines (or comparably compiled subroutines in other *
* languages) supplied by you and linked into this Package in order to *
* emulate subroutines and variables of the language defined by this *
* Package shall not be considered part of this Package, but are the *
* equivalent of input as in Paragraph 6, provided these subroutines do *
* not change the language in any way that would cause it to fail the *
* regression tests for the language. *
* *
* 8. Aggregation of this Package with a commercial distribution is always *
* permitted provided that the use of this Package is embedded; that is, *
* when no overt attempt is made to make this Package's interfaces visible *
* to the end user of the commercial distribution. Such use shall not be *
* construed as a distribution of this Package. *
* *
* 9. The name of the Copyright Holder may not be used to endorse or promote *
* products derived from this software without specific prior written *
* permission. *
* *
* 10. THIS PACKAGE IS PROVIDED "AS IS" AND WITHOUT ANY EXPRESS OR *
* IMPLIED WARRANTIES, INCLUDING, WITHOUT LIMITATION, THE IMPLIED *
* WARRANTIES OF MERCHANTIBILITY AND FITNESS FOR A PARTICULAR PURPOSE. *
* *
* The End *
* *
\******************************************************************************/
#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#define IsNumberDigit(c) ('0' <= c && c <= '9')
#define IsSignDigit(c) (c == '+' || c == '-')
#define isOperator(x) (x == '+' || x == '*' || x == '#' || x == '=')
#define freadline(fd) freadstr(fd, "\n");
int IsRealNumber(char *c);
int IsPosNumber(const char *c);
int IsNumber(const char *c);
char * freadstr(FILE *fd, const char *separators);
int CharIn(const char c, const char *in);
int patternmatch(char *pattern, char *thestr);

File diff suppressed because it is too large Load Diff

View File

@ -0,0 +1,287 @@
/******************************************************************************\
* *
* SimpleCUDD library (www.cs.kuleuven.be/~theo/tools/simplecudd.html) *
* SimpleCUDD was developed at Katholieke Universiteit Leuven(www.kuleuven.be) *
* *
* Copyright T. Mantadelis and Katholieke Universiteit Leuven 2008 *
* *
* Author: Theofrastos Mantadelis *
* File: simplecudd.h *
* *
********************************************************************************
* *
* The "Artistic License" *
* *
* Preamble *
* *
* The intent of this document is to state the conditions under which a *
* Package may be copied, such that the Copyright Holder maintains some *
* semblance of artistic control over the development of the package, *
* while giving the users of the package the right to use and distribute *
* the Package in a more-or-less customary fashion, plus the right to make *
* reasonable modifications. *
* *
* Definitions: *
* *
* "Package" refers to the collection of files distributed by the *
* Copyright Holder, and derivatives of that collection of files *
* created through textual modification. *
* *
* "Standard Version" refers to such a Package if it has not been *
* modified, or has been modified in accordance with the wishes *
* of the Copyright Holder as specified below. *
* *
* "Copyright Holder" is whoever is named in the copyright or *
* copyrights for the package. *
* *
* "You" is you, if you're thinking about copying or distributing *
* this Package. *
* *
* "Reasonable copying fee" is whatever you can justify on the *
* basis of media cost, duplication charges, time of people involved, *
* and so on. (You will not be required to justify it to the *
* Copyright Holder, but only to the computing community at large *
* as a market that must bear the fee.) *
* *
* "Freely Available" means that no fee is charged for the item *
* itself, though there may be fees involved in handling the item. *
* It also means that recipients of the item may redistribute it *
* under the same conditions they received it. *
* *
* 1. You may make and give away verbatim copies of the source form of the *
* Standard Version of this Package without restriction, provided that you *
* duplicate all of the original copyright notices and associated disclaimers. *
* *
* 2. You may apply bug fixes, portability fixes and other modifications *
* derived from the Public Domain or from the Copyright Holder. A Package *
* modified in such a way shall still be considered the Standard Version. *
* *
* 3. You may otherwise modify your copy of this Package in any way, provided *
* that you insert a prominent notice in each changed file stating how and *
* when you changed that file, and provided that you do at least ONE of the *
* following: *
* *
* a) place your modifications in the Public Domain or otherwise make them *
* Freely Available, such as by posting said modifications to Usenet or *
* an equivalent medium, or placing the modifications on a major archive *
* site such as uunet.uu.net, or by allowing the Copyright Holder to include *
* your modifications in the Standard Version of the Package. *
* *
* b) use the modified Package only within your corporation or organization. *
* *
* c) rename any non-standard executables so the names do not conflict *
* with standard executables, which must also be provided, and provide *
* a separate manual page for each non-standard executable that clearly *
* documents how it differs from the Standard Version. *
* *
* d) make other distribution arrangements with the Copyright Holder. *
* *
* 4. You may distribute the programs of this Package in object code or *
* executable form, provided that you do at least ONE of the following: *
* *
* a) distribute a Standard Version of the executables and library files, *
* together with instructions (in the manual page or equivalent) on where *
* to get the Standard Version. *
* *
* b) accompany the distribution with the machine-readable source of *
* the Package with your modifications. *
* *
* c) give non-standard executables non-standard names, and clearly *
* document the differences in manual pages (or equivalent), together *
* with instructions on where to get the Standard Version. *
* *
* d) make other distribution arrangements with the Copyright Holder. *
* *
* 5. You may charge a reasonable copying fee for any distribution of this *
* Package. You may charge any fee you choose for support of this *
* Package. You may not charge a fee for this Package itself. However, *
* you may distribute this Package in aggregate with other (possibly *
* commercial) programs as part of a larger (possibly commercial) software *
* distribution provided that you do not advertise this Package as a *
* product of your own. You may embed this Package's interpreter within *
* an executable of yours (by linking); this shall be construed as a mere *
* form of aggregation, provided that the complete Standard Version of the *
* interpreter is so embedded. *
* *
* 6. The scripts and library files supplied as input to or produced as *
* output from the programs of this Package do not automatically fall *
* under the copyright of this Package, but belong to whoever generated *
* them, and may be sold commercially, and may be aggregated with this *
* Package. If such scripts or library files are aggregated with this *
* Package via the so-called "undump" or "unexec" methods of producing a *
* binary executable image, then distribution of such an image shall *
* neither be construed as a distribution of this Package nor shall it *
* fall under the restrictions of Paragraphs 3 and 4, provided that you do *
* not represent such an executable image as a Standard Version of this *
* Package. *
* *
* 7. C subroutines (or comparably compiled subroutines in other *
* languages) supplied by you and linked into this Package in order to *
* emulate subroutines and variables of the language defined by this *
* Package shall not be considered part of this Package, but are the *
* equivalent of input as in Paragraph 6, provided these subroutines do *
* not change the language in any way that would cause it to fail the *
* regression tests for the language. *
* *
* 8. Aggregation of this Package with a commercial distribution is always *
* permitted provided that the use of this Package is embedded; that is, *
* when no overt attempt is made to make this Package's interfaces visible *
* to the end user of the commercial distribution. Such use shall not be *
* construed as a distribution of this Package. *
* *
* 9. The name of the Copyright Holder may not be used to endorse or promote *
* products derived from this software without specific prior written *
* permission. *
* *
* 10. THIS PACKAGE IS PROVIDED "AS IS" AND WITHOUT ANY EXPRESS OR *
* IMPLIED WARRANTIES, INCLUDING, WITHOUT LIMITATION, THE IMPLIED *
* WARRANTIES OF MERCHANTIBILITY AND FITNESS FOR A PARTICULAR PURPOSE. *
* *
* The End *
* *
\******************************************************************************/
#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <math.h>
#include <time.h>
#include "util.h"
#include "cudd.h"
#include "cuddInt.h"
#include "general.h"
#define IsHigh(manager, node) HIGH(manager) == node
#define IsLow(manager, node) LOW(manager) == node
#define HIGH(manager) Cudd_ReadOne(manager)
#define LOW(manager) Cudd_Not(Cudd_ReadOne(manager))
#define NOT(node) Cudd_Not(node)
#define GetIndex(node) Cudd_NodeReadIndex(node)
#define GetVar(manager, index) Cudd_bddIthVar(manager, index)
#define NewVar(manager) Cudd_bddNewVar(manager)
#define KillBDD(manager) Cudd_Quit(manager)
#define GetVarCount(manager) Cudd_ReadSize(manager)
#define DEBUGON _debug = 1
#define DEBUGOFF _debug = 0
#define RAPIDLOADON _RapidLoad = 1
#define RAPIDLOADOFF _RapidLoad = 0
#define SETMAXBUFSIZE(size) _maxbufsize = size
#define BDDFILE_ERROR -1
#define BDDFILE_OTHER 0
#define BDDFILE_SCRIPT 1
#define BDDFILE_NODEDUMP 2
extern int _RapidLoad;
extern int _debug;
extern int _maxbufsize;
typedef struct _bddfileheader {
FILE *inputfile;
int version;
int varcnt;
int varstart;
int intercnt;
int filetype;
} bddfileheader;
typedef struct _namedvars {
int varcnt;
int varstart;
char **vars;
int *loaded;
double *dvalue;
int *ivalue;
void **dynvalue;
} namedvars;
typedef struct _hisnode {
DdNode *key;
double dvalue;
int ivalue;
void *dynvalue;
} hisnode;
typedef struct _hisqueue {
int cnt;
hisnode *thenode;
} hisqueue;
typedef struct _nodeline {
char *varname;
char *truevar;
char *falsevar;
int nodenum;
int truenode;
int falsenode;
} nodeline;
/* Initialization */
DdManager* simpleBDDinit(int varcnt);
/* BDD Generation */
DdNode* D_BDDAnd(DdManager *manager, DdNode *bdd1, DdNode *bdd2);
DdNode* D_BDDNand(DdManager *manager, DdNode *bdd1, DdNode *bdd2);
DdNode* D_BDDOr(DdManager *manager, DdNode *bdd1, DdNode *bdd2);
DdNode* D_BDDNor(DdManager *manager, DdNode *bdd1, DdNode *bdd2);
DdNode* D_BDDXor(DdManager *manager, DdNode *bdd1, DdNode *bdd2);
DdNode* D_BDDXnor(DdManager *manager, DdNode *bdd1, DdNode *bdd2);
DdNode* FileGenerateBDD(DdManager *manager, namedvars varmap, bddfileheader fileheader);
DdNode* OnlineGenerateBDD(DdManager *manager, namedvars *varmap);
DdNode* LineParser(DdManager *manager, namedvars varmap, DdNode **inter, int maxinter, char *function, int iline);
DdNode* OnlineLineParser(DdManager *manager, namedvars *varmap, DdNode **inter, int maxinter, char *function, int iline);
DdNode* BDD_Operator(DdManager *manager, DdNode *bdd1, DdNode *bdd2, char Operator, int inegoper);
int getInterBDD(char *function);
char* getFileName(const char *function);
int GetParam(char *inputline, int iParam);
int LoadVariableData(namedvars varmap, char *filename);
/* Named variables */
namedvars InitNamedVars(int varcnt, int varstart);
void EnlargeNamedVars(namedvars *varmap, int newvarcnt);
int AddNamedVarAt(namedvars varmap, const char *varname, int index);
int AddNamedVar(namedvars varmap, const char *varname);
void SetNamedVarValuesAt(namedvars varmap, int index, double dvalue, int ivalue, void *dynvalue);
int SetNamedVarValues(namedvars varmap, const char *varname, double dvalue, int ivalue, void *dynvalue);
int GetNamedVarIndex(const namedvars varmap, const char *varname);
int RepairVarcnt(namedvars *varmap);
char* GetNodeVarName(DdManager *manager, namedvars varmap, DdNode *node);
char* GetNodeVarNameDisp(DdManager *manager, namedvars varmap, DdNode *node);
int all_loaded(namedvars varmap, int disp);
/* Traversal */
DdNode* HighNodeOf(DdManager *manager, DdNode *node);
DdNode* LowNodeOf(DdManager *manager, DdNode *node);
/* Traversal - History */
hisqueue* InitHistory(int varcnt);
void ReInitHistory(hisqueue *HisQueue, int varcnt);
void AddNode(hisqueue *HisQueue, int varstart, DdNode *node, double dvalue, int ivalue, void *dynvalue);
hisnode* GetNode(hisqueue *HisQueue, int varstart, DdNode *node);
int GetNodeIndex(hisqueue *HisQueue, int varstart, DdNode *node);
void onlinetraverse(DdManager *manager, namedvars varmap, hisqueue *HisQueue, DdNode *bdd);
/* Save-load */
bddfileheader ReadFileHeader(char *filename);
int CheckFileVersion(const char *version);
DdNode * LoadNodeDump(DdManager *manager, namedvars varmap, FILE *inputfile);
DdNode * LoadNodeRec(DdManager *manager, namedvars varmap, hisqueue *Nodes, FILE *inputfile, nodeline current);
DdNode * GetIfExists(DdManager *manager, namedvars varmap, hisqueue *Nodes, char *varname, int nodenum);
int SaveNodeDump(DdManager *manager, namedvars varmap, DdNode *bdd, char *filename);
void SaveExpand(DdManager *manager, namedvars varmap, hisqueue *Nodes, DdNode *Current, FILE *outputfile);
void ExpandNodes(hisqueue *Nodes, int index, int nodenum);
/* Export */
int simpleBDDtoDot(DdManager *manager, DdNode *bdd, char *filename);
int simpleNamedBDDtoDot(DdManager *manager, namedvars varmap, DdNode *bdd, char *filename);