136 |
138 |
137 (* Give the soft timeout a chance. *) |
139 (* Give the soft timeout a chance. *) |
138 val timeout_slack = seconds 1.0; |
140 val timeout_slack = seconds 1.0; |
139 |
141 |
140 fun run_chaku_on_prop state |
142 fun run_chaku_on_prop state |
141 ({mode_of_operation_params = {falsify, assms, spy, overlord, expect}, |
143 ({mode_of_operation_params = {solvers, falsify, assms, spy, overlord, expect}, |
142 scope_of_search_params = {wfs, whacks, cards, monos}, |
144 scope_of_search_params = {wfs, whacks, cards, monos}, |
143 output_format_params = {verbose, debug, evals, atomss, ...}, |
145 output_format_params = {verbose, debug, evals, atomss, ...}, |
144 optimization_params = {specialize, ...}, |
146 optimization_params = {specialize, ...}, |
145 timeout_params = {timeout, wf_timeout}}) |
147 timeout_params = {timeout, wf_timeout}}) |
146 mode i all_assms subgoal = |
148 mode i all_assms subgoal = |
155 fun print_d f = if debug then writeln (f ()) else (); |
157 fun print_d f = if debug then writeln (f ()) else (); |
156 |
158 |
157 val das_wort_Model = if falsify then "Countermodel" else "Model"; |
159 val das_wort_Model = if falsify then "Countermodel" else "Model"; |
158 val das_wort_model = if falsify then "countermodel" else "model"; |
160 val das_wort_model = if falsify then "countermodel" else "model"; |
159 |
161 |
160 val tool_params = {overlord = overlord, debug = debug, specialize = specialize, |
162 val tool_params = |
161 timeout = timeout}; |
163 {solvers = solvers, overlord = overlord, debug = debug, specialize = specialize, |
|
164 timeout = timeout}; |
162 |
165 |
163 fun run () = |
166 fun run () = |
164 let |
167 let |
165 val outcome as (outcome_code, _) = |
168 val outcome as (outcome_code, _) = |
166 let |
169 let |