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