update ProbLog
This commit is contained in:
parent
afd979a246
commit
f01fd0fbee
@ -3,7 +3,7 @@
|
|||||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
% Parameter Learning for ProbLog
|
% Parameter Learning for ProbLog
|
||||||
%
|
%
|
||||||
% 27.10.2008
|
% 28.11.2008
|
||||||
% bernd.gutmann@cs.kuleuven.be
|
% bernd.gutmann@cs.kuleuven.be
|
||||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
|
|
||||||
@ -61,6 +61,11 @@
|
|||||||
:- dynamic log_frequency/1.
|
:- dynamic log_frequency/1.
|
||||||
:- dynamic alpha/1.
|
:- dynamic alpha/1.
|
||||||
:- dynamic sigmoid_slope/1.
|
:- dynamic sigmoid_slope/1.
|
||||||
|
:- dynamic line_search/1.
|
||||||
|
:- dynamic line_search_tolerance/1.
|
||||||
|
:- dynamic line_search_tau/1.
|
||||||
|
:- dynamic line_search_never_stop/1.
|
||||||
|
:- dynamic line_search_interval/2.
|
||||||
|
|
||||||
|
|
||||||
%==========================================================================
|
%==========================================================================
|
||||||
@ -84,6 +89,7 @@ set_learning_flag(init_method,(Query,Probability,BDDFile,ProbFile,Call)) :-
|
|||||||
|
|
||||||
set_learning_flag(rebuild_bdds,Flag) :-
|
set_learning_flag(rebuild_bdds,Flag) :-
|
||||||
(Flag=true;Flag=false),
|
(Flag=true;Flag=false),
|
||||||
|
!,
|
||||||
retractall(rebuild_bdds(_)),
|
retractall(rebuild_bdds(_)),
|
||||||
assert(rebuild_bdds(Flag)).
|
assert(rebuild_bdds(Flag)).
|
||||||
|
|
||||||
@ -95,11 +101,13 @@ set_learning_flag(rebuild_bdds_it,Flag) :-
|
|||||||
|
|
||||||
set_learning_flag(reuse_initialized_bdds,Flag) :-
|
set_learning_flag(reuse_initialized_bdds,Flag) :-
|
||||||
(Flag=true;Flag=false),
|
(Flag=true;Flag=false),
|
||||||
|
!,
|
||||||
retractall(reuse_initialized_bdds(_)),
|
retractall(reuse_initialized_bdds(_)),
|
||||||
assert(reuse_initialized_bdds(Flag)).
|
assert(reuse_initialized_bdds(Flag)).
|
||||||
|
|
||||||
set_learning_flag(learning_rate,V) :-
|
set_learning_flag(learning_rate,V) :-
|
||||||
(V=examples -> true;(number(V),V>=0)),
|
(V=examples -> true;(number(V),V>=0)),
|
||||||
|
!,
|
||||||
retractall(learning_rate(_)),
|
retractall(learning_rate(_)),
|
||||||
assert(learning_rate(V)).
|
assert(learning_rate(V)).
|
||||||
|
|
||||||
@ -112,6 +120,7 @@ set_learning_flag(probability_initializer,(FactID,Probability,Query)) :-
|
|||||||
|
|
||||||
set_learning_flag(check_duplicate_bdds,Flag) :-
|
set_learning_flag(check_duplicate_bdds,Flag) :-
|
||||||
(Flag=true;Flag=false),
|
(Flag=true;Flag=false),
|
||||||
|
!,
|
||||||
retractall(check_duplicate_bdds(_)),
|
retractall(check_duplicate_bdds(_)),
|
||||||
assert(check_duplicate_bdds(Flag)).
|
assert(check_duplicate_bdds(Flag)).
|
||||||
|
|
||||||
@ -160,6 +169,34 @@ set_learning_flag(sigmoid_slope,Slope) :-
|
|||||||
assert(sigmoid_slope(Slope)).
|
assert(sigmoid_slope(Slope)).
|
||||||
|
|
||||||
|
|
||||||
|
set_learning_flag(line_search,Flag) :-
|
||||||
|
(Flag=true;Flag=false),
|
||||||
|
!,
|
||||||
|
retractall(line_search(_)),
|
||||||
|
assert(line_search(Flag)).
|
||||||
|
set_learning_flag(line_search_tolerance,Number) :-
|
||||||
|
number(Number),
|
||||||
|
Number>0,
|
||||||
|
retractall(line_search_tolerance(_)),
|
||||||
|
assert(line_search_tolerance(Number)).
|
||||||
|
set_learning_flag(line_search_interval,(L,R)) :-
|
||||||
|
number(L),
|
||||||
|
number(R),
|
||||||
|
L<R,
|
||||||
|
retractall(line_search_interval(_,_)),
|
||||||
|
assert(line_search_interval(L,R)).
|
||||||
|
set_learning_flag(line_search_tau,Number) :-
|
||||||
|
number(Number),
|
||||||
|
Number>0,
|
||||||
|
retractall(line_search_tau(_)),
|
||||||
|
assert(line_search_tau(Number)).
|
||||||
|
set_learning_flag(line_search_never_stop,Flag) :-
|
||||||
|
(Flag=true;Flag=false),
|
||||||
|
!,
|
||||||
|
retractall(line_search_nerver_stop(_)),
|
||||||
|
assert(line_search_never_stop(Flag)).
|
||||||
|
|
||||||
|
|
||||||
%========================================================================
|
%========================================================================
|
||||||
%= store the facts with the learned probabilities to a file
|
%= store the facts with the learned probabilities to a file
|
||||||
%= if F is a variable, a filename based on the current iteration is used
|
%= if F is a variable, a filename based on the current iteration is used
|
||||||
@ -358,7 +395,7 @@ do_learning_intern(Iterations,Epsilon) :-
|
|||||||
assert(current_iteration(CurrentIteration)),
|
assert(current_iteration(CurrentIteration)),
|
||||||
EndIteration is OldIteration+Iterations,
|
EndIteration is OldIteration+Iterations,
|
||||||
|
|
||||||
format(' Iteration ~d of ~d~n',[CurrentIteration,EndIteration]),
|
format('~n Iteration ~d of ~d~n',[CurrentIteration,EndIteration]),
|
||||||
logger_set_variable(iteration,CurrentIteration),
|
logger_set_variable(iteration,CurrentIteration),
|
||||||
|
|
||||||
logger_start_timer(duration),
|
logger_start_timer(duration),
|
||||||
@ -668,10 +705,14 @@ random_probability(_FactID,Probability) :-
|
|||||||
%========================================================================
|
%========================================================================
|
||||||
|
|
||||||
update_values :-
|
update_values :-
|
||||||
|
update_values(all).
|
||||||
|
|
||||||
|
|
||||||
|
update_values(_) :-
|
||||||
values_correct,
|
values_correct,
|
||||||
!.
|
!.
|
||||||
|
|
||||||
update_values :-
|
update_values(What_To_Update) :-
|
||||||
\+ values_correct,
|
\+ values_correct,
|
||||||
|
|
||||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
@ -688,12 +729,17 @@ update_values :-
|
|||||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
open(Input_Filename,'write',Handle),
|
open(Input_Filename,'write',Handle),
|
||||||
|
|
||||||
( % go over all tunable facts
|
( % go over all probabilistic fact
|
||||||
get_fact_probability(ID,Prob),
|
get_fact_probability(ID,Prob),
|
||||||
inv_sigmoid(Prob,Value),
|
inv_sigmoid(Prob,Value),
|
||||||
format(Handle,'@x~q~n~10f~n',[ID,Value]),
|
(
|
||||||
|
non_ground_fact(ID)
|
||||||
|
->
|
||||||
|
format(Handle,'@x~q_*~n~10f~n',[ID,Value]);
|
||||||
|
format(Handle,'@x~q~n~10f~n',[ID,Value])
|
||||||
|
),
|
||||||
|
|
||||||
fail; % go to next tunable fact
|
fail; % go to next probabilistic fact
|
||||||
true
|
true
|
||||||
),
|
),
|
||||||
|
|
||||||
@ -710,7 +756,7 @@ update_values :-
|
|||||||
( % go over all training examples
|
( % go over all training examples
|
||||||
current_predicate(user:example/3),
|
current_predicate(user:example/3),
|
||||||
user:example(QueryID,_Query,_QueryProb),
|
user:example(QueryID,_Query,_QueryProb),
|
||||||
once(call_bdd_tool(QueryID,'.')),
|
once(call_bdd_tool(QueryID,'.',What_To_Update)),
|
||||||
fail; % go to next training example
|
fail; % go to next training example
|
||||||
true
|
true
|
||||||
),
|
),
|
||||||
@ -723,13 +769,16 @@ update_values :-
|
|||||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
% start update values for all test examples
|
% start update values for all test examples
|
||||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
( % go over all training examples
|
( What_To_Update = all
|
||||||
current_predicate(user:test_example/3),
|
->
|
||||||
user:test_example(QueryID,_Query,_QueryProb),
|
( % go over all training examples
|
||||||
once(call_bdd_tool(QueryID,'+')),
|
current_predicate(user:test_example/3),
|
||||||
fail; % go to next training example
|
user:test_example(QueryID,_Query,_QueryProb),
|
||||||
true
|
once(call_bdd_tool(QueryID,'+',all)),
|
||||||
),
|
fail; % go to next training example
|
||||||
|
true
|
||||||
|
); true
|
||||||
|
),
|
||||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
% stop update values for all test examples
|
% stop update values for all test examples
|
||||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
@ -748,7 +797,7 @@ update_values :-
|
|||||||
%========================================================================
|
%========================================================================
|
||||||
|
|
||||||
|
|
||||||
call_bdd_tool(QueryID,Symbol) :-
|
call_bdd_tool(QueryID,Symbol,What_To_Update) :-
|
||||||
output_directory(Output_Directory),
|
output_directory(Output_Directory),
|
||||||
query_directory(Query_Directory),
|
query_directory(Query_Directory),
|
||||||
(
|
(
|
||||||
@ -759,15 +808,16 @@ call_bdd_tool(QueryID,Symbol) :-
|
|||||||
(
|
(
|
||||||
sigmoid_slope(Slope),
|
sigmoid_slope(Slope),
|
||||||
problog_dir(PD),
|
problog_dir(PD),
|
||||||
|
(What_To_Update=all -> Method='g' ; Method='l'),
|
||||||
atomic_concat([PD,
|
atomic_concat([PD,
|
||||||
'/ProblogBDD -i "',
|
'/ProblogBDD -i "',
|
||||||
Output_Directory,
|
Output_Directory,
|
||||||
'input.txt',
|
'input.txt',
|
||||||
'" -l "',
|
'" -l "',
|
||||||
Query_Directory,
|
Query_Directory,
|
||||||
'query_',
|
'query_',
|
||||||
QueryID,
|
QueryID,
|
||||||
'" -m g -id ',
|
'" -m ',Method,' -id ',
|
||||||
QueryID,
|
QueryID,
|
||||||
' -sl ',Slope,
|
' -sl ',Slope,
|
||||||
' > "',
|
' > "',
|
||||||
@ -894,6 +944,25 @@ ground_truth_difference :-
|
|||||||
%= -Float
|
%= -Float
|
||||||
%========================================================================
|
%========================================================================
|
||||||
|
|
||||||
|
mse_trainingset_only_for_linesearch(MSE) :-
|
||||||
|
(
|
||||||
|
current_predicate(user:example/3)
|
||||||
|
->
|
||||||
|
(
|
||||||
|
update_values(probabilities),
|
||||||
|
findall(SquaredError,
|
||||||
|
(user:example(QueryID,_Query,QueryProb),
|
||||||
|
query_probability(QueryID,CurrentProb),
|
||||||
|
SquaredError is (CurrentProb-QueryProb)**2),
|
||||||
|
AllSquaredErrors),
|
||||||
|
|
||||||
|
length(AllSquaredErrors,Length),
|
||||||
|
sum_list(AllSquaredErrors,SumAllSquaredErrors),
|
||||||
|
MSE is SumAllSquaredErrors/Length
|
||||||
|
); true
|
||||||
|
),
|
||||||
|
retractall(values_correct).
|
||||||
|
|
||||||
% calculate the mse of the training data
|
% calculate the mse of the training data
|
||||||
mse_trainingset :-
|
mse_trainingset :-
|
||||||
(
|
(
|
||||||
@ -947,7 +1016,6 @@ mse_testset :-
|
|||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
%========================================================================
|
%========================================================================
|
||||||
%= Calculates the sigmoid function respectivly the inverse of it
|
%= Calculates the sigmoid function respectivly the inverse of it
|
||||||
%= warning: applying inv_sigmoid to 0.0 or 1.0 will yield +/-inf
|
%= warning: applying inv_sigmoid to 0.0 or 1.0 will yield +/-inf
|
||||||
@ -988,8 +1056,64 @@ secure_probability(Prob,Prob_Secure) :-
|
|||||||
%= probabilities of the examples have to be recalculated
|
%= probabilities of the examples have to be recalculated
|
||||||
%========================================================================
|
%========================================================================
|
||||||
|
|
||||||
|
save_old_probabilities :-
|
||||||
|
( % go over all tunable facts
|
||||||
|
|
||||||
|
tunable_fact(FactID,_),
|
||||||
|
get_fact_probability(FactID,OldProbability),
|
||||||
|
atomic_concat(['old_prob_',FactID],Key),
|
||||||
|
bb_put(Key,OldProbability),
|
||||||
|
|
||||||
|
fail; % go to next tunable fact
|
||||||
|
true
|
||||||
|
).
|
||||||
|
|
||||||
|
forget_old_values :-
|
||||||
|
( % go over all tunable facts
|
||||||
|
|
||||||
|
tunable_fact(FactID,_),
|
||||||
|
atomic_concat(['old_prob_',FactID],Key),
|
||||||
|
atomic_concat(['grad_',FactID],Key2),
|
||||||
|
bb_delete(Key,_),
|
||||||
|
bb_delete(Key2,_),
|
||||||
|
|
||||||
|
fail; % go to next tunable fact
|
||||||
|
true
|
||||||
|
).
|
||||||
|
|
||||||
|
add_gradient(Learning_Rate) :-
|
||||||
|
( % go over all tunable facts
|
||||||
|
|
||||||
|
tunable_fact(FactID,_),
|
||||||
|
atomic_concat(['old_prob_',FactID],Key),
|
||||||
|
atomic_concat(['grad_',FactID],Key2),
|
||||||
|
|
||||||
|
bb_get(Key,OldProbability),
|
||||||
|
bb_get(Key2,GradValue),
|
||||||
|
|
||||||
|
inv_sigmoid(OldProbability,OldValue),
|
||||||
|
NewValue is OldValue -Learning_Rate*GradValue,
|
||||||
|
sigmoid(NewValue,NewProbability),
|
||||||
|
|
||||||
|
% Prevent "inf" by using values too close to 1.0
|
||||||
|
secure_probability(NewProbability,NewProbabilityS),
|
||||||
|
set_fact_probability(FactID,NewProbabilityS),
|
||||||
|
|
||||||
|
fail; % go to next tunable fact
|
||||||
|
|
||||||
|
true
|
||||||
|
),
|
||||||
|
retractall(values_correct).
|
||||||
|
|
||||||
|
simulate :-
|
||||||
|
L = [0.6,1.0,2.0,3.0,10,50,100,200,300],
|
||||||
|
|
||||||
|
findall((X,Y),(member(X,L),line_search_evaluate_point(X,Y)),List),
|
||||||
|
write(List),nl.
|
||||||
|
|
||||||
gradient_descent :-
|
gradient_descent :-
|
||||||
|
|
||||||
|
save_old_probabilities,
|
||||||
update_values,
|
update_values,
|
||||||
|
|
||||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
@ -998,7 +1122,8 @@ gradient_descent :-
|
|||||||
( % go over all tunable facts
|
( % go over all tunable facts
|
||||||
|
|
||||||
tunable_fact(FactID,_),
|
tunable_fact(FactID,_),
|
||||||
bb_put(FactID,0.0),
|
atomic_concat(['grad_',FactID],Key),
|
||||||
|
bb_put(Key,0.0),
|
||||||
fail; % go to next tunable fact
|
fail; % go to next tunable fact
|
||||||
|
|
||||||
true
|
true
|
||||||
@ -1029,15 +1154,18 @@ gradient_descent :-
|
|||||||
( % go over all tunable facts
|
( % go over all tunable facts
|
||||||
|
|
||||||
tunable_fact(FactID,_),
|
tunable_fact(FactID,_),
|
||||||
(
|
atomic_concat(['grad_',FactID],Key),
|
||||||
query_gradient(QueryID,FactID,GradValue)
|
|
||||||
->
|
% if the following query fails,
|
||||||
true;
|
% it means, the fact is not used in the proof
|
||||||
GradValue=0.0
|
% of QueryID, and the gradient is 0.0 and will
|
||||||
),
|
% not contribute to NewValue either way
|
||||||
bb_get(FactID,OldValue),
|
% DON'T FORGET THIS IF YOU CHANGE SOMETHING HERE!
|
||||||
|
query_gradient(QueryID,FactID,GradValue),
|
||||||
|
|
||||||
|
bb_get(Key,OldValue),
|
||||||
NewValue is OldValue + Y*GradValue,
|
NewValue is OldValue + Y*GradValue,
|
||||||
bb_put(FactID,NewValue),
|
bb_put(Key,NewValue),
|
||||||
fail; % go to next fact
|
fail; % go to next fact
|
||||||
|
|
||||||
true
|
true
|
||||||
@ -1054,7 +1182,7 @@ gradient_descent :-
|
|||||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
% start statistics on gradient
|
% start statistics on gradient
|
||||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
findall(V,(tunable_fact(FactID,_),bb_get(FactID,V)),GradientValues),
|
findall(V,(tunable_fact(FactID,_),atomic_concat(['grad_',FactID],Key),bb_get(Key,V)),GradientValues),
|
||||||
|
|
||||||
sum_list(GradientValues,GradSum),
|
sum_list(GradientValues,GradSum),
|
||||||
max_list(GradientValues,GradMax),
|
max_list(GradientValues,GradMax),
|
||||||
@ -1068,39 +1196,236 @@ gradient_descent :-
|
|||||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
% stop statistics on gradient
|
% stop statistics on gradient
|
||||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
|
|
||||||
|
|
||||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
% start add gradient to current probabilities
|
% start add gradient to current probabilities
|
||||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
|
(
|
||||||
learning_rate(LearningRate),
|
line_search(false)
|
||||||
|
->
|
||||||
( % go over all tunable facts
|
learning_rate(LearningRate);
|
||||||
|
lineSearch(LearningRate,_)
|
||||||
tunable_fact(FactID,_),
|
|
||||||
get_fact_probability(FactID,OldProbability),
|
|
||||||
bb_delete(FactID,GradValue),
|
|
||||||
|
|
||||||
inv_sigmoid(OldProbability,OldValue),
|
|
||||||
NewValue is OldValue -LearningRate*GradValue,
|
|
||||||
sigmoid(NewValue,NewProbability),
|
|
||||||
|
|
||||||
% Prevent "inf" by using values too close to 1.0
|
|
||||||
secure_probability(NewProbability,NewProbabilityS),
|
|
||||||
set_fact_probability(FactID,NewProbabilityS),
|
|
||||||
|
|
||||||
fail; % go to next tunable fact
|
|
||||||
|
|
||||||
true
|
|
||||||
),
|
),
|
||||||
|
format('learning rate = ~12f~n',[LearningRate]),
|
||||||
|
add_gradient(LearningRate),
|
||||||
|
logger_set_variable(learning_rate,LearningRate),
|
||||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
% stop add gradient to current probabilities
|
% stop add gradient to current probabilities
|
||||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
!,
|
!,
|
||||||
|
forget_old_values.
|
||||||
|
|
||||||
% we're done, mark old values as incorrect
|
%========================================================================
|
||||||
retractall(values_correct).
|
%=
|
||||||
|
%=
|
||||||
|
%========================================================================
|
||||||
|
|
||||||
|
line_search_evaluate_point(Learning_Rate,MSE) :-
|
||||||
|
add_gradient(Learning_Rate),
|
||||||
|
mse_trainingset_only_for_linesearch(MSE).
|
||||||
|
|
||||||
|
|
||||||
|
lineSearch(Final_X,Final_Value) :-
|
||||||
|
|
||||||
|
% Get Parameters for line search
|
||||||
|
line_search_tolerance(Tol),
|
||||||
|
line_search_tau(Tau),
|
||||||
|
line_search_interval(A,B),
|
||||||
|
|
||||||
|
format(' Running line search in interval (~5f,~5f)~n',[A,B]),
|
||||||
|
|
||||||
|
% init values
|
||||||
|
Acc is Tol * (B-A),
|
||||||
|
InitRight is A + Tau*(B-A),
|
||||||
|
InitLeft is A + B - InitRight,
|
||||||
|
|
||||||
|
line_search_evaluate_point(A,Value_A),
|
||||||
|
line_search_evaluate_point(B,Value_B),
|
||||||
|
line_search_evaluate_point(InitRight,Value_InitRight),
|
||||||
|
line_search_evaluate_point(InitLeft,Value_InitLeft),
|
||||||
|
|
||||||
|
bb_put(line_search_a,A),
|
||||||
|
bb_put(line_search_b,B),
|
||||||
|
bb_put(line_search_left,InitLeft),
|
||||||
|
bb_put(line_search_right,InitRight),
|
||||||
|
|
||||||
|
bb_put(line_search_value_a,Value_A),
|
||||||
|
bb_put(line_search_value_b,Value_B),
|
||||||
|
bb_put(line_search_value_left,Value_InitLeft),
|
||||||
|
bb_put(line_search_value_right,Value_InitRight),
|
||||||
|
|
||||||
|
bb_put(line_search_iteration,1),
|
||||||
|
|
||||||
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
|
%%%% BEGIN BACK TRACKING
|
||||||
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
|
(
|
||||||
|
repeat,
|
||||||
|
|
||||||
|
bb_get(line_search_iteration,Iteration),
|
||||||
|
bb_get(line_search_a,Ak),
|
||||||
|
bb_get(line_search_b,Bk),
|
||||||
|
bb_get(line_search_left,Left),
|
||||||
|
bb_get(line_search_right,Right),
|
||||||
|
|
||||||
|
bb_get(line_search_value_a,Fl),
|
||||||
|
bb_get(line_search_value_b,Fr),
|
||||||
|
bb_get(line_search_value_left,FLeft),
|
||||||
|
bb_get(line_search_value_right,FRight),
|
||||||
|
|
||||||
|
write(lineSearch(Iteration,Ak,Fl,Bk,Fr,Left,FLeft,Right,FRight)),nl,
|
||||||
|
|
||||||
|
(
|
||||||
|
% check for infinity, if there is, go to the left
|
||||||
|
( FLeft >= FRight, \+ FLeft = (+inf), \+ FRight = (+inf) )
|
||||||
|
->
|
||||||
|
(
|
||||||
|
AkNew=Left,
|
||||||
|
FlNew=FLeft,
|
||||||
|
LeftNew=Right,
|
||||||
|
FLeftNew=FRight,
|
||||||
|
RightNew is AkNew + Bk - LeftNew,
|
||||||
|
line_search_evaluate_point(RightNew,FRightNew),
|
||||||
|
BkNew=Bk,
|
||||||
|
FrNew=Fr
|
||||||
|
);
|
||||||
|
(
|
||||||
|
BkNew=Right,
|
||||||
|
FrNew=FRight,
|
||||||
|
RightNew=Left,
|
||||||
|
FRightNew=FLeft,
|
||||||
|
LeftNew is Ak + BkNew - RightNew,
|
||||||
|
|
||||||
|
line_search_evaluate_point(LeftNew,FLeftNew),
|
||||||
|
AkNew=Ak,
|
||||||
|
FlNew=Fl
|
||||||
|
)
|
||||||
|
),
|
||||||
|
|
||||||
|
Next_Iteration is Iteration + 1,
|
||||||
|
|
||||||
|
ActAcc is BkNew -AkNew,
|
||||||
|
|
||||||
|
bb_put(line_search_iteration,Next_Iteration),
|
||||||
|
|
||||||
|
bb_put(line_search_a,AkNew),
|
||||||
|
bb_put(line_search_b,BkNew),
|
||||||
|
bb_put(line_search_left,LeftNew),
|
||||||
|
bb_put(line_search_right,RightNew),
|
||||||
|
|
||||||
|
bb_put(line_search_value_a,FlNew),
|
||||||
|
bb_put(line_search_value_b,FrNew),
|
||||||
|
bb_put(line_search_value_left,FLeftNew),
|
||||||
|
bb_put(line_search_value_right,FRightNew),
|
||||||
|
|
||||||
|
% is the search interval smaller than the tolerance level?
|
||||||
|
ActAcc < Acc,
|
||||||
|
|
||||||
|
% apperantly it is, so get me out of here and
|
||||||
|
% cut away the choice point from repeat
|
||||||
|
!
|
||||||
|
),
|
||||||
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
|
%%%% END BACK TRACKING
|
||||||
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
|
|
||||||
|
% clean up the blackboard mess
|
||||||
|
bb_delete(line_search_iteration,_),
|
||||||
|
bb_delete(line_search_a,_),
|
||||||
|
bb_delete(line_search_b,_),
|
||||||
|
bb_delete(line_search_left,_),
|
||||||
|
bb_delete(line_search_right,_),
|
||||||
|
bb_delete(line_search_value_a,_),
|
||||||
|
bb_delete(line_search_value_b,_),
|
||||||
|
bb_delete(line_search_value_left,_),
|
||||||
|
bb_delete(line_search_value_right,_),
|
||||||
|
|
||||||
|
% it doesn't harm to check also the value in the middle
|
||||||
|
% of the current search interval
|
||||||
|
Middle is (AkNew + BkNew) / 2.0,
|
||||||
|
line_search_evaluate_point(Middle,Value_Middle),
|
||||||
|
|
||||||
|
% return the optimal value
|
||||||
|
my_5_min(Value_Middle,FlNew,FrNew,FLeftNew,FRightNew,
|
||||||
|
Middle,AkNew,BkNew,LeftNew,RightNew,
|
||||||
|
Optimal_Value,Optimal_X),
|
||||||
|
|
||||||
|
line_search_postcheck(Optimal_Value,Optimal_X,Final_Value,Final_X).
|
||||||
|
|
||||||
|
line_search_postcheck(V,X,V,X) :-
|
||||||
|
X>0,
|
||||||
|
!.
|
||||||
|
line_search_postcheck(V,X,V,X) :-
|
||||||
|
line_search_never_stop(false),
|
||||||
|
!.
|
||||||
|
line_search_postcheck(_,_, LLH, FinalPosition) :-
|
||||||
|
line_search_tolerance(Tolerance),
|
||||||
|
line_search_interval(Left,Right),
|
||||||
|
|
||||||
|
|
||||||
|
Offset is (Right - Left) * Tolerance,
|
||||||
|
|
||||||
|
bb_put(line_search_offset,Offset),
|
||||||
|
|
||||||
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
|
(
|
||||||
|
|
||||||
|
|
||||||
|
repeat,
|
||||||
|
|
||||||
|
bb_get(line_search_offset,OldOffset),
|
||||||
|
NewOffset is OldOffset * Tolerance,
|
||||||
|
bb_put(line_search_offset,NewOffset),
|
||||||
|
|
||||||
|
Position is Left + NewOffset,
|
||||||
|
set_linesearch_weights_calc_llh(Position,LLH),
|
||||||
|
bb_put(line_search_llh,LLH),
|
||||||
|
|
||||||
|
write(logAtom(lineSearchPostCheck(Position,LLH))),nl,
|
||||||
|
|
||||||
|
|
||||||
|
\+ LLH = (+inf),
|
||||||
|
!
|
||||||
|
), % cut away choice point from repeat
|
||||||
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
|
|
||||||
|
bb_delete(line_search_llh,LLH),
|
||||||
|
bb_delete(line_search_offset,FinalOffset),
|
||||||
|
FinalPosition is Left + FinalOffset.
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
my_5_min(V1,V2,V3,V4,V5,F1,F2,F3,F4,F5,VMin,FMin) :-
|
||||||
|
(
|
||||||
|
V1<V2
|
||||||
|
->
|
||||||
|
(VTemp1=V1,FTemp1=F1);
|
||||||
|
(VTemp1=V2,FTemp1=F2)
|
||||||
|
),
|
||||||
|
(
|
||||||
|
V3<V4
|
||||||
|
->
|
||||||
|
(VTemp2=V3,FTemp2=F3);
|
||||||
|
(VTemp2=V4,FTemp2=F4)
|
||||||
|
),
|
||||||
|
(
|
||||||
|
VTemp1<VTemp2
|
||||||
|
->
|
||||||
|
(VTemp3=VTemp1,FTemp3=FTemp1);
|
||||||
|
(VTemp3=VTemp2,FTemp3=FTemp2)
|
||||||
|
),
|
||||||
|
(
|
||||||
|
VTemp3<V5
|
||||||
|
->
|
||||||
|
(VMin=VTemp3,FMin=FTemp3);
|
||||||
|
(VMin=V5,FMin=F5)
|
||||||
|
).
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
%========================================================================
|
%========================================================================
|
||||||
@ -1123,6 +1448,11 @@ global_initialize :-
|
|||||||
set_learning_flag(sigmoid_slope,1.0), % 1.0 gives standard sigmoid
|
set_learning_flag(sigmoid_slope,1.0), % 1.0 gives standard sigmoid
|
||||||
set_learning_flag(init_method,(Query,Probability,BDDFile,ProbFile,
|
set_learning_flag(init_method,(Query,Probability,BDDFile,ProbFile,
|
||||||
problog_kbest_save(Query,10,Probability,_Status,BDDFile,ProbFile))),
|
problog_kbest_save(Query,10,Probability,_Status,BDDFile,ProbFile))),
|
||||||
|
set_learning_flag(line_search,false),
|
||||||
|
set_learning_flag(line_search_never_stop,true),
|
||||||
|
set_learning_flag(line_search_tau,0.618033988749895),
|
||||||
|
set_learning_flag(line_search_tolerance,0.05),
|
||||||
|
set_learning_flag(line_search_interval,(0,100)),
|
||||||
|
|
||||||
logger_define_variable(iteration, int),
|
logger_define_variable(iteration, int),
|
||||||
logger_define_variable(duration,time),
|
logger_define_variable(duration,time),
|
||||||
@ -1137,7 +1467,8 @@ global_initialize :-
|
|||||||
logger_define_variable(gradient_max,float),
|
logger_define_variable(gradient_max,float),
|
||||||
logger_define_variable(ground_truth_diff,float),
|
logger_define_variable(ground_truth_diff,float),
|
||||||
logger_define_variable(ground_truth_mindiff,float),
|
logger_define_variable(ground_truth_mindiff,float),
|
||||||
logger_define_variable(ground_truth_maxdiff,float).
|
logger_define_variable(ground_truth_maxdiff,float),
|
||||||
|
logger_define_variable(learning_rate,float).
|
||||||
|
|
||||||
%========================================================================
|
%========================================================================
|
||||||
%=
|
%=
|
||||||
|
@ -28,6 +28,7 @@
|
|||||||
set_fact_probability/2,
|
set_fact_probability/2,
|
||||||
get_fact/2,
|
get_fact/2,
|
||||||
tunable_fact/2,
|
tunable_fact/2,
|
||||||
|
non_ground_fact/1,
|
||||||
export_facts/1,
|
export_facts/1,
|
||||||
problog_help/0,
|
problog_help/0,
|
||||||
problog_dir/1,
|
problog_dir/1,
|
||||||
@ -73,6 +74,7 @@
|
|||||||
:- dynamic problog_predicate/2.
|
:- dynamic problog_predicate/2.
|
||||||
% global over all inference methods, exported
|
% global over all inference methods, exported
|
||||||
:- dynamic tunable_fact/2.
|
:- dynamic tunable_fact/2.
|
||||||
|
:- dynamic non_ground_fact/1.
|
||||||
:- dynamic problog_dir/1.
|
:- dynamic problog_dir/1.
|
||||||
% global, manipulated via problog_control/2
|
% global, manipulated via problog_control/2
|
||||||
:- dynamic up/0.
|
:- dynamic up/0.
|
||||||
@ -90,6 +92,12 @@
|
|||||||
:- dynamic max_proof/1.
|
:- dynamic max_proof/1.
|
||||||
% local to problog_montecarlo
|
% local to problog_montecarlo
|
||||||
:- dynamic mc_prob/1.
|
:- dynamic mc_prob/1.
|
||||||
|
% to keep track of the groundings for non-ground facts
|
||||||
|
:- dynamic grounding_is_known/2.
|
||||||
|
|
||||||
|
% for fact where the proabability is a variable
|
||||||
|
:- dynamic dynamic_probability_fact/1.
|
||||||
|
:- dynamic dynamic_probability_fact_extract/2.
|
||||||
|
|
||||||
% directory where ProblogBDD executable is located
|
% directory where ProblogBDD executable is located
|
||||||
% automatically set during loading -- assumes it is in same place as this file (problog.yap)
|
% automatically set during loading -- assumes it is in same place as this file (problog.yap)
|
||||||
@ -204,32 +212,88 @@ user:term_expansion(P::Goal,Goal) :-
|
|||||||
!.
|
!.
|
||||||
|
|
||||||
user:term_expansion(P::Goal, problog:ProbFact) :-
|
user:term_expansion(P::Goal, problog:ProbFact) :-
|
||||||
|
copy_term((P,Goal),(P_Copy,Goal_Copy)),
|
||||||
functor(Goal, Name, Arity),
|
functor(Goal, Name, Arity),
|
||||||
atomic_concat([problog_,Name],ProblogName),
|
atomic_concat([problog_,Name],ProblogName),
|
||||||
Goal =.. [Name|Args],
|
Goal =.. [Name|Args],
|
||||||
append(Args,[LProb],L1),
|
append(Args,[LProb],L1),
|
||||||
probclause_id(IDName),
|
probclause_id(ID),
|
||||||
term_variables(Goal,GVars),
|
|
||||||
(GVars=[] -> ID=IDName; ID=..[IDName|GVars]),
|
|
||||||
ProbFact =.. [ProblogName,ID|L1],
|
ProbFact =.. [ProblogName,ID|L1],
|
||||||
(P = t(TrueProb) ->
|
(
|
||||||
assert(tunable_fact(ID,TrueProb)),
|
(\+ var(P), P = t(TrueProb))
|
||||||
LProb is log(0.5)
|
->
|
||||||
;
|
(
|
||||||
LProb is log(P)
|
assert(tunable_fact(ID,TrueProb)),
|
||||||
),
|
LProb is log(0.5)
|
||||||
problog_predicate(Name, Arity, ProblogName).
|
);
|
||||||
|
(
|
||||||
|
ground(P)
|
||||||
|
->
|
||||||
|
LProb is log(P);
|
||||||
|
(
|
||||||
|
% Probability is a variable... check wether it appears in the term
|
||||||
|
(
|
||||||
|
variable_in_term(Goal,P)
|
||||||
|
->
|
||||||
|
true;
|
||||||
|
(
|
||||||
|
format(user_error,'If you use probabilisitic facts with a variable as probabilility, the variable has to appear inside the fact.~n',[]),
|
||||||
|
format(user_error,'You used ~q in your program.~2n',[P::Goal]),
|
||||||
|
throw(non_ground_fact_error(P::Goal))
|
||||||
|
)
|
||||||
|
),
|
||||||
|
LProb=log(P),
|
||||||
|
assert(dynamic_probability_fact(ID)),
|
||||||
|
assert(dynamic_probability_fact_extract(Goal_Copy,P_Copy))
|
||||||
|
)
|
||||||
|
)
|
||||||
|
),
|
||||||
|
(
|
||||||
|
ground(Goal)
|
||||||
|
->
|
||||||
|
true;
|
||||||
|
assert(non_ground_fact(ID))
|
||||||
|
),
|
||||||
|
problog_predicate(Name, Arity, ProblogName).
|
||||||
|
|
||||||
|
|
||||||
% introduce wrapper clause if predicate seen first time
|
% introduce wrapper clause if predicate seen first time
|
||||||
problog_predicate(Name, Arity, _) :-
|
problog_predicate(Name, Arity, _) :-
|
||||||
problog_predicate(Name, Arity), !.
|
problog_predicate(Name, Arity), !.
|
||||||
|
|
||||||
problog_predicate(Name, Arity, ProblogName) :-
|
problog_predicate(Name, Arity, ProblogName) :-
|
||||||
functor(OriginalGoal, Name, Arity),
|
functor(OriginalGoal, Name, Arity),
|
||||||
OriginalGoal =.. [_|Args],
|
OriginalGoal =.. [_|Args],
|
||||||
append(Args,[Prob],L1),
|
append(Args,[Prob],L1),
|
||||||
ProbFact =.. [ProblogName,ID|L1],
|
ProbFact =.. [ProblogName,ID|L1],
|
||||||
prolog_load_context(module,Mod),
|
prolog_load_context(module,Mod),
|
||||||
assert((Mod:OriginalGoal :- ProbFact, add_to_proof(ID,Prob))),
|
|
||||||
|
assert( (Mod:OriginalGoal :- ProbFact,
|
||||||
|
(
|
||||||
|
non_ground_fact(ID)
|
||||||
|
->
|
||||||
|
(non_ground_fact_grounding_id(OriginalGoal,G_ID),
|
||||||
|
atomic_concat([ID,'_',G_ID],ID2));
|
||||||
|
ID2=ID
|
||||||
|
),
|
||||||
|
% take the log of the probability (for non ground facts with variable as probability
|
||||||
|
ProbEval is Prob,
|
||||||
|
add_to_proof(ID2,ProbEval)
|
||||||
|
)),
|
||||||
|
|
||||||
|
assert( (Mod:problog_not(OriginalGoal) :- ProbFact,
|
||||||
|
(
|
||||||
|
non_ground_fact(ID)
|
||||||
|
->
|
||||||
|
( non_ground_fact_grounding_id(OriginalGoal,G_ID),
|
||||||
|
atomic_concat([ID,'_',G_ID],ID2));
|
||||||
|
ID2=ID
|
||||||
|
),
|
||||||
|
% take the log of the probability (for non ground facts with variable as probability
|
||||||
|
ProbEval is Prob,
|
||||||
|
add_to_proof_negated(ID2,ProbEval)
|
||||||
|
)),
|
||||||
|
|
||||||
assert(problog_predicate(Name, Arity)),
|
assert(problog_predicate(Name, Arity)),
|
||||||
ArityPlus2 is Arity+2,
|
ArityPlus2 is Arity+2,
|
||||||
dynamic(problog:ProblogName/ArityPlus2).
|
dynamic(problog:ProblogName/ArityPlus2).
|
||||||
@ -242,6 +306,34 @@ probclause_id(ID) :-
|
|||||||
probclause_id(0) :-
|
probclause_id(0) :-
|
||||||
nb_setval(probclause_counter,1).
|
nb_setval(probclause_counter,1).
|
||||||
|
|
||||||
|
non_ground_fact_grounding_id(Goal,ID) :-
|
||||||
|
(
|
||||||
|
ground(Goal)
|
||||||
|
->
|
||||||
|
true;
|
||||||
|
(
|
||||||
|
format(user_error,'The current program uses non-ground facts.~n', []),
|
||||||
|
format(user_error,'If you query those, you may only query fully-grounded versions of the fact.~n',[]),
|
||||||
|
format(user_error,'Within the current proof, you queried for ~q which is not ground.~n~n', [Goal]),
|
||||||
|
throw(error(non_ground_fact(Goal)))
|
||||||
|
)
|
||||||
|
),
|
||||||
|
(
|
||||||
|
grounding_is_known(Goal,ID)
|
||||||
|
->
|
||||||
|
true;
|
||||||
|
(
|
||||||
|
nb_getval(non_ground_fact_grounding_id_counter,ID),
|
||||||
|
ID2 is ID+1,
|
||||||
|
nb_setval(non_ground_fact_grounding_id_counter,ID2),
|
||||||
|
assert(grounding_is_known(Goal,ID))
|
||||||
|
)
|
||||||
|
).
|
||||||
|
|
||||||
|
reset_non_ground_facts :-
|
||||||
|
nb_setval(non_ground_fact_grounding_id_counter,0),
|
||||||
|
retractall(grounding_is_known(_,_)).
|
||||||
|
|
||||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
% access/update the probability of ID's fact
|
% access/update the probability of ID's fact
|
||||||
% hardware-access version: naively scan all problog-predicates
|
% hardware-access version: naively scan all problog-predicates
|
||||||
@ -306,7 +398,8 @@ get_fact(ID,OutsideTerm) :-
|
|||||||
|
|
||||||
get_fact_list([],[]).
|
get_fact_list([],[]).
|
||||||
get_fact_list([ID|IDs],[Fact|Facts]) :-
|
get_fact_list([ID|IDs],[Fact|Facts]) :-
|
||||||
get_fact(ID,Fact),
|
(ID=not(X) -> Fact=not(Y); Fact=Y, ID=X),
|
||||||
|
get_fact(X,Y),
|
||||||
get_fact_list(IDs,Facts).
|
get_fact_list(IDs,Facts).
|
||||||
|
|
||||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
@ -317,7 +410,7 @@ get_fact_list([ID|IDs],[Fact|Facts]) :-
|
|||||||
% - problog_probability holds the sum of their log probabilities
|
% - problog_probability holds the sum of their log probabilities
|
||||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
|
|
||||||
% called "inside" probabilistic facts to update current state of proving:
|
% called "inside" probabilistic facts to update current state of proving
|
||||||
% if number of steps exceeded, fail
|
% if number of steps exceeded, fail
|
||||||
% if fact used before, succeed and keep status as is
|
% if fact used before, succeed and keep status as is
|
||||||
% if not prunable, calculate probability and
|
% if not prunable, calculate probability and
|
||||||
@ -329,6 +422,11 @@ add_to_proof(ID,Prob) :-
|
|||||||
b_getval(problog_probability, CurrentP),
|
b_getval(problog_probability, CurrentP),
|
||||||
nb_getval(problog_threshold, CurrentThreshold),
|
nb_getval(problog_threshold, CurrentThreshold),
|
||||||
b_getval(problog_current_proof, IDs),
|
b_getval(problog_current_proof, IDs),
|
||||||
|
|
||||||
|
%%%% Bernd, changes for negated ground facts
|
||||||
|
\+ memberchk(not(ID),IDs),
|
||||||
|
%%%% Bernd, changes for negated ground facts
|
||||||
|
|
||||||
( MaxSteps =< 0 ->
|
( MaxSteps =< 0 ->
|
||||||
fail
|
fail
|
||||||
;
|
;
|
||||||
@ -349,6 +447,44 @@ add_to_proof(ID,Prob) :-
|
|||||||
b_setval(problog_steps,Steps)
|
b_setval(problog_steps,Steps)
|
||||||
).
|
).
|
||||||
|
|
||||||
|
%%%% Bernd, changes for negated ground facts
|
||||||
|
add_to_proof_negated(ID,Prob) :-
|
||||||
|
(
|
||||||
|
problog_control(check,mc)
|
||||||
|
->
|
||||||
|
% the sample has to fail if the fact is negated
|
||||||
|
\+ montecarlo_check(ID);
|
||||||
|
true
|
||||||
|
),
|
||||||
|
b_getval(problog_steps,MaxSteps),
|
||||||
|
b_getval(problog_probability, CurrentP),
|
||||||
|
nb_getval(problog_threshold, CurrentThreshold),
|
||||||
|
b_getval(problog_current_proof, IDs),
|
||||||
|
|
||||||
|
\+ memberchk(ID,IDs),
|
||||||
|
( MaxSteps =< 0 ->
|
||||||
|
fail
|
||||||
|
;
|
||||||
|
( memberchk(not(ID), IDs) ->
|
||||||
|
true
|
||||||
|
;
|
||||||
|
% \+ prune_check([ID|IDs],1),
|
||||||
|
InverseProb is log(1 - exp(Prob)),
|
||||||
|
multiply_probabilities(CurrentP, InverseProb, NProb),
|
||||||
|
( NProb < CurrentThreshold ->
|
||||||
|
upper_bound([not(ID)|IDs]), %% checkme
|
||||||
|
fail
|
||||||
|
;
|
||||||
|
b_setval(problog_probability, NProb),
|
||||||
|
b_setval(problog_current_proof, [not(ID)|IDs])
|
||||||
|
)
|
||||||
|
),
|
||||||
|
Steps is MaxSteps-1,
|
||||||
|
b_setval(problog_steps,Steps)
|
||||||
|
).
|
||||||
|
%%%% Bernd, changes for negated ground facts
|
||||||
|
|
||||||
|
|
||||||
% if in monte carlo mode, check array to see if fact can be used
|
% if in monte carlo mode, check array to see if fact can be used
|
||||||
montecarlo_check(ID) :-
|
montecarlo_check(ID) :-
|
||||||
(
|
(
|
||||||
@ -394,6 +530,7 @@ multiply_probabilities(CurrentLogP, LogProb, NLogProb) :-
|
|||||||
% this is called by all inference methods before the actual ProbLog goal
|
% this is called by all inference methods before the actual ProbLog goal
|
||||||
% to set up environment for proving
|
% to set up environment for proving
|
||||||
init_problog(Threshold) :-
|
init_problog(Threshold) :-
|
||||||
|
reset_non_ground_facts,
|
||||||
LT is log(Threshold),
|
LT is log(Threshold),
|
||||||
b_setval(problog_probability, 0.0),
|
b_setval(problog_probability, 0.0),
|
||||||
b_setval(problog_current_proof, []),
|
b_setval(problog_current_proof, []),
|
||||||
@ -412,6 +549,8 @@ prune_check(Proof,TreeID) :-
|
|||||||
% (as logical part is there, but probabilistic part in problog)
|
% (as logical part is there, but probabilistic part in problog)
|
||||||
problog_call(Goal) :-
|
problog_call(Goal) :-
|
||||||
yap_flag(typein_module,Module),
|
yap_flag(typein_module,Module),
|
||||||
|
%%% if user provides init_db, call this before proving goal
|
||||||
|
(current_predicate(_,Module:init_db) -> call(Module:init_db); true),
|
||||||
put_module(Goal,Module,ModGoal),
|
put_module(Goal,Module,ModGoal),
|
||||||
call(ModGoal).
|
call(ModGoal).
|
||||||
|
|
||||||
@ -446,7 +585,12 @@ put_module(Goal,Module,Module:Goal).
|
|||||||
eval_dnf(ID,Prob,Status) :-
|
eval_dnf(ID,Prob,Status) :-
|
||||||
((ID = 1, problog_flag(save_bdd,true)) -> problog_control(on,remember); problog_control(off,remember)),
|
((ID = 1, problog_flag(save_bdd,true)) -> problog_control(on,remember); problog_control(off,remember)),
|
||||||
count_ptree(ID,NX),
|
count_ptree(ID,NX),
|
||||||
format(user,'~w proofs~n',[NX]),
|
(
|
||||||
|
NX=1
|
||||||
|
->
|
||||||
|
format(user,'1 proof~n',[]);
|
||||||
|
format(user,'~w proofs~n',[NX])
|
||||||
|
),
|
||||||
problog_flag(dir,DirFlag),
|
problog_flag(dir,DirFlag),
|
||||||
problog_flag(bdd_file,BDDFileFlag),
|
problog_flag(bdd_file,BDDFileFlag),
|
||||||
atomic_concat([DirFlag,BDDFileFlag],BDDFile),
|
atomic_concat([DirFlag,BDDFileFlag],BDDFile),
|
||||||
@ -703,8 +847,8 @@ problog_max(Goal, Prob, Facts) :-
|
|||||||
problog_flag(first_threshold,InitT),
|
problog_flag(first_threshold,InitT),
|
||||||
init_problog_max(InitT),
|
init_problog_max(InitT),
|
||||||
problog_max_id(Goal, Prob, FactIDs),
|
problog_max_id(Goal, Prob, FactIDs),
|
||||||
( FactIDs == unprovable -> Facts = unprovable;
|
( FactIDs = [_|_] -> get_fact_list(FactIDs,Facts);
|
||||||
get_fact_list(FactIDs,Facts)).
|
Facts = FactIDs).
|
||||||
|
|
||||||
init_problog_max(Threshold) :-
|
init_problog_max(Threshold) :-
|
||||||
retractall(max_probability(_)),
|
retractall(max_probability(_)),
|
||||||
@ -736,7 +880,10 @@ problog_max_id(Goal, Prob, Clauses) :-
|
|||||||
nb_getval(problog_threshold, LT),
|
nb_getval(problog_threshold, LT),
|
||||||
problog_flag(last_threshold_log,ToSmall),
|
problog_flag(last_threshold_log,ToSmall),
|
||||||
((MaxP >= LT ; \+ problog_control(check,limit); LT < ToSmall) ->
|
((MaxP >= LT ; \+ problog_control(check,limit); LT < ToSmall) ->
|
||||||
max_proof(Clauses),
|
((max_proof(unprovable), problog_control(check,limit), LT < ToSmall) ->
|
||||||
|
problog_flag(last_threshold,Stopping),
|
||||||
|
Clauses = unprovable(Stopping)
|
||||||
|
; max_proof(Clauses)),
|
||||||
Prob is exp(MaxP)
|
Prob is exp(MaxP)
|
||||||
;
|
;
|
||||||
problog_flag(id_stepsize_log,Step),
|
problog_flag(id_stepsize_log,Step),
|
||||||
@ -880,6 +1027,14 @@ problog_exact(Goal,Prob,Status) :-
|
|||||||
% by method itself, only to write number to log-file
|
% by method itself, only to write number to log-file
|
||||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
|
|
||||||
|
problog_montecarlo(_,_,_) :-
|
||||||
|
non_ground_fact(_),
|
||||||
|
!,
|
||||||
|
format(user_error,'Current database contains non-ground facts.',[]),
|
||||||
|
format(user_error,'Monte Carlo inference is not possible in this case. Try k-best instead.',[]),
|
||||||
|
fail.
|
||||||
|
|
||||||
|
|
||||||
problog_montecarlo(Goal,Delta,Prob) :-
|
problog_montecarlo(Goal,Delta,Prob) :-
|
||||||
nb_getval(probclause_counter,ID), !,
|
nb_getval(probclause_counter,ID), !,
|
||||||
C is ID+1,
|
C is ID+1,
|
||||||
|
@ -226,6 +226,7 @@ bdd_ptree_map(ID,FileBDD,FileParam,Mapping) :-
|
|||||||
|
|
||||||
add_probs([],[]).
|
add_probs([],[]).
|
||||||
add_probs([m(A,Name)|Map],[m(A,Name,Prob)|Mapping]) :-
|
add_probs([m(A,Name)|Map],[m(A,Name,Prob)|Mapping]) :-
|
||||||
|
% FIXME: Does this work with non-ground facts
|
||||||
problog:get_fact_probability(A,Prob),
|
problog:get_fact_probability(A,Prob),
|
||||||
add_probs(Map,Mapping).
|
add_probs(Map,Mapping).
|
||||||
|
|
||||||
@ -236,7 +237,9 @@ bdd_ptree_script(ID,FileBDD,FileParam) :-
|
|||||||
edges_ptree(ID,Edges),
|
edges_ptree(ID,Edges),
|
||||||
tell(FileParam),
|
tell(FileParam),
|
||||||
bdd_vars_script(Edges),
|
bdd_vars_script(Edges),
|
||||||
|
|
||||||
flush_output,
|
flush_output,
|
||||||
|
|
||||||
told,
|
told,
|
||||||
length(Edges,VarCount),
|
length(Edges,VarCount),
|
||||||
assert(c_num(1)),
|
assert(c_num(1)),
|
||||||
@ -246,6 +249,8 @@ bdd_ptree_script(ID,FileBDD,FileParam) :-
|
|||||||
tell(FileBDD),
|
tell(FileBDD),
|
||||||
format('@BDD1~n~w~n~w~n~w~n',[VarCount,0,IntermediateSteps]),
|
format('@BDD1~n~w~n~w~n~w~n',[VarCount,0,IntermediateSteps]),
|
||||||
output_compressed_script(CT),
|
output_compressed_script(CT),
|
||||||
|
|
||||||
|
|
||||||
told,
|
told,
|
||||||
retractall(c_num(_)),
|
retractall(c_num(_)),
|
||||||
retractall(compression(_,_)).
|
retractall(compression(_,_)).
|
||||||
@ -254,8 +259,35 @@ bdd_ptree_script(ID,FileBDD,FileParam) :-
|
|||||||
bdd_vars_script(Edges) :-
|
bdd_vars_script(Edges) :-
|
||||||
bdd_vars_script(Edges,0).
|
bdd_vars_script(Edges,0).
|
||||||
bdd_vars_script([],_).
|
bdd_vars_script([],_).
|
||||||
bdd_vars_script([A|B],N) :-
|
%%%% Bernd, changes for negated ground facts
|
||||||
problog:get_fact_probability(A,P),
|
bdd_vars_script([A0|B],N) :-
|
||||||
|
( A0=not(A) -> true; A=A0 ),
|
||||||
|
%%%% Bernd, changes for negated ground facts
|
||||||
|
|
||||||
|
% check wether it is a non-ground fact ID
|
||||||
|
|
||||||
|
|
||||||
|
(
|
||||||
|
number(A)
|
||||||
|
->
|
||||||
|
A_Number=A;
|
||||||
|
(
|
||||||
|
atom_chars(A,A_Chars),
|
||||||
|
% 95 = '_'
|
||||||
|
append(Part1,[95|Part2],A_Chars),
|
||||||
|
number_chars(A_Number,Part1),
|
||||||
|
number_chars(Grounding_ID,Part2)
|
||||||
|
)
|
||||||
|
),
|
||||||
|
(
|
||||||
|
problog:dynamic_probability_fact(A_Number)
|
||||||
|
->
|
||||||
|
(
|
||||||
|
problog:grounding_is_known(Goal,Grounding_ID),
|
||||||
|
problog:dynamic_probability_fact_extract(Goal,P)
|
||||||
|
);
|
||||||
|
problog:get_fact_probability(A_Number,P)
|
||||||
|
),
|
||||||
get_var_name(A,NameA),
|
get_var_name(A,NameA),
|
||||||
format('@~w~n~12f~n',[NameA,P]),
|
format('@~w~n~12f~n',[NameA,P]),
|
||||||
NN is N+1,
|
NN is N+1,
|
||||||
@ -322,8 +354,8 @@ ins_pt([A|B],[],[s(A,NewAT)]) :-
|
|||||||
%%%%%%%%%%%%
|
%%%%%%%%%%%%
|
||||||
|
|
||||||
% T is completely compressed and contains single variable
|
% T is completely compressed and contains single variable
|
||||||
% i.e. T of form x12
|
% i.e. T of form x12 or ~x34
|
||||||
compress_pt(T,TT) :-
|
compress_pt(T,TT) :-
|
||||||
atom(T),
|
atom(T),
|
||||||
test_var_name(T),
|
test_var_name(T),
|
||||||
!,
|
!,
|
||||||
@ -331,12 +363,12 @@ compress_pt(T,TT) :-
|
|||||||
assertz(compression(TT,[T])).
|
assertz(compression(TT,[T])).
|
||||||
% T is completely compressed and contains subtrees
|
% T is completely compressed and contains subtrees
|
||||||
% i.e. T of form 'L56'
|
% i.e. T of form 'L56'
|
||||||
compress_pt(T,T) :-
|
compress_pt(T,T) :-
|
||||||
atom(T).
|
atom(T).
|
||||||
% T not yet compressed
|
% T not yet compressed
|
||||||
% i.e. T is a tree-term (nested list & s/2 structure)
|
% i.e. T is a tree-term (nested list & s/2 structure)
|
||||||
% -> execute one layer of compression, then check again
|
% -> execute one layer of compression, then check again
|
||||||
compress_pt(T,CT) :-
|
compress_pt(T,CT) :-
|
||||||
\+ atom(T),
|
\+ atom(T),
|
||||||
and_or_compression(T,IT),
|
and_or_compression(T,IT),
|
||||||
compress_pt(IT,CT).
|
compress_pt(IT,CT).
|
||||||
@ -364,7 +396,7 @@ all_leaves_pt(T,L) :-
|
|||||||
|
|
||||||
some_leaf_pt([s(A,[])|_],s(A,[])).
|
some_leaf_pt([s(A,[])|_],s(A,[])).
|
||||||
some_leaf_pt([s(A,L)|_],s(A,L)) :-
|
some_leaf_pt([s(A,L)|_],s(A,L)) :-
|
||||||
atom(L).
|
not_or_atom(L).
|
||||||
some_leaf_pt([s(_,L)|_],X) :-
|
some_leaf_pt([s(_,L)|_],X) :-
|
||||||
some_leaf_pt(L,X).
|
some_leaf_pt(L,X).
|
||||||
some_leaf_pt([_|L],X) :-
|
some_leaf_pt([_|L],X) :-
|
||||||
@ -383,9 +415,17 @@ some_leaflist_pt([s(_,L)|_],X) :-
|
|||||||
some_leaflist_pt([_|L],X) :-
|
some_leaflist_pt([_|L],X) :-
|
||||||
some_leaflist_pt(L,X).
|
some_leaflist_pt(L,X).
|
||||||
|
|
||||||
|
not_or_atom(T) :-
|
||||||
|
(
|
||||||
|
T=not(T0)
|
||||||
|
->
|
||||||
|
atom(T0);
|
||||||
|
atom(T)
|
||||||
|
).
|
||||||
|
|
||||||
atomlist([]).
|
atomlist([]).
|
||||||
atomlist([A|B]) :-
|
atomlist([A|B]) :-
|
||||||
atom(A),
|
not_or_atom(A),
|
||||||
atomlist(B).
|
atomlist(B).
|
||||||
|
|
||||||
% for each subtree that will be compressed, add its name
|
% for each subtree that will be compressed, add its name
|
||||||
@ -393,23 +433,31 @@ atomlist([A|B]) :-
|
|||||||
compression_mapping([],[]).
|
compression_mapping([],[]).
|
||||||
compression_mapping([First|B],[N-First|BB]) :-
|
compression_mapping([First|B],[N-First|BB]) :-
|
||||||
(
|
(
|
||||||
First = s(A,[]) % subtree is literal -> use variable's name x17 from map
|
First = s(A0,[]) % subtree is literal -> use variable's name x17 from map (add ~ for negative case)
|
||||||
->
|
->
|
||||||
recorded(map,m(A,N),_)
|
(
|
||||||
|
A0=not(A)
|
||||||
|
->
|
||||||
|
(
|
||||||
|
recorded(map,m(A,Tmp),_), %check
|
||||||
|
atomic_concat(['~',Tmp],N)
|
||||||
|
);
|
||||||
|
recorded(map,m(A0,N),_) %check
|
||||||
|
)
|
||||||
;
|
;
|
||||||
(First = s(A,L),atom(L)) % subtree is node with single completely reduced child -> use next 'L'-based name
|
(First = s(A,L),not_or_atom(L)) % subtree is node with single completely reduced child -> use next 'L'-based name
|
||||||
-> (get_next_name(N),
|
-> (get_next_name(N),
|
||||||
assertz(compression(N,s(A,L))))
|
assertz(compression(N,s(A,L))))
|
||||||
;
|
;
|
||||||
(First = [L],atom(L)) % subtree is an OR with a single completely reduced element -> use element's name
|
(First = [L],not_or_atom(L)) % subtree is an OR with a single completely reduced element -> use element's name
|
||||||
-> N=L
|
-> N=L
|
||||||
;
|
;
|
||||||
(atomlist(First), % subtree is an OR with only (>1) completely reduced elements -> use next 'L'-based name
|
(atomlist(First), % subtree is an OR with only (>1) completely reduced elements -> use next 'L'-based name
|
||||||
get_next_name(N),
|
get_next_name(N),
|
||||||
assertz(compression(N,First)))
|
assertz(compression(N,First)))
|
||||||
),
|
),
|
||||||
compression_mapping(B,BB).
|
compression_mapping(B,BB).
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
% replace_pt(+T,+Map,-NT)
|
% replace_pt(+T,+Map,-NT)
|
||||||
@ -442,7 +490,7 @@ replace_pt_single(s(A,T),[M|Map],Res) :-
|
|||||||
replace_pt_single(s(A,T),[M|Map],s(A,TT)) :-
|
replace_pt_single(s(A,T),[M|Map],s(A,TT)) :-
|
||||||
replace_pt_list(T,[M|Map],TT).
|
replace_pt_list(T,[M|Map],TT).
|
||||||
replace_pt_single(A,_,A) :-
|
replace_pt_single(A,_,A) :-
|
||||||
atom(A).
|
not_or_atom(A).
|
||||||
|
|
||||||
%%%%%%%%%%%%
|
%%%%%%%%%%%%
|
||||||
% output for script
|
% output for script
|
||||||
@ -467,9 +515,20 @@ output_compressed_script(T) :-
|
|||||||
format_compression_script(Long),
|
format_compression_script(Long),
|
||||||
output_compressed_script(T)).
|
output_compressed_script(T)).
|
||||||
|
|
||||||
format_compression_script(s(A,B)) :-
|
format_compression_script(s(A0,B0)) :-
|
||||||
recorded(map,m(A,C),_),
|
% checkme
|
||||||
format('~w * ~w~n',[C,B]).
|
(
|
||||||
|
A0=not(A)
|
||||||
|
->
|
||||||
|
(
|
||||||
|
recorded(map,m(A,C),_),
|
||||||
|
format('~~~w * ~w~n',[C,B0])
|
||||||
|
) ;
|
||||||
|
(
|
||||||
|
recorded(map,m(A0,C),_),
|
||||||
|
format('~w * ~w~n',[C,B0])
|
||||||
|
)
|
||||||
|
).
|
||||||
format_compression_script([A]) :-
|
format_compression_script([A]) :-
|
||||||
format('~w~n',[A]).
|
format('~w~n',[A]).
|
||||||
format_compression_script([A,B|C]) :-
|
format_compression_script([A,B|C]) :-
|
||||||
@ -492,9 +551,17 @@ get_next_name(Name) :-
|
|||||||
% when changing, also adapt test_var_name/1 below
|
% when changing, also adapt test_var_name/1 below
|
||||||
get_var_name(A,NameA) :-
|
get_var_name(A,NameA) :-
|
||||||
atomic_concat([x,A],NameA),
|
atomic_concat([x,A],NameA),
|
||||||
recorda(map,m(A,NameA),_).
|
(
|
||||||
|
recorded(map,m(A,NameA),_)
|
||||||
|
->
|
||||||
|
true
|
||||||
|
;
|
||||||
|
recorda(map,m(A,NameA),_)
|
||||||
|
).
|
||||||
|
|
||||||
% test used by base case of compression mapping to detect single-variable tree
|
% test used by base case of compression mapping to detect single-variable tree
|
||||||
% has to match above naming scheme
|
% has to match above naming scheme
|
||||||
test_var_name(T) :-
|
test_var_name(T) :-
|
||||||
atomic_concat(x,_,T).
|
atomic_concat(x,_,T).
|
||||||
|
test_var_name(T) :-
|
||||||
|
atomic_concat('~x',_,T).
|
@ -1,281 +0,0 @@
|
|||||||
/******************************************************************************\
|
|
||||||
* *
|
|
||||||
* 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;
|
|
||||||
}
|
|
@ -1,131 +0,0 @@
|
|||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
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
|
|
@ -1,34 +0,0 @@
|
|||||||
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)
|
|
@ -1,670 +0,0 @@
|
|||||||
/******************************************************************************\
|
|
||||||
* *
|
|
||||||
* 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;
|
|
||||||
}
|
|
@ -1,141 +0,0 @@
|
|||||||
:-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.
|
|
||||||
|
|
@ -1,234 +0,0 @@
|
|||||||
/******************************************************************************\
|
|
||||||
* *
|
|
||||||
* 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);
|
|
||||||
}
|
|
@ -1,159 +0,0 @@
|
|||||||
/******************************************************************************\
|
|
||||||
* *
|
|
||||||
* 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
@ -1,287 +0,0 @@
|
|||||||
/******************************************************************************\
|
|
||||||
* *
|
|
||||||
* 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);
|
|
||||||
|
|
Reference in New Issue
Block a user