30 fun times _ _ ts = if is_linear ts then SOME ("*", 2, ts, mk_times) else NONE |
30 fun times _ _ ts = if is_linear ts then SOME ("*", 2, ts, mk_times) else NONE |
31 in |
31 in |
32 |
32 |
33 val setup_builtins = |
33 val setup_builtins = |
34 SMT_Builtin.add_builtin_typ SMTLIB_Interface.smtlibC |
34 SMT_Builtin.add_builtin_typ SMTLIB_Interface.smtlibC |
35 (@{typ real}, K (SOME "Real"), real_num) #> |
35 (@{typ real}, K (SOME ("Real", [])), real_num) #> |
36 fold (SMT_Builtin.add_builtin_fun' SMTLIB_Interface.smtlibC) [ |
36 fold (SMT_Builtin.add_builtin_fun' SMTLIB_Interface.smtlibC) [ |
37 (@{const less (real)}, "<"), |
37 (@{const less (real)}, "<"), |
38 (@{const less_eq (real)}, "<="), |
38 (@{const less_eq (real)}, "<="), |
39 (@{const uminus (real)}, "-"), |
39 (@{const uminus (real)}, "-"), |
40 (@{const plus (real)}, "+"), |
40 (@{const plus (real)}, "+"), |