equal
deleted
inserted
replaced
17 |
17 |
18 (* interface *) |
18 (* interface *) |
19 |
19 |
20 local |
20 local |
21 fun translate_config ctxt = |
21 fun translate_config ctxt = |
22 {logic = K "", fp_kinds = [BNF_Util.Least_FP, BNF_Util.Greatest_FP], |
22 {logic = K "(set-logic AUFDTLIA)\n", fp_kinds = [BNF_Util.Least_FP, BNF_Util.Greatest_FP], |
23 serialize = #serialize (SMTLIB_Interface.translate_config ctxt)} |
23 serialize = #serialize (SMTLIB_Interface.translate_config ctxt)} |
24 in |
24 in |
25 |
25 |
26 val _ = |
26 val _ = |
27 Theory.setup (Context.theory_map (SMT_Translate.add_config (smtlib_cvc4C, translate_config))) |
27 Theory.setup (Context.theory_map (SMT_Translate.add_config (smtlib_cvc4C, translate_config))) |