1		% (c) 2015-2023 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
5		:- module(prob_state_predicates, [create_state_pred/4, create_state_pred/5]).
6
7		:- use_module(library(lists), [maplist/2]).
8
9		:- use_module(probsrc(bsyntaxtree), [safe_create_texpr/3,
10		conjunct_predicates/2]).
11		:- use_module(probsrc(translate), [translate_bexpression/2]).
12		:- use_module(probsrc(debug), [debug_format/3]).
13		:- use_module(probsrc(kernel_tools),[ground_value/1]).
14		:- use_module(probsrc(b_global_sets), [is_b_global_constant/3]).
15		:- use_module(probsrc(custom_explicit_sets), [expand_custom_set_to_list_now/2]).
16		:- use_module(probsrc(clpfd_interface), [clpfd_domain/3]).
17		:- use_module(probsrc(error_manager), [add_error/4]).
18
19		:- use_module(probsrc(module_information),[module_info/2]).
20		:- module_info(group,smt_solvers).
21		:- module_info(description,'This module translates ProB\'s (local) states to predicates understandable for CVC4/Z3').
22
23		create_state_pred(IDs,LS,S,P) :-
24		create_state_pred(IDs,LS,S,P,[allow_to_skip_vars(_)]).
25
26		create_state_pred(IDs,LS,S,P,Opts) :-
27		create_state_preds(IDs,LS,S,Preds,Opts),
28		conjunct_predicates(Preds,P),
29		translate_bexpression(P,PP),
30		debug_format(9,'smt_solvers_interface state_pred: ~w~n', [PP]).
31		create_state_preds([],_,_,[b(truth,pred,[])],_).
32		create_state_preds([b(identifier(Name),Type,Infos)|IDs],LS,S,[SubPred|Preds],Opts) :-
33	?	( member(bind(Name,Value),LS)
34	?	; member(bind(Name,Value),S)
35		),!,
36		create_state_preds_aux(Name,Type,Infos,Value,SubPred,Opts),
37		create_state_preds(IDs,LS,S,Preds,Opts).
38		create_state_preds([_|IDs],LS,S,Preds,Opts) :-
39		create_state_preds(IDs,LS,S,Preds,Opts).
40
41		% for integers: create fd interval
42		create_state_preds_aux(Name,integer,Infos,int(Value),Pred,_) :- !,
43		(number(Value) ->
44		safe_create_texpr(integer(Value),integer,TVal),
45		safe_create_texpr(equal(b(identifier(Name),integer,Infos),TVal),pred,Pred)
46		;
47		clpfd_domain(Value,Min,Max),
48		(number(Min)
49		-> safe_create_texpr(integer(Min),integer,MinValue),
50		safe_create_texpr(greater_equal(b(identifier(Name),integer,Infos),MinValue),pred,Greater)
51		; Greater = b(truth,pred,[])),
52		(number(Max)
53		-> safe_create_texpr(integer(Max),integer,MaxValue),
54		safe_create_texpr(less_equal(b(identifier(Name),integer,Infos),MaxValue),pred,Less)
55		; Less = b(truth,pred,[])),
56		conjunct_predicates([Less,Greater],Pred)
57		).
58		% non-integers: create equality if ground and simple enough
59		create_state_preds_aux(Name,Type,Infos,Value,Pred,_) :-
60		ground_value(Value),
61		useful_value_for_state_pred(Value), !,
62		Pred = b(equal(b(identifier(Name),Type,Infos),b(value(Value),Type,[])),pred,[]).
63		% else: create truth (i.e. no futher state information)
64		create_state_preds_aux(ID,_,_,Val,b(truth,pred,[]),Opts) :-
65		(var(Val) % for :z3 these are the quantified variables themselves; in general we should ensure there are no constraints, co-routines pending on Val
66		; member(allow_to_skip_vars(true),Opts)
67		-> debug_format(19,'Not creating state predicate for ~w (value too complex)~n',[ID])
68		; member(skipped_variables(L),Opts), member(ID,L)
69		-> debug_format(19,'Not creating state predicate for ~w (value too complex)~n',[ID])
70		),
71		!.
72		create_state_preds_aux(ID,_,Infos,Val,b(truth,pred,[]),_) :-
73		translate:print_bvalue(Val),nl,
74		add_error(create_state_pred,'Ignoring value (too complex) for identifier',ID,Infos). % TO DO: enum warning ; if no solution found ok
75
76
77		useful_value_for_state_pred([]). % empty sets
78		useful_value_for_state_pred([H|T]) :- % sets as lists
79		maplist(useful_value_for_state_pred,[H|T]).
80		useful_value_for_state_pred(avl_set(Val)) :-
81		expand_custom_set_to_list_now(avl_set(Val),Values),
82		maplist(useful_value_for_state_pred,Values).
83		useful_value_for_state_pred(int(Nr)) :- number(Nr).
84		useful_value_for_state_pred(term(floating(Nr))) :- number(Nr).
85		useful_value_for_state_pred(pred_true).
86		useful_value_for_state_pred(pred_false).
87		useful_value_for_state_pred(global_set(_)).
88		useful_value_for_state_pred(fd(Num,Name)) :-
89		is_b_global_constant(Name,Num,_).
90		%useful_value_for_state_pred(rec(Fields)) :- useful_fields(Fields). % mk_value failed for test 1719 if we comment this in
91		useful_value_for_state_pred((A,B)) :-
92		useful_value_for_state_pred(A),
93		useful_value_for_state_pred(B).
94
95		%useful_fields([]).
96		%useful_fields([field(_,Val)|T]) :- useful_value_for_state_pred(Val),useful_fields(T).