%%% -*- Mode: Prolog; -*- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % $Date: 2011-07-27 17:38:26 +0200 (Wed, 27 Jul 2011) $ % $Revision: 6461 $ % % This file is part of ProbLog % http://dtai.cs.kuleuven.be/problog % % ProbLog was developed at Katholieke Universiteit Leuven % % Copyright 2008, 2009, 2010 % Katholieke Universiteit Leuven % % Main author of this file: % Angelika Kimmig % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % Artistic License 2.0 % % Copyright (c) 2000-2006, The Perl Foundation. % % Everyone is permitted to copy and distribute verbatim copies of this % license document, but changing it is not allowed. Preamble % % This license establishes the terms under which a given free software % Package may be copied, modified, distributed, and/or % redistributed. The intent is that the Copyright Holder maintains some % artistic control over the development of that Package while still % keeping the Package available as open source and free software. % % You are always permitted to make arrangements wholly outside of this % license directly with the Copyright Holder of a given Package. If the % terms of this license do not permit the full use that you propose to % make of the Package, you should contact the Copyright Holder and seek % a different licensing arrangement. Definitions % % "Copyright Holder" means the individual(s) or organization(s) named in % the copyright notice for the entire Package. % % "Contributor" means any party that has contributed code or other % material to the Package, in accordance with the Copyright Holder's % procedures. % % "You" and "your" means any person who would like to copy, distribute, % or modify the Package. % % "Package" means the collection of files distributed by the Copyright % Holder, and derivatives of that collection and/or of those files. A % given Package may consist of either the Standard Version, or a % Modified Version. % % "Distribute" means providing a copy of the Package or making it % accessible to anyone else, or in the case of a company or % organization, to others outside of your company or organization. % % "Distributor Fee" means any fee that you charge for Distributing this % Package or providing support for this Package to another party. It % does not mean licensing fees. % % "Standard Version" refers to the Package if it has not been modified, % or has been modified only in ways explicitly requested by the % Copyright Holder. % % "Modified Version" means the Package, if it has been changed, and such % changes were not explicitly requested by the Copyright Holder. % % "Original License" means this Artistic License as Distributed with the % Standard Version of the Package, in its current version or as it may % be modified by The Perl Foundation in the future. % % "Source" form means the source code, documentation source, and % configuration files for the Package. % % "Compiled" form means the compiled bytecode, object code, binary, or % any other form resulting from mechanical transformation or translation % of the Source form. % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % Permission for Use and Modification Without Distribution % % (1) You are permitted to use the Standard Version and create and use % Modified Versions for any purpose without restriction, provided that % you do not Distribute the Modified Version. % % Permissions for Redistribution of the Standard Version % % (2) You may Distribute verbatim copies of the Source form of the % Standard Version of this Package in any medium without restriction, % either gratis or for a Distributor Fee, provided that you duplicate % all of the original copyright notices and associated disclaimers. At % your discretion, such verbatim copies may or may not include a % Compiled form of the Package. % % (3) You may apply any bug fixes, portability changes, and other % modifications made available from the Copyright Holder. The resulting % Package will still be considered the Standard Version, and as such % will be subject to the Original License. % % Distribution of Modified Versions of the Package as Source % % (4) You may Distribute your Modified Version as Source (either gratis % or for a Distributor Fee, and with or without a Compiled form of the % Modified Version) provided that you clearly document how it differs % from the Standard Version, including, but not limited to, documenting % any non-standard features, executables, or modules, and provided that % you do at least ONE of the following: % % (a) make the Modified Version available to the Copyright Holder of the % Standard Version, under the Original License, so that the Copyright % Holder may include your modifications in the Standard Version. (b) % ensure that installation of your Modified Version does not prevent the % user installing or running the Standard Version. In addition, the % modified Version must bear a name that is different from the name of % the Standard Version. (c) allow anyone who receives a copy of the % Modified Version to make the Source form of the Modified Version % available to others under (i) the Original License or (ii) a license % that permits the licensee to freely copy, modify and redistribute the % Modified Version using the same licensing terms that apply to the copy % that the licensee received, and requires that the Source form of the % Modified Version, and of any works derived from it, be made freely % available in that license fees are prohibited but Distributor Fees are % allowed. % % Distribution of Compiled Forms of the Standard Version or % Modified Versions without the Source % % (5) You may Distribute Compiled forms of the Standard Version without % the Source, provided that you include complete instructions on how to % get the Source of the Standard Version. Such instructions must be % valid at the time of your distribution. If these instructions, at any % time while you are carrying out such distribution, become invalid, you % must provide new instructions on demand or cease further % distribution. If you provide valid instructions or cease distribution % within thirty days after you become aware that the instructions are % invalid, then you do not forfeit any of your rights under this % license. % % (6) You may Distribute a Modified Version in Compiled form without the % Source, provided that you comply with Section 4 with respect to the % Source of the Modified Version. % % Aggregating or Linking the Package % % (7) You may aggregate the Package (either the Standard Version or % Modified Version) with other packages and Distribute the resulting % aggregation provided that you do not charge a licensing fee for the % Package. Distributor Fees are permitted, and licensing fees for other % components in the aggregation are permitted. The terms of this license % apply to the use and Distribution of the Standard or Modified Versions % as included in the aggregation. % % (8) You are permitted to link Modified and Standard Versions with % other works, to embed the Package in a larger work of your own, or to % build stand-alone binary or bytecode versions of applications that % include the Package, and Distribute the result without restriction, % provided the result does not expose a direct interface to the Package. % % Items That are Not Considered Part of a Modified Version % % (9) Works (including, but not limited to, modules and scripts) that % merely extend or make use of the Package, do not, by themselves, cause % the Package to be a Modified Version. In addition, such works are not % considered parts of the Package itself, and are not subject to the % terms of this license. % % General Provisions % % (10) Any use, modification, and distribution of the Standard or % Modified Versions is governed by this Artistic License. By using, % modifying or distributing the Package, you accept this license. Do not % use, modify, or distribute the Package, if you do not accept this % license. % % (11) If your Modified Version has been derived from a Modified Version % made by someone other than you, you are nevertheless required to % ensure that your Modified Version complies with the requirements of % this license. % % (12) This license does not grant you the right to use any trademark, % service mark, tradename, or logo of the Copyright Holder. % % (13) This license includes the non-exclusive, worldwide, % free-of-charge patent license to make, have made, use, offer to sell, % sell, import and otherwise transfer the Package with respect to any % patent claims licensable by the Copyright Holder that are necessarily % infringed by the Package. If you institute patent litigation % (including a cross-claim or counterclaim) against any party alleging % that the Package constitutes direct or contributory patent % infringement, then this Artistic License to you shall terminate on the % date that such litigation is filed. % % (14) Disclaimer of Warranty: THE PACKAGE IS PROVIDED BY THE COPYRIGHT % HOLDER AND CONTRIBUTORS "AS IS' AND WITHOUT ANY EXPRESS OR IMPLIED % WARRANTIES. THE IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR A % PARTICULAR PURPOSE, OR NON-INFRINGEMENT ARE DISCLAIMED TO THE EXTENT % PERMITTED BY YOUR LOCAL LAW. UNLESS REQUIRED BY LAW, NO COPYRIGHT % HOLDER OR CONTRIBUTOR WILL BE LIABLE FOR ANY DIRECT, INDIRECT, % INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING IN ANY WAY OUT OF THE USE % OF THE PACKAGE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % aProbLog prototype % % for background, see % Kimmig et al "An Algebraic Prolog for Reasoning about Possible Worlds" AAAI 2011 % http://dtai.cs.kuleuven.be/problog/publications.html % % includes ProbLog code fragments % uses the online interface to problogbdd/simplecudd written by Theofrastos Mantadelis (problog/bdd.yap) % % NOTE: % - flags neutral_sum and disjoint_sum decide which inference method is called from aproblog_label/2, they are ignored when calling these underlying methods directly % - all four methods use the set of explanations found by SLD resolution as covering set of explanations % - compensation for non-neutral sums is restricted to the variables that occur in some proof of the query by default, % setting flag compensate_unused to true will activate compensation for all ground unseen variables (throws error in programs with non-ground facts) % - for disjoint sum, no trie representation of the DNF is built, i.e. n proofs resulting in same explanation appear n times in sum (old versions _on_dnf not exported) % - BDDs are constructed using dbtries with optimization level 0 (predicates for naive preprocessing can be activated in the source code (search comments on dnf_to_bdd_naive)) % - dynamic labels are not yet supported (i.e. no L::fact(L).) % % hacker's corner: % - declaring sums to be neutral simulates labels defined in terms of the set of SLD-explanations (not considered in AAAI paper) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% :- module(aproblog,[op( 550, yfx, :: ), aproblog_label/2, % decide cases based on flags disjoint_sum and neutral_sum (default: both false -> case 4) label_neutral_disjoint/2, % case 1: sums are neutral and disjoint label_disjoint_neutral/2, % synonym for label_neutral_disjoint/2 label_disjoint/2, % case 2: sums are disjoint but not neutral (also solves case 1, but with overhead) label_neutral/2, % case 3: sums are neutral but not disjoint (also solves case 1, but with overhead) label/2, % case 4: sums are not neutral and not disjoint (also solves cases 1-3, but with overhead) '::'/2, set_aproblog_flag/2, aproblog_flag/2, print_bdd/1, print_dnf/1]). :- style_check(all). :- yap_flag(unknown,error). :- op( 550, yfx, :: ). :- multifile('::'/2). :- ensure_loaded('problog/ptree'). :- ensure_loaded('problog/bdd'). :- ensure_loaded('problog/gflags'). :- ensure_loaded('problog/flags'). :- ensure_loaded('problog/os'). :- ensure_loaded(library(tries)). :- ensure_loaded(library(terms)). :- ensure_loaded(library(lists)). :- dynamic(aproblog_predicate/2). :- dynamic(non_ground_fact/1). :- dynamic calcp/2. % used in lazy evaluation :- dynamic aproblog_cached/4. % cache in depth first search :- dynamic aproblog_cache_vars/0. % decides whether cache also contains variables which are then used for compensation % by default don't talk, take care of both potential problems, and do not compensate for unused facts :- initialization(( problog_define_flag(verbose, problog_flag_validate_boolean, 'display information', false, aproblog), problog_define_flag(disjoint_sum, problog_flag_validate_boolean, 'sum is disjoint', false, aproblog), problog_define_flag(neutral_sum, problog_flag_validate_boolean, 'sum is neutral', false, aproblog), problog_define_flag(compensate_unused, problog_flag_validate_boolean, 'compensate non-neutral sum for unused facts', false, aproblog) )). % directory where problogbdd executable is located % automatically set during loading -- assumes it is in same place as this file (problog.yap) :- getcwd(PD), set_problog_path(PD). aproblog_flag(F,V) :- problog_flag(F,V). set_aproblog_flag(F,V) :- set_problog_flag(F,V). % backtrack over all labeled facts % must come before term_expansion Label::Goal :- labeled_fact(Label,Goal,_ID). % backtrack over all labeled facts labeled_fact(Label,Goal,ID) :- ground(Goal), !, Goal =.. [F|Args], atomic_concat('aproblog_',F,F2), append([ID|Args],[Label],Args2), Goal2 =..[F2|Args2], length(Args2,N), current_predicate(F2/N), Goal2. labeled_fact(Label,Goal,ID) :- get_internal_fact(ID,ProblogTerm,_ProblogName,_ProblogArity), ProblogTerm =.. [F,_ID|Args], append(Args2,[Label],Args), name(F,[_a,_p,_r,_o,_b,_l,_o,_g,_|F2Chars]), name(F2,F2Chars), Goal =.. [F2|Args2]. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % term expansion / core is taken from problog_neg and adapted %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% user:term_expansion(_P::( _Goal :- _Body ), _Error) :- throw(error('we do not support this (yet?)!')). user:term_expansion(P::Goal, aproblog:ProbFact) :- functor(Goal, Name, Arity), atomic_concat([aproblog_,Name],AproblogName), Goal =.. [Name|Args], append(Args,[P],L1), labelclause_id(ID), ProbFact =.. [AproblogName,ID|L1], ( ground(P) -> assert_static(id_label(ID,P)) % Label is fixed -- assert it for quick retrieval ; % Label is a variable... we don't support that yet throw(error('Variable labels are not (yet) supported! Your program contains':P::Goal)) ), ( ground(Goal) -> true; assert(non_ground_fact(ID)) ), aproblog_predicate(Name, Arity, AproblogName). % introduce wrapper clause if predicate seen first time aproblog_predicate(Name, Arity, _) :- aproblog_predicate(Name, Arity), !. aproblog_predicate(Name, Arity, AproblogName) :- functor(OriginalGoal, Name, Arity), OriginalGoal =.. [_|Args], append(Args,[_],L1), ProbFact =.. [AproblogName,ID|L1], prolog_load_context(module,Mod), assert( (Mod:OriginalGoal :- ProbFact, ( non_ground_fact(ID) -> (non_ground_fact_grounding_id(OriginalGoal,G_ID), atomic_concat([ID,'_',G_ID],ID2)); ID2=ID ), add_to_proof(ID2) )), assert( (Mod:aproblog_not(OriginalGoal) :- ProbFact, ( non_ground_fact(ID) -> ( non_ground_fact_grounding_id(OriginalGoal,G_ID), atomic_concat([ID,'_',G_ID],ID2)); ID2=ID ), add_to_proof_negated(ID2) )), assert(aproblog_predicate(Name, Arity)), ArityPlus2 is Arity+2, dynamic(aproblog:AproblogName/ArityPlus2). % generate next global identifier :- nb_setval(labelclause_counter,0). labelclause_id(ID) :- nb_getval(labelclause_counter,ID), !, C1 is ID+1, nb_setval(labelclause_counter,C1), !. % managing non-ground facts 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(_,_)). % accessing internal information get_fact_label(ID,Prob) :- ( id_label(ID,W) -> Prob = W ; get_fact_from_id(ID,F), atom_number(F,N), id_label(N,Prob) ). get_internal_fact(ID,AproblogTerm,AproblogName,AproblogArity) :- aproblog_predicate(Name,Arity), atomic_concat([aproblog_,Name],AproblogName), AproblogArity is Arity+2, functor(AproblogTerm,AproblogName,AproblogArity), arg(1,AproblogTerm,ID), call(AproblogTerm). % have to keep choicepoint to allow for :: backtracking over all facts get_fact(ID,OutsideTerm) :- get_internal_fact(ID,AproblogTerm,AproblogName,AproblogArity), AproblogTerm =.. [_Functor,ID|Args], atomic_concat('aproblog_',OutsideFunctor,AproblogName), Last is AproblogArity-1, nth(Last,Args,_LogProb,OutsideArgs), OutsideTerm =.. [OutsideFunctor|OutsideArgs]. % ID of instance of non-ground fact: get fact from grounding table get_fact(ID,OutsideTerm) :- recover_grounding_id(ID,GID), grounding_is_known(OutsideTerm,GID). recover_grounding_id(Atom,ID) :- name(Atom,List), reverse(List,Rev), recover_number(Rev,NumRev), reverse(NumRev,Num), name(ID,Num). recover_number([95|_],[]) :- !. % name('_',[95]) recover_number([A|B],[A|C]) :- recover_number(B,C). get_fact_list([],[]). get_fact_list([neg(T)|IDs],[not(Goal)|Facts]) :- !, aproblog_context(Goal,_,T), get_fact_list(IDs,Facts). get_fact_list([ID|IDs],[Fact|Facts]) :- (ID=not(X) -> Fact=not(Y); Fact=Y, ID=X), get_fact(X,Y), get_fact_list(IDs,Facts). % 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 % else update state and succeed add_to_proof(ID) :- b_getval(aproblog_steps,MaxSteps), b_getval(aproblog_current_proof, IDs), %%%% Bernd, changes for negated ground facts \+ memberchk(not(ID),IDs), %%%% Bernd, changes for negated ground facts ( MaxSteps =< 0 -> fail ; ( memberchk(ID, IDs) -> true ; b_setval(aproblog_current_proof, [ID|IDs]) ), Steps is MaxSteps-1, b_setval(aproblog_steps,Steps) ). %%%% Bernd, changes for negated ground facts add_to_proof_negated(ID) :- b_getval(aproblog_steps,MaxSteps), b_getval(aproblog_current_proof, IDs), \+ memberchk(ID,IDs), ( MaxSteps =< 0 -> fail ; ( memberchk(not(ID), IDs) -> true ; b_setval(aproblog_current_proof, [not(ID)|IDs]) ), Steps is MaxSteps-1, b_setval(aproblog_steps,Steps) ). %%%% Bernd, changes for negated ground facts % this is called before the actual aProbLog goal % to set up environment for proving init_aproblog :- reset_non_ground_facts, b_setval(aproblog_current_proof, []), b_setval(aproblog_steps,999999). init_aproblog_trie :- init_ptree(Trie_Completed_Proofs), nb_setval(aproblog_completed_proofs, Trie_Completed_Proofs). % to call an aProbLog goal, patch all subgoals with the user's module context % (as logical part is there, but labeled part in aproblog) aproblog_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). put_module((Mod:Goal,Rest),Module,(Mod:Goal,Transformed)) :- !, put_module(Rest,Module,Transformed). put_module((Goal,Rest),Module,(Module:Goal,Transformed)) :- !, put_module(Rest,Module,Transformed). put_module((Mod:Goal),_Module,(Mod:Goal)) :- !. put_module(Goal,Module,Module:Goal). % end of core %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % predicates related to DNF construction and evaluation %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%% % given a query, build the DNF in the trie named aproblog_completed_proofs %%%%%%%%%%%%% build_dnf(Goal) :- init_aproblog, init_aproblog_trie, nb_getval(aproblog_completed_proofs, Trie), aproblog_call(Goal), add_solution(Trie), fail. build_dnf(_). add_solution(N) :- b_getval(aproblog_current_proof, IDs), (IDs == [] -> R = true ; reverse(IDs,R)), insert_ptree(R,N). delete_dnf :- nb_getval(aproblog_completed_proofs, Trie), delete_ptree(Trie). print_dnf :- nb_getval(aproblog_completed_proofs, Trie), print_ptree(Trie). %%%%%%%%%%%%%%%%%%%%%%%%%%% % calculating the label of the DNF: % iterates over all conjunctions, performing semiring multiplication in conj, semiring addition between conj %%%%%%%%%%%%%%%%%%%%%%%%%%% evaluate_dnf(_) :- semiring_zero(Zero), nb_setval(aproblog_label, Zero), nb_getval(aproblog_completed_proofs, Trie), traverse_ptree(Trie,Explanation), update_label(Explanation), fail. evaluate_dnf(Label) :- nb_getval(aproblog_label, Label). update_label(Explanation) :- semiring_one(One), multiply_label(Explanation,One,Label), nb_getval(aproblog_label, OldLabel), semiring_addition(OldLabel,Label,NewLabel), nb_setval(aproblog_label, NewLabel). multiply_label([],Result,Result). multiply_label([not(First)|Rest],Acc,Result) :- !, get_fact_label(First,W), label_negated(W,WBar), semiring_multiplication(Acc,WBar,Next), multiply_label(Rest,Next,Result). multiply_label([First|Rest],Acc,Result) :- !, get_fact_label(First,W), semiring_multiplication(Acc,W,Next), multiply_label(Rest,Next,Result). %%%%%%%%%%%%%%%%%%%%%%%%%%% % calculating the label of the DNF in case the sum is not neutral, % compensation ignores variables not appearing in DNF %%%%%%%%%%%%%%%%%%%%%%%%%%% evaluate_dnf_with_compensation(_) :- semiring_zero(Zero), nb_setval(aproblog_label, Zero), nb_setval(aproblog_variables, []), nb_getval(aproblog_completed_proofs, Trie), traverse_ptree(Trie,Explanation), update_label_with_compensation(Explanation), fail. evaluate_dnf_with_compensation(Label) :- nb_getval(aproblog_label, Label). update_label_with_compensation(Explanation) :- semiring_one(One), multiply_label(Explanation,One,LabelI), % LabelI is the label of the i-th explanation... nb_getval(aproblog_variables, Var), get_variables(Explanation,VarI), compensate_label(Var,VarI,LabelI,CLabelI), % ... which is corrected for Var\VarI nb_getval(aproblog_label, OldLabel), compensate_label(VarI,Var,OldLabel, COldLabel), % OldLabel gets corrected for VarI\Var semiring_addition(COldLabel,CLabelI,NewLabel), % now we sum corrected labels up nb_setval(aproblog_label, NewLabel), append(Var,VarI,List), sort(List,NewVar), nb_setval(aproblog_variables,NewVar). % and update the list of seen variables % variant that always compensates for the full set of DNF variables % does some unnecessary append and sort at the end of each update evaluate_dnf_with_compensation_naive(_) :- semiring_zero(Zero), nb_setval(aproblog_label, Zero), nb_getval(aproblog_completed_proofs, Trie), edges_ptree(Trie,Vars), nb_setval(aproblog_variables, Vars), traverse_ptree(Trie,Explanation), update_label_with_compensation(Explanation), fail. evaluate_dnf_with_compensation_naive(Label) :- nb_getval(aproblog_label, Label). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % predicates related to BDD construction and evaluation %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%% % dnf to bdd translation using naive preprocessing % (full conjunctions as intermediate results, one big disjunction at end) %%%%%%%%%%%%%%%%%%% dnf_to_bdd_naive :- bdd_init(FDO, PID), dnf_to_bdd_naive(FDO), bdd_kill(FDO, PID, _S). dnf_to_bdd_naive(FDO) :- nb_setval(aproblog_script_lines,[]), nb_getval(aproblog_completed_proofs, Trie), traverse_ptree(Trie,Explanation), add_to_bdd(Explanation, FDO), fail. dnf_to_bdd_naive(FDO) :- nb_getval(aproblog_script_lines,Lines), ( Lines = [] % empty trie is false -> bdd_line([],'FALSE',_,L) ; bdd_OR([], Lines, L) ), bdd_laststep(LID), bdd_commit(FDO, L), bdd_commit(FDO, LID). % trie with single element 'true" add_to_bdd([true],FDO) :- !, bdd_line([],'TRUE',_,L1), bdd_laststep(L1S), bdd_commit(FDO, L1), nb_getval(aproblog_script_lines,SoFar), nb_setval(aproblog_script_lines,[L1S|SoFar]). add_to_bdd(AndList,FDO) :- ids_to_vars(AndList,List),%write(List),nl, bdd_AND([], List, L1), bdd_laststep(L1S), bdd_commit(FDO, L1), nb_getval(aproblog_script_lines,SoFar), nb_setval(aproblog_script_lines,[L1S|SoFar]). %%%%%%%%%%%%%%%%%% % dnf to bdd translation using dbtrie at optimization level 0 % adapted copy of ptree's trie_to_bdd_trie %%%%%%%%%%%%%%%%%%% dnf_to_bdd :- bdd_init(FDO, PID), dnf_to_bdd(FDO), bdd_kill(FDO, PID, _S). % taken from ptree.yap's trie_to_bdd_trie and adapted to write to online interface dnf_to_bdd(FDO) :- nb_getval(aproblog_completed_proofs, Trie), trie_to_depth_breadth_trie(Trie, B, LL, 0), % the last one is the optimization level, LL the last definition's name (ptree:is_label(LL) -> tell(FDO), ptree:trie_write(B, LL), write(LL), nl, tell(user) ; (ptree:is_state(LL) -> Edges = [] ; Edges = [LL] ), tell(FDO), (LL = not(ID) -> ptree:get_var_name(ID, NLL), write('L1 = ~'), write(NLL),nl ; ptree:get_var_name(LL, NLL), write('L1 = '), write(NLL),nl ), write('L1'), nl, tell(user) ). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % core of Theo's BDD traversal with lazy evaluation, adapted to semiring operators % this does not use caching, so don't try with larger BDDs %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% lazy_eval(FDO,FDI,Value) :- repeat, bdd_current(FDO, FDI, N, I, NodeId), (calcp(R, L) -> retract(calcp(R, L)), L = [CP|T], (bdd_leaf(N) -> CP = N, NL = T ; CP = s(m(N,PH),m(c(N),PL)), NL = [PH,PL|T] ),%write(R),nl, assert(calcp(R, NL)) ; R = s(m(N,PH),m(c(N),PL)), NL = [PH, PL],%write(R),nl, assert(calcp(R, NL)) ), bdd_nextDFS(FDO), I = 0, bdd_leaf(N), bdd_current(FDO, FDI, N, I, NodeId), !, calcp(FR, FL), % write(FR),nl, evaluate_expression(FR,Value), retract(calcp(FR, FL)). %%%%%%%%%%%%%%% % lazy evaluation builds a nested term that needs to be evaluated: %%%%%%%%%%%%%%% % attempt to catch base cases evaluate_expression(s(m('FALSE',_),m(c('FALSE'),_)), Z) :- !, semiring_zero(Z). evaluate_expression(s(m('TRUE',_),m(c('TRUE'),_)), Z) :- !, semiring_one(Z). evaluate_expression(V,Z) :- var(V), !, format(user_error,'~n ERROR: unresolved variable in lazy evaluation, will be assumed zero...~n likely it is a trivial BDD, in which case the result should still be ok, but...~2n',[]), semiring_zero(Z). % normal evaluation evaluate_expression(s(A,B),C) :- !, evaluate_expression(A,AE), evaluate_expression(B,BE), semiring_addition(AE,BE,C). evaluate_expression(m(A,B),C) :- !, evaluate_expression(A,AE), evaluate_expression(B,BE), semiring_multiplication(AE,BE,C). evaluate_expression(c(A),C) :- !, evaluate_expression(A,V), label_negated(V,C). evaluate_expression('FALSE',Z) :- !, semiring_zero(Z). evaluate_expression('TRUE',Z) :- !, semiring_one(Z). evaluate_expression(A,C) :- get_var_label(A,C,_). %%%%%%%%%%%%% % depth first search in BDD with result caching (dymanic predicate aproblog_cached/4 with args NodeVar, NodeID, Label, SeenVars) % the first argument of traverse_bdd_caching/3 is a stack remembering how to combine cached results % - FDO and FDI are the output and input communication channels for the BDD % - it initially contains a dummy element "root" such that the empty stack indicates the end of the procedure % - other elements are of form n(Node,High,Low), each argument consisting of VariableID-BDDNodeID (the first two args of the cache) % key idea: % - always record the current BDD node in the stack as a child of the current element % - if current BDD node is cached already % then pop it from BDD traversal (bdd_ignoreDFS), % else add it to the stack as new current element and expand it in BDD traversal (bdd_nextDFS) % - before looking at the next node, reduce the stack %%%%%%%%%%%%%% eval_bdd_cached(FDO, FDI, Result,Vars ) :- retractall(aproblog_cached(_,_,_,_)), bdd_current(FDO, FDI, N, _I, NodeId), traverse_bdd_caching([root],FDO, FDI), % normally n(VariableID-BDDNodeID, HighChild, LowChild), but dummy "root" first aproblog_cached(N,NodeId,Result,Vars). traverse_bdd_caching([],_FDO, _FDI). traverse_bdd_caching([HeadS|RestS],FDO, FDI) :- bdd_current(FDO, FDI, N, _I, NodeID), add_child(N-NodeID,HeadS,NewHead), ( aproblog_cached(N,NodeID,_,_) -> bdd_ignoreDFS(FDO), NewStack = [NewHead|RestS] ; NewStack = [n(N-NodeID,_,_),NewHead|RestS], bdd_nextDFS(FDO) ), reduce_stack(NewStack,RedStack),%write(NewStack),nl,write(RedStack),nl,nl, traverse_bdd_caching(RedStack, FDO, FDI). % recording the current node as the next unknown child add_child(_Kid,root,root). add_child(Kid,n(Node,High,Low),n(Node,Kid,Low)) :- var(High),!. add_child(Kid,n(Node,High,Low),n(Node,High,Kid)) :- var(Low). %%%%%%%%%%%%%% % reducing the stack and caching the result: % - whenever the current stack element is either a leaf or ground, the entire subtree below has been evaluated % and we can calculate and cache the result % - once the first other element is reached, we know this is the parent of the next visited node % - "root" is the dummy at the end of the stack that makes it possible to use the empty stack as stopping criterion %%%%%%%%%%%%% reduce_stack([root],[]). reduce_stack([n(N-ID,_,_)|Stack],Red) :- bdd_leaf(N), !, cache_leaf(N,ID), reduce_stack(Stack,Red). reduce_stack([n(N-ID,H,L)|Stack],Reduced) :- ( ground(n(N-ID,H,L)) -> cache_inner_node(N-ID,H,L), reduce_stack(Stack,Reduced) ; Reduced = [n(N-ID,H,L)|Stack] ). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % evaluation and caching of labels associated to BDD nodes % - this takes care of keeping variables for compensation if needed %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % leaves cache_leaf(Var,Node) :- ( aproblog_cache_vars -> cache_leaf_vars(Var,Node) ; cache_leaf_pure(Var,Node) ). cache_leaf_pure('TRUE',ID) :- semiring_one(W), assert(aproblog_cached('TRUE',ID,W,na)). cache_leaf_pure('FALSE',ID) :- semiring_zero(W), assert(aproblog_cached('FALSE',ID,W,na)). cache_leaf_vars('TRUE',ID) :- semiring_one(W), assert(aproblog_cached('TRUE',ID,W,[])). cache_leaf_vars('FALSE',ID) :- semiring_zero(W), assert(aproblog_cached('FALSE',ID,W,[])). % for inner nodes, multiply value of children with corresponding label and sum cache_inner_node(N,H,L) :- ( aproblog_cache_vars -> cache_inner_node_vars(N,H,L) ; cache_inner_node_pure(N,H,L) ). cache_inner_node_pure(N-ID,H-HID,L-LID) :- aproblog_cached(H,HID,HW,_), aproblog_cached(L,LID,LW,_), get_var_label(N,W,_), label_negated(W,C), semiring_multiplication(W,HW,HighW), semiring_multiplication(C,LW,LowW), semiring_addition(HighW,LowW,Label), assert(aproblog_cached(N,ID,Label,na)). cache_inner_node_vars(N-ID,H-HID,L-LID) :- aproblog_cached(H,HID,HW,HV), aproblog_cached(L,LID,LW,LV), get_var_label(N,W,VarID), label_negated(W,C), compensate_label(LV,HV,HW,HighW),%format(user_error,'compensated ~w ~w ~w ~w~n',[LV,HV,HW,HighW]), semiring_multiplication(W,HighW,HWComp),%format(user_error,'multiplied ~w ~w ~w~n',[W,HighW,HWComp]), compensate_label(HV,LV,LW,LowW),%format(user_error,'compensated ~w ~w ~w ~w~n',[HV,LV,LW,LowW]), semiring_multiplication(C,LowW,LWComp),%format(user_error,'multiplied ~w ~w ~w~n',[C,LowW,LWComp]), semiring_addition(HWComp,LWComp,Label),%format(user_error,'added ~w ~w ~w~n',[HWComp,LWComp,Label]), append([VarID|HV],LV,AllV), sort(AllV,SortV),%format(user_error,'cache ~w ~w ~w ~w~n',[N,ID,Label,SortV]), assert(aproblog_cached(N,ID,Label,SortV)). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % general auxiliaries %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % given list of possibly negated fact identifiers (= random variables), strip off negation get_variables([],[]). get_variables([not(V)|Vs],[V|Others]) :- !, get_variables(Vs,Others). get_variables([V|Vs],[V|Others]) :- get_variables(Vs,Others). % for variables in the first but not the second list, we multiply by the sum of their positive and negative label compensate_label([],_,W,W). compensate_label([A|Rest],Vars,Acc,Result) :- memberchk(A,Vars), !, compensate_label(Rest,Vars,Acc,Result). compensate_label([A|Rest],Vars,Acc,Result) :- get_fact_label(A,W), label_negated(W,WW), semiring_addition(W,WW,CA), semiring_multiplication(CA,Acc,Next), compensate_label(Rest,Vars,Next,Result). % transform a list of possibly negated fact identifiers into the corresponding list of (negated) BDD variables ids_to_vars([],[]). ids_to_vars([not(A)|B],[C|D]) :- !, atomic_concat(['~x',A],C), ids_to_vars(B,D). ids_to_vars([A|B],[C|D]) :- atomic_concat(['x',A],C), ids_to_vars(B,D). % given a BDD variable, get the associated label and ID % for ground facts, return just the ID (without quotes - breaks compensation for unseen variables on BDD else!) % for non-ground facts, return the ID including the grounding ID get_var_label(XID,Label,VariableName) :- atom_concat(x,IAtom,XID), get_fact_from_id(IAtom,NumAtom), atom_number(NumAtom,FactID), get_fact_label(FactID,Label), ( IAtom == NumAtom -> VariableName = FactID ; VariableName = IAtom ). % for nonground facts, extract fact id get_fact_from_id(IAtom,NumAtom) :- atom_concat(NumAtom,Part2,IAtom), atom_concat('_',_GID,Part2),!. get_fact_from_id(I,I). conditional_format(_String,_Args) :- aproblog_flag(verbose,false),!. conditional_format(String,Args) :- format(String,Args). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % user needs to provide these five predicates as part of the aproblog program %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% semiring_zero(Z) :- user:semiring_zero(Z). semiring_one(Z) :- user:semiring_one(Z). semiring_addition(OldLabel,Label,NewLabel) :- user:semiring_addition(OldLabel,Label,NewLabel). semiring_multiplication(OldLabel,Label,NewLabel) :- user:semiring_multiplication(OldLabel,Label,NewLabel). label_negated(W,Wbar) :- user:label_negated(W,Wbar). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % top level predicates %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % choose automatically based on flags (default: both false) aproblog_label(Query,Label) :- aproblog_flag(disjoint_sum,true), aproblog_flag(neutral_sum,true), label_neutral_disjoint(Query,Label). aproblog_label(Query,Label) :- aproblog_flag(disjoint_sum,true), aproblog_flag(neutral_sum,false), label_disjoint(Query,Label). aproblog_label(Query,Label) :- aproblog_flag(disjoint_sum,false), aproblog_flag(neutral_sum,true), label_neutral(Query,Label). aproblog_label(Query,Label) :- aproblog_flag(disjoint_sum,false), aproblog_flag(neutral_sum,false), label(Query,Label). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % query label: if sums are neutral and disjoint, calculate the label on the fly %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % for those not remembering the order :) label_disjoint_neutral(Query,Label) :- label_neutral_disjoint(Query,Label). label_neutral_disjoint(Query,Label) :- conditional_format('disjoint and neutral~n',[]), statistics(walltime,[S,_]), direct_eval(Query,Label), statistics(walltime,[D,_]), Time is D - S, conditional_format('time to calculate label: ~w~n',[Time]). direct_eval(Goal,_) :- init_aproblog, semiring_zero(Zero), nb_setval(aproblog_label, Zero), aproblog_call(Goal), add_solution_to_eval, fail. direct_eval(_,Label) :- b_getval(aproblog_label, Label). add_solution_to_eval :- b_getval(aproblog_current_proof, IDs), update_label(IDs). % old version: evaluate DNF as is label_neutral_disjoint_on_dnf(Query,Label) :- conditional_format('disjoint and neutral~n',[]), statistics(walltime,[S,_]), build_dnf(Query), statistics(walltime,[D,_]), BT is D - S, conditional_format('time to build DNF: ~w~n',[BT]), evaluate_dnf(Label), statistics(walltime,[W,_]), WT is W - D, conditional_format('time to calculate label: ~w~n',[WT]), delete_dnf. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % query label: if sums are disjoint but not neutral, calculate the label on the fly with compensation; % compensation ignores labeled facts not used in any proof of the query %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% label_disjoint(Query,Label) :- conditional_format('disjoint but not neutral~n',[]), statistics(walltime,[S,_]), direct_eval_with_compensation(Query,Label), statistics(walltime,[D,_]), T is D - S, conditional_format('time to calculate label: ~w~n',[T]). direct_eval_with_compensation(Goal,_) :- init_aproblog, nb_setval(aproblog_variables, []), semiring_zero(Zero), nb_setval(aproblog_label, Zero), aproblog_call(Goal), add_solution_to_eval_with_compensation, fail. direct_eval_with_compensation(_,Label) :- b_getval(aproblog_label, LabelOnUsed), ( aproblog_flag(compensate_unused, true) -> b_getval(aproblog_variables, UsedVars), compensate_for_unseen_vars(LabelOnUsed, UsedVars, Label) ; Label = LabelOnUsed ). add_solution_to_eval_with_compensation :- b_getval(aproblog_current_proof, IDs), update_label_with_compensation(IDs). compensate_for_unseen_vars(LabelOnUsed, UsedVars, Label) :- findall(ID,(labeled_fact(_,_,ID),\+non_ground_fact(ID)),AllVars), compensate_label(AllVars,UsedVars,LabelOnUsed,Label), ( non_ground_fact(SomeId) -> get_fact(SomeId,SomeIdFact), SomeIdLabel::SomeIdFact, format(user_error,'~2nERROR: cannot fully compensate in program with non-ground facts such as ~q::~q!~nResult with respect to used and ground facts is ~q~2n',[SomeIdLabel,SomeIdFact,Label]), throw(error('tried compensation on non-ground facts')) ; true ). % old version: evaluate DNF with compensation label_disjoint_on_dnf(Query,Label) :- conditional_format('disjoint but not neutral~n',[]), statistics(walltime,[S,_]), build_dnf(Query), statistics(walltime,[D,_]), BT is D - S, conditional_format('time to build DNF: ~w~n',[BT]), evaluate_dnf_with_compensation(Label), statistics(walltime,[W,_]), WT is W - D, conditional_format('time to calculate label: ~w~n',[WT]), delete_dnf. % variant that always compensates for all DNF variables % intended for debugging purposes, does some redundant list operations in reused code label_disjoint_naive(Query,Label) :- statistics(walltime,[S,_]), build_dnf(Query), statistics(walltime,[D,_]), BT is D - S, conditional_format('time to build DNF: ~w~n',[BT]), evaluate_dnf_with_compensation_naive(Label), statistics(walltime,[W,_]), WT is W - D, conditional_format('time to calculate label: ~w~n',[WT]), delete_dnf. %%%%%%%%%%%%%%% % query label: if sums are neutral but not disjoint, evaluate the BDD; % using depth first search with caching %%%%%%%%%%%%%% label_neutral(Query,Result) :- conditional_format('not disjoint but neutral~n',[]), retractall(aproblog_cache_vars), % do not cache variables for compensation label_internal(Query,Result). % variant using lazy evaluation without caching label_lazy(Query,Label) :- statistics(walltime,[S,_]), build_dnf(Query), statistics(walltime,[D,_]), BT is D - S, conditional_format('time to build DNF: ~w~n',[BT]), bdd_init(FDO,FDI, PID), dnf_to_bdd(FDO), % change to dnf_to_bdd_naive to use naive preprocessing statistics(walltime,[B,_]), BBT is B - D, conditional_format('time to build BDD: ~w~n',[BBT]), lazy_eval(FDO,FDI,Label), statistics(walltime,[EB,_]), EBT is EB - B, conditional_format('time to lazily calculate label on BDD: ~w~n',[EBT]), bdd_kill(FDO,FDI, PID, _), delete_dnf. %%%%%%%%%%%%%%% % query label: if sums are neither neutral nor disjoint, evaluate the BDD with compensation; % using depth first search with caching % ignores labeled facts not used in any proof of the query %%%%%%%%%%%%%% label(Query,Result) :- conditional_format('neither disjoint nor neutral~n',[]), retractall(aproblog_cache_vars), assert(aproblog_cache_vars), % cache variables for compensation label_internal(Query,Result). % shared skeleton of bdd-based methods label_neutral/2 and label/2, controlled by dynamic predicate aproblog_cache_vars/0 % 1. collect explanations in DNF % 2. feed DNF to BDD tool % 3. evaluate BDD with caching label_internal(Query,Label) :- statistics(walltime,[S,_]), build_dnf(Query), statistics(walltime,[D,_]), BT is D - S, conditional_format('time to build DNF: ~w~n',[BT]), bdd_init(FDO,FDI, PID), dnf_to_bdd(FDO), % change to dnf_to_bdd_naive to use naive preprocessing statistics(walltime,[B,_]), BBT is B - D, conditional_format('time to build BDD: ~w~n',[BBT]), eval_bdd_cached(FDO, FDI, LabelOnUsed, UsedVars ), bdd_kill(FDO,FDI, PID, _), % clean up first, as compensate_for_unseen_vars throws error for non-ground facts retractall(aproblog_cached(_,_,_,_)), delete_dnf, ( (aproblog_flag(compensate_unused, true), aproblog_cache_vars) % only compensate if we're in the general case, not for neutral sums... -> compensate_for_unseen_vars(LabelOnUsed, UsedVars, Label) ; Label = LabelOnUsed ), statistics(walltime,[EB,_]), EBT is EB - B, conditional_format('time to calculate label on BDD: ~w~n',[EBT]). %%%%%%%%%%%%%%%%%%%%%% % structural output only %%%%%%%%%%%%%%%%%%%%%% % DNF print_dnf(Query) :- build_dnf(Query), print_dnf, delete_dnf. % BDD print_bdd(Query) :- build_dnf(Query), dnf_to_bdd, % change to dnf_to_bdd_naive to use naive preprocessing delete_dnf. % random variables / facts used used_vars(Query,Vars) :- build_dnf(Query), nb_getval(aproblog_completed_proofs, Trie), edges_ptree(Trie,Vars), delete_dnf. used_facts(Query,Facts) :- used_vars(Query,Vars), get_fact_list(Vars,Facts). %%%%%%%%%%%%%% % testing predicates %%%%%%%%%%%% % call all labeling functions test(Query) :- label_neutral_disjoint(Query,LND), format('~nResult: ~q~2n',[LND]), label_disjoint(Query,LD), format('~nResult: ~q~2n',[LD]), label_neutral(Query,LN), format('~nResult: ~q~2n',[LN]), label(Query,L), format('~nResult: ~q~2n',[L]). % this works on internal predicates on DNF, which aren't used any more directly test_inner(Query) :- statistics(walltime,[S,_]), build_dnf(Query), statistics(walltime,[DNF,_]), DNFTime is DNF - S, format('time to build DNF: ~w~n',[DNFTime]), evaluate_dnf(WX), statistics(walltime,[WXT,_]), DNFEvalTime is WXT - DNF, format('time to calculate label on DNF: ~w~2nResult: ~w~2n',[DNFEvalTime,WX]), statistics(walltime,[StartComp,_]), evaluate_dnf_with_compensation(DNFwithComp), statistics(walltime,[EndComp,_]), Diffwc is EndComp-StartComp, format('time to calculate label on DNF with compensation: ~w~2nResult: ~w~2n',[Diffwc,DNFwithComp]), bdd_init(FDO,FDI, PID), dnf_to_bdd(FDO), % change to dnf_to_bdd_naive to use naive preprocessing statistics(walltime,[BDD,_]), BddBuild is BDD - EndComp, format('time to build BDD: ~w~n',[BddBuild]), retractall(aproblog_cache_vars), eval_bdd_cached(FDO, FDI, WS, _Vars ), statistics(walltime,[TWS,_]), BddTimeWS is TWS - BDD, format('time to calculate label on BDD: ~w~2nResult: ~w~2n',[BddTimeWS,WS]), bdd_reset(FDO), assert(aproblog_cache_vars), eval_bdd_cached(FDO, FDI, WS2, _ ), statistics(walltime,[TWS2,_]), BddTimeWS2 is TWS2 - TWS, format('time to calculate label on BDD with compensation: ~w~2nResult: ~w~2n',[BddTimeWS2,WS2]), bdd_kill(FDO,FDI, PID, _), delete_dnf. %%%%%%%%%%%%%% trial area %%%%%%%%%%