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