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.