1/*  Part of sCASP
    2
    3    Author:        Jan Wielemaker
    4    E-mail:        jan@swi-prolog.org
    5    Copyright (c)  2021, SWI-Prolog Solutions b.v.
    6    All rights reserved.
    7
    8    Redistribution and use in source and binary forms, with or without
    9    modification, are permitted provided that the following conditions
   10    are met:
   11
   12    1. Redistributions of source code must retain the above copyright
   13       notice, this list of conditions and the following disclaimer.
   14
   15    2. Redistributions in binary form must reproduce the above copyright
   16       notice, this list of conditions and the following disclaimer in
   17       the documentation and/or other materials provided with the
   18       distribution.
   19
   20    THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
   21    "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
   22    LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
   23    FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
   24    COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
   25    INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
   26    BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
   27    LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
   28    CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
   29    LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
   30    ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
   31    POSSIBILITY OF SUCH DAMAGE.
   32*/
   33
   34:- module(scasp_model,
   35          [ canonical_model/2,          % +RawModel, -Canonical
   36            unqualify_model/3,          % +ModelIn, +Module, -ModelOut
   37            print_model/2               % :Model, +Options
   38          ]).   39:- use_module(library(apply)).   40:- use_module(library(lists)).   41:- use_module(library(pairs)).   42
   43:- use_module(common).   44:- use_module(modules).   45:- use_module(output).   46
   47:- meta_predicate
   48    canonical_model(:, -),
   49    print_model(:, +).   50
   51:- multifile
   52    model_hook/2.   53
   54/** <module> sCASP model handling
   55
   56
   57*/
   58
   59%!  canonical_model(:RawModel, -Canonical)
   60
   61canonical_model(M:Model, CanModel) :-
   62    flatten(Model, FlatModel),
   63    exclude(nonmodel_term, FlatModel, Model1),
   64    sort(Model1, Unique),
   65    maplist(raise_negation, Unique, Raised),
   66    filter_shown(M, Raised, Filtered),
   67    sort_model(Filtered, Sorted),
   68    simplify_model(Sorted, CanModel).
   69
   70nonmodel_term(abducible(_)).
   71nonmodel_term(proved(_)).
   72nonmodel_term(chs(_)).
   73nonmodel_term(o_nmr_check).
   74nonmodel_term(not(X)) :-
   75    nonvar(X),
   76    !,
   77    nonmodel_term(X).
   78nonmodel_term(Term) :-
   79    functor(Term, Name, _),
   80    (   sub_atom(Name, 0, _, _, 'o_')
   81    ->  true
   82    ;   sub_atom(Name, _, _, 0, '$')
   83    ).
   84
   85%!  filter_shown(+Module, +Model, -Shown) is det.
   86%
   87%   Handle the show/1 directives.  All  terms   are  shown  for a target
   88%   module if pr_show_predicate/1  is  not   defined  for  that  module.
   89%   Otherwise the terms associated with the   module  are filtered using
   90%   pr_show_predicate/1.
   91
   92filter_shown(M, Model, Shown) :-
   93    maplist(tag_module(M), Model, Tagged),
   94    maplist(arg(1), Tagged, Modules),
   95    sort(Modules, Unique),
   96    include(has_shown, Unique, Filter),
   97    (   Filter == []
   98    ->  Shown = Model
   99    ;   convlist(do_show(Filter), Tagged, Shown)
  100    ).
  101
  102tag_module(M, Term, t(Q, Unqualified, Term)) :-
  103    model_term_module(M:Term, Q),
  104    unqualify_model_term(Q, Term, Unqualified).
  105
  106has_shown(Module) :-
  107    clause(Module:pr_show_predicate(_), _),
  108    !.
  109
  110do_show(Filter, t(M,Unqualified,Term), Term) :-
  111    (   memberchk(M, Filter)
  112    ->  M:pr_show_predicate(Unqualified)
  113    ;   true
  114    ).
  115
  116%!  sort_model(+ModelIn, -Sorted) is det.
  117%
  118%   Sort the model by literal, getting   affirming and denying knowledge
  119%   about a literal together.  If multiple terms about the same literal
  120%   appear they are ordered:
  121%
  122%     1. positive
  123%     2. not(positive)
  124%     3. -positive
  125%     4. not(-positive).
  126
  127sort_model(ModelIn, Sorted) :-
  128    map_list_to_pairs(literal_key, ModelIn, Pairs),
  129    keysort(Pairs, KSorted),
  130    pairs_values(KSorted, Sorted).
  131
  132literal_key(Term, Literal-Flags) :-
  133    literal_key(Term, Literal, 0, Flags).
  134
  135literal_key(not(X), Key, F0, F) =>
  136    literal_key(X, Key, F0, F1),
  137    F is F1+0x1.
  138literal_key(-(X), Key, F0, F) =>
  139    literal_key(X, Key, F0, F1),
  140    F is F1+0x2.
  141literal_key(X, Key, F0, F) =>
  142    Key = X,
  143    F = F0.
  144
  145%!  simplify_model(+ModelIn, -ModelOut) is det.
  146%
  147%   Remove model terms that are entailed by other model terms.
  148
  149simplify_model([not(X0),-X1|T0], M), X0 == X1 =>
  150    M = [-X1|M0],
  151    simplify_model(T0, M0).
  152simplify_model([X0, not(-(X1))|T0], M), X0 == X1 =>
  153    M = [X0|M0],
  154    simplify_model(T0, M0).
  155simplify_model([H|T0], M) =>
  156    M = [H|M0],
  157    simplify_model(T0, M0).
  158simplify_model([], M) =>
  159    M = [].
  160
  161%!  unqualify_model(+ModelIn, +Module, -ModelOut) is det.
  162%
  163%   Restore the model relation to modules.
  164
  165unqualify_model(Model0, Module, Model) :-
  166    maplist(unqualify_model_term(Module), Model0, Model).
  167
  168%!  print_model(:Model, +Options) is det.
  169%
  170%   Print the model in aligned columns.  Options processed:
  171%
  172%     - width(Width)
  173%       Assumed terminal width.  Default from tty_size/2 or 80.
  174%
  175%   Model terms are printed in columns. E.g., for  a 10 atom model and 4
  176%   columns we get:
  177%
  178%   ```
  179%      1  4  7  10
  180%      2  5  8
  181%      3  6  9
  182%   ```
  183
  184:- if(\+current_predicate(tty_size/2)).  185tty_size(25,80).
  186:- endif.  187
  188print_model(Model, Options) :-
  189    model_hook(Model, Options),
  190    !.
  191print_model(_:Model, Options) :-
  192    (   option(width(Width), Options)
  193    ->  true
  194    ;   catch(tty_size(_, Width), _, Width = 80)
  195    ),
  196    layout(Model, Width, Layout),
  197    compound_name_arguments(Array, v, Model),
  198    format('{ ', []),
  199    print_table(0, Array, Layout.put(_{ sep:',',
  200                                        end:'\n}',
  201                                        prefix:'  ',
  202                                        options:Options
  203                                      })).
  204
  205print_table(I, Array, Layout) :-
  206    Cols = Layout.cols,
  207    Rows = Layout.rows,
  208    Row is I // Cols,
  209    Col is I mod Cols,
  210    Index is Row + Col * Rows + 1,
  211
  212    % If the next index is outside, we need a newline.  If we are
  213    % also on the last row we have the very last element
  214    (   NIndex is Row + (Col+1) * Rows + 1,
  215        functor(Array, _, LastIndex),
  216        NIndex =< LastIndex
  217    ->  NL = false,
  218        Last = false
  219    ;   NL = true,
  220        (   Row+1 =:= Rows
  221        ->  Last = true
  222        ;   Last = false
  223        )
  224    ),
  225
  226    % If we are not the last on the line and not the last, print the
  227    % cell, padding to the column with and followed by a separator (,)
  228    % Else we print withput padding either a separator or the end.
  229    (   arg(Index, Array, Atom)
  230    ->  (   NL == false,
  231            Last == false
  232        ->  format('~|~@~w~t~*+',
  233                   [print_model_term(Atom, Layout.options),
  234                    Layout.sep, Layout.col_width])
  235        ;   Last == false
  236        ->  format('~@~w', [print_model_term(Atom, Layout.options), Layout.sep])
  237        ;   format('~@~w', [print_model_term(Atom, Layout.options), Layout.end])
  238        ),
  239        Print = true
  240    ;   true
  241    ),
  242
  243    % Emit a newline if this is the last one on the line and we printed this
  244    % cell.
  245    (   Last == true
  246    ->  true
  247    ;   (   Print == true, NL == true
  248        ->  format('~n~w', [Layout.prefix])
  249        ;   true
  250        ),
  251        I2 is I+1,
  252        print_table(I2, Array, Layout)
  253    ).
  254
  255layout(Atoms, Width, _{cols:Cols, rows:Rows, col_width:ColWidth}) :-
  256    length(Atoms, L),
  257    longest(Atoms, Longest),
  258    Cols0 is max(1, Width // (Longest + 3)),
  259    Rows is ceiling(L / Cols0),
  260    Cols is ceiling(L/Rows),
  261    ColWidth is min(Longest+3, Width // Cols).
  262
  263longest(List, Longest) :-
  264    longest(List, 0, Longest).
  265
  266longest([], M, M) :- !.
  267longest([H|T], Sofar, M) :-
  268    write_length(H, Length,
  269                 [ portray(true),
  270                   numbervars(true),
  271                   quoted(true)
  272                 ]),
  273    Length >= Sofar,
  274    !,
  275    longest(T, Length, M).
  276longest([_|T], S, M) :-
  277    longest(T, S, M)