bvisual

add_subset_check(LHS,RHS,Result,EndOfList) :-
    % add subset check, unless "obvious"
    (bsyntaxtree:is_just_type(RHS) -> Result=EndOfList
    ; Result = [b(subset(LHS, RHS),pred,[])|EndOfList]
).

boolean_shape(Shape) :- get_preference(dot_predicate_node_shape,Shape). % ellipse, oval, record TO DO: other form for quantifiers

child_nodes(bind(ChildNodes,_,_,_,_), ChildNodes).

child_nodes(bind(ChildNodes,_,_), ChildNodes).

construct_pred([],[],TailPreds,TailPreds).

construct_pred([ID|T],[EXPR|ET],TailPreds,[b(equal(ID,EXPR),pred,[])|TR]) :-
    construct_pred(T,ET,TailPreds,TR).

create_long_tree_node(bind(Children, Label, Type, Value, LongDesc),
    Children, Label, Type, Value, LongDesc).

create_new_local_state(TExpr, Value, State, LocalState, NewLocalState):-
    get_texpr_expr(TExpr, Expr),
    (create_new_local_state2(Expr, Value, State, LocalState, NewLocalState)
    -> true
    ; %trace, create_new_local_state2(Expr, Value, State, LocalState, NewLocalState),
    fail).

create_new_local_state2(forall(IDs, LHS, _), true, State, LocalState, NewLocalState) :- !,
    (get_any(IDs, LHS, State, LocalState, NewLocalState)
    -> true /* there is a solution for LHS */
    ; /* Forall true because no solution for LHS */
    get_any(IDs, b(truth,pred,[]), State, LocalState, NewLocalState)
).

create_new_local_state2(forall(IDs, LHS, RHS), false,State, LocalState, NewLocalState) :- !,
    safe_create_texpr(negation(RHS), pred, NotRHS),
    conjunct_predicates([LHS, NotRHS], Condition),
    get_any(IDs, Condition, State, LocalState, NewLocalState).

create_new_local_state2(let_expression(Ids,AssignmentExprs,Expr), Value, State, LocalState, NewLocalState) :- !,
    create_typed_id('$VALUE',EType,TID), get_texpr_type(Expr,EType),
    construct_pred([TID],[Expr],[],Preds0),
    construct_pred(Ids,AssignmentExprs,Preds0,Preds),
    conjunct_predicates(Preds,NewPred),
    EXISTS = exists([TID|Ids],NewPred), %translate:print_bexpr(b(EXISTS,pred,[])),nl,
    (Value=unknown -> ExValue = undefined ; ExValue=true),
    create_new_local_state2(EXISTS, ExValue, State, LocalState, NewLocalState).

create_new_local_state2(let_predicate(Ids,AssignmentExprs,Pred), Value, State, LocalState, NewLocalState) :-
    construct_pred(Ids,AssignmentExprs,[Pred],Preds),
    conjunct_predicates(Preds,NewPred),
    EXISTS = exists(Ids,NewPred),
    create_new_local_state2(EXISTS, Value, State, LocalState, NewLocalState).

create_new_local_state2(exists(IDs, LHS), true, State, LocalState, NewLocalState) :- !,
    get_any(IDs, LHS, State, LocalState, NewLocalState).

create_new_local_state2(exists(IDs, LHS), Status, State, LocalState, NewLocalState) :-
    (Status=false ; Status=undefined),!, % for Status=undefined get_any can fail but get_any_most_satisfier should always succeed
    get_any_most_satisfier(IDs, LHS, State, LocalState, NewLocalState).

create_new_local_state2(X, undefined, State, LocalState, NewLocalState) :- !,
    create_new_local_state2(X, true, State, LocalState, NewLocalState).

create_new_local_state2(X, x_both_true_and_not_true, State, LocalState, NewLocalState) :-
    %print(x_both_true_and_not_true(X)),nl, % probably means a PROB BUG !
    (X = forall(_,_,_) -> VAL=false ; VAL=true),
    create_new_local_state2(X, VAL, State, LocalState, NewLocalState).

create_new_local_state2(comprehension_set(IDs, Body), Val, State, LocalState, NewLocalState) :- !,
    % 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
    % format(user_output,'Comprehension set ~w, Val=~w~n~n',[IDs,Val]),
    (is_empty_set_value(Val) ->
    get_any_most_satisfier(IDs, Body, State, LocalState, NewLocalState)
    % we could have a symbolic value; which we do not know if it is empty or not; Body could also have a WD error
    ; get_any_if_possible(IDs, Body, State, LocalState, NewLocalState)).

create_new_local_state2(general_sum(IDs, CondPred, _Expr), _Val, State, LocalState, NewLocalState) :- !,
    get_any_if_possible(IDs, CondPred, State, LocalState, NewLocalState).

create_new_local_state2(general_product(IDs, CondPred, _Expr), _Val, State, LocalState, NewLocalState) :- !,
    get_any_if_possible(IDs, CondPred, State, LocalState, NewLocalState).

create_new_local_state2(quantified_union(IDs, CondPred, _Expr), _Val, State, LocalState, NewLocalState) :- !,
    get_any_if_possible(IDs, CondPred, State, LocalState, NewLocalState).

create_new_local_state2(quantified_intersection(IDs, CondPred, _Expr), _Val, State, LocalState, NewLocalState) :- !,
    get_any_if_possible(IDs, CondPred, State, LocalState, NewLocalState).

create_new_local_state2(Expr, Value, _State, _LocalState, _NewLocalState) :-
    add_error(bvisual,'Uncovered Expr in create_new_local_state: ',Expr:Value),
    fail.

create_tree_node(bind(Children, NewLocalState, Metas),
    Children, NewLocalState, Metas).

do_not_expand(b(equal(A,B),pred,_)) :- get_preference(pp_propositional_logic_mode,true),
    A = b(identifier(_),boolean,_), % do not expand such nodes
    is_explicit_value(B).

filter_trivial_children_for(let_predicate). % avoid we see trivial values twice

gen_labels([],Res,Res).

gen_labels([Label|T],Tail,['/*@ ',Label,' */\\n' | Res]) :- gen_labels(T,Tail,Res).

get_any(IDs, Condition, State, LocalState, NewLocalState) :-
    catch(get_any1(IDs, Condition, State, LocalState, NewLocalState), E,
    (add_warning(bvisual,'Exception in bvisual while treating quantfier predicate: ',E),fail)).

get_any1(IDs, C, S, LS, NewLS) :-
    % used to be: on_enumeration_warning(bvisual:get_any2(IDs, C, S, LS, NewLS), fail).
    % call below does not force throwing enum warnings, which is ok as we just want one solution:
    catch_enumeration_warning_exceptions(bvisual:get_any2(IDs, C, S, LS, NewLS), fail, false, C).

get_any2(IDs, Condition, State, LocalState, NewLocalState) :-
    set_up_typed_localstate(IDs, _FreshVars, TypedVals, LocalState, NewLocalState,positive),
    init_wait_flags(WF,[get_any2]),
    b_interpreter:b_test_boolean_expression(Condition,NewLocalState, State, WF), /* check WHERE */
    b_tighter_enumerate_values_in_ctxt(TypedVals,Condition,WF),
    ground_wait_flags(WF).

get_any_if_possible(IDs, Condition, State, LocalState, NewLocalState) :-
    if(get_any(IDs, Condition, State, LocalState, NewLocalState),true,
    get_any_most_satisfier(IDs, Condition, State, LocalState, NewLocalState)).

get_any_most_satisfier(IDs, Condition, State, LocalState, NewLocalState):-
    ( any_maxsolver(IDs, Condition, State, LocalState, NewLocalState) ->
    true
    ; get_typing_solution(IDs, State, LocalState, NewLocalState)
).

get_expression_field_seperator('|') :- get_preference(dot_expression_node_shape,record).

get_expression_field_seperator('\\n').

get_lexeme([';'|T],_,[';'],TRes) :- !, TRes=T.

get_lexeme([H|T],L,[H|LexT],TRes) :- L>1, L1 is L-1, get_lexeme(T,L1,LexT,TRes).

get_long_label(Node,MaxPerLine,LongLabel) :-
    long_desc(Node, LongDesc),
    %tools:print_wtime(start_translate(ID)),
    LongDesc = b(P,T,Infos),
    (select_info_labels(Labels,Infos,I2) -> true ; Labels=[],I2=Infos),
    translate_bexpression_with_limit(b(P,T,I2), 250, Pretty0),
    %tools:print_wtime(translated(ID)),
    string_escape(Pretty0, Pretty1),
    shorten_atom(MaxPerLine, Pretty1, Pretty1h), % maximally 10 lines with 40 chars
    gen_labels(Labels,[Pretty1h],Atoms), % print labels separately one per line
    ajoin(Atoms,LongLabel).

get_predicate_field_seperator('|') :- get_preference(dot_predicate_node_shape,record).

get_predicate_field_seperator('\\n').

get_tree_from_expr(Tree, Expr, LocalState, State) :-
    (get_preference(dot_use_unicode,true) -> translate:set_unicode_mode ; true),
    add_prob_deferred_set_elements_to_store(State,State1,visible),
    call_cleanup(catch_call(get_tree_from_expr3(State1, LocalState, Expr, Tree)),
    (get_preference(dot_use_unicode,true) -> translate:unset_unicode_mode ; true)).

get_tree_from_expr2(State, LocalState, TExpr, Tree) :-
    get_texpr_expr(TExpr, Expr),
    functor(Expr, Op, _Arity),
    x_is_quantifier_like(Op),!,
    x_get_metas(State, LocalState, TExpr, Metas),
    member(value(Value), Metas),
    (create_new_local_state(TExpr, Value, State, LocalState, NewLocalState) ->
    x_get_sub_expressions(TExpr, State, LocalState, Children),
    create_tree_node(Tree, Children, NewLocalState, Metas)
    ;
    create_tree_node(Tree, [], LocalState, Metas)
    ),!.

get_tree_from_expr2(State, LocalState, TExpr, Tree):-
    x_get_metas(State, LocalState, TExpr, Metas),
    x_get_sub_expressions(TExpr, State, LocalState, Children),
    create_tree_node(Tree, Children, LocalState, Metas),!.

get_tree_from_expr3(State, LocalState, TExpr, Tree) :- rewrite_expression(TExpr,NewTExpr),!,
    get_tree_from_expr3(State, LocalState, NewTExpr, Tree).

get_tree_from_expr3(State, LocalState, Expr, Tree) :-
    get_tree_from_expr2(State, LocalState, Expr, NewTree),
    get_tree_node_info(NewTree, SubExprs, NewLocalState, _),
    label(NewTree, Label),
    value(NewTree, Value),
    create_long_tree_node(Tree, Children, Label, Type, Value, Expr),
    % print(value(Value)),nl,
    ( is_boolean(NewTree) -> Type = boolean ; Type = nonboolean ),
    maplist(get_tree_from_expr3(State, NewLocalState), SubExprs, Children).

get_tree_node_info(NODE, Children, NewLocalState, Metas) :-
    (create_tree_node(NODE, C,N,M) -> Children=C, NewLocalState=N, Metas=M
    ; add_error(bvisual,'Illegal node: ',NODE)).

get_typing_solution(IDs, State, LocalState, NewLocalState) :-
    conjunct_predicates([], Truth),
    get_any(IDs, Truth, State, LocalState, NewLocalState).

get_value_label(V,Label) :- var(V),!, Label='VAR-VALUE'.

get_value_label(V,Label) :- translate_bvalue_with_limit(V,40,Label).

has_no_children(Node) :- child_nodes(Node,[]).

is_a_unit(['&'|T1],T,['&'|T1R],TR) :- get_lexeme(T1,10,LexUnit,T),
    append(LexUnit,TR,T1R).

is_boolean(bind(_,_,boolean,_,_)).

is_boolean(bind(_,_, Metas)):- member(type(boolean), Metas),!.

is_empty_set_value('{}').

is_empty_set_value('[]').

is_empty_set_value(X) :- translate:unicode_translation(empty_set,X).

is_explicit_value(b(Val,_,_)) :- is_explicit_value2(Val).

is_explicit_value2(integer(_N)).

is_explicit_value2(string(_S)).

is_explicit_value2(boolean_true).

is_explicit_value2(boolean_false).

is_explicit_value2(identifier(N)) :- b_global_sets:lookup_global_constant(N,_).

is_explicit_value2(couple(A,B)) :- is_explicit_value(A), is_explicit_value(B).

is_explicit_value2(value(_)).

is_explicit_value_node(Node) :- long_desc(Node,Val), is_explicit_value(Val).

label(bind(_,Label,_,_,_), Label).

label(bind(_,_, Metas), Val) :- member(label(Val), Metas),!.

long_desc(bind(_,_,_,_,Val), Val).

long_desc(bind(_,_, Metas), Val):- member(long_desc(Val), Metas),!.

max_chars_per_line(40).

max_chars_total(400). % :- max_chars_per_line(X), max_lines(ML), T is X*ML.

max_lines(10).

print_dot_graph(Stream,Tree):-
    format(Stream,'digraph g {~nrankdir=RL;~n',[]),
    visit_tree(x_print_dot_graph_visitor(Stream), x_print_dot_graph_node(Stream), Tree, [],_),
    format(Stream,'}~n',[]).

rewrite_expression(b(value(StoredVal),Type,I),b(comprehension_set(IDs, Body),Type,[compiled_closure|I])) :-
    nonvar(StoredVal),
    StoredVal = closure(P,T,Body),
    \+ is_interval_closure(StoredVal,_,_),
    create_typed_ids(P,T,IDs).

shorten_atom(MaxLengthPerLine, Atom, NewAtom) :-
    max_lines(MaxLines),
    shorten_atom(MaxLengthPerLine, Atom, NewAtom,MaxLines).

shorten_atom(MaxLengthPerLine, Atom, NewAtom,MaxLines) :-
    ( atom(Atom) ->
    atom_chars(Atom, AtomChars),
    shorten_atom_list(MaxLengthPerLine, AtomChars, NewAtom,MaxLines)
    ;
    NewAtom = Atom
).

shorten_atom_list(MaxLengthPerLine, Chars, Atom,MaxLines):-
    %length(Chars, Length),
    split_chars(Chars,MaxLengthPerLine, Prefix,Suffix),
    ( Suffix=[] ->
    atom_chars(Atom, Chars)
    ;
    %lists:append_length(Prefix, Suffix, Chars, MaxLengthPerLine),
    %print( split_chars(Chars,MaxLengthPerLine, Prefix,Suffix) ),nl,
    (MaxLines>1 -> ML1 is MaxLines-1,
    shorten_atom_list(MaxLengthPerLine, Suffix, SuffixAtom,ML1)
    ; SuffixAtom = '...'),
    atom_chars(PrefixAtom, Prefix),
    atom_concat(PrefixAtom, '\\n', PrefixAtomNewLine),
    atom_concat(PrefixAtomNewLine, SuffixAtom, Atom)
).

simple_value(b(V,_,_)) :- simple_value_aux(V).

simple_value_aux(identifier(_)).

simple_value_aux(value(_)).

split_chars(List,MaxLen,Prefix,Suffix) :-
    split_chars(List,MaxLen,Prefix,Suffix,q(outside,outside)).

split_chars(List,MaxL,R,Suffix,Q) :- MaxL < 1, Q=q(outside,outside), !,
    % only add newline if we are outside of quotes
    R=[], Suffix=List.

split_chars([],_MaxL,[],[],_).

split_chars(L,MaxL,LR,LeftOver,Q) :-
    is_a_unit(L,T,LR,TR),!,
    M1 is MaxL-1, split_chars(T,M1,TR,LeftOver,Q).

split_chars([Slash,Quote|T],MaxL,[Slash,Quote|TR],LeftOver,Q) :- Slash = ('\\'),
    !, %(Quote=34;Quote=39), !, % \" or \'"
    toggle_quotes(Quote,Q,TQ),
    M1 is MaxL-1, split_chars(T,M1,TR,LeftOver,TQ).

split_chars([H|T],MaxL,[H|TR],LeftOver,Q) :-
    M1 is MaxL-1, split_chars(T,M1,TR,LeftOver,Q).

toggle_quotes('\'',q(outside,Q2),q(inside,Q2)) :- !.

toggle_quotes('\'',q(inside,Q2),q(outside,Q2)) :- !.

toggle_quotes('\"',q(Q1,outside),q(Q1,inside)) :- !."

toggle_quotes('\"',q(Q1,inside),q(Q1,outside)) :- !."

toggle_quotes(_,Q,Q).

value(bind(_,_,_,Val,_), Val).

value(bind(_,_, Metas), Val) :- member(value(Val), Metas),!.

visit_tree(VisitorFkt5, VisitorFkt3, Node, EnvIn, EnvOut):-
    child_nodes(Node, Children),
    ( Children == [] ->
    call(VisitorFkt3, Node, EnvIn, EnvOut)
    ;
    ( call(VisitorFkt5, enter, Node, Children, EnvIn, Env1) ->
    scanlist(visit_tree(VisitorFkt5, VisitorFkt3), Children, Env1, Env2),
    call(VisitorFkt5, leave, Node, Children, Env2, EnvOut)
    ;
    EnvOut = EnvIn
    )
    ),
    !.

write_dot_graph_to_file(Tree, FileSpec) :-
    catch_call(write_dot_graph_to_file_aux(Tree, FileSpec)).

write_dot_graph_to_file_aux(Tree, FileSpec) :-
    (get_preference(dot_use_unicode,true) -> translate:set_unicode_mode ; true),
    safe_intelligent_open_file(FileSpec,write,Stream),
    call_cleanup(print_dot_graph(Stream,Tree),
    (close(Stream),(get_preference(dot_use_unicode,true) -> translate:unset_unicode_mode ; true))).

x_append_reverse(X,Y,L):- append(Y,X,L).

x_associative_operator(conjunct).

x_associative_operator(disjunct).

x_associative_operator(add).

x_associative_operator(mul).

x_collect_exprs_with_op(Op, TExpr, Children):-
    syntaxtraversion(TExpr,Expr,_,_,_,_),
    ( functor(Expr, Op, _),
    \+ get_texpr_label(TExpr,_) % do not expand out if there is a separate label for the sub-conjunct/disjunct
    -> x_get_sub_expressions(TExpr, Children)
    ; Children = [TExpr]
).

x_functor_to_label(F,R) :- translate_prolog_constructor_in_mode(F,PPVersion), !, R=PPVersion.

x_functor_to_label(function, R):-!, R='func.applic.'.

x_functor_to_label(X, X).

x_get_custom_explanation_subexpressions(Expr,_Children0, Children):-
    functor(Expr, Op, _),
    x_operator_with_local_variables(Op),!,Children=[].

x_get_custom_explanation_subexpressions(Expr,Children0, Children):-
    functor(Expr, Op, _), Op = set_extension,
    length(Children0,Len), (Len>50 ; maplist(is_explicit_value,Children0)),
    % can be a very large explicit node; no sense in expanding and showing every element
    % print(no_child(Expr)),nl,
    % TO DO: check if simple value
    !,Children=[].

x_get_custom_explanation_subexpressions(Expr,Children0, Children):-
    functor(Expr, Op, _),
    x_associative_operator(Op),!,
    maplist(x_collect_exprs_with_op(Op), Children0, Children1),
    scanlist(x_append_reverse, Children1, [], Children).

x_get_custom_explanation_subexpressions(member(X,b(partial_function(Dom,Range),T,Info)),_,Children) :-
    T=set(set(couple(DomT,RanT))),
    %print(pf(Dom,Range)),nl,
    (\+ bsyntaxtree:is_just_type(Dom) ; \+ bsyntaxtree:is_just_type(Range)),
    nonmember(already_expanded,Info),
    % otherwise we may have an infinite recursion; maybe better to add other operator
    %print(not_type),nl,fail,
    !,
    Children = [A|TB],
    create_maximal_type_set(DomT,DomType),
    create_maximal_type_set(RanT,RanType),
    A = b(member(X,b(partial_function(DomType,RanType),T,[already_expanded|Info])),pred,[]),
    add_subset_check(b(domain(X),set(DomT),[]), Dom, TB,TC),
    add_subset_check(b(range(X),set(RanT),[]), Range, TC,[]),
    TB \= [],!.

x_get_custom_explanation_subexpressions(member(X,b(total_function(Dom,Range),T,Info)),_,Children) :-
    T=set(set(couple(DomT,RanT))), !,
    Children = [A,B|TC],
    %print(total_fun_check(DomT,RanT)),nl,
    create_maximal_type_set(DomT,DomType),
    create_maximal_type_set(RanT,RanType),
    A = b(member(X,b(partial_function(DomType,RanType),T,Info)),pred,[]),
    B = b(equal(b(domain(X),set(DomT),[]), Dom),pred,[]),
    add_subset_check(b(range(X),set(RanT),[]), Range, TC,[]).

x_get_custom_explanation_subexpressions(member(X,b(total_surjection(Dom,Range),T,Info)),_,Children) :-
    T=set(set(couple(DomT,RanT))), !,
    Children = [A,B,C],
    create_maximal_type_set(DomT,DomType),
    create_maximal_type_set(RanT,RanType),
    A = b(member(X,b(partial_function(DomType,RanType),T,Info)),pred,[]),
    B = b(equal(b(domain(X),set(DomT),[]), Dom),pred,[]),
    C = b(equal(b(range(X),set(RanT),[]), Range),pred,[]).

x_get_custom_explanation_subexpressions(member(X,b(partial_surjection(Dom,Range),T,Info)),_,Children) :-
    T=set(set(couple(DomT,RanT))), !,
    Children = [A|TB],
    create_maximal_type_set(DomT,DomType),
    create_maximal_type_set(RanT,RanType),
    A = b(member(X,b(partial_function(DomType,RanType),T,Info)),pred,[]),
    add_subset_check(b(domain(X),set(DomT),[]), Dom, TB,[C]),
    C = b(equal(b(range(X),set(RanT),[]), Range),pred,[]).

x_get_custom_explanation_subexpressions(Expr,Children, Res) :-
    functor(Expr,Functor,_),
    (filter_trivial_children_for(Functor) -> exclude(is_explicit_value,Children,Res) ; Res=Children).

x_get_custom_explanation_subexpressions(function(Fun,Value),State,LocalState,_C0,Children) :-
    % a custom rule for function application of closures
    % print(function(Fun)),nl, print(value(Value)),nl,print(C0),nl,
    simple_value(Fun),
    get_preference(formula_tree_minimal_timeout,TOVAL),
    time_out(b_compute_expression_no_wd(Fun, LocalState, State, FunValue),TOVAL,TRes), TRes \== time_out,
    FunValue = closure(P,T,Pred),
    P = [X,_Res], % TO DO: extend to functions with multiple arguments
    closures:is_lambda_closure(P,T,Pred, _OtherIDs,_OtherTypes, DomainPred, Expr),!,
    bsyntaxtree:replace_id_by_expr(Expr,X,Value,NewExpr),
    bsyntaxtree:replace_id_by_expr(DomainPred,X,Value,NewDomainPred),
    Children = [Fun,Value, NewDomainPred,NewExpr].

x_get_custom_explanation_subexpressions(Expr,_State,_LocalState, Children0,Children) :-
    x_get_custom_explanation_subexpressions(Expr, Children0,Children).

x_get_label(b(Expr,_,Infos), Label) :-
    x_get_label_aux(Expr,Infos,Label).

x_get_label_aux(comprehension_set(_,_),[compiled_closure|_],Label) :- !, % generated by rewrite_expression
    Label= 'comprehension_set (compiled closure)'.

x_get_label_aux(value(V), _, Label) :- !, get_value_label(V,Label).

x_get_label_aux(external_function_call(Name,_),_Infos,Label) :- !,
    Label=Name.

x_get_label_aux(external_pred_call(Name,_),_Infos,Label) :- !,
    Label=Name.

x_get_label_aux(Expr, _, Label) :-
    %Expr =.. [Op, Label],
    functor(Expr,Op,1), arg(1,Expr,Label),
    x_literal_value_operator(Op).

x_get_label_aux(Expr, _ , Label):-
    functor(Expr, Fkt, _),
    x_functor_to_label(Fkt, Label).

x_get_meta(State, LocalState, Expr, value(Value)):-
    max_chars_total(Lim),
    get_value_string_of_formula(State, LocalState, Expr, Lim, Value).

x_get_meta(_State, _LocalState, Expr, type(Type)):-
    ( check_if_typed_predicate(Expr) ->
    Type = boolean
    ;
    Type = nonboolean
).

x_get_meta(_State, _LocalState, Expr, label(Label)):-
    once(x_get_label(Expr, Label)).

x_get_meta(_State, _LocalState, TExpr, long_desc(Expr)):-
    get_texpr_expr(TExpr, Expr).

x_get_meta(_State, _LocalState, TExpr, rodin_label(Label)):-
    once(get_texpr_label(TExpr,Label)).

x_get_metas(State, LocalState, TExpr, Metas):-
    findall(MetaValue, x_get_meta(State, LocalState, TExpr, MetaValue), Metas).

x_get_sub_expressions(TExpr, Children) :-
    x_get_sub_expressions(TExpr, [], [], Children).

x_get_sub_expressions(TExpr, _, _, Children) :- nonvar(TExpr),
    do_not_expand(TExpr), !,
    Children=[].

x_get_sub_expressions(TExpr, State, LocalState, Children) :-
    syntaxtraversion(TExpr,Expr,_,_,Children0,_),
    % add custom explanation rules for certain nodes:
    x_get_custom_explanation_subexpressions(Expr,State, LocalState, Children0,Children).

x_is_quantifier(forall).

x_is_quantifier(exists).

x_is_quantifier(let_predicate).

x_is_quantifier(let_expression).

x_is_quantifier(true_guard).

x_is_quantifier_like(comprehension_set).

x_is_quantifier_like(general_sum).

x_is_quantifier_like(general_product).

x_is_quantifier_like(quantified_union).

x_is_quantifier_like(quantified_intersection).

x_is_quantifier_like(X) :- x_is_quantifier(X).

x_literal_value_operator(identifier).

x_literal_value_operator(value).

x_literal_value_operator(integer).

x_literal_value_operator(string).

x_operator_with_local_variables(lambda).

x_operator_with_local_variables(lazy_let_expr).

x_operator_with_local_variables(lazy_let_pred).

x_operator_with_local_variables(lazy_let_subst).

x_print_dot_graph_node(Stream,Node, [], []) :-
    x_print_dot_graph_node_only(Stream,Node, root),
    !.

x_print_dot_graph_node(Stream,Node, [ID|Rest], [NewID|Rest]) :-
    Rest = [PID|_],
    NewID is ID + 1,
    x_print_dot_graph_node_only(Stream,Node, ID),
    format(Stream,'~8|Node~p -> Node~p;~N', [ID, PID]),
    !.

x_print_dot_graph_node_only(Stream,Node, ID) :- %tools:print_wtime(node(ID,Node)),
    label(Node, Label0),
    max_chars_per_line(MaxPerLine),
    string_escape(Label0, Label1), %tools:print_wtime(escaped(ID)),
    ( ID \= root, is_boolean(Node)
    ->
    Label=Label1,
    get_long_label(Node,MaxPerLine,Pretty1h),
    value(Node, TruthValue),
    string_escape(TruthValue, TVEsc),
    get_predicate_field_seperator(Sep),
    atom_concat(TVEsc, Sep, Pretty4),
    atom_concat(Pretty4, Pretty1h, Pretty)
    ;
    value(Node, Val),
    string_escape(Val, Pretty1), % TO DO: check that we also escape | in case of records!
    (is_boolean(Node) -> get_predicate_field_seperator(Sep)
    ; get_expression_field_seperator(Sep)),
    ((Pretty1=Label1 ; is_explicit_value_node(Node))
    -> Pretty='', Label=Pretty1 % we have a simple value node like integer(1),...
    ; has_no_children(Node)
    -> get_long_label(Node,MaxPerLine,Label),
    shorten_atom(MaxPerLine, Pretty1, Pretty)
    ; Label=Label1,
    shorten_atom(MaxPerLine, Pretty1, Pretty)
    )
    ),
    %tools:print_wtime(node_style(ID)),
    x_print_dot_graph_node_style(Node, Shape, Color,Style),
    %tools:print_wtime(printing(ID)),
    (Pretty=''
    -> format(Stream,'~4|Node~p [label="~p", shape="~p", fillcolor="~p", style="~p"]~N',
    [ID, Label, Shape, Color,Style])
    ; format(Stream,'~4|Node~p [label="~p~p~p", shape="~p", fillcolor="~p", style="~p"]~N',
    [ID, Label, Sep, Pretty, Shape, Color,Style])). % ,tools:print_wtime(finished(ID)).

x_print_dot_graph_node_style(Node, Shape, 'tomato','filled,rounded') :-
    is_boolean(Node), value(Node, false),!, boolean_shape(Shape).

x_print_dot_graph_node_style(Node, Shape, 'olivedrab2','filled,rounded') :-
    is_boolean(Node), value(Node, true),!, boolean_shape(Shape).

x_print_dot_graph_node_style(Node, Shape, 'orange','filled,rounded') :- % styles could be dashed,dotted, rounded, ...
    is_boolean(Node),!, boolean_shape(Shape).

x_print_dot_graph_node_style(Node, Shape, 'yellow','filled') :-
    value(Node, unknown),!, get_preference(dot_expression_node_shape,Shape).

x_print_dot_graph_node_style(_, Shape, 'white',filled) :-
    get_preference(dot_expression_node_shape,Shape).

x_print_dot_graph_visitor(Stream,enter, Node, _Children, [], [1,root]) :-
    x_print_dot_graph_node_only(Stream,Node, root),!.

x_print_dot_graph_visitor(Stream,enter, Node, _Children, In, [NewID|In]):-
    x_print_dot_graph_node(Stream,Node, In, [NewID|_]).

x_print_dot_graph_visitor(_Stream,leave, _Node, _Children, [NewID,_ID|Out], [NewID|Out]).