1 | % (c) 2009-2015 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 | ||
6 | :- module(unsat_cores,[unsat_core/2, | |
7 | unsat_core_with_time_limit/3, | |
8 | unsat_core_with_fixed_conjuncts/3, | |
9 | minimum_unsat_core/2, | |
10 | minimum_unsat_core_with_fixed_conjuncts/3, | |
11 | tcltk_unsat_core_properties/1]). | |
12 | ||
13 | :- use_module(module_information,[module_info/2]). | |
14 | :- module_info(group,misc). | |
15 | :- module_info(description,'Computation of unsatisfiable cores of predicates.'). | |
16 | ||
17 | :- use_module(library(lists),[append/2,min_member/3]). | |
18 | ||
19 | :- use_module(bsyntaxtree,[conjunction_to_list/2, | |
20 | conjunct_predicates/2, | |
21 | create_negation/2]). | |
22 | :- use_module(solver_interface, [solve_predicate/4]). | |
23 | :- use_module(preferences, [get_preference/2]). | |
24 | :- use_module(debug, [debug_println/2]). | |
25 | :- use_module(self_check, [assert_must_succeed/1,assert_must_fail/1]). | |
26 | ||
27 | :- assert_must_succeed((unsat_core(b(falsity,pred,[]),Core), Core == b(falsity,pred,[]))). | |
28 | :- assert_must_succeed((unsat_core(b(conjunct(b(falsity,pred,[]),b(truth,pred,[])),pred,[]),Core), Core == b(falsity,pred,[]))). | |
29 | ||
30 | tcltk_unsat_core_properties(list(CorePredStrings)) :- | |
31 | bmachine:b_get_properties_from_machine(Properties), % TO DO: also provide for unsat component | |
32 | print('Computing (efficient) unsat core for PROPERTIES'),nl, | |
33 | unsat_core_chr(Properties,CorePredicate), | |
34 | print(finished),nl, | |
35 | findall(CS, (b_interpreter:member_conjunct(C,CorePredicate,_), % TO DO: move member_conjunct to another module | |
36 | translate:translate_bexpression(C,CS)), CorePredStrings), | |
37 | print(CorePredStrings),nl. | |
38 | ||
39 | :- use_module(preferences, [temporary_set_preference/3, reset_temporary_preference/2]). | |
40 | % calls unsat_core but with CHR and other preferences set | |
41 | unsat_core_chr(Pred,Core) :- | |
42 | temporary_set_preference(use_chr_solver,true,CHNG1), | |
43 | call_cleanup(unsat_core(Pred,Core), | |
44 | reset_temporary_preference(use_chr_solver,CHNG1)). | |
45 | ||
46 | % TODO: cleanup / rewrite predicate in order to minimize cores | |
47 | % i.e. implications could be rewritten into conjuncts | |
48 | ||
49 | :- assert_must_fail((minimum_unsat_core(b(conjunct(b(falsity,pred,[]), | |
50 | b(conjunct(b(less(b(integer(1),integer,[]),b(identifier(x),integer,[])),pred,[]), | |
51 | b(less(b(identifier(x),integer,[]),b(integer(1),integer,[])),pred,[])),pred,[])),pred,[]),Core), | |
52 | Core == b(less(b(integer(1),integer,[]),b(identifier(x),integer,[])),pred,[]))). | |
53 | :- assert_must_fail((minimum_unsat_core(b(conjunct(b(falsity,pred,[]), | |
54 | b(conjunct(b(less(b(integer(1),integer,[]),b(identifier(x),integer,[])),pred,[]),b(less(b(identifier(x),integer,[]),b(integer(1),integer,[])),pred,[])),pred,[])),pred,[]),Core), | |
55 | Core == b(less(b(identifier(x),integer,[]),b(integer(1),integer,[])),pred,[]))). | |
56 | % there should be two cores | |
57 | :- assert_must_succeed((findall(Core, unsat_core(b(conjunct(b(falsity,pred,[]), | |
58 | b(conjunct(b(less(b(integer(1),integer,[]),b(identifier(x),integer,[])),pred,[]),b(less(b(identifier(x),integer,[]),b(integer(1),integer,[])),pred,[])),pred,[])),pred,[]),Core), | |
59 | ListOfCores), length(ListOfCores,2))). | |
60 | ||
61 | % call if you know how much time (in ms) it took to find inconsistency in Predicate | |
62 | unsat_core_with_time_limit(Predicate,CorePredicate,TimeToFindContradiction) :- | |
63 | number(TimeToFindContradiction), TimeToFindContradiction>=0, | |
64 | NewTimeOut is TimeToFindContradiction+30, % in case we have 0; just add a few ms | |
65 | temporary_set_preference(time_out,NewTimeOut,CHNG1), | |
66 | % this time will be multiplied by 2 below | |
67 | call_cleanup(unsat_core(Predicate,CorePredicate), | |
68 | reset_temporary_preference(time_out,CHNG1)). | |
69 | ||
70 | unsat_core(Predicate,CorePredicate) :- | |
71 | uc_conjunction_to_list(Predicate,PredicateList), | |
72 | unsat_core_with_fixed_conjuncts_lists(PredicateList,[],CoreList), | |
73 | conjunct_predicates(CoreList,CorePredicate). | |
74 | ||
75 | % strip outermost existential quantifiers so that we can examine the conjunction inside | |
76 | uc_conjunction_to_list(b(exists(_V,Pred),pred,_),List) :- !, | |
77 | uc_conjunction_to_list(Pred,List). | |
78 | % TO DO: add let_predicate (decomposed further below) ? forall ? | |
79 | uc_conjunction_to_list(Pred,List) :- conjunction_to_list(Pred,List). | |
80 | ||
81 | unsat_core_with_fixed_conjuncts(Predicate,FixedConjuncts,Core) :- | |
82 | uc_conjunction_to_list(Predicate,PredicateList), | |
83 | conjunction_to_list(FixedConjuncts,FixedList), | |
84 | unsat_core_with_fixed_conjuncts_lists(PredicateList,FixedList,CoreList), | |
85 | conjunct_predicates(CoreList,Core). | |
86 | ||
87 | unsat_core_with_fixed_conjuncts_lists(PredicateList,FixedList,CoreList) :- | |
88 | get_preference(unsat_core_algorithm,divide_and_conquer), !, | |
89 | temporary_set_preference(allow_enumeration_of_infinite_types,false,OldValueOfPref), | |
90 | call_cleanup(unsat_core_with_fixed_conjuncts_lists_divide_and_conquer(PredicateList,FixedList,CoreList), | |
91 | reset_temporary_preference(allow_enumeration_of_infinite_types,OldValueOfPref)). | |
92 | unsat_core_with_fixed_conjuncts_lists(PredicateList,FixedList,CoreList) :- | |
93 | temporary_set_preference(allow_enumeration_of_infinite_types,true,OldValueOfPref), | |
94 | call_cleanup(unsat_core_with_fixed_conjuncts_lists_linear(PredicateList,[],FixedList,CoreList), | |
95 | reset_temporary_preference(allow_enumeration_of_infinite_types,OldValueOfPref)). | |
96 | ||
97 | ||
98 | % simple unsat core computation: remove conjuncts till satisfiability is reached | |
99 | unsat_core_with_fixed_conjuncts_lists_linear([],DefinitelyInCoreClauses,_FixedConjuncts,DefinitelyInCoreClauses). | |
100 | unsat_core_with_fixed_conjuncts_lists_linear([C|Cs],DefinitelyInCoreClauses,FixedConjuncts,Core) :- | |
101 | % remove C and check for satisfiability | |
102 | append([Cs,DefinitelyInCoreClauses,FixedConjuncts],ToCheck), | |
103 | conjunct_predicates(ToCheck,ConjunctionToCheck), | |
104 | % print('REMOVING: '), translate:print_bexpr(C),nl, | |
105 | solve_predicate(ConjunctionToCheck,_State,2,Res), | |
106 | debug_println(4,solve_predicate_result(Res)), | |
107 | progress_info(Res), | |
108 | solution_found(Res), !, % a solution has been found or a time-out occured - C can not be removed; corresponds to solve_result: contradiction_found or no_solution_found(unfixed_deferred_sets) | |
109 | % TO DO: if outermost predicate generates virtual_time_out(Reason) then also accepts this | |
110 | % TO DO: maybe make treatment uniform with divide_and_conquer_recur_condition which works on solver_result return value | |
111 | (can_be_further_decomposed(C,CA,CB) | |
112 | -> % print('% Split: '), translate:print_bexpr(CA),nl, print('% '),translate:print_bexpr(CB),nl, | |
113 | unsat_core_with_fixed_conjuncts_lists_linear([CA,CB|Cs],DefinitelyInCoreClauses,FixedConjuncts,Core) | |
114 | ; unsat_core_with_fixed_conjuncts_lists_linear(Cs,[C|DefinitelyInCoreClauses],FixedConjuncts,Core) | |
115 | ). | |
116 | unsat_core_with_fixed_conjuncts_lists_linear([C|Cs],DefinitelyInCoreClauses,FixedConjuncts,Core) :- | |
117 | % C can be removed - here we introduce a choice point to not remove C. | |
118 | % that way, further cores could be computed by backtracking (i.e. for finding the minimal one) | |
119 | unsat_core_with_fixed_conjuncts_lists_linear(Cs,DefinitelyInCoreClauses,FixedConjuncts,Core) | |
120 | ; % Possible TO DO: we could do a can_be_further_decomposed check and put either CA or CB in or both in core | |
121 | unsat_core_with_fixed_conjuncts_lists_linear(Cs,[C|DefinitelyInCoreClauses],FixedConjuncts,Core). | |
122 | ||
123 | ||
124 | solution_found(Res) :- | |
125 | Res \= contradiction_found, | |
126 | Res \= no_solution_found(_). %% change to e.g. error to find unsat error core | |
127 | %solution_found(Res) :- Res \= error. % TO DO: provide parameter to say what kind of core we are looking for | |
128 | ||
129 | can_be_further_decomposed(TE,A,B) :- can_be_further_decomposed(TE,positive,A,B). | |
130 | can_be_further_decomposed(b(E,pred,Info),NegPos,A,B) :- can_be_further_decomposed_aux(E,Info,NegPos,A,B). | |
131 | can_be_further_decomposed_aux(conjunct(A,B),_,positive,A,B). | |
132 | can_be_further_decomposed_aux(disjunct(A,B),_,negative,A,B). | |
133 | can_be_further_decomposed_aux(implication(A,B),_,negative,NA,B) :- % A=>B <--> not(A) or B | |
134 | create_negation(A,NA). | |
135 | can_be_further_decomposed_aux(negation(D),_,NegPos,NA,NB) :- neg(NegPos,PosNeg), | |
136 | can_be_further_decomposed(D,PosNeg,A,B), | |
137 | create_negation(A,NA), | |
138 | create_negation(B,NB). | |
139 | can_be_further_decomposed_aux(let_predicate(V,E,P),Info,NegPos,LEA,LEB) :- | |
140 | can_be_further_decomposed(P,NegPos,A,B), | |
141 | LEA = b(let_predicate(V,E,A),pred,Info), | |
142 | LEB = b(let_predicate(V,E,B),pred,Info). | |
143 | can_be_further_decomposed_aux(lazy_let_pred(V,E,P),Info,NegPos,LEA,LEB) :- | |
144 | can_be_further_decomposed(P,NegPos,A,B), | |
145 | LEA = b(lazy_let_pred(V,E,A),pred,Info), | |
146 | LEB = b(lazy_let_pred(V,E,B),pred,Info). | |
147 | ||
148 | neg(positive,negative). neg(negative,positive). | |
149 | ||
150 | % a binary search algorithm in order to only need log(n) instead of n solver calls | |
151 | % Idea: split list of conjuncts in half, C = [A,B] | |
152 | unsat_core_with_fixed_conjuncts_lists_divide_and_conquer([],_,_) :- !, fail. % we split to far! | |
153 | unsat_core_with_fixed_conjuncts_lists_divide_and_conquer([C],_FixedConjuncts,[C]) :- !. % if there is only one conjunct left, it has to belong to the core | |
154 | unsat_core_with_fixed_conjuncts_lists_divide_and_conquer(Clauses,FixedConjuncts,Core) :- | |
155 | split_in_half(Clauses,A,B), | |
156 | % print('SPLIT: '), print(A),nl,print(B),nl, | |
157 | unsat_core_with_fixed_conjuncts_lists_divide_and_conquer_split(A,B,FixedConjuncts,Core). | |
158 | ||
159 | unsat_core_with_fixed_conjuncts_lists_divide_and_conquer_split(A,B,FixedConjuncts,Core) :- | |
160 | append(A,FixedConjuncts,AllConjuncts), | |
161 | conjunct_predicates(AllConjuncts,APred), | |
162 | % print('SOLVING LHS: '), translate:print_bexpr(APred),nl, | |
163 | solve_predicate(APred,_AState,2,ARealRes), | |
164 | progress_info(ARealRes), | |
165 | % print(result(ARealRes)),nl, | |
166 | !, % do not backtrack into solving or multiple results can be found leading to duplicated cores | |
167 | unsat_core_with_fixed_conjuncts_lists_divide_and_conquer_recur1(ARealRes,A,B,FixedConjuncts,Core). | |
168 | ||
169 | progress_info(ARes) :- progress_info_aux(ARes),!,flush_output(user_output). | |
170 | progress_info_aux(time_out) :- write('T'). | |
171 | progress_info_aux(no_solution_found(unfixed_deferred_sets)) :- write('-'). | |
172 | progress_info_aux(contradiction_found) :- write('-'). | |
173 | progress_info_aux(solution(_)) :- write('+'). | |
174 | progress_info_aux(no_solution_found(_)) :- write('V'). | |
175 | progress_info_aux(clpfd_overflow) :- write('O'). | |
176 | ||
177 | unsat_core_with_fixed_conjuncts_lists_divide_and_conquer_recur1(ARealRes,A,_B,FixedConjuncts,Core) :- | |
178 | divide_and_conquer_recur_condition(ARealRes), % A is (virtually / effectively) unsat. Recur on A. | |
179 | unsat_core_with_fixed_conjuncts_lists_divide_and_conquer(A,FixedConjuncts,Core). | |
180 | unsat_core_with_fixed_conjuncts_lists_divide_and_conquer_recur1(ARealRes,A,B,FixedConjuncts,Core) :- | |
181 | append(B,FixedConjuncts,AllConjuncts), | |
182 | conjunct_predicates(AllConjuncts,BPred), | |
183 | % print('SOLVING RHS: '), translate:print_bexpr(BPred),nl, | |
184 | solve_predicate(BPred,_BState,2,BRealRes), | |
185 | progress_info(BRealRes), | |
186 | % print(result(BRealRes)),nl, | |
187 | !, | |
188 | unsat_core_with_fixed_conjuncts_lists_divide_and_conquer_recur2(ARealRes,BRealRes,A,B,FixedConjuncts,Core). | |
189 | ||
190 | unsat_core_with_fixed_conjuncts_lists_divide_and_conquer_recur2(_ARealRes,BRealRes,_A,B,FixedConjuncts,Core) :- | |
191 | divide_and_conquer_recur_condition(BRealRes), % B is (virtually / effectively) unsat. Recur on B. | |
192 | !, | |
193 | unsat_core_with_fixed_conjuncts_lists_divide_and_conquer(B,FixedConjuncts,Core). | |
194 | unsat_core_with_fixed_conjuncts_lists_divide_and_conquer_recur2(ARealRes,BRealRes,A,B,FixedConjuncts,Core) :- | |
195 | % the interesting case: if both are sat | |
196 | \+ divide_and_conquer_recur_condition(ARealRes), | |
197 | \+ divide_and_conquer_recur_condition(BRealRes), | |
198 | % minimize A assuming usat core includes B | |
199 | append(B,FixedConjuncts,FixedAndB), | |
200 | unsat_core_with_fixed_conjuncts_lists_divide_and_conquer(A,FixedAndB,ACore), | |
201 | % now ACore & B is unsat and minimal but not minimum core | |
202 | % minimize B assuming ACore | |
203 | append(ACore,FixedConjuncts,FixedAndA), | |
204 | unsat_core_with_fixed_conjuncts_lists_divide_and_conquer(B,FixedAndA,BCore), | |
205 | append(ACore,BCore,Core). | |
206 | ||
207 | divide_and_conquer_recur_condition(contradiction_found). | |
208 | divide_and_conquer_recur_condition(no_solution_found(X)) :- | |
209 | % to do: if the outermost conjunct already generates a time_out or critical enumeration warning then this should be enabled as a recur condition | |
210 | X \= enumeration_warning(_,_,_,_,critical). | |
211 | %divide_and_conquer_recur_condition(time_out). | |
212 | ||
213 | split_in_half(C, A, B) :- | |
214 | length(C,L), | |
215 | Half is L // 2, | |
216 | length(A, Half), | |
217 | append(A, B, C). | |
218 | ||
219 | % there is currently no known good algorithm to compute the minimum unsat core | |
220 | % we can just compute every core and take the minimum one out of the list | |
221 | :- assert_must_succeed((minimum_unsat_core(b(conjunct(b(falsity,pred,[]), | |
222 | b(conjunct(b(less(b(integer(1),integer,[]),b(identifier(x),integer,[])),pred,[]),b(less(b(identifier(x),integer,[]),b(integer(1),integer,[])),pred,[])),pred,[])),pred,[]),Core), | |
223 | Core == b(falsity,pred,[]))). | |
224 | minimum_unsat_core(Predicate,CorePredicate) :- | |
225 | uc_conjunction_to_list(Predicate,PredicateList), | |
226 | findall(CoreList,unsat_core_with_fixed_conjuncts_lists(PredicateList,[],CoreList),Cores), | |
227 | %print(all_cores(Cores)),nl, | |
228 | min_member(compare_length,MinList,Cores), | |
229 | conjunct_predicates(MinList,CorePredicate). | |
230 | ||
231 | minimum_unsat_core_with_fixed_conjuncts(Predicate,FixedConjuncts,CorePredicate) :- | |
232 | uc_conjunction_to_list(Predicate,PredicateList), | |
233 | conjunction_to_list(FixedConjuncts,FixedList), | |
234 | findall(CoreList,unsat_core_with_fixed_conjuncts_lists(PredicateList,FixedList,CoreList),Cores), | |
235 | min_member(compare_length,MinList,Cores), | |
236 | conjunct_predicates(MinList,CorePredicate). | |
237 | ||
238 | :- use_module(library(terms),[term_size/2]). | |
239 | compare_length(List1,List2) :- | |
240 | length(List1,L1), | |
241 | length(List2,L2), | |
242 | ( L1 < L2 -> true | |
243 | ; L1 = L2 -> term_size(List1,T1), term_size(List2,T2), T1 < T2). |