equal
deleted
inserted
replaced
7 structure SMT2_Word: sig end = |
7 structure SMT2_Word: sig end = |
8 struct |
8 struct |
9 |
9 |
10 open Word_Lib |
10 open Word_Lib |
11 |
11 |
|
12 |
12 (* SMT-LIB logic *) |
13 (* SMT-LIB logic *) |
13 |
14 |
14 fun smtlib_logic ts = |
15 fun smtlib_logic ts = |
15 if exists (Term.exists_type (Term.exists_subtype is_wordT)) ts |
16 if exists (Term.exists_type (Term.exists_subtype is_wordT)) ts then SOME "QF_AUFBV" else NONE |
16 then SOME "QF_AUFBV" |
|
17 else NONE |
|
18 |
17 |
19 |
18 |
20 (* SMT-LIB builtins *) |
19 (* SMT-LIB builtins *) |
21 |
20 |
22 local |
21 local |
139 |
138 |
140 val _ = Theory.setup (Context.theory_map ( |
139 val _ = Theory.setup (Context.theory_map ( |
141 SMTLIB2_Interface.add_logic (20, smtlib_logic) #> |
140 SMTLIB2_Interface.add_logic (20, smtlib_logic) #> |
142 setup_builtins)) |
141 setup_builtins)) |
143 |
142 |
144 end |
143 end; |