1%%% -*- Mode: Prolog; -*- 2 3%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 4% 5% $Date: 2011-11-28 14:41:26 +0100 (Mon, 28 Nov 2011) $ 6% $Revision: 6764 $ 7% 8% This file is part of ProbLog 9% http://dtai.cs.kuleuven.be/problog 10% 11% ProbLog was developed at Katholieke Universiteit Leuven 12% 13% Copyright 2008, 2009, 2010 14% Katholieke Universiteit Leuven 15% 16% Main authors of this file: 17% Angelika Kimmig, Vitor Santos Costa,Bernd Gutmann, 18% Theofrastos Mantadelis, Guy Van den Broeck 19% 20%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 21% 22% Artistic License 2.0 23% 24% Copyright (c) 2000-2006, The Perl Foundation. 25% 26% Everyone is permitted to copy and distribute verbatim copies of this 27% license document, but changing it is not allowed. Preamble 28% 29% This license establishes the terms under which a given free software 30% Package may be copied, modified, distributed, and/or 31% redistributed. The intent is that the Copyright Holder maintains some 32% artistic control over the development of that Package while still 33% keeping the Package available as open source and free software. 34% 35% You are always permitted to make arrangements wholly outside of this 36% license directly with the Copyright Holder of a given Package. If the 37% terms of this license do not permit the full use that you propose to 38% make of the Package, you should contact the Copyright Holder and seek 39% a different licensing arrangement. Definitions 40% 41% "Copyright Holder" means the individual(s) or organization(s) named in 42% the copyright notice for the entire Package. 43% 44% "Contributor" means any party that has contributed code or other 45% material to the Package, in accordance with the Copyright Holder's 46% procedures. 47% 48% "You" and "your" means any person who would like to copy, distribute, 49% or modify the Package. 50% 51% "Package" means the collection of files distributed by the Copyright 52% Holder, and derivatives of that collection and/or of those files. A 53% given Package may consist of either the Standard Version, or a 54% Modified Version. 55% 56% "Distribute" means providing a copy of the Package or making it 57% accessible to anyone else, or in the case of a company or 58% organization, to others outside of your company or organization. 59% 60% "Distributor Fee" means any fee that you charge for Distributing this 61% Package or providing support for this Package to another party. It 62% does not mean licensing fees. 63% 64% "Standard Version" refers to the Package if it has not been modified, 65% or has been modified only in ways explicitly requested by the 66% Copyright Holder. 67% 68% "Modified Version" means the Package, if it has been changed, and such 69% changes were not explicitly requested by the Copyright Holder. 70% 71% "Original License" means this Artistic License as Distributed with the 72% Standard Version of the Package, in its current version or as it may 73% be modified by The Perl Foundation in the future. 74% 75% "Source" form means the source code, documentation source, and 76% configuration files for the Package. 77% 78% "Compiled" form means the compiled bytecode, object code, binary, or 79% any other form resulting from mechanical transformation or translation 80% of the Source form. 81% 82%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 83% 84% Permission for Use and Modification Without Distribution 85% 86% (1) You are permitted to use the Standard Version and create and use 87% Modified Versions for any purpose without restriction, provided that 88% you do not Distribute the Modified Version. 89% 90% Permissions for Redistribution of the Standard Version 91% 92% (2) You may Distribute verbatim copies of the Source form of the 93% Standard Version of this Package in any medium without restriction, 94% either gratis or for a Distributor Fee, provided that you duplicate 95% all of the original copyright notices and associated disclaimers. At 96% your discretion, such verbatim copies may or may not include a 97% Compiled form of the Package. 98% 99% (3) You may apply any bug fixes, portability changes, and other 100% modifications made available from the Copyright Holder. The resulting 101% Package will still be considered the Standard Version, and as such 102% will be subject to the Original License. 103% 104% Distribution of Modified Versions of the Package as Source 105% 106% (4) You may Distribute your Modified Version as Source (either gratis 107% or for a Distributor Fee, and with or without a Compiled form of the 108% Modified Version) provided that you clearly document how it differs 109% from the Standard Version, including, but not limited to, documenting 110% any non-standard features, executables, or modules, and provided that 111% you do at least ONE of the following: 112% 113% (a) make the Modified Version available to the Copyright Holder of the 114% Standard Version, under the Original License, so that the Copyright 115% Holder may include your modifications in the Standard Version. (b) 116% ensure that installation of your Modified Version does not prevent the 117% user installing or running the Standard Version. In addition, the 118% modified Version must bear a name that is different from the name of 119% the Standard Version. (c) allow anyone who receives a copy of the 120% Modified Version to make the Source form of the Modified Version 121% available to others under (i) the Original License or (ii) a license 122% that permits the licensee to freely copy, modify and redistribute the 123% Modified Version using the same licensing terms that apply to the copy 124% that the licensee received, and requires that the Source form of the 125% Modified Version, and of any works derived from it, be made freely 126% available in that license fees are prohibited but Distributor Fees are 127% allowed. 128% 129% Distribution of Compiled Forms of the Standard Version or 130% Modified Versions without the Source 131% 132% (5) You may Distribute Compiled forms of the Standard Version without 133% the Source, provided that you include complete instructions on how to 134% get the Source of the Standard Version. Such instructions must be 135% valid at the time of your distribution. If these instructions, at any 136% time while you are carrying out such distribution, become invalid, you 137% must provide new instructions on demand or cease further 138% distribution. If you provide valid instructions or cease distribution 139% within thirty days after you become aware that the instructions are 140% invalid, then you do not forfeit any of your rights under this 141% license. 142% 143% (6) You may Distribute a Modified Version in Compiled form without the 144% Source, provided that you comply with Section 4 with respect to the 145% Source of the Modified Version. 146% 147% Aggregating or Linking the Package 148% 149% (7) You may aggregate the Package (either the Standard Version or 150% Modified Version) with other packages and Distribute the resulting 151% aggregation provided that you do not charge a licensing fee for the 152% Package. Distributor Fees are permitted, and licensing fees for other 153% components in the aggregation are permitted. The terms of this license 154% apply to the use and Distribution of the Standard or Modified Versions 155% as included in the aggregation. 156% 157% (8) You are permitted to link Modified and Standard Versions with 158% other works, to embed the Package in a larger work of your own, or to 159% build stand-alone binary or bytecode versions of applications that 160% include the Package, and Distribute the result without restriction, 161% provided the result does not expose a direct interface to the Package. 162% 163% Items That are Not Considered Part of a Modified Version 164% 165% (9) Works (including, but not limited to, modules and scripts) that 166% merely extend or make use of the Package, do not, by themselves, cause 167% the Package to be a Modified Version. In addition, such works are not 168% considered parts of the Package itself, and are not subject to the 169% terms of this license. 170% 171% General Provisions 172% 173% (10) Any use, modification, and distribution of the Standard or 174% Modified Versions is governed by this Artistic License. By using, 175% modifying or distributing the Package, you accept this license. Do not 176% use, modify, or distribute the Package, if you do not accept this 177% license. 178% 179% (11) If your Modified Version has been derived from a Modified Version 180% made by someone other than you, you are nevertheless required to 181% ensure that your Modified Version complies with the requirements of 182% this license. 183% 184% (12) This license does not grant you the right to use any trademark, 185% service mark, tradename, or logo of the Copyright Holder. 186% 187% (13) This license includes the non-exclusive, worldwide, 188% free-of-charge patent license to make, have made, use, offer to sell, 189% sell, import and otherwise transfer the Package with respect to any 190% patent claims licensable by the Copyright Holder that are necessarily 191% infringed by the Package. If you institute patent litigation 192% (including a cross-claim or counterclaim) against any party alleging 193% that the Package constitutes direct or contributory patent 194% infringement, then this Artistic License to you shall terminate on the 195% date that such litigation is filed. 196% 197% (14) Disclaimer of Warranty: THE PACKAGE IS PROVIDED BY THE COPYRIGHT 198% HOLDER AND CONTRIBUTORS "AS IS' AND WITHOUT ANY EXPRESS OR IMPLIED 199% WARRANTIES. THE IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR A 200% PARTICULAR PURPOSE, OR NON-INFRINGEMENT ARE DISCLAIMED TO THE EXTENT 201% PERMITTED BY YOUR LOCAL LAW. UNLESS REQUIRED BY LAW, NO COPYRIGHT 202% HOLDER OR CONTRIBUTOR WILL BE LIABLE FOR ANY DIRECT, INDIRECT, 203% INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING IN ANY WAY OUT OF THE USE 204% OF THE PACKAGE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. 205% 206%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 207 208 209%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 210% prefix-trees for managing a DNF 211% 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) 212% children are sorted, but branches aren't (to speed up search while keeping structure sharing from proof procedure) 213%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 214 215:- module(ptree, [init_ptree/1, 216 delete_ptree/1, 217 member_ptree/2, 218 enum_member_ptree/2, 219 insert_ptree/2, 220 delete_ptree/2, 221 edges_ptree/2, 222 count_ptree/2, 223 prune_check_ptree/2, 224 empty_ptree/1, 225 merge_ptree/2, 226 merge_ptree/3, 227 bdd_ptree/3, 228 bdd_struct_ptree/3, 229 bdd_ptree_map/4, 230 bdd_struct_ptree_map/4, 231 traverse_ptree/2, %theo 232 print_ptree/1, %theo 233 statistics_ptree/0, %theo 234 print_nested_ptree/1, %theo 235 trie_to_bdd_trie/5, %theo 236 trie_to_bdd_struct_trie/5, 237 nested_trie_to_bdd_trie/5, %theo 238 nested_trie_to_bdd_struct_trie/5, 239 ptree_decomposition/3, 240 ptree_decomposition_struct/3, 241 nested_ptree_to_BDD_script/3, %theo 242 nested_ptree_to_BDD_struct_script/3, 243 ptree_db_trie_opt_performed/3, 244 bdd_vars_script/1 245 ]). 246 247% load library modules 248:- use_module(library(tries)). 249:- use_module(library(lists), [append/3, member/2, memberchk/2, delete/3]). 250:- use_module(library(system), [tmpnam/1]). 251:- use_module(library(ordsets), [ord_intersection/3, ord_union/3]). 252 253 254 255% load our own modules 256:- use_module(flags). 257:- use_module(utils). 258:- use_module(nestedtries, [nested_trie_to_depth_breadth_trie/4]). 259 260% switch on all tests to reduce bug searching time 261:- style_check(all). 262:- yap_flag(unknown,error). 263 264 265% this is a test to determine whether YAP provides the needed trie library 266:- initialization( 267 ( predicate_property(trie_disable_hash, imported_from(tries)) -> 268 trie_disable_hash 269 ; print_message(warning,'The predicate tries:trie_disable_hash/0 does not exist. Please update trie library.') 270 ) 271). 272 273%%%%%%%%%%%%%%%%%%%%%%% 274% Define module flags 275%%%%%%%%%%%%%%%%%%%%%%% 276 277:- initialization(( 278 problog_define_flag(use_db_trie, problog_flag_validate_boolean, 'use the builtin trie 2 trie transformation', false), 279 problog_define_flag(db_trie_opt_lvl, problog_flag_validate_integer, 'optimization level for the trie 2 trie transformation', 0), 280 problog_define_flag(compare_opt_lvl, problog_flag_validate_boolean, 'comparison mode for optimization level', false), 281 problog_define_flag(db_min_prefix, problog_flag_validate_integer, 'minimum size of prefix for dbtrie to optimize', 2), 282 problog_define_flag(use_naive_trie, problog_flag_validate_boolean, 'use the naive algorithm to generate bdd scripts', false), 283 problog_define_flag(use_old_trie, problog_flag_validate_boolean, 'use the old trie 2 trie transformation no nested', true), 284 problog_define_flag(use_dec_trie, problog_flag_validate_boolean, 'use the decomposition method', false), 285 problog_define_flag(deref_terms, problog_flag_validate_boolean, 'deref BDD terms after last use', false), 286 problog_define_flag(export_map_file, problog_flag_validate_boolean, 'activates export of a variable map file', false, output) 287)). 288 289 290%%%%%%%%%%%%%%%%%%%%%%%% 291% ptree basics 292%%%%%%%%%%%%%%%%%%%%%%%% 293 294init_ptree(Trie) :- 295 trie_open(Trie). 296 297delete_ptree(Trie) :- 298 trie_close(Trie), !. 299delete_ptree(_). 300 301empty_ptree(Trie) :- 302 trie_usage(Trie, 0, 0, 0). 303 304traverse_ptree(Trie, List) :- 305 trie_traverse(Trie, Ref), 306 trie_get_entry(Ref, List). 307 308traverse_ptree_mode(Mode) :- 309 trie_traverse_mode(Mode). 310 311%%%%%%%%%%%%%%%%%%%%%%%% 312% member 313%%%%%%%%%%%%%%%%%%%%%%%% 314 315% non-backtrackable (to check) 316member_ptree(List, Trie) :- 317 trie_check_entry(Trie, List, _). 318 319% backtrackable (to list) 320enum_member_ptree(List, Trie) :- 321 trie_path(Trie, List). 322 323trie_path(Trie, List) :- 324 trie_traverse(Trie, Ref), 325 trie_get_entry(Ref, List). 326 327%%%%%%%%%%%%%%%%%%%%%%%% 328% insert conjunction 329%%%%%%%%%%%%%%%%%%%%%%%% 330insert_ptree(false, _Trie) :-!. 331insert_ptree(true, Trie) :- 332 !, 333 trie_delete(Trie), 334 trie_put_entry(Trie, [true], _). 335insert_ptree(List, Trie) :- 336 (trie_check_entry(Trie, [true], _) -> % prune if there is a prob=1 proof 337 true 338 ; 339 trie_put_entry(Trie, List, _) 340 ). 341 342 343%%%%%%%%%%%%%%%%%%%%%%%% 344% delete conjunction 345%%%%%%%%%%%%%%%%%%%%%%%% 346delete_ptree(List, Trie) :- 347 trie_check_entry(Trie, List, Ref), 348 trie_remove_entry(Ref). 349 350 351%%%%%%%% 352% return list -Edges of all edge labels in ptree 353% doesn't use any heuristic to order those for the BDD 354% (automatic reordering has to do the job) 355%%%%%%%%% 356edges_ptree(Trie, []) :- 357 empty_ptree(Trie), 358 !. 359edges_ptree(Trie, []) :- 360 trie_check_entry(Trie, [true], _), 361 !. 362edges_ptree(Trie ,Edges) :- 363 setof(X, trie_literal(Trie, X), Edges). 364 365trie_literal(Trie, X) :- 366 trie_traverse(Trie,Ref), 367 trie_get_entry(Ref, List), 368 member(X, List). 369 370%%%%%%%% 371% number of conjunctions in the tree 372%%%%%%%%% 373 374count_ptree(Trie, N) :- 375 trie_usage(Trie, N, _, _). 376 377%%%%%%%% 378% check whether some branch of ptree is a subset of conjunction List 379% useful for pruning the search for proofs (optional due to time overhead) 380% currently not implemented, just fails 381%%%%%%% 382 383prune_check_ptree(_List, _Trie) :- 384 format(user,'FAIL: prune check currently not supported~n',[]), 385 flush_output(user), 386 fail. 387 388%%%%%%%%%%%%% 389% merge two ptrees 390% - take care not to loose proper prefixes that are proofs! 391%%%%%%%%%%%%%%% 392merge_ptree(T1, _) :- 393 trie_check_entry(T1, [true], _), !. 394merge_ptree(_, T2) :- 395 trie_check_entry(T2, [true], _), !. % is this strange on the loop condition? 396merge_ptree(T1, T2) :- 397 trie_join(T1, T2). 398 399merge_ptree(T1, _, T3) :- 400 trie_check_entry(T1, [true], _), 401 !, 402 trie_open(T3), 403 trie_put_entry(T3, [true], _). 404merge_ptree(_, T2, T3) :- 405 trie_check_entry(T2, [true], _), 406 !, 407 trie_open(T3), 408 trie_put_entry(T3, [true], _). 409merge_ptree(T1, T2, T3) :- 410 trie_dup(T1, T3), 411 trie_join(T3, T2). 412 413%%%%%%%%%%%%%%%%%%%%%%%% 414% Write structural BDD script for given trie to file 415% does NOT write a parameter file but unifies a list of used variables 416% 417% Specialized versions are: 418% - bdd_ptree -> bdd_struct_ptree 419% - bdd_ptree_map -> bdd_struct_ptree_map 420% - nested_ptree_to_BDD_script -> nested_ptree_to_BDD_struct_script 421% - trie_to_bdd_trie -> trie_to_bdd_struct_trie 422% - nested_trie_to_bdd_trie -> nested_trie_to_bdd_struct_trie 423% - ptree_decomposition -> ptree_decomposition_struct 424% - bdd_ptree_script -> bdd_struct_ptree_script 425%%%%%%%%%%%%%%%%%%%%%%%% 426:- dynamic(c_num/1). 427 428bdd_struct_ptree(Trie, FileBDD, Variables) :- 429 bdd_struct_ptree_script(Trie, FileBDD, Variables), 430 eraseall(map). 431 432bdd_struct_ptree_map(Trie, FileBDD, Variables, Mapping) :- 433 bdd_struct_ptree_script(Trie, FileBDD, Variables), 434 findall(X, recorded(map, X, _), Map), 435 add_probs(Map, Mapping), 436 eraseall(map). 437 438bdd_struct_ptree_script(Trie, FileBDD, Variables) :- 439 edges_ptree(Trie, Variables), 440 name_vars(Variables), % expected by output_compressed_script/1? 441 length(Variables, VarCount), 442 assertz(c_num(1)), 443 bdd_pt(Trie, CT), 444 c_num(NN), 445 IntermediateSteps is NN - 1, 446 tell(FileBDD), 447 format('@BDD1~n~w~n~w~n~w~n', [VarCount, 0, IntermediateSteps]), 448 output_compressed_script(CT), 449 told, 450 retractall(c_num(_)), 451 retractall(compression(_, _)). 452 453name_vars([]). 454name_vars([A|B]) :- 455 ( 456 A=not(ID) 457 -> 458 get_var_name(ID,_) 459 ; 460 get_var_name(A,_) 461 ), 462 name_vars(B). 463 464nested_ptree_to_BDD_struct_script(Trie, BDDFileName, Variables):- 465 tmpnam(TmpFile1), 466 open(TmpFile1, 'write', BDDS), 467 468 ( 469 generate_BDD_from_trie(Trie, Inter, BDDS) 470 -> 471 ( 472 next_intermediate_step(TMP), 473 InterCNT is TMP - 1, 474 format(BDDS,'~q~n',[Inter]), 475 close(BDDS), 476 ( 477 get_used_vars(Variables, VarCNT) 478 -> 479 true; 480 VarCNT = 0 481 ), 482 prefix_bdd_file_with_header(BDDFileName,VarCNT,InterCNT,TmpFile1), 483 cleanup_BDD_generation 484 );( 485 close(BDDS), 486 delete_file_silently(TmpFile1), 487 cleanup_BDD_generation, 488 fail 489 ) 490 ). 491 492trie_to_bdd_struct_trie(A, B, OutputFile, OptimizationLevel, Variables) :- 493 trie_to_depth_breadth_trie(A, B, LL, OptimizationLevel), 494 (atomic_concat('L', InterStep, LL) -> % what does this mean? 495 retractall(deref(_,_)), 496 (problog_flag(deref_terms, true) -> 497 asserta(deref(LL,no)), 498 mark_for_deref(B), 499 V = 3 500 ; 501 V = 1 502 ), 503 variables_in_dbtrie(B, Variables), %not the most efficient solution 504 length(Variables, VarCNT), %this 2 should be changed 505 tell(OutputFile), 506 write('@BDD'), write(V), nl, 507 write(VarCNT), nl, 508 write(0), nl, 509 write(InterStep), nl, 510 trie_write(B, LL), 511 write(LL), nl, 512 told 513 ; 514 (is_state(LL) -> 515 Variables = [] 516 ; 517 Variables = [LL] 518 ), 519 tell(OutputFile), 520 write('@BDD1'), nl, 521 write(1), nl, 522 write(0), nl, 523 write(1), nl, 524 get_var_name(LL, NLL), 525 write('L1 = '),write(NLL),nl, 526 write('L1'), nl, 527 told 528 ). 529 530nested_trie_to_bdd_struct_trie(A, B, OutputFile, OptimizationLevel, Variables):- 531 %trie_nested_to_depth_breadth_trie(A, B, LL, OptimizationLevel, problog:problog_chktabled), 532 nested_trie_to_depth_breadth_trie(A, B, LL, OptimizationLevel), 533 (is_label(LL) -> 534 retractall(deref(_,_)), 535 (problog_flag(deref_terms, true) -> 536 asserta(deref(LL,no)), 537 mark_for_deref(B), 538 V = 3 539 ; 540 V = 1 541 ), 542 variables_in_dbtrie(B, Variables), %not the most efficient solution 543 length(Variables, VarCNT), %this 2 should be changed 544 tell(OutputFile), 545 write('@BDD'), write(V), nl, 546 write(VarCNT), nl, 547 write(0), nl, 548 (LL = not(NegL)-> 549 atomic_concat('L', NegStep, NegL), 550 number_atom(NegStepN, NegStep), 551 InterStep is NegStepN + 1, 552 atomic_concat('L', InterStep, FL), 553 write(InterStep), nl, 554 trie_write(B, FL), 555 write(FL), write(' = ~'), write(NegL), nl, 556 write(FL), nl 557 ; 558 atomic_concat('L', InterStep, LL), 559 write(InterStep), nl, 560 trie_write(B, LL), 561 write(LL), nl 562 ), 563 told 564 ; 565 (is_state(LL) -> 566 Variables = [] 567 ; 568 Variables = [LL] 569 ), 570 tell(OutputFile), 571 write('@BDD1'), nl, 572 write(1), nl, 573 write(0), nl, 574 write(1), nl, 575 simplify(LL, FLL), 576 (FLL = not(_) -> 577 write('L1 = ~') 578 ; 579 write('L1 = ') 580 ), 581 get_var_name(FLL, NLL), 582 write(NLL),nl, 583 write('L1'), nl, 584 told 585 ). 586 587ptree_decomposition_struct(Trie, BDDFileName, Variables) :- 588 tmpnam(TmpFile1), 589 nb_setval(next_inter_step, 1), 590 variables_in_dbtrie(Trie, Variables), 591 length(Variables, VarCnt), 592 tell(TmpFile1), 593 decompose_trie(Trie, Variables, L), 594 (is_label(L)-> 595 atomic_concat('L', LCnt, L), 596 write(L),nl 597 ; 598 LCnt = 1, 599 write('L1 = '), 600 (L == false -> 601 write('FALSE') 602 ; 603 write(L) 604 ), nl, 605 write('L1'), nl 606 ), 607 told, 608 prefix_bdd_file_with_header(BDDFileName,VarCnt,LCnt,TmpFile1). 609 610%%%%%%%%%%%%%%%%%%%%%%%% 611% write BDD info for given ptree to file 612% - initializes leaf BDDs (=variables) first 613% - then compresses ptree to exploit subtree sharing 614% - bdd_pt/1 does the work on the structure itself 615%%%%%%%%%%%%%%%%%%%%%%%% 616 617 618bdd_ptree(Trie, FileBDD, FileParam) :- 619 bdd_ptree_script(Trie, FileBDD, FileParam), 620 eraseall(map). 621 622% version returning variable mapping 623bdd_ptree_map(Trie, FileBDD, FileParam, Mapping) :- 624 bdd_ptree_script(Trie, FileBDD, FileParam), 625 findall(X, recorded(map, X, _), Map), 626 add_probs(Map, Mapping), 627 eraseall(map). 628 629add_probs([], []). 630add_probs([m(A,Name)|Map], [m(A, Name, Prob)|Mapping]) :- 631 % FIXME: Does this work with non-ground facts 632 problog:get_fact_probability(A, Prob), 633 add_probs(Map, Mapping). 634 635% number of variables may be to high: 636% counted on trie, but conversion to old tree representation 637% transforms A*B+A to A (prefix-test) 638bdd_ptree_script(Trie, FileBDD, FileParam) :- 639 edges_ptree(Trie, Edges), 640 tell(FileParam), 641 bdd_vars_script(Edges), 642 643 flush_output, 644 645 told, 646 length(Edges, VarCount), 647 assertz(c_num(1)), 648 bdd_pt(Trie, CT), 649 c_num(NN), 650 IntermediateSteps is NN - 1, 651 tell(FileBDD), 652 format('@BDD1~n~w~n~w~n~w~n', [VarCount, 0, IntermediateSteps]), 653 output_compressed_script(CT), 654 655 656 told, 657 retractall(c_num(_)), 658 retractall(compression(_, _)). 659 660% write parameter file by iterating over all var/not(var) occuring in the tree 661 662bdd_vars_script(Vars):- 663 bdd_vars_script(Vars, Names), 664 (problog_flag(export_map_file, true) -> 665 problog_flag(map_file, MapFile), 666 os:convert_filename_to_working_path(MapFile, MapFileName), 667 flush_output, 668 tell(MapFileName), 669 problog:get_fact_list(Vars, Facts), 670 writemap(Names, Facts), 671 flush_output, 672 told 673 ; 674 true 675 ). 676writemap([],[]). 677writemap([Name|Names],[Fact|Facts]):- 678 write(map(Name,Fact)),nl, 679 writemap(Names, Facts). 680 681bdd_vars_script([], []). 682bdd_vars_script([false|T], Names):- 683 bdd_vars_script(T, Names). 684bdd_vars_script([true|T], Names):- 685 bdd_vars_script(T, Names). 686bdd_vars_script([not(A)|B], Names) :- 687 !, bdd_vars_script([A|B], Names). 688bdd_vars_script([A|B], [NameA|Names]) :- 689 bdd_vars_script_intern(A, NameA), 690 bdd_vars_script(B, Names). 691 692bdd_vars_script_intern(A, NameA) :- 693 (number(A) -> % it's a ground fact 694 get_var_name(A,NameA), 695 (problog:decision_fact(A,_) -> % it's a ground decision 696 (problog:problog_control(check,internal_strategy) -> 697 problog:get_fact_probability(A,P), 698 format('@~w~n~12f~n~w~n',[NameA,P,1]) 699 ; 700 dtproblog:initial_probability(P), 701 format('@~w~n~12f~n~w~n',[NameA,P,1]) 702 ) 703 ; % it's a normal ProbLog fact 704 problog:get_fact_probability(A,P), 705 format('@~w~n~12f~n',[NameA,P]) 706 ) 707 ; % it's somethin else, call the specialist - it's a non-ground or continuous fact 708 bdd_vars_script_intern2(A, NameA) 709 ). 710 711bdd_vars_script_intern2(A, NameA) :- 712 get_var_name(A,NameA), 713 atom_codes(A,A_Codes), 714 715 once(append(Part1,[95|Part2],A_Codes)), % 95 = '_' 716 number_codes(ID,Part1), 717 718 ( % let's check whether Part2 contains an 'l' (l=low) 719 member(108,Part2) 720 -> 721 ( % it does, so it's a continuous fact 722 problog:get_continuous_fact_parameters(ID,gaussian(Mu,Sigma)), 723 format('@~w~n0~n0~n~12f;~12f~n',[NameA,Mu,Sigma]) 724 ); 725 ( 726 number_codes(Grounding_ID,Part2), 727 (problog:decision_fact(ID,_) -> 728 % it's a non-ground decision 729 (problog:problog_control(check,internal_strategy) -> 730 problog:grounding_is_known(Goal,Grounding_ID), 731 problog:dynamic_probability_fact_extract(Goal,P), 732 format('@~w~n~12f~n~w~n',[NameA,P,1]) 733 ; 734 dtproblog:initial_probability(P), 735 format('@~w~n~12f~n~w~n',[NameA,P,1]) 736 ) 737 ; 738 (problog:dynamic_probability_fact(ID) -> 739 problog:grounding_is_known(Goal,Grounding_ID), 740 problog:dynamic_probability_fact_extract(Goal,P) 741 ; 742 problog:get_fact_probability(ID,P) 743 ), 744 format('@~w~n~12f~n',[NameA,P]) 745 ) 746 ) 747 ). 748 749%%%%%%%%%%%%%%%%%%%%%%%% 750% find top level symbol for script 751%%%%%%%%%%%%%%%%%%%%%%%% 752 753% special cases: variable-free formulae 754bdd_pt(Trie, false) :- 755 empty_ptree(Trie), 756 !, 757 retractall(c_num(_)), 758 assertz(c_num(2)). 759bdd_pt(Trie, true) :- 760 trie_check_entry(Trie, [true], _), 761 !, 762 retractall(c_num(_)), 763 assertz(c_num(2)). 764 765% general case: transform trie to nested tree structure for compression 766bdd_pt(Trie, CT) :- 767 trie_to_tree(Trie, Tree), 768 once(compress_pt(Tree, CT)). 769 770trie_to_tree(Trie, Tree) :- 771 findall(Path, trie_path(Trie, Path), Paths), 772 add_trees(Paths, [], Tree). 773 774add_trees([], Tree, Tree). 775add_trees([List|Paths], Tree0, Tree) :- 776 ins_pt(List, Tree0, TreeI), 777 add_trees(Paths, TreeI, Tree). 778 779% default: prune if adding prefix of known proof(s) 780ins_pt([], _T, []) :- !. 781% alternative: keep extensions of prefix 782% ins_pt([],T,T) :- !. 783ins_pt([A|B], [s(A1, AT)|OldT], NewT) :- 784 compare(Comp, A1, A), 785 (Comp == = -> 786 (AT == [] -> 787 NewT=[s(A1, AT)|OldT] 788 ; 789 NewT = [s(A1, NewAT)|OldT], 790 ins_pt(B, AT, NewAT)) 791 ; 792 Comp == > -> 793 NewT = [s(A1, AT)|Tree], 794 ins_pt([A|B], OldT, Tree) 795 ; 796 NewT = [s(A, BTree), s(A1, AT)|OldT], 797 ins_pt(B, [], BTree) 798 ). 799ins_pt([A|B], [], [s(A, NewAT)]) :- 800 ins_pt(B, [], NewAT). 801 802%%%%%%%%%%%% 803% BDD compression: alternates and- and or-levels to build BDD bottom-up 804% each sub-BDD will be either a conjunction of a one-node BDD with some BDD or a disjunction of BDDs 805% uses the internal database to temporarily store a map of components 806%%%%%%%%%%%% 807 808% T is completely compressed and contains single variable 809% i.e. T of form x12 or ~x34 810compress_pt(T, TT) :- 811 atom(T), 812 test_var_name(T), 813 !, 814 get_next_name(TT), 815 assertz(compression(TT, [T])). 816% T is completely compressed and contains subtrees 817% i.e. T of form 'L56' 818compress_pt(T, T) :- 819 atom(T). 820% T not yet compressed 821% i.e. T is a tree-term (nested list & s/2 structure) 822% -> execute one layer of compression, then check again 823compress_pt(T, CT) :- 824 \+ atom(T), 825 and_or_compression(T, IT), 826 compress_pt(IT, CT). 827 828% transform tree-term T into tree-term CT where last two layers have been processed 829% i.e. introduce names for subparts (-> Map) and replace (all occurrenes of) subparts by this names 830and_or_compression(T, CT) :- 831 and_comp(T, AT), 832 or_comp(AT, CT). 833 834% replace leaves that are single child by variable representing father-AND-child 835and_comp(T, AT) :- 836 all_leaves_pt(T, Leaves), 837 compression_mapping(Leaves, Map), 838 replace_pt(T, Map, AT). 839 840% replace list of siblings by variable representing their disjunction 841or_comp(T, AT) :- 842 all_leaflists_pt(T, Leaves), 843 compression_mapping(Leaves, Map), 844 replace_pt(T, Map, AT). 845 846all_leaves_pt(T, L) :- 847 all(X, some_leaf_pt(T, X), L). 848 849some_leaf_pt([s(A, [])|_], s(A,[])). 850some_leaf_pt([s(A, L)|_], s(A, L)) :- 851 not_or_atom(L). 852some_leaf_pt([s(_, L)|_], X) :- 853 some_leaf_pt(L, X). 854some_leaf_pt([_|L],X) :- 855 some_leaf_pt(L,X). 856 857all_leaflists_pt(L, [L]) :- 858 atomlist(L), !. 859all_leaflists_pt(T, L) :- 860 all(X,some_leaflist_pt(T, X), L), !. 861all_leaflists_pt(_, []). 862 863some_leaflist_pt([s(_, L)|_], L) :- 864 atomlist(L). 865some_leaflist_pt([s(_, L)|_], X) :- 866 some_leaflist_pt(L, X). 867some_leaflist_pt([_|L], X) :- 868 some_leaflist_pt(L, X). 869 870not_or_atom(T) :- 871 ( 872 T = not(T0) 873 -> 874 atom(T0); 875 atom(T) 876 ). 877 878atomlist([]). 879atomlist([A|B]) :- 880 not_or_atom(A), 881 atomlist(B). 882 883% for each subtree that will be compressed, add its name 884% only introduce 'L'-based names when subtree composes elements, store these in compression/2 for printing the script 885compression_mapping([], []). 886compression_mapping([First|B], [N-First|BB]) :- 887 ( 888 First = s(A0, []) % subtree is literal -> use variable's name x17 from map (add ~ for negative case) 889 -> 890 ( 891 A0 = not(A) 892 -> 893 ( 894 recorded(map, m(A, Tmp), _), %check 895 atomic_concat(['~', Tmp], N) 896 ); 897 recorded(map, m(A0, N), _) %check 898 ) 899 ; 900 (First = s(A, L), not_or_atom(L)) % subtree is node with single completely reduced child -> use next 'L'-based name 901 -> (get_next_name(N), 902 assertz(compression(N, s(A, L)))) 903 ; 904 (First = [L], not_or_atom(L)) % subtree is an OR with a single completely reduced element -> use element's name 905 -> N = L 906 ; 907 (atomlist(First), % subtree is an OR with only (>1) completely reduced elements -> use next 'L'-based name 908 get_next_name(N), 909 assertz(compression(N, First))) 910 ), 911 compression_mapping(B, BB). 912 913 914 915% replace_pt(+T,+Map,-NT) 916% given the tree-term T and the Map of Name-Subtree entries, replace each occurence of Subtree in T with Name -> result NT 917replace_pt(T, [], T). 918replace_pt([], _, []). 919replace_pt(L, M, R) :- 920 atomlist(L), 921 member(R-L, M), 922 !. 923replace_pt([L|LL], [M|MM], R) :- 924 replace_pt_list([L|LL], [M|MM], R). 925 926replace_pt_list([T|Tree], [M|Map], [C|Compr]) :- 927 replace_pt_single(T, [M|Map], C), 928 replace_pt_list(Tree, [M|Map], Compr). 929replace_pt_list([], _, []). 930 931replace_pt_single(s(A, T), [M|Map], Res) :- 932 atomlist(T), 933 member(Res-s(A, T), [M|Map]), 934 !. 935replace_pt_single(s(A, T), [M|Map], s(A, Res)) :- 936 atomlist(T), 937 member(Res-T, [M|Map]), 938 !. 939replace_pt_single(s(A, T), [M|Map], Res) :- 940 member(Res-s(A, T), [M|Map]), 941 !. 942replace_pt_single(s(A, T), [M|Map], s(A, TT)) :- 943 !, 944 replace_pt_list(T, [M|Map], TT). 945replace_pt_single(A, _, A) :- 946 not_or_atom(A). 947 948%%%%%%%%%%%% 949% output for script 950% input argument is compressed tree, i.e. true/false or name assigned in last compression step 951%%%%%%%%%%%% 952output_compressed_script(false) :- 953 !, 954 format('L1 = FALSE~nL1~n', []). 955output_compressed_script(true) :- 956 !, 957 format('L1 = TRUE~nL1~n', []). 958% for each name-subtree pair, write corresponding line to script, e.g. L17 = x4 * L16 959% stop after writing definition of root (last entry in compression/2), add it's name to mark end of script 960output_compressed_script(T) :- 961 once(retract(compression(Short, Long))), 962 (T = Short -> 963 format('~w = ', [Short]), 964 format_compression_script(Long), 965 format('~w~n', [Short]) 966 ; 967 format('~w = ', [Short]), 968 format_compression_script(Long), 969 output_compressed_script(T)). 970 971format_compression_script(s(A0, B0)) :- 972 % checkme 973 ( 974 A0 = not(A) 975 -> 976 ( 977 recorded(map, m(A, C), _), 978 format('~~~w * ~w~n', [C, B0]) 979 ) ; 980 ( 981 recorded(map, m(A0, C), _), 982 format('~w * ~w~n', [C, B0]) 983 ) 984 ). 985format_compression_script([A]) :- 986 format('~w~n', [A]). 987format_compression_script([A, B|C]) :- 988 format('~w + ', [A]), 989 format_compression_script([B|C]). 990 991%%%%%%%%%%%%%%%%%%%%%%%% 992% auxiliaries for translation to BDD 993%%%%%%%%%%%%%%%%%%%%%%%% 994 995% prefix the current counter with "L" 996get_next_name(Name) :- 997 retract(c_num(N)), 998 NN is N + 1, 999 assertz(c_num(NN)), 1000 atomic_concat('L', N, Name). 1001 1002% create BDD-var as fact id prefixed by x 1003% learning.yap relies on this format! 1004% when changing, also adapt test_var_name/1 below 1005 1006 1007simplify_list(List, SList):- 1008 findall(NEL, (member(El, List), simplify(El, NEL)), SList). 1009 1010simplify(not(false), true):- !. 1011simplify(not(true), false):- !. 1012simplify(not(not(A)), B):- 1013 !, simplify(A, B). 1014simplify(A, A). 1015 1016 1017 1018simplify(not(false), true):- !. 1019simplify(not(true), false):- !. 1020simplify(not(not(A)), B):- 1021 !, simplify(A, B). 1022simplify(A, A). 1023 1024get_var_name(true, 'TRUE'):- !. 1025get_var_name(false, 'FALSE'):- !. 1026get_var_name(Variable, Name):- 1027 atomic(Variable), !, 1028 atomic_concat([x, Variable], Name), 1029 (recorded(map, m(Variable, Name), _) -> 1030 true 1031 ; 1032 recorda(map, m(Variable, Name), _) 1033 ). 1034get_var_name(not(A), NameA):- 1035 get_var_name(A, NameA). 1036 1037 1038/* 1039get_var_name(true, 'TRUE') :-!. 1040get_var_name(false, 'FALSE') :-!. 1041get_var_name(not(A), NameA):- 1042 !, get_var_name(A, NameA). 1043get_var_name(A, NameA) :- 1044 atomic_concat([x, A], NameA), 1045 ( 1046 recorded(map, m(A, NameA), _) 1047 -> 1048 true 1049 ; 1050 recorda(map, m(A, NameA), _) 1051 ).*/ 1052 1053% test used by base case of compression mapping to detect single-variable tree 1054% has to match above naming scheme 1055test_var_name(T) :- 1056 atomic_concat(x, _, T). 1057test_var_name(T) :- 1058 atomic_concat('~x', _, T). 1059 1060 1061% Theo debuging additions 1062 1063print_ptree(Trie):- 1064 trie_print(Trie). 1065 1066statistics_ptree:- 1067 trie_stats(Memory,Tries,Entries,Nodes), 1068 write('--------------------------------'),nl, 1069 write('Memory: '),write(Memory),nl, 1070 write('Tries: '), write(Tries),nl, 1071 write('Entries: '), write(Entries),nl, 1072 write('Nodes: '), write(Nodes),nl, 1073 write('--------------------------------'),nl. 1074 1075 1076:- dynamic(nested_ptree_printed/1). 1077 1078print_nested_ptree(Trie):- 1079 retractall(nested_ptree_printed(_)), 1080 print_nested_ptree(Trie, 0, ' '), 1081 retractall(nested_ptree_printed(_)). 1082print_nested_ptree(Trie, _, _):- 1083 nested_ptree_printed(Trie), !. 1084print_nested_ptree(Trie, Level, Space):- 1085 spacy_print(begin(t(Trie)), Level, Space), 1086 fail. 1087print_nested_ptree(Trie, Level, Space):- 1088 assertz(nested_ptree_printed(Trie)), 1089 trie_path(Trie, Path), 1090 NewLevel is Level + 1, 1091 spacy_print(Path, NewLevel, Space), 1092 (member(t(Hash), Path); member(not(t(Hash)), Path)), 1093 problog:problog_chktabled(Hash, SubTrie), 1094 NewLevel2 is NewLevel + 1, 1095 print_nested_ptree(SubTrie, NewLevel2, Space), 1096 fail. 1097print_nested_ptree(Trie, Level, Space):- 1098 spacy_print(end(t(Trie)), Level, Space). 1099 1100spacy_print(Msg, 0, _):- 1101 write(Msg), nl, !. 1102spacy_print(Msg, Level, Space):- 1103 Level > 0, 1104 write(Space), 1105 NewLevel is Level - 1, 1106 spacy_print(Msg, NewLevel, Space). 1107 1108% Theo Naive method works with Nested Trie to BDD Script 1109 1110:- dynamic(get_used_vars/2). 1111:- dynamic(generated_trie/2). 1112:- dynamic(next_intermediate_step/1). 1113 1114 1115nested_ptree_to_BDD_script(Trie, BDDFileName, VarFileName):- 1116 tmpnam(TmpFile1), 1117 open(TmpFile1, 'write', BDDS), 1118 (generate_BDD_from_trie(Trie, Inter, BDDS) -> 1119 next_intermediate_step(TMP), InterCNT is TMP - 1, 1120 write(BDDS, Inter), nl(BDDS), 1121 close(BDDS), 1122 ( 1123 get_used_vars(Vars, VarCNT) 1124 -> 1125 true; 1126 VarCNT = 0 1127 ), 1128 prefix_bdd_file_with_header(BDDFileName,VarCNT,InterCNT,TmpFile1), 1129 open(VarFileName, 'write', VarStream), 1130 bddvars_to_script(Vars, VarStream), 1131 close(VarStream), 1132 cleanup_BDD_generation 1133 ; 1134 close(BDDS), 1135 delete_file_silently(TmpFile1), 1136 cleanup_BDD_generation, 1137 fail 1138 ). 1139 1140cleanup_BDD_generation:- 1141 retractall(get_used_vars(_, _)), 1142 retractall(generated_trie(_, _)), 1143 retractall(next_intermediate_step(_)). 1144 1145generate_BDD_from_trie(Trie, TrieInter, Stream):- 1146 empty_ptree(Trie), !, 1147 get_next_intermediate_step(TrieInter), 1148 write(Stream, TrieInter), write(Stream, ' = FALSE'), nl(Stream), !. 1149generate_BDD_from_trie(Trie, TrieInter, _Stream):- 1150 clause(generated_trie(STrie, TrieInter), true), 1151 STrie = Trie, !. 1152generate_BDD_from_trie(Trie, TrieInter, Stream):- 1153 findall(LineInter, ( 1154 trie_path(Trie, L), 1155 generate_line(L, LineTerms, LineInter, Stream), 1156 write_bdd_line(LineTerms, LineInter, '*', Stream) 1157 ), OrLineTerms), 1158 (OrLineTerms = [Inter|[]] -> 1159 TrieInter = Inter 1160 ; 1161 get_next_intermediate_step(TrieInter), 1162 write_bdd_line(OrLineTerms, TrieInter, '+', Stream) 1163 ), 1164 assertz(generated_trie(Trie, TrieInter)). 1165 1166write_bdd_line([], _LineInter, _Operator, _Stream):-!. 1167write_bdd_line(LineTerms, LineInter, Operator, Stream):- 1168 write(Stream, LineInter), write(Stream, '='), 1169 write_bdd_lineterm(LineTerms, Operator, Stream). 1170 1171write_bdd_lineterm([LineTerm|[]], _Operator, Stream):- 1172 write(Stream, LineTerm), nl(Stream), !. 1173write_bdd_lineterm([LineTerm|LineTerms], Operator, Stream):- 1174 write(Stream, LineTerm), write(Stream, Operator), 1175 write_bdd_lineterm(LineTerms, Operator, Stream). 1176 1177generate_line([], [], Inter, _Stream):- 1178 !, get_next_intermediate_step(Inter). 1179generate_line([not(t(Hash))|L], [TrieInter|T] , Inter, Stream):- 1180 !, problog:problog_chktabled(Hash, Trie), 1181 generate_BDD_from_trie(Trie, TrieInterTmp, Stream), 1182 atomic_concat(['~', TrieInterTmp], TrieInter), 1183 generate_line(L, T, Inter, Stream). 1184generate_line([t(Hash)|L], [TrieInter|T] , Inter, Stream):- 1185 !, problog:problog_chktabled(Hash, Trie), 1186 generate_BDD_from_trie(Trie, TrieInter, Stream), 1187 generate_line(L, T, Inter, Stream). 1188generate_line([V|L], [BDDV|T], Inter, Stream):- 1189 make_bdd_var(V, BDDV), 1190 generate_line(L, T, Inter, Stream). 1191 1192% 1193% Currently it is dublicate with bdd_vars_script predicate 1194% finally should be merged 1195% 1196 1197bddvars_to_script([], _Stream):-!. 1198bddvars_to_script([H|T], Stream):- 1199 (number(H) -> 1200 CurVar = H 1201 ; 1202 atom_codes(H, H_Codes), 1203 % 95 = '_' 1204 append(Part1, [95|Part2], H_Codes), 1205 number_codes(CurVar, Part1), 1206 number_codes(Grounding_ID, Part2) 1207 ), 1208 (problog:dynamic_probability_fact(CurVar) -> 1209 problog:grounding_is_known(Goal, Grounding_ID), 1210 problog:dynamic_probability_fact_extract(Goal, P) 1211 ; 1212 problog:get_fact_probability(CurVar, P) 1213 ), 1214 get_var_name(H, VarName), 1215 format(Stream, '@~w~n~12f~n', [VarName, P]), 1216 bddvars_to_script(T, Stream). 1217 1218get_next_intermediate_step('L1'):- 1219 \+ clause(next_intermediate_step(_), _), !, 1220 assertz(next_intermediate_step(2)). 1221get_next_intermediate_step(Inter):- 1222 next_intermediate_step(InterStep), 1223 retract(next_intermediate_step(InterStep)), 1224 NextInterStep is InterStep + 1, 1225 assertz(next_intermediate_step(NextInterStep)), 1226 atomic_concat(['L', InterStep], Inter). 1227 1228make_bdd_var('true', 'TRUE'):-!. 1229make_bdd_var('false', 'FALSE'):-!. 1230/*make_bdd_var(neg(V), NotVName):- 1231 !, make_bdd_var(not(V), NotVName).*/ 1232make_bdd_var(not(V), NotVName):- 1233 !, 1234 get_var_name(V, VName), 1235 atomic_concat(['~', VName], NotVName), 1236 add_to_vars(V). 1237make_bdd_var(V, VName):- 1238 get_var_name(V, VName), 1239 add_to_vars(V). 1240 1241 1242add_to_vars(V):- 1243 clause(get_used_vars(Vars, _Cnt), true), 1244 memberchk(V, Vars),!. 1245add_to_vars(V):- 1246 clause(get_used_vars(Vars, Cnt), true), !, 1247 retract(get_used_vars(Vars, Cnt)), 1248 NewCnt is Cnt + 1, 1249 assertz(get_used_vars([V|Vars], NewCnt)). 1250add_to_vars(V):- 1251 assertz(get_used_vars([V], 1)). 1252 1253 1254%%%%%%%%%%%%%%% depth breadth builtin support %%%%%%%%%%%%%%%%% 1255%%% 1256%%% Pending: 1257%%% 1) Replace term in trie, written in C level 1258%%% *2) Support for false, true and 1 var 1259%%% 3) Decide if it is necessary to propagete loop from child 1260%%% 4) Possible memory leak with [true] (go(0)) 1261%%% *5) Handle correctly the trie_replace when not(false), not(true) 1262%%% 6) Compare sort with a good insert sort 1263%%% 7) Have a look to the write to file predicates 1264%%% 1265 1266 1267variables_in_dbtrie(Trie, []):- 1268 empty_ptree(Trie), !. 1269variables_in_dbtrie(Trie, []):- 1270 trie_check_entry(Trie, [true], _R), !. 1271variables_in_dbtrie(Trie, L):- 1272 all(V, variable_in_dbtrie(Trie,V), L). 1273 1274variable_in_dbtrie(Trie, V):- 1275 trie_traverse(Trie, R), 1276 trie_get_entry(R, L), 1277 get_next_variable(NV, L), 1278 get_variable(NV, V). 1279 1280get_next_variable(V, depth(L, _S)):- 1281 member(V, L), 1282 \+ is_label(V). 1283get_next_variable(V, breadth(L, _S)):- 1284 member(V, L), 1285 \+ is_label(V). 1286get_next_variable(V, L):- 1287 member(V, L), 1288 \+ is_label(V), 1289 \+ isnestedtrie(V). 1290 1291get_variable(not(V), R):- 1292 !, get_variable(V, R). 1293get_variable(R, R). 1294 1295 1296 %trie_get_depth_breadth_reduction_opt_level_count(1, CNT1), 1297 %trie_get_depth_breadth_reduction_opt_level_count(2, CNT2), 1298 %trie_get_depth_breadth_reduction_opt_level_count(3, CNT3), 1299 %writeln([CNT1, CNT2, CNT3]), 1300 %trie_print(B), 1301 1302trie_to_bdd_trie(A, B, OutputFile, OptimizationLevel, FileParam):- 1303 trie_to_depth_breadth_trie(A, B, LL, OptimizationLevel), 1304 (is_label(LL) -> 1305 atomic_concat('L', InterStep, LL), 1306 retractall(deref(_,_)), 1307 (problog_flag(deref_terms, true) -> 1308 asserta(deref(LL,no)), 1309 mark_for_deref(B), 1310 V = 3 1311 ; 1312 V = 1 1313 ), 1314 variables_in_dbtrie(B, Edges), %not the most efficient solution 1315 length(Edges, VarCNT), %this 2 should be changed 1316 tell(FileParam), 1317 bdd_vars_script(Edges), 1318 told, 1319 tell(OutputFile), 1320 write('@BDD'), write(V), nl, 1321 write(VarCNT), nl, 1322 write(0), nl, 1323 write(InterStep), nl, 1324 trie_write(B, LL), 1325 write(LL), nl, 1326 told 1327 ; 1328 (is_state(LL) -> 1329 Edges = [] 1330 ; 1331 Edges = [LL] 1332 ), 1333 tell(FileParam), 1334 bdd_vars_script(Edges), 1335 told, 1336 tell(OutputFile), 1337 write('@BDD1'), nl, 1338 write(1), nl, 1339 write(0), nl, 1340 write(1), nl, 1341 (LL = not(ID) -> 1342 get_var_name(ID, NLL), 1343 write('L1 = ~'), write(NLL),nl 1344 ; 1345 get_var_name(LL, NLL), 1346 write('L1 = '), write(NLL),nl 1347 ), 1348 write('L1'), nl, 1349 told 1350 ). 1351 1352is_state(true). 1353is_state(false). 1354 1355nested_trie_to_bdd_trie(A, B, OutputFile, OptimizationLevel, FileParam):- 1356% trie_nested_to_depth_breadth_trie(A, B, LL, OptimizationLevel, problog:problog_chktabled), 1357 nested_trie_to_depth_breadth_trie(A, B, LL, OptimizationLevel), 1358 simplify(LL, FLL), 1359 (is_label(FLL) -> 1360 retractall(deref(_,_)), 1361 (problog_flag(deref_terms, true) -> 1362 asserta(deref(FLL,no)), 1363 mark_for_deref(B), 1364 V = 3 1365 ; 1366 V = 1 1367 ), 1368 variables_in_dbtrie(B, Edges), %not the most efficient solution 1369 length(Edges, VarCNT), %this 2 should be changed 1370 tell(FileParam), 1371 bdd_vars_script(Edges), 1372 told, 1373 1374 tell(OutputFile), 1375 write('@BDD'), write(V), nl, 1376 write(VarCNT), nl, 1377 write(0), nl, 1378 (FLL = not(NegL)-> 1379 atomic_concat('L', NegStep, NegL), 1380 number_atom(NegStepN, NegStep), 1381 InterStep is NegStepN + 1, 1382 atomic_concat('L', InterStep, FL), 1383 write(InterStep), nl, 1384 trie_write(B, FL), 1385 write(FL), write(' = ~'), write(NegL), nl, 1386 write(FL), nl 1387 ; 1388 atomic_concat('L', InterStep, FLL), 1389 write(InterStep), nl, 1390 trie_write(B, FLL), 1391 write(FLL), nl 1392 ), 1393 told 1394 ; 1395 (is_state(FLL) -> 1396 Edges = [] 1397 ; 1398 Edges = [FLL] 1399 ), 1400 tell(FileParam), 1401 simplify_list(Edges, SEdges), 1402 bdd_vars_script(SEdges), 1403 told, 1404 tell(OutputFile), 1405 write('@BDD1'), nl, 1406 write(1), nl, 1407 write(0), nl, 1408 write(1), nl, 1409 (FLL = not(_) -> 1410 write('L1 = ~') 1411 ; 1412 write('L1 = ') 1413 ), 1414 get_var_name(FLL, NLL), 1415 write(NLL),nl, 1416 write('L1'), nl, 1417 told 1418 ). 1419 1420 1421/* 1422 variables_in_dbtrie(B, Edges), %not the most efficient solution 1423 1424 length(Edges, VarCNT), %this 2 should be changed 1425 tell(FileParam), 1426 bdd_vars_script(Edges), 1427 told, 1428 (atomic_concat('L', InterStep, LL) -> 1429 tell(OutputFile), 1430 write('@BDD1'), nl, 1431 write(VarCNT), nl, 1432 write(0), nl, 1433 write(InterStep), nl, 1434 trie_write(B, LL), 1435 write(LL), nl, 1436 told 1437 ; 1438 tell(OutputFile), 1439 write('@BDD1'), nl, 1440 write(1), nl, 1441 write(0), nl, 1442 write(1), nl, 1443 fix(LL, NLL), 1444 write('L1 = '),write(NLL),nl, 1445 write('L1'), nl, 1446 told 1447 ). 1448 1449fix(false, 'FALSE'):-!. 1450fix(true, 'TRUE'):-!. 1451fix(A, A). 1452*/ 1453 1454preprocess(Index, DepthBreadthTrie, OptimizationLevel, StartCount, FinalEndCount):- 1455 problog:problog_chktabled(Index, Trie), !, 1456 trie_dup(Trie, CopyTrie), 1457 initialise_ancestors(Ancestors), 1458 make_nested_trie_base_cases(CopyTrie, t(Index), DepthBreadthTrie, OptimizationLevel, StartCount, EndCount, Ancestors), 1459 trie_close(CopyTrie), 1460 Next is Index + 1, 1461 preprocess(Next, DepthBreadthTrie, OptimizationLevel, EndCount, FinalEndCount). 1462preprocess(_, _, _, FinalEndCount, FinalEndCount). 1463 1464make_nested_trie_base_cases(Trie, t(ID), DepthBreadthTrie, OptimizationLevel, StartCount, FinalEndCount, Ancestors):- 1465 trie_to_depth_breadth_trie(Trie, DepthBreadthTrie, Label, OptimizationLevel, StartCount, EndCount), 1466 (Label \= t(_) -> 1467 FinalEndCount = EndCount, 1468 problog:problog_chktabled(ID, RTrie),!, 1469 get_set_trie_from_id(t(ID), Label, RTrie, Ancestors, _, Ancestors) 1470 ; 1471 trie_get_depth_breadth_reduction_entry(NestedEntry), 1472 trie_replace_entry(Trie, NestedEntry, Label, false), 1473 add_to_ancestors(Label, Ancestors, NewAncestors), 1474 make_nested_trie_base_cases(Trie, t(ID), DepthBreadthTrie, OptimizationLevel, EndCount, FinalEndCount, NewAncestors) 1475 ). 1476 1477trie_nested_to_depth_breadth_trie(Trie, DepthBreadthTrie, FinalLabel, OptimizationLevel, Module:GetTriePredicate):- 1478 integer(OptimizationLevel), 1479 trie_open(DepthBreadthTrie), 1480 (problog_flag(trie_preprocess, true) -> 1481 preprocess(1, DepthBreadthTrie, OptimizationLevel, 0, StartCount) 1482 ; 1483 StartCount = 0 1484 ), 1485 initialise_ancestors(Ancestors), 1486 initialise_ancestors(Childs), 1487 trie_nested_to_db_trie(Trie, DepthBreadthTrie, FinalLabel, OptimizationLevel, StartCount, _, Module:GetTriePredicate, Ancestors, _, _, Childs), 1488 eraseall(problog_trie_table). 1489 1490trie_nested_to_db_trie(Trie, DepthBreadthTrie, FinalLabel, OptimizationLevel, StartCount, FinalEndCount, Module:GetTriePredicate, AncestorList, ContainsLoop, Childs, ChildsAcc):- 1491 trie_dup(Trie, CopyTrie), 1492 nested_trie_to_db_trie(CopyTrie, DepthBreadthTrie, FinalLabel, OptimizationLevel, StartCount, FinalEndCount, Module:GetTriePredicate, AncestorList, ContainsLoop, Childs, ChildsAcc), 1493 trie_close(CopyTrie). 1494 1495nested_trie_to_db_trie(Trie, DepthBreadthTrie, FinalLabel, OptimizationLevel, StartCount, FinalEndCount, Module:GetTriePredicate, Ancestors, ContainsLoop, Childs, ChildsAcc):- 1496 trie_to_depth_breadth_trie(Trie, DepthBreadthTrie, Label, OptimizationLevel, StartCount, EndCount), 1497 (Label \= t(_) -> 1498 (var(ContainsLoop) -> 1499 ContainsLoop = false 1500 ; 1501 true 1502 ), 1503 FinalLabel = Label, 1504 FinalEndCount = EndCount, 1505 Childs = ChildsAcc 1506 ; 1507 trie_get_depth_breadth_reduction_entry(NestedEntry), 1508 trie_get_entry(NestedEntry, Proof), 1509 (loopcheck(Proof, Ancestors) -> % to fix 1510 ContainsLoop = true, 1511 NewLabel = false, 1512 NewEndCount = EndCount 1513 ; 1514% writeln(in(Label)), 1515 get_set_trie_from_id(Label, NewLabel, NestedTrie, Ancestors, Module:GetTriePredicate, ChildChilds), 1516% writeln(out(NewLabel)), 1517 (nonvar(NewLabel) -> 1518 NewEndCount = EndCount 1519 ; 1520 add_to_ancestors(Label, Ancestors, CurAncestors), 1521 initialise_ancestors(ChildChildsAcc), 1522 trie_nested_to_db_trie(NestedTrie, DepthBreadthTrie, NewLabel, OptimizationLevel, EndCount, NewEndCount, Module:GetTriePredicate, CurAncestors, CheckLoop, ChildChilds, ChildChildsAcc), 1523 (CheckLoop -> 1524 StoreAncestors = CurAncestors 1525 ; 1526 initialise_ancestors(StoreAncestors) 1527 ), 1528 get_set_trie_from_id(Label, NewLabel, NestedTrie, StoreAncestors, Module:GetTriePredicate, ChildChilds) 1529 ) 1530 ), 1531 trie_replace_entry(Trie, NestedEntry, Label, NewLabel), 1532 (problog_flag(refine_anclst, true) -> 1533 combine_ancestors(ChildsAcc, ChildChilds, AllChilds), 1534 add_to_ancestors(Label, AllChilds, FAllChilds) 1535 ; 1536 initialise_ancestors(FAllChilds) 1537 ), 1538 nested_trie_to_db_trie(Trie, DepthBreadthTrie, FinalLabel, OptimizationLevel, NewEndCount, FinalEndCount, Module:GetTriePredicate, Ancestors, ContainsLoop, Childs, FAllChilds) 1539 ). 1540 1541initialise_ancestors(Ancestors):- 1542 (problog_flag(anclst_represent, list) -> 1543 Ancestors = [] 1544 ; 1545 Ancestors = 0 1546 ). 1547 1548add_to_ancestors(t(ID), Ancestors, NewAncestors):- 1549 (problog_flag(anclst_represent, list) -> 1550 ord_union(Ancestors, [t(ID)], NewAncestors) 1551 ; 1552 NewAncestors is Ancestors \/ (1 << (ID - 1)) 1553 ). 1554 1555combine_ancestors(Ancestors, AddAncestors, Ancestors):- 1556 var(AddAncestors), !. 1557combine_ancestors(Ancestors, AddAncestors, AllAncestors):- 1558 (problog_flag(anclst_represent, list) -> 1559 ord_union(Ancestors, AddAncestors, AllAncestors) 1560 ; 1561 AllAncestors is Ancestors \/ AddAncestors 1562 ). 1563 1564 1565my_trie_print(T):- 1566 trie_traverse(T, R), 1567 trie_get_entry(R, E), 1568 writeln(E), 1569 fail. 1570my_trie_print(_T). 1571 1572loopcheck(Proof, AncestorList):- 1573 contains_nested_trie(Proof, ID), 1574% memberchk(t(ID), AncestorList). 1575% writeln(chk_id(ID, AncestorList)), 1576 chk_id(ID, AncestorList), !. 1577chk_id(ID, AncestorList):- 1578 (problog_flag(anclst_represent, list) -> 1579 memberchk(t(ID), AncestorList) 1580 ; 1581 (AncestorList /\ (1 << (ID - 1))) > 0 1582 ). 1583chk_id(ID, AncestorList):- 1584 get_negated_synonym_id(ID, NegID), 1585% writeln(get_negated_synonym_id(ID, NegID)), 1586 (problog_flag(anclst_represent, list) -> 1587 memberchk(t(NegID), AncestorList) 1588 ; 1589 (AncestorList /\ (1 << (NegID - 1))) > 0 1590 ). 1591% % can also check for a proof with A, not(A) 1592% 1593% get_negated_synonym_id(ID, NegID):- 1594% tabling:problog_tabling_get_negated_from_id(ID, Ref), 1595% recorded(problog_table, store(_, NegID, _, _, _), Ref). 1596 1597get_negated_synonym_id(ID, NegID):- 1598 tabling:has_synonyms, 1599 recorded(problog_table, store(Pred, ID, _, _, _), _), 1600 Pred =.. [Name0|Args], 1601 atomic_concat(problog_, Name1, Name0), 1602 atomic_concat(Name, '_original', Name1), 1603 (recorded(problog_table_synonyms, negated(Name, NotName1), _); 1604 recorded(problog_table_synonyms, negated(NotName1, Name), _)), 1605 atomic_concat([problog_, NotName1, '_original'], NotName), 1606 NegPred =.. [NotName|Args], 1607 recorded(problog_table, store(NegPred, NegID, _, _, _), _). 1608 1609 1610is_nested_trie(T):- 1611 nonvar(T), 1612 is_nested_trie(T, _). 1613is_nested_trie(NT, ID):- 1614 nonvar(NT), 1615 NT = not(T), !, 1616 is_nested_trie(T, ID). 1617is_nested_trie(t(ID), ID). 1618 1619contains_nested_trie(L, ID):- 1620 member(T, L), 1621 is_nested_trie(T, ID). 1622 1623 1624subset([],_):-!. 1625subset(_,[]):-!,fail. 1626subset([H|T1], [H|T2]):- 1627 subset(T1, T2). 1628subset([H1|T1], [H2|T2]):- 1629 compare(>, H1, H2), 1630 subset([H1|T1],T2). 1631 1632get_set_trie_from_id(t(ID), L, T, AncestorList, _GetTriePredicate, Childs):- 1633 nonvar(ID), 1634 atomic(L), 1635 nonvar(AncestorList), 1636 nonvar(T), !, 1637 (problog_flag(refine_anclst, true) -> 1638 (problog_flag(anclst_represent, list) -> 1639 ord_intersection(AncestorList, Childs, RefinedAncestorList) 1640 ; 1641 RefinedAncestorList is AncestorList /\ Childs 1642 ) 1643 ; 1644 RefinedAncestorList = AncestorList 1645 ), 1646 recordz(problog_trie_table, get_step_from_id(ID, L, T, RefinedAncestorList, Childs), _). 1647get_set_trie_from_id(t(ID), L, T, SuperSetAncestorList, _GetTriePredicate, Childs):- 1648% (clause(theo,_) ->writeln(get_set_trie_from_id(t(ID), L, T, SuperSetAncestorList, _GetTriePredicate, Childs));true), 1649 recorded(problog_trie_table, get_step_from_id(ID, L, T, AncestorList, StoredChilds), _), 1650 (problog_flag(refine_anclst, true) -> 1651 StoredChilds = Childs 1652 ; 1653 true 1654 ), 1655 (problog_flag(subset_check, true) -> 1656 (problog_flag(anclst_represent, list) -> 1657 subset(AncestorList, SuperSetAncestorList) 1658 ; 1659 AncestorList is AncestorList /\ SuperSetAncestorList 1660% writeln(hi) 1661 ) 1662 ; 1663 AncestorList = SuperSetAncestorList 1664 ), !. 1665get_set_trie_from_id(t(ID), _L, T, _SuperSetAncestorList, _GetTriePredicate, _):- 1666 recorded(problog_trie_table, get_step_from_id(ID, _, T, _AncestorList, _Childs), _), !. 1667get_set_trie_from_id(t(ID), _L, T, _AncestorList, Module:GetTriePredicate, _):- 1668 Goal =.. [GetTriePredicate, ID, T], 1669 call(Module:Goal). 1670 1671trie_replace_entry(_Trie, Entry, _E, false):- 1672 !, trie_remove_entry(Entry). 1673trie_replace_entry(Trie, Entry, E, true):- 1674 !, trie_get_entry(Entry, Proof), 1675 delete(Proof, E, NewProof), 1676 (NewProof = [] -> 1677 trie_delete(Trie), 1678 trie_put_entry(Trie, [true], _) 1679 ; 1680 trie_remove_entry(Entry), 1681 trie_put_entry(Trie, NewProof, _) 1682 ). 1683/*trie_replace_entry(Trie, Entry, E, R):- 1684 trie_get_entry(Entry, List), 1685 replace_in_list(List, NewProof, E, R), 1686 trie_remove_entry(Entry), 1687 trie_put_entry(Trie, NewProof, _).*/ 1688/*trie_replace_entry(Trie, _Entry, E, R):- 1689 trie_replace_term2(Trie, E, R).*/ 1690trie_replace_entry(Trie, _Entry, t(ID), R):- 1691 trie_replace_nested_trie(Trie, ID, R). 1692 1693 1694 1695 1696trie_replace_term2(Trie, OldTerm, NewTerm):- 1697 trie_dup(Trie, A), 1698 %writeln(trie), 1699 %my_trie_print(A), 1700 trie_delete(Trie), 1701 trie_replace_term(A, Trie, OldTerm, NewTerm), 1702 trie_close(A). 1703 1704trie_delete(Trie):- 1705 trie_traverse(Trie, R), 1706 trie_remove_entry(R), 1707 fail. 1708trie_delete(_Trie). 1709 1710trie_replace_term(Trie, NewTrie, OldTerm, NewTerm):- 1711 trie_traverse(Trie, R), 1712 trie_get_entry(R, L), 1713 replace_in_list(L, NL, OldTerm, NewTerm), 1714 trie_put_entry(NewTrie, NL, _), 1715 fail. 1716trie_replace_term(_Trie, _NewTrie, _OldTerm, _NewTerm). 1717 1718replace_in_list([],[],_,_):-!. 1719replace_in_list([H|T], [N|NT], H, N):- 1720 !, replace_in_list(T, NT, H, N). 1721replace_in_list([H|T], [NH|NT], R, N):- 1722 functor(H, _, 1), !, 1723 replace_in_functor(H, NH, R, N), 1724 replace_in_list(T, NT, R, N). 1725replace_in_list([H|T], [H|NT], R, N):- 1726 replace_in_list(T, NT, R, N). 1727replace_in_functor(F, NF, T, R):- 1728 F =.. L, 1729 replace_in_list(L, NL, T, R), 1730 NF =.. NL. 1731 1732 1733 1734trie_write(T, MAXL):- 1735 atomic_concat('L', MAXLA, MAXL), 1736 atom_number(MAXLA, MAXLN), 1737 trie_traverse(T, R), 1738 trie_get_entry(R, L), 1739 %write(user_output, L),nl(user_output), 1740 (dnfbddformat(L, MAXLN) -> 1741 true 1742 ; 1743 write(user_error, warning(L, not_processed)), nl(user_error) 1744 ), 1745 fail. 1746trie_write(_, _). 1747 1748dnfbddformat(depth(T, L), MAXL):- 1749 atomic_concat('L', LA, L), 1750 atom_number(LA, LN), 1751 MAXL >= LN, 1752 seperate(T, Li, V), 1753 %sort(Li, SL), 1754 %reverse(SL, RSL), 1755 append(Li, V, R), 1756 bddlineformat(R, L, ' * '), 1757 forall(deref(I, L), ( 1758 atomic_concat('L', D, I), 1759 write('D'), write(D), nl 1760 )). 1761dnfbddformat(breadth(T, L), MAXL):- 1762 atomic_concat('L', LA, L), 1763 atom_number(LA, LN), 1764 MAXL >= LN, 1765 seperate(T, Li, V), 1766 %sort(Li, SL), 1767 %reverse(SL, RSL), 1768 append(V, Li, R), 1769 bddlineformat(R, L, ' + '), 1770 forall(deref(I, L), ( 1771 atomic_concat('L', D, I), 1772 write('D'), write(D), nl 1773 )). 1774 1775 1776bddlineformat([not(H)|T], O):- 1777 write('~'), !, 1778 bddlineformat([H|T], O). 1779bddlineformat([H], _O):- 1780 (is_label(H) -> 1781 Var = H 1782 ; 1783 get_var_name(H, Var) 1784 ), 1785 write(Var), nl, !. 1786bddlineformat([H|T], O):- 1787 (is_label(H) -> 1788 Var = H 1789 ; 1790 get_var_name(H, Var) 1791 ), 1792 write(Var), write(O), 1793 bddlineformat(T, O). 1794 1795/* 1796bddlineformat([not(H)], O):- 1797 !, write('~'), 1798 bddlineformat([H], O). 1799bddlineformat([H], _O):-!, 1800 (is_label(H) -> 1801 VarName = H 1802 ; 1803 get_var_name(H, VarName) 1804 ), 1805 write(VarName), nl. 1806bddlineformat([not(H)|T], O):- 1807 !, write('~'), 1808 bddlineformat([H|T], O). 1809bddlineformat([H|T], O):- 1810 (is_label(H) -> 1811 VarName = H 1812 ; 1813 get_var_name(H, VarName) 1814 ), 1815 write(VarName), write(O), 1816 bddlineformat(T, O).*/ 1817 1818bddlineformat(T, L, O):- 1819 (is_label(L) -> 1820 write(L), write(' = '), 1821 bddlineformat(T, O) 1822 ; 1823 write(user_output,bdd_script_error([L,T,O])),nl(user_output) 1824 ). 1825 1826is_label(not(L)):- 1827 !, is_label(L). 1828is_label(Label):- 1829 atom(Label), 1830 atomic_concat('L', _, Label). 1831 1832isnestedtrie(not(T)):- 1833 !, isnestedtrie(T). 1834isnestedtrie(t(_T)). 1835 1836seperate([], [], []). 1837seperate([H|T], [H|Labels], Vars):- 1838 is_label(H), !, 1839 seperate(T, Labels, Vars). 1840seperate([H|T], Labels, [H|Vars]):- 1841 seperate(T, Labels, Vars). 1842 1843 1844ptree_decomposition(Trie, BDDFileName, VarFileName) :- 1845 tmpnam(TmpFile1), 1846 nb_setval(next_inter_step, 1), 1847 variables_in_dbtrie(Trie, T), 1848 1849 length(T, VarCnt), 1850 tell(VarFileName), 1851 bdd_vars_script(T), 1852 told, 1853 tell(TmpFile1), 1854 decompose_trie(Trie, T, L), 1855 (is_label(L)-> 1856 atomic_concat('L', LCnt, L), 1857 write(L),nl 1858 ; 1859 LCnt = 1, 1860 write('L1 = '), 1861 (L == false -> 1862 write('FALSE') 1863 ; 1864 write(L) 1865 ), nl, 1866 write('L1'), nl 1867 ), 1868 told, 1869 prefix_bdd_file_with_header(BDDFileName,VarCnt,LCnt,TmpFile1). 1870 1871get_next_inter_step(I):- 1872 nb_getval(next_inter_step, I), 1873 NI is I + 1, 1874 nb_setval(next_inter_step, NI). 1875 1876decompose_trie(Trie, _, false):- 1877 empty_ptree(Trie), !. 1878 1879decompose_trie(Trie, _, 'TRUE'):- 1880 trie_check_entry(Trie, [true], _R),!. 1881 1882decompose_trie(Trie, [H|[]], Var):- 1883 trie_usage(Trie, 1, _, _), 1884 get_var_name(H, VarA), 1885 trie_check_entry(Trie, [L], _R), 1886 (not(H) == L -> 1887 Var = not(VarA) 1888 , 1889 Var = VarA 1890 ), 1891 !. 1892 1893decompose_trie(Trie, [H|_T], L3):- 1894 trie_open(TrieWith), 1895 trie_open(TrieWithNeg), 1896 trie_open(TrieWithOut), 1897 trie_seperate(Trie, H, TrieWith, TrieWithNeg, TrieWithOut), 1898 /*trie_print(Trie), 1899 dwriteln('-----------'), 1900 trie_print(TrieWith), 1901 dwriteln('-----------'), 1902 trie_print(TrieWithNeg), 1903 dwriteln('-----------'), 1904 trie_print(TrieWithOut), 1905 dwriteln('-----------'),*/ 1906 1907 variables_in_dbtrie(TrieWith, T1), 1908 variables_in_dbtrie(TrieWithNeg, T2), 1909 variables_in_dbtrie(TrieWithOut, T3), 1910 1911 %dwriteln([T1, not(T2), T3]), 1912 1913 decompose_trie(TrieWith, T1, LWith), 1914 trie_close(TrieWith), 1915 1916 decompose_trie(TrieWithNeg, T2, LWithNeg), 1917 trie_close(TrieWithNeg), 1918 1919 decompose_trie(TrieWithOut, T3, LWithOut), 1920 trie_close(TrieWithOut), 1921 1922 get_var_name(H, Var), 1923 %dwriteln([Var, ' * ', LWith, ' + ~', Var, ' * ', LWithNeg, ' + ', LWithOut]), 1924 (LWith == false -> 1925 L1 = false 1926 ; 1927 (Var == 'TRUE' -> 1928 L1 = LWith 1929 ; 1930 (LWith == 'TRUE' -> 1931 L1 = Var 1932 ; 1933 get_next_inter_step(I), 1934 atomic_concat(['L', I], L1), 1935 atomic_concat([L1, ' = ', Var, '*', LWith], W1), 1936 write(W1), nl 1937 ) 1938 ) 1939 ), 1940 (LWithNeg == false -> 1941 L2 = false 1942 ; 1943 (Var == 'TRUE' -> 1944 L2 = false 1945 ; 1946 (LWithNeg == 'TRUE' -> 1947 atomic_concat(['~', Var], L2) 1948 ; 1949 get_next_inter_step(I2), 1950 atomic_concat(['L', I2], L2), 1951 atomic_concat([L2, ' = ~', Var, '*', LWithNeg], W2), 1952 write(W2), nl 1953 ) 1954 ) 1955 ), 1956 (one_true(L1, L2, LWithOut) -> 1957 L3 = 'TRUE' 1958 ; 1959 (all_false(L1, L2, LWithOut)-> 1960 L3 = false 1961 ; 1962 (one_non_false(L1, L2, LWithOut, L3) -> 1963 true 1964 ; 1965 get_next_inter_step(I3), 1966 atomic_concat(['L', I3], L3), 1967 write(L3), write(' = '), 1968 non_false([L1,L2,LWithOut], [First|Rest]), 1969 write(First), 1970 forall(member(NonFalse, Rest), (write('+'), write(NonFalse))), 1971 nl 1972 ) 1973 ) 1974 ). 1975 1976dwriteln(A):- 1977 write(user_error, A),nl(user_error),flush_output. 1978 1979 1980non_false([], []):-!. 1981non_false([H|T], [H|NT]):- 1982 H \== false, 1983 non_false(T, NT). 1984non_false([H|T], NT):- 1985 H == false, 1986 non_false(T, NT). 1987 1988one_true('TRUE', _, _):-!. 1989one_true(_, 'TRUE', _):-!. 1990one_true(_, _, 'TRUE'):-!. 1991 1992all_false(false,false,false). 1993one_non_false(L, false, false, L):- 1994 L \== false, !. 1995one_non_false(false, L, false, L):- 1996 L \== false, !. 1997one_non_false(false, false, L, L):- 1998 L \== false, !. 1999 2000trie_seperate(Trie, Var, TrieWith, TrieWithNeg, TrieWithOut):- 2001 trie_traverse(Trie, R), 2002 trie_get_entry(R, Proof), 2003 (memberchk(Var, Proof) -> 2004 remove_from_list(Var, Proof, NProof), 2005 (NProof == [] -> 2006 trie_put_entry(TrieWith, [true], _) 2007 ; 2008 trie_put_entry(TrieWith, NProof, _) 2009 ) 2010 ; 2011 (memberchk(not(Var), Proof) -> 2012 remove_from_list(not(Var), Proof, NProof), 2013 (NProof == [] -> 2014 trie_put_entry(TrieWithNeg, [true], _) 2015 ; 2016 trie_put_entry(TrieWithNeg, NProof, _) 2017 ) 2018 ; 2019 trie_put_entry(TrieWithOut, Proof, _) 2020 ) 2021 ), 2022 fail. 2023trie_seperate(_Trie, _Var, _TrieWith, _TrieWithNeg, _TrieWithOut). 2024 2025remove_from_list(_E, [], []):-!. 2026remove_from_list(E, [E|T], NT):- 2027 !, remove_from_list(E, T, NT). 2028remove_from_list(E, [A|T], [A|NT]):- 2029 remove_from_list(E, T, NT). 2030 2031ptree_db_trie_opt_performed(LVL1, LVL2, LVL3):- 2032 trie_get_depth_breadth_reduction_opt_level_count(1, LVL1), 2033 trie_get_depth_breadth_reduction_opt_level_count(2, LVL2), 2034 trie_get_depth_breadth_reduction_opt_level_count(3, LVL3). 2035 2036:- dynamic(deref/2). 2037 2038mark_for_deref(DB_Trie):- 2039 traverse_ptree_mode(OLD), 2040 traverse_ptree_mode(backward), 2041 mark_deref(DB_Trie), 2042 traverse_ptree_mode(OLD). 2043 2044mark_deref(DB_Trie):- 2045 traverse_ptree(DB_Trie, DB_Term), 2046 (DB_Term = depth(List, Inter); DB_Term = breadth(List, Inter)), 2047 member(L, List), 2048 ((is_label(L), \+ deref(L, _)) -> 2049 asserta(deref(L, Inter)) 2050 ; 2051 true 2052 ), 2053 fail. 2054mark_deref(_). 2055