equal
deleted
inserted
replaced
9 datatype z3_non_commercial = |
9 datatype z3_non_commercial = |
10 Z3_Non_Commercial_Unknown | |
10 Z3_Non_Commercial_Unknown | |
11 Z3_Non_Commercial_Accepted | |
11 Z3_Non_Commercial_Accepted | |
12 Z3_Non_Commercial_Declined |
12 Z3_Non_Commercial_Declined |
13 val z3_non_commercial: unit -> z3_non_commercial |
13 val z3_non_commercial: unit -> z3_non_commercial |
|
14 val z3_with_extensions: bool Config.T |
14 val setup: theory -> theory |
15 val setup: theory -> theory |
15 end |
16 end |
16 |
17 |
17 structure SMT_Setup_Solvers: SMT_SETUP_SOLVERS = |
18 structure SMT_Setup_Solvers: SMT_SETUP_SOLVERS = |
18 struct |
19 struct |
130 (if getenv "Z3_COMPONENT" = "" then "" |
131 (if getenv "Z3_COMPONENT" = "" then "" |
131 else "\nSee also " ^ Path.print (Path.expand (Path.explode "$Z3_COMPONENT/etc/settings"))))) |
132 else "\nSee also " ^ Path.print (Path.expand (Path.explode "$Z3_COMPONENT/etc/settings"))))) |
132 |
133 |
133 end |
134 end |
134 |
135 |
|
136 |
|
137 val z3_with_extensions = |
|
138 Attrib.setup_config_bool @{binding z3_with_extensions} (K false) |
135 |
139 |
136 local |
140 local |
137 fun z3_make_command is_remote name () = |
141 fun z3_make_command is_remote name () = |
138 if_z3_non_commercial (make_command is_remote name) |
142 if_z3_non_commercial (make_command is_remote name) |
139 |
143 |
161 output rather than on the last line. *) |
165 output rather than on the last line. *) |
162 outcome (fn lines => (hd lines, tl lines)) |
166 outcome (fn lines => (hd lines, tl lines)) |
163 handle SMT_Failure.SMT _ => outcome (swap o split_last) |
167 handle SMT_Failure.SMT _ => outcome (swap o split_last) |
164 end |
168 end |
165 |
169 |
166 val with_extensions = |
|
167 Attrib.setup_config_bool @{binding z3_with_extensions} (K true) |
|
168 |
|
169 fun select_class ctxt = |
170 fun select_class ctxt = |
170 if Config.get ctxt with_extensions then Z3_Interface.smtlib_z3C |
171 if Config.get ctxt z3_with_extensions then Z3_Interface.smtlib_z3C |
171 else SMTLIB_Interface.smtlibC |
172 else SMTLIB_Interface.smtlibC |
172 |
173 |
173 fun mk is_remote = { |
174 fun mk is_remote = { |
174 name = make_name is_remote "z3", |
175 name = make_name is_remote "z3", |
175 class = select_class, |
176 class = select_class, |