1		% (c) 2009-2024 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(eval_interface,
5		[
6		get_value_string_of_formula/5,
7		b_compute_expression_no_wd/4
8
9		]
10		).
11
12		% TO DO: clean up API, and integrate parts form eval_strings and other modules
13
14		:- use_module(probsrc(module_information),[module_info/2]).
15		:- module_info(group,repl).
16		:- module_info(description,'Utilities for evaluating formulas, predicates, expressions.').
17
18		%%
19		% Evaluate predicate or expression ... at least it tries XD
20		% Expressions return value is translated by pretty printer.
21		% Value is unknown if Expr is neither a predicate or expression.
22		%
23
24		%%
25		% Evaluate the predicate Expr in LocaleState and State.
26		% It does check for consistency by checking Expr == !!Expr.
27		% Thus it yields in addition to true and false also
28		% x_both_true_and_not_true and undefined
29		% as flag signaling internal errors.
30
31		:- use_module(probsrc(error_manager)).
32		:- use_module(probsrc(bsyntaxtree),[check_if_typed_predicate/1,check_if_typed_expression/1]).
33		:- use_module(probsrc(preferences),[temporary_set_preference/3,reset_temporary_preference/2]).
34		:- use_module(probsrc(translate), [translate_bvalue_with_limit/3]).
35
36		% was x_get_value_of_expr
37
38		% get_value_of_expression or predicate without wd errors: TO DO: move to another module
39		get_value_string_of_formula(State, LocalState, Expr, _Lim, Value):-
40		check_if_typed_predicate(Expr),!,
41		temporary_set_preference(disprover_mode,false,CHNG), % avoid WD Errors, we detect WD issues by failure below
42		temporary_set_preference(find_abort_values,false,CHNG2),
43		% print('Test: '),translate:print_bexpr(Expr),nl,
44		get_bool_expr_value(Expr,LocalState,State,Value),
45		reset_temporary_preference(disprover_mode,CHNG),
46		reset_temporary_preference(find_abort_values,CHNG2),
47		clear_wd_errors. % ,print('Value: '), print(Value),nl.
48		get_value_string_of_formula(State, LocalState, Expr, Lim, Value):-
49		check_if_typed_expression(Expr),!,
50		% print('Eval: '),translate:print_bexpr(Expr),nl,
51		(b_compute_expression_no_wd(Expr, LocalState, State, Value0)
52		-> translate_bvalue_with_limit(Value0, Lim, Value) % we show maximally 10 lines a 40 chars
53		; Value = unknown).
54		get_value_string_of_formula(_State, _LocalState, _Expr, _, unknown).
55
56		% (error(representation_error(max_clpfd_integer)
57
58		:- use_module(probsrc(b_interpreter), [
59		b_test_boolean_expression_cs/5,
60		b_not_test_boolean_expression_cs/5]).
61
62		get_bool_expr_value(Expr,LocalState,State,Value) :-
63		catch(get_bool_expr_val2(Expr,LocalState,State,Value), E, (
64		add_exception_warning('Exception in bvisual while evaluating predicate: ', E),
65		Value=undefined
66		)).
67		get_bool_expr_val2(Expr,LocalState,State,Value) :-
68		( b_test_boolean_expression_cs(Expr,LocalState,State,'formula visualisation',0) ->
69		( b_not_test_boolean_expression_cs(Expr,LocalState,State,'formula visualisation (negated)',0)
70		-> Value = x_both_true_and_not_true, % was x_unknown_true_and_not_true
71		% we should add an error message here
72		% this should never happen
73		print('### Error, x_both_true_and_not_true: '), print(Expr),nl
74		; Value = true
75		)
76		; b_not_test_boolean_expression_cs(Expr,LocalState,State,'formula visualisation',0) ->
77		Value = false
78		%, print(value_false),nl
79		;
80		Value = undefined % was x_undefined_false_and_not_false
81		%, print(value_undefined),nl
82		).
83
84		add_exception_warning(_,E) :- is_enumeration_warning_exception(E),!.
85		add_exception_warning(Msg,E) :-
86		add_warning(bvisual,Msg,E).
87
88		:- use_module(probsrc(b_interpreter),[b_compute_expression_nowf/6]).
89
90		b_compute_expression_no_wd(Fun, LocalState, State, FunValue) :-
91		temporary_set_preference(disprover_mode,true,CHNG), % avoid WD Errors, we detect WD issues by failure below
92		temporary_set_preference(find_abort_values,false,CHNG2),
93		(catch(
94		b_compute_expression_nowf(Fun, LocalState, State, FunValue,'formula visualisation',0),
95		E,
96		(add_exception_warning('Exception in bvisual while evaluating expression: ',E),fail)
97		)
98		-> reset_temporary_preference(disprover_mode,CHNG),
99		reset_temporary_preference(find_abort_values,CHNG2)
100		; reset_temporary_preference(disprover_mode,CHNG),
101		reset_temporary_preference(find_abort_values,CHNG2), fail).
102
103