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