1 | % (c) 2014-2022 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 | :- module(unsat_core_generalization,[unsat_core_generalization/8]). | |
6 | ||
7 | :- use_module(probsrc(module_information)). | |
8 | :- module_info(group,symbolic_model_checker). | |
9 | :- module_info(description,'Counter example generalization based on unsat cores.'). | |
10 | ||
11 | :- use_module(library(heaps), [add_to_heap/4]). | |
12 | ||
13 | :- use_module(extrasrc(unsat_cores), [unsat_core_with_fixed_conjuncts/3]). | |
14 | :- use_module(probsrc(translate), [translate_bexpression/2]). | |
15 | ||
16 | :- use_module(probsrc(bsyntaxtree), [conjunct_predicates/2, | |
17 | create_negation/2]). | |
18 | :- use_module(probsrc(translate), [translate_bexpression/2]). | |
19 | :- use_module(probsrc(error_manager), [add_error/2]). | |
20 | ||
21 | :- use_module(symbolic_model_checker(predicate_handling)). | |
22 | :- use_module(symbolic_model_checker(solver_handling)). | |
23 | ||
24 | % inspired by "efficient implementation of property directed reachability" | |
25 | % see ic3 reference implementation | |
26 | % s state to lift, primary inputs i, T transition relation, t successor | |
27 | % => s & i & T & not t' is unsat | |
28 | % extract core to find generalization | |
29 | % currently, non-determinism in the transitions might render the predicate sat | |
30 | % hence, no core can be extracted in that case | |
31 | % the inputs should be used to make it deterministic! | |
32 | unsat_core_generalization(TransitionPredicate,HIn,N,Frames,State,Inputs,[SuccState|SuccStates],HOut) :- | |
33 | in_solver_on_level(N,Frames,IS), | |
34 | unsat_core_generalization_aux(TransitionPredicate,IS,State,Inputs,SuccState,Core), !, | |
35 | add_to_heap(HIn,N,obligation(Core,TransitionPredicate,Inputs,[SuccState|SuccStates]),HOut). | |
36 | ||
37 | unsat_core_generalization_aux(TransitionPredicate,IS,State,Inputs,SuccState,Core) :- | |
38 | prime_predicate(SuccState,TPrime), | |
39 | create_negation(TPrime,NotTPrime), | |
40 | conjunct_predicates([NotTPrime,Inputs,TransitionPredicate|IS],Conjunction), | |
41 | ||
42 | % verify that the query is actually unsat | |
43 | conjunct_predicates([State,Conjunction],VerifyQuery), | |
44 | solve(VerifyQuery,Result), | |
45 | Result = contradiction_found(_), !, | |
46 | ||
47 | %debug output | |
48 | translate_bexpression(Conjunction,PPConj), | |
49 | translate_bexpression(State,PPState), | |
50 | translate_bexpression(Inputs,PPInputs), | |
51 | format('unsat core generalization: generalizing~n~w~nby computing unsat core of it with fixed conjuncts~n~w~nand inputs~n~w~n.',[PPState,PPConj,PPInputs]), | |
52 | ||
53 | % the unsat core is a lifting to a partial assignment | |
54 | unsat_core_with_fixed_conjuncts(State,Conjunction,Core), | |
55 | translate_bexpression(Core,PPCore), | |
56 | format('unsat core is~n~w~n',[PPCore]). | |
57 | unsat_core_generalization_aux(_TP,_IS,State,_Inputs,_SuccState,Core) :- | |
58 | add_error(unsat_core_generalization, 'unsat core generalization failed. query is not unsat!'), | |
59 | Core = State. |