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.
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 ).
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 ).
not(positive)not(-positive).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.
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 = [].
165unqualify_model(Model0, Module, Model) :-
166 maplist(unqualify_model_term(Module), Model0, Model).Model terms are printed in columns. E.g., for a 10 atom model and 4 columns we get:
1 4 7 10 2 5 8 3 6 9
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)
sCASP model handling
*/