2055 lines
59 KiB
Prolog
2055 lines
59 KiB
Prolog
%%% -*- Mode: Prolog; -*-
|
|
|
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
%
|
|
% $Date: 2011-11-28 14:41:26 +0100 (Mon, 28 Nov 2011) $
|
|
% $Revision: 6764 $
|
|
%
|
|
% 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([false|T], Names):-
|
|
bdd_vars_script(T, Names).
|
|
bdd_vars_script([true|T], Names):-
|
|
bdd_vars_script(T, Names).
|
|
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])
|
|
;
|
|
dtproblog:initial_probability(P),
|
|
format('@~w~n~12f~n~w~n',[NameA,P,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])
|
|
;
|
|
dtproblog:initial_probability(P),
|
|
format('@~w~n~12f~n~w~n',[NameA,P,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(_).
|