author | blanchet |
Fri, 12 Aug 2022 15:35:07 +0200 | |
changeset 75806 | 2b106aae897c |
parent 74817 | src/HOL/Tools/SMT/cvc4_interface.ML@1fd8705503b4 |
permissions | -rw-r--r-- |
75806
2b106aae897c
added support for cvc5 (whose interface is almost identical to CVC4)
blanchet
parents:
74817
diff
changeset
|
1 |
(* Title: HOL/Tools/SMT/cvc_interface.ML |
58369 | 2 |
Author: Jasmin Blanchette, TU Muenchen |
58360 | 3 |
|
75806
2b106aae897c
added support for cvc5 (whose interface is almost identical to CVC4)
blanchet
parents:
74817
diff
changeset
|
4 |
Interface to CVC4 and cvc5 based on an extended version of SMT-LIB. |
58360 | 5 |
*) |
6 |
||
75806
2b106aae897c
added support for cvc5 (whose interface is almost identical to CVC4)
blanchet
parents:
74817
diff
changeset
|
7 |
signature CVC_INTERFACE = |
58360 | 8 |
sig |
75806
2b106aae897c
added support for cvc5 (whose interface is almost identical to CVC4)
blanchet
parents:
74817
diff
changeset
|
9 |
val smtlib_cvcC: SMT_Util.class |
2b106aae897c
added support for cvc5 (whose interface is almost identical to CVC4)
blanchet
parents:
74817
diff
changeset
|
10 |
val hosmtlib_cvcC: SMT_Util.class |
58360 | 11 |
end; |
12 |
||
75806
2b106aae897c
added support for cvc5 (whose interface is almost identical to CVC4)
blanchet
parents:
74817
diff
changeset
|
13 |
structure CVC_Interface: CVC_INTERFACE = |
58360 | 14 |
struct |
15 |
||
75806
2b106aae897c
added support for cvc5 (whose interface is almost identical to CVC4)
blanchet
parents:
74817
diff
changeset
|
16 |
val cvcC = ["cvc"] |
2b106aae897c
added support for cvc5 (whose interface is almost identical to CVC4)
blanchet
parents:
74817
diff
changeset
|
17 |
val smtlib_cvcC = SMTLIB_Interface.smtlibC @ cvcC |
2b106aae897c
added support for cvc5 (whose interface is almost identical to CVC4)
blanchet
parents:
74817
diff
changeset
|
18 |
val hosmtlib_cvcC = SMTLIB_Interface.hosmtlibC @ cvcC |
58360 | 19 |
|
20 |
||
21 |
(* interface *) |
|
22 |
||
23 |
local |
|
66551 | 24 |
fun translate_config order ctxt = |
25 |
{order = order, |
|
74817
1fd8705503b4
generate problems with correct logic for veriT
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
66551
diff
changeset
|
26 |
logic = K (K "(set-logic ALL_SUPPORTED)\n"), |
66551 | 27 |
fp_kinds = [BNF_Util.Least_FP, BNF_Util.Greatest_FP], |
28 |
serialize = #serialize (SMTLIB_Interface.translate_config order ctxt)} |
|
58360 | 29 |
in |
30 |
||
66551 | 31 |
val _ = Theory.setup (Context.theory_map |
75806
2b106aae897c
added support for cvc5 (whose interface is almost identical to CVC4)
blanchet
parents:
74817
diff
changeset
|
32 |
(SMT_Translate.add_config (smtlib_cvcC, translate_config SMT_Util.First_Order) #> |
2b106aae897c
added support for cvc5 (whose interface is almost identical to CVC4)
blanchet
parents:
74817
diff
changeset
|
33 |
SMT_Translate.add_config (hosmtlib_cvcC, translate_config SMT_Util.Higher_Order))) |
58360 | 34 |
|
35 |
end |
|
36 |
||
37 |
end; |