2011-09-05 02:07:15 +01:00
%%% -*- 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)
)).
2016-06-02 10:53:36 +01:00
% directory where simplecudd executable is located
2011-09-05 02:07:15 +01:00
% automatically set during loading -- assumes it is in same place as this file (problog.yap)
2016-06-02 10:53:36 +01:00
%:- PD = /usr/local/bin, set_problog_path(PD).
2011-09-05 02:07:15 +01:00
:- 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 %%%%%%%%%%
