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).