| 1 | % (c) 2009-2026 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 | % deactivate strict_raise_enum_warnings: when doing unsat core we often get enum warnings due to missing conjuncts | |
| 182 | temporary_set_preference(strict_raise_enum_warnings,false,OLD), % relevant for cdclt tests like 2167, ... | |
| 183 | call_cleanup(unsat_core_with_options_lists(PredicateList,Options,GlobalResult,CorePreds), | |
| 184 | (reset_temporary_preference(strict_raise_enum_warnings,OLD), | |
| 185 | set_silent_mode(CurMode))), | |
| 186 | ( CurMode = on | |
| 187 | -> true | |
| 188 | ; length(CorePreds,NewLen), | |
| 189 | debug_format(5, '~nFound core with ~w/~w conjuncts.~n', [NewLen,OrigLen]) | |
| 190 | ). | |
| 191 | ||
| 192 | % strip outermost existential quantifiers so that we can examine the conjunction inside | |
| 193 | uc_conjunction_to_list(b(exists(_V,Pred),pred,_), Options, List) :- | |
| 194 | member(inspect_quantifiers(true), Options), | |
| 195 | !, | |
| 196 | conjunction_to_list(Pred, List). | |
| 197 | % TO DO: add let_predicate (decomposed further below) ? forall ? | |
| 198 | uc_conjunction_to_list(Pred, _, List) :- conjunction_to_list(Pred, List). | |
| 199 | ||
| 200 | % called by ProB2 | |
| 201 | unsat_chr_core_with_fixed_conjuncts_auto_time_limit(Predicate,FixedConjuncts,MaxTimeLimit,CorePredicate) :- | |
| 202 | temporary_set_preference(use_chr_solver,true,CHNG1), % TODO: put into options ? | |
| 203 | Options = [], | |
| 204 | call_cleanup(unsat_core_with_fixed_conjuncts_auto_time_limit(Predicate,FixedConjuncts,MaxTimeLimit,Options,CorePredicate), | |
| 205 | reset_temporary_preference(use_chr_solver,CHNG1)). | |
| 206 | unsat_core_with_fixed_conjuncts_auto_time_limit(Predicate,FixedConjuncts,MaxTimeLimit,Options,CorePredicate) :- | |
| 207 | is_truth(FixedConjuncts),!, | |
| 208 | Options=[], | |
| 209 | unsat_core_wth_auto_time_limit(Predicate,MaxTimeLimit,Options,_,CorePreds), | |
| 210 | conjunct_predicates(CorePreds,CorePredicate). | |
| 211 | unsat_core_with_fixed_conjuncts_auto_time_limit(Predicate,FixedConjuncts,MaxTimeLimit,Options,CorePredicate) :- | |
| 212 | conjunct_predicates([Predicate,FixedConjuncts],FullPred), | |
| 213 | get_time_out_for_pred(FullPred,TimeToFindContradiction,Options,GlobalRes), % we cannot use component version due to FixedConjuncts | |
| 214 | progress_info(GlobalRes), | |
| 215 | (solution_found(GlobalRes) | |
| 216 | -> add_warning(unsat_cores,'Predicate has a solution, unsat core cannot be computed: ',Predicate,Predicate), | |
| 217 | CorePredicate=Predicate | |
| 218 | ; Limit is min((TimeToFindContradiction*110/100),MaxTimeLimit), | |
| 219 | temporary_set_timeout(Limit,CHNG1), | |
| 220 | call_cleanup(unsat_core_with_fixed_conjuncts(Predicate,FixedConjuncts,GlobalRes,CorePredicate), | |
| 221 | reset_temporary_preference(time_out,CHNG1)) | |
| 222 | ). | |
| 223 | ||
| 224 | unsat_core_with_fixed_conjuncts(P,FC,Core) :- unsat_core_with_fixed_conjuncts(P,FC,no_solution_found,Core). | |
| 225 | unsat_core_with_fixed_conjuncts(Predicate,FixedPreds,GlobalRes,CorePredicate) :- | |
| 226 | conjunction_to_list(FixedPreds,FixedList), | |
| 227 | Options = [fixed_conjuncts(FixedList)], % should we set inspect_nested_conjuncts(false) ? | |
| 228 | unsat_core_list(Predicate,Options,GlobalRes,CorePreds), | |
| 229 | conjunct_predicates(CorePreds,CorePredicate). | |
| 230 | ||
| 231 | unsat_core_with_options_lists(PredicateList,Options,GlobalResult,CorePreds) :- | |
| 232 | get_preference(unsat_core_algorithm,divide_and_conquer), !, % TO DO: pass GlobalResult | |
| 233 | temporary_set_preference(allow_enumeration_of_infinite_types,false,OldValueOfPref), | |
| 234 | (member(fixed_conjuncts(FixedList),Options) -> true ; FixedList=[]), | |
| 235 | call_cleanup(unsat_core_fixed_conjuncts_lists_divide_and_conquer(PredicateList,FixedList,GlobalResult,Options,CorePreds), | |
| 236 | reset_temporary_preference(allow_enumeration_of_infinite_types,OldValueOfPref)). | |
| 237 | unsat_core_with_options_lists(PredicateList,Options,GlobalResult,CorePreds) :- | |
| 238 | reset_max_core_size, | |
| 239 | temporary_set_preference(allow_enumeration_of_infinite_types,true, OldValueOfPref), | |
| 240 | %print('START: '),nl,translate:nested_print_bexpr(RPredicateList),nl, | |
| 241 | call_cleanup(unsat_core_with_options_linear(PredicateList,Options, GlobalResult, CorePreds), | |
| 242 | reset_temporary_preference(allow_enumeration_of_infinite_types, OldValueOfPref)), | |
| 243 | (member(branch_and_bound,Options) -> length(CorePreds,Len), set_max_core_size(Len) ; true). | |
| 244 | ||
| 245 | ||
| 246 | unsat_core_with_options_linear(PredicateList,Options, GlobalRes, CorePreds) :- | |
| 247 | reverse(PredicateList, RPredicateList), % so that we properly treat WD we start removing from the back | |
| 248 | compute_cores_linear(RPredicateList, Options, GlobalRes, CorePreds). | |
| 249 | ||
| 250 | compute_cores_linear(RPredicateList, Options, GlobalRes, CorePreds) :- | |
| 251 | compute_core_linear_loop(RPredicateList, 0, [], Options, GlobalRes, InCore,NotInCore,AllPreds),!, | |
| 252 | ( CorePreds = InCore | |
| 253 | ; % find more cores: | |
| 254 | debug_print('R'), | |
| 255 | restart_core_linear(InCore,NotInCore,AllPreds,Options,GlobalRes,CorePreds) | |
| 256 | ). | |
| 257 | ||
| 258 | % restart the unsat core algorithm with one conjunct from core removed from the original predicate list | |
| 259 | restart_core_linear([C|Cs],Keep,AllPreds,Options,GlobalRes,CorePreds) :- | |
| 260 | append(Keep,Cs,LL0), add_fixed_conj(Options,LL0,LL), | |
| 261 | conjunct_predicates(LL, ConjunctionToCheck), | |
| 262 | % print('TRY TO REMOVE CORE CONJUNCT FOR RESTART: '), translate:print_bexpr(C),nl, | |
| 263 | solve_core_pred(ConjunctionToCheck, 1, Options, Res), | |
| 264 | progress_info(Res), | |
| 265 | must_keep_conjunct(Res,GlobalRes,Options),!, | |
| 266 | % we need to keep C in PredicateList for restart; otherwise we change global result | |
| 267 | restart_core_linear(Cs,[C|Keep],AllPreds,Options,GlobalRes,CorePreds). | |
| 268 | restart_core_linear([C|_],_,AllPreds,Options,GlobalRes,CorePreds) :- | |
| 269 | % we can remove C from the global list | |
| 270 | (\+ get_preference(unsat_core_algorithm,divide_and_conquer) -> ! ; true), % linear_greedy | |
| 271 | remove_conjunct(C,AllPreds,NewAllPreds), % remove C, keeping original order | |
| 272 | debug_print('C'), | |
| 273 | compute_cores_linear(NewAllPreds, Options, GlobalRes, CorePreds). | |
| 274 | restart_core_linear([C|Cs],Keep,AllPreds,Options,GlobalRes,CorePreds) :- | |
| 275 | % try to remove another conjunct; we may find the same core multiple times | |
| 276 | restart_core_linear(Cs,[C|Keep],AllPreds,Options,GlobalRes,CorePreds). | |
| 277 | ||
| 278 | add_fixed_conj(Options,P,Res) :- member(fixed_conjuncts(FixedList),Options),!, | |
| 279 | (append(FixedList,P,FP) -> Res=FP | |
| 280 | ; add_internal_error('Illegal fixed list: ',FixedList), Res=P). | |
| 281 | add_fixed_conj(_,P,P). | |
| 282 | ||
| 283 | remove_conjunct(C,RPredicateList,NewRPredicateList) :- | |
| 284 | select(CC,RPredicateList,NewRPredicateList), % TO DO: remember position of C and use nth1 | |
| 285 | same_texpr(C,CC),!. | |
| 286 | remove_conjunct(C,RPredicateList,New) :- | |
| 287 | add_internal_error('Could not find conjunct from unsat core: ',remove_conjunct(C,RPredicateList,New)),fail. | |
| 288 | ||
| 289 | ||
| 290 | % implies_optional_hyp(C,DefinitelyInCore,_Hyp) | |
| 291 | % implied_by_core(C,DefinitelyInCore) | |
| 292 | % implies_optional_hyp(C,DefinitelyInCore,_Hyp) | |
| 293 | ||
| 294 | % simple unsat core computation: remove conjuncts till satisfiability is reached | |
| 295 | compute_core_linear_loop([], _,DefinitelyInCore, _Options, _, DefinitelyInCore,[],[]). | |
| 296 | compute_core_linear_loop([C|Cs], Counter,DefinitelyInCore, Options, GlobalRes, CorePreds,NotInCore,AllPreds) :- | |
| 297 | % remove C and check for satisfiability | |
| 298 | append(DefinitelyInCore,Cs,LL0), add_fixed_conj(Options,LL0,LL), | |
| 299 | conjunct_predicates(LL, ConjunctionToCheck), | |
| 300 | % print('TRY TO REMOVE: '), translate:print_bexpr(C),nl, | |
| 301 | solve_core_pred(ConjunctionToCheck, 1, Options, Res), | |
| 302 | debug_println(4, solve_predicate_result(Res)), | |
| 303 | progress_info(Res), | |
| 304 | must_keep_conjunct(Res,GlobalRes,Options), % a solution has been found or a time-out occured - C can not be removed; | |
| 305 | % normally corresponds to solve_result: contradiction_found or no_solution_found(unfixed_deferred_sets) | |
| 306 | !, | |
| 307 | % print('KEEPING: '), translate:print_bexpr(C),nl, | |
| 308 | % TO DO: when looking for minimal unsat core we could provide an upper-bound for the length | |
| 309 | increase_core_counter(Counter,Options,IncCtr), | |
| 310 | (can_be_further_decomposed(C, CA, CB), | |
| 311 | (member(inspect_nested_conjuncts(INC),Options) -> INC=true ; true) | |
| 312 | -> % print('% Split: '), translate:print_bexpr(CA),nl, print('% '),translate:print_bexpr(CB),nl, | |
| 313 | compute_core_linear_loop([CA,CB|Cs], Counter,DefinitelyInCore, Options, GlobalRes, CorePreds,NotInCore,AllPreds) | |
| 314 | ; add_uc_info(Res, C, IC), AllPreds = [C|TAP], | |
| 315 | append(DefinitelyInCore,[IC],NewDefInCore), % TODO: use DCG | |
| 316 | compute_core_linear_loop(Cs, IncCtr,NewDefInCore, Options, GlobalRes, CorePreds,NotInCore,TAP) | |
| 317 | ). | |
| 318 | compute_core_linear_loop([C|Cs], Ctr, DefinitelyInCore, Options, GlobalRes, CorePreds,NotInCore,[C|AllPreds]) :- | |
| 319 | % format('CAN BE REMOVED (~w): ',[GlobalRes]), translate:print_bexpr(C),nl, | |
| 320 | % C can be removed - we no longer introduce a choice point to not remove C; further cores are found by restarting | |
| 321 | NotInCore = [C|RestNotInCore], | |
| 322 | compute_core_linear_loop(Cs, Ctr, DefinitelyInCore, Options, GlobalRes, CorePreds,RestNotInCore,AllPreds). | |
| 323 | ||
| 324 | :- dynamic max_core_size/1. | |
| 325 | increase_core_counter(Cur,Options,_) :- max_core_size(Max), Cur >= Max, | |
| 326 | member(branch_and_bound,Options),!,format('B~w',[Max]),fail. | |
| 327 | increase_core_counter(Cur,_,C1) :- C1 is Cur+1. | |
| 328 | ||
| 329 | reset_max_core_size :- retractall(max_core_size(_)). | |
| 330 | set_max_core_size(Max) :- retractall(max_core_size(_)), assertz(max_core_size(Max)). | |
| 331 | ||
| 332 | % check if an optional hypothesis in the current core is implied by the rest and the new hyp C | |
| 333 | %implies_optional_hyp(C,CurrentCore,Hyp) :- | |
| 334 | % \+ is_truth(CurrentCore), | |
| 335 | % select(Hyp,CurrentCore,Rest), % DO THIS TEST also for C which must be kept | |
| 336 | % bsyntaxtree:get_texpr_info(Hyp,IL), member(optionally_in_core,IL), | |
| 337 | % % print(' --> '),translate:print_bexpr(Hyp), print(' <== '),translate:print_bexpr(Rest),nl, | |
| 338 | % prove_sequent(animation,Hyp,[C|Rest]). | |
| 339 | % | |
| 340 | %:- use_module(wdsrc(well_def_analyser),[prove_sequent/3]). | |
| 341 | %implied_by_core(C,CurrentCore) :- prove_sequent(animation,C,CurrentCore). | |
| 342 | ||
| 343 | ||
| 344 | add_uc_info(SolverRes, C, IC2) :- | |
| 345 | ( ( ground(SolverRes), | |
| 346 | SolverRes = solution(_), Labels = [], | |
| 347 | UCInfo = [description('definitely in unsat core (solution)')]) | |
| 348 | ; ( SolverRes == error, Labels = ['WD'], | |
| 349 | UCInfo = [description('definitely in unsat core (kept to prevent WD error)')]) | |
| 350 | ; ( SolverRes == time_out, Labels = ['TO'], % pretty printed as @TO | |
| 351 | UCInfo = [description('possibly in unsat core (kept to prevent timeout)')]) | |
| 352 | ; ( ground(SolverRes), Labels = ['VTO'], | |
| 353 | SolverRes = no_solution_found(enumeration_warning(_,_,_,_,_)), | |
| 354 | UCInfo = [description('possibly in unsat core (kept to prevent virtual timeout)')]) | |
| 355 | ; ( SolverRes == no_solution_found(unfixed_deferred_sets), Labels = ['DEFSETS'], | |
| 356 | UCInfo = [description('definitely in unsat core (kept to fix deferred sets)')]) | |
| 357 | ; ( ground(SolverRes), Labels = ['UNKNOWN'], | |
| 358 | SolverRes = no_solution_found(_), | |
| 359 | UCInfo = [description('possibly in unsat core (kept to prevent unknown solver result)')]) | |
| 360 | ), !, | |
| 361 | add_texpr_infos(C, UCInfo, IC1), | |
| 362 | add_labels_to_texpr(IC1,Labels,IC2). | |
| 363 | ||
| 364 | uc_label('WD'). | |
| 365 | uc_label('TO'). | |
| 366 | uc_label('VTO'). | |
| 367 | uc_label('DEFSETS'). | |
| 368 | ||
| 369 | pred_has_unsat_core_label(Pred,Label) :- get_texpr_label(Pred,Label), uc_label(Label). | |
| 370 | ||
| 371 | solution_found(Res) :- | |
| 372 | Res \= contradiction_found, | |
| 373 | Res \= no_solution_found(_), | |
| 374 | Res \= time_out, | |
| 375 | Res \= error, | |
| 376 | Res \= clpfd_overflow. | |
| 377 | ||
| 378 | % check if a removed conjunct has to be kept in unsat core given solver_result (w/o conjunct) and global result | |
| 379 | % possible value solution(_), contradiction_found, no_solution_found, ... | |
| 380 | must_keep_conjunct(solution(_),_,_) :- !. | |
| 381 | must_keep_conjunct(X,X,_) :- !,fail. % same result as global result, e.g., WD error or time_out | |
| 382 | must_keep_conjunct(_,_,Options) :- member(keep_exact_result,Options),!. | |
| 383 | must_keep_conjunct(contradiction_found,_,_) :- !,fail. % | |
| 384 | must_keep_conjunct(no_solution_found(X),GlobalRes,_) :- !, | |
| 385 | must_keep_no_sol_found(X,GlobalRes). | |
| 386 | must_keep_conjunct(_,_,_). | |
| 387 | ||
| 388 | must_keep_no_sol_found(enumeration_warning(_,_,_,_,critical),_). | |
| 389 | % relevant for e.g. :core f={1|->1} & x:dom(f) & f(x)>1 with -p TRY_FIND_ABORT TRUE | |
| 390 | must_keep_no_sol_found(solver_answered_unknown,_Global). % Global typically contradiction_found | |
| 391 | % TODO: look if there are other reasons where we should keep the conjunct | |
| 392 | ||
| 393 | can_be_further_decomposed(TE,A,B) :- can_be_further_decomposed(TE,positive,A,B). | |
| 394 | can_be_further_decomposed(b(E,pred,Info),NegPos,A,B) :- can_be_further_decomposed_aux(E,Info,NegPos,A,B). | |
| 395 | can_be_further_decomposed_aux(conjunct(A,B),_,positive,A,B). | |
| 396 | can_be_further_decomposed_aux(disjunct(A,B),_,negative,A,B). | |
| 397 | can_be_further_decomposed_aux(disjunct(A,B),_,positive,D1,D2) :- | |
| 398 | get_preference(unsat_core_algorithm,linear_greedy_decompose),!, % can blow up number of cases | |
| 399 | (can_be_further_decomposed(A,positive,A1,A2) % here we could try divide conjuncts in middle | |
| 400 | -> disjunct_predicates([A1,B],D1), | |
| 401 | disjunct_predicates([A2,B],D2) | |
| 402 | ; can_be_further_decomposed(B,positive,B1,B2) | |
| 403 | -> disjunct_predicates([A,B1],D1), | |
| 404 | disjunct_predicates([A,B2],D2) | |
| 405 | ). | |
| 406 | % above rule works for :core ((x=2&y=3) or (x=1&z=3)) & x>2 | |
| 407 | % for :core ((x=2 & y=3) or (x=3 & y=4)) & x>3 it sort of works but keeps both x/y | |
| 408 | can_be_further_decomposed_aux(implication(A,B),_,positive,I1,I2) :- | |
| 409 | (can_be_further_decomposed(B,positive,B1,B2) % A=>B1&B2 <--> A=>B1 & A=>B2 | |
| 410 | -> create_implication(A,B1,I1), | |
| 411 | create_implication(A,B2,I2) | |
| 412 | ; can_be_further_decomposed(A,negative,A1,A2) % (A1 or A2) => B <--> A1 => B & A2 => B | |
| 413 | -> create_implication(A1,B,I1), | |
| 414 | create_implication(A2,B,I2)). | |
| 415 | can_be_further_decomposed_aux(implication(A,B),_,negative,NA,B) :- % A=>B <--> not(A) or B | |
| 416 | create_negation(A,NA). | |
| 417 | can_be_further_decomposed_aux(negation(D),_,NegPos,NA,NB) :- neg_context(NegPos,PosNeg), | |
| 418 | can_be_further_decomposed(D,PosNeg,A,B), % not(A &/or B) <--> not(A) or/& not(B) | |
| 419 | create_negation(A,NA), | |
| 420 | create_negation(B,NB). | |
| 421 | can_be_further_decomposed_aux(let_predicate(V,E,P),Info,NegPos,LEA,LEB) :- | |
| 422 | can_be_further_decomposed(P,NegPos,A,B), | |
| 423 | LEA = b(let_predicate(V,E,A),pred,Info), % used_ids could be wrong; TO DO: think about exists | |
| 424 | LEB = b(let_predicate(V,E,B),pred,Info). | |
| 425 | can_be_further_decomposed_aux(lazy_let_pred(V,E,P),Info,NegPos,LEA,LEB) :- | |
| 426 | can_be_further_decomposed(P,NegPos,A,B), | |
| 427 | LEA = b(lazy_let_pred(V,E,A),pred,Info), | |
| 428 | LEB = b(lazy_let_pred(V,E,B),pred,Info). | |
| 429 | ||
| 430 | neg_context(positive,negative). neg_context(negative,positive). | |
| 431 | ||
| 432 | % a binary search algorithm in order to only need log(n) instead of n solver calls | |
| 433 | % Idea: split list of conjuncts in half, C = [A,B] | |
| 434 | unsat_core_fixed_conjuncts_lists_divide_and_conquer([],_,_,_,_) :- !, fail. % we split too far! | |
| 435 | unsat_core_fixed_conjuncts_lists_divide_and_conquer([C],_FixedConjuncts,_GlobalResult,_Options,[C]) :- | |
| 436 | !. % if there is only one conjunct left, it has to belong to the core | |
| 437 | unsat_core_fixed_conjuncts_lists_divide_and_conquer(Clauses,FixedConjuncts,GlobalResult,Options,Core) :- | |
| 438 | split_in_half(Clauses,A,B), | |
| 439 | % print('SPLIT: '), print(A),nl,print(B),nl, | |
| 440 | unsat_core_fixed_conjuncts_lists_divide_and_conquer_split(A,B,FixedConjuncts,GlobalResult,Options,Core). | |
| 441 | ||
| 442 | unsat_core_fixed_conjuncts_lists_divide_and_conquer_split(A,B,FixedConjuncts,GlobalResult,Options,Core) :- | |
| 443 | append(A,FixedConjuncts,AllConjuncts), | |
| 444 | conjunct_predicates(AllConjuncts,APred), | |
| 445 | % print('SOLVING LHS: '), translate:print_bexpr(APred),nl, | |
| 446 | solve_core_pred(APred, 1, Options, ARealRes), | |
| 447 | progress_info(ARealRes), | |
| 448 | % print(result(ARealRes)),nl, | |
| 449 | !, % do not backtrack into solving or multiple results can be found leading to duplicated cores | |
| 450 | unsat_core_fixed_conjuncts_lists_divide_and_conquer_recur1(ARealRes,A,B,FixedConjuncts,GlobalResult,Options,Core). | |
| 451 | ||
| 452 | progress_info(ARes) :- progress_info_aux(ARes),!,flush_output(user_output). | |
| 453 | progress_info_aux(time_out) :- progress_print('T'). | |
| 454 | progress_info_aux(error) :- progress_print('WD'). | |
| 455 | progress_info_aux(no_solution_found(E)) :- progress_info_no_sol_found_aux(E). | |
| 456 | progress_info_aux(contradiction_found) :- progress_print('-'). | |
| 457 | progress_info_aux(translation_or_setup_failed) :- progress_print('FAILED'). % Z3 or cvc4 translation failed | |
| 458 | progress_info_aux(solution(_)) :- progress_print('+'). | |
| 459 | progress_info_aux(clpfd_overflow) :- progress_print('O'). | |
| 460 | progress_info_aux(UNKNOWN) :- debug_format(5, '*~w*', [UNKNOWN]). | |
| 461 | ||
| 462 | %progress_print(C) :- !, write(C). | |
| 463 | progress_print(C) :- debug_print(C). | |
| 464 | ||
| 465 | progress_info_no_sol_found_aux(unfixed_deferred_sets) :- progress_print('-'). | |
| 466 | progress_info_no_sol_found_aux(solver_answered_unknown) :- progress_print('U'). | |
| 467 | progress_info_no_sol_found_aux(enumeration_warning(_,_,_,_,_)) :- progress_print('U(ENUM)'). | |
| 468 | progress_info_no_sol_found_aux(UNKNOWN) :- debug_format(5, '*~w*', [UNKNOWN]). | |
| 469 | ||
| 470 | explain_result(time_out,'UNKNOWN (TIME_OUT)'). | |
| 471 | explain_result(error,'UNKNOWN (ERROR)'). | |
| 472 | explain_result(clpfd_overflow,'UNKNOWN (CLPFD OVERFLOW)'). | |
| 473 | explain_result(no_solution_found(E),R) :- explain_no_sol(E,R). | |
| 474 | explain_result(contradiction_found,'FALSE'). | |
| 475 | explain_result(solution(_),'TRUE'). | |
| 476 | explain_result(_,'UNKNOWN'). | |
| 477 | ||
| 478 | explain_no_sol(solver_answered_unknown, 'UNKNOWN'). | |
| 479 | explain_no_sol(unfixed_deferred_sets,'FALSE (DEFERRED SETS)'). | |
| 480 | explain_no_sol(enumeration_warning(_,_,_,_,_), 'UNKNOWN (ENUMERATION WARNING)'). | |
| 481 | explain_no_sol(_, 'UNKNOWN'). | |
| 482 | ||
| 483 | definite_prob_result(solution(_),_). | |
| 484 | definite_prob_result(Res,Options) :- contradiction_result(Res,Options). | |
| 485 | ||
| 486 | solve_core_pred(BPred,_TOFactor,Options,Res) :- % translate:print_bexpr(BPred),nl, | |
| 487 | memberchk(try_prob_solver_first(TimeoutFactor),Options), | |
| 488 | solve_predicate(BPred,_State,TimeoutFactor,Res), | |
| 489 | formatsilent('ProB solve_predicate result : ~w~n',[Res]), | |
| 490 | definite_prob_result(Res,Options), !. | |
| 491 | solve_core_pred(BPred,TOFactor,Options,Res) :- % print(' --> Z3 SOLVE: '), translate:print_bexpr(BPred),nl, | |
| 492 | member(use_smt_solver(Solver),Options),!, | |
| 493 | Opts = [smt_time_out_factor(TOFactor), check_sat_skeleton(10), instantiate_quantifier_limit(5)], | |
| 494 | %formatsilent('Starting SMT solver ~w with ~w~n',[Solver,Opts]), | |
| 495 | smt_solve_predicate(Solver,Opts,BPred,_,Res), | |
| 496 | formatsilent('~w solve_predicate result : ~w~n',[Solver,Res]). | |
| 497 | solve_core_pred(BPred,_TOFactor,Options,Res) :- | |
| 498 | member(use_cdclt_solver,Options),!, % TODO: pass TOFactor to cdclt | |
| 499 | (cdclt_solve_predicate(BPred,_,Res) -> true | |
| 500 | ; Res= contradiction_found, | |
| 501 | add_internal_error('Solver call failed:',cdclt_solve_predicate(BPred,_,Res)) | |
| 502 | ). | |
| 503 | % TODO: add wd-prover | |
| 504 | solve_core_pred(BPred,TOFactor,Options,Res) :- | |
| 505 | (member(use_smt_mode/SMT,Options) -> true ; SMT=true), | |
| 506 | (member(use_clpfd_solver/CLPFD,Options) -> true ; CLPFD=true), | |
| 507 | (member(use_chr_solver/CHR,Options) -> T=[use_chr_solver/CHR] ; T=[]), | |
| 508 | solve_predicate(BPred,_BState,TOFactor,[use_smt_mode/SMT,use_clpfd_solver/CLPFD,ignore_wd_errors|T],Res). | |
| 509 | ||
| 510 | ||
| 511 | unsat_core_fixed_conjuncts_lists_divide_and_conquer_recur1(ARealRes,A,_B,FixedConjuncts,GlobalResult,Options,Core) :- | |
| 512 | \+ must_keep_conjunct(ARealRes,GlobalResult,[]), % A is (virtually / effectively) unsat. Recur on A. | |
| 513 | unsat_core_fixed_conjuncts_lists_divide_and_conquer(A,FixedConjuncts,GlobalResult,Options,Core). | |
| 514 | unsat_core_fixed_conjuncts_lists_divide_and_conquer_recur1(ARealRes,A,B,FixedConjuncts,GlobalResult,Options,Core) :- | |
| 515 | append(B,FixedConjuncts,AllConjuncts), | |
| 516 | conjunct_predicates(AllConjuncts,BPred), | |
| 517 | % print('SOLVING RHS: '), translate:print_bexpr(BPred),nl, | |
| 518 | solve_core_pred(BPred,1,Options,BRealRes), | |
| 519 | progress_info(BRealRes), | |
| 520 | % print(result(BRealRes)),nl, | |
| 521 | !, | |
| 522 | unsat_core_fixed_conjuncts_lists_divide_and_conquer_recur2(ARealRes,BRealRes,A,B,FixedConjuncts,GlobalResult,Options,Core). | |
| 523 | ||
| 524 | unsat_core_fixed_conjuncts_lists_divide_and_conquer_recur2(_ARealRes,BRealRes,_A,B,FixedConjuncts,GlobalResult,Options,Core) :- | |
| 525 | \+ must_keep_conjunct(BRealRes,GlobalResult,[]), % B is (virtually / effectively) unsat. Recur on B. | |
| 526 | !, | |
| 527 | unsat_core_fixed_conjuncts_lists_divide_and_conquer(B,FixedConjuncts,GlobalResult,Options,Core). | |
| 528 | unsat_core_fixed_conjuncts_lists_divide_and_conquer_recur2(ARealRes,BRealRes,A,B,FixedConjuncts,GlobalResult,Options,Core) :- | |
| 529 | % the interesting case: if both are sat | |
| 530 | must_keep_conjunct(ARealRes,GlobalResult,[]), | |
| 531 | must_keep_conjunct(BRealRes,GlobalResult,[]), | |
| 532 | % minimize A assuming usat core includes B | |
| 533 | append(B,FixedConjuncts,FixedAndB), | |
| 534 | unsat_core_fixed_conjuncts_lists_divide_and_conquer(A,FixedAndB,GlobalResult,Options,ACore), | |
| 535 | % now ACore & B is unsat and minimal but not minimum core | |
| 536 | % minimize B assuming ACore | |
| 537 | append(ACore,FixedConjuncts,FixedAndA), | |
| 538 | unsat_core_fixed_conjuncts_lists_divide_and_conquer(B,FixedAndA,GlobalResult,Options,BCore), | |
| 539 | append(ACore,BCore,Core). | |
| 540 | ||
| 541 | %divide_and_conquer_recur_condition(contradiction_found). | |
| 542 | %divide_and_conquer_recur_condition(no_solution_found(X)) :- | |
| 543 | % % to do: if the outermost conjunct already generates a time_out or critical enumeration warning then this should be enabled as a recur condition | |
| 544 | % X \= enumeration_warning(_,_,_,_,critical). | |
| 545 | %%divide_and_conquer_recur_condition(time_out). | |
| 546 | ||
| 547 | split_in_half(C, A, B) :- | |
| 548 | length(C,L), | |
| 549 | Half is L // 2, | |
| 550 | length(A, Half), | |
| 551 | append(A, B, C). | |
| 552 | ||
| 553 | % there is currently no known good algorithm to compute the minimum unsat core | |
| 554 | % we can just compute every core and take the minimum one out of the list | |
| 555 | :- assert_must_succeed((minimum_unsat_core(b(conjunct(b(falsity,pred,[]), | |
| 556 | 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), | |
| 557 | (ground(Core), Core = b(falsity,pred,_)))). | |
| 558 | minimum_unsat_core(Predicate,CorePredicate) :- | |
| 559 | minimum_unsat_core_with_fixed_conjuncts(Predicate,[],CorePredicate). | |
| 560 | ||
| 561 | minimum_unsat_core_with_fixed_conjuncts(Predicate,FixedConjuncts,CorePredicate) :- | |
| 562 | Options = [branch_and_bound,fixed_conjuncts(FixedConjuncts)], | |
| 563 | findall(CoreList, | |
| 564 | unsat_core_list(Predicate,Options,no_solution_found,CoreList), | |
| 565 | Cores), | |
| 566 | reset_max_core_size, | |
| 567 | min_member(compare_length,MinCs,Cores), | |
| 568 | conjunct_predicates(MinCs,CorePredicate). | |
| 569 | ||
| 570 | compare_length(P1,P2) :- length(P1,L1), length(P2,L2), | |
| 571 | (L1<L2 -> true | |
| 572 | ; L1=L2 -> | |
| 573 | term_size(P1, T1), | |
| 574 | term_size(P2, T2), | |
| 575 | T1 < T2 | |
| 576 | ). | |
| 577 | ||
| 578 | % ---------------------------------- | |
| 579 | ||
| 580 | % quick_bup_core | |
| 581 | ||
| 582 | % finding small unsat cores bottom-up by looking for 1, 2, ... conjuncts and looking for contradiction_found | |
| 583 | % useful e.g. for Z3 where some conjuncts are complex and lead to time outs or translation failed errors | |
| 584 | % could also be used with WD prover instead or in addition to Z3 | |
| 585 | % currently cannot be used to find unsat core for timeout or unknown result | |
| 586 | % useful as a "canary" for PROPERTIES/axioms as a quick check or as additional quick check | |
| 587 | ||
| 588 | ||
| 589 | preprocess_conjuncts([],_,_,[]). | |
| 590 | preprocess_conjuncts([Conj|T],Nr,Options,ListResult) :- | |
| 591 | format(' ==> Pre-processing conjunct ~w and checking for individual inconsistency~n',[Nr]), | |
| 592 | %translate:print_bexpr(Conj),nl, | |
| 593 | % we could =remove try_prob_solver_first(_) from Options, if we want to filter non-translatable conjuncts! | |
| 594 | solve_core_pred(Conj, 0.02, Options, Res), | |
| 595 | (explain_result(Res,Expl) -> debug_format(19,'Result for conjunct ~w: ~w (~w)~n',[Nr,Expl,Res])), | |
| 596 | N1 is Nr+1, | |
| 597 | (should_remove_conjunct(Res) | |
| 598 | -> % remove this conjunct; it can only disturb finding a core for a contradiction | |
| 599 | preprocess_conjuncts(T,N1,Options,ListResult) | |
| 600 | ; find_identifier_uses(Conj,[],UsedIds), | |
| 601 | ListResult = [conj(Nr,Conj,Res,UsedIds)|PT], | |
| 602 | (contradiction_result(Res,Options) | |
| 603 | -> PT=[] % stop processing, we have found an unsat core of a single conjunct | |
| 604 | ; preprocess_conjuncts(T,N1,Options,PT)) | |
| 605 | ). | |
| 606 | ||
| 607 | should_remove_conjunct(no_solution_found(translation_failed)). | |
| 608 | ||
| 609 | contradiction_result(contradiction_found,_). | |
| 610 | contradiction_result(no_solution_found(unfixed_deferred_sets),Options) :- | |
| 611 | member(allow_unfixed_deferred_sets,Options). | |
| 612 | ||
| 613 | quick_bup_core_up_to(Typed,MaxSize,CoreList,Result) :- | |
| 614 | quick_bup_core(Typed,[use_smt_solver(z3axm), | |
| 615 | maximum_core_size(MaxSize), | |
| 616 | try_prob_solver_first(fixed_time_out(5))], | |
| 617 | CoreList,Result). | |
| 618 | ||
| 619 | quick_bup_core(Predicate,Options,CoreList,Result) :- | |
| 620 | uc_conjunction_to_list(Predicate,Options,List), | |
| 621 | preprocess_conjuncts(List,1,Options,ProcessedList), | |
| 622 | (last(ProcessedList,conj(_,Last,LR,_)), | |
| 623 | contradiction_result(LR,Options) | |
| 624 | -> CoreList = [Last], Result=LR | |
| 625 | ; (member(maximum_core_size(MaxN),Options) -> true ; MaxN=3), | |
| 626 | between(2,MaxN,N), | |
| 627 | format(' ==> Finding cores of length ~w~n',[N]), | |
| 628 | contradiction_check(N,ProcessedList,Options,CoreList,Result) -> true | |
| 629 | ). | |
| 630 | ||
| 631 | ||
| 632 | ||
| 633 | select_core_target(N,List,Res) :- | |
| 634 | append(_,[conj(Nr,ConjN,_,UsedIdsN)|Rest],List), % now only use conjuncts to the right of ConjN | |
| 635 | format(' ==> finding (~w-ary) conflicts with conjunct ~w: ',[N,Nr]),translate:print_bexpr(ConjN),nl, | |
| 636 | N1 is N-1, | |
| 637 | select_core_target(N1,Rest,[ConjN],UsedIdsN,Res). | |
| 638 | ||
| 639 | has_common_ids(UsedIdsSoFar,conj(_,_,_,UsedIdsN)) :- ord_intersect(UsedIdsSoFar,UsedIdsN). | |
| 640 | ||
| 641 | % select a core target list of predicates of length N | |
| 642 | % TODO: this can still generate the same conjunct multiple times?? | |
| 643 | select_core_target(0,_,Core,_,Res) :- !, Res=Core. | |
| 644 | select_core_target(N,List,CoreSoFar,UsedIdsSoFar,Res) :- %print(n(N,UsedIdsSoFar)),nl, | |
| 645 | split_list(has_common_ids(UsedIdsSoFar),List,CommonList,DisjList), | |
| 646 | append(_,[conj(_Nr,ConjN,_,UsedIdsN)|Rest],CommonList), % only choose conjuncts with common ids larger than Nr | |
| 647 | %print(selected_conj(_Nr)),nl, translate:print_bexpr(ConjN),nl, | |
| 648 | append(Rest,DisjList,RestList), | |
| 649 | ord_union(UsedIdsN,UsedIdsSoFar,New), | |
| 650 | N1 is N-1, | |
| 651 | select_core_target(N1,RestList,[ConjN|CoreSoFar],New,Res). | |
| 652 | ||
| 653 | contradiction_check(N,ProcessedList,Options,CoreList,Res) :- | |
| 654 | select_core_target(N,ProcessedList,CoreList), | |
| 655 | conjunct_predicates(CoreList,Core), | |
| 656 | %nl,translate:print_bexpr(Core),nl,nl, | |
| 657 | solve_core_pred(Core, 0.02, Options, Res), | |
| 658 | progress_info(Res), | |
| 659 | contradiction_result(Res,Options). | |
| 660 | ||
| 661 | % could use WD prover as additional task: | |
| 662 | % >>> :prove x:NATURAL --> NATURAL => not(-1:ran(x)) | |
| 663 | % Universally quantified predicate is PROVED with [prob-wd-prover(no_double_check)] | |
| 664 | ||
| 665 | % example where we need three conjuncts: :z3-axm-qcore x<y & y<10 & x<10 & y+n<x & n=0 |