-
Notifications
You must be signed in to change notification settings - Fork 4
/
Copy pathfc.pro
221 lines (178 loc) · 6.37 KB
/
fc.pro
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
:-include('third_party/fCube-4.1/fCube/fCube').
%:-include('../SOFTWARE/PROVERS/fCube-11.1/fCube/fCube').
fcube(A):-toPrefix(A,X),fc(X).
fc(X):-intDecide0(X,_). % edit here for other version
%for version 4.1
intDecide0(X,COUNTERMODEL):-
permanenzaSegno([swff(f,X)],StartingSet),
orderEquivSet(StartingSet, OrderedStartingSet),
reapply(OrderedStartingSet, COUNTERMODEL, 1, 1),!,fail.
intDecide0(_,[valida]).
% for version 11
intDecide1(X,[]):-
permanenzaSegno([swff(f,X)],StartingSet, _),
orderEquivSet(StartingSet, OrderedStartingSet),
reapply(OrderedStartingSet, _, 1, 1),
!,fail.
intDecide1(_,[valida]).
notfc:-T0=(p <-> ~q)<-> (~q <-> p),ppp(T),
mints(T0,T),ppp(T),faprove(T),dprove(T).
fcbug:-T0=(p <-> ~q)<-> (~q <-> p),fsize(T0,S0),
fcube(T0),ppp(should_be_true(S0,T0)),nl,
mints(T0,T),fsize(T,S),
ppp(trying_equivalent(S)=T),
fcube(T).
fcbug1:-
T0=((p <-> ~q)-> (~q -> p)),
fcube(T0),ppp(should_be_true(T0)),
mints(T0,T),
ppp(trying_equivalent=T),
fcube(T).
fcbug2:-
T0=((~p <-> q)-> (q -> ~p)),
mints(T0,T),
fcube(T0),ppp(should_be_true(T0)),
ppp(trying_equivalent=T),
fcube(T).
fcbugs:-fcbugs(5).
mints_fcube(A):-mints(A,MA),fcube(MA).
fcbugs(N):-
do((
gold_eq_neg_test(N,mints_fcube,Culprit,Unexpected),ppp([Unexpected,Culprit])
)).
mints_dprove(A):-mints(A,MA),dprove(MA).
mints_faprove(A):-mints(A,MA),faprove(MA).
mints_coprove(A):-mints(A,MA),coprove(MA).
mints_eprove(A):-mints(A,MA),eprove(MA).
mints_impl_taut(N,T,MT):-implTaut(N,T),mints(T,MT).
alt_impl_taut(N,T,AT):-implTaut(N,T),toDisjBiCond(T,AT).
small_taut_bug(M,Prover):-
do((
between(0,M,N),
mints_impl_taut(N,T,MT),
\+ call(Prover,MT),
ppp(unexpected_failure_on),
ppp(T),
ppp((<=>)),
ppp(MT),nl
)).
alt_small_taut_bug(M,Prover):-
do((
between(0,M,N),
alt_impl_taut(N,T,MT),
ppp(trying=T),
ppp(as=MT),
\+ call(Prover,MT),
ppp(unexpected_failure_on),
ppp(T),
ppp((<=>)),
ppp(MT),nl
)).
dnobugs(N):-
do((
gold_eq_neg_test(N,mints_dprove,Culprit,Unexpected),ppp([Unexpected,Culprit])
)).
smallfcbugs:-ppp(fcube_at_4_bugs),
do((
between(0,4,N),gold_imp_test(N,mints_fcube,C,U),
ppp([N,U,C]),
mints(C,MC),fsize(MC,S),
ppp(culprit_size(S)=MC),nl
)).
nosmallbugs:-ppp(eprove_up_to_5_ok),
do((
between(0,5,N),gold_imp_test(N,mints_eprove,C,U),
ppp([N,U,C]),
mints(C,MC),fsize(MC,S),
ppp(culprit_size(S)=MC),nl
)).
/*
?- smallfcbugs.
fcube_at_4_bugs
[4,wrong_failure,(0->1->2->2->0)]
culprit_size(24)=((nv1->0->nv2)->(nv2->1->nv3)->(nv3->2->nv4)->(nv4->2->0)->((0->nv2)->nv1)->((1->nv3)->nv2)->((2->0)->nv4)->((2->nv4)->nv3)->nv1)
[4,wrong_failure,(0->1->2->3->0)]
culprit_size(24)=((nv1->0->nv2)->(nv2->1->nv3)->(nv3->2->nv4)->(nv4->3->0)->((0->nv2)->nv1)->((1->nv3)->nv2)->((2->nv4)->nv3)->((3->0)->nv4)->nv1)
[4,wrong_failure,(0->(1->2->0)->0)]
culprit_size(24)=((nv1->0->nv2)->(nv2->nv3->0)->(nv3->1->nv4)->(nv4->2->0)->((0->nv2)->nv1)->((1->nv4)->nv3)->((2->0)->nv4)->((nv3->0)->nv2)->nv1)
[4,wrong_failure,(0->(1->0->2)->0)]
culprit_size(24)=((nv1->0->nv2)->(nv2->nv3->0)->(nv3->1->nv4)->(nv4->0->2)->((0->2)->nv4)->((0->nv2)->nv1)->((1->nv4)->nv3)->((nv3->0)->nv2)->nv1)
[4,wrong_failure,(0->(1->2->3)->0)]
culprit_size(24)=((nv1->0->nv2)->(nv2->nv3->0)->(nv3->1->nv4)->(nv4->2->3)->((0->nv2)->nv1)->((1->nv4)->nv3)->((2->3)->nv4)->((nv3->0)->nv2)->nv1)
true.
?- fcbugs(5).
[wrong_failure,~ (0<->(1<-> ~ (1<->0)))]
[wrong_failure,~ (0<->(1<-> ~ (0<->1)))]
[wrong_failure,~ (0<->(1<->(0<-> ~1)))]
[wrong_failure,~ (0<->(0<->(1<-> ~1)))]
[wrong_failure,~ (0<->(1<->(~1<->0)))]
[wrong_failure,~ (0<->(0<->(~1<->1)))]
[wrong_failure,~ (0<->(~ (1<->0)<->1))]
[wrong_failure,~ (0<->(~ (0<->1)<->1))]
[wrong_failure,~ (0<->((1<-> ~1)<->0))]
[wrong_failure,~ (0<->((0<-> ~1)<->1))]
[wrong_failure,~ (0<->((~1<->1)<->0))]
[wrong_failure,~ (0<->((~1<->0)<->1))]
[wrong_failure,~0<->(1<->(1<-> ~0))]
[wrong_failure,~0<->(1<->(~0<->1))]
[wrong_failure,~0<->(~1<->(1<->0))]
[wrong_failure,~0<->(~1<->(0<->1))]
[wrong_failure,~0<->((1<->0)<-> ~1)]
[wrong_failure,~0<->((0<->1)<-> ~1)]
[wrong_failure,~0<->((1<-> ~0)<->1)]
[wrong_failure,~0<->((~0<->1)<->1)]
[wrong_failure,~ ((0<->1)<->(1<-> ~0))]
[wrong_failure,~ ((0<->1)<->(0<-> ~1))]
[wrong_failure,(0<->1)<->(0<->(0<->(1<->0)))]
[wrong_failure,(0<->1)<->(1<->(1<->(1<->0)))]
[wrong_failure,(0<->1)<->(0<->(0<->(0<->1)))]
[wrong_failure,(0<->1)<->(1<->(1<->(0<->1)))]
[wrong_failure,(0<->1)<->(0<->((1<->0)<->0))]
[wrong_failure,(0<->1)<->(0<->((0<->1)<->0))]
[wrong_failure,(0<->1)<->(1<->((1<->0)<->1))]
[wrong_failure,(0<->1)<->(1<->((0<->1)<->1))]
[wrong_failure,~ ((0<->1)<->(~1<->0))]
[wrong_failure,~ ((0<->1)<->(~0<->1))]
[wrong_failure,(0<->1)<->((0<->(1<->0))<->0)]
[wrong_failure,(0<->1)<->((0<->(0<->1))<->0)]
[wrong_failure,(0<->1)<->((1<->(1<->0))<->1)]
[wrong_failure,(0<->1)<->((1<->(0<->1))<->1)]
[wrong_failure,(0<->1)<->(((1<->0)<->0)<->0)]
[wrong_failure,(0<->1)<->(((0<->1)<->0)<->0)]
[wrong_failure,(0<->1)<->(((1<->0)<->1)<->1)]
[wrong_failure,(0<->1)<->(((0<->1)<->1)<->1)]
[wrong_failure,~ ((0<-> ~1)<->(1<->0))]
[wrong_failure,~ ((0<-> ~1)<->(0<->1))]
[wrong_failure,~ ((0<-> ~ (1<->0))<->1)]
[wrong_failure,~ ((0<-> ~ (0<->1))<->1)]
[wrong_failure,~ ((0<->(1<-> ~1))<->0)]
[wrong_failure,~ ((0<->(0<-> ~1))<->1)]
[wrong_failure,(0<->(0<->(1<->0)))<->(1<->0)]
[wrong_failure,(0<->(0<->(0<->1)))<->(1<->0)]
[wrong_failure,(0<->(0<->(1<->0)))<->(0<->1)]
[wrong_failure,(0<->(0<->(0<->1)))<->(0<->1)]
[wrong_failure,~ ((0<->(~1<->1))<->0)]
[wrong_failure,~ ((0<->(~1<->0))<->1)]
[wrong_failure,(0<->((1<->0)<->0))<->(1<->0)]
[wrong_failure,(0<->((0<->1)<->0))<->(1<->0)]
[wrong_failure,(0<->((1<->0)<->0))<->(0<->1)]
[wrong_failure,(0<->((0<->1)<->0))<->(0<->1)]
[wrong_failure,~ ((~0<->1)<->(1<->0))]
[wrong_failure,~ ((~0<->1)<->(0<->1))]
[wrong_failure,~ ((~ (0<->1)<->1)<->0)]
[wrong_failure,~ ((~ (0<->1)<->0)<->1)]
[wrong_failure,~ (((0<-> ~1)<->1)<->0)]
[wrong_failure,~ (((0<-> ~1)<->0)<->1)]
[wrong_failure,~ (((0<-> ~0)<->1)<->1)]
[wrong_failure,((0<->(1<->0))<->0)<->(1<->0)]
[wrong_failure,((0<->(0<->1))<->0)<->(1<->0)]
[wrong_failure,((0<->(1<->0))<->0)<->(0<->1)]
[wrong_failure,((0<->(0<->1))<->0)<->(0<->1)]
[wrong_failure,~ (((~0<->0)<->1)<->1)]
[wrong_failure,(((0<->1)<->0)<->0)<->(1<->0)]
[wrong_failure,(((0<->1)<->1)<->1)<->(1<->0)]
[wrong_failure,(((0<->1)<->0)<->0)<->(0<->1)]
[wrong_failure,(((0<->1)<->1)<->1)<->(0<->1)]
true.
?-
*/