%%% -*- Mode: Prolog; -*- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % $Date: 2011-01-16 19:24:10 +0100 (Sun, 16 Jan 2011) $ % $Revision: 5260 $ % % 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), [tmpnam/1]). :- use_module(library(ordsets), [ord_intersection/3, ord_union/3]). % load our own modules :- use_module(flags). :- use_module(utils). :- use_module(nestedtries, [nested_trie_to_depth_breadth_trie/4]). % 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(deref_terms, problog_flag_validate_boolean, 'deref BDD terms after last use', false), problog_define_flag(export_map_file, problog_flag_validate_boolean, 'activates export of a variable map file', false, output) )). %%%%%%%%%%%%%%%%%%%%%%%% % 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), open(TmpFile1, 'write', BDDS), ( generate_BDD_from_trie(Trie, Inter, BDDS) -> ( next_intermediate_step(TMP), InterCNT is TMP - 1, format(BDDS,'~q~n',[Inter]), close(BDDS), ( get_used_vars(Variables, VarCNT) -> true; VarCNT = 0 ), prefix_bdd_file_with_header(BDDFileName,VarCNT,InterCNT,TmpFile1), cleanup_BDD_generation );( close(BDDS), delete_file_silently(TmpFile1), 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), nested_trie_to_depth_breadth_trie(A, B, LL, OptimizationLevel), (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, simplify(LL, FLL), (FLL = not(_) -> write('L1 = ~') ; write('L1 = ') ), get_var_name(FLL, NLL), write(NLL),nl, write('L1'), nl, told ). ptree_decomposition_struct(Trie, BDDFileName, Variables) :- tmpnam(TmpFile1), 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, prefix_bdd_file_with_header(BDDFileName,VarCnt,LCnt,TmpFile1). %%%%%%%%%%%%%%%%%%%%%%%% % 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(Vars):- bdd_vars_script(Vars, Names), (problog_flag(export_map_file, true) -> problog_flag(map_file, MapFile), os:convert_filename_to_working_path(MapFile, MapFileName), flush_output, tell(MapFileName), problog:get_fact_list(Vars, Facts), writemap(Names, Facts), flush_output, told ; true ). writemap([],[]). writemap([Name|Names],[Fact|Facts]):- write(map(Name,Fact)),nl, writemap(Names, Facts). bdd_vars_script([], []). bdd_vars_script([not(A)|B], Names) :- !, bdd_vars_script([A|B], Names). bdd_vars_script([A|B], [NameA|Names]) :- bdd_vars_script_intern(A, NameA), bdd_vars_script(B, Names). bdd_vars_script_intern(A, NameA) :- (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, NameA) ). bdd_vars_script_intern2(A, NameA) :- get_var_name(A,NameA), atom_codes(A,A_Codes), once(append(Part1,[95|Part2],A_Codes)), % 95 = '_' number_codes(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_codes(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 simplify_list(List, SList):- findall(NEL, (member(El, List), simplify(El, NEL)), SList). simplify(not(false), true):- !. simplify(not(true), false):- !. simplify(not(not(A)), B):- !, simplify(A, B). simplify(A, A). simplify(not(false), true):- !. simplify(not(true), false):- !. simplify(not(not(A)), B):- !, simplify(A, B). simplify(A, A). get_var_name(true, 'TRUE'):- !. get_var_name(false, 'FALSE'):- !. get_var_name(Variable, Name):- atomic(Variable), !, atomic_concat([x, Variable], Name), (recorded(map, m(Variable, Name), _) -> true ; recorda(map, m(Variable, Name), _) ). get_var_name(not(A), NameA):- get_var_name(A, NameA). /* get_var_name(true, 'TRUE') :-!. get_var_name(false, 'FALSE') :-!. get_var_name(not(A), NameA):- !, get_var_name(A, NameA). 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). nested_ptree_to_BDD_script(Trie, BDDFileName, VarFileName):- tmpnam(TmpFile1), 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) -> true; VarCNT = 0 ), prefix_bdd_file_with_header(BDDFileName,VarCNT,InterCNT,TmpFile1), open(VarFileName, 'write', VarStream), bddvars_to_script(Vars, VarStream), close(VarStream), cleanup_BDD_generation ; close(BDDS), delete_file_silently(TmpFile1), 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([not(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_codes(H, H_Codes), % 95 = '_' append(Part1, [95|Part2], H_Codes), number_codes(CurVar, Part1), number_codes(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, []):- trie_check_entry(Trie, [true], _R), !. 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), nested_trie_to_depth_breadth_trie(A, B, LL, OptimizationLevel), simplify(LL, FLL), (is_label(FLL) -> retractall(deref(_,_)), (problog_flag(deref_terms, true) -> asserta(deref(FLL,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, (FLL = 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, FLL), write(InterStep), nl, trie_write(B, FLL), write(FLL), nl ), told ; (is_state(FLL) -> Edges = [] ; Edges = [FLL] ), tell(FileParam), simplify_list(Edges, SEdges), bdd_vars_script(SEdges), told, tell(OutputFile), write('@BDD1'), nl, write(1), nl, write(0), nl, write(1), nl, (FLL = not(_) -> write('L1 = ~') ; write('L1 = ') ), get_var_name(FLL, NLL), 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), 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, prefix_bdd_file_with_header(BDDFileName,VarCnt,LCnt,TmpFile1). 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, _, 'TRUE'):- trie_check_entry(Trie, [true], _R),!. 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, [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(_).