1 | % (c) 2014-2015 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(smtlib2_translation,[smt_type_to_prob_type/3, | |
6 | smt_term_to_prob_term/3, | |
7 | smt_type_to_prob_type_maplist/3, | |
8 | smt_term_to_prob_term_maplist/3, | |
9 | bool_to_pred/2, | |
10 | typing_constraint/2, | |
11 | is_function_constraint/3]). | |
12 | ||
13 | :- use_module(probsrc(module_information),[module_info/2]). | |
14 | :- module_info(group,smtlib). | |
15 | :- module_info(description,'The SMT-LIB 2 Interpreter - Translation from SMT-LIB 2 to B'). | |
16 | ||
17 | :- use_module(library(lists)). | |
18 | ||
19 | :- use_module(probsrc(bsyntaxtree),[get_texpr_type/2, | |
20 | get_texpr_expr/2, | |
21 | safe_create_texpr/3, | |
22 | create_forall/3, | |
23 | create_exists/3, | |
24 | create_couple/2, | |
25 | conjunct_predicates/2, | |
26 | replace_id_by_expr/4]). | |
27 | ||
28 | :- use_module(smtlib_solver(smtlib2_environment)). | |
29 | ||
30 | chain(Op,[A,B],BPred) :- !, | |
31 | Pred =.. [Op,A,B], | |
32 | BPred = b(Pred,pred,[]). | |
33 | chain(Op,[First,Second|Further],TermOut) :- | |
34 | chain(Op,[First,Second],Pred), | |
35 | chain(Op,[Second|Further],FurtherPred), | |
36 | conjunct_predicates([Pred,FurtherPred],TermOut). | |
37 | ||
38 | interleave(_Op,[A],A). | |
39 | interleave(Op,[First|Further],TermOut) :- | |
40 | interleave(Op,Further,FurtherPred), | |
41 | get_texpr_type(FurtherPred,FurtherType), | |
42 | Pred =.. [Op,First,FurtherPred], | |
43 | safe_create_texpr(Pred,FurtherType,TermOut). | |
44 | ||
45 | smt_type_to_prob_type(sort('Int'),_,integer) :- !. | |
46 | smt_type_to_prob_type(sort('Bool'),_,boolean) :- !. | |
47 | smt_type_to_prob_type(sort('Array',[From,To]),E,Out) :- !, | |
48 | smt_type_to_prob_type(From,E,FromType), | |
49 | smt_type_to_prob_type(To,E,ToType), | |
50 | Out = set(couple(FromType,ToType)). | |
51 | smt_type_to_prob_type(sort('BitVec',[_Length]),_E,Out) :- !, | |
52 | Out = set(couple(integer,integer)). | |
53 | smt_type_to_prob_type(sort('Set',[Sub]),E,Out) :- !, | |
54 | smt_type_to_prob_type(Sub,E,SubType), | |
55 | Out = set(SubType). | |
56 | smt_type_to_prob_type(sort(X),E,global(X)) :- | |
57 | is_custom_type(E,X), !. | |
58 | smt_type_to_prob_type(X,_,_) :- !, format('missing in smt_type_to_prob_type: ~w~n',[X]), fail. | |
59 | ||
60 | % special versions for maplist that keeps first argument indexing | |
61 | smt_term_to_prob_term_maplist(E,I,O) :- | |
62 | smt_term_to_prob_term(I,E,O). | |
63 | smt_type_to_prob_type_maplist(E,I,O) :- | |
64 | smt_type_to_prob_type(I,E,O). | |
65 | ||
66 | smt_term_to_prob_term(attributed_term(Term,_Attr),Env,Out) :- !, | |
67 | smt_term_to_prob_term(Term,Env,Out). | |
68 | smt_term_to_prob_term(id_term(id('not'),[Arg]),Env,Out) :- !, | |
69 | smt_term_to_prob_term(Arg,Env,BArg), | |
70 | get_texpr_type(BArg,Type), | |
71 | (Type = pred | |
72 | -> Out = b(negation(BArg),pred,[]) | |
73 | ; Out = b(equal(BArg,b(boolean_false,boolean,[])),pred,[])). | |
74 | smt_term_to_prob_term(id_term(id('-'),[SingleArg]),Env,Out) :- !, | |
75 | % special case for unary minus: can not be interleaved | |
76 | smt_term_to_prob_term(SingleArg,Env,BArg), | |
77 | Out = b(unary_minus(BArg),integer,[]). | |
78 | smt_term_to_prob_term(id_term(id('='),Args),Env,Out) :- !, | |
79 | maplist(smt_term_to_prob_term_maplist(Env),Args,BArgs), | |
80 | maplist(get_texpr_type,BArgs,Types), | |
81 | (member(pred,Types) | |
82 | -> maplist(bool_to_pred,BArgs,BArgsPreds), | |
83 | chain(equivalence,BArgsPreds,Out) | |
84 | ; chain(equal,BArgs,Out)). | |
85 | smt_term_to_prob_term(id_term(id('ite'),[Test,If,Then]),Env,Out) :- !, | |
86 | smt_term_to_prob_term(Test,Env,BTestT), | |
87 | smt_term_to_prob_term(If,Env,BIfT), | |
88 | smt_term_to_prob_term(Then,Env,BThenT), | |
89 | bool_to_pred(BTestT,BTest), | |
90 | to_bool_if_necessary(BIfT,BIf), | |
91 | to_bool_if_necessary(BThenT,BThen), | |
92 | get_texpr_type(BIf,Type), | |
93 | Out = b(if_then_else(BTest,BIf,BThen),Type,[]). | |
94 | % set logic | |
95 | smt_term_to_prob_term(id_term(id(member),[Element,Set]),Env,Out) :- !, | |
96 | smt_term_to_prob_term(Set,Env,BSet), | |
97 | smt_term_to_prob_term(Element,Env,BElement), | |
98 | Out = b(member(BElement,BSet),pred,[]). | |
99 | smt_term_to_prob_term(id_term(id(card),[Set]),Env,Out) :- !, | |
100 | smt_term_to_prob_term(Set,Env,BSet), | |
101 | Out = b(card(BSet),integer,[]). | |
102 | smt_term_to_prob_term(id_term(id(singleton),[Element]),Env,Out) :- !, | |
103 | smt_term_to_prob_term(Element,Env,BElement), | |
104 | get_texpr_type(BElement,ElementType), | |
105 | Out = b(set_extension([BElement]),set(ElementType),[]). | |
106 | smt_term_to_prob_term(id_term(id(union),[SetA,SetB]),Env,Out) :- !, | |
107 | smt_term_to_prob_term(SetA,Env,BSetA), | |
108 | smt_term_to_prob_term(SetB,Env,BSetB), | |
109 | get_texpr_type(BSetB,Type), | |
110 | Out = b(union(BSetA,BSetB),Type,[]). | |
111 | smt_term_to_prob_term(id_term(id(intersection),[SetA,SetB]),Env,Out) :- !, | |
112 | smt_term_to_prob_term(SetA,Env,BSetA), | |
113 | smt_term_to_prob_term(SetB,Env,BSetB), | |
114 | get_texpr_type(BSetB,Type), | |
115 | Out = b(intersection(BSetA,BSetB),Type,[]). | |
116 | smt_term_to_prob_term(id_term(id(subset),[SetA,SetB]),Env,Out) :- !, | |
117 | smt_term_to_prob_term(SetA,Env,BSetA), | |
118 | smt_term_to_prob_term(SetB,Env,BSetB), | |
119 | Out = b(subset(BSetA,BSetB),pred,[]). | |
120 | % array logics | |
121 | smt_term_to_prob_term(id_term(id('store'),[Array,Index,Element]),Env,Out) :- !, | |
122 | smt_term_to_prob_term(Array,Env,BArray), | |
123 | get_texpr_type(BArray,ArrayType), | |
124 | ArrayType = set(CoupleType), | |
125 | smt_term_to_prob_term(Index,Env,BIndex), | |
126 | smt_term_to_prob_term(Element,Env,BElement), | |
127 | SetEx = b(set_extension([b(couple(BIndex,BElement),CoupleType,[])]),ArrayType,[]), | |
128 | Out = b(overwrite(BArray,SetEx),ArrayType,[]). | |
129 | smt_term_to_prob_term(id_term(id('select'),[Array,Index]),Env,Out) :- !, | |
130 | smt_term_to_prob_term(Array,Env,BArray), | |
131 | get_texpr_type(BArray,ArrayType), | |
132 | ArrayType = set(couple(_From,To)), | |
133 | smt_term_to_prob_term(Index,Env,BIndex), | |
134 | Out = b(function(BArray,BIndex),To,[]). | |
135 | % bitvector logics | |
136 | smt_term_to_prob_term(id_term(id('concat'),[A,B]),Env,Out) :- !, | |
137 | smt_term_to_prob_term(A,Env,BA), | |
138 | smt_term_to_prob_term(B,Env,BB), | |
139 | bvwidth(BA,WidthA), | |
140 | bvwidth(BB,WidthB), | |
141 | WidthBP1 = b(add(WidthB,Int1),integer,[]), | |
142 | Int0 = b(integer(0),integer,[]), | |
143 | Int1 = b(integer(1),integer,[]), | |
144 | IdX1 = b(identifier('\\tmp1'),integer,[]), | |
145 | IdX2 = b(identifier('\\tmp2'),integer,[]), | |
146 | FullWidth = b(add(b(add(WidthA,WidthB),integer,[]),Int1),integer,[]), | |
147 | TypeOfX1 = b(member(IdX1,b(interval(Int0,FullWidth),set(integer),[])),pred,[]), | |
148 | TypeOfX2 = b(member(IdX2,b(interval(Int0,Int1),set(integer),[])),pred,[]), | |
149 | ValOfX2 = b(if_then_else(b(less_equal(IdX1,WidthB),pred,[]), | |
150 | b(function(BB,IdX1),integer,[]), | |
151 | b(function(BA,b(minus(IdX1,WidthBP1),integer,[])),integer,[])),integer,[]), | |
152 | conjunct_predicates([TypeOfX1,TypeOfX2,b(equal(IdX2,ValOfX2),pred,[])],Pred), | |
153 | Out = b(comprehension_set([IdX1,IdX2],Pred),set(couple(integer,integer)),[]). | |
154 | smt_term_to_prob_term(id_term(id(zero_extend(NewLength)),[A]),Env,Out) :- !, | |
155 | smt_term_to_prob_term(A,Env,BA), | |
156 | bvwidth(BA,WidthA), | |
157 | WidthAP1 = b(add(WidthA,Int1),integer,[]), | |
158 | Int0 = b(integer(0),integer,[]), | |
159 | Int1 = b(integer(1),integer,[]), | |
160 | IdX1 = b(identifier('\\tmp1'),integer,[]), | |
161 | IdX2 = b(identifier('\\tmp2'),integer,[]), | |
162 | FullWidth = b(add(WidthA,b(integer(NewLength),integer,[])),integer,[]), | |
163 | TypeOfX1 = b(member(IdX1,b(interval(Int0,FullWidth),set(integer),[])),pred,[]), | |
164 | TypeOfX2 = b(member(IdX2,b(interval(Int0,Int1),set(integer),[])),pred,[]), | |
165 | ValOfX2 = b(if_then_else(b(less_equal(IdX1,WidthA),pred,[]), | |
166 | b(integer(0),integer,[]), | |
167 | b(function(BA,b(minus(IdX1,WidthAP1),integer,[])),integer,[])),integer,[]), | |
168 | conjunct_predicates([TypeOfX1,TypeOfX2,b(equal(IdX2,ValOfX2),pred,[])],Pred), | |
169 | Out = b(comprehension_set([IdX1,IdX2],Pred),set(couple(integer,integer)),[]). | |
170 | smt_term_to_prob_term(id_term(id(sign_extend(NewLength)),[A]),Env,Out) :- !, | |
171 | smt_term_to_prob_term(A,Env,BA), | |
172 | bvwidth(BA,WidthA), | |
173 | Int0 = b(integer(0),integer,[]), | |
174 | Int1 = b(integer(1),integer,[]), | |
175 | IdX1 = b(identifier('\\tmp1'),integer,[]), | |
176 | IdX2 = b(identifier('\\tmp2'),integer,[]), | |
177 | WidthAP1 = b(add(WidthA,Int1),integer,[]), | |
178 | FullWidth = b(add(WidthA,b(integer(NewLength),integer,[])),integer,[]), | |
179 | TypeOfX1 = b(member(IdX1,b(interval(Int0,FullWidth),set(integer),[])),pred,[]), | |
180 | TypeOfX2 = b(member(IdX2,b(interval(Int0,Int1),set(integer),[])),pred,[]), | |
181 | ValOfX2 = b(if_then_else(b(less_equal(IdX1,WidthA),pred,[]), | |
182 | b(function(BA,IdX1),integer,[]), | |
183 | b(function(BA,b(minus(IdX1,WidthAP1),integer,[])),integer,[])),integer,[]), | |
184 | conjunct_predicates([TypeOfX1,TypeOfX2,b(equal(IdX2,ValOfX2),pred,[])],Pred), | |
185 | Out = b(comprehension_set([IdX1,IdX2],Pred),set(couple(integer,integer)),[]). | |
186 | smt_term_to_prob_term(id_term(id(extract(I,J)),[S]),Env,Out) :- !, | |
187 | BI = b(integer(I),integer,[]), | |
188 | BJ = b(integer(J),integer,[]), | |
189 | smt_term_to_prob_term(S,Env,BS), | |
190 | Int0 = b(integer(0),integer,[]), | |
191 | Int1 = b(integer(1),integer,[]), | |
192 | DomX1 = b(add(b(minus(BI,BJ),integer,[]),Int1),integer,[]), | |
193 | IdX1 = b(identifier('\\tmp1'),integer,[]), | |
194 | IdX2 = b(identifier('\\tmp2'),integer,[]), | |
195 | TypeOfX1 = b(member(IdX1,b(interval(Int0,DomX1),set(integer),[])),pred,[]), | |
196 | TypeOfX2 = b(member(IdX2,b(interval(Int0,Int1),set(integer),[])),pred,[]), | |
197 | ValOfX2 = b(function(BS,IdX1),integer,[]), | |
198 | conjunct_predicates([TypeOfX1,TypeOfX2,b(equal(IdX2,ValOfX2),pred,[])],Pred), | |
199 | Out = b(comprehension_set([IdX1,IdX2],Pred),set(couple(integer,integer)),[]). | |
200 | smt_term_to_prob_term(id_term(id('bvnot'),[A]),Env,Out) :- !, | |
201 | smt_term_to_prob_term(A,Env,BA), | |
202 | bvwidth(BA,Width), | |
203 | Int0 = b(integer(0),integer,[]), | |
204 | Int1 = b(integer(1),integer,[]), | |
205 | IdX1 = b(identifier('\\tmp1'),integer,[]), | |
206 | IdX2 = b(identifier('\\tmp2'),integer,[]), | |
207 | TypeOfX1 = b(member(IdX1,b(interval(Int0,Width),set(integer),[])),pred,[]), | |
208 | TypeOfX2 = b(member(IdX2,b(interval(Int0,Int1),set(integer),[])),pred,[]), | |
209 | ValOfX2 = b(if_then_else(b(equal(b(function(BA,IdX1),integer,[]),Int0),pred,[]),Int1,Int0),integer,[]), | |
210 | conjunct_predicates([TypeOfX1,TypeOfX2,b(equal(IdX2,ValOfX2),pred,[])],Pred), | |
211 | Out = b(comprehension_set([IdX1,IdX2],Pred),set(couple(integer,integer)),[]). | |
212 | smt_term_to_prob_term(id_term(id('bvand'),[A,B]),Env,Out) :- !, | |
213 | smt_term_to_prob_term(A,Env,BA), | |
214 | smt_term_to_prob_term(B,Env,BB), | |
215 | bvwidth(BA,Width), | |
216 | Int0 = b(integer(0),integer,[]), | |
217 | Int1 = b(integer(1),integer,[]), | |
218 | IdX1 = b(identifier('\\tmp1'),integer,[]), | |
219 | IdX2 = b(identifier('\\tmp2'),integer,[]), | |
220 | TypeOfX1 = b(member(IdX1,b(interval(Int0,Width),set(integer),[])),pred,[]), | |
221 | TypeOfX2 = b(member(IdX2,b(interval(Int0,Int1),set(integer),[])),pred,[]), | |
222 | ValOfX2 = b(if_then_else(b(equal(b(function(BA,IdX1),integer,[]),Int0),pred,[]),Int0,b(function(BB,IdX1),integer,[])),integer,[]), | |
223 | conjunct_predicates([TypeOfX1,TypeOfX2,b(equal(IdX2,ValOfX2),pred,[])],Pred), | |
224 | Out = b(comprehension_set([IdX1,IdX2],Pred),set(couple(integer,integer)),[]). | |
225 | smt_term_to_prob_term(id_term(id('bvor'),[A,B]),Env,Out) :- !, | |
226 | smt_term_to_prob_term(A,Env,BA), | |
227 | smt_term_to_prob_term(B,Env,BB), | |
228 | bvwidth(BA,Width), | |
229 | Int0 = b(integer(0),integer,[]), | |
230 | Int1 = b(integer(1),integer,[]), | |
231 | IdX1 = b(identifier('\\tmp1'),integer,[]), | |
232 | IdX2 = b(identifier('\\tmp2'),integer,[]), | |
233 | TypeOfX1 = b(member(IdX1,b(interval(Int0,Width),set(integer),[])),pred,[]), | |
234 | TypeOfX2 = b(member(IdX2,b(interval(Int0,Int1),set(integer),[])),pred,[]), | |
235 | ValOfX2 = b(if_then_else(b(equal(b(function(BA,IdX1),integer,[]),Int1),pred,[]),Int1,b(function(BB,IdX1),integer,[])),integer,[]), | |
236 | conjunct_predicates([TypeOfX1,TypeOfX2,b(equal(IdX2,ValOfX2),pred,[])],Pred), | |
237 | Out = b(comprehension_set([IdX1,IdX2],Pred),set(couple(integer,integer)),[]). | |
238 | smt_term_to_prob_term(id_term(id('bvxor'),[A,B]),Env,Out) :- !, | |
239 | smt_term_to_prob_term(A,Env,BA), | |
240 | smt_term_to_prob_term(B,Env,BB), | |
241 | bvwidth(BA,Width), | |
242 | Int0 = b(integer(0),integer,[]), | |
243 | Int1 = b(integer(1),integer,[]), | |
244 | IdX1 = b(identifier('\\tmp1'),integer,[]), | |
245 | IdX2 = b(identifier('\\tmp2'),integer,[]), | |
246 | TypeOfX1 = b(member(IdX1,b(interval(Int0,Width),set(integer),[])),pred,[]), | |
247 | TypeOfX2 = b(member(IdX2,b(interval(Int0,Int1),set(integer),[])),pred,[]), | |
248 | ValOfX2 = b(if_then_else(b(equal(b(function(BA,IdX1),integer,[]),b(function(BB,IdX1),integer,[])),pred,[]),Int0,Int1),integer,[]), | |
249 | conjunct_predicates([TypeOfX1,TypeOfX2,b(equal(IdX2,ValOfX2),pred,[])],Pred), | |
250 | Out = b(comprehension_set([IdX1,IdX2],Pred),set(couple(integer,integer)),[]). | |
251 | smt_term_to_prob_term(id_term(id('bvult'),[A,B]),Env,Out) :- !, | |
252 | bv_to_nat_and_compare(A,B,less,Env,Out). | |
253 | smt_term_to_prob_term(id_term(id('bvule'),[A,B]),Env,Out) :- !, | |
254 | bv_to_nat_and_compare(A,B,less_equal,Env,Out). | |
255 | smt_term_to_prob_term(id_term(id('bvuge'),[A,B]),Env,Out) :- !, | |
256 | bv_to_nat_and_compare(A,B,greater_equal,Env,Out). | |
257 | smt_term_to_prob_term(id_term(id('bvugt'),[A,B]),Env,Out) :- !, | |
258 | bv_to_nat_and_compare(A,B,greater,Env,Out). | |
259 | smt_term_to_prob_term(id_term(id('bvslt'),[A,B]),Env,Out) :- !, | |
260 | signed_bv_to_nat_and_compare(A,B,less,Env,Out). | |
261 | smt_term_to_prob_term(id_term(id('bvsle'),[A,B]),Env,Out) :- !, | |
262 | signed_bv_to_nat_and_compare(A,B,less_equal,Env,Out). | |
263 | smt_term_to_prob_term(id_term(id('bvsge'),[A,B]),Env,Out) :- !, | |
264 | signed_bv_to_nat_and_compare(A,B,greater_equal,Env,Out). | |
265 | smt_term_to_prob_term(id_term(id('bvsgt'),[A,B]),Env,Out) :- !, | |
266 | signed_bv_to_nat_and_compare(A,B,greater,Env,Out). | |
267 | smt_term_to_prob_term(id_term(id('bvneg'),[A]),Env,Out) :- !, | |
268 | smt_term_to_prob_term(A,Env,BA), | |
269 | bvwidth(BA,Width), | |
270 | WidthP1 = b(add(Width,b(integer(1),integer,[])),integer,[]), | |
271 | bv2nat(BA,BANat), | |
272 | Int2 = b(integer(2),integer,[]), | |
273 | Pow = b(power_of(Int2,WidthP1),integer,[]), | |
274 | Differenz = b(minus(Pow,BANat),integer,[]), | |
275 | nat2bv(Differenz,Width,Out). | |
276 | smt_term_to_prob_term(id_term(id('bvadd'),[A,B]),Env,Out) :- !, | |
277 | smt_term_to_prob_term(A,Env,BA), | |
278 | smt_term_to_prob_term(B,Env,BB), | |
279 | bvwidth(BA,Width), | |
280 | bv2nat(BA,BANat), | |
281 | bv2nat(BB,BBNat), | |
282 | Sum = b(add(BANat,BBNat),integer,[]), | |
283 | nat2bv(Sum,Width,Out). | |
284 | smt_term_to_prob_term(id_term(id('bvsub'),[A,B]),Env,Out) :- !, | |
285 | smt_term_to_prob_term(A,Env,BA), | |
286 | smt_term_to_prob_term(B,Env,BB), | |
287 | bvwidth(BA,Width), | |
288 | bv2nat(BA,BANat), | |
289 | bv2nat(BB,BBNat), | |
290 | Sum = b(minus(BANat,BBNat),integer,[]), | |
291 | nat2bv(Sum,Width,Out). | |
292 | smt_term_to_prob_term(id_term(id('bvmul'),[A,B]),Env,Out) :- !, | |
293 | smt_term_to_prob_term(A,Env,BA), | |
294 | smt_term_to_prob_term(B,Env,BB), | |
295 | bvwidth(BA,Width), | |
296 | bv2nat(BA,BANat), | |
297 | bv2nat(BB,BBNat), | |
298 | Prod = b(multiplication(BANat,BBNat),integer,[]), | |
299 | nat2bv(Prod,Width,Out). | |
300 | smt_term_to_prob_term(id_term(id('bvudiv'),[A,B]),Env,Out) :- !, | |
301 | smt_term_to_prob_term(A,Env,BA), | |
302 | smt_term_to_prob_term(B,Env,BB), | |
303 | bvwidth(BA,Width), | |
304 | bv2nat(BA,BANat), | |
305 | bv2nat(BB,BBNat), | |
306 | Div = b(div(BANat,BBNat),integer,[]), | |
307 | nat2bv(Div,Width,Out). | |
308 | smt_term_to_prob_term(id_term(id('bvurem'),[A,B]),Env,Out) :- !, | |
309 | smt_term_to_prob_term(A,Env,BA), | |
310 | smt_term_to_prob_term(B,Env,BB), | |
311 | bvwidth(BA,Width), | |
312 | bv2nat(BA,BANat), | |
313 | bv2nat(BB,BBNat), | |
314 | Rem = b(modulo(BANat,BBNat),integer,[]), | |
315 | nat2bv(Rem,Width,Out). | |
316 | smt_term_to_prob_term(id_term(id('bvshl'),[A,B]),Env,Out) :- !, | |
317 | smt_term_to_prob_term(A,Env,BA), | |
318 | smt_term_to_prob_term(B,Env,BB), | |
319 | bvwidth(BA,Width), | |
320 | bv2nat(BA,BANat), | |
321 | bv2nat(BB,BBNat), | |
322 | Int2 = b(integer(2),integer,[]), | |
323 | Exp = b(power_of(Int2,BBNat),integer,[]), | |
324 | Res = b(multiplication(BANat,Exp),integer,[]), | |
325 | nat2bv(Res,Width,Out). | |
326 | smt_term_to_prob_term(id_term(id('bvlshr'),[A,B]),Env,Out) :- !, | |
327 | smt_term_to_prob_term(A,Env,BA), | |
328 | smt_term_to_prob_term(B,Env,BB), | |
329 | bvwidth(BA,Width), | |
330 | bv2nat(BA,BANat), | |
331 | bv2nat(BB,BBNat), | |
332 | Int2 = b(integer(2),integer,[]), | |
333 | Exp = b(power_of(Int2,BBNat),integer,[]), | |
334 | Res = b(div(BANat,Exp),integer,[]), | |
335 | nat2bv(Res,Width,Out). | |
336 | % division is a special case, because it has a different | |
337 | % semantic in B and SMT-LIB | |
338 | smt_term_to_prob_term(id_term(id(div),[Dividend|Divisors]),Env,Out) :- !, | |
339 | smt_term_to_prob_term(id_term(id('*'),Divisors),Env,BDivisor), | |
340 | smt_term_to_prob_term(Dividend,Env,BDividend), | |
341 | Zero = b(integer(0),integer,[]), | |
342 | DividendLessZero = b(less(BDividend,Zero),pred,[]), | |
343 | DivisorLessZero = b(less(BDivisor,Zero),pred,[]), | |
344 | DivisorGreaterZero = b(greater(BDivisor,Zero),pred,[]), | |
345 | DivisorMinusOne = b(minus(BDivisor,b(integer(1),integer,[])),integer,[]), | |
346 | DivisorPlusOne = b(add(BDivisor,b(integer(1),integer,[])),integer,[]), | |
347 | MinusDivisorPlusOne = b(unary_minus(DivisorPlusOne),integer,[]), | |
348 | ||
349 | conjunct_predicates([DividendLessZero,DivisorGreaterZero],If1), | |
350 | conjunct_predicates([DividendLessZero,DivisorLessZero],If2), | |
351 | ||
352 | FixInner = b(if_then_else(If2,MinusDivisorPlusOne,Zero),integer,[]), | |
353 | Fix = b(if_then_else(If1,DivisorMinusOne,FixInner),integer,[]), | |
354 | NewBDividend = b(minus(BDividend,Fix),integer,[]), | |
355 | Out = b(div(NewBDividend,BDivisor),integer,[]). | |
356 | % general cases | |
357 | smt_term_to_prob_term(id_term(id(Id),Args),Env,Out) :- | |
358 | smt_id_to_prob_id_preds(Id,BId), !, | |
359 | maplist(smt_term_to_prob_term_maplist(Env),Args,BArgs), | |
360 | maplist(bool_to_pred,BArgs,PredBArgs), | |
361 | interleave(BId,PredBArgs,Out). | |
362 | smt_term_to_prob_term(id_term(id(Id),Args),Env,Out) :- | |
363 | smt_id_to_prob_id(Id,BId,ConnectingPred), !, | |
364 | maplist(smt_term_to_prob_term_maplist(Env),Args,BArgs), | |
365 | call(ConnectingPred,BId,BArgs,Out). | |
366 | smt_term_to_prob_term(id_term(id(Id),Args),Env,Out) :- | |
367 | get_function(Id,Env,Params,_Results,Definition), !, | |
368 | replace_identifiers(Params,Args,Definition,Out,Env). | |
369 | smt_term_to_prob_term(id_term(id(Id),Args),Env,Out) :- | |
370 | get_type(Id,Env,set(couple(_X,Y))), !, | |
371 | smt_term_to_prob_term(id(Id),Env,BId), | |
372 | maplist(smt_term_to_prob_term_maplist(Env),Args,BArgs), | |
373 | create_couple(BArgs,BArg), | |
374 | Out = b(function(BId,BArg),Y,[]). | |
375 | smt_term_to_prob_term(id(true),_,b(boolean_true,boolean,[])) :- !. | |
376 | smt_term_to_prob_term(id(false),_,b(boolean_false,boolean,[])) :- !. | |
377 | smt_term_to_prob_term(id(Id),Env,OutId) :- !, | |
378 | get_type(Id,Env,Type), | |
379 | OutId = b(identifier(Id),Type,[]).%, | |
380 | %(Type = boolean | |
381 | % -> bool_to_pred(OutId,Out) | |
382 | % ; Out = OutId). | |
383 | smt_term_to_prob_term(id(Id,Sort),Env,OutId) :- !, | |
384 | smt_type_to_prob_type(Sort,Env,Type), | |
385 | OutId = b(identifier(Id),Type,[]). | |
386 | smt_term_to_prob_term(svar(Id,Sort),Env,Out) :- !, | |
387 | smt_type_to_prob_type(Sort,Env,Type), | |
388 | Out = b(identifier(Id),Type,[]). | |
389 | smt_term_to_prob_term(integer(I),_,b(integer(I),integer,[])) :- !. | |
390 | smt_term_to_prob_term(let(Bindings,Term),Env,BTerm) :- !, | |
391 | let_equalities_and_bids(Bindings,BIDs,Assignments,Env), | |
392 | create_local_env(Env,BIDs,LocalEnv), | |
393 | smt_term_to_prob_term(Term,LocalEnv,InnerBTerm), | |
394 | get_texpr_type(InnerBTerm,InnerType), | |
395 | (InnerType = pred | |
396 | -> safe_create_texpr(let_predicate(BIDs,Assignments,InnerBTerm),pred,BTerm) | |
397 | ; safe_create_texpr(let_expression(BIDs,Assignments,InnerBTerm),InnerType,BTerm)). | |
398 | smt_term_to_prob_term(forall(IDs,Term),Env,Forall) :- !, | |
399 | maplist(smt_term_to_prob_term_maplist(Env),IDs,Identifiers), | |
400 | create_local_env(Env,Identifiers,LocalEnv), | |
401 | smt_term_to_prob_term(Term,LocalEnv,InnerTerm), | |
402 | convlist(typing_constraint,IDs,InnerConstraints), | |
403 | conjunct_predicates([InnerTerm|InnerConstraints],Inner), | |
404 | bool_to_pred(Inner,InnerAsPred), | |
405 | create_forall(Identifiers,InnerAsPred,Forall). | |
406 | smt_term_to_prob_term(exists(IDs,Term),Env,Forall) :- !, | |
407 | maplist(smt_term_to_prob_term_maplist(Env),IDs,Identifiers), | |
408 | create_local_env(Env,Identifiers,LocalEnv), | |
409 | smt_term_to_prob_term(Term,LocalEnv,InnerTerm), | |
410 | convlist(typing_constraint,IDs,InnerConstraints), | |
411 | conjunct_predicates([InnerTerm|InnerConstraints],Inner), | |
412 | bool_to_pred(Inner,InnerAsPred), | |
413 | create_exists(Identifiers,InnerAsPred,Forall). | |
414 | smt_term_to_prob_term(bitvector(Value,Length),_Env,Out) :- !, | |
415 | integer_to_binary_couples(Value,Length,Couples), | |
416 | Out = b(set_extension(Couples),set(couple(integer,integer)),[]). | |
417 | smt_term_to_prob_term(bitvector(Bits),_Env,Out) :- !, | |
418 | binary_to_binary_couples(Bits,Couples), | |
419 | Out = b(set_extension(Couples),set(couple(integer,integer)),[]). | |
420 | smt_term_to_prob_term(X,_,_) :- !, format('missing in smt_term_to_prob_term: ~w~n',[X]), fail. | |
421 | ||
422 | ||
423 | bool_to_pred(Bool,Pred) :- | |
424 | get_texpr_expr(Bool,convert_bool(Pred)), !. | |
425 | bool_to_pred(Bool,Pred) :- | |
426 | get_texpr_type(Bool,boolean), !, | |
427 | safe_create_texpr(equal(Bool,b(boolean_true,boolean,[])),pred,Pred). | |
428 | bool_to_pred(Bool,Bool) :- | |
429 | get_texpr_type(Bool,pred), !. | |
430 | ||
431 | to_bool_if_necessary(PossiblePred,Bool) :- | |
432 | get_texpr_type(PossiblePred,pred), !, | |
433 | safe_create_texpr(convert_bool(PossiblePred),boolean,Bool). | |
434 | to_bool_if_necessary(NonPred,NonPred). | |
435 | ||
436 | let_equalities_and_bids([bind(ID,Term)],[IDTerm],[AssOut],Env) :- !, | |
437 | smt_term_to_prob_term(Term,Env,Ass), | |
438 | get_texpr_type(Ass,IdentifierType), | |
439 | (IdentifierType == pred | |
440 | -> IDTerm = b(identifier(ID),boolean,[]), | |
441 | safe_create_texpr(convert_bool(Ass),boolean,AssOut) | |
442 | ; IDTerm = b(identifier(ID),IdentifierType,[]), | |
443 | AssOut = Ass). | |
444 | let_equalities_and_bids([bind(ID,Term)|Further],[IDTerm|FurtherIdentifiers],Assignments,Env) :- | |
445 | let_equalities_and_bids([bind(ID,Term)],[IDTerm],FirstAssignment,Env), | |
446 | let_equalities_and_bids(Further,FurtherIdentifiers,FurtherAssignments,Env), | |
447 | append(FirstAssignment,FurtherAssignments,Assignments). | |
448 | ||
449 | replace_identifiers([],[],D,D,_Env). | |
450 | replace_identifiers([b(identifier(I),_,_)|T1],[Term|Terms],In,Out,Env) :- | |
451 | smt_term_to_prob_term(Term,Env,BTerm), | |
452 | replace_id_by_expr(In,I,BTerm,TOut), | |
453 | replace_identifiers(T1,Terms,TOut,Out,Env). | |
454 | ||
455 | % certain sorts enforce an inner constrait to strengthen their type | |
456 | typing_constraint(svar(Name,sort('Array',[Index,Element])),Constraint) :- | |
457 | smt_type_to_prob_type(Index,EIn,BIndex), | |
458 | smt_type_to_prob_type(Element,EIn,BElement), | |
459 | FullType = set(couple(BIndex,BElement)), | |
460 | Identifier = b(identifier(Name),FullType,[]), | |
461 | Constraint = b(member(Identifier,b(total_function(From,To),set(FullType),[])),pred,[]), | |
462 | type_to_expr(BIndex,From), | |
463 | type_to_expr(BElement,To). | |
464 | typing_constraint(svar(Name,sort('BitVec',[Length])),Constraint) :- | |
465 | Zero = b(integer(0),integer,[]), | |
466 | One = b(integer(1),integer,[]), | |
467 | L2 is Length - 1, | |
468 | LengthMinusOne = b(integer(L2),integer,[]), | |
469 | FullType = set(couple(integer,integer)), | |
470 | Identifier = b(identifier(Name),FullType,[]), | |
471 | From = b(interval(Zero,LengthMinusOne),set(integer),[]), | |
472 | To = b(interval(Zero,One),set(integer),[]), | |
473 | Constraint = b(member(Identifier,b(total_function(From,To),set(FullType),[])),pred,[]). | |
474 | ||
475 | is_function_constraint(Id,FullType,Constraint) :- | |
476 | FullType = set(couple(From,To)), | |
477 | Identifier = b(identifier(Id),FullType,[]), | |
478 | type_to_expr(From,FromExpr), | |
479 | type_to_expr(To,ToExpr), | |
480 | Constraint = b(member(Identifier,b(partial_function(FromExpr,ToExpr),set(FullType),[])),pred,[]). | |
481 | ||
482 | integer_to_binary_couples(Value,Length,Couples) :- | |
483 | PLength is Length - 1, | |
484 | integer_to_binary_couples(Value,0,PLength,Couples). | |
485 | integer_to_binary_couples(Value,Current,Current,[b(couple(A,B),couple(integer,integer),[])]) :- !, | |
486 | A = b(integer(Current),integer,[]), | |
487 | BVal is mod(Value,2), | |
488 | B = b(integer(BVal),integer,[]). | |
489 | integer_to_binary_couples(Value,Current,PLength,[b(couple(A,B),couple(integer,integer),[])|Cs]) :- | |
490 | A = b(integer(Current),integer,[]), | |
491 | BVal is mod(Value,2), | |
492 | B = b(integer(BVal),integer,[]), | |
493 | NValue is Value // 2, | |
494 | NCurrent is Current + 1, | |
495 | integer_to_binary_couples(NValue,NCurrent,PLength,Cs). | |
496 | ||
497 | binary_to_binary_couples(Bits,Couples) :- | |
498 | length(Bits,L), FirstL is L - 1, | |
499 | binary_to_binary_couples(FirstL,Bits,Couples). | |
500 | binary_to_binary_couples(-1,[],[]). | |
501 | binary_to_binary_couples(L,[Bit|Bits],[Couple|Couples]) :- | |
502 | A = b(integer(L),integer,[]), | |
503 | B = b(integer(Bit),integer,[]), | |
504 | Couple = b(couple(A,B),couple(integer,integer),[]), | |
505 | L2 is L - 1, | |
506 | binary_to_binary_couples(L2,Bits,Couples). | |
507 | ||
508 | smt_id_to_prob_id('<=',less_equal,chain). | |
509 | smt_id_to_prob_id('>=',greater_equal,chain). | |
510 | smt_id_to_prob_id('<',less,chain). | |
511 | smt_id_to_prob_id('>',greater,chain). | |
512 | smt_id_to_prob_id('distinct',not_equal,chain). | |
513 | smt_id_to_prob_id('*',multiplication,interleave). | |
514 | smt_id_to_prob_id('+',add,interleave). | |
515 | smt_id_to_prob_id('-',minus,interleave). | |
516 | ||
517 | smt_id_to_prob_id_preds('or',disjunct). | |
518 | smt_id_to_prob_id_preds('and',conjunct). | |
519 | smt_id_to_prob_id_preds('=>',implication). | |
520 | ||
521 | bvwidth(BV,Width) :- | |
522 | Width = b(max(b(domain(BV),set(integer),[])),integer,[]). | |
523 | ||
524 | bv2nat(BV,Nat) :- | |
525 | IntOne = b(integer(1),integer,[]), | |
526 | IntTwo = b(integer(2),integer,[]), | |
527 | IdX1 = b(identifier('\\tmp1'),integer,[]), | |
528 | IdX2 = b(identifier('\\tmp2'),integer,[]), | |
529 | PowerOf = b(power_of(IntTwo,b(minus(IdX1,IntOne),integer,[])),integer,[]), | |
530 | Nat = b(general_sum([IdX1,IdX2],b(member(b(couple(IdX1,IdX2),couple(integer,integer),[]),BV),pred,[]),b(multiplication(IdX2,PowerOf),integer,[])),integer,[]). | |
531 | signed_bv2nat(BV,Nat) :- | |
532 | IntOne = b(integer(1),integer,[]), | |
533 | IntTwo = b(integer(2),integer,[]), | |
534 | IntMinusOne = b(integer(-1),integer,[]), | |
535 | % todo: make sure identifiers do not collide | |
536 | IdX1 = b(identifier('\\tmp1'),integer,[]), | |
537 | IdX2 = b(identifier('\\tmp2'),integer,[]), | |
538 | NotZeroIndex = b(not_equal(IdX1,b(integer(0),integer,[])),pred,[]), | |
539 | MemberConstraint = b(member(b(couple(IdX1,IdX2),couple(integer,integer),[]),BV),pred,[]), | |
540 | conjunct_predicates([NotZeroIndex,MemberConstraint],Const), | |
541 | PowerOf = b(power_of(IntTwo,b(minus(IdX1,IntOne),integer,[])),integer,[]), | |
542 | Sum = b(general_sum([IdX1,IdX2],Const,b(multiplication(IdX2,PowerOf),integer,[])),integer,[]), | |
543 | ZeroIndex = b(function(BV,b(integer(0),integer,[])),integer,[]), | |
544 | Sign = b(power_of(IntMinusOne,ZeroIndex),integer,[]), | |
545 | Nat = b(multiplication(Sign,Sum),integer,[]). | |
546 | ||
547 | nat2bv(Nat,Width,BV) :- | |
548 | IntOne = b(integer(1),integer,[]), | |
549 | IntTwo = b(integer(2),integer,[]), | |
550 | % todo: make sure identifiers do not collide | |
551 | IdX1 = b(identifier('\\tmp1'),integer,[]), | |
552 | IdX2 = b(identifier('\\tmp2'),integer,[]), | |
553 | TypeId1 = b(member(IdX1,b(interval(b(integer(1),integer,[]),Width),set(integer),[])),pred,[]), | |
554 | TypeId2 = b(member(IdX2,b(interval(b(integer(0),integer,[]),b(integer(1),integer,[])),set(integer),[])),pred,[]), | |
555 | PowerOf = b(power_of(IntTwo,b(minus(IdX1,IntOne),integer,[])),integer,[]), | |
556 | ValueOfId2 = b(equal(IdX2,b(modulo(b(div(Nat,PowerOf),integer,[]),IntTwo),integer,[])),pred,[]), | |
557 | conjunct_predicates([TypeId1,TypeId2,ValueOfId2],InnerPred), | |
558 | BV = b(comprehension_set([IdX1,IdX2],InnerPred),set(couple(integer,integer)),[]). | |
559 | ||
560 | type_to_expr(set(A),b(comprehension_set([Id],b(member(Id,AE),pred,[])),set(AET),[])) :- !, | |
561 | Id = b(identifier('\\tmp1'),AET,[]), | |
562 | type_to_expr(A,AE), | |
563 | get_texpr_type(AE,AET). | |
564 | type_to_expr(couple(A,B),b(cartesian_product(AE,BE),set(couple(AET,BET)),[])) :- !, | |
565 | type_to_expr(A,AE), type_to_expr(B,BE), | |
566 | get_texpr_type(AE,AET), get_texpr_type(BE,BET). | |
567 | type_to_expr(integer,b(integer_set('INTEGER'),set(integer),[])) :- !. | |
568 | type_to_expr(boolean,b(bool_set,set(boolean),[])) :- !. | |
569 | type_to_expr(global(E),b(identifier(E),set(global(E)),[])) :- !. | |
570 | type_to_expr(T,_) :- !, | |
571 | format('missing in type_to_expr: ~w~n',[T]), fail. | |
572 | ||
573 | signed_bv_to_nat_and_compare(A,B,Op,Env,Out) :- | |
574 | smt_term_to_prob_term(A,Env,BA), | |
575 | smt_term_to_prob_term(B,Env,BB), | |
576 | signed_bv2nat(BA,BANat), | |
577 | signed_bv2nat(BB,BBNat), | |
578 | Operation =.. [Op,BANat,BBNat], | |
579 | Out = b(Operation,pred,[]). | |
580 | ||
581 | bv_to_nat_and_compare(A,B,Op,Env,Out) :- | |
582 | smt_term_to_prob_term(A,Env,BA), | |
583 | smt_term_to_prob_term(B,Env,BB), | |
584 | bv2nat(BA,BANat), | |
585 | bv2nat(BB,BBNat), | |
586 | Operation =.. [Op,BANat,BBNat], | |
587 | Out = b(Operation,pred,[]). |