yap-6.3/packages/ProbLog/problog/tptree.yap

%%% -*- Mode: Prolog; -*-

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
%  $Date: 2010-09-28 21:04:43 +0200 (Tue, 28 Sep 2010) $
%  $Revision: 4838 $
%
%  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 authors of this file:
%  Angelika Kimmig, Vitor Santos Costa,Bernd Gutmann,
%  Theofrastos Mantadelis, Guy Van den Broeck
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% 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.
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% prefix-trees for managing a DNF
% remembers shortest prefix of a conjunction only (i.e. a*b+a*b*c results in a*b only, but b*a+a*b*c is not reduced)
% children are sorted, but branches aren't (to speed up search while keeping structure sharing from proof procedure)
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

:- module(ptree, [init_ptree/1,
                  delete_ptree/1,
                  member_ptree/2,
                  enum_member_ptree/2,
                  insert_ptree/2,
                  delete_ptree/2,
                  edges_ptree/2,
                  count_ptree/2,
                  prune_check_ptree/2,
                  empty_ptree/1,
                  merge_ptree/2,
                  merge_ptree/3,
                  bdd_ptree/3,
                  bdd_struct_ptree/3,
                  bdd_ptree_map/4,
                  bdd_struct_ptree_map/4,
                  traverse_ptree/2,            %theo
                  print_ptree/1,               %theo
                  statistics_ptree/0,          %theo
                  print_nested_ptree/1,        %theo
                  trie_to_bdd_trie/5,          %theo
                  trie_to_bdd_struct_trie/5,
                  nested_trie_to_bdd_trie/5,   %theo
                  nested_trie_to_bdd_struct_trie/5,
                  ptree_decomposition/3,
                  ptree_decomposition_struct/3,
                  nested_ptree_to_BDD_script/3, %theo
                  nested_ptree_to_BDD_struct_script/3,
                  ptree_db_trie_opt_performed/3,
                  bdd_vars_script/1
                 ]).

% load library modules
:- use_module(library(tries)).
:- use_module(library(lists), [append/3, member/2, memberchk/2, delete/3]).
:- use_module(library(system), [delete_file/1, shell/1]).
:- use_module(library(ordsets), [ord_intersection/3, ord_union/3]).

% load our own modules
:- use_module(flags).

% switch on all tests to reduce bug searching time
:- style_check(all).
:- yap_flag(unknown,error).


% this is a test to determine whether YAP provides the needed trie library
:- initialization(
        (       predicate_property(trie_disable_hash, imported_from(tries)) ->
                trie_disable_hash
        ;       print_message(warning,'The predicate tries:trie_disable_hash/0 does not exist. Please update trie library.')
        )
).

%%%%%%%%%%%%%%%%%%%%%%%
% Define module flags
%%%%%%%%%%%%%%%%%%%%%%%

:- initialization((
	problog_define_flag(use_db_trie,     problog_flag_validate_boolean, 'use the builtin trie 2 trie transformation', false),
	problog_define_flag(db_trie_opt_lvl, problog_flag_validate_integer, 'optimization level for the trie 2 trie transformation', 0),
	problog_define_flag(compare_opt_lvl, problog_flag_validate_boolean, 'comparison mode for optimization level', false),
	problog_define_flag(db_min_prefix,   problog_flag_validate_integer, 'minimum size of prefix for dbtrie to optimize', 2),
	problog_define_flag(use_naive_trie,  problog_flag_validate_boolean, 'use the naive algorithm to generate bdd scripts', false),
	problog_define_flag(use_old_trie,    problog_flag_validate_boolean, 'use the old trie 2 trie transformation no nested', true),
	problog_define_flag(use_dec_trie,    problog_flag_validate_boolean, 'use the decomposition method', false),
	problog_define_flag(subset_check,    problog_flag_validate_boolean, 'perform subset check in nested tries', true),
	problog_define_flag(deref_terms,     problog_flag_validate_boolean, 'deref BDD terms after last use', false),
	
	problog_define_flag(trie_preprocess, problog_flag_validate_boolean, 'perform a preprocess step to nested tries', false),
	problog_define_flag(refine_anclst,   problog_flag_validate_boolean, 'refine the ancestor list with their childs', false),
	problog_define_flag(anclst_represent,problog_flag_validate_in_list([list, integer]), 'represent the ancestor list', list)
)).


%%%%%%%%%%%%%%%%%%%%%%%%
% ptree basics
%%%%%%%%%%%%%%%%%%%%%%%%

init_ptree(Trie) :-
	trie_open(Trie).

delete_ptree(Trie) :-
	trie_close(Trie), !.
delete_ptree(_).

empty_ptree(Trie) :-
	trie_usage(Trie, 0, 0, 0).

traverse_ptree(Trie, List) :-
  trie_traverse(Trie, Ref),
  trie_get_entry(Ref, List).

traverse_ptree_mode(Mode) :-
  trie_traverse_mode(Mode).

%%%%%%%%%%%%%%%%%%%%%%%%
% member
%%%%%%%%%%%%%%%%%%%%%%%%

% non-backtrackable (to check)
member_ptree(List, Trie) :-
	trie_check_entry(Trie, List, _).

% backtrackable (to list)
enum_member_ptree(List, Trie) :-
	trie_path(Trie, List).

trie_path(Trie, List) :-
	trie_traverse(Trie, Ref),
	trie_get_entry(Ref, List).

%%%%%%%%%%%%%%%%%%%%%%%%
% insert conjunction
%%%%%%%%%%%%%%%%%%%%%%%%
insert_ptree(false, _Trie) :-!.
insert_ptree(true, Trie) :-
  !,
  trie_delete(Trie),
  trie_put_entry(Trie, [true], _).
insert_ptree(List, Trie) :-
  (trie_check_entry(Trie, [true], _) -> % prune if there is a prob=1 proof
    true
  ;
    trie_put_entry(Trie, List, _)
	).


%%%%%%%%%%%%%%%%%%%%%%%%
% delete conjunction
%%%%%%%%%%%%%%%%%%%%%%%%
delete_ptree(List, Trie) :-
	trie_check_entry(Trie, List, Ref),
	trie_remove_entry(Ref).


%%%%%%%%
% return list -Edges of all edge labels in ptree
% doesn't use any heuristic to order those for the BDD
% (automatic reordering has to do the job)
%%%%%%%%%
edges_ptree(Trie, []) :-
	empty_ptree(Trie),
	!.
edges_ptree(Trie, []) :-
	trie_check_entry(Trie, [true], _),
	!.
edges_ptree(Trie ,Edges) :-
	setof(X, trie_literal(Trie, X), Edges).

trie_literal(Trie, X) :-
	trie_traverse(Trie,Ref),
	trie_get_entry(Ref, List),
	member(X, List).

%%%%%%%%
% number of conjunctions in the tree
%%%%%%%%%

count_ptree(Trie, N) :-
	trie_usage(Trie, N, _, _).

%%%%%%%%
% check whether some branch of ptree is a subset of conjunction List
% useful for pruning the search for proofs (optional due to time overhead)
% currently not implemented, just fails
%%%%%%%

prune_check_ptree(_List, _Trie) :-
	format(user,'FAIL: prune check currently not supported~n',[]),
	flush_output(user),
	fail.

%%%%%%%%%%%%%
% merge two ptrees
% - take care not to loose proper prefixes that are proofs!
%%%%%%%%%%%%%%%
merge_ptree(T1, _) :-
	trie_check_entry(T1, [true], _), !.
merge_ptree(_, T2) :-
	trie_check_entry(T2, [true], _), !. % is this strange on the loop condition?
merge_ptree(T1, T2) :-
	trie_join(T1, T2).

merge_ptree(T1, _, T3) :-
	trie_check_entry(T1, [true], _),
	!,
	trie_open(T3),
	trie_put_entry(T3, [true], _).
merge_ptree(_, T2, T3) :-
	trie_check_entry(T2, [true], _),
	!,
	trie_open(T3),
	trie_put_entry(T3, [true], _).
merge_ptree(T1, T2, T3) :-
	trie_dup(T1, T3),
	trie_join(T3, T2).

%%%%%%%%%%%%%%%%%%%%%%%%
% Write structural BDD script for given trie to file
% does NOT write a parameter file but unifies a list of used variables
%
% Specialized versions are:
% - bdd_ptree -> bdd_struct_ptree
% - bdd_ptree_map -> bdd_struct_ptree_map
% - nested_ptree_to_BDD_script -> nested_ptree_to_BDD_struct_script
% - trie_to_bdd_trie -> trie_to_bdd_struct_trie
% - nested_trie_to_bdd_trie -> nested_trie_to_bdd_struct_trie
% - ptree_decomposition -> ptree_decomposition_struct
% - bdd_ptree_script -> bdd_struct_ptree_script
%%%%%%%%%%%%%%%%%%%%%%%%
:- dynamic(c_num/1).

bdd_struct_ptree(Trie, FileBDD, Variables) :-
    bdd_struct_ptree_script(Trie, FileBDD, Variables),
    eraseall(map).

bdd_struct_ptree_map(Trie, FileBDD, Variables, Mapping) :-
    bdd_struct_ptree_script(Trie, FileBDD, Variables),
    findall(X, recorded(map, X, _), Map),
    add_probs(Map, Mapping),
    eraseall(map).

bdd_struct_ptree_script(Trie, FileBDD, Variables) :-
    edges_ptree(Trie, Variables),
    name_vars(Variables), % expected by output_compressed_script/1?
    length(Variables, VarCount),
    assertz(c_num(1)),
    bdd_pt(Trie, CT),
    c_num(NN),
    IntermediateSteps is NN - 1,
    tell(FileBDD),
    format('@BDD1~n~w~n~w~n~w~n', [VarCount, 0, IntermediateSteps]),
    output_compressed_script(CT),
    told,
    retractall(c_num(_)),
    retractall(compression(_, _)).

name_vars([]).
name_vars([A|B]) :-
    (
     A=not(ID)
    ->
     get_var_name(ID,_)
     ;
     get_var_name(A,_)
    ),
    name_vars(B).

nested_ptree_to_BDD_struct_script(Trie, BDDFileName, Variables):-
  tmpnam(TmpFile1),
  tmpnam(TmpFile2),
  open(TmpFile1, 'write', BDDS),
  (generate_BDD_from_trie(Trie, Inter, BDDS) ->
    next_intermediate_step(TMP), InterCNT is TMP - 1,
    write(BDDS, Inter), nl(BDDS),
    close(BDDS),
    (get_used_vars(Variables, VarCNT);VarCNT = 0),
    open(TmpFile2, 'write', HEADERS),
    write(HEADERS, '@BDD1'), nl(HEADERS),
    write(HEADERS, VarCNT), nl(HEADERS),
    write(HEADERS, 0), nl(HEADERS),
    write(HEADERS, InterCNT), nl(HEADERS),
    close(HEADERS),
    atomic_concat(['cat ', TmpFile2, ' ', TmpFile1, ' > ', BDDFileName], CMD),
    shell(CMD),
    delete_file(TmpFile1),
    delete_file(TmpFile2),
    cleanup_BDD_generation
  ;
    close(BDDS),
    (delete_file(TmpFile1);true),
    (delete_file(TmpFile2);true),
    cleanup_BDD_generation,
    fail
  ).

trie_to_bdd_struct_trie(A, B, OutputFile, OptimizationLevel, Variables) :-
  trie_to_depth_breadth_trie(A, B, LL, OptimizationLevel),
  (atomic_concat('L', InterStep, LL) -> % what does this mean?
    retractall(deref(_,_)),
    (problog_flag(deref_terms, true) ->
      asserta(deref(LL,no)),
      mark_for_deref(B),
      V = 3
    ;
      V = 1
    ),
    variables_in_dbtrie(B, Variables), %not the most efficient solution
    length(Variables, VarCNT),         %this 2 should be changed
    tell(OutputFile),
    write('@BDD'), write(V), nl,
    write(VarCNT), nl,
    write(0), nl,
    write(InterStep), nl,
    trie_write(B, LL),
    write(LL), nl,
    told
  ;
    (is_state(LL) ->
      Variables = []
    ;
      Variables = [LL]
    ),
    tell(OutputFile),
    write('@BDD1'), nl,
    write(1), nl,
    write(0), nl,
    write(1), nl,
    get_var_name(LL, NLL),
    write('L1 = '),write(NLL),nl,
    write('L1'), nl,
    told
  ).

nested_trie_to_bdd_struct_trie(A, B, OutputFile, OptimizationLevel, Variables):-
  trie_nested_to_depth_breadth_trie(A, B, LL, OptimizationLevel, problog:problog_chktabled),
  (is_label(LL) ->
    retractall(deref(_,_)),
    (problog_flag(deref_terms, true) ->
      asserta(deref(LL,no)),
      mark_for_deref(B),
      V = 3
    ;
      V = 1
    ),
    variables_in_dbtrie(B, Variables), %not the most efficient solution
    length(Variables, VarCNT),         %this 2 should be changed
    tell(OutputFile),
    write('@BDD'), write(V), nl,
    write(VarCNT), nl,
    write(0), nl,
    (LL = not(NegL)->
      atomic_concat('L', NegStep, NegL),
      number_atom(NegStepN, NegStep),
      InterStep is NegStepN + 1,
      atomic_concat('L', InterStep, FL),
      write(InterStep), nl,
      trie_write(B, FL),
      write(FL), write(' = ~'), write(NegL), nl,
      write(FL), nl
    ;
      atomic_concat('L', InterStep, LL),
      write(InterStep), nl,
      trie_write(B, LL),
      write(LL), nl
    ),
    told
  ;
    (is_state(LL) ->
      Variables = []
    ;
      Variables = [LL]
    ),
    tell(OutputFile),
    write('@BDD1'), nl,
    write(1), nl,
    write(0), nl,
    write(1), nl,
    get_var_name(LL, NLL),
    write('L1 = '),write(NLL),nl,
    write('L1'), nl,
    told
  ).

ptree_decomposition_struct(Trie, BDDFileName, Variables) :-
  tmpnam(TmpFile1),
  tmpnam(TmpFile2),
  nb_setval(next_inter_step, 1),
  variables_in_dbtrie(Trie, Variables),
  length(Variables, VarCnt),
  tell(TmpFile1),
  decompose_trie(Trie, Variables, L),
  (is_label(L)->
    atomic_concat('L', LCnt, L),
    write(L),nl
  ;
    LCnt = 1,
    write('L1 = '),
    (L == false ->
      write('FALSE')
    ;
      write(L)
    ), nl,
    write('L1'), nl
  ),
  told,
  tell(TmpFile2),
  write('@BDD1'),nl,
  write(VarCnt),nl,
  write('0'),nl,
  write(LCnt),nl,
  told,
  atomic_concat(['cat ', TmpFile2, ' ', TmpFile1, ' > ', BDDFileName], CMD),
  shell(CMD),
  delete_file(TmpFile1),
  delete_file(TmpFile2).

%%%%%%%%%%%%%%%%%%%%%%%%
% write BDD info for given ptree to file
% - initializes leaf BDDs (=variables) first
% - then compresses ptree to exploit subtree sharing
% - bdd_pt/1 does the work on the structure itself
%%%%%%%%%%%%%%%%%%%%%%%%


bdd_ptree(Trie, FileBDD, FileParam) :-
	bdd_ptree_script(Trie, FileBDD, FileParam),
	eraseall(map).

% version returning variable mapping
bdd_ptree_map(Trie, FileBDD, FileParam, Mapping) :-
	bdd_ptree_script(Trie, FileBDD, FileParam),
	findall(X, recorded(map, X, _), Map),
	add_probs(Map, Mapping),
	eraseall(map).

add_probs([], []).
add_probs([m(A,Name)|Map], [m(A, Name, Prob)|Mapping]) :-
	% FIXME: Does this work with non-ground facts
	problog:get_fact_probability(A, Prob),
	add_probs(Map, Mapping).

% number of variables may be to high:
% counted on trie, but conversion to old tree representation
% transforms A*B+A to A (prefix-test)
bdd_ptree_script(Trie, FileBDD, FileParam) :-
	edges_ptree(Trie, Edges),
	tell(FileParam),
	bdd_vars_script(Edges),

	flush_output,

	told,
	length(Edges, VarCount),
	assertz(c_num(1)),
	bdd_pt(Trie, CT),
	c_num(NN),
	IntermediateSteps is NN - 1,
	tell(FileBDD),
	format('@BDD1~n~w~n~w~n~w~n', [VarCount, 0, IntermediateSteps]),
	output_compressed_script(CT),


	told,
	retractall(c_num(_)),
	retractall(compression(_, _)).

% write parameter file by iterating over all var/not(var) occuring in the tree
bdd_vars_script([]).
bdd_vars_script([A|B]) :-
	(
	 A=not(ID)
	->
	 bdd_vars_script_intern(ID);
	 bdd_vars_script_intern(A)
	),
	bdd_vars_script(B).
bdd_vars_script_intern(A) :-
	(
	 number(A)
	->
	 (
      % it's a ground fact
      get_var_name(A,NameA),
	  (problog:decision_fact(A,_) ->
        % it's a ground decision
        (problog:problog_control(check,internal_strategy) ->
          problog:get_fact_probability(A,P),
          format('@~w~n~12f~n~w~n',[NameA,P,1])
        ;
          format('@~w~n~12f~n~w~n',[NameA,0,1])
        )
      ;
        % it's a normal ProbLog fact
        problog:get_fact_probability(A,P),
        format('@~w~n~12f~n',[NameA,P])
      )
	 );     % it's somethin else, call the specialist
     % it's a non-ground or continuous fact
	 bdd_vars_script_intern2(A)
	).
bdd_vars_script_intern2(A) :-
	get_var_name(A,NameA),
	atom_chars(A,A_Chars),

	once(append(Part1,[95|Part2],A_Chars)),	% 95 = '_'
	number_chars(ID,Part1),

	(	     % let's check whether Part2 contains an 'l' (l=low)
         member(108,Part2)
	->
         ( % it does, so it's a continuous fact
	   problog:get_continuous_fact_parameters(ID,gaussian(Mu,Sigma)),
	   format('@~w~n0~n0~n~12f;~12f~n',[NameA,Mu,Sigma])
	 );
         (
	  number_chars(Grounding_ID,Part2),
      (problog:decision_fact(ID,_) ->
          % it's a non-ground decision
          (problog:problog_control(check,internal_strategy) ->
            problog:grounding_is_known(Goal,Grounding_ID),
            problog:dynamic_probability_fact_extract(Goal,P),
            format('@~w~n~12f~n~w~n',[NameA,P,1])
          ;
            format('@~w~n~12f~n~w~n',[NameA,0,1])
          )
        ;
          (problog:dynamic_probability_fact(ID) ->
              problog:grounding_is_known(Goal,Grounding_ID),
              problog:dynamic_probability_fact_extract(Goal,P)
          ;
              problog:get_fact_probability(ID,P)
          ),
          format('@~w~n~12f~n',[NameA,P])
        )
	 )
	).

%%%%%%%%%%%%%%%%%%%%%%%%
% find top level symbol for script
%%%%%%%%%%%%%%%%%%%%%%%%

% special cases: variable-free formulae
bdd_pt(Trie, false) :-
	empty_ptree(Trie),
	!,
	retractall(c_num(_)),
	assertz(c_num(2)).
bdd_pt(Trie, true) :-
	trie_check_entry(Trie, [true], _),
	!,
	retractall(c_num(_)),
	assertz(c_num(2)).

% general case: transform trie to nested tree structure for compression
bdd_pt(Trie, CT) :-
	trie_to_tree(Trie, Tree),
	once(compress_pt(Tree, CT)).

trie_to_tree(Trie, Tree) :-
	findall(Path, trie_path(Trie, Path), Paths),
	add_trees(Paths, [], Tree).

add_trees([], Tree, Tree).
add_trees([List|Paths], Tree0, Tree) :-
	ins_pt(List, Tree0, TreeI),
	add_trees(Paths, TreeI, Tree).

% default: prune if adding prefix of known proof(s)
ins_pt([], _T, []) :- !.
% alternative: keep extensions of prefix
% ins_pt([],T,T) :- !.
ins_pt([A|B], [s(A1, AT)|OldT], NewT) :-
	compare(Comp, A1, A),
  (Comp == = ->
    (AT == [] ->
      NewT=[s(A1, AT)|OldT]
    ;
      NewT = [s(A1, NewAT)|OldT],
      ins_pt(B, AT, NewAT))
  ;
    Comp == > ->
    NewT = [s(A1, AT)|Tree],
    ins_pt([A|B], OldT, Tree)
	;
    NewT = [s(A, BTree), s(A1, AT)|OldT],
    ins_pt(B, [], BTree)
	).
ins_pt([A|B], [], [s(A, NewAT)]) :-
	ins_pt(B, [], NewAT).

%%%%%%%%%%%%
% BDD compression: alternates and- and or-levels to build BDD bottom-up
% each sub-BDD will be either a conjunction of a one-node BDD with some BDD or a disjunction of BDDs
% uses the internal database to temporarily store a map of components
%%%%%%%%%%%%

% T is completely compressed and contains single variable
% i.e. T of form x12 or ~x34
compress_pt(T, TT) :-
	atom(T),
	test_var_name(T),
	!,
	get_next_name(TT),
	assertz(compression(TT, [T])).
% T is completely compressed and contains subtrees
% i.e. T of form 'L56'
compress_pt(T, T) :-
	atom(T).
% T not yet compressed
% i.e. T is a tree-term (nested list & s/2 structure)
% -> execute one layer of compression, then check again
compress_pt(T, CT) :-
	\+ atom(T),
	and_or_compression(T, IT),
	compress_pt(IT, CT).

% transform tree-term T into tree-term CT where last two layers have been processed
% i.e. introduce names for subparts (-> Map) and replace (all occurrenes of) subparts by this names
and_or_compression(T, CT) :-
	and_comp(T, AT),
	or_comp(AT, CT).

% replace leaves that are single child by variable representing father-AND-child
and_comp(T, AT) :-
	all_leaves_pt(T, Leaves),
	compression_mapping(Leaves, Map),
	replace_pt(T, Map, AT).

% replace list of siblings by variable representing their disjunction
or_comp(T, AT) :-
	all_leaflists_pt(T, Leaves),
	compression_mapping(Leaves, Map),
	replace_pt(T, Map, AT).

all_leaves_pt(T, L) :-
	all(X, some_leaf_pt(T, X), L).

some_leaf_pt([s(A, [])|_], s(A,[])).
some_leaf_pt([s(A, L)|_], s(A, L)) :-
	 not_or_atom(L).
some_leaf_pt([s(_, L)|_], X) :-
	some_leaf_pt(L, X).
some_leaf_pt([_|L],X) :-
	some_leaf_pt(L,X).

all_leaflists_pt(L, [L]) :-
	atomlist(L), !.
all_leaflists_pt(T, L) :-
	all(X,some_leaflist_pt(T, X), L), !.
all_leaflists_pt(_, []).

some_leaflist_pt([s(_, L)|_], L) :-
	atomlist(L).
some_leaflist_pt([s(_, L)|_], X) :-
	some_leaflist_pt(L, X).
some_leaflist_pt([_|L], X) :-
	some_leaflist_pt(L, X).

not_or_atom(T) :-
	(
	    T = not(T0)
	->
	    atom(T0);
	    atom(T)
	).

atomlist([]).
atomlist([A|B]) :-
  not_or_atom(A),
	atomlist(B).

% for each subtree that will be compressed, add its name
% only introduce 'L'-based names when subtree composes elements, store these in compression/2 for printing the script
compression_mapping([], []).
compression_mapping([First|B], [N-First|BB]) :-
	(
	    First = s(A0, [])          % subtree is literal -> use variable's name x17 from map (add ~ for negative case)
	->
	(
	    A0 = not(A)
	->
	    (
      		recorded(map, m(A, Tmp), _), %check
		atomic_concat(['~', Tmp], N)
	    );
    	    recorded(map, m(A0, N), _) %check
	)
	;
	    (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], 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
	    get_next_name(N),
	    assertz(compression(N, First)))
	),
	compression_mapping(B, BB).



% replace_pt(+T,+Map,-NT)
% given the tree-term T and the Map of Name-Subtree entries, replace each occurence of Subtree in T with Name -> result NT
replace_pt(T, [], T).
replace_pt([], _, []).
replace_pt(L, M, R) :-
	atomlist(L),
	member(R-L, M),
	!.
replace_pt([L|LL], [M|MM], R) :-
	replace_pt_list([L|LL], [M|MM], R).

replace_pt_list([T|Tree], [M|Map], [C|Compr]) :-
	replace_pt_single(T, [M|Map], C),
	replace_pt_list(Tree, [M|Map], Compr).
replace_pt_list([], _, []).

replace_pt_single(s(A, T), [M|Map], Res) :-
	atomlist(T),
	member(Res-s(A, T), [M|Map]),
	!.
replace_pt_single(s(A, T), [M|Map], s(A, Res)) :-
	atomlist(T),
	member(Res-T, [M|Map]),
	!.
replace_pt_single(s(A, T), [M|Map], Res) :-
	member(Res-s(A, T), [M|Map]),
	!.
replace_pt_single(s(A, T), [M|Map], s(A, TT)) :-
	!,
	replace_pt_list(T, [M|Map], TT).
replace_pt_single(A, _, A) :-
	 not_or_atom(A).

%%%%%%%%%%%%
% output for script
% input argument is compressed tree, i.e. true/false or name assigned in last compression step
%%%%%%%%%%%%
output_compressed_script(false) :-
	!,
	format('L1 = FALSE~nL1~n', []).
output_compressed_script(true) :-
	!,
	format('L1 = TRUE~nL1~n', []).
% for each name-subtree pair, write corresponding line to script, e.g. L17 = x4 * L16
% stop after writing definition of root (last entry in compression/2), add it's name to mark end of script
output_compressed_script(T) :-
	once(retract(compression(Short, Long))),
	(T = Short ->
	    format('~w = ', [Short]),
	    format_compression_script(Long),
	    format('~w~n', [Short])
	;
	    format('~w = ', [Short]),
	    format_compression_script(Long),
	    output_compressed_script(T)).

format_compression_script(s(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]) :-
	format('~w + ', [A]),
	format_compression_script([B|C]).

%%%%%%%%%%%%%%%%%%%%%%%%
% auxiliaries for translation to BDD
%%%%%%%%%%%%%%%%%%%%%%%%

% prefix the current counter with "L"
get_next_name(Name) :-
	retract(c_num(N)),
	NN is N + 1,
	assertz(c_num(NN)),
	atomic_concat('L', N, Name).

% create BDD-var as fact id prefixed by x
% learning.yap relies on this format!
% when changing, also adapt test_var_name/1 below
get_var_name(true, 'TRUE') :-!.
get_var_name(false, 'FALSE') :-!.
get_var_name(A, NameA) :-
	atomic_concat([x, 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).
test_var_name(T) :-
	atomic_concat('~x', _, T).


% Theo debuging additions

print_ptree(Trie):-
  trie_print(Trie).

statistics_ptree:-
  trie_stats(Memory,Tries,Entries,Nodes),
  write('--------------------------------'),nl,
  write('Memory: '),write(Memory),nl,
  write('Tries: '), write(Tries),nl,
  write('Entries: '), write(Entries),nl,
  write('Nodes: '), write(Nodes),nl,
  write('--------------------------------'),nl.


:- dynamic(nested_ptree_printed/1).

print_nested_ptree(Trie):-
  retractall(nested_ptree_printed(_)),
  print_nested_ptree(Trie, 0, '  '),
  retractall(nested_ptree_printed(_)).
print_nested_ptree(Trie, _, _):-
  nested_ptree_printed(Trie), !.
print_nested_ptree(Trie, Level, Space):-
  spacy_print(begin(t(Trie)), Level, Space),
  fail.
print_nested_ptree(Trie, Level, Space):-
  assertz(nested_ptree_printed(Trie)),
  trie_path(Trie, Path),
  NewLevel is Level + 1,
  spacy_print(Path, NewLevel, Space),
  (member(t(Hash), Path); member(not(t(Hash)), Path)),
  problog:problog_chktabled(Hash, SubTrie),
  NewLevel2 is NewLevel + 1,
  print_nested_ptree(SubTrie, NewLevel2, Space),
  fail.
print_nested_ptree(Trie, Level, Space):-
  spacy_print(end(t(Trie)), Level, Space).

spacy_print(Msg, 0, _):-
  write(Msg), nl, !.
spacy_print(Msg, Level, Space):-
  Level > 0,
  write(Space),
  NewLevel is Level - 1,
  spacy_print(Msg, NewLevel, Space).

% Theo Naive method works with Nested Trie to BDD Script

:- dynamic(get_used_vars/2).
:- dynamic(generated_trie/2).
:- dynamic(next_intermediate_step/1).

%
% This needs to be modified
% Include nasty code of temporary file usage
% also it is OS depended (requires the cat utility)
%

nested_ptree_to_BDD_script(Trie, BDDFileName, VarFileName):-
  tmpnam(TmpFile1),
  tmpnam(TmpFile2),
  open(TmpFile1, 'write', BDDS),
  (generate_BDD_from_trie(Trie, Inter, BDDS) ->
    next_intermediate_step(TMP), InterCNT is TMP - 1,
    write(BDDS, Inter), nl(BDDS),
    close(BDDS),
    (get_used_vars(Vars, VarCNT);VarCNT = 0),
    open(TmpFile2, 'write', HEADERS),
    write(HEADERS, '@BDD1'), nl(HEADERS),
    write(HEADERS, VarCNT), nl(HEADERS),
    write(HEADERS, 0), nl(HEADERS),
    write(HEADERS, InterCNT), nl(HEADERS),
    close(HEADERS),
    atomic_concat(['cat ', TmpFile2, ' ', TmpFile1, ' > ', BDDFileName], CMD),
    shell(CMD),
    delete_file(TmpFile1),
    delete_file(TmpFile2),
    open(VarFileName, 'write', VarStream),
    bddvars_to_script(Vars, VarStream),
    close(VarStream),
    cleanup_BDD_generation
  ;
    close(BDDS),
    (delete_file(TmpFile1);true),
    (delete_file(TmpFile2);true),
    cleanup_BDD_generation,
    fail
  ).

cleanup_BDD_generation:-
  retractall(get_used_vars(_, _)),
  retractall(generated_trie(_, _)),
  retractall(next_intermediate_step(_)).

generate_BDD_from_trie(Trie, TrieInter, Stream):-
  empty_ptree(Trie), !,
  get_next_intermediate_step(TrieInter),
  write(Stream, TrieInter), write(Stream, ' = FALSE'), nl(Stream), !.
generate_BDD_from_trie(Trie, TrieInter, _Stream):-
  clause(generated_trie(STrie, TrieInter), true),
  STrie = Trie, !.
generate_BDD_from_trie(Trie, TrieInter, Stream):-
  findall(LineInter, (
    trie_path(Trie, L),
    generate_line(L, LineTerms, LineInter, Stream),
    write_bdd_line(LineTerms, LineInter, '*', Stream)
  ), OrLineTerms),
  (OrLineTerms = [Inter|[]] ->
    TrieInter = Inter
  ;
    get_next_intermediate_step(TrieInter),
    write_bdd_line(OrLineTerms, TrieInter, '+', Stream)
  ),
  assertz(generated_trie(Trie, TrieInter)).

write_bdd_line([], _LineInter, _Operator, _Stream):-!.
write_bdd_line(LineTerms, LineInter, Operator, Stream):-
  write(Stream, LineInter), write(Stream, '='),
  write_bdd_lineterm(LineTerms, Operator, Stream).

write_bdd_lineterm([LineTerm|[]], _Operator, Stream):-
  write(Stream, LineTerm), nl(Stream), !.
write_bdd_lineterm([LineTerm|LineTerms], Operator, Stream):-
  write(Stream, LineTerm), write(Stream, Operator),
  write_bdd_lineterm(LineTerms, Operator, Stream).

generate_line([], [], Inter, _Stream):-
  !, get_next_intermediate_step(Inter).
generate_line([neg(t(Hash))|L], [TrieInter|T] , Inter, Stream):-
  !, problog:problog_chktabled(Hash, Trie),
  generate_BDD_from_trie(Trie, TrieInterTmp, Stream),
  atomic_concat(['~', TrieInterTmp], TrieInter),
  generate_line(L, T, Inter, Stream).
generate_line([t(Hash)|L], [TrieInter|T] , Inter, Stream):-
  !, problog:problog_chktabled(Hash, Trie),
  generate_BDD_from_trie(Trie, TrieInter, Stream),
  generate_line(L, T, Inter, Stream).
generate_line([V|L], [BDDV|T], Inter, Stream):-
  make_bdd_var(V, BDDV),
  generate_line(L, T, Inter, Stream).

%
% Currently it is dublicate with bdd_vars_script predicate
% finally should be merged
%

bddvars_to_script([], _Stream):-!.
bddvars_to_script([H|T], Stream):-
  (number(H) ->
    CurVar = H
  ;
    atom_chars(H, H_Chars),
    % 95 = '_'
    append(Part1, [95|Part2], H_Chars),
    number_chars(CurVar, Part1),
    number_chars(Grounding_ID, Part2)
  ),
  (problog:dynamic_probability_fact(CurVar) ->
    problog:grounding_is_known(Goal, Grounding_ID),
    problog:dynamic_probability_fact_extract(Goal, P)
  ;
    problog:get_fact_probability(CurVar, P)
  ),
  get_var_name(H, VarName),
  format(Stream, '@~w~n~12f~n', [VarName, P]),
  bddvars_to_script(T, Stream).

get_next_intermediate_step('L1'):-
  \+ clause(next_intermediate_step(_), _), !,
  assertz(next_intermediate_step(2)).
get_next_intermediate_step(Inter):-
  next_intermediate_step(InterStep),
  retract(next_intermediate_step(InterStep)),
  NextInterStep is InterStep + 1,
  assertz(next_intermediate_step(NextInterStep)),
  atomic_concat(['L', InterStep], Inter).

make_bdd_var('true', 'TRUE'):-!.
make_bdd_var('false', 'FALSE'):-!.
/*make_bdd_var(neg(V), NotVName):-
  !, make_bdd_var(not(V), NotVName).*/
make_bdd_var(not(V), NotVName):-
  !,
  get_var_name(V, VName),
  atomic_concat(['~', VName], NotVName),
  add_to_vars(V).
make_bdd_var(V, VName):-
  get_var_name(V, VName),
  add_to_vars(V).

add_to_vars(V):-
  clause(get_used_vars(Vars, _Cnt), true),
  memberchk(V, Vars),!.
add_to_vars(V):-
  clause(get_used_vars(Vars, Cnt), true), !,
  retract(get_used_vars(Vars, Cnt)),
  NewCnt is Cnt + 1,
  assertz(get_used_vars([V|Vars], NewCnt)).
add_to_vars(V):-
  assertz(get_used_vars([V], 1)).


%%%%%%%%%%%%%%% depth breadth builtin support %%%%%%%%%%%%%%%%%
%%%
%%% Pending:
%%%          1) Replace term in trie, written in C level
%%%         *2) Support for false, true and 1 var
%%%          3) Decide if it is necessary to propagete loop from child
%%%          4) Possible memory leak with [true] (go(0))
%%%         *5) Handle correctly the trie_replace when not(false), not(true)
%%%          6) Compare sort with a good insert sort
%%%          7) Have a look to the write to file predicates
%%%


variables_in_dbtrie(Trie, []):-
  empty_ptree(Trie), !.
variables_in_dbtrie(Trie, L):-
  all(V, variable_in_dbtrie(Trie,V), L).

variable_in_dbtrie(Trie, V):-
  trie_traverse(Trie, R),
  trie_get_entry(R, L),
  get_next_variable(NV, L),
  get_variable(NV, V).

get_next_variable(V, depth(L, _S)):-
  member(V, L),
  \+ is_label(V).
get_next_variable(V, breadth(L, _S)):-
  member(V, L),
  \+ is_label(V).
get_next_variable(V, L):-
  member(V, L),
  \+ is_label(V),
  \+ isnestedtrie(V).

get_variable(not(V), R):-
  !, get_variable(V, R).
get_variable(R, R).


  %trie_get_depth_breadth_reduction_opt_level_count(1, CNT1),
  %trie_get_depth_breadth_reduction_opt_level_count(2, CNT2),
  %trie_get_depth_breadth_reduction_opt_level_count(3, CNT3),
  %writeln([CNT1, CNT2, CNT3]),
  %trie_print(B),

trie_to_bdd_trie(A, B, OutputFile, OptimizationLevel, FileParam):-
  trie_to_depth_breadth_trie(A, B, LL, OptimizationLevel),
  (is_label(LL) ->
    atomic_concat('L', InterStep, LL),
    retractall(deref(_,_)),
    (problog_flag(deref_terms, true) ->
      asserta(deref(LL,no)),
      mark_for_deref(B),
      V = 3
    ;
      V = 1
    ),
    variables_in_dbtrie(B, Edges), %not the most efficient solution
    length(Edges, VarCNT),         %this 2 should be changed
    tell(FileParam),
    bdd_vars_script(Edges),
    told,
    tell(OutputFile),
    write('@BDD'), write(V), nl,
    write(VarCNT), nl,
    write(0), nl,
    write(InterStep), nl,
    trie_write(B, LL),
    write(LL), nl,
    told
  ;
    (is_state(LL) ->
      Edges = []
    ;
      Edges = [LL]
    ),
    tell(FileParam),
    bdd_vars_script(Edges),
    told,
    tell(OutputFile),
    write('@BDD1'), nl,
    write(1), nl,
    write(0), nl,
    write(1), nl,
    (LL = not(ID) ->
      get_var_name(ID, NLL),
      write('L1 = ~'), write(NLL),nl
    ;
      get_var_name(LL, NLL),
      write('L1 = '), write(NLL),nl
    ),
    write('L1'), nl,
    told
  ).

is_state(true).
is_state(false).

nested_trie_to_bdd_trie(A, B, OutputFile, OptimizationLevel, FileParam):-
  trie_nested_to_depth_breadth_trie(A, B, LL, OptimizationLevel, problog:problog_chktabled),
  (is_label(LL) ->
    retractall(deref(_,_)),
    (problog_flag(deref_terms, true) ->
      asserta(deref(LL,no)),
      mark_for_deref(B),
      V = 3
    ;
      V = 1
    ),
    variables_in_dbtrie(B, Edges), %not the most efficient solution
    length(Edges, VarCNT),         %this 2 should be changed
    tell(FileParam),
    bdd_vars_script(Edges),
    told,

    tell(OutputFile),
    write('@BDD'), write(V), nl,
    write(VarCNT), nl,
    write(0), nl,
    (LL = not(NegL)->
      atomic_concat('L', NegStep, NegL),
      number_atom(NegStepN, NegStep),
      InterStep is NegStepN + 1,
      atomic_concat('L', InterStep, FL),
      write(InterStep), nl,
      trie_write(B, FL),
      write(FL), write(' = ~'), write(NegL), nl,
      write(FL), nl
    ;
      atomic_concat('L', InterStep, LL),
      write(InterStep), nl,
      trie_write(B, LL),
      write(LL), nl
    ),
    told
  ;
    (is_state(LL) ->
      Edges = []
    ;
      Edges = [LL]
    ),
    tell(FileParam),
    bdd_vars_script(Edges),
    told,
    tell(OutputFile),
    write('@BDD1'), nl,
    write(1), nl,
    write(0), nl,
    write(1), nl,
    get_var_name(LL, NLL),
    write('L1 = '),write(NLL),nl,
    write('L1'), nl,
    told
  ).


/*
  variables_in_dbtrie(B, Edges), %not the most efficient solution

  length(Edges, VarCNT),         %this 2 should be changed
  tell(FileParam),
  bdd_vars_script(Edges),
  told,
  (atomic_concat('L', InterStep, LL) ->
    tell(OutputFile),
    write('@BDD1'), nl,
    write(VarCNT), nl,
    write(0), nl,
    write(InterStep), nl,
    trie_write(B, LL),
    write(LL), nl,
    told
  ;
    tell(OutputFile),
    write('@BDD1'), nl,
    write(1), nl,
    write(0), nl,
    write(1), nl,
    fix(LL, NLL),
    write('L1 = '),write(NLL),nl,
    write('L1'), nl,
    told
  ).

fix(false, 'FALSE'):-!.
fix(true, 'TRUE'):-!.
fix(A, A).
*/

preprocess(Index, DepthBreadthTrie, OptimizationLevel, StartCount, FinalEndCount):-
  problog:problog_chktabled(Index, Trie), !,
  trie_dup(Trie, CopyTrie),
  initialise_ancestors(Ancestors),
  make_nested_trie_base_cases(CopyTrie, t(Index), DepthBreadthTrie, OptimizationLevel, StartCount, EndCount, Ancestors),
  trie_close(CopyTrie),
  Next is Index + 1,
  preprocess(Next, DepthBreadthTrie, OptimizationLevel, EndCount, FinalEndCount).
preprocess(_, _, _, FinalEndCount, FinalEndCount).

make_nested_trie_base_cases(Trie, t(ID), DepthBreadthTrie, OptimizationLevel, StartCount, FinalEndCount, Ancestors):-
  trie_to_depth_breadth_trie(Trie, DepthBreadthTrie, Label, OptimizationLevel, StartCount, EndCount),
  (Label \= t(_) ->
    FinalEndCount = EndCount,
    problog:problog_chktabled(ID, RTrie),!,
    get_set_trie_from_id(t(ID), Label, RTrie, Ancestors, _, Ancestors)
  ;
    trie_get_depth_breadth_reduction_entry(NestedEntry),
    trie_replace_entry(Trie, NestedEntry, Label, false),
    add_to_ancestors(Label, Ancestors, NewAncestors),
    make_nested_trie_base_cases(Trie, t(ID), DepthBreadthTrie, OptimizationLevel, EndCount, FinalEndCount, NewAncestors)
  ).

trie_nested_to_depth_breadth_trie(Trie, DepthBreadthTrie, FinalLabel, OptimizationLevel, Module:GetTriePredicate):-
  integer(OptimizationLevel),
  trie_open(DepthBreadthTrie),
  (problog_flag(trie_preprocess, true) ->
    preprocess(1, DepthBreadthTrie, OptimizationLevel, 0, StartCount)
  ;
    StartCount = 0
  ),
  initialise_ancestors(Ancestors),
  initialise_ancestors(Childs),
  trie_nested_to_db_trie(Trie, DepthBreadthTrie, FinalLabel, OptimizationLevel, StartCount, _, Module:GetTriePredicate, Ancestors, _, _, Childs),
  eraseall(problog_trie_table).

trie_nested_to_db_trie(Trie, DepthBreadthTrie, FinalLabel, OptimizationLevel, StartCount, FinalEndCount, Module:GetTriePredicate, AncestorList, ContainsLoop, Childs, ChildsAcc):-
  trie_dup(Trie, CopyTrie),
  nested_trie_to_db_trie(CopyTrie, DepthBreadthTrie, FinalLabel, OptimizationLevel, StartCount, FinalEndCount, Module:GetTriePredicate, AncestorList, ContainsLoop, Childs, ChildsAcc),
  trie_close(CopyTrie).

nested_trie_to_db_trie(Trie, DepthBreadthTrie, FinalLabel, OptimizationLevel, StartCount, FinalEndCount, Module:GetTriePredicate, Ancestors, ContainsLoop, Childs, ChildsAcc):-
  trie_to_depth_breadth_trie(Trie, DepthBreadthTrie, Label, OptimizationLevel, StartCount, EndCount),
  (Label \= t(_) ->
    (var(ContainsLoop) ->
      ContainsLoop = false
    ;
      true
    ),
    FinalLabel = Label,
    FinalEndCount = EndCount,
    Childs = ChildsAcc
  ;
    trie_get_depth_breadth_reduction_entry(NestedEntry),
    trie_get_entry(NestedEntry, Proof),
    (loopcheck(Proof, Ancestors) -> % to fix
      ContainsLoop = true,
      NewLabel = false,
      NewEndCount = EndCount
    ;
%       writeln(in(Label)),
      get_set_trie_from_id(Label, NewLabel, NestedTrie, Ancestors, Module:GetTriePredicate, ChildChilds),
%       writeln(out(NewLabel)),
      (nonvar(NewLabel) ->
        NewEndCount = EndCount
      ;
        add_to_ancestors(Label, Ancestors, CurAncestors),
        initialise_ancestors(ChildChildsAcc),
        trie_nested_to_db_trie(NestedTrie, DepthBreadthTrie, NewLabel, OptimizationLevel, EndCount, NewEndCount, Module:GetTriePredicate, CurAncestors, CheckLoop, ChildChilds, ChildChildsAcc),
        (CheckLoop ->
          StoreAncestors = CurAncestors
        ;
          initialise_ancestors(StoreAncestors)
        ),
        get_set_trie_from_id(Label, NewLabel, NestedTrie, StoreAncestors, Module:GetTriePredicate, ChildChilds)
      )
    ),
    trie_replace_entry(Trie, NestedEntry, Label, NewLabel),
    (problog_flag(refine_anclst, true) ->
      combine_ancestors(ChildsAcc, ChildChilds, AllChilds),
      add_to_ancestors(Label, AllChilds, FAllChilds)
    ;
      initialise_ancestors(FAllChilds)
    ),
    nested_trie_to_db_trie(Trie, DepthBreadthTrie, FinalLabel, OptimizationLevel, NewEndCount, FinalEndCount, Module:GetTriePredicate, Ancestors, ContainsLoop, Childs, FAllChilds)
  ).

initialise_ancestors(Ancestors):-
  (problog_flag(anclst_represent, list) ->
    Ancestors = []
  ;
    Ancestors = 0
  ).

add_to_ancestors(t(ID), Ancestors, NewAncestors):-
  (problog_flag(anclst_represent, list) ->
    ord_union(Ancestors, [t(ID)], NewAncestors)
  ;
    NewAncestors is Ancestors \/ (1 << (ID - 1))
  ).

combine_ancestors(Ancestors, AddAncestors, Ancestors):-
  var(AddAncestors), !.
combine_ancestors(Ancestors, AddAncestors, AllAncestors):-
  (problog_flag(anclst_represent, list) ->
    ord_union(Ancestors, AddAncestors, AllAncestors)
  ;
    AllAncestors is Ancestors \/ AddAncestors
  ).


my_trie_print(T):-
  trie_traverse(T, R),
  trie_get_entry(R, E),
  writeln(E),
  fail.
my_trie_print(_T).

loopcheck(Proof, AncestorList):-
  contains_nested_trie(Proof, ID),
%   memberchk(t(ID), AncestorList).
%   writeln(chk_id(ID, AncestorList)),
  chk_id(ID, AncestorList), !.
chk_id(ID, AncestorList):-
  (problog_flag(anclst_represent, list) ->
    memberchk(t(ID), AncestorList)
  ;
    (AncestorList /\ (1 << (ID - 1))) > 0
  ).
chk_id(ID, AncestorList):-
  get_negated_synonym_id(ID, NegID),
%   writeln(get_negated_synonym_id(ID, NegID)),
  (problog_flag(anclst_represent, list) ->
    memberchk(t(NegID), AncestorList)
  ;
    (AncestorList /\ (1 << (NegID - 1))) > 0
  ).
% % can also check for a proof with A, not(A)
%
% get_negated_synonym_id(ID, NegID):-
%   tabling:problog_tabling_get_negated_from_id(ID, Ref),
%   recorded(problog_table, store(_, NegID, _, _, _), Ref).

get_negated_synonym_id(ID, NegID):-
  tabling:has_synonyms,
  recorded(problog_table, store(Pred, ID, _, _, _), _),
  Pred =.. [Name0|Args],
  atomic_concat(problog_, Name1, Name0),
  atomic_concat(Name, '_original', Name1),
  (recorded(problog_table_synonyms, negated(Name, NotName1), _);
   recorded(problog_table_synonyms, negated(NotName1, Name), _)),
  atomic_concat([problog_, NotName1, '_original'], NotName),
  NegPred =.. [NotName|Args],
  recorded(problog_table, store(NegPred, NegID, _, _, _), _).


is_nested_trie(T):-
  nonvar(T),
  is_nested_trie(T, _).
is_nested_trie(NT, ID):-
  nonvar(NT),
  NT = not(T), !,
  is_nested_trie(T, ID).
is_nested_trie(t(ID), ID).

contains_nested_trie(L, ID):-
  member(T, L),
  is_nested_trie(T, ID).


subset([],_):-!.
subset(_,[]):-!,fail.
subset([H|T1], [H|T2]):-
  subset(T1, T2).
subset([H1|T1], [H2|T2]):-
  compare(>, H1, H2),
  subset([H1|T1],T2).

get_set_trie_from_id(t(ID), L, T, AncestorList, _GetTriePredicate, Childs):-
  nonvar(ID),
  atomic(L),
  nonvar(AncestorList),
  nonvar(T), !,
  (problog_flag(refine_anclst, true) ->
    (problog_flag(anclst_represent, list) ->
      ord_intersection(AncestorList, Childs, RefinedAncestorList)
    ;
      RefinedAncestorList is AncestorList /\ Childs
    )
  ;
    RefinedAncestorList = AncestorList
  ),
  recordz(problog_trie_table, get_step_from_id(ID, L, T, RefinedAncestorList, Childs), _).
get_set_trie_from_id(t(ID), L, T, SuperSetAncestorList, _GetTriePredicate, Childs):-
%   (clause(theo,_) ->writeln(get_set_trie_from_id(t(ID), L, T, SuperSetAncestorList, _GetTriePredicate, Childs));true),
  recorded(problog_trie_table, get_step_from_id(ID, L, T, AncestorList, StoredChilds), _),
  (problog_flag(refine_anclst, true) ->
    StoredChilds = Childs
  ;
    true
  ),
  (problog_flag(subset_check, true) ->
    (problog_flag(anclst_represent, list) ->
      subset(AncestorList, SuperSetAncestorList)
    ;
      AncestorList is AncestorList /\ SuperSetAncestorList
%       writeln(hi)
    )
  ;
    AncestorList = SuperSetAncestorList
  ), !.
get_set_trie_from_id(t(ID), _L, T, _SuperSetAncestorList, _GetTriePredicate, _):-
  recorded(problog_trie_table, get_step_from_id(ID, _, T, _AncestorList, _Childs), _), !.
get_set_trie_from_id(t(ID), _L, T, _AncestorList, Module:GetTriePredicate, _):-
  Goal =.. [GetTriePredicate, ID, T],
  call(Module:Goal).

trie_replace_entry(_Trie, Entry, _E, false):-
  !, trie_remove_entry(Entry).
trie_replace_entry(Trie, Entry, E, true):-
  !, trie_get_entry(Entry, Proof),
  delete(Proof, E, NewProof),
  (NewProof = [] ->
    trie_delete(Trie),
    trie_put_entry(Trie, [true], _)
  ;
    trie_remove_entry(Entry),
    trie_put_entry(Trie, NewProof, _)
  ).
/*trie_replace_entry(Trie, Entry, E, R):-
  trie_get_entry(Entry, List),
  replace_in_list(List, NewProof, E, R),
  trie_remove_entry(Entry),
  trie_put_entry(Trie, NewProof, _).*/
/*trie_replace_entry(Trie, _Entry, E, R):-
  trie_replace_term2(Trie, E, R).*/
trie_replace_entry(Trie, _Entry, t(ID), R):-
  trie_replace_nested_trie(Trie, ID, R).




trie_replace_term2(Trie, OldTerm, NewTerm):-
  trie_dup(Trie, A),
  %writeln(trie),
  %my_trie_print(A),
  trie_delete(Trie),
  trie_replace_term(A, Trie, OldTerm, NewTerm),
  trie_close(A).

trie_delete(Trie):-
  trie_traverse(Trie, R),
  trie_remove_entry(R),
  fail.
trie_delete(_Trie).

trie_replace_term(Trie, NewTrie, OldTerm, NewTerm):-
  trie_traverse(Trie, R),
  trie_get_entry(R, L),
  replace_in_list(L, NL, OldTerm, NewTerm),
  trie_put_entry(NewTrie, NL, _),
  fail.
trie_replace_term(_Trie, _NewTrie, _OldTerm, _NewTerm).

replace_in_list([],[],_,_):-!.
replace_in_list([H|T], [N|NT], H, N):-
  !, replace_in_list(T, NT, H, N).
replace_in_list([H|T], [NH|NT], R, N):-
  functor(H, _, 1), !,
  replace_in_functor(H, NH, R, N),
  replace_in_list(T, NT, R, N).
replace_in_list([H|T], [H|NT], R, N):-
  replace_in_list(T, NT, R, N).
replace_in_functor(F, NF, T, R):-
  F =.. L,
  replace_in_list(L, NL, T, R),
  NF =.. NL.



trie_write(T, MAXL):-
  atomic_concat('L', MAXLA, MAXL),
  atom_number(MAXLA, MAXLN),
  trie_traverse(T, R),
  trie_get_entry(R, L),
  %write(user_output, L),nl(user_output),
  (dnfbddformat(L, MAXLN) ->
    true
  ;
    write(user_error, warning(L, not_processed)), nl(user_error)
  ),
  fail.
trie_write(_, _).

dnfbddformat(depth(T, L), MAXL):-
  atomic_concat('L', LA, L),
  atom_number(LA, LN),
  MAXL >= LN,
  seperate(T, Li, V),
  %sort(Li, SL),
  %reverse(SL, RSL),
  append(Li, V, R),
  bddlineformat(R, L, ' * '),
  forall(deref(I, L), (
    atomic_concat('L', D, I),
    write('D'), write(D), nl
    )).
dnfbddformat(breadth(T, L), MAXL):-
  atomic_concat('L', LA, L),
  atom_number(LA, LN),
  MAXL >= LN,
  seperate(T, Li, V),
  %sort(Li, SL),
  %reverse(SL, RSL),
  append(V, Li, R),
  bddlineformat(R, L, ' + '),
  forall(deref(I, L), (
    atomic_concat('L', D, I),
    write('D'), write(D), nl
    )).


bddlineformat([not(H)|T], O):-
  write('~'), !,
  bddlineformat([H|T], O).
bddlineformat([H], _O):-
  (is_label(H) ->
    Var = H
  ;
    get_var_name(H, Var)
  ),
  write(Var), nl, !.
bddlineformat([H|T], O):-
  (is_label(H) ->
    Var = H
  ;
    get_var_name(H, Var)
  ),
  write(Var), write(O),
  bddlineformat(T, O).

/*
bddlineformat([not(H)], O):-
  !, write('~'),
  bddlineformat([H], O).
bddlineformat([H], _O):-!,
  (is_label(H) ->
    VarName = H
  ;
    get_var_name(H, VarName)
  ),
  write(VarName), nl.
bddlineformat([not(H)|T], O):-
  !, write('~'),
  bddlineformat([H|T], O).
bddlineformat([H|T], O):-
  (is_label(H) ->
    VarName = H
  ;
    get_var_name(H, VarName)
  ),
  write(VarName), write(O),
  bddlineformat(T, O).*/

bddlineformat(T, L, O):-
  (is_label(L) ->
    write(L), write(' = '),
    bddlineformat(T, O)
  ;
    write(user_output,bdd_script_error([L,T,O])),nl(user_output)
  ).

is_label(not(L)):-
  !, is_label(L).
is_label(Label):-
  atom(Label),
  atomic_concat('L', _, Label).

isnestedtrie(not(T)):-
  !, isnestedtrie(T).
isnestedtrie(t(_T)).

seperate([], [], []).
seperate([H|T], [H|Labels], Vars):-
  is_label(H), !,
  seperate(T, Labels, Vars).
seperate([H|T], Labels, [H|Vars]):-
  seperate(T, Labels, Vars).


ptree_decomposition(Trie, BDDFileName, VarFileName) :-
  tmpnam(TmpFile1),
  tmpnam(TmpFile2),
  nb_setval(next_inter_step, 1),
  variables_in_dbtrie(Trie, T),
  length(T, VarCnt),
  tell(VarFileName),
  bdd_vars_script(T),
  told,
  tell(TmpFile1),
  decompose_trie(Trie, T, L),
  (is_label(L)->
    atomic_concat('L', LCnt, L),
    write(L),nl
  ;
    LCnt = 1,
    write('L1 = '),
    (L == false ->
      write('FALSE')
    ;
      write(L)
    ), nl,
    write('L1'), nl
  ),
  told,
  tell(TmpFile2),
  write('@BDD1'),nl,
  write(VarCnt),nl,
  write('0'),nl,
  write(LCnt),nl,
  told,
  atomic_concat(['cat ', TmpFile2, ' ', TmpFile1, ' > ', BDDFileName], CMD),
  shell(CMD),
  delete_file(TmpFile1),
  delete_file(TmpFile2).

get_next_inter_step(I):-
  nb_getval(next_inter_step, I),
  NI is I + 1,
  nb_setval(next_inter_step, NI).

decompose_trie(Trie, _, false):-
  empty_ptree(Trie), !.

decompose_trie(Trie, [H|[]], Var):-
  trie_usage(Trie, 1, _, _),
  get_var_name(H, VarA),
  trie_check_entry(Trie, [L], _R),
  (not(H) == L ->
    Var = not(VarA)
  ,
    Var = VarA
  ),
  !.

decompose_trie(Trie, _, 'TRUE'):-
  trie_check_entry(Trie, [true], _R),!.

decompose_trie(Trie, [H|_T], L3):-
  trie_open(TrieWith),
  trie_open(TrieWithNeg),
  trie_open(TrieWithOut),
  trie_seperate(Trie, H, TrieWith, TrieWithNeg, TrieWithOut),
  /*trie_print(Trie),
  dwriteln('-----------'),
  trie_print(TrieWith),
  dwriteln('-----------'),
  trie_print(TrieWithNeg),
  dwriteln('-----------'),
  trie_print(TrieWithOut),
  dwriteln('-----------'),*/

  variables_in_dbtrie(TrieWith, T1),
  variables_in_dbtrie(TrieWithNeg, T2),
  variables_in_dbtrie(TrieWithOut, T3),

  %dwriteln([T1, not(T2), T3]),

  decompose_trie(TrieWith, T1, LWith),
  trie_close(TrieWith),

  decompose_trie(TrieWithNeg, T2, LWithNeg),
  trie_close(TrieWithNeg),

  decompose_trie(TrieWithOut, T3, LWithOut),
  trie_close(TrieWithOut),

  get_var_name(H, Var),
  %dwriteln([Var, ' * ', LWith, ' + ~', Var, ' * ', LWithNeg, ' + ', LWithOut]),
  (LWith == false ->
    L1 = false
  ;
    (Var == 'TRUE' ->
      L1 = LWith
    ;
      (LWith == 'TRUE' ->
        L1 = Var
      ;
        get_next_inter_step(I),
        atomic_concat(['L', I], L1),
        atomic_concat([L1, ' = ', Var, '*', LWith], W1),
        write(W1), nl
      )
    )
  ),
  (LWithNeg == false ->
    L2 = false
  ;
    (Var == 'TRUE' ->
      L2 = false
    ;
      (LWithNeg == 'TRUE' ->
        atomic_concat(['~', Var], L2)
      ;
        get_next_inter_step(I2),
        atomic_concat(['L', I2], L2),
        atomic_concat([L2, ' = ~', Var, '*', LWithNeg], W2),
        write(W2), nl
      )
    )
  ),
  (one_true(L1, L2, LWithOut) ->
    L3 = 'TRUE'
  ;
    (all_false(L1, L2, LWithOut)->
      L3 = false
    ;
      (one_non_false(L1, L2, LWithOut, L3) ->
        true
      ;
        get_next_inter_step(I3),
        atomic_concat(['L', I3], L3),
        write(L3), write(' = '),
        non_false([L1,L2,LWithOut], [First|Rest]),
        write(First),
        forall(member(NonFalse, Rest), (write('+'), write(NonFalse))),
        nl
      )
    )
  ).

dwriteln(A):-
  write(user_error, A),nl(user_error),flush_output.


non_false([], []):-!.
non_false([H|T], [H|NT]):-
  H \== false,
  non_false(T, NT).
non_false([H|T], NT):-
  H == false,
  non_false(T, NT).

one_true('TRUE', _, _):-!.
one_true(_, 'TRUE', _):-!.
one_true(_, _, 'TRUE'):-!.

all_false(false,false,false).
one_non_false(L, false, false, L):-
  L \== false, !.
one_non_false(false, L, false, L):-
  L \== false, !.
one_non_false(false, false, L, L):-
  L \== false, !.

trie_seperate(Trie, Var, TrieWith, TrieWithNeg, TrieWithOut):-
  trie_traverse(Trie, R),
  trie_get_entry(R, Proof),
  (memberchk(Var, Proof) ->
    remove_from_list(Var, Proof, NProof),
    (NProof == [] ->
      trie_put_entry(TrieWith, [true], _)
    ;
      trie_put_entry(TrieWith, NProof, _)
    )
  ;
    (memberchk(not(Var), Proof) ->
      remove_from_list(not(Var), Proof, NProof),
      (NProof == [] ->
        trie_put_entry(TrieWithNeg, [true], _)
      ;
        trie_put_entry(TrieWithNeg, NProof, _)
      )
    ;
      trie_put_entry(TrieWithOut, Proof, _)
    )
  ),
  fail.
trie_seperate(_Trie, _Var, _TrieWith, _TrieWithNeg, _TrieWithOut).

remove_from_list(_E, [], []):-!.
remove_from_list(E, [E|T], NT):-
  !, remove_from_list(E, T, NT).
remove_from_list(E, [A|T], [A|NT]):-
  remove_from_list(E, T, NT).

ptree_db_trie_opt_performed(LVL1, LVL2, LVL3):-
  trie_get_depth_breadth_reduction_opt_level_count(1, LVL1),
  trie_get_depth_breadth_reduction_opt_level_count(2, LVL2),
  trie_get_depth_breadth_reduction_opt_level_count(3, LVL3).

:- dynamic(deref/2).

mark_for_deref(DB_Trie):-
  traverse_ptree_mode(OLD),
  traverse_ptree_mode(backward),
  mark_deref(DB_Trie),
  traverse_ptree_mode(OLD).

mark_deref(DB_Trie):-
  traverse_ptree(DB_Trie, DB_Term),
  (DB_Term = depth(List, Inter); DB_Term = breadth(List, Inter)),
  member(L, List),
  ((is_label(L), \+ deref(L, _)) ->
    asserta(deref(L, Inter))
  ;
    true
  ),
  fail.
mark_deref(_).

% end of Theo