| 1 | % (c) 2014-2019 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(disprover_test_runner, [test_repl/0, run_disprover_on_all_pos/1, load_po_file/1, | |
| 6 | set_disprover_timeout/1, reset_disprover_timeout/0, | |
| 7 | set_disprover_options/1, | |
| 8 | print_disprover_stats/0]). | |
| 9 | ||
| 10 | :- use_module(prob_startup, [startup_prob/0]). | |
| 11 | %:- use_module(pathes,[set_search_pathes/0]). % imported first to set_compile_time_search_pathes, now loaded by prob_startup | |
| 12 | ||
| 13 | portray_message(informational, _). | |
| 14 | ||
| 15 | :- use_module(module_information). | |
| 16 | :- module_info(group,cbc). | |
| 17 | :- module_info(description,'Rodin Prover / Disprover'). | |
| 18 | ||
| 19 | ||
| 20 | :- use_module(eclipse_interface). | |
| 21 | :- use_module(prob2_interface). | |
| 22 | :- use_module(disprover). | |
| 23 | :- use_module(error_manager). | |
| 24 | :- use_module(tools). | |
| 25 | :- use_module(solver_interface). | |
| 26 | :- use_module(debug). | |
| 27 | :- use_module(preferences). | |
| 28 | ||
| 29 | :- use_module(library(system)). | |
| 30 | :- use_module(library(lists)). | |
| 31 | ||
| 32 | ||
| 33 | ||
| 34 | %:- use_module(eventhandling, [announce_event/1]). | |
| 35 | ||
| 36 | test_repl :- | |
| 37 | startup_prob, | |
| 38 | init_eclipse_preferences, | |
| 39 | disprover_load_at_repl_startup, | |
| 40 | disprover_help, | |
| 41 | disprover_repl_loop. | |
| 42 | ||
| 43 | ||
| 44 | disprover_repl_loop :- print('DISPROVER ==> '),safe_read(T), | |
| 45 | (quit_command(T) -> get_total_number_of_errors(X), format('~nTotal number of errors: ~w~n~n',[X]) | |
| 46 | ; test_eval(T) -> disprover_repl_loop | |
| 47 | ; print('Command failed !!'),nl, disprover_repl_loop). | |
| 48 | ||
| 49 | safe_read(T) :- on_exception(E,read(T), | |
| 50 | ( format('Exception while reading user input: ~w ~n',[E]), T=help)). | |
| 51 | ||
| 52 | disprover_help :- | |
| 53 | print('Available commands: run, run(PO), timeout(T), stats, list, q, x, FILE, v, vv, write(S,FILE), '),nl, | |
| 54 | print(' trace_info, observe, debug, kodkod,core, cse, chr_off,smt_off, ...'),nl. | |
| 55 | ||
| 56 | :- meta_predicate wall(0). | |
| 57 | wall(Call) :- | |
| 58 | statistics(walltime,[Start,_]), | |
| 59 | call(Call), | |
| 60 | statistics(walltime,[Stop,_]), WT is Stop-Start, | |
| 61 | format('Walltime: ~w ms~n',[WT]). | |
| 62 | ||
| 63 | quit_command(q). | |
| 64 | quit_command(quit). | |
| 65 | quit_command(halt). | |
| 66 | ||
| 67 | test_eval(run) :- !,wall(run). | |
| 68 | test_eval(run(PO)) :- !,disprover_timeout(TO), wall(run_on_po(PO,TO)). | |
| 69 | test_eval(timeout(T)) :- !, set_disprover_timeout(T). | |
| 70 | test_eval(time_out(T)) :- !, set_disprover_timeout(T). | |
| 71 | test_eval(stats) :- !,print_disprover_stats. | |
| 72 | test_eval(x) :- !,halt. | |
| 73 | test_eval(list) :- !,list(_). | |
| 74 | test_eval(lup) :- !,list(unknown). | |
| 75 | test_eval(lf) :- !,list(false). | |
| 76 | test_eval(help) :- !,disprover_help. | |
| 77 | test_eval(h) :- !,disprover_help. | |
| 78 | test_eval(v) :- !,tcltk_turn_debugging_on(19). | |
| 79 | test_eval(vv) :- !,tcltk_turn_debugging_on(4). | |
| 80 | test_eval(load(FILE)) :- !,load_po_file(FILE). | |
| 81 | test_eval(wp) :- !, write_pos(true,_). | |
| 82 | test_eval(write(Status)) :- !, write_pos(Status,_). | |
| 83 | test_eval(wc) :- !, write_pos(true,contradiction_in_hypotheses). | |
| 84 | test_eval(wp(FILE)) :- !, tell(FILE), write_pos(true,_), told. | |
| 85 | test_eval(write(Status,FILE)) :- !, tell(FILE), write_pos(Status,_), told. | |
| 86 | test_eval(cse) :- !,enable_cse. | |
| 87 | test_eval(chr_off) :- !,disable_chr. | |
| 88 | test_eval(smt_off) :- !,disable_smt. | |
| 89 | test_eval(core) :- !,add_opts([disprover_option(unsat_core),unsat_core_algorithm/linear]). | |
| 90 | test_eval(corem) :- !,add_opts([disprover_option(unsat_core),disprover_option(unsat_core_as_machine),unsat_core_algorithm/linear]). | |
| 91 | test_eval(coredc) :- !,add_opts([disprover_option(unsat_core)]). | |
| 92 | test_eval(observe) :- !,add_opts([disprover_option(observe_state)]). | |
| 93 | test_eval(pob) :- !,add_opts([disprover_option(show_po_as_machine)]). | |
| 94 | test_eval(kodkod) :- !,enable_kodkod. | |
| 95 | test_eval(abort) :- !, print('TRY FIND ABORT true'),nl,set_preference(find_abort_values,true). | |
| 96 | test_eval(abortfull) :- !, print('TRY FIND ABORT full'),nl,set_preference(find_abort_values,full). | |
| 97 | test_eval(nocounter) :- print('ENUMERATE_INFINITE_TYPES=FALSE'),nl,!, set_preference(allow_enumeration_of_infinite_types,false). | |
| 98 | test_eval(trace_info) :- !, print('TRACE_INFO true'),nl,set_preference(provide_trace_information,true). | |
| 99 | test_eval(trace) :- !, print('Tracing upon error'),nl,set_preference(trace_upon_error,true). | |
| 100 | test_eval(debug) :- !, | |
| 101 | on_exception(error(existence_error(_,_),_),debug, print('CAN ONLY BE USED WHEN RUNNING PROB FROM SOURCE')). | |
| 102 | test_eval(eval(Atom)) :- !, | |
| 103 | eval_strings:eval_string(Atom,Result), | |
| 104 | format('Evaluation result: ~w~n',[Result]). | |
| 105 | test_eval(dir) :- | |
| 106 | loaded_po_file(File),!, | |
| 107 | directory_listing_for_file(File). | |
| 108 | test_eval(PO) :- disprover_po(PO,_,_,_,_,_),!, | |
| 109 | test_eval(run(PO)). | |
| 110 | test_eval(Filename) :- format('Trying to consult file: ~w~n',[Filename]), | |
| 111 | load_po_file(Filename), print_disprover_stats,!. | |
| 112 | test_eval(Cmd) :- format('Could not executed command: ~w~n',[Cmd]). | |
| 113 | ||
| 114 | ||
| 115 | :- use_module(library(file_systems)). | |
| 116 | % list the directory in which a file is in and allow use to load a po file in that directory | |
| 117 | directory_listing_for_file(File) :- | |
| 118 | get_parent_directory(File,Dir), | |
| 119 | findall(FF,(file_member_of_directory(Dir,F,FF),get_filename_extension(F,'pl')),List), | |
| 120 | sort(List,SList), | |
| 121 | prdir(SList), | |
| 122 | write('==Nr==>'), read(Nr), | |
| 123 | ((number(Nr),nth1(Nr,SList,NewFile)) -> load_po_file(NewFile) ; print('No file loaded'),nl). | |
| 124 | prdir(List) :- nth1(N,List,File), format(' ~w -> ~w~n',[N,File]), fail. | |
| 125 | prdir(_). | |
| 126 | ||
| 127 | print_disprover_stats :- | |
| 128 | disprover_timeout(TO), | |
| 129 | project_name(N), format('Project ~w~n',[N]), | |
| 130 | generated(_,D), | |
| 131 | machine_name(M), format('Machine ~w (exported ~w)~n',[M,D]), | |
| 132 | print_nr_pos('',_,_), | |
| 133 | print_nr_pos('proven (within Rodin)',true,_), | |
| 134 | format('ProB Disprover Analysis with timeout ~w ms~n',[TO]), | |
| 135 | print_nr_pos('proven (by ProB)',_,true), | |
| 136 | (disprover_result(_,_,contradiction_in_hypotheses) | |
| 137 | -> print_nr_pos('those with contradiction in hypotheses',_,true,contradiction_in_hypotheses) ; true), | |
| 138 | print_nr_pos('disproven (by ProB)',_,false), | |
| 139 | print_nr_pos('unproven (by ProB)',_,unknown), | |
| 140 | (raw_result_exists(failure) -> print_nr_pos('failure (of ProB)',_,failure) ; true). | |
| 141 | ||
| 142 | raw_result_exists(RawResult) :- disprover_po_with_info(_,_,_,RawResult). | |
| 143 | print_nr_pos(Msg,RodinStatus,ProBStatus) :- print_nr_pos(Msg,RodinStatus,ProBStatus,_). | |
| 144 | print_nr_pos(Msg,RodinStatus,ProBStatus,RawResult) :- | |
| 145 | findall(Name,disprover_po_with_info(Name,RodinStatus,ProBStatus,RawResult),L), | |
| 146 | length(L,Len), | |
| 147 | (Len<12 | |
| 148 | -> format('Number of ~w POs: ~w (~w)~n',[Msg,Len,L]) | |
| 149 | ; (L = [First|_],last(L,Last)) | |
| 150 | -> format('Number of ~w POs: ~w (~w -- ~w)~n',[Msg,Len,First,Last]) | |
| 151 | ; format('Number of ~w POs: ~w~n',[Msg,Len]) | |
| 152 | ). | |
| 153 | ||
| 154 | disprover_po_with_info(Name,RodinStatus,ProBStatus,RawResult) :- | |
| 155 | disprover_po(Name,_Context,_Goal,_All,_Sel,RodinStatus), | |
| 156 | (disprover_result(Name,ProBStatus,RawResult) -> true ; ProBStatus='not_run', RawResult='not_run'). | |
| 157 | ||
| 158 | :- dynamic disprover_timeout/1. | |
| 159 | disprover_timeout(300). | |
| 160 | set_disprover_timeout(N) :- retractall(disprover_timeout(_)), assert(disprover_timeout(N)). | |
| 161 | reset_disprover_timeout :- retractall(disprover_timeout(_)), assert(disprover_timeout(300)). | |
| 162 | ||
| 163 | run :- run_disprover_on_all_pos(_). | |
| 164 | ||
| 165 | :- use_module(tools_lists,[count_occurences/2]). | |
| 166 | ||
| 167 | run_disprover_on_all_pos(_) :- retractall(disprover_result(_,_,_)), disprover_timeout(TO),run_on_po(_,TO), fail. | |
| 168 | run_disprover_on_all_pos(Summary) :- findall(R,disprover_result(_,R,_),L), | |
| 169 | count_occurences(L,Occs), | |
| 170 | format('~nDisprover Run Summary: ~w~n',[Occs]), | |
| 171 | add_info(true,Occs,O1), add_info(false,O1,O2), add_info(unknown,O2,O3), | |
| 172 | add_info(failure,O3,Summary). | |
| 173 | ||
| 174 | add_info(Info,List,Result) :- member(Info-_,List) -> List=Result ; Result = [Info-0|List]. | |
| 175 | ||
| 176 | ||
| 177 | run_on_po(PO_Name,TimeOut) :- | |
| 178 | disprover_po(PO_Name,Context,Goal,AllHypotheses,SelectedHypotheses,Status), | |
| 179 | formatsilent('Testing ~w (~w)~n',[PO_Name,Status]), | |
| 180 | load_event_b_project([],[Context],[],_), | |
| 181 | start_animation, | |
| 182 | debug_println(5,loaded_context), | |
| 183 | (my_disprove(Goal,AllHypotheses,SelectedHypotheses,TimeOut,OutResult) | |
| 184 | -> translate_result_for_po(OutResult,ProverResult), | |
| 185 | formatsilent('Disprover Result ~w (PO is ~w)~n',[OutResult,ProverResult]), | |
| 186 | functor(OutResult,RawOutFunctor,_), | |
| 187 | assert(disprover_result(PO_Name,ProverResult,RawOutFunctor)), | |
| 188 | check_soundness(ProverResult,Status,PO_Name) | |
| 189 | ; add_error(disprover,'Disprover failed: ',(PO_Name:Status)), | |
| 190 | assert(disprover_result(PO_Name,'failure',unknown)) | |
| 191 | ). | |
| 192 | run_on_po(PO_Name,_TimeOut) :- nonvar(PO_Name), | |
| 193 | \+ disprover_po(PO_Name,_,_,_,_,_), | |
| 194 | format('PO ~w does not exist !~n',[PO_Name]), | |
| 195 | findall(PO,disprover_po(PO,_,_,_,_,_),L), | |
| 196 | format('Available POs: ~w~n',[L]), | |
| 197 | fail. | |
| 198 | ||
| 199 | translate_result_for_po(solution(_),R) :- !, R=false. | |
| 200 | translate_result_for_po(contradiction_found,R) :- !,R=true. | |
| 201 | translate_result_for_po(contradiction_in_hypotheses,R) :- !,R=true. | |
| 202 | translate_result_for_po(_,unknown). | |
| 203 | ||
| 204 | check_soundness(unknown,_,_) :- !. | |
| 205 | check_soundness(Status,unknown,PO_Name) :- !, | |
| 206 | format('ProB Disprover result ~w improves upon unknown Rodin prover status for ~w!~n',[Status,PO_Name]). | |
| 207 | check_soundness(X,X,_) :- !. | |
| 208 | check_soundness(Disprover,Prover,PO_Name) :- | |
| 209 | add_error(disprover_unsound,'Disprover result incompatible with Rodin proof status:',Disprover:Prover:PO_Name). | |
| 210 | ||
| 211 | ||
| 212 | :- dynamic extra_opts/1. | |
| 213 | extra_opts([]). | |
| 214 | add_opts(Extra) :- | |
| 215 | retract(extra_opts(Old)), | |
| 216 | append(Extra,Old,New), sort(New,SNew), | |
| 217 | assert(extra_opts(SNew)). | |
| 218 | enable_cse :- XO = [use_common_subexpression_elimination/true, | |
| 219 | use_common_subexpression_also_for_predicates/true], | |
| 220 | add_opts(XO). | |
| 221 | enable_kodkod :- XO = [try_kodkod_on_load/true, kodkod_for_components/true], add_opts(XO). | |
| 222 | disable_chr :- add_opts([use_chr_solver/false]). | |
| 223 | disable_smt :- add_opts([use_smt_mode/false]). | |
| 224 | set_disprover_options(L) :- | |
| 225 | retractall(extra_opts(_)), | |
| 226 | assert(extra_opts(L)). | |
| 227 | ||
| 228 | my_disprove(Goal,AllHypotheses,SelectedHypotheses,Timeout,OutResult) :- | |
| 229 | Opts = [use_smt_mode/true,use_clpfd_solver/true,use_chr_solver/true], | |
| 230 | % interesting extra opts : disprover_option(unsat_core),unsat_core_algorithm/linear | |
| 231 | extra_opts(X), merge_opts(X,Opts,AllOpts), | |
| 232 | % Note: disprover_mode is always set to true | |
| 233 | disprove_with_opts(Goal,AllHypotheses,SelectedHypotheses,Timeout,AllOpts,OutResult). | |
| 234 | ||
| 235 | merge_opts([],Opts,Opts). | |
| 236 | merge_opts([Opt/Val|T],Other,[Opt/Val|ResT]) :- | |
| 237 | delete(Other,Opt/_,Other2), | |
| 238 | merge_opts(T,Other2,ResT). | |
| 239 | ||
| 240 | :- use_module(translate). | |
| 241 | ||
| 242 | list(DPRes) :- disprover_po(Name,Context,Goal,_All,_Sel,Status), | |
| 243 | get_disprover_result(Name,DPRes,RawResult), | |
| 244 | format('~w (~w : ~w [~w]) : ',[Name,Status,DPRes,RawResult]), | |
| 245 | load_event_b_project([],[Context],[],_), | |
| 246 | start_animation, | |
| 247 | type_check_in_machine_context([Goal],[TypedGoal]), | |
| 248 | translate:print_bexpr(TypedGoal),nl,fail. | |
| 249 | list(_). | |
| 250 | ||
| 251 | :- dynamic project_name/1. | |
| 252 | :- dynamic machine_name/1. | |
| 253 | :- dynamic generated/2. | |
| 254 | :- dynamic disprover_po/6. | |
| 255 | :- dynamic disprover_result/3. | |
| 256 | project_name(unknown). | |
| 257 | machine_name(unknown). | |
| 258 | generated(unknown,unknown). | |
| 259 | disprover_po(unknown,unknown,unknown,unknown,unknown,unknown). | |
| 260 | disprover_result(unknown,unknown,unknown). | |
| 261 | ||
| 262 | reset_po_facts :- retractall(loaded_po_file(_)), | |
| 263 | retractall(project_name(_)), | |
| 264 | retractall(machine_name(_)), retractall(generated(_,_)), | |
| 265 | retractall(disprover_po(_,_,_,_,_,_)), retractall(disprover_result(_,_,_)). | |
| 266 | ||
| 267 | % write POs which have a certain status; can be used to generate .pl files with only proven or not-proven POs | |
| 268 | write_pos(Status,RawResult) :- | |
| 269 | format('% Proof Obligations with status = ~w~n',[Status]), | |
| 270 | write_facts(project_name(_)), write_facts(machine_name(_)), | |
| 271 | write_facts(generated(_,_)), | |
| 272 | disprover_result(Name,Status,RawResult), | |
| 273 | write_facts(disprover_po(Name,_Context,_Goal,_All,_Sel,_RodinStatus)), | |
| 274 | fail. | |
| 275 | write_pos(_,_) :- nl. | |
| 276 | ||
| 277 | write_facts(Fact) :- Fact, | |
| 278 | write_term(Fact,[quoted(true),numbervars(true)]), write('.'),nl,fail. | |
| 279 | write_facts(_). | |
| 280 | ||
| 281 | get_disprover_result(PO_Name,Result,RawResult) :- | |
| 282 | (disprover_result(PO_Name,R,Raw) -> Result=R,RawResult=Raw | |
| 283 | ; Result = 'not_yet_run', RawResult='not_yet_run'). | |
| 284 | ||
| 285 | :- dynamic loaded_po_file/1. | |
| 286 | load_po_file(File) :- reset_po_facts, | |
| 287 | % consult_without_redefine_warning | |
| 288 | prolog_flag(redefine_warnings, Old, off), | |
| 289 | (% load in dynamic mode: so that we can retract later | |
| 290 | my_po_consult(File) | |
| 291 | -> OK=true ; OK=false), | |
| 292 | prolog_flag(redefine_warnings, _, Old), | |
| 293 | (OK=true -> assert(loaded_po_file(File)) ; | |
| 294 | add_error_and_fail(disprover_test_runner,'Consulting of File failed: ',File)). | |
| 295 | ||
| 296 | my_po_consult(File) :- on_exception(error(existence_error(_,_),_), | |
| 297 | load_files(File,[compilation_mode(assert_all)]), | |
| 298 | add_error_fail(my_consult,'File does not exist: ',File)). | |
| 299 | ||
| 300 | ||
| 301 | disprover_load_at_repl_startup :- prolog_flag(argv,ArgV),ArgV = [FILE|T], | |
| 302 | (T=[] -> load_po_file(FILE) | |
| 303 | ; format('*** Please provide only one command-line argument: ~w~n',[ArgV]),fail). | |
| 304 | disprover_load_at_repl_startup :- | |
| 305 | print('Loading default file'),nl, | |
| 306 | load_po_file('../prob_examples/examples/ProofObligations/ABZ14_Mery/M3_mch.pl'). | |
| 307 | disprover_load_at_repl_startup. | |
| 308 | ||
| 309 | % :- load_po_file('../../prob_examples/examples/ProofObligations/ABZ14_Mery/M2_mch.pl'). | |
| 310 | % :- load_po_file('../../prob_examples/examples/ProofObligations/ABZ14_Mery/M3_mch.pl'). | |
| 311 | % :- load_po_file('../../prob_examples/examples/ProofObligations/ABZ14_Mery/M4_mch.pl'). | |
| 312 | % :- load_po_file('../../prob_examples/public_examples/EventBPrologPackages/Disprover/ProofTests/DefSetCst_ctx.pl'). | |
| 313 | % '/Users/leuschel/git_root/prob_examples/public_examples/SMT/QF_IDL/queens_bench/toroidal_bench/toroidal_queen_2_QF_IDL_ctx.pl'. | |
| 314 | ||
| 315 | %:- test_repl. | |
| 316 |