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
  184print_model(Model, Options) :-
  185    model_hook(Model, Options),
  186    !.
  187print_model(_:Model, Options) :-
  188    (   option(width(Width), Options)
  189    ->  true
  190    ;   catch(tty_size(_, Width), _, Width = 80)
  191    ),
  192    layout(Model, Width, Layout),
  193    compound_name_arguments(Array, v, Model),
  194    format('{ ', []),
  195    print_table(0, Array, Layout.put(_{ sep:',',
  196                                        end:'\n}',
  197                                        prefix:'  ',
  198                                        options:Options
  199                                      })).
  200
  201print_table(I, Array, Layout) :-
  202    Cols = Layout.cols,
  203    Rows = Layout.rows,
  204    Row is I // Cols,
  205    Col is I mod Cols,
  206    Index is Row + Col * Rows + 1,
  207
  208    % If the next index is outside, we need a newline.  If we are
  209    % also on the last row we have the very last element
  210    (   NIndex is Row + (Col+1) * Rows + 1,
  211        functor(Array, _, LastIndex),
  212        NIndex =< LastIndex
  213    ->  NL = false,
  214        Last = false
  215    ;   NL = true,
  216        (   Row+1 =:= Rows
  217        ->  Last = true
  218        ;   Last = false
  219        )
  220    ),
  221
  222    % If we are not the last on the line and not the last, print the
  223    % cell, padding to the column with and followed by a separator (,)
  224    % Else we print withput padding either a separator or the end.
  225    (   arg(Index, Array, Atom)
  226    ->  (   NL == false,
  227            Last == false
  228        ->  format('~|~@~w~t~*+',
  229                   [print_model_term(Atom, Layout.options),
  230                    Layout.sep, Layout.col_width])
  231        ;   Last == false
  232        ->  format('~@~w', [print_model_term(Atom, Layout.options), Layout.sep])
  233        ;   format('~@~w', [print_model_term(Atom, Layout.options), Layout.end])
  234        ),
  235        Print = true
  236    ;   true
  237    ),
  238
  239    % Emit a newline if this is the last one on the line and we printed this
  240    % cell.
  241    (   Last == true
  242    ->  true
  243    ;   (   Print == true, NL == true
  244        ->  format('~n~w', [Layout.prefix])
  245        ;   true
  246        ),
  247        I2 is I+1,
  248        print_table(I2, Array, Layout)
  249    ).
  250
  251layout(Atoms, Width, _{cols:Cols, rows:Rows, col_width:ColWidth}) :-
  252    length(Atoms, L),
  253    longest(Atoms, Longest),
  254    Cols0 is max(1, Width // (Longest + 3)),
  255    Rows is ceiling(L / Cols0),
  256    Cols is ceiling(L/Rows),
  257    ColWidth is min(Longest+3, Width // Cols).
  258
  259longest(List, Longest) :-
  260    longest(List, 0, Longest).
  261
  262longest([], M, M) :- !.
  263longest([H|T], Sofar, M) :-
  264    write_length(H, Length,
  265                 [ portray(true),
  266                   numbervars(true),
  267                   quoted(true)
  268                 ]),
  269    Length >= Sofar,
  270    !,
  271    longest(T, Length, M).
  272longest([_|T], S, M) :-
  273    longest(T, S, M)