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
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)
sCASP model handling
*/