equal
deleted
inserted
replaced
10 open Word_Lib |
10 open Word_Lib |
11 |
11 |
12 |
12 |
13 (* SMT-LIB logic *) |
13 (* SMT-LIB logic *) |
14 |
14 |
|
15 (* "QF_AUFBV" is too restricted for Isabelle's problems, which contain aritmetic and quantifiers. |
|
16 Better set the logic to "" and make at least Z3 happy. *) |
15 fun smtlib_logic ts = |
17 fun smtlib_logic ts = |
16 if exists (Term.exists_type (Term.exists_subtype is_wordT)) ts then SOME "QF_AUFBV" else NONE |
18 if exists (Term.exists_type (Term.exists_subtype is_wordT)) ts then SOME "" else NONE |
17 |
19 |
18 |
20 |
19 (* SMT-LIB builtins *) |
21 (* SMT-LIB builtins *) |
20 |
22 |
21 local |
23 local |