1 | % (c) 2013-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, [disprove/5, disprove_with_opts/6]). | |
6 | ||
7 | :- use_module(module_information). | |
8 | :- module_info(group,cbc). | |
9 | :- module_info(description,'Rodin Prover / Disprover'). | |
10 | ||
11 | % provide access to the Disprover algorithm with all hypotheses, selected hypotheses and goal | |
12 | ||
13 | :- use_module(extension('user_signal/user_signal'), [user_interruptable_call_det/2]). | |
14 | ||
15 | :- use_module(solver_interface, [solve_predicate/5,type_check_in_machine_context/2]). | |
16 | :- use_module(preferences, [temporary_set_preference/3, reset_temporary_preference/2, | |
17 | get_preference/2]). | |
18 | :- use_module(bsyntaxtree, [conjunct_predicates/2, create_negation/2, | |
19 | find_typed_identifier_uses/3, | |
20 | find_typed_identifier_uses_l/3, | |
21 | get_texpr_types/2]). | |
22 | :- use_module(error_manager, [reset_errors/0,add_warning/3]). | |
23 | :- use_module(library(lists)). | |
24 | :- use_module(tools,[start_ms_timer/1, stop_ms_timer/1]). | |
25 | :- use_module(debug, [debug_println/2,debug_mode/1]). | |
26 | :- use_module(b_global_sets,[contains_unfixed_deferred_set/1]). | |
27 | :- use_module(external_functions,[observe_state/1]). | |
28 | :- use_module(unsat_cores,[unsat_core/2]). | |
29 | ||
30 | disprove(Goal,AllHypotheses,SelectedHypotheses,Timeout,OutResult) :- | |
31 | % default options: | |
32 | Opts = [use_smt_mode/true,use_clpfd_solver/true,use_chr_solver/true], | |
33 | % Note: disprover_mode is always set to true | |
34 | disprove_with_opts(Goal,AllHypotheses,SelectedHypotheses,Timeout,Opts,OutResult). | |
35 | ||
36 | disprove_with_opts(Goal,AllHypotheses,SelectedHypotheses,Timeout,Opts,OutResult) :- | |
37 | temporary_set_preference(disprover_mode,true,DC), | |
38 | temporary_set_preference(time_out,Timeout,TC), | |
39 | start_ms_timer(Timer), | |
40 | user_interruptable_call_det(disprove1(Goal,AllHypotheses,SelectedHypotheses,Opts,Result),InterruptResult), | |
41 | %write(ir(InterruptResult)), nl, | |
42 | (InterruptResult = interrupted -> OutResult = interrupted ; OutResult = Result), | |
43 | %catch_internal_timeout(InterruptResult,Result,OutResult), | |
44 | (debug_mode(on) -> write(disprove_result(OutResult)),nl,stop_ms_timer(Timer),nl ; true), | |
45 | reset_temporary_preference(disprover_mode,DC), | |
46 | reset_temporary_preference(time_out,TC). | |
47 | ||
48 | :- use_module(error_manager,[add_all_perrors/3]). | |
49 | disprove1(Goal,AllHypotheses,SelectedHypotheses,Opts,Result) :- | |
50 | on_exception(type_errors(E), | |
51 | disprove2(Goal,AllHypotheses,SelectedHypotheses,Opts,Result), | |
52 | (add_all_perrors(E,[],disprover), Result=type_error)). | |
53 | ||
54 | %catch_internal_timeout(ok,contradiction_found,Out) :- | |
55 | % error_manager:check_warning_occured(warning(_X),Y), | |
56 | % is_time_out_message(Y), % Sebastian: why do we catch this ?? This is not necessarily a problem ?? | |
57 | % !, % Might be a problem for proofs, invalidate only if Result = contradiction_found | |
58 | % Out = time_out. % However, this might be old code that is superseded by the enum warnings | |
59 | %catch_internal_timeout(ok,Result,Result). | |
60 | ||
61 | % is_time_out_message(Y) :- atom(Y), atom_codes(Y,Codes), | |
62 | % append("TIME-OUT occurred while ProB was expanding", _, Codes). | |
63 | ||
64 | solve_disprover_predicate(Predicate,Opts,CBCResult) :- | |
65 | TimeoutFactor = 1, | |
66 | exclude(disprover_option,Opts,SOpts), | |
67 | (member(disprover_option(observe_state),Opts) -> observe_state(State) ; true), | |
68 | solve_predicate(Predicate,State,TimeoutFactor,SOpts,CBCResult). | |
69 | disprover_option(disprover_option(_)). | |
70 | ||
71 | :- public disprove2/5. % it is called by user_interruptable_call_det above; we should also add a meta_predicate annotation | |
72 | :- use_module(bsyntaxtree, [predicate_identifiers/2]). | |
73 | disprove2(Goal,AllHypotheses,SelectedHypotheses,Opts,ResultOut) :- | |
74 | type_check_in_machine_context([Goal|AllHypotheses],[TGoal|TAllHypotheses]), | |
75 | type_check_in_machine_context(SelectedHypotheses,TSelectedHypotheses), | |
76 | ||
77 | % build predicate H1 & H2 .... & not Goal | |
78 | create_negation(TGoal,NegatedGoal), | |
79 | ||
80 | %(debug_mode(on) -> write(NegatedGoal), nl ; true), | |
81 | ||
82 | (debug_mode(on) -> nl,write('Negated Goal:'), nl, | |
83 | translate:nested_print_bexpr_as_classicalb(NegatedGoal), | |
84 | write_hypothesis(TAllHypotheses) | |
85 | ; true), | |
86 | conjunct_predicates([NegatedGoal|TAllHypotheses],Predicate), | |
87 | (member(disprover_option(show_po_as_machine),Opts) | |
88 | -> print('PO as B Machine: '),nl, | |
89 | translate_predicate_into_machine(Predicate,ResultAtom), | |
90 | write(ResultAtom),nl | |
91 | ; true), | |
92 | %tools:print_bt_message(solving), | |
93 | solve_disprover_predicate(Predicate,Opts,Result), | |
94 | %tools:print_bt_message(solver_result(CBCResult)), | |
95 | debug_println(10,disprover_result_with_all_hypotheses(Result)), | |
96 | ||
97 | disprove_double_check(Result,NegatedGoal,TAllHypotheses,TSelectedHypotheses,Predicate,Opts,ResultOut). | |
98 | ||
99 | % res <— solve( All Hyp & not G ) | |
100 | % if res = solution then | |
101 | % return CounterExample Found, Goal definitely not provable | |
102 | % else if unfixed deferred set used in selected Hypotheses or Goal then | |
103 | % return Unknown | |
104 | % else if res = fail (without time-out & without enumeration warning & no unfixed deferred set in All Hypotheses) then | |
105 | % return Proof Found, Goal proven | |
106 | % else | |
107 | % res <— solve (Selected Hyp & not G) /* maybe use smaller time-out here ?? */ | |
108 | % if res = fail (without time-out & without enumeration warning) then | |
109 | % return Proof Found, Goal proven | |
110 | % else if res = solution then | |
111 | % return CounterExample for selected Hypotheses found, Goal not provable from selected Hypotheses (but may be provable with all Hyp) | |
112 | % else | |
113 | % return Unknown | |
114 | % fi | |
115 | % fi | |
116 | ||
117 | % we found a solution / counter example. no need to double check here. | |
118 | % just clear up the resulting state, keeping only variables occuring in the goal. | |
119 | % although: sometimes it is useful to have other IDs as well, at least in the same component as the Goal ! | |
120 | disprove_double_check(solution(X),NegatedGoal,_Hypotheses,_SelectedHypotheses,_,_,ResultOut) :- | |
121 | predicate_identifiers(NegatedGoal,GoalIdentifiers), | |
122 | findall(binding(Id,Value,PP), (member(binding(Id,Value,PP),X), member(Id,GoalIdentifiers)), FilteredState), | |
123 | ResultOut = solution(FilteredState). | |
124 | % check if the unfixed deferred sets occur in selected hyps or goal | |
125 | disprove_double_check(no_solution_found(unfixed_deferred_sets),NegatedGoal,_Hypotheses,SelectedHypotheses,_,_,no_solution_found(unfixed_deferred_sets)) :- | |
126 | find_typed_identifier_uses(NegatedGoal,[],GoalIdentifiers), | |
127 | get_texpr_types(GoalIdentifiers,GoalTypes), | |
128 | find_typed_identifier_uses_l(SelectedHypotheses,[],HypIdentifiers), | |
129 | get_texpr_types(HypIdentifiers,HypTypes), | |
130 | append(GoalTypes,HypTypes,Types), | |
131 | % exclude all types that are not unfixed | |
132 | include(contains_unfixed_deferred_set,Types,UnfixedTypes), | |
133 | % see if an unfixed type is left | |
134 | UnfixedTypes = [_|_], | |
135 | debug_println(4,goal_or_sel_hyp_contains_unfixed_deferred_sets(UnfixedTypes)), | |
136 | !. | |
137 | % contradiction was found, i.e. there was neither a timeout nor an enumeration warning | |
138 | disprove_double_check(contradiction_found,NegatedGoal,Hypotheses,SelectedHypotheses,FullPredicate,Opts,FinalResult) :- | |
139 | get_preference(double_evaluation_when_analysing,true) | |
140 | -> check_negated(NegatedGoal,Hypotheses,SelectedHypotheses,FullPredicate,Opts,FinalResult) | |
141 | ; FinalResult = contradiction_found. | |
142 | disprove_double_check(Result,_NegatedGoal,Hypotheses,SelectedHypotheses,_,_Opts,ResultOut) :- | |
143 | same_conjunction_list(Hypotheses,SelectedHypotheses),!, | |
144 | (debug_mode(on) -> nl,write('Selected hypotheses identical to all hypotheses.'),nl ; true), | |
145 | Result=ResultOut. | |
146 | % see what solving only selected hypotheses & not G gives us | |
147 | disprove_double_check(_OldResult,NegatedGoal,Hypotheses,SelectedHypotheses,_,Opts,ResultOut) :- | |
148 | % No proof found with all hypotheses, now try selected ones only | |
149 | % reset existing enumeration warnings, | |
150 | % that might have been generated in a previous run | |
151 | reset_errors, | |
152 | (debug_mode(on) | |
153 | -> nl,write('Trying to use only selected hypotheses.\nNegated Goal:'), nl, | |
154 | translate:nested_print_bexpr_as_classicalb(NegatedGoal), | |
155 | write_hypothesis(SelectedHypotheses) | |
156 | ; true), | |
157 | conjunct_predicates([NegatedGoal|SelectedHypotheses],Predicate), | |
158 | %external_functions:observe_state(State), | |
159 | solve_disprover_predicate(Predicate,Opts,Result), | |
160 | !, | |
161 | disprove_triple_check(Result,NegatedGoal,Hypotheses,SelectedHypotheses,Predicate,Opts,ResultOut). | |
162 | ||
163 | ||
164 | % we still have a contradiction -> double check it if preference set | |
165 | disprove_triple_check(contradiction_found,NegatedGoal,Hypotheses,SelectedHypotheses,FullPredicate,Opts,FinalResult) :- | |
166 | (get_preference(double_evaluation_when_analysing,true) | |
167 | -> check_negated(NegatedGoal,Hypotheses,SelectedHypotheses,FullPredicate,Opts,FinalResult) | |
168 | ; FinalResult = contradiction_found, | |
169 | compute_unsat_core_if_requested(FullPredicate,Opts) | |
170 | ). | |
171 | disprove_triple_check(solution(X),NegatedGoal,_,_,_FullPredicate,_,ResultOut) :- | |
172 | predicate_identifiers(NegatedGoal,GoalIdentifiers), | |
173 | findall(binding(Id,Value,PP), (member(binding(Id,Value,PP),X), member(Id,GoalIdentifiers)), FilteredState), | |
174 | ResultOut = solution_on_selected_hypotheses(FilteredState). | |
175 | disprove_triple_check(time_out,_,_,_,_,_,time_out). % TODO: We could try Kodkod here! | |
176 | disprove_triple_check(no_solution_found(X),_,_,_,_,_,no_solution_found(X)). % Or here? | |
177 | ||
178 | check_negated(NegatedGoal,Hypotheses,_,FullOrigPredicate,Opts,ResultOut) :- | |
179 | create_negation(NegatedGoal,Goal), | |
180 | conjunct_predicates([Goal|Hypotheses],Predicate), | |
181 | %tools:print_bt_message(check_negated), | |
182 | debug_println(20,'Check whether we can also prove negation of goal'), | |
183 | solve_disprover_predicate(Predicate,Opts,Result), | |
184 | %% tools:print_bt_message(solver_result(CBCResult)), | |
185 | !, | |
186 | (Result = contradiction_found % proven both (H & not G) and (H & G) | |
187 | -> ResultOut = contradiction_in_hypotheses, | |
188 | translate:translate_bexpression_with_limit(NegatedGoal,GS), | |
189 | add_warning(disprover_inconsistent_hypotheses, | |
190 | 'Disprover double check result: Contradiction in hypotheses (or Bug) detected for goal: ', | |
191 | GS), %% check_negated(NegatedGoal,Hypotheses)) | |
192 | compute_unsat_core_if_requested(Predicate,Opts) | |
193 | ; ResultOut = contradiction_found, | |
194 | compute_unsat_core_if_requested(FullOrigPredicate,Opts) | |
195 | ). | |
196 | ||
197 | compute_unsat_core_if_requested(Predicate,Opts) :- | |
198 | (member(disprover_option(unsat_core),Opts) -> compute_unsat_core(Opts,Predicate) ; true). | |
199 | :- use_module(preferences,[call_with_preference/3]). | |
200 | :- use_module(translate,[translate_predicate_into_machine/2,nested_print_bexpr_as_classicalb/1]). | |
201 | compute_unsat_core(Opts,Predicate) :- | |
202 | (member(unsat_core_algorithm/P,Opts) | |
203 | -> call_with_preference(compute_unsat_core_aux(Predicate,CorePredicate),unsat_core_algorithm,P) | |
204 | ; compute_unsat_core(Predicate,CorePredicate)), | |
205 | !, | |
206 | print('UNSAT CORE: '),nl,print('--------'),nl, | |
207 | (member(disprover_option(unsat_core_as_machine),Opts) | |
208 | -> translate_predicate_into_machine(CorePredicate,ResultAtom), | |
209 | write(ResultAtom),nl | |
210 | ; nested_print_bexpr_as_classicalb(CorePredicate)), | |
211 | nl, print('--------'),nl. | |
212 | ||
213 | compute_unsat_core_aux(Predicate,CorePredicate) :- | |
214 | print('Computing UNSAT CORE'),nl, | |
215 | unsat_core(Predicate,CorePredicate). % from unsat_cores | |
216 | ||
217 | :- use_module(probsrc(bsyntaxtree),[same_texpr/2]). | |
218 | % check if two lists of conjuncts represent the same conjunction (modulo info fields) | |
219 | same_conjunction_list(List1,List2) :- | |
220 | same_length(List1,List2,_), % avoid possibly expensive comparisons if lists clearly different | |
221 | % we could strip info field and the sort; but here we just want to catch the obvious case where the disprover is called with SelectedHyp = AllHyp | |
222 | maplist(same_texpr,List1,List2). | |
223 | ||
224 | write_hypothesis([]). | |
225 | write_hypothesis([Hyp|Hyps]) :- | |
226 | write(' & /* Hypothesis: */ '), nl, | |
227 | %(debug_mode(on) -> write(Hyp), nl ; true), | |
228 | translate:nested_print_bexpr_as_classicalb(Hyp), | |
229 | write_hypothesis(Hyps). |