41 |
41 |
42 fun is_int_div_mod @{const div (int)} = true |
42 fun is_int_div_mod @{const div (int)} = true |
43 | is_int_div_mod @{const mod (int)} = true |
43 | is_int_div_mod @{const mod (int)} = true |
44 | is_int_div_mod _ = false |
44 | is_int_div_mod _ = false |
45 |
45 |
46 fun add_div_mod irules = |
46 val have_int_div_mod = |
47 if exists (Term.exists_subterm is_int_div_mod o Thm.prop_of o snd) irules |
47 exists (Term.exists_subterm is_int_div_mod o Thm.prop_of) |
48 then [(~1, @{thm div_by_z3div}), (~1, @{thm mod_by_z3mod})] @ irules |
48 |
49 else irules |
49 fun add_div_mod _ (thms, extra_thms) = |
50 |
50 if have_int_div_mod thms orelse have_int_div_mod extra_thms then |
51 fun extra_norm' has_datatypes = extra_norm has_datatypes o add_div_mod |
51 (thms, @{thm div_by_z3div} :: @{thm mod_by_z3mod} :: extra_thms) |
|
52 else (thms, extra_thms) |
52 |
53 |
53 val setup_builtins = |
54 val setup_builtins = |
54 B.add_builtin_fun' smtlib_z3C (@{const z3div}, "div") #> |
55 B.add_builtin_fun' smtlib_z3C (@{const z3div}, "div") #> |
55 B.add_builtin_fun' smtlib_z3C (@{const z3mod}, "mod") |
56 B.add_builtin_fun' smtlib_z3C (@{const z3mod}, "mod") |
56 in |
57 in |
57 |
58 |
58 val interface = { |
59 val interface = { |
59 class = smtlib_z3C, |
60 class = smtlib_z3C, |
60 extra_norm = extra_norm', |
|
61 translate = { |
61 translate = { |
62 prefixes = prefixes, |
62 prefixes = prefixes, |
63 is_fol = is_fol, |
63 is_fol = is_fol, |
64 header = header, |
64 header = header, |
65 has_datatypes = true, |
65 has_datatypes = true, |
66 serialize = serialize}} |
66 serialize = serialize}} |
67 |
67 |
68 val setup = Context.theory_map setup_builtins |
68 val setup = Context.theory_map ( |
|
69 setup_builtins #> |
|
70 SMT_Normalize.add_extra_norm (smtlib_z3C, add_div_mod)) |
69 |
71 |
70 end |
72 end |
71 |
73 |
72 |
74 |
73 |
75 |