equal
deleted
inserted
replaced
17 |
17 |
18 (* SMT-LIB logic *) |
18 (* SMT-LIB logic *) |
19 |
19 |
20 (* "QF_AUFBV" is too restrictive for Isabelle's problems, which contain aritmetic and quantifiers. |
20 (* "QF_AUFBV" is too restrictive for Isabelle's problems, which contain aritmetic and quantifiers. |
21 Better set the logic to "" and make at least Z3 happy. *) |
21 Better set the logic to "" and make at least Z3 happy. *) |
22 fun smtlib_logic ts = |
22 fun smtlib_logic "z3" ts = |
23 if exists (Term.exists_type (Term.exists_subtype is_wordT)) ts then SOME "" else NONE |
23 if exists (Term.exists_type (Term.exists_subtype is_wordT)) ts then SOME "" else NONE |
|
24 | smtlib_logic "verit" _ = NONE |
|
25 | smtlib_logic _ ts = |
|
26 if exists (Term.exists_type (Term.exists_subtype is_wordT)) ts then SOME "AUFBVLIRA" else NONE |
24 |
27 |
25 |
28 |
26 (* SMT-LIB builtins *) |
29 (* SMT-LIB builtins *) |
27 |
30 |
28 local |
31 local |
29 val smtlibC = SMTLIB_Interface.smtlibC |
32 val smtlibC = SMTLIB_Interface.smtlibC @ SMTLIB_Interface.bvsmlibC |
30 |
33 |
31 val wordT = \<^typ>\<open>'a::len word\<close> |
34 val wordT = \<^typ>\<open>'a::len word\<close> |
32 |
35 |
33 fun index1 s i = "(_ " ^ s ^ " " ^ string_of_int i ^ ")" |
36 fun index1 s i = "(_ " ^ s ^ " " ^ string_of_int i ^ ")" |
34 fun index2 s i j = "(_ " ^ s ^ " " ^ string_of_int i ^ " " ^ string_of_int j ^ ")" |
37 fun index2 s i j = "(_ " ^ s ^ " " ^ string_of_int i ^ " " ^ string_of_int j ^ ")" |