1(* Copyright (c) 2010-2011 Tjark Weber. All rights reserved. *) 2 3(* SMT-LIB 2 logics *) 4 5structure SmtLib_Logics = 6struct 7 8local 9 10 val ERR = Feedback.mk_HOL_ERR "SmtLib_Logics" 11 12 fun union_dicts (x::xs) = 13 List.foldl (Lib.uncurry Library.union_dict o Lib.swap) x xs 14 | union_dicts [] = 15 raise ERR "union_dicts" "empty list" 16 17 (* because int-to-real conversions may be combined with :chainable 18 and :{left,right}-assoc functions, 'one_int_to_real' converts *at 19 most* (rather than exactly) one integer argument to real *) 20 fun one_int_to_real (t1, t2) = 21 (intrealSyntax.mk_real_of_int t1, t2) 22 handle Feedback.HOL_ERR _ => 23 (t1, intrealSyntax.mk_real_of_int t2) 24 handle Feedback.HOL_ERR _ => 25 (t1, t2) 26 27 (* converts *at most* (rather than exactly) two integer arguments to 28 reals (cf. 'one_int_to_real' *) 29 fun two_ints_to_real (t1, t2) = 30 (intrealSyntax.mk_real_of_int t1, intrealSyntax.mk_real_of_int t2) 31 handle Feedback.HOL_ERR _ => 32 one_int_to_real (t1, t2) 33 34 open SmtLib_Theories 35 36 val BV_extension_tmdict = Library.dict_from_list [ 37 (* bit-vector constants *) 38 ("_", one_zero (fn token => 39 if String.isPrefix "bv" token then 40 let 41 val decimal = String.extract (token, 2, NONE) 42 val value = Arbnum.fromString decimal 43 in 44 Lib.curry wordsSyntax.mk_word value 45 end 46 else 47 raise ERR "<BV_extension_dict._>" "not a bit-vector constant")), 48 ("bvnand", K_zero_two wordsSyntax.mk_word_nand), 49 ("bvnor", K_zero_two wordsSyntax.mk_word_nor), 50 ("bvxor", K_zero_two wordsSyntax.mk_word_xor), 51 ("bvxnor", K_zero_two wordsSyntax.mk_word_xnor), 52 ("bvcomp", K_zero_two wordsSyntax.mk_word_compare), 53 ("bvsub", K_zero_two wordsSyntax.mk_word_sub), 54 ("bvsdiv", K_zero_two wordsSyntax.mk_word_quot), 55 ("bvsrem", K_zero_two wordsSyntax.mk_word_rem), 56 ("bvsmod", K_zero_two integer_wordSyntax.mk_word_smod), 57 ("bvashr", K_zero_two wordsSyntax.mk_word_asr_bv), 58 ("repeat", K_one_one 59 (Lib.curry wordsSyntax.mk_word_replicate o numSyntax.mk_numeral)), 60 ("zero_extend", K_one_one (fn n => fn t => wordsSyntax.mk_w2w (t, 61 fcpLib.index_type 62 (Arbnum.+ (fcpLib.index_to_num (wordsSyntax.dim_of t), n))))), 63 ("sign_extend", K_one_one (fn n => fn t => wordsSyntax.mk_sw2sw (t, 64 fcpLib.index_type 65 (Arbnum.+ (fcpLib.index_to_num (wordsSyntax.dim_of t), n))))), 66 ("rotate_left", K_one_one 67 (Lib.C (Lib.curry wordsSyntax.mk_word_rol) o numSyntax.mk_numeral)), 68 ("rotate_right", K_one_one 69 (Lib.C (Lib.curry wordsSyntax.mk_word_ror) o numSyntax.mk_numeral)), 70 ("bvule", K_zero_two wordsSyntax.mk_word_ls), 71 ("bvugt", K_zero_two wordsSyntax.mk_word_hi), 72 ("bvuge", K_zero_two wordsSyntax.mk_word_hs), 73 ("bvslt", K_zero_two wordsSyntax.mk_word_lt), 74 ("bvsle", K_zero_two wordsSyntax.mk_word_le), 75 ("bvsgt", K_zero_two wordsSyntax.mk_word_gt), 76 ("bvsge", K_zero_two wordsSyntax.mk_word_ge) 77 ] 78 79in 80 81 (* In general, parsing is too liberal -- for instance, we do not 82 check that the input satisfies the linearity constraints that are 83 defined by various logics. Our aim is not to validate the SMT-LIB 84 input, but merely to produce meaningful results for valid 85 inputs. *) 86 87 structure AUFLIA = 88 struct 89 val tydict = union_dicts [Core.tydict, Ints.tydict, ArraysEx.tydict] 90 val tmdict = union_dicts [Core.tmdict, Ints.tmdict, ArraysEx.tmdict] 91 end 92 93 structure AUFLIRA = 94 struct 95 val tydict = union_dicts [Core.tydict, Reals_Ints.tydict, ArraysEx.tydict] 96 val tmdict = union_dicts [Core.tmdict, Reals_Ints.tmdict, ArraysEx.tmdict, 97 (* "For every operator op with declaration (op Real Real s) for 98 some sort s, and every term t1, t2 of sort Int and t of sort 99 Real, the expression 100 101 - (op t1 t) is syntactic sugar for (op (to_real t1) t) 102 - (op t t1) is syntactic sugar for (op t (to_real t1)) 103 - (/ t1 t2) is syntactic sugar for (/ (to_real t1) (to_real t2))" 104 105 We only implement this for the operators in 106 {Core,Reals_Ints,ArraysEx}.tmdict. Implementing it in 107 general, also for user-defined operators, would require a 108 change to our parser architecture. 109 110 A discussion on the SMT-LIB mailing list in October 2010 111 (http://www.cs.nyu.edu/pipermail/smt-lib/2010/000403.html) 112 was in favor of removing implicit conversions from the 113 SMT-LIB language altogether, but this is not reflected in the 114 SMT-LIB standard yet. *) 115 116 Library.dict_from_list [ 117 ("=", chainable (boolSyntax.mk_eq o one_int_to_real)), 118 ("-", leftassoc (realSyntax.mk_minus o one_int_to_real)), 119 ("+", leftassoc (realSyntax.mk_plus o one_int_to_real)), 120 ("*", leftassoc (realSyntax.mk_mult o one_int_to_real)), 121 ("/", leftassoc (realSyntax.mk_div o two_ints_to_real)), 122 ("<=", chainable (realSyntax.mk_leq o one_int_to_real)), 123 ("<", chainable (realSyntax.mk_less o one_int_to_real)), 124 (">=", chainable (realSyntax.mk_geq o one_int_to_real)), 125 (">", chainable (realSyntax.mk_great o one_int_to_real)) 126 ]] 127 end 128 129 structure AUFNIRA = 130 struct 131 val tydict = AUFLIRA.tydict 132 val tmdict = AUFLIRA.tmdict 133 end 134 135 structure LRA = 136 struct 137 val tydict = union_dicts [Core.tydict, Reals.tydict] 138 val tmdict = union_dicts [Core.tmdict, Reals.tmdict] 139 end 140 141 structure QF_ABV = 142 struct 143 val tydict = union_dicts [Core.tydict, Fixed_Size_BitVectors.tydict, 144 ArraysEx.tydict] 145 val tmdict = union_dicts [Core.tmdict, Fixed_Size_BitVectors.tmdict, 146 ArraysEx.tmdict, BV_extension_tmdict] 147 end 148 149 structure QF_AUFBV = 150 struct 151 val tydict = QF_ABV.tydict 152 val tmdict = QF_ABV.tmdict 153 end 154 155 structure QF_AUFLIA = 156 struct 157 val tydict = AUFLIA.tydict 158 val tmdict = AUFLIA.tmdict 159 end 160 161 structure QF_AX = 162 struct 163 val tydict = union_dicts [Core.tydict, ArraysEx.tydict] 164 val tmdict = union_dicts [Core.tmdict, ArraysEx.tmdict] 165 end 166 167 structure QF_BV = 168 struct 169 val tydict = union_dicts [Core.tydict, Fixed_Size_BitVectors.tydict] 170 val tmdict = union_dicts [Core.tmdict, Fixed_Size_BitVectors.tmdict, 171 BV_extension_tmdict] 172 end 173 174 structure QF_IDL = 175 struct 176 val tydict = union_dicts [Core.tydict, Ints.tydict] 177 val tmdict = union_dicts [Core.tmdict, Ints.tmdict] 178 end 179 180 structure QF_LIA = 181 struct 182 val tydict = QF_IDL.tydict 183 val tmdict = QF_IDL.tmdict 184 end 185 186 structure QF_LRA = 187 struct 188 val tydict = LRA.tydict 189 val tmdict = LRA.tmdict 190 end 191 192 structure QF_NIA = 193 struct 194 val tydict = QF_IDL.tydict 195 val tmdict = QF_IDL.tmdict 196 end 197 198 structure QF_NRA = 199 struct 200 val tydict = LRA.tydict 201 val tmdict = LRA.tmdict 202 end 203 204 structure QF_RDL = 205 struct 206 val tydict = LRA.tydict 207 val tmdict = LRA.tmdict 208 end 209 210 structure QF_UF = 211 struct 212 val tydict = Core.tydict 213 val tmdict = Core.tmdict 214 end 215 216 structure QF_UFBV = 217 struct 218 val tydict = QF_BV.tydict 219 val tmdict = QF_BV.tmdict 220 end 221 222 structure QF_UFIDL = 223 struct 224 val tydict = QF_IDL.tydict 225 val tmdict = QF_IDL.tmdict 226 end 227 228 structure QF_UFLIA = 229 struct 230 val tydict = QF_IDL.tydict 231 val tmdict = QF_IDL.tmdict 232 end 233 234 structure QF_UFLRA = 235 struct 236 val tydict = LRA.tydict 237 val tmdict = LRA.tmdict 238 end 239 240 structure QF_UFNRA = 241 struct 242 val tydict = LRA.tydict 243 val tmdict = LRA.tmdict 244 end 245 246 structure UFLRA = 247 struct 248 val tydict = LRA.tydict 249 val tmdict = LRA.tmdict 250 end 251 252 structure UFNIA = 253 struct 254 val tydict = QF_IDL.tydict 255 val tmdict = QF_IDL.tmdict 256 end 257 258 (* returns a type dictionary and a term dictionary that can be used 259 to parse types/terms of the given SMT-LIB 2 logic *) 260 fun parsedicts_of_logic (logic : string) = 261 case logic of 262 "AUFLIA" => 263 (AUFLIA.tydict, AUFLIA.tmdict) 264 | "AUFLIRA" => 265 (AUFLIRA.tydict, AUFLIRA.tmdict) 266 | "AUFNIRA" => 267 (AUFNIRA.tydict, AUFNIRA.tmdict) 268 | "LRA" => 269 (LRA.tydict, LRA.tmdict) 270 | "QF_ABV" => 271 (QF_ABV.tydict, QF_ABV.tmdict) 272 | "QF_AUFBV" => 273 (QF_AUFBV.tydict, QF_AUFBV.tmdict) 274 | "QF_AUFLIA" => 275 (QF_AUFLIA.tydict, QF_AUFLIA.tmdict) 276 | "QF_AX" => 277 (QF_AX.tydict, QF_AX.tmdict) 278 | "QF_BV" => 279 (QF_BV.tydict, QF_BV.tmdict) 280 | "QF_IDL" => 281 (QF_IDL.tydict, QF_IDL.tmdict) 282 | "QF_LIA" => 283 (QF_LIA.tydict, QF_LIA.tmdict) 284 | "QF_LRA" => 285 (QF_LRA.tydict, QF_LRA.tmdict) 286 | "QF_NIA" => 287 (QF_NIA.tydict, QF_NIA.tmdict) 288 | "QF_NRA" => 289 (QF_NRA.tydict, QF_NRA.tmdict) 290 | "QF_RDL" => 291 (QF_RDL.tydict, QF_RDL.tmdict) 292 | "QF_UF" => 293 (QF_UF.tydict, QF_UF.tmdict) 294 | "QF_UFBV" => 295 (QF_UFBV.tydict, QF_UFBV.tmdict) 296 | "QF_UFIDL" => 297 (QF_UFIDL.tydict, QF_UFIDL.tmdict) 298 | "QF_UFLIA" => 299 (QF_UFLIA.tydict, QF_UFLIA.tmdict) 300 | "QF_UFLRA" => 301 (QF_UFLRA.tydict, QF_UFLRA.tmdict) 302 | "QF_UFNRA" => 303 (QF_UFNRA.tydict, QF_UFNRA.tmdict) 304 | "UFLRA" => 305 (UFLRA.tydict, UFLRA.tmdict) 306 | "UFNIA" => 307 (UFNIA.tydict, UFNIA.tmdict) 308 | _ => 309 raise ERR "parsedicts_of_logic" ("unknown logic '" ^ logic ^ "'") 310 311end (* local *) 312 313end 314