equal
deleted
inserted
replaced
37 |
37 |
38 fun mk_times ts = Term.list_comb (@{const times (real)}, ts) |
38 fun mk_times ts = Term.list_comb (@{const times (real)}, ts) |
39 |
39 |
40 fun times _ T ts = if is_linear ts then SOME ("*", 2, ts, mk_times) else NONE |
40 fun times _ T ts = if is_linear ts then SOME ("*", 2, ts, mk_times) else NONE |
41 | times _ _ _ = NONE |
41 | times _ _ _ = NONE |
42 |
|
43 fun mk_divide ts = Term.list_comb (@{const divide (real)}, ts) |
|
44 |
|
45 fun divide _ T (ts as [_, t]) = |
|
46 if U.is_number t then SOME ("/", 2, ts, mk_divide) else NONE |
|
47 | divide _ _ _ = NONE |
|
48 in |
42 in |
49 |
43 |
50 val setup_builtins = |
44 val setup_builtins = |
51 B.add_builtin_typ smtlibC (@{typ real}, K (SOME "Real"), real_num) #> |
45 B.add_builtin_typ smtlibC (@{typ real}, K (SOME "Real"), real_num) #> |
52 fold (B.add_builtin_fun' smtlibC) [ |
46 fold (B.add_builtin_fun' smtlibC) [ |
55 (@{const uminus (real)}, "~"), |
49 (@{const uminus (real)}, "~"), |
56 (@{const plus (real)}, "+"), |
50 (@{const plus (real)}, "+"), |
57 (@{const minus (real)}, "-") ] #> |
51 (@{const minus (real)}, "-") ] #> |
58 B.add_builtin_fun SMTLIB_Interface.smtlibC |
52 B.add_builtin_fun SMTLIB_Interface.smtlibC |
59 (Term.dest_Const @{const times (real)}, times) #> |
53 (Term.dest_Const @{const times (real)}, times) #> |
60 B.add_builtin_fun Z3_Interface.smtlib_z3C |
54 B.add_builtin_fun' Z3_Interface.smtlib_z3C (@{const times (real)}, "*") #> |
61 (Term.dest_Const @{const divide (real)}, divide) |
55 B.add_builtin_fun' Z3_Interface.smtlib_z3C (@{const divide (real)}, "/") |
62 |
56 |
63 end |
57 end |
64 |
58 |
65 |
59 |
66 (* Z3 constructors *) |
60 (* Z3 constructors *) |