eval_interface

add_exception_warning(_,E) :- is_enumeration_warning_exception(E),!.

add_exception_warning(Msg,E) :-
    add_warning(bvisual,Msg,E).

b_compute_expression_no_wd(Fun, LocalState, State, FunValue) :-
    temporary_set_preference(disprover_mode,true,CHNG), % avoid WD Errors, we detect WD issues by failure below
    temporary_set_preference(find_abort_values,false,CHNG2),
    (catch(
    b_compute_expression_nowf(Fun, LocalState, State, FunValue,'formula visualisation',0),
    E,
    (add_exception_warning('Exception in bvisual while evaluating expression: ',E),fail)
    )
    -> reset_temporary_preference(disprover_mode,CHNG),
    reset_temporary_preference(find_abort_values,CHNG2)
    ; reset_temporary_preference(disprover_mode,CHNG),
    reset_temporary_preference(find_abort_values,CHNG2), fail).

get_bool_expr_val2(Expr,LocalState,State,Value) :-
    ( b_test_boolean_expression_cs(Expr,LocalState,State,'formula visualisation',0) ->
    ( b_not_test_boolean_expression_cs(Expr,LocalState,State,'formula visualisation (negated)',0)
    -> Value = x_both_true_and_not_true, % was x_unknown_true_and_not_true
    % we should add an error message here
    % this should never happen
    print('### Error, x_both_true_and_not_true: '), print(Expr),nl
    ; Value = true
    )
    ; b_not_test_boolean_expression_cs(Expr,LocalState,State,'formula visualisation',0) ->
    Value = false
    %, print(value_false),nl
    ;
    Value = undefined % was x_undefined_false_and_not_false
%, print(value_undefined),nl
).

get_bool_expr_value(Expr,LocalState,State,Value) :-
    catch(get_bool_expr_val2(Expr,LocalState,State,Value), E, (
    add_exception_warning('Exception in bvisual while evaluating predicate: ', E),
    Value=undefined
)).

get_value_string_of_formula(State, LocalState, Expr, _Lim, Value):-
    check_if_typed_predicate(Expr),!,
    temporary_set_preference(disprover_mode,false,CHNG), % avoid WD Errors, we detect WD issues by failure below
    temporary_set_preference(find_abort_values,false,CHNG2),
    % print('Test: '),translate:print_bexpr(Expr),nl,
    get_bool_expr_value(Expr,LocalState,State,Value),
    reset_temporary_preference(disprover_mode,CHNG),
    reset_temporary_preference(find_abort_values,CHNG2),
    clear_wd_errors. % ,print('Value: '), print(Value),nl.

get_value_string_of_formula(State, LocalState, Expr, Lim, Value):-
    check_if_typed_expression(Expr),!,
    % print('Eval: '),translate:print_bexpr(Expr),nl,
    (b_compute_expression_no_wd(Expr, LocalState, State, Value0)
    -> translate_bvalue_with_limit(Value0, Lim, Value) % we show maximally 10 lines a 40 chars
    ; Value = unknown).

get_value_string_of_formula(_State, _LocalState, _Expr, _, unknown).