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.forall() and intermediate nodes.100filter_tree(Tree, _, Tree, Options) :- 101 option(long(true), Options), !. 102filter_tree([],_,[], _) :- !. 103filter_tree([goal_origin(Atom0,_)-[goal_origin(Abd, O)-_]|Cs], 104 M, 105 [goal_origin(abduced(Atom), O)-[]|Fs], Options) :- 106 abduction_justification(Abd), 107 !, 108 raise_negation(Atom0, Atom), 109 filter_tree(Cs, M, Fs, Options). 110filter_tree([ proved(Atom0)-[], 111 not(_Neg)-[ not(_) - [proved(not(Abd))-[]]]], 112 _M, 113 [abduced(Atom)-[]], _Options) :- 114 abduction_justification(Abd), 115 !, 116 raise_negation(Atom0, Atom). 117filter_tree([ not(Atom0)-[not(_Neg)-[proved(not(Abd))-[]]]], 118 _M, 119 [abduced(Atom)-[]], _Options) :- 120 raise_negation(Atom0, Atom1), 121 neg(Atom1, Atom), 122 abduction_justification(Abd), 123 !. 124filter_tree([goal_origin(Term0,O)-Children|Cs], M, Tree, Options) :- 125 filter_pos(Term0, Options), 126 raise_negation(Term0, Term), 127 selected(Term, M), !, 128 filter_tree(Children, M, FChildren, Options), 129 Tree = [goal_origin(Term, O)-FChildren|Fs], 130 filter_tree(Cs, M, Fs, Options). 131filter_tree([Term0-Children|Cs], M, Tree, Options) :- 132 filter_pos(Term0, Options), 133 raise_negation(Term0, Term), 134 selected(Term, M), !, 135 filter_tree(Children, M, FChildren, Options), 136 ( Term == o_nmr_check, FChildren == [] 137 -> Tree = Fs 138 ; Tree = [Term-FChildren|Fs] 139 ), 140 filter_tree(Cs, M, Fs, Options). 141filter_tree([_-Childs|Cs], M, FilterChildren, Options) :- 142 append(Childs, Cs, AllCs), 143 filter_tree(AllCs, M, FilterChildren, Options). 144 145neg(-A, Neg) => Neg = A. 146neg(A, Neg) => Neg = -A.
--pos is active. We should not
filter the global constraint nodes.153filter_pos(not(GC), _Options), is_global_constraint(GC) => 154 true. 155filter_pos(not(_), Options) => 156 \+ option(pos(true), Options). 157filter_pos(_, _) => 158 true. 159 160selected(query, _) => true. 161selected(proved(_), _) => true. 162selected(chs(_), _) => true. 163selected(assume(_), _) => true. 164selected(not(-Goal), _) => 165 \+ aux_predicate(Goal). 166selected(not(Goal), _) => 167 \+ aux_predicate(Goal). 168selected(-(Goal), M) => 169 selected(Goal, M). 170selected(findall(_,_,_), _) => true. 171selected(is(_,_), _) => true. 172selected(_>_, _) => true. 173selected(_>=_, _) => true. 174selected(_<_, _) => true. 175selected(_=<_, _) => true. 176selected(Goal, M) => 177 ( aux_predicate(Goal) 178 -> fail 179 ; ( current_predicate(M:pr_user_predicate/1) 180 -> user_predicate(M:Goal) 181 ; true 182 ) 183 -> true 184 ; is_global_constraint(Goal) 185 ). 186 187aux_predicate(-(o_,_)) :- !. % copied from io.pl 188aux_predicate(A) :- 189 functor(A, Name, _Arity), 190 sub_atom(Name, 0, _, _, o_), 191 \+ is_global_constraint(Name). 192 193is_global_constraint(o_nmr_check) :- 194 !. 195is_global_constraint(Atom) :- 196 atom(Atom), 197 atom_concat(o_chk_, NA, Atom), 198 atom_number(NA, _). 199 200 201abduction_justification(Abd) :- 202 atom(Abd), 203 sub_atom(Abd, _, _, _, ':abducible$'), 204 !.
unicode (default) or ascii.false,
it ends with the last atom.224print_justification_tree(Tree) :- 225 print_justification_tree(Tree, []). 226 227:- det(print_justification_tree/2). 228 229print_justification_tree(Tree, Options) :- 230 justification_tree_hook(Tree, Options), 231 !. 232print_justification_tree(M:Tree, Options) :- 233 merge_options(Options, [depth(0),module(M)], Options1), 234 plain_output(Tree, Options1), 235 ( option(full_stop(true), Options, true) 236 -> format(".~n", []) 237 ; true 238 ).
242plain_output(goal_origin(Term, _)-Children, Options) :- 243 !, 244 plain_output(Term-Children, Options). 245plain_output(Term-[], Options) :- 246 !, 247 option(depth(D), Options), 248 Indent is D*3, 249 nl_indent(Indent), 250 term(Term, Options). 251plain_output(Term-Children, Options) :- 252 !, 253 select_option(depth(D), Options, Options1), 254 option(indent(Width), Options1, 3), 255 Indent is D*Width, 256 connector(implies, Conn, Options), 257 nl_indent(Indent), term(Term, Options), format(" ~w",[Conn]), 258 D1 is D+1, 259 plain_output_children(Children, [depth(D1)|Options1]). 260 261nl_indent(Indent) :- 262 format('~N~t~*|', [Indent]). 263 264plain_output_children([A,B|Rs], Options) :- 265 !, 266 plain_output(A, Options), 267 connector(and, Conn, Options), 268 format("~w",[Conn]), 269 plain_output_children([B|Rs], Options). 270plain_output_children([A], Options) :- 271 !, 272 plain_output(A, Options).
278term(proved(Term), Options) => 279 term1(proved, Term, Options). 280term(assume(Term), Options) => 281 term1(assume, Term, Options). 282term(chs(Term), Options) => 283 term1(chs, Term, Options). 284term(Term, Options) => 285 print_model_term(Term, Options). 286 287term1(Functor, Arg, Options) :- 288 print_connector(Functor, Options), 289 format('(', []), 290 print_model_term(Arg, Options), 291 format(')', []).
298:- det(unqualify_justitication_tree/3). 299 300unqualify_justitication_tree(_:Tree0, Module, Tree) :- 301 is_list(Tree0), 302 !, 303 maplist(unqualify_just(Module), Tree0, Tree). 304unqualify_justitication_tree(_:Tree0, Module, Tree) :- 305 unqualify_just(Module, Tree0, Tree). 306 307unqualify_just(M, Node0-Children0, Node-Children) :- 308 unqualify_model_term(M, Node0, Node), 309 maplist(unqualify_just(M), Children0, Children)