| 1 | | % (c) 2009-2025 Lehrstuhl fuer Softwaretechnik und Programmiersprachen, |
| 2 | | % Heinrich Heine Universitaet Duesseldorf |
| 3 | | % This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html) |
| 4 | | :- module(bvisual, |
| 5 | | [ |
| 6 | | get_tree_from_expr/4, |
| 7 | | %get_tree_from_expr2/4, |
| 8 | | write_dot_graph_to_file/2, |
| 9 | | %print_dot_graph/1, |
| 10 | | get_any/5 |
| 11 | | %get_any_most_satisfier/5, |
| 12 | | |
| 13 | | ] |
| 14 | | ). |
| 15 | | |
| 16 | | :- meta_predicate visit_tree(5,3,-,-,-). |
| 17 | | |
| 18 | | :- use_module(probsrc(module_information),[module_info/2]). |
| 19 | | :- module_info(group,dot). |
| 20 | | :- module_info(description,'Generate a dot visualization of B predicates and expressions.'). |
| 21 | | |
| 22 | | :- use_module(library(lists), [maplist/3, scanlist/4]). |
| 23 | | %:- use_module(library(terms)). |
| 24 | | |
| 25 | | :- use_module(probsrc(bsyntaxtree)). |
| 26 | | :- use_module(probsrc(translate), [translate_bvalue_with_limit/3, |
| 27 | | translate_bexpression_with_limit/3]). |
| 28 | | :- use_module(probsrc(kernel_waitflags), [ |
| 29 | | init_wait_flags/2, |
| 30 | | ground_wait_flags/1]). |
| 31 | | |
| 32 | | :- use_module(dotsrc(bvisual_any_maxsolver)). |
| 33 | | :- use_module(probsrc(error_manager)). |
| 34 | | :- use_module(probsrc(preferences)). |
| 35 | | |
| 36 | | |
| 37 | | %:- use_module(probsrc(self_check)). |
| 38 | | |
| 39 | | |
| 40 | | |
| 41 | | % PARAMETERS |
| 42 | | |
| 43 | | max_chars_per_line(40). |
| 44 | | max_lines(10). |
| 45 | | max_chars_total(400). % :- max_chars_per_line(X), max_lines(ML), T is X*ML. |
| 46 | | |
| 47 | | %% |
| 48 | | % Tree format: |
| 49 | | % Trees used by write_dot_graph_to_file/2 are modelled by the bind/3 |
| 50 | | % predicate: |
| 51 | | % bind(Children, NewLocalState, Metas). |
| 52 | | % Children is a list of subexpressions, whose numbers may be greater than two. |
| 53 | | % NewLocalState is a new local state for the subexpressions. |
| 54 | | % Metas are informations about the expression, like value, label etc. |
| 55 | | % |
| 56 | | % Important: Avoid access bind directly since it's structure may |
| 57 | | % be changed. Use accessors defined below. |
| 58 | | % They provide a convenient way to access the meta informations. |
| 59 | | % |
| 60 | | % Use get_tree_from_expr(Tree, Expr, LocalStale, State) to gain |
| 61 | | % a bind based tree from a predicate or expression evaluated in LocalState |
| 62 | | % and State. |
| 63 | | % |
| 64 | | % Use get_tree_from_expr2(State, LocalState, TExpr, Tree) to inspect the |
| 65 | | % predicate or expression only without walking down the children recursively. |
| 66 | | % |
| 67 | | |
| 68 | | %% |
| 69 | | % accessors & shortcuts |
| 70 | | % |
| 71 | | |
| 72 | | create_long_tree_node(bind(Children, Label, Type, Value, LongDesc), |
| 73 | | Children, Label, Type, Value, LongDesc). |
| 74 | | get_tree_node_info(NODE, Children, NewLocalState, Metas) :- |
| 75 | | (create_tree_node(NODE, C,N,M) -> Children=C, NewLocalState=N, Metas=M |
| 76 | | ; add_error(bvisual,'Illegal node: ',NODE)). |
| 77 | | create_tree_node(bind(Children, NewLocalState, Metas), |
| 78 | | Children, NewLocalState, Metas). |
| 79 | | |
| 80 | | |
| 81 | | % bind([],cv_o,nonboolean,137,b(identifier(cv_o),integer,[nodeid(pos(139677,56,192,18,192,21))])) |
| 82 | | |
| 83 | | has_no_children(Node) :- child_nodes(Node,[]). |
| 84 | | |
| 85 | | child_nodes(bind(ChildNodes,_,_,_,_), ChildNodes). |
| 86 | | child_nodes(bind(ChildNodes,_,_), ChildNodes). |
| 87 | | |
| 88 | | label(bind(_,Label,_,_,_), Label). |
| 89 | ? | label(bind(_,_, Metas), Val) :- member(label(Val), Metas),!. |
| 90 | | |
| 91 | | value(bind(_,_,_,Val,_), Val). |
| 92 | ? | value(bind(_,_, Metas), Val) :- member(value(Val), Metas),!. |
| 93 | | |
| 94 | | long_desc(bind(_,_,_,_,Val), Val). |
| 95 | | long_desc(bind(_,_, Metas), Val):- member(long_desc(Val), Metas),!. |
| 96 | | |
| 97 | | is_boolean(bind(_,_,boolean,_,_)). |
| 98 | ? | is_boolean(bind(_,_, Metas)):- member(type(boolean), Metas),!. |
| 99 | | |
| 100 | | %type(bind(_,_, Metas), Val):- member(type(Val), Metas),!. |
| 101 | | |
| 102 | | is_explicit_value_node(Node) :- long_desc(Node,Val), is_explicit_value(Val). |
| 103 | | |
| 104 | | %% |
| 105 | | % Evaluate an expression and it's subexpressions and |
| 106 | | % gain their values as a tree. |
| 107 | | % |
| 108 | | :- use_module(probsrc(tools),[catch_call/1]). |
| 109 | | :- use_module(probsrc(b_global_sets),[add_prob_deferred_set_elements_to_store/3]). |
| 110 | | |
| 111 | | |
| 112 | | get_tree_from_expr(Tree, Expr, LocalState, State) :- |
| 113 | | ground_store(LocalState), ground_store(State), |
| 114 | | write(State),nl,write(LocalState),nl,nl, |
| 115 | | (get_tree_from_expr0(R, Expr, LocalState, State) -> Tree=R |
| 116 | | ; add_error(bvisual,'Failed to construct formula visualisation:',Expr), |
| 117 | | Tree = bind([],'FAILED TO CONSTRUCT TREE',error,'UNKNOWN','UNKNOWN') |
| 118 | | ). |
| 119 | | |
| 120 | | % ground store, to ensure that no variables are left free; should normally not be necessary |
| 121 | | % if we have free variables we get confusing visualisations, where different values are chosen for different subformulas |
| 122 | | ground_store([]). |
| 123 | | ground_store([bind(_,Val)|T]) :- ground_to_any_value(Val), ground_store(T). |
| 124 | | |
| 125 | | :- use_module(probsrc(b_global_sets),[b_get_fd_type_bounds/3]). |
| 126 | | ground_to_any_value([H|T]) :- !, ground_to_any_value(H), ground_to_any_value(T). |
| 127 | | ground_to_any_value((A,B)) :- !, ground_to_any_value(A), ground_to_any_value(B). |
| 128 | | ground_to_any_value(fd(X,Type)) :- var(X),!, b_get_fd_type_bounds(Type,Low,_),X=Low. |
| 129 | | ground_to_any_value(int(X)) :- var(X),!, X=0. |
| 130 | | ground_to_any_value(term(floating(X))) :- var(X),!, X=0.0. |
| 131 | | ground_to_any_value(string(X)) :- var(X),!, X='some_string'. |
| 132 | | ground_to_any_value(rec(Fields)) :- !, ground_to_any_value(Fields). |
| 133 | | ground_to_any_value(field(_,V)) :- !, ground_to_any_value(V). |
| 134 | | % TO DO: free types |
| 135 | | ground_to_any_value(_). |
| 136 | | |
| 137 | | |
| 138 | | get_tree_from_expr0(Tree, Expr, LocalState, State) :- |
| 139 | | temp_set_prefs(CHNG), |
| 140 | | add_prob_deferred_set_elements_to_store(State,State1,visible), |
| 141 | | call_cleanup(catch_call(get_tree_from_expr3(State1, LocalState, Expr, Tree)), |
| 142 | | reset_prefs(CHNG)). |
| 143 | | % catch: as this can sometimes generate resource_error(memory) error exceptions |
| 144 | | |
| 145 | | temp_set_prefs([CHNG,Level]) :- |
| 146 | | enter_new_clean_error_scope(Level), |
| 147 | | (get_preference(dot_use_unicode,true) -> translate:set_unicode_mode ; true), |
| 148 | | temporary_set_preference(raise_abort_immediately,false,CHNG). |
| 149 | | reset_prefs([CHNG,Level]) :- |
| 150 | | clear_events_in_error_scope(Level,_), % avoid errors propagating into outside |
| 151 | | exit_error_scope(Level,_ErrOccured,bvisual), |
| 152 | | reset_temporary_preference(raise_abort_immediately, CHNG), |
| 153 | | (get_preference(dot_use_unicode,true) -> translate:unset_unicode_mode ; true). |
| 154 | | |
| 155 | | % whole tree at once |
| 156 | | get_tree_from_expr3(State, LocalState, TExpr, Tree) :- rewrite_expression(TExpr,NewTExpr),!, |
| 157 | | get_tree_from_expr3(State, LocalState, NewTExpr, Tree). |
| 158 | | get_tree_from_expr3(State, LocalState, Expr, Tree) :- |
| 159 | | get_tree_from_expr2(State, LocalState, Expr, NewTree), |
| 160 | | get_tree_node_info(NewTree, SubExprs, NewLocalState, _), |
| 161 | | label(NewTree, Label), |
| 162 | | value(NewTree, Value), |
| 163 | | create_long_tree_node(Tree, Children, Label, Type, Value, Expr), |
| 164 | | % print(value(Value)),nl, |
| 165 | | ( is_boolean(NewTree) -> Type = boolean ; Type = nonboolean ), |
| 166 | | !, |
| 167 | | maplist(get_tree_from_expr3(State, NewLocalState), SubExprs, Children). |
| 168 | | |
| 169 | | |
| 170 | | |
| 171 | | |
| 172 | | % only one layer |
| 173 | | %get_tree_from_expr2(State, LocalState, b(B,T,_), Tree) :- functor(B,F,N), print(visit(F,N,T)),nl,fail. |
| 174 | | get_tree_from_expr2(State, LocalState, TExpr, Tree) :- |
| 175 | | get_texpr_expr(TExpr, Expr), |
| 176 | | functor(Expr, Op, _Arity), |
| 177 | ? | x_is_quantifier_like(Op),!, |
| 178 | | x_get_metas(State, LocalState, TExpr, Metas), |
| 179 | ? | member(value(Value), Metas), |
| 180 | | (create_new_local_state(TExpr, Value, State, LocalState, NewLocalState) -> |
| 181 | | x_get_sub_expressions(TExpr, State, LocalState, Children), |
| 182 | | create_tree_node(Tree, Children, NewLocalState, Metas) |
| 183 | | ; |
| 184 | | create_tree_node(Tree, [], LocalState, Metas) |
| 185 | | ),!. |
| 186 | | get_tree_from_expr2(State, LocalState, TExpr, Tree):- |
| 187 | | x_get_metas(State, LocalState, TExpr, Metas), |
| 188 | | x_get_sub_expressions(TExpr, State, LocalState, Children), |
| 189 | | create_tree_node(Tree, Children, LocalState, Metas),!. |
| 190 | | |
| 191 | | |
| 192 | | |
| 193 | | %% |
| 194 | | % Get all meta information for an expression/predicate |
| 195 | | % |
| 196 | | x_get_metas(State, LocalState, TExpr, Metas):- |
| 197 | | findall(MetaValue, x_get_meta(State, LocalState, TExpr, MetaValue), Metas). |
| 198 | | |
| 199 | | |
| 200 | | :- use_module(probsrc(eval_interface),[get_value_string_of_formula/5, b_compute_expression_no_wd/4]). |
| 201 | | %% |
| 202 | | % Helpers, each single meta info. |
| 203 | | % There are value/1, type/1, label/1 and long_desc/1 |
| 204 | | % |
| 205 | | % compute the various attributes of a node: |
| 206 | | x_get_meta(State, LocalState, Expr, value(Value)):- |
| 207 | | max_chars_total(Lim), |
| 208 | | get_value_string_of_formula(State, LocalState, Expr, Lim, Value). |
| 209 | | x_get_meta(_State, _LocalState, Expr, type(Type)):- |
| 210 | | ( check_if_typed_predicate(Expr) -> |
| 211 | | Type = boolean |
| 212 | | ; |
| 213 | | Type = nonboolean |
| 214 | | ). |
| 215 | | x_get_meta(_State, _LocalState, Expr, label(Label)):- |
| 216 | ? | once(x_get_label(Expr, Label)). |
| 217 | | x_get_meta(_State, _LocalState, TExpr, long_desc(Expr)):- |
| 218 | | get_texpr_expr(TExpr, Expr). |
| 219 | | x_get_meta(_State, _LocalState, TExpr, rodin_label(Label)):- |
| 220 | ? | once(get_texpr_label(TExpr,Label)). |
| 221 | | |
| 222 | | |
| 223 | | |
| 224 | | %% |
| 225 | | % Generate a new local state for subexpressions if necessary, like a forall |
| 226 | | % predicate. called for x_is_quantifier/1 predicate. |
| 227 | | % |
| 228 | | |
| 229 | | create_new_local_state(TExpr, Value, State, LocalState, NewLocalState):- |
| 230 | | get_texpr_expr(TExpr, Expr), |
| 231 | | (create_new_local_state2(Expr, Value, State, LocalState, NewLocalState) |
| 232 | | -> true |
| 233 | | ; %trace, create_new_local_state2(Expr, Value, State, LocalState, NewLocalState), |
| 234 | | fail). |
| 235 | | |
| 236 | | :- use_module(probsrc(bsyntaxtree),[create_typed_id/3, create_typed_ids/3]). |
| 237 | | create_new_local_state2(forall(IDs, LHS, _), true, State, LocalState, NewLocalState) :- !, |
| 238 | | (get_any(IDs, LHS, State, LocalState, NewLocalState) |
| 239 | | -> true /* there is a solution for LHS */ |
| 240 | | ; /* Forall true because no solution for LHS */ |
| 241 | | get_any(IDs, b(truth,pred,[]), State, LocalState, NewLocalState) |
| 242 | | ). |
| 243 | | create_new_local_state2(forall(IDs, LHS, RHS), false, State, LocalState, NewLocalState) :- !, |
| 244 | | safe_create_texpr(negation(RHS), pred, NotRHS), |
| 245 | | conjunct_predicates([LHS, NotRHS], Condition), |
| 246 | | get_any(IDs, Condition, State, LocalState, NewLocalState). |
| 247 | | create_new_local_state2(let_expression(Ids,AssignmentExprs,Expr), Value, State, LocalState, NewLocalState) :- !, |
| 248 | | create_typed_id('$VALUE',EType,TID), get_texpr_type(Expr,EType), |
| 249 | | construct_pred([TID],[Expr],[],Preds0), |
| 250 | | construct_pred(Ids,AssignmentExprs,Preds0,Preds), |
| 251 | | conjunct_predicates(Preds,NewPred), |
| 252 | | EXISTS = exists([TID|Ids],NewPred), %translate:print_bexpr(b(EXISTS,pred,[])),nl, |
| 253 | | (Value=unknown -> ExValue = undefined ; ExValue=true), |
| 254 | | create_new_local_state2(EXISTS, ExValue, State, LocalState, NewLocalState). |
| 255 | | create_new_local_state2(let_predicate(Ids,AssignmentExprs,Pred), Value, State, LocalState, NewLocalState) :- |
| 256 | | construct_pred(Ids,AssignmentExprs,[Pred],Preds), |
| 257 | | conjunct_predicates(Preds,NewPred), |
| 258 | | EXISTS = exists(Ids,NewPred), |
| 259 | | create_new_local_state2(EXISTS, Value, State, LocalState, NewLocalState). |
| 260 | | create_new_local_state2(exists(IDs, LHS), true, State, LocalState, NewLocalState) :- !, |
| 261 | | get_any(IDs, LHS, State, LocalState, NewLocalState). |
| 262 | | create_new_local_state2(exists(IDs, LHS), Status, State, LocalState, NewLocalState) :- |
| 263 | | (Status=false ; Status=undefined),!, |
| 264 | | % for Status=undefined get_any can fail but get_any_most_satisfier should always succeed |
| 265 | | get_any_most_satisfier(IDs, LHS, State, LocalState, NewLocalState). |
| 266 | | create_new_local_state2(X, undefined, State, LocalState, NewLocalState) :- !, |
| 267 | | create_new_local_state2(X, true, State, LocalState, NewLocalState). |
| 268 | | create_new_local_state2(X, x_both_true_and_not_true, State, LocalState, NewLocalState) :- |
| 269 | | %print(x_both_true_and_not_true(X)),nl, % probably means a PROB BUG ! |
| 270 | | (X = forall(_,_,_) -> VAL=false ; VAL=true), |
| 271 | | create_new_local_state2(X, VAL, State, LocalState, NewLocalState). |
| 272 | | create_new_local_state2(comprehension_set(IDs, Body), Val, State, LocalState, NewLocalState) :- !, |
| 273 | | % TODO: we could extract values from the context; e.g., if we have x:{y|Pred} we could use value assigned to x for y |
| 274 | | % format(user_output,'Comprehension set ~w, Val=~w~n~n',[IDs,Val]), |
| 275 | | (is_empty_set_value(Val) -> |
| 276 | | get_any_most_satisfier(IDs, Body, State, LocalState, NewLocalState) |
| 277 | | % we could have a symbolic value; which we do not know if it is empty or not; Body could also have a WD error |
| 278 | | ; get_any_if_possible(IDs, Body, State, LocalState, NewLocalState)). |
| 279 | | create_new_local_state2(general_sum(IDs, CondPred, _Expr), _Val, State, LocalState, NewLocalState) :- !, |
| 280 | | get_any_if_possible(IDs, CondPred, State, LocalState, NewLocalState). |
| 281 | | create_new_local_state2(general_product(IDs, CondPred, _Expr), _Val, State, LocalState, NewLocalState) :- !, |
| 282 | | get_any_if_possible(IDs, CondPred, State, LocalState, NewLocalState). |
| 283 | | create_new_local_state2(quantified_union(IDs, CondPred, _Expr), _Val, State, LocalState, NewLocalState) :- !, |
| 284 | | get_any_if_possible(IDs, CondPred, State, LocalState, NewLocalState). |
| 285 | | create_new_local_state2(quantified_intersection(IDs, CondPred, _Expr), _Val, State, LocalState, NewLocalState) :- !, |
| 286 | | get_any_if_possible(IDs, CondPred, State, LocalState, NewLocalState). |
| 287 | | %create_new_local_state2(value(StoredVal), Val, State, LocalState, NewLocalState) :- nonvar(StoredVal), |
| 288 | | % StoredVal = closure(P,T,Body), |
| 289 | | % !, |
| 290 | | % create_typed_ids(P,T,IDs), |
| 291 | | % create_new_local_state2(comprehension_set(IDs, Body), Val, State, LocalState, NewLocalState). |
| 292 | | create_new_local_state2(Expr, Value, _State, _LocalState, _NewLocalState) :- |
| 293 | | add_error(bvisual,'Uncovered Expr in create_new_local_state: ',Expr:Value), |
| 294 | | fail. |
| 295 | | |
| 296 | | % a bit of a hack; it would be better to look at the Prolog version of the value |
| 297 | | is_empty_set_value('{}'). |
| 298 | | is_empty_set_value('[]'). |
| 299 | | is_empty_set_value(X) :- translate:unicode_translation(empty_set,X). |
| 300 | | |
| 301 | | % construct predicate from list of typed ids and expressions |
| 302 | | construct_pred([],[],TailPreds,TailPreds). |
| 303 | | construct_pred([ID|T],[EXPR|ET],TailPreds,[b(equal(ID,EXPR),pred,[])|TR]) :- |
| 304 | | construct_pred(T,ET,TailPreds,TR). |
| 305 | | |
| 306 | | |
| 307 | | :- use_module(probsrc(custom_explicit_sets),[is_interval_closure/3]). |
| 308 | | % rewrite rules to transform some values into a formula tree |
| 309 | | rewrite_expression(b(value(StoredVal),Type,I),b(comprehension_set(IDs, Body),Type,[compiled_closure|I])) :- |
| 310 | | nonvar(StoredVal), |
| 311 | | StoredVal = closure(P,T,Body), |
| 312 | | \+ is_interval_closure(StoredVal,_,_), |
| 313 | | create_typed_ids(P,T,IDs). |
| 314 | | |
| 315 | | |
| 316 | | %% |
| 317 | | % Get subexpressions, merge sub expressions with associative operators, like |
| 318 | | % 'and'. For example the predicate and(A,and(B,C)) has three sub expressions: |
| 319 | | % A, B and C. This behaviour is controlled by x_associative_operator/1. |
| 320 | | % |
| 321 | | |
| 322 | | x_get_sub_expressions(TExpr, Children) :- |
| 323 | | x_get_sub_expressions(TExpr, [], [], Children). |
| 324 | | |
| 325 | | x_get_sub_expressions(TExpr, _, _, Children) :- nonvar(TExpr), |
| 326 | | do_not_expand(TExpr), !, |
| 327 | | Children=[]. |
| 328 | | x_get_sub_expressions(TExpr, State, LocalState, Children) :- |
| 329 | | syntaxtraversion(TExpr,Expr,_,_,Children0,_), |
| 330 | | % add custom explanation rules for certain nodes: |
| 331 | | x_get_custom_explanation_subexpressions(Expr,State, LocalState, Children0,Children). |
| 332 | | |
| 333 | | |
| 334 | | do_not_expand(b(equal(A,B),pred,_)) :- get_preference(pp_propositional_logic_mode,true), |
| 335 | | A = b(identifier(_),boolean,_), % do not expand such nodes |
| 336 | | is_explicit_value(B). |
| 337 | | |
| 338 | | :- use_module(library(lists)). |
| 339 | | % is a value which does not need to be further decomposed |
| 340 | | is_explicit_value(b(Val,_,_)) :- is_explicit_value2(Val). |
| 341 | | is_explicit_value2(integer(_N)). |
| 342 | | is_explicit_value2(string(_S)). |
| 343 | | is_explicit_value2(boolean_true). |
| 344 | | is_explicit_value2(boolean_false). |
| 345 | | is_explicit_value2(identifier(N)) :- b_global_sets:lookup_global_constant(N,_). |
| 346 | | is_explicit_value2(couple(A,B)) :- is_explicit_value(A), is_explicit_value(B). |
| 347 | | is_explicit_value2(value(_)). |
| 348 | | % to do: add further cases |
| 349 | | |
| 350 | | |
| 351 | | :- use_module(library(timeout),[time_out/3]). |
| 352 | | x_get_custom_explanation_subexpressions(function(Fun,Value),State,LocalState,_C0,Children) :- |
| 353 | | % a custom rule for function application of closures |
| 354 | | % print(function(Fun)),nl, print(value(Value)),nl,print(C0),nl, |
| 355 | | simple_value(Fun), |
| 356 | | get_preference(formula_tree_minimal_timeout,TOVAL), |
| 357 | | time_out(b_compute_expression_no_wd(Fun, LocalState, State, FunValue),TOVAL,TRes), TRes \== time_out, |
| 358 | | FunValue = closure(P,T,Pred), |
| 359 | | P = [X,_Res], % TO DO: extend to functions with multiple arguments |
| 360 | | closures:is_lambda_closure(P,T,Pred, _OtherIDs,_OtherTypes, DomainPred, Expr),!, |
| 361 | | bsyntaxtree:replace_id_by_expr(Expr,X,Value,NewExpr), |
| 362 | | bsyntaxtree:replace_id_by_expr(DomainPred,X,Value,NewDomainPred), |
| 363 | | Children = [Fun,Value, NewDomainPred,NewExpr]. |
| 364 | | % we could do similar treatment for member(Tuple,Fun) |
| 365 | | x_get_custom_explanation_subexpressions(Expr,_State,_LocalState, Children0,Children) :- |
| 366 | | x_get_custom_explanation_subexpressions(Expr, Children0,Children). |
| 367 | | |
| 368 | | |
| 369 | | |
| 370 | | simple_value(b(V,_,_)) :- simple_value_aux(V). |
| 371 | | simple_value_aux(identifier(_)). |
| 372 | | simple_value_aux(value(_)). |
| 373 | | |
| 374 | | :- use_module(probsrc(typing_tools),[create_maximal_type_set/2]). |
| 375 | | |
| 376 | | % TO DO: add explanation rules, e.g., f:A --> B ==> f:TA +-> B & dom(f)=A ,... |
| 377 | | x_get_custom_explanation_subexpressions(Expr,_Children0, Children):- |
| 378 | | functor(Expr, Op, _), |
| 379 | | x_operator_with_local_variables(Op),!,Children=[]. |
| 380 | | x_get_custom_explanation_subexpressions(Expr,Children0, Children):- |
| 381 | | functor(Expr, Op, _), Op = set_extension, |
| 382 | | length(Children0,Len), (Len>50 ; maplist(is_explicit_value,Children0)), |
| 383 | | % can be a very large explicit node; no sense in expanding and showing every element |
| 384 | | % print(no_child(Expr)),nl, |
| 385 | | % TO DO: check if simple value |
| 386 | | !,Children=[]. |
| 387 | | x_get_custom_explanation_subexpressions(Expr,Children0, Children):- |
| 388 | | functor(Expr, Op, _), |
| 389 | | x_associative_operator(Op),!, |
| 390 | | maplist(x_collect_exprs_with_op(Op), Children0, Children1), |
| 391 | | scanlist(x_append_reverse, Children1, [], Children). |
| 392 | | x_get_custom_explanation_subexpressions(member(X,b(partial_function(Dom,Range),T,Info)),_,Children) :- |
| 393 | | T=set(set(couple(DomT,RanT))), |
| 394 | | %print(pf(Dom,Range)),nl, |
| 395 | | (\+ bsyntaxtree:is_just_type(Dom) ; \+ bsyntaxtree:is_just_type(Range)), |
| 396 | | nonmember(already_expanded,Info), |
| 397 | | % otherwise we may have an infinite recursion; maybe better to add other operator |
| 398 | | %print(not_type),nl,fail, |
| 399 | | !, |
| 400 | | Children = [A|TB], |
| 401 | | create_maximal_type_set(DomT,DomType), |
| 402 | | create_maximal_type_set(RanT,RanType), |
| 403 | | A = b(member(X,b(partial_function(DomType,RanType),T,[already_expanded|Info])),pred,[]), |
| 404 | | add_subset_check(b(domain(X),set(DomT),[]), Dom, TB,TC), |
| 405 | | add_subset_check(b(range(X),set(RanT),[]), Range, TC,[]), |
| 406 | | TB \= [],!. |
| 407 | | x_get_custom_explanation_subexpressions(member(X,b(total_function(Dom,Range),T,Info)),_,Children) :- |
| 408 | | T=set(set(couple(DomT,RanT))), !, |
| 409 | | Children = [A,B|TC], |
| 410 | | %print(total_fun_check(DomT,RanT)),nl, |
| 411 | | create_maximal_type_set(DomT,DomType), |
| 412 | | create_maximal_type_set(RanT,RanType), |
| 413 | | A = b(member(X,b(partial_function(DomType,RanType),T,Info)),pred,[]), |
| 414 | | B = b(equal(b(domain(X),set(DomT),[]), Dom),pred,[]), |
| 415 | | add_subset_check(b(range(X),set(RanT),[]), Range, TC,[]). |
| 416 | | x_get_custom_explanation_subexpressions(member(X,b(total_surjection(Dom,Range),T,Info)),_,Children) :- |
| 417 | | T=set(set(couple(DomT,RanT))), !, |
| 418 | | Children = [A,B,C], |
| 419 | | create_maximal_type_set(DomT,DomType), |
| 420 | | create_maximal_type_set(RanT,RanType), |
| 421 | | A = b(member(X,b(partial_function(DomType,RanType),T,Info)),pred,[]), |
| 422 | | B = b(equal(b(domain(X),set(DomT),[]), Dom),pred,[]), |
| 423 | | C = b(equal(b(range(X),set(RanT),[]), Range),pred,[]). |
| 424 | | x_get_custom_explanation_subexpressions(member(X,b(partial_surjection(Dom,Range),T,Info)),_,Children) :- |
| 425 | | T=set(set(couple(DomT,RanT))), !, |
| 426 | | Children = [A|TB], |
| 427 | | create_maximal_type_set(DomT,DomType), |
| 428 | | create_maximal_type_set(RanT,RanType), |
| 429 | | A = b(member(X,b(partial_function(DomType,RanType),T,Info)),pred,[]), |
| 430 | | add_subset_check(b(domain(X),set(DomT),[]), Dom, TB,[C]), |
| 431 | | C = b(equal(b(range(X),set(RanT),[]), Range),pred,[]). |
| 432 | | x_get_custom_explanation_subexpressions(Expr,Children, Res) :- |
| 433 | | functor(Expr,Functor,_), |
| 434 | | (filter_trivial_children_for(Functor) -> exclude(is_explicit_value,Children,Res) ; Res=Children). |
| 435 | | |
| 436 | | filter_trivial_children_for(let_predicate). % avoid we see trivial values twice |
| 437 | | |
| 438 | | |
| 439 | | |
| 440 | | add_subset_check(LHS,RHS,Result,EndOfList) :- |
| 441 | | % add subset check, unless "obvious" |
| 442 | | (bsyntaxtree:is_just_type(RHS) -> Result=EndOfList |
| 443 | | ; Result = [b(subset(LHS, RHS),pred,[])|EndOfList] |
| 444 | | ). |
| 445 | | |
| 446 | | x_collect_exprs_with_op(Op, TExpr, Children):- |
| 447 | | syntaxtraversion(TExpr,Expr,_,_,_,_), |
| 448 | | ( functor(Expr, Op, _), |
| 449 | | \+ get_texpr_label(TExpr,_) % do not expand out if there is a separate label for the sub-conjunct/disjunct |
| 450 | | -> x_get_sub_expressions(TExpr, Children) |
| 451 | | ; Children = [TExpr] |
| 452 | | ). |
| 453 | | |
| 454 | | x_append_reverse(X,Y,L):- append(Y,X,L). |
| 455 | | |
| 456 | | |
| 457 | | |
| 458 | | %% |
| 459 | | % Get label for an expression |
| 460 | | % |
| 461 | | |
| 462 | | x_get_label(b(Expr,_,Infos), Label) :- |
| 463 | ? | x_get_label_aux(Expr,Infos,Label). |
| 464 | | x_get_label_aux(comprehension_set(_,_),[compiled_closure|_],Label) :- !, % generated by rewrite_expression |
| 465 | | Label= 'comprehension_set (compiled closure)'. |
| 466 | | x_get_label_aux(value(V), _, Label) :- !, get_value_label(V,Label). |
| 467 | | x_get_label_aux(external_function_call(Name,_),_Infos,Label) :- !, |
| 468 | | Label=Name. |
| 469 | | x_get_label_aux(external_pred_call(Name,_),_Infos,Label) :- !, |
| 470 | | Label=Name. |
| 471 | | x_get_label_aux(Expr, _, Label) :- |
| 472 | | %Expr =.. [Op, Label], |
| 473 | | functor(Expr,Op,1), arg(1,Expr,Label), |
| 474 | | x_literal_value_operator(Op). |
| 475 | | x_get_label_aux(Expr, _ , Label):- |
| 476 | | functor(Expr, Fkt, _), |
| 477 | | x_functor_to_label(Fkt, Label). |
| 478 | | |
| 479 | | get_value_label(V,Label) :- var(V),!, Label='VAR-VALUE'. |
| 480 | | %get_value_label(global_set(GS),Label) :- !, Label=GS. % should we pretty print the value |
| 481 | | %get_value_label(V,stored_value(F)) :- functor(V,F,_N). |
| 482 | | get_value_label(V,Label) :- translate_bvalue_with_limit(V,40,Label). |
| 483 | | %% |
| 484 | | % Helpers |
| 485 | | % |
| 486 | | |
| 487 | | %% |
| 488 | | % Maps functor of prolog term to correct label |
| 489 | | % |
| 490 | | :- use_module(probsrc(translate),[translate_prolog_constructor_in_mode/2]). |
| 491 | | x_functor_to_label(F,R) :- translate_prolog_constructor_in_mode(F,PPVersion), !, R=PPVersion. |
| 492 | | %x_functor_to_label(conjunct, conjunction):-!. |
| 493 | | %x_functor_to_label(disjunct, disjunction):-!. |
| 494 | | x_functor_to_label(function, R):-!, R='func.applic.'. |
| 495 | | x_functor_to_label(X, X). |
| 496 | | |
| 497 | | %% |
| 498 | | % List of operators which may generate a new local state, |
| 499 | | % like a forall predicate. |
| 500 | | % |
| 501 | | x_is_quantifier_like(comprehension_set). |
| 502 | | x_is_quantifier_like(general_sum). |
| 503 | | x_is_quantifier_like(general_product). |
| 504 | | x_is_quantifier_like(quantified_union). |
| 505 | | x_is_quantifier_like(quantified_intersection). |
| 506 | | x_is_quantifier_like(X) :- x_is_quantifier(X). |
| 507 | | |
| 508 | | x_is_quantifier(forall). |
| 509 | | x_is_quantifier(exists). |
| 510 | | x_is_quantifier(let_predicate). |
| 511 | | x_is_quantifier(let_expression). |
| 512 | | |
| 513 | | x_is_quantifier(true_guard). |
| 514 | | |
| 515 | | %% |
| 516 | | % List of associative operators |
| 517 | | % |
| 518 | | |
| 519 | | x_associative_operator(conjunct). |
| 520 | | x_associative_operator(disjunct). |
| 521 | | x_associative_operator(add). |
| 522 | | x_associative_operator(mul). |
| 523 | | |
| 524 | | |
| 525 | | %% |
| 526 | | % List of operators with local variables |
| 527 | | % |
| 528 | | |
| 529 | | % x_operator_with_local_variables(comprehension_set). is now supported in create_new_local_state2 |
| 530 | | % x_operator_with_local_variables(let_predicate). ditto, and for let_expression |
| 531 | | %x_operator_with_local_variables(general_sum). |
| 532 | | %x_operator_with_local_variables(general_product). |
| 533 | | %x_operator_with_local_variables(quantified_union). |
| 534 | | %x_operator_with_local_variables(quantified_intersection). |
| 535 | | x_operator_with_local_variables(lambda). |
| 536 | | x_operator_with_local_variables(lazy_let_expr). |
| 537 | | x_operator_with_local_variables(lazy_let_pred). |
| 538 | | x_operator_with_local_variables(lazy_let_subst). |
| 539 | | |
| 540 | | |
| 541 | | %% |
| 542 | | % List of literal values |
| 543 | | % |
| 544 | | x_literal_value_operator(identifier). |
| 545 | | x_literal_value_operator(value). |
| 546 | | x_literal_value_operator(integer). |
| 547 | | x_literal_value_operator(string). |
| 548 | | |
| 549 | | |
| 550 | | |
| 551 | | |
| 552 | | |
| 553 | | |
| 554 | | %% |
| 555 | | % Try to execute an 'Any' statement on LocalState and State. |
| 556 | | % New state with the values is returned by NewLocalState. |
| 557 | | % Compare to b_interpreter:b_execute_statement2(any(Parameters,PreCond,Body),...) |
| 558 | | % |
| 559 | | |
| 560 | | :- use_module(probsrc(b_enumerate), [b_tighter_enumerate_values_in_ctxt/3]). |
| 561 | | :- use_module(probsrc(b_interpreter), [set_up_typed_localstate/6]). |
| 562 | | :- use_module(probsrc(error_manager), [add_message/4, time_out_with_enum_warning_one_solution/3, is_time_out_result/1]). |
| 563 | | |
| 564 | | |
| 565 | | |
| 566 | | get_any(IDs, Condition, State, LocalState, NewLocalState) :- |
| 567 | | catch(get_any1(IDs, Condition, State, LocalState, NewLocalState), E, |
| 568 | | (add_warning(bvisual,'Exception in bvisual while treating quantfier predicate: ',E),fail)). |
| 569 | | get_any1(IDs, C, S, LS, NewLS) :- |
| 570 | | % used to be: on_enumeration_warning(bvisual:get_any2(IDs, C, S, LS, NewLS), fail). |
| 571 | | % call below does not force throwing enum warnings, which is ok as we just want one solution: |
| 572 | | %BackupCall = fail, AddAsEventError = false, |
| 573 | | %catch_enumeration_warning_exceptions(bvisual:get_any2(IDs, C, S, LS, NewLS),BackupCall, AddAsEventError, C), |
| 574 | | get_preference(formula_tree_maximal_timeout,MaxTO), |
| 575 | | time_out_with_enum_warning_one_solution(bvisual:get_any2(IDs, C, S, LS, NewLS),MaxTO,Res), |
| 576 | | \+ is_time_out_result(Res). |
| 577 | | get_any2(IDs, Condition, State, LocalState, NewLocalState) :- |
| 578 | | set_up_typed_localstate(IDs, _FreshVars, TypedVals, LocalState, NewLocalState,positive), |
| 579 | | init_wait_flags(WF,[get_any2]), |
| 580 | | b_interpreter:b_test_boolean_expression(Condition,NewLocalState, State, WF), /* check WHERE */ |
| 581 | | b_tighter_enumerate_values_in_ctxt(TypedVals,Condition,WF), |
| 582 | ? | ground_wait_flags(WF). |
| 583 | | |
| 584 | | |
| 585 | | get_any_most_satisfier(IDs, Condition, State, LocalState, NewLocalState):- |
| 586 | | ( any_maxsolver(IDs, Condition, State, LocalState, NewLocalState) -> |
| 587 | | true |
| 588 | | ; get_typing_solution(IDs, State, LocalState, NewLocalState) |
| 589 | | ). |
| 590 | | |
| 591 | | % just get a solution for truth: i.e., find any value for the types |
| 592 | | get_typing_solution(IDs, State, LocalState, NewLocalState) :- |
| 593 | | conjunct_predicates([], Truth), |
| 594 | | get_any(IDs, Truth, State, LocalState, NewLocalState). |
| 595 | | |
| 596 | | % get some successful solution; or if this does not work: just call get_any_most_satisfier |
| 597 | | get_any_if_possible(IDs, Condition, State, LocalState, NewLocalState) :- |
| 598 | | if(get_any(IDs, Condition, State, LocalState, NewLocalState),true, |
| 599 | | get_any_most_satisfier(IDs, Condition, State, LocalState, NewLocalState)). |
| 600 | | |
| 601 | | |
| 602 | | |
| 603 | | %% |
| 604 | | % Main predicate for writing dot graph |
| 605 | | % Use it to start. |
| 606 | | % |
| 607 | | % FileSpec is used by tell/1 to open a stream. |
| 608 | | % The graph is printed by print_dot_graph_for_tree/1. |
| 609 | | % |
| 610 | | |
| 611 | | :- use_module(probsrc(tools),[catch_call/1]). |
| 612 | | :- use_module(probsrc(tools_io),[safe_intelligent_open_file/3]). |
| 613 | | |
| 614 | | write_dot_graph_to_file(Tree, FileSpec) :- |
| 615 | | catch_call(write_dot_graph_to_file_aux(Tree, FileSpec)). |
| 616 | | write_dot_graph_to_file_aux(Tree, FileSpec) :- |
| 617 | | temp_set_prefs(CHNG) , |
| 618 | | safe_intelligent_open_file(FileSpec,write,Stream), |
| 619 | | call_cleanup(print_dot_graph(Stream,Tree), |
| 620 | | (close(Stream),reset_prefs(CHNG))). |
| 621 | | |
| 622 | | print_dot_graph(Stream,Tree):- |
| 623 | | format(Stream,'digraph g {~nrankdir=RL;~n',[]), |
| 624 | | visit_tree(x_print_dot_graph_visitor(Stream), x_print_dot_graph_node(Stream), Tree, [],_), |
| 625 | | format(Stream,'}~n',[]). |
| 626 | | |
| 627 | | |
| 628 | | %% |
| 629 | | % Helpers |
| 630 | | % |
| 631 | | :- public x_print_dot_graph_visitor/6. |
| 632 | | x_print_dot_graph_visitor(Stream,enter, Node, _Children, [], [1,root]) :- |
| 633 | ? | x_print_dot_graph_node_only(Stream,Node, root),!. |
| 634 | | x_print_dot_graph_visitor(Stream,enter, Node, _Children, In, [NewID|In]):- |
| 635 | | x_print_dot_graph_node(Stream,Node, In, [NewID|_]). |
| 636 | | x_print_dot_graph_visitor(_Stream,leave, _Node, _Children, [NewID,_ID|Out], [NewID|Out]). |
| 637 | | |
| 638 | | /* for 3 args : */ |
| 639 | | x_print_dot_graph_node(Stream,Node, [], []) :- |
| 640 | | x_print_dot_graph_node_only(Stream,Node, root), |
| 641 | | !. |
| 642 | | x_print_dot_graph_node(Stream,Node, [ID|Rest], [NewID|Rest]) :- |
| 643 | | Rest = [PID|_], |
| 644 | | NewID is ID + 1, |
| 645 | ? | x_print_dot_graph_node_only(Stream,Node, ID), |
| 646 | | format(Stream,'~8|Node~p -> Node~p;~N', [ID, PID]), |
| 647 | | !. |
| 648 | | |
| 649 | | |
| 650 | | |
| 651 | | |
| 652 | | shorten_atom(MaxLengthPerLine, Atom, NewAtom) :- |
| 653 | | max_lines(MaxLines), |
| 654 | ? | shorten_atom(MaxLengthPerLine, Atom, NewAtom,MaxLines). |
| 655 | | shorten_atom(MaxLengthPerLine, Atom, NewAtom,MaxLines) :- |
| 656 | | ( atom(Atom) -> |
| 657 | | atom_chars(Atom, AtomChars), |
| 658 | ? | shorten_atom_list(MaxLengthPerLine, AtomChars, NewAtom,MaxLines) |
| 659 | | ; |
| 660 | | NewAtom = Atom |
| 661 | | ). |
| 662 | | |
| 663 | | shorten_atom_list(MaxLengthPerLine, Chars, Atom,MaxLines):- |
| 664 | | %length(Chars, Length), |
| 665 | ? | split_chars(Chars,MaxLengthPerLine, Prefix,Suffix), |
| 666 | | ( Suffix=[] -> |
| 667 | | atom_chars(Atom, Chars) |
| 668 | | ; |
| 669 | | %lists:append_length(Prefix, Suffix, Chars, MaxLengthPerLine), |
| 670 | | %print( split_chars(Chars,MaxLengthPerLine, Prefix,Suffix) ),nl, |
| 671 | | (MaxLines>1 -> ML1 is MaxLines-1, |
| 672 | ? | shorten_atom_list(MaxLengthPerLine, Suffix, SuffixAtom,ML1) |
| 673 | | ; SuffixAtom = '...'), |
| 674 | | atom_chars(PrefixAtom, Prefix), |
| 675 | | atom_concat(PrefixAtom, '\\n', PrefixAtomNewLine), |
| 676 | | atom_concat(PrefixAtomNewLine, SuffixAtom, Atom) |
| 677 | | ). |
| 678 | | |
| 679 | | % bvisual:split_chars([a,b,d,e,f],2,P,S), P==[a,b], S==[d,e,f] |
| 680 | | |
| 681 | | % a predicate to split List if it is longer than MaxLen, but only outside of single and double quotes |
| 682 | | % List is suppoed to be already encoded using string_escape |
| 683 | | split_chars(List,MaxLen,Prefix,Suffix) :- |
| 684 | ? | split_chars(List,MaxLen,Prefix,Suffix,q(outside,outside)). |
| 685 | | |
| 686 | | split_chars(List,MaxL,R,Suffix,Q) :- MaxL < 1, Q=q(outside,outside), !, |
| 687 | | % only add newline if we are outside of quotes |
| 688 | | R=[], Suffix=List. |
| 689 | | split_chars([],_MaxL,[],[],_). |
| 690 | | split_chars(L,MaxL,LR,LeftOver,Q) :- |
| 691 | | is_a_unit(L,T,LR,TR),!, |
| 692 | ? | M1 is MaxL-1, split_chars(T,M1,TR,LeftOver,Q). |
| 693 | | split_chars([Slash,Quote|T],MaxL,[Slash,Quote|TR],LeftOver,Q) :- Slash = ('\\'), |
| 694 | | !, %(Quote=34;Quote=39), !, % \" or \' |
| 695 | | toggle_quotes(Quote,Q,TQ), |
| 696 | ? | M1 is MaxL-1, split_chars(T,M1,TR,LeftOver,TQ). |
| 697 | | split_chars([H|T],MaxL,[H|TR],LeftOver,Q) :- |
| 698 | ? | M1 is MaxL-1, split_chars(T,M1,TR,LeftOver,Q). |
| 699 | | |
| 700 | | toggle_quotes('\'',q(outside,Q2),q(inside,Q2)) :- !. |
| 701 | | toggle_quotes('\'',q(inside,Q2),q(outside,Q2)) :- !. |
| 702 | | toggle_quotes('\"',q(Q1,outside),q(Q1,inside)) :- !. |
| 703 | | toggle_quotes('\"',q(Q1,inside),q(Q1,outside)) :- !. |
| 704 | | toggle_quotes(_,Q,Q). |
| 705 | | |
| 706 | | % check for HTML encodings like à Ë α ... |
| 707 | | % these should be counted as a single character and not be split |
| 708 | | is_a_unit(['&'|T1],T,['&'|T1R],TR) :- get_lexeme(T1,10,LexUnit,T), |
| 709 | | append(LexUnit,TR,T1R). |
| 710 | | |
| 711 | | get_lexeme([';'|T],_,[';'],TRes) :- !, TRes=T. |
| 712 | | get_lexeme([H|T],L,[H|LexT],TRes) :- L>1, L1 is L-1, get_lexeme(T,L1,LexT,TRes). |
| 713 | | |
| 714 | | :- use_module(probsrc(tools_strings),[ajoin/2]). |
| 715 | | get_long_label(Node,MaxPerLine,LongLabel) :- |
| 716 | | long_desc(Node, LongDesc), |
| 717 | | %tools:print_wtime(start_translate(ID)), |
| 718 | | LongDesc = b(P,T,Infos), |
| 719 | ? | (select_info_labels(Labels,Infos,I2) -> true ; Labels=[],I2=Infos), |
| 720 | | translate_bexpression_with_limit(b(P,T,I2), 250, Pretty0), |
| 721 | | %tools:print_wtime(translated(ID)), |
| 722 | | string_escape(Pretty0, Pretty1), |
| 723 | ? | shorten_atom(MaxPerLine, Pretty1, Pretty1h), % maximally 10 lines with 40 chars |
| 724 | | gen_labels(Labels,[Pretty1h],Atoms), % print labels separately one per line |
| 725 | | ajoin(Atoms,LongLabel). |
| 726 | | |
| 727 | | gen_labels([],Res,Res). |
| 728 | | gen_labels([Label|T],Tail,['/*@ ',Label,' */\\n' | Res]) :- gen_labels(T,Tail,Res). |
| 729 | | |
| 730 | | :- use_module(probsrc(tools),[string_escape/2]). |
| 731 | | x_print_dot_graph_node_only(Stream,Node, ID) :- %tools:print_wtime(node(ID,Node)), |
| 732 | | label(Node, Label0), |
| 733 | | max_chars_per_line(MaxPerLine), |
| 734 | | string_escape(Label0, Label1), %tools:print_wtime(escaped(ID)), |
| 735 | | ( ID \= root, is_boolean(Node) |
| 736 | | -> |
| 737 | | Label=Label1, |
| 738 | ? | get_long_label(Node,MaxPerLine,Pretty1h), |
| 739 | | value(Node, TruthValue), |
| 740 | | string_escape(TruthValue, TVEsc), |
| 741 | | get_predicate_field_seperator(Sep), |
| 742 | | atom_concat(TVEsc, Sep, Pretty4), |
| 743 | | atom_concat(Pretty4, Pretty1h, Pretty) |
| 744 | | ; |
| 745 | | value(Node, Val), |
| 746 | | string_escape(Val, Pretty1), % TO DO: check that we also escape | in case of records! |
| 747 | | (is_boolean(Node) -> get_predicate_field_seperator(Sep) |
| 748 | ? | ; get_expression_field_seperator(Sep)), |
| 749 | | ((Pretty1=Label1 ; is_explicit_value_node(Node)) |
| 750 | | -> Pretty='', Label=Pretty1 % we have a simple value node like integer(1),... |
| 751 | | ; has_no_children(Node) |
| 752 | ? | -> get_long_label(Node,MaxPerLine,Label), |
| 753 | ? | shorten_atom(MaxPerLine, Pretty1, Pretty) |
| 754 | | ; Label=Label1, |
| 755 | ? | shorten_atom(MaxPerLine, Pretty1, Pretty) |
| 756 | | ) |
| 757 | | ), |
| 758 | | %tools:print_wtime(node_style(ID)), |
| 759 | | x_print_dot_graph_node_style(Node, Shape, Color,Style), |
| 760 | | %tools:print_wtime(printing(ID)), |
| 761 | | (Pretty='' |
| 762 | | -> format(Stream,'~4|Node~p [label="~p", shape="~p", fillcolor="~p", style="~p"]~N', |
| 763 | | [ID, Label, Shape, Color,Style]) |
| 764 | | ; format(Stream,'~4|Node~p [label="~p~p~p", shape="~p", fillcolor="~p", style="~p"]~N', |
| 765 | | [ID, Label, Sep, Pretty, Shape, Color,Style])). % ,tools:print_wtime(finished(ID)). |
| 766 | | |
| 767 | | |
| 768 | | x_print_dot_graph_node_style(Node, Shape, 'tomato','filled,rounded') :- |
| 769 | | is_boolean(Node), value(Node, false),!, boolean_shape(Shape). |
| 770 | | x_print_dot_graph_node_style(Node, Shape, 'olivedrab2','filled,rounded') :- |
| 771 | | is_boolean(Node), value(Node, true),!, boolean_shape(Shape). |
| 772 | | x_print_dot_graph_node_style(Node, Shape, 'orange','filled,rounded') :- % styles could be dashed,dotted, rounded, ... |
| 773 | | is_boolean(Node),!, boolean_shape(Shape). |
| 774 | | x_print_dot_graph_node_style(Node, Shape, 'yellow','filled') :- |
| 775 | | value(Node, unknown),!, get_preference(dot_expression_node_shape,Shape). |
| 776 | | x_print_dot_graph_node_style(_, Shape, 'white',filled) :- |
| 777 | | get_preference(dot_expression_node_shape,Shape). |
| 778 | | |
| 779 | | |
| 780 | | boolean_shape(Shape) :- get_preference(dot_predicate_node_shape,Shape). % ellipse, oval, record TO DO: other form for quantifiers |
| 781 | | |
| 782 | | % if we use a Dot record, we can use | to separate fields |
| 783 | | get_predicate_field_seperator('|') :- get_preference(dot_predicate_node_shape,record). |
| 784 | | get_predicate_field_seperator('\\n'). |
| 785 | | get_expression_field_seperator('|') :- get_preference(dot_expression_node_shape,record). |
| 786 | | get_expression_field_seperator('\\n'). |
| 787 | | |
| 788 | | |
| 789 | | |
| 790 | | %% |
| 791 | | % Hierarchical Visitor Pattern for "trees" |
| 792 | | % used to be in gtree module |
| 793 | | % |
| 794 | | % For this implementation a tree is a (root) node and a functor, which |
| 795 | | % maps a node to it's child nodes. For example a Prolog term can be |
| 796 | | % understand as a tree by the functor: |
| 797 | | % children_fkt(Term, Subterms):- Term=..[_|Subterms]. |
| 798 | | % |
| 799 | | % Important: Do not use trees with cycles. This implementation will not |
| 800 | | % detect them and will not terminate. |
| 801 | | % |
| 802 | | % The indented calling is: |
| 803 | | % visit_tree(+VisitorFkt5, +VisitorFkt3, +Node, +EnvIn, -EnvOut) |
| 804 | | % |
| 805 | | % If no functor is specified, the former mentioned one is used. |
| 806 | | % EnvIn and EnvOut are Variables for intermediate values or states, |
| 807 | | % which you might need to maintain between calls to VisitorFkt. You |
| 808 | | % might omit them, if you do not need them. |
| 809 | | % |
| 810 | | % During the visiting process the VisitorFkt functor is called for each |
| 811 | | % node starting with the "root". Calls are made in following order: |
| 812 | | % - VisitorFkt(Node, EnvIn, EnvOut), if Node is a leaf, |
| 813 | | % i.e. ChildrenFkt(Node, []). |
| 814 | | % - VisitorFkt(enter, Node, Children, EnvIn, EnvOut), before branching, |
| 815 | | % - VisitorFkt(leave, Node, Children, EnvIn, EnvOut), after branching |
| 816 | | % to Node's child nodes. |
| 817 | | % !- Only if VisitorFkt(enter, ...) succeeds, child nodes will be |
| 818 | | % visited and VisitorFkt(leave, ...) will be called. |
| 819 | | % |
| 820 | | |
| 821 | | :- use_module(library(lists), [scanlist/4, maplist/2]). |
| 822 | | |
| 823 | | %:- meta_predicate visit_tree(5,3,-,-,-). |
| 824 | | |
| 825 | | visit_tree(VisitorFkt5, VisitorFkt3, Node, EnvIn, EnvOut):- |
| 826 | | child_nodes(Node, Children), |
| 827 | | ( Children == [] -> |
| 828 | | call(VisitorFkt3, Node, EnvIn, EnvOut) |
| 829 | | ; |
| 830 | ? | ( call(VisitorFkt5, enter, Node, Children, EnvIn, Env1) -> |
| 831 | | scanlist(visit_tree(VisitorFkt5, VisitorFkt3), Children, Env1, Env2), |
| 832 | | call(VisitorFkt5, leave, Node, Children, Env2, EnvOut) |
| 833 | | ; |
| 834 | | EnvOut = EnvIn |
| 835 | | ) |
| 836 | | ), |
| 837 | | !. |
| 838 | | |
| 839 | | |
| 840 | | |
| 841 | | |