| 1 | % (c) 2021-2025 Lehrstuhl fuer Softwaretechnik und Programmiersprachen, | |
| 2 | % Heinrich Heine Universitaet Duesseldorf | |
| 3 | % This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html) | |
| 4 | ||
| 5 | :- module(pathes_extensions_db,[ | |
| 6 | prob_extension/1, | |
| 7 | compile_time_unavailable_extension/2, | |
| 8 | module_path_implements_extension/3, | |
| 9 | silently_fail_unavailable_predicate/3, | |
| 10 | lib_component_implements_extension/4, | |
| 11 | lib_file_suffix/3, | |
| 12 | load_spec_file_requires_extension/2, | |
| 13 | preference_value_requires_extension/3, | |
| 14 | probcli_command_requires_extension/2, | |
| 15 | external_function_requires_extension/2 | |
| 16 | ]). | |
| 17 | ||
| 18 | ||
| 19 | % ------------------------------------ | |
| 20 | % PROB EXTENSIONS DECLARATION DATABASE | |
| 21 | % ------------------------------------ | |
| 22 | ||
| 23 | % keep track of which optional extensions of ProB are available | |
| 24 | % and patch use_modules to unloaded extensions | |
| 25 | % Note: only use_modules with explicit import lists are patched ! | |
| 26 | ||
| 27 | % This module is potentially loaded very early (from the pathes module). | |
| 28 | % To avoid cyclic dependency problems, do not import any other ProB modules | |
| 29 | % (or at least be very careful). | |
| 30 | ||
| 31 | % PROB-CORE EXTENSIONS: | |
| 32 | % --------------------- | |
| 33 | ||
| 34 | :- load_files(library(system), [when(compile_time), imports([environ/2])]). | |
| 35 | ||
| 36 | % TO DO: provide a way to choose which extensions are available | |
| 37 | % these are the extensions that are present in the prob-core: | |
| 38 | core_extension(counter_extension). % one can use Prolog version by setting prob_c_counter to false, but counter_extensions is available in both cases | |
| 39 | ||
| 40 | core_extension(core). | |
| 41 | core_extension(dot_extension). % do we need this in core? | |
| 42 | core_extension(plspec_extension). | |
| 43 | ||
| 44 | % compile_time_unavailable_extension cannot guarantee that an extension will be available! | |
| 45 | % It can only report that an extension will definitely be unavailable. | |
| 46 | % If this predicate fails, it means that the extension was compiled in, | |
| 47 | % but may still be unavailable at runtime for other reasons, | |
| 48 | % which can be checked using unavailable_extension/2 from the pathes_lib module. | |
| 49 | ||
| 50 | :- if(environ(prob_core_only,true)). | |
| 51 | compile_time_unavailable_extension(E, 'non-core extension disabled using prob_core_only=true') :- \+ core_extension(E). | |
| 52 | :- endif. | |
| 53 | ||
| 54 | :- if(environ(prob_myheap,false)). % otherwise we use Prolog version | |
| 55 | compile_time_unavailable_extension(myheap_extension, 'manually disabled using prob_myheap=false'). | |
| 56 | :- endif. | |
| 57 | ||
| 58 | :- if(environ(disable_chr,true)). % otherwise we use Prolog version | |
| 59 | compile_time_unavailable_extension(chr_extension, 'manually disabled using disable_chr=true'). | |
| 60 | :- endif. | |
| 61 | ||
| 62 | compile_time_unavailable_extension(_, _) :- fail. | |
| 63 | ||
| 64 | prob_extension(alloy2b_extension). | |
| 65 | prob_extension(atelierb_extension). | |
| 66 | prob_extension(avl_ugraphs_extension). | |
| 67 | prob_extension(bliss_extension). | |
| 68 | prob_extension(bvisual2_extension). | |
| 69 | prob_extension(cbc_extension). | |
| 70 | prob_extension(chr_extension). | |
| 71 | prob_extension(counter_extension). | |
| 72 | prob_extension(core). | |
| 73 | prob_extension(cse_extension). | |
| 74 | prob_extension(cspm_extension). | |
| 75 | prob_extension(coverage_extension). | |
| 76 | prob_extension(disprover_extension). | |
| 77 | prob_extension(dot_extension). | |
| 78 | prob_extension(cdclt_extension). | |
| 79 | prob_extension(external_svg_extension). | |
| 80 | prob_extension(external_reals_extension). | |
| 81 | prob_extension(fuzz_extension). | |
| 82 | prob_extension(fuzzing_extension). | |
| 83 | prob_extension(graphical_state_viewer_extension). | |
| 84 | prob_extension(hit_profiler_extension). | |
| 85 | prob_extension(json_extension). | |
| 86 | prob_extension(kodkod_extension). | |
| 87 | prob_extension(latex_extension). | |
| 88 | prob_extension(ltl_extension). | |
| 89 | prob_extension(ltl2ba_extension). | |
| 90 | prob_extension(ltsmin_extension). | |
| 91 | prob_extension(mcdc_coverage_extension). | |
| 92 | prob_extension(meta_interface_extension). | |
| 93 | prob_extension(myheap_extension). | |
| 94 | prob_extension(nauty_extension). | |
| 95 | prob_extension(opcache_extension). | |
| 96 | prob_extension(optimizing_solver_extension). | |
| 97 | prob_extension(pge_extension). | |
| 98 | prob_extension(plspec_extension). | |
| 99 | prob_extension(pltables_extension). | |
| 100 | prob_extension(por_extension). | |
| 101 | prob_extension(predicate_debugger_extension). | |
| 102 | prob_extension(probhash_extension). | |
| 103 | prob_extension(random_permutations). | |
| 104 | prob_extension(refinement_extension). | |
| 105 | prob_extension(regexp_extension). | |
| 106 | prob_extension(rulesdsl_extension). | |
| 107 | prob_extension(satsolver_extension). | |
| 108 | prob_extension(setlog_extension). | |
| 109 | prob_extension(smt_extension). | |
| 110 | prob_extension(smtlib_extension). | |
| 111 | prob_extension(state_graph_extension). | |
| 112 | prob_extension(symbolic_model_checker_extension). | |
| 113 | prob_extension(symmetry_extension). | |
| 114 | prob_extension(synthesis_extension). | |
| 115 | prob_extension(table_tools_extension). | |
| 116 | prob_extension(tcltk_extension). | |
| 117 | prob_extension(timer_extension). | |
| 118 | prob_extension(tla2b_extension). | |
| 119 | prob_extension(tlc4b_extension). | |
| 120 | prob_extension(unsat_core_extension). | |
| 121 | prob_extension(visb_extension). | |
| 122 | prob_extension(wd_extension). | |
| 123 | prob_extension(wp_ba_extension). | |
| 124 | prob_extension(xml2b_extension). | |
| 125 | prob_extension(zmq_extension). | |
| 126 | ||
| 127 | ||
| 128 | ||
| 129 | % PATHS/MODULES for EXTENSIONS: | |
| 130 | % ----------------------------- | |
| 131 | ||
| 132 | % module_path_implements_extension (PATH, ModuleName, ExtensionName) | |
| 133 | ||
| 134 | % TO DO: complete lists | |
| 135 | module_path_implements_extension(chrsrc(M),M,chr_extension). | |
| 136 | module_path_implements_extension(cbcsrc(M),M,cbc_extension). | |
| 137 | module_path_implements_extension(covsrc(hit_profiler),hit_profiler,hit_profiler_extension). | |
| 138 | module_path_implements_extension(disproversrc(M),M,disprover_extension). | |
| 139 | module_path_implements_extension(dotsrc(M),M,dot_extension). | |
| 140 | module_path_implements_extension(cdclt_solver(M),M,cdclt_extension). | |
| 141 | module_path_implements_extension(extrasrc(atelierb_provers_interface),atelierb_provers_interface,atelierb_extension). | |
| 142 | module_path_implements_extension(extrasrc(avl_ugraphs),avl_ugraphs,avl_ugraphs_extension). | |
| 143 | module_path_implements_extension(extrasrc(b_expression_sharing),b_expression_sharing,cse_extension). | |
| 144 | module_path_implements_extension(extrasrc(b_operation_cache),b_operation_cache,opcache_extension). | |
| 145 | module_path_implements_extension(extrasrc(b2setlog),b2setlog,setlog_extension). | |
| 146 | module_path_implements_extension(extrasrc(before_after_predicates),before_after_predicates,wp_ba_extension). | |
| 147 | module_path_implements_extension(extrasrc(bvisual2),bvisual2,bvisual2_extension). | |
| 148 | module_path_implements_extension(extrasrc(coverage_statistics),coverage_statistics,coverage_extension). | |
| 149 | module_path_implements_extension(extrasrc(external_functions_svg),external_functions_svg,external_svg_extension). | |
| 150 | module_path_implements_extension(extrasrc(external_functions_reals),external_functions_svg,external_reals_extension). | |
| 151 | module_path_implements_extension(extrasrc(graphical_state_viewer_images),graphical_state_viewer_images,graphical_state_viewer_extension). | |
| 152 | module_path_implements_extension(extrasrc(json_parser),json_parser,json_extension). | |
| 153 | module_path_implements_extension(extrasrc(latex_processor),latex_processor,latex_extension). | |
| 154 | module_path_implements_extension(extrasrc(meta_interface),meta_interface,meta_interface_extension). | |
| 155 | module_path_implements_extension(extrasrc(mcdc_coverage),mcdc_coverage,mcdc_coverage_extension). | |
| 156 | module_path_implements_extension(extrasrc(optimizing_solver),optimizing_solver,optimizing_solver_extension). | |
| 157 | module_path_implements_extension(extrasrc(predicate_debugger),predicate_debugger,predicate_debugger_extension). | |
| 158 | module_path_implements_extension(extrasrc(refinement_checker),refinement_checker,refinement_extension). | |
| 159 | module_path_implements_extension(extrasrc(state_graph_canon),state_graph_canon,state_graph_extension). | |
| 160 | module_path_implements_extension(extrasrc(unsat_cores),unsat_cores,unsat_core_extension). | |
| 161 | module_path_implements_extension(extrasrc(weakest_preconditions),weakest_preconditions,wp_ba_extension). | |
| 162 | module_path_implements_extension(extrasrc(xml2b),xml2b,xml2b_extension). | |
| 163 | module_path_implements_extension(extrasrc(table_tools),table_tools,table_tools_extension). | |
| 164 | module_path_implements_extension(kodkodsrc(M),M,kodkod_extension). | |
| 165 | module_path_implements_extension(pltablesrc(M),M,pltables_extension). | |
| 166 | module_path_implements_extension(probcspsrc(M),M,cspm_extension). | |
| 167 | module_path_implements_extension(probltlsrc(M),M,ltl_extension). | |
| 168 | module_path_implements_extension(probltlsrc(ltl_safety),ltl_safety,ltl2ba_extension). | |
| 169 | module_path_implements_extension(probpgesrc(M),M,pge_extension). %pge_algo:do_not_evaluate_guard/0 | |
| 170 | module_path_implements_extension(probporsrc(M),M,por_extension). | |
| 171 | module_path_implements_extension(probsrc('alloy2b/alloy2b'),alloy2b,alloy2b_extension). | |
| 172 | module_path_implements_extension(prozsrc(M),M,fuzz_extension). | |
| 173 | module_path_implements_extension(rulesdslsrc(M),M,rulesdsl_extension). | |
| 174 | module_path_implements_extension(smt_solvers_interface(M),M,smt_extension). | |
| 175 | module_path_implements_extension(smtlib_solver(M),M,smtlib_extension). | |
| 176 | module_path_implements_extension(symsrc(M),M,symmetry_extension). | |
| 177 | module_path_implements_extension(symbolic_model_checker(M),M,symbolic_model_checker_extension). | |
| 178 | module_path_implements_extension(synthesis(M),N,synthesis_extension) :- (get_module_name(M,N) -> true ; M=N). | |
| 179 | module_path_implements_extension(tcltkuisrc(M),M,tcltk_extension). | |
| 180 | module_path_implements_extension(visbsrc(M),M,visb_extension). | |
| 181 | module_path_implements_extension(wdsrc(M),M,wd_extension). | |
| 182 | ||
| 183 | % modules/files in extension (usually C/C++ related extensions): | |
| 184 | module_path_implements_extension(extension('bliss/bliss_interface'),bliss_interface,bliss_extension). | |
| 185 | module_path_implements_extension(extension('counter/counter'),counter,counter_extension). | |
| 186 | module_path_implements_extension(extension('cvc4interface/cvc4interface'),cvc4interface,smt_extension). | |
| 187 | module_path_implements_extension(extension('ltl2ba/ltl2ba'),ltl2ba,ltl2ba_extension). | |
| 188 | module_path_implements_extension(extension('ltlc/ltlc'),ltlc,ltl_extension). | |
| 189 | module_path_implements_extension(extension('ltsmin/ltsmin_trace'),ltsmin_trace,ltsmin_extension). | |
| 190 | module_path_implements_extension(extension('ltsmin/ltsmin'),ltsmin,ltsmin_extension). | |
| 191 | module_path_implements_extension(extension('myheap/myheap'),myheap,myheap_extension). | |
| 192 | module_path_implements_extension(extension('nauty/graphiso'),graphiso,nauty_extension). | |
| 193 | module_path_implements_extension(extension('plspec/plspec/plspec_core'),plspec_core,plspec_extension). | |
| 194 | module_path_implements_extension(extension('plspec/plspec/prettyprinter'),prettyprinter,plspec_extension). | |
| 195 | module_path_implements_extension(extension('probhash/probhash'),probhash,probhash_extension). | |
| 196 | module_path_implements_extension(extension('prolog_fuzzer/fuzzing'),fuzzing,fuzzing_extension). | |
| 197 | module_path_implements_extension(extension('random_permutations/random_permutations'),random_permutations,random_permutations). | |
| 198 | module_path_implements_extension(extension('regexp/regexp'),regexp,regexp_extension). | |
| 199 | module_path_implements_extension(extension('satsolver/satsolver'),satsolver,satsolver_extension). | |
| 200 | module_path_implements_extension(extension('timer/timer'),timer,timer_extension). | |
| 201 | module_path_implements_extension(extension('z3interface/z3interface'),z3interface,smt_extension). | |
| 202 | module_path_implements_extension(extension('zmq/master/master'),master,zmq_extension). | |
| 203 | module_path_implements_extension(extension('zmq/worker/worker'),worker,zmq_extension). | |
| 204 | module_path_implements_extension(extension('zmq/zmq'),zmq,zmq_extension). | |
| 205 | ||
| 206 | ||
| 207 | % TO DO: deconstruct programmatically | |
| 208 | get_module_name('deep_learning/ground_truth',ground_truth). | |
| 209 | get_module_name('deep_learning/b_machine_identifier_normalization',b_machine_identifier_normalization). | |
| 210 | get_module_name('deep_learning/predicate_data_generator',predicate_data_generator). | |
| 211 | get_module_name('deep_learning/operation_data_generator',operation_data_generator). | |
| 212 | ||
| 213 | % declare predicates that should silently fail | |
| 214 | % when the corresponding extension is not available | |
| 215 | silently_fail_unavailable_predicate(is_dot_command,1,meta_interface_extension). | |
| 216 | silently_fail_unavailable_predicate(is_dot_command_for_expr,1,meta_interface_extension). | |
| 217 | silently_fail_unavailable_predicate(is_plantuml_command,1,meta_interface_extension). | |
| 218 | silently_fail_unavailable_predicate(is_plantuml_command_for_expr,1,meta_interface_extension). | |
| 219 | silently_fail_unavailable_predicate(is_table_command,1,meta_interface_extension). | |
| 220 | silently_fail_unavailable_predicate(is_table_command_for_expr,1,meta_interface_extension). | |
| 221 | silently_fail_unavailable_predicate(get_profile_stats,2,hit_profiler_extension). | |
| 222 | silently_fail_unavailable_predicate(retract_profile_stats,2,hit_profiler_extension). | |
| 223 | ||
| 224 | ||
| 225 | % LIB FILES for EXTENSIONS: | |
| 226 | % ------------------------- | |
| 227 | ||
| 228 | % Required components: | |
| 229 | lib_component_implements_extension(java_parser,jar,'probcliparser',core). | |
| 230 | lib_component_implements_extension(statespace_queue,bundle,'myheap',core). % but fallback exists | |
| 231 | lib_component_implements_extension(user_signal,bundle,'user_signal',core). % required for ProB2 | |
| 232 | ||
| 233 | lib_component_implements_extension(kodkod,jar,'probkodkod',kodkod_extension). | |
| 234 | lib_component_implements_extension(tla2b,jar,'TLA2B',tla2b_extension). | |
| 235 | lib_component_implements_extension(tlc4b,jar,'TLC4B',tlc4b_extension). | |
| 236 | lib_component_implements_extension(alloy2b,jar,'alloy2b',alloy2b_extension). | |
| 237 | lib_component_implements_extension(ltl2ba,bundle,'ltl2ba',ltl2ba_extension). | |
| 238 | lib_component_implements_extension(ltlc,bundle,'ltlc',ltl_extension). | |
| 239 | lib_component_implements_extension(counter,bundle,'counter',counter_extension). | |
| 240 | lib_component_implements_extension(ltsmin_bundle,bundle,'ltsmin',ltsmin_extension). | |
| 241 | lib_component_implements_extension(ltsmin_sequential,executable,'prob2lts-seq',ltsmin_extension). | |
| 242 | lib_component_implements_extension(ltsmin_symbolic,executable,'prob2lts-sym',ltsmin_extension). | |
| 243 | lib_component_implements_extension(ltsmin_printtrace,executable,'ltsmin-printtrace',ltsmin_extension). | |
| 244 | lib_component_implements_extension(csp_parser,executable,'cspmf',cspm_extension). | |
| 245 | lib_component_implements_extension(fuzz_parser,executable,'fuzz',fuzz_extension). | |
| 246 | lib_component_implements_extension(fuzz_lib,file,'fuzzlib',fuzz_extension). | |
| 247 | lib_component_implements_extension(nauty,bundle,'graphiso',nauty_extension). | |
| 248 | lib_component_implements_extension(regexp,bundle,'regexp',regexp_extension). | |
| 249 | lib_component_implements_extension(random_permutations,bundle,'random_permutations',random_permutations). | |
| 250 | lib_component_implements_extension(setlog,qlf,'setlog-cli',setlog_extension). | |
| 251 | lib_component_implements_extension(z3,bundle,'z3interface',smt_extension). | |
| 252 | lib_component_implements_extension(zmq,bundle,'zmq',zmq_extension). | |
| 253 | ||
| 254 | lib_file_suffix(bundle,darwin,'.bundle'). | |
| 255 | lib_file_suffix(bundle,windows,'.dll'). | |
| 256 | lib_file_suffix(bundle,linux,'.so'). | |
| 257 | lib_file_suffix(executable,windows,'.exe'). | |
| 258 | lib_file_suffix(executable,P,'') :- P \= windows. | |
| 259 | lib_file_suffix(file,_,''). | |
| 260 | lib_file_suffix(jar,_,'.jar'). | |
| 261 | lib_file_suffix(qlf,_,'.qlf'). % SWI compiled Prolog program | |
| 262 | ||
| 263 | ||
| 264 | % FILENAME SUFFIXES (FILE EXTENSIONS): | |
| 265 | % ----------------- | |
| 266 | ||
| 267 | % see second argument of known_spec_file_extension | |
| 268 | load_spec_file_requires_extension(alloy,alloy2b_extension). | |
| 269 | load_spec_file_requires_extension(csp,cspm_extension). | |
| 270 | load_spec_file_requires_extension(smt,smtlib_extension). | |
| 271 | load_spec_file_requires_extension(tla,tla2b_extension). | |
| 272 | load_spec_file_requires_extension(z,fuzz_extension). | |
| 273 | ||
| 274 | ||
| 275 | % PREFERENCE VALUES: | |
| 276 | % ----------------- | |
| 277 | ||
| 278 | preference_value_requires_extension(symmetry_mode,hash,symmetry_extension). | |
| 279 | preference_value_requires_extension(symmetry_mode,flood,symmetry_extension). | |
| 280 | preference_value_requires_extension(symmetry_mode,nauty,symmetry_extension). | |
| 281 | preference_value_requires_extension(symmetry_mode,nauty,nauty_extension). | |
| 282 | ||
| 283 | %preference_value_requires_extension(use_chr_solver,true,chr_extension). | |
| 284 | preference_value_requires_extension(use_common_subexpression_elimination,true,cse_extension). | |
| 285 | preference_value_requires_extension(smt_supported_interpreter,true,smt_extension). | |
| 286 | ||
| 287 | preference_value_requires_extension(use_solver_on_load,kodkod,kodkod_extension). | |
| 288 | preference_value_requires_extension(use_solver_on_load,z3,smt_extension). | |
| 289 | preference_value_requires_extension(use_solver_on_load,z3cns,smt_extension). | |
| 290 | preference_value_requires_extension(use_solver_on_load,z3axm,smt_extension). | |
| 291 | preference_value_requires_extension(use_solver_on_load,sat,satsolver_extension). | |
| 292 | preference_value_requires_extension(use_solver_on_load,cdclt,cdclt_extension). | |
| 293 | ||
| 294 | preference_value_requires_extension(pge,Val,pge_extension) :- dif(Val,off). | |
| 295 | preference_value_requires_extension(por,Val,por_extension) :- dif(Val,off). | |
| 296 | preference_value_requires_extension(use_safety_ltl_model_checker,true,ltl2ba_extension). % ltl.pl performs a separate check is_ltl2ba_tool_installed before checking for the preference | |
| 297 | preference_value_requires_extension(randomise_enumeration_order,true,random_permutations). | |
| 298 | ||
| 299 | preference_value_requires_extension(use_cbc_analysis,true,cbc_extension). | |
| 300 | ||
| 301 | preference_value_requires_extension(try_atb_provers,true,atelierb_extension). | |
| 302 | ||
| 303 | preference_value_requires_extension(try_operation_reuse,Val,opcache_extension) :- Val \= false. | |
| 304 | ||
| 305 | preference_value_requires_extension(use_chr_solver,true,chr_extension). | |
| 306 | ||
| 307 | % PROBCLI COMMANDS: | |
| 308 | % ----------------- | |
| 309 | ||
| 310 | % which probcli commands requires which extension | |
| 311 | probcli_command_requires_extension(ltl_assertions,ltl_extension). | |
| 312 | probcli_command_requires_extension(ltl_formula_model_check(_,_),ltl_extension). | |
| 313 | probcli_command_requires_extension(ltl_file(_),ltl_extension). | |
| 314 | ||
| 315 | probcli_command_requires_extension(dot_command(_,_),dot_extension). | |
| 316 | probcli_command_requires_extension(dot_command_for_expr(_,_,_,_),dot_extension). | |
| 317 | probcli_command_requires_extension(csv_table_command(_,_,_,_),meta_interface_extension). | |
| 318 | ||
| 319 | probcli_command_requires_extension(process_latex_file(_,_),latex_extension). | |
| 320 | ||
| 321 | probcli_command_requires_extension(ltsmin2(_), ltsmin_extension). | |
| 322 | probcli_command_requires_extension(ltsmin_ltl_output(_), ltsmin_extension). | |
| 323 | probcli_command_requires_extension(ltsmin_option(_),ltsmin_extension). | |
| 324 | ||
| 325 | probcli_command_requires_extension(rule_report(_),rulesdsl_extension). | |
| 326 | probcli_command_requires_extension(visb_history(_,_,_),visb_extension). | |
| 327 | probcli_command_requires_extension(cli_start_mc_with_tlc,tlc4b_extension). | |
| 328 | ||
| 329 | probcli_command_requires_extension(cli_check_disprover_result(_),disprover_extension). | |
| 330 | ||
| 331 | probcli_command_requires_extension(kodkod_comparision(_),kodkod_extension). | |
| 332 | probcli_command_requires_extension(kodkod_performance(_),kodkod_extension). | |
| 333 | ||
| 334 | probcli_command_requires_extension(zmq_master(_),zmq_extension). | |
| 335 | probcli_command_requires_extension(zmq_worker(_),zmq_extension). | |
| 336 | probcli_command_requires_extension(zmq_assertion(_),zmq_extension). | |
| 337 | ||
| 338 | probcli_command_requires_extension(csp_main(_),cspm_extension). | |
| 339 | probcli_command_requires_extension(csp_in_situ_refinement_check(_,_,_),cspm_extension). | |
| 340 | probcli_command_requires_extension(csp_checkAssertion(_,_,_),cspm_extension). | |
| 341 | probcli_command_requires_extension(eval_csp_expression(_),cspm_extension). | |
| 342 | probcli_command_requires_extension(csp_get_assertions,cspm_extension). | |
| 343 | probcli_command_requires_extension(csp_translate_to_file(_),cspm_extension). | |
| 344 | probcli_command_requires_extension(add_csp_guide(_),cspm_extension). | |
| 345 | ||
| 346 | probcli_command_requires_extension(cli_wd_check(_,_),wd_extension). | |
| 347 | ||
| 348 | probcli_command_requires_extension(cli_symbolic_model_check(_),symbolic_model_checker_extension). | |
| 349 | ||
| 350 | probcli_command_requires_extension(cli_start_sym_mc_with_lts(_),ltsmin_extension). | |
| 351 | probcli_command_requires_extension(ltsmin,ltsmin_extension). | |
| 352 | ||
| 353 | probcli_command_requires_extension(get_min_max_coverage(_),coverage_extension). | |
| 354 | probcli_command_requires_extension(get_coverage_information(_),coverage_extension). | |
| 355 | probcli_command_requires_extension(coverage(_,_,ShowEnabledInfo),coverage_extension) :- | |
| 356 | ShowEnabledInfo \== just_check_stats, ShowEnabledInfo \== just_summary. | |
| 357 | ||
| 358 | probcli_command_requires_extension(refinement_check(_,_,_),refinement_extension). | |
| 359 | probcli_command_requires_extension(csp_in_situ_refinement_check(_,_),refinement_extension). | |
| 360 | probcli_command_requires_extension(csp_checkAssertion(_,_),refinement_extension). | |
| 361 | ||
| 362 | probcli_command_requires_extension(all_deadlocking_paths(_),cbc_extension). | |
| 363 | probcli_command_requires_extension(cbc_tests(_),cbc_extension). | |
| 364 | probcli_command_requires_extension(enabling_analysis_csv(_),cbc_extension). | |
| 365 | probcli_command_requires_extension(feasibility_analysis_csv(_),cbc_extension). | |
| 366 | probcli_command_requires_extension(test_description(_),cbc_extension). | |
| 367 | probcli_command_requires_extension(cbc_sequence(_,_,_),cbc_extension). | |
| 368 | ||
| 369 | ||
| 370 | probcli_command_requires_extension(trace_check(json,_,_),json_extension). | |
| 371 | probcli_command_requires_extension(trace_check('JSON',_,_),json_extension). | |
| 372 | ||
| 373 | probcli_command_requires_extension(cbc_option(unsat_core),unsat_core_extension). | |
| 374 | probcli_command_requires_extension(disprover_options(Opts),unsat_core_extension) :- | |
| 375 | member(disprover_option(unsat_core),Opts). | |
| 376 | ||
| 377 | probcli_command_requires_extension(dot_command(_,_),meta_interface_extension). | |
| 378 | probcli_command_requires_extension(dot_command_for_expr(_,_,_,_),meta_interface_extension). | |
| 379 | ||
| 380 | probcli_command_requires_extension(check_statespace_hash(_,_),probhash_extension). | |
| 381 | ||
| 382 | probcli_command_requires_extension(cli_print_statistics(hit_profile),hit_profiler_extension). % in covsrc | |
| 383 | ||
| 384 | ||
| 385 | % probcli_command_requires_extension(cli_check_properties(_),predicate_debugger_extension). % only used when PROPERTIES inconsistent; hence we just leave comment here | |
| 386 | ||
| 387 | ||
| 388 | % EXTERNAL FUNCTIONS: | |
| 389 | % ------------------- | |
| 390 | external_function_requires_extension('KODKOD',kodkod_extension). | |
| 391 | external_function_requires_extension('KODKOD_SOLVE',kodkod_extension). | |
| 392 | ||
| 393 | external_function_requires_extension('REGEX_MATCH',regexp_extension). | |
| 394 | external_function_requires_extension('REGEX_IMATCH',regexp_extension). | |
| 395 | external_function_requires_extension('IS_REGEX',regexp_extension). | |
| 396 | external_function_requires_extension('REGEX_REPLACE',regexp_extension). | |
| 397 | external_function_requires_extension('REGEX_IREPLACE',regexp_extension). | |
| 398 | external_function_requires_extension('REGEX_SEARCH_STR',regexp_extension). | |
| 399 | external_function_requires_extension('REGEX_ISEARCH_STR',regexp_extension). | |
| 400 | external_function_requires_extension('REGEX_SEARCH',regexp_extension). | |
| 401 | external_function_requires_extension('REGEX_ISEARCH',regexp_extension). | |
| 402 | external_function_requires_extension('REGEX_SEARCH_ALL',regexp_extension). | |
| 403 | external_function_requires_extension('REGEX_ISEARCH_ALL',regexp_extension). | |
| 404 | ||
| 405 | ||
| 406 | external_function_requires_extension('MACHINE_INFO',probhash_extension). | |
| 407 | external_function_requires_extension('SHA_HASH',probhash_extension). | |
| 408 | external_function_requires_extension('SHA_HASH_HEX',probhash_extension). | |
| 409 | external_function_requires_extension('SHA_HASH_FILE_HEX',probhash_extension). | |
| 410 | ||
| 411 | external_function_requires_extension('SATSOLVER_SOLVE',satsolver_extension). | |
| 412 | ||
| 413 | external_function_requires_extension('READ_XML',xml2b_extension). | |
| 414 | ||
| 415 | external_function_requires_extension(svg_points, external_svg_extension). | |
| 416 | external_function_requires_extension(svg_train, external_svg_extension). | |
| 417 | external_function_requires_extension(svg_axis, external_svg_extension). | |
| 418 | external_function_requires_extension(svg_set_polygon,external_svg_extension). | |
| 419 | external_function_requires_extension(svg_dasharray_for_intervals,external_svg_extension). | |
| 420 | ||
| 421 | ||
| 422 | external_function_requires_extension('STRING_TO_REAL',external_reals_extension). | |
| 423 | external_function_requires_extension('RADD',external_reals_extension). | |
| 424 | external_function_requires_extension('RSUB',external_reals_extension). | |
| 425 | external_function_requires_extension('RMUL',external_reals_extension). | |
| 426 | external_function_requires_extension('RDIV',external_reals_extension). | |
| 427 | %TODO: declare all exported functions of external_functions_reals |