| 1 | % (c) 2014-2026 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 | create_implication/3, | |
| 26 | create_negation/2, | |
| 27 | conjunct_predicates/2, | |
| 28 | replace_id_by_expr/4]). | |
| 29 | :- use_module(probsrc(kernel_reals),[is_real/2]). | |
| 30 | ||
| 31 | :- use_module(smtlib_solver(smtlib2_environment)). | |
| 32 | ||
| 33 | chain(Op,[A,B],BPred) :- !, | |
| 34 | BPred = b(Pred,pred,[]), | |
| 35 | (lift_types(A,B,AR,BR) | |
| 36 | -> construct_operator(Op,AR,BR,Pred), | |
| 37 | add_message(smtlib2_translation,'Lifting types: ',BPred) | |
| 38 | ; construct_operator(Op,A,B,Pred) | |
| 39 | ). | |
| 40 | chain(Op,[First,Second|Further],TermOut) :- | |
| 41 | chain(Op,[First,Second],Pred), | |
| 42 | chain(Op,[Second|Further],FurtherPred), | |
| 43 | conjunct_predicates([Pred,FurtherPred],TermOut). | |
| 44 | ||
| 45 | % all pairs must be related by Op, e.g., (distinct a b c) requires a/=b, a/=c and b/=c | |
| 46 | pairwise(Op,[A,B],BPred) :- !, chain(Op,[A,B],BPred). | |
| 47 | pairwise(Op,[First|Further],TermOut) :- | |
| 48 | maplist(pair_with(Op,First),Further,Preds), | |
| 49 | pairwise(Op,Further,FurtherPred), | |
| 50 | conjunct_predicates([FurtherPred|Preds],TermOut). | |
| 51 | pair_with(Op,A,B,Pred) :- chain(Op,[A,B],Pred). | |
| 52 | ||
| 53 | % lift types if necessary; SMTLib allows comparing integers and reals | |
| 54 | lift_types(A,B,AR,BR) :- get_texpr_type(A,AT), get_texpr_type(B,BT), | |
| 55 | adapt_types(AT,BT,A,B,A2,B2),!, | |
| 56 | AR=A2, BR=B2. | |
| 57 | adapt_types(real,integer,A,B,A,BR) :- safe_create_texpr(convert_real(B),real,BR). | |
| 58 | adapt_types(integer,real,A,B,AR,B) :- safe_create_texpr(convert_real(A),real,AR). | |
| 59 | ||
| 60 | construct_operator(Op,A,B,Pred) :- | |
| 61 | (get_texpr_type(A,real) -> true ; get_texpr_type(B,real)), | |
| 62 | construct_operator_real(Op,A,B,P),!, Pred=P. | |
| 63 | construct_operator(xor_b_pred,A,B,Pred) :- !, | |
| 64 | create_negation(B,NB), | |
| 65 | Pred = equivalence(A,NB). | |
| 66 | construct_operator(Op,A,B,Pred) :- Pred =.. [Op,A,B]. | |
| 67 | ||
| 68 | construct_operator_real(add,A,B,Pred) :- !, Pred =.. [add_real,A,B]. | |
| 69 | construct_operator_real(div,A,B,Pred) :- !, Pred =.. [div_real,A,B]. | |
| 70 | construct_operator_real(minus,A,B,Pred) :- !, Pred =.. [minus_real,A,B]. | |
| 71 | construct_operator_real(multiplication,A,B,Pred) :- !, Pred =.. [multiplication_real,A,B]. | |
| 72 | construct_operator_real(less_equal,A,B,Pred) :- !, Pred =.. [less_equal_real,A,B]. | |
| 73 | construct_operator_real(less,A,B,Pred) :- !, Pred =.. [less_real,A,B]. | |
| 74 | construct_operator_real(greater_equal,A,B,Pred) :- !, Pred =.. [less_equal_real,B,A]. | |
| 75 | construct_operator_real(greater,A,B,Pred) :- !, Pred =.. [less_real,B,A]. | |
| 76 | ||
| 77 | construct_unary_minus(Arg,Pred) :- get_texpr_type(Arg,real),!, Pred = b(unary_minus_real(Arg),real,[]). | |
| 78 | construct_unary_minus(Arg,b(unary_minus(Arg),integer,[])). | |
| 79 | ||
| 80 | lift_type_to(real,A,AR) :- get_texpr_type(A,integer), !, safe_create_texpr(convert_real(A),real,AR). | |
| 81 | lift_type_to(_,A,A). | |
| 82 | ||
| 83 | l_lift_types([],_,[]). | |
| 84 | l_lift_types([H|T],ExpectedType,[LH|LT]) :- | |
| 85 | lift_type_to(ExpectedType,H,LH), | |
| 86 | l_lift_types(T,ExpectedType,LT). | |
| 87 | ||
| 88 | % right-associative, e.g., (=> a b c) = a => (b => c) | |
| 89 | interleave(_Op,[A],TermOut) :- !, TermOut=A. | |
| 90 | interleave(Op,[First|Further],TermOut) :- | |
| 91 | interleave(Op,Further,FurtherPred), | |
| 92 | combine_binary(Op,First,FurtherPred,TermOut). | |
| 93 | ||
| 94 | % left-associative, e.g., (- a b c) = (a - b) - c | |
| 95 | interleave_left(_Op,[A],TermOut) :- !, TermOut=A. | |
| 96 | interleave_left(Op,[First,Second|Further],TermOut) :- | |
| 97 | combine_binary(Op,First,Second,Acc), | |
| 98 | interleave_left(Op,[Acc|Further],TermOut). | |
| 99 | ||
| 100 | combine_binary(Op,A,B,TermOut) :- | |
| 101 | (lift_types(A,B,AR,BR) | |
| 102 | -> construct_operator(Op,AR,BR,Pred), | |
| 103 | get_texpr_type(AR,Type) | |
| 104 | ; construct_operator(Op,A,B,Pred), | |
| 105 | get_texpr_type(B,Type) | |
| 106 | ), | |
| 107 | safe_create_texpr(Pred,Type,TermOut). | |
| 108 | ||
| 109 | :- use_module(probsrc(preferences), [get_preference/2]). | |
| 110 | :- use_module(probsrc(error_manager),[add_error/3, add_warning/3, add_message/3]). | |
| 111 | ||
| 112 | smt_type_to_prob_type(sort('Int'),_,Type) :- !, Type=integer. | |
| 113 | smt_type_to_prob_type(sort('Bool'),_,Type) :- !, Type=boolean. | |
| 114 | smt_type_to_prob_type(sort('Real'),_,Type) :- !, Type=real. | |
| 115 | smt_type_to_prob_type(sort('Array',[From,sort('Bool')]),E,Out) :- | |
| 116 | get_preference(smtlib2b_arrays_as_sets,true), | |
| 117 | !, % we could translate arrays to Bool as sets | |
| 118 | smt_type_to_prob_type(From,E,FromType), | |
| 119 | Out = set(FromType). | |
| 120 | smt_type_to_prob_type(sort('Array',[From,To]),E,Out) :- !, | |
| 121 | %format('Sort Array ~w to ~w~n',[From,To]),nl, | |
| 122 | smt_type_to_prob_type(From,E,FromType), | |
| 123 | smt_type_to_prob_type(To,E,ToType), | |
| 124 | Out = set(couple(FromType,ToType)). | |
| 125 | smt_type_to_prob_type(sort('BitVec',[_Length]),_E,Out) :- !, | |
| 126 | Out = set(couple(integer,integer)). | |
| 127 | smt_type_to_prob_type(sort('Set',[Sub]),E,Out) :- !, | |
| 128 | smt_type_to_prob_type(Sub,E,SubType), | |
| 129 | Out = set(SubType). | |
| 130 | smt_type_to_prob_type(sort(X),E,global(X)) :- | |
| 131 | is_custom_type(E,X), !. | |
| 132 | smt_type_to_prob_type(sort('Pair',[From,To]),E,Out) :- !, % in SMTLib 2.7 Pair can be defined as: | |
| 133 | % (declare-datatype Pair (par (T1 T2) ((pair (fst T1) (snd T2))))) ; TODO: infer from declare-datatype | |
| 134 | smt_type_to_prob_type(From,E,FromType), | |
| 135 | smt_type_to_prob_type(To,E,ToType), | |
| 136 | Out = couple(FromType,ToType). | |
| 137 | smt_type_to_prob_type(sort(smt_fun([From,To])),E,Out) :- !, | |
| 138 | smt_type_to_prob_type(From,E,FromType), | |
| 139 | smt_type_to_prob_type(To,E,ToType), | |
| 140 | add_warning(smtlib2_translation,'Translating SMTLib function to relation: ',[From,To]), | |
| 141 | Out = set(couple(FromType,ToType)). | |
| 142 | smt_type_to_prob_type(X,_,_) :- !, | |
| 143 | add_error(smtlib2_translation,'Unsupported sort in smt_type_to_prob_type:',X), fail. | |
| 144 | ||
| 145 | % special versions for maplist that keeps first argument indexing | |
| 146 | smt_term_to_prob_term_maplist(E,I,O) :- | |
| 147 | ? | smt_term_to_prob_term(I,E,O). |
| 148 | smt_type_to_prob_type_maplist(E,I,O) :- | |
| 149 | smt_type_to_prob_type(I,E,O). | |
| 150 | ||
| 151 | smt_term_to_prob_term(attributed_term(Term,_Attr),Env,Out) :- !, | |
| 152 | smt_term_to_prob_term(Term,Env,Out). | |
| 153 | smt_term_to_prob_term(id_term(id('not'),[Arg]),Env,Out) :- !, | |
| 154 | ? | smt_term_to_prob_term(Arg,Env,BArg), |
| 155 | get_texpr_type(BArg,Type), | |
| 156 | (Type = pred | |
| 157 | -> create_negation(BArg,Out) %Out = b(negation(BArg),pred,[]) | |
| 158 | ; Out = b(equal(BArg,b(boolean_false,boolean,[])),pred,[])). | |
| 159 | smt_term_to_prob_term(id_term(id('-'),[SingleArg]),Env,Out) :- !, | |
| 160 | % special case for unary minus: can not be interleaved | |
| 161 | smt_term_to_prob_term(SingleArg,Env,BArg), | |
| 162 | construct_unary_minus(BArg,Out). | |
| 163 | smt_term_to_prob_term(id_term(id('='),Args),Env,Out) :- !, | |
| 164 | ? | maplist(smt_term_to_prob_term_maplist(Env),Args,BArgs), |
| 165 | maplist(get_texpr_type,BArgs,Types), | |
| 166 | (member(pred,Types) | |
| 167 | -> maplist(bool_to_pred,BArgs,BArgsPreds), | |
| 168 | chain(equivalence,BArgsPreds,Out) | |
| 169 | ; chain(equal,BArgs,Out)). | |
| 170 | smt_term_to_prob_term(id_term(id('ite'),[Test,If,Then]),Env,Out) :- !, | |
| 171 | smt_term_to_prob_term(Test,Env,BTestT), | |
| 172 | smt_term_to_prob_term(If,Env,BIfT), | |
| 173 | smt_term_to_prob_term(Then,Env,BThenT), | |
| 174 | bool_to_pred(BTestT,BTest), | |
| 175 | to_bool_if_necessary(BIfT,BIf), | |
| 176 | to_bool_if_necessary(BThenT,BThen), | |
| 177 | get_texpr_type(BIf,Type), | |
| 178 | Out = b(if_then_else(BTest,BIf,BThen),Type,[]). | |
| 179 | % set logic | |
| 180 | smt_term_to_prob_term(id_term(id(member),[Element,Set]),Env,Out) :- !, | |
| 181 | smt_term_to_prob_term(Set,Env,BSet), | |
| 182 | smt_term_to_prob_term(Element,Env,BElement), | |
| 183 | Out = b(member(BElement,BSet),pred,[]). | |
| 184 | smt_term_to_prob_term(id_term(id(card),[Set]),Env,Out) :- !, | |
| 185 | smt_term_to_prob_term(Set,Env,BSet), | |
| 186 | Out = b(card(BSet),integer,[]). | |
| 187 | smt_term_to_prob_term(id_term(id(singleton),[Element]),Env,Out) :- !, | |
| 188 | smt_term_to_prob_term(Element,Env,BElement), | |
| 189 | get_texpr_type(BElement,ElementType), | |
| 190 | Out = b(set_extension([BElement]),set(ElementType),[]). | |
| 191 | smt_term_to_prob_term(id_term(id(union),[SetA,SetB]),Env,Out) :- !, | |
| 192 | smt_term_to_prob_term(SetA,Env,BSetA), | |
| 193 | smt_term_to_prob_term(SetB,Env,BSetB), | |
| 194 | get_texpr_type(BSetB,Type), | |
| 195 | Out = b(union(BSetA,BSetB),Type,[]). | |
| 196 | smt_term_to_prob_term(id_term(id(intersection),[SetA,SetB]),Env,Out) :- !, | |
| 197 | smt_term_to_prob_term(SetA,Env,BSetA), | |
| 198 | smt_term_to_prob_term(SetB,Env,BSetB), | |
| 199 | get_texpr_type(BSetB,Type), | |
| 200 | Out = b(intersection(BSetA,BSetB),Type,[]). | |
| 201 | smt_term_to_prob_term(id_term(id(subset),[SetA,SetB]),Env,Out) :- !, | |
| 202 | smt_term_to_prob_term(SetA,Env,BSetA), | |
| 203 | smt_term_to_prob_term(SetB,Env,BSetB), | |
| 204 | Out = b(subset(BSetA,BSetB),pred,[]). | |
| 205 | % array logics | |
| 206 | smt_term_to_prob_term(id_term(id('store'),[Array,Index,Element]),Env,Out) :- !, | |
| 207 | smt_term_to_prob_term(Array,Env,BArray), | |
| 208 | get_texpr_type(BArray,ArrayType), | |
| 209 | ArrayType = set(CoupleType), | |
| 210 | smt_term_to_prob_term(Index,Env,BIndex), | |
| 211 | smt_term_to_prob_term(Element,Env,BElement), | |
| 212 | % TO DO: generate union or set_difference depending on Element=true or false when smtlib2b_arrays_as_sets | |
| 213 | % store(X,Index,El) = IF El=TRUE THEN X \/ {Index} ELSE X \ {Index} END | |
| 214 | SetEx = b(set_extension([b(couple(BIndex,BElement),CoupleType,[])]),ArrayType,[]), | |
| 215 | Out = b(overwrite(BArray,SetEx),ArrayType,[]). | |
| 216 | smt_term_to_prob_term(id_term(id('select'),[Array,Index]),Env,Out) :- !, | |
| 217 | smt_term_to_prob_term(Array,Env,BArray), | |
| 218 | smt_term_to_prob_term(Index,Env,BIndex), | |
| 219 | get_texpr_type(BArray,ArrayType), | |
| 220 | %format('select of array ~w (type: ~w) at index ~w~n',[Array,ArrayType,Index]), | |
| 221 | (ArrayType = set(couple(_From,To)) % Array was translated as total function From --> To | |
| 222 | -> Out = b(function(BArray,BIndex),To,[]) | |
| 223 | ; ArrayType = set(_From), % Array was translated as set (smtlib2b_arrays_as_sets=true) | |
| 224 | MEM = b(member(BIndex,BArray),pred,[]), | |
| 225 | Out = b(convert_bool(MEM),boolean,[]) | |
| 226 | ). | |
| 227 | % bitvector logics | |
| 228 | % the bit vectors are built using union, as ProB may evaluate both branches of IF-THEN-ELSE | |
| 229 | % and a function application outside of the domain then fails | |
| 230 | smt_term_to_prob_term(id_term(id('concat'),[A,B]),Env,Out) :- !, | |
| 231 | % B is the low part, A is shifted by the width of B | |
| 232 | ? | smt_term_to_prob_term(A,Env,BA), |
| 233 | ? | smt_term_to_prob_term(B,Env,BB), |
| 234 | bvwidth(BA,WidthA), | |
| 235 | bvwidth(BB,WidthB), | |
| 236 | Int0 = b(integer(0),integer,[]), | |
| 237 | Int1 = b(integer(1),integer,[]), | |
| 238 | WidthBP1 = b(add(WidthB,Int1),integer,[]), | |
| 239 | IdX1 = b(identifier('\\tmp1'),integer,[]), | |
| 240 | IdX2 = b(identifier('\\tmp2'),integer,[]), | |
| 241 | FullWidth = b(add(b(add(WidthA,WidthB),integer,[]),Int1),integer,[]), | |
| 242 | TypeOfX1 = b(member(IdX1,b(interval(WidthBP1,FullWidth),set(integer),[])),pred,[]), | |
| 243 | TypeOfX2 = b(member(IdX2,b(interval(Int0,Int1),set(integer),[])),pred,[]), | |
| 244 | ShiftedCouple = b(couple(b(minus(IdX1,WidthBP1),integer,[]),IdX2),couple(integer,integer),[]), | |
| 245 | conjunct_predicates([TypeOfX1,TypeOfX2,b(member(ShiftedCouple,BA),pred,[])],Pred), | |
| 246 | High = b(comprehension_set([IdX1,IdX2],Pred),set(couple(integer,integer)),[]), | |
| 247 | Out = b(union(BB,High),set(couple(integer,integer)),[]). | |
| 248 | smt_term_to_prob_term(id_term(id(zero_extend(NewLength)),[A]),Env,Out) :- !, | |
| 249 | ? | smt_term_to_prob_term(A,Env,BA), |
| 250 | bvwidth(BA,WidthA), | |
| 251 | bv_extension(BA,WidthA,NewLength,b(integer(0),integer,[]),Out). | |
| 252 | smt_term_to_prob_term(id_term(id(sign_extend(NewLength)),[A]),Env,Out) :- !, | |
| 253 | ? | smt_term_to_prob_term(A,Env,BA), |
| 254 | bvwidth(BA,WidthA), | |
| 255 | bv_extension(BA,WidthA,NewLength,b(function(BA,WidthA),integer,[]),Out). | |
| 256 | smt_term_to_prob_term(id_term(id(extract(I,J)),[S]),Env,Out) :- !, | |
| 257 | BJ = b(integer(J),integer,[]), | |
| 258 | ? | smt_term_to_prob_term(S,Env,BS), |
| 259 | Int0 = b(integer(0),integer,[]), | |
| 260 | Int1 = b(integer(1),integer,[]), | |
| 261 | MaxIndex is I-J, | |
| 262 | DomX1 = b(integer(MaxIndex),integer,[]), | |
| 263 | IdX1 = b(identifier('\\tmp1'),integer,[]), | |
| 264 | IdX2 = b(identifier('\\tmp2'),integer,[]), | |
| 265 | TypeOfX1 = b(member(IdX1,b(interval(Int0,DomX1),set(integer),[])),pred,[]), | |
| 266 | TypeOfX2 = b(member(IdX2,b(interval(Int0,Int1),set(integer),[])),pred,[]), | |
| 267 | ValOfX2 = b(function(BS,b(add(IdX1,BJ),integer,[])),integer,[]), | |
| 268 | conjunct_predicates([TypeOfX1,TypeOfX2,b(equal(IdX2,ValOfX2),pred,[])],Pred), | |
| 269 | Out = b(comprehension_set([IdX1,IdX2],Pred),set(couple(integer,integer)),[]). | |
| 270 | smt_term_to_prob_term(id_term(id('bvnot'),[A]),Env,Out) :- !, | |
| 271 | ? | smt_term_to_prob_term(A,Env,BA), |
| 272 | bvwidth(BA,Width), | |
| 273 | Int0 = b(integer(0),integer,[]), | |
| 274 | Int1 = b(integer(1),integer,[]), | |
| 275 | IdX1 = b(identifier('\\tmp1'),integer,[]), | |
| 276 | IdX2 = b(identifier('\\tmp2'),integer,[]), | |
| 277 | TypeOfX1 = b(member(IdX1,b(interval(Int0,Width),set(integer),[])),pred,[]), | |
| 278 | TypeOfX2 = b(member(IdX2,b(interval(Int0,Int1),set(integer),[])),pred,[]), | |
| 279 | ValOfX2 = b(if_then_else(b(equal(b(function(BA,IdX1),integer,[]),Int0),pred,[]),Int1,Int0),integer,[]), | |
| 280 | conjunct_predicates([TypeOfX1,TypeOfX2,b(equal(IdX2,ValOfX2),pred,[])],Pred), | |
| 281 | Out = b(comprehension_set([IdX1,IdX2],Pred),set(couple(integer,integer)),[]). | |
| 282 | smt_term_to_prob_term(id_term(id('bvand'),[A,B]),Env,Out) :- !, | |
| 283 | ? | smt_term_to_prob_term(A,Env,BA), |
| 284 | ? | smt_term_to_prob_term(B,Env,BB), |
| 285 | bvwidth(BA,Width), | |
| 286 | Int0 = b(integer(0),integer,[]), | |
| 287 | Int1 = b(integer(1),integer,[]), | |
| 288 | IdX1 = b(identifier('\\tmp1'),integer,[]), | |
| 289 | IdX2 = b(identifier('\\tmp2'),integer,[]), | |
| 290 | TypeOfX1 = b(member(IdX1,b(interval(Int0,Width),set(integer),[])),pred,[]), | |
| 291 | TypeOfX2 = b(member(IdX2,b(interval(Int0,Int1),set(integer),[])),pred,[]), | |
| 292 | ValOfX2 = b(if_then_else(b(equal(b(function(BA,IdX1),integer,[]),Int0),pred,[]),Int0,b(function(BB,IdX1),integer,[])),integer,[]), | |
| 293 | conjunct_predicates([TypeOfX1,TypeOfX2,b(equal(IdX2,ValOfX2),pred,[])],Pred), | |
| 294 | Out = b(comprehension_set([IdX1,IdX2],Pred),set(couple(integer,integer)),[]). | |
| 295 | smt_term_to_prob_term(id_term(id('bvor'),[A,B]),Env,Out) :- !, | |
| 296 | ? | smt_term_to_prob_term(A,Env,BA), |
| 297 | ? | smt_term_to_prob_term(B,Env,BB), |
| 298 | bvwidth(BA,Width), | |
| 299 | Int0 = b(integer(0),integer,[]), | |
| 300 | Int1 = b(integer(1),integer,[]), | |
| 301 | IdX1 = b(identifier('\\tmp1'),integer,[]), | |
| 302 | IdX2 = b(identifier('\\tmp2'),integer,[]), | |
| 303 | TypeOfX1 = b(member(IdX1,b(interval(Int0,Width),set(integer),[])),pred,[]), | |
| 304 | TypeOfX2 = b(member(IdX2,b(interval(Int0,Int1),set(integer),[])),pred,[]), | |
| 305 | ValOfX2 = b(if_then_else(b(equal(b(function(BA,IdX1),integer,[]),Int1),pred,[]),Int1,b(function(BB,IdX1),integer,[])),integer,[]), | |
| 306 | conjunct_predicates([TypeOfX1,TypeOfX2,b(equal(IdX2,ValOfX2),pred,[])],Pred), | |
| 307 | Out = b(comprehension_set([IdX1,IdX2],Pred),set(couple(integer,integer)),[]). | |
| 308 | smt_term_to_prob_term(id_term(id('bvxor'),[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 | Int0 = b(integer(0),integer,[]), | |
| 313 | Int1 = b(integer(1),integer,[]), | |
| 314 | IdX1 = b(identifier('\\tmp1'),integer,[]), | |
| 315 | IdX2 = b(identifier('\\tmp2'),integer,[]), | |
| 316 | TypeOfX1 = b(member(IdX1,b(interval(Int0,Width),set(integer),[])),pred,[]), | |
| 317 | TypeOfX2 = b(member(IdX2,b(interval(Int0,Int1),set(integer),[])),pred,[]), | |
| 318 | ValOfX2 = b(if_then_else(b(equal(b(function(BA,IdX1),integer,[]),b(function(BB,IdX1),integer,[])),pred,[]),Int0,Int1),integer,[]), | |
| 319 | conjunct_predicates([TypeOfX1,TypeOfX2,b(equal(IdX2,ValOfX2),pred,[])],Pred), | |
| 320 | Out = b(comprehension_set([IdX1,IdX2],Pred),set(couple(integer,integer)),[]). | |
| 321 | smt_term_to_prob_term(id_term(id('bvult'),[A,B]),Env,Out) :- !, | |
| 322 | ? | bv_to_nat_and_compare(A,B,less,Env,Out). |
| 323 | smt_term_to_prob_term(id_term(id('bvule'),[A,B]),Env,Out) :- !, | |
| 324 | ? | bv_to_nat_and_compare(A,B,less_equal,Env,Out). |
| 325 | smt_term_to_prob_term(id_term(id('bvuge'),[A,B]),Env,Out) :- !, | |
| 326 | ? | bv_to_nat_and_compare(A,B,greater_equal,Env,Out). |
| 327 | smt_term_to_prob_term(id_term(id('bvugt'),[A,B]),Env,Out) :- !, | |
| 328 | ? | bv_to_nat_and_compare(A,B,greater,Env,Out). |
| 329 | smt_term_to_prob_term(id_term(id('bvslt'),[A,B]),Env,Out) :- !, | |
| 330 | ? | signed_bv_to_nat_and_compare(A,B,less,Env,Out). |
| 331 | smt_term_to_prob_term(id_term(id('bvsle'),[A,B]),Env,Out) :- !, | |
| 332 | ? | signed_bv_to_nat_and_compare(A,B,less_equal,Env,Out). |
| 333 | smt_term_to_prob_term(id_term(id('bvsge'),[A,B]),Env,Out) :- !, | |
| 334 | ? | signed_bv_to_nat_and_compare(A,B,greater_equal,Env,Out). |
| 335 | smt_term_to_prob_term(id_term(id('bvsgt'),[A,B]),Env,Out) :- !, | |
| 336 | ? | signed_bv_to_nat_and_compare(A,B,greater,Env,Out). |
| 337 | smt_term_to_prob_term(id_term(id('bvneg'),[A]),Env,Out) :- !, | |
| 338 | ? | smt_term_to_prob_term(A,Env,BA), |
| 339 | bvwidth(BA,Width), | |
| 340 | bv2nat(BA,BANat), | |
| 341 | bvmodulus(Width,Pow), | |
| 342 | Differenz = b(minus(Pow,BANat),integer,[]), | |
| 343 | nat2bv(Differenz,Width,Out). | |
| 344 | smt_term_to_prob_term(id_term(id('bvadd'),[A,B]),Env,Out) :- !, | |
| 345 | ? | smt_term_to_prob_term(A,Env,BA), |
| 346 | ? | smt_term_to_prob_term(B,Env,BB), |
| 347 | bvwidth(BA,Width), | |
| 348 | bv2nat(BA,BANat), | |
| 349 | bv2nat(BB,BBNat), | |
| 350 | Sum = b(add(BANat,BBNat),integer,[]), | |
| 351 | nat2bv(Sum,Width,Out). | |
| 352 | smt_term_to_prob_term(id_term(id('bvsub'),[A,B]),Env,Out) :- !, | |
| 353 | ? | smt_term_to_prob_term(A,Env,BA), |
| 354 | ? | smt_term_to_prob_term(B,Env,BB), |
| 355 | bvwidth(BA,Width), | |
| 356 | bv2nat(BA,BANat), | |
| 357 | bv2nat(BB,BBNat), | |
| 358 | bvmodulus(Width,Pow), | |
| 359 | Sum = b(add(b(minus(BANat,BBNat),integer,[]),Pow),integer,[]), | |
| 360 | nat2bv(Sum,Width,Out). | |
| 361 | smt_term_to_prob_term(id_term(id('bvmul'),[A,B]),Env,Out) :- !, | |
| 362 | ? | smt_term_to_prob_term(A,Env,BA), |
| 363 | ? | smt_term_to_prob_term(B,Env,BB), |
| 364 | bvwidth(BA,Width), | |
| 365 | bv2nat(BA,BANat), | |
| 366 | bv2nat(BB,BBNat), | |
| 367 | Prod = b(multiplication(BANat,BBNat),integer,[]), | |
| 368 | nat2bv(Prod,Width,Out). | |
| 369 | smt_term_to_prob_term(id_term(id('bvudiv'),[A,B]),Env,Out) :- !, | |
| 370 | ? | smt_term_to_prob_term(A,Env,BA), |
| 371 | ? | smt_term_to_prob_term(B,Env,BB), |
| 372 | bvwidth(BA,Width), | |
| 373 | bv2nat(BA,BANat), | |
| 374 | bv2nat(BB,BBNat), | |
| 375 | % (bvudiv a 0) is the vector of all ones | |
| 376 | bvmodulus(Width,Pow), | |
| 377 | AllOnes = b(minus(Pow,b(integer(1),integer,[])),integer,[]), | |
| 378 | IsZero = b(equal(BBNat,b(integer(0),integer,[])),pred,[]), | |
| 379 | Div = b(if_then_else(IsZero,AllOnes,b(div(BANat,BBNat),integer,[])),integer,[]), | |
| 380 | nat2bv(Div,Width,Out). | |
| 381 | smt_term_to_prob_term(id_term(id('bvurem'),[A,B]),Env,Out) :- !, | |
| 382 | ? | smt_term_to_prob_term(A,Env,BA), |
| 383 | ? | smt_term_to_prob_term(B,Env,BB), |
| 384 | bvwidth(BA,Width), | |
| 385 | bv2nat(BA,BANat), | |
| 386 | bv2nat(BB,BBNat), | |
| 387 | % (bvurem a 0) is a | |
| 388 | IsZero = b(equal(BBNat,b(integer(0),integer,[])),pred,[]), | |
| 389 | Rem = b(if_then_else(IsZero,BANat,b(modulo(BANat,BBNat),integer,[])),integer,[]), | |
| 390 | nat2bv(Rem,Width,Out). | |
| 391 | smt_term_to_prob_term(id_term(id('bvshl'),[A,B]),Env,Out) :- !, | |
| 392 | ? | smt_term_to_prob_term(A,Env,BA), |
| 393 | ? | smt_term_to_prob_term(B,Env,BB), |
| 394 | bvwidth(BA,Width), | |
| 395 | bv2nat(BA,BANat), | |
| 396 | bv2nat(BB,BBNat), | |
| 397 | Int2 = b(integer(2),integer,[]), | |
| 398 | Exp = b(power_of(Int2,BBNat),integer,[]), | |
| 399 | TooLarge = b(greater(BBNat,Width),pred,[]), | |
| 400 | Res = b(if_then_else(TooLarge,b(integer(0),integer,[]),b(multiplication(BANat,Exp),integer,[])),integer,[]), | |
| 401 | nat2bv(Res,Width,Out). | |
| 402 | smt_term_to_prob_term(id_term(id('bvlshr'),[A,B]),Env,Out) :- !, | |
| 403 | ? | smt_term_to_prob_term(A,Env,BA), |
| 404 | ? | smt_term_to_prob_term(B,Env,BB), |
| 405 | bvwidth(BA,Width), | |
| 406 | bv2nat(BA,BANat), | |
| 407 | bv2nat(BB,BBNat), | |
| 408 | Int2 = b(integer(2),integer,[]), | |
| 409 | Exp = b(power_of(Int2,BBNat),integer,[]), | |
| 410 | TooLarge = b(greater(BBNat,Width),pred,[]), | |
| 411 | Res = b(if_then_else(TooLarge,b(integer(0),integer,[]),b(div(BANat,Exp),integer,[])),integer,[]), | |
| 412 | nat2bv(Res,Width,Out). | |
| 413 | % division is a special case, because it has a different | |
| 414 | % semantic in B and SMT-LIB | |
| 415 | smt_term_to_prob_term(id_term(id(div),[Dividend|Divisors]),Env,Out) :- !, | |
| 416 | smt_term_to_prob_term(id_term(id('*'),Divisors),Env,BDivisor), | |
| 417 | smt_term_to_prob_term(Dividend,Env,BDividend), | |
| 418 | Zero = b(integer(0),integer,[]), | |
| 419 | DividendLessZero = b(less(BDividend,Zero),pred,[]), | |
| 420 | DivisorLessZero = b(less(BDivisor,Zero),pred,[]), | |
| 421 | DivisorGreaterZero = b(greater(BDivisor,Zero),pred,[]), | |
| 422 | DivisorMinusOne = b(minus(BDivisor,b(integer(1),integer,[])),integer,[]), | |
| 423 | DivisorPlusOne = b(add(BDivisor,b(integer(1),integer,[])),integer,[]), | |
| 424 | MinusDivisorPlusOne = b(unary_minus(DivisorPlusOne),integer,[]), | |
| 425 | ||
| 426 | conjunct_predicates([DividendLessZero,DivisorGreaterZero],If1), | |
| 427 | conjunct_predicates([DividendLessZero,DivisorLessZero],If2), | |
| 428 | ||
| 429 | FixInner = b(if_then_else(If2,MinusDivisorPlusOne,Zero),integer,[]), | |
| 430 | Fix = b(if_then_else(If1,DivisorMinusOne,FixInner),integer,[]), | |
| 431 | NewBDividend = b(minus(BDividend,Fix),integer,[]), | |
| 432 | Out = b(div(NewBDividend,BDivisor),integer,[]). | |
| 433 | % (mod a b) = a - b*(div a b), using the Euclidean div above; 0 <= result < |b| | |
| 434 | smt_term_to_prob_term(id_term(id(mod),[A,B]),Env,Out) :- !, | |
| 435 | smt_term_to_prob_term(id_term(id('-'),[A,id_term(id('*'),[B,id_term(id(div),[A,B])])]),Env,Out). | |
| 436 | % / is always real division in SMT-LIB, also for integer numerals as in (/ 1 3) | |
| 437 | smt_term_to_prob_term(id_term(id('/'),Args),Env,Out) :- !, | |
| 438 | maplist(smt_term_to_prob_term_maplist(Env),Args,BArgs), | |
| 439 | l_lift_types(BArgs,real,RArgs), | |
| 440 | interleave_left(div,RArgs,Out). | |
| 441 | % general cases | |
| 442 | smt_term_to_prob_term(id_term(id(Id),Args),Env,Out) :- | |
| 443 | smt_id_to_prob_id_preds(Id,BId), !, | |
| 444 | maplist(smt_term_to_prob_term_maplist(Env),Args,BArgs), | |
| 445 | maplist(bool_to_pred,BArgs,PredBArgs), | |
| 446 | interleave(BId,PredBArgs,Out). | |
| 447 | smt_term_to_prob_term(id_term(id(Id),Args),Env,Out) :- | |
| 448 | smt_id_to_prob_id(Id,BId,ConnectingPred), !, | |
| 449 | maplist(smt_term_to_prob_term_maplist(Env),Args,BArgs), | |
| 450 | call(ConnectingPred,BId,BArgs,Out). | |
| 451 | smt_term_to_prob_term(id_term(id(Id),Args),Env,Out) :- | |
| 452 | get_function(Id,Env,Params,_Results,Definition), !, | |
| 453 | replace_identifiers(Params,Args,Definition,Out,Env). | |
| 454 | smt_term_to_prob_term(id_term(id(Id),Args),Env,Out) :- | |
| 455 | get_type(Id,Env,set(couple(_X,Y))), !, | |
| 456 | smt_term_to_prob_term(id(Id),Env,BId), | |
| 457 | maplist(smt_term_to_prob_term_maplist(Env),Args,BArgs), | |
| 458 | create_couple(BArgs,BArg), | |
| 459 | Out = b(function(BId,BArg),Y,[]). | |
| 460 | smt_term_to_prob_term(id(true),_,b(boolean_true,boolean,[])) :- !. | |
| 461 | smt_term_to_prob_term(id(false),_,b(boolean_false,boolean,[])) :- !. | |
| 462 | smt_term_to_prob_term(id(Id),Env,Out) :- Params = [], | |
| 463 | get_function(Id,Env,Params,_Results,Definition), !, % a function without args exists, see dreal4:define_fun_04.smt2 | |
| 464 | Out = Definition. | |
| 465 | smt_term_to_prob_term(id(Id),Env,OutId) :- !, | |
| 466 | (get_type(Id,Env,Type) -> true | |
| 467 | ; add_error(smtlib2_translation,'Unknown identifier:',Id), | |
| 468 | portray_smtlib2_env(Env), | |
| 469 | Type=any), | |
| 470 | OutId = b(identifier(Id),Type,[]).%, | |
| 471 | %(Type = boolean | |
| 472 | % -> bool_to_pred(OutId,Out) | |
| 473 | % ; Out = OutId). | |
| 474 | smt_term_to_prob_term(id(Id,Sort),Env,OutId) :- !, | |
| 475 | smt_type_to_prob_type(Sort,Env,Type), | |
| 476 | OutId = b(identifier(Id),Type,[]). | |
| 477 | smt_term_to_prob_term(svar(Id,Sort),Env,Out) :- !, | |
| 478 | smt_type_to_prob_type(Sort,Env,Type), | |
| 479 | Out = b(identifier(Id),Type,[]). | |
| 480 | smt_term_to_prob_term(integer(I),_,INT) :- !, INT=b(integer(I),integer,[]). | |
| 481 | smt_term_to_prob_term(decimal(N),_,REAL) :- number(N),!, is_real(R,N), REAL=b(value(R),real,[]). | |
| 482 | smt_term_to_prob_term(let(Bindings,Term),Env,BTerm) :- !, | |
| 483 | let_equalities_and_bids(Bindings,BIDs,Assignments,Env), | |
| 484 | create_local_env(Env,BIDs,LocalEnv), | |
| 485 | smt_term_to_prob_term(Term,LocalEnv,InnerBTerm), | |
| 486 | get_texpr_type(InnerBTerm,InnerType), | |
| 487 | (InnerType = pred | |
| 488 | -> safe_create_texpr(let_predicate(BIDs,Assignments,InnerBTerm),pred,BTerm) | |
| 489 | ; safe_create_texpr(let_expression(BIDs,Assignments,InnerBTerm),InnerType,BTerm)). | |
| 490 | smt_term_to_prob_term(forall(IDs,Term),Env,Forall) :- !, | |
| 491 | maplist(smt_term_to_prob_term_maplist(Env),IDs,Identifiers), | |
| 492 | create_local_env(Env,Identifiers,LocalEnv), | |
| 493 | smt_term_to_prob_term(Term,LocalEnv,InnerTerm), | |
| 494 | convlist(typing_constraint,IDs,InnerConstraints), | |
| 495 | bool_to_pred(InnerTerm,InnerTermAsPred), % necessary ?? | |
| 496 | conjunct_predicates(InnerConstraints,LHS), | |
| 497 | create_implication(LHS,InnerTermAsPred,Body), | |
| 498 | create_forall(Identifiers,Body,Forall). | |
| 499 | smt_term_to_prob_term(exists(IDs,Term),Env,Forall) :- !, | |
| 500 | maplist(smt_term_to_prob_term_maplist(Env),IDs,Identifiers), | |
| 501 | create_local_env(Env,Identifiers,LocalEnv), | |
| 502 | smt_term_to_prob_term(Term,LocalEnv,InnerTerm), | |
| 503 | convlist(typing_constraint,IDs,InnerConstraints), | |
| 504 | append(InnerConstraints,[InnerTerm],IList), | |
| 505 | conjunct_predicates(IList,Inner), | |
| 506 | bool_to_pred(Inner,InnerAsPred), | |
| 507 | create_exists(Identifiers,InnerAsPred,Forall). | |
| 508 | smt_term_to_prob_term(bitvector(Value,Length),_Env,Out) :- !, | |
| 509 | integer_to_binary_couples(Value,Length,Couples), | |
| 510 | Out = b(set_extension(Couples),set(couple(integer,integer)),[]). | |
| 511 | smt_term_to_prob_term(bitvector(Bits),_Env,Out) :- !, | |
| 512 | ? | binary_to_binary_couples(Bits,Couples), |
| 513 | Out = b(set_extension(Couples),set(couple(integer,integer)),[]). | |
| 514 | smt_term_to_prob_term(id_term(id(NRAFUN),Args),Env,Out) :- | |
| 515 | external_function(NRAFUN,Name,Type), | |
| 516 | maplist(smt_term_to_prob_term_maplist(Env),Args,TArgs), | |
| 517 | l_lift_types(TArgs,Type,LTargs), | |
| 518 | Out = b(external_function_call(Name,LTargs),Type,[]). | |
| 519 | % conversions between Int and Real | |
| 520 | smt_term_to_prob_term(id_term(id(to_real),[A]),Env,Out) :- !, | |
| 521 | smt_term_to_prob_term(A,Env,BA), | |
| 522 | lift_type_to(real,BA,Out). | |
| 523 | smt_term_to_prob_term(id_term(id(to_int),[A]),Env,Out) :- !, % largest integer not greater than A | |
| 524 | smt_term_to_prob_term(A,Env,BA), | |
| 525 | lift_type_to(real,BA,RA), | |
| 526 | Out = b(convert_int_floor(RA),integer,[]). | |
| 527 | smt_term_to_prob_term(id_term(id(is_int),[A]),Env,Out) :- !, | |
| 528 | smt_term_to_prob_term(A,Env,BA), | |
| 529 | lift_type_to(real,BA,RA), | |
| 530 | Floor = b(convert_real(b(convert_int_floor(RA),integer,[])),real,[]), | |
| 531 | Out = b(equal(Floor,RA),pred,[]). | |
| 532 | % for Pair type; TODO: infer this processing from declare-datatype | |
| 533 | smt_term_to_prob_term(id_term(id(fst),[Pair]),Env,Out) :- !, | |
| 534 | smt_term_to_prob_term(Pair,Env,BPair), | |
| 535 | get_texpr_type(BPair,couple(TA,_)), | |
| 536 | Out = b(first_of_pair(BPair),TA,[]). | |
| 537 | smt_term_to_prob_term(id_term(id(snd),[Pair]),Env,Out) :- !, | |
| 538 | smt_term_to_prob_term(Pair,Env,BPair), | |
| 539 | get_texpr_type(BPair,couple(_,TB)), | |
| 540 | Out = b(second_of_pair(BPair),TB,[]). | |
| 541 | smt_term_to_prob_term(X,_,_) :- | |
| 542 | add_error(smtlib2_translation,'Unsupported term in smt_term_to_prob_term:',X), fail. | |
| 543 | ||
| 544 | % type is type of result and type of all arguments | |
| 545 | external_function(abs,'RABS',real). | |
| 546 | external_function(arccos,'RACOS',real). | |
| 547 | external_function(arcsin,'RASIN',real). | |
| 548 | external_function(asin,'RASIN',real). | |
| 549 | external_function(arctan,'RATAN',real). | |
| 550 | external_function(cos,'RCOS',real). | |
| 551 | external_function(sin,'RSIN',real). | |
| 552 | external_function(tan,'RTAN',real). | |
| 553 | external_function(exp,'REXP',real). | |
| 554 | external_function(sinh,'RSINH',real). | |
| 555 | external_function(cosh,'RCOSH',real). | |
| 556 | external_function(tanh,'RTANH',real). | |
| 557 | external_function('^','RPOW',real). % sometimes exponent is also integer | |
| 558 | external_function(pow,'RPOW',real). | |
| 559 | external_function(log,'RLOGe',real). | |
| 560 | external_function(sqrt,'RSQRT',real). | |
| 561 | external_function(arctan2,'RATAN2',real). | |
| 562 | external_function(max,'RMAX',real). | |
| 563 | external_function(min,'RMIN',real). | |
| 564 | ||
| 565 | ||
| 566 | bool_to_pred(Bool,Pred) :- | |
| 567 | get_texpr_expr(Bool,convert_bool(Pred)), !. | |
| 568 | bool_to_pred(Bool,Pred) :- | |
| 569 | get_texpr_type(Bool,boolean), !, | |
| 570 | safe_create_texpr(equal(Bool,b(boolean_true,boolean,[])),pred,Pred). | |
| 571 | bool_to_pred(Bool,Bool) :- | |
| 572 | get_texpr_type(Bool,pred), !. | |
| 573 | ||
| 574 | to_bool_if_necessary(PossiblePred,Bool) :- | |
| 575 | get_texpr_type(PossiblePred,pred), !, | |
| 576 | safe_create_texpr(convert_bool(PossiblePred),boolean,Bool). | |
| 577 | to_bool_if_necessary(NonPred,NonPred). | |
| 578 | ||
| 579 | let_equalities_and_bids([bind(ID,Term)],[IDTerm],[AssOut],Env) :- !, | |
| 580 | smt_term_to_prob_term(Term,Env,Ass), | |
| 581 | get_texpr_type(Ass,IdentifierType), | |
| 582 | (IdentifierType == pred | |
| 583 | -> IDTerm = b(identifier(ID),boolean,[]), | |
| 584 | safe_create_texpr(convert_bool(Ass),boolean,AssOut) | |
| 585 | ; IDTerm = b(identifier(ID),IdentifierType,[]), | |
| 586 | AssOut = Ass). | |
| 587 | let_equalities_and_bids([bind(ID,Term)|Further],[IDTerm|FurtherIdentifiers],Assignments,Env) :- | |
| 588 | let_equalities_and_bids([bind(ID,Term)],[IDTerm],FirstAssignment,Env), | |
| 589 | let_equalities_and_bids(Further,FurtherIdentifiers,FurtherAssignments,Env), | |
| 590 | append(FirstAssignment,FurtherAssignments,Assignments). | |
| 591 | ||
| 592 | replace_identifiers([],[],D,D,_Env). | |
| 593 | replace_identifiers([b(identifier(I),Type,_)|T1],[Term|Terms],In,Out,Env) :- | |
| 594 | smt_term_to_prob_term(Term,Env,BTerm), | |
| 595 | lift_type_to(Type,BTerm,LBTerm), | |
| 596 | replace_id_by_expr(In,I,LBTerm,TOut), | |
| 597 | replace_identifiers(T1,Terms,TOut,Out,Env). | |
| 598 | ||
| 599 | % certain sorts enforce an inner constrait to strengthen their type | |
| 600 | typing_constraint(svar(Name,sort('Array',[Index,Element])),Constraint) :- | |
| 601 | smt_type_to_prob_type(Index,EIn,BIndex), | |
| 602 | smt_type_to_prob_type(Element,EIn,BElement), | |
| 603 | Identifier = b(identifier(Name),FullType,[]), | |
| 604 | Constraint = b(member(Identifier,b(EXPR,set(FullType),[])),pred,[]), | |
| 605 | type_to_expr(BIndex,From), | |
| 606 | (BElement=boolean,get_preference(smtlib2b_arrays_as_sets,true) % we translate boolean Array as Set | |
| 607 | -> EXPR = pow_subset(From), | |
| 608 | FullType = set(BIndex) | |
| 609 | ; type_to_expr(BElement,To), | |
| 610 | EXPR=total_function(From,To), | |
| 611 | FullType = set(couple(BIndex,BElement)) | |
| 612 | ). | |
| 613 | typing_constraint(svar(Name,sort('BitVec',[Length])),Constraint) :- | |
| 614 | Zero = b(integer(0),integer,[]), | |
| 615 | One = b(integer(1),integer,[]), | |
| 616 | L2 is Length - 1, | |
| 617 | LengthMinusOne = b(integer(L2),integer,[]), | |
| 618 | FullType = set(couple(integer,integer)), | |
| 619 | Identifier = b(identifier(Name),FullType,[]), | |
| 620 | From = b(interval(Zero,LengthMinusOne),set(integer),[]), | |
| 621 | To = b(interval(Zero,One),set(integer),[]), | |
| 622 | Constraint = b(member(Identifier,b(total_function(From,To),set(FullType),[])),pred,[]). | |
| 623 | ||
| 624 | is_function_constraint(Id,FullType,Constraint) :- | |
| 625 | FullType = set(couple(From,To)), | |
| 626 | Identifier = b(identifier(Id),FullType,[]), | |
| 627 | type_to_expr(From,FromExpr), | |
| 628 | type_to_expr(To,ToExpr), | |
| 629 | Constraint = b(member(Identifier,b(partial_function(FromExpr,ToExpr),set(FullType),[])),pred,[]). | |
| 630 | ||
| 631 | integer_to_binary_couples(Value,Length,Couples) :- | |
| 632 | PLength is Length - 1, | |
| 633 | integer_to_binary_couples(Value,0,PLength,Couples). | |
| 634 | integer_to_binary_couples(Value,Current,Current,[b(couple(A,B),couple(integer,integer),[])]) :- !, | |
| 635 | A = b(integer(Current),integer,[]), | |
| 636 | BVal is mod(Value,2), | |
| 637 | B = b(integer(BVal),integer,[]). | |
| 638 | integer_to_binary_couples(Value,Current,PLength,[b(couple(A,B),couple(integer,integer),[])|Cs]) :- | |
| 639 | A = b(integer(Current),integer,[]), | |
| 640 | BVal is mod(Value,2), | |
| 641 | B = b(integer(BVal),integer,[]), | |
| 642 | NValue is Value // 2, | |
| 643 | NCurrent is Current + 1, | |
| 644 | integer_to_binary_couples(NValue,NCurrent,PLength,Cs). | |
| 645 | ||
| 646 | binary_to_binary_couples(Bits,Couples) :- | |
| 647 | length(Bits,L), FirstL is L - 1, | |
| 648 | ? | binary_to_binary_couples(FirstL,Bits,Couples). |
| 649 | binary_to_binary_couples(-1,[],[]). | |
| 650 | binary_to_binary_couples(L,[Bit|Bits],[Couple|Couples]) :- | |
| 651 | A = b(integer(L),integer,[]), | |
| 652 | B = b(integer(Bit),integer,[]), | |
| 653 | Couple = b(couple(A,B),couple(integer,integer),[]), | |
| 654 | L2 is L - 1, | |
| 655 | ? | binary_to_binary_couples(L2,Bits,Couples). |
| 656 | ||
| 657 | smt_id_to_prob_id('<=',less_equal,chain). | |
| 658 | smt_id_to_prob_id('>=',greater_equal,chain). | |
| 659 | smt_id_to_prob_id('<',less,chain). | |
| 660 | smt_id_to_prob_id('>',greater,chain). | |
| 661 | smt_id_to_prob_id('distinct',not_equal,pairwise). | |
| 662 | smt_id_to_prob_id('*',multiplication,interleave). | |
| 663 | smt_id_to_prob_id('+',add,interleave). | |
| 664 | smt_id_to_prob_id('-',minus,interleave_left). | |
| 665 | %smt_id_to_prob_id('^',power_of,interleave). % TODO: change associativity | |
| 666 | ||
| 667 | smt_id_to_prob_id_preds('or',disjunct). | |
| 668 | smt_id_to_prob_id_preds('and',conjunct). | |
| 669 | smt_id_to_prob_id_preds('=>',implication). | |
| 670 | smt_id_to_prob_id_preds('<=>',equivalence). | |
| 671 | smt_id_to_prob_id_preds(xor,xor_b_pred). % see construct_operator | |
| 672 | ||
| 673 | % bit vectors are total functions from 0..Width-1 to 0..1, index 0 is the least significant bit | |
| 674 | % note: bvwidth returns the largest index, i.e., Width-1 | |
| 675 | bvwidth(BV,Width) :- | |
| 676 | Width = b(max(b(domain(BV),set(integer),[])),integer,[]). | |
| 677 | ||
| 678 | % add NewLength bits with value Bit above the largest index WidthA of BA | |
| 679 | bv_extension(BA,WidthA,NewLength,Bit,Out) :- | |
| 680 | Int1 = b(integer(1),integer,[]), | |
| 681 | From = b(add(WidthA,Int1),integer,[]), | |
| 682 | To = b(add(WidthA,b(integer(NewLength),integer,[])),integer,[]), | |
| 683 | NewIndices = b(interval(From,To),set(integer),[]), | |
| 684 | NewBits = b(cartesian_product(NewIndices,b(set_extension([Bit]),set(integer),[])),set(couple(integer,integer)),[]), | |
| 685 | Out = b(union(BA,NewBits),set(couple(integer,integer)),[]). | |
| 686 | ||
| 687 | % 2^Width for the largest index Width-1 | |
| 688 | bvmodulus(MaxIndex,Pow) :- | |
| 689 | Pow = b(power_of(b(integer(2),integer,[]),b(add(MaxIndex,b(integer(1),integer,[])),integer,[])),integer,[]). | |
| 690 | ||
| 691 | bv2nat(BV,Nat) :- | |
| 692 | IntTwo = b(integer(2),integer,[]), | |
| 693 | IdX1 = b(identifier('\\tmp1'),integer,[]), | |
| 694 | IdX2 = b(identifier('\\tmp2'),integer,[]), | |
| 695 | PowerOf = b(power_of(IntTwo,IdX1),integer,[]), | |
| 696 | Nat = b(general_sum([IdX1,IdX2],b(member(b(couple(IdX1,IdX2),couple(integer,integer),[]),BV),pred,[]),b(multiplication(IdX2,PowerOf),integer,[])),integer,[]). | |
| 697 | % two's complement: the most significant bit has weight -2^(Width-1) | |
| 698 | signed_bv2nat(BV,Nat) :- | |
| 699 | bv2nat(BV,UNat), | |
| 700 | bvwidth(BV,MaxIndex), | |
| 701 | MSB = b(function(BV,MaxIndex),integer,[]), | |
| 702 | bvmodulus(MaxIndex,Pow), | |
| 703 | Nat = b(minus(UNat,b(multiplication(MSB,Pow),integer,[])),integer,[]). | |
| 704 | ||
| 705 | % Nat must be non-negative; it is taken modulo 2^Width (Width is the largest index) | |
| 706 | nat2bv(Nat,Width,BV) :- | |
| 707 | IntTwo = b(integer(2),integer,[]), | |
| 708 | IdX1 = b(identifier('\\tmp1'),integer,[]), | |
| 709 | IdX2 = b(identifier('\\tmp2'),integer,[]), | |
| 710 | TypeId1 = b(member(IdX1,b(interval(b(integer(0),integer,[]),Width),set(integer),[])),pred,[]), | |
| 711 | TypeId2 = b(member(IdX2,b(interval(b(integer(0),integer,[]),b(integer(1),integer,[])),set(integer),[])),pred,[]), | |
| 712 | PowerOf = b(power_of(IntTwo,IdX1),integer,[]), | |
| 713 | ValueOfId2 = b(equal(IdX2,b(modulo(b(div(Nat,PowerOf),integer,[]),IntTwo),integer,[])),pred,[]), | |
| 714 | conjunct_predicates([TypeId1,TypeId2,ValueOfId2],InnerPred), | |
| 715 | BV = b(comprehension_set([IdX1,IdX2],InnerPred),set(couple(integer,integer)),[]). | |
| 716 | ||
| 717 | type_to_expr(set(A),Res) :- !, Res = b(pow_subset(AE),set(set(A)),[]), | |
| 718 | type_to_expr(A,AE). | |
| 719 | type_to_expr(couple(A,B),b(cartesian_product(AE,BE),set(couple(AET,BET)),[])) :- !, | |
| 720 | type_to_expr(A,AE), type_to_expr(B,BE), | |
| 721 | get_texpr_type(AE,AET), get_texpr_type(BE,BET). | |
| 722 | type_to_expr(integer,b(integer_set('INTEGER'),set(integer),[])) :- !. | |
| 723 | type_to_expr(boolean,b(bool_set,set(boolean),[])) :- !. | |
| 724 | type_to_expr(global(E),b(identifier(E),set(global(E)),[])) :- !. | |
| 725 | type_to_expr(T,_) :- | |
| 726 | add_error(smtlib2_translation,'Unsupported type in type_to_expr:',T), fail. | |
| 727 | ||
| 728 | signed_bv_to_nat_and_compare(A,B,Op,Env,Out) :- | |
| 729 | ? | smt_term_to_prob_term(A,Env,BA), |
| 730 | ? | smt_term_to_prob_term(B,Env,BB), |
| 731 | signed_bv2nat(BA,BANat), | |
| 732 | signed_bv2nat(BB,BBNat), | |
| 733 | Operation =.. [Op,BANat,BBNat], | |
| 734 | Out = b(Operation,pred,[]). | |
| 735 | ||
| 736 | bv_to_nat_and_compare(A,B,Op,Env,Out) :- | |
| 737 | ? | smt_term_to_prob_term(A,Env,BA), |
| 738 | ? | smt_term_to_prob_term(B,Env,BB), |
| 739 | bv2nat(BA,BANat), | |
| 740 | bv2nat(BB,BBNat), | |
| 741 | Operation =.. [Op,BANat,BBNat], | |
| 742 | Out = b(Operation,pred,[]). |