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(mic_generation,[down/4,ctgDown/6]).
6
7 :- use_module(probsrc(module_information)).
8 :- module_info(group,symbolic_model_checker).
9 :- module_info(description,'Generation of minimal inductive (sub-)clauses.').
10
11 :- use_module(library(ordsets)).
12 :- use_module(library(lists)).
13
14 :- use_module(probsrc(bsyntaxtree), [conjunct_predicates/2,
15 conjunction_to_list/2,
16 create_negation/2,
17 create_implication/3]).
18
19 :- use_module(symbolic_model_checker(solver_handling)).
20 :- use_module(symbolic_model_checker(predicate_handling)).
21
22 % down algorithm. see "better generalization in ic3" listing 1
23 down(Cube,I,Frames,CubeOut) :-
24 down(Cube,[],I,Frames,CubeOut).
25
26 down([],Fixed,_,_,Fixed2) :- reverse(Fixed,Fixed2). % TODO: why do i need to reverse?!
27 down([C|Cs],Fixed,I,Frames,COut) :-
28 append(Cs,Fixed,FC),
29 conjunct_predicates(FC,Q),
30 (down_aux(Q,I,Frames)
31 -> down(Cs,Fixed,I,Frames,COut)
32 ; down(Cs,[C|Fixed],I,Frames,COut)).
33
34 down_aux(Q,_I,_Frames) :-
35 % return false if I does not imply not q
36 % i.e. if there is a solution for I & q
37 initial_state(Q), !, fail.
38 down_aux(Q,I,Frames) :-
39 % F_i & not q & T => not q'
40 create_negation(Q,NegQ),
41 prime_predicate(Q,PrimedQ),
42 in_solver_on_level(I,Frames,IS),
43 get_transition_predicate(T),
44 conjunct_predicates([NegQ,PrimedQ,T|IS],Pred),
45 solve(Pred,Result),
46 Result = contradiction_found(_), !.
47 down_aux(Q,I,Frames) :-
48 % with F_i ^ not q state
49 in_solver_on_level(I,Frames,IS),
50 create_negation(Q,NegQ),
51 get_transition_predicate(T),
52 conjunct_predicates([NegQ,T|IS],Pred),
53 solve(Pred,Result),
54 Result = solution(F_iQState), !,
55 create_state_predicate(F_iQState,F_iQStatePred),
56 common_literals(Q,F_iQStatePred,NewQ),
57 down_aux(NewQ,I,Frames).
58
59 % the ctg down algorithm taken from "better generalization in IC3"
60 ctgDown(Cube,I,K,FramesIn,FramesOut,CubeOut) :-
61 % set current depth to 1
62 ctgDown(Cube,[],1,I,K,FramesIn,FramesOut,CubeOut).
63
64 ctgDown([],Fixed,_,_,_,Frames,Frames,Fixed2) :- reverse(Fixed,Fixed2). % TODO: why do i need to reverse?!
65 ctgDown([C|Cs],Fixed,CurDepth,I,K,FramesIn,FramesOut,CubeOut) :-
66 append(Cs,Fixed,FC),
67 conjunct_predicates(FC,Q),
68 (ctgDown_aux(Q,CurDepth,I,K,FramesIn,FramesT)
69 -> ctgDown(Cs,Fixed,CurDepth,I,K,FramesT,FramesOut,CubeOut)
70 ; ctgDown(Cs,[C|Fixed],CurDepth,I,K,FramesIn,FramesOut,CubeOut)).
71
72 ctgDown_aux(Q,CurDepth,I,K,FramesIn,FramesOut) :-
73 % set current counter examples to generalization counter to 0
74 ctgDown_aux(Q,CurDepth,0,I,K,FramesIn,FramesOut).
75
76 ctgDown_aux(Q,_Depth,_CTGs,_I,_K,Frames,Frames) :-
77 % as in the simple down case
78 % return false if I does not imply not q
79 % i.e. if there is a solution for I & q
80 initial_state(Q), !, fail.
81 ctgDown_aux(Q,_Depth,_CTGs,I,_K,Frames,Frames) :-
82 % again this is equivalent to the simple case
83 % return true if
84 % F_i & not q & T => not q'
85 create_negation(Q,NegQ),
86 prime_predicate(Q,PrimedQ),
87 in_solver_on_level(I,Frames,IS),
88 conjunct_predicates([NegQ,PrimedQ|IS],Pred),
89 solve(Pred,Result),
90 Result = contradiction_found(_), !.
91 ctgDown_aux(_,Depth,_,_,_,Frames,Frames) :-
92 % fail if Depth is too large (currently 2 - needs experiments)
93 Depth > 2, !, fail.
94 ctgDown_aux(Q,Depth,CTGs,I,K,FramesIn,FramesOut) :-
95 % with F_i ^ not q state
96 in_solver_on_level(I,FramesIn,IS),
97 create_negation(Q,NegQ),
98 conjunct_predicates([NegQ|IS],Pred),
99 solve(Pred,Result),
100 Result = solution(F_iQState), !,
101 create_state_predicate(F_iQState,F_iQStatePred),
102 ctgDown_aux2(F_iQStatePred,Q,Depth,CTGs,I,K,FramesIn,FramesOut).
103
104 % the if / else in line 32ff of "better generalization in IC3"
105 ctgDown_aux2(S,Q,Depth,CTGs,I,K,FramesIn,FramesOut) :-
106 % max ctgs currently 3 - needs experiments
107 CTGs < 3, I > 0,
108
109 % Init => not S
110 get_initial_state_predicate(Init),
111 conjunct_predicates([Init,S],IAndS),
112 solve(IAndS,ResultIAndS),
113 ResultIAndS = contradiction_found(_), !,
114
115 % F_i-1 & not S & T => not s'
116 create_negation(S,NegS),
117 prime_predicate(S,SPrimed),
118 IMinus1 is I - 1,
119 in_solver_on_level(IMinus1,FramesIn,F_I),
120 conjunct_predicates([NegS,SPrimed|F_I],Consecution),
121 solve(Consecution,ResultConsecution),
122 ResultConsecution = contradiction_found(_), !,
123
124 % we found a new counterexample to generalization
125 NCTGs is CTGs + 1,
126 % TODO: for loop to find J
127 create_negation(SPrimed,NegSPrimed),
128 ctgDown_aux_find_level(I,K,NegS,NegSPrimed,FramesIn,J),
129 JMinus1 is J - 1,
130 Depth2 is Depth + 1,
131 conjunction_to_list(S,SList),
132 ctgDown(SList,[],Depth2,JMinus1,K,FramesIn,FramesT,SOut),
133 % add modified not s to frames on level J and recur (while loop in paper)
134 % instead of adding not s, we add the former conjuncts and use them as disjuncts
135 add_clauses_to_level(J,FramesT,SOut,FramesTT),
136 ctgDown_aux(Q,Depth,NCTGs,I,FramesTT,FramesOut).
137
138 ctgDown_aux2(S,Q,Depth,_CTGs,I,K,FramesIn,FramesOut) :-
139 % the else branch
140 common_literals(Q,S,NewQ),
141 ctgDown_aux(NewQ,Depth,I,K,FramesIn,FramesOut).
142
143 ctgDown_aux_find_level(K,K,_,_,_,K).
144 ctgDown_aux_find_level(I,_K,NegS,NegSPrimed,Frames,J) :-
145 in_solver_on_level(I,Frames,F_I),
146 conjunct_predicates([NegS|F_I],LHS),
147 create_implication(LHS,NegSPrimed,Implies),
148 solve(Implies,Result),
149 Result = contradiction_found(_), !,
150 J = I.
151 ctgDown_aux_find_level(I,K,NegSPrimed,SPrimed,Frames,J) :-
152 I2 is I + 1,
153 ctgDown_aux_find_level(I2,K,NegSPrimed,SPrimed,Frames,J).
154
155 common_literals(Q1,Q2,CQ) :-
156 conjunction_to_list(Q1,Q1L),
157 conjunction_to_list(Q2,Q2L),
158 list_to_ord_set(Q1L,Q1S),
159 list_to_ord_set(Q2L,Q2S),
160 ord_intersection(Q1S,Q2S,CQS),
161 conjunct_predicates(CQS,CQ).