From f01fd0fbee26a335ec9e4b18495cc3bbfbef2bd0 Mon Sep 17 00:00:00 2001 From: Vitor Santos Costa Date: Fri, 6 Mar 2009 09:53:09 +0000 Subject: [PATCH] update ProbLog --- packages/ProbLog/learning.yap | 437 +++++- packages/ProbLog/problog.yap | 189 ++- packages/ProbLog/problog/tptree.yap | 107 +- packages/ProbLog/simplecudd/Example.c | 281 ---- packages/ProbLog/simplecudd/LICENCE | 131 -- packages/ProbLog/simplecudd/Makefile.in | 34 - packages/ProbLog/simplecudd/ProblogBDD.c | 670 --------- packages/ProbLog/simplecudd/SimpleCUDD.pl | 141 -- packages/ProbLog/simplecudd/general.c | 234 --- packages/ProbLog/simplecudd/general.h | 159 -- packages/ProbLog/simplecudd/simplecudd.c | 1620 --------------------- packages/ProbLog/simplecudd/simplecudd.h | 287 ---- 12 files changed, 643 insertions(+), 3647 deletions(-) delete mode 100644 packages/ProbLog/simplecudd/Example.c delete mode 100644 packages/ProbLog/simplecudd/LICENCE delete mode 100644 packages/ProbLog/simplecudd/Makefile.in delete mode 100644 packages/ProbLog/simplecudd/ProblogBDD.c delete mode 100644 packages/ProbLog/simplecudd/SimpleCUDD.pl delete mode 100644 packages/ProbLog/simplecudd/general.c delete mode 100644 packages/ProbLog/simplecudd/general.h delete mode 100644 packages/ProbLog/simplecudd/simplecudd.c delete mode 100644 packages/ProbLog/simplecudd/simplecudd.h diff --git a/packages/ProbLog/learning.yap b/packages/ProbLog/learning.yap index 92de9c0c9..9650f0d21 100644 --- a/packages/ProbLog/learning.yap +++ b/packages/ProbLog/learning.yap @@ -3,7 +3,7 @@ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Parameter Learning for ProbLog % -% 27.10.2008 +% 28.11.2008 % bernd.gutmann@cs.kuleuven.be %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @@ -61,6 +61,11 @@ :- dynamic log_frequency/1. :- dynamic alpha/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) :- (Flag=true;Flag=false), + !, retractall(rebuild_bdds(_)), assert(rebuild_bdds(Flag)). @@ -95,11 +101,13 @@ set_learning_flag(rebuild_bdds_it,Flag) :- set_learning_flag(reuse_initialized_bdds,Flag) :- (Flag=true;Flag=false), + !, retractall(reuse_initialized_bdds(_)), assert(reuse_initialized_bdds(Flag)). set_learning_flag(learning_rate,V) :- (V=examples -> true;(number(V),V>=0)), + !, retractall(learning_rate(_)), assert(learning_rate(V)). @@ -112,6 +120,7 @@ set_learning_flag(probability_initializer,(FactID,Probability,Query)) :- set_learning_flag(check_duplicate_bdds,Flag) :- (Flag=true;Flag=false), + !, retractall(check_duplicate_bdds(_)), assert(check_duplicate_bdds(Flag)). @@ -160,6 +169,34 @@ set_learning_flag(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), + L0, + 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 %= 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)), 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_start_timer(duration), @@ -668,10 +705,14 @@ random_probability(_FactID,Probability) :- %======================================================================== update_values :- + update_values(all). + + +update_values(_) :- values_correct, !. -update_values :- +update_values(What_To_Update) :- \+ values_correct, %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @@ -688,12 +729,17 @@ update_values :- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% open(Input_Filename,'write',Handle), - ( % go over all tunable facts + ( % go over all probabilistic fact get_fact_probability(ID,Prob), 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 ), @@ -710,7 +756,7 @@ update_values :- ( % go over all training examples current_predicate(user:example/3), user:example(QueryID,_Query,_QueryProb), - once(call_bdd_tool(QueryID,'.')), + once(call_bdd_tool(QueryID,'.',What_To_Update)), fail; % go to next training example true ), @@ -723,13 +769,16 @@ update_values :- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % start update values for all test examples %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - ( % go over all training examples - current_predicate(user:test_example/3), - user:test_example(QueryID,_Query,_QueryProb), - once(call_bdd_tool(QueryID,'+')), - fail; % go to next training example - true - ), + ( What_To_Update = all + -> + ( % go over all training examples + current_predicate(user:test_example/3), + user:test_example(QueryID,_Query,_QueryProb), + once(call_bdd_tool(QueryID,'+',all)), + fail; % go to next training example + true + ); true + ), %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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), query_directory(Query_Directory), ( @@ -759,15 +808,16 @@ call_bdd_tool(QueryID,Symbol) :- ( sigmoid_slope(Slope), problog_dir(PD), + (What_To_Update=all -> Method='g' ; Method='l'), atomic_concat([PD, - '/ProblogBDD -i "', + '/ProblogBDD -i "', Output_Directory, 'input.txt', '" -l "', Query_Directory, 'query_', QueryID, - '" -m g -id ', + '" -m ',Method,' -id ', QueryID, ' -sl ',Slope, ' > "', @@ -894,6 +944,25 @@ ground_truth_difference :- %= -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 mse_trainingset :- ( @@ -947,7 +1016,6 @@ mse_testset :- - %======================================================================== %= Calculates the sigmoid function respectivly the inverse of it %= 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 %======================================================================== +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 :- + + save_old_probabilities, update_values, %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @@ -998,7 +1122,8 @@ gradient_descent :- ( % go over all tunable facts tunable_fact(FactID,_), - bb_put(FactID,0.0), + atomic_concat(['grad_',FactID],Key), + bb_put(Key,0.0), fail; % go to next tunable fact true @@ -1029,15 +1154,18 @@ gradient_descent :- ( % go over all tunable facts tunable_fact(FactID,_), - ( - query_gradient(QueryID,FactID,GradValue) - -> - true; - GradValue=0.0 - ), - bb_get(FactID,OldValue), + atomic_concat(['grad_',FactID],Key), + + % if the following query fails, + % it means, the fact is not used in the proof + % of QueryID, and the gradient is 0.0 and will + % not contribute to NewValue either way + % DON'T FORGET THIS IF YOU CHANGE SOMETHING HERE! + query_gradient(QueryID,FactID,GradValue), + + bb_get(Key,OldValue), NewValue is OldValue + Y*GradValue, - bb_put(FactID,NewValue), + bb_put(Key,NewValue), fail; % go to next fact true @@ -1054,7 +1182,7 @@ gradient_descent :- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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), max_list(GradientValues,GradMax), @@ -1068,39 +1196,236 @@ gradient_descent :- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % stop statistics on gradient %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - - + + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % start add gradient to current probabilities %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - - learning_rate(LearningRate), - - ( % go over all tunable facts - - 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 + ( + line_search(false) + -> + learning_rate(LearningRate); + lineSearch(LearningRate,_) ), + format('learning rate = ~12f~n',[LearningRate]), + add_gradient(LearningRate), + logger_set_variable(learning_rate,LearningRate), %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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 + (VTemp1=V1,FTemp1=F1); + (VTemp1=V2,FTemp1=F2) + ), + ( + V3 + (VTemp2=V3,FTemp2=F3); + (VTemp2=V4,FTemp2=F4) + ), + ( + VTemp1 + (VTemp3=VTemp1,FTemp3=FTemp1); + (VTemp3=VTemp2,FTemp3=FTemp2) + ), + ( + VTemp3 + (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(init_method,(Query,Probability,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(duration,time), @@ -1137,7 +1467,8 @@ global_initialize :- logger_define_variable(gradient_max,float), logger_define_variable(ground_truth_diff,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). %======================================================================== %= diff --git a/packages/ProbLog/problog.yap b/packages/ProbLog/problog.yap index fc79568d1..6a8fe010b 100644 --- a/packages/ProbLog/problog.yap +++ b/packages/ProbLog/problog.yap @@ -28,6 +28,7 @@ set_fact_probability/2, get_fact/2, tunable_fact/2, + non_ground_fact/1, export_facts/1, problog_help/0, problog_dir/1, @@ -73,6 +74,7 @@ :- dynamic problog_predicate/2. % global over all inference methods, exported :- dynamic tunable_fact/2. +:- dynamic non_ground_fact/1. :- dynamic problog_dir/1. % global, manipulated via problog_control/2 :- dynamic up/0. @@ -90,6 +92,12 @@ :- dynamic max_proof/1. % local to problog_montecarlo :- 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 % 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) :- + copy_term((P,Goal),(P_Copy,Goal_Copy)), functor(Goal, Name, Arity), atomic_concat([problog_,Name],ProblogName), Goal =.. [Name|Args], append(Args,[LProb],L1), - probclause_id(IDName), - term_variables(Goal,GVars), - (GVars=[] -> ID=IDName; ID=..[IDName|GVars]), + probclause_id(ID), ProbFact =.. [ProblogName,ID|L1], - (P = t(TrueProb) -> - assert(tunable_fact(ID,TrueProb)), - LProb is log(0.5) - ; - LProb is log(P) - ), - problog_predicate(Name, Arity, ProblogName). + ( + (\+ var(P), P = t(TrueProb)) + -> + ( + assert(tunable_fact(ID,TrueProb)), + LProb is log(0.5) + ); + ( + 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 problog_predicate(Name, Arity, _) :- problog_predicate(Name, Arity), !. + problog_predicate(Name, Arity, ProblogName) :- functor(OriginalGoal, Name, Arity), OriginalGoal =.. [_|Args], append(Args,[Prob],L1), ProbFact =.. [ProblogName,ID|L1], prolog_load_context(module,Mod), - assert((Mod:OriginalGoal :- ProbFact, add_to_proof(ID,Prob))), + + assert( (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)), ArityPlus2 is Arity+2, dynamic(problog:ProblogName/ArityPlus2). @@ -242,6 +306,34 @@ probclause_id(ID) :- probclause_id(0) :- 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 % hardware-access version: naively scan all problog-predicates @@ -306,7 +398,8 @@ get_fact(ID,OutsideTerm) :- get_fact_list([],[]). 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). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @@ -317,7 +410,7 @@ get_fact_list([ID|IDs],[Fact|Facts]) :- % - 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 fact used before, succeed and keep status as is % if not prunable, calculate probability and @@ -329,6 +422,11 @@ add_to_proof(ID,Prob) :- b_getval(problog_probability, CurrentP), nb_getval(problog_threshold, CurrentThreshold), b_getval(problog_current_proof, IDs), + +%%%% Bernd, changes for negated ground facts + \+ memberchk(not(ID),IDs), +%%%% Bernd, changes for negated ground facts + ( MaxSteps =< 0 -> fail ; @@ -349,6 +447,44 @@ add_to_proof(ID,Prob) :- 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 montecarlo_check(ID) :- ( @@ -394,6 +530,7 @@ multiply_probabilities(CurrentLogP, LogProb, NLogProb) :- % this is called by all inference methods before the actual ProbLog goal % to set up environment for proving init_problog(Threshold) :- + reset_non_ground_facts, LT is log(Threshold), b_setval(problog_probability, 0.0), b_setval(problog_current_proof, []), @@ -412,6 +549,8 @@ prune_check(Proof,TreeID) :- % (as logical part is there, but probabilistic part in problog) problog_call(Goal) :- 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), call(ModGoal). @@ -446,7 +585,12 @@ put_module(Goal,Module,Module:Goal). eval_dnf(ID,Prob,Status) :- ((ID = 1, problog_flag(save_bdd,true)) -> problog_control(on,remember); problog_control(off,remember)), count_ptree(ID,NX), - format(user,'~w proofs~n',[NX]), + ( + NX=1 + -> + format(user,'1 proof~n',[]); + format(user,'~w proofs~n',[NX]) + ), problog_flag(dir,DirFlag), problog_flag(bdd_file,BDDFileFlag), atomic_concat([DirFlag,BDDFileFlag],BDDFile), @@ -703,8 +847,8 @@ problog_max(Goal, Prob, Facts) :- problog_flag(first_threshold,InitT), init_problog_max(InitT), problog_max_id(Goal, Prob, FactIDs), - ( FactIDs == unprovable -> Facts = unprovable; - get_fact_list(FactIDs,Facts)). + ( FactIDs = [_|_] -> get_fact_list(FactIDs,Facts); + Facts = FactIDs). init_problog_max(Threshold) :- retractall(max_probability(_)), @@ -736,7 +880,10 @@ problog_max_id(Goal, Prob, Clauses) :- nb_getval(problog_threshold, LT), problog_flag(last_threshold_log,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) ; 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 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +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) :- nb_getval(probclause_counter,ID), !, C is ID+1, diff --git a/packages/ProbLog/problog/tptree.yap b/packages/ProbLog/problog/tptree.yap index a4fc28ee5..53a222785 100644 --- a/packages/ProbLog/problog/tptree.yap +++ b/packages/ProbLog/problog/tptree.yap @@ -226,6 +226,7 @@ bdd_ptree_map(ID,FileBDD,FileParam,Mapping) :- add_probs([],[]). 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), add_probs(Map,Mapping). @@ -236,7 +237,9 @@ bdd_ptree_script(ID,FileBDD,FileParam) :- edges_ptree(ID,Edges), tell(FileParam), bdd_vars_script(Edges), + flush_output, + told, length(Edges,VarCount), assert(c_num(1)), @@ -246,6 +249,8 @@ bdd_ptree_script(ID,FileBDD,FileParam) :- tell(FileBDD), format('@BDD1~n~w~n~w~n~w~n',[VarCount,0,IntermediateSteps]), output_compressed_script(CT), + + told, retractall(c_num(_)), retractall(compression(_,_)). @@ -254,8 +259,35 @@ bdd_ptree_script(ID,FileBDD,FileParam) :- bdd_vars_script(Edges) :- bdd_vars_script(Edges,0). bdd_vars_script([],_). -bdd_vars_script([A|B],N) :- - problog:get_fact_probability(A,P), +%%%% Bernd, changes for negated ground facts +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), format('@~w~n~12f~n',[NameA,P]), NN is N+1, @@ -322,8 +354,8 @@ ins_pt([A|B],[],[s(A,NewAT)]) :- %%%%%%%%%%%% % T is completely compressed and contains single variable -% i.e. T of form x12 -compress_pt(T,TT) :- +% i.e. T of form x12 or ~x34 +compress_pt(T,TT) :- atom(T), test_var_name(T), !, @@ -331,12 +363,12 @@ compress_pt(T,TT) :- assertz(compression(TT,[T])). % T is completely compressed and contains subtrees % i.e. T of form 'L56' -compress_pt(T,T) :- +compress_pt(T,T) :- atom(T). % T not yet compressed % i.e. T is a tree-term (nested list & s/2 structure) % -> execute one layer of compression, then check again -compress_pt(T,CT) :- +compress_pt(T,CT) :- \+ atom(T), and_or_compression(T,IT), 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,L)|_],s(A,L)) :- - atom(L). + not_or_atom(L). some_leaf_pt([s(_,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). +not_or_atom(T) :- + ( + T=not(T0) + -> + atom(T0); + atom(T) + ). + atomlist([]). atomlist([A|B]) :- - atom(A), + not_or_atom(A), atomlist(B). % for each subtree that will be compressed, add its name @@ -393,23 +433,31 @@ atomlist([A|B]) :- compression_mapping([],[]). 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), 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 ; - (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), assertz(compression(N,First))) ), compression_mapping(B,BB). - + % 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_list(T,[M|Map],TT). replace_pt_single(A,_,A) :- - atom(A). + not_or_atom(A). %%%%%%%%%%%% % output for script @@ -467,9 +515,20 @@ output_compressed_script(T) :- format_compression_script(Long), output_compressed_script(T)). -format_compression_script(s(A,B)) :- - recorded(map,m(A,C),_), - format('~w * ~w~n',[C,B]). +format_compression_script(s(A0,B0)) :- + % checkme + ( + 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('~w~n',[A]). format_compression_script([A,B|C]) :- @@ -492,9 +551,17 @@ get_next_name(Name) :- % when changing, also adapt test_var_name/1 below get_var_name(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 % has to match above naming scheme test_var_name(T) :- - atomic_concat(x,_,T). \ No newline at end of file + atomic_concat(x,_,T). +test_var_name(T) :- + atomic_concat('~x',_,T). \ No newline at end of file diff --git a/packages/ProbLog/simplecudd/Example.c b/packages/ProbLog/simplecudd/Example.c deleted file mode 100644 index c0dab075f..000000000 --- a/packages/ProbLog/simplecudd/Example.c +++ /dev/null @@ -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; -} diff --git a/packages/ProbLog/simplecudd/LICENCE b/packages/ProbLog/simplecudd/LICENCE deleted file mode 100644 index 5f221241e..000000000 --- a/packages/ProbLog/simplecudd/LICENCE +++ /dev/null @@ -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 diff --git a/packages/ProbLog/simplecudd/Makefile.in b/packages/ProbLog/simplecudd/Makefile.in deleted file mode 100644 index 287f91715..000000000 --- a/packages/ProbLog/simplecudd/Makefile.in +++ /dev/null @@ -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) diff --git a/packages/ProbLog/simplecudd/ProblogBDD.c b/packages/ProbLog/simplecudd/ProblogBDD.c deleted file mode 100644 index 687216e20..000000000 --- a/packages/ProbLog/simplecudd/ProblogBDD.c +++ /dev/null @@ -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 - -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; -} diff --git a/packages/ProbLog/simplecudd/SimpleCUDD.pl b/packages/ProbLog/simplecudd/SimpleCUDD.pl deleted file mode 100644 index 9fe1ecfb0..000000000 --- a/packages/ProbLog/simplecudd/SimpleCUDD.pl +++ /dev/null @@ -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. - diff --git a/packages/ProbLog/simplecudd/general.c b/packages/ProbLog/simplecudd/general.c deleted file mode 100644 index 64a7f88e1..000000000 --- a/packages/ProbLog/simplecudd/general.c +++ /dev/null @@ -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); -} diff --git a/packages/ProbLog/simplecudd/general.h b/packages/ProbLog/simplecudd/general.h deleted file mode 100644 index 4441ed623..000000000 --- a/packages/ProbLog/simplecudd/general.h +++ /dev/null @@ -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 -#include -#include - -#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); diff --git a/packages/ProbLog/simplecudd/simplecudd.c b/packages/ProbLog/simplecudd/simplecudd.c deleted file mode 100644 index 6ee290377..000000000 --- a/packages/ProbLog/simplecudd/simplecudd.c +++ /dev/null @@ -1,1620 +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.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" - -/* BDD manager initialization */ - -int _debug = 0; -int _RapidLoad = 0; -int _maxbufsize = 0; - -DdManager* simpleBDDinit(int varcnt) { - DdManager *temp; - temp = Cudd_Init(varcnt, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0); - Cudd_AutodynEnable(temp, CUDD_REORDER_GROUP_SIFT); - Cudd_SetMaxCacheHard(temp, 1024*1024*1024); - Cudd_SetLooseUpTo(temp, 1024*1024*512); - if (_debug) Cudd_EnableReorderingReporting(temp); - return temp; -} - -/* BDD tree travesrsing */ - -DdNode* HighNodeOf(DdManager *manager, DdNode *node) { - DdNode *tmp; - if (IsHigh(manager, node)) return HIGH(manager); - if (IsLow(manager, node)) return LOW(manager); - tmp = Cudd_Regular(node); - if (Cudd_IsComplement(node)) return NOT(tmp->type.kids.T); - return tmp->type.kids.T; -} - -DdNode* LowNodeOf(DdManager *manager, DdNode *node) { - DdNode *tmp; - if (IsHigh(manager, node)) return HIGH(manager); - if (IsLow(manager, node)) return LOW(manager); - tmp = Cudd_Regular(node); - if (Cudd_IsComplement(node)) return NOT(tmp->type.kids.E); - return tmp->type.kids.E; -} - -/* BDD tree generation */ - -DdNode* D_BDDAnd(DdManager *manager, DdNode *bdd1, DdNode *bdd2) { - DdNode *tmp; - tmp = Cudd_bddAnd(manager, bdd1, bdd2); - Cudd_Ref(tmp); - Cudd_RecursiveDeref(manager, bdd2); - return tmp; -} - -DdNode* D_BDDNand(DdManager *manager, DdNode *bdd1, DdNode *bdd2) { - DdNode *tmp; - tmp = Cudd_bddNand(manager, bdd1, bdd2); - Cudd_Ref(tmp); - Cudd_RecursiveDeref(manager, bdd2); - return tmp; -} - -DdNode* D_BDDOr(DdManager *manager, DdNode *bdd1, DdNode *bdd2) { - DdNode *tmp; - tmp = Cudd_bddOr(manager, bdd1, bdd2); - Cudd_Ref(tmp); - Cudd_RecursiveDeref(manager, bdd2); - return tmp; -} - -DdNode* D_BDDNor(DdManager *manager, DdNode *bdd1, DdNode *bdd2) { - DdNode *tmp; - tmp = Cudd_bddNor(manager, bdd1, bdd2); - Cudd_Ref(tmp); - Cudd_RecursiveDeref(manager, bdd2); - return tmp; -} - -DdNode* D_BDDXor(DdManager *manager, DdNode *bdd1, DdNode *bdd2) { - DdNode *tmp; - tmp = Cudd_bddXor(manager, bdd1, bdd2); - Cudd_Ref(tmp); - Cudd_RecursiveDeref(manager, bdd2); - return tmp; -} - -DdNode* D_BDDXnor(DdManager *manager, DdNode *bdd1, DdNode *bdd2) { - DdNode *tmp; - tmp = Cudd_bddXnor(manager, bdd1, bdd2); - Cudd_Ref(tmp); - Cudd_RecursiveDeref(manager, bdd2); - return tmp; -} - -/* file manipulation */ - -bddfileheader ReadFileHeader(char *filename) { - bddfileheader temp; - char *header; - temp.inputfile = NULL; - temp.version = 0; - temp.varcnt = 0; - temp.varstart = 0; - temp.intercnt = 0; - temp.filetype = BDDFILE_OTHER; - if ((temp.inputfile = fopen(filename, "r")) == NULL) { - perror(filename); - temp.filetype = BDDFILE_ERROR; - return temp; - } - // Read file header - if (!feof(temp.inputfile)) { - header = freadline(temp.inputfile); - temp.version = CheckFileVersion(header); - if (temp.version > -1) temp.filetype = (strlen(header) == 5) * BDDFILE_SCRIPT + (strlen(header) == 7) * BDDFILE_NODEDUMP; - free(header); - switch (temp.filetype) { - case BDDFILE_SCRIPT: - switch (temp.version) { - case 1: - fscanf(temp.inputfile, "%i\n", &temp.varcnt); - fscanf(temp.inputfile, "%i\n", &temp.varstart); - fscanf(temp.inputfile, "%i\n", &temp.intercnt); - break; - default: - fclose(temp.inputfile); - temp.inputfile = NULL; - break; - } - break; - case BDDFILE_NODEDUMP: - switch (temp.version) { - case 1: - fscanf(temp.inputfile, "%i\n", &temp.varcnt); - fscanf(temp.inputfile, "%i\n", &temp.varstart); - break; - default: - fclose(temp.inputfile); - temp.inputfile = NULL; - break; - } - break; - case BDDFILE_OTHER: - fclose(temp.inputfile); - temp.inputfile = NULL; - break; - default: - fclose(temp.inputfile); - temp.inputfile = NULL; - break; - } - } - return temp; -} - -int CheckFileVersion(const char *version) { - if (strlen(version) < 5) return -1; - if (strlen(version) == 5 && version[0] == '@' && version[1] == 'B' && version[2] == 'D' && version[3] == 'D') return atoi(version + 4); - if (strlen(version) == 7 && version[0] == '@' && version[1] == 'N' && version[2] == 'O' && version[3] == 'D' - && version[4] == 'E' && version[5] == 'S') return atoi(version + 6); - return -1; -} - -int simpleBDDtoDot(DdManager *manager, DdNode *bdd, char *filename) { - DdNode *f[1]; - int ret; - FILE *fd; - f[0] = Cudd_BddToAdd(manager, bdd); - fd = fopen(filename, "w"); - if (fd == NULL) { - perror(filename); - return -1; - } - ret = Cudd_DumpDot(manager, 1, f, NULL, NULL, fd); - fclose(fd); - return ret; -} - -int simpleNamedBDDtoDot(DdManager *manager, namedvars varmap, DdNode *bdd, char *filename) { - DdNode *f[1]; - int ret; - FILE *fd; - f[0] = Cudd_BddToAdd(manager, bdd); - fd = fopen(filename, "w"); - if (fd == NULL) { - perror(filename); - return -1; - } - ret = Cudd_DumpDot(manager, 1, f, varmap.vars, NULL, fd); - fclose(fd); - return ret; -} - -int SaveNodeDump(DdManager *manager, namedvars varmap, DdNode *bdd, char *filename) { - hisqueue *Nodes; - FILE *outputfile; - int i; - if ((outputfile = fopen(filename, "w")) == NULL) { - perror(filename); - return -1; - } - fprintf(outputfile, "%s\n%i\n%i\n", "@NODES1", varmap.varcnt, varmap.varstart); - Nodes = InitHistory(varmap.varcnt); - for (i = 0; i < varmap.varcnt; i++) - fprintf(outputfile, "%s\t%i\n", varmap.vars[i], Cudd_ReadPerm(manager, i)); - if (bdd == HIGH(manager)) fprintf(outputfile, "TRUE\t0\tTRUE\t0\tTRUE\t0\n"); - else if (bdd == LOW(manager)) fprintf(outputfile, "FALSE\t0\tFALSE\t0\tFALSE\t0\n"); - else SaveExpand(manager, varmap, Nodes, bdd, outputfile); - ReInitHistory(Nodes, varmap.varcnt); - free(Nodes); - fclose(outputfile); - return 0; -} - -void SaveExpand(DdManager *manager, namedvars varmap, hisqueue *Nodes, DdNode *Current, FILE *outputfile) { - DdNode *h, *l; - hisnode *Found; - char *curnode; - int inode; - if (Current != HIGH(manager) && Current != LOW(manager)) { - if ((Found = GetNode(Nodes, varmap.varstart, Current)) == NULL) { - AddNode(Nodes, varmap.varstart, Current, 0.0, 0, NULL); - Found = GetNode(Nodes, varmap.varstart, Current); - } - if (!(Found->ivalue)) { - Found->ivalue = 1; - curnode = GetNodeVarNameDisp(manager, varmap, Current); - inode = GetNodeIndex(Nodes, varmap.varstart, Current); - fprintf(outputfile, "%s\t%i\t", curnode, inode); - h = HighNodeOf(manager, Current); - if (h == HIGH(manager)) { - fprintf(outputfile, "TRUE\t0\t"); - } else if (h == LOW(manager)) { - fprintf(outputfile, "FALSE\t0\t"); - } else { - if (GetNode(Nodes, varmap.varstart, h) == NULL) AddNode(Nodes, varmap.varstart, h, 0.0, 0, NULL); - curnode = GetNodeVarNameDisp(manager, varmap, h); - inode = GetNodeIndex(Nodes, varmap.varstart, h); - fprintf(outputfile, "%s\t%i\t", curnode, inode); - } - l = LowNodeOf(manager, Current); - if (l == HIGH(manager)) { - fprintf(outputfile, "TRUE\t0\n"); - } else if (l == LOW(manager)) { - fprintf(outputfile, "FALSE\t0\n"); - } else { - if (GetNode(Nodes, varmap.varstart, l) == NULL) AddNode(Nodes, varmap.varstart, l, 0.0, 0, NULL); - curnode = GetNodeVarNameDisp(manager, varmap, l); - inode = GetNodeIndex(Nodes, varmap.varstart, l); - fprintf(outputfile, "%s\t%i\n", curnode, inode); - } - SaveExpand(manager, varmap, Nodes, l, outputfile); - SaveExpand(manager, varmap, Nodes, h, outputfile); - } - } -} - -DdNode * LoadNodeDump(DdManager *manager, namedvars varmap, FILE *inputfile) { - hisqueue *Nodes; - nodeline temp; - DdNode *ret; - int i, pos, *perm; - char *varnam; - perm = (int *) malloc(sizeof(int) * varmap.varcnt); - Nodes = InitHistory(varmap.varcnt); - for (i = 0; i < varmap.varcnt; i++) { - varnam = freadstr(inputfile, "\t"); - pos = atoi(freadstr(inputfile, "\n")); - AddNamedVarAt(varmap, varnam, pos); - perm[pos] = pos; - } - temp.varname = freadstr(inputfile, "\t"); - fscanf(inputfile, "%i\t", &temp.nodenum); - temp.truevar = freadstr(inputfile, "\t"); - fscanf(inputfile, "%i\t", &temp.truenode); - temp.falsevar = freadstr(inputfile, "\t"); - fscanf(inputfile, "%i\n", &temp.falsenode); - ret = LoadNodeRec(manager, varmap, Nodes, inputfile, temp); - free(temp.varname); - free(temp.truevar); - free(temp.falsevar); - fclose(inputfile); - ReInitHistory(Nodes, varmap.varcnt); - free(Nodes); - Cudd_Ref(ret); - Cudd_ShuffleHeap(manager, perm); - for (i = 0; i < varmap.varcnt; i++) varmap.ivalue[i] = 0; - return ret; -} - -DdNode * LoadNodeRec(DdManager *manager, namedvars varmap, hisqueue *Nodes, FILE *inputfile, nodeline current) { - nodeline temp; - DdNode *newnode, *truenode, *falsenode; - int index; - newnode = GetIfExists(manager, varmap, Nodes, current.varname, current.nodenum); - if (newnode != NULL) return newnode; - falsenode = GetIfExists(manager, varmap, Nodes, current.falsevar, current.falsenode); - if (falsenode == NULL) { - temp.varname = freadstr(inputfile, "\t"); - fscanf(inputfile, "%i\t", &temp.nodenum); - temp.truevar = freadstr(inputfile, "\t"); - fscanf(inputfile, "%i\t", &temp.truenode); - temp.falsevar = freadstr(inputfile, "\t"); - fscanf(inputfile, "%i\n", &temp.falsenode); - falsenode = LoadNodeRec(manager, varmap, Nodes, inputfile, temp); - free(temp.varname); - free(temp.truevar); - free(temp.falsevar); - } - truenode = GetIfExists(manager, varmap, Nodes, current.truevar, current.truenode); - if (truenode == NULL) { - temp.varname = freadstr(inputfile, "\t"); - fscanf(inputfile, "%i\t", &temp.nodenum); - temp.truevar = freadstr(inputfile, "\t"); - fscanf(inputfile, "%i\t", &temp.truenode); - temp.falsevar = freadstr(inputfile, "\t"); - fscanf(inputfile, "%i\n", &temp.falsenode); - truenode = LoadNodeRec(manager, varmap, Nodes, inputfile, temp); - free(temp.varname); - free(temp.truevar); - free(temp.falsevar); - } - index = GetNamedVarIndex(varmap, current.varname); - if (!varmap.ivalue[index]) { - varmap.ivalue[index] = 1; - newnode = GetVar(manager, varmap.varstart + index); - //Cudd_RecursiveDeref(manager, newnode->type.kids.T); - //Cudd_RecursiveDeref(manager, newnode->type.kids.E); - newnode->type.kids.T = Cudd_NotCond(truenode, Cudd_IsComplement(truenode)); - newnode->type.kids.E = Cudd_NotCond(falsenode, Cudd_IsComplement(truenode)); - Cudd_Ref(newnode->type.kids.T); - Cudd_Ref(newnode->type.kids.E); - Cudd_Ref(newnode); - } else { - if (_RapidLoad == 1) { - newnode = cuddAllocNode(manager); - if (newnode != NULL) { - newnode->index = varmap.varstart + index; - newnode->type.kids.T = Cudd_NotCond(truenode, Cudd_IsComplement(truenode)); - newnode->type.kids.E = Cudd_NotCond(falsenode, Cudd_IsComplement(truenode)); - Cudd_Ref(newnode->type.kids.T); - Cudd_Ref(newnode->type.kids.E); - Cudd_Ref(newnode); - } - } else { - newnode = cuddUniqueInter(manager, varmap.varstart + index, Cudd_NotCond(truenode, Cudd_IsComplement(truenode)), Cudd_NotCond(falsenode, Cudd_IsComplement(truenode))); - if (newnode != NULL) { - Cudd_Ref(newnode); - } else { - newnode = cuddAllocNode(manager); - if (newnode != NULL) { - newnode->index = varmap.varstart + index; - newnode->type.kids.T = Cudd_NotCond(truenode, Cudd_IsComplement(truenode)); - newnode->type.kids.E = Cudd_NotCond(falsenode, Cudd_IsComplement(truenode)); - Cudd_Ref(newnode->type.kids.T); - Cudd_Ref(newnode->type.kids.E); - Cudd_Ref(newnode); - } - } - } - } - if (newnode != NULL) { - Nodes[index].thenode[current.nodenum].key = Cudd_NotCond(newnode, Cudd_IsComplement(truenode)); - return Cudd_NotCond(newnode, Cudd_IsComplement(truenode)); - } - return NULL; -} - -DdNode * GetIfExists(DdManager *manager, namedvars varmap, hisqueue *Nodes, char *varname, int nodenum) { - int index; - if (strcmp(varname, "TRUE") == 0) return HIGH(manager); - if (strcmp(varname, "FALSE") == 0) return LOW(manager); - index = GetNamedVarIndex(varmap, varname); - if (index == -1 * varmap.varcnt) { - fprintf(stderr, "Error: more variables requested than initialized.\n"); - exit(-1); - } - if ((index < 0) || (index == 0 && varmap.vars[0] == NULL)) { - index = AddNamedVar(varmap, varname); - } - ExpandNodes(Nodes, index, nodenum); - if (Nodes[index].thenode[nodenum].key != NULL) return Nodes[index].thenode[nodenum].key; - return NULL; -} - -void ExpandNodes(hisqueue *Nodes, int index, int nodenum) { - int i; - if (Nodes[index].cnt > nodenum) return; - Nodes[index].thenode = (hisnode *) realloc(Nodes[index].thenode, (nodenum + 1) * sizeof(hisnode)); - for (i = Nodes[index].cnt; i < nodenum + 1; i++) { - Nodes[index].thenode[i].key = NULL; - Nodes[index].thenode[i].ivalue = 0; - Nodes[index].thenode[i].dvalue = 0.0; - Nodes[index].thenode[i].dynvalue = NULL; - } - Nodes[index].cnt = nodenum + 1; -} - -int LoadVariableData(namedvars varmap, char *filename) { - FILE *data; - char *dataread, buf, *varname, *dynvalue; - double dvalue = 0.0; - int icur = 0, maxbufsize = 10, hasvar = 0, index = -1, idat = 0, ivalue = 0; - dynvalue = NULL; - if ((data = fopen(filename, "r")) == NULL) { - perror("fopen"); - return -1; - } - dataread = (char *) malloc(sizeof(char) * maxbufsize); - while(!feof(data)) { - fread(&buf, 1, 1, data); - if (buf == '\n') { - dataread[icur] = '\0'; - icur = 0; - buf = ' '; - if (dataread[0] == '@') { - if (hasvar) { - for (index = 0; index < varmap.varcnt; index++) { - if (patternmatch(varname, varmap.vars[index])) { - varmap.loaded[index] = 1; - varmap.dvalue[index] = dvalue; - varmap.ivalue[index] = ivalue; - if (varmap.dynvalue[index] != NULL) { - free(varmap.dynvalue[index]); - varmap.dynvalue[index] = NULL; - } - if (dynvalue != NULL) { - varmap.dynvalue[index] = (void *) malloc(sizeof(char) * (strlen(dynvalue) + 1)); - strcpy(varmap.dynvalue[index], dynvalue); - } - } - } - dvalue = 0.0; - ivalue = 0; - if (dynvalue != NULL) { - free(dynvalue); - dynvalue = NULL; - } - free(varname); - } - varname = (char *) malloc(sizeof(char) * strlen(dataread)); - strcpy(varname, dataread + 1); - hasvar = 1; - idat = 0; - } else { - if (hasvar >= 0) { - switch(idat) { - case 0: - if (IsRealNumber(dataread)) dvalue = atof(dataread); - else { - fprintf(stderr, "Error at file: %s. Variable: %s can't have non real value: %s.\n", filename, varname, dataread); - fclose(data); - free(varname); - free(dataread); - return -2; - } - idat++; - break; - case 1: - if (IsNumber(dataread)) ivalue = atoi(dataread); - else { - fprintf(stderr, "Error at file: %s. Variable: %s can't have non integer value: %s.\n", filename, varname, dataread); - fclose(data); - free(varname); - free(dataread); - return -2; - } - idat++; - break; - case 2: - dynvalue = malloc(sizeof(char) * (strlen(dataread) + 1)); - strcpy(dynvalue, dataread); - break; - } - } - } - } else { - dataread[icur] = buf; - icur++; - if (icur == _maxbufsize) { - fprintf(stderr, "Error: Maximum buffer size(%i) exceeded.\n", _maxbufsize); - fclose(data); - free(varname); - free(dataread); - return -2; - } - while (icur > maxbufsize - 1) { - maxbufsize *= 2; - dataread = (char *) realloc(dataread, sizeof(char) * maxbufsize); - } - } - } - if (hasvar) { - for (index = 0; index < varmap.varcnt; index++) { - if (patternmatch(varname, varmap.vars[index])) { - varmap.loaded[index] = 1; - varmap.dvalue[index] = dvalue; - varmap.ivalue[index] = ivalue; - if (dynvalue != NULL) { - varmap.dynvalue[index] = (void *) malloc(sizeof(char) * (strlen(dynvalue) + 1)); - strcpy(varmap.dynvalue[index], dynvalue); - } - } - } - if (dynvalue != NULL) { - free(dynvalue); - dynvalue = NULL; - } - free(varname); - } - fclose(data); - free(dataread); - return 0; -} - -/* Queue for node storing to avoid loops */ - -hisqueue* InitHistory(int varcnt) { - int i; - hisqueue *HisQueue; - HisQueue = (hisqueue *) malloc(sizeof(hisqueue) * varcnt); - for (i = 0; i < varcnt; i++) { - HisQueue[i].thenode = NULL; - HisQueue[i].cnt = 0; - } - return HisQueue; -} - -void ReInitHistory(hisqueue *HisQueue, int varcnt) { - int i, j; - for (i = 0; i < varcnt; i++) { - if (HisQueue[i].thenode != NULL) { - for (j = 0; j < HisQueue[i].cnt; j++) - if (HisQueue[i].thenode[j].dynvalue != NULL) free(HisQueue[i].thenode[j].dynvalue); - free(HisQueue[i].thenode); - HisQueue[i].thenode = NULL; - } - HisQueue[i].cnt = 0; - } -} - -void AddNode(hisqueue *HisQueue, int varstart, DdNode *node, double dvalue, int ivalue, void *dynvalue) { - int index = GetIndex(node) - varstart; - HisQueue[index].thenode = (hisnode *) realloc(HisQueue[index].thenode, (HisQueue[index].cnt + 1) * sizeof(hisnode)); - HisQueue[index].thenode[HisQueue[index].cnt].key = node; - HisQueue[index].thenode[HisQueue[index].cnt].dvalue = dvalue; - HisQueue[index].thenode[HisQueue[index].cnt].ivalue = ivalue; - HisQueue[index].thenode[HisQueue[index].cnt].dynvalue = dynvalue; - HisQueue[index].cnt += 1; -} - -hisnode* GetNode(hisqueue *HisQueue, int varstart, DdNode *node) { - int i; - int index = GetIndex(node) - varstart; - for(i = 0; i < HisQueue[index].cnt; i++) { - if (HisQueue[index].thenode[i].key == node) return &(HisQueue[index].thenode[i]); - } - return NULL; -} - -int GetNodeIndex(hisqueue *HisQueue, int varstart, DdNode *node) { - int i; - int index = GetIndex(node) - varstart; - for(i = 0; i < HisQueue[index].cnt; i++) { - if (HisQueue[index].thenode[i].key == node) return i; - } - return -1; -} - -/* Named variables */ - -namedvars InitNamedVars(int varcnt, int varstart) { - namedvars temp; - int i; - temp.varcnt = varcnt; - temp.varstart = varstart; - temp.vars = (char **) malloc(sizeof(char *) * varcnt); - temp.loaded = (int *) malloc(sizeof(int) * varcnt); - temp.dvalue = (double *) malloc(sizeof(double) * varcnt); - temp.ivalue = (int *) malloc(sizeof(int) * varcnt); - temp.dynvalue = (void **) malloc(sizeof(int) * varcnt); - for (i = 0; i < varcnt; i++) { - temp.vars[i] = NULL; - temp.loaded[i] = 0; - temp.dvalue[i] = 0.0; - temp.ivalue[i] = 0; - temp.dynvalue[i] = NULL; - } - return temp; -} - -void EnlargeNamedVars(namedvars *varmap, int newvarcnt) { - int i; - varmap->vars = (char **) realloc(varmap->vars, sizeof(char *) * newvarcnt); - varmap->loaded = (int *) realloc(varmap->loaded, sizeof(int) * newvarcnt); - varmap->dvalue = (double *) realloc(varmap->dvalue, sizeof(double) * newvarcnt); - varmap->ivalue = (int *) realloc(varmap->ivalue, sizeof(int) * newvarcnt); - varmap->dynvalue = (void **) realloc(varmap->dynvalue, sizeof(int) * newvarcnt); - for (i = varmap->varcnt; i < newvarcnt; i++) { - varmap->vars[i] = NULL; - varmap->loaded[i] = 0; - varmap->dvalue[i] = 0.0; - varmap->ivalue[i] = 0; - varmap->dynvalue[i] = NULL; - } - varmap->varcnt = newvarcnt; -} - -int AddNamedVarAt(namedvars varmap, const char *varname, int index) { - if (varmap.varcnt > index) { - varmap.vars[index] = (char *) malloc(sizeof(char) * (strlen(varname) + 1)); - strcpy(varmap.vars[index], varname); - return index; - } - return -1; -} - -int AddNamedVar(namedvars varmap, const char *varname) { - int index = GetNamedVarIndex(varmap, varname); - if (index == -1 * varmap.varcnt) { - return -1; - } else if ((index < 0) || (index == 0 && varmap.vars[0] == NULL)) { - index *= -1; - varmap.vars[index] = (char *) malloc(sizeof(char) * (strlen(varname) + 1)); - strcpy(varmap.vars[index], varname); - } - return index; -} - -void SetNamedVarValuesAt(namedvars varmap, int index, double dvalue, int ivalue, void *dynvalue) { - varmap.dvalue[index] = dvalue; - varmap.ivalue[index] = ivalue; - varmap.dynvalue[index] = dynvalue; -} - -int SetNamedVarValues(namedvars varmap, const char *varname, double dvalue, int ivalue, void *dynvalue) { - int index = GetNamedVarIndex(varmap, varname); - if (index == -1 * varmap.varcnt) { - return -1; - } else if ((index < 0) || (index == 0 && varmap.vars[0] == NULL)) { - index *= -1; - varmap.vars[index] = (char *) malloc(sizeof(char) * (strlen(varname) + 1)); - strcpy(varmap.vars[index], varname); - varmap.dvalue[index] = dvalue; - varmap.ivalue[index] = ivalue; - varmap.dynvalue[index] = dynvalue; - } else { - varmap.dvalue[index] = dvalue; - varmap.ivalue[index] = ivalue; - varmap.dynvalue[index] = dynvalue; - } - return index; -} - -int GetNamedVarIndex(const namedvars varmap, const char *varname) { - int i; - for (i = 0; i < varmap.varcnt; i++) { - if (varmap.vars[i] == NULL) return -1 * i; - if (strcmp(varmap.vars[i], varname) == 0) return i; - } - return -1 * varmap.varcnt; -} - -char* GetNodeVarName(DdManager *manager, namedvars varmap, DdNode *node) { - if (node == NULL) return NULL; - if (node == HIGH(manager)) return "true"; - if (node == LOW(manager)) return "false"; - return varmap.vars[GetIndex(node) - varmap.varstart]; -} - -char* GetNodeVarNameDisp(DdManager *manager, namedvars varmap, DdNode *node) { - if (HIGH(manager) == node) return "TRUE"; - if (LOW(manager) == node) return "FALSE"; - if (NULL == node) return "(null)"; - return varmap.vars[GetIndex(node) - varmap.varstart]; -} - -int RepairVarcnt(namedvars *varmap) { - while (varmap->vars[varmap->varcnt - 1] == NULL) - varmap->varcnt--; - return varmap->varcnt; -} - -int all_loaded(namedvars varmap, int disp) { - int i, res = 1; - for (i = 0; i < varmap.varcnt; i++) { - if (varmap.loaded[i] == 0) { - res = 0; - if (disp) fprintf(stderr, "The variable: %s was not loaded with values.\n", varmap.vars[i]); else return 0; - } - } - return res; -} - -/* Parser */ - -DdNode* FileGenerateBDD(DdManager *manager, namedvars varmap, bddfileheader fileheader) { - int icomment, maxlinesize, icur, iline, curinter, iequal; - DdNode *Line, **inter; - char buf, *inputline, *filename; - bddfileheader interfileheader; - // Initialization of intermediate steps - inter = (DdNode **) malloc(sizeof(DdNode *) * fileheader.intercnt); - for (icur = 0; icur < fileheader.intercnt; icur++) inter[icur] = NULL; - // Read file data - interfileheader.inputfile = NULL; - filename = NULL; // For nested files - iequal = 0; // Flag for encountered = sign - icur = 0; // Pointer for inputline buffer location - iline = 5; // Current file line (first after header) - icomment = 0; // Flag for comments - maxlinesize = 80; // inputline starting buffer size - inputline = (char *) malloc(sizeof(char) * maxlinesize); - while(!feof(fileheader.inputfile)) { - fread(&buf, 1, 1, fileheader.inputfile); - if (buf == ';' || buf == '%' || buf == '$') icomment = 1; - if (buf == '\n') { - if (icomment) icomment = 0; - if (iequal > 1) { - fprintf(stderr, "Error at line: %i. Line contains more than 1 equal(=) signs.\n", iline); - fclose(fileheader.inputfile); - free(inter); - free(inputline); - return NULL; - } else iequal = 0; - if (icur > 0) { - inputline[icur] = '\0'; - if (inputline[0] != 'L') { - fprintf(stderr, "Error at line: %i. Intermediate results should start with L.\n", iline); - fclose(fileheader.inputfile); - free(inter); - free(inputline); - return NULL; - } - curinter = getInterBDD(inputline); - if (curinter == -1) { - if (inputline[0] == 'L' && IsPosNumber(inputline + 1)) { - curinter = atoi(inputline + 1) - 1; - if (curinter > -1 && curinter < fileheader.intercnt && inter[curinter] != NULL) { - if (_debug) fprintf(stderr, "Returned: %s\n", inputline); - fclose(fileheader.inputfile); - Line = inter[curinter]; - free(inter); - free(inputline); - return Line; - } else { - fprintf(stderr, "Error at line: %i. Return result asked doesn't exist.\n", iline); - fclose(fileheader.inputfile); - free(inter); - free(inputline); - return NULL; - } - } else { - fprintf(stderr, "Error at line: %i. Invalid intermediate result format.\n", iline); - fclose(fileheader.inputfile); - free(inter); - free(inputline); - return NULL; - } - } else if (curinter > -1 && curinter < fileheader.intercnt && inter[curinter] == NULL) { - if (_debug) fprintf(stderr, "%i %s\n", curinter, inputline); - filename = getFileName(inputline); - if (filename == NULL) { - Line = LineParser(manager, varmap, inter, fileheader.intercnt, inputline, iline); - } else { - interfileheader = ReadFileHeader(filename); - if (interfileheader.inputfile == NULL) { - //Line = simpleBDDload(manager, &varmap, filename); - Line = NULL; - } else { - Line = FileGenerateBDD(manager, varmap, interfileheader); - } - if (Line == NULL) fprintf(stderr, "Error at line: %i. Error in nested BDD file: %s.\n", iline, filename); - free(filename); - filename = NULL; - interfileheader.inputfile = NULL; - } - if (Line == NULL) { - fclose(fileheader.inputfile); - free(inter); - free(inputline); - return NULL; - } - inter[curinter] = Line; - icur = 0; - } else if (curinter > -1 && curinter < fileheader.intercnt && inter[curinter] != NULL) { - fprintf(stderr, "Error at line: %i. Intermediate results can't be overwritten.\n", iline); - fclose(fileheader.inputfile); - free(inter); - free(inputline); - return NULL; - } else { - fprintf(stderr, "Error at line: %i. Intermediate result asked doesn't exist.\n", iline); - fclose(fileheader.inputfile); - free(inter); - free(inputline); - return NULL; - } - } - iline++; - } else if (buf != ' ' && buf != '\t' && !icomment) { - if (buf == '=') iequal++; - inputline[icur] = buf; - icur += 1; - if (icur == _maxbufsize) { - fprintf(stderr, "Error: Maximum buffer size(%i) exceeded.\n", _maxbufsize); - fclose(fileheader.inputfile); - free(inter); - free(inputline); - return NULL; - } - while (icur > maxlinesize - 1) { - maxlinesize *= 2; - inputline = (char *) realloc(inputline, sizeof(char) * maxlinesize); - } - } - } - fprintf(stderr, "Error, file either doesn't end with a blank line or no return result was asked.\n"); - fclose(fileheader.inputfile); - free(inter); - free(inputline); - return NULL; -} - -int getInterBDD(char *function) { - int i, ret; - char *inter; - for (i = 0; i < strlen(function); i++) { - if (function[i] == '=') { - inter = (char *) malloc(sizeof(char) * i); - strncpy(inter, function + 1, i - 1); - inter[i - 1] = '\0'; - if (IsPosNumber(inter)) { - ret = atoi(inter) - 1; - free(inter); - return ret; - } else { - free(inter); - return -1; - } - } - } - return -1; -} - -char* getFileName(const char *function) { - int i = 0; - char *filename; - while(function[i] != '=' && (i + 1) < strlen(function)) i++; - if ((i + 1) < strlen(function)) { - i++; - if (function[i] == '<' && function[strlen(function) - 1] == '>') { - filename = (char *) malloc(sizeof(char) * strlen(function) - i); - strcpy(filename, function + i + 1); - filename[strlen(function) - i - 2] = '\0'; - return filename; - } - } - return NULL; -} - -DdNode* LineParser(DdManager *manager, namedvars varmap, DdNode **inter, int maxinter, char *function, int iline) { - int istart, iend, ilength, i, symbol, ivar, inegvar, inegoper, iconst; - long startAt, endAt; - double secs; - DdNode *bdd; - char *term, curoper; - bdd = HIGH(manager); - Cudd_Ref(bdd); - term = NULL; - ivar = -1; - curoper = '*'; - istart = -1; - iend = strlen(function) - 1; - ilength = -1; - symbol = -1; - inegvar = 0; - inegoper = 0; - iconst = 0; - for (i = strlen(function) - 1; i > -1; i--) { - if (symbol == -1 && isOperator(function[i])) { - symbol = i; - istart = i + 1; - ilength = iend - i; - iend = i - 1; - if (ilength > 0 && !(ilength == 1 && function[istart] == '~')) { - term = (char *) malloc(sizeof(char) * (ilength + 1)); - strncpy(term, function + istart, ilength); - term[ilength] = '\0'; - } else { - fprintf(stderr, "Line Parser Error at line: %i. An operator was encounter with no term at its right side.\n", iline); - free(term); - return NULL; - } - } - if (symbol != -1) { - if (term[0] == '~') inegvar = 1; else inegvar = 0; - if (term[0 + inegvar] != 'L') { - // Term is a variable - if (strcmp(term + inegvar, "TRUE") == 0) { - iconst = 1; - } else if (strcmp(term + inegvar, "FALSE") == 0) { - iconst = 1; - inegvar = 1; - } else { - iconst = 0; - ivar = AddNamedVar(varmap, term + inegvar); - if (ivar == -1) { - fprintf(stderr, "Line Parser Error at line: %i. More BDD variables than the reserved term: %s.\n", iline, term); - free(term); - return NULL; - } - } - if (_debug) fprintf(stderr, "%s\n", term); - if (_debug && !iconst) fprintf(stderr, "PNZ1:%.0f P1:%.0f S1:%i PNZ2:%.0f P2:%.0f S2:%i\n", - Cudd_CountPathsToNonZero(bdd), - Cudd_CountPath(bdd), - Cudd_DagSize(bdd), - Cudd_CountPathsToNonZero(GetVar(manager, ivar + varmap.varstart)), - Cudd_CountPath(GetVar(manager, ivar + varmap.varstart)), - Cudd_DagSize(GetVar(manager, ivar + varmap.varstart)) ); - startAt = clock(); - if (!iconst) { - if (inegvar) bdd = BDD_Operator(manager, NOT(GetVar(manager, ivar + varmap.varstart)), bdd, curoper, inegoper); - else bdd = BDD_Operator(manager, GetVar(manager, ivar + varmap.varstart), bdd, curoper, inegoper); - } else { - switch(curoper) { - case '+': - if (inegvar ^ inegoper) ; else { - bdd = HIGH(manager); - Cudd_Ref(bdd); - } - break; - case '*': - if (inegvar ^ inegoper) { - bdd = LOW(manager); - Cudd_Ref(bdd); - } - break; - case '#': - if (inegvar ^ inegoper) ; else bdd = NOT(bdd); - break; - } - } - endAt = clock(); - secs = ((double) (endAt - startAt)) / ((double) CLOCKS_PER_SEC); - if (_debug) fprintf(stderr, "term: %s of line: %i took: %i\n", term, iline, endAt - startAt); - //if ((endAt - startAt) > 10000000) Cudd_AutodynDisable(manager); - if (bdd == NULL) { - fprintf(stderr, "Line Parser Error at line: %i. Error using operator %c on term: %s.\n", iline, curoper, term); - free(term); - return NULL; - } - } else { - // Term is an intermediate result - if (IsPosNumber(term + inegvar + 1)) ivar = atoi(term + inegvar + 1) - 1; else { - fprintf(stderr, "Line Parser Error at line: %i. Invalid intermediate result format term: %s.\n", iline, term); - free(term); - return NULL; - } - if (ivar < 0 || ivar > maxinter || inter[ivar] == NULL) { - fprintf(stderr, "Line Parser Error at line: %i. Usage of undeclared intermediate result term: %s.\n", iline, term); - free(term); - return NULL; - } - if (_debug) fprintf(stderr, "%s\n", term); - if (_debug) fprintf(stderr, "PNZ1:%.0f P1:%.0f S1:%i PNZ2:%.0f P2:%.0f S2:%i\n", - Cudd_CountPathsToNonZero(bdd), - Cudd_CountPath(bdd), - Cudd_DagSize(bdd), - Cudd_CountPathsToNonZero(inter[ivar]), - Cudd_CountPath(inter[ivar]), - Cudd_DagSize(inter[ivar]) ); - startAt = clock(); - if (inegvar) bdd = BDD_Operator(manager, NOT(inter[ivar]), bdd, curoper, inegoper); - else bdd = BDD_Operator(manager, inter[ivar], bdd, curoper, inegoper); - endAt = clock(); - secs = ((double) (endAt - startAt)) / ((double) CLOCKS_PER_SEC); - if (_debug) fprintf(stderr, "term: %s of line: %i took: %i\n", term, iline, endAt - startAt); - //if ((endAt - startAt) > 10000000) Cudd_AutodynDisable(manager); - if (bdd == NULL) { - fprintf(stderr, "Line Parser Error at line: %i. Error using operator %c on term: %s.\n", iline, curoper, term); - free(term); - return NULL; - } - } - free(term); - term = NULL; - curoper = function[symbol]; - if (curoper == '=') return bdd; - if (function[symbol - 1] == '~') { - inegoper = 1; - i--; - iend--; - } else { - inegoper = 0; - } - symbol = -1; - } - } - return NULL; -} - -DdNode* BDD_Operator(DdManager *manager, DdNode *bdd1, DdNode *bdd2, char Operator, int inegoper) { - switch (Operator) { - case '+': - if (inegoper) return D_BDDNor(manager, bdd1, bdd2); - else return D_BDDOr(manager, bdd1, bdd2); - break; - case '*': - if (inegoper) return D_BDDNand(manager, bdd1, bdd2); - else return D_BDDAnd(manager, bdd1, bdd2); - break; - case '#': - if (inegoper) return D_BDDXnor(manager, bdd1, bdd2); - else return D_BDDXor(manager, bdd1, bdd2); - break; - default: - return NULL; - break; - } -} - -DdNode* OnlineGenerateBDD(DdManager *manager, namedvars *varmap) { - int icomment, maxlinesize, icur, iline, curinter, iequal, iinters, itmp, i; - DdNode *Line, **inter; - char buf, *inputline, *filename; - bddfileheader interfileheader; - // Initialization of intermediate steps - iinters = 1; - inter = (DdNode **) malloc(sizeof(DdNode *) * iinters); - for (icur = 0; icur < iinters; icur++) inter[icur] = NULL; - // Read file data - interfileheader.inputfile = NULL; - filename = NULL; // For nested files - iequal = 0; // Flag for encountered = sign - icur = 0; // Pointer for inputline buffer location - iline = 1; // Current file line (first after header) - icomment = 0; // Flag for comments - maxlinesize = 80; // inputline starting buffer size - inputline = (char *) malloc(sizeof(char) * maxlinesize); - - do { - buf = fgetc(stdin); - if (buf == ';' || buf == '%' || buf == '$') icomment = 1; - if (buf == '\n') { - if (icomment) icomment = 0; - if (iequal > 1) { - fprintf(stderr, "Error at line: %i. Line contains more than 1 equal(=) signs.\n", iline); - free(inter); - free(inputline); - return NULL; - } else iequal = 0; - if (icur > 0) { - inputline[icur] = '\0'; - if (inputline[0] == '@') { - if (inputline[1] == 'e') { - free(inter); - free(inputline); - exit(0); - } else { - itmp = GetParam(inputline, 1); - if (itmp > varmap->varcnt) - EnlargeNamedVars(varmap, itmp); - itmp = GetParam(inputline, 2); - if (itmp > iinters) { - inter = (DdNode **) realloc(inter, sizeof(DdNode *) * itmp); - for (i = iinters; i < itmp; i++) inter[i] = NULL; - iinters = itmp; - } - } - icur = 0; - } else { - if (inputline[0] != 'L') { - fprintf(stderr, "Error at line: %i. Intermediate results should start with L.\n", iline); - free(inter); - free(inputline); - return NULL; - } - curinter = getInterBDD(inputline); - if (curinter == -1) { - if (inputline[0] == 'L' && IsPosNumber(inputline + 1)) { - curinter = atoi(inputline + 1) - 1; - if (curinter > -1 && curinter < iinters && inter[curinter] != NULL) { - if (_debug) fprintf(stderr, "Returned: %s\n", inputline); - Line = inter[curinter]; - free(inter); - free(inputline); - return Line; - } else { - fprintf(stderr, "Error at line: %i. Return result asked doesn't exist.\n", iline); - free(inter); - free(inputline); - return NULL; - } - } else { - fprintf(stderr, "Error at line: %i. Invalid intermediate result format.\n", iline); - free(inter); - free(inputline); - return NULL; - } - } else if (curinter > -1) { - if (curinter >= iinters) { - inter = (DdNode **) realloc(inter, sizeof(DdNode *) * (curinter + 1)); - for (i = iinters; i < curinter + 1; i++) inter[i] = NULL; - iinters = curinter + 1; - } - if (inter[curinter] == NULL) { - if (_debug) fprintf(stderr, "%i %s\n", curinter, inputline); - filename = getFileName(inputline); - if (filename == NULL) { - Line = OnlineLineParser(manager, varmap, inter, iinters, inputline, iline); - } else { - interfileheader = ReadFileHeader(filename); - if (interfileheader.inputfile == NULL) { - //Line = simpleBDDload(manager, varmap, filename); - Line = NULL; - } else { - Line = FileGenerateBDD(manager, *varmap, interfileheader); - } - if (Line == NULL) fprintf(stderr, "Error at line: %i. Error in nested BDD file: %s.\n", iline, filename); - free(filename); - filename = NULL; - interfileheader.inputfile = NULL; - } - if (Line == NULL) { - free(inter); - free(inputline); - return NULL; - } - inter[curinter] = Line; - icur = 0; - } else if (inter[curinter] != NULL) { - fprintf(stderr, "Error at line: %i. Intermediate results can't be overwritten.\n", iline); - free(inter); - free(inputline); - return NULL; - } - } else { - fprintf(stderr, "Error at line: %i. Intermediate result asked doesn't exist.\n", iline); - free(inter); - free(inputline); - return NULL; - } - } - } - iline++; - } else if (buf != ' ' && buf != '\t' && !icomment) { - if (buf == '=') iequal++; - inputline[icur] = buf; - icur += 1; - if (icur == _maxbufsize) { - fprintf(stderr, "Error: Maximum buffer size(%i) exceeded.\n", _maxbufsize); - free(inter); - free(inputline); - return NULL; - } - while (icur > maxlinesize - 1) { - maxlinesize *= 2; - inputline = (char *) realloc(inputline, sizeof(char) * maxlinesize); - } - } - } while(1); - fprintf(stderr, "Error, file either doesn't end with a blank line or no return result was asked.\n"); - free(inter); - free(inputline); - return NULL; -} - -DdNode* OnlineLineParser(DdManager *manager, namedvars *varmap, DdNode **inter, int maxinter, char *function, int iline) { - int istart, iend, ilength, i, symbol, ivar, inegvar, inegoper, iconst; - long startAt, endAt; - double secs; - DdNode *bdd; - char *term, curoper; - bdd = HIGH(manager); - Cudd_Ref(bdd); - term = NULL; - ivar = -1; - curoper = '*'; - istart = -1; - iend = strlen(function) - 1; - ilength = -1; - symbol = -1; - inegvar = 0; - inegoper = 0; - iconst = 0; - for (i = strlen(function) - 1; i > -1; i--) { - if (symbol == -1 && isOperator(function[i])) { - symbol = i; - istart = i + 1; - ilength = iend - i; - iend = i - 1; - if (ilength > 0 && !(ilength == 1 && function[istart] == '~')) { - term = (char *) malloc(sizeof(char) * (ilength + 1)); - strncpy(term, function + istart, ilength); - term[ilength] = '\0'; - } else { - fprintf(stderr, "Line Parser Error at line: %i. An operator was encounter with no term at its right side.\n", iline); - free(term); - return NULL; - } - } - if (symbol != -1) { - if (term[0] == '~') inegvar = 1; else inegvar = 0; - if (term[0 + inegvar] != 'L') { - // Term is a variable - if (strcmp(term + inegvar, "TRUE") == 0) { - iconst = 1; - } else if (strcmp(term + inegvar, "FALSE") == 0) { - iconst = 1; - inegvar = 1; - } else { - iconst = 0; - ivar = AddNamedVar(*varmap, term + inegvar); - if (ivar == -1) { - EnlargeNamedVars(varmap, varmap->varcnt + 1); - ivar = AddNamedVar(*varmap, term + inegvar); - } - if (ivar == -1) { - fprintf(stderr, "Line Parser Error at line: %i. More BDD variables than the reserved term: %s.\n", iline, term); - free(term); - return NULL; - } - } - if (_debug) fprintf(stderr, "%s\n", term); - if (_debug && !iconst) fprintf(stderr, "PNZ1:%.0f P1:%.0f S1:%i PNZ2:%.0f P2:%.0f S2:%i\n", - Cudd_CountPathsToNonZero(bdd), - Cudd_CountPath(bdd), - Cudd_DagSize(bdd), - Cudd_CountPathsToNonZero(GetVar(manager, ivar + varmap->varstart)), - Cudd_CountPath(GetVar(manager, ivar + varmap->varstart)), - Cudd_DagSize(GetVar(manager, ivar + varmap->varstart)) ); - startAt = clock(); - if (!iconst) { - if (inegvar) bdd = BDD_Operator(manager, NOT(GetVar(manager, ivar + varmap->varstart)), bdd, curoper, inegoper); - else bdd = BDD_Operator(manager, GetVar(manager, ivar + varmap->varstart), bdd, curoper, inegoper); - } else { - switch(curoper) { - case '+': - if (inegvar ^ inegoper) ; else { - bdd = HIGH(manager); - Cudd_Ref(bdd); - } - break; - case '*': - if (inegvar ^ inegoper) { - bdd = LOW(manager); - Cudd_Ref(bdd); - } - break; - case '#': - if (inegvar ^ inegoper) ; else bdd = NOT(bdd); - break; - } - } - endAt = clock(); - secs = ((double) (endAt - startAt)) / ((double) CLOCKS_PER_SEC); - if (_debug) fprintf(stderr, "term: %s of line: %i took: %i\n", term, iline, endAt - startAt); - //if ((endAt - startAt) > 10000000) Cudd_AutodynDisable(manager); - if (bdd == NULL) { - fprintf(stderr, "Line Parser Error at line: %i. Error using operator %c on term: %s.\n", iline, curoper, term); - free(term); - return NULL; - } - } else { - // Term is an intermediate result - if (IsPosNumber(term + inegvar + 1)) ivar = atoi(term + inegvar + 1) - 1; else { - fprintf(stderr, "Line Parser Error at line: %i. Invalid intermediate result format term: %s.\n", iline, term); - free(term); - return NULL; - } - if (ivar < 0 || ivar > maxinter || inter[ivar] == NULL) { - fprintf(stderr, "Line Parser Error at line: %i. Usage of undeclared intermediate result term: %s.\n", iline, term); - free(term); - return NULL; - } - if (_debug) fprintf(stderr, "%s\n", term); - if (_debug) fprintf(stderr, "PNZ1:%.0f P1:%.0f S1:%i PNZ2:%.0f P2:%.0f S2:%i\n", - Cudd_CountPathsToNonZero(bdd), - Cudd_CountPath(bdd), - Cudd_DagSize(bdd), - Cudd_CountPathsToNonZero(inter[ivar]), - Cudd_CountPath(inter[ivar]), - Cudd_DagSize(inter[ivar]) ); - startAt = clock(); - if (inegvar) bdd = BDD_Operator(manager, NOT(inter[ivar]), bdd, curoper, inegoper); - else bdd = BDD_Operator(manager, inter[ivar], bdd, curoper, inegoper); - endAt = clock(); - secs = ((double) (endAt - startAt)) / ((double) CLOCKS_PER_SEC); - if (_debug) fprintf(stderr, "term: %s of line: %i took: %i\n", term, iline, endAt - startAt); - //if ((endAt - startAt) > 10000000) Cudd_AutodynDisable(manager); - if (bdd == NULL) { - fprintf(stderr, "Line Parser Error at line: %i. Error using operator %c on term: %s.\n", iline, curoper, term); - free(term); - return NULL; - } - } - free(term); - term = NULL; - curoper = function[symbol]; - if (curoper == '=') return bdd; - if (function[symbol - 1] == '~') { - inegoper = 1; - i--; - iend--; - } else { - inegoper = 0; - } - symbol = -1; - } - } - return NULL; -} - -int GetParam(char *inputline, int iParam) { - int icoma, istart, iend, ret; - char *numb; - istart = 1; - icoma = istart; - iend = strlen(inputline); - while((inputline[icoma] != ',') && (icoma < iend)) - icoma++; - if (iParam == 1) { - numb = (char *) malloc(sizeof(char) * icoma); - strncpy(numb, inputline + 1, icoma - 1); - numb[icoma - 1] = '\0'; - if (IsPosNumber(numb)) { - ret = atoi(numb); - free(numb); - return ret; - } - } else if(iParam == 2) { - numb = (char *) malloc(sizeof(char) * (iend - icoma + 1)); - strncpy(numb, inputline + icoma + 1, iend - icoma); - numb[iend - icoma] = '\0'; - if (IsPosNumber(numb)) { - ret = atoi(numb); - free(numb); - return ret; - } - } - return 0; -} - -void onlinetraverse(DdManager *manager, namedvars varmap, hisqueue *HisQueue, DdNode *bdd) { - char buf, *inputline; - int icur, maxlinesize, iline, index, iloop, ivalue, iQsize, i, inQ; - double dvalue; - DdNode **Q, **Q2, *h_node, *l_node, *curnode; - hisqueue *his; - hisnode *hnode; - iloop = 1; - icur = 0; // Pointer for inputline buffer location - iline = 1; // Current file line (first after header) - maxlinesize = 80; // inputline starting buffer size - inputline = (char *) malloc(sizeof(char) * maxlinesize); - curnode = bdd; - iQsize = 0; - Q = (DdNode **) malloc(sizeof(DdNode *) * iQsize); - Q2 = NULL; - his = InitHistory(varmap.varcnt); - do { - buf = fgetc(stdin); - if (buf == '\n') { - inputline[icur] = '\0'; - if ((icur > 0) && (inputline[0] == '@') && (inputline[2] == ',' || inputline[2] == '\0')) { - switch(inputline[1]) { - case 'c': - printf("bdd_temp_value('%s', %i).\n", GetNodeVarNameDisp(manager, varmap, curnode), iQsize); - break; - case 'n': - if (curnode != HIGH(manager) && curnode != LOW(manager) && (hnode = GetNode(his, varmap.varstart, curnode)) == NULL) { - AddNode(his, varmap.varstart, curnode, 0.0, 0, NULL); - l_node = LowNodeOf(manager, curnode); - h_node = HighNodeOf(manager, curnode); - inQ = 0; - for(i = 0; (i < iQsize / 2) && (inQ < 3); i++) - inQ = (Q[i] == l_node) || (Q[iQsize - i] == l_node) + 2 * (Q[i] == h_node) || (Q[iQsize - i] == h_node); - if (inQ & 1 == 0) inQ = inQ + (GetNode(his, varmap.varstart, l_node) != NULL); - if (inQ & 2 == 0) inQ = inQ + 2 * (GetNode(his, varmap.varstart, h_node) != NULL); - if (inQ & 1 == 1) inQ = inQ - (l_node == HIGH(manager) || l_node == LOW(manager)); - if (inQ & 2 == 2) inQ = inQ - 2 * (h_node == HIGH(manager) || h_node == LOW(manager)); - switch(inQ) { - case 0: - iQsize += 2; - Q = (DdNode **) realloc(Q, sizeof(DdNode *) * iQsize); - Q[iQsize - 2] = l_node; - Q[iQsize - 1] = h_node; - break; - case 1: - iQsize++; - Q = (DdNode **) realloc(Q, sizeof(DdNode *) * iQsize); - Q[iQsize - 1] = h_node; - break; - case 2: - iQsize++; - Q = (DdNode **) realloc(Q, sizeof(DdNode *) * iQsize); - Q[iQsize - 1] = l_node; - break; - case 3: - break; - default: - break; - } - } - if (inputline[2] == '\0' || strcmp(inputline + 3, "DFS") == 0) { - if (iQsize > 0) { - iQsize--; - curnode = Q[iQsize]; - Q = (DdNode **) realloc(Q, sizeof(DdNode *) * iQsize); - } - } else if (strcmp(inputline + 3, "BFS") == 0) { - if (iQsize > 0) { - iQsize--; - curnode = Q[0]; - Q2 = (DdNode **) malloc(sizeof(DdNode *) * iQsize); - for(i = 0; i < iQsize; i++) - Q2[i] = Q[i + 1]; - free(Q); - Q = Q2; - } - } else { - fprintf(stderr, "Error: Could not find method: %s, Correct syntax @n,[DFS, BFS].\n", inputline + 3); - free(Q); - free(inputline); - exit(-1); - } - break; - case 'h': - printf("bdd_temp_value('%s').\n", GetNodeVarNameDisp(manager, varmap, HighNodeOf(manager, curnode))); - break; - case 'l': - printf("bdd_temp_value('%s').\n", GetNodeVarNameDisp(manager, varmap, LowNodeOf(manager, curnode))); - break; - case 'v': - index = GetNamedVarIndex(varmap, inputline + 3); - if (index >= 0) { - fprintf(stdout, "bdd_temp_value([%f,%i,%s]).\n", varmap.dvalue[index], varmap.ivalue[index], (char *) varmap.dynvalue[index]); - } else { - fprintf(stderr, "Error: Could not find variable: %s, Correct syntax @v,[variable name].\n", inputline + 3); - free(Q); - free(inputline); - exit(-1); - } - break; - case 'e': - iloop = 0; - break; - default: - fprintf(stderr, "Error: Not recognizable instruction: %s.\n", inputline); - free(Q); - free(inputline); - exit(-1); - break; - } - icur = 0; - } else { - fprintf(stderr, "Error: Not recognizable instruction: %s.\n", inputline); - free(Q); - free(inputline); - exit(-1); - } - iline++; - } else if (buf != ' ' && buf != '\t') { - inputline[icur] = buf; - icur += 1; - if (icur == _maxbufsize) { - fprintf(stderr, "Error: Maximum buffer size(%i) exceeded.\n", _maxbufsize); - free(Q); - free(inputline); - exit(-1); - } - while (icur > maxlinesize - 1) { - maxlinesize *= 2; - inputline = (char *) realloc(inputline, sizeof(char) * maxlinesize); - } - } - } while(iloop); - free(Q); - free(inputline); -} diff --git a/packages/ProbLog/simplecudd/simplecudd.h b/packages/ProbLog/simplecudd/simplecudd.h deleted file mode 100644 index 49ed3a5aa..000000000 --- a/packages/ProbLog/simplecudd/simplecudd.h +++ /dev/null @@ -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 -#include -#include -#include -#include -#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); -