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