1		% (c) 2015-2019 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]).
6
7		:- use_module(probsrc(module_information),[module_info/2]).
8		:- module_info(group,smt_solvers).
9		:- module_info(description,'This module translates ProB\'s (local) states to predicates understandable for CVC4/Z3').
10
11		:- use_module(library(lists), [maplist/2]).
12
13		:- use_module(probsrc(bsyntaxtree), [get_texpr_id/2,
14		safe_create_texpr/3,
15		conjunct_predicates/2]).
16		:- use_module(probsrc(translate), [translate_bexpression/2]).
17		:- use_module(probsrc(debug), [debug_format/3]).
18		:- use_module(probsrc(b_global_sets), [is_b_global_constant/3]).
19		:- use_module(probsrc(custom_explicit_sets), [expand_custom_set_to_list_now/2]).
20		:- use_module(probsrc(clpfd_interface), [clpfd_domain/3]).
21
22		create_state_pred(IDs,LS,S,P) :-
23		create_state_preds(IDs,LS,S,Preds),
24		conjunct_predicates(Preds,P),
25		translate_bexpression(P,PP),
26		debug_format(9,'smt_solvers_interface state_pred: ~w~n', [PP]).
27		create_state_preds([],_,_,[b(truth,pred,[])]).
28		create_state_preds([ID|IDs],LS,S,[SubPred|Preds]) :-
29		get_texpr_id(ID,Identifier),
30		member(bind(Identifier,Value),LS), !,
31		create_state_preds_aux(ID,Value,SubPred),
32		create_state_preds(IDs,LS,S,Preds).
33		create_state_preds([ID|IDs],LS,S,[SubPred|Preds]) :-
34		get_texpr_id(ID,Identifier),
35		member(bind(Identifier,Value),S), !,
36		create_state_preds_aux(ID,Value,SubPred),
37		create_state_preds(IDs,LS,S,Preds).
38		create_state_preds([_|IDs],LS,S,Preds) :-
39		create_state_preds(IDs,LS,S,Preds).
40
41		% for integers: create fd interval
42		create_state_preds_aux(b(identifier(Name),integer,Infos),int(Value),Pred) :- !,
43		clpfd_domain(Value,Min,Max),
44		(number(Min)
45		-> safe_create_texpr(integer(Min),integer,MinValue),
46		safe_create_texpr(greater_equal(b(identifier(Name),integer,Infos),MinValue),pred,Greater)
47		; Greater = b(truth,pred,[])),
48		(number(Max)
49		-> safe_create_texpr(integer(Max),integer,MaxValue),
50		safe_create_texpr(less_equal(b(identifier(Name),integer,Infos),MaxValue),pred,Less)
51		; Less = b(truth,pred,[])),
52		conjunct_predicates([Less,Greater],Pred).
53		% non-integers: create equality if ground and simple enough
54		create_state_preds_aux(b(identifier(Name),Type,Infos),Value,Pred) :-
55		ground(Value), useful_value_for_state_pred(Value), !,
56		Pred = b(equal(b(identifier(Name),Type,Infos),b(value(Value),Type,[])),pred,[]).
57		% else: create truth (i.e. no futher state information)
58		create_state_preds_aux(_,_,b(truth,pred,[])).
59
60		useful_value_for_state_pred([]). % empty sets
61		useful_value_for_state_pred([H|T]) :- % sets as lists
62		maplist(useful_value_for_state_pred,[H|T]).
63		useful_value_for_state_pred(avl_set(Val)) :-
64		expand_custom_set_to_list_now(avl_set(Val),Values),
65		maplist(useful_value_for_state_pred,Values).
66		useful_value_for_state_pred(pred_true).
67		useful_value_for_state_pred(pred_false).
68		useful_value_for_state_pred(global_set(_)).
69		useful_value_for_state_pred(fd(Num,Name)) :-
70		is_b_global_constant(Name,Num,_).
71		useful_value_for_state_pred((A,B)) :-
72		useful_value_for_state_pred(A),
73		useful_value_for_state_pred(B).