1		% (c) 2014-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(predicate_handling,[prime_predicate/2,
6		create_state_predicate/2,
7		create_succ_state_predicate/2,
8		create_constants_state_predicate/2,
9		get_initial_state_predicate/1,
10		get_transition_predicate/1,
11		get_single_transition_predicate/2,
12		create_negation_and_cleanup/2,
13		create_primary_inputs_predicate/2,
14		deprime_state/2,
15		prime_n_times/3,
16		unprimed/1]).
17
18		:- use_module(probsrc(module_information)).
19		:- module_info(group,symbolic_model_checker).
20		:- module_info(description,'Handling and creation of predicates used in the symbolic model checker.').
21
22		:- use_module(library(lists)).
23
24		:- use_module(probsrc(b_global_sets), [b_global_set/1,
25		is_b_global_constant/3]).
26		:- use_module(probsrc(bmachine),[b_get_machine_operation/4,
27		b_get_machine_constants/1,
28		b_get_machine_variables/1,
29		b_get_initialisation_from_machine/2,
30		b_get_properties_from_machine/1,
31		get_proven_invariant/2]).
32		:- use_module(probsrc(before_after_predicates),[before_after_predicate_with_equalities/3,
33		before_after_predicate_list_disjunct_with_equalities/3,
34		before_after_predicate_for_operation/2]).
35		:- use_module(probsrc(bsyntaxtree), [conjunct_predicates/2,
36		disjunct_predicates/2,
37		disjunction_to_list/2,
38		transform_bexpr/3,
39		syntaxtransformation/5,
40		create_texpr/4,
41		safe_create_texpr/3,
42		create_negation/2,
43		get_texpr_expr/2,
44		get_texpr_type/2,
45		unique_typed_id/3]).
46
47		:- use_module(probsrc(preferences), [get_preference/2]).
48
49		get_initial_state_predicate(Init) :-
50		% the initial state contains both the constants defined by the properties
51		% and the variables set by the initialisation
52		b_get_properties_from_machine(Properties),
53		b_get_initialisation_from_machine(Initialisation,_),
54		before_after_predicate_with_equalities(Initialisation,[],InitialisationPred),
55		conjunct_predicates([Properties,InitialisationPred],PredWithPrimes),
56		transform_bexpr(predicate_handling:remove_prime_from_expression,PredWithPrimes,Init).
57
58		get_transition_predicate(TransitionPredicate) :-
59		get_preference(use_po,false), !,
60		findall(Body,b_get_machine_operation(_Name,_Results,_Parameters,Body),ListOfBodies),
61		b_get_machine_variables(Variables),
62		b_get_machine_constants(Constants),
63		append(Variables,Constants,VarsAndConsts),
64		before_after_predicate_list_disjunct_with_equalities(ListOfBodies,VarsAndConsts,TransitionPredicateNoInputs),
65		add_primary_inputs(TransitionPredicateNoInputs,TransitionPredicate).
66		get_transition_predicate(TransitionPredicate) :-
67		get_preference(use_po,true), !,
68		findall(op(OpName,Pred),(before_after_predicate_for_operation(OpName,Pred)),Ops),
69		maplist(op_to_transition,Ops,SingleSteps),
70		disjunct_predicates(SingleSteps,TransitionPredicateNoInputs),
71		add_primary_inputs(TransitionPredicateNoInputs,TransitionPredicate).
72
73		op_to_transition(op(OpName,BaPred),StepConstraint) :-
74		(get_proven_invariant(OpName,ProvenInvariant)
75		-> true ; ProvenInvariant = b(truth,pred,[])),
76		prime_predicate(ProvenInvariant,PrimedProvenInvariant),
77		conjunct_predicates([BaPred,PrimedProvenInvariant],StepConstraint).
78
79		get_single_transition_predicate(OpName,TP) :-
80		b_get_machine_operation(OpName,_Results,_Parameters,Body),
81		b_get_machine_variables(Variables),
82		b_get_machine_constants(Constants),
83		append(Variables,Constants,VarsAndConsts),
84		before_after_predicate_with_equalities(Body,VarsAndConsts,TransitionPredicateNoInputs),
85		add_primary_inputs(TransitionPredicateNoInputs,TP).
86
87		:- meta_predicate maplist(4,-,-,-,-).
88		maplist(Pred, As, Bs, Cs, Ds) :-
89		(foreach(A,As),
90		foreach(B,Bs),
91		foreach(C,Cs),
92		foreach(D,Ds),
93		param(Pred)
94		do call(Pred, A, B, C, D)
95		).
96
97		add_primary_inputs(TIn,TOut) :-
98		% transition is a disjunction
99		% as a first step add an integer variable to each disjunct
100		% + a constraint stating that the sum is 1
101		disjunction_to_list(TIn,Disjuncts),
102		maplist(add_input_to_op,Disjuncts,TopLevelIdentifiers,_InnerIdentifiers,DisjunctsOut),
103		sum_is_one(TopLevelIdentifiers,Constraint),
104		disjunct_predicates(DisjunctsOut,Disjunction),
105		conjunct_predicates([Disjunction,Constraint],TOut).
106
107		add_input_to_op(Op,IId,InnerIIds,OpOut) :-
108		unique_typed_id("_ic3_pi",integer,IId),
109		safe_create_texpr(integer(1),integer,Int1),
110		safe_create_texpr(equal(IId,Int1),pred,EqualToOne),
111		add_inner_inputs_to_op(Op,InnerIIds,Op2),
112		conjunct_predicates([Op2,EqualToOne],OpOut).
113
114		% add variables to substitutions like ANY, etc.
115		% these variables should make the substitution deterministic
116		% once they are fixed to a value
117		add_inner_inputs_to_op(Subst,Ids,SubstOut) :-
118		get_texpr_expr(Subst,Expr),
119		add_inner_inputs_to_op_aux(Expr,Ids,ExprOut), !,
120		safe_create_texpr(ExprOut,pred,SubstOut).
121		%add_inner_inputs_to_op(Subst,[],Subst) :-
122		% translate:translate_bexpression(Subst,PPSubst),
123		% format('not implemented in add_inner_inputs_to_op: ~w~n',[PPSubst]).
124		add_inner_inputs_to_op(Subst,[],Subst).
125		% these might contain a non-deterministic choice somewhere
126		add_inner_inputs_to_op_aux(conjunct(A,B),Ids,conjunct(NA,NB)) :- !,
127		add_inner_inputs_to_op(A,AIds,NA),
128		add_inner_inputs_to_op(B,BIds,NB),
129		append(AIds,BIds,Ids).
130		add_inner_inputs_to_op_aux(disjunct(A,B),Ids,disjunct(NA,NB)) :- !,
131		add_inner_inputs_to_op(A,AIds,NA),
132		add_inner_inputs_to_op(B,BIds,NB),
133		append(AIds,BIds,Ids).
134		% these have a non-deterministic choice. add a variable.
135		add_inner_inputs_to_op_aux(member(A,B),[InputId],conjunct(b(member(A,B),pred,[]),Eq)) :- !,
136		get_texpr_type(A,Type),
137		unique_typed_id("_ic3_pi",Type,InputId),
138		safe_create_texpr(equal(A,InputId),pred,Eq).
139		% these should always be deterministic
140		add_inner_inputs_to_op_aux(equal(A,B),[],equal(A,B)) :- !.
141
142		sum_is_one(Identifiers,Constraint) :-
143		build_sum(Identifiers,Sum),
144		safe_create_texpr(integer(1),integer,Int1),
145		safe_create_texpr(equal(Sum,Int1),pred,Constraint).
146
147		build_sum([Id],Id).
148		build_sum([Id|Ids],Sum) :-
149		build_sum(Ids,SubSum),
150		safe_create_texpr(add(Id,SubSum),integer,Sum).
151
152		remove_prime_from_binding(binding(Id,Res,PP),binding(NId,Res,PP)) :-
153		remove_prime(Id,NId).
154
155		remove_prime_from_expression(b(identifier(Id),Type,Infos),b(identifier(NId),Type,Infos)) :- !,
156		remove_prime(Id,NId).
157		remove_prime_from_expression(Expr,Expr).
158
159		remove_prime(Id,NoPrimeId) :-
160		atom_codes(Id,Codes),
161		append(NoPrimeIdCodes,[39],Codes), !, % last character is 39 = prime
162		atom_codes(NoPrimeId,NoPrimeIdCodes).
163		remove_prime(Id,Id).
164
165		create_state_predicate(Solution,StatePredicate) :-
166		include(unprimed,Solution,UPSolution),
167		create_state_predicate_aux(UPSolution,StatePredicate).
168
169		create_succ_state_predicate(Solution,SStatePredicate) :-
170		deprime_state(Solution,DePrimedState),
171		create_state_predicate_aux(DePrimedState,SStatePredicate).
172
173		deprime_state(State,DeprimedState) :-
174		include(primed,State,PSolution),
175		maplist(remove_prime_from_binding,PSolution,DeprimedState).
176
177		create_constants_state_predicate(Solution,ConstantsStatePred) :-
178		include(unprimed,Solution,UPSolution),
179		b_get_machine_constants(Csts),
180		include(filter_vars_and_constants(Csts),UPSolution,UPSolutionOnlyConstants),
181		UPSolutionOnlyConstants \= [],
182		create_state_predicate_aux(UPSolutionOnlyConstants,ConstantsStatePred).
183
184		create_primary_inputs_predicate(Solution,InputsPred) :-
185		exclude(primed,Solution,NoPrimes),
186		include(primary_input,NoPrimes,NoPrimesNoState),
187		maplist(create_single_assignment_predicate(NoPrimesNoState),NoPrimesNoState,SolutionPreds),
188		conjunct_predicates(SolutionPreds,InputsPred).
189
190		create_state_predicate_aux(Solution,StatePredicate) :-
191		b_get_machine_variables(Vars), b_get_machine_constants(Csts),
192		append(Vars,Csts,VandC),
193		include(filter_vars_and_constants(VandC),Solution,SolutionOnlyStateVars),
194		maplist(create_single_assignment_predicate(VandC),SolutionOnlyStateVars,SolutionPreds),
195		conjunct_predicates(SolutionPreds,StatePredicate).
196
197		create_single_assignment_predicate(VandC,binding(Name,Value,_PP),Pred) :-
198		% fetch the type for the particular variable / constant
199		member(b(identifier(Name),Type,Infos),VandC),
200		Pred = b(equal(b(identifier(Name),Type,Infos),b(value(Value),Type,[])),pred,[]).
201
202		filter_vars_and_constants(VandC,binding(Id,_,_)) :-
203		member(b(identifier(Id),_,_),VandC).
204
205		unprimed(binding(Id,_,_)) :- atom_codes(Id,Codes), \+last(Codes,39).
206		primed(binding(Id,_,_)) :- atom_codes(Id,Codes), last(Codes,39).
207
208		primary_input(binding(Id,_,_)) :- atom_codes(Id,Codes), prefix("_ic3_pi", Codes).
209
210		prime_predicate(A,B) :-
211		create_texpr(OExpr,Type,Info,A),
212		create_texpr(NExpr,Type,Info,B),
213		prime_texpr(OExpr,Type,NExpr).
214
215		% certain identifiers should not be primed
216		% global sets
217		do_not_prime_identifier(Id,set(global(Id))) :-
218		b_global_set(Id).
219		% members of global sets
220		do_not_prime_identifier(MId,global(SId)) :-
221		is_b_global_constant(SId,_,MId).
222
223		prime_texpr(identifier(Old),Type,identifier(New)) :-
224		% write(pt(Old,Type)), nl,
225		do_not_prime_identifier(Old,Type), !,
226		Old = New.
227		prime_texpr(identifier(Old),_Type,identifier(New)) :- !,
228		atom_concat(Old,'\'',New).
229		prime_texpr(lazy_lookup_expr(Old),_,lazy_lookup_expr(New)) :-
230		!, atom_concat(Old,'\'',New).
231		prime_texpr(lazy_lookup_pred(Old),_,lazy_lookup_pred(New)) :-
232		!, atom_concat(Old,'\'',New).
233		prime_texpr(OExpr,_,NExpr) :-
234		syntaxtransformation(OExpr,Subs,_TNames,NSubs,NExpr),
235		prime_texpr_l(Subs,NSubs).
236		prime_texpr_l([],[]).
237
238		prime_texpr_l([Old|ORest],[New|NRest]) :-
239		prime_predicate(Old,New),
240		prime_texpr_l(ORest,NRest).
241
242		% involves specialised cleanup rules for atb provers
243		create_negation_and_cleanup(P,NP) :-
244		get_texpr_expr(P,implication(A,B)), !,
245		create_negation_and_cleanup(B,NegB),
246		safe_create_texpr(conjunct(A,NegB),pred,NP).
247		create_negation_and_cleanup(P,NP) :-
248		create_negation(P,NP).
249
250		prime_n_times(0,P,P) :- !.
251		prime_n_times(N,P,Primed) :-
252		prime_predicate(P,T),
253		N2 is N - 1,
254		prime_n_times(N2,T,Primed).