1:- module(scasp_stack, 2 [ justification_tree/3, % :Stack, -JustTree, +Options 3 print_justification_tree/1, % :JustTree 4 print_justification_tree/2, % :JustTree, +Options 5 unqualify_justitication_tree/3 % +TreeIn, +Module, -TreeOut 6 ]). 7:- use_module(predicates). 8:- use_module(common). 9:- use_module(modules). 10:- use_module(output). 11 12:- autoload(library(apply), [maplist/3]). 13:- autoload(library(lists), [reverse/2, append/3]). 14:- autoload(library(option), 15 [option/2, merge_options/3, option/3, select_option/3]). 16 17:- meta_predicate 18 justification_tree(, , ), 19 print_justification_tree(), 20 print_justification_tree(, ). 21 22:- multifile 23 justification_tree_hook/2.
<none yet>
The tree format is defined as follows.
Node-Children, where Node
is an atom (in the logical sense) and Children is
a (possibly empty) list of sub-trees that justify the
Node.chs(Node)).
The root node has the atom query and has two children: the actual
query and the atom o_nmr_check which represents the global
constraints.
56:- det(justification_tree/3). 57 58justification_tree(M:Stack, M:JustificationTree, Options) :- 59 reverse(Stack, RevStack), 60 stack_tree([query|RevStack], Trees), 61 filter_tree(Trees, M, [JustificationTree], Options).
[] indicates
this branch is complete. Here are some examples
[p, []] p-[] [p, q, [], []] p-[q-[]] [p, q, [], r, [], []] p-[q-[],r-[]]
We maintain a stack of difference lists in the 4th argument.
On encountering a [] we pop this stack.
76stack_tree(Stack, Tree) :- 77 stack_tree(Stack, Tree, [], []). 78 79stack_tree([], Children0, Children, []) => 80 Children = Children0. 81stack_tree([[]|Stack], Children0, Children, [T0/T|Parents]) => 82 Children = Children0, 83 stack_tree(Stack, T0, T, Parents). 84stack_tree([H|Stack], Tree, T, Parents) => 85 Tree = [H-Children|T0], 86 stack_tree(Stack, Children, [], [T0/T|Parents]).
not(_) nodes from the tree.98filter_tree([],_,[], _) :- !. 99filter_tree([goal_origin(_,_)-[_,goal_origin(Abd, O)-_]|Cs], 100 M, 101 [goal_origin(abduced(Atom), O)-[]|Fs], Options) :- 102 abduction_justification(Abd, Atom), 103 !, 104 filter_tree(Cs, M, Fs, Options). 105filter_tree([proved(Abd)-[]|Cs], 106 M, 107 [proved(Atom)-[]|Fs], Options) :- 108 abduction_justification(Abd, Atom), 109 !, 110 filter_tree(Cs, M, Fs, Options). 111filter_tree([goal_origin(Term0,O)-Children|Cs], M, Tree, Options) :- 112 filter_pos(Term0, Options), 113 raise_negation(Term0, Term), 114 selected(Term, M), !, 115 filter_tree(Children, M, FChildren, Options), 116 Tree = [goal_origin(Term, O)-FChildren|Fs], 117 filter_tree(Cs, M, Fs, Options). 118filter_tree([Term0-Children|Cs], M, Tree, Options) :- 119 filter_pos(Term0, Options), 120 raise_negation(Term0, Term), 121 selected(Term, M), !, 122 filter_tree(Children, M, FChildren, Options), 123 ( Term == o_nmr_check, FChildren == [] 124 -> Tree = Fs 125 ; Tree = [Term-FChildren|Fs] 126 ), 127 filter_tree(Cs, M, Fs, Options). 128filter_tree([_-Childs|Cs], M, FilterChildren, Options) :- 129 append(Childs, Cs, AllCs), 130 filter_tree(AllCs, M, FilterChildren, Options).
--pos is active. We should not
filter the global constraint nodes.137filter_pos(not(GC), _Options), is_global_constraint(GC) => 138 true. 139filter_pos(not(_), Options) => 140 \+ option(pos(true), Options). 141filter_pos(_, _) => 142 true. 143 144selected(query, _) => true. 145selected(proved(_), _) => true. 146selected(chs(_), _) => true. 147selected(assume(_), _) => true. 148selected(not(-Goal), _) => 149 \+ aux_predicate(Goal). 150selected(not(Goal), _) => 151 \+ aux_predicate(Goal). 152selected(-(Goal), M) => 153 selected(Goal, M). 154selected(findall(_,_,_), _) => true. 155selected(is(_,_), _) => true. 156selected(_>_, _) => true. 157selected(_>=_, _) => true. 158selected(_<_, _) => true. 159selected(_=<_, _) => true. 160selected(Goal, M) => 161 ( aux_predicate(Goal) 162 -> fail 163 ; ( current_predicate(M:pr_user_predicate/1) 164 -> user_predicate(M:Goal) 165 ; true 166 ) 167 -> true 168 ; is_global_constraint(Goal) 169 ). 170 171aux_predicate(-(o_,_)) :- !. % copied from io.pl 172aux_predicate(A) :- 173 functor(A, Name, _Arity), 174 sub_atom(Name, 0, _, _, o_), 175 \+ is_global_constraint(Name). 176 177is_global_constraint(o_nmr_check) :- 178 !. 179is_global_constraint(Atom) :- 180 atom(Atom), 181 atom_concat(o_chk_, NA, Atom), 182 atom_number(NA, _). 183 184 185abduction_justification(Abd, Atom) :- 186 Abd =.. [F, Atom], 187 abduction_justification_(F). 188 189abduction_justification_(F) :- 190 sub_atom(F, _, _, 0, 'abducible$'), 191 !. 192abduction_justification_(abducible).
unicode (default) or ascii.false,
it ends with the last atom.212print_justification_tree(Tree) :- 213 print_justification_tree(Tree, []). 214 215:- det(print_justification_tree/2). 216 217print_justification_tree(Tree, Options) :- 218 justification_tree_hook(Tree, Options), 219 !. 220print_justification_tree(M:Tree, Options) :- 221 merge_options(Options, [depth(0),module(M)], Options1), 222 plain_output(Tree, Options1), 223 ( option(full_stop(true), Options, true) 224 -> format(".~n", []) 225 ; true 226 ).
230plain_output(goal_origin(Term, _)-Children, Options) :- 231 !, 232 plain_output(Term-Children, Options). 233plain_output(Term-[], Options) :- 234 !, 235 option(depth(D), Options), 236 Indent is D*3, 237 nl_indent(Indent), 238 term(Term, Options). 239plain_output(Term-Children, Options) :- 240 !, 241 select_option(depth(D), Options, Options1), 242 option(indent(Width), Options1, 3), 243 Indent is D*Width, 244 connector(implies, Conn, Options), 245 nl_indent(Indent), term(Term, Options), format(" ~w",[Conn]), 246 D1 is D+1, 247 plain_output_children(Children, [depth(D1)|Options1]). 248 249nl_indent(Indent) :- 250 format('~N~t~*|', [Indent]). 251 252plain_output_children([A,B|Rs], Options) :- 253 !, 254 plain_output(A, Options), 255 connector(and, Conn, Options), 256 format("~w",[Conn]), 257 plain_output_children([B|Rs], Options). 258plain_output_children([A], Options) :- 259 !, 260 plain_output(A, Options).
266term(proved(Term), Options) => 267 term1(proved, Term, Options). 268term(assume(Term), Options) => 269 term1(assume, Term, Options). 270term(chs(Term), Options) => 271 term1(chs, Term, Options). 272term(Term, Options) => 273 print_model_term(Term, Options). 274 275term1(Functor, Arg, Options) :- 276 print_connector(Functor, Options), 277 format('(', []), 278 print_model_term(Arg, Options), 279 format(')', []).
286:- det(unqualify_justitication_tree/3). 287 288unqualify_justitication_tree(_:Tree0, Module, Tree) :- 289 is_list(Tree0), 290 !, 291 maplist(unqualify_just(Module), Tree0, Tree). 292unqualify_justitication_tree(_:Tree0, Module, Tree) :- 293 unqualify_just(Module, Tree0, Tree). 294 295unqualify_just(M, Node0-Children0, Node-Children) :- 296 unqualify_model_term(M, Node0, Node), 297 maplist(unqualify_just(M), Children0, Children)