| 1 | % (c) 2009-2024 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_list_with_time_limit/5, unsat_chr_core_list_with_auto_time_limit/5, | |
| 8 | unsat_core_wth_auto_time_limit/5, | |
| 9 | unsat_core_with_fixed_conjuncts/3, unsat_chr_core_with_fixed_conjuncts_auto_time_limit/4, | |
| 10 | minimum_unsat_core/2, | |
| 11 | minimum_unsat_core_with_fixed_conjuncts/3, | |
| 12 | tcltk_unsat_core_properties/3, unsat_core_properties_table/1, | |
| 13 | quick_bup_core_up_to/4, quick_bup_core/4]). | |
| 14 | ||
| 15 | :- use_module(library(terms),[term_size/2]). | |
| 16 | :- use_module(library(between),[between/3]). | |
| 17 | :- use_module(library(ordsets),[ord_intersect/2, ord_union/3]). | |
| 18 | :- use_module(library(lists),[min_member/3, reverse/2, select/3, last/2, maplist/2, maplist/3, nth1/3]). | |
| 19 | ||
| 20 | :- use_module(probsrc(bsyntaxtree)). | |
| 21 | :- use_module(probsrc(solver_interface), [solve_predicate/5]). | |
| 22 | :- use_module(probsrc(preferences), [get_preference/2]). | |
| 23 | :- use_module(probsrc(debug), [debug_println/2, debug_print/1,debug_format/3, silent_mode/1, set_silent_mode/1, formatsilent/2]). | |
| 24 | :- use_module(probsrc(self_check), [assert_must_succeed/1,assert_must_fail/1]). | |
| 25 | :- use_module(probsrc(translate),[translate_bexpression_with_limit/3, set_unicode_mode/0, unset_unicode_mode/0]). | |
| 26 | :- use_module(probsrc(specfile),[get_specification_description/2]). | |
| 27 | :- use_module(probsrc(error_manager),[get_tk_table_position_info/2,add_warning/4, add_message/4,add_internal_error/2]). | |
| 28 | :- use_module(probsrc(tools_strings),[ajoin/2]). | |
| 29 | :- use_module(probsrc(preferences), [temporary_set_preference/3, reset_temporary_preference/2]). | |
| 30 | :- use_module(probsrc(solver_interface), [solve_predicate/4]). | |
| 31 | :- use_module(probsrc(tools),[split_list/4]). | |
| 32 | ||
| 33 | :- use_module(cdclt_solver('cdclt_solver'), [cdclt_solve_predicate/3]). | |
| 34 | :- use_module(smt_solvers_interface(smt_solvers_interface),[smt_solve_predicate/5]). | |
| 35 | ||
| 36 | :- use_module(probsrc(module_information),[module_info/2]). | |
| 37 | :- module_info(group,cbc). | |
| 38 | :- module_info(description,'Computation of unsatisfiable cores of predicates.'). | |
| 39 | ||
| 40 | % possible options are: | |
| 41 | % - keep_exact_result: keep exact top-level result obtained for entire predicate (e.g., to find cause of time-out) | |
| 42 | % - no_warning_if_sol_found | |
| 43 | % - ignore_if_sol_found: potentially dangerous and one has to check manually that GlobalRes is a contradiction | |
| 44 | % - auto_time_out_factor(Factor) | |
| 45 | % - fixed_conjuncts(FixedList) | |
| 46 | % - branch_and_bound | |
| 47 | % - inspect_nested_conjuncts(BOOL) (default true) | |
| 48 | % - inspect_quantifiers(BOOL) (default true) | |
| 49 | ||
| 50 | ||
| 51 | :- assert_must_succeed((unsat_core(b(falsity,pred,[]),Core), (ground(Core), Core = b(falsity,pred,_)))). | |
| 52 | :- assert_must_succeed((unsat_core(b(conjunct(b(falsity,pred,[]),b(truth,pred,[])),pred,[]),Core), (ground(Core), Core = b(falsity,pred,_)))). | |
| 53 | ||
| 54 | % for meta_interface and ProB2: | |
| 55 | unsat_core_properties_table(list([list([PropsHeader,'Source'])|ResList])) :- | |
| 56 | get_preference(translation_limit_for_table_commands,Limit), | |
| 57 | get_specification_description(properties,PROPS), | |
| 58 | unsat_core_of_properties(CorePredicates,[no_warning_if_sol_found],StrRes), | |
| 59 | ajoin([PROPS,' : ',StrRes],PropsHeader), | |
| 60 | set_unicode_mode, | |
| 61 | call_cleanup(findall(list([TS,PosInfo]), | |
| 62 | (member(CP,CorePredicates), translate_bexpression_with_limit(CP,Limit,TS), | |
| 63 | get_tk_table_position_info(CP,PosInfo)),ResList), | |
| 64 | unset_unicode_mode). | |
| 65 | ||
| 66 | % HasUCLabels is true if the CorePredicates have UnsatCore special labels like @TO, @WD, ... | |
| 67 | tcltk_unsat_core_properties(list(CorePredStrings),HasUCLabels,StrRes) :- | |
| 68 | % TO DO: transmit runtime from Runtime to FINALISE SETUP_CONSTANTS to avoid re-checking Properties | |
| 69 | unsat_core_of_properties(CorePredicates,[],StrRes), | |
| 70 | set_unicode_mode, | |
| 71 | call_cleanup(maplist(translate:translate_bexpression,CorePredicates,CorePredStrings), | |
| 72 | unset_unicode_mode), | |
| 73 | (member(CP,CorePredicates), pred_has_unsat_core_label(CP,_) -> HasUCLabels=true ; HasUCLabels=false), | |
| 74 | maplist(add_warn,CorePredicates). % so that we see the spans of the unsat core in the edit window | |
| 75 | ||
| 76 | unsat_core_of_properties(CorePredicates,Options,StrRes) :- | |
| 77 | bmachine:b_get_properties_from_machine(Properties), % TO DO: also provide for unsat component | |
| 78 | debug_print('Computing (efficient) unsat core for PROPERTIES'),nl, | |
| 79 | unsat_chr_core_list_with_auto_time_limit(Properties,5000,Options,GlobalResult,CorePredicates), | |
| 80 | (explain_result(GlobalResult,Explanation) -> StrRes=Explanation ; StrRes='**UNKNOWN**'). | |
| 81 | ||
| 82 | add_warn(Conjunct) :- | |
| 83 | add_warning(unsat_cores,'This is part of an unsatisfiable core of the PROPERTIES clause: ',Conjunct,Conjunct). | |
| 84 | ||
| 85 | ||
| 86 | % TODO: cleanup / rewrite predicate in order to minimize cores | |
| 87 | % i.e. implications could be rewritten into conjuncts | |
| 88 | ||
| 89 | :- assert_must_fail((minimum_unsat_core(b(conjunct(b(falsity,pred,[]), | |
| 90 | b(conjunct(b(less(b(integer(1),integer,[]),b(identifier(x),integer,[])),pred,[]), | |
| 91 | b(less(b(identifier(x),integer,[]),b(integer(1),integer,[])),pred,[])),pred,[])),pred,[]),Core), | |
| 92 | (ground(Core), Core = b(less(b(integer(1),integer,[]),b(identifier(x),integer,[])),pred,_)))). | |
| 93 | :- assert_must_fail((minimum_unsat_core(b(conjunct(b(falsity,pred,[]), | |
| 94 | 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), | |
| 95 | (ground(Core), Core = b(less(b(identifier(x),integer,[]),b(integer(1),integer,[])),pred,_)))). | |
| 96 | % there should be two cores | |
| 97 | :- assert_must_succeed((findall(Core, unsat_core(b(conjunct(b(falsity,pred,[]), | |
| 98 | 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), | |
| 99 | ListOfCores), length(ListOfCores,2))). % was 5 | |
| 100 | ||
| 101 | % call if you know how much time (in ms) it took to find inconsistency in Predicate | |
| 102 | unsat_core_list_with_time_limit(Predicate,TimeToFindContradiction,Options,GlobalRes, CorePredicates) :- | |
| 103 | temporary_set_timeout(TimeToFindContradiction,CHNG1), | |
| 104 | % this time will be multiplied by 2 below | |
| 105 | call_cleanup(unsat_core_list(Predicate,Options,GlobalRes,CorePredicates), | |
| 106 | reset_temporary_preference(time_out,CHNG1)). | |
| 107 | ||
| 108 | ||
| 109 | unsat_chr_core_list_with_auto_time_limit(Predicate,MaxTime,Options,GlobalRes,CorePredicates) :- | |
| 110 | temporary_set_preference(use_chr_solver,true,CHNG1), | |
| 111 | call_cleanup(unsat_core_wth_auto_time_limit(Predicate,MaxTime,Options,GlobalRes,CorePredicates), | |
| 112 | reset_temporary_preference(use_chr_solver,CHNG1)). | |
| 113 | ||
| 114 | % automatically determine time limit by checking that full predicate is false and registering time | |
| 115 | unsat_core_wth_auto_time_limit(Predicate,MaxTime,Options,GlobalRes,CorePredicates) :- | |
| 116 | % TODO: if unsat_core_target(.) provided and fixed time-out then we do not need to compute this: | |
| 117 | get_time_out_for_comp_pred(Predicate,_Nr,CompPred,TimeToFindContradiction,Options,GlobalRes), | |
| 118 | progress_info(GlobalRes), | |
| 119 | (solution_found(GlobalRes) | |
| 120 | -> ( member(no_warning_if_sol_found,Options) | |
| 121 | -> add_message(unsat_cores,'Predicate has a solution, unsat core cannot be computed: ',Predicate,Predicate) | |
| 122 | ; member(ignore_if_sol_found,Options) | |
| 123 | -> true | |
| 124 | ; add_warning(unsat_cores,'Predicate has a solution, unsat core cannot be computed: ',Predicate,Predicate) | |
| 125 | ), | |
| 126 | CorePredicates=[Predicate] | |
| 127 | ; (member(auto_time_out_factor(Factor),Options) -> true ; Factor=120), | |
| 128 | Limit0 is min(((TimeToFindContradiction*Factor)/100),MaxTime), %print(time_limit(Limit)),nl, | |
| 129 | (member(min_time_out(MinTime),Options) -> true ; MinTime = 5), | |
| 130 | Limit is max(MinTime,Limit0), | |
| 131 | (member(unsat_core_target(Target),Options) -> true ; Target = GlobalRes), | |
| 132 | % with unsat_core_target(contradiction_found) we can look for real contradictions even if the whole predicate has a time-out or translation error | |
| 133 | debug_format(19,'Time out: ~w ms, target for unsat core: ~w~n',[Limit,Target]), | |
| 134 | unsat_core_list_with_time_limit(CompPred,Limit,Options,Target,CorePredicates) | |
| 135 | ). | |
| 136 | ||
| 137 | %get_time_out_for_comp_pred(SubPred,1,SubPred,TimeToFindContradiction,Options,Res) :- !,get_time_out_for_pred(SubPred,TimeToFindContradiction,Options,Res). | |
| 138 | get_time_out_for_comp_pred(Predicate,Nr,SubPred,TimeToFindContradiction,Options,Res) :- % partition | |
| 139 | temporary_set_preference(partition_predicates_inline_equalities,false,OldValueOfPref), % avoid inlining equalities | |
| 140 | % TO DO: maybe provide an option for this | |
| 141 | call_cleanup(predicate_components(Predicate,Components), | |
| 142 | reset_temporary_preference(partition_predicates_inline_equalities, OldValueOfPref)), | |
| 143 | if( (nth1(Nr,Components,component(SubPred,Ids)), % select component via backtracking | |
| 144 | debug_println(19,examining_component(Nr,Ids)), | |
| 145 | get_time_out_for_pred(SubPred,TimeToFindContradiction,Options,Res), | |
| 146 | progress_info(Res), | |
| 147 | %print(sol_comp(Nr,Res)),nl, | |
| 148 | % TODO: if translation_or_setup_failed and target is contradiction_found: filter predicate to that part that can be translated | |
| 149 | \+ solution_found(Res)), | |
| 150 | % we have found a sub-component that has a contradiction | |
| 151 | true, | |
| 152 | (SubPred=Predicate, | |
| 153 | get_time_out_for_pred(SubPred,TimeToFindContradiction,Options,Res) | |
| 154 | ) | |
| 155 | ). | |
| 156 | ||
| 157 | get_time_out_for_pred(Predicate,TimeToFindContradiction,Options,Res) :- | |
| 158 | silent_mode(CurMode), set_silent_mode(on), | |
| 159 | statistics(walltime,[T1,_]), | |
| 160 | solve_core_pred(Predicate, 2, Options, Res), | |
| 161 | statistics(walltime,[T2,_]), TimeToFindContradiction is T2-T1, | |
| 162 | set_silent_mode(CurMode), !. | |
| 163 | ||
| 164 | temporary_set_timeout(TimeToFindContradiction,CHNG1) :- | |
| 165 | number(TimeToFindContradiction), TimeToFindContradiction>=0, | |
| 166 | NewTimeOut is round(TimeToFindContradiction+10), % in case we have 0; just add a few ms | |
| 167 | temporary_set_preference(time_out,NewTimeOut,CHNG1). | |
| 168 | ||
| 169 | unsat_core(Predicate,CorePredicate) :- | |
| 170 | unsat_core(Predicate,no_solution_found,CorePredicate). | |
| 171 | unsat_core(Predicate,GlobalResult,CorePredicate) :- | |
| 172 | unsat_core_list(Predicate,[],GlobalResult,CorePreds), | |
| 173 | conjunct_predicates(CorePreds,CorePredicate). | |
| 174 | ||
| 175 | unsat_core_list(Predicate,Options,GlobalResult,CorePreds) :- | |
| 176 | %print('COMPUTING CORE:'),nl,translate:nested_print_bexpr(Predicate),nl, | |
| 177 | %(member(fixed_conjuncts(FL),Options) -> print('FIXED CONJ:'),nl,translate:nested_print_bexpr(FL),nl ; true),nl, | |
| 178 | uc_conjunction_to_list(Predicate,Options,PredicateList), | |
| 179 | length(PredicateList,OrigLen), | |
| 180 | silent_mode(CurMode), set_silent_mode(on), | |
| 181 | call_cleanup(unsat_core_with_options_lists(PredicateList,Options,GlobalResult,CorePreds), | |
| 182 | set_silent_mode(CurMode)), | |
| 183 | ( CurMode = on | |
| 184 | -> true | |
| 185 | ; length(CorePreds,NewLen), | |
| 186 | debug_format(5, '~nFound core with ~w/~w conjuncts.~n', [NewLen,OrigLen]) | |
| 187 | ). | |
| 188 | ||
| 189 | % strip outermost existential quantifiers so that we can examine the conjunction inside | |
| 190 | uc_conjunction_to_list(b(exists(_V,Pred),pred,_), Options, List) :- | |
| 191 | member(inspect_quantifiers(true), Options), | |
| 192 | !, | |
| 193 | conjunction_to_list(Pred, List). | |
| 194 | % TO DO: add let_predicate (decomposed further below) ? forall ? | |
| 195 | uc_conjunction_to_list(Pred, _, List) :- conjunction_to_list(Pred, List). | |
| 196 | ||
| 197 | % called by ProB2 | |
| 198 | unsat_chr_core_with_fixed_conjuncts_auto_time_limit(Predicate,FixedConjuncts,MaxTimeLimit,CorePredicate) :- | |
| 199 | temporary_set_preference(use_chr_solver,true,CHNG1), % TODO: put into options ? | |
| 200 | Options = [], | |
| 201 | call_cleanup(unsat_core_with_fixed_conjuncts_auto_time_limit(Predicate,FixedConjuncts,MaxTimeLimit,Options,CorePredicate), | |
| 202 | reset_temporary_preference(use_chr_solver,CHNG1)). | |
| 203 | unsat_core_with_fixed_conjuncts_auto_time_limit(Predicate,FixedConjuncts,MaxTimeLimit,Options,CorePredicate) :- | |
| 204 | is_truth(FixedConjuncts),!, | |
| 205 | Options=[], | |
| 206 | unsat_core_wth_auto_time_limit(Predicate,MaxTimeLimit,Options,_,CorePreds), | |
| 207 | conjunct_predicates(CorePreds,CorePredicate). | |
| 208 | unsat_core_with_fixed_conjuncts_auto_time_limit(Predicate,FixedConjuncts,MaxTimeLimit,Options,CorePredicate) :- | |
| 209 | conjunct_predicates([Predicate,FixedConjuncts],FullPred), | |
| 210 | get_time_out_for_pred(FullPred,TimeToFindContradiction,Options,GlobalRes), % we cannot use component version due to FixedConjuncts | |
| 211 | progress_info(GlobalRes), | |
| 212 | (solution_found(GlobalRes) | |
| 213 | -> add_warning(unsat_cores,'Predicate has a solution, unsat core cannot be computed: ',Predicate,Predicate), | |
| 214 | CorePredicate=Predicate | |
| 215 | ; Limit is min((TimeToFindContradiction*110/100),MaxTimeLimit), | |
| 216 | temporary_set_timeout(Limit,CHNG1), | |
| 217 | call_cleanup(unsat_core_with_fixed_conjuncts(Predicate,FixedConjuncts,GlobalRes,CorePredicate), | |
| 218 | reset_temporary_preference(time_out,CHNG1)) | |
| 219 | ). | |
| 220 | ||
| 221 | unsat_core_with_fixed_conjuncts(P,FC,Core) :- unsat_core_with_fixed_conjuncts(P,FC,no_solution_found,Core). | |
| 222 | unsat_core_with_fixed_conjuncts(Predicate,FixedPreds,GlobalRes,CorePredicate) :- | |
| 223 | conjunction_to_list(FixedPreds,FixedList), | |
| 224 | Options = [fixed_conjuncts(FixedList)], % should we set inspect_nested_conjuncts(false) ? | |
| 225 | unsat_core_list(Predicate,Options,GlobalRes,CorePreds), | |
| 226 | conjunct_predicates(CorePreds,CorePredicate). | |
| 227 | ||
| 228 | unsat_core_with_options_lists(PredicateList,Options,GlobalResult,CorePreds) :- | |
| 229 | get_preference(unsat_core_algorithm,divide_and_conquer), !, % TO DO: pass GlobalResult | |
| 230 | temporary_set_preference(allow_enumeration_of_infinite_types,false,OldValueOfPref), | |
| 231 | (member(fixed_conjuncts(FixedList),Options) -> true ; FixedList=[]), | |
| 232 | call_cleanup(unsat_core_fixed_conjuncts_lists_divide_and_conquer(PredicateList,FixedList,GlobalResult,Options,CorePreds), | |
| 233 | reset_temporary_preference(allow_enumeration_of_infinite_types,OldValueOfPref)). | |
| 234 | unsat_core_with_options_lists(PredicateList,Options,GlobalResult,CorePreds) :- | |
| 235 | reset_max_core_size, | |
| 236 | temporary_set_preference(allow_enumeration_of_infinite_types,true, OldValueOfPref), | |
| 237 | %print('START: '),nl,translate:nested_print_bexpr(RPredicateList),nl, | |
| 238 | call_cleanup(unsat_core_with_options_linear(PredicateList,Options, GlobalResult, CorePreds), | |
| 239 | reset_temporary_preference(allow_enumeration_of_infinite_types, OldValueOfPref)), | |
| 240 | (member(branch_and_bound,Options) -> length(CorePreds,Len), set_max_core_size(Len) ; true). | |
| 241 | ||
| 242 | ||
| 243 | unsat_core_with_options_linear(PredicateList,Options, GlobalRes, CorePreds) :- | |
| 244 | reverse(PredicateList, RPredicateList), % so that we properly treat WD we start removing from the back | |
| 245 | compute_cores_linear(RPredicateList, Options, GlobalRes, CorePreds). | |
| 246 | ||
| 247 | compute_cores_linear(RPredicateList, Options, GlobalRes, CorePreds) :- | |
| 248 | compute_core_linear_loop(RPredicateList, 0, [], Options, GlobalRes, InCore,NotInCore,AllPreds),!, | |
| 249 | ( CorePreds = InCore | |
| 250 | ; % find more cores: | |
| 251 | debug_print('R'), | |
| 252 | restart_core_linear(InCore,NotInCore,AllPreds,Options,GlobalRes,CorePreds) | |
| 253 | ). | |
| 254 | ||
| 255 | % restart the unsat core algorithm with one conjunct from core removed from the original predicate list | |
| 256 | restart_core_linear([C|Cs],Keep,AllPreds,Options,GlobalRes,CorePreds) :- | |
| 257 | append(Keep,Cs,LL0), add_fixed_conj(Options,LL0,LL), | |
| 258 | conjunct_predicates(LL, ConjunctionToCheck), | |
| 259 | % print('TRY TO REMOVE CORE CONJUNCT FOR RESTART: '), translate:print_bexpr(C),nl, | |
| 260 | solve_core_pred(ConjunctionToCheck, 1, Options, Res), | |
| 261 | progress_info(Res), | |
| 262 | must_keep_conjunct(Res,GlobalRes,Options),!, | |
| 263 | % we need to keep C in PredicateList for restart; otherwise we change global result | |
| 264 | restart_core_linear(Cs,[C|Keep],AllPreds,Options,GlobalRes,CorePreds). | |
| 265 | restart_core_linear([C|_],_,AllPreds,Options,GlobalRes,CorePreds) :- | |
| 266 | % we can remove C from the global list | |
| 267 | (\+ get_preference(unsat_core_algorithm,divide_and_conquer) -> ! ; true), % linear_greedy | |
| 268 | remove_conjunct(C,AllPreds,NewAllPreds), % remove C, keeping original order | |
| 269 | debug_print('C'), | |
| 270 | compute_cores_linear(NewAllPreds, Options, GlobalRes, CorePreds). | |
| 271 | restart_core_linear([C|Cs],Keep,AllPreds,Options,GlobalRes,CorePreds) :- | |
| 272 | % try to remove another conjunct; we may find the same core multiple times | |
| 273 | restart_core_linear(Cs,[C|Keep],AllPreds,Options,GlobalRes,CorePreds). | |
| 274 | ||
| 275 | add_fixed_conj(Options,P,Res) :- member(fixed_conjuncts(FixedList),Options),!, | |
| 276 | (append(FixedList,P,FP) -> Res=FP | |
| 277 | ; add_internal_error('Illegal fixed list: ',FixedList), Res=P). | |
| 278 | add_fixed_conj(_,P,P). | |
| 279 | ||
| 280 | remove_conjunct(C,RPredicateList,NewRPredicateList) :- | |
| 281 | select(CC,RPredicateList,NewRPredicateList), % TO DO: remember position of C and use nth1 | |
| 282 | same_texpr(C,CC),!. | |
| 283 | remove_conjunct(C,RPredicateList,New) :- | |
| 284 | add_internal_error('Could not find conjunct from unsat core: ',remove_conjunct(C,RPredicateList,New)),fail. | |
| 285 | ||
| 286 | ||
| 287 | % implies_optional_hyp(C,DefinitelyInCore,_Hyp) | |
| 288 | % implied_by_core(C,DefinitelyInCore) | |
| 289 | % implies_optional_hyp(C,DefinitelyInCore,_Hyp) | |
| 290 | ||
| 291 | % simple unsat core computation: remove conjuncts till satisfiability is reached | |
| 292 | compute_core_linear_loop([], _,DefinitelyInCore, _Options, _, DefinitelyInCore,[],[]). | |
| 293 | compute_core_linear_loop([C|Cs], Counter,DefinitelyInCore, Options, GlobalRes, CorePreds,NotInCore,AllPreds) :- | |
| 294 | % remove C and check for satisfiability | |
| 295 | append(DefinitelyInCore,Cs,LL0), add_fixed_conj(Options,LL0,LL), | |
| 296 | conjunct_predicates(LL, ConjunctionToCheck), | |
| 297 | % print('TRY TO REMOVE: '), translate:print_bexpr(C),nl, | |
| 298 | solve_core_pred(ConjunctionToCheck, 1, Options, Res), | |
| 299 | debug_println(4, solve_predicate_result(Res)), | |
| 300 | progress_info(Res), | |
| 301 | must_keep_conjunct(Res,GlobalRes,Options), % a solution has been found or a time-out occured - C can not be removed; | |
| 302 | % normally corresponds to solve_result: contradiction_found or no_solution_found(unfixed_deferred_sets) | |
| 303 | !, | |
| 304 | % print('KEEPING: '), translate:print_bexpr(C),nl, | |
| 305 | % TO DO: when looking for minimal unsat core we could provide an upper-bound for the length | |
| 306 | increase_core_counter(Counter,Options,IncCtr), | |
| 307 | (can_be_further_decomposed(C, CA, CB), | |
| 308 | (member(inspect_nested_conjuncts(INC),Options) -> INC=true ; true) | |
| 309 | -> % print('% Split: '), translate:print_bexpr(CA),nl, print('% '),translate:print_bexpr(CB),nl, | |
| 310 | compute_core_linear_loop([CA,CB|Cs], Counter,DefinitelyInCore, Options, GlobalRes, CorePreds,NotInCore,AllPreds) | |
| 311 | ; add_uc_info(Res, C, IC), AllPreds = [C|TAP], | |
| 312 | append(DefinitelyInCore,[IC],NewDefInCore), % TODO: use DCG | |
| 313 | compute_core_linear_loop(Cs, IncCtr,NewDefInCore, Options, GlobalRes, CorePreds,NotInCore,TAP) | |
| 314 | ). | |
| 315 | compute_core_linear_loop([C|Cs], Ctr, DefinitelyInCore, Options, GlobalRes, CorePreds,NotInCore,[C|AllPreds]) :- | |
| 316 | % format('CAN BE REMOVED (~w): ',[GlobalRes]), translate:print_bexpr(C),nl, | |
| 317 | % C can be removed - we no longer introduce a choice point to not remove C; further cores are found by restarting | |
| 318 | NotInCore = [C|RestNotInCore], | |
| 319 | compute_core_linear_loop(Cs, Ctr, DefinitelyInCore, Options, GlobalRes, CorePreds,RestNotInCore,AllPreds). | |
| 320 | ||
| 321 | :- dynamic max_core_size/1. | |
| 322 | increase_core_counter(Cur,Options,_) :- max_core_size(Max), Cur >= Max, | |
| 323 | member(branch_and_bound,Options),!,format('B~w',[Max]),fail. | |
| 324 | increase_core_counter(Cur,_,C1) :- C1 is Cur+1. | |
| 325 | ||
| 326 | reset_max_core_size :- retractall(max_core_size(_)). | |
| 327 | set_max_core_size(Max) :- retractall(max_core_size(_)), assertz(max_core_size(Max)). | |
| 328 | ||
| 329 | % check if an optional hypothesis in the current core is implied by the rest and the new hyp C | |
| 330 | %implies_optional_hyp(C,CurrentCore,Hyp) :- | |
| 331 | % \+ is_truth(CurrentCore), | |
| 332 | % select(Hyp,CurrentCore,Rest), % DO THIS TEST also for C which must be kept | |
| 333 | % bsyntaxtree:get_texpr_info(Hyp,IL), member(optionally_in_core,IL), | |
| 334 | % % print(' --> '),translate:print_bexpr(Hyp), print(' <== '),translate:print_bexpr(Rest),nl, | |
| 335 | % prove_sequent(animation,Hyp,[C|Rest]). | |
| 336 | % | |
| 337 | %:- use_module(wdsrc(well_def_analyser),[prove_sequent/3]). | |
| 338 | %implied_by_core(C,CurrentCore) :- prove_sequent(animation,C,CurrentCore). | |
| 339 | ||
| 340 | ||
| 341 | add_uc_info(SolverRes, C, IC2) :- | |
| 342 | ( ( ground(SolverRes), | |
| 343 | SolverRes = solution(_), Labels = [], | |
| 344 | UCInfo = [description('definitely in unsat core (solution)')]) | |
| 345 | ; ( SolverRes == error, Labels = ['WD'], | |
| 346 | UCInfo = [description('definitely in unsat core (kept to prevent WD error)')]) | |
| 347 | ; ( SolverRes == time_out, Labels = ['TO'], % pretty printed as @TO | |
| 348 | UCInfo = [description('possibly in unsat core (kept to prevent timeout)')]) | |
| 349 | ; ( ground(SolverRes), Labels = ['VTO'], | |
| 350 | SolverRes = no_solution_found(enumeration_warning(_,_,_,_,_)), | |
| 351 | UCInfo = [description('possibly in unsat core (kept to prevent virtual timeout)')]) | |
| 352 | ; ( SolverRes == no_solution_found(unfixed_deferred_sets), Labels = ['DEFSETS'], | |
| 353 | UCInfo = [description('definitely in unsat core (kept to fix deferred sets)')]) | |
| 354 | ; ( ground(SolverRes), Labels = ['UNKNOWN'], | |
| 355 | SolverRes = no_solution_found(_), | |
| 356 | UCInfo = [description('possibly in unsat core (kept to prevent unknown solver result)')]) | |
| 357 | ), !, | |
| 358 | add_texpr_infos(C, UCInfo, IC1), | |
| 359 | add_labels_to_texpr(IC1,Labels,IC2). | |
| 360 | ||
| 361 | uc_label('WD'). | |
| 362 | uc_label('TO'). | |
| 363 | uc_label('VTO'). | |
| 364 | uc_label('DEFSETS'). | |
| 365 | ||
| 366 | pred_has_unsat_core_label(Pred,Label) :- get_texpr_label(Pred,Label), uc_label(Label). | |
| 367 | ||
| 368 | solution_found(Res) :- | |
| 369 | Res \= contradiction_found, | |
| 370 | Res \= no_solution_found(_), | |
| 371 | Res \= time_out, | |
| 372 | Res \= error, | |
| 373 | Res \= clpfd_overflow. | |
| 374 | ||
| 375 | % check if a removed conjunct has to be kept in unsat core given solver_result (w/o conjunct) and global result | |
| 376 | % possible value solution(_), contradiction_found, no_solution_found, ... | |
| 377 | must_keep_conjunct(solution(_),_,_) :- !. | |
| 378 | must_keep_conjunct(X,X,_) :- !,fail. % same result as global result, e.g., WD error or time_out | |
| 379 | must_keep_conjunct(_,_,Options) :- member(keep_exact_result,Options),!. | |
| 380 | must_keep_conjunct(contradiction_found,_,_) :- !,fail. % | |
| 381 | must_keep_conjunct(no_solution_found(X),GlobalRes,_) :- !, | |
| 382 | must_keep_no_sol_found(X,GlobalRes). | |
| 383 | must_keep_conjunct(_,_,_). | |
| 384 | ||
| 385 | must_keep_no_sol_found(enumeration_warning(_,_,_,_,critical),_). | |
| 386 | % relevant for e.g. :core f={1|->1} & x:dom(f) & f(x)>1 with -p TRY_FIND_ABORT TRUE | |
| 387 | must_keep_no_sol_found(solver_answered_unknown,_Global). % Global typically contradiction_found | |
| 388 | % TODO: look if there are other reasons where we should keep the conjunct | |
| 389 | ||
| 390 | can_be_further_decomposed(TE,A,B) :- can_be_further_decomposed(TE,positive,A,B). | |
| 391 | can_be_further_decomposed(b(E,pred,Info),NegPos,A,B) :- can_be_further_decomposed_aux(E,Info,NegPos,A,B). | |
| 392 | can_be_further_decomposed_aux(conjunct(A,B),_,positive,A,B). | |
| 393 | can_be_further_decomposed_aux(disjunct(A,B),_,negative,A,B). | |
| 394 | can_be_further_decomposed_aux(disjunct(A,B),_,positive,D1,D2) :- | |
| 395 | get_preference(unsat_core_algorithm,linear_greedy_decompose),!, % can blow up number of cases | |
| 396 | (can_be_further_decomposed(A,positive,A1,A2) % here we could try divide conjuncts in middle | |
| 397 | -> disjunct_predicates([A1,B],D1), | |
| 398 | disjunct_predicates([A2,B],D2) | |
| 399 | ; can_be_further_decomposed(B,positive,B1,B2) | |
| 400 | -> disjunct_predicates([A,B1],D1), | |
| 401 | disjunct_predicates([A,B2],D2) | |
| 402 | ). | |
| 403 | % above rule works for :core ((x=2&y=3) or (x=1&z=3)) & x>2 | |
| 404 | % for :core ((x=2 & y=3) or (x=3 & y=4)) & x>3 it sort of works but keeps both x/y | |
| 405 | can_be_further_decomposed_aux(implication(A,B),_,positive,I1,I2) :- | |
| 406 | (can_be_further_decomposed(B,positive,B1,B2) % A=>B1&B2 <--> A=>B1 & A=>B2 | |
| 407 | -> create_implication(A,B1,I1), | |
| 408 | create_implication(A,B2,I2) | |
| 409 | ; can_be_further_decomposed(A,negative,A1,A2) % (A1 or A2) => B <--> A1 => B & A2 => B | |
| 410 | -> create_implication(A1,B,I1), | |
| 411 | create_implication(A2,B,I2)). | |
| 412 | can_be_further_decomposed_aux(implication(A,B),_,negative,NA,B) :- % A=>B <--> not(A) or B | |
| 413 | create_negation(A,NA). | |
| 414 | can_be_further_decomposed_aux(negation(D),_,NegPos,NA,NB) :- neg_context(NegPos,PosNeg), | |
| 415 | can_be_further_decomposed(D,PosNeg,A,B), % not(A &/or B) <--> not(A) or/& not(B) | |
| 416 | create_negation(A,NA), | |
| 417 | create_negation(B,NB). | |
| 418 | can_be_further_decomposed_aux(let_predicate(V,E,P),Info,NegPos,LEA,LEB) :- | |
| 419 | can_be_further_decomposed(P,NegPos,A,B), | |
| 420 | LEA = b(let_predicate(V,E,A),pred,Info), % used_ids could be wrong; TO DO: think about exists | |
| 421 | LEB = b(let_predicate(V,E,B),pred,Info). | |
| 422 | can_be_further_decomposed_aux(lazy_let_pred(V,E,P),Info,NegPos,LEA,LEB) :- | |
| 423 | can_be_further_decomposed(P,NegPos,A,B), | |
| 424 | LEA = b(lazy_let_pred(V,E,A),pred,Info), | |
| 425 | LEB = b(lazy_let_pred(V,E,B),pred,Info). | |
| 426 | ||
| 427 | neg_context(positive,negative). neg_context(negative,positive). | |
| 428 | ||
| 429 | % a binary search algorithm in order to only need log(n) instead of n solver calls | |
| 430 | % Idea: split list of conjuncts in half, C = [A,B] | |
| 431 | unsat_core_fixed_conjuncts_lists_divide_and_conquer([],_,_,_,_) :- !, fail. % we split too far! | |
| 432 | unsat_core_fixed_conjuncts_lists_divide_and_conquer([C],_FixedConjuncts,_GlobalResult,_Options,[C]) :- | |
| 433 | !. % if there is only one conjunct left, it has to belong to the core | |
| 434 | unsat_core_fixed_conjuncts_lists_divide_and_conquer(Clauses,FixedConjuncts,GlobalResult,Options,Core) :- | |
| 435 | split_in_half(Clauses,A,B), | |
| 436 | % print('SPLIT: '), print(A),nl,print(B),nl, | |
| 437 | unsat_core_fixed_conjuncts_lists_divide_and_conquer_split(A,B,FixedConjuncts,GlobalResult,Options,Core). | |
| 438 | ||
| 439 | unsat_core_fixed_conjuncts_lists_divide_and_conquer_split(A,B,FixedConjuncts,GlobalResult,Options,Core) :- | |
| 440 | append(A,FixedConjuncts,AllConjuncts), | |
| 441 | conjunct_predicates(AllConjuncts,APred), | |
| 442 | % print('SOLVING LHS: '), translate:print_bexpr(APred),nl, | |
| 443 | solve_core_pred(APred, 1, Options, ARealRes), | |
| 444 | progress_info(ARealRes), | |
| 445 | % print(result(ARealRes)),nl, | |
| 446 | !, % do not backtrack into solving or multiple results can be found leading to duplicated cores | |
| 447 | unsat_core_fixed_conjuncts_lists_divide_and_conquer_recur1(ARealRes,A,B,FixedConjuncts,GlobalResult,Options,Core). | |
| 448 | ||
| 449 | progress_info(ARes) :- progress_info_aux(ARes),!,flush_output(user_output). | |
| 450 | progress_info_aux(time_out) :- progress_print('T'). | |
| 451 | progress_info_aux(error) :- progress_print('WD'). | |
| 452 | progress_info_aux(no_solution_found(E)) :- progress_info_no_sol_found_aux(E). | |
| 453 | progress_info_aux(contradiction_found) :- progress_print('-'). | |
| 454 | progress_info_aux(translation_or_setup_failed) :- progress_print('FAILED'). % Z3 or cvc4 translation failed | |
| 455 | progress_info_aux(solution(_)) :- progress_print('+'). | |
| 456 | progress_info_aux(clpfd_overflow) :- progress_print('O'). | |
| 457 | progress_info_aux(UNKNOWN) :- debug_format(5, '*~w*', [UNKNOWN]). | |
| 458 | ||
| 459 | %progress_print(C) :- !, write(C). | |
| 460 | progress_print(C) :- debug_print(C). | |
| 461 | ||
| 462 | progress_info_no_sol_found_aux(unfixed_deferred_sets) :- progress_print('-'). | |
| 463 | progress_info_no_sol_found_aux(solver_answered_unknown) :- progress_print('U'). | |
| 464 | progress_info_no_sol_found_aux(enumeration_warning(_,_,_,_,_)) :- progress_print('U(ENUM)'). | |
| 465 | progress_info_no_sol_found_aux(UNKNOWN) :- debug_format(5, '*~w*', [UNKNOWN]). | |
| 466 | ||
| 467 | explain_result(time_out,'UNKNOWN (TIME_OUT)'). | |
| 468 | explain_result(error,'UNKNOWN (ERROR)'). | |
| 469 | explain_result(clpfd_overflow,'UNKNOWN (CLPFD OVERFLOW)'). | |
| 470 | explain_result(no_solution_found(E),R) :- explain_no_sol(E,R). | |
| 471 | explain_result(contradiction_found,'FALSE'). | |
| 472 | explain_result(solution(_),'TRUE'). | |
| 473 | explain_result(_,'UNKNOWN'). | |
| 474 | ||
| 475 | explain_no_sol(solver_answered_unknown, 'UNKNOWN'). | |
| 476 | explain_no_sol(unfixed_deferred_sets,'FALSE (DEFERRED SETS)'). | |
| 477 | explain_no_sol(enumeration_warning(_,_,_,_,_), 'UNKNOWN (ENUMERATION WARNING)'). | |
| 478 | explain_no_sol(_, 'UNKNOWN'). | |
| 479 | ||
| 480 | definite_prob_result(solution(_),_). | |
| 481 | definite_prob_result(Res,Options) :- contradiction_result(Res,Options). | |
| 482 | ||
| 483 | solve_core_pred(BPred,_TOFactor,Options,Res) :- % translate:print_bexpr(BPred),nl, | |
| 484 | memberchk(try_prob_solver_first(TimeoutFactor),Options), | |
| 485 | solve_predicate(BPred,_State,TimeoutFactor,Res), | |
| 486 | formatsilent('ProB solve_predicate result : ~w~n',[Res]), | |
| 487 | definite_prob_result(Res,Options), !. | |
| 488 | solve_core_pred(BPred,TOFactor,Options,Res) :- % print(' --> Z3 SOLVE: '), translate:print_bexpr(BPred),nl, | |
| 489 | member(use_smt_solver(Solver),Options),!, | |
| 490 | Opts = [smt_time_out_factor(TOFactor), check_sat_skeleton(10), instantiate_quantifier_limit(5)], | |
| 491 | %formatsilent('Starting SMT solver ~w with ~w~n',[Solver,Opts]), | |
| 492 | smt_solve_predicate(Solver,Opts,BPred,_,Res), | |
| 493 | formatsilent('~w solve_predicate result : ~w~n',[Solver,Res]). | |
| 494 | solve_core_pred(BPred,_TOFactor,Options,Res) :- | |
| 495 | member(use_cdclt_solver,Options),!, % TODO: pass TOFactor to cdclt | |
| 496 | (cdclt_solve_predicate(BPred,_,Res) -> true | |
| 497 | ; Res= contradiction_found, | |
| 498 | add_internal_error('Solver call failed:',cdclt_solve_predicate(BPred,_,Res)) | |
| 499 | ). | |
| 500 | % TODO: add wd-prover | |
| 501 | solve_core_pred(BPred,TOFactor,Options,Res) :- | |
| 502 | (member(use_smt_mode/SMT,Options) -> true ; SMT=true), | |
| 503 | (member(use_clpfd_solver/CLPFD,Options) -> true ; CLPFD=true), | |
| 504 | (member(use_chr_solver/CHR,Options) -> T=[use_chr_solver/CHR] ; T=[]), | |
| 505 | solve_predicate(BPred,_BState,TOFactor,[use_smt_mode/SMT,use_clpfd_solver/CLPFD,ignore_wd_errors|T],Res). | |
| 506 | ||
| 507 | ||
| 508 | unsat_core_fixed_conjuncts_lists_divide_and_conquer_recur1(ARealRes,A,_B,FixedConjuncts,GlobalResult,Options,Core) :- | |
| 509 | \+ must_keep_conjunct(ARealRes,GlobalResult,[]), % A is (virtually / effectively) unsat. Recur on A. | |
| 510 | unsat_core_fixed_conjuncts_lists_divide_and_conquer(A,FixedConjuncts,GlobalResult,Options,Core). | |
| 511 | unsat_core_fixed_conjuncts_lists_divide_and_conquer_recur1(ARealRes,A,B,FixedConjuncts,GlobalResult,Options,Core) :- | |
| 512 | append(B,FixedConjuncts,AllConjuncts), | |
| 513 | conjunct_predicates(AllConjuncts,BPred), | |
| 514 | % print('SOLVING RHS: '), translate:print_bexpr(BPred),nl, | |
| 515 | solve_core_pred(BPred,1,Options,BRealRes), | |
| 516 | progress_info(BRealRes), | |
| 517 | % print(result(BRealRes)),nl, | |
| 518 | !, | |
| 519 | unsat_core_fixed_conjuncts_lists_divide_and_conquer_recur2(ARealRes,BRealRes,A,B,FixedConjuncts,GlobalResult,Options,Core). | |
| 520 | ||
| 521 | unsat_core_fixed_conjuncts_lists_divide_and_conquer_recur2(_ARealRes,BRealRes,_A,B,FixedConjuncts,GlobalResult,Options,Core) :- | |
| 522 | \+ must_keep_conjunct(BRealRes,GlobalResult,[]), % B is (virtually / effectively) unsat. Recur on B. | |
| 523 | !, | |
| 524 | unsat_core_fixed_conjuncts_lists_divide_and_conquer(B,FixedConjuncts,GlobalResult,Options,Core). | |
| 525 | unsat_core_fixed_conjuncts_lists_divide_and_conquer_recur2(ARealRes,BRealRes,A,B,FixedConjuncts,GlobalResult,Options,Core) :- | |
| 526 | % the interesting case: if both are sat | |
| 527 | must_keep_conjunct(ARealRes,GlobalResult,[]), | |
| 528 | must_keep_conjunct(BRealRes,GlobalResult,[]), | |
| 529 | % minimize A assuming usat core includes B | |
| 530 | append(B,FixedConjuncts,FixedAndB), | |
| 531 | unsat_core_fixed_conjuncts_lists_divide_and_conquer(A,FixedAndB,GlobalResult,Options,ACore), | |
| 532 | % now ACore & B is unsat and minimal but not minimum core | |
| 533 | % minimize B assuming ACore | |
| 534 | append(ACore,FixedConjuncts,FixedAndA), | |
| 535 | unsat_core_fixed_conjuncts_lists_divide_and_conquer(B,FixedAndA,GlobalResult,Options,BCore), | |
| 536 | append(ACore,BCore,Core). | |
| 537 | ||
| 538 | %divide_and_conquer_recur_condition(contradiction_found). | |
| 539 | %divide_and_conquer_recur_condition(no_solution_found(X)) :- | |
| 540 | % % to do: if the outermost conjunct already generates a time_out or critical enumeration warning then this should be enabled as a recur condition | |
| 541 | % X \= enumeration_warning(_,_,_,_,critical). | |
| 542 | %%divide_and_conquer_recur_condition(time_out). | |
| 543 | ||
| 544 | split_in_half(C, A, B) :- | |
| 545 | length(C,L), | |
| 546 | Half is L // 2, | |
| 547 | length(A, Half), | |
| 548 | append(A, B, C). | |
| 549 | ||
| 550 | % there is currently no known good algorithm to compute the minimum unsat core | |
| 551 | % we can just compute every core and take the minimum one out of the list | |
| 552 | :- assert_must_succeed((minimum_unsat_core(b(conjunct(b(falsity,pred,[]), | |
| 553 | 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), | |
| 554 | (ground(Core), Core = b(falsity,pred,_)))). | |
| 555 | minimum_unsat_core(Predicate,CorePredicate) :- | |
| 556 | minimum_unsat_core_with_fixed_conjuncts(Predicate,[],CorePredicate). | |
| 557 | ||
| 558 | minimum_unsat_core_with_fixed_conjuncts(Predicate,FixedConjuncts,CorePredicate) :- | |
| 559 | Options = [branch_and_bound,fixed_conjuncts(FixedConjuncts)], | |
| 560 | findall(CoreList, | |
| 561 | unsat_core_list(Predicate,Options,no_solution_found,CoreList), | |
| 562 | Cores), | |
| 563 | reset_max_core_size, | |
| 564 | min_member(compare_length,MinCs,Cores), | |
| 565 | conjunct_predicates(MinCs,CorePredicate). | |
| 566 | ||
| 567 | compare_length(P1,P2) :- length(P1,L1), length(P2,L2), | |
| 568 | (L1<L2 -> true | |
| 569 | ; L1=L2 -> | |
| 570 | term_size(P1, T1), | |
| 571 | term_size(P2, T2), | |
| 572 | T1 < T2 | |
| 573 | ). | |
| 574 | ||
| 575 | % ---------------------------------- | |
| 576 | ||
| 577 | % quick_bup_core | |
| 578 | ||
| 579 | % finding small unsat cores bottom-up by looking for 1, 2, ... conjuncts and looking for contradiction_found | |
| 580 | % useful e.g. for Z3 where some conjuncts are complex and lead to time outs or translation failed errors | |
| 581 | % could also be used with WD prover instead or in addition to Z3 | |
| 582 | % currently cannot be used to find unsat core for timeout or unknown result | |
| 583 | % useful as a "canary" for PROPERTIES/axioms as a quick check or as additional quick check | |
| 584 | ||
| 585 | ||
| 586 | preprocess_conjuncts([],_,_,[]). | |
| 587 | preprocess_conjuncts([Conj|T],Nr,Options,ListResult) :- | |
| 588 | format(' ==> Pre-processing conjunct ~w and checking for individual inconsistency~n',[Nr]), | |
| 589 | %translate:print_bexpr(Conj),nl, | |
| 590 | % we could =remove try_prob_solver_first(_) from Options, if we want to filter non-translatable conjuncts! | |
| 591 | solve_core_pred(Conj, 0.02, Options, Res), | |
| 592 | (explain_result(Res,Expl) -> debug_format(19,'Result for conjunct ~w: ~w (~w)~n',[Nr,Expl,Res])), | |
| 593 | N1 is Nr+1, | |
| 594 | (should_remove_conjunct(Res) | |
| 595 | -> % remove this conjunct; it can only disturb finding a core for a contradiction | |
| 596 | preprocess_conjuncts(T,N1,Options,ListResult) | |
| 597 | ; find_identifier_uses(Conj,[],UsedIds), | |
| 598 | ListResult = [conj(Nr,Conj,Res,UsedIds)|PT], | |
| 599 | (contradiction_result(Res,Options) | |
| 600 | -> PT=[] % stop processing, we have found an unsat core of a single conjunct | |
| 601 | ; preprocess_conjuncts(T,N1,Options,PT)) | |
| 602 | ). | |
| 603 | ||
| 604 | should_remove_conjunct(no_solution_found(translation_failed)). | |
| 605 | ||
| 606 | contradiction_result(contradiction_found,_). | |
| 607 | contradiction_result(no_solution_found(unfixed_deferred_sets),Options) :- | |
| 608 | member(allow_unfixed_deferred_sets,Options). | |
| 609 | ||
| 610 | quick_bup_core_up_to(Typed,MaxSize,CoreList,Result) :- | |
| 611 | quick_bup_core(Typed,[use_smt_solver(z3axm), | |
| 612 | maximum_core_size(MaxSize), | |
| 613 | try_prob_solver_first(fixed_time_out(5))], | |
| 614 | CoreList,Result). | |
| 615 | ||
| 616 | quick_bup_core(Predicate,Options,CoreList,Result) :- | |
| 617 | uc_conjunction_to_list(Predicate,Options,List), | |
| 618 | preprocess_conjuncts(List,1,Options,ProcessedList), | |
| 619 | (last(ProcessedList,conj(_,Last,LR,_)), | |
| 620 | contradiction_result(LR,Options) | |
| 621 | -> CoreList = [Last], Result=LR | |
| 622 | ; (member(maximum_core_size(MaxN),Options) -> true ; MaxN=3), | |
| 623 | between(2,MaxN,N), | |
| 624 | format(' ==> Finding cores of length ~w~n',[N]), | |
| 625 | contradiction_check(N,ProcessedList,Options,CoreList,Result) -> true | |
| 626 | ). | |
| 627 | ||
| 628 | ||
| 629 | ||
| 630 | select_core_target(N,List,Res) :- | |
| 631 | append(_,[conj(Nr,ConjN,_,UsedIdsN)|Rest],List), % now only use conjuncts to the right of ConjN | |
| 632 | format(' ==> finding (~w-ary) conflicts with conjunct ~w: ',[N,Nr]),translate:print_bexpr(ConjN),nl, | |
| 633 | N1 is N-1, | |
| 634 | select_core_target(N1,Rest,[ConjN],UsedIdsN,Res). | |
| 635 | ||
| 636 | has_common_ids(UsedIdsSoFar,conj(_,_,_,UsedIdsN)) :- ord_intersect(UsedIdsSoFar,UsedIdsN). | |
| 637 | ||
| 638 | % select a core target list of predicates of length N | |
| 639 | % TODO: this can still generate the same conjunct multiple times?? | |
| 640 | select_core_target(0,_,Core,_,Res) :- !, Res=Core. | |
| 641 | select_core_target(N,List,CoreSoFar,UsedIdsSoFar,Res) :- %print(n(N,UsedIdsSoFar)),nl, | |
| 642 | split_list(has_common_ids(UsedIdsSoFar),List,CommonList,DisjList), | |
| 643 | append(_,[conj(_Nr,ConjN,_,UsedIdsN)|Rest],CommonList), % only choose conjuncts with common ids larger than Nr | |
| 644 | %print(selected_conj(_Nr)),nl, translate:print_bexpr(ConjN),nl, | |
| 645 | append(Rest,DisjList,RestList), | |
| 646 | ord_union(UsedIdsN,UsedIdsSoFar,New), | |
| 647 | N1 is N-1, | |
| 648 | select_core_target(N1,RestList,[ConjN|CoreSoFar],New,Res). | |
| 649 | ||
| 650 | contradiction_check(N,ProcessedList,Options,CoreList,Res) :- | |
| 651 | select_core_target(N,ProcessedList,CoreList), | |
| 652 | conjunct_predicates(CoreList,Core), | |
| 653 | %nl,translate:print_bexpr(Core),nl,nl, | |
| 654 | solve_core_pred(Core, 0.02, Options, Res), | |
| 655 | progress_info(Res), | |
| 656 | contradiction_result(Res,Options). | |
| 657 | ||
| 658 | % could use WD prover as additional task: | |
| 659 | % >>> :prove x:NATURAL --> NATURAL => not(-1:ran(x)) | |
| 660 | % Universally quantified predicate is PROVED with [prob-wd-prover(no_double_check)] | |
| 661 | ||
| 662 | % example where we need three conjuncts: :z3-axm-qcore x<y & y<10 & x<10 & y+n<x & n=0 |