equal
deleted
inserted
replaced
22 end; |
22 end; |
23 |
23 |
24 structure Z3_Interface: Z3_INTERFACE = |
24 structure Z3_Interface: Z3_INTERFACE = |
25 struct |
25 struct |
26 |
26 |
27 val smtlib_z3C = SMTLIB_Interface.smtlibC @ ["z3"] |
27 val z3C = ["z3"] |
|
28 |
|
29 val smtlib_z3C = SMTLIB_Interface.smtlibC @ z3C |
28 |
30 |
29 |
31 |
30 (* interface *) |
32 (* interface *) |
31 |
33 |
32 local |
34 local |
33 fun translate_config ctxt = |
35 fun translate_config ctxt = |
34 {logic = K "", fp_kinds = [BNF_Util.Least_FP], |
36 {order = SMT_Util.First_Order, |
35 serialize = #serialize (SMTLIB_Interface.translate_config ctxt)} |
37 logic = K "", |
|
38 fp_kinds = [BNF_Util.Least_FP], |
|
39 serialize = #serialize (SMTLIB_Interface.translate_config SMT_Util.First_Order ctxt)} |
36 |
40 |
37 fun is_div_mod @{const divide (int)} = true |
41 fun is_div_mod @{const divide (int)} = true |
38 | is_div_mod @{const modulo (int)} = true |
42 | is_div_mod @{const modulo (int)} = true |
39 | is_div_mod _ = false |
43 | is_div_mod _ = false |
40 |
44 |